%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC404+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:23 PM UTC 2026
% Result : Theorem 9.76s 6.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC404+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.53 % Computer : n015.cluster.edu
% 0.08/5.53 % Model : x86_64 x86_64
% 0.08/5.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.53 % Memory : 8046.5625MB
% 0.08/5.53 % OS : Linux 6.8.0-71-generic
% 0.08/5.53 % CPULimit : 300
% 0.08/5.53 % WCLimit : 300
% 0.08/5.53 % DateTime : Mon Sep 21 08:25:12 UTC 2026
% 0.08/5.53 % CPUTime :
% 0.08/5.55 % Drodi V4.1.1
% 9.76/6.88 % Refutation found
% 9.76/6.88 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.76/6.88 % SZS output start CNFRefutation for theBenchmark
% 9.76/6.88 fof(f26,axiom,(
% 9.76/6.88 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ssList(app(U,V)) ) )) )),
% 9.76/6.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.76/6.88 fof(f36,axiom,(
% 9.76/6.88 (! [U] :( ssItem(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( memberP(app(V,W),U)<=> ( memberP(V,U)| memberP(W,U) ) ) ) )) )) )),
% 9.76/6.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.76/6.88 fof(f96,conjecture,(
% 9.76/6.88 (! [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| ~ strictorderedP(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& lt(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& lt(X7,X5) ) )) )) )) )) ) )))| (! [X9] :( ssItem(X9)=> ( ~ memberP(U,X9)| memberP(V,X9) ) ))| ( nil != X& nil = W ) ) ) )) )) )) )),
% 9.76/6.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.76/6.88 fof(f97,negated_conjecture,(
% 9.76/6.88 ~((! [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| ~ strictorderedP(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& lt(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& lt(X7,X5) ) )) )) )) )) ) )))| (! [X9] :( ssItem(X9)=> ( ~ memberP(U,X9)| memberP(V,X9) ) ))| ( nil != X& nil = W ) ) ) )) )) )) ))),
% 9.76/6.88 inference(negated_conjecture,[status(cth)],[f96])).
% 9.76/6.88 fof(f244,plain,(
% 9.76/6.88 ![U]: (~ssList(U)|(![V]: (~ssList(V)|ssList(app(U,V)))))),
% 9.76/6.88 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 9.76/6.88 fof(f245,plain,(
% 9.76/6.88 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X0,X1)))),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f244])).
% 9.76/6.88 fof(f268,plain,(
% 9.76/6.88 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(memberP(app(V,W),U)<=>(memberP(V,U)|memberP(W,U))))))))),
% 9.76/6.88 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 9.76/6.88 fof(f269,plain,(
% 9.76/6.88 ![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)))))))))),
% 9.76/6.88 inference(NNF_transformation,[status(thm)],[f268])).
% 9.76/6.88 fof(f271,plain,(
% 9.76/6.88 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X1,X0))),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f269])).
% 9.76/6.88 fof(f272,plain,(
% 9.76/6.88 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X2,X0))),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f269])).
% 9.76/6.88 fof(f415,plain,(
% 9.76/6.88 (?[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&strictorderedP(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)|~lt(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)|~lt(X7,X5)))))))))))))))&(?[X9]: (ssItem(X9)&(memberP(U,X9)&~memberP(V,X9)))))&(nil=X|~nil=W))))))))))),
% 9.76/6.88 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 9.76/6.88 fof(f416,plain,(
% 9.76/6.88 ?[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&strictorderedP(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))|~lt(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))|~lt(X7,X5)))))))))))))&(?[X9]: (ssItem(X9)&(memberP(U,X9)&~memberP(V,X9)))))&(nil=X|~nil=W)))))))))),
% 9.76/6.88 inference(miniscoping,[status(thm)],[f415])).
% 9.76/6.88 fof(f417,plain,(
% 9.76/6.88 (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&strictorderedP(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))|~lt(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))|~lt(X7,X5)))))))))))&(ssItem(sK53_skl)&(memberP(sK47_skl,sK53_skl)&~memberP(sK48_skl,sK53_skl))))&(nil=sK50_skl|~nil=sK49_skl))))))),
% 9.76/6.88 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])).
% 9.76/6.88 fof(f418,plain,(
% 9.76/6.88 ssList(sK47_skl)),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f417])).
% 9.76/6.88 fof(f422,plain,(
% 9.76/6.88 sK48_skl=sK50_skl),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f417])).
% 9.76/6.88 fof(f423,plain,(
% 9.76/6.88 sK47_skl=sK49_skl),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f417])).
% 9.76/6.88 fof(f424,plain,(
% 9.76/6.88 ssList(sK51_skl)),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f417])).
% 9.76/6.88 fof(f425,plain,(
% 9.76/6.88 ssList(sK52_skl)),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f417])).
% 9.76/6.88 fof(f426,plain,(
% 9.76/6.88 app(app(sK51_skl,sK49_skl),sK52_skl)=sK50_skl),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f417])).
% 9.76/6.88 fof(f430,plain,(
% 9.76/6.88 ssItem(sK53_skl)),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f417])).
% 9.76/6.88 fof(f431,plain,(
% 9.76/6.88 memberP(sK47_skl,sK53_skl)),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f417])).
% 9.76/6.88 fof(f432,plain,(
% 9.76/6.88 ~memberP(sK48_skl,sK53_skl)),
% 9.76/6.88 inference(cnf_transformation,[status(thm)],[f417])).
% 9.76/6.88 fof(f502,plain,(
% 9.76/6.88 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|memberP(app(sK51_skl,X1),X0)|~memberP(X1,X0))),
% 9.76/6.88 inference(resolution,[status(thm)],[f424,f272])).
% 9.76/6.88 fof(f512,plain,(
% 9.76/6.88 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|memberP(app(X1,sK52_skl),X0)|~memberP(X1,X0))),
% 9.76/6.88 inference(resolution,[status(thm)],[f425,f271])).
% 9.76/6.88 fof(f516,plain,(
% 9.76/6.88 app(app(sK51_skl,sK47_skl),sK52_skl)=sK50_skl),
% 9.76/6.88 inference(forward_demodulation,[status(thm)],[f423,f426])).
% 9.76/6.88 fof(f517,plain,(
% 9.76/6.88 app(app(sK51_skl,sK47_skl),sK52_skl)=sK48_skl),
% 9.76/6.88 inference(forward_demodulation,[status(thm)],[f422,f516])).
% 9.76/6.88 fof(f522,definition,(
% 9.76/6.88 sQ3_spl <=> (ssList(app(sK51_skl,sK47_skl)))),
% 9.76/6.88 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 9.76/6.88 fof(f524,plain,(
% 9.76/6.88 ~ssList(app(sK51_skl,sK47_skl))|sQ3_spl),
% 9.76/6.88 inference(component_clause,[status(thm)],[f522])).
% 9.76/6.88 fof(f547,definition,(
% 9.76/6.88 sQ7_spl <=> (ssList(sK47_skl))),
% 9.76/6.88 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 9.76/6.88 fof(f549,plain,(
% 9.76/6.88 ~ssList(sK47_skl)|sQ7_spl),
% 9.76/6.88 inference(component_clause,[status(thm)],[f547])).
% 9.76/6.88 fof(f551,plain,(
% 9.76/6.88 $false|sQ7_spl),
% 9.76/6.88 inference(forward_subsumption_resolution,[status(thm)],[f549,f418])).
% 9.76/6.88 fof(f552,plain,(
% 9.76/6.88 sQ7_spl),
% 9.76/6.88 inference(contradiction_clause,[status(thm)],[f551])).
% 9.76/6.88 fof(f625,definition,(
% 9.76/6.88 sQ15_spl <=> (ssItem(sK53_skl))),
% 9.76/6.88 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 9.76/6.88 fof(f627,plain,(
% 9.76/6.88 ~ssItem(sK53_skl)|sQ15_spl),
% 9.76/6.88 inference(component_clause,[status(thm)],[f625])).
% 9.76/6.88 fof(f632,plain,(
% 9.76/6.88 $false|sQ15_spl),
% 9.76/6.88 inference(forward_subsumption_resolution,[status(thm)],[f627,f430])).
% 9.76/6.88 fof(f633,plain,(
% 9.76/6.88 sQ15_spl),
% 9.76/6.88 inference(contradiction_clause,[status(thm)],[f632])).
% 9.76/6.88 fof(f1307,plain,(
% 9.76/6.88 ![X0]: (~ssList(X0)|ssList(app(sK51_skl,X0)))),
% 9.76/6.88 inference(resolution,[status(thm)],[f245,f424])).
% 9.76/6.88 fof(f3384,plain,(
% 9.76/6.88 ~ssItem(sK53_skl)|~ssList(sK47_skl)|memberP(app(sK51_skl,sK47_skl),sK53_skl)),
% 9.76/6.88 inference(resolution,[status(thm)],[f502,f431])).
% 9.76/6.88 fof(f3457,definition,(
% 9.76/6.88 sQ507_spl <=> (memberP(app(sK51_skl,sK47_skl),sK53_skl))),
% 9.76/6.88 introduced(definition,[new_symbols(definition,[sQ507_spl])],[split_symbol_definition])).
% 1.77/6.90 fof(f3458,plain,(
% 1.77/6.90 memberP(app(sK51_skl,sK47_skl),sK53_skl)|~sQ507_spl),
% 1.77/6.90 inference(component_clause,[status(thm)],[f3457])).
% 1.77/6.90 fof(f3460,plain,(
% 1.77/6.90 ~sQ15_spl|~sQ7_spl|sQ507_spl),
% 1.77/6.90 inference(split_clause,[status(thm)],[f3384,f625,f547,f3457])).
% 1.77/6.90 fof(f3791,plain,(
% 1.77/6.90 ~ssItem(sK53_skl)|~ssList(app(sK51_skl,sK47_skl))|memberP(app(app(sK51_skl,sK47_skl),sK52_skl),sK53_skl)|~sQ507_spl),
% 1.77/6.90 inference(resolution,[status(thm)],[f512,f3458])).
% 1.77/6.90 fof(f3816,definition,(
% 1.77/6.90 sQ573_spl <=> (memberP(app(app(sK51_skl,sK47_skl),sK52_skl),sK53_skl))),
% 1.77/6.90 introduced(definition,[new_symbols(definition,[sQ573_spl])],[split_symbol_definition])).
% 1.77/6.90 fof(f3817,plain,(
% 1.77/6.90 memberP(app(app(sK51_skl,sK47_skl),sK52_skl),sK53_skl)|~sQ573_spl),
% 1.77/6.90 inference(component_clause,[status(thm)],[f3816])).
% 1.77/6.90 fof(f3819,plain,(
% 1.77/6.90 ~sQ15_spl|~sQ3_spl|sQ573_spl|~sQ507_spl),
% 1.77/6.90 inference(split_clause,[status(thm)],[f3791,f625,f522,f3816,f3457])).
% 1.77/6.90 fof(f11616,plain,(
% 1.77/6.90 ssList(app(sK51_skl,sK47_skl))),
% 1.77/6.90 inference(resolution,[status(thm)],[f1307,f418])).
% 1.77/6.90 fof(f11618,plain,(
% 1.77/6.90 $false|sQ3_spl),
% 1.77/6.90 inference(forward_subsumption_resolution,[status(thm)],[f11616,f524])).
% 1.77/6.90 fof(f11619,plain,(
% 1.77/6.90 sQ3_spl),
% 1.77/6.90 inference(contradiction_clause,[status(thm)],[f11618])).
% 1.77/6.90 fof(f11622,plain,(
% 1.77/6.90 memberP(sK48_skl,sK53_skl)|~sQ573_spl),
% 1.77/6.90 inference(forward_demodulation,[status(thm)],[f517,f3817])).
% 1.77/6.90 fof(f11623,plain,(
% 1.77/6.90 $false|~sQ573_spl),
% 1.77/6.90 inference(forward_subsumption_resolution,[status(thm)],[f11622,f432])).
% 1.77/6.90 fof(f11624,plain,(
% 1.77/6.90 ~sQ573_spl),
% 1.77/6.90 inference(contradiction_clause,[status(thm)],[f11623])).
% 1.77/6.90 fof(f11625,plain,(
% 1.77/6.90 $false),
% 1.77/6.90 inference(sat_refutation,[status(thm)],[f552,f633,f3460,f3819,f11619,f11624])).
% 1.77/6.90 % SZS output end CNFRefutation for theBenchmark.p
% 1.77/6.92 % Elapsed time: 1.368118 seconds
% 1.77/6.92 % CPU time: 10.617027 seconds
% 1.77/6.92 % Total memory used: 225.048 MB
% 1.77/6.92 % Net memory used: 217.447 MB
%------------------------------------------------------------------------------