%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU394+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:22:30 PM UTC 2026
% Result : Theorem 0.99s 0.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU394+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n007.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 06:17:21 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.13/0.39 % Drodi V4.1.1
% 0.99/0.72 % Refutation found
% 0.99/0.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.99/0.72 % SZS output start CNFRefutation for theBenchmark
% 0.99/0.72 fof(f50,axiom,(
% 0.99/0.72 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 0.99/0.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.99/0.72 fof(f59,axiom,(
% 0.99/0.72 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> ~ empty(cast_as_carrier_subset(A)) ) )),
% 0.99/0.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.99/0.72 fof(f87,axiom,(
% 0.99/0.72 (? [A] :( empty(A)& relation(A) ) )),
% 0.99/0.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.99/0.72 fof(f113,axiom,(
% 0.99/0.72 (! [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)) ) )) )),
% 0.99/0.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.99/0.72 fof(f114,conjecture,(
% 0.99/0.72 (! [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)) ) )) )),
% 0.99/0.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.99/0.72 fof(f115,negated_conjecture,(
% 0.99/0.72 ~((! [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)) ) )) ))),
% 0.99/0.72 inference(negated_conjecture,[status(cth)],[f114])).
% 0.99/0.72 fof(f119,axiom,(
% 0.99/0.72 (! [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) ) )) )) )),
% 0.99/0.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.99/0.72 fof(f125,axiom,(
% 0.99/0.72 (! [A,B] :( set_difference(A,singleton(B)) = A<=> ~ in(B,A) ) )),
% 0.99/0.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.99/0.72 fof(f127,axiom,(
% 0.99/0.72 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 0.99/0.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.99/0.72 fof(f128,axiom,(
% 0.99/0.72 (! [A,B] :~ ( empty(A)& A != B& empty(B) ) )),
% 0.99/0.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.99/0.72 fof(f253,plain,(
% 0.99/0.72 empty(empty_set)),
% 0.99/0.72 inference(cnf_transformation,[status(thm)],[f50])).
% 0.99/0.72 fof(f296,plain,(
% 0.99/0.72 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|~empty(cast_as_carrier_subset(A)))),
% 0.99/0.72 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.99/0.72 fof(f297,plain,(
% 0.99/0.72 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|~empty(cast_as_carrier_subset(X0)))),
% 0.99/0.72 inference(cnf_transformation,[status(thm)],[f296])).
% 0.99/0.72 fof(f458,plain,(
% 0.99/0.72 (empty(sK13_skl)&relation(sK13_skl))),
% 0.99/0.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f87])).
% 0.99/0.72 fof(f459,plain,(
% 0.99/0.72 empty(sK13_skl)),
% 0.99/0.72 inference(cnf_transformation,[status(thm)],[f458])).
% 0.99/0.72 fof(f612,plain,(
% 0.99/0.72 ![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)))))),
% 0.99/0.72 inference(pre_NNF_transformation,[status(thm)],[f113])).
% 0.99/0.72 fof(f613,plain,(
% 0.99/0.72 ![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)))),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f612])).
% 0.99/0.73 fof(f614,plain,(
% 0.99/0.73 (?[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))))))),
% 0.99/0.73 inference(pre_NNF_transformation,[status(thm)],[f115])).
% 0.99/0.73 fof(f615,plain,(
% 0.99/0.73 ((~empty_carrier(sK37_skl)&one_sorted_str(sK37_skl))&(((((~empty(sK38_skl)&filtered_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl))))&upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl))))&proper_element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl))))))&element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl))))))&~sK38_skl=filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl))))),
% 0.99/0.73 inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl,sK38_skl]),skolemize(A,sK37_skl),skolemize(B,sK38_skl)],[f614])).
% 0.99/0.73 fof(f616,plain,(
% 0.99/0.73 ~empty_carrier(sK37_skl)),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f615])).
% 0.99/0.73 fof(f617,plain,(
% 0.99/0.73 one_sorted_str(sK37_skl)),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f615])).
% 0.99/0.73 fof(f618,plain,(
% 0.99/0.73 ~empty(sK38_skl)),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f615])).
% 0.99/0.73 fof(f619,plain,(
% 0.99/0.73 filtered_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f615])).
% 0.99/0.73 fof(f620,plain,(
% 0.99/0.73 upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f615])).
% 0.99/0.73 fof(f621,plain,(
% 0.99/0.73 proper_element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f615])).
% 0.99/0.73 fof(f622,plain,(
% 0.99/0.73 element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f615])).
% 0.99/0.73 fof(f623,plain,(
% 0.99/0.73 ~sK38_skl=filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl))),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f615])).
% 0.99/0.73 fof(f633,plain,(
% 0.99/0.73 ![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))))))),
% 0.99/0.73 inference(pre_NNF_transformation,[status(thm)],[f119])).
% 0.99/0.73 fof(f634,plain,(
% 0.99/0.73 ![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))),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f633])).
% 0.99/0.73 fof(f647,plain,(
% 0.99/0.73 ![A,B]: ((~set_difference(A,singleton(B))=A|~in(B,A))&(set_difference(A,singleton(B))=A|in(B,A)))),
% 0.99/0.73 inference(NNF_transformation,[status(thm)],[f125])).
% 0.99/0.73 fof(f648,plain,(
% 0.99/0.73 (![A,B]: (~set_difference(A,singleton(B))=A|~in(B,A)))&(![A,B]: (set_difference(A,singleton(B))=A|in(B,A)))),
% 0.99/0.73 inference(miniscoping,[status(thm)],[f647])).
% 0.99/0.73 fof(f650,plain,(
% 0.99/0.73 ![X0,X1]: (set_difference(X0,singleton(X1))=X0|in(X1,X0))),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f648])).
% 0.99/0.73 fof(f653,plain,(
% 0.99/0.73 ![A,B]: (~in(A,B)|~empty(B))),
% 0.99/0.73 inference(pre_NNF_transformation,[status(thm)],[f127])).
% 0.99/0.73 fof(f654,plain,(
% 0.99/0.73 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 0.99/0.73 inference(miniscoping,[status(thm)],[f653])).
% 0.99/0.73 fof(f655,plain,(
% 0.99/0.73 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f654])).
% 0.99/0.73 fof(f656,plain,(
% 0.99/0.73 ![A,B]: ((~empty(A)|A=B)|~empty(B))),
% 0.99/0.73 inference(pre_NNF_transformation,[status(thm)],[f128])).
% 0.99/0.73 fof(f657,plain,(
% 0.99/0.73 ![B]: ((![A]: (~empty(A)|A=B))|~empty(B))),
% 0.99/0.73 inference(miniscoping,[status(thm)],[f656])).
% 0.99/0.73 fof(f658,plain,(
% 0.99/0.73 ![X0,X1]: (~empty(X0)|X0=X1|~empty(X1))),
% 0.99/0.73 inference(cnf_transformation,[status(thm)],[f657])).
% 0.99/0.73 fof(f664,plain,(
% 0.99/0.73 ![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))),
% 0.99/0.73 inference(backward_subsumption_resolution,[status(thm)],[f634,f655])).
% 0.99/0.73 fof(f695,plain,(
% 0.99/0.73 ![X0]: (~empty(X0)|X0=sK13_skl)),
% 0.99/0.73 inference(resolution,[status(thm)],[f459,f658])).
% 0.99/0.73 fof(f704,plain,(
% 0.99/0.73 empty_set=sK13_skl),
% 0.99/0.73 inference(resolution,[status(thm)],[f695,f253])).
% 0.99/0.73 fof(f712,plain,(
% 0.99/0.73 ![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(sK13_skl))=filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))),
% 0.99/0.73 inference(backward_demodulation,[status(thm)],[f704,f613])).
% 0.99/0.73 fof(f716,plain,(
% 0.99/0.73 empty_carrier(sK37_skl)|~one_sorted_str(sK37_skl)|empty(sK38_skl)|~upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))|~element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))|set_difference(sK38_skl,singleton(sK13_skl))=filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl))),
% 0.99/0.73 inference(resolution,[status(thm)],[f712,f619])).
% 0.99/0.73 fof(f717,plain,(
% 0.99/0.73 ~one_sorted_str(sK37_skl)|empty(sK38_skl)|~upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))|~element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))|set_difference(sK38_skl,singleton(sK13_skl))=filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl))),
% 0.99/0.73 inference(forward_subsumption_resolution,[status(thm)],[f716,f616])).
% 0.99/0.73 fof(f718,plain,(
% 0.99/0.73 empty(sK38_skl)|~upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))|~element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))|set_difference(sK38_skl,singleton(sK13_skl))=filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl))),
% 0.99/0.73 inference(resolution,[status(thm)],[f717,f617])).
% 0.99/0.73 fof(f719,plain,(
% 0.99/0.73 ~upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))|~element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))|set_difference(sK38_skl,singleton(sK13_skl))=filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl))),
% 0.99/0.73 inference(forward_subsumption_resolution,[status(thm)],[f718,f618])).
% 0.99/0.73 fof(f720,plain,(
% 0.99/0.73 ~upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))|set_difference(sK38_skl,singleton(sK13_skl))=filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl))),
% 0.99/0.73 inference(resolution,[status(thm)],[f719,f622])).
% 0.99/0.73 fof(f722,plain,(
% 0.99/0.73 ~sK38_skl=set_difference(sK38_skl,singleton(sK13_skl))),
% 0.99/0.73 inference(backward_demodulation,[status(thm)],[f723,f623])).
% 0.99/0.73 fof(f723,plain,(
% 0.99/0.73 set_difference(sK38_skl,singleton(sK13_skl))=filter_of_net_str(sK37_skl,net_of_bool_filter(sK37_skl,cast_as_carrier_subset(sK37_skl),sK38_skl))),
% 0.99/0.73 inference(forward_subsumption_resolution,[status(thm)],[f720,f620])).
% 0.99/0.73 fof(f1398,plain,(
% 0.99/0.73 ![X0,X1,X2]: (set_difference(X0,singleton(X1))=X0|empty(X2)|~filtered_subset(X0,boole_POSet(X2))|~upper_relstr_subset(X0,boole_POSet(X2))|~proper_element(X0,powerset(the_carrier(boole_POSet(X2))))|~element(X0,powerset(the_carrier(boole_POSet(X2))))|~empty(X1))),
% 0.99/0.73 inference(resolution,[status(thm)],[f650,f664])).
% 0.99/0.73 fof(f1448,plain,(
% 0.99/0.73 ![X0,X1]: (set_difference(X0,singleton(sK13_skl))=X0|empty(X1)|~filtered_subset(X0,boole_POSet(X1))|~upper_relstr_subset(X0,boole_POSet(X1))|~proper_element(X0,powerset(the_carrier(boole_POSet(X1))))|~element(X0,powerset(the_carrier(boole_POSet(X1)))))),
% 1.98/0.75 inference(resolution,[status(thm)],[f1398,f459])).
% 1.98/0.75 fof(f1511,plain,(
% 1.98/0.75 set_difference(sK38_skl,singleton(sK13_skl))=sK38_skl|empty(cast_as_carrier_subset(sK37_skl))|~filtered_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))|~upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))|~element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))),
% 1.98/0.75 inference(resolution,[status(thm)],[f1448,f621])).
% 1.98/0.75 fof(f1513,plain,(
% 1.98/0.75 empty(cast_as_carrier_subset(sK37_skl))|~filtered_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))|~upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))|~element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))),
% 1.98/0.75 inference(forward_subsumption_resolution,[status(thm)],[f1511,f722])).
% 1.98/0.75 fof(f1514,plain,(
% 1.98/0.75 empty(cast_as_carrier_subset(sK37_skl))|~upper_relstr_subset(sK38_skl,boole_POSet(cast_as_carrier_subset(sK37_skl)))|~element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))),
% 1.98/0.75 inference(resolution,[status(thm)],[f1513,f619])).
% 1.98/0.75 fof(f1515,plain,(
% 1.98/0.75 empty(cast_as_carrier_subset(sK37_skl))|~element(sK38_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK37_skl)))))),
% 1.98/0.75 inference(forward_subsumption_resolution,[status(thm)],[f1514,f620])).
% 1.98/0.75 fof(f1516,plain,(
% 1.98/0.75 empty(cast_as_carrier_subset(sK37_skl))),
% 1.98/0.75 inference(resolution,[status(thm)],[f1515,f622])).
% 1.98/0.75 fof(f1520,plain,(
% 1.98/0.75 empty_carrier(sK37_skl)|~one_sorted_str(sK37_skl)),
% 1.98/0.75 inference(resolution,[status(thm)],[f1516,f297])).
% 1.98/0.75 fof(f1530,plain,(
% 1.98/0.75 ~one_sorted_str(sK37_skl)),
% 1.98/0.75 inference(forward_subsumption_resolution,[status(thm)],[f1520,f616])).
% 1.98/0.75 fof(f1531,plain,(
% 1.98/0.75 $false),
% 1.98/0.75 inference(backward_subsumption_resolution,[status(thm)],[f617,f1530])).
% 1.98/0.75 % SZS output end CNFRefutation for theBenchmark.p
% 1.98/0.77 % Elapsed time: 0.386781 seconds
% 1.98/0.77 % CPU time: 2.583369 seconds
% 1.98/0.77 % Total memory used: 170.649 MB
% 1.98/0.77 % Net memory used: 169.100 MB
%------------------------------------------------------------------------------