%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC392+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 : n005.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:21 PM UTC 2026
% Result : Theorem 0.17s 5.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC392+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.13/5.39 % Computer : n005.cluster.edu
% 0.13/5.39 % Model : x86_64 x86_64
% 0.13/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.39 % Memory : 8046.5625MB
% 0.13/5.39 % OS : Linux 6.8.0-71-generic
% 0.13/5.39 % CPULimit : 300
% 0.13/5.39 % WCLimit : 300
% 0.13/5.39 % DateTime : Mon Sep 21 08:20:53 UTC 2026
% 0.13/5.40 % CPUTime :
% 0.17/5.42 % Drodi V4.1.1
% 0.17/5.56 % Refutation found
% 0.17/5.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/5.56 % SZS output start CNFRefutation for theBenchmark
% 0.17/5.56 fof(f3,axiom,(
% 0.17/5.56 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ( memberP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(W,cons(V,X)) = U ) )) )) ) )) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f4,axiom,(
% 0.17/5.56 (! [U] :( ssList(U)=> ( singletonP(U)<=> (? [V] :( ssItem(V)& cons(V,nil) = U ) )) ) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f5,axiom,(
% 0.17/5.56 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f6,axiom,(
% 0.17/5.56 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( rearsegP(U,V)<=> (? [W] :( ssList(W)& app(W,V) = U ) )) ) )) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f7,axiom,(
% 0.17/5.56 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( segmentP(U,V)<=> (? [W] :( ssList(W)& (? [X] :( ssList(X)& app(app(W,V),X) = U ) )) )) ) )) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f16,axiom,(
% 0.17/5.56 (! [U] :( ssList(U)=> (! [V] :( ssItem(V)=> ssList(cons(V,U)) ) )) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f17,axiom,(
% 0.17/5.56 ssList(nil) ),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f28,axiom,(
% 0.17/5.56 (! [U] :( ssList(U)=> app(nil,U) = U ) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f36,axiom,(
% 0.17/5.56 (! [U] :( ssItem(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> ( memberP(app(V,W),U)<=> ( memberP(V,U)| memberP(W,U) ) ) ) )) )) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f37,axiom,(
% 0.17/5.56 (! [U] :( ssItem(U)=> (! [V] :( ssItem(V)=> (! [W] :( ssList(W)=> ( memberP(cons(V,W),U)<=> ( U = V| memberP(W,U) ) ) ) )) )) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f38,axiom,(
% 0.17/5.56 (! [U] :( ssItem(U)=> ~ memberP(nil,U) ) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f45,axiom,(
% 0.17/5.56 (! [U] :( ssList(U)=> frontsegP(U,nil) ) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f51,axiom,(
% 0.17/5.56 (! [U] :( ssList(U)=> rearsegP(U,nil) ) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f57,axiom,(
% 0.17/5.56 (! [U] :( ssList(U)=> segmentP(U,nil) ) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f84,axiom,(
% 0.17/5.56 (! [U] :( ssList(U)=> app(U,nil) = U ) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f96,conjecture,(
% 0.17/5.56 (! [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)| (? [X1] :( ssItem(X1)& Z != X1& memberP(X,X1)& leq(X1,Z) ) )) ))& ( nil != X| nil != W ) ) ) ) )) )) )) )),
% 0.17/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.56 fof(f97,negated_conjecture,(
% 0.17/5.56 ~((! [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)| (? [X1] :( ssItem(X1)& Z != X1& memberP(X,X1)& leq(X1,Z) ) )) ))& ( nil != X| nil != W ) ) ) ) )) )) )) ))),
% 0.17/5.56 inference(negated_conjecture,[status(cth)],[f96])).
% 0.17/5.56 fof(f106,plain,(
% 0.17/5.56 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|(memberP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(W,cons(V,X))=U))))))))),
% 0.17/5.56 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.17/5.56 fof(f107,plain,(
% 0.17/5.56 ![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.17/5.56 inference(NNF_transformation,[status(thm)],[f106])).
% 0.17/5.56 fof(f108,plain,(
% 0.17/5.56 ![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.17/5.56 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.17/5.57 fof(f111,plain,(
% 0.17/5.57 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|~memberP(X0,X1)|app(sK2_skl(X1,X0),cons(X1,sK3_skl(X1,X0)))=X0)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f108])).
% 0.17/5.57 fof(f113,plain,(
% 0.17/5.57 ![U]: (~ssList(U)|(singletonP(U)<=>(?[V]: (ssItem(V)&cons(V,nil)=U))))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.17/5.57 fof(f114,plain,(
% 0.17/5.57 ![U]: (~ssList(U)|((~singletonP(U)|(?[V]: (ssItem(V)&cons(V,nil)=U)))&(singletonP(U)|(![V]: (~ssItem(V)|~cons(V,nil)=U)))))),
% 0.17/5.57 inference(NNF_transformation,[status(thm)],[f113])).
% 0.17/5.57 fof(f115,plain,(
% 0.17/5.57 ![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.17/5.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(V,sK4_skl(U))],[f114])).
% 0.17/5.57 fof(f118,plain,(
% 0.17/5.57 ![X0,X1]: (~ssList(X0)|singletonP(X0)|~ssItem(X1)|~cons(X1,nil)=X0)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f115])).
% 0.17/5.57 fof(f119,plain,(
% 0.17/5.57 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.17/5.57 fof(f120,plain,(
% 0.17/5.57 ![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.17/5.57 inference(NNF_transformation,[status(thm)],[f119])).
% 0.17/5.57 fof(f121,plain,(
% 0.17/5.57 ![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.17/5.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 0.17/5.57 fof(f123,plain,(
% 0.17/5.57 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(X1,sK5_skl(X1,X0))=X0)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f121])).
% 0.17/5.57 fof(f124,plain,(
% 0.17/5.57 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|frontsegP(X0,X1)|~ssList(X2)|~app(X1,X2)=X0)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f121])).
% 0.17/5.57 fof(f125,plain,(
% 0.17/5.57 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(rearsegP(U,V)<=>(?[W]: (ssList(W)&app(W,V)=U))))))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.17/5.57 fof(f126,plain,(
% 0.17/5.57 ![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.17/5.57 inference(NNF_transformation,[status(thm)],[f125])).
% 0.17/5.57 fof(f127,plain,(
% 0.17/5.57 ![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.17/5.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W,sK6_skl(V,U))],[f126])).
% 0.17/5.57 fof(f128,plain,(
% 0.17/5.57 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|ssList(sK6_skl(X1,X0)))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f127])).
% 0.17/5.57 fof(f129,plain,(
% 0.17/5.57 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|app(sK6_skl(X1,X0),X1)=X0)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f127])).
% 0.17/5.57 fof(f130,plain,(
% 0.17/5.57 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|rearsegP(X0,X1)|~ssList(X2)|~app(X2,X1)=X0)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f127])).
% 0.17/5.57 fof(f131,plain,(
% 0.17/5.57 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(segmentP(U,V)<=>(?[W]: (ssList(W)&(?[X]: (ssList(X)&app(app(W,V),X)=U))))))))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.17/5.57 fof(f132,plain,(
% 0.17/5.57 ![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.17/5.57 inference(NNF_transformation,[status(thm)],[f131])).
% 0.17/5.57 fof(f133,plain,(
% 0.17/5.57 ![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.17/5.57 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.17/5.57 fof(f134,plain,(
% 0.17/5.57 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK7_skl(X1,X0)))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f133])).
% 0.17/5.57 fof(f135,plain,(
% 0.17/5.57 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|ssList(sK8_skl(X1,X0)))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f133])).
% 0.17/5.57 fof(f136,plain,(
% 0.17/5.57 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(X0,X1)|app(app(sK7_skl(X1,X0),X1),sK8_skl(X1,X0))=X0)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f133])).
% 0.17/5.57 fof(f137,plain,(
% 0.17/5.57 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~app(app(X2,X1),X3)=X0)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f133])).
% 0.17/5.57 fof(f221,plain,(
% 0.17/5.57 ![U]: (~ssList(U)|(![V]: (~ssItem(V)|ssList(cons(V,U)))))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.17/5.57 fof(f222,plain,(
% 0.17/5.57 ![X0,X1]: (~ssList(X0)|~ssItem(X1)|ssList(cons(X1,X0)))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f221])).
% 0.17/5.57 fof(f223,plain,(
% 0.17/5.57 ssList(nil)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f17])).
% 0.17/5.57 fof(f248,plain,(
% 0.17/5.57 ![U]: (~ssList(U)|app(nil,U)=U)),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.17/5.57 fof(f249,plain,(
% 0.17/5.57 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f248])).
% 0.17/5.57 fof(f268,plain,(
% 0.17/5.57 ![U]: (~ssItem(U)|(![V]: (~ssList(V)|(![W]: (~ssList(W)|(memberP(app(V,W),U)<=>(memberP(V,U)|memberP(W,U))))))))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.17/5.57 fof(f269,plain,(
% 0.17/5.57 ![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.17/5.57 inference(NNF_transformation,[status(thm)],[f268])).
% 0.17/5.57 fof(f271,plain,(
% 0.17/5.57 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X1,X0))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f269])).
% 0.17/5.57 fof(f272,plain,(
% 0.17/5.57 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|memberP(app(X1,X2),X0)|~memberP(X2,X0))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f269])).
% 0.17/5.57 fof(f273,plain,(
% 0.17/5.57 ![U]: (~ssItem(U)|(![V]: (~ssItem(V)|(![W]: (~ssList(W)|(memberP(cons(V,W),U)<=>(U=V|memberP(W,U))))))))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.17/5.57 fof(f274,plain,(
% 0.17/5.57 ![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.17/5.57 inference(NNF_transformation,[status(thm)],[f273])).
% 0.17/5.57 fof(f275,plain,(
% 0.17/5.57 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~memberP(cons(X1,X2),X0)|X0=X1|memberP(X2,X0))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f274])).
% 0.17/5.57 fof(f277,plain,(
% 0.17/5.57 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|memberP(cons(X1,X2),X0)|~memberP(X2,X0))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f274])).
% 0.17/5.57 fof(f278,plain,(
% 0.17/5.57 ![U]: (~ssItem(U)|~memberP(nil,U))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.17/5.57 fof(f279,plain,(
% 0.17/5.57 ![X0]: (~ssItem(X0)|~memberP(nil,X0))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f278])).
% 0.17/5.57 fof(f294,plain,(
% 0.17/5.57 ![U]: (~ssList(U)|frontsegP(U,nil))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.17/5.57 fof(f295,plain,(
% 0.17/5.57 ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f294])).
% 0.17/5.57 fof(f308,plain,(
% 0.17/5.57 ![U]: (~ssList(U)|rearsegP(U,nil))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.17/5.57 fof(f309,plain,(
% 0.17/5.57 ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f308])).
% 0.17/5.57 fof(f322,plain,(
% 0.17/5.57 ![U]: (~ssList(U)|segmentP(U,nil))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.17/5.57 fof(f323,plain,(
% 0.17/5.57 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f322])).
% 0.17/5.57 fof(f388,plain,(
% 0.17/5.57 ![U]: (~ssList(U)|app(U,nil)=U)),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 0.17/5.57 fof(f389,plain,(
% 0.17/5.57 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f388])).
% 0.17/5.57 fof(f415,plain,(
% 0.17/5.57 (?[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))&(![X1]: (((~ssItem(X1)|Z=X1)|~memberP(X,X1))|~leq(X1,Z))))))|(nil=X&nil=W)))))))))))),
% 0.17/5.57 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.17/5.57 fof(f416,definition,(
% 0.17/5.57 ![W,X,Z]: (sP0_prd(Z,X,W)<=>(ssItem(Z)&((cons(Z,nil)=W&memberP(X,Z))&(![X1]: (((~ssItem(X1)|Z=X1)|~memberP(X,X1))|~leq(X1,Z))))))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.17/5.57 fof(f417,plain,(
% 0.17/5.57 ?[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.17/5.57 inference(formula_renaming,[status(thm)],[f415,f416])).
% 0.17/5.57 fof(f418,plain,(
% 0.17/5.57 (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.17/5.57 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.17/5.57 fof(f419,plain,(
% 0.17/5.57 ssList(sK47_skl)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f418])).
% 0.17/5.57 fof(f420,plain,(
% 0.17/5.57 ssList(sK48_skl)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f418])).
% 0.17/5.57 fof(f423,plain,(
% 0.17/5.57 sK48_skl=sK50_skl),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f418])).
% 0.17/5.57 fof(f424,plain,(
% 0.17/5.57 sK47_skl=sK49_skl),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f418])).
% 0.17/5.57 fof(f425,plain,(
% 0.17/5.57 ssItem(sK51_skl)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f418])).
% 0.17/5.57 fof(f426,plain,(
% 0.17/5.57 memberP(sK47_skl,sK51_skl)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f418])).
% 0.17/5.57 fof(f427,plain,(
% 0.17/5.57 ~memberP(sK48_skl,sK51_skl)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f418])).
% 0.17/5.57 fof(f428,plain,(
% 0.17/5.57 sP0_prd(sK52_skl,sK50_skl,sK49_skl)|nil=sK50_skl),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f418])).
% 0.17/5.57 fof(f429,plain,(
% 0.17/5.57 sP0_prd(sK52_skl,sK50_skl,sK49_skl)|nil=sK49_skl),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f418])).
% 0.17/5.57 fof(f430,plain,(
% 0.17/5.57 ![W,X,Z]: ((~sP0_prd(Z,X,W)|(ssItem(Z)&((cons(Z,nil)=W&memberP(X,Z))&(![X1]: (((~ssItem(X1)|Z=X1)|~memberP(X,X1))|~leq(X1,Z))))))&(sP0_prd(Z,X,W)|(~ssItem(Z)|((~cons(Z,nil)=W|~memberP(X,Z))|(?[X1]: (((ssItem(X1)&~Z=X1)&memberP(X,X1))&leq(X1,Z)))))))),
% 0.17/5.57 inference(NNF_transformation,[status(thm)],[f416])).
% 0.17/5.57 fof(f431,plain,(
% 0.17/5.57 (![W,X,Z]: (~sP0_prd(Z,X,W)|(ssItem(Z)&((cons(Z,nil)=W&memberP(X,Z))&(![X1]: (((~ssItem(X1)|Z=X1)|~memberP(X,X1))|~leq(X1,Z)))))))&(![W,X,Z]: (sP0_prd(Z,X,W)|(~ssItem(Z)|((~cons(Z,nil)=W|~memberP(X,Z))|(?[X1]: (((ssItem(X1)&~Z=X1)&memberP(X,X1))&leq(X1,Z)))))))),
% 0.17/5.57 inference(miniscoping,[status(thm)],[f430])).
% 0.17/5.57 fof(f432,plain,(
% 0.17/5.57 (![W,X,Z]: (~sP0_prd(Z,X,W)|(ssItem(Z)&((cons(Z,nil)=W&memberP(X,Z))&(![X1]: (((~ssItem(X1)|Z=X1)|~memberP(X,X1))|~leq(X1,Z)))))))&(![W,X,Z]: (sP0_prd(Z,X,W)|(~ssItem(Z)|((~cons(Z,nil)=W|~memberP(X,Z))|(((ssItem(sK53_skl(Z,X,W))&~Z=sK53_skl(Z,X,W))&memberP(X,sK53_skl(Z,X,W)))&leq(sK53_skl(Z,X,W),Z))))))),
% 0.17/5.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK53_skl]),skolemize(X1,sK53_skl(Z,X,W))],[f431])).
% 0.17/5.57 fof(f433,plain,(
% 0.17/5.57 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ssItem(X0))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f432])).
% 0.17/5.57 fof(f434,plain,(
% 0.17/5.57 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|cons(X0,nil)=X2)),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f432])).
% 0.17/5.57 fof(f435,plain,(
% 0.17/5.57 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|memberP(X1,X0))),
% 0.17/5.57 inference(cnf_transformation,[status(thm)],[f432])).
% 0.17/5.57 fof(f441,definition,(
% 0.17/5.57 sQ0_spl <=> (sP0_prd(sK52_skl,sK50_skl,sK49_skl))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f442,plain,(
% 0.17/5.57 sP0_prd(sK52_skl,sK50_skl,sK49_skl)|~sQ0_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f441])).
% 0.17/5.57 fof(f444,definition,(
% 0.17/5.57 sQ1_spl <=> (nil=sK50_skl)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f445,plain,(
% 0.17/5.57 nil=sK50_skl|~sQ1_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f444])).
% 0.17/5.57 fof(f447,plain,(
% 0.17/5.57 sQ0_spl|sQ1_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f428,f441,f444])).
% 0.17/5.57 fof(f448,definition,(
% 0.17/5.57 sQ2_spl <=> (nil=sK49_skl)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f449,plain,(
% 0.17/5.57 nil=sK49_skl|~sQ2_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f448])).
% 0.17/5.57 fof(f451,plain,(
% 0.17/5.57 sQ0_spl|sQ2_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f429,f441,f448])).
% 0.17/5.57 fof(f455,plain,(
% 0.17/5.57 ![X0]: (~ssList(cons(X0,nil))|singletonP(cons(X0,nil))|~ssItem(X0))),
% 0.17/5.57 inference(destructive_equality_resolution,[status(thm)],[f118])).
% 0.17/5.57 fof(f456,plain,(
% 0.17/5.57 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X0)|frontsegP(app(X0,X1),X0)|~ssList(X1))),
% 0.17/5.57 inference(destructive_equality_resolution,[status(thm)],[f124])).
% 0.17/5.57 fof(f457,plain,(
% 0.17/5.57 ![X0,X1]: (~ssList(app(X0,X1))|~ssList(X1)|rearsegP(app(X0,X1),X1)|~ssList(X0))),
% 0.17/5.57 inference(destructive_equality_resolution,[status(thm)],[f130])).
% 0.17/5.57 fof(f458,plain,(
% 0.17/5.57 ![X0,X1,X2]: (~ssList(app(app(X0,X1),X2))|~ssList(X1)|segmentP(app(app(X0,X1),X2),X1)|~ssList(X0)|~ssList(X2))),
% 0.17/5.57 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 0.17/5.57 fof(f489,plain,(
% 0.17/5.57 sP0_prd(sK52_skl,sK48_skl,sK49_skl)|~sQ0_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f423,f442])).
% 0.17/5.57 fof(f490,plain,(
% 0.17/5.57 sP0_prd(sK52_skl,sK48_skl,sK47_skl)|~sQ0_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f424,f489])).
% 0.17/5.57 fof(f491,plain,(
% 0.17/5.57 ssItem(sK52_skl)|~sQ0_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f490,f433])).
% 0.17/5.57 fof(f492,plain,(
% 0.17/5.57 cons(sK52_skl,nil)=sK47_skl|~sQ0_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f434,f490])).
% 0.17/5.57 fof(f493,plain,(
% 0.17/5.57 ~ssList(nil)|~ssItem(sK52_skl)|ssList(sK47_skl)|~sQ0_spl),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f492,f222])).
% 0.17/5.57 fof(f495,definition,(
% 0.17/5.57 sQ3_spl <=> (ssList(nil))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f497,plain,(
% 0.17/5.57 ~ssList(nil)|sQ3_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f495])).
% 0.17/5.57 fof(f498,definition,(
% 0.17/5.57 sQ4_spl <=> (ssItem(sK52_skl))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f500,plain,(
% 0.17/5.57 ~ssItem(sK52_skl)|sQ4_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f498])).
% 0.17/5.57 fof(f501,definition,(
% 0.17/5.57 sQ5_spl <=> (ssList(sK47_skl))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f504,plain,(
% 0.17/5.57 ~sQ3_spl|~sQ4_spl|sQ5_spl|~sQ0_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f493,f495,f498,f501,f441])).
% 0.17/5.57 fof(f509,plain,(
% 0.17/5.57 $false|sQ3_spl),
% 0.17/5.57 inference(forward_subsumption_resolution,[status(thm)],[f497,f223])).
% 0.17/5.57 fof(f510,plain,(
% 0.17/5.57 sQ3_spl),
% 0.17/5.57 inference(contradiction_clause,[status(thm)],[f509])).
% 0.17/5.57 fof(f511,plain,(
% 0.17/5.57 sK48_skl=nil|~sQ1_spl),
% 0.17/5.57 inference(backward_demodulation,[status(thm)],[f445,f423])).
% 0.17/5.57 fof(f512,plain,(
% 0.17/5.57 sK47_skl=nil|~sQ2_spl),
% 0.17/5.57 inference(backward_demodulation,[status(thm)],[f449,f424])).
% 0.17/5.57 fof(f519,plain,(
% 0.17/5.57 ~memberP(nil,sK51_skl)|~sQ1_spl),
% 0.17/5.57 inference(backward_demodulation,[status(thm)],[f511,f427])).
% 0.17/5.57 fof(f521,plain,(
% 0.17/5.57 memberP(nil,sK51_skl)|~sQ2_spl),
% 0.17/5.57 inference(backward_demodulation,[status(thm)],[f512,f426])).
% 0.17/5.57 fof(f523,plain,(
% 0.17/5.57 $false|~sQ1_spl|~sQ2_spl),
% 0.17/5.57 inference(forward_subsumption_resolution,[status(thm)],[f521,f519])).
% 0.17/5.57 fof(f524,plain,(
% 0.17/5.57 ~sQ1_spl|~sQ2_spl),
% 0.17/5.57 inference(contradiction_clause,[status(thm)],[f523])).
% 0.17/5.57 fof(f525,plain,(
% 0.17/5.57 $false|sQ4_spl|~sQ0_spl),
% 0.17/5.57 inference(forward_subsumption_resolution,[status(thm)],[f491,f500])).
% 0.17/5.57 fof(f526,plain,(
% 0.17/5.57 sQ4_spl|~sQ0_spl),
% 0.17/5.57 inference(contradiction_clause,[status(thm)],[f525])).
% 0.17/5.57 fof(f530,plain,(
% 0.17/5.57 ~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.17/5.57 inference(resolution,[status(thm)],[f426,f111])).
% 0.17/5.57 fof(f531,definition,(
% 0.17/5.57 sQ7_spl <=> (ssItem(sK51_skl))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f533,plain,(
% 0.17/5.57 ~ssItem(sK51_skl)|sQ7_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f531])).
% 0.17/5.57 fof(f534,definition,(
% 0.17/5.57 sQ8_spl <=> (app(sK2_skl(sK51_skl,sK47_skl),cons(sK51_skl,sK3_skl(sK51_skl,sK47_skl)))=sK47_skl)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f537,plain,(
% 0.17/5.57 ~sQ5_spl|~sQ7_spl|sQ8_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f530,f501,f531,f534])).
% 0.17/5.57 fof(f538,plain,(
% 0.17/5.57 $false|sQ7_spl),
% 0.17/5.57 inference(forward_subsumption_resolution,[status(thm)],[f533,f425])).
% 0.17/5.57 fof(f539,plain,(
% 0.17/5.57 sQ7_spl),
% 0.17/5.57 inference(contradiction_clause,[status(thm)],[f538])).
% 0.17/5.57 fof(f540,plain,(
% 0.17/5.57 memberP(sK48_skl,sK52_skl)|~sQ0_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f490,f435])).
% 0.17/5.57 fof(f544,definition,(
% 0.17/5.57 sQ9_spl <=> (ssList(sK48_skl))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f546,plain,(
% 0.17/5.57 ~ssList(sK48_skl)|sQ9_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f544])).
% 0.17/5.57 fof(f551,plain,(
% 0.17/5.57 $false|sQ9_spl),
% 0.17/5.57 inference(forward_subsumption_resolution,[status(thm)],[f546,f420])).
% 0.17/5.57 fof(f552,plain,(
% 0.17/5.57 sQ9_spl),
% 0.17/5.57 inference(contradiction_clause,[status(thm)],[f551])).
% 0.17/5.57 fof(f566,plain,(
% 0.17/5.57 ![X0]: (singletonP(cons(X0,nil))|~ssItem(X0)|~ssList(nil)|~ssItem(X0))),
% 0.17/5.57 inference(resolution,[status(thm)],[f455,f222])).
% 0.17/5.57 fof(f567,definition,(
% 0.17/5.57 ![X0]: (sQ13_spl <=> (singletonP(cons(X0,nil))|~ssItem(X0)|~ssItem(X0)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f570,plain,(
% 0.17/5.57 sQ13_spl|~sQ3_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f566,f567,f495])).
% 0.17/5.57 fof(f620,plain,(
% 0.17/5.57 app(nil,sK47_skl)=sK47_skl),
% 0.17/5.57 inference(resolution,[status(thm)],[f249,f419])).
% 0.17/5.57 fof(f622,plain,(
% 0.17/5.57 app(nil,sK48_skl)=sK48_skl),
% 0.17/5.57 inference(resolution,[status(thm)],[f249,f420])).
% 0.17/5.57 fof(f625,plain,(
% 0.17/5.57 app(nil,nil)=nil),
% 0.17/5.57 inference(resolution,[status(thm)],[f249,f223])).
% 0.17/5.57 fof(f627,plain,(
% 0.17/5.57 app(sK47_skl,nil)=sK47_skl),
% 0.17/5.57 inference(resolution,[status(thm)],[f389,f419])).
% 0.17/5.57 fof(f629,plain,(
% 0.17/5.57 app(sK48_skl,nil)=sK48_skl),
% 0.17/5.57 inference(resolution,[status(thm)],[f389,f420])).
% 0.17/5.57 fof(f633,plain,(
% 0.17/5.57 ![X0]: (~ssList(X0)|~ssList(nil)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0))),
% 0.17/5.57 inference(resolution,[status(thm)],[f123,f295])).
% 0.17/5.57 fof(f635,definition,(
% 0.17/5.57 ![X0]: (sQ18_spl <=> (~ssList(X0)|app(nil,sK5_skl(nil,X0))=X0|~ssList(X0)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f638,plain,(
% 0.17/5.57 sQ18_spl|~sQ3_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f633,f635,f495])).
% 0.17/5.57 fof(f641,plain,(
% 0.17/5.57 ~ssList(nil)|~ssList(nil)|frontsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f625,f456])).
% 0.17/5.57 fof(f642,plain,(
% 0.17/5.57 ~ssList(sK48_skl)|~ssList(nil)|frontsegP(app(nil,sK48_skl),nil)|~ssList(sK48_skl)),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f622,f456])).
% 0.17/5.57 fof(f643,plain,(
% 0.17/5.57 ~ssList(sK47_skl)|~ssList(nil)|frontsegP(app(nil,sK47_skl),nil)|~ssList(sK47_skl)),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f620,f456])).
% 0.17/5.57 fof(f644,definition,(
% 0.17/5.57 sQ19_spl <=> (frontsegP(app(nil,nil),nil))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f645,plain,(
% 0.17/5.57 frontsegP(app(nil,nil),nil)|~sQ19_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f644])).
% 0.17/5.57 fof(f647,plain,(
% 0.17/5.57 ~sQ3_spl|sQ19_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f641,f495,f644])).
% 0.17/5.57 fof(f648,definition,(
% 0.17/5.57 sQ20_spl <=> (frontsegP(app(nil,sK48_skl),nil))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f649,plain,(
% 0.17/5.57 frontsegP(app(nil,sK48_skl),nil)|~sQ20_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f648])).
% 0.17/5.57 fof(f651,plain,(
% 0.17/5.57 ~sQ9_spl|~sQ3_spl|sQ20_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f642,f544,f495,f648])).
% 0.17/5.57 fof(f652,definition,(
% 0.17/5.57 sQ21_spl <=> (frontsegP(app(nil,sK47_skl),nil))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f653,plain,(
% 0.17/5.57 frontsegP(app(nil,sK47_skl),nil)|~sQ21_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f652])).
% 0.17/5.57 fof(f655,plain,(
% 0.17/5.57 ~sQ5_spl|~sQ3_spl|sQ21_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f643,f501,f495,f652])).
% 0.17/5.57 fof(f656,plain,(
% 0.17/5.57 frontsegP(nil,nil)|~sQ19_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f625,f645])).
% 0.17/5.57 fof(f657,plain,(
% 0.17/5.57 frontsegP(sK48_skl,nil)|~sQ20_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f622,f649])).
% 0.17/5.57 fof(f658,plain,(
% 0.17/5.57 frontsegP(sK47_skl,nil)|~sQ21_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f620,f653])).
% 0.17/5.57 fof(f659,plain,(
% 0.17/5.57 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK6_skl(nil,X0))|~ssList(X0))),
% 0.17/5.57 inference(resolution,[status(thm)],[f128,f309])).
% 0.17/5.57 fof(f661,definition,(
% 0.17/5.57 ![X0]: (sQ22_spl <=> (~ssList(X0)|ssList(sK6_skl(nil,X0))|~ssList(X0)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f664,plain,(
% 0.17/5.57 sQ22_spl|~sQ3_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f659,f661,f495])).
% 0.17/5.57 fof(f667,plain,(
% 0.17/5.57 ~ssList(sK48_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK48_skl))=sK48_skl|~sQ20_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f657,f123])).
% 0.17/5.57 fof(f668,definition,(
% 0.17/5.57 sQ23_spl <=> (app(nil,sK5_skl(nil,sK48_skl))=sK48_skl)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f671,plain,(
% 0.17/5.57 ~sQ9_spl|~sQ3_spl|sQ23_spl|~sQ20_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f667,f544,f495,f668,f648])).
% 0.17/5.57 fof(f672,plain,(
% 0.17/5.57 ~ssList(sK47_skl)|~ssList(nil)|app(nil,sK5_skl(nil,sK47_skl))=sK47_skl|~sQ21_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f658,f123])).
% 0.17/5.57 fof(f673,definition,(
% 0.17/5.57 sQ24_spl <=> (app(nil,sK5_skl(nil,sK47_skl))=sK47_skl)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f676,plain,(
% 0.17/5.57 ~sQ5_spl|~sQ3_spl|sQ24_spl|~sQ21_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f672,f501,f495,f673,f652])).
% 0.17/5.57 fof(f677,plain,(
% 0.17/5.57 ~ssList(sK47_skl)|~ssList(sK47_skl)|frontsegP(app(sK47_skl,nil),sK47_skl)|~ssList(nil)),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f627,f456])).
% 0.17/5.57 fof(f678,definition,(
% 0.17/5.57 sQ25_spl <=> (frontsegP(app(sK47_skl,nil),sK47_skl))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f679,plain,(
% 0.17/5.57 frontsegP(app(sK47_skl,nil),sK47_skl)|~sQ25_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f678])).
% 0.17/5.57 fof(f681,plain,(
% 0.17/5.57 ~sQ5_spl|sQ25_spl|~sQ3_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f677,f501,f678,f495])).
% 0.17/5.57 fof(f682,plain,(
% 0.17/5.57 frontsegP(sK47_skl,sK47_skl)|~sQ25_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f627,f679])).
% 0.17/5.57 fof(f700,plain,(
% 0.17/5.57 ~ssList(nil)|~ssList(nil)|app(nil,sK5_skl(nil,nil))=nil|~sQ19_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f656,f123])).
% 0.17/5.57 fof(f701,definition,(
% 0.17/5.57 sQ30_spl <=> (app(nil,sK5_skl(nil,nil))=nil)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f704,plain,(
% 0.17/5.57 ~sQ3_spl|sQ30_spl|~sQ19_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f700,f495,f701,f644])).
% 0.17/5.57 fof(f705,plain,(
% 0.17/5.57 ~ssList(sK47_skl)|~ssList(sK47_skl)|app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl|~sQ25_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f682,f123])).
% 0.17/5.57 fof(f706,definition,(
% 0.17/5.57 sQ31_spl <=> (app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))=sK47_skl)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f709,plain,(
% 0.17/5.57 ~sQ5_spl|sQ31_spl|~sQ25_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f705,f501,f706,f678])).
% 0.17/5.57 fof(f710,plain,(
% 0.17/5.57 ~ssList(sK48_skl)|~ssList(sK48_skl)|frontsegP(app(sK48_skl,nil),sK48_skl)|~ssList(nil)),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f629,f456])).
% 0.17/5.57 fof(f711,definition,(
% 0.17/5.57 sQ32_spl <=> (frontsegP(app(sK48_skl,nil),sK48_skl))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f712,plain,(
% 0.17/5.57 frontsegP(app(sK48_skl,nil),sK48_skl)|~sQ32_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f711])).
% 0.17/5.57 fof(f714,plain,(
% 0.17/5.57 ~sQ9_spl|sQ32_spl|~sQ3_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f710,f544,f711,f495])).
% 0.17/5.57 fof(f715,plain,(
% 0.17/5.57 frontsegP(sK48_skl,sK48_skl)|~sQ32_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f629,f712])).
% 0.17/5.57 fof(f716,plain,(
% 0.17/5.57 ~ssList(sK48_skl)|~ssList(sK48_skl)|app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))=sK48_skl|~sQ32_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f715,f123])).
% 0.17/5.57 fof(f717,definition,(
% 0.17/5.57 sQ33_spl <=> (app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))=sK48_skl)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f720,plain,(
% 0.17/5.57 ~sQ9_spl|sQ33_spl|~sQ32_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f716,f544,f717,f711])).
% 0.17/5.57 fof(f734,plain,(
% 0.17/5.57 ![X0]: (~ssItem(sK51_skl)|~ssList(sK47_skl)|~ssList(X0)|memberP(app(sK47_skl,X0),sK51_skl))),
% 0.17/5.57 inference(resolution,[status(thm)],[f271,f426])).
% 0.17/5.57 fof(f739,definition,(
% 0.17/5.57 ![X0]: (sQ35_spl <=> (~ssList(X0)|memberP(app(sK47_skl,X0),sK51_skl)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f742,plain,(
% 0.17/5.57 ~sQ7_spl|~sQ5_spl|sQ35_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f734,f531,f501,f739])).
% 0.17/5.57 fof(f757,plain,(
% 0.17/5.57 ![X0]: (~ssList(X0)|~ssList(nil)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0))),
% 0.17/5.57 inference(resolution,[status(thm)],[f129,f309])).
% 0.17/5.57 fof(f759,definition,(
% 0.17/5.57 ![X0]: (sQ36_spl <=> (~ssList(X0)|app(sK6_skl(nil,X0),nil)=X0|~ssList(X0)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f762,plain,(
% 0.17/5.57 sQ36_spl|~sQ3_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f757,f759,f495])).
% 0.17/5.57 fof(f765,plain,(
% 0.17/5.57 ~ssList(sK48_skl)|~ssList(nil)|rearsegP(app(sK48_skl,nil),nil)|~ssList(sK48_skl)),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f629,f457])).
% 0.17/5.57 fof(f766,plain,(
% 0.17/5.57 ~ssList(sK47_skl)|~ssList(nil)|rearsegP(app(sK47_skl,nil),nil)|~ssList(sK47_skl)),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f627,f457])).
% 0.17/5.57 fof(f767,plain,(
% 0.17/5.57 ~ssList(nil)|~ssList(nil)|rearsegP(app(nil,nil),nil)|~ssList(nil)),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f625,f457])).
% 0.17/5.57 fof(f768,plain,(
% 0.17/5.57 ~ssList(sK48_skl)|~ssList(sK48_skl)|rearsegP(app(nil,sK48_skl),sK48_skl)|~ssList(nil)),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f622,f457])).
% 0.17/5.57 fof(f769,plain,(
% 0.17/5.57 ~ssList(sK47_skl)|~ssList(sK47_skl)|rearsegP(app(nil,sK47_skl),sK47_skl)|~ssList(nil)),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f620,f457])).
% 0.17/5.57 fof(f770,definition,(
% 0.17/5.57 sQ37_spl <=> (rearsegP(app(sK48_skl,nil),nil))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f771,plain,(
% 0.17/5.57 rearsegP(app(sK48_skl,nil),nil)|~sQ37_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f770])).
% 0.17/5.57 fof(f773,plain,(
% 0.17/5.57 ~sQ9_spl|~sQ3_spl|sQ37_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f765,f544,f495,f770])).
% 0.17/5.57 fof(f774,definition,(
% 0.17/5.57 sQ38_spl <=> (rearsegP(app(sK47_skl,nil),nil))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f775,plain,(
% 0.17/5.57 rearsegP(app(sK47_skl,nil),nil)|~sQ38_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f774])).
% 0.17/5.57 fof(f777,plain,(
% 0.17/5.57 ~sQ5_spl|~sQ3_spl|sQ38_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f766,f501,f495,f774])).
% 0.17/5.57 fof(f778,definition,(
% 0.17/5.57 sQ39_spl <=> (rearsegP(app(nil,nil),nil))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f779,plain,(
% 0.17/5.57 rearsegP(app(nil,nil),nil)|~sQ39_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f778])).
% 0.17/5.57 fof(f781,plain,(
% 0.17/5.57 ~sQ3_spl|sQ39_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f767,f495,f778])).
% 0.17/5.57 fof(f782,definition,(
% 0.17/5.57 sQ40_spl <=> (rearsegP(app(nil,sK48_skl),sK48_skl))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f783,plain,(
% 0.17/5.57 rearsegP(app(nil,sK48_skl),sK48_skl)|~sQ40_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f782])).
% 0.17/5.57 fof(f785,plain,(
% 0.17/5.57 ~sQ9_spl|sQ40_spl|~sQ3_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f768,f544,f782,f495])).
% 0.17/5.57 fof(f786,definition,(
% 0.17/5.57 sQ41_spl <=> (rearsegP(app(nil,sK47_skl),sK47_skl))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f787,plain,(
% 0.17/5.57 rearsegP(app(nil,sK47_skl),sK47_skl)|~sQ41_spl),
% 0.17/5.57 inference(component_clause,[status(thm)],[f786])).
% 0.17/5.57 fof(f789,plain,(
% 0.17/5.57 ~sQ5_spl|sQ41_spl|~sQ3_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f769,f501,f786,f495])).
% 0.17/5.57 fof(f790,plain,(
% 0.17/5.57 rearsegP(sK48_skl,nil)|~sQ37_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f629,f771])).
% 0.17/5.57 fof(f791,plain,(
% 0.17/5.57 rearsegP(nil,nil)|~sQ39_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f625,f779])).
% 0.17/5.57 fof(f792,plain,(
% 0.17/5.57 rearsegP(sK48_skl,sK48_skl)|~sQ40_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f622,f783])).
% 0.17/5.57 fof(f793,plain,(
% 0.17/5.57 rearsegP(sK47_skl,nil)|~sQ38_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f627,f775])).
% 0.17/5.57 fof(f794,plain,(
% 0.17/5.57 rearsegP(sK47_skl,sK47_skl)|~sQ41_spl),
% 0.17/5.57 inference(forward_demodulation,[status(thm)],[f620,f787])).
% 0.17/5.57 fof(f795,plain,(
% 0.17/5.57 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK7_skl(nil,X0))|~ssList(X0))),
% 0.17/5.57 inference(resolution,[status(thm)],[f134,f323])).
% 0.17/5.57 fof(f797,definition,(
% 0.17/5.57 ![X0]: (sQ42_spl <=> (~ssList(X0)|ssList(sK7_skl(nil,X0))|~ssList(X0)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f800,plain,(
% 0.17/5.57 sQ42_spl|~sQ3_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f795,f797,f495])).
% 0.17/5.57 fof(f803,plain,(
% 0.17/5.57 ~ssList(sK48_skl)|~ssList(nil)|app(sK6_skl(nil,sK48_skl),nil)=sK48_skl|~sQ37_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f790,f129])).
% 0.17/5.57 fof(f804,plain,(
% 0.17/5.57 ~ssList(sK48_skl)|~ssList(nil)|ssList(sK6_skl(nil,sK48_skl))|~sQ37_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f790,f128])).
% 0.17/5.57 fof(f805,definition,(
% 0.17/5.57 sQ43_spl <=> (app(sK6_skl(nil,sK48_skl),nil)=sK48_skl)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f808,plain,(
% 0.17/5.57 ~sQ9_spl|~sQ3_spl|sQ43_spl|~sQ37_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f803,f544,f495,f805,f770])).
% 0.17/5.57 fof(f809,definition,(
% 0.17/5.57 sQ44_spl <=> (ssList(sK6_skl(nil,sK48_skl)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f812,plain,(
% 0.17/5.57 ~sQ9_spl|~sQ3_spl|sQ44_spl|~sQ37_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f804,f544,f495,f809,f770])).
% 0.17/5.57 fof(f813,plain,(
% 0.17/5.57 ~ssList(sK48_skl)|~ssList(sK48_skl)|app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)=sK48_skl|~sQ40_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f792,f129])).
% 0.17/5.57 fof(f814,plain,(
% 0.17/5.57 ~ssList(sK48_skl)|~ssList(sK48_skl)|ssList(sK6_skl(sK48_skl,sK48_skl))|~sQ40_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f792,f128])).
% 0.17/5.57 fof(f815,definition,(
% 0.17/5.57 sQ45_spl <=> (app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)=sK48_skl)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f818,plain,(
% 0.17/5.57 ~sQ9_spl|sQ45_spl|~sQ40_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f813,f544,f815,f782])).
% 0.17/5.57 fof(f819,definition,(
% 0.17/5.57 sQ46_spl <=> (ssList(sK6_skl(sK48_skl,sK48_skl)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f822,plain,(
% 0.17/5.57 ~sQ9_spl|sQ46_spl|~sQ40_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f814,f544,f819,f782])).
% 0.17/5.57 fof(f823,plain,(
% 0.17/5.57 ~ssList(sK47_skl)|~ssList(nil)|app(sK6_skl(nil,sK47_skl),nil)=sK47_skl|~sQ38_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f793,f129])).
% 0.17/5.57 fof(f824,plain,(
% 0.17/5.57 ~ssList(sK47_skl)|~ssList(nil)|ssList(sK6_skl(nil,sK47_skl))|~sQ38_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f793,f128])).
% 0.17/5.57 fof(f825,definition,(
% 0.17/5.57 sQ47_spl <=> (app(sK6_skl(nil,sK47_skl),nil)=sK47_skl)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f828,plain,(
% 0.17/5.57 ~sQ5_spl|~sQ3_spl|sQ47_spl|~sQ38_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f823,f501,f495,f825,f774])).
% 0.17/5.57 fof(f829,definition,(
% 0.17/5.57 sQ48_spl <=> (ssList(sK6_skl(nil,sK47_skl)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f832,plain,(
% 0.17/5.57 ~sQ5_spl|~sQ3_spl|sQ48_spl|~sQ38_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f824,f501,f495,f829,f774])).
% 0.17/5.57 fof(f843,plain,(
% 0.17/5.57 ~ssList(nil)|~ssList(nil)|app(sK6_skl(nil,nil),nil)=nil|~sQ39_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f791,f129])).
% 0.17/5.57 fof(f844,plain,(
% 0.17/5.57 ~ssList(nil)|~ssList(nil)|ssList(sK6_skl(nil,nil))|~sQ39_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f791,f128])).
% 0.17/5.57 fof(f845,definition,(
% 0.17/5.57 sQ51_spl <=> (app(sK6_skl(nil,nil),nil)=nil)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f848,plain,(
% 0.17/5.57 ~sQ3_spl|sQ51_spl|~sQ39_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f843,f495,f845,f778])).
% 0.17/5.57 fof(f849,definition,(
% 0.17/5.57 sQ52_spl <=> (ssList(sK6_skl(nil,nil)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f852,plain,(
% 0.17/5.57 ~sQ3_spl|sQ52_spl|~sQ39_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f844,f495,f849,f778])).
% 0.17/5.57 fof(f853,plain,(
% 0.17/5.57 ~ssList(sK47_skl)|~ssList(sK47_skl)|app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)=sK47_skl|~sQ41_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f794,f129])).
% 0.17/5.57 fof(f854,plain,(
% 0.17/5.57 ~ssList(sK47_skl)|~ssList(sK47_skl)|ssList(sK6_skl(sK47_skl,sK47_skl))|~sQ41_spl),
% 0.17/5.57 inference(resolution,[status(thm)],[f794,f128])).
% 0.17/5.57 fof(f855,definition,(
% 0.17/5.57 sQ53_spl <=> (app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)=sK47_skl)),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f858,plain,(
% 0.17/5.57 ~sQ5_spl|sQ53_spl|~sQ41_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f853,f501,f855,f786])).
% 0.17/5.57 fof(f859,definition,(
% 0.17/5.57 sQ54_spl <=> (ssList(sK6_skl(sK47_skl,sK47_skl)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f862,plain,(
% 0.17/5.57 ~sQ5_spl|sQ54_spl|~sQ41_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f854,f501,f859,f786])).
% 0.17/5.57 fof(f888,plain,(
% 0.17/5.57 ![X0]: (~ssItem(sK51_skl)|~ssList(X0)|~ssList(sK47_skl)|memberP(app(X0,sK47_skl),sK51_skl))),
% 0.17/5.57 inference(resolution,[status(thm)],[f272,f426])).
% 0.17/5.57 fof(f893,definition,(
% 0.17/5.57 ![X0]: (sQ56_spl <=> (~ssList(X0)|memberP(app(X0,sK47_skl),sK51_skl)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f896,plain,(
% 0.17/5.57 ~sQ7_spl|sQ56_spl|~sQ5_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f888,f531,f893,f501])).
% 0.17/5.57 fof(f897,plain,(
% 0.17/5.57 ![X0]: (~ssItem(X0)|~ssItem(sK52_skl)|~ssList(nil)|~memberP(sK47_skl,X0)|X0=sK52_skl|memberP(nil,X0)|~sQ0_spl)),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f492,f275])).
% 0.17/5.57 fof(f898,definition,(
% 0.17/5.57 ![X0]: (sQ57_spl <=> (~ssItem(X0)|~memberP(sK47_skl,X0)|X0=sK52_skl|memberP(nil,X0)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f899,plain,(
% 0.17/5.57 ![X0]: (~ssItem(X0)|~memberP(sK47_skl,X0)|X0=sK52_skl|memberP(nil,X0)|~sQ57_spl)),
% 0.17/5.57 inference(component_clause,[status(thm)],[f898])).
% 0.17/5.57 fof(f901,plain,(
% 0.17/5.57 sQ57_spl|~sQ4_spl|~sQ3_spl|~sQ0_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f897,f898,f498,f495,f441])).
% 0.17/5.57 fof(f902,plain,(
% 0.17/5.57 ![X0]: (~ssItem(X0)|~memberP(sK47_skl,X0)|X0=sK52_skl|~sQ57_spl)),
% 0.17/5.57 inference(forward_subsumption_resolution,[status(thm)],[f899,f279])).
% 0.17/5.57 fof(f930,plain,(
% 0.17/5.57 ![X0]: (~ssList(X0)|~ssList(nil)|ssList(sK8_skl(nil,X0))|~ssList(X0))),
% 0.17/5.57 inference(resolution,[status(thm)],[f135,f323])).
% 0.17/5.57 fof(f932,definition,(
% 0.17/5.57 ![X0]: (sQ61_spl <=> (~ssList(X0)|ssList(sK8_skl(nil,X0))|~ssList(X0)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f935,plain,(
% 0.17/5.57 sQ61_spl|~sQ3_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f930,f932,f495])).
% 0.17/5.57 fof(f938,plain,(
% 0.17/5.57 ![X0]: (~ssList(X0)|~ssList(nil)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0))),
% 0.17/5.57 inference(resolution,[status(thm)],[f136,f323])).
% 0.17/5.57 fof(f940,definition,(
% 0.17/5.57 ![X0]: (sQ62_spl <=> (~ssList(X0)|app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0))=X0|~ssList(X0)))),
% 0.17/5.57 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.17/5.57 fof(f943,plain,(
% 0.17/5.57 sQ62_spl|~sQ3_spl),
% 0.17/5.57 inference(split_clause,[status(thm)],[f938,f940,f495])).
% 0.17/5.57 fof(f946,plain,(
% 0.17/5.57 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(nil)|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(sK48_skl)|~ssList(X0))),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f629,f458])).
% 0.17/5.57 fof(f947,plain,(
% 0.17/5.57 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(nil)|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(sK47_skl)|~ssList(X0))),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f627,f458])).
% 0.17/5.57 fof(f948,plain,(
% 0.17/5.57 ![X0]: (~ssList(app(nil,X0))|~ssList(nil)|segmentP(app(app(nil,nil),X0),nil)|~ssList(nil)|~ssList(X0))),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f625,f458])).
% 0.17/5.57 fof(f949,plain,(
% 0.17/5.57 ![X0]: (~ssList(app(sK48_skl,X0))|~ssList(sK48_skl)|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(nil)|~ssList(X0))),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f622,f458])).
% 0.17/5.57 fof(f950,plain,(
% 0.17/5.57 ![X0]: (~ssList(app(sK47_skl,X0))|~ssList(sK47_skl)|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(nil)|~ssList(X0))),
% 0.17/5.57 inference(paramodulation,[status(thm)],[f620,f458])).
% 0.17/5.57 fof(f951,definition,(
% 0.17/5.57 ![X0]: (sQ63_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(sK48_skl,nil),X0),nil)|~ssList(X0)))),
% 0.17/5.58 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.17/5.58 fof(f954,plain,(
% 0.17/5.58 sQ63_spl|~sQ3_spl|~sQ9_spl),
% 0.17/5.58 inference(split_clause,[status(thm)],[f946,f951,f495,f544])).
% 0.17/5.58 fof(f955,definition,(
% 0.17/5.58 ![X0]: (sQ64_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(sK47_skl,nil),X0),nil)|~ssList(X0)))),
% 0.17/5.58 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.17/5.58 fof(f958,plain,(
% 0.17/5.58 sQ64_spl|~sQ3_spl|~sQ5_spl),
% 0.17/5.58 inference(split_clause,[status(thm)],[f947,f955,f495,f501])).
% 0.17/5.58 fof(f959,definition,(
% 0.17/5.58 ![X0]: (sQ65_spl <=> (~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)|~ssList(X0)))),
% 0.17/5.58 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.17/5.58 fof(f962,plain,(
% 0.17/5.58 sQ65_spl|~sQ3_spl),
% 0.17/5.58 inference(split_clause,[status(thm)],[f948,f959,f495])).
% 0.17/5.58 fof(f963,definition,(
% 0.17/5.58 ![X0]: (sQ66_spl <=> (~ssList(app(sK48_skl,X0))|segmentP(app(app(nil,sK48_skl),X0),sK48_skl)|~ssList(X0)))),
% 0.17/5.58 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.17/5.58 fof(f966,plain,(
% 0.17/5.58 sQ66_spl|~sQ9_spl|~sQ3_spl),
% 0.17/5.58 inference(split_clause,[status(thm)],[f949,f963,f544,f495])).
% 0.17/5.58 fof(f967,definition,(
% 0.17/5.58 ![X0]: (sQ67_spl <=> (~ssList(app(sK47_skl,X0))|segmentP(app(app(nil,sK47_skl),X0),sK47_skl)|~ssList(X0)))),
% 0.17/5.58 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.17/5.58 fof(f970,plain,(
% 0.17/5.58 sQ67_spl|~sQ5_spl|~sQ3_spl),
% 0.17/5.58 inference(split_clause,[status(thm)],[f950,f967,f501,f495])).
% 0.17/5.58 fof(f1035,plain,(
% 0.17/5.58 ![X0]: (~ssItem(sK51_skl)|~ssItem(X0)|~ssList(sK47_skl)|memberP(cons(X0,sK47_skl),sK51_skl))),
% 0.17/5.58 inference(resolution,[status(thm)],[f277,f426])).
% 0.17/5.58 fof(f1040,definition,(
% 0.17/5.58 ![X0]: (sQ71_spl <=> (~ssItem(X0)|memberP(cons(X0,sK47_skl),sK51_skl)))),
% 0.17/5.58 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.17/5.58 fof(f1043,plain,(
% 0.17/5.58 ~sQ7_spl|sQ71_spl|~sQ5_spl),
% 0.17/5.58 inference(split_clause,[status(thm)],[f1035,f531,f1040,f501])).
% 0.17/5.58 fof(f1168,plain,(
% 0.17/5.58 ~ssItem(sK51_skl)|sK51_skl=sK52_skl|~sQ57_spl),
% 0.17/5.58 inference(resolution,[status(thm)],[f902,f426])).
% 0.17/5.58 fof(f1169,definition,(
% 0.17/5.58 sQ81_spl <=> (sK51_skl=sK52_skl)),
% 0.17/5.58 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.17/5.58 fof(f1170,plain,(
% 0.17/5.58 sK51_skl=sK52_skl|~sQ81_spl),
% 0.17/5.58 inference(component_clause,[status(thm)],[f1169])).
% 0.17/5.58 fof(f1172,plain,(
% 0.17/5.58 ~sQ7_spl|sQ81_spl|~sQ57_spl),
% 0.17/5.58 inference(split_clause,[status(thm)],[f1168,f531,f1169,f898])).
% 0.17/5.58 fof(f1259,plain,(
% 0.17/5.58 ~memberP(sK48_skl,sK52_skl)|~sQ81_spl),
% 0.17/5.58 inference(backward_demodulation,[status(thm)],[f1170,f427])).
% 0.17/5.58 fof(f1262,plain,(
% 0.17/5.58 $false|~sQ0_spl|~sQ81_spl),
% 0.17/5.58 inference(forward_subsumption_resolution,[status(thm)],[f1259,f540])).
% 0.17/5.58 fof(f1263,plain,(
% 0.17/5.58 ~sQ0_spl|~sQ81_spl),
% 0.17/5.58 inference(contradiction_clause,[status(thm)],[f1262])).
% 0.17/5.58 fof(f1264,plain,(
% 0.17/5.58 $false),
% 0.17/5.58 inference(sat_refutation,[status(thm)],[f447,f451,f504,f510,f524,f526,f537,f539,f552,f570,f638,f647,f651,f655,f664,f671,f676,f681,f704,f709,f714,f720,f742,f762,f773,f777,f781,f785,f789,f800,f808,f812,f818,f822,f828,f832,f848,f852,f858,f862,f896,f901,f935,f943,f954,f958,f962,f966,f970,f1043,f1172,f1263])).
% 0.17/5.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/5.60 % Elapsed time: 0.190564 seconds
% 0.17/5.60 % CPU time: 0.936656 seconds
% 0.17/5.60 % Total memory used: 120.316 MB
% 0.17/5.60 % Net memory used: 119.664 MB
%------------------------------------------------------------------------------