%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU328+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 : n008.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.38s 0.98s
% Output : CNFRefutation 0.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 11
% Syntax : Number of formulae : 48 ( 10 unt; 4 def)
% Number of atoms : 102 ( 45 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 96 ( 42 ~; 31 |; 8 &)
% ( 4 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 5 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 44 ( 42 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f160,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> element(union_of_subsets(A,B),powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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(f256,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,subset_complement(A,B)) = B ),
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,lemma,
! [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(f369,lemma,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ( B != empty_set
=> meet_of_subsets(A,complements_of_subsets(A,B)) = subset_complement(A,union_of_subsets(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f372,conjecture,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ( B != empty_set
=> union_of_subsets(A,complements_of_subsets(A,B)) = subset_complement(A,meet_of_subsets(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f373,negated_conjecture,
~ ! [A,B] :
( element(B,powerset(powerset(A)))
=> ( B != empty_set
=> union_of_subsets(A,complements_of_subsets(A,B)) = subset_complement(A,meet_of_subsets(A,B)) ) ),
inference(negated_conjecture,[status(cth)],[f372]) ).
fof(f1262,plain,
! [A,B] :
( element(union_of_subsets(A,B),powerset(A))
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f160]) ).
fof(f1263,plain,
! [X0,X1] :
( element(union_of_subsets(X1,X0),powerset(X1))
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f1262]) ).
fof(f1276,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(f1277,plain,
! [X0,X1] :
( element(complements_of_subsets(X1,X0),powerset(powerset(X1)))
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f1276]) ).
fof(f1540,plain,
! [A,B] :
( subset_complement(A,subset_complement(A,B)) = B
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f256]) ).
fof(f1541,plain,
! [X0,X1] :
( subset_complement(X1,subset_complement(X1,X0)) = X0
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f1540]) ).
fof(f1544,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(f1545,plain,
! [X0,X1] :
( complements_of_subsets(X1,complements_of_subsets(X1,X0)) = X0
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f1544]) ).
fof(f2157,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)],[f360]) ).
fof(f2158,plain,
! [X0,X1] :
( complements_of_subsets(X1,X0) != empty_set
| X0 = empty_set
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f2157]) ).
fof(f2187,plain,
! [A,B] :
( meet_of_subsets(A,complements_of_subsets(A,B)) = subset_complement(A,union_of_subsets(A,B))
| B = empty_set
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f369]) ).
fof(f2188,plain,
! [X0,X1] :
( meet_of_subsets(X1,complements_of_subsets(X1,X0)) = subset_complement(X1,union_of_subsets(X1,X0))
| X0 = empty_set
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f2187]) ).
fof(f2194,plain,
? [A,B] :
( union_of_subsets(A,complements_of_subsets(A,B)) != subset_complement(A,meet_of_subsets(A,B))
& B != empty_set
& element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f373]) ).
fof(f2195,plain,
( union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl)) != subset_complement(sK276_skl,meet_of_subsets(sK276_skl,sK277_skl))
& sK277_skl != empty_set
& 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)],[f2194]) ).
fof(f2196,plain,
element(sK277_skl,powerset(powerset(sK276_skl))),
inference(cnf_transformation,[status(thm)],[f2195]) ).
fof(f2197,plain,
sK277_skl != empty_set,
inference(cnf_transformation,[status(thm)],[f2195]) ).
fof(f2198,plain,
union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl)) != subset_complement(sK276_skl,meet_of_subsets(sK276_skl,sK277_skl)),
inference(cnf_transformation,[status(thm)],[f2195]) ).
fof(f3614,plain,
complements_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl)) = sK277_skl,
inference(resolution,[status(thm)],[f1545,f2196]) ).
fof(f3617,definition,
( sQ63_spl
<=> element(complements_of_subsets(sK276_skl,sK277_skl),powerset(powerset(sK276_skl))) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f3619,plain,
( sQ63_spl
| ~ element(complements_of_subsets(sK276_skl,sK277_skl),powerset(powerset(sK276_skl))) ),
inference(component_clause,[status(thm)],[f3617]) ).
fof(f3626,plain,
! [X0,X1] :
( subset_complement(X1,subset_complement(X1,union_of_subsets(X1,X0))) = union_of_subsets(X1,X0)
| ~ element(X0,powerset(powerset(X1))) ),
inference(resolution,[status(thm)],[f1263,f1541]) ).
fof(f3641,plain,
( complements_of_subsets(sK276_skl,sK277_skl) != empty_set
| sK277_skl = empty_set ),
inference(resolution,[status(thm)],[f2158,f2196]) ).
fof(f3650,definition,
( sQ67_spl
<=> sK277_skl = empty_set ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f3651,plain,
( ~ sQ67_spl
| sK277_skl = empty_set ),
inference(component_clause,[status(thm)],[f3650]) ).
fof(f3653,definition,
( sQ68_spl
<=> complements_of_subsets(sK276_skl,sK277_skl) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f3656,plain,
( ~ sQ68_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f3641,f3650,f3653]) ).
fof(f3657,plain,
( ~ sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3651,f2197]) ).
fof(f3658,plain,
~ sQ67_spl,
inference(contradiction_clause,[status(thm)],[f3657]) ).
fof(f3670,plain,
element(complements_of_subsets(sK276_skl,sK277_skl),powerset(powerset(sK276_skl))),
inference(resolution,[status(thm)],[f1277,f2196]) ).
fof(f3672,plain,
( sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3670,f3619]) ).
fof(f3673,plain,
sQ63_spl,
inference(contradiction_clause,[status(thm)],[f3672]) ).
fof(f3712,plain,
( meet_of_subsets(sK276_skl,sK277_skl) = subset_complement(sK276_skl,union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl)))
| complements_of_subsets(sK276_skl,sK277_skl) = empty_set
| ~ element(complements_of_subsets(sK276_skl,sK277_skl),powerset(powerset(sK276_skl))) ),
inference(paramodulation,[status(thm)],[f3614,f2188]) ).
fof(f3717,definition,
( sQ75_spl
<=> meet_of_subsets(sK276_skl,sK277_skl) = subset_complement(sK276_skl,union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl))) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f3718,plain,
( ~ sQ75_spl
| meet_of_subsets(sK276_skl,sK277_skl) = subset_complement(sK276_skl,union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl))) ),
inference(component_clause,[status(thm)],[f3717]) ).
fof(f3720,plain,
( sQ75_spl
| sQ68_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f3712,f3617,f3653,f3717]) ).
fof(f4133,plain,
subset_complement(sK276_skl,subset_complement(sK276_skl,union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl)))) = union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl)),
inference(resolution,[status(thm)],[f3670,f3626]) ).
fof(f4140,plain,
( ~ sQ75_spl
| subset_complement(sK276_skl,meet_of_subsets(sK276_skl,sK277_skl)) = union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl)) ),
inference(forward_demodulation,[status(thm)],[f3718,f4133]) ).
fof(f4141,plain,
( ~ sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4140,f2198]) ).
fof(f4142,plain,
~ sQ75_spl,
inference(contradiction_clause,[status(thm)],[f4141]) ).
fof(f4143,plain,
$false,
inference(sat_refutation,[status(thm)],[f3656,f3658,f3673,f3720,f4142]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU328+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n008.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 06:12:54 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.27/0.55 % Drodi V4.1.1
% 0.38/0.98 % Refutation found
% 0.38/0.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.38/0.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.40/1.02 % Elapsed time: 0.553588 seconds
% 0.40/1.02 % CPU time: 3.275793 seconds
% 0.40/1.02 % Total memory used: 198.452 MB
% 0.40/1.02 % Net memory used: 194.957 MB
%------------------------------------------------------------------------------