%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU304+2 : 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 : n001.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:16 PM UTC 2026
% Result : Theorem 0.16s 5.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU304+2 : 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.09/5.38 % Computer : n001.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Mon Sep 21 06:15:34 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.16/5.41 % Drodi V4.1.1
% 0.16/5.45 % Refutation found
% 0.16/5.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/5.45 % SZS output start CNFRefutation for theBenchmark
% 0.16/5.45 fof(f20,axiom,(
% 0.16/5.45 (! [A,B,C] :( ( ~ empty_carrier(A)& meet_commutative(A)& meet_semilatt_str(A)& element(B,the_carrier(A))& element(C,the_carrier(A)) )=> meet_commut(A,B,C) = meet_commut(A,C,B) ) )),
% 0.16/5.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f58,axiom,(
% 0.16/5.45 (! [A] :( ( ~ empty_carrier(A)& join_semilatt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> ( below(A,B,C)<=> join(A,B,C) = C ) ) )) )) )),
% 0.16/5.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f87,axiom,(
% 0.16/5.45 (! [A] :( ( ~ empty_carrier(A)& latt_str(A) )=> ( meet_absorbing(A)<=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> join(A,meet(A,B,C),C) = C ) )) )) ) )),
% 0.16/5.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f122,axiom,(
% 0.16/5.45 (! [A,B,C] :( ( ~ empty_carrier(A)& meet_commutative(A)& meet_semilatt_str(A)& element(B,the_carrier(A))& element(C,the_carrier(A)) )=> element(meet_commut(A,B,C),the_carrier(A)) ) )),
% 0.16/5.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f141,axiom,(
% 0.16/5.45 (! [A] :( latt_str(A)=> ( meet_semilatt_str(A)& join_semilatt_str(A) ) ) )),
% 0.16/5.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f245,axiom,(
% 0.16/5.45 (! [A,B,C] :( ( ~ empty_carrier(A)& meet_commutative(A)& meet_semilatt_str(A)& element(B,the_carrier(A))& element(C,the_carrier(A)) )=> meet_commut(A,B,C) = meet(A,B,C) ) )),
% 0.16/5.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f339,conjecture,(
% 0.16/5.45 (! [A] :( ( ~ empty_carrier(A)& meet_commutative(A)& meet_absorbing(A)& latt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> below(A,meet_commut(A,B,C),B) ) )) )) )),
% 0.16/5.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f340,negated_conjecture,(
% 0.16/5.45 ~((! [A] :( ( ~ empty_carrier(A)& meet_commutative(A)& meet_absorbing(A)& latt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> below(A,meet_commut(A,B,C),B) ) )) )) ))),
% 0.16/5.45 inference(negated_conjecture,[status(cth)],[f339])).
% 0.16/5.45 fof(f502,plain,(
% 0.16/5.45 ![A,B,C]: (((((empty_carrier(A)|~meet_commutative(A))|~meet_semilatt_str(A))|~element(B,the_carrier(A)))|~element(C,the_carrier(A)))|meet_commut(A,B,C)=meet_commut(A,C,B))),
% 0.16/5.45 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.16/5.45 fof(f503,plain,(
% 0.16/5.45 ![X0,X1,X2]: (empty_carrier(X0)|~meet_commutative(X0)|~meet_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|meet_commut(X0,X1,X2)=meet_commut(X0,X2,X1))),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f502])).
% 0.16/5.45 fof(f773,plain,(
% 0.16/5.45 ![A]: ((empty_carrier(A)|~join_semilatt_str(A))|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|(below(A,B,C)<=>join(A,B,C)=C))))))),
% 0.16/5.45 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.16/5.45 fof(f774,plain,(
% 0.16/5.45 ![A]: ((empty_carrier(A)|~join_semilatt_str(A))|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|((~below(A,B,C)|join(A,B,C)=C)&(below(A,B,C)|~join(A,B,C)=C)))))))),
% 0.16/5.45 inference(NNF_transformation,[status(thm)],[f773])).
% 0.16/5.45 fof(f776,plain,(
% 0.16/5.45 ![X0,X1,X2]: (empty_carrier(X0)|~join_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|below(X0,X1,X2)|~join(X0,X1,X2)=X2)),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f774])).
% 0.16/5.45 fof(f977,plain,(
% 0.16/5.45 ![A]: ((empty_carrier(A)|~latt_str(A))|(meet_absorbing(A)<=>(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|join(A,meet(A,B,C),C)=C))))))),
% 0.16/5.45 inference(pre_NNF_transformation,[status(thm)],[f87])).
% 0.16/5.45 fof(f978,plain,(
% 0.16/5.45 ![A]: ((empty_carrier(A)|~latt_str(A))|((~meet_absorbing(A)|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|join(A,meet(A,B,C),C)=C)))))&(meet_absorbing(A)|(?[B]: (element(B,the_carrier(A))&(?[C]: (element(C,the_carrier(A))&~join(A,meet(A,B,C),C)=C)))))))),
% 0.16/5.45 inference(NNF_transformation,[status(thm)],[f977])).
% 0.16/5.45 fof(f979,plain,(
% 0.16/5.45 ![A]: ((empty_carrier(A)|~latt_str(A))|((~meet_absorbing(A)|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|join(A,meet(A,B,C),C)=C)))))&(meet_absorbing(A)|(element(sK83_skl(A),the_carrier(A))&(element(sK84_skl(A),the_carrier(A))&~join(A,meet(A,sK83_skl(A),sK84_skl(A)),sK84_skl(A))=sK84_skl(A))))))),
% 0.16/5.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK83_skl,sK84_skl]),skolemize(B,sK83_skl(A)),skolemize(C,sK84_skl(A))],[f978])).
% 0.16/5.45 fof(f980,plain,(
% 0.16/5.45 ![X0,X1,X2]: (empty_carrier(X0)|~latt_str(X0)|~meet_absorbing(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|join(X0,meet(X0,X1,X2),X2)=X2)),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f979])).
% 0.16/5.45 fof(f1040,plain,(
% 0.16/5.45 ![A,B,C]: (((((empty_carrier(A)|~meet_commutative(A))|~meet_semilatt_str(A))|~element(B,the_carrier(A)))|~element(C,the_carrier(A)))|element(meet_commut(A,B,C),the_carrier(A)))),
% 0.16/5.45 inference(pre_NNF_transformation,[status(thm)],[f122])).
% 0.16/5.45 fof(f1041,plain,(
% 0.16/5.45 ![X0,X1,X2]: (empty_carrier(X0)|~meet_commutative(X0)|~meet_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|element(meet_commut(X0,X1,X2),the_carrier(X0)))),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f1040])).
% 0.16/5.45 fof(f1069,plain,(
% 0.16/5.45 ![A]: (~latt_str(A)|(meet_semilatt_str(A)&join_semilatt_str(A)))),
% 0.16/5.45 inference(pre_NNF_transformation,[status(thm)],[f141])).
% 0.16/5.45 fof(f1070,plain,(
% 0.16/5.45 ![X0]: (~latt_str(X0)|meet_semilatt_str(X0))),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f1069])).
% 0.16/5.45 fof(f1071,plain,(
% 0.16/5.45 ![X0]: (~latt_str(X0)|join_semilatt_str(X0))),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f1069])).
% 0.16/5.45 fof(f1408,plain,(
% 0.16/5.45 ![A,B,C]: (((((empty_carrier(A)|~meet_commutative(A))|~meet_semilatt_str(A))|~element(B,the_carrier(A)))|~element(C,the_carrier(A)))|meet_commut(A,B,C)=meet(A,B,C))),
% 0.16/5.45 inference(pre_NNF_transformation,[status(thm)],[f245])).
% 0.16/5.45 fof(f1409,plain,(
% 0.16/5.45 ![X0,X1,X2]: (empty_carrier(X0)|~meet_commutative(X0)|~meet_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|meet_commut(X0,X1,X2)=meet(X0,X1,X2))),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f1408])).
% 0.16/5.45 fof(f1918,plain,(
% 0.16/5.45 (?[A]: ((((~empty_carrier(A)&meet_commutative(A))&meet_absorbing(A))&latt_str(A))&(?[B]: (element(B,the_carrier(A))&(?[C]: (element(C,the_carrier(A))&~below(A,meet_commut(A,B,C),B)))))))),
% 0.16/5.45 inference(pre_NNF_transformation,[status(thm)],[f340])).
% 0.16/5.45 fof(f1919,plain,(
% 0.16/5.45 ((((~empty_carrier(sK254_skl)&meet_commutative(sK254_skl))&meet_absorbing(sK254_skl))&latt_str(sK254_skl))&(element(sK255_skl,the_carrier(sK254_skl))&(element(sK256_skl,the_carrier(sK254_skl))&~below(sK254_skl,meet_commut(sK254_skl,sK255_skl,sK256_skl),sK255_skl))))),
% 0.16/5.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK254_skl,sK255_skl,sK256_skl]),skolemize(A,sK254_skl),skolemize(B,sK255_skl),skolemize(C,sK256_skl)],[f1918])).
% 0.16/5.45 fof(f1920,plain,(
% 0.16/5.45 ~empty_carrier(sK254_skl)),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f1919])).
% 0.16/5.45 fof(f1921,plain,(
% 0.16/5.45 meet_commutative(sK254_skl)),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f1919])).
% 0.16/5.45 fof(f1922,plain,(
% 0.16/5.45 meet_absorbing(sK254_skl)),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f1919])).
% 0.16/5.45 fof(f1923,plain,(
% 0.16/5.45 latt_str(sK254_skl)),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f1919])).
% 0.16/5.45 fof(f1924,plain,(
% 0.16/5.45 element(sK255_skl,the_carrier(sK254_skl))),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f1919])).
% 0.16/5.45 fof(f1925,plain,(
% 0.16/5.45 element(sK256_skl,the_carrier(sK254_skl))),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f1919])).
% 0.16/5.45 fof(f1926,plain,(
% 0.16/5.45 ~below(sK254_skl,meet_commut(sK254_skl,sK255_skl,sK256_skl),sK255_skl)),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f1919])).
% 0.16/5.45 fof(f3077,plain,(
% 0.16/5.45 meet_semilatt_str(sK254_skl)),
% 0.16/5.45 inference(resolution,[status(thm)],[f1070,f1923])).
% 0.16/5.45 fof(f3078,plain,(
% 0.16/5.45 join_semilatt_str(sK254_skl)),
% 0.16/5.45 inference(resolution,[status(thm)],[f1071,f1923])).
% 0.16/5.45 fof(f3092,plain,(
% 0.16/5.45 ![X0]: (empty_carrier(sK254_skl)|~meet_commutative(sK254_skl)|~meet_semilatt_str(sK254_skl)|~element(X0,the_carrier(sK254_skl))|meet_commut(sK254_skl,X0,sK256_skl)=meet_commut(sK254_skl,sK256_skl,X0))),
% 0.16/5.45 inference(resolution,[status(thm)],[f503,f1925])).
% 0.16/5.45 fof(f3094,definition,(
% 0.16/5.45 sQ60_spl <=> (empty_carrier(sK254_skl))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3095,plain,(
% 0.16/5.45 empty_carrier(sK254_skl)|~sQ60_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3094])).
% 0.16/5.45 fof(f3097,definition,(
% 0.16/5.45 sQ61_spl <=> (meet_commutative(sK254_skl))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3099,plain,(
% 0.16/5.45 ~meet_commutative(sK254_skl)|sQ61_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3097])).
% 0.16/5.45 fof(f3100,definition,(
% 0.16/5.45 sQ62_spl <=> (meet_semilatt_str(sK254_skl))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3102,plain,(
% 0.16/5.45 ~meet_semilatt_str(sK254_skl)|sQ62_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3100])).
% 0.16/5.45 fof(f3103,definition,(
% 0.16/5.45 ![X0]: (sQ63_spl <=> (~element(X0,the_carrier(sK254_skl))|meet_commut(sK254_skl,X0,sK256_skl)=meet_commut(sK254_skl,sK256_skl,X0)))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3104,plain,(
% 0.16/5.45 ![X0]: (~element(X0,the_carrier(sK254_skl))|meet_commut(sK254_skl,X0,sK256_skl)=meet_commut(sK254_skl,sK256_skl,X0)|~sQ63_spl)),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3103])).
% 0.16/5.45 fof(f3106,plain,(
% 0.16/5.45 sQ60_spl|~sQ61_spl|~sQ62_spl|sQ63_spl),
% 0.16/5.45 inference(split_clause,[status(thm)],[f3092,f3094,f3097,f3100,f3103])).
% 0.16/5.45 fof(f3111,plain,(
% 0.16/5.45 $false|sQ62_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f3102,f3077])).
% 0.16/5.45 fof(f3112,plain,(
% 0.16/5.45 sQ62_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f3111])).
% 0.16/5.45 fof(f3113,plain,(
% 0.16/5.45 $false|sQ61_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f3099,f1921])).
% 0.16/5.45 fof(f3114,plain,(
% 0.16/5.45 sQ61_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f3113])).
% 0.16/5.45 fof(f3115,plain,(
% 0.16/5.45 $false|~sQ60_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f3095,f1920])).
% 0.16/5.45 fof(f3116,plain,(
% 0.16/5.45 ~sQ60_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f3115])).
% 0.16/5.45 fof(f3119,definition,(
% 0.16/5.45 sQ65_spl <=> (join_semilatt_str(sK254_skl))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3121,plain,(
% 0.16/5.45 ~join_semilatt_str(sK254_skl)|sQ65_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3119])).
% 0.16/5.45 fof(f3130,plain,(
% 0.16/5.45 $false|sQ65_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f3121,f3078])).
% 0.16/5.45 fof(f3131,plain,(
% 0.16/5.45 sQ65_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f3130])).
% 0.16/5.45 fof(f3145,plain,(
% 0.16/5.45 meet_commut(sK254_skl,sK255_skl,sK256_skl)=meet_commut(sK254_skl,sK256_skl,sK255_skl)|~sQ63_spl),
% 0.16/5.45 inference(resolution,[status(thm)],[f3104,f1924])).
% 0.16/5.45 fof(f3146,plain,(
% 0.16/5.45 ~below(sK254_skl,meet_commut(sK254_skl,sK256_skl,sK255_skl),sK255_skl)|~sQ63_spl),
% 0.16/5.45 inference(backward_demodulation,[status(thm)],[f3145,f1926])).
% 0.16/5.45 fof(f3182,plain,(
% 0.16/5.45 ![X0]: (empty_carrier(sK254_skl)|~latt_str(sK254_skl)|~meet_absorbing(sK254_skl)|~element(X0,the_carrier(sK254_skl))|join(sK254_skl,meet(sK254_skl,X0,sK255_skl),sK255_skl)=sK255_skl)),
% 0.16/5.45 inference(resolution,[status(thm)],[f980,f1924])).
% 0.16/5.45 fof(f3183,definition,(
% 0.16/5.45 sQ78_spl <=> (latt_str(sK254_skl))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3185,plain,(
% 0.16/5.45 ~latt_str(sK254_skl)|sQ78_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3183])).
% 0.16/5.45 fof(f3186,definition,(
% 0.16/5.45 sQ79_spl <=> (meet_absorbing(sK254_skl))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3188,plain,(
% 0.16/5.45 ~meet_absorbing(sK254_skl)|sQ79_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3186])).
% 0.16/5.45 fof(f3193,definition,(
% 0.16/5.45 ![X0]: (sQ81_spl <=> (~element(X0,the_carrier(sK254_skl))|join(sK254_skl,meet(sK254_skl,X0,sK255_skl),sK255_skl)=sK255_skl))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3194,plain,(
% 0.16/5.45 ![X0]: (~element(X0,the_carrier(sK254_skl))|join(sK254_skl,meet(sK254_skl,X0,sK255_skl),sK255_skl)=sK255_skl|~sQ81_spl)),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3193])).
% 0.16/5.45 fof(f3196,plain,(
% 0.16/5.45 sQ60_spl|~sQ78_spl|~sQ79_spl|sQ81_spl),
% 0.16/5.45 inference(split_clause,[status(thm)],[f3182,f3094,f3183,f3186,f3193])).
% 0.16/5.45 fof(f3197,plain,(
% 0.16/5.45 $false|sQ79_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f3188,f1922])).
% 0.16/5.45 fof(f3198,plain,(
% 0.16/5.45 sQ79_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f3197])).
% 0.16/5.45 fof(f3199,plain,(
% 0.16/5.45 $false|sQ78_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f3185,f1923])).
% 0.16/5.45 fof(f3200,plain,(
% 0.16/5.45 sQ78_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f3199])).
% 0.16/5.45 fof(f3219,plain,(
% 0.16/5.45 ![X0]: (empty_carrier(sK254_skl)|~meet_commutative(sK254_skl)|~meet_semilatt_str(sK254_skl)|~element(X0,the_carrier(sK254_skl))|element(meet_commut(sK254_skl,sK256_skl,X0),the_carrier(sK254_skl)))),
% 0.16/5.45 inference(resolution,[status(thm)],[f1041,f1925])).
% 0.16/5.45 fof(f3221,definition,(
% 0.16/5.45 ![X0]: (sQ86_spl <=> (~element(X0,the_carrier(sK254_skl))|element(meet_commut(sK254_skl,sK256_skl,X0),the_carrier(sK254_skl))))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3222,plain,(
% 0.16/5.45 ![X0]: (~element(X0,the_carrier(sK254_skl))|element(meet_commut(sK254_skl,sK256_skl,X0),the_carrier(sK254_skl))|~sQ86_spl)),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3221])).
% 0.16/5.45 fof(f3224,plain,(
% 0.16/5.45 sQ60_spl|~sQ61_spl|~sQ62_spl|sQ86_spl),
% 0.16/5.45 inference(split_clause,[status(thm)],[f3219,f3094,f3097,f3100,f3221])).
% 0.16/5.45 fof(f3230,plain,(
% 0.16/5.45 ![X0]: (empty_carrier(sK254_skl)|~meet_commutative(sK254_skl)|~meet_semilatt_str(sK254_skl)|~element(X0,the_carrier(sK254_skl))|meet_commut(sK254_skl,X0,sK255_skl)=meet(sK254_skl,X0,sK255_skl))),
% 0.16/5.45 inference(resolution,[status(thm)],[f1409,f1924])).
% 0.16/5.45 fof(f3235,definition,(
% 0.16/5.45 ![X0]: (sQ89_spl <=> (~element(X0,the_carrier(sK254_skl))|meet_commut(sK254_skl,X0,sK255_skl)=meet(sK254_skl,X0,sK255_skl)))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3236,plain,(
% 0.16/5.45 ![X0]: (~element(X0,the_carrier(sK254_skl))|meet_commut(sK254_skl,X0,sK255_skl)=meet(sK254_skl,X0,sK255_skl)|~sQ89_spl)),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3235])).
% 0.16/5.45 fof(f3238,plain,(
% 0.16/5.45 sQ60_spl|~sQ61_spl|~sQ62_spl|sQ89_spl),
% 0.16/5.45 inference(split_clause,[status(thm)],[f3230,f3094,f3097,f3100,f3235])).
% 0.16/5.45 fof(f3262,plain,(
% 0.16/5.45 join(sK254_skl,meet(sK254_skl,sK256_skl,sK255_skl),sK255_skl)=sK255_skl|~sQ81_spl),
% 0.16/5.45 inference(resolution,[status(thm)],[f3194,f1925])).
% 0.16/5.45 fof(f3264,plain,(
% 0.16/5.45 empty_carrier(sK254_skl)|~join_semilatt_str(sK254_skl)|~element(meet(sK254_skl,sK256_skl,sK255_skl),the_carrier(sK254_skl))|~element(sK255_skl,the_carrier(sK254_skl))|below(sK254_skl,meet(sK254_skl,sK256_skl,sK255_skl),sK255_skl)|~sQ81_spl),
% 0.16/5.45 inference(resolution,[status(thm)],[f3262,f776])).
% 0.16/5.45 fof(f3266,definition,(
% 0.16/5.45 sQ94_spl <=> (element(meet(sK254_skl,sK256_skl,sK255_skl),the_carrier(sK254_skl)))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3268,plain,(
% 0.16/5.45 ~element(meet(sK254_skl,sK256_skl,sK255_skl),the_carrier(sK254_skl))|sQ94_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3266])).
% 0.16/5.45 fof(f3269,definition,(
% 0.16/5.45 sQ95_spl <=> (element(sK255_skl,the_carrier(sK254_skl)))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3271,plain,(
% 0.16/5.45 ~element(sK255_skl,the_carrier(sK254_skl))|sQ95_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3269])).
% 0.16/5.45 fof(f3272,definition,(
% 0.16/5.45 sQ96_spl <=> (below(sK254_skl,meet(sK254_skl,sK256_skl,sK255_skl),sK255_skl))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f3273,plain,(
% 0.16/5.45 below(sK254_skl,meet(sK254_skl,sK256_skl,sK255_skl),sK255_skl)|~sQ96_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f3272])).
% 0.16/5.45 fof(f3275,plain,(
% 0.16/5.45 sQ60_spl|~sQ65_spl|~sQ94_spl|~sQ95_spl|sQ96_spl|~sQ81_spl),
% 0.16/5.45 inference(split_clause,[status(thm)],[f3264,f3094,f3119,f3266,f3269,f3272,f3193])).
% 0.16/5.45 fof(f3290,plain,(
% 0.16/5.45 $false|sQ95_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f3271,f1924])).
% 0.16/5.45 fof(f3291,plain,(
% 0.16/5.45 sQ95_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f3290])).
% 0.16/5.45 fof(f3293,plain,(
% 0.16/5.45 element(meet_commut(sK254_skl,sK256_skl,sK255_skl),the_carrier(sK254_skl))|~sQ86_spl),
% 0.16/5.45 inference(resolution,[status(thm)],[f3222,f1924])).
% 0.16/5.45 fof(f3497,plain,(
% 0.16/5.45 meet_commut(sK254_skl,sK256_skl,sK255_skl)=meet(sK254_skl,sK256_skl,sK255_skl)|~sQ89_spl),
% 0.16/5.45 inference(resolution,[status(thm)],[f3236,f1925])).
% 0.16/5.45 fof(f3571,plain,(
% 0.16/5.45 element(meet(sK254_skl,sK256_skl,sK255_skl),the_carrier(sK254_skl))|~sQ89_spl|~sQ86_spl),
% 0.16/5.45 inference(backward_demodulation,[status(thm)],[f3497,f3293])).
% 0.16/5.45 fof(f3572,plain,(
% 0.16/5.45 ~below(sK254_skl,meet(sK254_skl,sK256_skl,sK255_skl),sK255_skl)|~sQ89_spl|~sQ63_spl),
% 0.16/5.45 inference(backward_demodulation,[status(thm)],[f3497,f3146])).
% 0.16/5.45 fof(f3573,plain,(
% 0.16/5.45 $false|sQ94_spl|~sQ89_spl|~sQ86_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f3571,f3268])).
% 0.16/5.45 fof(f3574,plain,(
% 0.16/5.45 sQ94_spl|~sQ89_spl|~sQ86_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f3573])).
% 0.16/5.45 fof(f3601,plain,(
% 0.16/5.45 $false|~sQ89_spl|~sQ63_spl|~sQ96_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f3273,f3572])).
% 0.16/5.45 fof(f3602,plain,(
% 0.16/5.45 ~sQ89_spl|~sQ63_spl|~sQ96_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f3601])).
% 0.16/5.45 fof(f3603,plain,(
% 0.16/5.45 $false),
% 0.16/5.45 inference(sat_refutation,[status(thm)],[f3106,f3112,f3114,f3116,f3131,f3196,f3198,f3200,f3224,f3238,f3275,f3291,f3574,f3602])).
% 0.16/5.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/5.49 % Elapsed time: 0.095107 seconds
% 0.16/5.49 % CPU time: 0.374508 seconds
% 0.16/5.49 % Total memory used: 164.886 MB
% 0.16/5.49 % Net memory used: 164.008 MB
%------------------------------------------------------------------------------