%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU394+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:22:31 PM UTC 2026
% Result : Theorem 22.83s 3.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU394+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n005.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 06:19:18 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.37/0.63 % Drodi V4.1.1
% 22.83/3.69 % Refutation found
% 22.83/3.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 22.83/3.69 % SZS output start CNFRefutation for theBenchmark
% 22.83/3.69 fof(f138,axiom,(
% 22.83/3.69 (! [A] :( one_sorted_str(A)=> ( empty_carrier(A)<=> empty(the_carrier(A)) ) ) )),
% 22.83/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.83/3.69 fof(f173,axiom,(
% 22.83/3.69 (! [A] :( one_sorted_str(A)=> cast_as_carrier_subset(A) = the_carrier(A) ) )),
% 22.83/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.83/3.69 fof(f368,axiom,(
% 22.83/3.69 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 22.83/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.83/3.69 fof(f531,axiom,(
% 22.83/3.69 (? [A] :( relation(A)& function(A)& one_to_one(A)& empty(A) ) )),
% 22.83/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.83/3.69 fof(f708,lemma,(
% 22.83/3.69 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty(B)& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))& element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) )=> set_difference(B,singleton(empty_set)) = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)) ) )) )),
% 22.83/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.83/3.69 fof(f711,conjecture,(
% 22.83/3.69 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty(B)& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))& element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) )=> B = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)) ) )) )),
% 22.83/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.83/3.69 fof(f712,negated_conjecture,(
% 22.83/3.69 ~((! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty(B)& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))& element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) )=> B = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)) ) )) ))),
% 22.83/3.69 inference(negated_conjecture,[status(cth)],[f711])).
% 22.83/3.69 fof(f785,lemma,(
% 22.83/3.69 (! [A] :( ~ empty(A)=> (! [B] :( ( ~ empty(B)& filtered_subset(B,boole_POSet(A))& upper_relstr_subset(B,boole_POSet(A))& proper_element(B,powerset(the_carrier(boole_POSet(A))))& element(B,powerset(the_carrier(boole_POSet(A)))) )=> (! [C] :~ ( in(C,B)& empty(C) ) )) )) )),
% 22.83/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.83/3.69 fof(f879,lemma,(
% 22.83/3.69 (! [A,B] :( set_difference(A,singleton(B)) = A<=> ~ in(B,A) ) )),
% 22.83/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.83/3.69 fof(f892,axiom,(
% 22.83/3.69 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 22.83/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.83/3.69 fof(f901,axiom,(
% 22.83/3.69 (! [A,B] :~ ( empty(A)& A != B& empty(B) ) )),
% 22.83/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.83/3.69 fof(f1645,plain,(
% 22.83/3.69 ![A]: (~one_sorted_str(A)|(empty_carrier(A)<=>empty(the_carrier(A))))),
% 22.83/3.69 inference(pre_NNF_transformation,[status(thm)],[f138])).
% 22.83/3.69 fof(f1646,plain,(
% 22.83/3.69 ![A]: (~one_sorted_str(A)|((~empty_carrier(A)|empty(the_carrier(A)))&(empty_carrier(A)|~empty(the_carrier(A)))))),
% 22.83/3.69 inference(NNF_transformation,[status(thm)],[f1645])).
% 22.83/3.69 fof(f1648,plain,(
% 22.83/3.69 ![X0]: (~one_sorted_str(X0)|empty_carrier(X0)|~empty(the_carrier(X0)))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f1646])).
% 22.83/3.69 fof(f1868,plain,(
% 22.83/3.69 ![A]: (~one_sorted_str(A)|cast_as_carrier_subset(A)=the_carrier(A))),
% 22.83/3.69 inference(pre_NNF_transformation,[status(thm)],[f173])).
% 22.83/3.69 fof(f1869,plain,(
% 22.83/3.69 ![X0]: (~one_sorted_str(X0)|cast_as_carrier_subset(X0)=the_carrier(X0))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f1868])).
% 22.83/3.69 fof(f2560,plain,(
% 22.83/3.69 empty(empty_set)),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f368])).
% 22.83/3.69 fof(f3416,plain,(
% 22.83/3.69 (((relation(sK210_skl)&function(sK210_skl))&one_to_one(sK210_skl))&empty(sK210_skl))),
% 22.83/3.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK210_skl]),skolemize(A,sK210_skl)],[f531])).
% 22.83/3.69 fof(f3420,plain,(
% 22.83/3.69 empty(sK210_skl)),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f3416])).
% 22.83/3.69 fof(f4533,plain,(
% 22.83/3.69 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: ((((empty(B)|~filtered_subset(B,boole_POSet(cast_as_carrier_subset(A))))|~upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A))))|~element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))|set_difference(B,singleton(empty_set))=filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)))))),
% 22.83/3.69 inference(pre_NNF_transformation,[status(thm)],[f708])).
% 22.83/3.69 fof(f4534,plain,(
% 22.83/3.69 ![X0,X1]: (empty_carrier(X0)|~one_sorted_str(X0)|empty(X1)|~filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))|~upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))|~element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))|set_difference(X1,singleton(empty_set))=filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f4533])).
% 22.83/3.69 fof(f4540,plain,(
% 22.83/3.69 (?[A]: ((~empty_carrier(A)&one_sorted_str(A))&(?[B]: (((((~empty(B)&filtered_subset(B,boole_POSet(cast_as_carrier_subset(A))))&upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A))))&proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))&element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))&~B=filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B))))))),
% 22.83/3.69 inference(pre_NNF_transformation,[status(thm)],[f712])).
% 22.83/3.69 fof(f4541,plain,(
% 22.83/3.69 ((~empty_carrier(sK465_skl)&one_sorted_str(sK465_skl))&(((((~empty(sK466_skl)&filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl))))&upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl))))&proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl))))))&element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl))))))&~sK466_skl=filter_of_net_str(sK465_skl,net_of_bool_filter(sK465_skl,cast_as_carrier_subset(sK465_skl),sK466_skl))))),
% 22.83/3.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK465_skl,sK466_skl]),skolemize(A,sK465_skl),skolemize(B,sK466_skl)],[f4540])).
% 22.83/3.69 fof(f4542,plain,(
% 22.83/3.69 ~empty_carrier(sK465_skl)),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f4541])).
% 22.83/3.69 fof(f4543,plain,(
% 22.83/3.69 one_sorted_str(sK465_skl)),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f4541])).
% 22.83/3.69 fof(f4544,plain,(
% 22.83/3.69 ~empty(sK466_skl)),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f4541])).
% 22.83/3.69 fof(f4545,plain,(
% 22.83/3.69 filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f4541])).
% 22.83/3.69 fof(f4546,plain,(
% 22.83/3.69 upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f4541])).
% 22.83/3.69 fof(f4547,plain,(
% 22.83/3.69 proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl)))))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f4541])).
% 22.83/3.69 fof(f4548,plain,(
% 22.83/3.69 element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl)))))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f4541])).
% 22.83/3.69 fof(f4549,plain,(
% 22.83/3.69 ~sK466_skl=filter_of_net_str(sK465_skl,net_of_bool_filter(sK465_skl,cast_as_carrier_subset(sK465_skl),sK466_skl))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f4541])).
% 22.83/3.69 fof(f4791,plain,(
% 22.83/3.69 ![A]: (empty(A)|(![B]: (((((empty(B)|~filtered_subset(B,boole_POSet(A)))|~upper_relstr_subset(B,boole_POSet(A)))|~proper_element(B,powerset(the_carrier(boole_POSet(A)))))|~element(B,powerset(the_carrier(boole_POSet(A)))))|(![C]: (~in(C,B)|~empty(C))))))),
% 22.83/3.69 inference(pre_NNF_transformation,[status(thm)],[f785])).
% 22.83/3.69 fof(f4792,plain,(
% 22.83/3.69 ![X0,X1,X2]: (empty(X0)|empty(X1)|~filtered_subset(X1,boole_POSet(X0))|~upper_relstr_subset(X1,boole_POSet(X0))|~proper_element(X1,powerset(the_carrier(boole_POSet(X0))))|~element(X1,powerset(the_carrier(boole_POSet(X0))))|~in(X2,X1)|~empty(X2))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f4791])).
% 22.83/3.69 fof(f5111,plain,(
% 22.83/3.69 ![A,B]: ((~set_difference(A,singleton(B))=A|~in(B,A))&(set_difference(A,singleton(B))=A|in(B,A)))),
% 22.83/3.69 inference(NNF_transformation,[status(thm)],[f879])).
% 22.83/3.69 fof(f5112,plain,(
% 22.83/3.69 (![A,B]: (~set_difference(A,singleton(B))=A|~in(B,A)))&(![A,B]: (set_difference(A,singleton(B))=A|in(B,A)))),
% 22.83/3.69 inference(miniscoping,[status(thm)],[f5111])).
% 22.83/3.69 fof(f5114,plain,(
% 22.83/3.69 ![X0,X1]: (set_difference(X0,singleton(X1))=X0|in(X1,X0))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f5112])).
% 22.83/3.69 fof(f5157,plain,(
% 22.83/3.69 ![A,B]: (~in(A,B)|~empty(B))),
% 22.83/3.69 inference(pre_NNF_transformation,[status(thm)],[f892])).
% 22.83/3.69 fof(f5158,plain,(
% 22.83/3.69 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 22.83/3.69 inference(miniscoping,[status(thm)],[f5157])).
% 22.83/3.69 fof(f5159,plain,(
% 22.83/3.69 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f5158])).
% 22.83/3.69 fof(f5188,plain,(
% 22.83/3.69 ![A,B]: ((~empty(A)|A=B)|~empty(B))),
% 22.83/3.69 inference(pre_NNF_transformation,[status(thm)],[f901])).
% 22.83/3.69 fof(f5189,plain,(
% 22.83/3.69 ![B]: ((![A]: (~empty(A)|A=B))|~empty(B))),
% 22.83/3.69 inference(miniscoping,[status(thm)],[f5188])).
% 22.83/3.69 fof(f5190,plain,(
% 22.83/3.69 ![X0,X1]: (~empty(X0)|X0=X1|~empty(X1))),
% 22.83/3.69 inference(cnf_transformation,[status(thm)],[f5189])).
% 22.83/3.69 fof(f6017,plain,(
% 22.83/3.69 ![X0,X1,X2]: (empty(X0)|~filtered_subset(X1,boole_POSet(X0))|~upper_relstr_subset(X1,boole_POSet(X0))|~proper_element(X1,powerset(the_carrier(boole_POSet(X0))))|~element(X1,powerset(the_carrier(boole_POSet(X0))))|~in(X2,X1)|~empty(X2))),
% 22.83/3.69 inference(forward_subsumption_resolution,[status(thm)],[f4792,f5159])).
% 22.83/3.69 fof(f6165,plain,(
% 22.83/3.69 empty_carrier(sK465_skl)|~one_sorted_str(sK465_skl)|empty(sK466_skl)|~filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))|~upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))|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))),
% 22.83/3.69 inference(resolution,[status(thm)],[f4548,f4534])).
% 22.83/3.69 fof(f6167,plain,(
% 22.83/3.69 ![X0]: (empty(cast_as_carrier_subset(sK465_skl))|~filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))|~upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))|~proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl)))))|~in(X0,sK466_skl)|~empty(X0))),
% 22.83/3.69 inference(resolution,[status(thm)],[f4548,f6017])).
% 22.83/3.69 fof(f6173,plain,(
% 22.83/3.69 ~one_sorted_str(sK465_skl)|empty(sK466_skl)|~filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))|~upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))|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))),
% 22.83/3.69 inference(forward_subsumption_resolution,[status(thm)],[f6165,f4542])).
% 22.83/3.69 fof(f6175,plain,(
% 22.83/3.69 ![X0]: (empty(cast_as_carrier_subset(sK465_skl))|~upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))|~proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl)))))|~in(X0,sK466_skl)|~empty(X0))),
% 22.83/3.69 inference(forward_subsumption_resolution,[status(thm)],[f6167,f4545])).
% 22.83/3.69 fof(f6186,plain,(
% 22.83/3.69 ![X0]: (~empty(X0)|X0=empty_set)),
% 22.83/3.69 inference(resolution,[status(thm)],[f5190,f2560])).
% 22.83/3.69 fof(f6194,plain,(
% 22.83/3.69 empty(sK466_skl)|~filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))|~upper_relstr_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))|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))),
% 22.83/3.69 inference(forward_subsumption_resolution,[status(thm)],[f6173,f4543])).
% 22.83/3.69 fof(f6195,plain,(
% 22.83/3.69 empty(sK466_skl)|~filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))|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))),
% 22.83/3.69 inference(resolution,[status(thm)],[f6194,f4546])).
% 22.83/3.69 fof(f6196,plain,(
% 22.83/3.69 ~filtered_subset(sK466_skl,boole_POSet(cast_as_carrier_subset(sK465_skl)))|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))),
% 22.83/3.70 inference(forward_subsumption_resolution,[status(thm)],[f6195,f4544])).
% 22.83/3.70 fof(f6380,plain,(
% 22.83/3.70 ![X0]: (empty(cast_as_carrier_subset(sK465_skl))|~proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl)))))|~in(X0,sK466_skl)|~empty(X0))),
% 22.83/3.70 inference(forward_subsumption_resolution,[status(thm)],[f6175,f4546])).
% 22.83/3.70 fof(f6411,plain,(
% 22.83/3.70 cast_as_carrier_subset(sK465_skl)=the_carrier(sK465_skl)),
% 22.83/3.70 inference(resolution,[status(thm)],[f1869,f4543])).
% 22.83/3.70 fof(f6568,plain,(
% 22.83/3.70 ~one_sorted_str(sK465_skl)|empty_carrier(sK465_skl)|~empty(cast_as_carrier_subset(sK465_skl))),
% 22.83/3.70 inference(paramodulation,[status(thm)],[f6411,f1648])).
% 22.83/3.70 fof(f6590,plain,(
% 22.83/3.70 empty_carrier(sK465_skl)|~empty(cast_as_carrier_subset(sK465_skl))),
% 22.83/3.70 inference(forward_subsumption_resolution,[status(thm)],[f6568,f4543])).
% 22.83/3.70 fof(f6784,plain,(
% 22.83/3.70 ![X0]: (~proper_element(sK466_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK465_skl)))))|~in(X0,sK466_skl)|~empty(X0))),
% 22.83/3.70 inference(backward_subsumption_resolution,[status(thm)],[f6380,f6787])).
% 22.83/3.70 fof(f6787,plain,(
% 22.83/3.70 ~empty(cast_as_carrier_subset(sK465_skl))),
% 22.83/3.70 inference(forward_subsumption_resolution,[status(thm)],[f6590,f4542])).
% 22.83/3.70 fof(f6788,plain,(
% 22.83/3.70 ![X0]: (~in(X0,sK466_skl)|~empty(X0))),
% 22.83/3.70 inference(forward_subsumption_resolution,[status(thm)],[f6784,f4547])).
% 22.83/3.70 fof(f7215,plain,(
% 22.83/3.70 ~in(sK210_skl,sK466_skl)),
% 22.83/3.70 inference(resolution,[status(thm)],[f3420,f6788])).
% 22.83/3.70 fof(f7216,plain,(
% 22.83/3.70 sK210_skl=empty_set),
% 22.83/3.70 inference(resolution,[status(thm)],[f3420,f6186])).
% 22.83/3.70 fof(f7550,plain,(
% 22.83/3.70 ~sK466_skl=set_difference(sK466_skl,singleton(empty_set))),
% 22.83/3.70 inference(backward_demodulation,[status(thm)],[f7551,f4549])).
% 22.83/3.70 fof(f7551,plain,(
% 22.83/3.70 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))),
% 22.83/3.70 inference(forward_subsumption_resolution,[status(thm)],[f6196,f4545])).
% 22.83/3.70 fof(f8015,plain,(
% 22.83/3.70 ~sK466_skl=set_difference(sK466_skl,singleton(sK210_skl))),
% 22.83/3.70 inference(forward_demodulation,[status(thm)],[f7216,f7550])).
% 22.83/3.70 fof(f9432,plain,(
% 22.83/3.70 set_difference(sK466_skl,singleton(sK210_skl))=sK466_skl),
% 22.83/3.70 inference(resolution,[status(thm)],[f5114,f7215])).
% 22.83/3.70 fof(f9441,plain,(
% 22.83/3.70 $false),
% 22.83/3.70 inference(forward_subsumption_resolution,[status(thm)],[f9432,f8015])).
% 22.83/3.70 % SZS output end CNFRefutation for theBenchmark.p
% 22.83/3.81 % Elapsed time: 3.361124 seconds
% 22.83/3.81 % CPU time: 24.562719 seconds
% 22.83/3.81 % Total memory used: 388.251 MB
% 22.83/3.81 % Net memory used: 380.062 MB
%------------------------------------------------------------------------------