%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC030+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:41:23 PM UTC 2026
% Result : Theorem 0.15s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC030+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.08/0.36 % Computer : n019.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 07:50:21 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.15/0.37 % Drodi V4.1.1
% 0.15/0.50 % Refutation found
% 0.15/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.50 fof(f2,axiom,(
% 0.15/0.50 (? [U] :( ssItem(U)& (? [V] :( ssItem(V)& U != V ) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f5,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f6,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( rearsegP(U,V)<=> (? [W] :( ssList(W)& app(W,V) = U ) )) ) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f7,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( segmentP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(app(W,V),X) = U ) )) )) ) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f17,axiom,(
% 0.15/0.50 ssList(nil) ),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f26,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ssList(app(U,V)) ) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f28,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f42,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> frontsegP(U,U) ) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f45,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> frontsegP(U,nil) ) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f51,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> rearsegP(U,nil) ) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f57,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> segmentP(U,nil) ) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f79,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( app(W,V) = app(U,V)=> W = U ) ) )) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f80,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( app(V,W) = app(V,U)=> W = U ) ) )) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f83,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( nil = app(U,V)<=> ( nil = V& nil = U ) ) ) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f84,axiom,(
% 0.15/0.50 (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f96,conjecture,(
% 0.15/0.50 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(Y,Z) != X| app(Z,Y) != W ) ) )))| ( ( nil != V| nil = U )& ( nil != U| nil = V ) ) ) ) )) )) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f97,negated_conjecture,(
% 0.15/0.50 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (! [Y] :( ssList(Y)=> (! [Z] :( ssList(Z)=> ( app(Y,Z) != X| app(Z,Y) != W ) ) )))| ( ( nil != V| nil = U )& ( nil != U| nil = V ) ) ) ) )) )) )) ))),
% 0.15/0.50 inference(negated_conjecture,[status(cth)],[f96])).
% 0.15/0.50 fof(f102,plain,(
% 0.15/0.50 (ssItem(sK0_skl)&(ssItem(sK1_skl)&~sK0_skl=sK1_skl))),
% 0.15/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2])).
% 0.15/0.50 fof(f105,plain,(
% 0.15/0.50 ~sK0_skl=sK1_skl),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f102])).
% 0.15/0.50 fof(f119,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.15/0.50 fof(f120,plain,(
% 0.15/0.50 ![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)))))))),
% 0.15/0.50 inference(NNF_transformation,[status(thm)],[f119])).
% 0.15/0.50 fof(f121,plain,(
% 0.15/0.50 ![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)))))))),
% 0.15/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 0.15/0.50 fof(f122,plain,(
% 0.15/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|ssList(sK5_skl(X1,X0)))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f121])).
% 0.15/0.50 fof(f123,plain,(
% 0.15/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(X1,sK5_skl(X1,X0))=X0)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f121])).
% 0.15/0.50 fof(f125,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(rearsegP(U,V)<=>(?[W]: (ssList(W)&app(W,V)=U))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.15/0.50 fof(f126,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~rearsegP(U,V)|(?[W]: (ssList(W)&app(W,V)=U)))&(rearsegP(U,V)|(![W]: (~ssList(W)|~app(W,V)=U)))))))),
% 0.15/0.50 inference(NNF_transformation,[status(thm)],[f125])).
% 0.15/0.50 fof(f127,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~rearsegP(U,V)|(ssList(sK6_skl(V,U))&app(sK6_skl(V,U),V)=U))&(rearsegP(U,V)|(![W]: (~ssList(W)|~app(W,V)=U)))))))),
% 0.15/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W,sK6_skl(V,U))],[f126])).
% 0.15/0.50 fof(f128,plain,(
% 0.15/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|ssList(sK6_skl(X1,X0)))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f127])).
% 0.15/0.50 fof(f129,plain,(
% 0.15/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|app(sK6_skl(X1,X0),X1)=X0)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f127])).
% 0.15/0.50 fof(f131,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(segmentP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U))))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.15/0.50 fof(f132,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U)))))&(segmentP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(app(W,V),X)=U)))))))))),
% 0.15/0.50 inference(NNF_transformation,[status(thm)],[f131])).
% 0.15/0.50 fof(f133,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~segmentP(U,V)|(ssList(sK7_skl(V,U))&(ssList(sK8_skl(V,U))&app(app(sK7_skl(V,U),V),sK8_skl(V,U))=U)))&(segmentP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(app(W,V),X)=U)))))))))),
% 0.15/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(W,sK7_skl(V,U)),skolemize(X,sK8_skl(V,U))],[f132])).
% 0.15/0.50 fof(f134,plain,(
% 0.15/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK7_skl(X1,X0)))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f133])).
% 0.15/0.50 fof(f135,plain,(
% 0.15/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK8_skl(X1,X0)))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f133])).
% 0.15/0.50 fof(f136,plain,(
% 0.15/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|app(app(sK7_skl(X1,X0),X1),sK8_skl(X1,X0))=X0)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f133])).
% 0.15/0.50 fof(f137,plain,(
% 0.15/0.50 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(app(X2,X1),X3)=X0)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f133])).
% 0.15/0.50 fof(f223,plain,(
% 0.15/0.50 ssList(nil)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f17])).
% 0.15/0.50 fof(f244,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|ssList(app(U,V)))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.15/0.50 fof(f245,plain,(
% 0.15/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X0,X1)))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f244])).
% 0.15/0.50 fof(f248,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|app(nil,U)=U)),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.15/0.50 fof(f249,plain,(
% 0.15/0.50 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f248])).
% 0.15/0.50 fof(f285,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|frontsegP(U,U))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.15/0.50 fof(f286,plain,(
% 0.15/0.50 ![X0]: (~ssList(X0)|frontsegP(X0,X0))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f285])).
% 0.15/0.50 fof(f294,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|frontsegP(U,nil))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.15/0.50 fof(f295,plain,(
% 0.15/0.50 ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f294])).
% 0.15/0.50 fof(f308,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|rearsegP(U,nil))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.15/0.50 fof(f309,plain,(
% 0.15/0.50 ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f308])).
% 0.15/0.50 fof(f322,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|segmentP(U,nil))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.15/0.50 fof(f323,plain,(
% 0.15/0.50 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f322])).
% 0.15/0.50 fof(f375,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(~app(W,V)=app(U,V)|W=U))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 0.15/0.50 fof(f376,plain,(
% 0.15/0.50 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~app(X2,X1)=app(X0,X1)|X2=X0)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f375])).
% 0.15/0.50 fof(f377,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(~app(V,W)=app(V,U)|W=U))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f80])).
% 0.15/0.50 fof(f378,plain,(
% 0.15/0.50 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~app(X1,X2)=app(X1,X0)|X2=X0)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f377])).
% 0.15/0.50 fof(f383,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(nil=app(U,V)<=>(nil=V&nil=U)))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 0.15/0.50 fof(f384,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~nil=app(U,V)|(nil=V&nil=U))&(nil=app(U,V)|(~nil=V|~nil=U))))))),
% 0.15/0.50 inference(NNF_transformation,[status(thm)],[f383])).
% 0.15/0.50 fof(f385,plain,(
% 0.15/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~nil=app(X0,X1)|nil=X1)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f384])).
% 0.15/0.50 fof(f388,plain,(
% 0.15/0.50 ![U]: (~ssList(U)|app(U,nil)=U)),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 0.15/0.50 fof(f389,plain,(
% 0.15/0.50 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f388])).
% 0.15/0.50 fof(f415,plain,(
% 0.15/0.50 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((V=X&U=W)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(Y,Z)=X&app(Z,Y)=W))))))&((nil=V&~nil=U)|(nil=U&~nil=V)))))))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.15/0.50 fof(f416,definition,(
% 0.15/0.50 ![U,V]: (sP0_prd(V,U)<=>(nil=V&~nil=U))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.15/0.50 fof(f417,plain,(
% 0.15/0.50 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((V=X&U=W)&(?[Y]: (ssList(Y)&(?[Z]: (ssList(Z)&(app(Y,Z)=X&app(Z,Y)=W))))))&(sP0_prd(V,U)|(nil=U&~nil=V))))))))))),
% 0.15/0.50 inference(formula_renaming,[status(thm)],[f415,f416])).
% 0.15/0.50 fof(f418,plain,(
% 0.15/0.50 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(ssList(sK50_skl)&(((sK48_skl=sK50_skl&sK47_skl=sK49_skl)&(ssList(sK51_skl)&(ssList(sK52_skl)&(app(sK51_skl,sK52_skl)=sK50_skl&app(sK52_skl,sK51_skl)=sK49_skl))))&(sP0_prd(sK48_skl,sK47_skl)|(nil=sK47_skl&~nil=sK48_skl)))))))),
% 0.15/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Y,sK51_skl),skolemize(Z,sK52_skl)],[f417])).
% 0.15/0.50 fof(f421,plain,(
% 0.15/0.50 ssList(sK49_skl)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f418])).
% 0.15/0.50 fof(f423,plain,(
% 0.15/0.50 sK48_skl=sK50_skl),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f418])).
% 0.15/0.50 fof(f424,plain,(
% 0.15/0.50 sK47_skl=sK49_skl),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f418])).
% 0.15/0.50 fof(f425,plain,(
% 0.15/0.50 ssList(sK51_skl)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f418])).
% 0.15/0.50 fof(f426,plain,(
% 0.15/0.50 ssList(sK52_skl)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f418])).
% 0.15/0.50 fof(f427,plain,(
% 0.15/0.50 app(sK51_skl,sK52_skl)=sK50_skl),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f418])).
% 0.15/0.50 fof(f428,plain,(
% 0.15/0.50 app(sK52_skl,sK51_skl)=sK49_skl),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f418])).
% 0.15/0.50 fof(f429,plain,(
% 0.15/0.50 sP0_prd(sK48_skl,sK47_skl)|nil=sK47_skl),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f418])).
% 0.15/0.50 fof(f430,plain,(
% 0.15/0.50 sP0_prd(sK48_skl,sK47_skl)|~nil=sK48_skl),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f418])).
% 0.15/0.50 fof(f431,plain,(
% 0.15/0.50 ![U,V]: ((~sP0_prd(V,U)|(nil=V&~nil=U))&(sP0_prd(V,U)|(~nil=V|nil=U)))),
% 0.15/0.50 inference(NNF_transformation,[status(thm)],[f416])).
% 0.15/0.50 fof(f432,plain,(
% 0.15/0.50 (![U,V]: (~sP0_prd(V,U)|(nil=V&~nil=U)))&(![U,V]: (sP0_prd(V,U)|(~nil=V|nil=U)))),
% 0.15/0.50 inference(miniscoping,[status(thm)],[f431])).
% 0.15/0.50 fof(f433,plain,(
% 0.15/0.50 ![X0,X1]: (~sP0_prd(X0,X1)|nil=X0)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f432])).
% 0.15/0.50 fof(f434,plain,(
% 0.15/0.50 ![X0,X1]: (~sP0_prd(X0,X1)|~nil=X1)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f432])).
% 0.15/0.50 fof(f435,plain,(
% 0.15/0.50 ![X0,X1]: (sP0_prd(X0,X1)|~nil=X0|nil=X1)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f432])).
% 0.15/0.50 fof(f436,definition,(
% 0.15/0.50 sQ0_spl <=> (sP0_prd(sK48_skl,sK47_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f437,plain,(
% 0.15/0.50 sP0_prd(sK48_skl,sK47_skl)|~sQ0_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f436])).
% 0.15/0.50 fof(f439,definition,(
% 0.15/0.50 sQ1_spl <=> (nil=sK47_skl)),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f440,plain,(
% 0.15/0.50 nil=sK47_skl|~sQ1_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f439])).
% 0.15/0.50 fof(f442,plain,(
% 0.15/0.50 sQ0_spl|sQ1_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f429,f436,f439])).
% 0.15/0.50 fof(f443,definition,(
% 0.15/0.50 sQ2_spl <=> (nil=sK48_skl)),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f445,plain,(
% 0.15/0.50 ~nil=sK48_skl|sQ2_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f443])).
% 0.15/0.50 fof(f446,plain,(
% 0.15/0.50 sQ0_spl|~sQ2_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f430,f436,f443])).
% 0.15/0.50 fof(f453,plain,(
% 0.15/0.50 ![X0,X1,X2]: (~ssList(app(app(X0,X1),X2))|~ssList(X1)|segmentP(app(app(X0,X1),X2),X1)|~ssList(X0)|~ssList(X2))),
% 0.15/0.50 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 0.15/0.50 fof(f477,plain,(
% 0.15/0.50 ![X0]: (~sP0_prd(X0,nil))),
% 0.15/0.50 inference(destructive_equality_resolution,[status(thm)],[f434])).
% 0.15/0.50 fof(f478,plain,(
% 0.15/0.50 ![X0]: (sP0_prd(nil,X0)|nil=X0)),
% 0.15/0.50 inference(destructive_equality_resolution,[status(thm)],[f435])).
% 0.15/0.50 fof(f484,plain,(
% 0.15/0.50 sP0_prd(sK50_skl,sK47_skl)|~sQ0_spl),
% 0.15/0.50 inference(forward_demodulation,[status(thm)],[f423,f437])).
% 0.15/0.50 fof(f485,plain,(
% 0.15/0.50 sP0_prd(sK50_skl,sK49_skl)|~sQ0_spl),
% 0.15/0.50 inference(forward_demodulation,[status(thm)],[f424,f484])).
% 0.15/0.50 fof(f486,plain,(
% 0.15/0.50 nil=sK50_skl|~sQ0_spl),
% 0.15/0.50 inference(resolution,[status(thm)],[f433,f485])).
% 0.15/0.50 fof(f487,plain,(
% 0.15/0.50 sP0_prd(nil,sK49_skl)|~sQ0_spl),
% 0.15/0.50 inference(backward_demodulation,[status(thm)],[f486,f485])).
% 0.15/0.50 fof(f492,definition,(
% 0.15/0.50 sQ3_spl <=> (ssList(sK51_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f494,plain,(
% 0.15/0.50 ~ssList(sK51_skl)|sQ3_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f492])).
% 0.15/0.50 fof(f495,definition,(
% 0.15/0.50 sQ4_spl <=> (ssList(sK52_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f497,plain,(
% 0.15/0.50 ~ssList(sK52_skl)|sQ4_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f495])).
% 0.15/0.50 fof(f498,definition,(
% 0.15/0.50 sQ5_spl <=> (ssList(nil))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f500,plain,(
% 0.15/0.50 ~ssList(nil)|sQ5_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f498])).
% 0.15/0.50 fof(f503,plain,(
% 0.15/0.50 ~ssList(sK52_skl)|~ssList(sK51_skl)|ssList(sK49_skl)),
% 0.15/0.50 inference(paramodulation,[status(thm)],[f428,f245])).
% 0.15/0.50 fof(f504,definition,(
% 0.15/0.50 sQ6_spl <=> (ssList(sK49_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f507,plain,(
% 0.15/0.50 ~sQ4_spl|~sQ3_spl|sQ6_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f503,f495,f492,f504])).
% 0.15/0.50 fof(f508,plain,(
% 0.15/0.50 $false|sQ3_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f494,f425])).
% 0.15/0.50 fof(f509,plain,(
% 0.15/0.50 sQ3_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f508])).
% 0.15/0.50 fof(f510,plain,(
% 0.15/0.50 $false|sQ4_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f497,f426])).
% 0.15/0.50 fof(f511,plain,(
% 0.15/0.50 sQ4_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f510])).
% 0.15/0.50 fof(f513,plain,(
% 0.15/0.50 ![X0]: (nil=X0|nil=nil)),
% 0.15/0.50 inference(resolution,[status(thm)],[f478,f433])).
% 0.15/0.50 fof(f514,definition,(
% 0.15/0.50 ![X0]: (sQ7_spl <=> (nil=X0))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f515,plain,(
% 0.15/0.50 ![X0]: (nil=X0|~sQ7_spl)),
% 0.15/0.50 inference(component_clause,[status(thm)],[f514])).
% 0.15/0.50 fof(f517,definition,(
% 0.15/0.50 sQ8_spl <=> (nil=nil)),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f520,plain,(
% 0.15/0.50 sQ7_spl|sQ8_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f513,f514,f517])).
% 0.15/0.50 fof(f521,plain,(
% 0.15/0.50 ![X0,X1]: (X0=X1|~sQ7_spl)),
% 0.15/0.50 inference(paramodulation,[status(thm)],[f515,f515])).
% 0.15/0.51 fof(f531,plain,(
% 0.15/0.51 $false|~sQ7_spl),
% 0.15/0.51 inference(backward_subsumption_resolution,[status(thm)],[f105,f521])).
% 0.15/0.51 fof(f532,plain,(
% 0.15/0.51 ~sQ7_spl),
% 0.15/0.51 inference(contradiction_clause,[status(thm)],[f531])).
% 0.15/0.51 fof(f535,plain,(
% 0.15/0.51 app(nil,sK52_skl)=sK52_skl),
% 0.15/0.51 inference(resolution,[status(thm)],[f249,f426])).
% 0.15/0.51 fof(f536,plain,(
% 0.15/0.51 app(nil,sK51_skl)=sK51_skl),
% 0.15/0.51 inference(resolution,[status(thm)],[f249,f425])).
% 0.15/0.51 fof(f537,plain,(
% 0.15/0.51 app(nil,nil)=nil),
% 0.15/0.51 inference(resolution,[status(thm)],[f249,f223])).
% 0.15/0.51 fof(f538,plain,(
% 0.15/0.51 app(nil,sK49_skl)=sK49_skl),
% 0.15/0.51 inference(resolution,[status(thm)],[f249,f421])).
% 0.15/0.51 fof(f550,plain,(
% 0.15/0.51 ![X0]: (~ssList(sK52_skl)|~ssList(sK51_skl)|~ssList(X0)|~app(X0,sK51_skl)=sK49_skl|X0=sK52_skl)),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f428,f376])).
% 0.15/0.51 fof(f553,definition,(
% 0.15/0.51 ![X0]: (sQ11_spl <=> (~ssList(X0)|~app(X0,sK51_skl)=sK49_skl|X0=sK52_skl))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f554,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~app(X0,sK51_skl)=sK49_skl|X0=sK52_skl|~sQ11_spl)),
% 0.15/0.51 inference(component_clause,[status(thm)],[f553])).
% 0.15/0.51 fof(f556,plain,(
% 0.15/0.51 ~sQ4_spl|~sQ3_spl|sQ11_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f550,f495,f492,f553])).
% 0.15/0.51 fof(f571,plain,(
% 0.15/0.51 nil=sK49_skl|~sQ1_spl),
% 0.15/0.51 inference(backward_demodulation,[status(thm)],[f440,f424])).
% 0.15/0.51 fof(f572,plain,(
% 0.15/0.51 ~nil=sK50_skl|sQ2_spl),
% 0.15/0.51 inference(backward_demodulation,[status(thm)],[f423,f445])).
% 0.15/0.51 fof(f582,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~app(sK52_skl,sK52_skl)=app(sK52_skl,X0)|sK52_skl=X0)),
% 0.15/0.51 inference(resolution,[status(thm)],[f378,f426])).
% 0.15/0.51 fof(f584,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~app(sK51_skl,sK51_skl)=app(sK51_skl,X0)|sK51_skl=X0)),
% 0.15/0.51 inference(resolution,[status(thm)],[f378,f425])).
% 0.15/0.51 fof(f596,plain,(
% 0.15/0.51 ![X0]: (~ssList(nil)|~ssList(sK52_skl)|~ssList(X0)|~app(X0,sK52_skl)=sK52_skl|X0=nil)),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f535,f376])).
% 0.15/0.51 fof(f599,definition,(
% 0.15/0.51 ![X0]: (sQ13_spl <=> (~ssList(X0)|~app(X0,sK52_skl)=sK52_skl|X0=nil))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f602,plain,(
% 0.15/0.51 ~sQ5_spl|~sQ4_spl|sQ13_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f596,f498,f495,f599])).
% 0.15/0.51 fof(f605,plain,(
% 0.15/0.51 ![X0]: (~ssList(nil)|~ssList(sK51_skl)|~ssList(X0)|~app(X0,sK51_skl)=sK51_skl|X0=nil)),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f536,f376])).
% 0.15/0.51 fof(f608,definition,(
% 0.15/0.51 ![X0]: (sQ14_spl <=> (~ssList(X0)|~app(X0,sK51_skl)=sK51_skl|X0=nil))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f611,plain,(
% 0.15/0.51 ~sQ5_spl|~sQ3_spl|sQ14_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f605,f498,f492,f608])).
% 0.15/0.51 fof(f619,definition,(
% 0.15/0.51 ![X0]: (sQ15_spl <=> (~ssList(X0)|~app(X0,nil)=nil|X0=nil))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f625,plain,(
% 0.15/0.51 ![X0]: (~ssList(sK51_skl)|~ssList(sK52_skl)|~ssList(X0)|~app(X0,sK52_skl)=sK50_skl|X0=sK51_skl)),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f427,f376])).
% 0.15/0.51 fof(f627,plain,(
% 0.15/0.51 ~ssList(sK51_skl)|~ssList(sK52_skl)|ssList(sK50_skl)),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f427,f245])).
% 0.15/0.51 fof(f628,definition,(
% 0.15/0.51 ![X0]: (sQ16_spl <=> (~ssList(X0)|~app(X0,sK52_skl)=sK50_skl|X0=sK51_skl))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f631,plain,(
% 0.15/0.51 ~sQ3_spl|~sQ4_spl|sQ16_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f625,f492,f495,f628])).
% 0.15/0.51 fof(f633,definition,(
% 0.15/0.51 sQ17_spl <=> (ssList(sK50_skl))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f636,plain,(
% 0.15/0.51 ~sQ3_spl|~sQ4_spl|sQ17_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f627,f492,f495,f633])).
% 0.15/0.51 fof(f667,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~nil=app(X0,sK52_skl)|nil=sK52_skl)),
% 0.15/0.51 inference(resolution,[status(thm)],[f385,f426])).
% 0.15/0.51 fof(f668,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~nil=app(X0,sK51_skl)|nil=sK51_skl)),
% 0.15/0.51 inference(resolution,[status(thm)],[f385,f425])).
% 0.15/0.51 fof(f677,definition,(
% 0.15/0.51 ![X0]: (sQ20_spl <=> (~ssList(X0)|~nil=app(X0,sK52_skl)))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f678,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~nil=app(X0,sK52_skl)|~sQ20_spl)),
% 0.15/0.51 inference(component_clause,[status(thm)],[f677])).
% 0.15/0.51 fof(f680,definition,(
% 0.15/0.51 sQ21_spl <=> (nil=sK52_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f681,plain,(
% 0.15/0.51 nil=sK52_skl|~sQ21_spl),
% 0.15/0.51 inference(component_clause,[status(thm)],[f680])).
% 0.15/0.51 fof(f683,plain,(
% 0.15/0.51 sQ20_spl|sQ21_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f667,f677,f680])).
% 0.15/0.51 fof(f684,definition,(
% 0.15/0.51 ![X0]: (sQ22_spl <=> (~ssList(X0)|~nil=app(X0,sK51_skl)))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f685,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~nil=app(X0,sK51_skl)|~sQ22_spl)),
% 0.15/0.51 inference(component_clause,[status(thm)],[f684])).
% 0.15/0.51 fof(f687,definition,(
% 0.15/0.51 sQ23_spl <=> (nil=sK51_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f688,plain,(
% 0.15/0.51 nil=sK51_skl|~sQ23_spl),
% 0.15/0.51 inference(component_clause,[status(thm)],[f687])).
% 0.15/0.51 fof(f690,plain,(
% 0.15/0.51 sQ22_spl|sQ23_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f668,f684,f687])).
% 0.15/0.51 fof(f695,plain,(
% 0.15/0.51 ![X0]: (~ssList(nil)|~ssList(nil)|~ssList(X0)|~app(X0,nil)=nil|X0=nil)),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f537,f376])).
% 0.15/0.51 fof(f698,plain,(
% 0.15/0.51 ~sQ5_spl|sQ15_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f695,f498,f619])).
% 0.15/0.51 fof(f709,plain,(
% 0.15/0.51 ![X0]: (~ssList(nil)|~ssList(sK49_skl)|~ssList(X0)|~app(X0,sK49_skl)=sK49_skl|X0=nil)),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f538,f376])).
% 0.15/0.51 fof(f712,definition,(
% 0.15/0.51 ![X0]: (sQ25_spl <=> (~ssList(X0)|~app(X0,sK49_skl)=sK49_skl|X0=nil))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f715,plain,(
% 0.15/0.51 ~sQ5_spl|~sQ6_spl|sQ25_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f709,f498,f504,f712])).
% 0.15/0.51 fof(f718,plain,(
% 0.15/0.51 $false|sQ5_spl),
% 0.15/0.51 inference(forward_subsumption_resolution,[status(thm)],[f500,f223])).
% 0.15/0.51 fof(f719,plain,(
% 0.15/0.51 sQ5_spl),
% 0.15/0.51 inference(contradiction_clause,[status(thm)],[f718])).
% 0.15/0.51 fof(f733,definition,(
% 0.15/0.51 sQ27_spl <=> (nil=sK50_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f734,plain,(
% 0.15/0.51 nil=sK50_skl|~sQ27_spl),
% 0.15/0.51 inference(component_clause,[status(thm)],[f733])).
% 0.15/0.51 fof(f739,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK5_skl(nil,X0))|~ssList(X0))),
% 0.15/0.51 inference(resolution,[status(thm)],[f122,f295])).
% 0.15/0.51 fof(f740,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~ssList(X0)|ssList(sK5_skl(X0,X0))|~ssList(X0))),
% 0.15/0.51 inference(resolution,[status(thm)],[f122,f286])).
% 0.15/0.51 fof(f741,definition,(
% 0.15/0.51 ![X0]: (sQ28_spl <=> (~ssList(X0)|ssList(sK5_skl(nil,X0))|~ssList(X0)))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f744,plain,(
% 0.15/0.51 sQ28_spl|~sQ5_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f739,f741,f498])).
% 0.15/0.51 fof(f745,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|ssList(sK5_skl(X0,X0)))),
% 0.15/0.51 inference(duplicate_literals_removal,[status(thm)],[f740])).
% 0.15/0.51 fof(f747,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0))),
% 0.15/0.51 inference(resolution,[status(thm)],[f123,f295])).
% 0.15/0.51 fof(f749,definition,(
% 0.15/0.51 ![X0]: (sQ29_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0)))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f752,plain,(
% 0.15/0.51 sQ29_spl|~sQ5_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f747,f749,f498])).
% 0.15/0.51 fof(f769,plain,(
% 0.15/0.51 app(sK51_skl,sK52_skl)=nil|~sQ0_spl),
% 0.15/0.51 inference(forward_demodulation,[status(thm)],[f486,f427])).
% 0.15/0.51 fof(f780,plain,(
% 0.15/0.51 app(sK49_skl,nil)=sK49_skl),
% 0.15/0.51 inference(resolution,[status(thm)],[f389,f421])).
% 0.15/0.51 fof(f783,plain,(
% 0.15/0.51 app(sK52_skl,nil)=sK52_skl),
% 0.15/0.51 inference(resolution,[status(thm)],[f389,f426])).
% 0.15/0.51 fof(f784,plain,(
% 0.15/0.51 app(sK51_skl,nil)=sK51_skl),
% 0.15/0.51 inference(resolution,[status(thm)],[f389,f425])).
% 0.15/0.51 fof(f786,plain,(
% 0.15/0.51 ![X0]: (~ssList(sK49_skl)|~ssList(nil)|~ssList(X0)|~app(X0,nil)=sK49_skl|X0=sK49_skl)),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f780,f376])).
% 0.15/0.51 fof(f789,definition,(
% 0.15/0.51 ![X0]: (sQ30_spl <=> (~ssList(X0)|~app(X0,nil)=sK49_skl|X0=sK49_skl))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f792,plain,(
% 0.15/0.51 ~sQ6_spl|~sQ5_spl|sQ30_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f786,f504,f498,f789])).
% 0.15/0.51 fof(f801,plain,(
% 0.15/0.51 ![X0]: (~ssList(sK52_skl)|~ssList(nil)|~ssList(X0)|~app(X0,nil)=sK52_skl|X0=sK52_skl)),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f783,f376])).
% 0.15/0.51 fof(f804,definition,(
% 0.15/0.51 ![X0]: (sQ31_spl <=> (~ssList(X0)|~app(X0,nil)=sK52_skl|X0=sK52_skl))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f807,plain,(
% 0.15/0.51 ~sQ4_spl|~sQ5_spl|sQ31_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f801,f495,f498,f804])).
% 0.15/0.51 fof(f810,plain,(
% 0.15/0.51 ![X0]: (~ssList(sK51_skl)|~ssList(nil)|~ssList(X0)|~app(X0,nil)=sK51_skl|X0=sK51_skl)),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f784,f376])).
% 0.15/0.51 fof(f813,definition,(
% 0.15/0.51 ![X0]: (sQ32_spl <=> (~ssList(X0)|~app(X0,nil)=sK51_skl|X0=sK51_skl))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f816,plain,(
% 0.15/0.51 ~sQ3_spl|~sQ5_spl|sQ32_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f810,f492,f498,f813])).
% 0.15/0.51 fof(f819,plain,(
% 0.15/0.51 ssList(sK5_skl(sK49_skl,sK49_skl))),
% 0.15/0.51 inference(resolution,[status(thm)],[f745,f421])).
% 0.15/0.51 fof(f822,plain,(
% 0.15/0.51 ssList(sK5_skl(sK52_skl,sK52_skl))),
% 0.15/0.51 inference(resolution,[status(thm)],[f745,f426])).
% 0.15/0.51 fof(f823,plain,(
% 0.15/0.51 ssList(sK5_skl(sK51_skl,sK51_skl))),
% 0.15/0.51 inference(resolution,[status(thm)],[f745,f425])).
% 0.15/0.51 fof(f824,plain,(
% 0.15/0.51 ssList(sK5_skl(nil,nil))),
% 0.15/0.51 inference(resolution,[status(thm)],[f745,f223])).
% 0.15/0.51 fof(f909,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK6_skl(nil,X0))|~ssList(X0))),
% 0.15/0.51 inference(resolution,[status(thm)],[f128,f309])).
% 0.15/0.51 fof(f911,definition,(
% 0.15/0.51 ![X0]: (sQ41_spl <=> (~ssList(X0)|ssList(sK6_skl(nil,X0))|~ssList(X0)))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f914,plain,(
% 0.15/0.51 sQ41_spl|~sQ5_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f909,f911,f498])).
% 0.15/0.51 fof(f917,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~ssList(nil)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0))),
% 0.15/0.51 inference(resolution,[status(thm)],[f129,f309])).
% 0.15/0.51 fof(f919,definition,(
% 0.15/0.51 ![X0]: (sQ42_spl <=> (~ssList(X0)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0)))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f922,plain,(
% 0.15/0.51 sQ42_spl|~sQ5_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f917,f919,f498])).
% 0.15/0.51 fof(f943,plain,(
% 0.15/0.51 ~nil=app(sK52_skl,sK51_skl)|~sQ22_spl),
% 0.15/0.51 inference(resolution,[status(thm)],[f685,f426])).
% 0.15/0.51 fof(f945,plain,(
% 0.15/0.51 ~nil=app(nil,sK51_skl)|~sQ22_spl),
% 0.15/0.51 inference(resolution,[status(thm)],[f685,f223])).
% 0.15/0.51 fof(f946,plain,(
% 0.15/0.51 ~nil=sK49_skl|~sQ22_spl),
% 0.15/0.51 inference(forward_demodulation,[status(thm)],[f428,f943])).
% 0.15/0.51 fof(f947,plain,(
% 0.15/0.51 ~nil=sK51_skl|~sQ22_spl),
% 0.15/0.51 inference(forward_demodulation,[status(thm)],[f536,f945])).
% 0.15/0.51 fof(f948,plain,(
% 0.15/0.51 ~app(sK5_skl(nil,nil),sK51_skl)=sK49_skl|sK5_skl(nil,nil)=sK52_skl|~sQ11_spl),
% 0.15/0.51 inference(resolution,[status(thm)],[f554,f824])).
% 0.15/0.51 fof(f949,plain,(
% 0.15/0.51 ~app(sK5_skl(sK51_skl,sK51_skl),sK51_skl)=sK49_skl|sK5_skl(sK51_skl,sK51_skl)=sK52_skl|~sQ11_spl),
% 0.15/0.51 inference(resolution,[status(thm)],[f554,f823])).
% 0.15/0.51 fof(f950,plain,(
% 0.15/0.51 ~app(sK5_skl(sK52_skl,sK52_skl),sK51_skl)=sK49_skl|sK5_skl(sK52_skl,sK52_skl)=sK52_skl|~sQ11_spl),
% 0.15/0.51 inference(resolution,[status(thm)],[f554,f822])).
% 0.15/0.51 fof(f951,plain,(
% 0.15/0.51 ~app(sK5_skl(sK49_skl,sK49_skl),sK51_skl)=sK49_skl|sK5_skl(sK49_skl,sK49_skl)=sK52_skl|~sQ11_spl),
% 0.15/0.51 inference(resolution,[status(thm)],[f554,f819])).
% 0.15/0.51 fof(f952,plain,(
% 0.15/0.51 ~app(sK49_skl,sK51_skl)=sK49_skl|sK49_skl=sK52_skl|~sQ11_spl),
% 0.15/0.51 inference(resolution,[status(thm)],[f554,f421])).
% 0.15/0.51 fof(f955,plain,(
% 0.15/0.51 ~app(sK52_skl,sK51_skl)=sK49_skl|sK52_skl=sK52_skl|~sQ11_spl),
% 0.15/0.51 inference(resolution,[status(thm)],[f554,f426])).
% 0.15/0.51 fof(f958,definition,(
% 0.15/0.51 sQ43_spl <=> (app(sK5_skl(nil,nil),sK51_skl)=sK49_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f961,definition,(
% 0.15/0.51 sQ44_spl <=> (sK5_skl(nil,nil)=sK52_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f964,plain,(
% 0.15/0.51 ~sQ43_spl|sQ44_spl|~sQ11_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f948,f958,f961,f553])).
% 0.15/0.51 fof(f965,definition,(
% 0.15/0.51 sQ45_spl <=> (app(sK5_skl(sK51_skl,sK51_skl),sK51_skl)=sK49_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f968,definition,(
% 0.15/0.51 sQ46_spl <=> (sK5_skl(sK51_skl,sK51_skl)=sK52_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f971,plain,(
% 0.15/0.51 ~sQ45_spl|sQ46_spl|~sQ11_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f949,f965,f968,f553])).
% 0.15/0.51 fof(f972,definition,(
% 0.15/0.51 sQ47_spl <=> (app(sK5_skl(sK52_skl,sK52_skl),sK51_skl)=sK49_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f975,definition,(
% 0.15/0.51 sQ48_spl <=> (sK5_skl(sK52_skl,sK52_skl)=sK52_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f978,plain,(
% 0.15/0.51 ~sQ47_spl|sQ48_spl|~sQ11_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f950,f972,f975,f553])).
% 0.15/0.51 fof(f979,definition,(
% 0.15/0.51 sQ49_spl <=> (app(sK5_skl(sK49_skl,sK49_skl),sK51_skl)=sK49_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f982,definition,(
% 0.15/0.51 sQ50_spl <=> (sK5_skl(sK49_skl,sK49_skl)=sK52_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f985,plain,(
% 0.15/0.51 ~sQ49_spl|sQ50_spl|~sQ11_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f951,f979,f982,f553])).
% 0.15/0.51 fof(f986,definition,(
% 0.15/0.51 sQ51_spl <=> (app(sK49_skl,sK51_skl)=sK49_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f988,plain,(
% 0.15/0.51 ~app(sK49_skl,sK51_skl)=sK49_skl|sQ51_spl),
% 0.15/0.51 inference(component_clause,[status(thm)],[f986])).
% 0.15/0.51 fof(f989,definition,(
% 0.15/0.51 sQ52_spl <=> (sK49_skl=sK52_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f990,plain,(
% 0.15/0.51 sK49_skl=sK52_skl|~sQ52_spl),
% 0.15/0.51 inference(component_clause,[status(thm)],[f989])).
% 0.15/0.51 fof(f992,plain,(
% 0.15/0.51 ~sQ51_spl|sQ52_spl|~sQ11_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f952,f986,f989,f553])).
% 0.15/0.51 fof(f993,definition,(
% 0.15/0.51 sQ53_spl <=> (app(sK52_skl,sK51_skl)=sK49_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f995,plain,(
% 0.15/0.51 ~app(sK52_skl,sK51_skl)=sK49_skl|sQ53_spl),
% 0.15/0.51 inference(component_clause,[status(thm)],[f993])).
% 0.15/0.51 fof(f996,definition,(
% 0.15/0.51 sQ54_spl <=> (sK52_skl=sK52_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f999,plain,(
% 0.15/0.51 ~sQ53_spl|sQ54_spl|~sQ11_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f955,f993,f996,f553])).
% 0.15/0.51 fof(f1007,definition,(
% 0.15/0.51 sQ57_spl <=> (app(nil,sK51_skl)=sK49_skl)),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f1008,plain,(
% 0.15/0.51 app(nil,sK51_skl)=sK49_skl|~sQ57_spl),
% 0.15/0.51 inference(component_clause,[status(thm)],[f1007])).
% 0.15/0.51 fof(f1009,plain,(
% 0.15/0.51 ~app(nil,sK51_skl)=sK49_skl|sQ57_spl),
% 0.15/0.51 inference(component_clause,[status(thm)],[f1007])).
% 0.15/0.51 fof(f1011,plain,(
% 0.15/0.51 ~sK49_skl=sK49_skl|sQ53_spl),
% 0.15/0.51 inference(forward_demodulation,[status(thm)],[f428,f995])).
% 0.15/0.51 fof(f1012,plain,(
% 0.15/0.51 $false|sQ53_spl),
% 0.15/0.51 inference(trivial_equality_resolution,[status(thm)],[f1011])).
% 0.15/0.51 fof(f1013,plain,(
% 0.15/0.51 sQ53_spl),
% 0.15/0.51 inference(contradiction_clause,[status(thm)],[f1012])).
% 0.15/0.51 fof(f1017,plain,(
% 0.15/0.51 app(sK51_skl,nil)=nil|~sQ21_spl|~sQ0_spl),
% 0.15/0.51 inference(backward_demodulation,[status(thm)],[f681,f769])).
% 0.15/0.51 fof(f1024,plain,(
% 0.15/0.51 nil=sK51_skl|~sQ21_spl|~sQ0_spl),
% 0.15/0.51 inference(backward_demodulation,[status(thm)],[f1017,f784])).
% 0.15/0.51 fof(f1028,plain,(
% 0.15/0.51 $false|~sQ22_spl|~sQ21_spl|~sQ0_spl),
% 0.15/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1024,f947])).
% 0.15/0.51 fof(f1029,plain,(
% 0.15/0.51 ~sQ22_spl|~sQ21_spl|~sQ0_spl),
% 0.15/0.51 inference(contradiction_clause,[status(thm)],[f1028])).
% 0.15/0.51 fof(f1030,plain,(
% 0.15/0.51 ~sK51_skl=sK49_skl|sQ57_spl),
% 0.15/0.51 inference(forward_demodulation,[status(thm)],[f536,f1009])).
% 0.15/0.51 fof(f1036,plain,(
% 0.15/0.51 ~app(sK49_skl,nil)=sK49_skl|~sQ23_spl|sQ51_spl),
% 0.15/0.51 inference(backward_demodulation,[status(thm)],[f688,f988])).
% 0.15/0.51 fof(f1042,plain,(
% 0.15/0.51 ~sK49_skl=sK49_skl|~sQ23_spl|sQ51_spl),
% 0.15/0.51 inference(forward_demodulation,[status(thm)],[f780,f1036])).
% 0.15/0.51 fof(f1043,plain,(
% 0.15/0.51 $false|~sQ23_spl|sQ51_spl),
% 0.15/0.51 inference(trivial_equality_resolution,[status(thm)],[f1042])).
% 0.15/0.51 fof(f1044,plain,(
% 0.15/0.51 ~sQ23_spl|sQ51_spl),
% 0.15/0.51 inference(contradiction_clause,[status(thm)],[f1043])).
% 0.15/0.51 fof(f1062,plain,(
% 0.15/0.51 ssList(sK5_skl(sK52_skl,sK52_skl))),
% 0.15/0.51 inference(resolution,[status(thm)],[f426,f745])).
% 0.15/0.51 fof(f1064,plain,(
% 0.15/0.51 app(sK52_skl,nil)=sK52_skl),
% 0.15/0.51 inference(resolution,[status(thm)],[f426,f389])).
% 0.15/0.51 fof(f1075,plain,(
% 0.15/0.51 app(nil,sK52_skl)=sK52_skl),
% 0.15/0.51 inference(resolution,[status(thm)],[f426,f249])).
% 0.15/0.51 fof(f1087,plain,(
% 0.15/0.51 ~sK51_skl=nil|~sQ1_spl|sQ57_spl),
% 0.15/0.51 inference(forward_demodulation,[status(thm)],[f571,f1030])).
% 0.15/0.51 fof(f1088,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK7_skl(nil,X0))|~ssList(X0))),
% 0.15/0.51 inference(resolution,[status(thm)],[f134,f323])).
% 0.15/0.51 fof(f1090,definition,(
% 0.15/0.51 ![X0]: (sQ58_spl <=> (~ssList(X0)|ssList(sK7_skl(nil,X0))|~ssList(X0)))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f1093,plain,(
% 0.15/0.51 sQ58_spl|~sQ5_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f1088,f1090,f498])).
% 0.15/0.51 fof(f1096,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK8_skl(nil,X0))|~ssList(X0))),
% 0.15/0.51 inference(resolution,[status(thm)],[f135,f323])).
% 0.15/0.51 fof(f1098,definition,(
% 0.15/0.51 ![X0]: (sQ59_spl <=> (~ssList(X0)|ssList(sK8_skl(nil,X0))|~ssList(X0)))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f1101,plain,(
% 0.15/0.51 sQ59_spl|~sQ5_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f1096,f1098,f498])).
% 0.15/0.51 fof(f1104,plain,(
% 0.15/0.51 ![X0]: (~ssList(X0)|~ssList(nil)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0))),
% 0.15/0.51 inference(resolution,[status(thm)],[f136,f323])).
% 0.15/0.51 fof(f1106,definition,(
% 0.15/0.51 ![X0]: (sQ60_spl <=> (~ssList(X0)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0)))),
% 0.15/0.51 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.15/0.51 fof(f1109,plain,(
% 0.15/0.51 sQ60_spl|~sQ5_spl),
% 0.15/0.51 inference(split_clause,[status(thm)],[f1104,f1106,f498])).
% 0.15/0.51 fof(f1115,plain,(
% 0.15/0.51 app(sK51_skl,nil)=sK51_skl),
% 0.15/0.51 inference(resolution,[status(thm)],[f425,f389])).
% 0.15/0.51 fof(f1128,plain,(
% 0.15/0.51 ~nil=nil|~sQ1_spl|~sQ22_spl),
% 0.15/0.51 inference(forward_demodulation,[status(thm)],[f571,f946])).
% 0.15/0.51 fof(f1129,plain,(
% 0.15/0.51 $false|~sQ1_spl|~sQ22_spl),
% 0.15/0.51 inference(trivial_equality_resolution,[status(thm)],[f1128])).
% 0.15/0.51 fof(f1130,plain,(
% 0.15/0.51 ~sQ1_spl|~sQ22_spl),
% 0.15/0.51 inference(contradiction_clause,[status(thm)],[f1129])).
% 0.15/0.51 fof(f1131,plain,(
% 0.15/0.51 $false|~sQ1_spl|sQ57_spl|~sQ23_spl),
% 0.15/0.51 inference(forward_subsumption_resolution,[status(thm)],[f688,f1087])).
% 0.15/0.51 fof(f1132,plain,(
% 0.15/0.51 ~sQ1_spl|sQ57_spl|~sQ23_spl),
% 0.15/0.51 inference(contradiction_clause,[status(thm)],[f1131])).
% 0.15/0.51 fof(f1168,plain,(
% 0.15/0.51 app(nil,sK52_skl)=sK50_skl|~sQ23_spl),
% 0.15/0.51 inference(forward_demodulation,[status(thm)],[f688,f427])).
% 0.15/0.51 fof(f1186,plain,(
% 0.15/0.51 ![X0]: (~ssList(app(nil,X0))|~ssList(nil)|segmentP(app(app(nil,nil),X0),nil)|~ssList(nil)|~ssList(X0))),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f537,f453])).
% 0.15/0.52 fof(f1189,definition,(
% 0.15/0.52 ![X0]: (sQ63_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)|~ssList(X0)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f1192,plain,(
% 0.15/0.52 sQ63_spl|~sQ5_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f1186,f1189,f498])).
% 0.15/0.52 fof(f1221,plain,(
% 0.15/0.52 app(nil,sK52_skl)=nil|~sQ23_spl|~sQ0_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f688,f769])).
% 0.15/0.52 fof(f1222,plain,(
% 0.15/0.52 app(nil,sK49_skl)=nil|~sQ52_spl|~sQ23_spl|~sQ0_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f990,f1221])).
% 0.15/0.52 fof(f1238,plain,(
% 0.15/0.52 app(nil,sK49_skl)=sK50_skl|~sQ52_spl|~sQ23_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f990,f1168])).
% 0.15/0.52 fof(f1264,definition,(
% 0.15/0.52 ![X0]: (sQ66_spl <=> (~ssList(app(sK49_skl,X0))|segmentP(app(app(sK49_skl,nil),X0),nil)|~ssList(X0)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f1272,plain,(
% 0.15/0.52 app(nil,sK49_skl)=sK52_skl|~sQ52_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f990,f535])).
% 0.15/0.52 fof(f1273,plain,(
% 0.15/0.52 sK49_skl=nil|~sQ23_spl|~sQ0_spl|~sQ52_spl),
% 0.15/0.52 inference(backward_demodulation,[status(thm)],[f1274,f990])).
% 0.15/0.52 fof(f1274,plain,(
% 0.15/0.52 nil=sK52_skl|~sQ23_spl|~sQ0_spl|~sQ52_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f1222,f1272])).
% 0.15/0.52 fof(f1277,plain,(
% 0.15/0.52 app(nil,nil)=sK49_skl|~sQ23_spl|~sQ57_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f688,f1008])).
% 0.15/0.52 fof(f1278,plain,(
% 0.15/0.52 nil=sK49_skl|~sQ23_spl|~sQ57_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f537,f1277])).
% 0.15/0.52 fof(f1286,plain,(
% 0.15/0.52 sP0_prd(nil,nil)|~sQ23_spl|~sQ52_spl|~sQ0_spl),
% 0.15/0.52 inference(backward_demodulation,[status(thm)],[f1273,f487])).
% 0.15/0.52 fof(f1291,plain,(
% 0.15/0.52 $false|~sQ23_spl|~sQ52_spl|~sQ0_spl),
% 0.15/0.52 inference(forward_subsumption_resolution,[status(thm)],[f1286,f477])).
% 0.15/0.52 fof(f1292,plain,(
% 0.15/0.52 ~sQ23_spl|~sQ52_spl|~sQ0_spl),
% 0.15/0.52 inference(contradiction_clause,[status(thm)],[f1291])).
% 0.15/0.52 fof(f1293,plain,(
% 0.15/0.52 app(sK51_skl,sK52_skl)=nil|~sQ0_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f486,f427])).
% 0.15/0.52 fof(f1297,plain,(
% 0.15/0.52 app(sK49_skl,nil)=sK49_skl),
% 0.15/0.52 inference(resolution,[status(thm)],[f421,f389])).
% 0.15/0.52 fof(f1308,plain,(
% 0.15/0.52 app(nil,sK49_skl)=sK49_skl),
% 0.15/0.52 inference(resolution,[status(thm)],[f421,f249])).
% 0.15/0.52 fof(f1415,plain,(
% 0.15/0.52 ![X0]: (~ssList(app(sK51_skl,X0))|~ssList(sK51_skl)|segmentP(app(app(nil,sK51_skl),X0),sK51_skl)|~ssList(nil)|~ssList(X0))),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f536,f453])).
% 0.15/0.52 fof(f1419,definition,(
% 0.15/0.52 ![X0]: (sQ82_spl <=> (~ssList(app(sK51_skl,X0))|segmentP(app(app(nil,sK51_skl),X0),sK51_skl)|~ssList(X0)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f1422,plain,(
% 0.15/0.52 sQ82_spl|~sQ3_spl|~sQ5_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f1415,f1419,f492,f498])).
% 0.15/0.52 fof(f1443,plain,(
% 0.15/0.52 app(sK49_skl,sK51_skl)=sK49_skl|~sQ52_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f990,f428])).
% 0.15/0.52 fof(f1444,plain,(
% 0.15/0.52 ![X0]: (~ssList(app(sK49_skl,X0))|~ssList(sK51_skl)|segmentP(app(app(sK49_skl,sK51_skl),X0),sK51_skl)|~ssList(sK49_skl)|~ssList(X0)|~sQ52_spl)),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f1443,f453])).
% 0.15/0.52 fof(f1445,plain,(
% 0.15/0.52 ![X0]: (~ssList(sK49_skl)|~ssList(sK51_skl)|~ssList(X0)|~app(X0,sK51_skl)=sK49_skl|X0=sK49_skl|~sQ52_spl)),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f1443,f376])).
% 0.15/0.52 fof(f1448,definition,(
% 0.15/0.52 ![X0]: (sQ85_spl <=> (~ssList(app(sK49_skl,X0))|segmentP(app(app(sK49_skl,sK51_skl),X0),sK51_skl)|~ssList(X0)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f1451,plain,(
% 0.15/0.52 sQ85_spl|~sQ3_spl|~sQ6_spl|~sQ52_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f1444,f1448,f492,f504,f989])).
% 0.15/0.52 fof(f1452,definition,(
% 0.15/0.52 ![X0]: (sQ86_spl <=> (~ssList(X0)|~app(X0,sK51_skl)=sK49_skl|X0=sK49_skl))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f1455,plain,(
% 0.15/0.52 ~sQ6_spl|~sQ3_spl|sQ86_spl|~sQ52_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f1445,f504,f492,f1452,f989])).
% 0.15/0.52 fof(f1506,plain,(
% 0.15/0.52 app(nil,sK49_skl)=sK52_skl|~sQ52_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f990,f1075])).
% 0.15/0.52 fof(f1507,plain,(
% 0.15/0.52 app(nil,sK49_skl)=sK49_skl|~sQ52_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f990,f1506])).
% 0.15/0.52 fof(f1512,definition,(
% 0.15/0.52 ![X0]: (sQ90_spl <=> (~ssList(app(sK49_skl,X0))|segmentP(app(app(nil,sK49_skl),X0),sK49_skl)|~ssList(X0)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f1520,plain,(
% 0.15/0.52 ![X0]: (~ssList(app(sK51_skl,X0))|~ssList(nil)|segmentP(app(app(sK51_skl,nil),X0),nil)|~ssList(sK51_skl)|~ssList(X0))),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f1115,f453])).
% 0.15/0.52 fof(f1524,definition,(
% 0.15/0.52 ![X0]: (sQ91_spl <=> (~ssList(app(sK51_skl,X0))|segmentP(app(app(sK51_skl,nil),X0),nil)|~ssList(X0)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f1527,plain,(
% 0.15/0.52 sQ91_spl|~sQ5_spl|~sQ3_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f1520,f1524,f498,f492])).
% 0.15/0.52 fof(f1684,plain,(
% 0.15/0.52 app(sK51_skl,sK49_skl)=sK50_skl|~sQ52_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f990,f427])).
% 0.15/0.52 fof(f1685,plain,(
% 0.15/0.52 sK49_skl=sK50_skl|~sQ52_spl|~sQ23_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f1507,f1238])).
% 0.15/0.52 fof(f1689,plain,(
% 0.15/0.52 ![X0]: (~ssList(app(sK50_skl,X0))|~ssList(sK49_skl)|segmentP(app(app(sK51_skl,sK49_skl),X0),sK49_skl)|~ssList(sK51_skl)|~ssList(X0)|~sQ52_spl)),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f1684,f453])).
% 0.15/0.52 fof(f1690,plain,(
% 0.15/0.52 ![X0]: (~ssList(sK51_skl)|~ssList(sK49_skl)|~ssList(X0)|~app(X0,sK49_skl)=sK50_skl|X0=sK51_skl|~sQ52_spl)),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f1684,f376])).
% 0.15/0.52 fof(f1693,definition,(
% 0.15/0.52 ![X0]: (sQ110_spl <=> (~ssList(app(sK50_skl,X0))|segmentP(app(app(sK51_skl,sK49_skl),X0),sK49_skl)|~ssList(X0)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f1696,plain,(
% 0.15/0.52 sQ110_spl|~sQ6_spl|~sQ3_spl|~sQ52_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f1689,f1693,f504,f492,f989])).
% 0.15/0.52 fof(f1697,definition,(
% 0.15/0.52 ![X0]: (sQ111_spl <=> (~ssList(X0)|~app(X0,sK49_skl)=sK50_skl|X0=sK51_skl))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f1700,plain,(
% 0.15/0.52 ~sQ3_spl|~sQ6_spl|sQ111_spl|~sQ52_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f1690,f492,f504,f1697,f989])).
% 0.15/0.52 fof(f1704,plain,(
% 0.15/0.52 $false|sQ2_spl|~sQ27_spl),
% 0.15/0.52 inference(forward_subsumption_resolution,[status(thm)],[f734,f572])).
% 0.15/0.52 fof(f1705,plain,(
% 0.15/0.52 sQ2_spl|~sQ27_spl),
% 0.15/0.52 inference(contradiction_clause,[status(thm)],[f1704])).
% 0.15/0.52 fof(f1720,plain,(
% 0.15/0.52 nil=sK50_skl|~sQ57_spl|~sQ52_spl|~sQ23_spl),
% 0.15/0.52 inference(backward_demodulation,[status(thm)],[f1278,f1685])).
% 0.15/0.52 fof(f1728,plain,(
% 0.15/0.52 sQ27_spl|~sQ57_spl|~sQ52_spl|~sQ23_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f1720,f733,f1007,f989,f687])).
% 0.15/0.52 fof(f1860,plain,(
% 0.15/0.52 ![X0]: (~ssList(app(sK50_skl,X0))|~ssList(sK52_skl)|segmentP(app(app(sK51_skl,sK52_skl),X0),sK52_skl)|~ssList(sK51_skl)|~ssList(X0))),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f427,f453])).
% 0.15/0.52 fof(f1864,definition,(
% 0.15/0.52 ![X0]: (sQ131_spl <=> (~ssList(app(sK50_skl,X0))|segmentP(app(app(sK51_skl,sK52_skl),X0),sK52_skl)|~ssList(X0)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f1867,plain,(
% 0.15/0.52 sQ131_spl|~sQ4_spl|~sQ3_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f1860,f1864,f495,f492])).
% 0.15/0.52 fof(f1926,plain,(
% 0.15/0.52 ![X0]: (~ssList(app(sK49_skl,X0))|~ssList(sK51_skl)|segmentP(app(app(sK52_skl,sK51_skl),X0),sK51_skl)|~ssList(sK52_skl)|~ssList(X0))),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f428,f453])).
% 0.15/0.52 fof(f1930,definition,(
% 0.15/0.52 ![X0]: (sQ136_spl <=> (~ssList(app(sK49_skl,X0))|segmentP(app(app(sK52_skl,sK51_skl),X0),sK51_skl)|~ssList(X0)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f1933,plain,(
% 0.15/0.52 sQ136_spl|~sQ3_spl|~sQ4_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f1926,f1930,f492,f495])).
% 0.15/0.52 fof(f2036,plain,(
% 0.15/0.52 ![X0]: (~ssList(app(sK49_skl,X0))|~ssList(sK49_skl)|segmentP(app(app(nil,sK49_skl),X0),sK49_skl)|~ssList(nil)|~ssList(X0))),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f1308,f453])).
% 0.15/0.52 fof(f2040,plain,(
% 0.15/0.52 sQ90_spl|~sQ6_spl|~sQ5_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f2036,f1512,f504,f498])).
% 0.15/0.52 fof(f2045,plain,(
% 0.15/0.52 ![X0]: (~ssList(app(sK49_skl,X0))|~ssList(nil)|segmentP(app(app(sK49_skl,nil),X0),nil)|~ssList(sK49_skl)|~ssList(X0))),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f1297,f453])).
% 0.15/0.52 fof(f2049,plain,(
% 0.15/0.52 sQ66_spl|~sQ5_spl|~sQ6_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f2045,f1264,f498,f504])).
% 0.15/0.52 fof(f2116,plain,(
% 0.15/0.52 ![X0]: (~ssList(app(sK52_skl,X0))|~ssList(sK52_skl)|segmentP(app(app(nil,sK52_skl),X0),sK52_skl)|~ssList(nil)|~ssList(X0))),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f1075,f453])).
% 0.15/0.52 fof(f2120,definition,(
% 0.15/0.52 ![X0]: (sQ153_spl <=> (~ssList(app(sK52_skl,X0))|segmentP(app(app(nil,sK52_skl),X0),sK52_skl)|~ssList(X0)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f2123,plain,(
% 0.15/0.52 sQ153_spl|~sQ4_spl|~sQ5_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f2116,f2120,f495,f498])).
% 0.15/0.52 fof(f2128,plain,(
% 0.15/0.52 ![X0]: (~ssList(app(sK52_skl,X0))|~ssList(nil)|segmentP(app(app(sK52_skl,nil),X0),nil)|~ssList(sK52_skl)|~ssList(X0))),
% 0.15/0.52 inference(paramodulation,[status(thm)],[f1064,f453])).
% 0.15/0.52 fof(f2132,definition,(
% 0.15/0.52 ![X0]: (sQ154_spl <=> (~ssList(app(sK52_skl,X0))|segmentP(app(app(sK52_skl,nil),X0),nil)|~ssList(X0)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f2135,plain,(
% 0.15/0.52 sQ154_spl|~sQ5_spl|~sQ4_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f2128,f2132,f498,f495])).
% 0.15/0.52 fof(f2302,plain,(
% 0.15/0.52 ~app(sK52_skl,sK52_skl)=app(sK52_skl,sK5_skl(sK52_skl,sK52_skl))|sK52_skl=sK5_skl(sK52_skl,sK52_skl)),
% 0.15/0.52 inference(resolution,[status(thm)],[f582,f1062])).
% 0.15/0.52 fof(f2309,definition,(
% 0.15/0.52 sQ180_spl <=> (app(sK52_skl,sK52_skl)=app(sK52_skl,sK5_skl(sK52_skl,sK52_skl)))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f2312,plain,(
% 0.15/0.52 ~sQ180_spl|sQ48_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f2302,f2309,f975])).
% 0.15/0.52 fof(f2552,plain,(
% 0.15/0.52 ~app(sK51_skl,sK51_skl)=app(sK51_skl,sK51_skl)|sK51_skl=sK51_skl),
% 0.15/0.52 inference(resolution,[status(thm)],[f584,f425])).
% 0.15/0.52 fof(f2561,definition,(
% 0.15/0.52 sQ196_spl <=> (app(sK51_skl,sK51_skl)=app(sK51_skl,sK51_skl))),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f2563,plain,(
% 0.15/0.52 ~app(sK51_skl,sK51_skl)=app(sK51_skl,sK51_skl)|sQ196_spl),
% 0.15/0.52 inference(component_clause,[status(thm)],[f2561])).
% 0.15/0.52 fof(f2564,definition,(
% 0.15/0.52 sQ197_spl <=> (sK51_skl=sK51_skl)),
% 0.15/0.52 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 0.15/0.52 fof(f2567,plain,(
% 0.15/0.52 ~sQ196_spl|sQ197_spl),
% 0.15/0.52 inference(split_clause,[status(thm)],[f2552,f2561,f2564])).
% 0.15/0.52 fof(f2581,plain,(
% 0.15/0.52 $false|sQ196_spl),
% 0.15/0.52 inference(trivial_equality_resolution,[status(thm)],[f2563])).
% 0.15/0.52 fof(f2582,plain,(
% 0.15/0.52 sQ196_spl),
% 0.15/0.52 inference(contradiction_clause,[status(thm)],[f2581])).
% 0.15/0.52 fof(f2584,plain,(
% 0.15/0.52 ~nil=app(sK51_skl,sK52_skl)|~sQ20_spl),
% 0.15/0.52 inference(resolution,[status(thm)],[f678,f425])).
% 0.15/0.52 fof(f2589,plain,(
% 0.15/0.52 ~nil=nil|~sQ0_spl|~sQ20_spl),
% 0.15/0.52 inference(forward_demodulation,[status(thm)],[f1293,f2584])).
% 0.15/0.52 fof(f2590,plain,(
% 0.15/0.52 $false|~sQ0_spl|~sQ20_spl),
% 0.15/0.52 inference(trivial_equality_resolution,[status(thm)],[f2589])).
% 0.15/0.52 fof(f2591,plain,(
% 0.15/0.52 ~sQ0_spl|~sQ20_spl),
% 0.15/0.52 inference(contradiction_clause,[status(thm)],[f2590])).
% 0.15/0.52 fof(f2592,plain,(
% 0.15/0.52 $false),
% 0.15/0.52 inference(sat_refutation,[status(thm)],[f442,f446,f507,f509,f511,f520,f532,f556,f602,f611,f631,f636,f683,f690,f698,f715,f719,f744,f752,f792,f807,f816,f914,f922,f964,f971,f978,f985,f992,f999,f1013,f1029,f1044,f1093,f1101,f1109,f1130,f1132,f1192,f1292,f1422,f1451,f1455,f1527,f1696,f1700,f1705,f1728,f1867,f1933,f2040,f2049,f2123,f2135,f2312,f2567,f2582,f2591])).
% 0.15/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 1.06/0.53 % Elapsed time: 0.156180 seconds
% 1.06/0.53 % CPU time: 0.995302 seconds
% 1.06/0.53 % Total memory used: 126.212 MB
% 1.06/0.53 % Net memory used: 124.916 MB
%------------------------------------------------------------------------------