%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC153+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:44 PM UTC 2026
% Result : Theorem 0.12s 5.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC153+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.36 % Computer : n017.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Mon Sep 21 07:55:48 UTC 2026
% 0.08/5.36 % CPUTime :
% 0.08/5.38 % Drodi V4.1.1
% 0.12/5.69 % Refutation found
% 0.12/5.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/5.69 % SZS output start CNFRefutation for theBenchmark
% 0.12/5.69 fof(f30,axiom,(
% 0.12/5.69 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> ( ( leq(U,V)& leq(V,W) )=> leq(U,W) ) ) )) )) )),
% 0.12/5.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.69 fof(f31,axiom,(
% 0.12/5.69 (! [U] :( ssItem(U)=> leq(U,U) ) )),
% 0.12/5.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.69 fof(f96,conjecture,(
% 0.12/5.69 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( X != V| W != U| (? [Y] :( ssItem(Y)& (? [Z] :( ssItem(Z)& (? [X1] :( ssList(X1)& (? [X2] :( ssList(X2)& (? [X3] :( ssList(X3)& app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3) = W& leq(Z,Y)& ( ~ leq(Y,Z)| (? [X4] :( ssItem(X4)& memberP(X2,X4)& ( ~ leq(Y,X4)| ~ leq(X4,Z) ) ) )) ) )) )) )) )))| (! [X5] :( ssItem(X5)=> (! [X6] :( ssItem(X6)=> (! [X7] :( ssList(X7)=> (! [X8] :( ssList(X8)=> (! [X9] :( ssList(X9)=> ( app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9) != U| ~ leq(X6,X5)| ( (! [X10] :( ssItem(X10)=> ( ~ memberP(X8,X10)| ( leq(X10,X6)& leq(X5,X10) ) ) ))& leq(X5,X6) ) ) ) )) )) )) )) )) ) )) )) )) )),
% 0.12/5.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.69 fof(f97,negated_conjecture,(
% 0.12/5.69 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( X != V| W != U| (? [Y] :( ssItem(Y)& (? [Z] :( ssItem(Z)& (? [X1] :( ssList(X1)& (? [X2] :( ssList(X2)& (? [X3] :( ssList(X3)& app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3) = W& leq(Z,Y)& ( ~ leq(Y,Z)| (? [X4] :( ssItem(X4)& memberP(X2,X4)& ( ~ leq(Y,X4)| ~ leq(X4,Z) ) ) )) ) )) )) )) )))| (! [X5] :( ssItem(X5)=> (! [X6] :( ssItem(X6)=> (! [X7] :( ssList(X7)=> (! [X8] :( ssList(X8)=> (! [X9] :( ssList(X9)=> ( app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9) != U| ~ leq(X6,X5)| ( (! [X10] :( ssItem(X10)=> ( ~ memberP(X8,X10)| ( leq(X10,X6)& leq(X5,X10) ) ) ))& leq(X5,X6) ) ) ) )) )) )) )) )) ) )) )) )) ))),
% 0.12/5.69 inference(negated_conjecture,[status(cth)],[f96])).
% 0.12/5.69 fof(f252,plain,(
% 0.12/5.69 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|((~leq(U,V)|~leq(V,W))|leq(U,W)))))))),
% 0.12/5.69 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.12/5.69 fof(f253,plain,(
% 0.12/5.69 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssItem(X2)|~leq(X0,X1)|~leq(X1,X2)|leq(X0,X2))),
% 0.12/5.69 inference(cnf_transformation,[status(thm)],[f252])).
% 0.12/5.69 fof(f254,plain,(
% 0.12/5.69 ![U]: (~ssItem(U)|leq(U,U))),
% 0.12/5.69 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.12/5.69 fof(f255,plain,(
% 0.12/5.69 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 0.12/5.69 inference(cnf_transformation,[status(thm)],[f254])).
% 0.12/5.69 fof(f415,plain,(
% 0.12/5.69 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((X=V&W=U)&(![Y]: (~ssItem(Y)|(![Z]: (~ssItem(Z)|(![X1]: (~ssList(X1)|(![X2]: (~ssList(X2)|(![X3]: (((~ssList(X3)|~app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3)=W)|~leq(Z,Y))|(leq(Y,Z)&(![X4]: ((~ssItem(X4)|~memberP(X2,X4))|(leq(Y,X4)&leq(X4,Z))))))))))))))))&(?[X5]: (ssItem(X5)&(?[X6]: (ssItem(X6)&(?[X7]: (ssList(X7)&(?[X8]: (ssList(X8)&(?[X9]: (ssList(X9)&((app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9)=U&leq(X6,X5))&((?[X10]: (ssItem(X10)&(memberP(X8,X10)&(~leq(X10,X6)|~leq(X5,X10)))))|~leq(X5,X6))))))))))))))))))))))),
% 0.12/5.69 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.12/5.69 fof(f416,plain,(
% 0.12/5.69 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((X=V&W=U)&(![Y]: (~ssItem(Y)|(![Z]: (~ssItem(Z)|(![X1]: (~ssList(X1)|(![X2]: (~ssList(X2)|(((![X3]: (~ssList(X3)|~app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3)=W))|~leq(Z,Y))|(leq(Y,Z)&(![X4]: ((~ssItem(X4)|~memberP(X2,X4))|(leq(Y,X4)&leq(X4,Z)))))))))))))))&(?[X5]: (ssItem(X5)&(?[X6]: (ssItem(X6)&(?[X7]: (ssList(X7)&(?[X8]: (ssList(X8)&(?[X9]: (ssList(X9)&((app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9)=U&leq(X6,X5))&((?[X10]: (ssItem(X10)&(memberP(X8,X10)&(~leq(X10,X6)|~leq(X5,X10)))))|~leq(X5,X6)))))))))))))))))))))),
% 0.12/5.69 inference(miniscoping,[status(thm)],[f415])).
% 0.12/5.69 fof(f417,plain,(
% 0.12/5.69 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(ssList(sK50_skl)&(((sK50_skl=sK48_skl&sK49_skl=sK47_skl)&(![Y]: (~ssItem(Y)|(![Z]: (~ssItem(Z)|(![X1]: (~ssList(X1)|(![X2]: (~ssList(X2)|(((![X3]: (~ssList(X3)|~app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3)=sK49_skl))|~leq(Z,Y))|(leq(Y,Z)&(![X4]: ((~ssItem(X4)|~memberP(X2,X4))|(leq(Y,X4)&leq(X4,Z)))))))))))))))&(ssItem(sK51_skl)&(ssItem(sK52_skl)&(ssList(sK53_skl)&(ssList(sK54_skl)&(ssList(sK55_skl)&((app(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),sK55_skl)=sK47_skl&leq(sK52_skl,sK51_skl))&((ssItem(sK56_skl)&(memberP(sK54_skl,sK56_skl)&(~leq(sK56_skl,sK52_skl)|~leq(sK51_skl,sK56_skl))))|~leq(sK51_skl,sK52_skl)))))))))))))),
% 0.12/5.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl,sK53_skl,sK54_skl,sK55_skl,sK56_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(X5,sK51_skl),skolemize(X6,sK52_skl),skolemize(X7,sK53_skl),skolemize(X8,sK54_skl),skolemize(X9,sK55_skl),skolemize(X10,sK56_skl)],[f416])).
% 0.12/5.70 fof(f423,plain,(
% 0.12/5.70 sK49_skl=sK47_skl),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f424,plain,(
% 0.12/5.70 ![X0,X1,X2,X3,X4]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4)=sK49_skl|~leq(X1,X0)|leq(X0,X1))),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f425,plain,(
% 0.12/5.70 ![X0,X1,X2,X3,X4,X5]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4)=sK49_skl|~leq(X1,X0)|~ssItem(X5)|~memberP(X3,X5)|leq(X0,X5))),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f426,plain,(
% 0.12/5.70 ![X0,X1,X2,X3,X4,X5]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4)=sK49_skl|~leq(X1,X0)|~ssItem(X5)|~memberP(X3,X5)|leq(X5,X1))),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f427,plain,(
% 0.12/5.70 ssItem(sK51_skl)),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f428,plain,(
% 0.12/5.70 ssItem(sK52_skl)),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f429,plain,(
% 0.12/5.70 ssList(sK53_skl)),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f430,plain,(
% 0.12/5.70 ssList(sK54_skl)),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f431,plain,(
% 0.12/5.70 ssList(sK55_skl)),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f432,plain,(
% 0.12/5.70 app(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),sK55_skl)=sK47_skl),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f433,plain,(
% 0.12/5.70 leq(sK52_skl,sK51_skl)),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f434,plain,(
% 0.12/5.70 ssItem(sK56_skl)|~leq(sK51_skl,sK52_skl)),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f435,plain,(
% 0.12/5.70 memberP(sK54_skl,sK56_skl)|~leq(sK51_skl,sK52_skl)),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f436,plain,(
% 0.12/5.70 ~leq(sK56_skl,sK52_skl)|~leq(sK51_skl,sK56_skl)|~leq(sK51_skl,sK52_skl)),
% 0.12/5.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.12/5.70 fof(f437,definition,(
% 0.12/5.70 sQ0_spl <=> (ssItem(sK56_skl))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f440,definition,(
% 0.12/5.70 sQ1_spl <=> (leq(sK51_skl,sK52_skl))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f443,plain,(
% 0.12/5.70 sQ0_spl|~sQ1_spl),
% 0.12/5.70 inference(split_clause,[status(thm)],[f434,f437,f440])).
% 0.12/5.70 fof(f444,definition,(
% 0.12/5.70 sQ2_spl <=> (memberP(sK54_skl,sK56_skl))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f445,plain,(
% 0.12/5.70 memberP(sK54_skl,sK56_skl)|~sQ2_spl),
% 0.12/5.70 inference(component_clause,[status(thm)],[f444])).
% 0.12/5.70 fof(f447,plain,(
% 0.12/5.70 sQ2_spl|~sQ1_spl),
% 0.12/5.70 inference(split_clause,[status(thm)],[f435,f444,f440])).
% 0.12/5.70 fof(f448,definition,(
% 0.12/5.70 sQ3_spl <=> (leq(sK56_skl,sK52_skl))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f451,definition,(
% 0.12/5.70 sQ4_spl <=> (leq(sK51_skl,sK56_skl))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f454,plain,(
% 0.12/5.70 ~sQ3_spl|~sQ4_spl|~sQ1_spl),
% 0.12/5.70 inference(split_clause,[status(thm)],[f436,f448,f451,f440])).
% 0.12/5.70 fof(f526,plain,(
% 0.12/5.70 leq(sK52_skl,sK52_skl)),
% 0.12/5.70 inference(resolution,[status(thm)],[f428,f255])).
% 0.12/5.70 fof(f552,plain,(
% 0.12/5.70 ![X0]: (~ssItem(X0)|~ssItem(sK52_skl)|~ssItem(sK51_skl)|~leq(X0,sK52_skl)|leq(X0,sK51_skl))),
% 0.12/5.70 inference(resolution,[status(thm)],[f433,f253])).
% 0.12/5.70 fof(f553,definition,(
% 0.12/5.70 ![X0]: (sQ5_spl <=> (~ssItem(X0)|~leq(X0,sK52_skl)|leq(X0,sK51_skl)))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f554,plain,(
% 0.12/5.70 ![X0]: (~ssItem(X0)|~leq(X0,sK52_skl)|leq(X0,sK51_skl)|~sQ5_spl)),
% 0.12/5.70 inference(component_clause,[status(thm)],[f553])).
% 0.12/5.70 fof(f556,definition,(
% 0.12/5.70 sQ6_spl <=> (ssItem(sK52_skl))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f558,plain,(
% 0.12/5.70 ~ssItem(sK52_skl)|sQ6_spl),
% 0.12/5.70 inference(component_clause,[status(thm)],[f556])).
% 0.12/5.70 fof(f559,definition,(
% 0.12/5.70 sQ7_spl <=> (ssItem(sK51_skl))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f561,plain,(
% 0.12/5.70 ~ssItem(sK51_skl)|sQ7_spl),
% 0.12/5.70 inference(component_clause,[status(thm)],[f559])).
% 0.12/5.70 fof(f562,plain,(
% 0.12/5.70 sQ5_spl|~sQ6_spl|~sQ7_spl),
% 0.12/5.70 inference(split_clause,[status(thm)],[f552,f553,f556,f559])).
% 0.12/5.70 fof(f563,plain,(
% 0.12/5.70 $false|sQ7_spl),
% 0.12/5.70 inference(forward_subsumption_resolution,[status(thm)],[f561,f427])).
% 0.12/5.70 fof(f564,plain,(
% 0.12/5.70 sQ7_spl),
% 0.12/5.70 inference(contradiction_clause,[status(thm)],[f563])).
% 0.12/5.70 fof(f590,plain,(
% 0.12/5.70 ![X0,X1,X2,X3,X4]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4)=sK47_skl|~leq(X1,X0)|leq(X0,X1))),
% 0.12/5.70 inference(forward_demodulation,[status(thm)],[f423,f424])).
% 0.12/5.70 fof(f687,plain,(
% 0.12/5.70 $false|sQ6_spl),
% 0.12/5.70 inference(forward_subsumption_resolution,[status(thm)],[f558,f428])).
% 0.12/5.70 fof(f688,plain,(
% 0.12/5.70 sQ6_spl),
% 0.12/5.70 inference(contradiction_clause,[status(thm)],[f687])).
% 0.12/5.70 fof(f693,definition,(
% 0.12/5.70 sQ25_spl <=> (ssList(sK53_skl))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f695,plain,(
% 0.12/5.70 ~ssList(sK53_skl)|sQ25_spl),
% 0.12/5.70 inference(component_clause,[status(thm)],[f693])).
% 0.12/5.70 fof(f707,definition,(
% 0.12/5.70 sQ27_spl <=> (ssList(sK54_skl))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f709,plain,(
% 0.12/5.70 ~ssList(sK54_skl)|sQ27_spl),
% 0.12/5.70 inference(component_clause,[status(thm)],[f707])).
% 0.12/5.70 fof(f711,plain,(
% 0.12/5.70 ![X0,X1,X2,X3,X4,X5]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4)=sK47_skl|~leq(X1,X0)|~ssItem(X5)|~memberP(X3,X5)|leq(X0,X5))),
% 0.12/5.70 inference(forward_demodulation,[status(thm)],[f423,f425])).
% 0.12/5.70 fof(f722,definition,(
% 0.12/5.70 sQ29_spl <=> (ssList(sK55_skl))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f724,plain,(
% 0.12/5.70 ~ssList(sK55_skl)|sQ29_spl),
% 0.12/5.70 inference(component_clause,[status(thm)],[f722])).
% 0.12/5.70 fof(f1026,plain,(
% 0.12/5.70 ![X0,X1,X2,X3,X4,X5]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4)=sK47_skl|~leq(X1,X0)|~ssItem(X5)|~memberP(X3,X5)|leq(X5,X1))),
% 0.12/5.70 inference(forward_demodulation,[status(thm)],[f423,f426])).
% 0.12/5.70 fof(f1192,plain,(
% 0.12/5.70 ~ssItem(sK52_skl)|leq(sK52_skl,sK51_skl)|~sQ5_spl),
% 0.12/5.70 inference(resolution,[status(thm)],[f554,f526])).
% 0.12/5.70 fof(f1193,definition,(
% 0.12/5.70 sQ123_spl <=> (leq(sK52_skl,sK51_skl))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f1196,plain,(
% 0.12/5.70 ~sQ6_spl|sQ123_spl|~sQ5_spl),
% 0.12/5.70 inference(split_clause,[status(thm)],[f1192,f556,f1193,f553])).
% 0.12/5.70 fof(f1367,plain,(
% 0.12/5.70 ![X0]: (~ssItem(sK51_skl)|~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|~ssList(sK55_skl)|~leq(sK52_skl,sK51_skl)|~ssItem(X0)|~memberP(sK54_skl,X0)|leq(X0,sK52_skl))),
% 0.12/5.70 inference(resolution,[status(thm)],[f432,f1026])).
% 0.12/5.70 fof(f1371,definition,(
% 0.12/5.70 ![X0]: (sQ161_spl <=> (~ssItem(X0)|~memberP(sK54_skl,X0)|leq(X0,sK52_skl)))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f1372,plain,(
% 0.12/5.70 ![X0]: (~ssItem(X0)|~memberP(sK54_skl,X0)|leq(X0,sK52_skl)|~sQ161_spl)),
% 0.12/5.70 inference(component_clause,[status(thm)],[f1371])).
% 0.12/5.70 fof(f1374,plain,(
% 0.12/5.70 ~sQ7_spl|~sQ6_spl|~sQ25_spl|~sQ27_spl|~sQ29_spl|~sQ123_spl|sQ161_spl),
% 0.12/5.70 inference(split_clause,[status(thm)],[f1367,f559,f556,f693,f707,f722,f1193,f1371])).
% 0.12/5.70 fof(f2000,plain,(
% 0.12/5.70 $false|sQ27_spl),
% 0.12/5.70 inference(forward_subsumption_resolution,[status(thm)],[f709,f430])).
% 0.12/5.70 fof(f2001,plain,(
% 0.12/5.70 sQ27_spl),
% 0.12/5.70 inference(contradiction_clause,[status(thm)],[f2000])).
% 0.12/5.70 fof(f2004,plain,(
% 0.12/5.70 $false|sQ29_spl),
% 0.12/5.70 inference(forward_subsumption_resolution,[status(thm)],[f724,f431])).
% 0.12/5.70 fof(f2005,plain,(
% 0.12/5.70 sQ29_spl),
% 0.12/5.70 inference(contradiction_clause,[status(thm)],[f2004])).
% 0.12/5.70 fof(f2281,plain,(
% 0.12/5.70 $false|sQ25_spl),
% 0.12/5.70 inference(forward_subsumption_resolution,[status(thm)],[f695,f429])).
% 0.12/5.70 fof(f2282,plain,(
% 0.12/5.70 sQ25_spl),
% 0.12/5.70 inference(contradiction_clause,[status(thm)],[f2281])).
% 0.12/5.70 fof(f2611,plain,(
% 0.12/5.70 ![X0]: (~ssItem(sK51_skl)|~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|~ssList(sK55_skl)|~leq(sK52_skl,sK51_skl)|~ssItem(X0)|~memberP(sK54_skl,X0)|leq(sK51_skl,X0))),
% 0.12/5.70 inference(resolution,[status(thm)],[f711,f432])).
% 0.12/5.70 fof(f2614,definition,(
% 0.12/5.70 ![X0]: (sQ349_spl <=> (~ssItem(X0)|~memberP(sK54_skl,X0)|leq(sK51_skl,X0)))),
% 0.12/5.70 introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition])).
% 0.12/5.70 fof(f2615,plain,(
% 0.12/5.70 ![X0]: (~ssItem(X0)|~memberP(sK54_skl,X0)|leq(sK51_skl,X0)|~sQ349_spl)),
% 0.12/5.70 inference(component_clause,[status(thm)],[f2614])).
% 0.12/5.70 fof(f2617,plain,(
% 0.12/5.70 ~sQ7_spl|~sQ6_spl|~sQ25_spl|~sQ27_spl|~sQ29_spl|~sQ123_spl|sQ349_spl),
% 0.12/5.70 inference(split_clause,[status(thm)],[f2611,f559,f556,f693,f707,f722,f1193,f2614])).
% 0.12/5.70 fof(f3664,plain,(
% 0.12/5.70 ~ssItem(sK51_skl)|~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|~ssList(sK55_skl)|~leq(sK52_skl,sK51_skl)|leq(sK51_skl,sK52_skl)),
% 0.12/5.70 inference(resolution,[status(thm)],[f590,f432])).
% 0.12/5.70 fof(f3667,plain,(
% 0.12/5.70 ~sQ7_spl|~sQ6_spl|~sQ25_spl|~sQ27_spl|~sQ29_spl|~sQ123_spl|sQ1_spl),
% 0.12/5.70 inference(split_clause,[status(thm)],[f3664,f559,f556,f693,f707,f722,f1193,f440])).
% 0.12/5.70 fof(f3686,plain,(
% 0.12/5.70 ~ssItem(sK56_skl)|leq(sK51_skl,sK56_skl)|~sQ2_spl|~sQ349_spl),
% 0.12/5.70 inference(resolution,[status(thm)],[f445,f2615])).
% 0.12/5.70 fof(f3687,plain,(
% 0.12/5.70 ~ssItem(sK56_skl)|leq(sK56_skl,sK52_skl)|~sQ2_spl|~sQ161_spl),
% 0.12/5.70 inference(resolution,[status(thm)],[f445,f1372])).
% 0.12/5.70 fof(f3693,plain,(
% 0.12/5.70 ~sQ0_spl|sQ4_spl|~sQ2_spl|~sQ349_spl),
% 0.12/5.70 inference(split_clause,[status(thm)],[f3686,f437,f451,f444,f2614])).
% 0.12/5.70 fof(f3694,plain,(
% 0.12/5.70 ~sQ0_spl|sQ3_spl|~sQ2_spl|~sQ161_spl),
% 0.12/5.70 inference(split_clause,[status(thm)],[f3687,f437,f448,f444,f1371])).
% 0.12/5.70 fof(f3715,plain,(
% 0.12/5.70 $false),
% 0.12/5.70 inference(sat_refutation,[status(thm)],[f443,f447,f454,f562,f564,f688,f1196,f1374,f2001,f2005,f2282,f2617,f3667,f3693,f3694])).
% 0.12/5.70 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/5.71 % Elapsed time: 0.340286 seconds
% 0.12/5.71 % CPU time: 2.433584 seconds
% 0.12/5.71 % Total memory used: 144.910 MB
% 0.12/5.71 % Net memory used: 142.579 MB
%------------------------------------------------------------------------------