%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU387+1 : 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 : n026.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:29 PM UTC 2026
% Result : Theorem 0.14s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU387+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 06:20:51 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 0.14/0.42 % Refutation found
% 0.14/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.42 fof(f26,axiom,(
% 0.14/0.42 (! [A] :( strict_rel_str(boole_POSet(A))& rel_str(boole_POSet(A)) ) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f39,axiom,(
% 0.14/0.42 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f43,axiom,(
% 0.14/0.42 (! [A] :( ~ empty_carrier(boole_POSet(A))& strict_rel_str(boole_POSet(A))& reflexive_relstr(boole_POSet(A))& transitive_relstr(boole_POSet(A))& antisymmetric_relstr(boole_POSet(A))& lower_bounded_relstr(boole_POSet(A))& upper_bounded_relstr(boole_POSet(A))& bounded_relstr(boole_POSet(A))& up_complete_relstr(boole_POSet(A))& join_complete_relstr(boole_POSet(A))& ~ v1_yellow_3(boole_POSet(A))& distributive_relstr(boole_POSet(A))& heyting_relstr(boole_POSet(A))& complemented_relstr(boole_POSet(A))& boolean_relstr(boole_POSet(A))& with_suprema_relstr(boole_POSet(A))& with_infima_relstr(boole_POSet(A))& complete_relstr(boole_POSet(A)) ) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f75,axiom,(
% 0.14/0.42 (! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f78,conjecture,(
% 0.14/0.42 (! [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.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f79,negated_conjecture,(
% 0.14/0.42 ~((! [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.14/0.42 inference(negated_conjecture,[status(cth)],[f78])).
% 0.14/0.42 fof(f84,axiom,(
% 0.14/0.42 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f85,axiom,(
% 0.14/0.42 (! [A,B] :~ ( empty(A)& A != B& empty(B) ) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f86,axiom,(
% 0.14/0.42 (! [A] :( ( ~ empty_carrier(A)& reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& lower_bounded_relstr(A)& rel_str(A) )=> (! [B] :( ( ~ empty(B)& filtered_subset(B,A)& upper_relstr_subset(B,A)& element(B,powerset(the_carrier(A))) )=> ( proper_element(B,powerset(the_carrier(A)))<=> ~ in(bottom_of_relstr(A),B) ) ) )) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f167,plain,(
% 0.14/0.42 (![A]: strict_rel_str(boole_POSet(A)))&(![A]: rel_str(boole_POSet(A)))),
% 0.14/0.42 inference(miniscoping,[status(thm)],[f26])).
% 0.14/0.42 fof(f169,plain,(
% 0.14/0.42 ![X0]: (rel_str(boole_POSet(X0)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f167])).
% 0.14/0.42 fof(f186,plain,(
% 0.14/0.42 empty(empty_set)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f39])).
% 0.14/0.42 fof(f194,plain,(
% 0.14/0.42 (((((((((((((((((![A]: ~empty_carrier(boole_POSet(A)))&(![A]: strict_rel_str(boole_POSet(A))))&(![A]: reflexive_relstr(boole_POSet(A))))&(![A]: transitive_relstr(boole_POSet(A))))&(![A]: antisymmetric_relstr(boole_POSet(A))))&(![A]: lower_bounded_relstr(boole_POSet(A))))&(![A]: upper_bounded_relstr(boole_POSet(A))))&(![A]: bounded_relstr(boole_POSet(A))))&(![A]: up_complete_relstr(boole_POSet(A))))&(![A]: join_complete_relstr(boole_POSet(A))))&(![A]: ~v1_yellow_3(boole_POSet(A))))&(![A]: distributive_relstr(boole_POSet(A))))&(![A]: heyting_relstr(boole_POSet(A))))&(![A]: complemented_relstr(boole_POSet(A))))&(![A]: boolean_relstr(boole_POSet(A))))&(![A]: with_suprema_relstr(boole_POSet(A))))&(![A]: with_infima_relstr(boole_POSet(A))))&(![A]: complete_relstr(boole_POSet(A)))),
% 0.14/0.42 inference(miniscoping,[status(thm)],[f43])).
% 0.14/0.42 fof(f195,plain,(
% 0.14/0.42 ![X0]: (~empty_carrier(boole_POSet(X0)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f194])).
% 0.14/0.42 fof(f197,plain,(
% 0.14/0.42 ![X0]: (reflexive_relstr(boole_POSet(X0)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f194])).
% 0.14/0.42 fof(f198,plain,(
% 0.14/0.42 ![X0]: (transitive_relstr(boole_POSet(X0)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f194])).
% 0.14/0.42 fof(f199,plain,(
% 0.14/0.42 ![X0]: (antisymmetric_relstr(boole_POSet(X0)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f194])).
% 0.14/0.42 fof(f200,plain,(
% 0.14/0.42 ![X0]: (lower_bounded_relstr(boole_POSet(X0)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f194])).
% 0.14/0.42 fof(f425,plain,(
% 0.14/0.42 ![X0]: (bottom_of_relstr(boole_POSet(X0))=empty_set)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f75])).
% 0.14/0.42 fof(f430,plain,(
% 0.14/0.42 (?[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.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 0.14/0.42 fof(f431,plain,(
% 0.14/0.42 (~empty(sK27_skl)&(((((~empty(sK28_skl)&filtered_subset(sK28_skl,boole_POSet(sK27_skl)))&upper_relstr_subset(sK28_skl,boole_POSet(sK27_skl)))&proper_element(sK28_skl,powerset(the_carrier(boole_POSet(sK27_skl)))))&element(sK28_skl,powerset(the_carrier(boole_POSet(sK27_skl)))))&(in(sK29_skl,sK28_skl)&empty(sK29_skl))))),
% 0.14/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl,sK29_skl]),skolemize(A,sK27_skl),skolemize(B,sK28_skl),skolemize(C,sK29_skl)],[f430])).
% 0.14/0.42 fof(f434,plain,(
% 0.14/0.42 filtered_subset(sK28_skl,boole_POSet(sK27_skl))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f431])).
% 0.14/0.42 fof(f435,plain,(
% 0.14/0.42 upper_relstr_subset(sK28_skl,boole_POSet(sK27_skl))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f431])).
% 0.14/0.42 fof(f436,plain,(
% 0.14/0.42 proper_element(sK28_skl,powerset(the_carrier(boole_POSet(sK27_skl))))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f431])).
% 0.14/0.42 fof(f437,plain,(
% 0.14/0.42 element(sK28_skl,powerset(the_carrier(boole_POSet(sK27_skl))))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f431])).
% 0.14/0.42 fof(f438,plain,(
% 0.14/0.42 in(sK29_skl,sK28_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f431])).
% 0.14/0.42 fof(f439,plain,(
% 0.14/0.42 empty(sK29_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f431])).
% 0.14/0.42 fof(f452,plain,(
% 0.14/0.42 ![A,B]: (~in(A,B)|~empty(B))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 0.14/0.42 fof(f453,plain,(
% 0.14/0.42 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 0.14/0.42 inference(miniscoping,[status(thm)],[f452])).
% 0.14/0.42 fof(f454,plain,(
% 0.14/0.42 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f453])).
% 0.14/0.42 fof(f455,plain,(
% 0.14/0.42 ![A,B]: ((~empty(A)|A=B)|~empty(B))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f85])).
% 0.14/0.42 fof(f456,plain,(
% 0.14/0.42 ![B]: ((![A]: (~empty(A)|A=B))|~empty(B))),
% 0.14/0.42 inference(miniscoping,[status(thm)],[f455])).
% 0.14/0.42 fof(f457,plain,(
% 0.14/0.42 ![X0,X1]: (~empty(X0)|X0=X1|~empty(X1))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f456])).
% 0.14/0.42 fof(f458,plain,(
% 0.14/0.42 ![A]: ((((((empty_carrier(A)|~reflexive_relstr(A))|~transitive_relstr(A))|~antisymmetric_relstr(A))|~lower_bounded_relstr(A))|~rel_str(A))|(![B]: ((((empty(B)|~filtered_subset(B,A))|~upper_relstr_subset(B,A))|~element(B,powerset(the_carrier(A))))|(proper_element(B,powerset(the_carrier(A)))<=>~in(bottom_of_relstr(A),B)))))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 0.14/0.42 fof(f459,plain,(
% 0.14/0.42 ![A]: ((((((empty_carrier(A)|~reflexive_relstr(A))|~transitive_relstr(A))|~antisymmetric_relstr(A))|~lower_bounded_relstr(A))|~rel_str(A))|(![B]: ((((empty(B)|~filtered_subset(B,A))|~upper_relstr_subset(B,A))|~element(B,powerset(the_carrier(A))))|((~proper_element(B,powerset(the_carrier(A)))|~in(bottom_of_relstr(A),B))&(proper_element(B,powerset(the_carrier(A)))|in(bottom_of_relstr(A),B))))))),
% 0.14/0.42 inference(NNF_transformation,[status(thm)],[f458])).
% 0.14/0.42 fof(f460,plain,(
% 0.14/0.42 ![X0,X1]: (empty_carrier(X0)|~reflexive_relstr(X0)|~transitive_relstr(X0)|~antisymmetric_relstr(X0)|~lower_bounded_relstr(X0)|~rel_str(X0)|empty(X1)|~filtered_subset(X1,X0)|~upper_relstr_subset(X1,X0)|~element(X1,powerset(the_carrier(X0)))|~proper_element(X1,powerset(the_carrier(X0)))|~in(bottom_of_relstr(X0),X1))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f459])).
% 0.14/0.42 fof(f634,plain,(
% 0.14/0.42 ![X0]: (~empty(X0)|X0=sK29_skl)),
% 0.14/0.42 inference(resolution,[status(thm)],[f457,f439])).
% 0.14/0.42 fof(f786,plain,(
% 0.14/0.42 empty_set=sK29_skl),
% 0.14/0.42 inference(resolution,[status(thm)],[f634,f186])).
% 0.14/0.42 fof(f805,plain,(
% 0.14/0.42 ![X0,X1]: (empty_carrier(X0)|~reflexive_relstr(X0)|~transitive_relstr(X0)|~antisymmetric_relstr(X0)|~lower_bounded_relstr(X0)|~rel_str(X0)|~filtered_subset(X1,X0)|~upper_relstr_subset(X1,X0)|~element(X1,powerset(the_carrier(X0)))|~proper_element(X1,powerset(the_carrier(X0)))|~in(bottom_of_relstr(X0),X1))),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f460,f454])).
% 0.14/0.42 fof(f806,plain,(
% 0.14/0.42 empty_carrier(boole_POSet(sK27_skl))|~reflexive_relstr(boole_POSet(sK27_skl))|~transitive_relstr(boole_POSet(sK27_skl))|~antisymmetric_relstr(boole_POSet(sK27_skl))|~lower_bounded_relstr(boole_POSet(sK27_skl))|~rel_str(boole_POSet(sK27_skl))|~filtered_subset(sK28_skl,boole_POSet(sK27_skl))|~upper_relstr_subset(sK28_skl,boole_POSet(sK27_skl))|~proper_element(sK28_skl,powerset(the_carrier(boole_POSet(sK27_skl))))|~in(bottom_of_relstr(boole_POSet(sK27_skl)),sK28_skl)),
% 0.14/0.42 inference(resolution,[status(thm)],[f805,f437])).
% 0.14/0.42 fof(f807,definition,(
% 0.14/0.42 sQ74_spl <=> (empty_carrier(boole_POSet(sK27_skl)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f808,plain,(
% 0.14/0.42 empty_carrier(boole_POSet(sK27_skl))|~sQ74_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f807])).
% 0.14/0.42 fof(f810,definition,(
% 0.14/0.42 sQ75_spl <=> (reflexive_relstr(boole_POSet(sK27_skl)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f812,plain,(
% 0.14/0.42 ~reflexive_relstr(boole_POSet(sK27_skl))|sQ75_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f810])).
% 0.14/0.42 fof(f813,definition,(
% 0.14/0.42 sQ76_spl <=> (transitive_relstr(boole_POSet(sK27_skl)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f815,plain,(
% 0.14/0.42 ~transitive_relstr(boole_POSet(sK27_skl))|sQ76_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f813])).
% 0.14/0.42 fof(f816,definition,(
% 0.14/0.42 sQ77_spl <=> (antisymmetric_relstr(boole_POSet(sK27_skl)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f818,plain,(
% 0.14/0.42 ~antisymmetric_relstr(boole_POSet(sK27_skl))|sQ77_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f816])).
% 0.14/0.42 fof(f819,definition,(
% 0.14/0.42 sQ78_spl <=> (lower_bounded_relstr(boole_POSet(sK27_skl)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f821,plain,(
% 0.14/0.42 ~lower_bounded_relstr(boole_POSet(sK27_skl))|sQ78_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f819])).
% 0.14/0.42 fof(f822,definition,(
% 0.14/0.42 sQ79_spl <=> (rel_str(boole_POSet(sK27_skl)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f824,plain,(
% 0.14/0.42 ~rel_str(boole_POSet(sK27_skl))|sQ79_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f822])).
% 0.14/0.42 fof(f825,definition,(
% 0.14/0.42 sQ80_spl <=> (filtered_subset(sK28_skl,boole_POSet(sK27_skl)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f827,plain,(
% 0.14/0.42 ~filtered_subset(sK28_skl,boole_POSet(sK27_skl))|sQ80_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f825])).
% 0.14/0.42 fof(f828,definition,(
% 0.14/0.42 sQ81_spl <=> (upper_relstr_subset(sK28_skl,boole_POSet(sK27_skl)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f830,plain,(
% 0.14/0.42 ~upper_relstr_subset(sK28_skl,boole_POSet(sK27_skl))|sQ81_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f828])).
% 0.14/0.42 fof(f831,definition,(
% 0.14/0.42 sQ82_spl <=> (proper_element(sK28_skl,powerset(the_carrier(boole_POSet(sK27_skl)))))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f833,plain,(
% 0.14/0.42 ~proper_element(sK28_skl,powerset(the_carrier(boole_POSet(sK27_skl))))|sQ82_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f831])).
% 0.14/0.42 fof(f834,definition,(
% 0.14/0.42 sQ83_spl <=> (in(bottom_of_relstr(boole_POSet(sK27_skl)),sK28_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f836,plain,(
% 0.14/0.42 ~in(bottom_of_relstr(boole_POSet(sK27_skl)),sK28_skl)|sQ83_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f834])).
% 0.14/0.42 fof(f837,plain,(
% 0.14/0.42 sQ74_spl|~sQ75_spl|~sQ76_spl|~sQ77_spl|~sQ78_spl|~sQ79_spl|~sQ80_spl|~sQ81_spl|~sQ82_spl|~sQ83_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f806,f807,f810,f813,f816,f819,f822,f825,f828,f831,f834])).
% 0.14/0.42 fof(f980,plain,(
% 0.14/0.42 $false|sQ81_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f830,f435])).
% 0.14/0.42 fof(f981,plain,(
% 0.14/0.42 sQ81_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f980])).
% 0.14/0.42 fof(f982,plain,(
% 0.14/0.42 $false|sQ80_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f827,f434])).
% 0.14/0.42 fof(f983,plain,(
% 0.14/0.42 sQ80_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f982])).
% 0.14/0.42 fof(f1468,plain,(
% 0.14/0.42 $false|~sQ74_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f808,f195])).
% 0.14/0.42 fof(f1469,plain,(
% 0.14/0.42 ~sQ74_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1468])).
% 0.14/0.42 fof(f1636,plain,(
% 0.14/0.42 $false|sQ79_spl),
% 0.14/0.42 inference(backward_subsumption_resolution,[status(thm)],[f824,f169])).
% 0.14/0.42 fof(f1660,plain,(
% 0.14/0.42 sQ79_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1636])).
% 0.14/0.42 fof(f1687,plain,(
% 0.14/0.42 $false|sQ78_spl),
% 0.14/0.42 inference(backward_subsumption_resolution,[status(thm)],[f821,f200])).
% 0.14/0.42 fof(f1688,plain,(
% 0.14/0.42 sQ78_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1687])).
% 0.14/0.42 fof(f1689,plain,(
% 0.14/0.42 $false|sQ77_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f818,f199])).
% 0.14/0.42 fof(f1690,plain,(
% 0.14/0.42 sQ77_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1689])).
% 0.14/0.42 fof(f1691,plain,(
% 0.14/0.42 $false|sQ76_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f815,f198])).
% 0.14/0.42 fof(f1692,plain,(
% 0.14/0.42 sQ76_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1691])).
% 0.14/0.42 fof(f1693,plain,(
% 0.14/0.42 $false|sQ75_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f812,f197])).
% 0.14/0.42 fof(f1694,plain,(
% 0.14/0.42 sQ75_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1693])).
% 0.14/0.42 fof(f2020,plain,(
% 0.14/0.42 ~in(sK29_skl,sK28_skl)|sQ83_spl),
% 0.14/0.42 inference(backward_demodulation,[status(thm)],[f2021,f836])).
% 0.14/0.42 fof(f2021,plain,(
% 0.14/0.42 ![X0]: (bottom_of_relstr(boole_POSet(X0))=sK29_skl)),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f786,f425])).
% 0.14/0.42 fof(f2022,plain,(
% 0.14/0.42 $false|sQ83_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f2020,f438])).
% 0.14/0.42 fof(f2023,plain,(
% 0.14/0.42 sQ83_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f2022])).
% 0.14/0.42 fof(f2025,plain,(
% 0.14/0.42 $false|sQ82_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f833,f436])).
% 0.14/0.42 fof(f2026,plain,(
% 0.14/0.42 sQ82_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f2025])).
% 0.14/0.42 fof(f2027,plain,(
% 0.14/0.42 $false),
% 0.14/0.42 inference(sat_refutation,[status(thm)],[f837,f981,f983,f1469,f1660,f1688,f1690,f1692,f1694,f2023,f2026])).
% 0.14/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.44 % Elapsed time: 0.083198 seconds
% 0.14/0.44 % CPU time: 0.319360 seconds
% 0.14/0.44 % Total memory used: 115.521 MB
% 0.14/0.44 % Net memory used: 115.228 MB
%------------------------------------------------------------------------------