%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC273+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:02 PM UTC 2026
% Result : Theorem 97.92s 12.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC273+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.41 % Computer : n019.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Mon Sep 21 08:10:37 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.19/0.44 % Drodi V4.1.1
% 97.92/12.91 % Refutation found
% 97.92/12.91 % SZS status Theorem for theBenchmark: Theorem is valid
% 97.92/12.91 % SZS output start CNFRefutation for theBenchmark
% 97.92/12.91 fof(f2,axiom,(
% 97.92/12.91 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 97.92/12.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 97.92/12.91 fof(f11,axiom,(
% 97.92/12.91 (! [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) ) ) )) )) )) )) )) ) )),
% 97.92/12.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 97.92/12.91 fof(f12,axiom,(
% 97.92/12.91 (! [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) ) ) )) )) )) )) )) ) )),
% 97.92/12.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 97.92/12.91 fof(f16,axiom,(
% 97.92/12.91 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ssList(cons(V,U)) ) )) )),
% 97.92/12.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 97.92/12.91 fof(f17,axiom,(
% 97.92/12.91 ssList(nil) ),
% 97.92/12.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 97.92/12.91 fof(f18,axiom,(
% 97.92/12.91 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> cons(V,U) != U ) )) )),
% 97.92/12.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 97.92/12.91 fof(f93,axiom,(
% 97.92/12.91 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> ( lt(U,V)<=> ( U != V& leq(U,V) ) ) ) )) )),
% 97.92/12.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 97.92/12.91 fof(f96,conjecture,(
% 97.92/12.91 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ~ segmentP(X,W)| ~ strictorderedP(W)| (? [Y] :( ssList(Y)& neq(W,Y)& segmentP(X,Y)& segmentP(Y,W)& strictorderedP(Y) ))| totalorderedP(U) ) )) )) )) )),
% 97.92/12.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 97.92/12.91 fof(f97,negated_conjecture,(
% 97.92/12.91 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ~ segmentP(X,W)| ~ strictorderedP(W)| (? [Y] :( ssList(Y)& neq(W,Y)& segmentP(X,Y)& segmentP(Y,W)& strictorderedP(Y) ))| totalorderedP(U) ) )) )) )) ))),
% 97.92/12.91 inference(negated_conjecture,[status(cth)],[f96])).
% 97.92/12.91 fof(f102,plain,(
% 97.92/12.91 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 97.92/12.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 97.92/12.91 fof(f104,plain,(
% 97.92/12.91 ssItem(sK1_skl)),
% 97.92/12.91 inference(cnf_transformation,[status(thm)],[f102])).
% 97.92/12.91 fof(f174,plain,(
% 97.92/12.91 ![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))))))))))))))),
% 97.92/12.91 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 97.92/12.91 fof(f175,plain,(
% 97.92/12.91 ![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)))))))))))))))),
% 97.92/12.91 inference(NNF_transformation,[status(thm)],[f174])).
% 97.92/12.91 fof(f176,plain,(
% 97.92/12.91 ![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)))))))))))),
% 97.92/12.91 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])).
% 97.92/12.91 fof(f178,plain,(
% 97.92/12.91 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssItem(sK24_skl(X0)))),
% 97.92/12.91 inference(cnf_transformation,[status(thm)],[f176])).
% 97.92/12.91 fof(f179,plain,(
% 97.92/12.91 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssItem(sK25_skl(X0)))),
% 97.92/12.91 inference(cnf_transformation,[status(thm)],[f176])).
% 98.69/12.92 fof(f180,plain,(
% 98.69/12.92 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssList(sK26_skl(X0)))),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f176])).
% 98.69/12.92 fof(f181,plain,(
% 98.69/12.92 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssList(sK27_skl(X0)))),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f176])).
% 98.69/12.92 fof(f182,plain,(
% 98.69/12.92 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssList(sK28_skl(X0)))),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f176])).
% 98.69/12.92 fof(f183,plain,(
% 98.69/12.92 ![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)),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f176])).
% 98.69/12.92 fof(f184,plain,(
% 98.69/12.92 ![X0]: (~ssList(X0)|totalorderedP(X0)|~leq(sK24_skl(X0),sK25_skl(X0)))),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f176])).
% 98.69/12.92 fof(f185,plain,(
% 98.69/12.92 ![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))))))))))))))),
% 98.69/12.92 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 98.69/12.92 fof(f186,plain,(
% 98.69/12.92 ![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)))))))))))))))),
% 98.69/12.92 inference(NNF_transformation,[status(thm)],[f185])).
% 98.69/12.92 fof(f187,plain,(
% 98.69/12.92 ![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)))))))))))),
% 98.69/12.92 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])).
% 98.69/12.92 fof(f188,plain,(
% 98.69/12.92 ![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))),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f187])).
% 98.69/12.92 fof(f221,plain,(
% 98.69/12.92 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|ssList(cons(V,U)))))),
% 98.69/12.92 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 98.69/12.92 fof(f222,plain,(
% 98.69/12.92 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|ssList(cons(X1,X0)))),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f221])).
% 98.69/12.92 fof(f223,plain,(
% 98.69/12.92 ssList(nil)),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f17])).
% 98.69/12.92 fof(f224,plain,(
% 98.69/12.92 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|~cons(V,U)=U)))),
% 98.69/12.92 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 98.69/12.92 fof(f225,plain,(
% 98.69/12.92 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|~cons(X1,X0)=X0)),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f224])).
% 98.69/12.92 fof(f406,plain,(
% 98.69/12.92 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(lt(U,V)<=>(~U=V&leq(U,V))))))),
% 98.69/12.92 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 98.69/12.92 fof(f407,plain,(
% 98.69/12.92 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|((~lt(U,V)|(~U=V&leq(U,V)))&(lt(U,V)|(U=V|~leq(U,V)))))))),
% 98.69/12.92 inference(NNF_transformation,[status(thm)],[f406])).
% 98.69/12.92 fof(f409,plain,(
% 98.69/12.92 ![X0,X1]: (~ssItem(X0)|~ssItem(X1)|~lt(X0,X1)|leq(X0,X1))),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f407])).
% 98.69/12.92 fof(f415,plain,(
% 98.69/12.92 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: ((((((ssList(X)&V=X)&U=W)&segmentP(X,W))&strictorderedP(W))&(![Y]: ((((~ssList(Y)|~neq(W,Y))|~segmentP(X,Y))|~segmentP(Y,W))|~strictorderedP(Y))))&~totalorderedP(U)))))))))),
% 98.69/12.92 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 98.69/12.92 fof(f416,plain,(
% 98.69/12.92 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&((?[X]: (((((ssList(X)&V=X)&U=W)&segmentP(X,W))&strictorderedP(W))&(![Y]: ((((~ssList(Y)|~neq(W,Y))|~segmentP(X,Y))|~segmentP(Y,W))|~strictorderedP(Y)))))&~totalorderedP(U)))))))),
% 98.69/12.92 inference(miniscoping,[status(thm)],[f415])).
% 98.69/12.92 fof(f417,plain,(
% 98.69/12.92 (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))&(![Y]: ((((~ssList(Y)|~neq(sK49_skl,Y))|~segmentP(sK50_skl,Y))|~segmentP(Y,sK49_skl))|~strictorderedP(Y))))&~totalorderedP(sK47_skl)))))),
% 98.69/12.92 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])).
% 98.69/12.92 fof(f418,plain,(
% 98.69/12.92 ssList(sK47_skl)),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f417])).
% 98.69/12.92 fof(f419,plain,(
% 98.69/12.92 ssList(sK48_skl)),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f417])).
% 98.69/12.92 fof(f423,plain,(
% 98.69/12.92 sK47_skl=sK49_skl),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f417])).
% 98.69/12.92 fof(f425,plain,(
% 98.69/12.92 strictorderedP(sK49_skl)),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f417])).
% 98.69/12.92 fof(f427,plain,(
% 98.69/12.92 ~totalorderedP(sK47_skl)),
% 98.69/12.92 inference(cnf_transformation,[status(thm)],[f417])).
% 98.69/12.92 fof(f439,plain,(
% 98.69/12.92 ![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))),
% 98.69/12.92 inference(destructive_equality_resolution,[status(thm)],[f188])).
% 98.69/12.92 fof(f462,plain,(
% 98.69/12.92 strictorderedP(sK47_skl)),
% 98.69/12.92 inference(forward_demodulation,[status(thm)],[f423,f425])).
% 98.69/12.92 fof(f542,definition,(
% 98.69/12.92 sQ12_spl <=> (ssList(sK47_skl))),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f544,plain,(
% 98.69/12.92 ~ssList(sK47_skl)|sQ12_spl),
% 98.69/12.92 inference(component_clause,[status(thm)],[f542])).
% 98.69/12.92 fof(f549,plain,(
% 98.69/12.92 $false|sQ12_spl),
% 98.69/12.92 inference(forward_subsumption_resolution,[status(thm)],[f544,f418])).
% 98.69/12.92 fof(f550,plain,(
% 98.69/12.92 sQ12_spl),
% 98.69/12.92 inference(contradiction_clause,[status(thm)],[f549])).
% 98.69/12.92 fof(f5992,plain,(
% 98.69/12.92 totalorderedP(sK47_skl)|ssList(sK26_skl(sK47_skl))),
% 98.69/12.92 inference(resolution,[status(thm)],[f180,f418])).
% 98.69/12.92 fof(f6162,definition,(
% 98.69/12.92 sQ666_spl <=> (totalorderedP(sK47_skl))),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ666_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f6163,plain,(
% 98.69/12.92 totalorderedP(sK47_skl)|~sQ666_spl),
% 98.69/12.92 inference(component_clause,[status(thm)],[f6162])).
% 98.69/12.92 fof(f6165,definition,(
% 98.69/12.92 sQ667_spl <=> (ssList(sK26_skl(sK47_skl)))),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ667_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f6168,plain,(
% 98.69/12.92 sQ666_spl|sQ667_spl),
% 98.69/12.92 inference(split_clause,[status(thm)],[f5992,f6162,f6165])).
% 98.69/12.92 fof(f6201,plain,(
% 98.69/12.92 $false|~sQ666_spl),
% 98.69/12.92 inference(forward_subsumption_resolution,[status(thm)],[f6163,f427])).
% 98.69/12.92 fof(f6202,plain,(
% 98.69/12.92 ~sQ666_spl),
% 98.69/12.92 inference(contradiction_clause,[status(thm)],[f6201])).
% 98.69/12.92 fof(f7101,plain,(
% 98.69/12.92 totalorderedP(sK47_skl)|ssList(sK27_skl(sK47_skl))),
% 98.69/12.92 inference(resolution,[status(thm)],[f181,f418])).
% 98.69/12.92 fof(f7222,definition,(
% 98.69/12.92 sQ807_spl <=> (ssList(sK27_skl(sK47_skl)))),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ807_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f7225,plain,(
% 98.69/12.92 sQ666_spl|sQ807_spl),
% 98.69/12.92 inference(split_clause,[status(thm)],[f7101,f6162,f7222])).
% 98.69/12.92 fof(f8185,plain,(
% 98.69/12.92 totalorderedP(sK47_skl)|ssList(sK28_skl(sK47_skl))),
% 98.69/12.92 inference(resolution,[status(thm)],[f182,f418])).
% 98.69/12.92 fof(f8326,definition,(
% 98.69/12.92 sQ954_spl <=> (ssList(sK28_skl(sK47_skl)))),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ954_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f8329,plain,(
% 98.69/12.92 sQ666_spl|sQ954_spl),
% 98.69/12.92 inference(split_clause,[status(thm)],[f8185,f6162,f8326])).
% 98.69/12.92 fof(f8534,plain,(
% 98.69/12.92 ~ssList(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),
% 98.69/12.92 inference(resolution,[status(thm)],[f183,f427])).
% 98.69/12.92 fof(f8536,definition,(
% 98.69/12.92 sQ976_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)),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ976_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f8537,plain,(
% 98.69/12.92 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|~sQ976_spl),
% 98.69/12.92 inference(component_clause,[status(thm)],[f8536])).
% 98.69/12.92 fof(f8539,plain,(
% 98.69/12.92 ~sQ12_spl|sQ976_spl),
% 98.69/12.92 inference(split_clause,[status(thm)],[f8534,f542,f8536])).
% 98.69/12.92 fof(f8972,plain,(
% 98.69/12.92 ~ssList(app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl))))|~strictorderedP(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))|~sQ976_spl),
% 98.69/12.92 inference(paramodulation,[status(thm)],[f8537,f439])).
% 98.69/12.92 fof(f8988,definition,(
% 98.69/12.92 sQ1025_spl <=> (ssList(app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl)))))),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ1025_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f8990,plain,(
% 98.69/12.92 ~ssList(app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl))))|sQ1025_spl),
% 98.69/12.92 inference(component_clause,[status(thm)],[f8988])).
% 98.69/12.92 fof(f8991,definition,(
% 98.69/12.92 sQ1026_spl <=> (ssItem(sK24_skl(sK47_skl)))),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ1026_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f8993,plain,(
% 98.69/12.92 ~ssItem(sK24_skl(sK47_skl))|sQ1026_spl),
% 98.69/12.92 inference(component_clause,[status(thm)],[f8991])).
% 98.69/12.92 fof(f8994,definition,(
% 98.69/12.92 sQ1027_spl <=> (ssItem(sK25_skl(sK47_skl)))),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ1027_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f8996,plain,(
% 98.69/12.92 ~ssItem(sK25_skl(sK47_skl))|sQ1027_spl),
% 98.69/12.92 inference(component_clause,[status(thm)],[f8994])).
% 98.69/12.92 fof(f8997,definition,(
% 98.69/12.92 sQ1028_spl <=> (lt(sK24_skl(sK47_skl),sK25_skl(sK47_skl)))),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ1028_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f8998,plain,(
% 98.69/12.92 lt(sK24_skl(sK47_skl),sK25_skl(sK47_skl))|~sQ1028_spl),
% 98.69/12.92 inference(component_clause,[status(thm)],[f8997])).
% 98.69/12.92 fof(f9004,definition,(
% 98.69/12.92 sQ1030_spl <=> (leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl)))),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ1030_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f9005,plain,(
% 98.69/12.92 leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl))|~sQ1030_spl),
% 98.69/12.92 inference(component_clause,[status(thm)],[f9004])).
% 98.69/12.92 fof(f9012,definition,(
% 98.69/12.92 sQ1032_spl <=> (strictorderedP(sK47_skl))),
% 98.69/12.92 introduced(definition,[new_symbols(definition,[sQ1032_spl])],[split_symbol_definition])).
% 98.69/12.92 fof(f9014,plain,(
% 98.69/12.92 ~strictorderedP(sK47_skl)|sQ1032_spl),
% 98.69/12.92 inference(component_clause,[status(thm)],[f9012])).
% 98.69/12.92 fof(f9015,plain,(
% 98.69/12.92 ~sQ1025_spl|~sQ1032_spl|~sQ1026_spl|~sQ1027_spl|~sQ667_spl|~sQ807_spl|~sQ954_spl|sQ1028_spl|~sQ976_spl),
% 98.69/12.92 inference(split_clause,[status(thm)],[f8972,f8988,f9012,f8991,f8994,f6165,f7222,f8326,f8997,f8536])).
% 98.69/12.92 fof(f9076,plain,(
% 98.69/12.92 ~ssList(sK47_skl)|totalorderedP(sK47_skl)|sQ1027_spl),
% 98.69/12.92 inference(resolution,[status(thm)],[f8996,f179])).
% 98.69/12.92 fof(f9077,plain,(
% 98.69/12.92 ~sQ12_spl|sQ666_spl|sQ1027_spl),
% 98.69/12.92 inference(split_clause,[status(thm)],[f9076,f542,f6162,f8994])).
% 98.69/12.92 fof(f9078,plain,(
% 98.69/12.92 ~ssList(sK47_skl)|totalorderedP(sK47_skl)|sQ1026_spl),
% 98.69/12.92 inference(resolution,[status(thm)],[f8993,f178])).
% 98.69/12.92 fof(f9079,plain,(
% 98.69/12.92 ~sQ12_spl|sQ666_spl|sQ1026_spl),
% 98.69/12.92 inference(split_clause,[status(thm)],[f9078,f542,f6162,f8991])).
% 98.69/12.92 fof(f9080,plain,(
% 98.69/12.92 ~ssList(sK47_skl)|~sQ976_spl|sQ1025_spl),
% 98.69/12.92 inference(forward_demodulation,[status(thm)],[f8537,f8990])).
% 98.69/12.92 fof(f9081,plain,(
% 98.69/12.92 $false|~sQ976_spl|sQ1025_spl),
% 98.69/12.92 inference(forward_subsumption_resolution,[status(thm)],[f9080,f418])).
% 98.69/12.92 fof(f9082,plain,(
% 98.69/12.92 ~sQ976_spl|sQ1025_spl),
% 98.69/12.92 inference(contradiction_clause,[status(thm)],[f9081])).
% 98.69/12.92 fof(f11030,plain,(
% 98.69/12.92 $false|sQ1032_spl),
% 98.69/12.92 inference(forward_subsumption_resolution,[status(thm)],[f9014,f462])).
% 98.69/12.92 fof(f11031,plain,(
% 98.69/12.92 sQ1032_spl),
% 98.69/12.92 inference(contradiction_clause,[status(thm)],[f11030])).
% 98.69/12.92 fof(f13072,plain,(
% 98.69/12.92 ~ssList(sK47_skl)|totalorderedP(sK47_skl)|~sQ1030_spl),
% 98.69/12.92 inference(resolution,[status(thm)],[f9005,f184])).
% 98.69/12.92 fof(f13073,plain,(
% 98.69/12.92 ~sQ12_spl|sQ666_spl|~sQ1030_spl),
% 98.69/12.92 inference(split_clause,[status(thm)],[f13072,f542,f6162,f9004])).
% 98.69/12.92 fof(f13330,plain,(
% 98.69/12.92 ![X0]: (~ssList(X0)|ssList(cons(sK1_skl,X0)))),
% 98.69/12.94 inference(resolution,[status(thm)],[f222,f104])).
% 98.69/12.94 fof(f13348,plain,(
% 98.69/12.94 ![X0]: (~ssList(X0)|~cons(sK1_skl,X0)=X0)),
% 98.69/12.94 inference(resolution,[status(thm)],[f225,f104])).
% 98.69/12.94 fof(f19492,plain,(
% 98.69/12.94 ~cons(sK1_skl,nil)=nil),
% 98.69/12.94 inference(resolution,[status(thm)],[f13348,f223])).
% 98.69/12.94 fof(f19744,plain,(
% 98.69/12.94 ssList(cons(sK1_skl,sK48_skl))),
% 98.69/12.94 inference(resolution,[status(thm)],[f13330,f419])).
% 98.69/12.94 fof(f19745,plain,(
% 98.69/12.94 ssList(cons(sK1_skl,sK47_skl))),
% 98.69/12.94 inference(resolution,[status(thm)],[f13330,f418])).
% 98.69/12.94 fof(f19752,plain,(
% 98.69/12.94 ssList(cons(sK1_skl,nil))),
% 98.69/12.94 inference(resolution,[status(thm)],[f13330,f223])).
% 98.69/12.94 fof(f20268,definition,(
% 98.69/12.94 sQ2429_spl <=> (ssItem(sK1_skl))),
% 98.69/12.94 introduced(definition,[new_symbols(definition,[sQ2429_spl])],[split_symbol_definition])).
% 98.69/12.94 fof(f20270,plain,(
% 98.69/12.94 ~ssItem(sK1_skl)|sQ2429_spl),
% 98.69/12.94 inference(component_clause,[status(thm)],[f20268])).
% 98.69/12.94 fof(f20272,definition,(
% 98.69/12.94 sQ2430_spl <=> (nil=cons(sK1_skl,nil))),
% 98.69/12.94 introduced(definition,[new_symbols(definition,[sQ2430_spl])],[split_symbol_definition])).
% 98.69/12.94 fof(f20273,plain,(
% 98.69/12.94 nil=cons(sK1_skl,nil)|~sQ2430_spl),
% 98.69/12.94 inference(component_clause,[status(thm)],[f20272])).
% 98.69/12.94 fof(f20388,plain,(
% 98.69/12.94 $false|~sQ2430_spl),
% 98.69/12.94 inference(forward_subsumption_resolution,[status(thm)],[f20273,f19492])).
% 98.69/12.94 fof(f20389,plain,(
% 98.69/12.94 ~sQ2430_spl),
% 98.69/12.94 inference(contradiction_clause,[status(thm)],[f20388])).
% 98.69/12.94 fof(f20424,plain,(
% 98.69/12.94 $false|sQ2429_spl),
% 98.69/12.94 inference(forward_subsumption_resolution,[status(thm)],[f20270,f104])).
% 98.69/12.94 fof(f20425,plain,(
% 98.69/12.94 sQ2429_spl),
% 98.69/12.94 inference(contradiction_clause,[status(thm)],[f20424])).
% 98.69/12.94 fof(f20732,definition,(
% 98.69/12.94 sQ2514_spl <=> (ssList(cons(sK1_skl,nil)))),
% 98.69/12.94 introduced(definition,[new_symbols(definition,[sQ2514_spl])],[split_symbol_definition])).
% 98.69/12.94 fof(f20734,plain,(
% 98.69/12.94 ~ssList(cons(sK1_skl,nil))|sQ2514_spl),
% 98.69/12.94 inference(component_clause,[status(thm)],[f20732])).
% 98.69/12.94 fof(f20743,plain,(
% 98.69/12.94 $false|sQ2514_spl),
% 98.69/12.94 inference(forward_subsumption_resolution,[status(thm)],[f20734,f19752])).
% 98.69/12.94 fof(f20744,plain,(
% 98.69/12.94 sQ2514_spl),
% 98.69/12.94 inference(contradiction_clause,[status(thm)],[f20743])).
% 98.69/12.94 fof(f20750,definition,(
% 98.69/12.94 sQ2518_spl <=> (ssList(cons(sK1_skl,sK48_skl)))),
% 98.69/12.94 introduced(definition,[new_symbols(definition,[sQ2518_spl])],[split_symbol_definition])).
% 98.69/12.94 fof(f20752,plain,(
% 98.69/12.94 ~ssList(cons(sK1_skl,sK48_skl))|sQ2518_spl),
% 98.69/12.94 inference(component_clause,[status(thm)],[f20750])).
% 98.69/12.94 fof(f20881,definition,(
% 98.69/12.94 sQ2521_spl <=> (ssList(cons(sK1_skl,sK47_skl)))),
% 98.69/12.94 introduced(definition,[new_symbols(definition,[sQ2521_spl])],[split_symbol_definition])).
% 98.69/12.94 fof(f20883,plain,(
% 98.69/12.94 ~ssList(cons(sK1_skl,sK47_skl))|sQ2521_spl),
% 98.69/12.94 inference(component_clause,[status(thm)],[f20881])).
% 98.69/12.94 fof(f21054,plain,(
% 98.69/12.94 $false|sQ2518_spl),
% 98.69/12.94 inference(forward_subsumption_resolution,[status(thm)],[f20752,f19744])).
% 98.69/12.94 fof(f21055,plain,(
% 98.69/12.94 sQ2518_spl),
% 98.69/12.94 inference(contradiction_clause,[status(thm)],[f21054])).
% 98.69/12.94 fof(f27884,plain,(
% 98.69/12.94 $false|sQ2521_spl),
% 98.69/12.94 inference(forward_subsumption_resolution,[status(thm)],[f20883,f19745])).
% 98.69/12.94 fof(f27885,plain,(
% 98.69/12.94 sQ2521_spl),
% 98.69/12.94 inference(contradiction_clause,[status(thm)],[f27884])).
% 98.69/12.94 fof(f27903,plain,(
% 98.69/12.94 ~ssItem(sK24_skl(sK47_skl))|~ssItem(sK25_skl(sK47_skl))|leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl))|~sQ1028_spl),
% 98.69/12.94 inference(resolution,[status(thm)],[f409,f8998])).
% 98.69/12.94 fof(f27904,plain,(
% 98.69/12.94 ~sQ1026_spl|~sQ1027_spl|sQ1030_spl|~sQ1028_spl),
% 98.69/12.94 inference(split_clause,[status(thm)],[f27903,f8991,f8994,f9004,f8997])).
% 98.69/12.94 fof(f27905,plain,(
% 98.69/12.94 $false),
% 98.69/12.94 inference(sat_refutation,[status(thm)],[f550,f6168,f6202,f7225,f8329,f8539,f9015,f9077,f9079,f9082,f11031,f13073,f20389,f20425,f20744,f21055,f27885,f27904])).
% 98.69/12.94 % SZS output end CNFRefutation for theBenchmark.p
% 98.69/13.00 % Elapsed time: 12.563324 seconds
% 98.69/13.00 % CPU time: 99.214608 seconds
% 98.69/13.00 % Total memory used: 543.884 MB
% 98.69/13.00 % Net memory used: 512.036 MB
%------------------------------------------------------------------------------