%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM544+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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.18s 10.65s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 3
% Syntax : Number of formulae : 27 ( 8 unt; 0 def)
% Number of atoms : 138 ( 6 equ)
% Maximal formula atoms : 15 ( 5 avg)
% Number of connectives : 169 ( 58 ~; 41 |; 53 &)
% ( 5 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-1 aty)
% Number of variables : 40 ( 32 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f32,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(W0,W1)
<=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,hypothesis,
( isFinite0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,szNzAzT0) )
& aSet0(xS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,conjecture,
( ~ ( xS = slcrc0
| ~ ? [W0] : aElementOf0(W0,xS) )
=> ( ( ! [W0] :
( aElementOf0(W0,xS)
=> sdtlseqdt0(W0,szmzazxdt0(xS)) )
& aElementOf0(szmzazxdt0(xS),xS) )
=> ( ( ! [W0] :
( aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
<=> ( sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))
& aElementOf0(W0,szNzAzT0) ) )
& aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) )
=> ( aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
| ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,negated_conjecture,
~ ( ~ ( xS = slcrc0
| ~ ? [W0] : aElementOf0(W0,xS) )
=> ( ( ! [W0] :
( aElementOf0(W0,xS)
=> sdtlseqdt0(W0,szmzazxdt0(xS)) )
& aElementOf0(szmzazxdt0(xS),xS) )
=> ( ( ! [W0] :
( aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
<=> ( sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))
& aElementOf0(W0,szNzAzT0) ) )
& aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) )
=> ( aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
| ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f154,plain,
! [W0,W1] :
( ( sdtlseqdt0(W0,W1)
<=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f155,plain,
! [W0,W1] :
( ( ( ~ sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1))
| sdtlseqdt0(W0,W1) )
& ( sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1))
| ~ sdtlseqdt0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f154]) ).
fof(f156,plain,
! [X0,X1] :
( sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1))
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f233,plain,
( isFinite0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f235,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f238,plain,
( ~ aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& ? [W0] :
( ~ aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& aElementOf0(W0,xS) )
& ! [W0] :
( aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
<=> ( sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))
& aElementOf0(W0,szNzAzT0) ) )
& aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& ! [W0] :
( sdtlseqdt0(W0,szmzazxdt0(xS))
| ~ aElementOf0(W0,xS) )
& aElementOf0(szmzazxdt0(xS),xS)
& xS != slcrc0
& ? [W0] : aElementOf0(W0,xS) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f239,plain,
( ~ aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& ? [W0] :
( ~ aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& aElementOf0(W0,xS) )
& ! [W0] :
( ( ~ sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))
| ~ aElementOf0(W0,szNzAzT0)
| aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) )
& ( ( sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))
& aElementOf0(W0,szNzAzT0) )
| ~ aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ) )
& aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& ! [W0] :
( sdtlseqdt0(W0,szmzazxdt0(xS))
| ~ aElementOf0(W0,xS) )
& aElementOf0(szmzazxdt0(xS),xS)
& xS != slcrc0
& ? [W0] : aElementOf0(W0,xS) ),
inference(NNF_transformation,[status(thm)],[f238]) ).
fof(f240,plain,
( ~ aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& ? [W0] :
( ~ aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& aElementOf0(W0,xS) )
& ! [W0] :
( ~ sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))
| ~ aElementOf0(W0,szNzAzT0)
| aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) )
& ! [W0] :
( ( sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))
& aElementOf0(W0,szNzAzT0) )
| ~ aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) )
& aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& ! [W0] :
( sdtlseqdt0(W0,szmzazxdt0(xS))
| ~ aElementOf0(W0,xS) )
& aElementOf0(szmzazxdt0(xS),xS)
& xS != slcrc0
& ? [W0] : aElementOf0(W0,xS) ),
inference(miniscoping,[status(thm)],[f239]) ).
fof(f241,plain,
( ~ aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& ~ aElementOf0(sK10_skl,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& aElementOf0(sK10_skl,xS)
& ! [W0] :
( ~ sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))
| ~ aElementOf0(W0,szNzAzT0)
| aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) )
& ! [W0] :
( ( sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))
& aElementOf0(W0,szNzAzT0) )
| ~ aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) )
& aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
& ! [W0] :
( sdtlseqdt0(W0,szmzazxdt0(xS))
| ~ aElementOf0(W0,xS) )
& aElementOf0(szmzazxdt0(xS),xS)
& xS != slcrc0
& aElementOf0(sK9_skl,xS) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl]),skolemize(W0,sK9_skl),skolemize(W0,sK10_skl)],[f240]) ).
fof(f244,plain,
aElementOf0(szmzazxdt0(xS),xS),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f245,plain,
! [X0] :
( sdtlseqdt0(X0,szmzazxdt0(xS))
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f249,plain,
! [X0] :
( ~ sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(szmzazxdt0(xS)))
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f250,plain,
aElementOf0(sK10_skl,xS),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f251,plain,
~ aElementOf0(sK10_skl,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f266,plain,
aElementOf0(szmzazxdt0(xS),szNzAzT0),
inference(resolution,[status(thm)],[f235,f244]) ).
fof(f267,plain,
aElementOf0(sK10_skl,szNzAzT0),
inference(resolution,[status(thm)],[f235,f250]) ).
fof(f460,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
| ~ sdtlseqdt0(X0,szmzazxdt0(xS))
| ~ aElementOf0(szmzazxdt0(xS),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f156,f249]) ).
fof(f465,plain,
! [X0] :
( aElementOf0(X0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
| ~ sdtlseqdt0(X0,szmzazxdt0(xS))
| ~ aElementOf0(szmzazxdt0(xS),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(duplicate_literals_removal,[status(thm)],[f460]) ).
fof(f466,plain,
! [X0] :
( aElementOf0(X0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))
| ~ sdtlseqdt0(X0,szmzazxdt0(xS))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f465,f266]) ).
fof(f647,plain,
( ~ sdtlseqdt0(sK10_skl,szmzazxdt0(xS))
| ~ aElementOf0(sK10_skl,szNzAzT0) ),
inference(resolution,[status(thm)],[f251,f466]) ).
fof(f649,plain,
~ sdtlseqdt0(sK10_skl,szmzazxdt0(xS)),
inference(forward_subsumption_resolution,[status(thm)],[f647,f267]) ).
fof(f651,plain,
~ aElementOf0(sK10_skl,xS),
inference(resolution,[status(thm)],[f649,f245]) ).
fof(f652,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f651,f250]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM544+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/10.40 % Computer : n004.cluster.edu
% 0.15/10.40 % Model : x86_64 x86_64
% 0.15/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/10.40 % Memory : 8046.5625MB
% 0.15/10.40 % OS : Linux 6.8.0-71-generic
% 0.15/10.40 % CPULimit : 300
% 0.15/10.40 % WCLimit : 300
% 0.15/10.40 % DateTime : Mon Sep 21 02:39:01 UTC 2026
% 0.15/10.40 % CPUTime :
% 0.15/10.42 % Drodi V4.1.1
% 0.18/10.65 % Refutation found
% 0.18/10.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/10.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.18/10.67 % Elapsed time: 0.245924 seconds
% 0.18/10.67 % CPU time: 1.686905 seconds
% 0.18/10.67 % Total memory used: 126.058 MB
% 0.18/10.67 % Net memory used: 124.414 MB
%------------------------------------------------------------------------------