%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC387+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:20 PM UTC 2026
% Result : Theorem 0.15s 5.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC387+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n020.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Mon Sep 21 08:21:38 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.15/5.41 % Drodi V4.1.1
% 0.15/5.46 % Refutation found
% 0.15/5.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/5.46 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.46 fof(f4,axiom,(
% 0.15/5.46 (! [U] :( ssList(U)=> ( singletonP(U)<=> (? [V] :( ssItem(V)& cons(V,nil) = U ) )) ) )),
% 0.15/5.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.46 fof(f5,axiom,(
% 0.15/5.46 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( frontsegP(U,V)<=> (? [W] :( ssList(W)& app(V,W) = U ) )) ) )) )),
% 0.15/5.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.46 fof(f6,axiom,(
% 0.15/5.46 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( rearsegP(U,V)<=> (? [W] :( ssList(W)& app(W,V) = U ) )) ) )) )),
% 0.15/5.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.46 fof(f15,axiom,(
% 0.15/5.46 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> ( neq(U,V)<=> U != V ) ) )) )),
% 0.15/5.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.46 fof(f17,axiom,(
% 0.15/5.46 ssList(nil) ),
% 0.15/5.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.46 fof(f19,axiom,(
% 0.15/5.46 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssItem(W)=> (! [X] :( ssItem(X)=> ( cons(W,U) = cons(X,V)=> ( W = X& V = U ) ) ) )) )) )) )),
% 0.15/5.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.46 fof(f42,axiom,(
% 0.15/5.46 (! [U] :( ssList(U)=> frontsegP(U,U) ) )),
% 0.15/5.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.46 fof(f49,axiom,(
% 0.15/5.46 (! [U] :( ssList(U)=> rearsegP(U,U) ) )),
% 0.15/5.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.46 fof(f96,conjecture,(
% 0.15/5.46 (! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (? [Y] :( ssItem(Y)& cons(Y,nil) = U& memberP(V,Y) ))| ( nil != W& nil = X )| ( nil = V& nil = U )| ( (! [Z] :( ssItem(Z)=> ( cons(Z,nil) != W| ~ memberP(X,Z) ) ))& neq(X,nil) ) ) ) )) )) )) )),
% 0.15/5.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.46 fof(f97,negated_conjecture,(
% 0.15/5.46 ~((! [U] :( ssList(U)=> (! [V] :( ssList(V)=> (! [W] :( ssList(W)=> (! [X] :( ssList(X)=> ( V != X| U != W| (? [Y] :( ssItem(Y)& cons(Y,nil) = U& memberP(V,Y) ))| ( nil != W& nil = X )| ( nil = V& nil = U )| ( (! [Z] :( ssItem(Z)=> ( cons(Z,nil) != W| ~ memberP(X,Z) ) ))& neq(X,nil) ) ) ) )) )) )) ))),
% 0.15/5.46 inference(negated_conjecture,[status(cth)],[f96])).
% 0.15/5.46 fof(f113,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|(singletonP(U)<=>(?[V]: (ssItem(V)&cons(V,nil)=U))))),
% 0.15/5.46 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.15/5.46 fof(f114,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|((~singletonP(U)|(?[V]: (ssItem(V)&cons(V,nil)=U)))&(singletonP(U)|(![V]: (~ssItem(V)|~cons(V,nil)=U)))))),
% 0.15/5.46 inference(NNF_transformation,[status(thm)],[f113])).
% 0.15/5.46 fof(f115,plain,(
% 0.15/5.46 ![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.15/5.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(V,sK4_skl(U))],[f114])).
% 0.15/5.46 fof(f116,plain,(
% 0.15/5.46 ![X0]: (~ssList(X0)|~singletonP(X0)|ssItem(sK4_skl(X0)))),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f115])).
% 0.15/5.46 fof(f119,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(frontsegP(U,V)<=>(?[W]: (ssList(W)&app(V,W)=U))))))),
% 0.15/5.46 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.15/5.46 fof(f120,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~frontsegP(U,V)|(?[W]: (ssList(W)&app(V,W)=U)))&(frontsegP(U,V)|(![W]: (~ssList(W)|~app(V,W)=U)))))))),
% 0.15/5.46 inference(NNF_transformation,[status(thm)],[f119])).
% 0.15/5.46 fof(f121,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~frontsegP(U,V)|(ssList(sK5_skl(V,U))&app(V,sK5_skl(V,U))=U))&(frontsegP(U,V)|(![W]: (~ssList(W)|~app(V,W)=U)))))))),
% 0.15/5.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120])).
% 0.15/5.46 fof(f122,plain,(
% 0.15/5.46 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|ssList(sK5_skl(X1,X0)))),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f121])).
% 0.15/5.46 fof(f123,plain,(
% 0.15/5.46 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~frontsegP(X0,X1)|app(X1,sK5_skl(X1,X0))=X0)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f121])).
% 0.15/5.46 fof(f125,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(rearsegP(U,V)<=>(?[W]: (ssList(W)&app(W,V)=U))))))),
% 0.15/5.46 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.15/5.46 fof(f126,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~rearsegP(U,V)|(?[W]: (ssList(W)&app(W,V)=U)))&(rearsegP(U,V)|(![W]: (~ssList(W)|~app(W,V)=U)))))))),
% 0.15/5.46 inference(NNF_transformation,[status(thm)],[f125])).
% 0.15/5.46 fof(f127,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~rearsegP(U,V)|(ssList(sK6_skl(V,U))&app(sK6_skl(V,U),V)=U))&(rearsegP(U,V)|(![W]: (~ssList(W)|~app(W,V)=U)))))))),
% 0.15/5.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W,sK6_skl(V,U))],[f126])).
% 0.15/5.46 fof(f128,plain,(
% 0.15/5.46 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|ssList(sK6_skl(X1,X0)))),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f127])).
% 0.15/5.46 fof(f129,plain,(
% 0.15/5.46 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X0,X1)|app(sK6_skl(X1,X0),X1)=X0)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f127])).
% 0.15/5.46 fof(f217,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(neq(U,V)<=>~U=V))))),
% 0.15/5.46 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.15/5.46 fof(f218,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|(![V]: (~ssList(V)|((~neq(U,V)|~U=V)&(neq(U,V)|U=V)))))),
% 0.15/5.46 inference(NNF_transformation,[status(thm)],[f217])).
% 0.15/5.46 fof(f219,plain,(
% 0.15/5.46 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~neq(X0,X1)|~X0=X1)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f218])).
% 0.15/5.46 fof(f220,plain,(
% 0.15/5.46 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X0,X1)|X0=X1)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f218])).
% 0.15/5.46 fof(f223,plain,(
% 0.15/5.46 ssList(nil)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f17])).
% 0.15/5.46 fof(f226,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|(![V]: (~ssList(V)|(![W]: (~ssItem(W)|(![X]: (~ssItem(X)|(~cons(W,U)=cons(X,V)|(W=X&V=U)))))))))),
% 0.15/5.46 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.15/5.46 fof(f227,plain,(
% 0.15/5.46 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssItem(X2)|~ssItem(X3)|~cons(X2,X0)=cons(X3,X1)|X2=X3)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f226])).
% 0.15/5.46 fof(f228,plain,(
% 0.15/5.46 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssItem(X2)|~ssItem(X3)|~cons(X2,X0)=cons(X3,X1)|X1=X0)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f226])).
% 0.15/5.46 fof(f285,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|frontsegP(U,U))),
% 0.15/5.46 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.15/5.46 fof(f286,plain,(
% 0.15/5.46 ![X0]: (~ssList(X0)|frontsegP(X0,X0))),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f285])).
% 0.15/5.46 fof(f304,plain,(
% 0.15/5.46 ![U]: (~ssList(U)|rearsegP(U,U))),
% 0.15/5.46 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.15/5.46 fof(f305,plain,(
% 0.15/5.46 ![X0]: (~ssList(X0)|rearsegP(X0,X0))),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f304])).
% 0.15/5.46 fof(f415,plain,(
% 0.15/5.46 (?[U]: (ssList(U)&(?[V]: (ssList(V)&(?[W]: (ssList(W)&(?[X]: (ssList(X)&(((((V=X&U=W)&(![Y]: ((~ssItem(Y)|~cons(Y,nil)=U)|~memberP(V,Y))))&(nil=W|~nil=X))&(~nil=V|~nil=U))&((?[Z]: (ssItem(Z)&(cons(Z,nil)=W&memberP(X,Z))))|~neq(X,nil)))))))))))),
% 0.15/5.46 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 0.15/5.46 fof(f416,plain,(
% 0.15/5.46 (ssList(sK47_skl)&(ssList(sK48_skl)&(ssList(sK49_skl)&(ssList(sK50_skl)&(((((sK48_skl=sK50_skl&sK47_skl=sK49_skl)&(![Y]: ((~ssItem(Y)|~cons(Y,nil)=sK47_skl)|~memberP(sK48_skl,Y))))&(nil=sK49_skl|~nil=sK50_skl))&(~nil=sK48_skl|~nil=sK47_skl))&((ssItem(sK51_skl)&(cons(sK51_skl,nil)=sK49_skl&memberP(sK50_skl,sK51_skl)))|~neq(sK50_skl,nil)))))))),
% 0.15/5.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Z,sK51_skl)],[f415])).
% 0.15/5.46 fof(f419,plain,(
% 0.15/5.46 ssList(sK49_skl)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/5.46 fof(f420,plain,(
% 0.15/5.46 ssList(sK50_skl)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/5.46 fof(f421,plain,(
% 0.15/5.46 sK48_skl=sK50_skl),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/5.46 fof(f422,plain,(
% 0.15/5.46 sK47_skl=sK49_skl),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/5.46 fof(f423,plain,(
% 0.15/5.46 ![X0]: (~ssItem(X0)|~cons(X0,nil)=sK47_skl|~memberP(sK48_skl,X0))),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/5.46 fof(f424,plain,(
% 0.15/5.46 nil=sK49_skl|~nil=sK50_skl),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/5.46 fof(f425,plain,(
% 0.15/5.46 ~nil=sK48_skl|~nil=sK47_skl),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/5.46 fof(f426,plain,(
% 0.15/5.46 ssItem(sK51_skl)|~neq(sK50_skl,nil)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/5.46 fof(f427,plain,(
% 0.15/5.46 cons(sK51_skl,nil)=sK49_skl|~neq(sK50_skl,nil)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/5.46 fof(f428,plain,(
% 0.15/5.46 memberP(sK50_skl,sK51_skl)|~neq(sK50_skl,nil)),
% 0.15/5.46 inference(cnf_transformation,[status(thm)],[f416])).
% 0.15/5.46 fof(f429,definition,(
% 0.15/5.46 sQ0_spl <=> (nil=sK49_skl)),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f430,plain,(
% 0.15/5.46 nil=sK49_skl|~sQ0_spl),
% 0.15/5.46 inference(component_clause,[status(thm)],[f429])).
% 0.15/5.46 fof(f432,definition,(
% 0.15/5.46 sQ1_spl <=> (nil=sK50_skl)),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f435,plain,(
% 0.15/5.46 sQ0_spl|~sQ1_spl),
% 0.15/5.46 inference(split_clause,[status(thm)],[f424,f429,f432])).
% 0.15/5.46 fof(f436,definition,(
% 0.15/5.46 sQ2_spl <=> (nil=sK48_skl)),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f438,plain,(
% 0.15/5.46 ~nil=sK48_skl|sQ2_spl),
% 0.15/5.46 inference(component_clause,[status(thm)],[f436])).
% 0.15/5.46 fof(f439,definition,(
% 0.15/5.46 sQ3_spl <=> (nil=sK47_skl)),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f441,plain,(
% 0.15/5.46 ~nil=sK47_skl|sQ3_spl),
% 0.15/5.46 inference(component_clause,[status(thm)],[f439])).
% 0.15/5.46 fof(f442,plain,(
% 0.15/5.46 ~sQ2_spl|~sQ3_spl),
% 0.15/5.46 inference(split_clause,[status(thm)],[f425,f436,f439])).
% 0.15/5.46 fof(f443,definition,(
% 0.15/5.46 sQ4_spl <=> (ssItem(sK51_skl))),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f446,definition,(
% 0.15/5.46 sQ5_spl <=> (neq(sK50_skl,nil))),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f448,plain,(
% 0.15/5.46 ~neq(sK50_skl,nil)|sQ5_spl),
% 0.15/5.46 inference(component_clause,[status(thm)],[f446])).
% 0.15/5.46 fof(f449,plain,(
% 0.15/5.46 sQ4_spl|~sQ5_spl),
% 0.15/5.46 inference(split_clause,[status(thm)],[f426,f443,f446])).
% 0.15/5.46 fof(f450,definition,(
% 0.15/5.46 sQ6_spl <=> (cons(sK51_skl,nil)=sK49_skl)),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f451,plain,(
% 0.15/5.46 cons(sK51_skl,nil)=sK49_skl|~sQ6_spl),
% 0.15/5.46 inference(component_clause,[status(thm)],[f450])).
% 0.15/5.46 fof(f453,plain,(
% 0.15/5.46 sQ6_spl|~sQ5_spl),
% 0.15/5.46 inference(split_clause,[status(thm)],[f427,f450,f446])).
% 0.15/5.46 fof(f454,definition,(
% 0.15/5.46 sQ7_spl <=> (memberP(sK50_skl,sK51_skl))),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f457,plain,(
% 0.15/5.46 sQ7_spl|~sQ5_spl),
% 0.15/5.46 inference(split_clause,[status(thm)],[f428,f454,f446])).
% 0.15/5.46 fof(f473,plain,(
% 0.15/5.46 ![X1]: (~ssList(X1)|~ssList(X1)|~neq(X1,X1))),
% 0.15/5.46 inference(destructive_equality_resolution,[status(thm)],[f219])).
% 0.15/5.46 fof(f474,plain,(
% 0.15/5.46 ![X0]: (~ssList(X0)|~neq(X0,X0))),
% 0.15/5.46 inference(duplicate_literals_removal,[status(thm)],[f473])).
% 0.15/5.46 fof(f490,plain,(
% 0.15/5.46 ~nil=sK50_skl|sQ2_spl),
% 0.15/5.46 inference(forward_demodulation,[status(thm)],[f421,f438])).
% 0.15/5.46 fof(f491,plain,(
% 0.15/5.46 ~sK49_skl=sK50_skl|~sQ0_spl|sQ2_spl),
% 0.15/5.46 inference(backward_demodulation,[status(thm)],[f430,f490])).
% 0.15/5.46 fof(f493,plain,(
% 0.15/5.46 ~neq(sK50_skl,sK49_skl)|~sQ0_spl|sQ5_spl),
% 0.15/5.46 inference(forward_demodulation,[status(thm)],[f430,f448])).
% 0.15/5.46 fof(f495,plain,(
% 0.15/5.46 ![X0]: (~ssList(X0)|neq(sK50_skl,X0)|sK50_skl=X0)),
% 0.15/5.46 inference(resolution,[status(thm)],[f220,f420])).
% 0.15/5.46 fof(f509,plain,(
% 0.15/5.46 frontsegP(sK50_skl,sK50_skl)),
% 0.15/5.46 inference(resolution,[status(thm)],[f286,f420])).
% 0.15/5.46 fof(f510,plain,(
% 0.15/5.46 frontsegP(sK49_skl,sK49_skl)),
% 0.15/5.46 inference(resolution,[status(thm)],[f286,f419])).
% 0.15/5.46 fof(f511,plain,(
% 0.15/5.46 neq(sK50_skl,sK50_skl)|sK50_skl=sK50_skl),
% 0.15/5.46 inference(resolution,[status(thm)],[f495,f420])).
% 0.15/5.46 fof(f512,plain,(
% 0.15/5.46 neq(sK50_skl,sK49_skl)|sK50_skl=sK49_skl),
% 0.15/5.46 inference(resolution,[status(thm)],[f495,f419])).
% 0.15/5.46 fof(f513,definition,(
% 0.15/5.46 sQ8_spl <=> (neq(sK50_skl,sK50_skl))),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f514,plain,(
% 0.15/5.46 neq(sK50_skl,sK50_skl)|~sQ8_spl),
% 0.15/5.46 inference(component_clause,[status(thm)],[f513])).
% 0.15/5.46 fof(f516,definition,(
% 0.15/5.46 sQ9_spl <=> (sK50_skl=sK50_skl)),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f519,plain,(
% 0.15/5.46 sQ8_spl|sQ9_spl),
% 0.15/5.46 inference(split_clause,[status(thm)],[f511,f513,f516])).
% 0.15/5.46 fof(f520,definition,(
% 0.15/5.46 sQ10_spl <=> (neq(sK50_skl,sK49_skl))),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f521,plain,(
% 0.15/5.46 neq(sK50_skl,sK49_skl)|~sQ10_spl),
% 0.15/5.46 inference(component_clause,[status(thm)],[f520])).
% 0.15/5.46 fof(f523,definition,(
% 0.15/5.46 sQ11_spl <=> (sK50_skl=sK49_skl)),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f524,plain,(
% 0.15/5.46 sK50_skl=sK49_skl|~sQ11_spl),
% 0.15/5.46 inference(component_clause,[status(thm)],[f523])).
% 0.15/5.46 fof(f526,plain,(
% 0.15/5.46 sQ10_spl|sQ11_spl),
% 0.15/5.46 inference(split_clause,[status(thm)],[f512,f520,f523])).
% 0.15/5.46 fof(f527,plain,(
% 0.15/5.46 $false|~sQ0_spl|sQ5_spl|~sQ10_spl),
% 0.15/5.46 inference(forward_subsumption_resolution,[status(thm)],[f521,f493])).
% 0.15/5.46 fof(f528,plain,(
% 0.15/5.46 ~sQ0_spl|sQ5_spl|~sQ10_spl),
% 0.15/5.46 inference(contradiction_clause,[status(thm)],[f527])).
% 0.15/5.46 fof(f533,plain,(
% 0.15/5.46 ![X0]: (~ssItem(X0)|~cons(X0,nil)=sK47_skl|~memberP(sK50_skl,X0))),
% 0.15/5.46 inference(forward_demodulation,[status(thm)],[f421,f423])).
% 0.15/5.46 fof(f534,plain,(
% 0.15/5.46 neq(sK50_skl,nil)|sK50_skl=nil),
% 0.15/5.46 inference(resolution,[status(thm)],[f223,f495])).
% 0.15/5.46 fof(f535,plain,(
% 0.15/5.46 frontsegP(nil,nil)),
% 0.15/5.46 inference(resolution,[status(thm)],[f223,f286])).
% 0.15/5.46 fof(f537,plain,(
% 0.15/5.46 sQ5_spl|sQ1_spl),
% 0.15/5.46 inference(split_clause,[status(thm)],[f534,f446,f432])).
% 0.15/5.46 fof(f540,plain,(
% 0.15/5.46 ~sK50_skl=sK50_skl|~sQ11_spl|~sQ0_spl|sQ2_spl),
% 0.15/5.46 inference(forward_demodulation,[status(thm)],[f524,f491])).
% 0.15/5.46 fof(f541,plain,(
% 0.15/5.46 $false|~sQ11_spl|~sQ0_spl|sQ2_spl),
% 0.15/5.46 inference(trivial_equality_resolution,[status(thm)],[f540])).
% 0.15/5.46 fof(f542,plain,(
% 0.15/5.46 ~sQ11_spl|~sQ0_spl|sQ2_spl),
% 0.15/5.46 inference(contradiction_clause,[status(thm)],[f541])).
% 0.15/5.46 fof(f547,plain,(
% 0.15/5.46 ![X0,X1]: (~ssList(X0)|~ssList(X0)|~ssItem(X1)|~ssItem(X1)|X1=X1)),
% 0.15/5.46 inference(equality_resolution,[status(thm)],[f227])).
% 0.15/5.46 fof(f548,definition,(
% 0.15/5.46 ![X0]: (sQ12_spl <=> (~ssList(X0)|~ssList(X0)))),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f549,plain,(
% 0.15/5.46 ![X0]: (~ssList(X0)|~ssList(X0)|~sQ12_spl)),
% 0.15/5.46 inference(component_clause,[status(thm)],[f548])).
% 0.15/5.46 fof(f551,definition,(
% 0.15/5.46 ![X1]: (sQ13_spl <=> (~ssItem(X1)|~ssItem(X1)|X1=X1))),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f554,plain,(
% 0.15/5.46 sQ12_spl|sQ13_spl),
% 0.15/5.46 inference(split_clause,[status(thm)],[f547,f548,f551])).
% 0.15/5.46 fof(f555,plain,(
% 0.15/5.46 ![X0]: (~ssList(X0)|~sQ12_spl)),
% 0.15/5.46 inference(duplicate_literals_removal,[status(thm)],[f549])).
% 0.15/5.46 fof(f556,plain,(
% 0.15/5.46 $false|~sQ12_spl),
% 0.15/5.46 inference(backward_subsumption_resolution,[status(thm)],[f223,f555])).
% 0.15/5.46 fof(f558,plain,(
% 0.15/5.46 ~sQ12_spl),
% 0.15/5.46 inference(contradiction_clause,[status(thm)],[f556])).
% 0.15/5.46 fof(f559,plain,(
% 0.15/5.46 ~sK49_skl=sK47_skl|~sQ0_spl|sQ3_spl),
% 0.15/5.46 inference(backward_demodulation,[status(thm)],[f430,f441])).
% 0.15/5.46 fof(f598,plain,(
% 0.15/5.46 ~sK49_skl=sK49_skl|~sQ0_spl|sQ3_spl),
% 0.15/5.46 inference(forward_demodulation,[status(thm)],[f422,f559])).
% 0.15/5.46 fof(f599,plain,(
% 0.15/5.46 $false|~sQ0_spl|sQ3_spl),
% 0.15/5.46 inference(trivial_equality_resolution,[status(thm)],[f598])).
% 0.15/5.46 fof(f600,plain,(
% 0.15/5.46 ~sQ0_spl|sQ3_spl),
% 0.15/5.46 inference(contradiction_clause,[status(thm)],[f599])).
% 0.15/5.46 fof(f601,plain,(
% 0.15/5.46 ![X0]: (~ssItem(X0)|~cons(X0,nil)=sK49_skl|~memberP(sK50_skl,X0))),
% 0.15/5.46 inference(forward_demodulation,[status(thm)],[f422,f533])).
% 0.15/5.46 fof(f602,plain,(
% 0.15/5.46 ~singletonP(nil)|ssItem(sK4_skl(nil))),
% 0.15/5.46 inference(resolution,[status(thm)],[f223,f116])).
% 0.15/5.46 fof(f603,definition,(
% 0.15/5.46 sQ20_spl <=> (singletonP(nil))),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f606,definition,(
% 0.15/5.46 sQ21_spl <=> (ssItem(sK4_skl(nil)))),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f609,plain,(
% 0.15/5.46 ~sQ20_spl|sQ21_spl),
% 0.15/5.46 inference(split_clause,[status(thm)],[f602,f603,f606])).
% 0.15/5.46 fof(f612,plain,(
% 0.15/5.46 ![X0,X1]: (~ssList(X0)|~ssList(X0)|~ssItem(X1)|~ssItem(X1)|X0=X0)),
% 0.15/5.46 inference(equality_resolution,[status(thm)],[f228])).
% 0.15/5.46 fof(f613,definition,(
% 0.15/5.46 ![X0]: (sQ22_spl <=> (~ssList(X0)|~ssList(X0)|X0=X0))),
% 0.15/5.46 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.15/5.46 fof(f616,definition,(
% 0.15/5.46 ![X1]: (sQ23_spl <=> (~ssItem(X1)|~ssItem(X1)))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f619,plain,(
% 0.15/5.47 sQ22_spl|sQ23_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f612,f613,f616])).
% 0.15/5.47 fof(f632,plain,(
% 0.15/5.47 ~ssList(sK50_skl)|~ssList(sK50_skl)|ssList(sK5_skl(sK50_skl,sK50_skl))),
% 0.15/5.47 inference(resolution,[status(thm)],[f122,f509])).
% 0.15/5.47 fof(f633,definition,(
% 0.15/5.47 sQ24_spl <=> (ssList(sK50_skl))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f635,plain,(
% 0.15/5.47 ~ssList(sK50_skl)|sQ24_spl),
% 0.15/5.47 inference(component_clause,[status(thm)],[f633])).
% 0.15/5.47 fof(f636,definition,(
% 0.15/5.47 sQ25_spl <=> (ssList(sK5_skl(sK50_skl,sK50_skl)))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f637,plain,(
% 0.15/5.47 ssList(sK5_skl(sK50_skl,sK50_skl))|~sQ25_spl),
% 0.15/5.47 inference(component_clause,[status(thm)],[f636])).
% 0.15/5.47 fof(f639,plain,(
% 0.15/5.47 ~sQ24_spl|sQ25_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f632,f633,f636])).
% 0.15/5.47 fof(f640,plain,(
% 0.15/5.47 $false|sQ24_spl),
% 0.15/5.47 inference(forward_subsumption_resolution,[status(thm)],[f635,f420])).
% 0.15/5.47 fof(f641,plain,(
% 0.15/5.47 sQ24_spl),
% 0.15/5.47 inference(contradiction_clause,[status(thm)],[f640])).
% 0.15/5.47 fof(f642,plain,(
% 0.15/5.47 ~ssList(sK50_skl)|~ssList(sK50_skl)|app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))=sK50_skl),
% 0.15/5.47 inference(resolution,[status(thm)],[f123,f509])).
% 0.15/5.47 fof(f643,definition,(
% 0.15/5.47 sQ26_spl <=> (app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))=sK50_skl)),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f646,plain,(
% 0.15/5.47 ~sQ24_spl|sQ26_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f642,f633,f643])).
% 0.15/5.47 fof(f648,plain,(
% 0.15/5.47 ~ssList(sK49_skl)|~ssList(sK49_skl)|app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))=sK49_skl),
% 0.15/5.47 inference(resolution,[status(thm)],[f510,f123])).
% 0.15/5.47 fof(f649,plain,(
% 0.15/5.47 ~ssList(sK49_skl)|~ssList(sK49_skl)|ssList(sK5_skl(sK49_skl,sK49_skl))),
% 0.15/5.47 inference(resolution,[status(thm)],[f510,f122])).
% 0.15/5.47 fof(f650,definition,(
% 0.15/5.47 sQ27_spl <=> (ssList(sK49_skl))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f652,plain,(
% 0.15/5.47 ~ssList(sK49_skl)|sQ27_spl),
% 0.15/5.47 inference(component_clause,[status(thm)],[f650])).
% 0.15/5.47 fof(f653,definition,(
% 0.15/5.47 sQ28_spl <=> (app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))=sK49_skl)),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f656,plain,(
% 0.15/5.47 ~sQ27_spl|sQ28_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f648,f650,f653])).
% 0.15/5.47 fof(f657,definition,(
% 0.15/5.47 sQ29_spl <=> (ssList(sK5_skl(sK49_skl,sK49_skl)))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f658,plain,(
% 0.15/5.47 ssList(sK5_skl(sK49_skl,sK49_skl))|~sQ29_spl),
% 0.15/5.47 inference(component_clause,[status(thm)],[f657])).
% 0.15/5.47 fof(f660,plain,(
% 0.15/5.47 ~sQ27_spl|sQ29_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f649,f650,f657])).
% 0.15/5.47 fof(f661,plain,(
% 0.15/5.47 $false|sQ27_spl),
% 0.15/5.47 inference(forward_subsumption_resolution,[status(thm)],[f652,f419])).
% 0.15/5.47 fof(f662,plain,(
% 0.15/5.47 sQ27_spl),
% 0.15/5.47 inference(contradiction_clause,[status(thm)],[f661])).
% 0.15/5.47 fof(f681,plain,(
% 0.15/5.47 ~ssList(nil)|~ssList(nil)|app(nil,sK5_skl(nil,nil))=nil),
% 0.15/5.47 inference(resolution,[status(thm)],[f535,f123])).
% 0.15/5.47 fof(f682,plain,(
% 0.15/5.47 ~ssList(nil)|~ssList(nil)|ssList(sK5_skl(nil,nil))),
% 0.15/5.47 inference(resolution,[status(thm)],[f535,f122])).
% 0.15/5.47 fof(f683,definition,(
% 0.15/5.47 sQ32_spl <=> (ssList(nil))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f685,plain,(
% 0.15/5.47 ~ssList(nil)|sQ32_spl),
% 0.15/5.47 inference(component_clause,[status(thm)],[f683])).
% 0.15/5.47 fof(f686,definition,(
% 0.15/5.47 sQ33_spl <=> (app(nil,sK5_skl(nil,nil))=nil)),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f689,plain,(
% 0.15/5.47 ~sQ32_spl|sQ33_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f681,f683,f686])).
% 0.15/5.47 fof(f690,definition,(
% 0.15/5.47 sQ34_spl <=> (ssList(sK5_skl(nil,nil)))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f693,plain,(
% 0.15/5.47 ~sQ32_spl|sQ34_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f682,f683,f690])).
% 0.15/5.47 fof(f694,plain,(
% 0.15/5.47 $false|sQ32_spl),
% 0.15/5.47 inference(forward_subsumption_resolution,[status(thm)],[f685,f223])).
% 0.15/5.47 fof(f695,plain,(
% 0.15/5.47 sQ32_spl),
% 0.15/5.47 inference(contradiction_clause,[status(thm)],[f694])).
% 0.15/5.47 fof(f696,plain,(
% 0.15/5.47 ~ssList(sK50_skl)|~sQ8_spl),
% 0.15/5.47 inference(resolution,[status(thm)],[f474,f514])).
% 0.15/5.47 fof(f697,plain,(
% 0.15/5.47 ~sQ24_spl|~sQ8_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f696,f633,f513])).
% 0.15/5.47 fof(f701,plain,(
% 0.15/5.47 rearsegP(nil,nil)),
% 0.15/5.47 inference(resolution,[status(thm)],[f305,f223])).
% 0.15/5.47 fof(f702,plain,(
% 0.15/5.47 rearsegP(sK50_skl,sK50_skl)),
% 0.15/5.47 inference(resolution,[status(thm)],[f305,f420])).
% 0.15/5.47 fof(f703,plain,(
% 0.15/5.47 rearsegP(sK49_skl,sK49_skl)),
% 0.15/5.47 inference(resolution,[status(thm)],[f305,f419])).
% 0.15/5.47 fof(f707,plain,(
% 0.15/5.47 ~ssList(sK49_skl)|~ssList(sK49_skl)|ssList(sK6_skl(sK49_skl,sK49_skl))),
% 0.15/5.47 inference(resolution,[status(thm)],[f128,f703])).
% 0.15/5.47 fof(f708,plain,(
% 0.15/5.47 ~ssList(sK50_skl)|~ssList(sK50_skl)|ssList(sK6_skl(sK50_skl,sK50_skl))),
% 0.15/5.47 inference(resolution,[status(thm)],[f128,f702])).
% 0.15/5.47 fof(f709,plain,(
% 0.15/5.47 ~ssList(nil)|~ssList(nil)|ssList(sK6_skl(nil,nil))),
% 0.15/5.47 inference(resolution,[status(thm)],[f128,f701])).
% 0.15/5.47 fof(f710,definition,(
% 0.15/5.47 sQ35_spl <=> (ssList(sK6_skl(sK49_skl,sK49_skl)))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f711,plain,(
% 0.15/5.47 ssList(sK6_skl(sK49_skl,sK49_skl))|~sQ35_spl),
% 0.15/5.47 inference(component_clause,[status(thm)],[f710])).
% 0.15/5.47 fof(f713,plain,(
% 0.15/5.47 ~sQ27_spl|sQ35_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f707,f650,f710])).
% 0.15/5.47 fof(f714,definition,(
% 0.15/5.47 sQ36_spl <=> (ssList(sK6_skl(sK50_skl,sK50_skl)))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f715,plain,(
% 0.15/5.47 ssList(sK6_skl(sK50_skl,sK50_skl))|~sQ36_spl),
% 0.15/5.47 inference(component_clause,[status(thm)],[f714])).
% 0.15/5.47 fof(f717,plain,(
% 0.15/5.47 ~sQ24_spl|sQ36_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f708,f633,f714])).
% 0.15/5.47 fof(f718,definition,(
% 0.15/5.47 sQ37_spl <=> (ssList(sK6_skl(nil,nil)))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f721,plain,(
% 0.15/5.47 ~sQ32_spl|sQ37_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f709,f683,f718])).
% 0.15/5.47 fof(f722,plain,(
% 0.15/5.47 ~ssList(sK49_skl)|~ssList(sK49_skl)|app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)=sK49_skl),
% 0.15/5.47 inference(resolution,[status(thm)],[f129,f703])).
% 0.15/5.47 fof(f723,plain,(
% 0.15/5.47 ~ssList(sK50_skl)|~ssList(sK50_skl)|app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)=sK50_skl),
% 0.15/5.47 inference(resolution,[status(thm)],[f129,f702])).
% 0.15/5.47 fof(f724,plain,(
% 0.15/5.47 ~ssList(nil)|~ssList(nil)|app(sK6_skl(nil,nil),nil)=nil),
% 0.15/5.47 inference(resolution,[status(thm)],[f129,f701])).
% 0.15/5.47 fof(f725,definition,(
% 0.15/5.47 sQ38_spl <=> (app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)=sK49_skl)),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f728,plain,(
% 0.15/5.47 ~sQ27_spl|sQ38_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f722,f650,f725])).
% 0.15/5.47 fof(f729,definition,(
% 0.15/5.47 sQ39_spl <=> (app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)=sK50_skl)),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f732,plain,(
% 0.15/5.47 ~sQ24_spl|sQ39_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f723,f633,f729])).
% 0.15/5.47 fof(f733,definition,(
% 0.15/5.47 sQ40_spl <=> (app(sK6_skl(nil,nil),nil)=nil)),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f736,plain,(
% 0.15/5.47 ~sQ32_spl|sQ40_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f724,f683,f733])).
% 0.15/5.47 fof(f740,plain,(
% 0.15/5.47 ~singletonP(sK5_skl(sK50_skl,sK50_skl))|ssItem(sK4_skl(sK5_skl(sK50_skl,sK50_skl)))|~sQ25_spl),
% 0.15/5.47 inference(resolution,[status(thm)],[f637,f116])).
% 0.15/5.47 fof(f741,definition,(
% 0.15/5.47 sQ41_spl <=> (singletonP(sK5_skl(sK50_skl,sK50_skl)))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f744,definition,(
% 0.15/5.47 sQ42_spl <=> (ssItem(sK4_skl(sK5_skl(sK50_skl,sK50_skl))))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f747,plain,(
% 0.15/5.47 ~sQ41_spl|sQ42_spl|~sQ25_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f740,f741,f744,f636])).
% 0.15/5.47 fof(f751,plain,(
% 0.15/5.47 ~singletonP(sK5_skl(sK49_skl,sK49_skl))|ssItem(sK4_skl(sK5_skl(sK49_skl,sK49_skl)))|~sQ29_spl),
% 0.15/5.47 inference(resolution,[status(thm)],[f658,f116])).
% 0.15/5.47 fof(f752,definition,(
% 0.15/5.47 sQ43_spl <=> (singletonP(sK5_skl(sK49_skl,sK49_skl)))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f755,definition,(
% 0.15/5.47 sQ44_spl <=> (ssItem(sK4_skl(sK5_skl(sK49_skl,sK49_skl))))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f758,plain,(
% 0.15/5.47 ~sQ43_spl|sQ44_spl|~sQ29_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f751,f752,f755,f657])).
% 0.15/5.47 fof(f769,plain,(
% 0.15/5.47 ~singletonP(sK6_skl(sK50_skl,sK50_skl))|ssItem(sK4_skl(sK6_skl(sK50_skl,sK50_skl)))|~sQ36_spl),
% 0.15/5.47 inference(resolution,[status(thm)],[f715,f116])).
% 0.15/5.47 fof(f770,definition,(
% 0.15/5.47 sQ46_spl <=> (singletonP(sK6_skl(sK50_skl,sK50_skl)))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f773,definition,(
% 0.15/5.47 sQ47_spl <=> (ssItem(sK4_skl(sK6_skl(sK50_skl,sK50_skl))))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f776,plain,(
% 0.15/5.47 ~sQ46_spl|sQ47_spl|~sQ36_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f769,f770,f773,f714])).
% 0.15/5.47 fof(f780,plain,(
% 0.15/5.47 ~singletonP(sK6_skl(sK49_skl,sK49_skl))|ssItem(sK4_skl(sK6_skl(sK49_skl,sK49_skl)))|~sQ35_spl),
% 0.15/5.47 inference(resolution,[status(thm)],[f711,f116])).
% 0.15/5.47 fof(f781,definition,(
% 0.15/5.47 sQ48_spl <=> (singletonP(sK6_skl(sK49_skl,sK49_skl)))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f784,definition,(
% 0.15/5.47 sQ49_spl <=> (ssItem(sK4_skl(sK6_skl(sK49_skl,sK49_skl))))),
% 0.15/5.47 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.15/5.47 fof(f787,plain,(
% 0.15/5.47 ~sQ48_spl|sQ49_spl|~sQ35_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f780,f781,f784,f710])).
% 0.15/5.47 fof(f788,plain,(
% 0.15/5.47 ~ssItem(sK51_skl)|~memberP(sK50_skl,sK51_skl)|~sQ6_spl),
% 0.15/5.47 inference(resolution,[status(thm)],[f601,f451])).
% 0.15/5.47 fof(f790,plain,(
% 0.15/5.47 ~sQ4_spl|~sQ7_spl|~sQ6_spl),
% 0.15/5.47 inference(split_clause,[status(thm)],[f788,f443,f454,f450])).
% 0.15/5.47 fof(f792,plain,(
% 0.15/5.47 $false),
% 0.15/5.47 inference(sat_refutation,[status(thm)],[f435,f442,f449,f453,f457,f519,f526,f528,f537,f542,f554,f558,f600,f609,f619,f639,f641,f646,f656,f660,f662,f689,f693,f695,f697,f713,f717,f721,f728,f732,f736,f747,f758,f776,f787,f790])).
% 0.15/5.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.55 % Elapsed time: 0.158262 seconds
% 0.15/5.55 % CPU time: 0.235082 seconds
% 0.15/5.55 % Total memory used: 28.404 MB
% 0.15/5.55 % Net memory used: 28.323 MB
%------------------------------------------------------------------------------