%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC241+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:41:57 PM UTC 2026
% Result : Theorem 7.10s 6.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC241+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n006.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Mon Sep 21 08:08:03 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.39 % Drodi V4.1.1
% 7.10/6.37 % Refutation found
% 7.10/6.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.10/6.37 % SZS output start CNFRefutation for theBenchmark
% 7.10/6.37 fof(f2,axiom,(
% 7.10/6.37 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 7.10/6.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.10/6.37 fof(f17,axiom,(
% 7.10/6.37 ssList(nil) ),
% 7.10/6.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.10/6.37 fof(f31,axiom,(
% 7.10/6.37 (! [U] :( ssItem(U)=> leq(U,U) ) )),
% 7.10/6.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.10/6.37 fof(f93,axiom,(
% 7.10/6.37 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> ( lt(U,V)<=> ( U != V& leq(U,V) ) ) ) )) )),
% 7.10/6.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.10/6.37 fof(f96,conjecture,(
% 7.10/6.37 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| nil = U| (? [Y] :( ssItem(Y)& (? [Z] :( ssList(Z)& (? [X1] :( ssList(X1)& app(app(Z,cons(Y,nil)),X1) = U& (! [X2] :( ~ ssItem(X2)| ~ memberP(Z,X2)| ~ memberP(X1,X2)| ~ lt(Y,X2)| leq(Y,X2) ) )) )) )))| ( nil != W& (! [X3] :( ssItem(X3)=> (! [X4] :( ssList(X4)=> (! [X5] :( ~ ssList(X5)| app(app(X4,cons(X3,nil)),X5) != W| (? [X6] :( ssItem(X6)& ~ leq(X6,X3)& memberP(X4,X6)& memberP(X5,X6)& leq(X3,X6) ) )) )) )) )) ) )) )) )) )),
% 7.10/6.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.10/6.37 fof(f97,negated_conjecture,(
% 7.10/6.37 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| nil = U| (? [Y] :( ssItem(Y)& (? [Z] :( ssList(Z)& (? [X1] :( ssList(X1)& app(app(Z,cons(Y,nil)),X1) = U& (! [X2] :( ~ ssItem(X2)| ~ memberP(Z,X2)| ~ memberP(X1,X2)| ~ lt(Y,X2)| leq(Y,X2) ) )) )) )))| ( nil != W& (! [X3] :( ssItem(X3)=> (! [X4] :( ssList(X4)=> (! [X5] :( ~ ssList(X5)| app(app(X4,cons(X3,nil)),X5) != W| (? [X6] :( ssItem(X6)& ~ leq(X6,X3)& memberP(X4,X6)& memberP(X5,X6)& leq(X3,X6) ) )) )) )) )) ) )) )) )) ))),
% 7.10/6.37 inference(negated_conjecture,[status(cth)],[f96])).
% 7.10/6.37 fof(f102,plain,(
% 7.10/6.37 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 7.10/6.37 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 7.10/6.37 fof(f103,plain,(
% 7.10/6.37 ssItem(sK0_skl)),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f102])).
% 7.10/6.37 fof(f104,plain,(
% 7.10/6.37 ssItem(sK1_skl)),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f102])).
% 7.10/6.37 fof(f105,plain,(
% 7.10/6.37 ~sK0_skl=sK1_skl),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f102])).
% 7.10/6.37 fof(f223,plain,(
% 7.10/6.37 ssList(nil)),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f17])).
% 7.10/6.37 fof(f254,plain,(
% 7.10/6.37 ![U]: (~ssItem(U)|leq(U,U))),
% 7.10/6.37 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 7.10/6.37 fof(f255,plain,(
% 7.10/6.37 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f254])).
% 7.10/6.37 fof(f406,plain,(
% 7.10/6.37 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(lt(U,V)<=>(~U=V&leq(U,V))))))),
% 7.10/6.37 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 7.10/6.37 fof(f407,plain,(
% 7.10/6.37 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|((~lt(U,V)|(~U=V&leq(U,V)))&(lt(U,V)|(U=V|~leq(U,V)))))))),
% 7.10/6.37 inference(NNF_transformation,[status(thm)],[f406])).
% 7.10/6.37 fof(f409,plain,(
% 7.10/6.37 ![X0,X1]: (~ssItem(X0)|~ssItem(X1)|~lt(X0,X1)|leq(X0,X1))),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f407])).
% 7.10/6.37 fof(f415,plain,(
% 7.10/6.37 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (((((ssList(X)&V=X)&U=W)&~nil=U)&(![Y]: (~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((~ssList(X1)|~app(app(Z,cons(Y,nil)),X1)=U)|(?[X2]: ((((ssItem(X2)&memberP(Z,X2))&memberP(X1,X2))<(Y,X2))&~leq(Y,X2))))))))))&(nil=W|(?[X3]: (ssItem(X3)&(?[X4]: (ssList(X4)&(?[X5]: ((ssList(X5)&app(app(X4,cons(X3,nil)),X5)=W)&(![X6]: ((((~ssItem(X6)|leq(X6,X3))|~memberP(X4,X6))|~memberP(X5,X6))|~leq(X3,X6))))))))))))))))))),
% 7.10/6.37 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 7.10/6.37 fof(f416,plain,(
% 7.10/6.37 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(((((?[X]: (ssList(X)&V=X))&U=W)&~nil=U)&(![Y]: (~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((~ssList(X1)|~app(app(Z,cons(Y,nil)),X1)=U)|(?[X2]: ((((ssItem(X2)&memberP(Z,X2))&memberP(X1,X2))<(Y,X2))&~leq(Y,X2))))))))))&(nil=W|(?[X3]: (ssItem(X3)&(?[X4]: (ssList(X4)&(?[X5]: ((ssList(X5)&app(app(X4,cons(X3,nil)),X5)=W)&(![X6]: ((((~ssItem(X6)|leq(X6,X3))|~memberP(X4,X6))|~memberP(X5,X6))|~leq(X3,X6))))))))))))))))),
% 7.10/6.37 inference(miniscoping,[status(thm)],[f415])).
% 7.10/6.37 fof(f417,plain,(
% 7.10/6.37 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(((((ssList(sK50_skl)&sK48_skl=sK50_skl)&sK47_skl=sK49_skl)&~nil=sK47_skl)&(![Y]: (~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((~ssList(X1)|~app(app(Z,cons(Y,nil)),X1)=sK47_skl)|((((ssItem(sK51_skl(X1,Z,Y))&memberP(Z,sK51_skl(X1,Z,Y)))&memberP(X1,sK51_skl(X1,Z,Y)))<(Y,sK51_skl(X1,Z,Y)))&~leq(Y,sK51_skl(X1,Z,Y))))))))))&(nil=sK49_skl|(ssItem(sK52_skl)&(ssList(sK53_skl)&((ssList(sK54_skl)&app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK49_skl)&(![X6]: ((((~ssItem(X6)|leq(X6,sK52_skl))|~memberP(sK53_skl,X6))|~memberP(sK54_skl,X6))|~leq(sK52_skl,X6)))))))))))),
% 7.10/6.37 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl,sK53_skl,sK54_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(X2,sK51_skl(X1,Z,Y)),skolemize(X3,sK52_skl),skolemize(X4,sK53_skl),skolemize(X5,sK54_skl)],[f416])).
% 7.10/6.37 fof(f418,plain,(
% 7.10/6.37 ssList(sK47_skl)),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f417])).
% 7.10/6.37 fof(f419,plain,(
% 7.10/6.37 ssList(sK48_skl)),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f417])).
% 7.10/6.37 fof(f423,plain,(
% 7.10/6.37 sK47_skl=sK49_skl),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f417])).
% 7.10/6.37 fof(f424,plain,(
% 7.10/6.37 ~nil=sK47_skl),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f417])).
% 7.10/6.37 fof(f425,plain,(
% 7.10/6.37 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK47_skl|ssItem(sK51_skl(X2,X1,X0)))),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f417])).
% 7.10/6.37 fof(f428,plain,(
% 7.10/6.37 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK47_skl|lt(X0,sK51_skl(X2,X1,X0)))),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f417])).
% 7.10/6.37 fof(f429,plain,(
% 7.10/6.37 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK47_skl|~leq(X0,sK51_skl(X2,X1,X0)))),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f417])).
% 7.10/6.37 fof(f430,plain,(
% 7.10/6.37 nil=sK49_skl|ssItem(sK52_skl)),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f417])).
% 7.10/6.37 fof(f431,plain,(
% 7.10/6.37 nil=sK49_skl|ssList(sK53_skl)),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f417])).
% 7.10/6.37 fof(f432,plain,(
% 7.10/6.37 nil=sK49_skl|ssList(sK54_skl)),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f417])).
% 7.10/6.37 fof(f433,plain,(
% 7.10/6.37 nil=sK49_skl|app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK49_skl),
% 7.10/6.37 inference(cnf_transformation,[status(thm)],[f417])).
% 7.10/6.37 fof(f435,definition,(
% 7.10/6.37 sQ0_spl <=> (nil=sK49_skl)),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f436,plain,(
% 7.10/6.37 nil=sK49_skl|~sQ0_spl),
% 7.10/6.37 inference(component_clause,[status(thm)],[f435])).
% 7.10/6.37 fof(f438,definition,(
% 7.10/6.37 sQ1_spl <=> (ssItem(sK52_skl))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f441,plain,(
% 7.10/6.37 sQ0_spl|sQ1_spl),
% 7.10/6.37 inference(split_clause,[status(thm)],[f430,f435,f438])).
% 7.10/6.37 fof(f442,definition,(
% 7.10/6.37 sQ2_spl <=> (ssList(sK53_skl))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f445,plain,(
% 7.10/6.37 sQ0_spl|sQ2_spl),
% 7.10/6.37 inference(split_clause,[status(thm)],[f431,f435,f442])).
% 7.10/6.37 fof(f446,definition,(
% 7.10/6.37 sQ3_spl <=> (ssList(sK54_skl))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f449,plain,(
% 7.10/6.37 sQ0_spl|sQ3_spl),
% 7.10/6.37 inference(split_clause,[status(thm)],[f432,f435,f446])).
% 7.10/6.37 fof(f450,definition,(
% 7.10/6.37 sQ4_spl <=> (app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK49_skl)),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f451,plain,(
% 7.10/6.37 app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK49_skl|~sQ4_spl),
% 7.10/6.37 inference(component_clause,[status(thm)],[f450])).
% 7.10/6.37 fof(f453,plain,(
% 7.10/6.37 sQ0_spl|sQ4_spl),
% 7.10/6.37 inference(split_clause,[status(thm)],[f433,f435,f450])).
% 7.10/6.37 fof(f501,plain,(
% 7.10/6.37 leq(sK0_skl,sK0_skl)),
% 7.10/6.37 inference(resolution,[status(thm)],[f103,f255])).
% 7.10/6.37 fof(f502,plain,(
% 7.10/6.37 leq(sK1_skl,sK1_skl)),
% 7.10/6.37 inference(resolution,[status(thm)],[f104,f255])).
% 7.10/6.37 fof(f526,plain,(
% 7.10/6.37 sK47_skl=nil|~sQ0_spl),
% 7.10/6.37 inference(backward_demodulation,[status(thm)],[f436,f423])).
% 7.10/6.37 fof(f527,plain,(
% 7.10/6.37 $false|~sQ0_spl),
% 7.10/6.37 inference(forward_subsumption_resolution,[status(thm)],[f526,f424])).
% 7.10/6.37 fof(f528,plain,(
% 7.10/6.37 ~sQ0_spl),
% 7.10/6.37 inference(contradiction_clause,[status(thm)],[f527])).
% 7.10/6.37 fof(f533,definition,(
% 7.10/6.37 sQ7_spl <=> (ssList(nil))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f535,plain,(
% 7.10/6.37 ~ssList(nil)|sQ7_spl),
% 7.10/6.37 inference(component_clause,[status(thm)],[f533])).
% 7.10/6.37 fof(f536,definition,(
% 7.10/6.37 sQ8_spl <=> (ssList(sK49_skl))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f538,plain,(
% 7.10/6.37 ~ssList(sK49_skl)|sQ8_spl),
% 7.10/6.37 inference(component_clause,[status(thm)],[f536])).
% 7.10/6.37 fof(f544,definition,(
% 7.10/6.37 sQ10_spl <=> (ssList(sK48_skl))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f546,plain,(
% 7.10/6.37 ~ssList(sK48_skl)|sQ10_spl),
% 7.10/6.37 inference(component_clause,[status(thm)],[f544])).
% 7.10/6.37 fof(f548,plain,(
% 7.10/6.37 $false|sQ7_spl),
% 7.10/6.37 inference(forward_subsumption_resolution,[status(thm)],[f535,f223])).
% 7.10/6.37 fof(f549,plain,(
% 7.10/6.37 sQ7_spl),
% 7.10/6.37 inference(contradiction_clause,[status(thm)],[f548])).
% 7.10/6.37 fof(f554,definition,(
% 7.10/6.37 sQ12_spl <=> (ssList(sK47_skl))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f556,plain,(
% 7.10/6.37 ~ssList(sK47_skl)|sQ12_spl),
% 7.10/6.37 inference(component_clause,[status(thm)],[f554])).
% 7.10/6.37 fof(f569,definition,(
% 7.10/6.37 sQ15_spl <=> (ssItem(sK0_skl))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f571,plain,(
% 7.10/6.37 ~ssItem(sK0_skl)|sQ15_spl),
% 7.10/6.37 inference(component_clause,[status(thm)],[f569])).
% 7.10/6.37 fof(f577,definition,(
% 7.10/6.37 sQ17_spl <=> (ssItem(sK1_skl))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f579,plain,(
% 7.10/6.37 ~ssItem(sK1_skl)|sQ17_spl),
% 7.10/6.37 inference(component_clause,[status(thm)],[f577])).
% 7.10/6.37 fof(f650,definition,(
% 7.10/6.37 sQ23_spl <=> (ssItem(sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f661,plain,(
% 7.10/6.37 app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK47_skl|~sQ4_spl),
% 7.10/6.37 inference(backward_demodulation,[status(thm)],[f423,f451])).
% 7.10/6.37 fof(f711,definition,(
% 7.10/6.37 sQ31_spl <=> (leq(sK1_skl,sK1_skl))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f713,plain,(
% 7.10/6.37 ~leq(sK1_skl,sK1_skl)|sQ31_spl),
% 7.10/6.37 inference(component_clause,[status(thm)],[f711])).
% 7.10/6.37 fof(f718,definition,(
% 7.10/6.37 sQ33_spl <=> (leq(sK0_skl,sK0_skl))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f720,plain,(
% 7.10/6.37 ~leq(sK0_skl,sK0_skl)|sQ33_spl),
% 7.10/6.37 inference(component_clause,[status(thm)],[f718])).
% 7.10/6.37 fof(f725,plain,(
% 7.10/6.37 $false|sQ17_spl),
% 7.10/6.37 inference(forward_subsumption_resolution,[status(thm)],[f579,f104])).
% 7.10/6.37 fof(f726,plain,(
% 7.10/6.37 sQ17_spl),
% 7.10/6.37 inference(contradiction_clause,[status(thm)],[f725])).
% 7.10/6.37 fof(f727,plain,(
% 7.10/6.37 $false|sQ15_spl),
% 7.10/6.37 inference(forward_subsumption_resolution,[status(thm)],[f571,f103])).
% 7.10/6.37 fof(f728,plain,(
% 7.10/6.37 sQ15_spl),
% 7.10/6.37 inference(contradiction_clause,[status(thm)],[f727])).
% 7.10/6.37 fof(f729,plain,(
% 7.10/6.37 $false|sQ33_spl),
% 7.10/6.37 inference(forward_subsumption_resolution,[status(thm)],[f720,f501])).
% 7.10/6.37 fof(f730,plain,(
% 7.10/6.37 sQ33_spl),
% 7.10/6.37 inference(contradiction_clause,[status(thm)],[f729])).
% 7.10/6.37 fof(f731,plain,(
% 7.10/6.37 $false|sQ31_spl),
% 7.10/6.37 inference(forward_subsumption_resolution,[status(thm)],[f713,f502])).
% 7.10/6.37 fof(f732,plain,(
% 7.10/6.37 sQ31_spl),
% 7.10/6.37 inference(contradiction_clause,[status(thm)],[f731])).
% 7.10/6.37 fof(f995,plain,(
% 7.10/6.37 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|lt(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 7.10/6.37 inference(resolution,[status(thm)],[f428,f661])).
% 7.10/6.37 fof(f997,definition,(
% 7.10/6.37 sQ80_spl <=> (lt(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 7.10/6.37 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 7.10/6.37 fof(f998,plain,(
% 7.10/6.37 lt(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ80_spl),
% 7.10/6.37 inference(component_clause,[status(thm)],[f997])).
% 7.10/6.37 fof(f1000,plain,(
% 7.10/6.37 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ80_spl|~sQ4_spl),
% 7.10/6.38 inference(split_clause,[status(thm)],[f995,f438,f442,f446,f997,f450])).
% 7.10/6.38 fof(f1200,definition,(
% 7.10/6.38 ![X1]: (sQ108_spl <=> (~ssList(X1)))),
% 7.10/6.38 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 7.10/6.38 fof(f1201,plain,(
% 7.10/6.38 ![X0]: (~ssList(X0)|~sQ108_spl)),
% 7.10/6.38 inference(component_clause,[status(thm)],[f1200])).
% 7.10/6.38 fof(f1228,plain,(
% 7.10/6.38 $false|sQ10_spl),
% 7.10/6.38 inference(forward_subsumption_resolution,[status(thm)],[f546,f419])).
% 7.10/6.38 fof(f1229,plain,(
% 7.10/6.38 sQ10_spl),
% 7.10/6.38 inference(contradiction_clause,[status(thm)],[f1228])).
% 7.10/6.38 fof(f1230,plain,(
% 7.10/6.38 $false|sQ12_spl),
% 7.10/6.38 inference(forward_subsumption_resolution,[status(thm)],[f556,f418])).
% 7.10/6.38 fof(f1231,plain,(
% 7.10/6.38 sQ12_spl),
% 7.10/6.38 inference(contradiction_clause,[status(thm)],[f1230])).
% 7.10/6.38 fof(f1336,plain,(
% 7.10/6.38 ~ssList(sK47_skl)|sQ8_spl),
% 7.10/6.38 inference(forward_demodulation,[status(thm)],[f423,f538])).
% 7.10/6.38 fof(f1337,plain,(
% 7.10/6.38 $false|sQ8_spl),
% 7.10/6.38 inference(forward_subsumption_resolution,[status(thm)],[f1336,f418])).
% 7.10/6.38 fof(f1338,plain,(
% 7.10/6.38 sQ8_spl),
% 7.10/6.38 inference(contradiction_clause,[status(thm)],[f1337])).
% 7.10/6.38 fof(f1340,plain,(
% 7.10/6.38 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|~leq(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 7.10/6.38 inference(resolution,[status(thm)],[f429,f661])).
% 7.10/6.38 fof(f1342,definition,(
% 7.10/6.38 sQ131_spl <=> (leq(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 7.10/6.38 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 7.10/6.38 fof(f1345,plain,(
% 7.10/6.38 ~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ131_spl|~sQ4_spl),
% 7.10/6.38 inference(split_clause,[status(thm)],[f1340,f438,f442,f446,f1342,f450])).
% 7.10/6.38 fof(f1374,plain,(
% 7.10/6.38 $false|~sQ108_spl),
% 7.10/6.38 inference(backward_subsumption_resolution,[status(thm)],[f418,f1201])).
% 7.10/6.38 fof(f1378,plain,(
% 7.10/6.38 ~sQ108_spl),
% 7.10/6.38 inference(contradiction_clause,[status(thm)],[f1374])).
% 7.10/6.38 fof(f1760,definition,(
% 7.10/6.38 sQ172_spl <=> (nil=sK47_skl)),
% 7.10/6.38 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 7.10/6.38 fof(f1761,plain,(
% 7.10/6.38 nil=sK47_skl|~sQ172_spl),
% 7.10/6.38 inference(component_clause,[status(thm)],[f1760])).
% 7.10/6.38 fof(f1842,plain,(
% 7.10/6.38 $false|~sQ172_spl),
% 7.10/6.38 inference(forward_subsumption_resolution,[status(thm)],[f1761,f424])).
% 7.10/6.38 fof(f1843,plain,(
% 7.10/6.38 ~sQ172_spl),
% 7.10/6.38 inference(contradiction_clause,[status(thm)],[f1842])).
% 7.10/6.38 fof(f2233,definition,(
% 7.10/6.38 sQ225_spl <=> (sK0_skl=sK1_skl)),
% 7.10/6.38 introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition])).
% 7.10/6.38 fof(f2234,plain,(
% 7.10/6.38 sK0_skl=sK1_skl|~sQ225_spl),
% 7.10/6.38 inference(component_clause,[status(thm)],[f2233])).
% 7.10/6.38 fof(f2244,plain,(
% 7.10/6.38 $false|~sQ225_spl),
% 7.10/6.38 inference(forward_subsumption_resolution,[status(thm)],[f2234,f105])).
% 7.10/6.38 fof(f2245,plain,(
% 7.10/6.38 ~sQ225_spl),
% 7.10/6.38 inference(contradiction_clause,[status(thm)],[f2244])).
% 7.10/6.38 fof(f2288,plain,(
% 7.10/6.38 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|ssItem(sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 7.10/6.38 inference(resolution,[status(thm)],[f661,f425])).
% 7.10/6.38 fof(f2301,plain,(
% 7.10/6.38 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ23_spl|~sQ4_spl),
% 7.10/6.38 inference(split_clause,[status(thm)],[f2288,f438,f442,f446,f650,f450])).
% 7.10/6.38 fof(f9364,plain,(
% 7.10/6.38 ~ssItem(sK52_skl)|~ssItem(sK51_skl(sK54_skl,sK53_skl,sK52_skl))|leq(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ80_spl),
% 7.10/6.38 inference(resolution,[status(thm)],[f998,f409])).
% 7.10/6.38 fof(f9381,plain,(
% 7.10/6.38 ~sQ1_spl|~sQ23_spl|sQ131_spl|~sQ80_spl),
% 7.10/6.38 inference(split_clause,[status(thm)],[f9364,f438,f650,f1342,f997])).
% 7.10/6.38 fof(f9382,plain,(
% 7.10/6.38 $false),
% 7.10/6.38 inference(sat_refutation,[status(thm)],[f441,f445,f449,f453,f528,f549,f726,f728,f730,f732,f1000,f1229,f1231,f1338,f1345,f1378,f1843,f2245,f2301,f9381])).
% 7.10/6.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.40/6.40 % Elapsed time: 1.014873 seconds
% 0.40/6.40 % CPU time: 7.802028 seconds
% 0.40/6.40 % Total memory used: 201.098 MB
% 0.40/6.40 % Net memory used: 194.719 MB
%------------------------------------------------------------------------------