%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU326+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 02:20:11 PM UTC 2026
% Result : Theorem 0.14s 0.44s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 12
% Syntax : Number of formulae : 60 ( 4 unt; 8 def)
% Number of atoms : 152 ( 50 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 163 ( 71 ~; 60 |; 19 &)
% ( 8 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 39 ( 35 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f167,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> element(complements_of_subsets(A,B),powerset(powerset(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f258,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> complements_of_subsets(A,complements_of_subsets(A,B)) = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f360,conjecture,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ( ~ ( B = empty_set
& complements_of_subsets(A,B) != empty_set )
& ~ ( complements_of_subsets(A,B) = empty_set
& B != empty_set ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f361,negated_conjecture,
~ ! [A,B] :
( element(B,powerset(powerset(A)))
=> ( ~ ( B = empty_set
& complements_of_subsets(A,B) != empty_set )
& ~ ( complements_of_subsets(A,B) = empty_set
& B != empty_set ) ) ),
inference(negated_conjecture,[status(cth)],[f360]) ).
fof(f476,lemma,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ~ ( complements_of_subsets(A,B) = empty_set
& B != empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1274,plain,
! [A,B] :
( element(complements_of_subsets(A,B),powerset(powerset(A)))
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f167]) ).
fof(f1275,plain,
! [X0,X1] :
( element(complements_of_subsets(X1,X0),powerset(powerset(X1)))
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f1274]) ).
fof(f1542,plain,
! [A,B] :
( complements_of_subsets(A,complements_of_subsets(A,B)) = B
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f258]) ).
fof(f1543,plain,
! [X0,X1] :
( complements_of_subsets(X1,complements_of_subsets(X1,X0)) = X0
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f1542]) ).
fof(f2155,plain,
? [A,B] :
( ( ( B = empty_set
& complements_of_subsets(A,B) != empty_set )
| ( complements_of_subsets(A,B) = empty_set
& B != empty_set ) )
& element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f361]) ).
fof(f2156,definition,
! [A,B] :
( sP24_prd(B,A)
<=> ( complements_of_subsets(A,B) = empty_set
& B != empty_set ) ),
introduced(definition,[new_symbols(definition,[sP24_prd])],[]) ).
fof(f2157,plain,
? [A,B] :
( ( ( B = empty_set
& complements_of_subsets(A,B) != empty_set )
| sP24_prd(B,A) )
& element(B,powerset(powerset(A))) ),
inference(formula_renaming,[status(thm)],[f2155,f2156]) ).
fof(f2158,plain,
( ( ( sK277_skl = empty_set
& complements_of_subsets(sK276_skl,sK277_skl) != empty_set )
| sP24_prd(sK277_skl,sK276_skl) )
& element(sK277_skl,powerset(powerset(sK276_skl))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK276_skl,sK277_skl]),skolemize(A,sK276_skl),skolemize(B,sK277_skl)],[f2157]) ).
fof(f2159,plain,
element(sK277_skl,powerset(powerset(sK276_skl))),
inference(cnf_transformation,[status(thm)],[f2158]) ).
fof(f2160,plain,
( complements_of_subsets(sK276_skl,sK277_skl) != empty_set
| sP24_prd(sK277_skl,sK276_skl) ),
inference(cnf_transformation,[status(thm)],[f2158]) ).
fof(f2161,plain,
( sK277_skl = empty_set
| sP24_prd(sK277_skl,sK276_skl) ),
inference(cnf_transformation,[status(thm)],[f2158]) ).
fof(f2544,plain,
! [A,B] :
( complements_of_subsets(A,B) != empty_set
| B = empty_set
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f476]) ).
fof(f2545,plain,
! [X0,X1] :
( complements_of_subsets(X1,X0) != empty_set
| X0 = empty_set
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f2544]) ).
fof(f3068,plain,
! [A,B] :
( ( complements_of_subsets(A,B) != empty_set
| B = empty_set
| sP24_prd(B,A) )
& ( ( complements_of_subsets(A,B) = empty_set
& B != empty_set )
| ~ sP24_prd(B,A) ) ),
inference(NNF_transformation,[status(thm)],[f2156]) ).
fof(f3069,plain,
( ! [A,B] :
( complements_of_subsets(A,B) != empty_set
| B = empty_set
| sP24_prd(B,A) )
& ! [A,B] :
( ( complements_of_subsets(A,B) = empty_set
& B != empty_set )
| ~ sP24_prd(B,A) ) ),
inference(miniscoping,[status(thm)],[f3068]) ).
fof(f3070,plain,
! [X0,X1] :
( X0 != empty_set
| ~ sP24_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3069]) ).
fof(f3071,plain,
! [X0,X1] :
( complements_of_subsets(X1,X0) = empty_set
| ~ sP24_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3069]) ).
fof(f3253,definition,
( sQ31_spl
<=> sP24_prd(sK277_skl,sK276_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f3254,plain,
( ~ sQ31_spl
| sP24_prd(sK277_skl,sK276_skl) ),
inference(component_clause,[status(thm)],[f3253]) ).
fof(f3256,definition,
( sQ32_spl
<=> complements_of_subsets(sK276_skl,sK277_skl) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f3258,plain,
( sQ32_spl
| complements_of_subsets(sK276_skl,sK277_skl) != empty_set ),
inference(component_clause,[status(thm)],[f3256]) ).
fof(f3259,plain,
( ~ sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f2160,f3253,f3256]) ).
fof(f3260,definition,
( sQ33_spl
<=> sK277_skl = empty_set ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f3261,plain,
( ~ sQ33_spl
| sK277_skl = empty_set ),
inference(component_clause,[status(thm)],[f3260]) ).
fof(f3263,plain,
( sQ33_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f2161,f3253,f3260]) ).
fof(f3593,plain,
! [X0] : ~ sP24_prd(empty_set,X0),
inference(destructive_equality_resolution,[status(thm)],[f3070]) ).
fof(f3608,plain,
( ~ sQ31_spl
| complements_of_subsets(sK276_skl,sK277_skl) = empty_set ),
inference(resolution,[status(thm)],[f3071,f3254]) ).
fof(f3610,definition,
( sQ64_spl
<=> element(sK277_skl,powerset(powerset(sK276_skl))) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f3612,plain,
( sQ64_spl
| ~ element(sK277_skl,powerset(powerset(sK276_skl))) ),
inference(component_clause,[status(thm)],[f3610]) ).
fof(f3613,definition,
( sQ65_spl
<=> element(empty_set,powerset(powerset(sK276_skl))) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f3615,plain,
( sQ65_spl
| ~ element(empty_set,powerset(powerset(sK276_skl))) ),
inference(component_clause,[status(thm)],[f3613]) ).
fof(f3644,plain,
( ~ sQ33_spl
| element(empty_set,powerset(powerset(sK276_skl))) ),
inference(backward_demodulation,[status(thm)],[f3261,f2159]) ).
fof(f3648,plain,
( sQ65_spl
| ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3615,f3644]) ).
fof(f3649,plain,
( sQ65_spl
| ~ sQ33_spl ),
inference(contradiction_clause,[status(thm)],[f3648]) ).
fof(f3659,plain,
( ~ sQ31_spl
| sK277_skl = empty_set
| ~ element(sK277_skl,powerset(powerset(sK276_skl))) ),
inference(resolution,[status(thm)],[f2545,f3608]) ).
fof(f3661,plain,
( ~ sQ31_spl
| sQ33_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f3659,f3610,f3260,f3253]) ).
fof(f3664,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2159,f3612]) ).
fof(f3665,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f3664]) ).
fof(f3667,plain,
( sQ32_spl
| ~ sQ33_spl
| complements_of_subsets(sK276_skl,empty_set) != empty_set ),
inference(forward_demodulation,[status(thm)],[f3261,f3258]) ).
fof(f3673,plain,
( ~ sQ33_spl
| element(empty_set,powerset(powerset(sK276_skl))) ),
inference(forward_demodulation,[status(thm)],[f3261,f2159]) ).
fof(f3676,plain,
( ~ sQ33_spl
| complements_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,empty_set)) = empty_set ),
inference(resolution,[status(thm)],[f3673,f1543]) ).
fof(f3686,plain,
( ~ sQ33_spl
| complements_of_subsets(sK276_skl,empty_set) = empty_set
| ~ element(complements_of_subsets(sK276_skl,empty_set),powerset(powerset(sK276_skl))) ),
inference(resolution,[status(thm)],[f3676,f2545]) ).
fof(f3691,definition,
( sQ69_spl
<=> element(complements_of_subsets(sK276_skl,empty_set),powerset(powerset(sK276_skl))) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f3693,plain,
( sQ69_spl
| ~ element(complements_of_subsets(sK276_skl,empty_set),powerset(powerset(sK276_skl))) ),
inference(component_clause,[status(thm)],[f3691]) ).
fof(f3694,definition,
( sQ70_spl
<=> complements_of_subsets(sK276_skl,empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f3695,plain,
( ~ sQ70_spl
| complements_of_subsets(sK276_skl,empty_set) = empty_set ),
inference(component_clause,[status(thm)],[f3694]) ).
fof(f3697,plain,
( ~ sQ33_spl
| sQ70_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f3686,f3691,f3694,f3260]) ).
fof(f3705,plain,
( ~ sQ70_spl
| sQ32_spl
| ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3695,f3667]) ).
fof(f3706,plain,
( ~ sQ70_spl
| sQ32_spl
| ~ sQ33_spl ),
inference(contradiction_clause,[status(thm)],[f3705]) ).
fof(f3708,plain,
( sQ69_spl
| ~ element(empty_set,powerset(powerset(sK276_skl))) ),
inference(resolution,[status(thm)],[f3693,f1275]) ).
fof(f3710,plain,
( sQ69_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f3708,f3613,f3691]) ).
fof(f3715,plain,
( ~ sQ31_spl
| ~ sQ33_spl
| sP24_prd(empty_set,sK276_skl) ),
inference(forward_demodulation,[status(thm)],[f3261,f3254]) ).
fof(f3716,plain,
( ~ sQ31_spl
| ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3715,f3593]) ).
fof(f3717,plain,
( ~ sQ31_spl
| ~ sQ33_spl ),
inference(contradiction_clause,[status(thm)],[f3716]) ).
fof(f3718,plain,
$false,
inference(sat_refutation,[status(thm)],[f3259,f3263,f3649,f3661,f3665,f3697,f3706,f3710,f3717]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU326+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n011.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 06:11:55 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.40 % Drodi V4.1.1
% 0.14/0.44 % Refutation found
% 0.14/0.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.47 % Elapsed time: 0.100426 seconds
% 0.14/0.47 % CPU time: 0.408096 seconds
% 0.14/0.47 % Total memory used: 166.896 MB
% 0.14/0.47 % Net memory used: 165.937 MB
%------------------------------------------------------------------------------