%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC419+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 : n010.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:25 PM UTC 2026
% Result : Theorem 67.70s 9.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC419+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.39 % Computer : n010.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Mon Sep 21 08:23:24 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.19/0.44 % Drodi V4.1.1
% 67.70/9.09 % Refutation found
% 67.70/9.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 67.70/9.09 % SZS output start CNFRefutation for theBenchmark
% 67.70/9.09 fof(f16,axiom,(
% 67.70/9.09 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ssList(cons(V,U)) ) )) )),
% 67.70/9.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 67.70/9.09 fof(f17,axiom,(
% 67.70/9.09 ssList(nil) ),
% 67.70/9.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 67.70/9.09 fof(f28,axiom,(
% 67.70/9.09 (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 67.70/9.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 67.70/9.09 fof(f84,axiom,(
% 67.70/9.09 (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 67.70/9.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 67.70/9.09 fof(f96,conjecture,(
% 67.70/9.09 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ~ neq(V,nil)| (? [Y] :( ssItem(Y)& (? [Z] :( ssList(Z)& (? [X1] :( ssList(X1)& app(app(Z,cons(Y,nil)),X1) = V& app(app(X1,cons(Y,nil)),Z) = U ) )) )))| ( nil != W& nil = X )| ( (! [X2] :( ssItem(X2)=> (! [X3] :( ~ ssList(X3)| app(cons(X2,nil),X3) != X| app(X3,cons(X2,nil)) != W ) )))& neq(X,nil) ) ) )) )) )) )),
% 67.70/9.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 67.70/9.09 fof(f97,negated_conjecture,(
% 67.70/9.09 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ~ neq(V,nil)| (? [Y] :( ssItem(Y)& (? [Z] :( ssList(Z)& (? [X1] :( ssList(X1)& app(app(Z,cons(Y,nil)),X1) = V& app(app(X1,cons(Y,nil)),Z) = U ) )) )))| ( nil != W& nil = X )| ( (! [X2] :( ssItem(X2)=> (! [X3] :( ~ ssList(X3)| app(cons(X2,nil),X3) != X| app(X3,cons(X2,nil)) != W ) )))& neq(X,nil) ) ) )) )) )) ))),
% 67.70/9.09 inference(negated_conjecture,[status(cth)],[f96])).
% 67.70/9.09 fof(f221,plain,(
% 67.70/9.09 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|ssList(cons(V,U)))))),
% 67.70/9.09 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 67.70/9.09 fof(f222,plain,(
% 67.70/9.09 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|ssList(cons(X1,X0)))),
% 67.70/9.09 inference(cnf_transformation,[status(thm)],[f221])).
% 67.70/9.09 fof(f223,plain,(
% 67.70/9.09 ssList(nil)),
% 67.70/9.09 inference(cnf_transformation,[status(thm)],[f17])).
% 67.70/9.09 fof(f248,plain,(
% 67.70/9.09 ![U]: (~ssList(U)|app(nil,U)=U)),
% 67.70/9.09 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 67.70/9.09 fof(f249,plain,(
% 67.70/9.09 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 67.70/9.09 inference(cnf_transformation,[status(thm)],[f248])).
% 67.70/9.09 fof(f388,plain,(
% 67.70/9.09 ![U]: (~ssList(U)|app(U,nil)=U)),
% 67.70/9.09 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 67.70/9.09 fof(f389,plain,(
% 67.70/9.09 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 67.70/9.09 inference(cnf_transformation,[status(thm)],[f388])).
% 67.70/9.09 fof(f415,plain,(
% 67.70/9.09 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: ((((((ssList(X)&V=X)&U=W)&neq(V,nil))&(![Y]: (~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((~ssList(X1)|~app(app(Z,cons(Y,nil)),X1)=V)|~app(app(X1,cons(Y,nil)),Z)=U)))))))&(nil=W|~nil=X))&((?[X2]: (ssItem(X2)&(?[X3]: ((ssList(X3)&app(cons(X2,nil),X3)=X)&app(X3,cons(X2,nil))=W))))|~neq(X,nil))))))))))),
% 67.70/9.09 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 67.70/9.09 fof(f416,plain,(
% 67.70/9.09 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&((((((ssList(sK50_skl)&sK48_skl=sK50_skl)&sK47_skl=sK49_skl)&neq(sK48_skl,nil))&(![Y]: (~ssItem(Y)|(![Z]: (~ssList(Z)|(![X1]: ((~ssList(X1)|~app(app(Z,cons(Y,nil)),X1)=sK48_skl)|~app(app(X1,cons(Y,nil)),Z)=sK47_skl)))))))&(nil=sK49_skl|~nil=sK50_skl))&((ssItem(sK51_skl)&((ssList(sK52_skl)&app(cons(sK51_skl,nil),sK52_skl)=sK50_skl)&app(sK52_skl,cons(sK51_skl,nil))=sK49_skl))|~neq(sK50_skl,nil))))))),
% 67.70/9.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(X2,sK51_skl),skolemize(X3,sK52_skl)],[f415])).
% 67.70/9.09 fof(f417,plain,(
% 67.70/9.09 ssList(sK47_skl)),
% 67.70/9.09 inference(cnf_transformation,[status(thm)],[f416])).
% 67.70/9.09 fof(f421,plain,(
% 67.70/9.09 sK48_skl=sK50_skl),
% 67.70/9.09 inference(cnf_transformation,[status(thm)],[f416])).
% 67.70/9.09 fof(f422,plain,(
% 67.70/9.09 sK47_skl=sK49_skl),
% 67.70/9.09 inference(cnf_transformation,[status(thm)],[f416])).
% 67.70/9.09 fof(f423,plain,(
% 67.70/9.09 neq(sK48_skl,nil)),
% 67.70/9.09 inference(cnf_transformation,[status(thm)],[f416])).
% 67.70/9.09 fof(f424,plain,(
% 67.70/9.09 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sK48_skl|~app(app(X2,cons(X0,nil)),X1)=sK47_skl)),
% 67.70/9.11 inference(cnf_transformation,[status(thm)],[f416])).
% 67.70/9.11 fof(f426,plain,(
% 67.70/9.11 ssItem(sK51_skl)|~neq(sK50_skl,nil)),
% 67.70/9.11 inference(cnf_transformation,[status(thm)],[f416])).
% 67.70/9.11 fof(f427,plain,(
% 67.70/9.11 ssList(sK52_skl)|~neq(sK50_skl,nil)),
% 67.70/9.11 inference(cnf_transformation,[status(thm)],[f416])).
% 67.70/9.11 fof(f428,plain,(
% 67.70/9.11 app(cons(sK51_skl,nil),sK52_skl)=sK50_skl|~neq(sK50_skl,nil)),
% 67.70/9.11 inference(cnf_transformation,[status(thm)],[f416])).
% 67.70/9.11 fof(f429,plain,(
% 67.70/9.11 app(sK52_skl,cons(sK51_skl,nil))=sK49_skl|~neq(sK50_skl,nil)),
% 67.70/9.11 inference(cnf_transformation,[status(thm)],[f416])).
% 67.70/9.11 fof(f437,definition,(
% 67.70/9.11 sQ2_spl <=> (ssItem(sK51_skl))),
% 67.70/9.11 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 67.70/9.11 fof(f438,plain,(
% 67.70/9.11 ssItem(sK51_skl)|~sQ2_spl),
% 67.70/9.11 inference(component_clause,[status(thm)],[f437])).
% 67.70/9.11 fof(f440,definition,(
% 67.70/9.11 sQ3_spl <=> (neq(sK50_skl,nil))),
% 67.70/9.11 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 67.70/9.11 fof(f442,plain,(
% 67.70/9.11 ~neq(sK50_skl,nil)|sQ3_spl),
% 67.70/9.11 inference(component_clause,[status(thm)],[f440])).
% 67.70/9.11 fof(f443,plain,(
% 67.70/9.11 sQ2_spl|~sQ3_spl),
% 67.70/9.11 inference(split_clause,[status(thm)],[f426,f437,f440])).
% 67.70/9.11 fof(f444,definition,(
% 67.70/9.11 sQ4_spl <=> (ssList(sK52_skl))),
% 67.70/9.11 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 67.70/9.11 fof(f447,plain,(
% 67.70/9.11 sQ4_spl|~sQ3_spl),
% 67.70/9.11 inference(split_clause,[status(thm)],[f427,f444,f440])).
% 67.70/9.11 fof(f448,definition,(
% 67.70/9.11 sQ5_spl <=> (app(cons(sK51_skl,nil),sK52_skl)=sK50_skl)),
% 67.70/9.11 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 67.70/9.11 fof(f449,plain,(
% 67.70/9.11 app(cons(sK51_skl,nil),sK52_skl)=sK50_skl|~sQ5_spl),
% 67.70/9.11 inference(component_clause,[status(thm)],[f448])).
% 67.70/9.11 fof(f451,plain,(
% 67.70/9.11 sQ5_spl|~sQ3_spl),
% 67.70/9.11 inference(split_clause,[status(thm)],[f428,f448,f440])).
% 67.70/9.11 fof(f452,definition,(
% 67.70/9.11 sQ6_spl <=> (app(sK52_skl,cons(sK51_skl,nil))=sK49_skl)),
% 67.70/9.11 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 67.70/9.11 fof(f453,plain,(
% 67.70/9.11 app(sK52_skl,cons(sK51_skl,nil))=sK49_skl|~sQ6_spl),
% 67.70/9.11 inference(component_clause,[status(thm)],[f452])).
% 67.70/9.11 fof(f455,plain,(
% 67.70/9.11 sQ6_spl|~sQ3_spl),
% 67.70/9.11 inference(split_clause,[status(thm)],[f429,f452,f440])).
% 67.70/9.11 fof(f490,plain,(
% 67.70/9.11 ~neq(sK48_skl,nil)|sQ3_spl),
% 67.70/9.11 inference(forward_demodulation,[status(thm)],[f421,f442])).
% 67.70/9.11 fof(f491,plain,(
% 67.70/9.11 $false|sQ3_spl),
% 67.70/9.11 inference(forward_subsumption_resolution,[status(thm)],[f490,f423])).
% 67.70/9.11 fof(f492,plain,(
% 67.70/9.11 sQ3_spl),
% 67.70/9.11 inference(contradiction_clause,[status(thm)],[f491])).
% 67.70/9.11 fof(f494,plain,(
% 67.70/9.11 app(cons(sK51_skl,nil),sK52_skl)=sK48_skl|~sQ5_spl),
% 67.70/9.11 inference(forward_demodulation,[status(thm)],[f421,f449])).
% 67.70/9.11 fof(f537,plain,(
% 67.70/9.11 ![X0]: (~ssItem(X0)|ssList(cons(X0,nil)))),
% 67.70/9.11 inference(resolution,[status(thm)],[f222,f223])).
% 67.70/9.11 fof(f553,plain,(
% 67.70/9.11 app(sK52_skl,cons(sK51_skl,nil))=sK47_skl|~sQ6_spl),
% 67.70/9.11 inference(forward_demodulation,[status(thm)],[f422,f453])).
% 67.70/9.11 fof(f557,plain,(
% 67.70/9.11 app(sK47_skl,nil)=sK47_skl),
% 67.70/9.11 inference(resolution,[status(thm)],[f417,f389])).
% 67.70/9.11 fof(f664,plain,(
% 67.70/9.11 ![X0]: (~ssItem(sK51_skl)|~ssList(X0)|~ssList(sK52_skl)|~app(app(X0,cons(sK51_skl,nil)),sK52_skl)=sK48_skl|~app(sK47_skl,X0)=sK47_skl|~sQ6_spl)),
% 67.70/9.11 inference(paramodulation,[status(thm)],[f553,f424])).
% 67.70/9.11 fof(f666,definition,(
% 67.70/9.11 ![X0]: (sQ18_spl <=> (~ssList(X0)|~app(app(X0,cons(sK51_skl,nil)),sK52_skl)=sK48_skl|~app(sK47_skl,X0)=sK47_skl))),
% 67.70/9.11 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 67.70/9.11 fof(f667,plain,(
% 67.70/9.11 ![X0]: (~ssList(X0)|~app(app(X0,cons(sK51_skl,nil)),sK52_skl)=sK48_skl|~app(sK47_skl,X0)=sK47_skl|~sQ18_spl)),
% 67.70/9.11 inference(component_clause,[status(thm)],[f666])).
% 67.70/9.11 fof(f669,plain,(
% 67.70/9.11 ~sQ2_spl|sQ18_spl|~sQ4_spl|~sQ6_spl),
% 67.70/9.11 inference(split_clause,[status(thm)],[f664,f437,f666,f444,f452])).
% 67.70/9.11 fof(f678,plain,(
% 67.70/9.11 ssList(cons(sK51_skl,nil))|~sQ2_spl),
% 67.70/9.11 inference(resolution,[status(thm)],[f537,f438])).
% 67.70/9.11 fof(f693,plain,(
% 67.70/9.11 app(nil,cons(sK51_skl,nil))=cons(sK51_skl,nil)|~sQ2_spl),
% 67.70/9.11 inference(resolution,[status(thm)],[f678,f249])).
% 67.70/9.11 fof(f2676,plain,(
% 67.70/9.11 ~app(app(nil,cons(sK51_skl,nil)),sK52_skl)=sK48_skl|~app(sK47_skl,nil)=sK47_skl|~sQ18_spl),
% 67.70/9.15 inference(resolution,[status(thm)],[f667,f223])).
% 67.70/9.15 fof(f2790,definition,(
% 67.70/9.15 sQ263_spl <=> (app(app(nil,cons(sK51_skl,nil)),sK52_skl)=sK48_skl)),
% 67.70/9.15 introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition])).
% 67.70/9.15 fof(f2792,plain,(
% 67.70/9.15 ~app(app(nil,cons(sK51_skl,nil)),sK52_skl)=sK48_skl|sQ263_spl),
% 67.70/9.15 inference(component_clause,[status(thm)],[f2790])).
% 67.70/9.15 fof(f2793,definition,(
% 67.70/9.15 sQ264_spl <=> (app(sK47_skl,nil)=sK47_skl)),
% 67.70/9.15 introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition])).
% 67.70/9.15 fof(f2795,plain,(
% 67.70/9.15 ~app(sK47_skl,nil)=sK47_skl|sQ264_spl),
% 67.70/9.15 inference(component_clause,[status(thm)],[f2793])).
% 67.70/9.15 fof(f2796,plain,(
% 67.70/9.15 ~sQ263_spl|~sQ264_spl|~sQ18_spl),
% 67.70/9.15 inference(split_clause,[status(thm)],[f2676,f2790,f2793,f666])).
% 67.70/9.15 fof(f2805,plain,(
% 67.70/9.15 ~app(cons(sK51_skl,nil),sK52_skl)=sK48_skl|~sQ2_spl|sQ263_spl),
% 67.70/9.15 inference(forward_demodulation,[status(thm)],[f693,f2792])).
% 67.70/9.15 fof(f2806,plain,(
% 67.70/9.15 ~sK48_skl=sK48_skl|~sQ5_spl|~sQ2_spl|sQ263_spl),
% 67.70/9.15 inference(forward_demodulation,[status(thm)],[f494,f2805])).
% 67.70/9.15 fof(f2807,plain,(
% 67.70/9.15 $false|~sQ5_spl|~sQ2_spl|sQ263_spl),
% 67.70/9.15 inference(trivial_equality_resolution,[status(thm)],[f2806])).
% 67.70/9.15 fof(f2808,plain,(
% 67.70/9.15 ~sQ5_spl|~sQ2_spl|sQ263_spl),
% 67.70/9.15 inference(contradiction_clause,[status(thm)],[f2807])).
% 67.70/9.15 fof(f2809,plain,(
% 67.70/9.15 ~sK47_skl=sK47_skl|sQ264_spl),
% 67.70/9.15 inference(forward_demodulation,[status(thm)],[f557,f2795])).
% 67.70/9.15 fof(f2810,plain,(
% 67.70/9.15 $false|sQ264_spl),
% 67.70/9.15 inference(trivial_equality_resolution,[status(thm)],[f2809])).
% 67.70/9.15 fof(f2811,plain,(
% 67.70/9.15 sQ264_spl),
% 67.70/9.15 inference(contradiction_clause,[status(thm)],[f2810])).
% 67.70/9.15 fof(f2812,plain,(
% 67.70/9.15 $false),
% 67.70/9.15 inference(sat_refutation,[status(thm)],[f443,f447,f451,f455,f492,f669,f2796,f2808,f2811])).
% 67.70/9.15 % SZS output end CNFRefutation for theBenchmark.p
% 39.35/9.19 % Elapsed time: 8.769439 seconds
% 39.35/9.19 % CPU time: 68.669229 seconds
% 39.35/9.19 % Total memory used: 392.746 MB
% 39.35/9.19 % Net memory used: 373.131 MB
%------------------------------------------------------------------------------