%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM604+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 : n007.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:32 AM UTC 2026
% Result : Theorem 119.52s 16.98s
% Output : CNFRefutation 119.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 4
% Syntax : Number of formulae : 14 ( 9 unt; 0 def)
% Number of atoms : 25 ( 4 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 15 ( 4 ~; 2 |; 6 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 5 ( 0 sgn 3 !; 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__5034,axiom,
( sdtlpdtrp0(xe,xi) = xx
& aElementOf0(xi,szNzAzT0) ),
file('theBenchmark.p',m__5034) ).
fof(m__5045,axiom,
( aSubsetOf0(sdtlpdtrp0(xN,xi),xS)
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> aElementOf0(W0,xS) ) ),
file('theBenchmark.p',m__5045) ).
fof(m__,conjecture,
aElementOf0(xx,xS),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ aElementOf0(xx,xS),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_909,plain,
( aElementOf0(sdtlpdtrp0(xe,A),sdtlpdtrp0(xN,A))
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[m__4660]) ).
cnf(c_952,plain,
aElementOf0(xi,szNzAzT0),
inference(clausify,[status(thm)],[m__5034]) ).
cnf(c_953,plain,
sdtlpdtrp0(xe,xi) = xx,
inference(clausify,[status(thm)],[m__5034]) ).
cnf(c_954,plain,
( aElementOf0(A,xS)
| ~ aElementOf0(A,sdtlpdtrp0(xN,xi)) ),
inference(clausify,[status(thm)],[m__5045]) ).
cnf(c_956,negated_conjecture,
~ aElementOf0(xx,xS),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_6359,plain,
aElementOf0(sdtlpdtrp0(xe,xi),sdtlpdtrp0(xN,xi)),
inference(resolve,[status(thm)],[c_952,c_909]) ).
cnf(c_14687,plain,
aElementOf0(sdtlpdtrp0(xe,xi),xS),
inference(resolve,[status(thm)],[c_6359,c_954]) ).
cnf(c_14828,plain,
aElementOf0(xx,xS),
inference(paramod,[status(thm)],[c_953,c_14687]) ).
cnf(c_14827,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_956,c_14828]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM604+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n007.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 03:23:08 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.44 % Process 2682701 was started by sandbox on n007,
% 0.17/0.44 % Sat Sep 26 03:23:08 2026
% 0.17/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.56/0.83
% 0.56/0.83 % From the command line: assign(max_seconds, 300).
% 119.52/16.98
% 119.52/16.98 % given #500 (I,wt=25): 895 -aElementOf0(A,szNzAzT0) | -aElementOf0(B,f39(A)) | aElementOf0(B,sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A)))) # tptp_name(m__4411). [clausify(83)].
% 119.52/16.98
% 119.52/16.98 % given #1000 (I,wt=64): 1657 -aSubsetOf0(f23(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | aSet0(f23(A,B,C)) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aSubsetOf0(sdtlcdtrc0(C,szDzozmdt0(C)),xT) | -iLess0(A,xK) | -aSet0(D) | aElementOf0(f29(A,B,C,D),D) | sbrdtbr0(D) != A | f27(A,B,C) = sdtlpdtrp0(C,D). [copy(1656),flip(m)].
% 119.52/16.98
% 119.52/16.98 % given #1500 (I,wt=57): 2433 -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) | aSet0(sdtlcdtrc0(C,szDzozmdt0(C))) | -iLess0(A,xK) | aElementOf0(f27(A,B,C),xT). [resolve(291,a,159,e)].
% 119.52/16.98
% 119.52/16.98 % given #2000 (I,wt=60): 3157 -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) | aSet0(sdtlcdtrc0(C,szDzozmdt0(C))) | -iLess0(A,xK) | isCountable0(f28(A,B,C)). [resolve(293,a,281,f)].
% 119.52/16.98
% 119.52/16.98 % given #2500 (I,wt=78): 3743 -aSubsetOf0(f23(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(f23(A,B,C),szDzozmdt0(C)) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | aElementOf0(f22(A,B),B) | -isCountable0(B) | -aFunction0(C) | aElementOf0(D,sdtlcdtrc0(C,szDzozmdt0(C))) | -aElementOf0(E,szDzozmdt0(C)) | sdtlpdtrp0(C,E) != D | -iLess0(A,xK) | -aSubsetOf0(f23(A,B,C),f28(A,B,C)) | f27(A,B,C) = sdtlpdtrp0(C,f23(A,B,C)). [factor(1454,b,n)].
% 119.52/16.98
% 119.52/16.98 % given #3000 (I,wt=103): 4250 -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 | aSubsetOf0(f23(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))),sdtlcdtrc0(B,szDzozmdt0(B))) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | -aElementOf0(C,szDzozmdt0(B)) | f22(A,sdtlcdtrc0(B,szDzozmdt0(B))) != sdtlpdtrp0(B,C) | -iLess0(A,xK) | aSet0(f28(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)). [factor(2302,g,j),flip(k)].
% 119.52/16.98
% 119.52/16.98 % given #3500 (I,wt=89): 4771 -aSet0(f23(A,B,C)) | aElementOf0(f24(A,B,C),f23(A,B,C)) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(f23(A,B,C),szDzozmdt0(C)) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | -aElementOf0(f22(A,B),szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(D,sdtlcdtrc0(C,szDzozmdt0(C))) | aElementOf0(f25(A,B,C,D),szDzozmdt0(C)) | -iLess0(A,xK) | aElementOf0(f29(A,B,C,f23(A,B,C)),f23(A,B,C)) | f27(A,B,C) = sdtlpdtrp0(C,f23(A,B,C)). [factor(2779,a,m),merge(n)].
% 119.52/16.98
% 119.52/16.98 % given #4000 (I,wt=73): 5292 -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) | defn_00(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,C) | -aElementOf0(D,szDzozmdt0(B)) | f22(A,sdtlcdtrc0(B,szDzozmdt0(B))) != sdtlpdtrp0(B,D) | -iLess0(A,xK) | -aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),f28(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)). [factor(3476,c,k)].
% 119.52/16.98
% 119.52/16.98 % given #4500 (I,wt=138): 5796 -aSet0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | aElementOf0(f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),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))),sdtlcdtrc0(B,szDzozmdt0(B))) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | -iLess0(A,xK) | aElementOf0(f29(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)),f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | f27(A,sdtlcdtrc0(B,szDzozmdt0(B)),B) = sdtlpdtrp0(B,f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)). [factor(5167,e,k)].
% 119.52/16.98
% 119.52/16.98 % given #5000 (F,wt=12): 9655 -aSet0(slbdtsldtrb0(xT,sz00)) | -isCountable0(slbdtsldtrb0(xT,sz00)). [resolve(9640,a,650,c)].
% 119.52/16.98
% 119.52/16.98 % SZS status Theorem for theBenchmark
% 119.52/16.98
% 119.52/16.98 % Proof 1 at 7.51 (+ 0.44) seconds.
% 119.52/16.98 % Length of proof is 12.
% 119.52/16.98 % Level of proof is 4.
% 119.52/16.98 % Maximum clause weight is 14.000.
% 119.52/16.98 % Given clauses 5423.
% 119.52/16.98
% 119.52/16.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------