%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM621+3 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:58:04 PM UTC 2026
% Result : Theorem 52.15s 29.62s
% Output : CNFRefutation 52.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 13
% Syntax : Number of formulae : 59 ( 20 unt; 0 def)
% Number of atoms : 204 ( 34 equ)
% Maximal formula atoms : 32 ( 3 avg)
% Number of connectives : 225 ( 80 ~; 80 |; 45 &)
% ( 4 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 11 con; 0-2 aty)
% Number of variables : 58 ( 0 sgn 38 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__,conjecture,
( ( ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xn))
=> aElementOf0(X1,sdtlpdtrp0(xN,xm)) )
& aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)) )
=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(m__4660,hypothesis,
( aFunction0(xe)
& szDzozmdt0(xe) = szNzAzT0
& ! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ( aElementOf0(sdtlpdtrp0(xe,X1),sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(sdtlpdtrp0(xe,X1),X2) )
& sdtlpdtrp0(xe,X1) = szmzizndt0(sdtlpdtrp0(xN,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4660) ).
fof(m__5106,hypothesis,
( ! [X1] :
( aElementOf0(X1,xQ)
=> aElementOf0(X1,szNzAzT0) )
& aSubsetOf0(xQ,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5106) ).
fof(m__5147,hypothesis,
( aElementOf0(xp,xQ)
& ! [X1] :
( aElementOf0(X1,xQ)
=> sdtlseqdt0(xp,X1) )
& xp = szmzizndt0(xQ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5147) ).
fof(m__5309,hypothesis,
( aElementOf0(xn,szDzozmdt0(xd))
& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)
& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(xn,szNzAzT0)
& sdtlpdtrp0(xe,xn) = xp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5309) ).
fof(mSegLess,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( sdtlseqdt0(X1,X2)
<=> aSubsetOf0(slbdtrb0(X1),slbdtrb0(X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSegLess) ).
fof(m__5401,hypothesis,
! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xm))
=> sdtlseqdt0(xx,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5401) ).
fof(m__5365,hypothesis,
( aElementOf0(xx,szNzAzT0)
& ? [X1] :
( aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,X1) = xx ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5365) ).
fof(mDefSeg,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ! [X2] :
( X2 = slbdtrb0(X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElementOf0(X3,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X3),X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSeg) ).
fof(mSubASymm,axiom,
! [X1,X2] :
( ( aSet0(X1)
& aSet0(X2) )
=> ( ( aSubsetOf0(X1,X2)
& aSubsetOf0(X2,X1) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSubASymm) ).
fof(mDefSub,axiom,
! [X1] :
( aSet0(X1)
=> ! [X2] :
( aSubsetOf0(X2,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSub) ).
fof(m__5348,hypothesis,
( aElement0(xx)
& aElementOf0(xx,xQ)
& xx != szmzizndt0(xQ)
& aElementOf0(xx,xP) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5348) ).
fof(mCardSeg,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> sbrdtbr0(slbdtrb0(X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mCardSeg) ).
fof(c_0_13,negated_conjecture,
~ ( ( ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xn))
=> aElementOf0(X1,sdtlpdtrp0(xN,xm)) )
& aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)) )
=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(c_0_14,hypothesis,
! [X479,X480] :
( aFunction0(xe)
& szDzozmdt0(xe) = szNzAzT0
& ( aElementOf0(sdtlpdtrp0(xe,X479),sdtlpdtrp0(xN,X479))
| ~ aElementOf0(X479,szNzAzT0) )
& ( ~ aElementOf0(X480,sdtlpdtrp0(xN,X479))
| sdtlseqdt0(sdtlpdtrp0(xe,X479),X480)
| ~ aElementOf0(X479,szNzAzT0) )
& ( sdtlpdtrp0(xe,X479) = szmzizndt0(sdtlpdtrp0(xN,X479))
| ~ aElementOf0(X479,szNzAzT0) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__4660])])])]) ).
fof(c_0_15,hypothesis,
! [X502] :
( ( ~ aElementOf0(X502,xQ)
| aElementOf0(X502,szNzAzT0) )
& aSubsetOf0(xQ,szNzAzT0) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__5106])])]) ).
fof(c_0_16,hypothesis,
! [X505] :
( aElementOf0(xp,xQ)
& ( ~ aElementOf0(X505,xQ)
| sdtlseqdt0(xp,X505) )
& xp = szmzizndt0(xQ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__5147])])]) ).
fof(c_0_17,negated_conjecture,
! [X514] :
( ( ~ aElementOf0(X514,sdtlpdtrp0(xN,xn))
| aElementOf0(X514,sdtlpdtrp0(xN,xm)) )
& aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))
& ~ aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_13])])]) ).
cnf(c_0_18,hypothesis,
( aElementOf0(sdtlpdtrp0(xe,X1),sdtlpdtrp0(xN,X1))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
cnf(c_0_19,hypothesis,
aElementOf0(xn,szNzAzT0),
inference(split_conjunct,[status(thm)],[m__5309]) ).
cnf(c_0_20,hypothesis,
sdtlpdtrp0(xe,xn) = xp,
inference(split_conjunct,[status(thm)],[m__5309]) ).
fof(c_0_21,plain,
! [X361,X362] :
( ( ~ sdtlseqdt0(X361,X362)
| aSubsetOf0(slbdtrb0(X361),slbdtrb0(X362))
| ~ aElementOf0(X361,szNzAzT0)
| ~ aElementOf0(X362,szNzAzT0) )
& ( ~ aSubsetOf0(slbdtrb0(X361),slbdtrb0(X362))
| sdtlseqdt0(X361,X362)
| ~ aElementOf0(X361,szNzAzT0)
| ~ aElementOf0(X362,szNzAzT0) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSegLess])])]) ).
cnf(c_0_22,hypothesis,
( aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,xQ) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_23,hypothesis,
aElementOf0(xp,xQ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
fof(c_0_24,hypothesis,
! [X512] :
( ~ aElementOf0(X512,sdtlpdtrp0(xN,xm))
| sdtlseqdt0(xx,X512) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[m__5401])]) ).
cnf(c_0_25,negated_conjecture,
( aElementOf0(X1,sdtlpdtrp0(xN,xm))
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xn)) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_26,hypothesis,
aElementOf0(xp,sdtlpdtrp0(xN,xn)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18,c_0_19]),c_0_20]) ).
fof(c_0_27,hypothesis,
( aElementOf0(xx,szNzAzT0)
& aElementOf0(esk42_0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,esk42_0) = xx ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[m__5365])]) ).
fof(c_0_28,plain,
! [X352,X353,X354,X355,X356] :
( ( aSet0(X353)
| X353 != slbdtrb0(X352)
| ~ aElementOf0(X352,szNzAzT0) )
& ( aElementOf0(X354,szNzAzT0)
| ~ aElementOf0(X354,X353)
| X353 != slbdtrb0(X352)
| ~ aElementOf0(X352,szNzAzT0) )
& ( sdtlseqdt0(szszuzczcdt0(X354),X352)
| ~ aElementOf0(X354,X353)
| X353 != slbdtrb0(X352)
| ~ aElementOf0(X352,szNzAzT0) )
& ( ~ aElementOf0(X355,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X355),X352)
| aElementOf0(X355,X353)
| X353 != slbdtrb0(X352)
| ~ aElementOf0(X352,szNzAzT0) )
& ( ~ aElementOf0(esk9_2(X352,X356),X356)
| ~ aElementOf0(esk9_2(X352,X356),szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(esk9_2(X352,X356)),X352)
| ~ aSet0(X356)
| X356 = slbdtrb0(X352)
| ~ aElementOf0(X352,szNzAzT0) )
& ( aElementOf0(esk9_2(X352,X356),szNzAzT0)
| aElementOf0(esk9_2(X352,X356),X356)
| ~ aSet0(X356)
| X356 = slbdtrb0(X352)
| ~ aElementOf0(X352,szNzAzT0) )
& ( sdtlseqdt0(szszuzczcdt0(esk9_2(X352,X356)),X352)
| aElementOf0(esk9_2(X352,X356),X356)
| ~ aSet0(X356)
| X356 = slbdtrb0(X352)
| ~ aElementOf0(X352,szNzAzT0) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefSeg])])])])])]) ).
fof(c_0_29,plain,
! [X277,X278] :
( ~ aSet0(X277)
| ~ aSet0(X278)
| ~ aSubsetOf0(X277,X278)
| ~ aSubsetOf0(X278,X277)
| X277 = X278 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSubASymm])]) ).
fof(c_0_30,plain,
! [X269,X270,X271,X272] :
( ( aSet0(X270)
| ~ aSubsetOf0(X270,X269)
| ~ aSet0(X269) )
& ( ~ aElementOf0(X271,X270)
| aElementOf0(X271,X269)
| ~ aSubsetOf0(X270,X269)
| ~ aSet0(X269) )
& ( aElementOf0(esk2_2(X269,X272),X272)
| ~ aSet0(X272)
| aSubsetOf0(X272,X269)
| ~ aSet0(X269) )
& ( ~ aElementOf0(esk2_2(X269,X272),X269)
| ~ aSet0(X272)
| aSubsetOf0(X272,X269)
| ~ aSet0(X269) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefSub])])])])])]) ).
cnf(c_0_31,plain,
( aSubsetOf0(slbdtrb0(X1),slbdtrb0(X2))
| ~ sdtlseqdt0(X1,X2)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_32,hypothesis,
aElementOf0(xp,szNzAzT0),
inference(spm,[status(thm)],[c_0_22,c_0_23]) ).
cnf(c_0_33,hypothesis,
( sdtlseqdt0(xx,X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xm)) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
cnf(c_0_34,negated_conjecture,
aElementOf0(xp,sdtlpdtrp0(xN,xm)),
inference(spm,[status(thm)],[c_0_25,c_0_26]) ).
cnf(c_0_35,hypothesis,
aElementOf0(xx,szNzAzT0),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_36,hypothesis,
( sdtlseqdt0(xp,X1)
| ~ aElementOf0(X1,xQ) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_37,hypothesis,
aElementOf0(xx,xQ),
inference(split_conjunct,[status(thm)],[m__5348]) ).
cnf(c_0_38,plain,
( aSet0(X1)
| X1 != slbdtrb0(X2)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
fof(c_0_39,plain,
! [X365] :
( ~ aElementOf0(X365,szNzAzT0)
| sbrdtbr0(slbdtrb0(X365)) = X365 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCardSeg])]) ).
cnf(c_0_40,plain,
( X1 = X2
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_41,plain,
( aSet0(X1)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
cnf(c_0_42,hypothesis,
( aSubsetOf0(slbdtrb0(X1),slbdtrb0(xp))
| ~ sdtlseqdt0(X1,xp)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[c_0_31,c_0_32]) ).
cnf(c_0_43,hypothesis,
sdtlseqdt0(xx,xp),
inference(spm,[status(thm)],[c_0_33,c_0_34]) ).
cnf(c_0_44,hypothesis,
( aSubsetOf0(slbdtrb0(X1),slbdtrb0(xx))
| ~ sdtlseqdt0(X1,xx)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[c_0_31,c_0_35]) ).
cnf(c_0_45,hypothesis,
sdtlseqdt0(xp,xx),
inference(spm,[status(thm)],[c_0_36,c_0_37]) ).
cnf(c_0_46,plain,
( aSet0(slbdtrb0(X1))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(er,[status(thm)],[c_0_38]) ).
cnf(c_0_47,plain,
( sbrdtbr0(slbdtrb0(X1)) = X1
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_48,plain,
( X1 = X2
| ~ aSubsetOf0(X2,X1)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X2) ),
inference(csr,[status(thm)],[c_0_40,c_0_41]) ).
cnf(c_0_49,hypothesis,
aSubsetOf0(slbdtrb0(xx),slbdtrb0(xp)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_43]),c_0_35])]) ).
cnf(c_0_50,hypothesis,
aSubsetOf0(slbdtrb0(xp),slbdtrb0(xx)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_45]),c_0_32])]) ).
cnf(c_0_51,hypothesis,
aSet0(slbdtrb0(xx)),
inference(spm,[status(thm)],[c_0_46,c_0_35]) ).
cnf(c_0_52,hypothesis,
xx != szmzizndt0(xQ),
inference(split_conjunct,[status(thm)],[m__5348]) ).
cnf(c_0_53,hypothesis,
xp = szmzizndt0(xQ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_54,hypothesis,
sbrdtbr0(slbdtrb0(xp)) = xp,
inference(spm,[status(thm)],[c_0_47,c_0_32]) ).
cnf(c_0_55,hypothesis,
slbdtrb0(xp) = slbdtrb0(xx),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_49]),c_0_50]),c_0_51])]) ).
cnf(c_0_56,hypothesis,
sbrdtbr0(slbdtrb0(xx)) = xx,
inference(spm,[status(thm)],[c_0_47,c_0_35]) ).
cnf(c_0_57,hypothesis,
xp != xx,
inference(rw,[status(thm)],[c_0_52,c_0_53]) ).
cnf(c_0_58,hypothesis,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_54,c_0_55]),c_0_56]),c_0_57]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM621+3 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n007.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 00:50:38 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 52.15/29.62 % Version : CSE_E---1.7
% 52.15/29.62 % Problem : theBenchmark.p
% 52.15/29.62 % SZS status Theorem for theBenchmark.p
% 52.15/29.62 % SZS output start CNFRefutation
% See solution above
% 52.25/29.75 % Total time : 23.876s
%------------------------------------------------------------------------------