%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU325+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:10 PM UTC 2026
% Result : Theorem 0.12s 0.40s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 14
% Syntax : Number of formulae : 80 ( 28 unt; 0 def)
% Number of atoms : 210 ( 40 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 219 ( 89 ~; 74 |; 40 &)
% ( 4 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-3 aty)
% Number of variables : 117 ( 106 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f17,axiom,
! [A] :
( one_sorted_str(A)
=> cast_as_carrier_subset(A) = the_carrier(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A,B] :
( B = union(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( in(D,A)
& in(C,D) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( element(B,powerset(powerset(the_carrier(A))))
=> ( is_a_cover_of_carrier(A,B)
<=> cast_as_carrier_subset(A) = union_of_subsets(the_carrier(A),B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
( v5_membered(empty_set)
& v4_membered(empty_set)
& v3_membered(empty_set)
& v2_membered(empty_set)
& v1_membered(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> union_of_subsets(A,B) = union(B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,conjecture,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,powerset(powerset(the_carrier(A))))
=> ~ ( B = empty_set
& is_a_cover_of_carrier(A,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
~ ! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,powerset(powerset(the_carrier(A))))
=> ~ ( B = empty_set
& is_a_cover_of_carrier(A,B) ) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f48,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,plain,
! [A] :
( cast_as_carrier_subset(A) = the_carrier(A)
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f108,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
! [A,B] :
( ( ? [C] :
( ( ? [D] :
( in(D,A)
& in(C,D) )
| in(C,B) )
& ( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
| ~ in(C,B) ) )
| B = union(A) )
& ( ! [C] :
( ( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
| in(C,B) )
& ( ? [D] :
( in(D,A)
& in(C,D) )
| ~ in(C,B) ) )
| B != union(A) ) ),
inference(NNF_transformation,[status(thm)],[f18]) ).
fof(f110,plain,
( ! [A,B] :
( ? [C] :
( ( ? [D] :
( in(D,A)
& in(C,D) )
| in(C,B) )
& ( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
| ~ in(C,B) ) )
| B = union(A) )
& ! [A,B] :
( ( ! [C] :
( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
| in(C,B) )
& ! [C] :
( ? [D] :
( in(D,A)
& in(C,D) )
| ~ in(C,B) ) )
| B != union(A) ) ),
inference(miniscoping,[status(thm)],[f109]) ).
fof(f111,plain,
( ! [A,B] :
( ( ( ( in(sK2_skl(B,A),A)
& in(sK1_skl(B,A),sK2_skl(B,A)) )
| in(sK1_skl(B,A),B) )
& ( ! [D] :
( ~ in(D,A)
| ~ in(sK1_skl(B,A),D) )
| ~ in(sK1_skl(B,A),B) ) )
| B = union(A) )
& ! [A,B] :
( ( ! [C] :
( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
| in(C,B) )
& ! [C] :
( ( in(sK0_skl(C,B,A),A)
& in(C,sK0_skl(C,B,A)) )
| ~ in(C,B) ) )
| B != union(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(D,sK0_skl(C,B,A)),skolemize(C,sK1_skl(B,A)),skolemize(D,sK2_skl(B,A))],[f110]) ).
fof(f117,plain,
! [X0,X1] :
( in(sK2_skl(X0,X1),X1)
| in(sK1_skl(X0,X1),X0)
| X0 = union(X1) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f118,plain,
! [A] :
( ! [B] :
( ( is_a_cover_of_carrier(A,B)
<=> cast_as_carrier_subset(A) = union_of_subsets(the_carrier(A),B) )
| ~ element(B,powerset(powerset(the_carrier(A)))) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f119,plain,
! [A] :
( ! [B] :
( ( ( cast_as_carrier_subset(A) != union_of_subsets(the_carrier(A),B)
| is_a_cover_of_carrier(A,B) )
& ( cast_as_carrier_subset(A) = union_of_subsets(the_carrier(A),B)
| ~ is_a_cover_of_carrier(A,B) ) )
| ~ element(B,powerset(powerset(the_carrier(A)))) )
| ~ one_sorted_str(A) ),
inference(NNF_transformation,[status(thm)],[f118]) ).
fof(f120,plain,
! [X0,X1] :
( cast_as_carrier_subset(X0) = union_of_subsets(the_carrier(X0),X1)
| ~ is_a_cover_of_carrier(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f128,plain,
! [A] : element(sK4_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B,sK4_skl(A))],[f29]) ).
fof(f129,plain,
! [X0] : element(sK4_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [A] :
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f131,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f135,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f152,plain,
! [A] :
( empty(sK7_skl(A))
& element(sK7_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(B,sK7_skl(A))],[f36]) ).
fof(f153,plain,
! [X0] : element(sK7_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f154,plain,
! [X0] : empty(sK7_skl(X0)),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f162,plain,
! [A,B] :
( union_of_subsets(A,B) = union(B)
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f163,plain,
! [X0,X1] :
( union_of_subsets(X1,X0) = union(X0)
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f166,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f167,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f168,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f169,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f177,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f178,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f177]) ).
fof(f179,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f180,plain,
? [A] :
( ? [B] :
( B = empty_set
& is_a_cover_of_carrier(A,B)
& element(B,powerset(powerset(the_carrier(A)))) )
& one_sorted_str(A)
& ~ empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f181,plain,
( sK11_skl = empty_set
& is_a_cover_of_carrier(sK10_skl,sK11_skl)
& element(sK11_skl,powerset(powerset(the_carrier(sK10_skl))))
& one_sorted_str(sK10_skl)
& ~ empty_carrier(sK10_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl]),skolemize(A,sK10_skl),skolemize(B,sK11_skl)],[f180]) ).
fof(f182,plain,
~ empty_carrier(sK10_skl),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f183,plain,
one_sorted_str(sK10_skl),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f184,plain,
element(sK11_skl,powerset(powerset(the_carrier(sK10_skl)))),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f185,plain,
is_a_cover_of_carrier(sK10_skl,sK11_skl),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f186,plain,
sK11_skl = empty_set,
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f187,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f188,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f189,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f190,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f189]) ).
fof(f191,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f203,plain,
empty(sK11_skl),
inference(backward_demodulation,[status(thm)],[f186,f135]) ).
fof(f204,plain,
( cast_as_carrier_subset(sK10_skl) = union_of_subsets(the_carrier(sK10_skl),sK11_skl)
| ~ element(sK11_skl,powerset(powerset(the_carrier(sK10_skl))))
| ~ one_sorted_str(sK10_skl) ),
inference(resolution,[status(thm)],[f185,f120]) ).
fof(f205,plain,
( cast_as_carrier_subset(sK10_skl) = union_of_subsets(the_carrier(sK10_skl),sK11_skl)
| ~ element(sK11_skl,powerset(powerset(the_carrier(sK10_skl)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f204,f183]) ).
fof(f206,plain,
! [X0] :
( X0 = sK11_skl
| ~ empty(X0) ),
inference(forward_demodulation,[status(thm)],[f186,f188]) ).
fof(f208,plain,
cast_as_carrier_subset(sK10_skl) = union_of_subsets(the_carrier(sK10_skl),sK11_skl),
inference(forward_subsumption_resolution,[status(thm)],[f205,f184]) ).
fof(f212,plain,
! [X0] : sK7_skl(X0) = sK11_skl,
inference(resolution,[status(thm)],[f154,f206]) ).
fof(f214,plain,
! [X0] : element(sK11_skl,powerset(X0)),
inference(forward_demodulation,[status(thm)],[f212,f153]) ).
fof(f218,plain,
cast_as_carrier_subset(sK10_skl) = the_carrier(sK10_skl),
inference(resolution,[status(thm)],[f108,f183]) ).
fof(f229,plain,
cast_as_carrier_subset(sK10_skl) = union_of_subsets(cast_as_carrier_subset(sK10_skl),sK11_skl),
inference(backward_demodulation,[status(thm)],[f218,f208]) ).
fof(f230,plain,
( ~ empty(cast_as_carrier_subset(sK10_skl))
| ~ one_sorted_str(sK10_skl)
| empty_carrier(sK10_skl) ),
inference(paramodulation,[status(thm)],[f218,f131]) ).
fof(f232,plain,
( ~ empty(cast_as_carrier_subset(sK10_skl))
| ~ one_sorted_str(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f230,f182]) ).
fof(f235,plain,
~ empty(cast_as_carrier_subset(sK10_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f232,f183]) ).
fof(f248,plain,
! [X0,X1] :
( ~ element(X1,powerset(sK11_skl))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f179,f203]) ).
fof(f249,plain,
! [X0,X1] :
( empty(X0)
| ~ element(X1,X0)
| ~ element(X0,powerset(sK11_skl)) ),
inference(resolution,[status(thm)],[f248,f169]) ).
fof(f254,plain,
! [X0] :
( empty(sK4_skl(powerset(sK11_skl)))
| ~ element(X0,sK4_skl(powerset(sK11_skl))) ),
inference(resolution,[status(thm)],[f249,f129]) ).
fof(f260,plain,
empty(sK4_skl(powerset(sK11_skl))),
inference(resolution,[status(thm)],[f254,f129]) ).
fof(f261,plain,
! [X0] :
( ~ in(X0,sK4_skl(powerset(sK11_skl)))
| empty(sK4_skl(powerset(sK11_skl))) ),
inference(resolution,[status(thm)],[f254,f167]) ).
fof(f262,plain,
! [X0] : ~ in(X0,sK4_skl(powerset(sK11_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f261,f191]) ).
fof(f265,plain,
sK4_skl(powerset(sK11_skl)) = sK11_skl,
inference(resolution,[status(thm)],[f260,f206]) ).
fof(f268,plain,
! [X0] : ~ in(X0,sK11_skl),
inference(forward_demodulation,[status(thm)],[f265,f262]) ).
fof(f308,plain,
! [X0] :
( in(sK1_skl(X0,sK11_skl),X0)
| X0 = union(sK11_skl) ),
inference(resolution,[status(thm)],[f117,f268]) ).
fof(f318,plain,
sK11_skl = union(sK11_skl),
inference(resolution,[status(thm)],[f308,f268]) ).
fof(f395,plain,
! [X0] : union_of_subsets(X0,sK11_skl) = union(sK11_skl),
inference(resolution,[status(thm)],[f163,f214]) ).
fof(f400,plain,
! [X0] : union_of_subsets(X0,sK11_skl) = sK11_skl,
inference(forward_demodulation,[status(thm)],[f318,f395]) ).
fof(f401,plain,
cast_as_carrier_subset(sK10_skl) = sK11_skl,
inference(backward_demodulation,[status(thm)],[f400,f229]) ).
fof(f411,plain,
~ empty(sK11_skl),
inference(backward_demodulation,[status(thm)],[f401,f235]) ).
fof(f418,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f411,f203]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU325+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n007.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 06:09:50 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.40 % Refutation found
% 0.12/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.42 % Elapsed time: 0.057711 seconds
% 0.12/0.42 % CPU time: 0.166936 seconds
% 0.12/0.42 % Total memory used: 105.193 MB
% 0.12/0.42 % Net memory used: 105.104 MB
%------------------------------------------------------------------------------