%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC407+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 : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:42:23 PM UTC 2026
% Result : Theorem 0.12s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC407+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n020.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 08:23:05 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.43 % Refutation found
% 0.12/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.43 fof(f3,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ( memberP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(W,cons(V,X)) = U ) )) )) ) )) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f4,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> ( singletonP(U)<=> (? [V] :( ssItem(V)& cons(V,nil) = U ) )) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f5,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f6,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( rearsegP(U,V)<=> (? [W] :( ssList(W)& app(W,V) = U ) )) ) )) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f7,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( segmentP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(app(W,V),X) = U ) )) )) ) )) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f8,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> ( cyclefreeP(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)& leq(W,V) ) ) ) )) )) )) )) )) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f16,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ssList(cons(V,U)) ) )) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f17,axiom,(
% 0.12/0.43 ssList(nil) ),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f28,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f36,axiom,(
% 0.12/0.43 (! [U] :( ssItem(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( memberP(app(V,W),U)<=> ( memberP(V,U)| memberP(W,U) ) ) ) )) )) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f37,axiom,(
% 0.12/0.43 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> (! [W] :( ssList(W)=> ( memberP(cons(V,W),U)<=> ( U = V| memberP(W,U) ) ) ) )) )) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f38,axiom,(
% 0.12/0.43 (! [U] :( ssItem(U)=> ~ memberP(nil,U) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f45,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> frontsegP(U,nil) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f51,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> rearsegP(U,nil) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f57,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> segmentP(U,nil) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f84,axiom,(
% 0.12/0.43 (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f96,conjecture,(
% 0.12/0.43 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (! [Y] :( ssItem(Y)=> ( ~ memberP(U,Y)| memberP(V,Y) ) ))| ( (! [Z] :( ssItem(Z)=> ( cons(Z,nil) != W| ~ memberP(X,Z) ) ))& ( nil != X| nil != W ) ) ) ) )) )) )) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f97,negated_conjecture,(
% 0.12/0.43 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (! [Y] :( ssItem(Y)=> ( ~ memberP(U,Y)| memberP(V,Y) ) ))| ( (! [Z] :( ssItem(Z)=> ( cons(Z,nil) != W| ~ memberP(X,Z) ) ))& ( nil != X| nil != W ) ) ) ) )) )) )) ))),
% 0.12/0.43 inference(negated_conjecture,[status(cth)],[f96])).
% 0.12/0.43 fof(f106,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|(memberP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(W,cons(V,X))=U))))))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.12/0.43 fof(f107,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|((~memberP(U,V)|(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(W,cons(V,X))=U)))))&(memberP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(W,cons(V,X))=U)))))))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f106])).
% 0.12/0.43 fof(f108,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|((~memberP(U,V)|(ssList(sK2_skl(V,U))&(ssList(sK3_skl(V,U))&app(sK2_skl(V,U),cons(V,sK3_skl(V,U)))=U)))&(memberP(U,V)|(![W]: (~ssList(W)|(![X]: (~ssList(X)|~app(W,cons(V,X))=U)))))))))),
% 0.12/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(W,sK2_skl(V,U)),skolemize(X,sK3_skl(V,U))],[f107])).
% 0.12/0.43 fof(f109,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|~memberP(X0,X1)|ssList(sK2_skl(X1,X0)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f108])).
% 0.12/0.43 fof(f111,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|~memberP(X0,X1)|app(sK2_skl(X1,X0),cons(X1,sK3_skl(X1,X0)))=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f108])).
% 0.12/0.43 fof(f112,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssItem(X1)|memberP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(X2,cons(X1,X3))=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f108])).
% 0.12/0.43 fof(f113,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|(singletonP(U)<=>(?[V]: (ssItem(V)&cons(V,nil)=U))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.12/0.43 fof(f114,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|((~singletonP(U)|(?[V]: (ssItem(V)&cons(V,nil)=U)))&(singletonP(U)|(![V]: (~ssItem(V)|~cons(V,nil)=U)))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f113])).
% 0.12/0.43 fof(f115,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|((~singletonP(U)|(ssItem(sK4_skl(U))&cons(sK4_skl(U),nil)=U))&(singletonP(U)|(![V]: (~ssItem(V)|~cons(V,nil)=U)))))),
% 0.12/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(V,sK4_skl(U))],[f114])).
% 0.12/0.43 fof(f118,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|singletonP(X0)|~ssItem(X1)|~cons(X1,nil)=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f115])).
% 0.12/0.43 fof(f119,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.12/0.43 fof(f120,plain,(
% 0.12/0.43 ![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.12/0.43 inference(NNF_transformation,[status(thm)],[f119])).
% 0.12/0.43 fof(f121,plain,(
% 0.12/0.43 ![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.12/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 0.12/0.43 fof(f123,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(X1,sK5_skl(X1,X0))=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f121])).
% 0.12/0.43 fof(f124,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)|~ssList(X2)|~app(X1,X2)=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f121])).
% 0.12/0.43 fof(f125,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(rearsegP(U,V)<=>(?[W]: (ssList(W)&app(W,V)=U))))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.12/0.43 fof(f126,plain,(
% 0.12/0.43 ![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.12/0.43 inference(NNF_transformation,[status(thm)],[f125])).
% 0.12/0.43 fof(f127,plain,(
% 0.12/0.43 ![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.12/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W,sK6_skl(V,U))],[f126])).
% 0.12/0.43 fof(f128,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|ssList(sK6_skl(X1,X0)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f127])).
% 0.12/0.43 fof(f129,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|app(sK6_skl(X1,X0),X1)=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f127])).
% 0.12/0.43 fof(f130,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|rearsegP(X0,X1)|~ssList(X2)|~app(X2,X1)=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f127])).
% 0.12/0.43 fof(f131,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(segmentP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U))))))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.12/0.43 fof(f132,plain,(
% 0.12/0.43 ![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.12/0.43 inference(NNF_transformation,[status(thm)],[f131])).
% 0.12/0.43 fof(f133,plain,(
% 0.12/0.43 ![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.12/0.43 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.12/0.43 fof(f134,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK7_skl(X1,X0)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f133])).
% 0.12/0.43 fof(f135,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK8_skl(X1,X0)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f133])).
% 0.12/0.43 fof(f136,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|app(app(sK7_skl(X1,X0),X1),sK8_skl(X1,X0))=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f133])).
% 0.12/0.43 fof(f137,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(app(X2,X1),X3)=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f133])).
% 0.12/0.43 fof(f138,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|(cyclefreeP(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)|~leq(W,V)))))))))))))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.12/0.43 fof(f139,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|((~cyclefreeP(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)|~leq(W,V))))))))))))))&(cyclefreeP(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)&leq(W,V))))))))))))))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f138])).
% 0.12/0.43 fof(f140,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|((~cyclefreeP(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)|~leq(W,V))))))))))))))&(cyclefreeP(U)|(ssItem(sK9_skl(U))&(ssItem(sK10_skl(U))&(ssList(sK11_skl(U))&(ssList(sK12_skl(U))&(ssList(sK13_skl(U))&(app(app(sK11_skl(U),cons(sK9_skl(U),sK12_skl(U))),cons(sK10_skl(U),sK13_skl(U)))=U&(leq(sK9_skl(U),sK10_skl(U))&leq(sK10_skl(U),sK9_skl(U))))))))))))),
% 0.12/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(V,sK9_skl(U)),skolemize(W,sK10_skl(U)),skolemize(X,sK11_skl(U)),skolemize(Y,sK12_skl(U)),skolemize(Z,sK13_skl(U))],[f139])).
% 0.12/0.43 fof(f147,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|cyclefreeP(X0)|app(app(sK11_skl(X0),cons(sK9_skl(X0),sK12_skl(X0))),cons(sK10_skl(X0),sK13_skl(X0)))=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f140])).
% 0.12/0.43 fof(f221,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|ssList(cons(V,U)))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.12/0.43 fof(f222,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|ssList(cons(X1,X0)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f221])).
% 0.12/0.43 fof(f223,plain,(
% 0.12/0.43 ssList(nil)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.43 fof(f248,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|app(nil,U)=U)),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.12/0.43 fof(f249,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f248])).
% 0.12/0.43 fof(f268,plain,(
% 0.12/0.43 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(memberP(app(V,W),U)<=>(memberP(V,U)|memberP(W,U))))))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.12/0.43 fof(f269,plain,(
% 0.12/0.43 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|((~memberP(app(V,W),U)|(memberP(V,U)|memberP(W,U)))&(memberP(app(V,W),U)|(~memberP(V,U)&~memberP(W,U)))))))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f268])).
% 0.12/0.43 fof(f270,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~memberP(app(X1,X2),X0)|memberP(X1,X0)|memberP(X2,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f269])).
% 0.12/0.43 fof(f271,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X1,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f269])).
% 0.12/0.43 fof(f272,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X2,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f269])).
% 0.12/0.43 fof(f273,plain,(
% 0.12/0.43 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(![W]: (~ssList(W)|(memberP(cons(V,W),U)<=>(U=V|memberP(W,U))))))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.12/0.43 fof(f274,plain,(
% 0.12/0.43 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(![W]: (~ssList(W)|((~memberP(cons(V,W),U)|(U=V|memberP(W,U)))&(memberP(cons(V,W),U)|(~U=V&~memberP(W,U)))))))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f273])).
% 0.12/0.43 fof(f275,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~memberP(cons(X1,X2),X0)|X0=X1|memberP(X2,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f274])).
% 0.12/0.43 fof(f277,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|memberP(cons(X1,X2),X0)|~memberP(X2,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f274])).
% 0.12/0.43 fof(f278,plain,(
% 0.12/0.43 ![U]: (~ssItem(U)|~memberP(nil,U))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.12/0.43 fof(f279,plain,(
% 0.12/0.43 ![X0]: (~ssItem(X0)|~memberP(nil,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f278])).
% 0.12/0.43 fof(f294,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|frontsegP(U,nil))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.12/0.43 fof(f295,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f294])).
% 0.12/0.43 fof(f308,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|rearsegP(U,nil))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.12/0.43 fof(f309,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f308])).
% 0.12/0.43 fof(f322,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|segmentP(U,nil))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.12/0.43 fof(f323,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f322])).
% 0.12/0.43 fof(f388,plain,(
% 0.12/0.43 ![U]: (~ssList(U)|app(U,nil)=U)),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 0.12/0.43 fof(f389,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f388])).
% 0.12/0.43 fof(f415,plain,(
% 0.12/0.43 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((V=X&U=W)&(?[Y]: (ssItem(Y)&(memberP(U,Y)&~memberP(V,Y)))))&((?[Z]: (ssItem(Z)&(cons(Z,nil)=W&memberP(X,Z))))|(nil=X&nil=W)))))))))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.12/0.43 fof(f416,definition,(
% 0.12/0.43 ![W,X,Z]: (sP0_prd(Z,X,W)<=>(ssItem(Z)&(cons(Z,nil)=W&memberP(X,Z))))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.12/0.43 fof(f417,plain,(
% 0.12/0.43 ?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((V=X&U=W)&(?[Y]: (ssItem(Y)&(memberP(U,Y)&~memberP(V,Y)))))&((?[Z]: sP0_prd(Z,X,W))|(nil=X&nil=W))))))))))),
% 0.12/0.43 inference(formula_renaming,[status(thm)],[f415,f416])).
% 0.12/0.43 fof(f418,plain,(
% 0.12/0.43 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(ssList(sK50_skl)&(((sK48_skl=sK50_skl&sK47_skl=sK49_skl)&(ssItem(sK51_skl)&(memberP(sK47_skl,sK51_skl)&~memberP(sK48_skl,sK51_skl))))&(sP0_prd(sK52_skl,sK50_skl,sK49_skl)|(nil=sK50_skl&nil=sK49_skl)))))))),
% 0.12/0.43 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.12/0.43 fof(f419,plain,(
% 0.12/0.43 ssList(sK47_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f418])).
% 0.12/0.43 fof(f420,plain,(
% 0.12/0.43 ssList(sK48_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f418])).
% 0.12/0.43 fof(f423,plain,(
% 0.12/0.43 sK48_skl=sK50_skl),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f418])).
% 0.12/0.43 fof(f424,plain,(
% 0.12/0.43 sK47_skl=sK49_skl),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f418])).
% 0.12/0.43 fof(f425,plain,(
% 0.12/0.43 ssItem(sK51_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f418])).
% 0.12/0.43 fof(f426,plain,(
% 0.12/0.43 memberP(sK47_skl,sK51_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f418])).
% 0.12/0.43 fof(f427,plain,(
% 0.12/0.43 ~memberP(sK48_skl,sK51_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f418])).
% 0.12/0.43 fof(f428,plain,(
% 0.12/0.43 sP0_prd(sK52_skl,sK50_skl,sK49_skl)|nil=sK50_skl),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f418])).
% 0.12/0.43 fof(f429,plain,(
% 0.12/0.43 sP0_prd(sK52_skl,sK50_skl,sK49_skl)|nil=sK49_skl),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f418])).
% 0.12/0.43 fof(f430,plain,(
% 0.12/0.43 ![W,X,Z]: ((~sP0_prd(Z,X,W)|(ssItem(Z)&(cons(Z,nil)=W&memberP(X,Z))))&(sP0_prd(Z,X,W)|(~ssItem(Z)|(~cons(Z,nil)=W|~memberP(X,Z)))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f416])).
% 0.12/0.43 fof(f431,plain,(
% 0.12/0.43 (![W,X,Z]: (~sP0_prd(Z,X,W)|(ssItem(Z)&(cons(Z,nil)=W&memberP(X,Z)))))&(![W,X,Z]: (sP0_prd(Z,X,W)|(~ssItem(Z)|(~cons(Z,nil)=W|~memberP(X,Z)))))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f430])).
% 0.12/0.43 fof(f432,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ssItem(X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f431])).
% 0.12/0.43 fof(f433,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|cons(X0,nil)=X2)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f431])).
% 0.12/0.43 fof(f434,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|memberP(X1,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f431])).
% 0.12/0.43 fof(f435,plain,(
% 0.12/0.43 ![X0,X1,X2]: (sP0_prd(X0,X1,X2)|~ssItem(X0)|~cons(X0,nil)=X2|~memberP(X1,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f431])).
% 0.12/0.43 fof(f436,definition,(
% 0.12/0.43 sQ0_spl <=> (sP0_prd(sK52_skl,sK50_skl,sK49_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f437,plain,(
% 0.12/0.43 sP0_prd(sK52_skl,sK50_skl,sK49_skl)|~sQ0_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f436])).
% 0.12/0.43 fof(f439,definition,(
% 0.12/0.43 sQ1_spl <=> (nil=sK50_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f440,plain,(
% 0.12/0.43 nil=sK50_skl|~sQ1_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f439])).
% 0.12/0.43 fof(f442,plain,(
% 0.12/0.43 sQ0_spl|sQ1_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f428,f436,f439])).
% 0.12/0.43 fof(f443,definition,(
% 0.12/0.43 sQ2_spl <=> (nil=sK49_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f444,plain,(
% 0.12/0.43 nil=sK49_skl|~sQ2_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f443])).
% 0.12/0.43 fof(f446,plain,(
% 0.12/0.43 sQ0_spl|sQ2_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f429,f436,f443])).
% 0.12/0.43 fof(f449,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~ssList(app(X0,cons(X1,X2)))|~ssItem(X1)|memberP(app(X0,cons(X1,X2)),X1)|~ssList(X0)|~ssList(X2))),
% 0.12/0.43 inference(destructive_equality_resolution,[status(thm)],[f112])).
% 0.12/0.43 fof(f450,plain,(
% 0.12/0.43 ![X0]: (~ssList(cons(X0,nil))|singletonP(cons(X0,nil))|~ssItem(X0))),
% 0.12/0.43 inference(destructive_equality_resolution,[status(thm)],[f118])).
% 0.12/0.43 fof(f451,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 0.12/0.43 inference(destructive_equality_resolution,[status(thm)],[f124])).
% 0.12/0.43 fof(f452,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|rearsegP(app(X0,X1),X1)|~ssList(X0))),
% 0.12/0.43 inference(destructive_equality_resolution,[status(thm)],[f130])).
% 0.12/0.43 fof(f453,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~ssList(app(app(X0,X1),X2))|~ssList(X1)|segmentP(app(app(X0,X1),X2),X1)|~ssList(X0)|~ssList(X2))),
% 0.12/0.43 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 0.12/0.43 fof(f477,plain,(
% 0.12/0.43 ![X0,X1]: (sP0_prd(X0,X1,cons(X0,nil))|~ssItem(X0)|~memberP(X1,X0))),
% 0.12/0.43 inference(destructive_equality_resolution,[status(thm)],[f435])).
% 0.12/0.43 fof(f481,plain,(
% 0.12/0.43 sP0_prd(sK52_skl,sK48_skl,sK49_skl)|~sQ0_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f423,f437])).
% 0.12/0.43 fof(f482,plain,(
% 0.12/0.43 sP0_prd(sK52_skl,sK48_skl,sK47_skl)|~sQ0_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f424,f481])).
% 0.12/0.43 fof(f483,plain,(
% 0.12/0.43 ssItem(sK52_skl)|~sQ0_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f482,f432])).
% 0.12/0.43 fof(f484,plain,(
% 0.12/0.43 cons(sK52_skl,nil)=sK47_skl|~sQ0_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f433,f482])).
% 0.12/0.43 fof(f485,plain,(
% 0.12/0.43 ~ssList(nil)|~ssItem(sK52_skl)|ssList(sK47_skl)|~sQ0_spl),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f484,f222])).
% 0.12/0.43 fof(f487,definition,(
% 0.12/0.43 sQ3_spl <=> (ssList(nil))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f489,plain,(
% 0.12/0.43 ~ssList(nil)|sQ3_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f487])).
% 0.12/0.43 fof(f490,definition,(
% 0.12/0.43 sQ4_spl <=> (ssItem(sK52_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f492,plain,(
% 0.12/0.43 ~ssItem(sK52_skl)|sQ4_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f490])).
% 0.12/0.43 fof(f493,definition,(
% 0.12/0.43 sQ5_spl <=> (ssList(sK47_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f496,plain,(
% 0.12/0.43 ~sQ3_spl|~sQ4_spl|sQ5_spl|~sQ0_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f485,f487,f490,f493,f436])).
% 0.12/0.43 fof(f501,plain,(
% 0.12/0.43 $false|sQ3_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f489,f223])).
% 0.12/0.43 fof(f502,plain,(
% 0.12/0.43 sQ3_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f501])).
% 0.12/0.43 fof(f503,plain,(
% 0.12/0.43 sK48_skl=nil|~sQ1_spl),
% 0.12/0.43 inference(backward_demodulation,[status(thm)],[f440,f423])).
% 0.12/0.43 fof(f504,plain,(
% 0.12/0.43 sK47_skl=nil|~sQ2_spl),
% 0.12/0.43 inference(backward_demodulation,[status(thm)],[f444,f424])).
% 0.12/0.43 fof(f505,plain,(
% 0.12/0.43 ~memberP(nil,sK51_skl)|~sQ1_spl),
% 0.12/0.43 inference(backward_demodulation,[status(thm)],[f503,f427])).
% 0.12/0.43 fof(f513,plain,(
% 0.12/0.43 memberP(nil,sK51_skl)|~sQ2_spl),
% 0.12/0.43 inference(backward_demodulation,[status(thm)],[f504,f426])).
% 0.12/0.43 fof(f515,plain,(
% 0.12/0.43 $false|~sQ1_spl|~sQ2_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f513,f505])).
% 0.12/0.43 fof(f516,plain,(
% 0.12/0.43 ~sQ1_spl|~sQ2_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f515])).
% 0.12/0.43 fof(f517,plain,(
% 0.12/0.43 $false|sQ4_spl|~sQ0_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f483,f492])).
% 0.12/0.43 fof(f518,plain,(
% 0.12/0.43 sQ4_spl|~sQ0_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f517])).
% 0.12/0.43 fof(f522,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssItem(sK51_skl)|app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)))=sK47_skl),
% 0.12/0.43 inference(resolution,[status(thm)],[f426,f111])).
% 0.12/0.43 fof(f523,definition,(
% 0.12/0.43 sQ7_spl <=> (ssItem(sK51_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f525,plain,(
% 0.12/0.43 ~ssItem(sK51_skl)|sQ7_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f523])).
% 0.12/0.43 fof(f526,definition,(
% 0.12/0.43 sQ8_spl <=> (app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)))=sK47_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f527,plain,(
% 0.12/0.43 app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)))=sK47_skl|~sQ8_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f526])).
% 0.12/0.43 fof(f529,plain,(
% 0.12/0.43 ~sQ5_spl|~sQ7_spl|sQ8_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f522,f493,f523,f526])).
% 0.12/0.43 fof(f530,plain,(
% 0.12/0.43 $false|sQ7_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f525,f425])).
% 0.12/0.43 fof(f531,plain,(
% 0.12/0.43 sQ7_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f530])).
% 0.12/0.43 fof(f532,plain,(
% 0.12/0.43 memberP(sK48_skl,sK52_skl)|~sQ0_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f482,f434])).
% 0.12/0.43 fof(f536,definition,(
% 0.12/0.43 sQ9_spl <=> (ssList(sK48_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f538,plain,(
% 0.12/0.43 ~ssList(sK48_skl)|sQ9_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f536])).
% 0.12/0.43 fof(f543,plain,(
% 0.12/0.43 $false|sQ9_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f538,f420])).
% 0.12/0.43 fof(f544,plain,(
% 0.12/0.43 sQ9_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f543])).
% 0.12/0.43 fof(f558,plain,(
% 0.12/0.43 ![X0]: (singletonP(cons(X0,nil))|~ssItem(X0)|~ssList(nil)|~ssItem(X0))),
% 0.12/0.43 inference(resolution,[status(thm)],[f450,f222])).
% 0.12/0.43 fof(f560,definition,(
% 0.12/0.43 ![X0]: (sQ11_spl <=> (singletonP(cons(X0,nil))|~ssItem(X0)|~ssItem(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f563,plain,(
% 0.12/0.43 sQ11_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f558,f560,f487])).
% 0.12/0.43 fof(f585,plain,(
% 0.12/0.43 sP0_prd(sK51_skl,sK47_skl,cons(sK51_skl,nil))|~ssItem(sK51_skl)),
% 0.12/0.43 inference(resolution,[status(thm)],[f477,f426])).
% 0.12/0.43 fof(f590,definition,(
% 0.12/0.43 sQ16_spl <=> (sP0_prd(sK51_skl,sK47_skl,cons(sK51_skl,nil)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f593,plain,(
% 0.12/0.43 sQ16_spl|~sQ7_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f585,f590,f523])).
% 0.12/0.43 fof(f610,plain,(
% 0.12/0.43 ![X0]: (~ssItem(sK51_skl)|~ssList(sK47_skl)|~ssList(X0)|memberP(app(sK47_skl,X0),sK51_skl))),
% 0.12/0.43 inference(resolution,[status(thm)],[f271,f426])).
% 0.12/0.43 fof(f615,definition,(
% 0.12/0.43 ![X0]: (sQ18_spl <=> (~ssList(X0)|memberP(app(sK47_skl,X0),sK51_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f618,plain,(
% 0.12/0.43 ~sQ7_spl|~sQ5_spl|sQ18_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f610,f523,f493,f615])).
% 0.12/0.43 fof(f621,plain,(
% 0.12/0.43 app(nil,sK47_skl)=sK47_skl),
% 0.12/0.43 inference(resolution,[status(thm)],[f249,f419])).
% 0.12/0.43 fof(f622,plain,(
% 0.12/0.43 app(nil,sK48_skl)=sK48_skl),
% 0.12/0.43 inference(resolution,[status(thm)],[f249,f420])).
% 0.12/0.43 fof(f625,plain,(
% 0.12/0.43 app(nil,nil)=nil),
% 0.12/0.43 inference(resolution,[status(thm)],[f249,f223])).
% 0.12/0.43 fof(f626,plain,(
% 0.12/0.43 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK47_skl)|~memberP(sK47_skl,X0)|memberP(nil,X0)|memberP(sK47_skl,X0))),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f621,f270])).
% 0.12/0.43 fof(f627,definition,(
% 0.12/0.43 ![X0]: (sQ19_spl <=> (~ssItem(X0)|~memberP(sK47_skl,X0)|memberP(nil,X0)|memberP(sK47_skl,X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f630,plain,(
% 0.12/0.43 sQ19_spl|~sQ3_spl|~sQ5_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f626,f627,f487,f493])).
% 0.12/0.43 fof(f631,plain,(
% 0.12/0.43 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(sK48_skl)|~memberP(sK48_skl,X0)|memberP(nil,X0)|memberP(sK48_skl,X0))),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f622,f270])).
% 0.12/0.43 fof(f632,definition,(
% 0.12/0.43 ![X0]: (sQ20_spl <=> (~ssItem(X0)|~memberP(sK48_skl,X0)|memberP(nil,X0)|memberP(sK48_skl,X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f635,plain,(
% 0.12/0.43 sQ20_spl|~sQ3_spl|~sQ9_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f631,f632,f487,f536])).
% 0.12/0.43 fof(f636,plain,(
% 0.12/0.43 ![X0]: (~ssItem(X0)|~ssList(nil)|~ssList(nil)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0))),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f625,f270])).
% 0.12/0.43 fof(f637,definition,(
% 0.12/0.43 ![X0]: (sQ21_spl <=> (~ssItem(X0)|~memberP(nil,X0)|memberP(nil,X0)|memberP(nil,X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f640,plain,(
% 0.12/0.43 sQ21_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f636,f637,f487])).
% 0.12/0.43 fof(f643,plain,(
% 0.12/0.43 app(sK47_skl,nil)=sK47_skl),
% 0.12/0.43 inference(resolution,[status(thm)],[f389,f419])).
% 0.12/0.43 fof(f644,plain,(
% 0.12/0.43 app(sK48_skl,nil)=sK48_skl),
% 0.12/0.43 inference(resolution,[status(thm)],[f389,f420])).
% 0.12/0.43 fof(f648,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0))),
% 0.12/0.43 inference(resolution,[status(thm)],[f123,f295])).
% 0.12/0.43 fof(f650,definition,(
% 0.12/0.43 ![X0]: (sQ22_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f653,plain,(
% 0.12/0.43 sQ22_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f648,f650,f487])).
% 0.12/0.43 fof(f656,plain,(
% 0.12/0.43 ~ssList(nil)|~ssList(nil)|frontsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f625,f451])).
% 0.12/0.43 fof(f657,plain,(
% 0.12/0.43 ~ssList(sK48_skl)|~ssList(nil)|frontsegP(app(nil,sK48_skl),nil)|~ssList(sK48_skl)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f622,f451])).
% 0.12/0.43 fof(f658,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(nil)|frontsegP(app(nil,sK47_skl),nil)|~ssList(sK47_skl)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f621,f451])).
% 0.12/0.43 fof(f659,definition,(
% 0.12/0.43 sQ23_spl <=> (frontsegP(app(nil,nil),nil))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f660,plain,(
% 0.12/0.43 frontsegP(app(nil,nil),nil)|~sQ23_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f659])).
% 0.12/0.43 fof(f662,plain,(
% 0.12/0.43 ~sQ3_spl|sQ23_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f656,f487,f659])).
% 0.12/0.43 fof(f663,definition,(
% 0.12/0.43 sQ24_spl <=> (frontsegP(app(nil,sK48_skl),nil))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f664,plain,(
% 0.12/0.43 frontsegP(app(nil,sK48_skl),nil)|~sQ24_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f663])).
% 0.12/0.43 fof(f666,plain,(
% 0.12/0.43 ~sQ9_spl|~sQ3_spl|sQ24_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f657,f536,f487,f663])).
% 0.12/0.43 fof(f667,definition,(
% 0.12/0.43 sQ25_spl <=> (frontsegP(app(nil,sK47_skl),nil))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f668,plain,(
% 0.12/0.43 frontsegP(app(nil,sK47_skl),nil)|~sQ25_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f667])).
% 0.12/0.43 fof(f670,plain,(
% 0.12/0.43 ~sQ5_spl|~sQ3_spl|sQ25_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f658,f493,f487,f667])).
% 0.12/0.43 fof(f671,plain,(
% 0.12/0.43 frontsegP(nil,nil)|~sQ23_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f625,f660])).
% 0.12/0.43 fof(f672,plain,(
% 0.12/0.43 frontsegP(sK48_skl,nil)|~sQ24_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f622,f664])).
% 0.12/0.43 fof(f673,plain,(
% 0.12/0.43 frontsegP(sK47_skl,nil)|~sQ25_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f621,f668])).
% 0.12/0.43 fof(f674,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK6_skl(nil,X0))|~ssList(X0))),
% 0.12/0.43 inference(resolution,[status(thm)],[f128,f309])).
% 0.12/0.43 fof(f676,definition,(
% 0.12/0.43 ![X0]: (sQ26_spl <=> (~ssList(X0)|ssList(sK6_skl(nil,X0))|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f679,plain,(
% 0.12/0.43 sQ26_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f674,f676,f487])).
% 0.12/0.43 fof(f682,plain,(
% 0.12/0.43 ~ssList(sK48_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK48_skl))=sK48_skl|~sQ24_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f672,f123])).
% 0.12/0.43 fof(f683,definition,(
% 0.12/0.43 sQ27_spl <=> (app(nil,sK5_skl(nil,sK48_skl))=sK48_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f686,plain,(
% 0.12/0.43 ~sQ9_spl|~sQ3_spl|sQ27_spl|~sQ24_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f682,f536,f487,f683,f663])).
% 0.12/0.43 fof(f687,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK47_skl))=sK47_skl|~sQ25_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f673,f123])).
% 0.12/0.43 fof(f688,definition,(
% 0.12/0.43 sQ28_spl <=> (app(nil,sK5_skl(nil,sK47_skl))=sK47_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f691,plain,(
% 0.12/0.43 ~sQ5_spl|~sQ3_spl|sQ28_spl|~sQ25_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f687,f493,f487,f688,f667])).
% 0.12/0.43 fof(f692,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(sK47_skl)|frontsegP(app(sK47_skl,nil),sK47_skl)|~ssList(nil)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f643,f451])).
% 0.12/0.43 fof(f694,definition,(
% 0.12/0.43 sQ29_spl <=> (frontsegP(app(sK47_skl,nil),sK47_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f695,plain,(
% 0.12/0.43 frontsegP(app(sK47_skl,nil),sK47_skl)|~sQ29_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f694])).
% 0.12/0.43 fof(f697,plain,(
% 0.12/0.43 ~sQ5_spl|sQ29_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f692,f493,f694,f487])).
% 0.12/0.43 fof(f699,plain,(
% 0.12/0.43 frontsegP(sK47_skl,sK47_skl)|~sQ29_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f643,f695])).
% 0.12/0.43 fof(f707,plain,(
% 0.12/0.43 ~ssList(nil)|~ssList(nil)|app(nil,sK5_skl(nil,nil))=nil|~sQ23_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f671,f123])).
% 0.12/0.43 fof(f708,definition,(
% 0.12/0.43 sQ30_spl <=> (app(nil,sK5_skl(nil,nil))=nil)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f711,plain,(
% 0.12/0.43 ~sQ3_spl|sQ30_spl|~sQ23_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f707,f487,f708,f659])).
% 0.12/0.43 fof(f712,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(sK47_skl)|app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl|~sQ29_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f699,f123])).
% 0.12/0.43 fof(f713,definition,(
% 0.12/0.43 sQ31_spl <=> (app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f716,plain,(
% 0.12/0.43 ~sQ5_spl|sQ31_spl|~sQ29_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f712,f493,f713,f694])).
% 0.12/0.43 fof(f717,plain,(
% 0.12/0.43 ~ssList(sK48_skl)|~ssList(sK48_skl)|frontsegP(app(sK48_skl,nil),sK48_skl)|~ssList(nil)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f644,f451])).
% 0.12/0.43 fof(f719,definition,(
% 0.12/0.43 sQ32_spl <=> (frontsegP(app(sK48_skl,nil),sK48_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f720,plain,(
% 0.12/0.43 frontsegP(app(sK48_skl,nil),sK48_skl)|~sQ32_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f719])).
% 0.12/0.43 fof(f722,plain,(
% 0.12/0.43 ~sQ9_spl|sQ32_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f717,f536,f719,f487])).
% 0.12/0.43 fof(f724,plain,(
% 0.12/0.43 frontsegP(sK48_skl,sK48_skl)|~sQ32_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f644,f720])).
% 0.12/0.43 fof(f725,plain,(
% 0.12/0.43 ~ssList(sK48_skl)|~ssList(sK48_skl)|app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))=sK48_skl|~sQ32_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f724,f123])).
% 0.12/0.43 fof(f726,definition,(
% 0.12/0.43 sQ33_spl <=> (app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))=sK48_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f729,plain,(
% 0.12/0.43 ~sQ9_spl|sQ33_spl|~sQ32_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f725,f536,f726,f719])).
% 0.12/0.43 fof(f731,plain,(
% 0.12/0.43 ![X0]: (~ssItem(sK51_skl)|~ssList(X0)|~ssList(sK47_skl)|memberP(app(X0,sK47_skl),sK51_skl))),
% 0.12/0.43 inference(resolution,[status(thm)],[f272,f426])).
% 0.12/0.43 fof(f736,definition,(
% 0.12/0.43 ![X0]: (sQ35_spl <=> (~ssList(X0)|memberP(app(X0,sK47_skl),sK51_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f739,plain,(
% 0.12/0.43 ~sQ7_spl|sQ35_spl|~sQ5_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f731,f523,f736,f493])).
% 0.12/0.43 fof(f740,plain,(
% 0.12/0.43 ![X0]: (~ssItem(X0)|~ssItem(sK52_skl)|~ssList(nil)|~memberP(sK47_skl,X0)|X0=sK52_skl|memberP(nil,X0)|~sQ0_spl)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f484,f275])).
% 0.12/0.43 fof(f741,definition,(
% 0.12/0.43 ![X0]: (sQ36_spl <=> (~ssItem(X0)|~memberP(sK47_skl,X0)|X0=sK52_skl|memberP(nil,X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f742,plain,(
% 0.12/0.43 ![X0]: (~ssItem(X0)|~memberP(sK47_skl,X0)|X0=sK52_skl|memberP(nil,X0)|~sQ36_spl)),
% 0.12/0.43 inference(component_clause,[status(thm)],[f741])).
% 0.12/0.43 fof(f744,plain,(
% 0.12/0.43 sQ36_spl|~sQ4_spl|~sQ3_spl|~sQ0_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f740,f741,f490,f487,f436])).
% 0.12/0.43 fof(f745,plain,(
% 0.12/0.43 ![X0]: (~ssItem(X0)|~memberP(sK47_skl,X0)|X0=sK52_skl|~sQ36_spl)),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f742,f279])).
% 0.12/0.43 fof(f760,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|~ssList(nil)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0))),
% 0.12/0.43 inference(resolution,[status(thm)],[f129,f309])).
% 0.12/0.43 fof(f762,definition,(
% 0.12/0.43 ![X0]: (sQ37_spl <=> (~ssList(X0)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f765,plain,(
% 0.12/0.43 sQ37_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f760,f762,f487])).
% 0.12/0.43 fof(f768,plain,(
% 0.12/0.43 ~ssList(sK48_skl)|~ssList(nil)|rearsegP(app(sK48_skl,nil),nil)|~ssList(sK48_skl)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f644,f452])).
% 0.12/0.43 fof(f769,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(nil)|rearsegP(app(sK47_skl,nil),nil)|~ssList(sK47_skl)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f643,f452])).
% 0.12/0.43 fof(f770,plain,(
% 0.12/0.43 ~ssList(nil)|~ssList(nil)|rearsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f625,f452])).
% 0.12/0.43 fof(f771,plain,(
% 0.12/0.43 ~ssList(sK48_skl)|~ssList(sK48_skl)|rearsegP(app(nil,sK48_skl),sK48_skl)|~ssList(nil)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f622,f452])).
% 0.12/0.43 fof(f772,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(sK47_skl)|rearsegP(app(nil,sK47_skl),sK47_skl)|~ssList(nil)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f621,f452])).
% 0.12/0.43 fof(f773,definition,(
% 0.12/0.43 sQ38_spl <=> (rearsegP(app(sK48_skl,nil),nil))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f774,plain,(
% 0.12/0.43 rearsegP(app(sK48_skl,nil),nil)|~sQ38_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f773])).
% 0.12/0.43 fof(f776,plain,(
% 0.12/0.43 ~sQ9_spl|~sQ3_spl|sQ38_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f768,f536,f487,f773])).
% 0.12/0.43 fof(f777,definition,(
% 0.12/0.43 sQ39_spl <=> (rearsegP(app(sK47_skl,nil),nil))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f778,plain,(
% 0.12/0.43 rearsegP(app(sK47_skl,nil),nil)|~sQ39_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f777])).
% 0.12/0.43 fof(f780,plain,(
% 0.12/0.43 ~sQ5_spl|~sQ3_spl|sQ39_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f769,f493,f487,f777])).
% 0.12/0.43 fof(f781,definition,(
% 0.12/0.43 sQ40_spl <=> (rearsegP(app(nil,nil),nil))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f782,plain,(
% 0.12/0.43 rearsegP(app(nil,nil),nil)|~sQ40_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f781])).
% 0.12/0.43 fof(f784,plain,(
% 0.12/0.43 ~sQ3_spl|sQ40_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f770,f487,f781])).
% 0.12/0.43 fof(f785,definition,(
% 0.12/0.43 sQ41_spl <=> (rearsegP(app(nil,sK48_skl),sK48_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f786,plain,(
% 0.12/0.43 rearsegP(app(nil,sK48_skl),sK48_skl)|~sQ41_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f785])).
% 0.12/0.43 fof(f788,plain,(
% 0.12/0.43 ~sQ9_spl|sQ41_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f771,f536,f785,f487])).
% 0.12/0.43 fof(f789,definition,(
% 0.12/0.43 sQ42_spl <=> (rearsegP(app(nil,sK47_skl),sK47_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f790,plain,(
% 0.12/0.43 rearsegP(app(nil,sK47_skl),sK47_skl)|~sQ42_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f789])).
% 0.12/0.43 fof(f792,plain,(
% 0.12/0.43 ~sQ5_spl|sQ42_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f772,f493,f789,f487])).
% 0.12/0.43 fof(f793,plain,(
% 0.12/0.43 rearsegP(sK48_skl,nil)|~sQ38_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f644,f774])).
% 0.12/0.43 fof(f794,plain,(
% 0.12/0.43 rearsegP(nil,nil)|~sQ40_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f625,f782])).
% 0.12/0.43 fof(f795,plain,(
% 0.12/0.43 rearsegP(sK48_skl,sK48_skl)|~sQ41_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f622,f786])).
% 0.12/0.43 fof(f796,plain,(
% 0.12/0.43 rearsegP(sK47_skl,nil)|~sQ39_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f643,f778])).
% 0.12/0.43 fof(f797,plain,(
% 0.12/0.43 rearsegP(sK47_skl,sK47_skl)|~sQ42_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f621,f790])).
% 0.12/0.43 fof(f798,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK7_skl(nil,X0))|~ssList(X0))),
% 0.12/0.43 inference(resolution,[status(thm)],[f134,f323])).
% 0.12/0.43 fof(f800,definition,(
% 0.12/0.43 ![X0]: (sQ43_spl <=> (~ssList(X0)|ssList(sK7_skl(nil,X0))|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f803,plain,(
% 0.12/0.43 sQ43_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f798,f800,f487])).
% 0.12/0.43 fof(f806,plain,(
% 0.12/0.43 ~ssList(sK48_skl)|~ssList(nil)|app(sK6_skl(nil,sK48_skl),nil)=sK48_skl|~sQ38_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f793,f129])).
% 0.12/0.43 fof(f807,plain,(
% 0.12/0.43 ~ssList(sK48_skl)|~ssList(nil)|ssList(sK6_skl(nil,sK48_skl))|~sQ38_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f793,f128])).
% 0.12/0.43 fof(f808,definition,(
% 0.12/0.43 sQ44_spl <=> (app(sK6_skl(nil,sK48_skl),nil)=sK48_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f811,plain,(
% 0.12/0.43 ~sQ9_spl|~sQ3_spl|sQ44_spl|~sQ38_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f806,f536,f487,f808,f773])).
% 0.12/0.43 fof(f812,definition,(
% 0.12/0.43 sQ45_spl <=> (ssList(sK6_skl(nil,sK48_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f813,plain,(
% 0.12/0.43 ssList(sK6_skl(nil,sK48_skl))|~sQ45_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f812])).
% 0.12/0.43 fof(f815,plain,(
% 0.12/0.43 ~sQ9_spl|~sQ3_spl|sQ45_spl|~sQ38_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f807,f536,f487,f812,f773])).
% 0.12/0.43 fof(f816,plain,(
% 0.12/0.43 ~ssList(sK48_skl)|~ssList(sK48_skl)|app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)=sK48_skl|~sQ41_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f795,f129])).
% 0.12/0.43 fof(f817,plain,(
% 0.12/0.43 ~ssList(sK48_skl)|~ssList(sK48_skl)|ssList(sK6_skl(sK48_skl,sK48_skl))|~sQ41_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f795,f128])).
% 0.12/0.43 fof(f818,definition,(
% 0.12/0.43 sQ46_spl <=> (app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)=sK48_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f821,plain,(
% 0.12/0.43 ~sQ9_spl|sQ46_spl|~sQ41_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f816,f536,f818,f785])).
% 0.12/0.43 fof(f822,definition,(
% 0.12/0.43 sQ47_spl <=> (ssList(sK6_skl(sK48_skl,sK48_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f823,plain,(
% 0.12/0.43 ssList(sK6_skl(sK48_skl,sK48_skl))|~sQ47_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f822])).
% 0.12/0.43 fof(f825,plain,(
% 0.12/0.43 ~sQ9_spl|sQ47_spl|~sQ41_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f817,f536,f822,f785])).
% 0.12/0.43 fof(f826,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(nil)|app(sK6_skl(nil,sK47_skl),nil)=sK47_skl|~sQ39_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f796,f129])).
% 0.12/0.43 fof(f827,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(nil)|ssList(sK6_skl(nil,sK47_skl))|~sQ39_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f796,f128])).
% 0.12/0.43 fof(f828,definition,(
% 0.12/0.43 sQ48_spl <=> (app(sK6_skl(nil,sK47_skl),nil)=sK47_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f831,plain,(
% 0.12/0.43 ~sQ5_spl|~sQ3_spl|sQ48_spl|~sQ39_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f826,f493,f487,f828,f777])).
% 0.12/0.43 fof(f832,definition,(
% 0.12/0.43 sQ49_spl <=> (ssList(sK6_skl(nil,sK47_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f833,plain,(
% 0.12/0.43 ssList(sK6_skl(nil,sK47_skl))|~sQ49_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f832])).
% 0.12/0.43 fof(f835,plain,(
% 0.12/0.43 ~sQ5_spl|~sQ3_spl|sQ49_spl|~sQ39_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f827,f493,f487,f832,f777])).
% 0.12/0.43 fof(f851,definition,(
% 0.12/0.43 sQ53_spl <=> (sK52_skl=sK51_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f852,plain,(
% 0.12/0.43 sK52_skl=sK51_skl|~sQ53_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f851])).
% 0.12/0.43 fof(f876,plain,(
% 0.12/0.43 ~ssList(nil)|~ssList(nil)|app(sK6_skl(nil,nil),nil)=nil|~sQ40_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f794,f129])).
% 0.12/0.43 fof(f877,plain,(
% 0.12/0.43 ~ssList(nil)|~ssList(nil)|ssList(sK6_skl(nil,nil))|~sQ40_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f794,f128])).
% 0.12/0.43 fof(f878,definition,(
% 0.12/0.43 sQ60_spl <=> (app(sK6_skl(nil,nil),nil)=nil)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f881,plain,(
% 0.12/0.43 ~sQ3_spl|sQ60_spl|~sQ40_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f876,f487,f878,f781])).
% 0.12/0.43 fof(f882,definition,(
% 0.12/0.43 sQ61_spl <=> (ssList(sK6_skl(nil,nil)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f883,plain,(
% 0.12/0.43 ssList(sK6_skl(nil,nil))|~sQ61_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f882])).
% 0.12/0.43 fof(f885,plain,(
% 0.12/0.43 ~sQ3_spl|sQ61_spl|~sQ40_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f877,f487,f882,f781])).
% 0.12/0.43 fof(f886,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(sK47_skl)|app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)=sK47_skl|~sQ42_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f797,f129])).
% 0.12/0.43 fof(f887,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(sK47_skl)|ssList(sK6_skl(sK47_skl,sK47_skl))|~sQ42_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f797,f128])).
% 0.12/0.43 fof(f888,definition,(
% 0.12/0.43 sQ62_spl <=> (app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)=sK47_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f891,plain,(
% 0.12/0.43 ~sQ5_spl|sQ62_spl|~sQ42_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f886,f493,f888,f789])).
% 0.12/0.43 fof(f892,definition,(
% 0.12/0.43 sQ63_spl <=> (ssList(sK6_skl(sK47_skl,sK47_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f893,plain,(
% 0.12/0.43 ssList(sK6_skl(sK47_skl,sK47_skl))|~sQ63_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f892])).
% 0.12/0.43 fof(f895,plain,(
% 0.12/0.43 ~sQ5_spl|sQ63_spl|~sQ42_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f887,f493,f892,f789])).
% 0.12/0.43 fof(f926,plain,(
% 0.12/0.43 ![X0]: (~ssItem(sK51_skl)|~ssItem(X0)|~ssList(sK47_skl)|memberP(cons(X0,sK47_skl),sK51_skl))),
% 0.12/0.43 inference(resolution,[status(thm)],[f277,f426])).
% 0.12/0.43 fof(f931,definition,(
% 0.12/0.43 ![X0]: (sQ65_spl <=> (~ssItem(X0)|memberP(cons(X0,sK47_skl),sK51_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f934,plain,(
% 0.12/0.43 ~sQ7_spl|sQ65_spl|~sQ5_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f926,f523,f931,f493])).
% 0.12/0.43 fof(f967,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK8_skl(nil,X0))|~ssList(X0))),
% 0.12/0.43 inference(resolution,[status(thm)],[f135,f323])).
% 0.12/0.43 fof(f969,definition,(
% 0.12/0.43 ![X0]: (sQ70_spl <=> (~ssList(X0)|ssList(sK8_skl(nil,X0))|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f972,plain,(
% 0.12/0.43 sQ70_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f967,f969,f487])).
% 0.12/0.43 fof(f975,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|~ssList(nil)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0))),
% 0.12/0.43 inference(resolution,[status(thm)],[f136,f323])).
% 0.12/0.43 fof(f977,definition,(
% 0.12/0.43 ![X0]: (sQ71_spl <=> (~ssList(X0)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f980,plain,(
% 0.12/0.43 sQ71_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f975,f977,f487])).
% 0.12/0.43 fof(f983,plain,(
% 0.12/0.43 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(nil)|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(sK48_skl)|~ssList(X0))),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f644,f453])).
% 0.12/0.43 fof(f984,plain,(
% 0.12/0.43 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(nil)|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(sK47_skl)|~ssList(X0))),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f643,f453])).
% 0.12/0.43 fof(f985,plain,(
% 0.12/0.43 ![X0]: (~ssList(app(nil,X0))|~ssList(nil)|segmentP(app(app(nil,nil),X0),nil)|~ssList(nil)|~ssList(X0))),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f625,f453])).
% 0.12/0.43 fof(f986,plain,(
% 0.12/0.43 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(sK48_skl)|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(nil)|~ssList(X0))),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f622,f453])).
% 0.12/0.43 fof(f987,plain,(
% 0.12/0.43 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK47_skl)|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(nil)|~ssList(X0))),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f621,f453])).
% 0.12/0.43 fof(f988,definition,(
% 0.12/0.43 ![X0]: (sQ72_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f991,plain,(
% 0.12/0.43 sQ72_spl|~sQ3_spl|~sQ9_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f983,f988,f487,f536])).
% 0.12/0.43 fof(f992,definition,(
% 0.12/0.43 ![X0]: (sQ73_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f995,plain,(
% 0.12/0.43 sQ73_spl|~sQ3_spl|~sQ5_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f984,f992,f487,f493])).
% 0.12/0.43 fof(f996,definition,(
% 0.12/0.43 ![X0]: (sQ74_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f999,plain,(
% 0.12/0.43 sQ74_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f985,f996,f487])).
% 0.12/0.43 fof(f1000,definition,(
% 0.12/0.43 ![X0]: (sQ75_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1003,plain,(
% 0.12/0.43 sQ75_spl|~sQ9_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f986,f1000,f536,f487])).
% 0.12/0.43 fof(f1004,definition,(
% 0.12/0.43 ![X0]: (sQ76_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1007,plain,(
% 0.12/0.43 sQ76_spl|~sQ5_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f987,f1004,f493,f487])).
% 0.12/0.43 fof(f1028,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssItem(sK51_skl)|memberP(app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl))),sK51_skl)|~ssList(sK2_skl(sK51_skl,sK47_skl))|~ssList(sK3_skl(sK51_skl,sK47_skl))|~sQ8_spl),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f527,f449])).
% 0.12/0.43 fof(f1029,plain,(
% 0.12/0.43 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)))|segmentP(app(app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl))),X0),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)))|~ssList(sK2_skl(sK51_skl,sK47_skl))|~ssList(X0)|~sQ8_spl)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f527,f453])).
% 0.12/0.43 fof(f1030,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)))|rearsegP(app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl))),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)))|~ssList(sK2_skl(sK51_skl,sK47_skl))|~sQ8_spl),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f527,f452])).
% 0.12/0.43 fof(f1031,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssList(sK2_skl(sK51_skl,sK47_skl))|frontsegP(app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl))),sK2_skl(sK51_skl,sK47_skl))|~ssList(cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)))|~sQ8_spl),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f527,f451])).
% 0.12/0.43 fof(f1032,plain,(
% 0.12/0.43 ![X0]: (~ssItem(X0)|~ssList(sK2_skl(sK51_skl,sK47_skl))|~ssList(cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)))|~memberP(sK47_skl,X0)|memberP(sK2_skl(sK51_skl,sK47_skl),X0)|memberP(cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)),X0)|~sQ8_spl)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f527,f270])).
% 0.12/0.43 fof(f1033,definition,(
% 0.12/0.43 sQ77_spl <=> (memberP(app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl))),sK51_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1036,definition,(
% 0.12/0.43 sQ78_spl <=> (ssList(sK2_skl(sK51_skl,sK47_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1037,plain,(
% 0.12/0.43 ssList(sK2_skl(sK51_skl,sK47_skl))|~sQ78_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f1036])).
% 0.12/0.43 fof(f1038,plain,(
% 0.12/0.43 ~ssList(sK2_skl(sK51_skl,sK47_skl))|sQ78_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f1036])).
% 0.12/0.43 fof(f1039,definition,(
% 0.12/0.43 sQ79_spl <=> (ssList(sK3_skl(sK51_skl,sK47_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1042,plain,(
% 0.12/0.43 ~sQ5_spl|~sQ7_spl|sQ77_spl|~sQ78_spl|~sQ79_spl|~sQ8_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1028,f493,f523,f1033,f1036,f1039,f526])).
% 0.12/0.43 fof(f1043,definition,(
% 0.12/0.43 ![X0]: (sQ80_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl))),X0),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)))|~ssList(X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1046,definition,(
% 0.12/0.43 sQ81_spl <=> (ssList(cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl))))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1049,plain,(
% 0.12/0.43 sQ80_spl|~sQ81_spl|~sQ78_spl|~sQ8_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1029,f1043,f1046,f1036,f526])).
% 0.12/0.43 fof(f1050,definition,(
% 0.12/0.43 sQ82_spl <=> (rearsegP(app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl))),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl))))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1053,plain,(
% 0.12/0.43 ~sQ5_spl|~sQ81_spl|sQ82_spl|~sQ78_spl|~sQ8_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1030,f493,f1046,f1050,f1036,f526])).
% 0.12/0.43 fof(f1054,definition,(
% 0.12/0.43 sQ83_spl <=> (frontsegP(app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl))),sK2_skl(sK51_skl,sK47_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1057,plain,(
% 0.12/0.43 ~sQ5_spl|~sQ78_spl|sQ83_spl|~sQ81_spl|~sQ8_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1031,f493,f1036,f1054,f1046,f526])).
% 0.12/0.43 fof(f1058,definition,(
% 0.12/0.43 ![X0]: (sQ84_spl <=> (~ssItem(X0)|~memberP(sK47_skl,X0)|memberP(sK2_skl(sK51_skl,sK47_skl),X0)|memberP(cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)),X0)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1061,plain,(
% 0.12/0.43 sQ84_spl|~sQ78_spl|~sQ81_spl|~sQ8_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1032,f1058,f1036,f1046,f526])).
% 0.12/0.43 fof(f1062,plain,(
% 0.12/0.43 ~ssList(sK47_skl)|~ssItem(sK51_skl)|~memberP(sK47_skl,sK51_skl)|sQ78_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f1038,f109])).
% 0.12/0.43 fof(f1063,definition,(
% 0.12/0.43 sQ85_spl <=> (memberP(sK47_skl,sK51_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1066,plain,(
% 0.12/0.43 ~sQ5_spl|~sQ7_spl|~sQ85_spl|sQ78_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1062,f493,f523,f1063,f1036])).
% 0.12/0.43 fof(f1408,plain,(
% 0.12/0.43 cyclefreeP(sK6_skl(sK47_skl,sK47_skl))|app(app(sK11_skl(sK6_skl(sK47_skl,sK47_skl)),cons(sK9_skl(sK6_skl(sK47_skl,sK47_skl)),sK12_skl(sK6_skl(sK47_skl,sK47_skl)))),cons(sK10_skl(sK6_skl(sK47_skl,sK47_skl)),sK13_skl(sK6_skl(sK47_skl,sK47_skl))))=sK6_skl(sK47_skl,sK47_skl)|~sQ63_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f147,f893])).
% 0.12/0.43 fof(f1409,plain,(
% 0.12/0.43 cyclefreeP(sK6_skl(sK48_skl,sK48_skl))|app(app(sK11_skl(sK6_skl(sK48_skl,sK48_skl)),cons(sK9_skl(sK6_skl(sK48_skl,sK48_skl)),sK12_skl(sK6_skl(sK48_skl,sK48_skl)))),cons(sK10_skl(sK6_skl(sK48_skl,sK48_skl)),sK13_skl(sK6_skl(sK48_skl,sK48_skl))))=sK6_skl(sK48_skl,sK48_skl)|~sQ47_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f147,f823])).
% 0.12/0.43 fof(f1410,plain,(
% 0.12/0.43 cyclefreeP(sK6_skl(nil,nil))|app(app(sK11_skl(sK6_skl(nil,nil)),cons(sK9_skl(sK6_skl(nil,nil)),sK12_skl(sK6_skl(nil,nil)))),cons(sK10_skl(sK6_skl(nil,nil)),sK13_skl(sK6_skl(nil,nil))))=sK6_skl(nil,nil)|~sQ61_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f147,f883])).
% 0.12/0.43 fof(f1411,plain,(
% 0.12/0.43 cyclefreeP(sK6_skl(nil,sK47_skl))|app(app(sK11_skl(sK6_skl(nil,sK47_skl)),cons(sK9_skl(sK6_skl(nil,sK47_skl)),sK12_skl(sK6_skl(nil,sK47_skl)))),cons(sK10_skl(sK6_skl(nil,sK47_skl)),sK13_skl(sK6_skl(nil,sK47_skl))))=sK6_skl(nil,sK47_skl)|~sQ49_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f147,f833])).
% 0.12/0.43 fof(f1412,plain,(
% 0.12/0.43 cyclefreeP(sK6_skl(nil,sK48_skl))|app(app(sK11_skl(sK6_skl(nil,sK48_skl)),cons(sK9_skl(sK6_skl(nil,sK48_skl)),sK12_skl(sK6_skl(nil,sK48_skl)))),cons(sK10_skl(sK6_skl(nil,sK48_skl)),sK13_skl(sK6_skl(nil,sK48_skl))))=sK6_skl(nil,sK48_skl)|~sQ45_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f147,f813])).
% 0.12/0.43 fof(f1419,plain,(
% 0.12/0.43 cyclefreeP(sK2_skl(sK51_skl,sK47_skl))|app(app(sK11_skl(sK2_skl(sK51_skl,sK47_skl)),cons(sK9_skl(sK2_skl(sK51_skl,sK47_skl)),sK12_skl(sK2_skl(sK51_skl,sK47_skl)))),cons(sK10_skl(sK2_skl(sK51_skl,sK47_skl)),sK13_skl(sK2_skl(sK51_skl,sK47_skl))))=sK2_skl(sK51_skl,sK47_skl)|~sQ78_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f147,f1037])).
% 0.12/0.43 fof(f1423,definition,(
% 0.12/0.43 sQ106_spl <=> (cyclefreeP(sK6_skl(sK47_skl,sK47_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1426,definition,(
% 0.12/0.43 sQ107_spl <=> (app(app(sK11_skl(sK6_skl(sK47_skl,sK47_skl)),cons(sK9_skl(sK6_skl(sK47_skl,sK47_skl)),sK12_skl(sK6_skl(sK47_skl,sK47_skl)))),cons(sK10_skl(sK6_skl(sK47_skl,sK47_skl)),sK13_skl(sK6_skl(sK47_skl,sK47_skl))))=sK6_skl(sK47_skl,sK47_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1429,plain,(
% 0.12/0.43 sQ106_spl|sQ107_spl|~sQ63_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1408,f1423,f1426,f892])).
% 0.12/0.43 fof(f1430,definition,(
% 0.12/0.43 sQ108_spl <=> (cyclefreeP(sK6_skl(sK48_skl,sK48_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1433,definition,(
% 0.12/0.43 sQ109_spl <=> (app(app(sK11_skl(sK6_skl(sK48_skl,sK48_skl)),cons(sK9_skl(sK6_skl(sK48_skl,sK48_skl)),sK12_skl(sK6_skl(sK48_skl,sK48_skl)))),cons(sK10_skl(sK6_skl(sK48_skl,sK48_skl)),sK13_skl(sK6_skl(sK48_skl,sK48_skl))))=sK6_skl(sK48_skl,sK48_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1436,plain,(
% 0.12/0.43 sQ108_spl|sQ109_spl|~sQ47_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1409,f1430,f1433,f822])).
% 0.12/0.43 fof(f1437,definition,(
% 0.12/0.43 sQ110_spl <=> (cyclefreeP(sK6_skl(nil,nil)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1440,definition,(
% 0.12/0.43 sQ111_spl <=> (app(app(sK11_skl(sK6_skl(nil,nil)),cons(sK9_skl(sK6_skl(nil,nil)),sK12_skl(sK6_skl(nil,nil)))),cons(sK10_skl(sK6_skl(nil,nil)),sK13_skl(sK6_skl(nil,nil))))=sK6_skl(nil,nil))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1443,plain,(
% 0.12/0.43 sQ110_spl|sQ111_spl|~sQ61_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1410,f1437,f1440,f882])).
% 0.12/0.43 fof(f1444,definition,(
% 0.12/0.43 sQ112_spl <=> (cyclefreeP(sK6_skl(nil,sK47_skl)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1447,definition,(
% 0.12/0.43 sQ113_spl <=> (app(app(sK11_skl(sK6_skl(nil,sK47_skl)),cons(sK9_skl(sK6_skl(nil,sK47_skl)),sK12_skl(sK6_skl(nil,sK47_skl)))),cons(sK10_skl(sK6_skl(nil,sK47_skl)),sK13_skl(sK6_skl(nil,sK47_skl))))=sK6_skl(nil,sK47_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1450,plain,(
% 0.12/0.43 sQ112_spl|sQ113_spl|~sQ49_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1411,f1444,f1447,f832])).
% 0.12/0.43 fof(f1451,definition,(
% 0.12/0.43 sQ114_spl <=> (cyclefreeP(sK6_skl(nil,sK48_skl)))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f1454,definition,(
% 0.12/0.45 sQ115_spl <=> (app(app(sK11_skl(sK6_skl(nil,sK48_skl)),cons(sK9_skl(sK6_skl(nil,sK48_skl)),sK12_skl(sK6_skl(nil,sK48_skl)))),cons(sK10_skl(sK6_skl(nil,sK48_skl)),sK13_skl(sK6_skl(nil,sK48_skl))))=sK6_skl(nil,sK48_skl))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f1457,plain,(
% 0.12/0.45 sQ114_spl|sQ115_spl|~sQ45_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f1412,f1451,f1454,f812])).
% 0.12/0.45 fof(f1469,definition,(
% 0.12/0.45 sQ119_spl <=> (cyclefreeP(sK2_skl(sK51_skl,sK47_skl)))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f1472,definition,(
% 0.12/0.45 sQ120_spl <=> (app(app(sK11_skl(sK2_skl(sK51_skl,sK47_skl)),cons(sK9_skl(sK2_skl(sK51_skl,sK47_skl)),sK12_skl(sK2_skl(sK51_skl,sK47_skl)))),cons(sK10_skl(sK2_skl(sK51_skl,sK47_skl)),sK13_skl(sK2_skl(sK51_skl,sK47_skl))))=sK2_skl(sK51_skl,sK47_skl))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f1475,plain,(
% 0.12/0.45 sQ119_spl|sQ120_spl|~sQ78_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f1419,f1469,f1472,f1036])).
% 0.12/0.45 fof(f1490,plain,(
% 0.12/0.45 ~ssItem(sK51_skl)|sK51_skl=sK52_skl|~sQ36_spl),
% 0.12/0.45 inference(resolution,[status(thm)],[f745,f426])).
% 0.12/0.45 fof(f1491,plain,(
% 0.12/0.45 ~sQ7_spl|sQ53_spl|~sQ36_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f1490,f523,f851,f741])).
% 0.12/0.45 fof(f1506,plain,(
% 0.12/0.45 ~memberP(sK48_skl,sK52_skl)|~sQ53_spl),
% 0.12/0.45 inference(backward_demodulation,[status(thm)],[f852,f427])).
% 0.12/0.45 fof(f1514,plain,(
% 0.12/0.45 $false|~sQ0_spl|~sQ53_spl),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1506,f532])).
% 0.12/0.45 fof(f1515,plain,(
% 0.12/0.45 ~sQ0_spl|~sQ53_spl),
% 0.12/0.45 inference(contradiction_clause,[status(thm)],[f1514])).
% 0.12/0.45 fof(f1516,plain,(
% 0.12/0.45 $false),
% 0.12/0.45 inference(sat_refutation,[status(thm)],[f442,f446,f496,f502,f516,f518,f529,f531,f544,f563,f593,f618,f630,f635,f640,f653,f662,f666,f670,f679,f686,f691,f697,f711,f716,f722,f729,f739,f744,f765,f776,f780,f784,f788,f792,f803,f811,f815,f821,f825,f831,f835,f881,f885,f891,f895,f934,f972,f980,f991,f995,f999,f1003,f1007,f1042,f1049,f1053,f1057,f1061,f1066,f1429,f1436,f1443,f1450,f1457,f1475,f1491,f1515])).
% 0.12/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.45 % Elapsed time: 0.096670 seconds
% 0.12/0.45 % CPU time: 0.396510 seconds
% 0.12/0.45 % Total memory used: 114.745 MB
% 0.12/0.45 % Net memory used: 114.344 MB
%------------------------------------------------------------------------------