%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC270+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 : n026.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:01 PM UTC 2026
% Result : Theorem 39.03s 5.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC270+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n026.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 08:12:22 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.50 % Drodi V4.1.1
% 39.03/5.55 % Refutation found
% 39.03/5.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 39.03/5.55 % SZS output start CNFRefutation for theBenchmark
% 39.03/5.55 fof(f11,axiom,(
% 39.03/5.55 (! [U] :( ssList(U)=> ( totalorderedP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> leq(V,W) ) ) )) )) )) )) )) ) )),
% 39.03/5.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.03/5.55 fof(f12,axiom,(
% 39.03/5.55 (! [U] :( ssList(U)=> ( strictorderedP(U)<=> (! [V] :( ssItem(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssList(X)=> (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U=> lt(V,W) ) ) )) )) )) )) )) ) )),
% 39.03/5.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.03/5.55 fof(f93,axiom,(
% 39.03/5.55 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> ( lt(U,V)<=> ( U != V& leq(U,V) ) ) ) )) )),
% 39.03/5.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.03/5.55 fof(f96,conjecture,(
% 39.03/5.55 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ~ segmentP(X,W)| ~ strictorderedP(W)| totalorderedP(U) ) )) )) )) )),
% 39.03/5.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.03/5.55 fof(f97,negated_conjecture,(
% 39.03/5.55 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ~ segmentP(X,W)| ~ strictorderedP(W)| totalorderedP(U) ) )) )) )) ))),
% 39.03/5.55 inference(negated_conjecture,[status(cth)],[f96])).
% 39.03/5.55 fof(f174,plain,(
% 39.03/5.55 ![U]: (~ssList(U)|(totalorderedP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|leq(V,W))))))))))))))),
% 39.03/5.55 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 39.03/5.55 fof(f175,plain,(
% 39.03/5.55 ![U]: (~ssList(U)|((~totalorderedP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|leq(V,W)))))))))))))&(totalorderedP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&~leq(V,W)))))))))))))))),
% 39.03/5.55 inference(NNF_transformation,[status(thm)],[f174])).
% 39.03/5.55 fof(f176,plain,(
% 39.03/5.55 ![U]: (~ssList(U)|((~totalorderedP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|leq(V,W)))))))))))))&(totalorderedP(U)|(ssItem(sK24_skl(U))&(ssItem(sK25_skl(U))&(ssList(sK26_skl(U))&(ssList(sK27_skl(U))&(ssList(sK28_skl(U))&(app(app(sK26_skl(U),cons(sK24_skl(U),sK27_skl(U))),cons(sK25_skl(U),sK28_skl(U)))=U&~leq(sK24_skl(U),sK25_skl(U)))))))))))),
% 39.03/5.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl]),skolemize(V,sK24_skl(U)),skolemize(W,sK25_skl(U)),skolemize(X,sK26_skl(U)),skolemize(Y,sK27_skl(U)),skolemize(Z,sK28_skl(U))],[f175])).
% 39.03/5.55 fof(f178,plain,(
% 39.03/5.55 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssItem(sK24_skl(X0)))),
% 39.03/5.55 inference(cnf_transformation,[status(thm)],[f176])).
% 39.03/5.55 fof(f179,plain,(
% 39.03/5.55 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssItem(sK25_skl(X0)))),
% 39.03/5.55 inference(cnf_transformation,[status(thm)],[f176])).
% 39.03/5.55 fof(f180,plain,(
% 39.03/5.55 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssList(sK26_skl(X0)))),
% 39.03/5.55 inference(cnf_transformation,[status(thm)],[f176])).
% 39.03/5.55 fof(f181,plain,(
% 39.03/5.55 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssList(sK27_skl(X0)))),
% 39.03/5.55 inference(cnf_transformation,[status(thm)],[f176])).
% 39.03/5.55 fof(f182,plain,(
% 39.03/5.55 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssList(sK28_skl(X0)))),
% 39.03/5.55 inference(cnf_transformation,[status(thm)],[f176])).
% 39.03/5.55 fof(f183,plain,(
% 39.03/5.55 ![X0]: (~ssList(X0)|totalorderedP(X0)|app(app(sK26_skl(X0),cons(sK24_skl(X0),sK27_skl(X0))),cons(sK25_skl(X0),sK28_skl(X0)))=X0)),
% 39.03/5.55 inference(cnf_transformation,[status(thm)],[f176])).
% 39.03/5.55 fof(f184,plain,(
% 39.03/5.55 ![X0]: (~ssList(X0)|totalorderedP(X0)|~leq(sK24_skl(X0),sK25_skl(X0)))),
% 39.03/5.55 inference(cnf_transformation,[status(thm)],[f176])).
% 39.03/5.55 fof(f185,plain,(
% 39.03/5.55 ![U]: (~ssList(U)|(strictorderedP(U)<=>(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|lt(V,W))))))))))))))),
% 39.03/5.55 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 39.03/5.56 fof(f186,plain,(
% 39.03/5.56 ![U]: (~ssList(U)|((~strictorderedP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|lt(V,W)))))))))))))&(strictorderedP(U)|(?[V]: (ssItem(V)&(?[W]: (ssItem(W)&(?[X]: (ssList(X)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(app(X,cons(V,Y)),cons(W,Z))=U&~lt(V,W)))))))))))))))),
% 39.03/5.56 inference(NNF_transformation,[status(thm)],[f185])).
% 39.03/5.56 fof(f187,plain,(
% 39.03/5.56 ![U]: (~ssList(U)|((~strictorderedP(U)|(![V]: (~ssItem(V)|(![W]: (~ssItem(W)|(![X]: (~ssList(X)|(![Y]: (~ssList(Y)|(![Z]: (~ssList(Z)|(~app(app(X,cons(V,Y)),cons(W,Z))=U|lt(V,W)))))))))))))&(strictorderedP(U)|(ssItem(sK29_skl(U))&(ssItem(sK30_skl(U))&(ssList(sK31_skl(U))&(ssList(sK32_skl(U))&(ssList(sK33_skl(U))&(app(app(sK31_skl(U),cons(sK29_skl(U),sK32_skl(U))),cons(sK30_skl(U),sK33_skl(U)))=U&~lt(sK29_skl(U),sK30_skl(U)))))))))))),
% 39.03/5.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl,sK30_skl,sK31_skl,sK32_skl,sK33_skl]),skolemize(V,sK29_skl(U)),skolemize(W,sK30_skl(U)),skolemize(X,sK31_skl(U)),skolemize(Y,sK32_skl(U)),skolemize(Z,sK33_skl(U))],[f186])).
% 39.03/5.56 fof(f188,plain,(
% 39.03/5.56 ![X0,X1,X2,X3,X4,X5]: (~ssList(X0)|~strictorderedP(X0)|~ssItem(X1)|~ssItem(X2)|~ssList(X3)|~ssList(X4)|~ssList(X5)|~app(app(X3,cons(X1,X4)),cons(X2,X5))=X0|lt(X1,X2))),
% 39.03/5.56 inference(cnf_transformation,[status(thm)],[f187])).
% 39.03/5.56 fof(f406,plain,(
% 39.03/5.56 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(lt(U,V)<=>(~U=V&leq(U,V))))))),
% 39.03/5.56 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 39.03/5.56 fof(f407,plain,(
% 39.03/5.56 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|((~lt(U,V)|(~U=V&leq(U,V)))&(lt(U,V)|(U=V|~leq(U,V)))))))),
% 39.03/5.56 inference(NNF_transformation,[status(thm)],[f406])).
% 39.03/5.56 fof(f409,plain,(
% 39.03/5.56 ![X0,X1]: (~ssItem(X0)|~ssItem(X1)|~lt(X0,X1)|leq(X0,X1))),
% 39.03/5.56 inference(cnf_transformation,[status(thm)],[f407])).
% 39.03/5.56 fof(f415,plain,(
% 39.03/5.56 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (((((ssList(X)&V=X)&U=W)&segmentP(X,W))&strictorderedP(W))&~totalorderedP(U)))))))))),
% 39.03/5.56 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 39.03/5.56 fof(f416,plain,(
% 39.03/5.56 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(((?[X]: (((ssList(X)&V=X)&U=W)&segmentP(X,W)))&strictorderedP(W))&~totalorderedP(U)))))))),
% 39.03/5.56 inference(miniscoping,[status(thm)],[f415])).
% 39.03/5.56 fof(f417,plain,(
% 39.03/5.56 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(((((ssList(sK50_skl)&sK48_skl=sK50_skl)&sK47_skl=sK49_skl)&segmentP(sK50_skl,sK49_skl))&strictorderedP(sK49_skl))&~totalorderedP(sK47_skl)))))),
% 39.03/5.56 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])).
% 39.03/5.56 fof(f418,plain,(
% 39.03/5.56 ssList(sK47_skl)),
% 39.03/5.56 inference(cnf_transformation,[status(thm)],[f417])).
% 39.03/5.56 fof(f423,plain,(
% 39.03/5.56 sK47_skl=sK49_skl),
% 39.03/5.56 inference(cnf_transformation,[status(thm)],[f417])).
% 39.03/5.56 fof(f425,plain,(
% 39.03/5.56 strictorderedP(sK49_skl)),
% 39.03/5.56 inference(cnf_transformation,[status(thm)],[f417])).
% 39.03/5.56 fof(f426,plain,(
% 39.03/5.56 ~totalorderedP(sK47_skl)),
% 39.03/5.56 inference(cnf_transformation,[status(thm)],[f417])).
% 39.03/5.56 fof(f438,plain,(
% 39.03/5.56 ![X0,X1,X2,X3,X4]: (~ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))|~strictorderedP(app(app(X0,cons(X1,X2)),cons(X3,X4)))|~ssItem(X1)|~ssItem(X3)|~ssList(X0)|~ssList(X2)|~ssList(X4)|lt(X1,X3))),
% 39.03/5.56 inference(destructive_equality_resolution,[status(thm)],[f188])).
% 39.03/5.56 fof(f459,plain,(
% 39.03/5.56 strictorderedP(sK47_skl)),
% 39.03/5.56 inference(forward_demodulation,[status(thm)],[f423,f425])).
% 39.03/5.56 fof(f523,definition,(
% 39.03/5.56 sQ10_spl <=> (ssList(sK47_skl))),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f525,plain,(
% 39.03/5.56 ~ssList(sK47_skl)|sQ10_spl),
% 39.03/5.56 inference(component_clause,[status(thm)],[f523])).
% 39.03/5.56 fof(f538,plain,(
% 39.03/5.56 $false|sQ10_spl),
% 39.03/5.56 inference(forward_subsumption_resolution,[status(thm)],[f525,f418])).
% 39.03/5.56 fof(f539,plain,(
% 39.03/5.56 sQ10_spl),
% 39.03/5.56 inference(contradiction_clause,[status(thm)],[f538])).
% 39.03/5.56 fof(f2189,plain,(
% 39.03/5.56 totalorderedP(sK47_skl)|app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl)))=sK47_skl),
% 39.03/5.56 inference(resolution,[status(thm)],[f183,f418])).
% 39.03/5.56 fof(f2212,definition,(
% 39.03/5.56 sQ256_spl <=> (totalorderedP(sK47_skl))),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f2213,plain,(
% 39.03/5.56 totalorderedP(sK47_skl)|~sQ256_spl),
% 39.03/5.56 inference(component_clause,[status(thm)],[f2212])).
% 39.03/5.56 fof(f2215,definition,(
% 39.03/5.56 sQ257_spl <=> (app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl)))=sK47_skl)),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f2216,plain,(
% 39.03/5.56 app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl)))=sK47_skl|~sQ257_spl),
% 39.03/5.56 inference(component_clause,[status(thm)],[f2215])).
% 39.03/5.56 fof(f2218,plain,(
% 39.03/5.56 sQ256_spl|sQ257_spl),
% 39.03/5.56 inference(split_clause,[status(thm)],[f2189,f2212,f2215])).
% 39.03/5.56 fof(f2258,plain,(
% 39.03/5.56 $false|~sQ256_spl),
% 39.03/5.56 inference(forward_subsumption_resolution,[status(thm)],[f2213,f426])).
% 39.03/5.56 fof(f2259,plain,(
% 39.03/5.56 ~sQ256_spl),
% 39.03/5.56 inference(contradiction_clause,[status(thm)],[f2258])).
% 39.03/5.56 fof(f2690,definition,(
% 39.03/5.56 sQ337_spl <=> (strictorderedP(sK47_skl))),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f2692,plain,(
% 39.03/5.56 ~strictorderedP(sK47_skl)|sQ337_spl),
% 39.03/5.56 inference(component_clause,[status(thm)],[f2690])).
% 39.03/5.56 fof(f3427,plain,(
% 39.03/5.56 ~ssList(sK47_skl)|~strictorderedP(app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl))))|~ssItem(sK24_skl(sK47_skl))|~ssItem(sK25_skl(sK47_skl))|~ssList(sK26_skl(sK47_skl))|~ssList(sK27_skl(sK47_skl))|~ssList(sK28_skl(sK47_skl))|lt(sK24_skl(sK47_skl),sK25_skl(sK47_skl))|~sQ257_spl),
% 39.03/5.56 inference(paramodulation,[status(thm)],[f2216,f438])).
% 39.03/5.56 fof(f3443,definition,(
% 39.03/5.56 sQ463_spl <=> (ssItem(sK24_skl(sK47_skl)))),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ463_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f3445,plain,(
% 39.03/5.56 ~ssItem(sK24_skl(sK47_skl))|sQ463_spl),
% 39.03/5.56 inference(component_clause,[status(thm)],[f3443])).
% 39.03/5.56 fof(f3446,definition,(
% 39.03/5.56 sQ464_spl <=> (ssItem(sK25_skl(sK47_skl)))),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ464_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f3448,plain,(
% 39.03/5.56 ~ssItem(sK25_skl(sK47_skl))|sQ464_spl),
% 39.03/5.56 inference(component_clause,[status(thm)],[f3446])).
% 39.03/5.56 fof(f3449,definition,(
% 39.03/5.56 sQ465_spl <=> (ssList(sK26_skl(sK47_skl)))),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ465_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f3451,plain,(
% 39.03/5.56 ~ssList(sK26_skl(sK47_skl))|sQ465_spl),
% 39.03/5.56 inference(component_clause,[status(thm)],[f3449])).
% 39.03/5.56 fof(f3452,definition,(
% 39.03/5.56 sQ466_spl <=> (ssList(sK27_skl(sK47_skl)))),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ466_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f3454,plain,(
% 39.03/5.56 ~ssList(sK27_skl(sK47_skl))|sQ466_spl),
% 39.03/5.56 inference(component_clause,[status(thm)],[f3452])).
% 39.03/5.56 fof(f3455,definition,(
% 39.03/5.56 sQ467_spl <=> (ssList(sK28_skl(sK47_skl)))),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ467_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f3457,plain,(
% 39.03/5.56 ~ssList(sK28_skl(sK47_skl))|sQ467_spl),
% 39.03/5.56 inference(component_clause,[status(thm)],[f3455])).
% 39.03/5.56 fof(f3458,definition,(
% 39.03/5.56 sQ468_spl <=> (lt(sK24_skl(sK47_skl),sK25_skl(sK47_skl)))),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ468_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f3459,plain,(
% 39.03/5.56 lt(sK24_skl(sK47_skl),sK25_skl(sK47_skl))|~sQ468_spl),
% 39.03/5.56 inference(component_clause,[status(thm)],[f3458])).
% 39.03/5.56 fof(f3468,definition,(
% 39.03/5.56 sQ471_spl <=> (leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl)))),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ471_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f3469,plain,(
% 39.03/5.56 leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl))|~sQ471_spl),
% 39.03/5.56 inference(component_clause,[status(thm)],[f3468])).
% 39.03/5.56 fof(f3483,definition,(
% 39.03/5.56 sQ475_spl <=> (strictorderedP(app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl)))))),
% 39.03/5.56 introduced(definition,[new_symbols(definition,[sQ475_spl])],[split_symbol_definition])).
% 39.03/5.56 fof(f3485,plain,(
% 39.03/5.56 ~strictorderedP(app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl))))|sQ475_spl),
% 39.83/5.61 inference(component_clause,[status(thm)],[f3483])).
% 39.83/5.61 fof(f3486,plain,(
% 39.83/5.61 ~sQ10_spl|~sQ475_spl|~sQ463_spl|~sQ464_spl|~sQ465_spl|~sQ466_spl|~sQ467_spl|sQ468_spl|~sQ257_spl),
% 39.83/5.61 inference(split_clause,[status(thm)],[f3427,f523,f3483,f3443,f3446,f3449,f3452,f3455,f3458,f2215])).
% 39.83/5.61 fof(f3554,plain,(
% 39.83/5.61 ~strictorderedP(sK47_skl)|~sQ257_spl|sQ475_spl),
% 39.83/5.61 inference(forward_demodulation,[status(thm)],[f2216,f3485])).
% 39.83/5.61 fof(f3555,plain,(
% 39.83/5.61 $false|~sQ257_spl|sQ475_spl),
% 39.83/5.61 inference(forward_subsumption_resolution,[status(thm)],[f3554,f459])).
% 39.83/5.61 fof(f3556,plain,(
% 39.83/5.61 ~sQ257_spl|sQ475_spl),
% 39.83/5.61 inference(contradiction_clause,[status(thm)],[f3555])).
% 39.83/5.61 fof(f3688,plain,(
% 39.83/5.61 ~ssList(sK47_skl)|totalorderedP(sK47_skl)|sQ467_spl),
% 39.83/5.61 inference(resolution,[status(thm)],[f3457,f182])).
% 39.83/5.61 fof(f3689,plain,(
% 39.83/5.61 ~sQ10_spl|sQ256_spl|sQ467_spl),
% 39.83/5.61 inference(split_clause,[status(thm)],[f3688,f523,f2212,f3455])).
% 39.83/5.61 fof(f3690,plain,(
% 39.83/5.61 ~ssList(sK47_skl)|totalorderedP(sK47_skl)|sQ464_spl),
% 39.83/5.61 inference(resolution,[status(thm)],[f3448,f179])).
% 39.83/5.61 fof(f3691,plain,(
% 39.83/5.61 ~sQ10_spl|sQ256_spl|sQ464_spl),
% 39.83/5.61 inference(split_clause,[status(thm)],[f3690,f523,f2212,f3446])).
% 39.83/5.61 fof(f3692,plain,(
% 39.83/5.61 ~ssList(sK47_skl)|totalorderedP(sK47_skl)|sQ465_spl),
% 39.83/5.61 inference(resolution,[status(thm)],[f3451,f180])).
% 39.83/5.61 fof(f3693,plain,(
% 39.83/5.61 ~sQ10_spl|sQ256_spl|sQ465_spl),
% 39.83/5.61 inference(split_clause,[status(thm)],[f3692,f523,f2212,f3449])).
% 39.83/5.61 fof(f3694,plain,(
% 39.83/5.61 ~ssList(sK47_skl)|totalorderedP(sK47_skl)|sQ466_spl),
% 39.83/5.61 inference(resolution,[status(thm)],[f3454,f181])).
% 39.83/5.61 fof(f3695,plain,(
% 39.83/5.61 ~sQ10_spl|sQ256_spl|sQ466_spl),
% 39.83/5.61 inference(split_clause,[status(thm)],[f3694,f523,f2212,f3452])).
% 39.83/5.61 fof(f3696,plain,(
% 39.83/5.61 ~ssList(sK47_skl)|totalorderedP(sK47_skl)|sQ463_spl),
% 39.83/5.61 inference(resolution,[status(thm)],[f3445,f178])).
% 39.83/5.61 fof(f3697,plain,(
% 39.83/5.61 ~sQ10_spl|sQ256_spl|sQ463_spl),
% 39.83/5.61 inference(split_clause,[status(thm)],[f3696,f523,f2212,f3443])).
% 39.83/5.61 fof(f8836,plain,(
% 39.83/5.61 $false|sQ337_spl),
% 39.83/5.61 inference(forward_subsumption_resolution,[status(thm)],[f2692,f459])).
% 39.83/5.61 fof(f8837,plain,(
% 39.83/5.61 sQ337_spl),
% 39.83/5.61 inference(contradiction_clause,[status(thm)],[f8836])).
% 39.83/5.61 fof(f11106,plain,(
% 39.83/5.61 ~ssItem(sK24_skl(sK47_skl))|~ssItem(sK25_skl(sK47_skl))|leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl))|~sQ468_spl),
% 39.83/5.61 inference(resolution,[status(thm)],[f3459,f409])).
% 39.83/5.61 fof(f11112,plain,(
% 39.83/5.61 ~sQ463_spl|~sQ464_spl|sQ471_spl|~sQ468_spl),
% 39.83/5.61 inference(split_clause,[status(thm)],[f11106,f3443,f3446,f3468,f3458])).
% 39.83/5.61 fof(f11129,plain,(
% 39.83/5.61 ~ssList(sK47_skl)|totalorderedP(sK47_skl)|~sQ471_spl),
% 39.83/5.61 inference(resolution,[status(thm)],[f3469,f184])).
% 39.83/5.61 fof(f11131,plain,(
% 39.83/5.61 ~sQ10_spl|sQ256_spl|~sQ471_spl),
% 39.83/5.61 inference(split_clause,[status(thm)],[f11129,f523,f2212,f3468])).
% 39.83/5.61 fof(f11136,plain,(
% 39.83/5.61 $false),
% 39.83/5.61 inference(sat_refutation,[status(thm)],[f539,f2218,f2259,f3486,f3556,f3689,f3691,f3693,f3695,f3697,f8837,f11112,f11131])).
% 39.83/5.61 % SZS output end CNFRefutation for theBenchmark.p
% 39.83/5.63 % Elapsed time: 5.156308 seconds
% 39.83/5.63 % CPU time: 40.261361 seconds
% 39.83/5.63 % Total memory used: 327.493 MB
% 39.83/5.63 % Net memory used: 312.953 MB
%------------------------------------------------------------------------------