%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM612+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 : Sun Sep 27 08:17:34 AM UTC 2026
% Result : Theorem 43.43s 6.15s
% Output : CNFRefutation 43.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 9
% Syntax : Number of formulae : 43 ( 16 unt; 0 def)
% Number of atoms : 100 ( 22 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 95 ( 38 ~; 30 |; 16 &)
% ( 2 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 18 ( 0 sgn 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSubFSet,axiom,
! [W0] :
( ( isFinite0(W0)
& aSet0(W0) )
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> isFinite0(W1) ) ),
file('theBenchmark.p',mSubFSet) ).
fof(mCardNum,axiom,
! [W0] :
( aSet0(W0)
=> ( aElementOf0(sbrdtbr0(W0),szNzAzT0)
<=> isFinite0(W0) ) ),
file('theBenchmark.p',mCardNum) ).
fof(mCardDiff,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( ( aElementOf0(W1,W0)
& isFinite0(W0) )
=> szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ),
file('theBenchmark.p',mCardDiff) ).
fof(m__5078,axiom,
( aElementOf0(xQ,slbdtsldtrb0(xO,xK))
& sbrdtbr0(xQ) = xK
& aSubsetOf0(xQ,xO)
& ! [W0] :
( aElementOf0(W0,xQ)
=> aElementOf0(W0,xO) )
& aSet0(xQ) ),
file('theBenchmark.p',m__5078) ).
fof(m__5147,axiom,
( xp = szmzizndt0(xQ)
& ! [W0] :
( aElementOf0(W0,xQ)
=> sdtlseqdt0(xp,W0) )
& aElementOf0(xp,xQ) ),
file('theBenchmark.p',m__5147) ).
fof(m__5164,axiom,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& ! [W0] :
( aElementOf0(W0,xP)
<=> ( W0 != szmzizndt0(xQ)
& aElementOf0(W0,xQ)
& aElement0(W0) ) )
& ! [W0] :
( aElementOf0(W0,xQ)
=> sdtlseqdt0(szmzizndt0(xQ),W0) )
& aSet0(xP) ),
file('theBenchmark.p',m__5164) ).
fof(m__5195,axiom,
( aSubsetOf0(xP,xQ)
& ! [W0] :
( aElementOf0(W0,xP)
=> aElementOf0(W0,xQ) ) ),
file('theBenchmark.p',m__5195) ).
fof(m__,conjecture,
( aElementOf0(sbrdtbr0(xP),szNzAzT0)
& szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( aElementOf0(sbrdtbr0(xP),szNzAzT0)
& szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(m__3418,axiom,
aElementOf0(xK,szNzAzT0),
file('theBenchmark.p',m__3418) ).
cnf(c_519,plain,
aElementOf0(xK,szNzAzT0),
inference(clausify,[status(thm)],[m__3418]) ).
cnf(c_595,plain,
( sbrdtbr0(A) = szszuzczcdt0(sbrdtbr0(sdtmndt0(A,B)))
| ~ aElementOf0(B,A)
| ~ isFinite0(A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardDiff]) ).
cnf(c_596,plain,
( szszuzczcdt0(sbrdtbr0(sdtmndt0(A,B))) = sbrdtbr0(A)
| ~ aElementOf0(B,A)
| ~ isFinite0(A)
| ~ aSet0(A) ),
inference(copy,[status(thm)],[c_595]) ).
cnf(c_600,plain,
( ~ isFinite0(A)
| aElementOf0(sbrdtbr0(A),szNzAzT0)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardNum]) ).
cnf(c_601,plain,
( isFinite0(A)
| ~ aElementOf0(sbrdtbr0(A),szNzAzT0)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mCardNum]) ).
cnf(c_649,plain,
( isFinite0(B)
| ~ aSubsetOf0(B,A)
| ~ isFinite0(A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mSubFSet]) ).
cnf(c_975,plain,
aSet0(xQ),
inference(clausify,[status(thm)],[m__5078]) ).
cnf(c_978,plain,
sbrdtbr0(xQ) = xK,
inference(clausify,[status(thm)],[m__5078]) ).
cnf(c_987,plain,
aElementOf0(xp,xQ),
inference(clausify,[status(thm)],[m__5147]) ).
cnf(c_989,plain,
szmzizndt0(xQ) = xp,
inference(clausify,[status(thm)],[m__5147]) ).
cnf(c_990,plain,
aSet0(xP),
inference(clausify,[status(thm)],[m__5164]) ).
cnf(c_998,plain,
sdtmndt0(xQ,szmzizndt0(xQ)) = xP,
inference(clausify,[status(thm)],[m__5164]) ).
cnf(c_999,plain,
sdtmndt0(xQ,xp) = xP,
inference(paramod,[status(thm)],[c_989,c_998]) ).
cnf(c_1002,plain,
aSubsetOf0(xP,xQ),
inference(clausify,[status(thm)],[m__5195]) ).
cnf(c_1005,negated_conjecture,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| sbrdtbr0(xQ) != szszuzczcdt0(sbrdtbr0(xP)) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_7160,negated_conjecture,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| xK != szszuzczcdt0(sbrdtbr0(xP)) ),
inference(paramod,[status(thm)],[c_978,c_1005]) ).
cnf(c_1006,negated_conjecture,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| szszuzczcdt0(sbrdtbr0(xP)) != xK ),
inference(copy,[status(thm)],[c_7160]) ).
cnf(c_7161,plain,
( isFinite0(xQ)
| ~ aElementOf0(sbrdtbr0(xQ),szNzAzT0) ),
inference(resolve,[status(thm)],[c_975,c_601]) ).
cnf(c_7162,plain,
( isFinite0(xQ)
| ~ aElementOf0(xK,szNzAzT0) ),
inference(paramod,[status(thm)],[c_978,c_7161]) ).
cnf(c_6836,plain,
isFinite0(xQ),
inference(resolve,[status(thm)],[c_519,c_7162]) ).
cnf(c_7163,plain,
( szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xp))) = sbrdtbr0(xQ)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_987,c_596]) ).
cnf(c_7164,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(paramod,[status(thm)],[c_999,c_7163]) ).
cnf(c_7165,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = xK
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(paramod,[status(thm)],[c_978,c_7164]) ).
cnf(c_7166,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = xK
| ~ isFinite0(xQ) ),
inference(resolve,[status(thm)],[c_975,c_7165]) ).
cnf(c_7003,plain,
szszuzczcdt0(sbrdtbr0(xP)) = xK,
inference(resolve,[status(thm)],[c_6836,c_7166]) ).
cnf(c_7167,negated_conjecture,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| xK != xK ),
inference(paramod,[status(thm)],[c_7003,c_1006]) ).
cnf(c_7017,negated_conjecture,
~ aElementOf0(sbrdtbr0(xP),szNzAzT0),
inference(copy,[status(thm)],[c_7167]) ).
cnf(c_7168,plain,
( ~ isFinite0(xP)
| aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
inference(resolve,[status(thm)],[c_990,c_600]) ).
cnf(c_7083,negated_conjecture,
~ isFinite0(xP),
inference(resolve,[status(thm)],[c_7017,c_7168]) ).
cnf(c_7169,plain,
( isFinite0(xP)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_1002,c_649]) ).
cnf(c_7170,plain,
( isFinite0(xP)
| ~ isFinite0(xQ) ),
inference(resolve,[status(thm)],[c_975,c_7169]) ).
cnf(c_7171,plain,
isFinite0(xP),
inference(resolve,[status(thm)],[c_6836,c_7170]) ).
cnf(c_7159,plain,
$false,
inference(resolve,[status(thm)],[c_7083,c_7171]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM612+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n026.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 03:29:39 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 4181096 was started by sandbox2 on n026,
% 0.08/0.36 % Sat Sep 26 03:29:39 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.31/0.62
% 0.31/0.62 % From the command line: assign(max_seconds, 300).
% 43.43/6.15
% 43.43/6.15 % given #500 (I,wt=25): 911 -aElementOf0(A,szNzAzT0) | -aElementOf0(B,f39(A)) | aElementOf0(B,sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A)))) # tptp_name(m__4411). [clausify(83)].
% 43.43/6.15
% 43.43/6.15 % SZS status Theorem for theBenchmark
% 43.43/6.15
% 43.43/6.15 % Proof 1 at 5.11 (+ 0.30) seconds.
% 43.43/6.15 % Length of proof is 29.
% 43.43/6.15 % Level of proof is 6.
% 43.43/6.15 % Maximum clause weight is 23.000.
% 43.43/6.15 % Given clauses 573.
% 43.43/6.15
% 43.43/6.15 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------