%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC308+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 : n016.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:07 PM UTC 2026
% Result : Theorem 48.47s 6.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC308+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.09/0.35 % Computer : n016.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 08:18:52 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 48.47/6.61 % Refutation found
% 48.47/6.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 48.47/6.61 % SZS output start CNFRefutation for theBenchmark
% 48.47/6.61 fof(f15,axiom,(
% 48.47/6.61 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( neq(U,V)<=> U != V ) ) )) )),
% 48.47/6.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.61 fof(f16,axiom,(
% 48.47/6.61 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ssList(cons(V,U)) ) )) )),
% 48.47/6.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.61 fof(f17,axiom,(
% 48.47/6.61 ssList(nil) ),
% 48.47/6.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.61 fof(f22,axiom,(
% 48.47/6.61 (! [U] :( ssList(U)=> ( nil != U=> ssItem(hd(U)) ) ) )),
% 48.47/6.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.61 fof(f24,axiom,(
% 48.47/6.61 (! [U] :( ssList(U)=> ( nil != U=> ssList(tl(U)) ) ) )),
% 48.47/6.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.61 fof(f78,axiom,(
% 48.47/6.61 (! [U] :( ssList(U)=> ( nil != U=> cons(hd(U),tl(U)) = U ) ) )),
% 48.47/6.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.61 fof(f81,axiom,(
% 48.47/6.61 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> cons(V,U) = app(cons(V,nil),U) ) )) )),
% 48.47/6.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.61 fof(f96,conjecture,(
% 48.47/6.61 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| ~ neq(V,nil)| (? [Y] :( ssList(Y)& U = Y& (? [Z] :( ssList(Z)& (? [X1] :( ssList(X1)& tl(V) = Z& app(Z,X1) = Y& (? [X2] :( ssItem(X2)& cons(X2,nil) = X1& hd(V) = X2& neq(nil,V) ))& neq(nil,V) ) )) )))| (? [X3] :( ssItem(X3)& (? [X4] :( ssList(X4)& app(X4,cons(X3,nil)) != W& app(cons(X3,nil),X4) = X ) )))| ( nil != W& nil = X ) ) ) )) )) )) )),
% 48.47/6.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.61 fof(f97,negated_conjecture,(
% 48.47/6.61 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| ~ neq(V,nil)| (? [Y] :( ssList(Y)& U = Y& (? [Z] :( ssList(Z)& (? [X1] :( ssList(X1)& tl(V) = Z& app(Z,X1) = Y& (? [X2] :( ssItem(X2)& cons(X2,nil) = X1& hd(V) = X2& neq(nil,V) ))& neq(nil,V) ) )) )))| (? [X3] :( ssItem(X3)& (? [X4] :( ssList(X4)& app(X4,cons(X3,nil)) != W& app(cons(X3,nil),X4) = X ) )))| ( nil != W& nil = X ) ) ) )) )) )) ))),
% 48.47/6.61 inference(negated_conjecture,[status(cth)],[f96])).
% 48.47/6.61 fof(f217,plain,(
% 48.47/6.61 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(neq(U,V)<=>~U=V))))),
% 48.47/6.61 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 48.47/6.61 fof(f218,plain,(
% 48.47/6.61 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~neq(U,V)|~U=V)&(neq(U,V)|U=V)))))),
% 48.47/6.61 inference(NNF_transformation,[status(thm)],[f217])).
% 48.47/6.61 fof(f219,plain,(
% 48.47/6.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~neq(X0,X1)|~X0=X1)),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f218])).
% 48.47/6.61 fof(f220,plain,(
% 48.47/6.61 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X0,X1)|X0=X1)),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f218])).
% 48.47/6.61 fof(f221,plain,(
% 48.47/6.61 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|ssList(cons(V,U)))))),
% 48.47/6.61 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 48.47/6.61 fof(f222,plain,(
% 48.47/6.61 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|ssList(cons(X1,X0)))),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f221])).
% 48.47/6.61 fof(f223,plain,(
% 48.47/6.61 ssList(nil)),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f17])).
% 48.47/6.61 fof(f236,plain,(
% 48.47/6.61 ![U]: (~ssList(U)|(nil=U|ssItem(hd(U))))),
% 48.47/6.61 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 48.47/6.61 fof(f237,plain,(
% 48.47/6.61 ![X0]: (~ssList(X0)|nil=X0|ssItem(hd(X0)))),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f236])).
% 48.47/6.61 fof(f240,plain,(
% 48.47/6.61 ![U]: (~ssList(U)|(nil=U|ssList(tl(U))))),
% 48.47/6.61 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 48.47/6.61 fof(f241,plain,(
% 48.47/6.61 ![X0]: (~ssList(X0)|nil=X0|ssList(tl(X0)))),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f240])).
% 48.47/6.61 fof(f373,plain,(
% 48.47/6.61 ![U]: (~ssList(U)|(nil=U|cons(hd(U),tl(U))=U))),
% 48.47/6.61 inference(pre_NNF_transformation,[status(thm)],[f78])).
% 48.47/6.61 fof(f374,plain,(
% 48.47/6.61 ![X0]: (~ssList(X0)|nil=X0|cons(hd(X0),tl(X0))=X0)),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f373])).
% 48.47/6.61 fof(f379,plain,(
% 48.47/6.61 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|cons(V,U)=app(cons(V,nil),U))))),
% 48.47/6.61 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 48.47/6.61 fof(f380,plain,(
% 48.47/6.61 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|cons(X1,X0)=app(cons(X1,nil),X0))),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f379])).
% 48.47/6.61 fof(f415,plain,(
% 48.47/6.61 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((((V=X&U=W)&neq(V,nil))&(![Y]: ((~ssList(Y)|~U=Y)|(![Z]: (~ssList(Z)|(![X1]: ((((~ssList(X1)|~tl(V)=Z)|~app(Z,X1)=Y)|(![X2]: (((~ssItem(X2)|~cons(X2,nil)=X1)|~hd(V)=X2)|~neq(nil,V))))|~neq(nil,V))))))))&(![X3]: (~ssItem(X3)|(![X4]: ((~ssList(X4)|app(X4,cons(X3,nil))=W)|~app(cons(X3,nil),X4)=X)))))&(nil=W|~nil=X))))))))))),
% 48.47/6.61 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 48.47/6.61 fof(f416,plain,(
% 48.47/6.61 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((((V=X&U=W)&neq(V,nil))&(![Y]: ((~ssList(Y)|~U=Y)|(![Z]: (~ssList(Z)|((![X1]: (((~ssList(X1)|~tl(V)=Z)|~app(Z,X1)=Y)|((![X2]: ((~ssItem(X2)|~cons(X2,nil)=X1)|~hd(V)=X2))|~neq(nil,V))))|~neq(nil,V)))))))&(![X3]: (~ssItem(X3)|(![X4]: ((~ssList(X4)|app(X4,cons(X3,nil))=W)|~app(cons(X3,nil),X4)=X)))))&(nil=W|~nil=X)))))))))),
% 48.47/6.61 inference(miniscoping,[status(thm)],[f415])).
% 48.47/6.61 fof(f417,plain,(
% 48.47/6.61 (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]: ((~ssList(Y)|~sK47_skl=Y)|(![Z]: (~ssList(Z)|((![X1]: (((~ssList(X1)|~tl(sK48_skl)=Z)|~app(Z,X1)=Y)|((![X2]: ((~ssItem(X2)|~cons(X2,nil)=X1)|~hd(sK48_skl)=X2))|~neq(nil,sK48_skl))))|~neq(nil,sK48_skl)))))))&(![X3]: (~ssItem(X3)|(![X4]: ((~ssList(X4)|app(X4,cons(X3,nil))=sK49_skl)|~app(cons(X3,nil),X4)=sK50_skl)))))&(nil=sK49_skl|~nil=sK50_skl))))))),
% 48.47/6.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl)],[f416])).
% 48.47/6.61 fof(f418,plain,(
% 48.47/6.61 ssList(sK47_skl)),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f417])).
% 48.47/6.61 fof(f419,plain,(
% 48.47/6.61 ssList(sK48_skl)),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f417])).
% 48.47/6.61 fof(f422,plain,(
% 48.47/6.61 sK48_skl=sK50_skl),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f417])).
% 48.47/6.61 fof(f423,plain,(
% 48.47/6.61 sK47_skl=sK49_skl),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f417])).
% 48.47/6.61 fof(f424,plain,(
% 48.47/6.61 neq(sK48_skl,nil)),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f417])).
% 48.47/6.61 fof(f425,plain,(
% 48.47/6.61 ![X0,X1,X2,X3]: (~ssList(X0)|~sK47_skl=X0|~ssList(X1)|~ssList(X2)|~tl(sK48_skl)=X1|~app(X1,X2)=X0|~ssItem(X3)|~cons(X3,nil)=X2|~hd(sK48_skl)=X3|~neq(nil,sK48_skl)|~neq(nil,sK48_skl))),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f417])).
% 48.47/6.61 fof(f426,plain,(
% 48.47/6.61 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(X1,cons(X0,nil))=sK49_skl|~app(cons(X0,nil),X1)=sK50_skl)),
% 48.47/6.61 inference(cnf_transformation,[status(thm)],[f417])).
% 48.47/6.61 fof(f428,definition,(
% 48.47/6.61 ![X0,X1,X2,X3]: (sQ0_spl <=> (~ssList(X0)|~sK47_skl=X0|~ssList(X1)|~ssList(X2)|~tl(sK48_skl)=X1|~app(X1,X2)=X0|~ssItem(X3)|~cons(X3,nil)=X2|~hd(sK48_skl)=X3))),
% 48.47/6.61 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 48.47/6.61 fof(f429,plain,(
% 48.47/6.61 ![X0,X1,X2,X3]: (~ssList(X0)|~sK47_skl=X0|~ssList(X1)|~ssList(X2)|~tl(sK48_skl)=X1|~app(X1,X2)=X0|~ssItem(X3)|~cons(X3,nil)=X2|~hd(sK48_skl)=X3|~sQ0_spl)),
% 48.47/6.61 inference(component_clause,[status(thm)],[f428])).
% 48.47/6.61 fof(f431,definition,(
% 48.47/6.61 sQ1_spl <=> (neq(nil,sK48_skl))),
% 48.47/6.61 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 48.47/6.61 fof(f434,plain,(
% 48.47/6.61 sQ0_spl|~sQ1_spl),
% 48.47/6.61 inference(split_clause,[status(thm)],[f425,f428,f431])).
% 48.47/6.61 fof(f457,plain,(
% 48.47/6.61 ![X1]: (~ssList(X1)|~ssList(X1)|~neq(X1,X1))),
% 48.47/6.61 inference(destructive_equality_resolution,[status(thm)],[f219])).
% 48.47/6.61 fof(f458,plain,(
% 48.47/6.61 ![X0]: (~ssList(X0)|~neq(X0,X0))),
% 48.47/6.61 inference(duplicate_literals_removal,[status(thm)],[f457])).
% 48.47/6.61 fof(f472,plain,(
% 48.47/6.61 ~ssList(sK47_skl)|~ssList(tl(sK48_skl))|~ssList(cons(hd(sK48_skl),nil))|~app(tl(sK48_skl),cons(hd(sK48_skl),nil))=sK47_skl|~ssItem(hd(sK48_skl))|~sQ0_spl),
% 48.47/6.61 inference(destructive_equality_resolution,[status(thm)],[f429])).
% 48.47/6.61 fof(f495,plain,(
% 48.47/6.61 nil=sK48_skl|cons(hd(sK48_skl),tl(sK48_skl))=sK48_skl),
% 48.47/6.61 inference(resolution,[status(thm)],[f374,f419])).
% 48.47/6.61 fof(f501,definition,(
% 48.47/6.61 sQ5_spl <=> (nil=sK48_skl)),
% 48.47/6.61 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 48.47/6.61 fof(f502,plain,(
% 48.47/6.61 nil=sK48_skl|~sQ5_spl),
% 48.47/6.61 inference(component_clause,[status(thm)],[f501])).
% 48.47/6.61 fof(f504,definition,(
% 48.47/6.61 sQ6_spl <=> (cons(hd(sK48_skl),tl(sK48_skl))=sK48_skl)),
% 48.47/6.61 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 48.47/6.61 fof(f505,plain,(
% 48.47/6.61 cons(hd(sK48_skl),tl(sK48_skl))=sK48_skl|~sQ6_spl),
% 48.47/6.61 inference(component_clause,[status(thm)],[f504])).
% 48.47/6.61 fof(f507,plain,(
% 48.47/6.61 sQ5_spl|sQ6_spl),
% 48.47/6.61 inference(split_clause,[status(thm)],[f495,f501,f504])).
% 48.47/6.61 fof(f558,plain,(
% 48.47/6.61 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(X1,cons(X0,nil))=sK49_skl|~app(cons(X0,nil),X1)=sK48_skl)),
% 48.47/6.61 inference(forward_demodulation,[status(thm)],[f422,f426])).
% 48.47/6.61 fof(f595,plain,(
% 48.47/6.61 ![X0]: (~ssList(X0)|neq(nil,X0)|nil=X0)),
% 48.47/6.61 inference(resolution,[status(thm)],[f223,f220])).
% 48.47/6.61 fof(f600,plain,(
% 48.47/6.61 ![X0]: (~ssItem(X0)|ssList(cons(X0,nil)))),
% 48.47/6.61 inference(resolution,[status(thm)],[f223,f222])).
% 48.47/6.61 fof(f668,plain,(
% 48.47/6.61 neq(nil,nil)|~sQ5_spl),
% 48.47/6.61 inference(backward_demodulation,[status(thm)],[f502,f424])).
% 48.47/6.61 fof(f725,definition,(
% 48.47/6.61 sQ32_spl <=> (ssList(nil))),
% 48.47/6.61 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 48.47/6.61 fof(f727,plain,(
% 48.47/6.61 ~ssList(nil)|sQ32_spl),
% 48.47/6.61 inference(component_clause,[status(thm)],[f725])).
% 48.47/6.61 fof(f728,definition,(
% 48.47/6.61 sQ33_spl <=> (ssList(tl(sK48_skl)))),
% 48.47/6.61 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 48.47/6.61 fof(f729,plain,(
% 48.47/6.61 ssList(tl(sK48_skl))|~sQ33_spl),
% 48.47/6.61 inference(component_clause,[status(thm)],[f728])).
% 48.47/6.61 fof(f731,definition,(
% 48.47/6.61 sQ34_spl <=> (ssList(cons(hd(sK48_skl),nil)))),
% 48.47/6.61 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 48.47/6.61 fof(f733,plain,(
% 48.47/6.61 ~ssList(cons(hd(sK48_skl),nil))|sQ34_spl),
% 48.47/6.61 inference(component_clause,[status(thm)],[f731])).
% 48.47/6.61 fof(f734,definition,(
% 48.47/6.61 sQ35_spl <=> (app(tl(sK48_skl),cons(hd(sK48_skl),nil))=sK47_skl)),
% 48.47/6.61 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 48.47/6.61 fof(f737,definition,(
% 48.47/6.61 sQ36_spl <=> (ssItem(hd(sK48_skl)))),
% 48.47/6.61 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 48.47/6.61 fof(f738,plain,(
% 48.47/6.61 ssItem(hd(sK48_skl))|~sQ36_spl),
% 48.47/6.61 inference(component_clause,[status(thm)],[f737])).
% 48.47/6.61 fof(f799,definition,(
% 48.47/6.61 sQ44_spl <=> (ssList(sK47_skl))),
% 48.47/6.61 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 48.47/6.61 fof(f801,plain,(
% 48.47/6.61 ~ssList(sK47_skl)|sQ44_spl),
% 48.47/6.61 inference(component_clause,[status(thm)],[f799])).
% 48.47/6.61 fof(f802,plain,(
% 48.47/6.61 ~sQ44_spl|~sQ33_spl|~sQ34_spl|~sQ35_spl|~sQ36_spl|~sQ0_spl),
% 48.47/6.61 inference(split_clause,[status(thm)],[f472,f799,f728,f731,f734,f737,f428])).
% 48.47/6.61 fof(f837,plain,(
% 48.47/6.61 nil=sK48_skl|ssList(tl(sK48_skl))),
% 48.47/6.61 inference(resolution,[status(thm)],[f419,f241])).
% 48.47/6.61 fof(f838,plain,(
% 48.47/6.61 nil=sK48_skl|ssItem(hd(sK48_skl))),
% 48.47/6.61 inference(resolution,[status(thm)],[f419,f237])).
% 48.47/6.61 fof(f844,plain,(
% 48.47/6.61 sQ5_spl|sQ33_spl),
% 48.47/6.61 inference(split_clause,[status(thm)],[f837,f501,f728])).
% 48.47/6.61 fof(f845,plain,(
% 48.47/6.61 sQ5_spl|sQ36_spl),
% 48.47/6.61 inference(split_clause,[status(thm)],[f838,f501,f737])).
% 48.47/6.61 fof(f1020,plain,(
% 48.47/6.61 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(X1,cons(X0,nil))=sK47_skl|~app(cons(X0,nil),X1)=sK48_skl)),
% 48.47/6.61 inference(forward_demodulation,[status(thm)],[f423,f558])).
% 48.47/6.61 fof(f1179,plain,(
% 48.47/6.61 ~ssList(nil)|~sQ5_spl),
% 48.47/6.61 inference(resolution,[status(thm)],[f668,f458])).
% 48.47/6.61 fof(f1251,plain,(
% 48.47/6.61 $false|sQ44_spl),
% 48.47/6.61 inference(forward_subsumption_resolution,[status(thm)],[f801,f418])).
% 48.47/6.61 fof(f1252,plain,(
% 48.47/6.61 sQ44_spl),
% 48.47/6.61 inference(contradiction_clause,[status(thm)],[f1251])).
% 48.47/6.61 fof(f1991,plain,(
% 48.47/6.61 ![X0]: (~ssItem(X0)|cons(X0,tl(sK48_skl))=app(cons(X0,nil),tl(sK48_skl))|~sQ33_spl)),
% 48.47/6.61 inference(resolution,[status(thm)],[f729,f380])).
% 48.47/6.61 fof(f2305,plain,(
% 48.47/6.61 $false|sQ32_spl),
% 48.47/6.61 inference(forward_subsumption_resolution,[status(thm)],[f223,f727])).
% 48.47/6.61 fof(f2306,plain,(
% 48.47/6.61 sQ32_spl),
% 48.47/6.61 inference(contradiction_clause,[status(thm)],[f2305])).
% 48.47/6.61 fof(f2327,plain,(
% 48.47/6.61 cons(hd(sK48_skl),tl(sK48_skl))=app(cons(hd(sK48_skl),nil),tl(sK48_skl))|~sQ33_spl|~sQ36_spl),
% 48.47/6.61 inference(resolution,[status(thm)],[f1991,f738])).
% 48.47/6.61 fof(f2330,plain,(
% 48.47/6.61 sK48_skl=app(cons(hd(sK48_skl),nil),tl(sK48_skl))|~sQ6_spl|~sQ33_spl|~sQ36_spl),
% 47.79/6.64 inference(forward_demodulation,[status(thm)],[f505,f2327])).
% 47.79/6.64 fof(f2894,plain,(
% 47.79/6.64 ~ssItem(hd(sK48_skl))|~ssList(tl(sK48_skl))|app(tl(sK48_skl),cons(hd(sK48_skl),nil))=sK47_skl|~sQ6_spl|~sQ33_spl|~sQ36_spl),
% 47.79/6.64 inference(resolution,[status(thm)],[f2330,f1020])).
% 47.79/6.64 fof(f2898,plain,(
% 47.79/6.64 ~sQ36_spl|~sQ33_spl|sQ35_spl|~sQ6_spl),
% 47.79/6.64 inference(split_clause,[status(thm)],[f2894,f737,f728,f734,f504])).
% 47.79/6.64 fof(f8829,plain,(
% 47.79/6.64 neq(nil,sK48_skl)|nil=sK48_skl),
% 47.79/6.64 inference(resolution,[status(thm)],[f595,f419])).
% 47.79/6.64 fof(f8843,plain,(
% 47.79/6.64 sQ1_spl|sQ5_spl),
% 47.79/6.64 inference(split_clause,[status(thm)],[f8829,f431,f501])).
% 47.79/6.64 fof(f18724,plain,(
% 47.79/6.64 ssList(cons(hd(sK48_skl),nil))|~sQ36_spl),
% 47.79/6.64 inference(resolution,[status(thm)],[f738,f600])).
% 47.79/6.64 fof(f18737,plain,(
% 47.79/6.64 $false|sQ34_spl|~sQ36_spl),
% 47.79/6.64 inference(forward_subsumption_resolution,[status(thm)],[f18724,f733])).
% 47.79/6.64 fof(f18738,plain,(
% 47.79/6.64 sQ34_spl|~sQ36_spl),
% 47.79/6.64 inference(contradiction_clause,[status(thm)],[f18737])).
% 47.79/6.64 fof(f18754,plain,(
% 47.79/6.64 ~sQ32_spl|~sQ5_spl),
% 47.79/6.64 inference(split_clause,[status(thm)],[f1179,f725,f501])).
% 47.79/6.64 fof(f18790,plain,(
% 47.79/6.64 $false),
% 47.79/6.64 inference(sat_refutation,[status(thm)],[f434,f507,f802,f844,f845,f1252,f2306,f2898,f8843,f18738,f18754])).
% 47.79/6.64 % SZS output end CNFRefutation for theBenchmark.p
% 47.79/6.67 % Elapsed time: 6.293383 seconds
% 47.79/6.67 % CPU time: 49.591936 seconds
% 47.79/6.67 % Total memory used: 445.882 MB
% 47.79/6.67 % Net memory used: 423.264 MB
%------------------------------------------------------------------------------