%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM610+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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:41:11 PM UTC 2026
% Result : Theorem 0.10s 0.40s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 14
% Syntax : Number of formulae : 50 ( 13 unt; 7 def)
% Number of atoms : 145 ( 1 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 164 ( 69 ~; 66 |; 17 &)
% ( 8 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 7 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 42 ( 40 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [W0,W1,W2] :
( ( aSet0(W2)
& aSet0(W1)
& aSet0(W0) )
=> ( ( aSubsetOf0(W1,W2)
& aSubsetOf0(W0,W1) )
=> aSubsetOf0(W0,W2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,hypothesis,
aSubsetOf0(xO,xS),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,hypothesis,
( xQ != slcrc0
& aSubsetOf0(xQ,xO) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,hypothesis,
aSubsetOf0(xP,xQ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,conjecture,
aSubsetOf0(xP,xO),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,negated_conjecture,
~ aSubsetOf0(xP,xO),
inference(negated_conjecture,[status(cth)],[f108]) ).
fof(f134,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(f135,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)],[f134]) ).
fof(f136,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)],[f135]) ).
fof(f137,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))],[f136]) ).
fof(f138,plain,
! [X0,X1] :
( aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f148,plain,
! [W0,W1,W2] :
( aSubsetOf0(W0,W2)
| ~ aSubsetOf0(W1,W2)
| ~ aSubsetOf0(W0,W1)
| ~ aSet0(W2)
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f149,plain,
! [X0,X1,X2] :
( aSubsetOf0(X0,X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f186,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f369,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f439,plain,
aSubsetOf0(xO,xS),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f441,plain,
aSubsetOf0(xQ,xO),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f450,plain,
aSubsetOf0(xP,xQ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f451,plain,
~ aSubsetOf0(xP,xO),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f518,plain,
! [X0,X1,X2] :
( aSubsetOf0(X2,X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X2,X0)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f149,f138]) ).
fof(f527,definition,
( sQ5_spl
<=> aSet0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f529,plain,
( sQ5_spl
| ~ aSet0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f527]) ).
fof(f534,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f529,f186]) ).
fof(f535,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f534]) ).
fof(f801,plain,
( aSet0(xS)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f369,f138]) ).
fof(f835,definition,
( sQ44_spl
<=> aSet0(xS) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f838,plain,
( sQ44_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f801,f527,f835]) ).
fof(f953,plain,
! [X0] :
( aSubsetOf0(xO,X0)
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(X0)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f439,f518]) ).
fof(f972,definition,
! [X0] :
( sQ54_spl
<=> ( aSubsetOf0(xO,X0)
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f973,plain,
! [X0] :
( ~ sQ54_spl
| aSubsetOf0(xO,X0)
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f972]) ).
fof(f975,plain,
( sQ54_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f953,f835,f972]) ).
fof(f983,definition,
( sQ57_spl
<=> aSet0(xO) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1049,plain,
( ~ sQ54_spl
| aSubsetOf0(xO,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f973,f369]) ).
fof(f1051,definition,
( sQ63_spl
<=> aSubsetOf0(xO,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1052,plain,
( ~ sQ63_spl
| aSubsetOf0(xO,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1051]) ).
fof(f1054,plain,
( ~ sQ54_spl
| sQ63_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1049,f527,f1051,f972]) ).
fof(f1062,plain,
( ~ sQ63_spl
| aSet0(xO)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f1052,f138]) ).
fof(f1075,plain,
( ~ sQ63_spl
| sQ57_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1062,f527,f983,f1051]) ).
fof(f1120,plain,
! [X0,X1,X2] :
( aSubsetOf0(X1,X0)
| ~ aSubsetOf0(X2,X0)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f518,f138]) ).
fof(f1122,plain,
! [X0] :
( aSubsetOf0(X0,xO)
| ~ aSubsetOf0(X0,xQ)
| ~ aSet0(xO) ),
inference(resolution,[status(thm)],[f1120,f441]) ).
fof(f1132,definition,
! [X0] :
( sQ71_spl
<=> ( aSubsetOf0(X0,xO)
| ~ aSubsetOf0(X0,xQ) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1133,plain,
! [X0] :
( ~ sQ71_spl
| aSubsetOf0(X0,xO)
| ~ aSubsetOf0(X0,xQ) ),
inference(component_clause,[status(thm)],[f1132]) ).
fof(f1135,plain,
( sQ71_spl
| ~ sQ57_spl ),
inference(split_clause,[status(thm)],[f1122,f983,f1132]) ).
fof(f1157,plain,
( ~ sQ71_spl
| aSubsetOf0(xP,xO) ),
inference(resolution,[status(thm)],[f1133,f450]) ).
fof(f1159,plain,
( ~ sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1157,f451]) ).
fof(f1160,plain,
~ sQ71_spl,
inference(contradiction_clause,[status(thm)],[f1159]) ).
fof(f1161,plain,
$false,
inference(sat_refutation,[status(thm)],[f535,f838,f975,f1054,f1075,f1135,f1160]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM610+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:47:35 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.40 % Refutation found
% 0.10/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.43 % Elapsed time: 0.058823 seconds
% 0.10/0.43 % CPU time: 0.169436 seconds
% 0.10/0.43 % Total memory used: 46.007 MB
% 0.10/0.43 % Net memory used: 45.869 MB
%------------------------------------------------------------------------------