%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM631+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:38 AM UTC 2026
% Result : Theorem 20.29s 6.71s
% Output : CNFRefutation 20.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 11
% Syntax : Number of formulae : 51 ( 31 unt; 0 def)
% Number of atoms : 120 ( 54 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 98 ( 29 ~; 27 |; 28 &)
% ( 2 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 13 con; 0-2 aty)
% Number of variables : 19 ( 0 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mConsDiff,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ),
file('theBenchmark.p',mConsDiff) ).
fof(m__4660,axiom,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(sdtlpdtrp0(xe,W0),W1) )
& aElementOf0(sdtlpdtrp0(xe,W0),sdtlpdtrp0(xN,W0)) ) )
& szDzozmdt0(xe) = szNzAzT0
& aFunction0(xe) ),
file('theBenchmark.p',m__4660) ).
fof(m__4730,axiom,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( ( ( aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
| ( sbrdtbr0(W1) = xk
& ( aSubsetOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
| ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) )
& aSet0(W1) )
=> sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) ) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
file('theBenchmark.p',m__4730) ).
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__5309,axiom,
( sdtlpdtrp0(xe,xn) = xp
& aElementOf0(xn,szNzAzT0)
& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)
& aElementOf0(xn,szDzozmdt0(xd)) ),
file('theBenchmark.p',m__5309) ).
fof(m__5334,axiom,
( aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
& ! [W0] :
( aElementOf0(W0,xP)
=> aElementOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) ),
file('theBenchmark.p',m__5334) ).
fof(m__5632,axiom,
( sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)
& ! [W0] :
( aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xn))
| aElementOf0(W0,xP) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0) ) ),
file('theBenchmark.p',m__5632) ).
fof(m__,conjecture,
sdtlpdtrp0(xc,xQ) = sdtlpdtrp0(xd,xn),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
sdtlpdtrp0(xc,xQ) != sdtlpdtrp0(xd,xn),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_626,plain,
( sdtpldt0(sdtmndt0(A,B),B) = A
| ~ aElementOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mConsDiff]) ).
cnf(c_929,plain,
( sdtlpdtrp0(xe,A) = szmzizndt0(sdtlpdtrp0(xN,A))
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[m__4660]) ).
cnf(c_931,plain,
szDzozmdt0(xd) = szNzAzT0,
inference(clausify,[status(thm)],[m__4730]) ).
cnf(c_934,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,A),B) = sdtlpdtrp0(xd,A)
| sbrdtbr0(B) != xk
| ~ aSubsetOf0(B,sdtlpdtrp0(xN,szszuzczcdt0(A)))
| ~ aSet0(B)
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[m__4730]) ).
cnf(c_977,plain,
aSet0(xQ),
inference(clausify,[status(thm)],[m__5078]) ).
cnf(c_989,plain,
aElementOf0(xp,xQ),
inference(clausify,[status(thm)],[m__5147]) ).
cnf(c_991,plain,
szmzizndt0(xQ) = xp,
inference(clausify,[status(thm)],[m__5147]) ).
cnf(c_992,plain,
aSet0(xP),
inference(clausify,[status(thm)],[m__5164]) ).
cnf(c_1000,plain,
sdtmndt0(xQ,szmzizndt0(xQ)) = xP,
inference(clausify,[status(thm)],[m__5164]) ).
cnf(c_1001,plain,
sdtmndt0(xQ,xp) = xP,
inference(paramod,[status(thm)],[c_991,c_1000]) ).
fof(m__5217,axiom,
sbrdtbr0(xP) = xk,
file('theBenchmark.p',m__5217) ).
cnf(c_1007,plain,
sbrdtbr0(xP) = xk,
inference(clausify,[status(thm)],[m__5217]) ).
cnf(c_1009,plain,
aElementOf0(xn,szDzozmdt0(xd)),
inference(clausify,[status(thm)],[m__5309]) ).
cnf(c_1010,plain,
aElementOf0(xn,szNzAzT0),
inference(paramod,[status(thm)],[c_931,c_1009]) ).
cnf(c_1011,plain,
szDzizrdt0(xd) = sdtlpdtrp0(xd,xn),
inference(clausify,[status(thm)],[m__5309]) ).
cnf(c_1012,plain,
sdtlpdtrp0(xd,xn) = szDzizrdt0(xd),
inference(copy,[status(thm)],[c_1011]) ).
cnf(c_1014,plain,
sdtlpdtrp0(xe,xn) = xp,
inference(clausify,[status(thm)],[m__5309]) ).
cnf(c_1017,plain,
aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))),
inference(clausify,[status(thm)],[m__5334]) ).
cnf(c_1033,plain,
sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) = sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))),
inference(clausify,[status(thm)],[m__5632]) ).
cnf(c_1034,plain,
sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP),
inference(copy,[status(thm)],[c_1033]) ).
cnf(c_1035,negated_conjecture,
sdtlpdtrp0(xd,xn) != sdtlpdtrp0(xc,xQ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_4819,negated_conjecture,
szDzizrdt0(xd) != sdtlpdtrp0(xc,xQ),
inference(paramod,[status(thm)],[c_1012,c_1035]) ).
cnf(c_1036,negated_conjecture,
sdtlpdtrp0(xc,xQ) != szDzizrdt0(xd),
inference(copy,[status(thm)],[c_4819]) ).
cnf(c_4820,plain,
( sdtpldt0(sdtmndt0(xQ,xp),xp) = xQ
| ~ aSet0(xQ) ),
inference(resolve,[status(thm)],[c_989,c_626]) ).
cnf(c_4821,plain,
( sdtpldt0(xP,xp) = xQ
| ~ aSet0(xQ) ),
inference(paramod,[status(thm)],[c_1001,c_4820]) ).
cnf(c_4487,plain,
sdtpldt0(xP,xp) = xQ,
inference(resolve,[status(thm)],[c_977,c_4821]) ).
cnf(c_4822,plain,
sdtlpdtrp0(xe,xn) = szmzizndt0(sdtlpdtrp0(xN,xn)),
inference(resolve,[status(thm)],[c_1010,c_929]) ).
cnf(c_4823,plain,
xp = szmzizndt0(sdtlpdtrp0(xN,xn)),
inference(paramod,[status(thm)],[c_1014,c_4822]) ).
cnf(c_4613,plain,
szmzizndt0(sdtlpdtrp0(xN,xn)) = xp,
inference(copy,[status(thm)],[c_4823]) ).
cnf(c_4824,plain,
sdtlpdtrp0(xc,sdtpldt0(xP,xp)) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP),
inference(paramod,[status(thm)],[c_4613,c_1034]) ).
cnf(c_4825,plain,
sdtlpdtrp0(xc,xQ) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP),
inference(paramod,[status(thm)],[c_4487,c_4824]) ).
cnf(c_4741,plain,
sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) = sdtlpdtrp0(xc,xQ),
inference(copy,[status(thm)],[c_4825]) ).
cnf(c_4826,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) = sdtlpdtrp0(xd,xn)
| sbrdtbr0(xP) != xk
| ~ aSet0(xP)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(resolve,[status(thm)],[c_1017,c_934]) ).
cnf(c_4827,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) = sdtlpdtrp0(xd,xn)
| xk != xk
| ~ aSet0(xP)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(paramod,[status(thm)],[c_1007,c_4826]) ).
cnf(c_4828,plain,
( sdtlpdtrp0(xc,xQ) = sdtlpdtrp0(xd,xn)
| xk != xk
| ~ aSet0(xP)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(paramod,[status(thm)],[c_4741,c_4827]) ).
cnf(c_4829,plain,
( sdtlpdtrp0(xc,xQ) = szDzizrdt0(xd)
| xk != xk
| ~ aSet0(xP)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(paramod,[status(thm)],[c_1012,c_4828]) ).
cnf(c_4830,plain,
( sdtlpdtrp0(xc,xQ) = szDzizrdt0(xd)
| ~ aSet0(xP)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(copy,[status(thm)],[c_4829]) ).
cnf(c_4831,plain,
( sdtlpdtrp0(xc,xQ) = szDzizrdt0(xd)
| ~ aSet0(xP) ),
inference(resolve,[status(thm)],[c_1010,c_4830]) ).
cnf(c_4832,plain,
sdtlpdtrp0(xc,xQ) = szDzizrdt0(xd),
inference(resolve,[status(thm)],[c_992,c_4831]) ).
cnf(c_4818,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1036,c_4832]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM631+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n005.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 03:31:16 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 1101650 was started by sandbox on n005,
% 0.09/0.37 % Sat Sep 26 03:31:16 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.23/0.48
% 0.23/0.48 % From the command line: assign(max_seconds, 300).
% 20.29/6.71
% 20.29/6.71 % given #500 (I,wt=17): 913 -aElementOf0(A,szNzAzT0) | -aElementOf0(B,f39(A)) | aElementOf0(B,sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A)))) # tptp_name(m__4411). [clausify(83)].
% 20.29/6.71
% 20.29/6.71 % SZS status Theorem for theBenchmark
% 20.29/6.71
% 20.29/6.71 % Proof 1 at 2.69 (+ 0.14) seconds.
% 20.29/6.71 % Length of proof is 35.
% 20.29/6.71 % Level of proof is 5.
% 20.29/6.71 % Maximum clause weight is 24.000.
% 20.29/6.71 % Given clauses 583.
% 20.29/6.71
% 20.29/6.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------