%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC008+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 : n020.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:41:19 PM UTC 2026
% Result : Theorem 51.42s 7.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC008+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/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 07:49:48 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 51.42/7.01 % Refutation found
% 51.42/7.01 % SZS status Theorem for theBenchmark: Theorem is valid
% 51.42/7.01 % SZS output start CNFRefutation for theBenchmark
% 51.42/7.01 fof(f5,axiom,(
% 51.42/7.01 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 51.42/7.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.42/7.01 fof(f17,axiom,(
% 51.42/7.01 ssList(nil) ),
% 51.42/7.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.42/7.01 fof(f26,axiom,(
% 51.42/7.01 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ssList(app(U,V)) ) )) )),
% 51.42/7.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.42/7.01 fof(f41,axiom,(
% 51.42/7.01 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( ( frontsegP(U,V)& frontsegP(V,U) )=> U = V ) ) )) )),
% 51.42/7.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.42/7.01 fof(f84,axiom,(
% 51.42/7.01 (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 51.42/7.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.42/7.01 fof(f96,conjecture,(
% 51.42/7.01 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| ~ frontsegP(X,W)| ~ equalelemsP(W)| (? [Y] :( ssList(Y)& (? [Z] :( ssList(Z)& (? [X1] :( ssList(X1)& app(app(Y,Z),X1) = V& app(Y,X1) = U ) )) )))| (? [X2] :( ssList(X2)& neq(W,X2)& frontsegP(X,X2)& segmentP(X2,W)& equalelemsP(X2) ) )) ) )) )) )) )),
% 51.42/7.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.42/7.01 fof(f97,negated_conjecture,(
% 51.42/7.01 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| ~ frontsegP(X,W)| ~ equalelemsP(W)| (? [Y] :( ssList(Y)& (? [Z] :( ssList(Z)& (? [X1] :( ssList(X1)& app(app(Y,Z),X1) = V& app(Y,X1) = U ) )) )))| (? [X2] :( ssList(X2)& neq(W,X2)& frontsegP(X,X2)& segmentP(X2,W)& equalelemsP(X2) ) )) ) )) )) )) ))),
% 51.42/7.01 inference(negated_conjecture,[status(cth)],[f96])).
% 51.42/7.01 fof(f119,plain,(
% 51.42/7.01 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 51.42/7.01 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 51.42/7.01 fof(f120,plain,(
% 51.42/7.01 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~frontsegP(U,V)|(?[W]: (ssList(W)&app(V,W)=U)))&(frontsegP(U,V)|(![W]: (~ssList(W)|~app(V,W)=U)))))))),
% 51.42/7.01 inference(NNF_transformation,[status(thm)],[f119])).
% 51.42/7.01 fof(f121,plain,(
% 51.42/7.01 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~frontsegP(U,V)|(ssList(sK5_skl(V,U))&app(V,sK5_skl(V,U))=U))&(frontsegP(U,V)|(![W]: (~ssList(W)|~app(V,W)=U)))))))),
% 51.42/7.01 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 51.42/7.01 fof(f122,plain,(
% 51.42/7.01 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|ssList(sK5_skl(X1,X0)))),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f121])).
% 51.42/7.01 fof(f123,plain,(
% 51.42/7.01 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(X1,sK5_skl(X1,X0))=X0)),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f121])).
% 51.42/7.01 fof(f124,plain,(
% 51.42/7.01 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)|~ssList(X2)|~app(X1,X2)=X0)),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f121])).
% 51.42/7.01 fof(f223,plain,(
% 51.42/7.01 ssList(nil)),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f17])).
% 51.42/7.01 fof(f244,plain,(
% 51.42/7.01 ![U]: (~ssList(U)|(![V]: (~ssList(V)|ssList(app(U,V)))))),
% 51.42/7.01 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 51.42/7.01 fof(f245,plain,(
% 51.42/7.01 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X0,X1)))),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f244])).
% 51.42/7.01 fof(f283,plain,(
% 51.42/7.01 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~frontsegP(U,V)|~frontsegP(V,U))|U=V))))),
% 51.42/7.01 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 51.42/7.01 fof(f284,plain,(
% 51.42/7.01 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|~frontsegP(X1,X0)|X0=X1)),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f283])).
% 51.42/7.01 fof(f388,plain,(
% 51.42/7.01 ![U]: (~ssList(U)|app(U,nil)=U)),
% 51.42/7.01 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 51.42/7.01 fof(f389,plain,(
% 51.42/7.01 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f388])).
% 51.42/7.01 fof(f415,plain,(
% 51.42/7.01 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((((V=X&U=W)&frontsegP(X,W))&equalelemsP(W))&(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(![X1]: ((~ssList(X1)|~app(app(Y,Z),X1)=V)|~app(Y,X1)=U)))))))&(![X2]: ((((~ssList(X2)|~neq(W,X2))|~frontsegP(X,X2))|~segmentP(X2,W))|~equalelemsP(X2))))))))))))),
% 51.42/7.01 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 51.42/7.01 fof(f416,plain,(
% 51.42/7.01 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(ssList(sK50_skl)&(((((sK48_skl=sK50_skl&sK47_skl=sK49_skl)&frontsegP(sK50_skl,sK49_skl))&equalelemsP(sK49_skl))&(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(![X1]: ((~ssList(X1)|~app(app(Y,Z),X1)=sK48_skl)|~app(Y,X1)=sK47_skl)))))))&(![X2]: ((((~ssList(X2)|~neq(sK49_skl,X2))|~frontsegP(sK50_skl,X2))|~segmentP(X2,sK49_skl))|~equalelemsP(X2))))))))),
% 51.42/7.01 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)],[f415])).
% 51.42/7.01 fof(f419,plain,(
% 51.42/7.01 ssList(sK49_skl)),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f416])).
% 51.42/7.01 fof(f420,plain,(
% 51.42/7.01 ssList(sK50_skl)),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f416])).
% 51.42/7.01 fof(f421,plain,(
% 51.42/7.01 sK48_skl=sK50_skl),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f416])).
% 51.42/7.01 fof(f422,plain,(
% 51.42/7.01 sK47_skl=sK49_skl),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f416])).
% 51.42/7.01 fof(f423,plain,(
% 51.42/7.01 frontsegP(sK50_skl,sK49_skl)),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f416])).
% 51.42/7.01 fof(f424,plain,(
% 51.42/7.01 equalelemsP(sK49_skl)),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f416])).
% 51.42/7.01 fof(f425,plain,(
% 51.42/7.01 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~app(app(X0,X1),X2)=sK48_skl|~app(X0,X2)=sK47_skl)),
% 51.42/7.01 inference(cnf_transformation,[status(thm)],[f416])).
% 51.42/7.01 fof(f431,plain,(
% 51.42/7.01 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 51.42/7.01 inference(destructive_equality_resolution,[status(thm)],[f124])).
% 51.42/7.01 fof(f461,plain,(
% 51.42/7.01 ![X0,X1]: (~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 51.42/7.01 inference(backward_subsumption_resolution,[status(thm)],[f431,f245])).
% 51.42/7.01 fof(f483,plain,(
% 51.42/7.01 ~ssList(sK50_skl)|~ssList(sK49_skl)|ssList(sK5_skl(sK49_skl,sK50_skl))),
% 51.42/7.01 inference(resolution,[status(thm)],[f423,f122])).
% 51.42/7.01 fof(f486,plain,(
% 51.42/7.01 ~ssList(sK50_skl)|~ssList(sK49_skl)|app(sK49_skl,sK5_skl(sK49_skl,sK50_skl))=sK50_skl),
% 51.42/7.01 inference(resolution,[status(thm)],[f423,f123])).
% 51.42/7.01 fof(f487,definition,(
% 51.42/7.01 sQ0_spl <=> (ssList(sK50_skl))),
% 51.42/7.01 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 51.42/7.01 fof(f489,plain,(
% 51.42/7.01 ~ssList(sK50_skl)|sQ0_spl),
% 51.42/7.01 inference(component_clause,[status(thm)],[f487])).
% 51.42/7.01 fof(f490,definition,(
% 51.42/7.01 sQ1_spl <=> (ssList(sK49_skl))),
% 51.42/7.01 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 51.42/7.01 fof(f492,plain,(
% 51.42/7.01 ~ssList(sK49_skl)|sQ1_spl),
% 51.42/7.01 inference(component_clause,[status(thm)],[f490])).
% 51.42/7.01 fof(f493,definition,(
% 51.42/7.01 sQ2_spl <=> (ssList(sK5_skl(sK49_skl,sK50_skl)))),
% 51.42/7.01 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 51.42/7.01 fof(f494,plain,(
% 51.42/7.01 ssList(sK5_skl(sK49_skl,sK50_skl))|~sQ2_spl),
% 51.42/7.01 inference(component_clause,[status(thm)],[f493])).
% 51.42/7.01 fof(f496,plain,(
% 51.42/7.01 ~sQ0_spl|~sQ1_spl|sQ2_spl),
% 51.42/7.01 inference(split_clause,[status(thm)],[f483,f487,f490,f493])).
% 51.42/7.01 fof(f508,definition,(
% 51.42/7.01 sQ6_spl <=> (app(sK49_skl,sK5_skl(sK49_skl,sK50_skl))=sK50_skl)),
% 51.42/7.01 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 51.42/7.01 fof(f509,plain,(
% 51.42/7.01 app(sK49_skl,sK5_skl(sK49_skl,sK50_skl))=sK50_skl|~sQ6_spl),
% 51.42/7.01 inference(component_clause,[status(thm)],[f508])).
% 51.42/7.01 fof(f511,plain,(
% 51.42/7.01 ~sQ0_spl|~sQ1_spl|sQ6_spl),
% 51.42/7.01 inference(split_clause,[status(thm)],[f486,f487,f490,f508])).
% 51.42/7.01 fof(f512,plain,(
% 51.42/7.01 $false|sQ1_spl),
% 51.42/7.01 inference(forward_subsumption_resolution,[status(thm)],[f492,f419])).
% 51.42/7.01 fof(f513,plain,(
% 51.42/7.01 sQ1_spl),
% 51.42/7.01 inference(contradiction_clause,[status(thm)],[f512])).
% 51.42/7.01 fof(f514,plain,(
% 51.42/7.01 $false|sQ0_spl),
% 51.42/7.01 inference(forward_subsumption_resolution,[status(thm)],[f489,f420])).
% 51.42/7.01 fof(f515,plain,(
% 51.42/7.01 sQ0_spl),
% 51.42/7.01 inference(contradiction_clause,[status(thm)],[f514])).
% 51.42/7.01 fof(f534,plain,(
% 51.42/7.01 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~app(app(X0,X1),X2)=sK50_skl|~app(X0,X2)=sK47_skl)),
% 51.42/7.01 inference(forward_demodulation,[status(thm)],[f421,f425])).
% 51.42/7.01 fof(f535,plain,(
% 51.42/7.01 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~app(app(X0,X1),X2)=sK50_skl|~app(X0,X2)=sK49_skl)),
% 51.42/7.01 inference(forward_demodulation,[status(thm)],[f422,f534])).
% 51.42/7.01 fof(f551,plain,(
% 51.42/7.01 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~app(app(X0,X1),nil)=sK50_skl|~app(X0,nil)=sK49_skl)),
% 51.42/7.01 inference(resolution,[status(thm)],[f535,f223])).
% 51.42/7.01 fof(f568,definition,(
% 51.42/7.01 sQ9_spl <=> (ssList(nil))),
% 51.42/7.01 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 51.42/7.01 fof(f570,plain,(
% 51.42/7.01 ~ssList(nil)|sQ9_spl),
% 51.42/7.01 inference(component_clause,[status(thm)],[f568])).
% 51.42/7.01 fof(f588,plain,(
% 51.42/7.01 $false|sQ9_spl),
% 51.42/7.01 inference(forward_subsumption_resolution,[status(thm)],[f570,f223])).
% 51.42/7.01 fof(f589,plain,(
% 51.42/7.01 sQ9_spl),
% 51.42/7.01 inference(contradiction_clause,[status(thm)],[f588])).
% 51.42/7.01 fof(f659,definition,(
% 51.42/7.01 sQ23_spl <=> (equalelemsP(sK49_skl))),
% 51.42/7.01 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 51.42/7.01 fof(f661,plain,(
% 51.42/7.01 ~equalelemsP(sK49_skl)|sQ23_spl),
% 51.42/7.01 inference(component_clause,[status(thm)],[f659])).
% 51.42/7.01 fof(f666,plain,(
% 51.42/7.01 $false|sQ23_spl),
% 51.42/7.01 inference(forward_subsumption_resolution,[status(thm)],[f661,f424])).
% 51.42/7.01 fof(f667,plain,(
% 51.42/7.01 sQ23_spl),
% 51.42/7.01 inference(contradiction_clause,[status(thm)],[f666])).
% 51.42/7.01 fof(f928,plain,(
% 51.42/7.01 app(sK50_skl,nil)=sK50_skl),
% 51.42/7.01 inference(resolution,[status(thm)],[f389,f420])).
% 51.42/7.01 fof(f929,plain,(
% 51.42/7.01 app(sK49_skl,nil)=sK49_skl),
% 51.42/7.01 inference(resolution,[status(thm)],[f389,f419])).
% 51.42/7.01 fof(f1042,plain,(
% 51.42/7.01 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(X0)|~ssList(app(X0,X1))|~frontsegP(X0,app(X0,X1))|X0=app(X0,X1))),
% 51.42/7.01 inference(resolution,[status(thm)],[f461,f284])).
% 51.42/7.01 fof(f1056,plain,(
% 51.42/7.01 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(app(X0,X1))|~frontsegP(X0,app(X0,X1))|X0=app(X0,X1))),
% 51.42/7.01 inference(duplicate_literals_removal,[status(thm)],[f1042])).
% 51.42/7.01 fof(f1057,plain,(
% 51.42/7.01 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,app(X0,X1))|X0=app(X0,X1))),
% 51.42/7.01 inference(forward_subsumption_resolution,[status(thm)],[f1056,f245])).
% 51.42/7.01 fof(f1199,definition,(
% 51.42/7.01 sQ83_spl <=> (app(sK49_skl,nil)=sK49_skl)),
% 51.42/7.01 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 51.42/7.01 fof(f1539,plain,(
% 51.42/7.01 ![X0]: (~ssList(X0)|~app(app(X0,sK5_skl(sK49_skl,sK50_skl)),nil)=sK50_skl|~app(X0,nil)=sK49_skl|~sQ2_spl)),
% 51.42/7.01 inference(resolution,[status(thm)],[f551,f494])).
% 51.42/7.01 fof(f2222,definition,(
% 51.42/7.01 sQ171_spl <=> (app(sK50_skl,sK50_skl)=app(sK50_skl,sK50_skl))),
% 51.42/7.01 introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition])).
% 51.42/7.01 fof(f2224,plain,(
% 51.42/7.01 ~app(sK50_skl,sK50_skl)=app(sK50_skl,sK50_skl)|sQ171_spl),
% 51.42/7.01 inference(component_clause,[status(thm)],[f2222])).
% 51.42/7.01 fof(f2233,plain,(
% 51.42/7.01 $false|sQ171_spl),
% 51.42/7.01 inference(trivial_equality_resolution,[status(thm)],[f2224])).
% 51.42/7.01 fof(f2234,plain,(
% 51.42/7.01 sQ171_spl),
% 51.42/7.01 inference(contradiction_clause,[status(thm)],[f2233])).
% 51.42/7.01 fof(f3631,plain,(
% 51.42/7.01 ~ssList(sK49_skl)|frontsegP(sK49_skl,sK49_skl)|~ssList(nil)),
% 51.42/7.01 inference(paramodulation,[status(thm)],[f929,f461])).
% 51.42/7.01 fof(f3648,definition,(
% 51.42/7.01 sQ277_spl <=> (frontsegP(sK49_skl,sK49_skl))),
% 51.42/7.01 introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition])).
% 51.42/7.01 fof(f3651,plain,(
% 51.42/7.01 ~sQ1_spl|sQ277_spl|~sQ9_spl),
% 51.42/7.01 inference(split_clause,[status(thm)],[f3631,f490,f3648,f568])).
% 51.42/7.01 fof(f4086,plain,(
% 51.42/7.01 ~ssList(sK49_skl)|~ssList(nil)|~frontsegP(sK49_skl,sK49_skl)|sK49_skl=app(sK49_skl,nil)),
% 51.42/7.01 inference(paramodulation,[status(thm)],[f929,f1057])).
% 51.42/7.01 fof(f4100,plain,(
% 51.42/7.01 ~sQ1_spl|~sQ9_spl|~sQ277_spl|sQ83_spl),
% 51.42/7.01 inference(split_clause,[status(thm)],[f4086,f490,f568,f3648,f1199])).
% 51.42/7.01 fof(f7928,plain,(
% 51.42/7.01 ~app(app(sK49_skl,sK5_skl(sK49_skl,sK50_skl)),nil)=sK50_skl|~app(sK49_skl,nil)=sK49_skl|~sQ2_spl),
% 51.42/7.01 inference(resolution,[status(thm)],[f1539,f419])).
% 51.42/7.01 fof(f7943,definition,(
% 51.42/7.01 sQ600_spl <=> (app(app(sK49_skl,sK5_skl(sK49_skl,sK50_skl)),nil)=sK50_skl)),
% 51.42/7.01 introduced(definition,[new_symbols(definition,[sQ600_spl])],[split_symbol_definition])).
% 51.42/7.01 fof(f7945,plain,(
% 51.42/7.01 ~app(app(sK49_skl,sK5_skl(sK49_skl,sK50_skl)),nil)=sK50_skl|sQ600_spl),
% 51.42/7.01 inference(component_clause,[status(thm)],[f7943])).
% 51.42/7.01 fof(f7946,plain,(
% 51.42/7.01 ~sQ600_spl|~sQ83_spl|~sQ2_spl),
% 51.42/7.01 inference(split_clause,[status(thm)],[f7928,f7943,f1199,f493])).
% 51.42/7.01 fof(f7947,plain,(
% 51.42/7.01 ~app(sK50_skl,nil)=sK50_skl|~sQ6_spl|sQ600_spl),
% 51.42/7.01 inference(forward_demodulation,[status(thm)],[f509,f7945])).
% 50.05/7.02 fof(f7948,plain,(
% 50.05/7.02 ~sK50_skl=sK50_skl|~sQ6_spl|sQ600_spl),
% 50.05/7.02 inference(forward_demodulation,[status(thm)],[f928,f7947])).
% 50.05/7.02 fof(f7949,plain,(
% 50.05/7.02 $false|~sQ6_spl|sQ600_spl),
% 50.05/7.02 inference(trivial_equality_resolution,[status(thm)],[f7948])).
% 50.05/7.02 fof(f7950,plain,(
% 50.05/7.02 ~sQ6_spl|sQ600_spl),
% 50.05/7.02 inference(contradiction_clause,[status(thm)],[f7949])).
% 50.05/7.02 fof(f7951,plain,(
% 50.05/7.02 $false),
% 50.05/7.02 inference(sat_refutation,[status(thm)],[f496,f511,f513,f515,f589,f667,f2234,f3651,f4100,f7946,f7950])).
% 50.05/7.02 % SZS output end CNFRefutation for theBenchmark.p
% 50.05/7.06 % Elapsed time: 6.692794 seconds
% 50.05/7.06 % CPU time: 52.572888 seconds
% 50.05/7.06 % Total memory used: 426.101 MB
% 50.05/7.06 % Net memory used: 402.161 MB
%------------------------------------------------------------------------------