%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC242+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 : n008.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 0.58s 1.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC242+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n008.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 08:08:38 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.45 % Drodi V4.1.1
% 0.58/1.03 % Refutation found
% 0.58/1.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.58/1.03 % SZS output start CNFRefutation for theBenchmark
% 0.58/1.03 fof(f2,axiom,(
% 0.58/1.03 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 0.58/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.58/1.03 fof(f17,axiom,(
% 0.58/1.03 ssList(nil) ),
% 0.58/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.58/1.03 fof(f31,axiom,(
% 0.58/1.03 (! [U] :( ssItem(U)=> leq(U,U) ) )),
% 0.58/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.58/1.03 fof(f96,conjecture,(
% 0.58/1.03 (! [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(X3,X6)& memberP(X4,X6)& memberP(X5,X6)& lt(X3,X6) ) )) )) )) )) ) )) )) )) )),
% 0.58/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.58/1.03 fof(f97,negated_conjecture,(
% 0.58/1.03 ~((! [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(X3,X6)& memberP(X4,X6)& memberP(X5,X6)& lt(X3,X6) ) )) )) )) )) ) )) )) )) ))),
% 0.58/1.03 inference(negated_conjecture,[status(cth)],[f96])).
% 0.58/1.03 fof(f102,plain,(
% 0.58/1.03 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 0.58/1.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 0.58/1.03 fof(f103,plain,(
% 0.58/1.03 ssItem(sK0_skl)),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f102])).
% 0.58/1.03 fof(f104,plain,(
% 0.58/1.03 ssItem(sK1_skl)),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f102])).
% 0.58/1.03 fof(f223,plain,(
% 0.58/1.03 ssList(nil)),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f17])).
% 0.58/1.03 fof(f254,plain,(
% 0.58/1.03 ![U]: (~ssItem(U)|leq(U,U))),
% 0.58/1.03 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.58/1.03 fof(f255,plain,(
% 0.58/1.03 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f254])).
% 0.58/1.03 fof(f415,plain,(
% 0.58/1.03 (?[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(X3,X6))|~memberP(X4,X6))|~memberP(X5,X6))|~lt(X3,X6))))))))))))))))))),
% 0.58/1.03 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.58/1.03 fof(f416,plain,(
% 0.58/1.03 ?[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(X3,X6))|~memberP(X4,X6))|~memberP(X5,X6))|~lt(X3,X6))))))))))))))))),
% 0.58/1.03 inference(miniscoping,[status(thm)],[f415])).
% 0.58/1.03 fof(f417,plain,(
% 0.58/1.03 (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(sK52_skl,X6))|~memberP(sK53_skl,X6))|~memberP(sK54_skl,X6))|~lt(sK52_skl,X6)))))))))))),
% 0.58/1.03 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])).
% 0.58/1.03 fof(f418,plain,(
% 0.58/1.03 ssList(sK47_skl)),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f419,plain,(
% 0.58/1.03 ssList(sK48_skl)),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f423,plain,(
% 0.58/1.03 sK47_skl=sK49_skl),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f424,plain,(
% 0.58/1.03 ~nil=sK47_skl),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f425,plain,(
% 0.58/1.03 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK47_skl|ssItem(sK51_skl(X2,X1,X0)))),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f426,plain,(
% 0.58/1.03 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK47_skl|memberP(X1,sK51_skl(X2,X1,X0)))),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f427,plain,(
% 0.58/1.03 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK47_skl|memberP(X2,sK51_skl(X2,X1,X0)))),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f428,plain,(
% 0.58/1.03 ![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)))),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f429,plain,(
% 0.58/1.03 ![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)))),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f430,plain,(
% 0.58/1.03 nil=sK49_skl|ssItem(sK52_skl)),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f431,plain,(
% 0.58/1.03 nil=sK49_skl|ssList(sK53_skl)),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f432,plain,(
% 0.58/1.03 nil=sK49_skl|ssList(sK54_skl)),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f433,plain,(
% 0.58/1.03 nil=sK49_skl|app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK49_skl),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f434,plain,(
% 0.58/1.03 ![X0]: (nil=sK49_skl|~ssItem(X0)|leq(sK52_skl,X0)|~memberP(sK53_skl,X0)|~memberP(sK54_skl,X0)|~lt(sK52_skl,X0))),
% 0.58/1.03 inference(cnf_transformation,[status(thm)],[f417])).
% 0.58/1.03 fof(f435,definition,(
% 0.58/1.03 sQ0_spl <=> (nil=sK49_skl)),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f436,plain,(
% 0.58/1.03 nil=sK49_skl|~sQ0_spl),
% 0.58/1.03 inference(component_clause,[status(thm)],[f435])).
% 0.58/1.03 fof(f438,definition,(
% 0.58/1.03 sQ1_spl <=> (ssItem(sK52_skl))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f441,plain,(
% 0.58/1.03 sQ0_spl|sQ1_spl),
% 0.58/1.03 inference(split_clause,[status(thm)],[f430,f435,f438])).
% 0.58/1.03 fof(f442,definition,(
% 0.58/1.03 sQ2_spl <=> (ssList(sK53_skl))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f445,plain,(
% 0.58/1.03 sQ0_spl|sQ2_spl),
% 0.58/1.03 inference(split_clause,[status(thm)],[f431,f435,f442])).
% 0.58/1.03 fof(f446,definition,(
% 0.58/1.03 sQ3_spl <=> (ssList(sK54_skl))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f449,plain,(
% 0.58/1.03 sQ0_spl|sQ3_spl),
% 0.58/1.03 inference(split_clause,[status(thm)],[f432,f435,f446])).
% 0.58/1.03 fof(f450,definition,(
% 0.58/1.03 sQ4_spl <=> (app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK49_skl)),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f451,plain,(
% 0.58/1.03 app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK49_skl|~sQ4_spl),
% 0.58/1.03 inference(component_clause,[status(thm)],[f450])).
% 0.58/1.03 fof(f453,plain,(
% 0.58/1.03 sQ0_spl|sQ4_spl),
% 0.58/1.03 inference(split_clause,[status(thm)],[f433,f435,f450])).
% 0.58/1.03 fof(f454,definition,(
% 0.58/1.03 ![X0]: (sQ5_spl <=> (~ssItem(X0)|leq(sK52_skl,X0)|~memberP(sK53_skl,X0)|~memberP(sK54_skl,X0)|~lt(sK52_skl,X0)))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f455,plain,(
% 0.58/1.03 ![X0]: (~ssItem(X0)|leq(sK52_skl,X0)|~memberP(sK53_skl,X0)|~memberP(sK54_skl,X0)|~lt(sK52_skl,X0)|~sQ5_spl)),
% 0.58/1.03 inference(component_clause,[status(thm)],[f454])).
% 0.58/1.03 fof(f457,plain,(
% 0.58/1.03 sQ0_spl|sQ5_spl),
% 0.58/1.03 inference(split_clause,[status(thm)],[f434,f435,f454])).
% 0.58/1.03 fof(f501,plain,(
% 0.58/1.03 leq(sK0_skl,sK0_skl)),
% 0.58/1.03 inference(resolution,[status(thm)],[f103,f255])).
% 0.58/1.03 fof(f502,plain,(
% 0.58/1.03 leq(sK1_skl,sK1_skl)),
% 0.58/1.03 inference(resolution,[status(thm)],[f104,f255])).
% 0.58/1.03 fof(f526,plain,(
% 0.58/1.03 sK47_skl=nil|~sQ0_spl),
% 0.58/1.03 inference(backward_demodulation,[status(thm)],[f436,f423])).
% 0.58/1.03 fof(f527,plain,(
% 0.58/1.03 $false|~sQ0_spl),
% 0.58/1.03 inference(forward_subsumption_resolution,[status(thm)],[f526,f424])).
% 0.58/1.03 fof(f528,plain,(
% 0.58/1.03 ~sQ0_spl),
% 0.58/1.03 inference(contradiction_clause,[status(thm)],[f527])).
% 0.58/1.03 fof(f533,definition,(
% 0.58/1.03 sQ7_spl <=> (ssList(nil))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f535,plain,(
% 0.58/1.03 ~ssList(nil)|sQ7_spl),
% 0.58/1.03 inference(component_clause,[status(thm)],[f533])).
% 0.58/1.03 fof(f544,definition,(
% 0.58/1.03 sQ10_spl <=> (ssList(sK48_skl))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f546,plain,(
% 0.58/1.03 ~ssList(sK48_skl)|sQ10_spl),
% 0.58/1.03 inference(component_clause,[status(thm)],[f544])).
% 0.58/1.03 fof(f548,plain,(
% 0.58/1.03 $false|sQ7_spl),
% 0.58/1.03 inference(forward_subsumption_resolution,[status(thm)],[f535,f223])).
% 0.58/1.03 fof(f549,plain,(
% 0.58/1.03 sQ7_spl),
% 0.58/1.03 inference(contradiction_clause,[status(thm)],[f548])).
% 0.58/1.03 fof(f554,definition,(
% 0.58/1.03 sQ12_spl <=> (ssList(sK47_skl))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f556,plain,(
% 0.58/1.03 ~ssList(sK47_skl)|sQ12_spl),
% 0.58/1.03 inference(component_clause,[status(thm)],[f554])).
% 0.58/1.03 fof(f569,definition,(
% 0.58/1.03 sQ15_spl <=> (ssItem(sK0_skl))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f571,plain,(
% 0.58/1.03 ~ssItem(sK0_skl)|sQ15_spl),
% 0.58/1.03 inference(component_clause,[status(thm)],[f569])).
% 0.58/1.03 fof(f577,definition,(
% 0.58/1.03 sQ17_spl <=> (ssItem(sK1_skl))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f579,plain,(
% 0.58/1.03 ~ssItem(sK1_skl)|sQ17_spl),
% 0.58/1.03 inference(component_clause,[status(thm)],[f577])).
% 0.58/1.03 fof(f650,definition,(
% 0.58/1.03 sQ23_spl <=> (ssItem(sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f661,plain,(
% 0.58/1.03 app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK47_skl|~sQ4_spl),
% 0.58/1.03 inference(backward_demodulation,[status(thm)],[f423,f451])).
% 0.58/1.03 fof(f703,definition,(
% 0.58/1.03 sQ29_spl <=> (leq(sK1_skl,sK1_skl))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f705,plain,(
% 0.58/1.03 ~leq(sK1_skl,sK1_skl)|sQ29_spl),
% 0.58/1.03 inference(component_clause,[status(thm)],[f703])).
% 0.58/1.03 fof(f710,definition,(
% 0.58/1.03 sQ31_spl <=> (leq(sK0_skl,sK0_skl))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f712,plain,(
% 0.58/1.03 ~leq(sK0_skl,sK0_skl)|sQ31_spl),
% 0.58/1.03 inference(component_clause,[status(thm)],[f710])).
% 0.58/1.03 fof(f717,plain,(
% 0.58/1.03 $false|sQ17_spl),
% 0.58/1.03 inference(forward_subsumption_resolution,[status(thm)],[f579,f104])).
% 0.58/1.03 fof(f718,plain,(
% 0.58/1.03 sQ17_spl),
% 0.58/1.03 inference(contradiction_clause,[status(thm)],[f717])).
% 0.58/1.03 fof(f719,plain,(
% 0.58/1.03 $false|sQ15_spl),
% 0.58/1.03 inference(forward_subsumption_resolution,[status(thm)],[f571,f103])).
% 0.58/1.03 fof(f720,plain,(
% 0.58/1.03 sQ15_spl),
% 0.58/1.03 inference(contradiction_clause,[status(thm)],[f719])).
% 0.58/1.03 fof(f723,plain,(
% 0.58/1.03 $false|sQ29_spl),
% 0.58/1.03 inference(forward_subsumption_resolution,[status(thm)],[f705,f502])).
% 0.58/1.03 fof(f724,plain,(
% 0.58/1.03 sQ29_spl),
% 0.58/1.03 inference(contradiction_clause,[status(thm)],[f723])).
% 0.58/1.03 fof(f725,plain,(
% 0.58/1.03 $false|sQ31_spl),
% 0.58/1.03 inference(forward_subsumption_resolution,[status(thm)],[f712,f501])).
% 0.58/1.03 fof(f726,plain,(
% 0.58/1.03 sQ31_spl),
% 0.58/1.03 inference(contradiction_clause,[status(thm)],[f725])).
% 0.58/1.03 fof(f777,plain,(
% 0.58/1.03 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|memberP(sK54_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 0.58/1.03 inference(resolution,[status(thm)],[f661,f427])).
% 0.58/1.03 fof(f779,definition,(
% 0.58/1.03 sQ43_spl <=> (memberP(sK54_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 0.58/1.03 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.58/1.03 fof(f780,plain,(
% 0.58/1.03 memberP(sK54_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ43_spl),
% 0.58/1.05 inference(component_clause,[status(thm)],[f779])).
% 0.58/1.05 fof(f782,plain,(
% 0.58/1.05 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ43_spl|~sQ4_spl),
% 0.58/1.05 inference(split_clause,[status(thm)],[f777,f438,f442,f446,f779,f450])).
% 0.58/1.05 fof(f987,plain,(
% 0.58/1.05 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|lt(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 0.58/1.05 inference(resolution,[status(thm)],[f428,f661])).
% 0.58/1.05 fof(f989,definition,(
% 0.58/1.05 sQ78_spl <=> (lt(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 0.58/1.05 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.58/1.05 fof(f992,plain,(
% 0.58/1.05 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ78_spl|~sQ4_spl),
% 0.58/1.05 inference(split_clause,[status(thm)],[f987,f438,f442,f446,f989,f450])).
% 0.58/1.05 fof(f1220,plain,(
% 0.58/1.05 $false|sQ10_spl),
% 0.58/1.05 inference(forward_subsumption_resolution,[status(thm)],[f546,f419])).
% 0.58/1.05 fof(f1221,plain,(
% 0.58/1.05 sQ10_spl),
% 0.58/1.05 inference(contradiction_clause,[status(thm)],[f1220])).
% 0.58/1.05 fof(f1222,plain,(
% 0.58/1.05 $false|sQ12_spl),
% 0.58/1.05 inference(forward_subsumption_resolution,[status(thm)],[f556,f418])).
% 0.58/1.05 fof(f1223,plain,(
% 0.58/1.05 sQ12_spl),
% 0.58/1.05 inference(contradiction_clause,[status(thm)],[f1222])).
% 0.58/1.05 fof(f1281,plain,(
% 0.58/1.05 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|~leq(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 0.58/1.05 inference(resolution,[status(thm)],[f429,f661])).
% 0.58/1.05 fof(f1283,definition,(
% 0.58/1.05 sQ123_spl <=> (leq(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 0.58/1.05 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.58/1.05 fof(f1286,plain,(
% 0.58/1.05 ~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ123_spl|~sQ4_spl),
% 0.58/1.05 inference(split_clause,[status(thm)],[f1281,f438,f442,f446,f1283,f450])).
% 0.58/1.05 fof(f1295,plain,(
% 0.58/1.05 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|memberP(sK53_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 0.58/1.05 inference(resolution,[status(thm)],[f426,f661])).
% 0.58/1.05 fof(f1297,definition,(
% 0.58/1.05 sQ124_spl <=> (memberP(sK53_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 0.58/1.05 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.58/1.05 fof(f1300,plain,(
% 0.58/1.05 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ124_spl|~sQ4_spl),
% 0.58/1.05 inference(split_clause,[status(thm)],[f1295,f438,f442,f446,f1297,f450])).
% 0.58/1.05 fof(f2212,plain,(
% 0.58/1.05 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|ssItem(sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 0.58/1.05 inference(resolution,[status(thm)],[f425,f661])).
% 0.58/1.05 fof(f2214,plain,(
% 0.58/1.05 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ23_spl|~sQ4_spl),
% 0.58/1.05 inference(split_clause,[status(thm)],[f2212,f438,f442,f446,f650,f450])).
% 0.58/1.05 fof(f5244,plain,(
% 0.58/1.05 ~ssItem(sK51_skl(sK54_skl,sK53_skl,sK52_skl))|leq(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~memberP(sK53_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~lt(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ43_spl|~sQ5_spl),
% 0.58/1.05 inference(resolution,[status(thm)],[f780,f455])).
% 0.58/1.05 fof(f5258,plain,(
% 0.58/1.05 ~sQ23_spl|sQ123_spl|~sQ124_spl|~sQ78_spl|~sQ43_spl|~sQ5_spl),
% 0.58/1.05 inference(split_clause,[status(thm)],[f5244,f650,f1283,f1297,f989,f779,f454])).
% 0.58/1.05 fof(f5308,plain,(
% 0.58/1.05 $false),
% 0.58/1.05 inference(sat_refutation,[status(thm)],[f441,f445,f449,f453,f457,f528,f549,f718,f720,f724,f726,f782,f992,f1221,f1223,f1286,f1300,f2214,f5258])).
% 0.58/1.05 % SZS output end CNFRefutation for theBenchmark.p
% 0.58/1.07 % Elapsed time: 0.625569 seconds
% 0.58/1.07 % CPU time: 4.509617 seconds
% 0.58/1.07 % Total memory used: 147.768 MB
% 0.58/1.07 % Net memory used: 144.995 MB
%------------------------------------------------------------------------------