%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC402+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 : n019.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:42:22 PM UTC 2026
% Result : Theorem 10.96s 2.11s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.23 % Problem : SWC402+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.24 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.58 % Computer : n019.cluster.edu
% 0.09/0.58 % Model : x86_64 x86_64
% 0.09/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.58 % Memory : 8046.5625MB
% 0.09/0.58 % OS : Linux 6.8.0-71-generic
% 0.09/0.58 % CPULimit : 300
% 0.09/0.58 % WCLimit : 300
% 0.09/0.58 % DateTime : Mon Sep 21 08:21:37 UTC 2026
% 0.09/0.58 % CPUTime :
% 0.09/0.60 % Drodi V4.1.1
% 10.96/2.11 % Refutation found
% 10.96/2.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.96/2.11 % SZS output start CNFRefutation for theBenchmark
% 10.96/2.11 fof(f26,axiom,(
% 10.96/2.11 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ssList(app(U,V)) ) )) )),
% 10.96/2.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.96/2.11 fof(f36,axiom,(
% 10.96/2.11 (! [U] :( ssItem(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( memberP(app(V,W),U)<=> ( memberP(V,U)| memberP(W,U) ) ) ) )) )) )),
% 10.96/2.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.96/2.11 fof(f96,conjecture,(
% 10.96/2.11 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| (! [Y] :( ssList(Y)=> (! [Z] :( ~ ssList(Z)| app(app(Y,W),Z) != X| ~ totalorderedP(W)| (? [X1] :( ssItem(X1)& (? [X2] :( ssList(X2)& app(X2,cons(X1,nil)) = Y& (? [X3] :( ssItem(X3)& (? [X4] :( ssList(X4)& app(cons(X3,nil),X4) = W& leq(X1,X3) ) )) )) )))| (? [X5] :( ssItem(X5)& (? [X6] :( ssList(X6)& app(cons(X5,nil),X6) = Z& (? [X7] :( ssItem(X7)& (? [X8] :( ssList(X8)& app(X8,cons(X7,nil)) = W& leq(X7,X5) ) )) )) )) )) )))| (! [X9] :( ~ ssItem(X9)| ~ memberP(U,X9)| memberP(V,X9) ))| ( nil != X& nil = W ) ) )) )) )) )),
% 10.96/2.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.96/2.11 fof(f97,negated_conjecture,(
% 10.96/2.11 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| (! [Y] :( ssList(Y)=> (! [Z] :( ~ ssList(Z)| app(app(Y,W),Z) != X| ~ totalorderedP(W)| (? [X1] :( ssItem(X1)& (? [X2] :( ssList(X2)& app(X2,cons(X1,nil)) = Y& (? [X3] :( ssItem(X3)& (? [X4] :( ssList(X4)& app(cons(X3,nil),X4) = W& leq(X1,X3) ) )) )) )))| (? [X5] :( ssItem(X5)& (? [X6] :( ssList(X6)& app(cons(X5,nil),X6) = Z& (? [X7] :( ssItem(X7)& (? [X8] :( ssList(X8)& app(X8,cons(X7,nil)) = W& leq(X7,X5) ) )) )) )) )) )))| (! [X9] :( ~ ssItem(X9)| ~ memberP(U,X9)| memberP(V,X9) ))| ( nil != X& nil = W ) ) )) )) )) ))),
% 10.96/2.11 inference(negated_conjecture,[status(cth)],[f96])).
% 10.96/2.11 fof(f244,plain,(
% 10.96/2.11 ![U]: (~ssList(U)|(![V]: (~ssList(V)|ssList(app(U,V)))))),
% 10.96/2.11 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 10.96/2.11 fof(f245,plain,(
% 10.96/2.11 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X0,X1)))),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f244])).
% 10.96/2.11 fof(f268,plain,(
% 10.96/2.11 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(memberP(app(V,W),U)<=>(memberP(V,U)|memberP(W,U))))))))),
% 10.96/2.11 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 10.96/2.11 fof(f269,plain,(
% 10.96/2.11 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~memberP(app(V,W),U)|(memberP(V,U)|memberP(W,U)))&(memberP(app(V,W),U)|(~memberP(V,U)&~memberP(W,U)))))))))),
% 10.96/2.11 inference(NNF_transformation,[status(thm)],[f268])).
% 10.96/2.11 fof(f271,plain,(
% 10.96/2.11 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X1,X0))),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f269])).
% 10.96/2.11 fof(f272,plain,(
% 10.96/2.11 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X2,X0))),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f269])).
% 10.96/2.11 fof(f415,plain,(
% 10.96/2.11 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (((((ssList(X)&V=X)&U=W)&(?[Y]: (ssList(Y)&(?[Z]: ((((ssList(Z)&app(app(Y,W),Z)=X)&totalorderedP(W))&(![X1]: (~ssItem(X1)|(![X2]: ((~ssList(X2)|~app(X2,cons(X1,nil))=Y)|(![X3]: (~ssItem(X3)|(![X4]: ((~ssList(X4)|~app(cons(X3,nil),X4)=W)|~leq(X1,X3))))))))))&(![X5]: (~ssItem(X5)|(![X6]: ((~ssList(X6)|~app(cons(X5,nil),X6)=Z)|(![X7]: (~ssItem(X7)|(![X8]: ((~ssList(X8)|~app(X8,cons(X7,nil))=W)|~leq(X7,X5))))))))))))))&(?[X9]: ((ssItem(X9)&memberP(U,X9))&~memberP(V,X9))))&(nil=X|~nil=W)))))))))),
% 10.96/2.11 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 10.96/2.11 fof(f416,plain,(
% 10.96/2.11 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (((((ssList(X)&V=X)&U=W)&(?[Y]: (ssList(Y)&(?[Z]: ((((ssList(Z)&app(app(Y,W),Z)=X)&totalorderedP(W))&(![X1]: (~ssItem(X1)|((![X2]: (~ssList(X2)|~app(X2,cons(X1,nil))=Y))|(![X3]: (~ssItem(X3)|((![X4]: (~ssList(X4)|~app(cons(X3,nil),X4)=W))|~leq(X1,X3))))))))&(![X5]: (~ssItem(X5)|((![X6]: (~ssList(X6)|~app(cons(X5,nil),X6)=Z))|(![X7]: (~ssItem(X7)|((![X8]: (~ssList(X8)|~app(X8,cons(X7,nil))=W))|~leq(X7,X5))))))))))))&(?[X9]: ((ssItem(X9)&memberP(U,X9))&~memberP(V,X9))))&(nil=X|~nil=W))))))))),
% 10.96/2.11 inference(miniscoping,[status(thm)],[f415])).
% 10.96/2.11 fof(f417,plain,(
% 10.96/2.11 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(((((ssList(sK50_skl)&sK48_skl=sK50_skl)&sK47_skl=sK49_skl)&(ssList(sK51_skl)&((((ssList(sK52_skl)&app(app(sK51_skl,sK49_skl),sK52_skl)=sK50_skl)&totalorderedP(sK49_skl))&(![X1]: (~ssItem(X1)|((![X2]: (~ssList(X2)|~app(X2,cons(X1,nil))=sK51_skl))|(![X3]: (~ssItem(X3)|((![X4]: (~ssList(X4)|~app(cons(X3,nil),X4)=sK49_skl))|~leq(X1,X3))))))))&(![X5]: (~ssItem(X5)|((![X6]: (~ssList(X6)|~app(cons(X5,nil),X6)=sK52_skl))|(![X7]: (~ssItem(X7)|((![X8]: (~ssList(X8)|~app(X8,cons(X7,nil))=sK49_skl))|~leq(X7,X5))))))))))&((ssItem(sK53_skl)&memberP(sK47_skl,sK53_skl))&~memberP(sK48_skl,sK53_skl)))&(nil=sK50_skl|~nil=sK49_skl)))))),
% 10.96/2.11 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl,sK53_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Y,sK51_skl),skolemize(Z,sK52_skl),skolemize(X9,sK53_skl)],[f416])).
% 10.96/2.11 fof(f418,plain,(
% 10.96/2.11 ssList(sK47_skl)),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f417])).
% 10.96/2.11 fof(f422,plain,(
% 10.96/2.11 sK48_skl=sK50_skl),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f417])).
% 10.96/2.11 fof(f423,plain,(
% 10.96/2.11 sK47_skl=sK49_skl),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f417])).
% 10.96/2.11 fof(f424,plain,(
% 10.96/2.11 ssList(sK51_skl)),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f417])).
% 10.96/2.11 fof(f425,plain,(
% 10.96/2.11 ssList(sK52_skl)),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f417])).
% 10.96/2.11 fof(f426,plain,(
% 10.96/2.11 app(app(sK51_skl,sK49_skl),sK52_skl)=sK50_skl),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f417])).
% 10.96/2.11 fof(f430,plain,(
% 10.96/2.11 ssItem(sK53_skl)),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f417])).
% 10.96/2.11 fof(f431,plain,(
% 10.96/2.11 memberP(sK47_skl,sK53_skl)),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f417])).
% 10.96/2.11 fof(f432,plain,(
% 10.96/2.11 ~memberP(sK48_skl,sK53_skl)),
% 10.96/2.11 inference(cnf_transformation,[status(thm)],[f417])).
% 10.96/2.11 fof(f504,plain,(
% 10.96/2.11 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|memberP(app(sK51_skl,X1),X0)|~memberP(X1,X0))),
% 10.96/2.12 inference(resolution,[status(thm)],[f424,f272])).
% 10.96/2.12 fof(f512,plain,(
% 10.96/2.12 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|memberP(app(X1,sK52_skl),X0)|~memberP(X1,X0))),
% 10.96/2.12 inference(resolution,[status(thm)],[f425,f271])).
% 10.96/2.12 fof(f516,plain,(
% 10.96/2.12 app(app(sK51_skl,sK47_skl),sK52_skl)=sK50_skl),
% 10.96/2.12 inference(forward_demodulation,[status(thm)],[f423,f426])).
% 10.96/2.12 fof(f517,plain,(
% 10.96/2.12 app(app(sK51_skl,sK47_skl),sK52_skl)=sK48_skl),
% 10.96/2.12 inference(forward_demodulation,[status(thm)],[f422,f516])).
% 10.96/2.12 fof(f522,definition,(
% 10.96/2.12 sQ3_spl <=> (ssList(app(sK51_skl,sK47_skl)))),
% 10.96/2.12 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 10.96/2.12 fof(f524,plain,(
% 10.96/2.12 ~ssList(app(sK51_skl,sK47_skl))|sQ3_spl),
% 10.96/2.12 inference(component_clause,[status(thm)],[f522])).
% 10.96/2.12 fof(f550,definition,(
% 10.96/2.12 sQ7_spl <=> (ssList(sK47_skl))),
% 10.96/2.12 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 10.96/2.12 fof(f552,plain,(
% 10.96/2.12 ~ssList(sK47_skl)|sQ7_spl),
% 10.96/2.12 inference(component_clause,[status(thm)],[f550])).
% 10.96/2.12 fof(f554,plain,(
% 10.96/2.12 $false|sQ7_spl),
% 10.96/2.12 inference(forward_subsumption_resolution,[status(thm)],[f552,f418])).
% 10.96/2.12 fof(f555,plain,(
% 10.96/2.12 sQ7_spl),
% 10.96/2.12 inference(contradiction_clause,[status(thm)],[f554])).
% 10.96/2.12 fof(f644,definition,(
% 10.96/2.12 sQ19_spl <=> (ssItem(sK53_skl))),
% 10.96/2.12 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 10.96/2.12 fof(f646,plain,(
% 10.96/2.12 ~ssItem(sK53_skl)|sQ19_spl),
% 10.96/2.12 inference(component_clause,[status(thm)],[f644])).
% 10.96/2.12 fof(f651,plain,(
% 10.96/2.12 $false|sQ19_spl),
% 10.96/2.12 inference(forward_subsumption_resolution,[status(thm)],[f646,f430])).
% 10.96/2.12 fof(f652,plain,(
% 10.96/2.12 sQ19_spl),
% 10.96/2.12 inference(contradiction_clause,[status(thm)],[f651])).
% 10.96/2.12 fof(f1286,plain,(
% 10.96/2.12 ![X0]: (~ssList(X0)|ssList(app(sK51_skl,X0)))),
% 10.96/2.12 inference(resolution,[status(thm)],[f245,f424])).
% 10.96/2.12 fof(f3151,plain,(
% 10.96/2.12 ~ssItem(sK53_skl)|~ssList(sK47_skl)|memberP(app(sK51_skl,sK47_skl),sK53_skl)),
% 10.96/2.12 inference(resolution,[status(thm)],[f504,f431])).
% 10.96/2.12 fof(f3224,definition,(
% 10.96/2.12 sQ456_spl <=> (memberP(app(sK51_skl,sK47_skl),sK53_skl))),
% 10.96/2.12 introduced(definition,[new_symbols(definition,[sQ456_spl])],[split_symbol_definition])).
% 10.96/2.13 fof(f3225,plain,(
% 10.96/2.13 memberP(app(sK51_skl,sK47_skl),sK53_skl)|~sQ456_spl),
% 10.96/2.13 inference(component_clause,[status(thm)],[f3224])).
% 10.96/2.13 fof(f3227,plain,(
% 10.96/2.13 ~sQ19_spl|~sQ7_spl|sQ456_spl),
% 10.96/2.13 inference(split_clause,[status(thm)],[f3151,f644,f550,f3224])).
% 10.96/2.13 fof(f3778,plain,(
% 10.96/2.13 ~ssItem(sK53_skl)|~ssList(app(sK51_skl,sK47_skl))|memberP(app(app(sK51_skl,sK47_skl),sK52_skl),sK53_skl)|~sQ456_spl),
% 10.96/2.13 inference(resolution,[status(thm)],[f512,f3225])).
% 10.96/2.13 fof(f3803,definition,(
% 10.96/2.13 sQ567_spl <=> (memberP(app(app(sK51_skl,sK47_skl),sK52_skl),sK53_skl))),
% 10.96/2.13 introduced(definition,[new_symbols(definition,[sQ567_spl])],[split_symbol_definition])).
% 10.96/2.13 fof(f3804,plain,(
% 10.96/2.13 memberP(app(app(sK51_skl,sK47_skl),sK52_skl),sK53_skl)|~sQ567_spl),
% 10.96/2.13 inference(component_clause,[status(thm)],[f3803])).
% 10.96/2.13 fof(f3806,plain,(
% 10.96/2.13 ~sQ19_spl|~sQ3_spl|sQ567_spl|~sQ456_spl),
% 10.96/2.13 inference(split_clause,[status(thm)],[f3778,f644,f522,f3803,f3224])).
% 10.96/2.13 fof(f12002,plain,(
% 10.96/2.13 ssList(app(sK51_skl,sK47_skl))),
% 10.96/2.13 inference(resolution,[status(thm)],[f1286,f418])).
% 10.96/2.13 fof(f12004,plain,(
% 10.96/2.13 $false|sQ3_spl),
% 10.96/2.13 inference(forward_subsumption_resolution,[status(thm)],[f12002,f524])).
% 10.96/2.13 fof(f12005,plain,(
% 10.96/2.13 sQ3_spl),
% 10.96/2.13 inference(contradiction_clause,[status(thm)],[f12004])).
% 10.96/2.13 fof(f12008,plain,(
% 10.96/2.13 memberP(sK48_skl,sK53_skl)|~sQ567_spl),
% 10.96/2.13 inference(forward_demodulation,[status(thm)],[f517,f3804])).
% 10.96/2.13 fof(f12009,plain,(
% 10.96/2.13 $false|~sQ567_spl),
% 10.96/2.13 inference(forward_subsumption_resolution,[status(thm)],[f12008,f432])).
% 10.96/2.13 fof(f12010,plain,(
% 10.96/2.13 ~sQ567_spl),
% 10.96/2.13 inference(contradiction_clause,[status(thm)],[f12009])).
% 10.96/2.13 fof(f12011,plain,(
% 10.96/2.13 $false),
% 10.96/2.13 inference(sat_refutation,[status(thm)],[f555,f652,f3227,f3806,f12005,f12010])).
% 10.96/2.13 % SZS output end CNFRefutation for theBenchmark.p
% 10.96/2.15 % Elapsed time: 1.546211 seconds
% 10.96/2.15 % CPU time: 12.011913 seconds
% 10.96/2.15 % Total memory used: 223.410 MB
% 10.96/2.15 % Net memory used: 216.062 MB
%------------------------------------------------------------------------------