%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC399+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 : n015.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.34s 1.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC399+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.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 08:24:51 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 10.34/1.77 % Refutation found
% 10.34/1.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.34/1.77 % SZS output start CNFRefutation for theBenchmark
% 10.34/1.77 fof(f26,axiom,(
% 10.34/1.77 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ssList(app(U,V)) ) )) )),
% 10.34/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.34/1.77 fof(f36,axiom,(
% 10.34/1.77 (! [U] :( ssItem(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( memberP(app(V,W),U)<=> ( memberP(V,U)| memberP(W,U) ) ) ) )) )) )),
% 10.34/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.34/1.77 fof(f96,conjecture,(
% 10.34/1.77 (! [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| ~ equalelemsP(W)| (? [X1] :( ssItem(X1)& (? [X2] :( ssList(X2)& app(X2,cons(X1,nil)) = Y& (? [X3] :( ssList(X3)& app(cons(X1,nil),X3) = W ) )) )))| (? [X4] :( ssItem(X4)& (? [X5] :( ssList(X5)& app(cons(X4,nil),X5) = Z& (? [X6] :( ssList(X6)& app(X6,cons(X4,nil)) = W ) )) )) )) )))| (! [X7] :( ~ ssItem(X7)| ~ memberP(U,X7)| memberP(V,X7) ))| ( nil != X& nil = W ) ) )) )) )) )),
% 10.34/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.34/1.77 fof(f97,negated_conjecture,(
% 10.34/1.77 ~((! [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| ~ equalelemsP(W)| (? [X1] :( ssItem(X1)& (? [X2] :( ssList(X2)& app(X2,cons(X1,nil)) = Y& (? [X3] :( ssList(X3)& app(cons(X1,nil),X3) = W ) )) )))| (? [X4] :( ssItem(X4)& (? [X5] :( ssList(X5)& app(cons(X4,nil),X5) = Z& (? [X6] :( ssList(X6)& app(X6,cons(X4,nil)) = W ) )) )) )) )))| (! [X7] :( ~ ssItem(X7)| ~ memberP(U,X7)| memberP(V,X7) ))| ( nil != X& nil = W ) ) )) )) )) ))),
% 10.34/1.77 inference(negated_conjecture,[status(cth)],[f96])).
% 10.34/1.77 fof(f244,plain,(
% 10.34/1.77 ![U]: (~ssList(U)|(![V]: (~ssList(V)|ssList(app(U,V)))))),
% 10.34/1.77 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 10.34/1.77 fof(f245,plain,(
% 10.34/1.77 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X0,X1)))),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f244])).
% 10.34/1.77 fof(f268,plain,(
% 10.34/1.77 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(memberP(app(V,W),U)<=>(memberP(V,U)|memberP(W,U))))))))),
% 10.34/1.77 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 10.34/1.77 fof(f269,plain,(
% 10.34/1.77 ![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.34/1.77 inference(NNF_transformation,[status(thm)],[f268])).
% 10.34/1.77 fof(f271,plain,(
% 10.34/1.77 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X1,X0))),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f269])).
% 10.34/1.77 fof(f272,plain,(
% 10.34/1.77 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X2,X0))),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f269])).
% 10.34/1.77 fof(f415,plain,(
% 10.34/1.77 (?[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)&equalelemsP(W))&(![X1]: (~ssItem(X1)|(![X2]: ((~ssList(X2)|~app(X2,cons(X1,nil))=Y)|(![X3]: (~ssList(X3)|~app(cons(X1,nil),X3)=W)))))))&(![X4]: (~ssItem(X4)|(![X5]: ((~ssList(X5)|~app(cons(X4,nil),X5)=Z)|(![X6]: (~ssList(X6)|~app(X6,cons(X4,nil))=W)))))))))))&(?[X7]: ((ssItem(X7)&memberP(U,X7))&~memberP(V,X7))))&(nil=X|~nil=W)))))))))),
% 10.34/1.77 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 10.34/1.77 fof(f416,plain,(
% 10.34/1.77 ?[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)&equalelemsP(W))&(![X1]: (~ssItem(X1)|((![X2]: (~ssList(X2)|~app(X2,cons(X1,nil))=Y))|(![X3]: (~ssList(X3)|~app(cons(X1,nil),X3)=W))))))&(![X4]: (~ssItem(X4)|((![X5]: (~ssList(X5)|~app(cons(X4,nil),X5)=Z))|(![X6]: (~ssList(X6)|~app(X6,cons(X4,nil))=W))))))))))&(?[X7]: ((ssItem(X7)&memberP(U,X7))&~memberP(V,X7))))&(nil=X|~nil=W))))))))),
% 10.34/1.77 inference(miniscoping,[status(thm)],[f415])).
% 10.34/1.77 fof(f417,plain,(
% 10.34/1.77 (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)&equalelemsP(sK49_skl))&(![X1]: (~ssItem(X1)|((![X2]: (~ssList(X2)|~app(X2,cons(X1,nil))=sK51_skl))|(![X3]: (~ssList(X3)|~app(cons(X1,nil),X3)=sK49_skl))))))&(![X4]: (~ssItem(X4)|((![X5]: (~ssList(X5)|~app(cons(X4,nil),X5)=sK52_skl))|(![X6]: (~ssList(X6)|~app(X6,cons(X4,nil))=sK49_skl))))))))&((ssItem(sK53_skl)&memberP(sK47_skl,sK53_skl))&~memberP(sK48_skl,sK53_skl)))&(nil=sK50_skl|~nil=sK49_skl)))))),
% 10.34/1.77 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(X7,sK53_skl)],[f416])).
% 10.34/1.77 fof(f418,plain,(
% 10.34/1.77 ssList(sK47_skl)),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f417])).
% 10.34/1.77 fof(f422,plain,(
% 10.34/1.77 sK48_skl=sK50_skl),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f417])).
% 10.34/1.77 fof(f423,plain,(
% 10.34/1.77 sK47_skl=sK49_skl),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f417])).
% 10.34/1.77 fof(f424,plain,(
% 10.34/1.77 ssList(sK51_skl)),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f417])).
% 10.34/1.77 fof(f425,plain,(
% 10.34/1.77 ssList(sK52_skl)),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f417])).
% 10.34/1.77 fof(f426,plain,(
% 10.34/1.77 app(app(sK51_skl,sK49_skl),sK52_skl)=sK50_skl),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f417])).
% 10.34/1.77 fof(f430,plain,(
% 10.34/1.77 ssItem(sK53_skl)),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f417])).
% 10.34/1.77 fof(f431,plain,(
% 10.34/1.77 memberP(sK47_skl,sK53_skl)),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f417])).
% 10.34/1.77 fof(f432,plain,(
% 10.34/1.77 ~memberP(sK48_skl,sK53_skl)),
% 10.34/1.77 inference(cnf_transformation,[status(thm)],[f417])).
% 10.34/1.77 fof(f502,plain,(
% 10.34/1.77 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|memberP(app(sK51_skl,X1),X0)|~memberP(X1,X0))),
% 10.34/1.77 inference(resolution,[status(thm)],[f424,f272])).
% 10.34/1.77 fof(f510,plain,(
% 10.34/1.77 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|memberP(app(X1,sK52_skl),X0)|~memberP(X1,X0))),
% 10.34/1.77 inference(resolution,[status(thm)],[f425,f271])).
% 10.34/1.77 fof(f514,plain,(
% 10.34/1.77 app(app(sK51_skl,sK47_skl),sK52_skl)=sK50_skl),
% 10.34/1.77 inference(forward_demodulation,[status(thm)],[f423,f426])).
% 10.34/1.77 fof(f515,plain,(
% 10.34/1.77 app(app(sK51_skl,sK47_skl),sK52_skl)=sK48_skl),
% 10.34/1.77 inference(forward_demodulation,[status(thm)],[f422,f514])).
% 10.34/1.77 fof(f520,definition,(
% 10.34/1.77 sQ3_spl <=> (ssList(app(sK51_skl,sK47_skl)))),
% 10.34/1.77 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 10.34/1.77 fof(f522,plain,(
% 10.34/1.77 ~ssList(app(sK51_skl,sK47_skl))|sQ3_spl),
% 10.34/1.77 inference(component_clause,[status(thm)],[f520])).
% 10.34/1.77 fof(f546,definition,(
% 10.34/1.77 sQ7_spl <=> (ssList(sK47_skl))),
% 10.34/1.77 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 10.34/1.77 fof(f548,plain,(
% 10.34/1.77 ~ssList(sK47_skl)|sQ7_spl),
% 10.34/1.77 inference(component_clause,[status(thm)],[f546])).
% 10.34/1.77 fof(f550,plain,(
% 10.34/1.77 $false|sQ7_spl),
% 10.34/1.77 inference(forward_subsumption_resolution,[status(thm)],[f548,f418])).
% 10.34/1.77 fof(f551,plain,(
% 10.34/1.77 sQ7_spl),
% 10.34/1.77 inference(contradiction_clause,[status(thm)],[f550])).
% 10.34/1.77 fof(f658,definition,(
% 10.34/1.77 sQ20_spl <=> (ssItem(sK53_skl))),
% 10.34/1.77 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 10.34/1.77 fof(f660,plain,(
% 10.34/1.77 ~ssItem(sK53_skl)|sQ20_spl),
% 10.34/1.77 inference(component_clause,[status(thm)],[f658])).
% 10.34/1.77 fof(f667,plain,(
% 10.34/1.77 $false|sQ20_spl),
% 10.34/1.77 inference(forward_subsumption_resolution,[status(thm)],[f660,f430])).
% 10.34/1.77 fof(f668,plain,(
% 10.34/1.77 sQ20_spl),
% 10.34/1.77 inference(contradiction_clause,[status(thm)],[f667])).
% 10.34/1.77 fof(f1172,plain,(
% 10.34/1.77 ![X0]: (~ssList(X0)|ssList(app(sK51_skl,X0)))),
% 10.34/1.77 inference(resolution,[status(thm)],[f424,f245])).
% 10.34/1.77 fof(f2879,plain,(
% 10.34/1.77 ~ssItem(sK53_skl)|~ssList(sK47_skl)|memberP(app(sK51_skl,sK47_skl),sK53_skl)),
% 10.34/1.77 inference(resolution,[status(thm)],[f502,f431])).
% 10.34/1.77 fof(f2944,definition,(
% 10.34/1.77 sQ399_spl <=> (memberP(app(sK51_skl,sK47_skl),sK53_skl))),
% 10.34/1.77 introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition])).
% 10.34/1.77 fof(f2945,plain,(
% 10.34/1.77 memberP(app(sK51_skl,sK47_skl),sK53_skl)|~sQ399_spl),
% 10.34/1.77 inference(component_clause,[status(thm)],[f2944])).
% 10.34/1.77 fof(f2947,plain,(
% 10.34/1.77 ~sQ20_spl|~sQ7_spl|sQ399_spl),
% 10.34/1.77 inference(split_clause,[status(thm)],[f2879,f658,f546,f2944])).
% 10.34/1.77 fof(f3938,plain,(
% 10.34/1.77 ~ssItem(sK53_skl)|~ssList(app(sK51_skl,sK47_skl))|memberP(app(app(sK51_skl,sK47_skl),sK52_skl),sK53_skl)|~sQ399_spl),
% 10.34/1.79 inference(resolution,[status(thm)],[f510,f2945])).
% 10.34/1.79 fof(f3963,definition,(
% 10.34/1.79 sQ594_spl <=> (memberP(app(app(sK51_skl,sK47_skl),sK52_skl),sK53_skl))),
% 10.34/1.79 introduced(definition,[new_symbols(definition,[sQ594_spl])],[split_symbol_definition])).
% 10.34/1.79 fof(f3964,plain,(
% 10.34/1.79 memberP(app(app(sK51_skl,sK47_skl),sK52_skl),sK53_skl)|~sQ594_spl),
% 10.34/1.79 inference(component_clause,[status(thm)],[f3963])).
% 10.34/1.79 fof(f3966,plain,(
% 10.34/1.79 ~sQ20_spl|~sQ3_spl|sQ594_spl|~sQ399_spl),
% 10.34/1.79 inference(split_clause,[status(thm)],[f3938,f658,f520,f3963,f2944])).
% 10.34/1.79 fof(f11386,plain,(
% 10.34/1.79 ssList(app(sK51_skl,sK47_skl))),
% 10.34/1.79 inference(resolution,[status(thm)],[f1172,f418])).
% 10.34/1.79 fof(f11388,plain,(
% 10.34/1.79 $false|sQ3_spl),
% 10.34/1.79 inference(forward_subsumption_resolution,[status(thm)],[f11386,f522])).
% 10.34/1.79 fof(f11389,plain,(
% 10.34/1.79 sQ3_spl),
% 10.34/1.79 inference(contradiction_clause,[status(thm)],[f11388])).
% 10.34/1.79 fof(f11392,plain,(
% 10.34/1.79 memberP(sK48_skl,sK53_skl)|~sQ594_spl),
% 10.34/1.79 inference(forward_demodulation,[status(thm)],[f515,f3964])).
% 10.34/1.79 fof(f11393,plain,(
% 10.34/1.79 $false|~sQ594_spl),
% 10.34/1.79 inference(forward_subsumption_resolution,[status(thm)],[f11392,f432])).
% 10.34/1.79 fof(f11394,plain,(
% 10.34/1.79 ~sQ594_spl),
% 10.34/1.79 inference(contradiction_clause,[status(thm)],[f11393])).
% 10.34/1.79 fof(f11395,plain,(
% 10.34/1.79 $false),
% 10.34/1.79 inference(sat_refutation,[status(thm)],[f551,f668,f2947,f3966,f11389,f11394])).
% 10.34/1.79 % SZS output end CNFRefutation for theBenchmark.p
% 10.34/1.79 % Elapsed time: 1.413428 seconds
% 10.34/1.79 % CPU time: 10.978714 seconds
% 10.34/1.79 % Total memory used: 217.733 MB
% 10.34/1.79 % Net memory used: 210.106 MB
%------------------------------------------------------------------------------