%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU394+2 : 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:24 PM UTC 2026
% Result : Theorem 20.02s 3.16s
% Output : CNFRefutation 20.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 10
% Syntax : Number of formulae : 65 ( 19 unt; 0 def)
% Number of atoms : 213 ( 33 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 256 ( 108 ~; 88 |; 47 &)
% ( 3 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-3 aty)
% Number of variables : 64 ( 61 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f138,axiom,
! [A] :
( one_sorted_str(A)
=> ( empty_carrier(A)
<=> empty(the_carrier(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [A] :
( one_sorted_str(A)
=> cast_as_carrier_subset(A) = the_carrier(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f368,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f531,axiom,
? [A] :
( empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f708,lemma,
! [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(f711,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(f712,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)],[f711]) ).
fof(f785,lemma,
! [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(f879,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f892,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f901,axiom,
! [A,B] :
~ ( empty(B)
& A != B
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1645,plain,
! [A] :
( ( empty_carrier(A)
<=> empty(the_carrier(A)) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f138]) ).
fof(f1646,plain,
! [A] :
( ( ( ~ empty(the_carrier(A))
| empty_carrier(A) )
& ( empty(the_carrier(A))
| ~ empty_carrier(A) ) )
| ~ one_sorted_str(A) ),
inference(NNF_transformation,[status(thm)],[f1645]) ).
fof(f1648,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1646]) ).
fof(f1868,plain,
! [A] :
( cast_as_carrier_subset(A) = the_carrier(A)
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f173]) ).
fof(f1869,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1868]) ).
fof(f2560,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f3416,plain,
( empty(sK210_skl)
& one_to_one(sK210_skl)
& function(sK210_skl)
& relation(sK210_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK210_skl]),skolemize(A,sK210_skl)],[f531]) ).
fof(f3420,plain,
empty(sK210_skl),
inference(cnf_transformation,[status(thm)],[f3416]) ).
fof(f4533,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)],[f708]) ).
fof(f4534,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)],[f4533]) ).
fof(f4540,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)],[f712]) ).
fof(f4541,plain,
( sK466_skl != filter_of_net_str(sK465_skl,net_of_bool_filter(sK465_skl,cast_as_carrier_subset(sK465_skl),sK466_skl))
& element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl)))))
& proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl)))))
& upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
& filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
& ~ empty(sK466_skl)
& one_sorted_str(sK465_skl)
& ~ empty_carrier(sK465_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK465_skl,sK466_skl]),skolemize(A,sK465_skl),skolemize(B,sK466_skl)],[f4540]) ).
fof(f4542,plain,
~ empty_carrier(sK465_skl),
inference(cnf_transformation,[status(thm)],[f4541]) ).
fof(f4543,plain,
one_sorted_str(sK465_skl),
inference(cnf_transformation,[status(thm)],[f4541]) ).
fof(f4544,plain,
~ empty(sK466_skl),
inference(cnf_transformation,[status(thm)],[f4541]) ).
fof(f4545,plain,
filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl))),
inference(cnf_transformation,[status(thm)],[f4541]) ).
fof(f4546,plain,
upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl))),
inference(cnf_transformation,[status(thm)],[f4541]) ).
fof(f4547,plain,
proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl))))),
inference(cnf_transformation,[status(thm)],[f4541]) ).
fof(f4548,plain,
element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl))))),
inference(cnf_transformation,[status(thm)],[f4541]) ).
fof(f4549,plain,
sK466_skl != filter_of_net_str(sK465_skl,net_of_bool_filter(sK465_skl,cast_as_carrier_subset(sK465_skl),sK466_skl)),
inference(cnf_transformation,[status(thm)],[f4541]) ).
fof(f4791,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)],[f785]) ).
fof(f4792,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)],[f4791]) ).
fof(f5111,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)],[f879]) ).
fof(f5112,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)],[f5111]) ).
fof(f5114,plain,
! [X0,X1] :
( in(X1,X0)
| set_difference(X0,singleton(X1)) = X0 ),
inference(cnf_transformation,[status(thm)],[f5112]) ).
fof(f5157,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f892]) ).
fof(f5158,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f5157]) ).
fof(f5159,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f5158]) ).
fof(f5188,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f901]) ).
fof(f5189,plain,
! [B] :
( ~ empty(B)
| ! [A] :
( A = B
| ~ empty(A) ) ),
inference(miniscoping,[status(thm)],[f5188]) ).
fof(f5190,plain,
! [X0,X1] :
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f5189]) ).
fof(f6017,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(forward_subsumption_resolution,[status(thm)],[f4792,f5159]) ).
fof(f6165,plain,
( set_difference(sK466_skl,singleton(empty_set)) = filter_of_net_str(sK465_skl,net_of_bool_filter(sK465_skl,cast_as_carrier_subset(sK465_skl),sK466_skl))
| ~ upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
| ~ filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
| empty(sK466_skl)
| ~ one_sorted_str(sK465_skl)
| empty_carrier(sK465_skl) ),
inference(resolution,[status(thm)],[f4548,f4534]) ).
fof(f6167,plain,
! [X0] :
( ~ empty(X0)
| ~ in(X0,sK466_skl)
| ~ proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl)))))
| ~ upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
| ~ filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
| empty(cast_as_carrier_subset(sK465_skl)) ),
inference(resolution,[status(thm)],[f4548,f6017]) ).
fof(f6173,plain,
( set_difference(sK466_skl,singleton(empty_set)) = filter_of_net_str(sK465_skl,net_of_bool_filter(sK465_skl,cast_as_carrier_subset(sK465_skl),sK466_skl))
| ~ upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
| ~ filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
| empty(sK466_skl)
| ~ one_sorted_str(sK465_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f6165,f4542]) ).
fof(f6175,plain,
! [X0] :
( ~ empty(X0)
| ~ in(X0,sK466_skl)
| ~ proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl)))))
| ~ upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
| empty(cast_as_carrier_subset(sK465_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6167,f4545]) ).
fof(f6186,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f5190,f2560]) ).
fof(f6194,plain,
( set_difference(sK466_skl,singleton(empty_set)) = filter_of_net_str(sK465_skl,net_of_bool_filter(sK465_skl,cast_as_carrier_subset(sK465_skl),sK466_skl))
| ~ upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
| ~ filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
| empty(sK466_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f6173,f4543]) ).
fof(f6195,plain,
( set_difference(sK466_skl,singleton(empty_set)) = filter_of_net_str(sK465_skl,net_of_bool_filter(sK465_skl,cast_as_carrier_subset(sK465_skl),sK466_skl))
| ~ filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))
| empty(sK466_skl) ),
inference(resolution,[status(thm)],[f6194,f4546]) ).
fof(f6196,plain,
( set_difference(sK466_skl,singleton(empty_set)) = filter_of_net_str(sK465_skl,net_of_bool_filter(sK465_skl,cast_as_carrier_subset(sK465_skl),sK466_skl))
| ~ filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f6195,f4544]) ).
fof(f6380,plain,
! [X0] :
( ~ empty(X0)
| ~ in(X0,sK466_skl)
| ~ proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl)))))
| empty(cast_as_carrier_subset(sK465_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6175,f4546]) ).
fof(f6411,plain,
cast_as_carrier_subset(sK465_skl) = the_carrier(sK465_skl),
inference(resolution,[status(thm)],[f1869,f4543]) ).
fof(f6568,plain,
( ~ empty(cast_as_carrier_subset(sK465_skl))
| empty_carrier(sK465_skl)
| ~ one_sorted_str(sK465_skl) ),
inference(paramodulation,[status(thm)],[f6411,f1648]) ).
fof(f6590,plain,
( ~ empty(cast_as_carrier_subset(sK465_skl))
| empty_carrier(sK465_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f6568,f4543]) ).
fof(f6784,plain,
! [X0] :
( ~ empty(X0)
| ~ in(X0,sK466_skl)
| ~ proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl))))) ),
inference(backward_subsumption_resolution,[status(thm)],[f6380,f6787]) ).
fof(f6787,plain,
~ empty(cast_as_carrier_subset(sK465_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f6590,f4542]) ).
fof(f6788,plain,
! [X0] :
( ~ empty(X0)
| ~ in(X0,sK466_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f6784,f4547]) ).
fof(f7215,plain,
~ in(sK210_skl,sK466_skl),
inference(resolution,[status(thm)],[f3420,f6788]) ).
fof(f7216,plain,
sK210_skl = empty_set,
inference(resolution,[status(thm)],[f3420,f6186]) ).
fof(f7550,plain,
sK466_skl != set_difference(sK466_skl,singleton(empty_set)),
inference(backward_demodulation,[status(thm)],[f7551,f4549]) ).
fof(f7551,plain,
set_difference(sK466_skl,singleton(empty_set)) = filter_of_net_str(sK465_skl,net_of_bool_filter(sK465_skl,cast_as_carrier_subset(sK465_skl),sK466_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f6196,f4545]) ).
fof(f8015,plain,
sK466_skl != set_difference(sK466_skl,singleton(sK210_skl)),
inference(forward_demodulation,[status(thm)],[f7216,f7550]) ).
fof(f9432,plain,
set_difference(sK466_skl,singleton(sK210_skl)) = sK466_skl,
inference(resolution,[status(thm)],[f5114,f7215]) ).
fof(f9441,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f9432,f8015]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU394+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.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:17:21 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.27/0.57 % Drodi V4.1.1
% 20.02/3.16 % Refutation found
% 20.02/3.16 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.02/3.16 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.23/3.24 % Elapsed time: 2.863386 seconds
% 2.23/3.24 % CPU time: 20.774542 seconds
% 2.23/3.24 % Total memory used: 389.690 MB
% 2.23/3.24 % Net memory used: 365.895 MB
%------------------------------------------------------------------------------