%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM611+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 : Thu Sep 24 01:41:11 PM UTC 2026
% Result : Theorem 2.97s 0.83s
% Output : CNFRefutation 2.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 11
% Syntax : Number of formulae : 58 ( 20 unt; 0 def)
% Number of atoms : 178 ( 42 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 191 ( 71 ~; 64 |; 41 &)
% ( 4 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 40 ( 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [W0] :
( ( isFinite0(W0)
& aSet0(W0) )
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> isFinite0(W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( szszuzczcdt0(W0) = szszuzczcdt0(W1)
=> W0 = W1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [W0] :
( aSet0(W0)
=> ( aElementOf0(sbrdtbr0(W0),szNzAzT0)
<=> isFinite0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( ( aElementOf0(W1,W0)
& isFinite0(W0) )
=> szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,hypothesis,
aElementOf0(xK,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,hypothesis,
( aElementOf0(xQ,slbdtsldtrb0(xO,xK))
& sbrdtbr0(xQ) = xK
& aSubsetOf0(xQ,xO)
& ! [W0] :
( aElementOf0(W0,xQ)
=> aElementOf0(W0,xO) )
& aSet0(xQ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,hypothesis,
( xp = szmzizndt0(xQ)
& ! [W0] :
( aElementOf0(W0,xQ)
=> sdtlseqdt0(xp,W0) )
& aElementOf0(xp,xQ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,hypothesis,
( 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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,hypothesis,
( aSubsetOf0(xP,xQ)
& ! [W0] :
( aElementOf0(W0,xP)
=> aElementOf0(W0,xQ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,conjecture,
sbrdtbr0(xP) = xk,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f110,negated_conjecture,
sbrdtbr0(xP) != xk,
inference(negated_conjecture,[status(cth)],[f109]) ).
fof(f143,plain,
! [W0] :
( ! [W1] :
( isFinite0(W1)
| ~ aSubsetOf0(W1,W0) )
| ~ isFinite0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f144,plain,
! [X0,X1] :
( isFinite0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f193,plain,
! [W0,W1] :
( W0 = W1
| szszuzczcdt0(W0) != szszuzczcdt0(W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f194,plain,
! [X0,X1] :
( X0 = X1
| szszuzczcdt0(X0) != szszuzczcdt0(X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f227,plain,
! [W0] :
( ( aElementOf0(sbrdtbr0(W0),szNzAzT0)
<=> isFinite0(W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f228,plain,
! [W0] :
( ( ( ~ isFinite0(W0)
| aElementOf0(sbrdtbr0(W0),szNzAzT0) )
& ( isFinite0(W0)
| ~ aElementOf0(sbrdtbr0(W0),szNzAzT0) ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f227]) ).
fof(f229,plain,
! [X0] :
( isFinite0(X0)
| ~ aElementOf0(sbrdtbr0(X0),szNzAzT0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f230,plain,
! [X0] :
( ~ isFinite0(X0)
| aElementOf0(sbrdtbr0(X0),szNzAzT0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f237,plain,
! [W0] :
( ! [W1] :
( szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0)
| ~ aElementOf0(W1,W0)
| ~ isFinite0(W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f238,plain,
! [X0,X1] :
( szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1))) = sbrdtbr0(X0)
| ~ aElementOf0(X1,X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f369,plain,
aElementOf0(xK,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f405,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f406,plain,
szszuzczcdt0(xk) = xK,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f598,plain,
( aElementOf0(xQ,slbdtsldtrb0(xO,xK))
& sbrdtbr0(xQ) = xK
& aSubsetOf0(xQ,xO)
& ! [W0] :
( aElementOf0(W0,xO)
| ~ aElementOf0(W0,xQ) )
& aSet0(xQ) ),
inference(pre_NNF_transformation,[status(thm)],[f99]) ).
fof(f599,plain,
aSet0(xQ),
inference(cnf_transformation,[status(thm)],[f598]) ).
fof(f602,plain,
sbrdtbr0(xQ) = xK,
inference(cnf_transformation,[status(thm)],[f598]) ).
fof(f618,plain,
( xp = szmzizndt0(xQ)
& ! [W0] :
( sdtlseqdt0(xp,W0)
| ~ aElementOf0(W0,xQ) )
& aElementOf0(xp,xQ) ),
inference(pre_NNF_transformation,[status(thm)],[f103]) ).
fof(f619,plain,
aElementOf0(xp,xQ),
inference(cnf_transformation,[status(thm)],[f618]) ).
fof(f621,plain,
xp = szmzizndt0(xQ),
inference(cnf_transformation,[status(thm)],[f618]) ).
fof(f622,plain,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& ! [W0] :
( aElementOf0(W0,xP)
<=> ( W0 != szmzizndt0(xQ)
& aElementOf0(W0,xQ)
& aElement0(W0) ) )
& ! [W0] :
( sdtlseqdt0(szmzizndt0(xQ),W0)
| ~ aElementOf0(W0,xQ) )
& aSet0(xP) ),
inference(pre_NNF_transformation,[status(thm)],[f104]) ).
fof(f623,plain,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& ! [W0] :
( ( W0 = szmzizndt0(xQ)
| ~ aElementOf0(W0,xQ)
| ~ aElement0(W0)
| aElementOf0(W0,xP) )
& ( ( W0 != szmzizndt0(xQ)
& aElementOf0(W0,xQ)
& aElement0(W0) )
| ~ aElementOf0(W0,xP) ) )
& ! [W0] :
( sdtlseqdt0(szmzizndt0(xQ),W0)
| ~ aElementOf0(W0,xQ) )
& aSet0(xP) ),
inference(NNF_transformation,[status(thm)],[f622]) ).
fof(f624,plain,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& ! [W0] :
( W0 = szmzizndt0(xQ)
| ~ aElementOf0(W0,xQ)
| ~ aElement0(W0)
| aElementOf0(W0,xP) )
& ! [W0] :
( ( W0 != szmzizndt0(xQ)
& aElementOf0(W0,xQ)
& aElement0(W0) )
| ~ aElementOf0(W0,xP) )
& ! [W0] :
( sdtlseqdt0(szmzizndt0(xQ),W0)
| ~ aElementOf0(W0,xQ) )
& aSet0(xP) ),
inference(miniscoping,[status(thm)],[f623]) ).
fof(f625,plain,
aSet0(xP),
inference(cnf_transformation,[status(thm)],[f624]) ).
fof(f631,plain,
xP = sdtmndt0(xQ,szmzizndt0(xQ)),
inference(cnf_transformation,[status(thm)],[f624]) ).
fof(f636,plain,
( aSubsetOf0(xP,xQ)
& ! [W0] :
( aElementOf0(W0,xQ)
| ~ aElementOf0(W0,xP) ) ),
inference(pre_NNF_transformation,[status(thm)],[f107]) ).
fof(f638,plain,
aSubsetOf0(xP,xQ),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f642,plain,
sbrdtbr0(xP) != xk,
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f1063,plain,
( isFinite0(xP)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(resolution,[status(thm)],[f144,f638]) ).
fof(f1066,plain,
( isFinite0(xP)
| ~ isFinite0(xQ) ),
inference(forward_subsumption_resolution,[status(thm)],[f1063,f599]) ).
fof(f1144,plain,
xP = sdtmndt0(xQ,xp),
inference(backward_demodulation,[status(thm)],[f621,f631]) ).
fof(f2092,plain,
! [X0] :
( xk = X0
| xK != szszuzczcdt0(X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f406,f194]) ).
fof(f2095,plain,
! [X0] :
( xk = X0
| xK != szszuzczcdt0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2092,f405]) ).
fof(f2538,plain,
( isFinite0(xQ)
| ~ aElementOf0(xK,szNzAzT0)
| ~ aSet0(xQ) ),
inference(paramodulation,[status(thm)],[f602,f229]) ).
fof(f2539,plain,
( isFinite0(xQ)
| ~ aElementOf0(xK,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2538,f599]) ).
fof(f2702,plain,
isFinite0(xP),
inference(backward_subsumption_resolution,[status(thm)],[f1066,f2703]) ).
fof(f2703,plain,
isFinite0(xQ),
inference(forward_subsumption_resolution,[status(thm)],[f2539,f369]) ).
fof(f2744,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ)
| ~ aElementOf0(xp,xQ)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(paramodulation,[status(thm)],[f1144,f238]) ).
fof(f2745,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = xK
| ~ aElementOf0(xp,xQ)
| ~ isFinite0(xQ)
| ~ aSet0(xQ) ),
inference(forward_demodulation,[status(thm)],[f602,f2744]) ).
fof(f2746,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = xK
| ~ aElementOf0(xp,xQ)
| ~ isFinite0(xQ) ),
inference(forward_subsumption_resolution,[status(thm)],[f2745,f599]) ).
fof(f2785,plain,
( szszuzczcdt0(sbrdtbr0(xP)) = xK
| ~ aElementOf0(xp,xQ) ),
inference(forward_subsumption_resolution,[status(thm)],[f2746,f2703]) ).
fof(f2786,plain,
( xk = sbrdtbr0(xP)
| ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| ~ aElementOf0(xp,xQ) ),
inference(resolution,[status(thm)],[f2785,f2095]) ).
fof(f2787,plain,
( xk = sbrdtbr0(xP)
| ~ aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2786,f619]) ).
fof(f2788,plain,
~ aElementOf0(sbrdtbr0(xP),szNzAzT0),
inference(forward_subsumption_resolution,[status(thm)],[f2787,f642]) ).
fof(f2789,plain,
( ~ isFinite0(xP)
| ~ aSet0(xP) ),
inference(resolution,[status(thm)],[f2788,f230]) ).
fof(f2790,plain,
~ isFinite0(xP),
inference(forward_subsumption_resolution,[status(thm)],[f2789,f625]) ).
fof(f2791,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2790,f2702]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM611+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 02:44:39 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 2.97/0.83 % Refutation found
% 2.97/0.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.97/0.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.97/0.87 % Elapsed time: 0.496527 seconds
% 2.97/0.87 % CPU time: 3.472231 seconds
% 2.97/0.87 % Total memory used: 165.435 MB
% 2.97/0.87 % Net memory used: 161.377 MB
%------------------------------------------------------------------------------