%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM545+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:40:56 PM UTC 2026
% Result : Theorem 0.19s 0.64s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 11
% Syntax : Number of formulae : 57 ( 13 unt; 2 def)
% Number of atoms : 192 ( 29 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 223 ( 88 ~; 89 |; 32 &)
% ( 6 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 66 ( 60 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlseqdt0(W0,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,definition,
! [W0] :
( ( W0 != slcrc0
& isFinite0(W0)
& aSubsetOf0(W0,szNzAzT0) )
=> ! [W1] :
( W1 = szmzazxdt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
=> sdtlseqdt0(W2,W1) )
& aElementOf0(W1,W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
slbdtrb0(sz00) = slcrc0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(W0,W1)
<=> aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,hypothesis,
( isFinite0(xS)
& aSubsetOf0(xS,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,hypothesis,
( xS != slcrc0
=> aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,conjecture,
? [W0] :
( aSubsetOf0(xS,slbdtrb0(W0))
& aElementOf0(W0,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,negated_conjecture,
~ ? [W0] :
( aSubsetOf0(xS,slbdtrb0(W0))
& aElementOf0(W0,szNzAzT0) ),
inference(negated_conjecture,[status(cth)],[f57]) ).
fof(f83,plain,
! [W0] :
( ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f84,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f83]) ).
fof(f85,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f84]) ).
fof(f86,plain,
! [W0] :
( ( ! [W1] :
( ( ~ aElementOf0(sK1_skl(W1,W0),W0)
& aElementOf0(sK1_skl(W1,W0),W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f85]) ).
fof(f88,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f135,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f137,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f138,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f139,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f161,plain,
! [W0] :
( sdtlseqdt0(W0,W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f162,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f201,plain,
! [W0] :
( ! [W1] :
( W1 = szmzazxdt0(W0)
<=> ( ! [W2] :
( sdtlseqdt0(W2,W1)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) ) )
| W0 = slcrc0
| ~ isFinite0(W0)
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f202,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ sdtlseqdt0(W2,W1)
& aElementOf0(W2,W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzazxdt0(W0) )
& ( ( ! [W2] :
( sdtlseqdt0(W2,W1)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzazxdt0(W0) ) )
| W0 = slcrc0
| ~ isFinite0(W0)
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f201]) ).
fof(f203,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ sdtlseqdt0(W2,W1)
& aElementOf0(W2,W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzazxdt0(W0) )
& ! [W1] :
( ( ! [W2] :
( sdtlseqdt0(W2,W1)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzazxdt0(W0) ) )
| W0 = slcrc0
| ~ isFinite0(W0)
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(miniscoping,[status(thm)],[f202]) ).
fof(f204,plain,
! [W0] :
( ( ! [W1] :
( ( ~ sdtlseqdt0(sK7_skl(W1,W0),W1)
& aElementOf0(sK7_skl(W1,W0),W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzazxdt0(W0) )
& ! [W1] :
( ( ! [W2] :
( sdtlseqdt0(W2,W1)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzazxdt0(W0) ) )
| W0 = slcrc0
| ~ isFinite0(W0)
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(W2,sK7_skl(W1,W0))],[f203]) ).
fof(f205,plain,
! [X0,X1] :
( aElementOf0(X1,X0)
| X1 != szmzazxdt0(X0)
| X0 = slcrc0
| ~ isFinite0(X0)
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f224,plain,
slbdtrb0(sz00) = slcrc0,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f230,plain,
! [W0,W1] :
( ( sdtlseqdt0(W0,W1)
<=> aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1)) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f231,plain,
! [W0,W1] :
( ( ( ~ aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1))
| sdtlseqdt0(W0,W1) )
& ( aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1))
| ~ sdtlseqdt0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f230]) ).
fof(f232,plain,
! [X0,X1] :
( aSubsetOf0(slbdtrb0(X0),slbdtrb0(X1))
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f234,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f235,plain,
isFinite0(xS),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f236,plain,
( aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
| xS = slcrc0 ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f237,plain,
( aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
| xS = slcrc0 ),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f238,plain,
! [W0] :
( ~ aSubsetOf0(xS,slbdtrb0(W0))
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f58]) ).
fof(f239,plain,
! [X0] :
( ~ aSubsetOf0(xS,slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f261,plain,
! [X0] :
( aElementOf0(szmzazxdt0(X0),X0)
| X0 = slcrc0
| ~ isFinite0(X0)
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f205]) ).
fof(f272,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xS)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f88,f234]) ).
fof(f293,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xS) ),
inference(backward_subsumption_resolution,[status(thm)],[f272,f135]) ).
fof(f299,plain,
( ~ aSubsetOf0(xS,slcrc0)
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f224,f239]) ).
fof(f300,plain,
~ aSubsetOf0(xS,slcrc0),
inference(forward_subsumption_resolution,[status(thm)],[f299,f137]) ).
fof(f351,plain,
! [X0] :
( aSubsetOf0(slcrc0,slbdtrb0(X0))
| ~ sdtlseqdt0(sz00,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f224,f232]) ).
fof(f356,plain,
! [X0] :
( aSubsetOf0(slcrc0,slbdtrb0(X0))
| ~ sdtlseqdt0(sz00,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f351,f137]) ).
fof(f368,plain,
( aSubsetOf0(slcrc0,slcrc0)
| ~ sdtlseqdt0(sz00,sz00)
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f224,f356]) ).
fof(f371,plain,
( aSubsetOf0(slcrc0,slcrc0)
| ~ sdtlseqdt0(sz00,sz00) ),
inference(forward_subsumption_resolution,[status(thm)],[f368,f137]) ).
fof(f403,plain,
sdtlseqdt0(sz00,sz00),
inference(resolution,[status(thm)],[f162,f137]) ).
fof(f406,plain,
aSubsetOf0(slcrc0,slcrc0),
inference(backward_subsumption_resolution,[status(thm)],[f371,f403]) ).
fof(f905,plain,
( ~ aElementOf0(szszuzczcdt0(szmzazxdt0(xS)),szNzAzT0)
| xS = slcrc0 ),
inference(resolution,[status(thm)],[f237,f239]) ).
fof(f912,plain,
( ~ aElementOf0(szmzazxdt0(xS),szNzAzT0)
| xS = slcrc0 ),
inference(resolution,[status(thm)],[f905,f139]) ).
fof(f1041,plain,
( aElementOf0(szmzazxdt0(xS),szNzAzT0)
| xS = slcrc0
| ~ isFinite0(xS)
| ~ aSubsetOf0(xS,szNzAzT0) ),
inference(resolution,[status(thm)],[f261,f293]) ).
fof(f1059,plain,
( aElementOf0(szmzazxdt0(xS),szNzAzT0)
| xS = slcrc0
| ~ isFinite0(xS) ),
inference(forward_subsumption_resolution,[status(thm)],[f1041,f234]) ).
fof(f1065,plain,
xS = slcrc0,
inference(backward_subsumption_resolution,[status(thm)],[f912,f1066]) ).
fof(f1066,plain,
( aElementOf0(szmzazxdt0(xS),szNzAzT0)
| xS = slcrc0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1059,f235]) ).
fof(f1113,plain,
~ aSubsetOf0(slcrc0,slcrc0),
inference(backward_demodulation,[status(thm)],[f1065,f300]) ).
fof(f1128,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1113,f406]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM545+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n015.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 02:42:06 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.49 % Drodi V4.1.1
% 0.19/0.64 % Refutation found
% 0.19/0.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.27/0.69 % Elapsed time: 0.213020 seconds
% 0.27/0.69 % CPU time: 1.051374 seconds
% 0.27/0.69 % Total memory used: 117.270 MB
% 0.27/0.69 % Net memory used: 116.054 MB
%------------------------------------------------------------------------------