%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU394+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 : n016.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:24 PM UTC 2026
% Result : Theorem 0.23s 0.72s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 17
% Syntax : Number of formulae : 78 ( 17 unt; 10 def)
% Number of atoms : 230 ( 19 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 256 ( 104 ~; 93 |; 39 &)
% ( 11 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 11 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 47 ( 45 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f50,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(cast_as_carrier_subset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& ~ empty(B) )
=> set_difference(B,singleton(empty_set)) = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,conjecture,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& ~ empty(B) )
=> B = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,negated_conjecture,
~ ! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& ~ empty(B) )
=> B = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)) ) ),
inference(negated_conjecture,[status(cth)],[f114]) ).
fof(f119,axiom,
! [A] :
( ~ empty(A)
=> ! [B] :
( ( element(B,powerset(the_carrier(boole_POSet(A))))
& proper_element(B,powerset(the_carrier(boole_POSet(A))))
& upper_relstr_subset(B,boole_POSet(A))
& filtered_subset(B,boole_POSet(A))
& ~ empty(B) )
=> ! [C] :
~ ( empty(C)
& in(C,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f125,axiom,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f127,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f253,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f296,plain,
! [A] :
( ~ empty(cast_as_carrier_subset(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f59]) ).
fof(f297,plain,
! [X0] :
( ~ empty(cast_as_carrier_subset(X0))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f612,plain,
! [A] :
( ! [B] :
( set_difference(B,singleton(empty_set)) = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B))
| ~ element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
| ~ upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
| ~ filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
| empty(B) )
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f113]) ).
fof(f613,plain,
! [X0,X1] :
( set_difference(X1,singleton(empty_set)) = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f612]) ).
fof(f614,plain,
? [A] :
( ? [B] :
( B != filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B))
& element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& ~ empty(B) )
& one_sorted_str(A)
& ~ empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f115]) ).
fof(f615,plain,
( sK38_skl != filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl))
& element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))
& proper_element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))
& upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))
& filtered_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))
& ~ empty(sK38_skl)
& one_sorted_str(sK37_skl)
& ~ empty_carrier(sK37_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl,sK38_skl]),skolemize(A,sK37_skl),skolemize(B,sK38_skl)],[f614]) ).
fof(f616,plain,
~ empty_carrier(sK37_skl),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f617,plain,
one_sorted_str(sK37_skl),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f618,plain,
~ empty(sK38_skl),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f619,plain,
filtered_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl))),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f620,plain,
upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl))),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f621,plain,
proper_element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl))))),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f622,plain,
element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl))))),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f623,plain,
sK38_skl != filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl)),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f633,plain,
! [A] :
( ! [B] :
( ! [C] :
( ~ empty(C)
| ~ in(C,B) )
| ~ element(B,powerset(the_carrier(boole_POSet(A))))
| ~ proper_element(B,powerset(the_carrier(boole_POSet(A))))
| ~ upper_relstr_subset(B,boole_POSet(A))
| ~ filtered_subset(B,boole_POSet(A))
| empty(B) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f119]) ).
fof(f634,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ in(X2,X1)
| ~ element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ upper_relstr_subset(X1,boole_POSet(X0))
| ~ filtered_subset(X1,boole_POSet(X0))
| empty(X1)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f633]) ).
fof(f647,plain,
! [A,B] :
( ( in(B,A)
| set_difference(A,singleton(B)) = A )
& ( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(NNF_transformation,[status(thm)],[f125]) ).
fof(f648,plain,
( ! [A,B] :
( in(B,A)
| set_difference(A,singleton(B)) = A )
& ! [A,B] :
( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(miniscoping,[status(thm)],[f647]) ).
fof(f650,plain,
! [X0,X1] :
( in(X1,X0)
| set_difference(X0,singleton(X1)) = X0 ),
inference(cnf_transformation,[status(thm)],[f648]) ).
fof(f653,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f127]) ).
fof(f654,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f653]) ).
fof(f655,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f654]) ).
fof(f664,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ in(X2,X1)
| ~ element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ upper_relstr_subset(X1,boole_POSet(X0))
| ~ filtered_subset(X1,boole_POSet(X0))
| empty(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f634,f655]) ).
fof(f683,plain,
( set_difference(sK38_skl,singleton(empty_set)) = filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl))
| ~ element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))
| ~ upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))
| empty(sK38_skl)
| ~ one_sorted_str(sK37_skl)
| empty_carrier(sK37_skl) ),
inference(resolution,[status(thm)],[f619,f613]) ).
fof(f687,definition,
( sQ0_spl
<=> empty_carrier(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f688,plain,
( ~ sQ0_spl
| empty_carrier(sK37_skl) ),
inference(component_clause,[status(thm)],[f687]) ).
fof(f690,definition,
( sQ1_spl
<=> one_sorted_str(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f692,plain,
( sQ1_spl
| ~ one_sorted_str(sK37_skl) ),
inference(component_clause,[status(thm)],[f690]) ).
fof(f693,definition,
( sQ2_spl
<=> empty(sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f694,plain,
( ~ sQ2_spl
| empty(sK38_skl) ),
inference(component_clause,[status(thm)],[f693]) ).
fof(f696,definition,
( sQ3_spl
<=> upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl))) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f698,plain,
( sQ3_spl
| ~ upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl))) ),
inference(component_clause,[status(thm)],[f696]) ).
fof(f699,definition,
( sQ4_spl
<=> element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f701,plain,
( sQ4_spl
| ~ element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl))))) ),
inference(component_clause,[status(thm)],[f699]) ).
fof(f702,definition,
( sQ5_spl
<=> set_difference(sK38_skl,singleton(empty_set)) = filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f703,plain,
( ~ sQ5_spl
| set_difference(sK38_skl,singleton(empty_set)) = filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl)) ),
inference(component_clause,[status(thm)],[f702]) ).
fof(f705,plain,
( sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| sQ2_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f683,f687,f690,f693,f696,f699,f702]) ).
fof(f709,definition,
( sQ7_spl
<=> empty(cast_as_carrier_subset(sK37_skl)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f710,plain,
( ~ sQ7_spl
| empty(cast_as_carrier_subset(sK37_skl)) ),
inference(component_clause,[status(thm)],[f709]) ).
fof(f712,definition,
( sQ8_spl
<=> proper_element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f714,plain,
( sQ8_spl
| ~ proper_element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl))))) ),
inference(component_clause,[status(thm)],[f712]) ).
fof(f724,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f701,f622]) ).
fof(f725,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f724]) ).
fof(f726,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f698,f620]) ).
fof(f727,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f726]) ).
fof(f728,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f694,f618]) ).
fof(f729,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f728]) ).
fof(f730,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f714,f621]) ).
fof(f731,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f730]) ).
fof(f732,plain,
( ~ sQ5_spl
| sK38_skl != set_difference(sK38_skl,singleton(empty_set)) ),
inference(backward_demodulation,[status(thm)],[f703,f623]) ).
fof(f738,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f688,f616]) ).
fof(f739,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f738]) ).
fof(f740,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f692,f617]) ).
fof(f741,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f740]) ).
fof(f745,plain,
( ~ sQ7_spl
| ~ one_sorted_str(sK37_skl)
| empty_carrier(sK37_skl) ),
inference(resolution,[status(thm)],[f297,f710]) ).
fof(f746,plain,
( ~ sQ7_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f745,f687,f690,f709]) ).
fof(f747,plain,
! [X0,X1] :
( ~ in(empty_set,X1)
| ~ element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ upper_relstr_subset(X1,boole_POSet(X0))
| ~ filtered_subset(X1,boole_POSet(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f664,f253]) ).
fof(f827,definition,
( sQ28_spl
<=> filtered_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl))) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f829,plain,
( sQ28_spl
| ~ filtered_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl))) ),
inference(component_clause,[status(thm)],[f827]) ).
fof(f846,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f829,f619]) ).
fof(f847,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f846]) ).
fof(f1211,plain,
( ~ in(empty_set,sK38_skl)
| ~ element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))
| ~ proper_element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))
| ~ upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))
| empty(cast_as_carrier_subset(sK37_skl)) ),
inference(resolution,[status(thm)],[f747,f619]) ).
fof(f1213,definition,
( sQ88_spl
<=> in(empty_set,sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1215,plain,
( sQ88_spl
| ~ in(empty_set,sK38_skl) ),
inference(component_clause,[status(thm)],[f1213]) ).
fof(f1216,plain,
( ~ sQ88_spl
| ~ sQ4_spl
| ~ sQ8_spl
| ~ sQ3_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f1211,f709,f696,f712,f699,f1213]) ).
fof(f1217,plain,
( sQ88_spl
| set_difference(sK38_skl,singleton(empty_set)) = sK38_skl ),
inference(resolution,[status(thm)],[f1215,f650]) ).
fof(f1219,plain,
( sQ88_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1217,f732]) ).
fof(f1220,plain,
( sQ88_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f1219]) ).
fof(f1221,plain,
$false,
inference(sat_refutation,[status(thm)],[f705,f725,f727,f729,f731,f739,f741,f746,f847,f1216,f1220]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU394+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n016.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 06:24:08 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.49 % Drodi V4.1.1
% 0.23/0.72 % Refutation found
% 0.23/0.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.23/0.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.23/0.76 % Elapsed time: 0.279020 seconds
% 0.23/0.76 % CPU time: 1.567247 seconds
% 0.23/0.76 % Total memory used: 139.417 MB
% 0.23/0.76 % Net memory used: 138.576 MB
%------------------------------------------------------------------------------