%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU354+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 : n015.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:16 PM UTC 2026
% Result : Theorem 0.21s 0.50s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 28
% Syntax : Number of formulae : 127 ( 24 unt; 17 def)
% Number of atoms : 292 ( 49 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 263 ( 98 ~; 94 |; 42 &)
% ( 21 <=>; 7 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 18 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-3 aty)
% Number of variables : 35 ( 26 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A] :
( rel_str(A)
=> ( strict_rel_str(A)
=> A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A] :
( latt_str(A)
=> ( strict_latt_str(A)
=> A = latt_str_of(the_carrier(A),the_L_join(A),the_L_meet(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,axiom,
! [A,B] :
( element(B,A)
=> ( proper_element(B,A)
<=> B != union(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f363,axiom,
? [A] :
( strict_rel_str(A)
& rel_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f374,axiom,
? [A] :
( antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f384,axiom,
? [A] :
( strict_latt_str(A)
& latt_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f392,axiom,
? [A] :
( strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f395,axiom,
? [A] :
( lattice(A)
& join_absorbing(A)
& meet_absorbing(A)
& meet_associative(A)
& meet_commutative(A)
& join_associative(A)
& join_commutative(A)
& strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f398,axiom,
! [A] : k1_pcomps_1(A) = powerset(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f627,conjecture,
! [A,B] :
( element(B,powerset(A))
=> ( proper_element(B,powerset(A))
<=> B != A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f628,negated_conjecture,
~ ! [A,B] :
( element(B,powerset(A))
=> ( proper_element(B,powerset(A))
<=> B != A ) ),
inference(negated_conjecture,[status(cth)],[f627]) ).
fof(f668,lemma,
! [A] : union(powerset(A)) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f672,plain,
! [A] :
( A = rel_str_of(the_carrier(A),the_InternalRel(A))
| ~ strict_rel_str(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f673,plain,
! [X0] :
( X0 = rel_str_of(the_carrier(X0),the_InternalRel(X0))
| ~ strict_rel_str(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f672]) ).
fof(f674,plain,
! [A] :
( A = latt_str_of(the_carrier(A),the_L_join(A),the_L_meet(A))
| ~ strict_latt_str(A)
| ~ latt_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f675,plain,
! [X0] :
( X0 = latt_str_of(the_carrier(X0),the_L_join(X0),the_L_meet(X0))
| ~ strict_latt_str(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[status(thm)],[f674]) ).
fof(f1193,plain,
! [A,B] :
( ( proper_element(B,A)
<=> B != union(A) )
| ~ element(B,A) ),
inference(pre_NNF_transformation,[status(thm)],[f102]) ).
fof(f1194,plain,
! [A,B] :
( ( ( B = union(A)
| proper_element(B,A) )
& ( B != union(A)
| ~ proper_element(B,A) ) )
| ~ element(B,A) ),
inference(NNF_transformation,[status(thm)],[f1193]) ).
fof(f1195,plain,
! [X0,X1] :
( X0 != union(X1)
| ~ proper_element(X0,X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1194]) ).
fof(f1196,plain,
! [X0,X1] :
( X0 = union(X1)
| proper_element(X0,X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1194]) ).
fof(f2135,plain,
( strict_rel_str(sK143_skl)
& rel_str(sK143_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK143_skl]),skolemize(A,sK143_skl)],[f363]) ).
fof(f2136,plain,
rel_str(sK143_skl),
inference(cnf_transformation,[status(thm)],[f2135]) ).
fof(f2137,plain,
strict_rel_str(sK143_skl),
inference(cnf_transformation,[status(thm)],[f2135]) ).
fof(f2188,plain,
( antisymmetric_relstr(sK154_skl)
& transitive_relstr(sK154_skl)
& reflexive_relstr(sK154_skl)
& strict_rel_str(sK154_skl)
& ~ empty_carrier(sK154_skl)
& rel_str(sK154_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK154_skl]),skolemize(A,sK154_skl)],[f374]) ).
fof(f2189,plain,
rel_str(sK154_skl),
inference(cnf_transformation,[status(thm)],[f2188]) ).
fof(f2191,plain,
strict_rel_str(sK154_skl),
inference(cnf_transformation,[status(thm)],[f2188]) ).
fof(f2232,plain,
( strict_latt_str(sK164_skl)
& latt_str(sK164_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK164_skl]),skolemize(A,sK164_skl)],[f384]) ).
fof(f2233,plain,
latt_str(sK164_skl),
inference(cnf_transformation,[status(thm)],[f2232]) ).
fof(f2234,plain,
strict_latt_str(sK164_skl),
inference(cnf_transformation,[status(thm)],[f2232]) ).
fof(f2267,plain,
( strict_latt_str(sK172_skl)
& ~ empty_carrier(sK172_skl)
& latt_str(sK172_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK172_skl]),skolemize(A,sK172_skl)],[f392]) ).
fof(f2268,plain,
latt_str(sK172_skl),
inference(cnf_transformation,[status(thm)],[f2267]) ).
fof(f2270,plain,
strict_latt_str(sK172_skl),
inference(cnf_transformation,[status(thm)],[f2267]) ).
fof(f2280,plain,
( lattice(sK175_skl)
& join_absorbing(sK175_skl)
& meet_absorbing(sK175_skl)
& meet_associative(sK175_skl)
& meet_commutative(sK175_skl)
& join_associative(sK175_skl)
& join_commutative(sK175_skl)
& strict_latt_str(sK175_skl)
& ~ empty_carrier(sK175_skl)
& latt_str(sK175_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK175_skl]),skolemize(A,sK175_skl)],[f395]) ).
fof(f2281,plain,
latt_str(sK175_skl),
inference(cnf_transformation,[status(thm)],[f2280]) ).
fof(f2283,plain,
strict_latt_str(sK175_skl),
inference(cnf_transformation,[status(thm)],[f2280]) ).
fof(f2295,plain,
! [X0] : k1_pcomps_1(X0) = powerset(X0),
inference(cnf_transformation,[status(thm)],[f398]) ).
fof(f3374,plain,
? [A,B] :
( ( proper_element(B,powerset(A))
<~> B != A )
& element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f628]) ).
fof(f3375,plain,
? [A,B] :
( ( B = A
| ~ proper_element(B,powerset(A)) )
& ( B != A
| proper_element(B,powerset(A)) )
& element(B,powerset(A)) ),
inference(NNF_transformation,[status(thm)],[f3374]) ).
fof(f3376,plain,
( ( sK386_skl = sK385_skl
| ~ proper_element(sK386_skl,powerset(sK385_skl)) )
& ( sK386_skl != sK385_skl
| proper_element(sK386_skl,powerset(sK385_skl)) )
& element(sK386_skl,powerset(sK385_skl)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK385_skl,sK386_skl]),skolemize(A,sK385_skl),skolemize(B,sK386_skl)],[f3375]) ).
fof(f3377,plain,
element(sK386_skl,powerset(sK385_skl)),
inference(cnf_transformation,[status(thm)],[f3376]) ).
fof(f3378,plain,
( sK386_skl != sK385_skl
| proper_element(sK386_skl,powerset(sK385_skl)) ),
inference(cnf_transformation,[status(thm)],[f3376]) ).
fof(f3379,plain,
( sK386_skl = sK385_skl
| ~ proper_element(sK386_skl,powerset(sK385_skl)) ),
inference(cnf_transformation,[status(thm)],[f3376]) ).
fof(f3502,plain,
! [X0] : union(powerset(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f668]) ).
fof(f4195,definition,
( sQ35_spl
<=> proper_element(sK386_skl,powerset(sK385_skl)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f4196,plain,
( ~ sQ35_spl
| proper_element(sK386_skl,powerset(sK385_skl)) ),
inference(component_clause,[status(thm)],[f4195]) ).
fof(f4197,plain,
( sQ35_spl
| ~ proper_element(sK386_skl,powerset(sK385_skl)) ),
inference(component_clause,[status(thm)],[f4195]) ).
fof(f4198,definition,
( sQ36_spl
<=> sK386_skl = sK385_skl ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f4199,plain,
( ~ sQ36_spl
| sK386_skl = sK385_skl ),
inference(component_clause,[status(thm)],[f4198]) ).
fof(f4201,plain,
( ~ sQ36_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f3378,f4195,f4198]) ).
fof(f4202,plain,
( sQ36_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f3379,f4195,f4198]) ).
fof(f4395,plain,
! [X0] :
( ~ proper_element(union(X0),X0)
| ~ element(union(X0),X0) ),
inference(destructive_equality_resolution,[status(thm)],[f1195]) ).
fof(f4648,plain,
( sK386_skl = union(powerset(sK385_skl))
| proper_element(sK386_skl,powerset(sK385_skl)) ),
inference(resolution,[status(thm)],[f1196,f3377]) ).
fof(f4649,definition,
( sQ63_spl
<=> sK386_skl = union(powerset(sK385_skl)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f4650,plain,
( ~ sQ63_spl
| sK386_skl = union(powerset(sK385_skl)) ),
inference(component_clause,[status(thm)],[f4649]) ).
fof(f4652,plain,
( sQ63_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f4648,f4195,f4649]) ).
fof(f4654,plain,
( ~ sQ35_spl
| ~ sQ36_spl
| proper_element(sK386_skl,powerset(sK386_skl)) ),
inference(forward_demodulation,[status(thm)],[f4199,f4196]) ).
fof(f4683,plain,
( sK143_skl = rel_str_of(the_carrier(sK143_skl),the_InternalRel(sK143_skl))
| ~ strict_rel_str(sK143_skl) ),
inference(resolution,[status(thm)],[f2136,f673]) ).
fof(f4684,definition,
( sQ70_spl
<=> strict_rel_str(sK143_skl) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f4686,plain,
( sQ70_spl
| ~ strict_rel_str(sK143_skl) ),
inference(component_clause,[status(thm)],[f4684]) ).
fof(f4687,definition,
( sQ71_spl
<=> sK143_skl = rel_str_of(the_carrier(sK143_skl),the_InternalRel(sK143_skl)) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f4690,plain,
( sQ71_spl
| ~ sQ70_spl ),
inference(split_clause,[status(thm)],[f4683,f4684,f4687]) ).
fof(f4691,plain,
( sK154_skl = rel_str_of(the_carrier(sK154_skl),the_InternalRel(sK154_skl))
| ~ strict_rel_str(sK154_skl) ),
inference(resolution,[status(thm)],[f2189,f673]) ).
fof(f4692,definition,
( sQ72_spl
<=> strict_rel_str(sK154_skl) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f4694,plain,
( sQ72_spl
| ~ strict_rel_str(sK154_skl) ),
inference(component_clause,[status(thm)],[f4692]) ).
fof(f4695,definition,
( sQ73_spl
<=> sK154_skl = rel_str_of(the_carrier(sK154_skl),the_InternalRel(sK154_skl)) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f4698,plain,
( sQ73_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f4691,f4692,f4695]) ).
fof(f4701,plain,
( sK164_skl = latt_str_of(the_carrier(sK164_skl),the_L_join(sK164_skl),the_L_meet(sK164_skl))
| ~ strict_latt_str(sK164_skl) ),
inference(resolution,[status(thm)],[f2233,f675]) ).
fof(f4702,definition,
( sQ74_spl
<=> strict_latt_str(sK164_skl) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f4704,plain,
( sQ74_spl
| ~ strict_latt_str(sK164_skl) ),
inference(component_clause,[status(thm)],[f4702]) ).
fof(f4705,definition,
( sQ75_spl
<=> sK164_skl = latt_str_of(the_carrier(sK164_skl),the_L_join(sK164_skl),the_L_meet(sK164_skl)) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f4708,plain,
( sQ75_spl
| ~ sQ74_spl ),
inference(split_clause,[status(thm)],[f4701,f4702,f4705]) ).
fof(f4711,plain,
( sK172_skl = latt_str_of(the_carrier(sK172_skl),the_L_join(sK172_skl),the_L_meet(sK172_skl))
| ~ strict_latt_str(sK172_skl) ),
inference(resolution,[status(thm)],[f2268,f675]) ).
fof(f4712,definition,
( sQ76_spl
<=> strict_latt_str(sK172_skl) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f4714,plain,
( sQ76_spl
| ~ strict_latt_str(sK172_skl) ),
inference(component_clause,[status(thm)],[f4712]) ).
fof(f4715,definition,
( sQ77_spl
<=> sK172_skl = latt_str_of(the_carrier(sK172_skl),the_L_join(sK172_skl),the_L_meet(sK172_skl)) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f4718,plain,
( sQ77_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f4711,f4712,f4715]) ).
fof(f4719,plain,
( sK175_skl = latt_str_of(the_carrier(sK175_skl),the_L_join(sK175_skl),the_L_meet(sK175_skl))
| ~ strict_latt_str(sK175_skl) ),
inference(resolution,[status(thm)],[f2281,f675]) ).
fof(f4720,definition,
( sQ78_spl
<=> strict_latt_str(sK175_skl) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f4722,plain,
( sQ78_spl
| ~ strict_latt_str(sK175_skl) ),
inference(component_clause,[status(thm)],[f4720]) ).
fof(f4723,definition,
( sQ79_spl
<=> sK175_skl = latt_str_of(the_carrier(sK175_skl),the_L_join(sK175_skl),the_L_meet(sK175_skl)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f4726,plain,
( sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f4719,f4720,f4723]) ).
fof(f4732,plain,
( sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4686,f2137]) ).
fof(f4733,plain,
sQ70_spl,
inference(contradiction_clause,[status(thm)],[f4732]) ).
fof(f4734,plain,
( sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4694,f2191]) ).
fof(f4735,plain,
sQ72_spl,
inference(contradiction_clause,[status(thm)],[f4734]) ).
fof(f4736,plain,
( sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4704,f2234]) ).
fof(f4737,plain,
sQ74_spl,
inference(contradiction_clause,[status(thm)],[f4736]) ).
fof(f4738,plain,
( sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4714,f2270]) ).
fof(f4739,plain,
sQ76_spl,
inference(contradiction_clause,[status(thm)],[f4738]) ).
fof(f4740,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4722,f2283]) ).
fof(f4741,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f4740]) ).
fof(f4768,plain,
( ~ sQ35_spl
| ~ sQ36_spl
| proper_element(sK386_skl,k1_pcomps_1(sK386_skl)) ),
inference(backward_demodulation,[status(thm)],[f2295,f4654]) ).
fof(f4802,plain,
( ~ sQ63_spl
| sK386_skl = union(k1_pcomps_1(sK385_skl)) ),
inference(forward_demodulation,[status(thm)],[f2295,f4650]) ).
fof(f4803,plain,
element(sK386_skl,k1_pcomps_1(sK385_skl)),
inference(forward_demodulation,[status(thm)],[f2295,f3377]) ).
fof(f4804,plain,
( sQ35_spl
| ~ proper_element(sK386_skl,k1_pcomps_1(sK385_skl)) ),
inference(forward_demodulation,[status(thm)],[f2295,f4197]) ).
fof(f4805,plain,
( sK386_skl = union(k1_pcomps_1(sK385_skl))
| proper_element(sK386_skl,k1_pcomps_1(sK385_skl)) ),
inference(resolution,[status(thm)],[f4803,f1196]) ).
fof(f4806,definition,
( sQ84_spl
<=> proper_element(sK386_skl,k1_pcomps_1(sK385_skl)) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f4807,plain,
( ~ sQ84_spl
| proper_element(sK386_skl,k1_pcomps_1(sK385_skl)) ),
inference(component_clause,[status(thm)],[f4806]) ).
fof(f4809,definition,
( sQ85_spl
<=> sK386_skl = union(k1_pcomps_1(sK385_skl)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f4810,plain,
( ~ sQ85_spl
| sK386_skl = union(k1_pcomps_1(sK385_skl)) ),
inference(component_clause,[status(thm)],[f4809]) ).
fof(f4811,plain,
( sQ85_spl
| sK386_skl != union(k1_pcomps_1(sK385_skl)) ),
inference(component_clause,[status(thm)],[f4809]) ).
fof(f4812,plain,
( sQ85_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f4805,f4806,f4809]) ).
fof(f4813,plain,
( ~ sQ63_spl
| ~ proper_element(union(k1_pcomps_1(sK385_skl)),k1_pcomps_1(sK385_skl))
| ~ element(sK386_skl,k1_pcomps_1(sK385_skl)) ),
inference(paramodulation,[status(thm)],[f4802,f4395]) ).
fof(f4814,definition,
( sQ86_spl
<=> element(sK386_skl,k1_pcomps_1(sK385_skl)) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f4816,plain,
( sQ86_spl
| ~ element(sK386_skl,k1_pcomps_1(sK385_skl)) ),
inference(component_clause,[status(thm)],[f4814]) ).
fof(f4817,definition,
( sQ87_spl
<=> proper_element(union(k1_pcomps_1(sK385_skl)),k1_pcomps_1(sK385_skl)) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f4819,plain,
( sQ87_spl
| ~ proper_element(union(k1_pcomps_1(sK385_skl)),k1_pcomps_1(sK385_skl)) ),
inference(component_clause,[status(thm)],[f4817]) ).
fof(f4820,plain,
( ~ sQ63_spl
| ~ sQ87_spl
| ~ sQ86_spl ),
inference(split_clause,[status(thm)],[f4813,f4814,f4817,f4649]) ).
fof(f4821,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4816,f4803]) ).
fof(f4822,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f4821]) ).
fof(f4824,plain,
( ~ sQ84_spl
| sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4807,f4804]) ).
fof(f4825,plain,
( ~ sQ84_spl
| sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f4824]) ).
fof(f4848,plain,
( ~ sQ85_spl
| ~ proper_element(union(k1_pcomps_1(sK385_skl)),k1_pcomps_1(sK385_skl))
| ~ element(sK386_skl,k1_pcomps_1(sK385_skl)) ),
inference(paramodulation,[status(thm)],[f4810,f4395]) ).
fof(f4849,plain,
( ~ sQ85_spl
| ~ sQ87_spl
| ~ sQ86_spl ),
inference(split_clause,[status(thm)],[f4848,f4814,f4817,f4809]) ).
fof(f4901,plain,
( ~ sQ85_spl
| sK386_skl = sK385_skl ),
inference(backward_demodulation,[status(thm)],[f4902,f4810]) ).
fof(f4902,plain,
! [X0] : union(k1_pcomps_1(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f2295,f3502]) ).
fof(f4904,plain,
( ~ sQ85_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f4901,f4198,f4809]) ).
fof(f4917,plain,
( sQ87_spl
| ~ proper_element(sK385_skl,k1_pcomps_1(sK385_skl)) ),
inference(forward_demodulation,[status(thm)],[f4902,f4819]) ).
fof(f4918,plain,
( sQ87_spl
| ~ sQ36_spl
| ~ proper_element(sK386_skl,k1_pcomps_1(sK385_skl)) ),
inference(forward_demodulation,[status(thm)],[f4199,f4917]) ).
fof(f4919,plain,
( sQ87_spl
| ~ sQ36_spl
| ~ proper_element(sK386_skl,k1_pcomps_1(sK386_skl)) ),
inference(forward_demodulation,[status(thm)],[f4199,f4918]) ).
fof(f4920,plain,
( sQ87_spl
| ~ sQ36_spl
| ~ sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4919,f4768]) ).
fof(f4921,plain,
( sQ87_spl
| ~ sQ36_spl
| ~ sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f4920]) ).
fof(f4922,plain,
( sQ85_spl
| sK386_skl != sK385_skl ),
inference(forward_demodulation,[status(thm)],[f4902,f4811]) ).
fof(f4923,plain,
( sQ85_spl
| ~ sQ36_spl
| sK386_skl != sK386_skl ),
inference(forward_demodulation,[status(thm)],[f4199,f4922]) ).
fof(f4924,plain,
( sQ85_spl
| ~ sQ36_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4923]) ).
fof(f4925,plain,
( sQ85_spl
| ~ sQ36_spl ),
inference(contradiction_clause,[status(thm)],[f4924]) ).
fof(f4926,plain,
$false,
inference(sat_refutation,[status(thm)],[f4201,f4202,f4652,f4690,f4698,f4708,f4718,f4726,f4733,f4735,f4737,f4739,f4741,f4812,f4820,f4822,f4825,f4849,f4904,f4921,f4925]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU354+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.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:18:05 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.45 % Drodi V4.1.1
% 0.21/0.50 % Refutation found
% 0.21/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/0.55 % Elapsed time: 0.183840 seconds
% 0.21/0.55 % CPU time: 0.527639 seconds
% 0.21/0.55 % Total memory used: 203.564 MB
% 0.21/0.55 % Net memory used: 202.542 MB
%------------------------------------------------------------------------------