%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU102+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:21:41 PM UTC 2026
% Result : Theorem 0.14s 5.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU102+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n010.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 05:50:49 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 0.14/5.55 % Refutation found
% 0.14/5.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.55 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.55 fof(f2,axiom,(
% 0.14/5.55 (! [A] :( empty(A)=> finite(A) ) )),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f3,axiom,(
% 0.14/5.55 (! [A] :( preboolean(A)=> ( cup_closed(A)& diff_closed(A) ) ) )),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f5,axiom,(
% 0.14/5.55 (! [A] :( ( cup_closed(A)& diff_closed(A) )=> preboolean(A) ) )),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f7,axiom,(
% 0.14/5.55 (! [A,B,C] :( ( ~ empty(A)& preboolean(A)& element(B,A)& element(C,A) )=> element(prebool_difference(A,B,C),A) ) )),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f12,axiom,(
% 0.14/5.55 (! [A] : ~ empty(powerset(A)) )),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f13,axiom,(
% 0.14/5.55 empty(empty_set) ),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f14,axiom,(
% 0.14/5.55 (! [A,B] : set_intersection2(A,A) = A )),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f15,axiom,(
% 0.14/5.55 (? [A] :( ~ empty(A)& finite(A) ) )),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f16,axiom,(
% 0.14/5.55 (? [A] :( ~ empty(A)& cup_closed(A)& cap_closed(A)& diff_closed(A)& preboolean(A) ) )),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f24,axiom,(
% 0.14/5.55 (! [A,B,C] :( ( ~ empty(A)& preboolean(A)& element(B,A)& element(C,A) )=> prebool_difference(A,B,C) = set_difference(B,C) ) )),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f26,conjecture,(
% 0.14/5.55 (! [A,B,C] :( ( ~ empty(C)& preboolean(C) )=> ( ( element(A,C)& element(B,C) )=> element(set_intersection2(A,B),C) ) ) )),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f27,negated_conjecture,(
% 0.14/5.55 ~((! [A,B,C] :( ( ~ empty(C)& preboolean(C) )=> ( ( element(A,C)& element(B,C) )=> element(set_intersection2(A,B),C) ) ) ))),
% 0.14/5.55 inference(negated_conjecture,[status(cth)],[f26])).
% 0.14/5.55 fof(f33,axiom,(
% 0.14/5.55 (! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B) )),
% 0.14/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.55 fof(f42,plain,(
% 0.14/5.55 ![A]: (~empty(A)|finite(A))),
% 0.14/5.55 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/5.55 fof(f43,plain,(
% 0.14/5.55 ![X0]: (~empty(X0)|finite(X0))),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f42])).
% 0.14/5.55 fof(f44,plain,(
% 0.14/5.55 ![A]: (~preboolean(A)|(cup_closed(A)&diff_closed(A)))),
% 0.14/5.55 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.14/5.55 fof(f45,plain,(
% 0.14/5.55 ![X0]: (~preboolean(X0)|cup_closed(X0))),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f44])).
% 0.14/5.55 fof(f46,plain,(
% 0.14/5.55 ![X0]: (~preboolean(X0)|diff_closed(X0))),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f44])).
% 0.14/5.55 fof(f49,plain,(
% 0.14/5.55 ![A]: ((~cup_closed(A)|~diff_closed(A))|preboolean(A))),
% 0.14/5.55 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.14/5.55 fof(f50,plain,(
% 0.14/5.55 ![X0]: (~cup_closed(X0)|~diff_closed(X0)|preboolean(X0))),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f49])).
% 0.14/5.55 fof(f52,plain,(
% 0.14/5.55 ![A,B,C]: ((((empty(A)|~preboolean(A))|~element(B,A))|~element(C,A))|element(prebool_difference(A,B,C),A))),
% 0.14/5.55 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.14/5.55 fof(f53,plain,(
% 0.14/5.55 ![X0,X1,X2]: (empty(X0)|~preboolean(X0)|~element(X1,X0)|~element(X2,X0)|element(prebool_difference(X0,X1,X2),X0))),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f52])).
% 0.14/5.55 fof(f65,plain,(
% 0.14/5.55 ![X0]: (~empty(powerset(X0)))),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.55 fof(f66,plain,(
% 0.14/5.55 empty(empty_set)),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/5.55 fof(f67,plain,(
% 0.14/5.55 ![A]: set_intersection2(A,A)=A),
% 0.14/5.55 inference(miniscoping,[status(thm)],[f14])).
% 0.14/5.55 fof(f68,plain,(
% 0.14/5.55 ![X0]: (set_intersection2(X0,X0)=X0)),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f67])).
% 0.14/5.55 fof(f69,plain,(
% 0.14/5.55 (~empty(sK1_skl)&finite(sK1_skl))),
% 0.14/5.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(A,sK1_skl)],[f15])).
% 0.14/5.55 fof(f70,plain,(
% 0.14/5.55 ~empty(sK1_skl)),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f69])).
% 0.14/5.55 fof(f72,plain,(
% 0.14/5.55 ((((~empty(sK2_skl)&cup_closed(sK2_skl))&cap_closed(sK2_skl))&diff_closed(sK2_skl))&preboolean(sK2_skl))),
% 0.14/5.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f16])).
% 0.14/5.55 fof(f73,plain,(
% 0.14/5.55 ~empty(sK2_skl)),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.55 fof(f110,plain,(
% 0.14/5.55 ![A,B,C]: ((((empty(A)|~preboolean(A))|~element(B,A))|~element(C,A))|prebool_difference(A,B,C)=set_difference(B,C))),
% 0.14/5.55 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.14/5.55 fof(f111,plain,(
% 0.14/5.55 ![X0,X1,X2]: (empty(X0)|~preboolean(X0)|~element(X1,X0)|~element(X2,X0)|prebool_difference(X0,X1,X2)=set_difference(X1,X2))),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f110])).
% 0.14/5.55 fof(f114,plain,(
% 0.14/5.55 (?[A,B,C]: ((~empty(C)&preboolean(C))&((element(A,C)&element(B,C))&~element(set_intersection2(A,B),C))))),
% 0.14/5.55 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.14/5.55 fof(f115,plain,(
% 0.14/5.55 ?[C]: ((~empty(C)&preboolean(C))&(?[A,B]: ((element(A,C)&element(B,C))&~element(set_intersection2(A,B),C))))),
% 0.14/5.55 inference(miniscoping,[status(thm)],[f114])).
% 0.14/5.55 fof(f116,plain,(
% 0.14/5.55 ((~empty(sK10_skl)&preboolean(sK10_skl))&((element(sK11_skl,sK10_skl)&element(sK12_skl,sK10_skl))&~element(set_intersection2(sK11_skl,sK12_skl),sK10_skl)))),
% 0.14/5.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(C,sK10_skl),skolemize(A,sK11_skl),skolemize(B,sK12_skl)],[f115])).
% 0.14/5.55 fof(f117,plain,(
% 0.14/5.55 ~empty(sK10_skl)),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f116])).
% 0.14/5.55 fof(f118,plain,(
% 0.14/5.55 preboolean(sK10_skl)),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f116])).
% 0.14/5.55 fof(f119,plain,(
% 0.14/5.55 element(sK11_skl,sK10_skl)),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f116])).
% 0.14/5.55 fof(f120,plain,(
% 0.14/5.55 element(sK12_skl,sK10_skl)),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f116])).
% 0.14/5.55 fof(f121,plain,(
% 0.14/5.55 ~element(set_intersection2(sK11_skl,sK12_skl),sK10_skl)),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f116])).
% 0.14/5.55 fof(f132,plain,(
% 0.14/5.55 ![X0,X1]: (set_difference(X0,set_difference(X0,X1))=set_intersection2(X0,X1))),
% 0.14/5.55 inference(cnf_transformation,[status(thm)],[f33])).
% 0.14/5.55 fof(f153,plain,(
% 0.14/5.55 finite(empty_set)),
% 0.14/5.55 inference(resolution,[status(thm)],[f43,f66])).
% 0.14/5.55 fof(f154,plain,(
% 0.14/5.55 cup_closed(sK10_skl)),
% 0.14/5.55 inference(resolution,[status(thm)],[f45,f118])).
% 0.14/5.55 fof(f166,plain,(
% 0.14/5.55 diff_closed(sK10_skl)),
% 0.14/5.55 inference(resolution,[status(thm)],[f46,f118])).
% 0.14/5.55 fof(f167,plain,(
% 0.14/5.55 ~cup_closed(sK10_skl)|preboolean(sK10_skl)),
% 0.14/5.55 inference(resolution,[status(thm)],[f166,f50])).
% 0.14/5.55 fof(f168,definition,(
% 0.14/5.55 sQ0_spl <=> (cup_closed(sK10_skl))),
% 0.14/5.55 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/5.55 fof(f170,plain,(
% 0.14/5.55 ~cup_closed(sK10_skl)|sQ0_spl),
% 0.14/5.55 inference(component_clause,[status(thm)],[f168])).
% 0.14/5.55 fof(f171,definition,(
% 0.14/5.55 sQ1_spl <=> (preboolean(sK10_skl))),
% 0.14/5.55 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/5.55 fof(f174,plain,(
% 0.14/5.55 ~sQ0_spl|sQ1_spl),
% 0.14/5.55 inference(split_clause,[status(thm)],[f167,f168,f171])).
% 0.14/5.55 fof(f175,plain,(
% 0.14/5.55 $false|sQ0_spl),
% 0.14/5.55 inference(forward_subsumption_resolution,[status(thm)],[f170,f154])).
% 0.14/5.55 fof(f176,plain,(
% 0.14/5.55 sQ0_spl),
% 0.14/5.55 inference(contradiction_clause,[status(thm)],[f175])).
% 0.14/5.55 fof(f211,plain,(
% 0.14/5.55 ![X0]: (empty(sK10_skl)|~preboolean(sK10_skl)|~element(X0,sK10_skl)|element(prebool_difference(sK10_skl,sK11_skl,X0),sK10_skl))),
% 0.14/5.55 inference(resolution,[status(thm)],[f53,f119])).
% 0.14/5.55 fof(f212,definition,(
% 0.14/5.55 sQ4_spl <=> (empty(sK10_skl))),
% 0.14/5.55 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/5.55 fof(f213,plain,(
% 0.14/5.55 empty(sK10_skl)|~sQ4_spl),
% 0.14/5.55 inference(component_clause,[status(thm)],[f212])).
% 0.14/5.55 fof(f219,definition,(
% 0.14/5.55 ![X0]: (sQ6_spl <=> (~element(X0,sK10_skl)|element(prebool_difference(sK10_skl,sK11_skl,X0),sK10_skl)))),
% 0.14/5.55 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/5.55 fof(f220,plain,(
% 0.14/5.55 ![X0]: (~element(X0,sK10_skl)|element(prebool_difference(sK10_skl,sK11_skl,X0),sK10_skl)|~sQ6_spl)),
% 0.14/5.55 inference(component_clause,[status(thm)],[f219])).
% 0.14/5.55 fof(f222,plain,(
% 0.14/5.55 sQ4_spl|~sQ1_spl|sQ6_spl),
% 0.14/5.55 inference(split_clause,[status(thm)],[f211,f212,f171,f219])).
% 0.14/5.55 fof(f223,plain,(
% 0.14/5.55 $false|~sQ4_spl),
% 0.14/5.55 inference(forward_subsumption_resolution,[status(thm)],[f213,f117])).
% 0.14/5.56 fof(f224,plain,(
% 0.14/5.56 ~sQ4_spl),
% 0.14/5.56 inference(contradiction_clause,[status(thm)],[f223])).
% 0.14/5.56 fof(f236,plain,(
% 0.14/5.56 element(prebool_difference(sK10_skl,sK11_skl,sK12_skl),sK10_skl)|~sQ6_spl),
% 0.14/5.56 inference(resolution,[status(thm)],[f220,f120])).
% 0.14/5.56 fof(f289,plain,(
% 0.14/5.56 element(prebool_difference(sK10_skl,sK11_skl,prebool_difference(sK10_skl,sK11_skl,sK12_skl)),sK10_skl)|~sQ6_spl),
% 0.14/5.56 inference(resolution,[status(thm)],[f236,f220])).
% 0.14/5.56 fof(f323,definition,(
% 0.14/5.56 ![X0]: (sQ14_spl <=> (~finite(X0)))),
% 0.14/5.56 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/5.56 fof(f324,plain,(
% 0.14/5.56 ![X0]: (~finite(X0)|~sQ14_spl)),
% 0.14/5.56 inference(component_clause,[status(thm)],[f323])).
% 0.14/5.56 fof(f332,plain,(
% 0.14/5.56 $false|~sQ14_spl),
% 0.14/5.56 inference(backward_subsumption_resolution,[status(thm)],[f153,f324])).
% 0.14/5.56 fof(f341,plain,(
% 0.14/5.56 ~sQ14_spl),
% 0.14/5.56 inference(contradiction_clause,[status(thm)],[f332])).
% 0.14/5.56 fof(f508,plain,(
% 0.14/5.56 ![X0]: (empty(sK10_skl)|~preboolean(sK10_skl)|~element(X0,sK10_skl)|prebool_difference(sK10_skl,sK11_skl,X0)=set_difference(sK11_skl,X0))),
% 0.14/5.56 inference(resolution,[status(thm)],[f111,f119])).
% 0.14/5.56 fof(f566,definition,(
% 0.14/5.56 ![X0]: (sQ34_spl <=> (~element(X0,sK10_skl)|prebool_difference(sK10_skl,sK11_skl,X0)=set_difference(sK11_skl,X0)))),
% 0.14/5.56 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/5.56 fof(f567,plain,(
% 0.14/5.56 ![X0]: (~element(X0,sK10_skl)|prebool_difference(sK10_skl,sK11_skl,X0)=set_difference(sK11_skl,X0)|~sQ34_spl)),
% 0.14/5.56 inference(component_clause,[status(thm)],[f566])).
% 0.14/5.56 fof(f569,plain,(
% 0.14/5.56 sQ4_spl|~sQ1_spl|sQ34_spl),
% 0.14/5.56 inference(split_clause,[status(thm)],[f508,f212,f171,f566])).
% 0.14/5.56 fof(f706,plain,(
% 0.14/5.56 prebool_difference(sK10_skl,sK11_skl,prebool_difference(sK10_skl,sK11_skl,sK12_skl))=set_difference(sK11_skl,prebool_difference(sK10_skl,sK11_skl,sK12_skl))|~sQ34_spl|~sQ6_spl),
% 0.14/5.56 inference(resolution,[status(thm)],[f567,f236])).
% 0.14/5.56 fof(f715,plain,(
% 0.14/5.56 prebool_difference(sK10_skl,sK11_skl,sK12_skl)=set_difference(sK11_skl,sK12_skl)|~sQ34_spl),
% 0.14/5.56 inference(resolution,[status(thm)],[f567,f120])).
% 0.14/5.56 fof(f933,definition,(
% 0.14/5.56 sQ65_spl <=> (empty(sK1_skl))),
% 0.14/5.56 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.14/5.56 fof(f934,plain,(
% 0.14/5.56 empty(sK1_skl)|~sQ65_spl),
% 0.14/5.56 inference(component_clause,[status(thm)],[f933])).
% 0.14/5.56 fof(f947,plain,(
% 0.14/5.56 $false|~sQ65_spl),
% 0.14/5.56 inference(forward_subsumption_resolution,[status(thm)],[f934,f70])).
% 0.14/5.56 fof(f948,plain,(
% 0.14/5.56 ~sQ65_spl),
% 0.14/5.56 inference(contradiction_clause,[status(thm)],[f947])).
% 0.14/5.56 fof(f1204,definition,(
% 0.14/5.56 sQ81_spl <=> (empty(powerset(sK1_skl)))),
% 0.14/5.56 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.14/5.56 fof(f1205,plain,(
% 0.14/5.56 empty(powerset(sK1_skl))|~sQ81_spl),
% 0.14/5.56 inference(component_clause,[status(thm)],[f1204])).
% 0.14/5.56 fof(f1211,definition,(
% 0.14/5.56 sQ83_spl <=> (empty(powerset(empty_set)))),
% 0.14/5.56 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.14/5.56 fof(f1212,plain,(
% 0.14/5.56 empty(powerset(empty_set))|~sQ83_spl),
% 0.14/5.56 inference(component_clause,[status(thm)],[f1211])).
% 0.14/5.56 fof(f1218,plain,(
% 0.14/5.56 $false|~sQ83_spl),
% 0.14/5.56 inference(forward_subsumption_resolution,[status(thm)],[f1212,f65])).
% 0.14/5.56 fof(f1219,plain,(
% 0.14/5.56 ~sQ83_spl),
% 0.14/5.56 inference(contradiction_clause,[status(thm)],[f1218])).
% 0.14/5.56 fof(f2242,plain,(
% 0.14/5.56 $false|~sQ81_spl),
% 0.14/5.56 inference(forward_subsumption_resolution,[status(thm)],[f1205,f65])).
% 0.14/5.56 fof(f2243,plain,(
% 0.14/5.56 ~sQ81_spl),
% 0.14/5.56 inference(contradiction_clause,[status(thm)],[f2242])).
% 0.14/5.56 fof(f2255,plain,(
% 0.14/5.56 element(prebool_difference(sK10_skl,sK11_skl,set_difference(sK11_skl,sK12_skl)),sK10_skl)|~sQ34_spl|~sQ6_spl),
% 0.14/5.56 inference(forward_demodulation,[status(thm)],[f715,f289])).
% 0.14/5.56 fof(f2400,definition,(
% 0.14/5.56 sQ156_spl <=> (empty(powerset(sK3_skl(sK1_skl))))),
% 0.14/5.56 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 0.14/5.56 fof(f2401,plain,(
% 0.14/5.56 empty(powerset(sK3_skl(sK1_skl)))|~sQ156_spl),
% 0.14/5.56 inference(component_clause,[status(thm)],[f2400])).
% 0.14/5.56 fof(f2411,plain,(
% 0.14/5.56 $false|~sQ156_spl),
% 0.14/5.56 inference(forward_subsumption_resolution,[status(thm)],[f2401,f65])).
% 0.14/5.56 fof(f2412,plain,(
% 0.14/5.56 ~sQ156_spl),
% 0.14/5.56 inference(contradiction_clause,[status(thm)],[f2411])).
% 0.14/5.56 fof(f2478,definition,(
% 0.14/5.56 sQ161_spl <=> (empty(sK2_skl))),
% 0.14/5.56 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 0.14/5.56 fof(f2479,plain,(
% 0.14/5.56 empty(sK2_skl)|~sQ161_spl),
% 0.14/5.56 inference(component_clause,[status(thm)],[f2478])).
% 0.14/5.56 fof(f2489,plain,(
% 0.14/5.56 $false|~sQ161_spl),
% 0.14/5.56 inference(forward_subsumption_resolution,[status(thm)],[f2479,f73])).
% 0.14/5.56 fof(f2490,plain,(
% 0.14/5.56 ~sQ161_spl),
% 0.14/5.56 inference(contradiction_clause,[status(thm)],[f2489])).
% 0.14/5.56 fof(f2688,definition,(
% 0.14/5.56 sQ173_spl <=> (empty(set_intersection2(sK1_skl,sK1_skl)))),
% 0.14/5.56 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 0.14/5.56 fof(f2689,plain,(
% 0.14/5.56 empty(set_intersection2(sK1_skl,sK1_skl))|~sQ173_spl),
% 0.14/5.56 inference(component_clause,[status(thm)],[f2688])).
% 0.14/5.56 fof(f2692,plain,(
% 0.14/5.56 empty(sK1_skl)|~sQ173_spl),
% 0.14/5.56 inference(forward_demodulation,[status(thm)],[f68,f2689])).
% 0.14/5.56 fof(f2693,plain,(
% 0.14/5.56 $false|~sQ173_spl),
% 0.14/5.56 inference(forward_subsumption_resolution,[status(thm)],[f2692,f70])).
% 0.14/5.56 fof(f2694,plain,(
% 0.14/5.56 ~sQ173_spl),
% 0.14/5.56 inference(contradiction_clause,[status(thm)],[f2693])).
% 0.14/5.56 fof(f3080,definition,(
% 0.14/5.56 ![X0]: (sQ178_spl <=> (~empty(X0)))),
% 0.14/5.56 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 0.14/5.56 fof(f3081,plain,(
% 0.14/5.56 ![X0]: (~empty(X0)|~sQ178_spl)),
% 0.14/5.56 inference(component_clause,[status(thm)],[f3080])).
% 0.14/5.56 fof(f3197,plain,(
% 0.14/5.56 $false|~sQ178_spl),
% 0.14/5.56 inference(backward_subsumption_resolution,[status(thm)],[f66,f3081])).
% 0.14/5.56 fof(f3202,plain,(
% 0.14/5.56 ~sQ178_spl),
% 0.14/5.56 inference(contradiction_clause,[status(thm)],[f3197])).
% 0.14/5.56 fof(f3524,plain,(
% 0.14/5.56 prebool_difference(sK10_skl,sK11_skl,set_difference(sK11_skl,sK12_skl))=set_difference(sK11_skl,prebool_difference(sK10_skl,sK11_skl,sK12_skl))|~sQ34_spl|~sQ6_spl),
% 0.14/5.56 inference(forward_demodulation,[status(thm)],[f715,f706])).
% 0.14/5.56 fof(f3525,plain,(
% 0.14/5.56 prebool_difference(sK10_skl,sK11_skl,set_difference(sK11_skl,sK12_skl))=set_difference(sK11_skl,set_difference(sK11_skl,sK12_skl))|~sQ34_spl|~sQ6_spl),
% 0.14/5.56 inference(forward_demodulation,[status(thm)],[f715,f3524])).
% 0.14/5.56 fof(f3526,plain,(
% 0.14/5.56 element(set_intersection2(sK11_skl,sK12_skl),sK10_skl)|~sQ34_spl|~sQ6_spl),
% 0.14/5.56 inference(backward_demodulation,[status(thm)],[f3527,f2255])).
% 0.14/5.56 fof(f3527,plain,(
% 0.14/5.56 prebool_difference(sK10_skl,sK11_skl,set_difference(sK11_skl,sK12_skl))=set_intersection2(sK11_skl,sK12_skl)|~sQ34_spl|~sQ6_spl),
% 0.14/5.56 inference(forward_demodulation,[status(thm)],[f132,f3525])).
% 0.14/5.56 fof(f3528,plain,(
% 0.14/5.56 $false|~sQ34_spl|~sQ6_spl),
% 0.14/5.56 inference(forward_subsumption_resolution,[status(thm)],[f3526,f121])).
% 0.14/5.56 fof(f3529,plain,(
% 0.14/5.56 ~sQ34_spl|~sQ6_spl),
% 0.14/5.56 inference(contradiction_clause,[status(thm)],[f3528])).
% 0.14/5.56 fof(f3530,plain,(
% 0.14/5.56 $false),
% 0.14/5.56 inference(sat_refutation,[status(thm)],[f174,f176,f222,f224,f341,f569,f948,f1219,f2243,f2412,f2490,f2694,f3202,f3529])).
% 0.14/5.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.57 % Elapsed time: 0.183449 seconds
% 0.14/5.57 % CPU time: 1.262629 seconds
% 0.14/5.57 % Total memory used: 125.603 MB
% 0.14/5.57 % Net memory used: 123.826 MB
%------------------------------------------------------------------------------