%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM630+1 : 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 : n006.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 19.33s 3.24s
% Output : CNFRefutation 19.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 6
% Syntax : Number of formulae : 21 ( 13 unt; 0 def)
% Number of atoms : 43 ( 18 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 37 ( 15 ~; 12 |; 8 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-2 aty)
% Number of variables : 8 ( 0 sgn 2 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__4151,axiom,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ! [W1] :
( ( aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
& aSet0(W1) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& aFunction0(sdtlpdtrp0(xC,W0)) ) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
file('theBenchmark.p',m__4151) ).
fof(m__5164,axiom,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& aSet0(xP) ),
file('theBenchmark.p',m__5164) ).
fof(m__5309,axiom,
( sdtlpdtrp0(xe,xn) = xp
& aElementOf0(xn,szNzAzT0)
& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
file('theBenchmark.p',m__5309) ).
fof(m__,conjecture,
sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) != sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_266,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,A),B) = sdtlpdtrp0(xc,sdtpldt0(B,szmzizndt0(sdtlpdtrp0(xN,A))))
| ~ aElementOf0(B,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A))),xk))
| ~ aSet0(B)
| ~ aElementOf0(A,szNzAzT0) ),
inference(clausify,[status(thm)],[m__4151]) ).
cnf(c_267,plain,
( sdtlpdtrp0(xc,sdtpldt0(B,szmzizndt0(sdtlpdtrp0(xN,A)))) = sdtlpdtrp0(sdtlpdtrp0(xC,A),B)
| ~ aElementOf0(B,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,A),szmzizndt0(sdtlpdtrp0(xN,A))),xk))
| ~ aSet0(B)
| ~ aElementOf0(A,szNzAzT0) ),
inference(copy,[status(thm)],[c_266]) ).
cnf(c_299,plain,
aSet0(xP),
inference(clausify,[status(thm)],[m__5164]) ).
cnf(c_308,plain,
aElementOf0(xn,szNzAzT0),
inference(clausify,[status(thm)],[m__5309]) ).
fof(m__5585,axiom,
xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),
file('theBenchmark.p',m__5585) ).
cnf(c_312,plain,
xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),
inference(clausify,[status(thm)],[m__5585]) ).
cnf(c_313,plain,
sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))) = xD,
inference(copy,[status(thm)],[c_312]) ).
fof(m__5599,axiom,
aElementOf0(xP,slbdtsldtrb0(xD,xk)),
file('theBenchmark.p',m__5599) ).
cnf(c_314,plain,
aElementOf0(xP,slbdtsldtrb0(xD,xk)),
inference(clausify,[status(thm)],[m__5599]) ).
cnf(c_315,negated_conjecture,
sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) != sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_316,negated_conjecture,
sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) != sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP),
inference(copy,[status(thm)],[c_315]) ).
cnf(c_19799,plain,
( sdtlpdtrp0(xc,sdtpldt0(A,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),A)
| ~ aElementOf0(A,slbdtsldtrb0(xD,xk))
| ~ aSet0(A)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(paramod,[status(thm)],[c_313,c_267]) ).
cnf(c_1062,plain,
( sdtlpdtrp0(xc,sdtpldt0(A,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),A)
| ~ aElementOf0(A,slbdtsldtrb0(xD,xk))
| ~ aSet0(A) ),
inference(resolve,[status(thm)],[c_308,c_19799]) ).
cnf(c_19800,plain,
( sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)
| ~ aSet0(xP) ),
inference(resolve,[status(thm)],[c_1062,c_314]) ).
cnf(c_19801,plain,
sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP),
inference(resolve,[status(thm)],[c_299,c_19800]) ).
cnf(c_19798,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_316,c_19801]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM630+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n006.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Sat Sep 26 03:30:41 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 279924 was started by sandbox2 on n006,
% 0.08/0.37 % Sat Sep 26 03:30:41 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/0.40
% 0.14/0.40 % From the command line: assign(max_seconds, 300).
% 19.33/3.24
% 19.33/3.24 % given #500 (A,wt=18): 427 -aSet0(A) | -isFinite0(A) | isFinite0(slbdtsldtrb0(A,xK)). [resolve(236,a,197,c)].
% 19.33/3.24
% 19.33/3.24 % given #1000 (T,wt=14): 8413 aElement0(sdtlpdtrp0(xN,sz00)). [resolve(592,a,136,a)].
% 19.33/3.24
% 19.33/3.24 % given #1500 (A,wt=18): 732 -aElement0(A) | aSubsetOf0(sdtlbdtrb0(xd,A),szDzozmdt0(xd)). [resolve(279,a,213,a)].
% 19.33/3.24
% 19.33/3.24 % given #2000 (F,wt=19): 16458 sdtmndt0(xP,xp) != xT | szDzizrdt0(xd) != xp. [resolve(14620,a,299,a)].
% 19.33/3.24
% 19.33/3.24 % SZS status Theorem for theBenchmark
% 19.33/3.24
% 19.33/3.24 % Proof 1 at 2.09 (+ 0.67) seconds.
% 19.33/3.24 % Length of proof is 15.
% 19.33/3.24 % Level of proof is 4.
% 19.33/3.24 % Maximum clause weight is 58.000.
% 19.33/3.24 % Given clauses 2410.
% 19.33/3.24
% 19.33/3.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------