%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC220+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 : 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:54 PM UTC 2026
% Result : Theorem 0.13s 11.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC220+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.08/10.37 % Computer : n017.cluster.edu
% 0.08/10.37 % Model : x86_64 x86_64
% 0.08/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/10.37 % Memory : 8046.5625MB
% 0.08/10.37 % OS : Linux 6.8.0-71-generic
% 0.08/10.38 % CPULimit : 300
% 0.08/10.38 % WCLimit : 300
% 0.08/10.38 % DateTime : Mon Sep 21 08:00:53 UTC 2026
% 0.08/10.38 % CPUTime :
% 0.13/10.40 % Drodi V4.1.1
% 0.13/11.00 % Refutation found
% 0.13/11.00 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/11.00 % SZS output start CNFRefutation for theBenchmark
% 0.13/11.00 fof(f2,axiom,(
% 0.13/11.00 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 0.13/11.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/11.00 fof(f16,axiom,(
% 0.13/11.00 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ssList(cons(V,U)) ) )) )),
% 0.13/11.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/11.00 fof(f17,axiom,(
% 0.13/11.00 ssList(nil) ),
% 0.13/11.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/11.00 fof(f31,axiom,(
% 0.13/11.00 (! [U] :( ssItem(U)=> leq(U,U) ) )),
% 0.13/11.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/11.00 fof(f96,conjecture,(
% 0.13/11.00 (! [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)| ~ leq(Y,X2)| leq(X2,Y) ) ) )) )) )))| ( 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) ) )) ) )) )) )) ) ) )) )) )) )),
% 0.13/11.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/11.00 fof(f97,negated_conjecture,(
% 0.13/11.00 ~((! [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)| ~ leq(Y,X2)| leq(X2,Y) ) ) )) )) )))| ( 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) ) )) ) )) )) )) ) ) )) )) )) ))),
% 0.13/11.00 inference(negated_conjecture,[status(cth)],[f96])).
% 0.13/11.00 fof(f102,plain,(
% 0.13/11.00 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 0.13/11.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 0.13/11.00 fof(f103,plain,(
% 0.13/11.00 ssItem(sK0_skl)),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f102])).
% 0.13/11.00 fof(f104,plain,(
% 0.13/11.00 ssItem(sK1_skl)),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f102])).
% 0.13/11.00 fof(f221,plain,(
% 0.13/11.00 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|ssList(cons(V,U)))))),
% 0.13/11.00 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.13/11.00 fof(f222,plain,(
% 0.13/11.00 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|ssList(cons(X1,X0)))),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f221])).
% 0.13/11.00 fof(f223,plain,(
% 0.13/11.00 ssList(nil)),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/11.00 fof(f254,plain,(
% 0.13/11.00 ![U]: (~ssItem(U)|leq(U,U))),
% 0.13/11.00 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.13/11.00 fof(f255,plain,(
% 0.13/11.00 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f254])).
% 0.13/11.00 fof(f415,plain,(
% 0.13/11.00 (?[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))&leq(Y,X2))&~leq(X2,Y)))))))))))&(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))))))))))))))))))))),
% 0.13/11.00 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.13/11.00 fof(f416,plain,(
% 0.13/11.00 (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)))&leq(Y,sK51_skl(X1,Z,Y)))&~leq(sK51_skl(X1,Z,Y),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)))))))))))))),
% 0.13/11.00 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)],[f415])).
% 0.13/11.00 fof(f417,plain,(
% 0.13/11.00 ssList(sK47_skl)),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f418,plain,(
% 0.13/11.00 ssList(sK48_skl)),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f422,plain,(
% 0.13/11.00 sK47_skl=sK49_skl),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f423,plain,(
% 0.13/11.00 ~nil=sK47_skl),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f424,plain,(
% 0.13/11.00 ![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.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f425,plain,(
% 0.13/11.00 ![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.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f426,plain,(
% 0.13/11.00 ![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.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f427,plain,(
% 0.13/11.00 ![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.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f428,plain,(
% 0.13/11.00 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK47_skl|~leq(sK51_skl(X2,X1,X0),X0))),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f429,plain,(
% 0.13/11.00 nil=sK49_skl|ssItem(sK52_skl)),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f430,plain,(
% 0.13/11.00 nil=sK49_skl|ssList(sK53_skl)),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f431,plain,(
% 0.13/11.00 nil=sK49_skl|ssList(sK54_skl)),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f432,plain,(
% 0.13/11.00 nil=sK49_skl|app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK49_skl),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f433,plain,(
% 0.13/11.00 ![X0]: (nil=sK49_skl|~ssItem(X0)|leq(X0,sK52_skl)|~memberP(sK53_skl,X0)|~memberP(sK54_skl,X0)|~leq(sK52_skl,X0))),
% 0.13/11.00 inference(cnf_transformation,[status(thm)],[f416])).
% 0.13/11.00 fof(f434,definition,(
% 0.13/11.00 sQ0_spl <=> (nil=sK49_skl)),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f435,plain,(
% 0.13/11.00 nil=sK49_skl|~sQ0_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f434])).
% 0.13/11.00 fof(f437,definition,(
% 0.13/11.00 sQ1_spl <=> (ssItem(sK52_skl))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f440,plain,(
% 0.13/11.00 sQ0_spl|sQ1_spl),
% 0.13/11.00 inference(split_clause,[status(thm)],[f429,f434,f437])).
% 0.13/11.00 fof(f441,definition,(
% 0.13/11.00 sQ2_spl <=> (ssList(sK53_skl))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f444,plain,(
% 0.13/11.00 sQ0_spl|sQ2_spl),
% 0.13/11.00 inference(split_clause,[status(thm)],[f430,f434,f441])).
% 0.13/11.00 fof(f445,definition,(
% 0.13/11.00 sQ3_spl <=> (ssList(sK54_skl))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f448,plain,(
% 0.13/11.00 sQ0_spl|sQ3_spl),
% 0.13/11.00 inference(split_clause,[status(thm)],[f431,f434,f445])).
% 0.13/11.00 fof(f449,definition,(
% 0.13/11.00 sQ4_spl <=> (app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK49_skl)),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f450,plain,(
% 0.13/11.00 app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK49_skl|~sQ4_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f449])).
% 0.13/11.00 fof(f452,plain,(
% 0.13/11.00 sQ0_spl|sQ4_spl),
% 0.13/11.00 inference(split_clause,[status(thm)],[f432,f434,f449])).
% 0.13/11.00 fof(f453,definition,(
% 0.13/11.00 ![X0]: (sQ5_spl <=> (~ssItem(X0)|leq(X0,sK52_skl)|~memberP(sK53_skl,X0)|~memberP(sK54_skl,X0)|~leq(sK52_skl,X0)))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f454,plain,(
% 0.13/11.00 ![X0]: (~ssItem(X0)|leq(X0,sK52_skl)|~memberP(sK53_skl,X0)|~memberP(sK54_skl,X0)|~leq(sK52_skl,X0)|~sQ5_spl)),
% 0.13/11.00 inference(component_clause,[status(thm)],[f453])).
% 0.13/11.00 fof(f456,plain,(
% 0.13/11.00 sQ0_spl|sQ5_spl),
% 0.13/11.00 inference(split_clause,[status(thm)],[f433,f434,f453])).
% 0.13/11.00 fof(f503,plain,(
% 0.13/11.00 ![X0]: (~ssItem(X0)|ssList(cons(X0,nil)))),
% 0.13/11.00 inference(resolution,[status(thm)],[f223,f222])).
% 0.13/11.00 fof(f504,plain,(
% 0.13/11.00 leq(sK0_skl,sK0_skl)),
% 0.13/11.00 inference(resolution,[status(thm)],[f103,f255])).
% 0.13/11.00 fof(f505,plain,(
% 0.13/11.00 leq(sK1_skl,sK1_skl)),
% 0.13/11.00 inference(resolution,[status(thm)],[f104,f255])).
% 0.13/11.00 fof(f523,plain,(
% 0.13/11.00 sK47_skl=nil|~sQ0_spl),
% 0.13/11.00 inference(backward_demodulation,[status(thm)],[f435,f422])).
% 0.13/11.00 fof(f524,plain,(
% 0.13/11.00 $false|~sQ0_spl),
% 0.13/11.00 inference(forward_subsumption_resolution,[status(thm)],[f523,f423])).
% 0.13/11.00 fof(f525,plain,(
% 0.13/11.00 ~sQ0_spl),
% 0.13/11.00 inference(contradiction_clause,[status(thm)],[f524])).
% 0.13/11.00 fof(f530,definition,(
% 0.13/11.00 sQ7_spl <=> (ssList(nil))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f532,plain,(
% 0.13/11.00 ~ssList(nil)|sQ7_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f530])).
% 0.13/11.00 fof(f533,definition,(
% 0.13/11.00 sQ8_spl <=> (ssList(sK49_skl))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f535,plain,(
% 0.13/11.00 ~ssList(sK49_skl)|sQ8_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f533])).
% 0.13/11.00 fof(f541,definition,(
% 0.13/11.00 sQ10_spl <=> (ssList(sK48_skl))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f543,plain,(
% 0.13/11.00 ~ssList(sK48_skl)|sQ10_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f541])).
% 0.13/11.00 fof(f545,plain,(
% 0.13/11.00 $false|sQ7_spl),
% 0.13/11.00 inference(forward_subsumption_resolution,[status(thm)],[f532,f223])).
% 0.13/11.00 fof(f546,plain,(
% 0.13/11.00 sQ7_spl),
% 0.13/11.00 inference(contradiction_clause,[status(thm)],[f545])).
% 0.13/11.00 fof(f553,definition,(
% 0.13/11.00 sQ12_spl <=> (ssList(sK47_skl))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f555,plain,(
% 0.13/11.00 ~ssList(sK47_skl)|sQ12_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f553])).
% 0.13/11.00 fof(f568,plain,(
% 0.13/11.00 ssList(cons(sK1_skl,nil))),
% 0.13/11.00 inference(resolution,[status(thm)],[f503,f104])).
% 0.13/11.00 fof(f574,definition,(
% 0.13/11.00 sQ15_spl <=> (ssItem(sK0_skl))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f576,plain,(
% 0.13/11.00 ~ssItem(sK0_skl)|sQ15_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f574])).
% 0.13/11.00 fof(f582,definition,(
% 0.13/11.00 sQ17_spl <=> (ssItem(sK1_skl))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f584,plain,(
% 0.13/11.00 ~ssItem(sK1_skl)|sQ17_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f582])).
% 0.13/11.00 fof(f649,definition,(
% 0.13/11.00 sQ23_spl <=> (ssItem(sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f660,plain,(
% 0.13/11.00 app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)=sK47_skl|~sQ4_spl),
% 0.13/11.00 inference(backward_demodulation,[status(thm)],[f422,f450])).
% 0.13/11.00 fof(f674,definition,(
% 0.13/11.00 sQ27_spl <=> (ssList(cons(sK1_skl,nil)))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f676,plain,(
% 0.13/11.00 ~ssList(cons(sK1_skl,nil))|sQ27_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f674])).
% 0.13/11.00 fof(f678,plain,(
% 0.13/11.00 $false|sQ12_spl),
% 0.13/11.00 inference(forward_subsumption_resolution,[status(thm)],[f555,f417])).
% 0.13/11.00 fof(f679,plain,(
% 0.13/11.00 sQ12_spl),
% 0.13/11.00 inference(contradiction_clause,[status(thm)],[f678])).
% 0.13/11.00 fof(f695,plain,(
% 0.13/11.00 $false|sQ10_spl),
% 0.13/11.00 inference(forward_subsumption_resolution,[status(thm)],[f543,f418])).
% 0.13/11.00 fof(f696,plain,(
% 0.13/11.00 sQ10_spl),
% 0.13/11.00 inference(contradiction_clause,[status(thm)],[f695])).
% 0.13/11.00 fof(f722,plain,(
% 0.13/11.00 $false|sQ17_spl),
% 0.13/11.00 inference(forward_subsumption_resolution,[status(thm)],[f584,f104])).
% 0.13/11.00 fof(f723,plain,(
% 0.13/11.00 sQ17_spl),
% 0.13/11.00 inference(contradiction_clause,[status(thm)],[f722])).
% 0.13/11.00 fof(f790,plain,(
% 0.13/11.00 $false|sQ15_spl),
% 0.13/11.00 inference(forward_subsumption_resolution,[status(thm)],[f576,f103])).
% 0.13/11.00 fof(f791,plain,(
% 0.13/11.00 sQ15_spl),
% 0.13/11.00 inference(contradiction_clause,[status(thm)],[f790])).
% 0.13/11.00 fof(f884,plain,(
% 0.13/11.00 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|memberP(sK54_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 0.13/11.00 inference(resolution,[status(thm)],[f660,f426])).
% 0.13/11.00 fof(f886,definition,(
% 0.13/11.00 sQ66_spl <=> (memberP(sK54_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f887,plain,(
% 0.13/11.00 memberP(sK54_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ66_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f886])).
% 0.13/11.00 fof(f889,plain,(
% 0.13/11.00 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ66_spl|~sQ4_spl),
% 0.13/11.00 inference(split_clause,[status(thm)],[f884,f437,f441,f445,f886,f449])).
% 0.13/11.00 fof(f951,definition,(
% 0.13/11.00 sQ77_spl <=> (leq(sK1_skl,sK1_skl))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f953,plain,(
% 0.13/11.00 ~leq(sK1_skl,sK1_skl)|sQ77_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f951])).
% 0.13/11.00 fof(f958,definition,(
% 0.13/11.00 sQ79_spl <=> (leq(sK0_skl,sK0_skl))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f960,plain,(
% 0.13/11.00 ~leq(sK0_skl,sK0_skl)|sQ79_spl),
% 0.13/11.00 inference(component_clause,[status(thm)],[f958])).
% 0.13/11.00 fof(f965,plain,(
% 0.13/11.00 $false|sQ77_spl),
% 0.13/11.00 inference(forward_subsumption_resolution,[status(thm)],[f953,f505])).
% 0.13/11.00 fof(f966,plain,(
% 0.13/11.00 sQ77_spl),
% 0.13/11.00 inference(contradiction_clause,[status(thm)],[f965])).
% 0.13/11.00 fof(f967,plain,(
% 0.13/11.00 $false|sQ79_spl),
% 0.13/11.00 inference(forward_subsumption_resolution,[status(thm)],[f960,f504])).
% 0.13/11.00 fof(f968,plain,(
% 0.13/11.00 sQ79_spl),
% 0.13/11.00 inference(contradiction_clause,[status(thm)],[f967])).
% 0.13/11.00 fof(f1137,plain,(
% 0.13/11.00 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|leq(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 0.13/11.00 inference(resolution,[status(thm)],[f427,f660])).
% 0.13/11.00 fof(f1139,definition,(
% 0.13/11.00 sQ100_spl <=> (leq(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f1142,plain,(
% 0.13/11.00 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ100_spl|~sQ4_spl),
% 0.13/11.00 inference(split_clause,[status(thm)],[f1137,f437,f441,f445,f1139,f449])).
% 0.13/11.00 fof(f1352,definition,(
% 0.13/11.00 ![X1]: (sQ132_spl <=> (~ssList(X1)))),
% 0.13/11.00 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 0.13/11.00 fof(f1353,plain,(
% 0.13/11.00 ![X0]: (~ssList(X0)|~sQ132_spl)),
% 0.13/11.00 inference(component_clause,[status(thm)],[f1352])).
% 0.13/11.01 fof(f1444,plain,(
% 0.13/11.01 ~ssList(sK47_skl)|sQ8_spl),
% 0.13/11.01 inference(forward_demodulation,[status(thm)],[f422,f535])).
% 0.13/11.01 fof(f1445,plain,(
% 0.13/11.01 $false|sQ8_spl),
% 0.13/11.01 inference(forward_subsumption_resolution,[status(thm)],[f1444,f417])).
% 0.13/11.01 fof(f1446,plain,(
% 0.13/11.01 sQ8_spl),
% 0.13/11.01 inference(contradiction_clause,[status(thm)],[f1445])).
% 0.13/11.01 fof(f1489,plain,(
% 0.13/11.01 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|~leq(sK51_skl(sK54_skl,sK53_skl,sK52_skl),sK52_skl)|~sQ4_spl),
% 0.13/11.01 inference(resolution,[status(thm)],[f428,f660])).
% 0.13/11.01 fof(f1491,definition,(
% 0.13/11.01 sQ155_spl <=> (leq(sK51_skl(sK54_skl,sK53_skl,sK52_skl),sK52_skl))),
% 0.13/11.01 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 0.13/11.01 fof(f1494,plain,(
% 0.13/11.01 ~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ155_spl|~sQ4_spl),
% 0.13/11.01 inference(split_clause,[status(thm)],[f1489,f437,f441,f445,f1491,f449])).
% 0.13/11.01 fof(f1502,plain,(
% 0.13/11.01 $false|~sQ132_spl),
% 0.13/11.01 inference(backward_subsumption_resolution,[status(thm)],[f417,f1353])).
% 0.13/11.01 fof(f1506,plain,(
% 0.13/11.01 ~sQ132_spl),
% 0.13/11.01 inference(contradiction_clause,[status(thm)],[f1502])).
% 0.13/11.01 fof(f1846,plain,(
% 0.13/11.01 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|memberP(sK53_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 0.13/11.01 inference(resolution,[status(thm)],[f425,f660])).
% 0.13/11.01 fof(f1848,definition,(
% 0.13/11.01 sQ188_spl <=> (memberP(sK53_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl)))),
% 0.13/11.01 introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition])).
% 0.13/11.01 fof(f1851,plain,(
% 0.13/11.01 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ188_spl|~sQ4_spl),
% 0.13/11.01 inference(split_clause,[status(thm)],[f1846,f437,f441,f445,f1848,f449])).
% 0.13/11.01 fof(f1915,definition,(
% 0.13/11.01 sQ190_spl <=> (nil=sK47_skl)),
% 0.13/11.01 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 0.13/11.01 fof(f1916,plain,(
% 0.13/11.01 nil=sK47_skl|~sQ190_spl),
% 0.13/11.01 inference(component_clause,[status(thm)],[f1915])).
% 0.13/11.01 fof(f1997,plain,(
% 0.13/11.01 $false|~sQ190_spl),
% 0.13/11.01 inference(forward_subsumption_resolution,[status(thm)],[f1916,f423])).
% 0.13/11.01 fof(f1998,plain,(
% 0.13/11.01 ~sQ190_spl),
% 0.13/11.01 inference(contradiction_clause,[status(thm)],[f1997])).
% 0.13/11.01 fof(f2364,plain,(
% 0.13/11.01 ~ssItem(sK52_skl)|~ssList(sK53_skl)|~ssList(sK54_skl)|ssItem(sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ4_spl),
% 0.13/11.01 inference(resolution,[status(thm)],[f660,f424])).
% 0.13/11.01 fof(f2375,plain,(
% 0.13/11.01 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ23_spl|~sQ4_spl),
% 0.13/11.01 inference(split_clause,[status(thm)],[f2364,f437,f441,f445,f649,f449])).
% 0.13/11.01 fof(f7047,plain,(
% 0.13/11.01 $false|sQ27_spl),
% 0.13/11.01 inference(forward_subsumption_resolution,[status(thm)],[f676,f568])).
% 0.13/11.01 fof(f7048,plain,(
% 0.13/11.01 sQ27_spl),
% 0.13/11.01 inference(contradiction_clause,[status(thm)],[f7047])).
% 0.13/11.01 fof(f9313,plain,(
% 0.13/11.01 ~ssItem(sK51_skl(sK54_skl,sK53_skl,sK52_skl))|leq(sK51_skl(sK54_skl,sK53_skl,sK52_skl),sK52_skl)|~memberP(sK53_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~leq(sK52_skl,sK51_skl(sK54_skl,sK53_skl,sK52_skl))|~sQ66_spl|~sQ5_spl),
% 0.13/11.01 inference(resolution,[status(thm)],[f887,f454])).
% 0.13/11.01 fof(f9325,plain,(
% 0.13/11.01 ~sQ23_spl|sQ155_spl|~sQ188_spl|~sQ100_spl|~sQ66_spl|~sQ5_spl),
% 0.13/11.01 inference(split_clause,[status(thm)],[f9313,f649,f1491,f1848,f1139,f886,f453])).
% 0.13/11.01 fof(f9370,plain,(
% 0.13/11.01 $false),
% 0.13/11.01 inference(sat_refutation,[status(thm)],[f440,f444,f448,f452,f456,f525,f546,f679,f696,f723,f791,f889,f966,f968,f1142,f1446,f1494,f1506,f1851,f1998,f2375,f7048,f9325])).
% 0.13/11.01 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/11.03 % Elapsed time: 0.633938 seconds
% 0.13/11.03 % CPU time: 4.797461 seconds
% 0.13/11.03 % Total memory used: 170.176 MB
% 0.13/11.03 % Net memory used: 165.865 MB
%------------------------------------------------------------------------------