%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC264+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 : 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:00 PM UTC 2026
% Result : Theorem 23.14s 3.34s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC264+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n016.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 08:14:09 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 23.14/3.34 % Refutation found
% 23.14/3.34 % SZS status Theorem for theBenchmark: Theorem is valid
% 23.14/3.34 % SZS output start CNFRefutation for theBenchmark
% 23.14/3.34 fof(f2,axiom,(
% 23.14/3.34 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 23.14/3.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.14/3.34 fof(f11,axiom,(
% 23.14/3.34 (! [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) ) ) )) )) )) )) )) ) )),
% 23.14/3.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.14/3.34 fof(f12,axiom,(
% 23.14/3.34 (! [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) ) ) )) )) )) )) )) ) )),
% 23.14/3.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.14/3.34 fof(f17,axiom,(
% 23.14/3.34 ssList(nil) ),
% 23.14/3.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.14/3.34 fof(f42,axiom,(
% 23.14/3.34 (! [U] :( ssList(U)=> frontsegP(U,U) ) )),
% 23.14/3.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.14/3.34 fof(f49,axiom,(
% 23.14/3.34 (! [U] :( ssList(U)=> rearsegP(U,U) ) )),
% 23.14/3.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.14/3.34 fof(f55,axiom,(
% 23.14/3.34 (! [U] :( ssList(U)=> segmentP(U,U) ) )),
% 23.14/3.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.14/3.34 fof(f66,axiom,(
% 23.14/3.34 totalorderedP(nil) ),
% 23.14/3.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.14/3.34 fof(f89,axiom,(
% 23.14/3.34 (! [U] :( ssItem(U)=> geq(U,U) ) )),
% 23.14/3.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.14/3.34 fof(f93,axiom,(
% 23.14/3.34 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> ( lt(U,V)<=> ( U != V& leq(U,V) ) ) ) )) )),
% 23.14/3.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.14/3.34 fof(f96,conjecture,(
% 23.14/3.34 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ~ strictorderedP(W)| totalorderedP(U) ) )) )) )) )),
% 23.14/3.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.14/3.34 fof(f97,negated_conjecture,(
% 23.14/3.34 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ~ ssList(X)| V != X| U != W| ~ strictorderedP(W)| totalorderedP(U) ) )) )) )) ))),
% 23.14/3.34 inference(negated_conjecture,[status(cth)],[f96])).
% 23.14/3.34 fof(f102,plain,(
% 23.14/3.34 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 23.14/3.34 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 23.14/3.34 fof(f103,plain,(
% 23.14/3.34 ssItem(sK0_skl)),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f102])).
% 23.14/3.34 fof(f104,plain,(
% 23.14/3.34 ssItem(sK1_skl)),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f102])).
% 23.14/3.34 fof(f105,plain,(
% 23.14/3.34 ~sK0_skl=sK1_skl),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f102])).
% 23.14/3.34 fof(f174,plain,(
% 23.14/3.34 ![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))))))))))))))),
% 23.14/3.34 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 23.14/3.34 fof(f175,plain,(
% 23.14/3.34 ![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)))))))))))))))),
% 23.14/3.34 inference(NNF_transformation,[status(thm)],[f174])).
% 23.14/3.34 fof(f176,plain,(
% 23.14/3.34 ![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)))))))))))),
% 23.14/3.34 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])).
% 23.14/3.34 fof(f178,plain,(
% 23.14/3.34 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssItem(sK24_skl(X0)))),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f176])).
% 23.14/3.34 fof(f179,plain,(
% 23.14/3.34 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssItem(sK25_skl(X0)))),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f176])).
% 23.14/3.34 fof(f180,plain,(
% 23.14/3.34 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssList(sK26_skl(X0)))),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f176])).
% 23.14/3.34 fof(f181,plain,(
% 23.14/3.34 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssList(sK27_skl(X0)))),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f176])).
% 23.14/3.34 fof(f182,plain,(
% 23.14/3.34 ![X0]: (~ssList(X0)|totalorderedP(X0)|ssList(sK28_skl(X0)))),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f176])).
% 23.14/3.34 fof(f183,plain,(
% 23.14/3.34 ![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)),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f176])).
% 23.14/3.34 fof(f184,plain,(
% 23.14/3.34 ![X0]: (~ssList(X0)|totalorderedP(X0)|~leq(sK24_skl(X0),sK25_skl(X0)))),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f176])).
% 23.14/3.34 fof(f185,plain,(
% 23.14/3.34 ![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))))))))))))))),
% 23.14/3.34 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 23.14/3.34 fof(f186,plain,(
% 23.14/3.34 ![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)))))))))))))))),
% 23.14/3.34 inference(NNF_transformation,[status(thm)],[f185])).
% 23.14/3.34 fof(f187,plain,(
% 23.14/3.34 ![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)))))))))))),
% 23.14/3.34 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])).
% 23.14/3.34 fof(f188,plain,(
% 23.14/3.34 ![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))),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f187])).
% 23.14/3.34 fof(f223,plain,(
% 23.14/3.34 ssList(nil)),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f17])).
% 23.14/3.34 fof(f285,plain,(
% 23.14/3.34 ![U]: (~ssList(U)|frontsegP(U,U))),
% 23.14/3.34 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 23.14/3.34 fof(f286,plain,(
% 23.14/3.34 ![X0]: (~ssList(X0)|frontsegP(X0,X0))),
% 23.14/3.34 inference(cnf_transformation,[status(thm)],[f285])).
% 23.14/3.34 fof(f304,plain,(
% 23.14/3.34 ![U]: (~ssList(U)|rearsegP(U,U))),
% 23.14/3.34 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 23.14/3.35 fof(f305,plain,(
% 23.14/3.35 ![X0]: (~ssList(X0)|rearsegP(X0,X0))),
% 23.14/3.35 inference(cnf_transformation,[status(thm)],[f304])).
% 23.14/3.35 fof(f318,plain,(
% 23.14/3.35 ![U]: (~ssList(U)|segmentP(U,U))),
% 23.14/3.35 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 23.14/3.35 fof(f319,plain,(
% 23.14/3.35 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 23.14/3.35 inference(cnf_transformation,[status(thm)],[f318])).
% 23.14/3.35 fof(f339,plain,(
% 23.14/3.35 totalorderedP(nil)),
% 23.14/3.35 inference(cnf_transformation,[status(thm)],[f66])).
% 23.14/3.35 fof(f398,plain,(
% 23.14/3.35 ![U]: (~ssItem(U)|geq(U,U))),
% 23.14/3.35 inference(pre_NNF_transformation,[status(thm)],[f89])).
% 23.14/3.35 fof(f399,plain,(
% 23.14/3.35 ![X0]: (~ssItem(X0)|geq(X0,X0))),
% 23.14/3.35 inference(cnf_transformation,[status(thm)],[f398])).
% 23.14/3.35 fof(f406,plain,(
% 23.14/3.35 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(lt(U,V)<=>(~U=V&leq(U,V))))))),
% 23.14/3.35 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 23.14/3.35 fof(f407,plain,(
% 23.14/3.35 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|((~lt(U,V)|(~U=V&leq(U,V)))&(lt(U,V)|(U=V|~leq(U,V)))))))),
% 23.14/3.35 inference(NNF_transformation,[status(thm)],[f406])).
% 23.14/3.35 fof(f409,plain,(
% 23.14/3.35 ![X0,X1]: (~ssItem(X0)|~ssItem(X1)|~lt(X0,X1)|leq(X0,X1))),
% 23.14/3.35 inference(cnf_transformation,[status(thm)],[f407])).
% 23.14/3.35 fof(f415,plain,(
% 23.14/3.35 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: ((((ssList(X)&V=X)&U=W)&strictorderedP(W))&~totalorderedP(U)))))))))),
% 23.14/3.35 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 23.14/3.35 fof(f416,plain,(
% 23.14/3.35 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&((((?[X]: (ssList(X)&V=X))&U=W)&strictorderedP(W))&~totalorderedP(U)))))))),
% 23.14/3.35 inference(miniscoping,[status(thm)],[f415])).
% 23.14/3.35 fof(f417,plain,(
% 23.14/3.35 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&((((ssList(sK50_skl)&sK48_skl=sK50_skl)&sK47_skl=sK49_skl)&strictorderedP(sK49_skl))&~totalorderedP(sK47_skl)))))),
% 23.14/3.35 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])).
% 23.14/3.35 fof(f418,plain,(
% 23.14/3.35 ssList(sK47_skl)),
% 23.14/3.35 inference(cnf_transformation,[status(thm)],[f417])).
% 23.14/3.35 fof(f419,plain,(
% 23.14/3.35 ssList(sK48_skl)),
% 23.14/3.35 inference(cnf_transformation,[status(thm)],[f417])).
% 23.14/3.35 fof(f423,plain,(
% 23.14/3.35 sK47_skl=sK49_skl),
% 23.14/3.35 inference(cnf_transformation,[status(thm)],[f417])).
% 23.14/3.35 fof(f424,plain,(
% 23.14/3.35 strictorderedP(sK49_skl)),
% 23.14/3.35 inference(cnf_transformation,[status(thm)],[f417])).
% 23.14/3.35 fof(f425,plain,(
% 23.14/3.35 ~totalorderedP(sK47_skl)),
% 23.14/3.35 inference(cnf_transformation,[status(thm)],[f417])).
% 23.14/3.35 fof(f437,plain,(
% 23.14/3.35 ![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))),
% 23.14/3.35 inference(destructive_equality_resolution,[status(thm)],[f188])).
% 23.14/3.35 fof(f458,plain,(
% 23.14/3.35 strictorderedP(sK47_skl)),
% 23.14/3.35 inference(forward_demodulation,[status(thm)],[f423,f424])).
% 23.14/3.35 fof(f463,plain,(
% 23.14/3.35 geq(sK1_skl,sK1_skl)),
% 23.14/3.35 inference(resolution,[status(thm)],[f399,f104])).
% 23.14/3.35 fof(f464,plain,(
% 23.14/3.35 geq(sK0_skl,sK0_skl)),
% 23.14/3.35 inference(resolution,[status(thm)],[f399,f103])).
% 23.14/3.35 fof(f468,definition,(
% 23.14/3.35 sQ0_spl <=> (ssItem(sK0_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f470,plain,(
% 23.14/3.35 ~ssItem(sK0_skl)|sQ0_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f468])).
% 23.14/3.35 fof(f471,definition,(
% 23.14/3.35 sQ1_spl <=> (ssList(nil))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f473,plain,(
% 23.14/3.35 ~ssList(nil)|sQ1_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f471])).
% 23.14/3.35 fof(f487,definition,(
% 23.14/3.35 sQ5_spl <=> (ssItem(sK1_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f489,plain,(
% 23.14/3.35 ~ssItem(sK1_skl)|sQ5_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f487])).
% 23.14/3.35 fof(f712,plain,(
% 23.14/3.35 totalorderedP(sK47_skl)|ssItem(sK24_skl(sK47_skl))),
% 23.14/3.35 inference(resolution,[status(thm)],[f178,f418])).
% 23.14/3.35 fof(f720,definition,(
% 23.14/3.35 sQ54_spl <=> (totalorderedP(sK47_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f721,plain,(
% 23.14/3.35 totalorderedP(sK47_skl)|~sQ54_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f720])).
% 23.14/3.35 fof(f723,definition,(
% 23.14/3.35 sQ55_spl <=> (ssItem(sK24_skl(sK47_skl)))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f726,plain,(
% 23.14/3.35 sQ54_spl|sQ55_spl),
% 23.14/3.35 inference(split_clause,[status(thm)],[f712,f720,f723])).
% 23.14/3.35 fof(f727,plain,(
% 23.14/3.35 $false|~sQ54_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f721,f425])).
% 23.14/3.35 fof(f728,plain,(
% 23.14/3.35 ~sQ54_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f727])).
% 23.14/3.35 fof(f730,plain,(
% 23.14/3.35 totalorderedP(sK47_skl)|ssItem(sK25_skl(sK47_skl))),
% 23.14/3.35 inference(resolution,[status(thm)],[f179,f418])).
% 23.14/3.35 fof(f735,definition,(
% 23.14/3.35 sQ57_spl <=> (ssItem(sK25_skl(sK47_skl)))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f738,plain,(
% 23.14/3.35 sQ54_spl|sQ57_spl),
% 23.14/3.35 inference(split_clause,[status(thm)],[f730,f720,f735])).
% 23.14/3.35 fof(f740,plain,(
% 23.14/3.35 totalorderedP(sK47_skl)|ssList(sK26_skl(sK47_skl))),
% 23.14/3.35 inference(resolution,[status(thm)],[f180,f418])).
% 23.14/3.35 fof(f745,definition,(
% 23.14/3.35 sQ59_spl <=> (ssList(sK26_skl(sK47_skl)))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f748,plain,(
% 23.14/3.35 sQ54_spl|sQ59_spl),
% 23.14/3.35 inference(split_clause,[status(thm)],[f740,f720,f745])).
% 23.14/3.35 fof(f750,plain,(
% 23.14/3.35 totalorderedP(sK47_skl)|ssList(sK27_skl(sK47_skl))),
% 23.14/3.35 inference(resolution,[status(thm)],[f181,f418])).
% 23.14/3.35 fof(f755,definition,(
% 23.14/3.35 sQ61_spl <=> (ssList(sK27_skl(sK47_skl)))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f758,plain,(
% 23.14/3.35 sQ54_spl|sQ61_spl),
% 23.14/3.35 inference(split_clause,[status(thm)],[f750,f720,f755])).
% 23.14/3.35 fof(f760,plain,(
% 23.14/3.35 totalorderedP(sK47_skl)|ssList(sK28_skl(sK47_skl))),
% 23.14/3.35 inference(resolution,[status(thm)],[f182,f418])).
% 23.14/3.35 fof(f765,definition,(
% 23.14/3.35 sQ63_spl <=> (ssList(sK28_skl(sK47_skl)))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f768,plain,(
% 23.14/3.35 sQ54_spl|sQ63_spl),
% 23.14/3.35 inference(split_clause,[status(thm)],[f760,f720,f765])).
% 23.14/3.35 fof(f770,plain,(
% 23.14/3.35 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),
% 23.14/3.35 inference(resolution,[status(thm)],[f183,f418])).
% 23.14/3.35 fof(f775,definition,(
% 23.14/3.35 sQ65_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)),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f776,plain,(
% 23.14/3.35 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|~sQ65_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f775])).
% 23.14/3.35 fof(f778,plain,(
% 23.14/3.35 sQ54_spl|sQ65_spl),
% 23.14/3.35 inference(split_clause,[status(thm)],[f770,f720,f775])).
% 23.14/3.35 fof(f788,definition,(
% 23.14/3.35 sQ68_spl <=> (strictorderedP(sK47_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f790,plain,(
% 23.14/3.35 ~strictorderedP(sK47_skl)|sQ68_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f788])).
% 23.14/3.35 fof(f1331,plain,(
% 23.14/3.35 ~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))|~sQ65_spl),
% 23.14/3.35 inference(paramodulation,[status(thm)],[f776,f437])).
% 23.14/3.35 fof(f1343,definition,(
% 23.14/3.35 sQ181_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)))))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f1345,plain,(
% 23.14/3.35 ~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))))|sQ181_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f1343])).
% 23.14/3.35 fof(f1346,definition,(
% 23.14/3.35 sQ182_spl <=> (lt(sK24_skl(sK47_skl),sK25_skl(sK47_skl)))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f1347,plain,(
% 23.14/3.35 lt(sK24_skl(sK47_skl),sK25_skl(sK47_skl))|~sQ182_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f1346])).
% 23.14/3.35 fof(f1353,definition,(
% 23.14/3.35 sQ184_spl <=> (leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl)))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f1354,plain,(
% 23.14/3.35 leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl))|~sQ184_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f1353])).
% 23.14/3.35 fof(f1361,plain,(
% 23.14/3.35 ~sQ181_spl|~sQ68_spl|~sQ55_spl|~sQ57_spl|~sQ59_spl|~sQ61_spl|~sQ63_spl|sQ182_spl|~sQ65_spl),
% 23.14/3.35 inference(split_clause,[status(thm)],[f1331,f1343,f788,f723,f735,f745,f755,f765,f1346,f775])).
% 23.14/3.35 fof(f1363,definition,(
% 23.14/3.35 sQ186_spl <=> (ssList(sK47_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f1365,plain,(
% 23.14/3.35 ~ssList(sK47_skl)|sQ186_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f1363])).
% 23.14/3.35 fof(f1415,plain,(
% 23.14/3.35 ~ssList(sK47_skl)|~sQ65_spl|sQ181_spl),
% 23.14/3.35 inference(forward_demodulation,[status(thm)],[f776,f1345])).
% 23.14/3.35 fof(f1416,plain,(
% 23.14/3.35 $false|~sQ65_spl|sQ181_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f1415,f418])).
% 23.14/3.35 fof(f1417,plain,(
% 23.14/3.35 ~sQ65_spl|sQ181_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f1416])).
% 23.14/3.35 fof(f1418,plain,(
% 23.14/3.35 $false|sQ186_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f1365,f418])).
% 23.14/3.35 fof(f1419,plain,(
% 23.14/3.35 sQ186_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f1418])).
% 23.14/3.35 fof(f1421,plain,(
% 23.14/3.35 $false|sQ68_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f790,f458])).
% 23.14/3.35 fof(f1422,plain,(
% 23.14/3.35 sQ68_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f1421])).
% 23.14/3.35 fof(f2894,definition,(
% 23.14/3.35 ![X0]: (sQ506_spl <=> (~ssList(X0)|~ssList(X0)))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ506_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f2895,plain,(
% 23.14/3.35 ![X0]: (~ssList(X0)|~ssList(X0)|~sQ506_spl)),
% 23.14/3.35 inference(component_clause,[status(thm)],[f2894])).
% 23.14/3.35 fof(f2901,plain,(
% 23.14/3.35 ![X0]: (~ssList(X0)|~sQ506_spl)),
% 23.14/3.35 inference(duplicate_literals_removal,[status(thm)],[f2895])).
% 23.14/3.35 fof(f2902,plain,(
% 23.14/3.35 $false|~sQ506_spl),
% 23.14/3.35 inference(backward_subsumption_resolution,[status(thm)],[f223,f2901])).
% 23.14/3.35 fof(f2911,plain,(
% 23.14/3.35 ~sQ506_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f2902])).
% 23.14/3.35 fof(f2922,definition,(
% 23.14/3.35 sQ510_spl <=> (nil=sK47_skl)),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ510_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f2923,plain,(
% 23.14/3.35 nil=sK47_skl|~sQ510_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f2922])).
% 23.14/3.35 fof(f2969,plain,(
% 23.14/3.35 $false|sQ5_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f489,f104])).
% 23.14/3.35 fof(f2970,plain,(
% 23.14/3.35 sQ5_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f2969])).
% 23.14/3.35 fof(f2971,plain,(
% 23.14/3.35 $false|sQ0_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f470,f103])).
% 23.14/3.35 fof(f2972,plain,(
% 23.14/3.35 sQ0_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f2971])).
% 23.14/3.35 fof(f3081,plain,(
% 23.14/3.35 frontsegP(sK48_skl,sK48_skl)),
% 23.14/3.35 inference(resolution,[status(thm)],[f286,f419])).
% 23.14/3.35 fof(f3152,plain,(
% 23.14/3.35 rearsegP(sK48_skl,sK48_skl)),
% 23.14/3.35 inference(resolution,[status(thm)],[f305,f419])).
% 23.14/3.35 fof(f3214,plain,(
% 23.14/3.35 segmentP(sK48_skl,sK48_skl)),
% 23.14/3.35 inference(resolution,[status(thm)],[f319,f419])).
% 23.14/3.35 fof(f3683,plain,(
% 23.14/3.35 ~totalorderedP(nil)|~sQ510_spl),
% 23.14/3.35 inference(backward_demodulation,[status(thm)],[f2923,f425])).
% 23.14/3.35 fof(f3699,plain,(
% 23.14/3.35 $false|~sQ510_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f3683,f339])).
% 23.14/3.35 fof(f3700,plain,(
% 23.14/3.35 ~sQ510_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f3699])).
% 23.14/3.35 fof(f3706,plain,(
% 23.14/3.35 segmentP(sK47_skl,sK47_skl)),
% 23.14/3.35 inference(resolution,[status(thm)],[f418,f319])).
% 23.14/3.35 fof(f3709,plain,(
% 23.14/3.35 rearsegP(sK47_skl,sK47_skl)),
% 23.14/3.35 inference(resolution,[status(thm)],[f418,f305])).
% 23.14/3.35 fof(f3712,plain,(
% 23.14/3.35 frontsegP(sK47_skl,sK47_skl)),
% 23.14/3.35 inference(resolution,[status(thm)],[f418,f286])).
% 23.14/3.35 fof(f4181,definition,(
% 23.14/3.35 ![X1]: (sQ680_spl <=> (~ssList(X1)))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ680_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f4182,plain,(
% 23.14/3.35 ![X0]: (~ssList(X0)|~sQ680_spl)),
% 23.14/3.35 inference(component_clause,[status(thm)],[f4181])).
% 23.14/3.35 fof(f4185,plain,(
% 23.14/3.35 $false|~sQ680_spl),
% 23.14/3.35 inference(backward_subsumption_resolution,[status(thm)],[f418,f4182])).
% 23.14/3.35 fof(f4187,plain,(
% 23.14/3.35 ~sQ680_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f4185])).
% 23.14/3.35 fof(f4273,definition,(
% 23.14/3.35 sQ682_spl <=> (ssList(sK48_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ682_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f4275,plain,(
% 23.14/3.35 ~ssList(sK48_skl)|sQ682_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f4273])).
% 23.14/3.35 fof(f4283,plain,(
% 23.14/3.35 $false|sQ682_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f4275,f419])).
% 23.14/3.35 fof(f4284,plain,(
% 23.14/3.35 sQ682_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f4283])).
% 23.14/3.35 fof(f4312,definition,(
% 23.14/3.35 sQ685_spl <=> (geq(sK1_skl,sK1_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ685_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f4314,plain,(
% 23.14/3.35 ~geq(sK1_skl,sK1_skl)|sQ685_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f4312])).
% 23.14/3.35 fof(f4323,plain,(
% 23.14/3.35 $false|sQ685_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f4314,f463])).
% 23.14/3.35 fof(f4324,plain,(
% 23.14/3.35 sQ685_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f4323])).
% 23.14/3.35 fof(f4466,plain,(
% 23.14/3.35 ~ssItem(sK24_skl(sK47_skl))|~ssItem(sK25_skl(sK47_skl))|leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl))|~sQ182_spl),
% 23.14/3.35 inference(resolution,[status(thm)],[f1347,f409])).
% 23.14/3.35 fof(f4471,plain,(
% 23.14/3.35 ~sQ55_spl|~sQ57_spl|sQ184_spl|~sQ182_spl),
% 23.14/3.35 inference(split_clause,[status(thm)],[f4466,f723,f735,f1353,f1346])).
% 23.14/3.35 fof(f4510,definition,(
% 23.14/3.35 sQ713_spl <=> (geq(sK0_skl,sK0_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ713_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f4512,plain,(
% 23.14/3.35 ~geq(sK0_skl,sK0_skl)|sQ713_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f4510])).
% 23.14/3.35 fof(f4521,plain,(
% 23.14/3.35 $false|sQ713_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f4512,f464])).
% 23.14/3.35 fof(f4522,plain,(
% 23.14/3.35 sQ713_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f4521])).
% 23.14/3.35 fof(f4548,definition,(
% 23.14/3.35 sQ722_spl <=> (sK1_skl=sK0_skl)),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ722_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f4549,plain,(
% 23.14/3.35 sK1_skl=sK0_skl|~sQ722_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f4548])).
% 23.14/3.35 fof(f4552,plain,(
% 23.14/3.35 $false|~sQ722_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f4549,f105])).
% 23.14/3.35 fof(f4553,plain,(
% 23.14/3.35 ~sQ722_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f4552])).
% 23.14/3.35 fof(f9467,definition,(
% 23.14/3.35 sQ1530_spl <=> (segmentP(sK48_skl,sK48_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ1530_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f9469,plain,(
% 23.14/3.35 ~segmentP(sK48_skl,sK48_skl)|sQ1530_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f9467])).
% 23.14/3.35 fof(f9471,plain,(
% 23.14/3.35 $false|sQ1530_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f9469,f3214])).
% 23.14/3.35 fof(f9472,plain,(
% 23.14/3.35 sQ1530_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f9471])).
% 23.14/3.35 fof(f11456,plain,(
% 23.14/3.35 $false|sQ1_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f473,f223])).
% 23.14/3.35 fof(f11457,plain,(
% 23.14/3.35 sQ1_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f11456])).
% 23.14/3.35 fof(f11464,definition,(
% 23.14/3.35 sQ1903_spl <=> (rearsegP(sK48_skl,sK48_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ1903_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f11466,plain,(
% 23.14/3.35 ~rearsegP(sK48_skl,sK48_skl)|sQ1903_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f11464])).
% 23.14/3.35 fof(f11468,plain,(
% 23.14/3.35 $false|sQ1903_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f11466,f3152])).
% 23.14/3.35 fof(f11469,plain,(
% 23.14/3.35 sQ1903_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f11468])).
% 23.14/3.35 fof(f13032,definition,(
% 23.14/3.35 sQ2165_spl <=> (frontsegP(sK48_skl,sK48_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ2165_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f13034,plain,(
% 23.14/3.35 ~frontsegP(sK48_skl,sK48_skl)|sQ2165_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f13032])).
% 23.14/3.35 fof(f13036,plain,(
% 23.14/3.35 $false|sQ2165_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f13034,f3081])).
% 23.14/3.35 fof(f13037,plain,(
% 23.14/3.35 sQ2165_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f13036])).
% 23.14/3.35 fof(f13207,definition,(
% 23.14/3.35 sQ2184_spl <=> (segmentP(sK47_skl,sK47_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ2184_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f13209,plain,(
% 23.14/3.35 ~segmentP(sK47_skl,sK47_skl)|sQ2184_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f13207])).
% 23.14/3.35 fof(f13214,plain,(
% 23.14/3.35 $false|sQ2184_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f13209,f3706])).
% 23.14/3.35 fof(f13215,plain,(
% 23.14/3.35 sQ2184_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f13214])).
% 23.14/3.35 fof(f13249,definition,(
% 23.14/3.35 sQ2188_spl <=> (rearsegP(sK47_skl,sK47_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ2188_spl])],[split_symbol_definition])).
% 23.14/3.35 fof(f13251,plain,(
% 23.14/3.35 ~rearsegP(sK47_skl,sK47_skl)|sQ2188_spl),
% 23.14/3.35 inference(component_clause,[status(thm)],[f13249])).
% 23.14/3.35 fof(f13256,plain,(
% 23.14/3.35 $false|sQ2188_spl),
% 23.14/3.35 inference(forward_subsumption_resolution,[status(thm)],[f13251,f3709])).
% 23.14/3.35 fof(f13257,plain,(
% 23.14/3.35 sQ2188_spl),
% 23.14/3.35 inference(contradiction_clause,[status(thm)],[f13256])).
% 23.14/3.35 fof(f13303,definition,(
% 23.14/3.35 sQ2194_spl <=> (frontsegP(sK47_skl,sK47_skl))),
% 23.14/3.35 introduced(definition,[new_symbols(definition,[sQ2194_spl])],[split_symbol_definition])).
% 23.14/3.37 fof(f13305,plain,(
% 23.14/3.37 ~frontsegP(sK47_skl,sK47_skl)|sQ2194_spl),
% 23.14/3.37 inference(component_clause,[status(thm)],[f13303])).
% 23.14/3.37 fof(f13318,plain,(
% 23.14/3.37 $false|sQ2194_spl),
% 23.14/3.37 inference(forward_subsumption_resolution,[status(thm)],[f13305,f3712])).
% 23.14/3.37 fof(f13319,plain,(
% 23.14/3.37 sQ2194_spl),
% 23.14/3.37 inference(contradiction_clause,[status(thm)],[f13318])).
% 23.14/3.37 fof(f14804,plain,(
% 23.14/3.37 ~ssList(sK47_skl)|totalorderedP(sK47_skl)|~sQ184_spl),
% 23.14/3.37 inference(resolution,[status(thm)],[f1354,f184])).
% 23.14/3.37 fof(f14809,plain,(
% 23.14/3.37 ~sQ186_spl|sQ54_spl|~sQ184_spl),
% 23.14/3.37 inference(split_clause,[status(thm)],[f14804,f1363,f720,f1353])).
% 23.14/3.37 fof(f14820,plain,(
% 23.14/3.37 $false),
% 23.14/3.37 inference(sat_refutation,[status(thm)],[f726,f728,f738,f748,f758,f768,f778,f1361,f1417,f1419,f1422,f2911,f2970,f2972,f3700,f4187,f4284,f4324,f4471,f4522,f4553,f9472,f11457,f11469,f13037,f13215,f13257,f13319,f14809])).
% 23.14/3.37 % SZS output end CNFRefutation for theBenchmark.p
% 23.14/3.39 % Elapsed time: 3.015080 seconds
% 23.14/3.39 % CPU time: 23.672089 seconds
% 23.14/3.39 % Total memory used: 340.419 MB
% 23.14/3.39 % Net memory used: 325.241 MB
%------------------------------------------------------------------------------