%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM571+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 : n018.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:26 AM UTC 2026
% Result : Theorem 37.04s 11.06s
% Output : CNFRefutation 37.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 4
% Syntax : Number of formulae : 21 ( 7 unt; 0 def)
% Number of atoms : 70 ( 15 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 60 ( 11 ~; 12 |; 26 &)
% ( 1 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 10 ( 0 sgn 9 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__3435,axiom,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,szNzAzT0) )
& aSet0(xS) ),
file('theBenchmark.p',m__3435) ).
fof(m__3623,axiom,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ( isCountable0(sdtlpdtrp0(xN,W0))
& ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
| ( ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> aElementOf0(W1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,W0)) ) ) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
=> aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
file('theBenchmark.p',m__3623) ).
fof(m__3702_02,axiom,
( xi != sz00
=> ( isCountable0(sdtlpdtrp0(xN,xi))
& aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> aElementOf0(W0,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,xi))
& ? [W0] :
( szszuzczcdt0(W0) = xi
& aElementOf0(W0,szNzAzT0) ) ) ),
file('theBenchmark.p',m__3702_02) ).
fof(m__,conjecture,
( isCountable0(sdtlpdtrp0(xN,xi))
& ( aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
| ( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> aElementOf0(W0,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,xi)) ) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( isCountable0(sdtlpdtrp0(xN,xi))
& ( aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
| ( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> aElementOf0(W0,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,xi)) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_1027,negated_conjecture,
( ~ isCountable0(sdtlpdtrp0(xN,xi))
| ~ aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_1030,plain,
( isCountable0(sdtlpdtrp0(xN,xi))
| xi = sz00 ),
inference(clausify,[status(thm)],[m__3702_02]) ).
cnf(c_1031,plain,
( isCountable0(sdtlpdtrp0(xN,xi))
| sz00 = xi ),
inference(copy,[status(thm)],[c_1030]) ).
cnf(c_1032,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
| xi = sz00 ),
inference(clausify,[status(thm)],[m__3702_02]) ).
cnf(c_1033,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
| sz00 = xi ),
inference(copy,[status(thm)],[c_1032]) ).
cnf(c_1080,plain,
sdtlpdtrp0(xN,sz00) = xS,
inference(clausify,[status(thm)],[m__3623]) ).
cnf(c_1307,plain,
isCountable0(xS),
inference(clausify,[status(thm)],[m__3435]) ).
cnf(c_1308,plain,
aSubsetOf0(xS,szNzAzT0),
inference(clausify,[status(thm)],[m__3435]) ).
cnf(c_7654,negated_conjecture,
( sz00 = xi
| ~ isCountable0(sdtlpdtrp0(xN,xi)) ),
inference(resolve,[status(thm)],[c_1027,c_1033]) ).
cnf(c_7655,negated_conjecture,
( sz00 = xi
| sz00 = xi ),
inference(resolve,[status(thm)],[c_7654,c_1031]) ).
cnf(c_7638,negated_conjecture,
sz00 = xi,
inference(copy,[status(thm)],[c_7655]) ).
cnf(c_7650,plain,
sdtlpdtrp0(xN,xi) = xS,
inference(paramod,[status(thm)],[c_7638,c_1080]) ).
cnf(c_7656,negated_conjecture,
( ~ isCountable0(sdtlpdtrp0(xN,xi))
| ~ aSubsetOf0(xS,szNzAzT0) ),
inference(paramod,[status(thm)],[c_7650,c_1027]) ).
cnf(c_7657,negated_conjecture,
( ~ isCountable0(xS)
| ~ aSubsetOf0(xS,szNzAzT0) ),
inference(paramod,[status(thm)],[c_7650,c_7656]) ).
cnf(c_7658,negated_conjecture,
~ isCountable0(xS),
inference(resolve,[status(thm)],[c_1308,c_7657]) ).
cnf(c_7653,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1307,c_7658]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM571+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/5.64 % Computer : n018.cluster.edu
% 0.15/5.64 % Model : x86_64 x86_64
% 0.15/5.64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.64 % Memory : 8046.5625MB
% 0.15/5.64 % OS : Linux 6.8.0-71-generic
% 0.15/5.64 % CPULimit : 300
% 0.15/5.64 % WCLimit : 300
% 0.15/5.64 % DateTime : Sat Sep 26 03:18:58 UTC 2026
% 0.15/5.65 % CPUTime :
% 0.15/5.65 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/5.65 % Process 3588097 was started by sandbox2 on n018,
% 0.15/5.65 % Sat Sep 26 03:18:58 2026
% 0.15/5.65 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.21/5.75
% 0.21/5.75 % From the command line: assign(max_seconds, 300).
% 37.04/11.06
% 37.04/11.06 % SZS status Theorem for theBenchmark
% 37.04/11.06
% 37.04/11.06 % Proof 1 at 5.06 (+ 0.18) seconds.
% 37.04/11.06 % Length of proof is 15.
% 37.04/11.06 % Level of proof is 5.
% 37.04/11.06 % Maximum clause weight is 19.000.
% 37.04/11.06 % Given clauses 446.
% 37.04/11.06
% 37.04/11.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------