%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM622+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 : n004.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:36 AM UTC 2026
% Result : Theorem 104.98s 14.92s
% Output : CNFRefutation 104.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 5
% Syntax : Number of formulae : 17 ( 11 unt; 0 def)
% Number of atoms : 40 ( 9 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 27 ( 4 ~; 4 |; 13 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-2 aty)
% Number of variables : 8 ( 0 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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__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__5461,axiom,
( aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> aElementOf0(W0,sdtlpdtrp0(xN,xm)) ) ),
file('theBenchmark.p',m__5461) ).
fof(m__,conjecture,
aElementOf0(xp,sdtlpdtrp0(xN,xm)),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ aElementOf0(xp,sdtlpdtrp0(xN,xm)),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_932,plain,
( aElementOf0(sdtlpdtrp0(xe,A),sdtlpdtrp0(xN,A))
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[m__4660]) ).
cnf(c_936,plain,
szDzozmdt0(xd) = szNzAzT0,
inference(clausify,[status(thm)],[m__4730]) ).
cnf(c_1014,plain,
aElementOf0(xn,szDzozmdt0(xd)),
inference(clausify,[status(thm)],[m__5309]) ).
cnf(c_1015,plain,
aElementOf0(xn,szNzAzT0),
inference(paramod,[status(thm)],[c_936,c_1014]) ).
cnf(c_1019,plain,
sdtlpdtrp0(xe,xn) = xp,
inference(clausify,[status(thm)],[m__5309]) ).
cnf(c_1035,plain,
( aElementOf0(A,sdtlpdtrp0(xN,xm))
| ~ aElementOf0(A,sdtlpdtrp0(xN,xn)) ),
inference(clausify,[status(thm)],[m__5461]) ).
cnf(c_1037,negated_conjecture,
~ aElementOf0(xp,sdtlpdtrp0(xN,xm)),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_21238,plain,
aElementOf0(sdtlpdtrp0(xe,xn),sdtlpdtrp0(xN,xn)),
inference(resolve,[status(thm)],[c_1015,c_932]) ).
cnf(c_6395,plain,
aElementOf0(xp,sdtlpdtrp0(xN,xn)),
inference(paramod,[status(thm)],[c_1019,c_21238]) ).
cnf(c_21239,plain,
aElementOf0(xp,sdtlpdtrp0(xN,xm)),
inference(resolve,[status(thm)],[c_6395,c_1035]) ).
cnf(c_21237,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1037,c_21239]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM622+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.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 03:29:08 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 714387 was started by sandbox on n004,
% 0.10/0.37 % Sat Sep 26 03:29:08 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.22/0.51
% 0.22/0.51 % From the command line: assign(max_seconds, 300).
% 104.98/14.92
% 104.98/14.92 % given #500 (I,wt=17): 918 -aElementOf0(A,szNzAzT0) | -aElementOf0(B,f39(A)) | aElementOf0(B,sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A)))) # tptp_name(m__4411). [clausify(83)].
% 104.98/14.92
% 104.98/14.92 % given #1000 (I,wt=53): 1620 -aSubsetOf0(f23(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(D,f23(A,B,C)) | aElementOf0(D,B) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(C) | aElementOf0(f26(A,B,C),sdtlcdtrc0(C,szDzozmdt0(C))) | -iLess0(A,xK) | -aElementOf0(E,f28(A,B,C)) | aElementOf0(E,B). [resolve(301,a,135,e)].
% 104.98/14.92
% 104.98/14.92 % given #1500 (I,wt=73): 2455 -aSet0(f23(A,B,C)) | -aElementOf0(f24(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(D,f23(A,B,C)) | aElementOf0(D,B) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(C) | aElementOf0(f26(A,B,C),sdtlcdtrc0(C,szDzozmdt0(C))) | -iLess0(A,xK) | -aSet0(E) | -aElementOf0(f29(A,B,C,E),f28(A,B,C)) | sbrdtbr0(E) != A | f27(A,B,C) = sdtlpdtrp0(C,E). [copy(2454),flip(o)].
% 104.98/14.92
% 104.98/14.92 % given #2000 (I,wt=55): 3176 -aSet0(f23(A,B,C)) | aElementOf0(f24(A,B,C),f23(A,B,C)) | sbrdtbr0(f23(A,B,C)) != A | aSubsetOf0(f23(A,B,C),B) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | aElementOf0(f22(A,B),B) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(f26(A,B,C),xT) | -iLess0(A,xK) | aSet0(f28(A,B,C)). [resolve(307,a,253,f)].
% 104.98/14.92
% 104.98/14.92 % given #2500 (I,wt=107): 3705 -aSet0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | -aElementOf0(f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))) | sbrdtbr0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) != A | -aElementOf0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),szDzozmdt0(B)) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(sdtlcdtrc0(B,szDzozmdt0(B)),szNzAzT0) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | sdtlpdtrp0(B,f25(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B))) = f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B) | -iLess0(A,xK) | -aSubsetOf0(C,f28(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | sbrdtbr0(C) != A | f27(A,sdtlcdtrc0(B,szDzozmdt0(B)),B) = sdtlpdtrp0(B,C). [factor(1933,b,i)].
% 104.98/14.92
% 104.98/14.92 % given #3000 (I,wt=105): 4214 -aSet0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | -aElementOf0(f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))) | sbrdtbr0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) != A | -aElementOf0(f26(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | aElementOf0(f26(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(A,szNzAzT0) | -aSet0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),szNzAzT0) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | -iLess0(A,xK) | -aElementOf0(C,slbdtsldtrb0(f28(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),A)) | f27(A,sdtlcdtrc0(B,szDzozmdt0(B)),B) = sdtlpdtrp0(B,C). [factor(2542,e,k)].
% 104.98/14.92
% 104.98/14.92 % given #3500 (I,wt=58): 4726 -aSet0(f23(A,B,C)) | aElementOf0(f24(A,B,C),f23(A,B,C)) | sbrdtbr0(f23(A,B,C)) != A | aSubsetOf0(f23(A,B,C),B) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | aElementOf0(f22(A,B),B) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(f26(A,B,C),xT) | -iLess0(A,xK) | -aElementOf0(f22(A,B),f28(A,B,C)). [factor(3175,g,m)].
% 104.98/14.92
% 104.98/14.92 % given #4000 (I,wt=119): 5232 -aSubsetOf0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))) | sbrdtbr0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) != A | -aElementOf0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),szDzozmdt0(B)) | -aElementOf0(A,szNzAzT0) | -aSet0(sdtlcdtrc0(B,szDzozmdt0(B))) | aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),sdtlcdtrc0(B,szDzozmdt0(B))) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | aElementOf0(f29(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,sdtlcdtrc0(B,szDzozmdt0(B))),sdtlcdtrc0(B,szDzozmdt0(B))) | f29(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,sdtlcdtrc0(B,szDzozmdt0(B))) != sdtlpdtrp0(B,f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | -iLess0(A,xK) | sbrdtbr0(sdtlcdtrc0(B,szDzozmdt0(B))) != A | f27(A,sdtlcdtrc0(B,szDzozmdt0(B)),B) = sdtlpdtrp0(B,sdtlcdtrc0(B,szDzozmdt0(B))). [factor(4812,i,l),flip(j)].
% 104.98/14.92
% 104.98/14.92 % given #4500 (T,wt=4): 11081 aFunction0(sdtlpdtrp0(xC,c1)). [resolve(6189,a,836,a)].
% 104.98/14.92
% 104.98/14.92 % given #5000 (F,wt=7): 20117 sdtmndt0(f39(f46(xp)),xK) != szNzAzT0. [resolve(17054,a,19536,a)].
% 104.98/14.92
% 104.98/14.92 % SZS status Theorem for theBenchmark
% 104.98/14.92
% 104.98/14.92 % Proof 1 at 13.22 (+ 0.61) seconds.
% 104.98/14.92 % Length of proof is 14.
% 104.98/14.92 % Level of proof is 4.
% 104.98/14.92 % Maximum clause weight is 10.000.
% 104.98/14.92 % Given clauses 5006.
% 104.98/14.92
% 104.98/14.92 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------