%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU176+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 : n001.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:19:32 PM UTC 2026
% Result : Theorem 15.81s 2.58s
% Output : CNFRefutation 15.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 16
% Syntax : Number of formulae : 87 ( 37 unt; 0 def)
% Number of atoms : 154 ( 84 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 121 ( 54 ~; 44 |; 6 &)
% ( 0 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-3 aty)
% Number of variables : 94 ( 91 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f17,axiom,
! [A] : cast_to_subset(A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,B) = set_difference(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] : element(cast_to_subset(A),powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> element(union_of_subsets(A,B),powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> element(meet_of_subsets(A,B),powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,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(f51,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,subset_complement(A,B)) = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,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(f67,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> union_of_subsets(A,B) = union(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> meet_of_subsets(A,B) = set_meet(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [A,B,C] :
( ( element(C,powerset(A))
& element(B,powerset(A)) )
=> subset_difference(A,B,C) = set_difference(B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,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(f110,lemma,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ( B != empty_set
=> subset_difference(A,cast_to_subset(A),union_of_subsets(A,B)) = meet_of_subsets(A,complements_of_subsets(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f111,conjecture,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ( B != empty_set
=> union_of_subsets(A,complements_of_subsets(A,B)) = subset_difference(A,cast_to_subset(A),meet_of_subsets(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,negated_conjecture,
~ ! [A,B] :
( element(B,powerset(powerset(A)))
=> ( B != empty_set
=> union_of_subsets(A,complements_of_subsets(A,B)) = subset_difference(A,cast_to_subset(A),meet_of_subsets(A,B)) ) ),
inference(negated_conjecture,[status(cth)],[f111]) ).
fof(f124,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f229,plain,
! [X0] : cast_to_subset(X0) = X0,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f248,plain,
! [A,B] :
( subset_complement(A,B) = set_difference(A,B)
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f249,plain,
! [X0,X1] :
( subset_complement(X1,X0) = set_difference(X1,X0)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f268,plain,
! [X0] : element(cast_to_subset(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f271,plain,
! [A,B] :
( element(union_of_subsets(A,B),powerset(A))
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f272,plain,
! [X0,X1] :
( element(union_of_subsets(X1,X0),powerset(X1))
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f273,plain,
! [A,B] :
( element(meet_of_subsets(A,B),powerset(A))
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f274,plain,
! [X0,X1] :
( element(meet_of_subsets(X1,X0),powerset(X1))
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f277,plain,
! [A,B] :
( element(complements_of_subsets(A,B),powerset(powerset(A)))
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f278,plain,
! [X0,X1] :
( element(complements_of_subsets(X1,X0),powerset(powerset(X1)))
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f294,plain,
! [A,B] :
( subset_complement(A,subset_complement(A,B)) = B
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f295,plain,
! [X0,X1] :
( subset_complement(X1,subset_complement(X1,X0)) = X0
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f296,plain,
! [A,B] :
( complements_of_subsets(A,complements_of_subsets(A,B)) = B
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f297,plain,
! [X0,X1] :
( complements_of_subsets(X1,complements_of_subsets(X1,X0)) = X0
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f340,plain,
empty(sK23_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(A,sK23_skl)],[f67]) ).
fof(f341,plain,
empty(sK23_skl),
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f347,plain,
! [A,B] :
( union_of_subsets(A,B) = union(B)
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f70]) ).
fof(f348,plain,
! [X0,X1] :
( union_of_subsets(X1,X0) = union(X0)
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f349,plain,
! [A,B] :
( meet_of_subsets(A,B) = set_meet(B)
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f71]) ).
fof(f350,plain,
! [X0,X1] :
( meet_of_subsets(X1,X0) = set_meet(X0)
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f351,plain,
! [A,B,C] :
( subset_difference(A,B,C) = set_difference(B,C)
| ~ element(C,powerset(A))
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f72]) ).
fof(f352,plain,
! [X0,X1,X2] :
( subset_difference(X1,X0,X2) = set_difference(X0,X2)
| ~ element(X2,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f351]) ).
fof(f450,plain,
! [A,B] :
( complements_of_subsets(A,B) != empty_set
| B = empty_set
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f108]) ).
fof(f451,plain,
! [X0,X1] :
( complements_of_subsets(X1,X0) != empty_set
| X0 = empty_set
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f454,plain,
! [A,B] :
( subset_difference(A,cast_to_subset(A),union_of_subsets(A,B)) = meet_of_subsets(A,complements_of_subsets(A,B))
| B = empty_set
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f110]) ).
fof(f455,plain,
! [X0,X1] :
( subset_difference(X1,cast_to_subset(X1),union_of_subsets(X1,X0)) = meet_of_subsets(X1,complements_of_subsets(X1,X0))
| X0 = empty_set
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f454]) ).
fof(f456,plain,
? [A,B] :
( union_of_subsets(A,complements_of_subsets(A,B)) != subset_difference(A,cast_to_subset(A),meet_of_subsets(A,B))
& B != empty_set
& element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f112]) ).
fof(f457,plain,
( union_of_subsets(sK29_skl,complements_of_subsets(sK29_skl,sK30_skl)) != subset_difference(sK29_skl,cast_to_subset(sK29_skl),meet_of_subsets(sK29_skl,sK30_skl))
& sK30_skl != empty_set
& element(sK30_skl,powerset(powerset(sK29_skl))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl,sK30_skl]),skolemize(A,sK29_skl),skolemize(B,sK30_skl)],[f456]) ).
fof(f458,plain,
element(sK30_skl,powerset(powerset(sK29_skl))),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f459,plain,
sK30_skl != empty_set,
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f460,plain,
union_of_subsets(sK29_skl,complements_of_subsets(sK29_skl,sK30_skl)) != subset_difference(sK29_skl,cast_to_subset(sK29_skl),meet_of_subsets(sK29_skl,sK30_skl)),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f489,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f124]) ).
fof(f490,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f489]) ).
fof(f561,plain,
! [X0] : element(X0,powerset(X0)),
inference(forward_demodulation,[status(thm)],[f229,f268]) ).
fof(f569,plain,
! [X0,X1] :
( subset_difference(X1,X1,union_of_subsets(X1,X0)) = meet_of_subsets(X1,complements_of_subsets(X1,X0))
| X0 = empty_set
| ~ element(X0,powerset(powerset(X1))) ),
inference(forward_demodulation,[status(thm)],[f229,f455]) ).
fof(f570,plain,
union_of_subsets(sK29_skl,complements_of_subsets(sK29_skl,sK30_skl)) != subset_difference(sK29_skl,sK29_skl,meet_of_subsets(sK29_skl,sK30_skl)),
inference(forward_demodulation,[status(thm)],[f229,f460]) ).
fof(f574,plain,
element(meet_of_subsets(sK29_skl,sK30_skl),powerset(sK29_skl)),
inference(resolution,[status(thm)],[f274,f458]) ).
fof(f590,plain,
element(complements_of_subsets(sK29_skl,sK30_skl),powerset(powerset(sK29_skl))),
inference(resolution,[status(thm)],[f278,f458]) ).
fof(f592,plain,
complements_of_subsets(sK29_skl,complements_of_subsets(sK29_skl,sK30_skl)) = sK30_skl,
inference(resolution,[status(thm)],[f297,f458]) ).
fof(f659,plain,
sK23_skl = empty_set,
inference(resolution,[status(thm)],[f490,f341]) ).
fof(f674,plain,
sK30_skl != sK23_skl,
inference(backward_demodulation,[status(thm)],[f659,f459]) ).
fof(f685,plain,
! [X0,X1] :
( subset_difference(X1,X1,union_of_subsets(X1,X0)) = meet_of_subsets(X1,complements_of_subsets(X1,X0))
| X0 = sK23_skl
| ~ element(X0,powerset(powerset(X1))) ),
inference(backward_demodulation,[status(thm)],[f659,f569]) ).
fof(f686,plain,
! [X0,X1] :
( complements_of_subsets(X1,X0) != sK23_skl
| X0 = empty_set
| ~ element(X0,powerset(powerset(X1))) ),
inference(backward_demodulation,[status(thm)],[f659,f451]) ).
fof(f709,plain,
! [X0,X1] :
( complements_of_subsets(X1,X0) != sK23_skl
| X0 = sK23_skl
| ~ element(X0,powerset(powerset(X1))) ),
inference(forward_demodulation,[status(thm)],[f659,f686]) ).
fof(f720,plain,
union_of_subsets(sK29_skl,complements_of_subsets(sK29_skl,sK30_skl)) = union(complements_of_subsets(sK29_skl,sK30_skl)),
inference(resolution,[status(thm)],[f590,f348]) ).
fof(f724,plain,
element(union_of_subsets(sK29_skl,complements_of_subsets(sK29_skl,sK30_skl)),powerset(sK29_skl)),
inference(resolution,[status(thm)],[f590,f272]) ).
fof(f728,plain,
union(complements_of_subsets(sK29_skl,sK30_skl)) != subset_difference(sK29_skl,sK29_skl,meet_of_subsets(sK29_skl,sK30_skl)),
inference(backward_demodulation,[status(thm)],[f720,f570]) ).
fof(f730,plain,
element(union(complements_of_subsets(sK29_skl,sK30_skl)),powerset(sK29_skl)),
inference(forward_demodulation,[status(thm)],[f720,f724]) ).
fof(f741,plain,
meet_of_subsets(sK29_skl,sK30_skl) = set_meet(sK30_skl),
inference(resolution,[status(thm)],[f350,f458]) ).
fof(f746,plain,
element(set_meet(sK30_skl),powerset(sK29_skl)),
inference(backward_demodulation,[status(thm)],[f741,f574]) ).
fof(f747,plain,
union(complements_of_subsets(sK29_skl,sK30_skl)) != subset_difference(sK29_skl,sK29_skl,set_meet(sK30_skl)),
inference(backward_demodulation,[status(thm)],[f741,f728]) ).
fof(f756,plain,
! [X0,X1] :
( subset_difference(X1,X1,X0) = set_difference(X1,X0)
| ~ element(X0,powerset(X1)) ),
inference(resolution,[status(thm)],[f352,f561]) ).
fof(f842,plain,
( subset_difference(sK29_skl,sK29_skl,union_of_subsets(sK29_skl,complements_of_subsets(sK29_skl,sK30_skl))) = meet_of_subsets(sK29_skl,complements_of_subsets(sK29_skl,complements_of_subsets(sK29_skl,sK30_skl)))
| complements_of_subsets(sK29_skl,sK30_skl) = sK23_skl ),
inference(resolution,[status(thm)],[f685,f590]) ).
fof(f846,plain,
( subset_difference(sK29_skl,sK29_skl,union(complements_of_subsets(sK29_skl,sK30_skl))) = meet_of_subsets(sK29_skl,complements_of_subsets(sK29_skl,complements_of_subsets(sK29_skl,sK30_skl)))
| complements_of_subsets(sK29_skl,sK30_skl) = sK23_skl ),
inference(forward_demodulation,[status(thm)],[f720,f842]) ).
fof(f847,plain,
( subset_difference(sK29_skl,sK29_skl,union(complements_of_subsets(sK29_skl,sK30_skl))) = meet_of_subsets(sK29_skl,sK30_skl)
| complements_of_subsets(sK29_skl,sK30_skl) = sK23_skl ),
inference(forward_demodulation,[status(thm)],[f592,f846]) ).
fof(f848,plain,
( subset_difference(sK29_skl,sK29_skl,union(complements_of_subsets(sK29_skl,sK30_skl))) = set_meet(sK30_skl)
| complements_of_subsets(sK29_skl,sK30_skl) = sK23_skl ),
inference(forward_demodulation,[status(thm)],[f741,f847]) ).
fof(f921,plain,
( complements_of_subsets(sK29_skl,sK30_skl) != sK23_skl
| sK30_skl = sK23_skl ),
inference(resolution,[status(thm)],[f709,f458]) ).
fof(f924,plain,
subset_difference(sK29_skl,sK29_skl,union(complements_of_subsets(sK29_skl,sK30_skl))) = set_meet(sK30_skl),
inference(backward_subsumption_resolution,[status(thm)],[f848,f925]) ).
fof(f925,plain,
complements_of_subsets(sK29_skl,sK30_skl) != sK23_skl,
inference(forward_subsumption_resolution,[status(thm)],[f921,f674]) ).
fof(f2284,plain,
subset_difference(sK29_skl,sK29_skl,set_meet(sK30_skl)) = set_difference(sK29_skl,set_meet(sK30_skl)),
inference(resolution,[status(thm)],[f756,f746]) ).
fof(f2305,plain,
union(complements_of_subsets(sK29_skl,sK30_skl)) != set_difference(sK29_skl,set_meet(sK30_skl)),
inference(backward_demodulation,[status(thm)],[f2284,f747]) ).
fof(f2772,plain,
subset_difference(sK29_skl,sK29_skl,union(complements_of_subsets(sK29_skl,sK30_skl))) = set_difference(sK29_skl,union(complements_of_subsets(sK29_skl,sK30_skl))),
inference(resolution,[status(thm)],[f730,f756]) ).
fof(f2782,plain,
set_meet(sK30_skl) = set_difference(sK29_skl,union(complements_of_subsets(sK29_skl,sK30_skl))),
inference(forward_demodulation,[status(thm)],[f924,f2772]) ).
fof(f3439,plain,
subset_complement(sK29_skl,set_meet(sK30_skl)) = set_difference(sK29_skl,set_meet(sK30_skl)),
inference(resolution,[status(thm)],[f249,f746]) ).
fof(f3440,plain,
subset_complement(sK29_skl,union(complements_of_subsets(sK29_skl,sK30_skl))) = set_difference(sK29_skl,union(complements_of_subsets(sK29_skl,sK30_skl))),
inference(resolution,[status(thm)],[f249,f730]) ).
fof(f3453,plain,
subset_complement(sK29_skl,union(complements_of_subsets(sK29_skl,sK30_skl))) = set_meet(sK30_skl),
inference(forward_demodulation,[status(thm)],[f2782,f3440]) ).
fof(f3994,plain,
subset_complement(sK29_skl,subset_complement(sK29_skl,union(complements_of_subsets(sK29_skl,sK30_skl)))) = union(complements_of_subsets(sK29_skl,sK30_skl)),
inference(resolution,[status(thm)],[f295,f730]) ).
fof(f4034,plain,
subset_complement(sK29_skl,set_meet(sK30_skl)) = union(complements_of_subsets(sK29_skl,sK30_skl)),
inference(forward_demodulation,[status(thm)],[f3453,f3994]) ).
fof(f4035,plain,
set_difference(sK29_skl,set_meet(sK30_skl)) = union(complements_of_subsets(sK29_skl,sK30_skl)),
inference(forward_demodulation,[status(thm)],[f3439,f4034]) ).
fof(f4036,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4035,f2305]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU176+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.46 % Computer : n001.cluster.edu
% 0.17/0.46 % Model : x86_64 x86_64
% 0.17/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.46 % Memory : 8046.5625MB
% 0.17/0.46 % OS : Linux 6.8.0-71-generic
% 0.17/0.46 % CPULimit : 300
% 0.17/0.46 % WCLimit : 300
% 0.17/0.46 % DateTime : Mon Sep 21 06:00:28 UTC 2026
% 0.17/0.47 % CPUTime :
% 0.17/0.49 % Drodi V4.1.1
% 15.81/2.58 % Refutation found
% 15.81/2.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.81/2.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.24/2.65 % Elapsed time: 2.166003 seconds
% 2.24/2.65 % CPU time: 16.497319 seconds
% 2.24/2.65 % Total memory used: 222.890 MB
% 2.24/2.65 % Net memory used: 206.167 MB
%------------------------------------------------------------------------------