%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC112-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:41:37 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC112-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.09/0.53 % Computer : n020.cluster.edu
% 0.09/0.53 % Model : x86_64 x86_64
% 0.09/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.53 % Memory : 8046.5625MB
% 0.09/0.53 % OS : Linux 6.8.0-71-generic
% 0.09/0.53 % CPULimit : 300
% 0.09/0.53 % WCLimit : 300
% 0.09/0.53 % DateTime : Mon Sep 21 07:57:20 UTC 2026
% 0.09/0.53 % CPUTime :
% 0.09/0.55 % Drodi V4.1.1
% 0.14/0.71 % Refutation found
% 0.14/0.71 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.71 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.71 fof(f8,axiom,(
% 0.14/0.71 ssList(nil) ),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f57,axiom,(
% 0.14/0.71 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f58,axiom,(
% 0.14/0.71 (![U]: (( ~ ssList(U)| rearsegP(U,nil) ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f59,axiom,(
% 0.14/0.71 (![U]: (( ~ ssList(U)| rearsegP(U,U) ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f60,axiom,(
% 0.14/0.71 (![U]: (( ~ ssList(U)| frontsegP(U,nil) ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f73,axiom,(
% 0.14/0.71 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f74,axiom,(
% 0.14/0.71 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f79,axiom,(
% 0.14/0.71 (![U]: (( nil != U| ~ ssList(U)| segmentP(nil,U) ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f80,axiom,(
% 0.14/0.71 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f82,axiom,(
% 0.14/0.71 (![U]: (( ~ rearsegP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f85,axiom,(
% 0.14/0.71 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f100,axiom,(
% 0.14/0.71 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f104,axiom,(
% 0.14/0.71 (![U]: (( ~ ssList(U)| cons(hd(U),tl(U)) = U| nil = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f109,axiom,(
% 0.14/0.71 (![U]: (( ~ ssList(U)| cons(skaf83(U),skaf82(U)) = U| nil = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f115,axiom,(
% 0.14/0.71 (![U,V]: (( U != V| ~ neq(U,V)| ~ ssList(V)| ~ ssList(U) ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f118,axiom,(
% 0.14/0.71 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f119,axiom,(
% 0.14/0.71 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = V ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f127,axiom,(
% 0.14/0.71 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f128,axiom,(
% 0.14/0.71 (![U,V]: (( ~ rearsegP(U,V)| ~ rearsegP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f129,axiom,(
% 0.14/0.71 (![U,V]: (( ~ frontsegP(U,V)| ~ frontsegP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f131,axiom,(
% 0.14/0.71 (![U,V]: (( ~ rearsegP(U,V)| ~ ssList(V)| ~ ssList(U)| app(skaf46(U,V),V) = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f132,axiom,(
% 0.14/0.71 (![U,V]: (( ~ frontsegP(U,V)| ~ ssList(V)| ~ ssList(U)| app(V,skaf45(U,V)) = U ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f145,axiom,(
% 0.14/0.71 (![U,V]: (( nil != U| nil != V| ~ ssList(V)| ~ ssList(U)| app(U,V) = nil ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f150,axiom,(
% 0.14/0.71 (![U,V,W]: (( app(U,V) != app(U,W)| ~ ssList(V)| ~ ssList(U)| ~ ssList(W)| V = W ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f151,axiom,(
% 0.14/0.71 (![U,V,W]: (( app(U,V) != app(W,V)| ~ ssList(U)| ~ ssList(V)| ~ ssList(W)| U = W ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f152,axiom,(
% 0.14/0.71 (![U,V,W]: (( ~ segmentP(U,V)| ~ segmentP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| segmentP(U,W) ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f172,axiom,(
% 0.14/0.71 (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f173,axiom,(
% 0.14/0.71 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f188,negated_conjecture,(
% 0.14/0.71 ssList(sk3) ),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f189,negated_conjecture,(
% 0.14/0.71 ssList(sk4) ),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f190,negated_conjecture,(
% 0.14/0.71 sk2 = sk4 ),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f191,negated_conjecture,(
% 0.14/0.71 sk1 = sk3 ),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f192,negated_conjecture,(
% 0.14/0.71 ssList(sk5) ),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f193,negated_conjecture,(
% 0.14/0.71 ssList(sk6) ),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f194,negated_conjecture,(
% 0.14/0.71 app(app(sk5,sk3),sk6) = sk4 ),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f198,negated_conjecture,(
% 0.14/0.71 ( nil = sk4| nil != sk3 ) ),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f200,negated_conjecture,(
% 0.14/0.71 ( nil = sk2| ~ neq(sk1,nil)| ~ segmentP(sk2,sk1) ) ),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f201,negated_conjecture,(
% 0.14/0.71 ( nil != sk1| neq(sk2,nil) ) ),
% 0.14/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.71 fof(f210,plain,(
% 0.14/0.71 ssList(nil)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.71 fof(f259,plain,(
% 0.14/0.71 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f57])).
% 0.14/0.71 fof(f260,plain,(
% 0.14/0.71 ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f58])).
% 0.14/0.71 fof(f261,plain,(
% 0.14/0.71 ![X0]: (~ssList(X0)|rearsegP(X0,X0))),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f59])).
% 0.14/0.71 fof(f262,plain,(
% 0.14/0.71 ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f60])).
% 0.14/0.71 fof(f276,plain,(
% 0.14/0.71 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/0.71 fof(f277,plain,(
% 0.14/0.71 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f74])).
% 0.14/0.71 fof(f282,plain,(
% 0.14/0.71 ![X0]: (~nil=X0|~ssList(X0)|segmentP(nil,X0))),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f79])).
% 0.14/0.71 fof(f283,plain,(
% 0.14/0.71 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f80])).
% 0.14/0.71 fof(f285,plain,(
% 0.14/0.71 ![X0]: (~rearsegP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f82])).
% 0.14/0.71 fof(f288,plain,(
% 0.14/0.71 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f85])).
% 0.14/0.71 fof(f305,plain,(
% 0.14/0.71 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f100])).
% 0.14/0.71 fof(f309,plain,(
% 0.14/0.71 ![X0]: (~ssList(X0)|cons(hd(X0),tl(X0))=X0|nil=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f104])).
% 0.14/0.71 fof(f314,plain,(
% 0.14/0.71 ![X0]: (~ssList(X0)|cons(skaf83(X0),skaf82(X0))=X0|nil=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f109])).
% 0.14/0.71 fof(f323,plain,(
% 0.14/0.71 ![U]: ((![V]: ((~U=V|~neq(U,V))|~ssList(V)))|~ssList(U))),
% 0.14/0.71 inference(miniscoping,[status(thm)],[f115])).
% 0.14/0.71 fof(f324,plain,(
% 0.14/0.71 ![X0,X1]: (~X0=X1|~neq(X0,X1)|~ssList(X1)|~ssList(X0))),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f323])).
% 0.14/0.71 fof(f329,plain,(
% 0.14/0.71 ![U]: (((![V]: (~app(U,V)=nil|~ssList(V)))|~ssList(U))|nil=U)),
% 0.14/0.71 inference(miniscoping,[status(thm)],[f118])).
% 0.14/0.71 fof(f330,plain,(
% 0.14/0.71 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f329])).
% 0.14/0.71 fof(f331,plain,(
% 0.14/0.71 ![V]: ((![U]: ((~app(U,V)=nil|~ssList(V))|~ssList(U)))|nil=V)),
% 0.14/0.71 inference(miniscoping,[status(thm)],[f119])).
% 0.14/0.71 fof(f332,plain,(
% 0.14/0.71 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X1)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f331])).
% 0.14/0.71 fof(f342,plain,(
% 0.14/0.71 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f127])).
% 0.14/0.71 fof(f343,plain,(
% 0.14/0.71 ![X0,X1]: (~rearsegP(X0,X1)|~rearsegP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f128])).
% 0.14/0.71 fof(f344,plain,(
% 0.14/0.71 ![X0,X1]: (~frontsegP(X0,X1)|~frontsegP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f129])).
% 0.14/0.71 fof(f346,plain,(
% 0.14/0.71 ![X0,X1]: (~rearsegP(X0,X1)|~ssList(X1)|~ssList(X0)|app(skaf46(X0,X1),X1)=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f131])).
% 0.14/0.71 fof(f347,plain,(
% 0.14/0.71 ![X0,X1]: (~frontsegP(X0,X1)|~ssList(X1)|~ssList(X0)|app(X1,skaf45(X0,X1))=X0)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f132])).
% 0.14/0.71 fof(f364,plain,(
% 0.14/0.71 ![X0,X1]: (~nil=X0|~nil=X1|~ssList(X1)|~ssList(X0)|app(X0,X1)=nil)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f145])).
% 0.14/0.71 fof(f372,plain,(
% 0.14/0.71 ![V,W]: (((![U]: ((~app(U,V)=app(U,W)|~ssList(V))|~ssList(U)))|~ssList(W))|V=W)),
% 0.14/0.71 inference(miniscoping,[status(thm)],[f150])).
% 0.14/0.71 fof(f373,plain,(
% 0.14/0.71 ![X0,X1,X2]: (~app(X0,X1)=app(X0,X2)|~ssList(X1)|~ssList(X0)|~ssList(X2)|X1=X2)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f372])).
% 0.14/0.71 fof(f374,plain,(
% 0.14/0.71 ![U,W]: (((![V]: ((~app(U,V)=app(W,V)|~ssList(U))|~ssList(V)))|~ssList(W))|U=W)),
% 0.14/0.71 inference(miniscoping,[status(thm)],[f151])).
% 0.14/0.71 fof(f375,plain,(
% 0.14/0.71 ![X0,X1,X2]: (~app(X0,X1)=app(X2,X1)|~ssList(X0)|~ssList(X1)|~ssList(X2)|X0=X2)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f374])).
% 0.14/0.71 fof(f376,plain,(
% 0.14/0.71 ![U,W]: (((![V]: (((~segmentP(U,V)|~segmentP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|segmentP(U,W))),
% 0.14/0.71 inference(miniscoping,[status(thm)],[f152])).
% 0.14/0.71 fof(f377,plain,(
% 0.14/0.71 ![X0,X1,X2]: (~segmentP(X0,X1)|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|segmentP(X0,X2))),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f376])).
% 0.14/0.71 fof(f407,plain,(
% 0.14/0.71 ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f172])).
% 0.14/0.71 fof(f408,plain,(
% 0.14/0.71 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 0.14/0.71 inference(miniscoping,[status(thm)],[f173])).
% 0.14/0.71 fof(f409,plain,(
% 0.14/0.71 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f408])).
% 0.14/0.71 fof(f435,plain,(
% 0.14/0.71 ssList(sk3)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f188])).
% 0.14/0.71 fof(f436,plain,(
% 0.14/0.71 ssList(sk4)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f189])).
% 0.14/0.71 fof(f437,plain,(
% 0.14/0.71 sk2=sk4),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f190])).
% 0.14/0.71 fof(f438,plain,(
% 0.14/0.71 sk1=sk3),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f191])).
% 0.14/0.71 fof(f439,plain,(
% 0.14/0.71 ssList(sk5)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f192])).
% 0.14/0.71 fof(f440,plain,(
% 0.14/0.71 ssList(sk6)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f193])).
% 0.14/0.71 fof(f441,plain,(
% 0.14/0.71 app(app(sk5,sk3),sk6)=sk4),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f194])).
% 0.14/0.71 fof(f447,plain,(
% 0.14/0.71 nil=sk4|~nil=sk3),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f198])).
% 0.14/0.71 fof(f449,plain,(
% 0.14/0.71 nil=sk2|~neq(sk1,nil)|~segmentP(sk2,sk1)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f200])).
% 0.14/0.71 fof(f450,plain,(
% 0.14/0.71 ~nil=sk1|neq(sk2,nil)),
% 0.14/0.71 inference(cnf_transformation,[status(thm)],[f201])).
% 0.14/0.71 fof(f459,definition,(
% 0.14/0.71 sQ2_spl <=> (nil=sk4)),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f460,plain,(
% 0.14/0.71 nil=sk4|~sQ2_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f459])).
% 0.14/0.71 fof(f462,definition,(
% 0.14/0.71 sQ3_spl <=> (nil=sk3)),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f464,plain,(
% 0.14/0.71 ~nil=sk3|sQ3_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f462])).
% 0.14/0.71 fof(f465,plain,(
% 0.14/0.71 sQ2_spl|~sQ3_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f447,f459,f462])).
% 0.14/0.71 fof(f466,definition,(
% 0.14/0.71 sQ4_spl <=> (nil=sk2)),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f467,plain,(
% 0.14/0.71 nil=sk2|~sQ4_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f466])).
% 0.14/0.71 fof(f469,definition,(
% 0.14/0.71 sQ5_spl <=> (neq(sk2,nil))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f470,plain,(
% 0.14/0.71 neq(sk2,nil)|~sQ5_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f469])).
% 0.14/0.71 fof(f473,definition,(
% 0.14/0.71 sQ6_spl <=> (neq(sk1,nil))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f475,plain,(
% 0.14/0.71 ~neq(sk1,nil)|sQ6_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f473])).
% 0.14/0.71 fof(f476,definition,(
% 0.14/0.71 sQ7_spl <=> (segmentP(sk2,sk1))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f478,plain,(
% 0.14/0.71 ~segmentP(sk2,sk1)|sQ7_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f476])).
% 0.14/0.71 fof(f479,plain,(
% 0.14/0.71 sQ4_spl|~sQ6_spl|~sQ7_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f449,f466,f473,f476])).
% 0.14/0.71 fof(f480,definition,(
% 0.14/0.71 sQ8_spl <=> (nil=sk1)),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f482,plain,(
% 0.14/0.71 ~nil=sk1|sQ8_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f480])).
% 0.14/0.71 fof(f483,plain,(
% 0.14/0.71 ~sQ8_spl|sQ5_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f450,f480,f469])).
% 0.14/0.71 fof(f485,plain,(
% 0.14/0.71 ~ssList(nil)|segmentP(nil,nil)),
% 0.14/0.71 inference(destructive_equality_resolution,[status(thm)],[f282])).
% 0.14/0.71 fof(f492,plain,(
% 0.14/0.71 ![X1]: (~neq(X1,X1)|~ssList(X1)|~ssList(X1))),
% 0.14/0.71 inference(destructive_equality_resolution,[status(thm)],[f324])).
% 0.14/0.71 fof(f493,plain,(
% 0.14/0.71 ![X0]: (~neq(X0,X0)|~ssList(X0))),
% 0.14/0.71 inference(duplicate_literals_removal,[status(thm)],[f492])).
% 0.14/0.71 fof(f501,plain,(
% 0.14/0.71 ~ssList(nil)|~ssList(nil)|app(nil,nil)=nil),
% 0.14/0.71 inference(destructive_equality_resolution,[status(thm)],[f364])).
% 0.14/0.71 fof(f502,plain,(
% 0.14/0.71 ~ssList(nil)|app(nil,nil)=nil),
% 0.14/0.71 inference(duplicate_literals_removal,[status(thm)],[f501])).
% 0.14/0.71 fof(f503,plain,(
% 0.14/0.71 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 0.14/0.71 inference(destructive_equality_resolution,[status(thm)],[f409])).
% 0.14/0.71 fof(f516,plain,(
% 0.14/0.71 ~nil=sk3|sQ8_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f438,f482])).
% 0.14/0.71 fof(f528,plain,(
% 0.14/0.71 nil=sk4|~sQ4_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f437,f467])).
% 0.14/0.71 fof(f579,definition,(
% 0.14/0.71 sQ9_spl <=> (ssList(sk4))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f587,plain,(
% 0.14/0.71 neq(sk4,nil)|~sQ5_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f437,f470])).
% 0.14/0.71 fof(f588,plain,(
% 0.14/0.71 ~segmentP(sk4,sk1)|sQ7_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f437,f478])).
% 0.14/0.71 fof(f589,plain,(
% 0.14/0.71 ~segmentP(sk4,sk3)|sQ7_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f438,f588])).
% 0.14/0.71 fof(f590,plain,(
% 0.14/0.71 ~neq(sk3,nil)|sQ6_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f438,f475])).
% 0.14/0.71 fof(f591,definition,(
% 0.14/0.71 sQ11_spl <=> (ssList(nil))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f593,plain,(
% 0.14/0.71 ~ssList(nil)|sQ11_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f591])).
% 0.14/0.71 fof(f594,definition,(
% 0.14/0.71 sQ12_spl <=> (segmentP(nil,nil))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f595,plain,(
% 0.14/0.71 segmentP(nil,nil)|~sQ12_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f594])).
% 0.14/0.71 fof(f597,plain,(
% 0.14/0.71 ~sQ11_spl|sQ12_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f485,f591,f594])).
% 0.14/0.71 fof(f598,plain,(
% 0.14/0.71 ~ssList(sk6)|~ssList(app(sk5,sk3))|ssList(sk4)),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f441,f288])).
% 0.14/0.71 fof(f599,definition,(
% 0.14/0.71 sQ13_spl <=> (ssList(sk6))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f601,plain,(
% 0.14/0.71 ~ssList(sk6)|sQ13_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f599])).
% 0.14/0.71 fof(f602,definition,(
% 0.14/0.71 sQ14_spl <=> (ssList(app(sk5,sk3)))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f604,plain,(
% 0.14/0.71 ~ssList(app(sk5,sk3))|sQ14_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f602])).
% 0.14/0.71 fof(f605,plain,(
% 0.14/0.71 ~sQ13_spl|~sQ14_spl|sQ9_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f598,f599,f602,f579])).
% 0.14/0.71 fof(f606,plain,(
% 0.14/0.71 $false|sQ13_spl),
% 0.14/0.71 inference(forward_subsumption_resolution,[status(thm)],[f601,f440])).
% 0.14/0.71 fof(f607,plain,(
% 0.14/0.71 sQ13_spl),
% 0.14/0.71 inference(contradiction_clause,[status(thm)],[f606])).
% 0.14/0.71 fof(f616,plain,(
% 0.14/0.71 neq(sk4,sk4)|~sQ2_spl|~sQ5_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f460,f587])).
% 0.14/0.71 fof(f618,plain,(
% 0.14/0.71 ~ssList(sk4)|~sQ2_spl|~sQ5_spl),
% 0.14/0.71 inference(resolution,[status(thm)],[f616,f493])).
% 0.14/0.71 fof(f619,plain,(
% 0.14/0.71 $false|~sQ2_spl|~sQ5_spl),
% 0.14/0.71 inference(forward_subsumption_resolution,[status(thm)],[f618,f436])).
% 0.14/0.71 fof(f620,plain,(
% 0.14/0.71 ~sQ2_spl|~sQ5_spl),
% 0.14/0.71 inference(contradiction_clause,[status(thm)],[f619])).
% 0.14/0.71 fof(f631,plain,(
% 0.14/0.71 ~ssList(sk3)|~ssList(sk5)|sQ14_spl),
% 0.14/0.71 inference(resolution,[status(thm)],[f604,f288])).
% 0.14/0.71 fof(f632,definition,(
% 0.14/0.71 sQ15_spl <=> (ssList(sk3))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f634,plain,(
% 0.14/0.71 ~ssList(sk3)|sQ15_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f632])).
% 0.14/0.71 fof(f635,definition,(
% 0.14/0.71 sQ16_spl <=> (ssList(sk5))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f637,plain,(
% 0.14/0.71 ~ssList(sk5)|sQ16_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f635])).
% 0.14/0.71 fof(f638,plain,(
% 0.14/0.71 ~sQ15_spl|~sQ16_spl|sQ14_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f631,f632,f635,f602])).
% 0.14/0.71 fof(f639,plain,(
% 0.14/0.71 $false|sQ15_spl),
% 0.14/0.71 inference(forward_subsumption_resolution,[status(thm)],[f634,f435])).
% 0.14/0.71 fof(f640,plain,(
% 0.14/0.71 sQ15_spl),
% 0.14/0.71 inference(contradiction_clause,[status(thm)],[f639])).
% 0.14/0.71 fof(f641,plain,(
% 0.14/0.71 $false|sQ16_spl),
% 0.14/0.71 inference(forward_subsumption_resolution,[status(thm)],[f637,f439])).
% 0.14/0.71 fof(f642,plain,(
% 0.14/0.71 sQ16_spl),
% 0.14/0.71 inference(contradiction_clause,[status(thm)],[f641])).
% 0.14/0.71 fof(f647,plain,(
% 0.14/0.71 app(nil,nil)=nil),
% 0.14/0.71 inference(resolution,[status(thm)],[f277,f210])).
% 0.14/0.71 fof(f665,plain,(
% 0.14/0.71 app(nil,sk6)=sk6),
% 0.14/0.71 inference(resolution,[status(thm)],[f277,f440])).
% 0.14/0.71 fof(f666,plain,(
% 0.14/0.71 app(nil,sk5)=sk5),
% 0.14/0.71 inference(resolution,[status(thm)],[f277,f439])).
% 0.14/0.71 fof(f667,plain,(
% 0.14/0.71 app(nil,sk4)=sk4),
% 0.14/0.71 inference(resolution,[status(thm)],[f277,f436])).
% 0.14/0.71 fof(f668,plain,(
% 0.14/0.71 app(nil,sk3)=sk3),
% 0.14/0.71 inference(resolution,[status(thm)],[f277,f435])).
% 0.14/0.71 fof(f685,plain,(
% 0.14/0.71 ~ssList(nil)|~ssList(sk3)|sk3=nil|sQ6_spl),
% 0.14/0.71 inference(resolution,[status(thm)],[f305,f590])).
% 0.14/0.71 fof(f688,plain,(
% 0.14/0.71 ~sQ11_spl|~sQ15_spl|sQ3_spl|sQ6_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f685,f591,f632,f462,f473])).
% 0.14/0.71 fof(f689,plain,(
% 0.14/0.71 $false|sQ11_spl),
% 0.14/0.71 inference(forward_subsumption_resolution,[status(thm)],[f593,f210])).
% 0.14/0.71 fof(f690,plain,(
% 0.14/0.71 sQ11_spl),
% 0.14/0.71 inference(contradiction_clause,[status(thm)],[f689])).
% 0.14/0.71 fof(f737,plain,(
% 0.14/0.71 app(sk6,nil)=sk6),
% 0.14/0.71 inference(resolution,[status(thm)],[f276,f440])).
% 0.14/0.71 fof(f738,plain,(
% 0.14/0.71 app(sk5,nil)=sk5),
% 0.14/0.71 inference(resolution,[status(thm)],[f276,f439])).
% 0.14/0.71 fof(f739,plain,(
% 0.14/0.71 app(sk4,nil)=sk4),
% 0.14/0.71 inference(resolution,[status(thm)],[f276,f436])).
% 0.14/0.71 fof(f740,plain,(
% 0.14/0.71 app(sk3,nil)=sk3),
% 0.14/0.71 inference(resolution,[status(thm)],[f276,f435])).
% 0.14/0.71 fof(f934,plain,(
% 0.14/0.71 ![X0]: (~app(X0,sk5)=nil|~ssList(X0)|nil=sk5)),
% 0.14/0.71 inference(resolution,[status(thm)],[f332,f439])).
% 0.14/0.71 fof(f941,definition,(
% 0.14/0.71 sQ18_spl <=> (nil=nil)),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f955,definition,(
% 0.14/0.71 sQ22_spl <=> (nil=sk6)),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f956,plain,(
% 0.14/0.71 nil=sk6|~sQ22_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f955])).
% 0.14/0.71 fof(f959,definition,(
% 0.14/0.71 ![X0]: (sQ23_spl <=> (~app(X0,sk5)=nil|~ssList(X0)))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f960,plain,(
% 0.14/0.71 ![X0]: (~app(X0,sk5)=nil|~ssList(X0)|~sQ23_spl)),
% 0.14/0.71 inference(component_clause,[status(thm)],[f959])).
% 0.14/0.71 fof(f962,definition,(
% 0.14/0.71 sQ24_spl <=> (nil=sk5)),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f963,plain,(
% 0.14/0.71 nil=sk5|~sQ24_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f962])).
% 0.14/0.71 fof(f965,plain,(
% 0.14/0.71 sQ23_spl|sQ24_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f934,f959,f962])).
% 0.14/0.71 fof(f974,plain,(
% 0.14/0.71 ~sQ3_spl|sQ8_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f516,f462,f480])).
% 0.14/0.71 fof(f1068,plain,(
% 0.14/0.71 ~app(nil,sk5)=nil|~sQ23_spl),
% 0.14/0.71 inference(resolution,[status(thm)],[f960,f210])).
% 0.14/0.71 fof(f1103,plain,(
% 0.14/0.71 ~sk5=nil|~sQ23_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f666,f1068])).
% 0.14/0.71 fof(f1173,plain,(
% 0.14/0.71 app(sk5,sk3)=sk3|~sQ24_spl),
% 0.14/0.71 inference(backward_demodulation,[status(thm)],[f963,f668])).
% 0.14/0.71 fof(f1187,plain,(
% 0.14/0.71 segmentP(nil,sk5)|~sQ24_spl|~sQ12_spl),
% 0.14/0.71 inference(backward_demodulation,[status(thm)],[f963,f595])).
% 0.14/0.71 fof(f1202,plain,(
% 0.14/0.71 ~sk5=sk3|~sQ24_spl|sQ3_spl),
% 0.14/0.71 inference(backward_demodulation,[status(thm)],[f963,f464])).
% 0.14/0.71 fof(f1209,plain,(
% 0.14/0.71 segmentP(sk5,sk5)|~sQ24_spl|~sQ12_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f963,f1187])).
% 0.14/0.71 fof(f1221,plain,(
% 0.14/0.71 ~segmentP(sk5,sk5)|~ssList(sk5)|~ssList(sk5)|sk5=sk5|~sQ24_spl|~sQ12_spl),
% 0.14/0.71 inference(resolution,[status(thm)],[f1209,f342])).
% 0.14/0.71 fof(f1222,definition,(
% 0.14/0.71 sQ33_spl <=> (segmentP(sk5,sk5))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1225,definition,(
% 0.14/0.71 sQ34_spl <=> (sk5=sk5)),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1228,plain,(
% 0.14/0.71 ~sQ33_spl|~sQ16_spl|sQ34_spl|~sQ24_spl|~sQ12_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1221,f1222,f635,f1225,f962,f594])).
% 0.14/0.71 fof(f1238,plain,(
% 0.14/0.71 ~sk5=sk6|~sQ22_spl|~sQ23_spl),
% 0.14/0.71 inference(backward_demodulation,[status(thm)],[f956,f1103])).
% 0.14/0.71 fof(f1245,plain,(
% 0.14/0.71 ~sk6=sk3|~sQ22_spl|sQ3_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f956,f464])).
% 0.14/0.71 fof(f1259,plain,(
% 0.14/0.71 segmentP(sk6,nil)|~sQ22_spl|~sQ12_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f956,f595])).
% 0.14/0.71 fof(f1260,plain,(
% 0.14/0.71 segmentP(sk6,sk6)|~sQ22_spl|~sQ12_spl),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f956,f1259])).
% 0.14/0.71 fof(f1261,plain,(
% 0.14/0.71 ~segmentP(sk6,sk6)|~ssList(sk6)|~ssList(sk6)|sk6=sk6|~sQ22_spl|~sQ12_spl),
% 0.14/0.71 inference(resolution,[status(thm)],[f1260,f342])).
% 0.14/0.71 fof(f1262,definition,(
% 0.14/0.71 sQ35_spl <=> (segmentP(sk6,sk6))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1264,plain,(
% 0.14/0.71 ~segmentP(sk6,sk6)|sQ35_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f1262])).
% 0.14/0.71 fof(f1265,definition,(
% 0.14/0.71 sQ36_spl <=> (sk6=sk6)),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1268,plain,(
% 0.14/0.71 ~sQ35_spl|~sQ13_spl|sQ36_spl|~sQ22_spl|~sQ12_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1261,f1262,f599,f1265,f955,f594])).
% 0.14/0.71 fof(f1269,definition,(
% 0.14/0.71 sQ37_spl <=> (app(nil,nil)=nil)),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1270,plain,(
% 0.14/0.71 app(nil,nil)=nil|~sQ37_spl),
% 0.14/0.71 inference(component_clause,[status(thm)],[f1269])).
% 0.14/0.71 fof(f1272,plain,(
% 0.14/0.71 ~sQ11_spl|sQ37_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f502,f591,f1269])).
% 0.14/0.71 fof(f1273,plain,(
% 0.14/0.71 ~ssList(nil)|nil=nil|~ssList(nil)),
% 0.14/0.71 inference(resolution,[status(thm)],[f285,f261])).
% 0.14/0.71 fof(f1274,plain,(
% 0.14/0.71 ~sQ11_spl|sQ18_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1273,f591,f941])).
% 0.14/0.71 fof(f1385,plain,(
% 0.14/0.71 ![X0]: (~sk4=app(app(sk5,sk3),X0)|~ssList(sk6)|~ssList(app(sk5,sk3))|~ssList(X0)|sk6=X0)),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f441,f373])).
% 0.14/0.71 fof(f1387,plain,(
% 0.14/0.71 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(X0)|X0=X0)),
% 0.14/0.71 inference(equality_resolution,[status(thm)],[f373])).
% 0.14/0.71 fof(f1388,definition,(
% 0.14/0.71 ![X0]: (sQ38_spl <=> (~sk4=app(app(sk5,sk3),X0)|~ssList(X0)|sk6=X0))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1391,plain,(
% 0.14/0.71 sQ38_spl|~sQ13_spl|~sQ14_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1385,f1388,f599,f602])).
% 0.14/0.71 fof(f1393,definition,(
% 0.14/0.71 ![X0]: (sQ39_spl <=> (~ssList(X0)|~ssList(X0)|X0=X0))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1396,definition,(
% 0.14/0.71 ![X1]: (sQ40_spl <=> (~ssList(X1)))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1397,plain,(
% 0.14/0.71 ![X0]: (~ssList(X0)|~sQ40_spl)),
% 0.14/0.71 inference(component_clause,[status(thm)],[f1396])).
% 0.14/0.71 fof(f1399,plain,(
% 0.14/0.71 sQ39_spl|sQ40_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1387,f1393,f1396])).
% 0.14/0.71 fof(f1400,plain,(
% 0.14/0.71 $false|~sQ40_spl),
% 0.14/0.71 inference(backward_subsumption_resolution,[status(thm)],[f210,f1397])).
% 0.14/0.71 fof(f1433,plain,(
% 0.14/0.71 ~sQ40_spl),
% 0.14/0.71 inference(contradiction_clause,[status(thm)],[f1400])).
% 0.14/0.71 fof(f1445,plain,(
% 0.14/0.71 ~ssList(sk6)|sQ35_spl),
% 0.14/0.71 inference(resolution,[status(thm)],[f259,f1264])).
% 0.14/0.71 fof(f1446,plain,(
% 0.14/0.71 ~sQ13_spl|sQ35_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1445,f599,f1262])).
% 0.14/0.71 fof(f1484,plain,(
% 0.14/0.71 ![X0]: (~app(X0,sk6)=sk6|~ssList(X0)|~ssList(sk6)|~ssList(nil)|X0=nil)),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f665,f375])).
% 0.14/0.71 fof(f1486,definition,(
% 0.14/0.71 ![X0]: (sQ43_spl <=> (~app(X0,sk6)=sk6|~ssList(X0)|X0=nil))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1489,plain,(
% 0.14/0.71 sQ43_spl|~sQ13_spl|~sQ11_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1484,f1486,f599,f591])).
% 0.14/0.71 fof(f1491,plain,(
% 0.14/0.71 ![X0]: (~app(X0,sk5)=sk5|~ssList(X0)|~ssList(sk5)|~ssList(nil)|X0=nil)),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f666,f375])).
% 0.14/0.71 fof(f1493,definition,(
% 0.14/0.71 ![X0]: (sQ44_spl <=> (~app(X0,sk5)=sk5|~ssList(X0)|X0=nil))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1496,plain,(
% 0.14/0.71 sQ44_spl|~sQ16_spl|~sQ11_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1491,f1493,f635,f591])).
% 0.14/0.71 fof(f1498,plain,(
% 0.14/0.71 ![X0]: (~app(X0,sk6)=sk4|~ssList(X0)|~ssList(sk6)|~ssList(app(sk5,sk3))|X0=app(sk5,sk3))),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f441,f375])).
% 0.14/0.71 fof(f1500,definition,(
% 0.14/0.71 ![X0]: (sQ45_spl <=> (~app(X0,sk6)=sk4|~ssList(X0)|X0=app(sk5,sk3)))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1503,plain,(
% 0.14/0.71 sQ45_spl|~sQ13_spl|~sQ14_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1498,f1500,f599,f602])).
% 0.14/0.71 fof(f1505,plain,(
% 0.14/0.71 ![X0]: (~app(X0,nil)=nil|~ssList(X0)|~ssList(nil)|~ssList(nil)|X0=nil)),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f647,f375])).
% 0.14/0.71 fof(f1507,definition,(
% 0.14/0.71 ![X0]: (sQ46_spl <=> (~app(X0,nil)=nil|~ssList(X0)|X0=nil))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1510,plain,(
% 0.14/0.71 sQ46_spl|~sQ11_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1505,f1507,f591])).
% 0.14/0.71 fof(f1512,plain,(
% 0.14/0.71 ![X0]: (~app(X0,sk4)=sk4|~ssList(X0)|~ssList(sk4)|~ssList(nil)|X0=nil)),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f667,f375])).
% 0.14/0.71 fof(f1514,definition,(
% 0.14/0.71 ![X0]: (sQ47_spl <=> (~app(X0,sk4)=sk4|~ssList(X0)|X0=nil))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1517,plain,(
% 0.14/0.71 sQ47_spl|~sQ9_spl|~sQ11_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1512,f1514,f579,f591])).
% 0.14/0.71 fof(f1519,plain,(
% 0.14/0.71 ![X0]: (~app(X0,sk3)=sk3|~ssList(X0)|~ssList(sk3)|~ssList(nil)|X0=nil)),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f668,f375])).
% 0.14/0.71 fof(f1521,definition,(
% 0.14/0.71 ![X0]: (sQ48_spl <=> (~app(X0,sk3)=sk3|~ssList(X0)|X0=nil))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1524,plain,(
% 0.14/0.71 sQ48_spl|~sQ15_spl|~sQ11_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1519,f1521,f632,f591])).
% 0.14/0.71 fof(f1526,plain,(
% 0.14/0.71 ![X0]: (~app(X0,nil)=sk6|~ssList(X0)|~ssList(nil)|~ssList(sk6)|X0=sk6)),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f737,f375])).
% 0.14/0.71 fof(f1528,definition,(
% 0.14/0.71 ![X0]: (sQ49_spl <=> (~app(X0,nil)=sk6|~ssList(X0)|X0=sk6))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1531,plain,(
% 0.14/0.71 sQ49_spl|~sQ11_spl|~sQ13_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1526,f1528,f591,f599])).
% 0.14/0.71 fof(f1533,plain,(
% 0.14/0.71 ![X0]: (~app(X0,nil)=sk5|~ssList(X0)|~ssList(nil)|~ssList(sk5)|X0=sk5)),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f738,f375])).
% 0.14/0.71 fof(f1535,definition,(
% 0.14/0.71 ![X0]: (sQ50_spl <=> (~app(X0,nil)=sk5|~ssList(X0)|X0=sk5))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1538,plain,(
% 0.14/0.71 sQ50_spl|~sQ11_spl|~sQ16_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1533,f1535,f591,f635])).
% 0.14/0.71 fof(f1540,plain,(
% 0.14/0.71 ![X0]: (~app(X0,nil)=sk4|~ssList(X0)|~ssList(nil)|~ssList(sk4)|X0=sk4)),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f739,f375])).
% 0.14/0.71 fof(f1542,definition,(
% 0.14/0.71 ![X0]: (sQ51_spl <=> (~app(X0,nil)=sk4|~ssList(X0)|X0=sk4))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1545,plain,(
% 0.14/0.71 sQ51_spl|~sQ11_spl|~sQ9_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1540,f1542,f591,f579])).
% 0.14/0.71 fof(f1637,plain,(
% 0.14/0.71 ![X0]: (~app(X0,nil)=sk3|~ssList(X0)|~ssList(nil)|~ssList(sk3)|X0=sk3)),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f740,f375])).
% 0.14/0.71 fof(f1639,definition,(
% 0.14/0.71 ![X0]: (sQ52_spl <=> (~app(X0,nil)=sk3|~ssList(X0)|X0=sk3))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1642,plain,(
% 0.14/0.71 sQ52_spl|~sQ11_spl|~sQ15_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1637,f1639,f591,f632])).
% 0.14/0.71 fof(f1742,plain,(
% 0.14/0.71 ![X0]: (~segmentP(sk3,X0)|~ssList(sk6)|~ssList(sk5)|~ssList(X0)|~ssList(sk3)|segmentP(sk4,X0))),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f441,f407])).
% 0.14/0.71 fof(f1743,plain,(
% 0.14/0.71 ![X0,X1]: (~segmentP(sk6,X0)|~ssList(X1)|~ssList(app(sk5,sk3))|~ssList(X0)|~ssList(sk6)|segmentP(app(sk4,X1),X0))),
% 0.14/0.71 inference(paramodulation,[status(thm)],[f441,f407])).
% 0.14/0.71 fof(f1744,definition,(
% 0.14/0.71 ![X0]: (sQ59_spl <=> (~segmentP(sk3,X0)|~ssList(X0)|segmentP(sk4,X0)))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1747,plain,(
% 0.14/0.71 sQ59_spl|~sQ13_spl|~sQ16_spl|~sQ15_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1742,f1744,f599,f635,f632])).
% 0.14/0.71 fof(f1748,definition,(
% 0.14/0.71 ![X0,X1]: (sQ60_spl <=> (~segmentP(sk6,X0)|~ssList(X1)|~ssList(X0)|segmentP(app(sk4,X1),X0)))),
% 0.14/0.71 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.14/0.71 fof(f1751,plain,(
% 0.14/0.71 sQ60_spl|~sQ14_spl|~sQ13_spl),
% 0.14/0.71 inference(split_clause,[status(thm)],[f1743,f1748,f602,f599])).
% 0.14/0.71 fof(f1752,plain,(
% 0.14/0.71 ![X0]: (~ssList(X0)|cons(hd(X0),tl(X0))=X0|sk5=X0|~sQ24_spl)),
% 0.14/0.71 inference(forward_demodulation,[status(thm)],[f963,f309])).
% 0.14/0.71 fof(f1779,plain,(
% 0.14/0.71 cons(hd(sk3),tl(sk3))=sk3|sk5=sk3|~sQ24_spl),
% 0.14/0.71 inference(resolution,[status(thm)],[f1752,f435])).
% 0.14/0.71 fof(f1780,plain,(
% 0.14/0.71 cons(hd(sk4),tl(sk4))=sk4|sk5=sk4|~sQ24_spl),
% 0.14/0.71 inference(resolution,[status(thm)],[f1752,f436])).
% 0.14/0.71 fof(f1781,plain,(
% 0.14/0.72 cons(hd(sk5),tl(sk5))=sk5|sk5=sk5|~sQ24_spl),
% 0.14/0.72 inference(resolution,[status(thm)],[f1752,f439])).
% 0.14/0.72 fof(f1783,definition,(
% 0.14/0.72 sQ61_spl <=> (cons(hd(sk3),tl(sk3))=sk3)),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1786,definition,(
% 0.14/0.72 sQ62_spl <=> (sk5=sk3)),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1787,plain,(
% 0.14/0.72 sk5=sk3|~sQ62_spl),
% 0.14/0.72 inference(component_clause,[status(thm)],[f1786])).
% 0.14/0.72 fof(f1789,plain,(
% 0.14/0.72 sQ61_spl|sQ62_spl|~sQ24_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f1779,f1783,f1786,f962])).
% 0.14/0.72 fof(f1790,definition,(
% 0.14/0.72 sQ63_spl <=> (cons(hd(sk4),tl(sk4))=sk4)),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1793,definition,(
% 0.14/0.72 sQ64_spl <=> (sk5=sk4)),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1796,plain,(
% 0.14/0.72 sQ63_spl|sQ64_spl|~sQ24_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f1780,f1790,f1793,f962])).
% 0.14/0.72 fof(f1797,definition,(
% 0.14/0.72 sQ65_spl <=> (cons(hd(sk5),tl(sk5))=sk5)),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1800,plain,(
% 0.14/0.72 sQ65_spl|sQ34_spl|~sQ24_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f1781,f1797,f1225,f962])).
% 0.14/0.72 fof(f1804,definition,(
% 0.14/0.72 sQ67_spl <=> (sk5=sk6)),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1805,plain,(
% 0.14/0.72 sk5=sk6|~sQ67_spl),
% 0.14/0.72 inference(component_clause,[status(thm)],[f1804])).
% 0.14/0.72 fof(f1811,plain,(
% 0.14/0.72 ~ssList(sk6)|~ssList(sk5)|~ssList(sk3)|~ssList(sk4)|segmentP(app(app(sk5,sk3),sk6),sk3)),
% 0.14/0.72 inference(paramodulation,[status(thm)],[f441,f503])).
% 0.14/0.72 fof(f1812,plain,(
% 0.14/0.72 ![X0]: (~ssList(X0)|~ssList(app(sk5,sk3))|~ssList(sk6)|~ssList(app(sk4,X0))|segmentP(app(app(app(sk5,sk3),sk6),X0),sk6))),
% 0.14/0.72 inference(paramodulation,[status(thm)],[f441,f503])).
% 0.14/0.72 fof(f1813,definition,(
% 0.14/0.72 sQ68_spl <=> (segmentP(app(app(sk5,sk3),sk6),sk3))),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1814,plain,(
% 0.14/0.72 segmentP(app(app(sk5,sk3),sk6),sk3)|~sQ68_spl),
% 0.14/0.72 inference(component_clause,[status(thm)],[f1813])).
% 0.14/0.72 fof(f1816,plain,(
% 0.14/0.72 ~sQ13_spl|~sQ16_spl|~sQ15_spl|~sQ9_spl|sQ68_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f1811,f599,f635,f632,f579,f1813])).
% 0.14/0.72 fof(f1817,definition,(
% 0.14/0.72 ![X0]: (sQ69_spl <=> (~ssList(X0)|~ssList(app(sk4,X0))|segmentP(app(app(app(sk5,sk3),sk6),X0),sk6)))),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1820,plain,(
% 0.14/0.72 sQ69_spl|~sQ14_spl|~sQ13_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f1812,f1817,f602,f599])).
% 0.14/0.72 fof(f1821,plain,(
% 0.14/0.72 segmentP(sk4,sk3)|~sQ68_spl),
% 0.14/0.72 inference(forward_demodulation,[status(thm)],[f441,f1814])).
% 0.14/0.72 fof(f1822,plain,(
% 0.14/0.72 $false|sQ7_spl|~sQ68_spl),
% 0.14/0.72 inference(forward_subsumption_resolution,[status(thm)],[f1821,f589])).
% 0.14/0.72 fof(f1823,plain,(
% 0.14/0.72 sQ7_spl|~sQ68_spl),
% 0.14/0.72 inference(contradiction_clause,[status(thm)],[f1822])).
% 0.14/0.72 fof(f1827,plain,(
% 0.14/0.72 sQ2_spl|~sQ4_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f528,f459,f466])).
% 0.14/0.72 fof(f1838,plain,(
% 0.14/0.72 ![X0]: (~ssList(X0)|cons(skaf83(X0),skaf82(X0))=X0|sk5=X0|~sQ24_spl)),
% 0.14/0.72 inference(forward_demodulation,[status(thm)],[f963,f314])).
% 0.14/0.72 fof(f1865,plain,(
% 0.14/0.72 cons(skaf83(sk3),skaf82(sk3))=sk3|sk5=sk3|~sQ24_spl),
% 0.14/0.72 inference(resolution,[status(thm)],[f1838,f435])).
% 0.14/0.72 fof(f1866,plain,(
% 0.14/0.72 cons(skaf83(sk4),skaf82(sk4))=sk4|sk5=sk4|~sQ24_spl),
% 0.14/0.72 inference(resolution,[status(thm)],[f1838,f436])).
% 0.14/0.72 fof(f1867,plain,(
% 0.14/0.72 cons(skaf83(sk5),skaf82(sk5))=sk5|sk5=sk5|~sQ24_spl),
% 0.14/0.72 inference(resolution,[status(thm)],[f1838,f439])).
% 0.14/0.72 fof(f1869,definition,(
% 0.14/0.72 sQ70_spl <=> (cons(skaf83(sk3),skaf82(sk3))=sk3)),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1872,plain,(
% 0.14/0.72 sQ70_spl|sQ62_spl|~sQ24_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f1865,f1869,f1786,f962])).
% 0.14/0.72 fof(f1873,definition,(
% 0.14/0.72 sQ71_spl <=> (cons(skaf83(sk4),skaf82(sk4))=sk4)),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1876,plain,(
% 0.14/0.72 sQ71_spl|sQ64_spl|~sQ24_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f1866,f1873,f1793,f962])).
% 0.14/0.72 fof(f1877,definition,(
% 0.14/0.72 sQ72_spl <=> (cons(skaf83(sk5),skaf82(sk5))=sk5)),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1880,plain,(
% 0.14/0.72 sQ72_spl|sQ34_spl|~sQ24_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f1867,f1877,f1225,f962])).
% 0.14/0.72 fof(f1885,plain,(
% 0.14/0.72 $false|~sQ24_spl|sQ3_spl|~sQ62_spl),
% 0.14/0.72 inference(forward_subsumption_resolution,[status(thm)],[f1787,f1202])).
% 0.14/0.72 fof(f1886,plain,(
% 0.14/0.72 ~sQ24_spl|sQ3_spl|~sQ62_spl),
% 0.14/0.72 inference(contradiction_clause,[status(thm)],[f1885])).
% 0.14/0.72 fof(f1887,plain,(
% 0.14/0.72 ![X0,X1]: (~ssList(X0)|nil=X0|~segmentP(nil,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|~ssList(nil))),
% 0.14/0.72 inference(resolution,[status(thm)],[f283,f377])).
% 0.14/0.72 fof(f1889,definition,(
% 0.14/0.72 ![X0,X1]: (sQ74_spl <=> (~ssList(X0)|nil=X0|~segmentP(nil,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)))),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1892,plain,(
% 0.14/0.72 sQ74_spl|~sQ11_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f1887,f1889,f591])).
% 0.14/0.72 fof(f1895,plain,(
% 0.14/0.72 ~sk4=nil|~ssList(sk6)|~ssList(app(sk5,sk3))|nil=sk6),
% 0.14/0.72 inference(paramodulation,[status(thm)],[f441,f332])).
% 0.14/0.72 fof(f1896,plain,(
% 0.14/0.72 ~sQ2_spl|~sQ13_spl|~sQ14_spl|sQ22_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f1895,f459,f599,f602,f955])).
% 0.14/0.72 fof(f1916,plain,(
% 0.14/0.72 sk6=sk4|~sQ22_spl|~sQ2_spl),
% 0.14/0.72 inference(backward_demodulation,[status(thm)],[f956,f460])).
% 0.14/0.72 fof(f1917,plain,(
% 0.14/0.72 ![X0,X1]: (~app(X0,X1)=sk6|~ssList(X1)|~ssList(X0)|nil=X0|~sQ22_spl)),
% 0.14/0.72 inference(forward_demodulation,[status(thm)],[f956,f330])).
% 0.14/0.72 fof(f1918,plain,(
% 0.14/0.72 ![X0,X1]: (~app(X0,X1)=sk6|~ssList(X1)|~ssList(X0)|sk6=X0|~sQ22_spl)),
% 0.14/0.72 inference(forward_demodulation,[status(thm)],[f956,f1917])).
% 0.14/0.72 fof(f1919,plain,(
% 0.14/0.72 ~sk4=sk6|~ssList(sk6)|~ssList(app(sk5,sk3))|sk6=app(sk5,sk3)|~sQ22_spl),
% 0.14/0.72 inference(paramodulation,[status(thm)],[f441,f1918])).
% 0.14/0.72 fof(f1920,definition,(
% 0.14/0.72 sQ75_spl <=> (sk4=sk6)),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1922,plain,(
% 0.14/0.72 ~sk4=sk6|sQ75_spl),
% 0.14/0.72 inference(component_clause,[status(thm)],[f1920])).
% 0.14/0.72 fof(f1923,definition,(
% 0.14/0.72 sQ76_spl <=> (sk6=app(sk5,sk3))),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f1924,plain,(
% 0.14/0.72 sk6=app(sk5,sk3)|~sQ76_spl),
% 0.14/0.72 inference(component_clause,[status(thm)],[f1923])).
% 0.14/0.72 fof(f1926,plain,(
% 0.14/0.72 ~sQ75_spl|~sQ13_spl|~sQ14_spl|sQ76_spl|~sQ22_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f1919,f1920,f599,f602,f1923,f955])).
% 0.14/0.72 fof(f1952,plain,(
% 0.14/0.72 ~sk6=sk6|~sQ22_spl|~sQ2_spl|sQ75_spl),
% 0.14/0.72 inference(forward_demodulation,[status(thm)],[f1916,f1922])).
% 0.14/0.72 fof(f1953,plain,(
% 0.14/0.72 $false|~sQ22_spl|~sQ2_spl|sQ75_spl),
% 0.14/0.72 inference(trivial_equality_resolution,[status(thm)],[f1952])).
% 0.14/0.72 fof(f1954,plain,(
% 0.14/0.72 ~sQ22_spl|~sQ2_spl|sQ75_spl),
% 0.14/0.72 inference(contradiction_clause,[status(thm)],[f1953])).
% 0.14/0.72 fof(f2003,plain,(
% 0.14/0.72 $false|~sQ22_spl|~sQ23_spl|~sQ67_spl),
% 0.14/0.72 inference(forward_subsumption_resolution,[status(thm)],[f1805,f1238])).
% 0.14/0.72 fof(f2004,plain,(
% 0.14/0.72 ~sQ22_spl|~sQ23_spl|~sQ67_spl),
% 0.14/0.72 inference(contradiction_clause,[status(thm)],[f2003])).
% 0.14/0.72 fof(f2023,plain,(
% 0.14/0.72 app(sk6,nil)=nil|~sQ22_spl|~sQ37_spl),
% 0.14/0.72 inference(forward_demodulation,[status(thm)],[f956,f1270])).
% 0.14/0.72 fof(f2024,plain,(
% 0.14/0.72 app(sk6,sk6)=nil|~sQ22_spl|~sQ37_spl),
% 0.14/0.72 inference(forward_demodulation,[status(thm)],[f956,f2023])).
% 0.14/0.72 fof(f2025,plain,(
% 0.14/0.72 app(sk6,sk6)=sk6|~sQ22_spl|~sQ37_spl),
% 0.14/0.72 inference(forward_demodulation,[status(thm)],[f956,f2024])).
% 0.14/0.72 fof(f2028,plain,(
% 0.14/0.72 ![X0]: (~ssList(X0)|~ssList(sk6)|~ssList(sk6)|~ssList(app(sk6,X0))|segmentP(app(app(sk6,sk6),X0),sk6)|~sQ22_spl|~sQ37_spl)),
% 0.14/0.72 inference(paramodulation,[status(thm)],[f2025,f503])).
% 0.14/0.72 fof(f2029,plain,(
% 0.14/0.72 ![X0,X1]: (~segmentP(sk6,X0)|~ssList(X1)|~ssList(sk6)|~ssList(X0)|~ssList(sk6)|segmentP(app(sk6,X1),X0)|~sQ22_spl|~sQ37_spl)),
% 0.14/0.72 inference(paramodulation,[status(thm)],[f2025,f407])).
% 0.14/0.72 fof(f2030,plain,(
% 0.14/0.72 ![X0]: (~app(X0,sk6)=sk6|~ssList(X0)|~ssList(sk6)|~ssList(sk6)|X0=sk6|~sQ22_spl|~sQ37_spl)),
% 0.14/0.72 inference(paramodulation,[status(thm)],[f2025,f375])).
% 0.14/0.72 fof(f2034,definition,(
% 0.14/0.72 ![X0]: (sQ82_spl <=> (~ssList(X0)|~ssList(app(sk6,X0))|segmentP(app(app(sk6,sk6),X0),sk6)))),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f2037,plain,(
% 0.14/0.72 sQ82_spl|~sQ13_spl|~sQ22_spl|~sQ37_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f2028,f2034,f599,f955,f1269])).
% 0.14/0.72 fof(f2038,definition,(
% 0.14/0.72 ![X0,X1]: (sQ83_spl <=> (~segmentP(sk6,X0)|~ssList(X1)|~ssList(X0)|segmentP(app(sk6,X1),X0)))),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f2041,plain,(
% 0.14/0.72 sQ83_spl|~sQ13_spl|~sQ22_spl|~sQ37_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f2029,f2038,f599,f955,f1269])).
% 0.14/0.72 fof(f2042,definition,(
% 0.14/0.72 ![X0]: (sQ84_spl <=> (~app(X0,sk6)=sk6|~ssList(X0)|X0=sk6))),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f2045,plain,(
% 0.14/0.72 sQ84_spl|~sQ13_spl|~sQ22_spl|~sQ37_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f2030,f2042,f599,f955,f1269])).
% 0.14/0.72 fof(f2112,plain,(
% 0.14/0.72 ![X0]: (~ssList(X0)|frontsegP(X0,sk6)|~sQ22_spl)),
% 0.14/0.72 inference(forward_demodulation,[status(thm)],[f956,f262])).
% 0.14/0.72 fof(f2113,plain,(
% 0.14/0.72 ![X0]: (~ssList(X0)|rearsegP(X0,sk6)|~sQ22_spl)),
% 0.14/0.72 inference(forward_demodulation,[status(thm)],[f956,f260])).
% 0.14/0.72 fof(f2127,plain,(
% 0.14/0.72 ![X0]: (~rearsegP(sk6,X0)|~ssList(sk6)|~ssList(X0)|X0=sk6|~ssList(X0)|~sQ22_spl)),
% 0.14/0.72 inference(resolution,[status(thm)],[f343,f2113])).
% 0.14/0.72 fof(f2129,definition,(
% 0.14/0.72 ![X0]: (sQ86_spl <=> (~rearsegP(sk6,X0)|~ssList(X0)|X0=sk6|~ssList(X0)))),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f2132,plain,(
% 0.14/0.72 sQ86_spl|~sQ13_spl|~sQ22_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f2127,f2129,f599,f955])).
% 0.14/0.72 fof(f2134,plain,(
% 0.14/0.72 ![X0]: (~frontsegP(sk6,X0)|~ssList(sk6)|~ssList(X0)|X0=sk6|~ssList(X0)|~sQ22_spl)),
% 0.14/0.72 inference(resolution,[status(thm)],[f344,f2112])).
% 0.14/0.72 fof(f2136,definition,(
% 0.14/0.72 ![X0]: (sQ87_spl <=> (~frontsegP(sk6,X0)|~ssList(X0)|X0=sk6|~ssList(X0)))),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f2139,plain,(
% 0.14/0.72 sQ87_spl|~sQ13_spl|~sQ22_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f2134,f2136,f599,f955])).
% 0.14/0.72 fof(f2278,plain,(
% 0.14/0.72 ![X0]: (~ssList(sk6)|~ssList(X0)|app(skaf46(X0,sk6),sk6)=X0|~ssList(X0)|~sQ22_spl)),
% 0.14/0.72 inference(resolution,[status(thm)],[f346,f2113])).
% 0.14/0.72 fof(f2280,definition,(
% 0.14/0.72 ![X0]: (sQ101_spl <=> (~ssList(X0)|app(skaf46(X0,sk6),sk6)=X0|~ssList(X0)))),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f2283,plain,(
% 0.14/0.72 ~sQ13_spl|sQ101_spl|~sQ22_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f2278,f599,f2280,f955])).
% 0.14/0.72 fof(f2286,plain,(
% 0.14/0.72 ![X0]: (~ssList(sk6)|~ssList(X0)|app(sk6,skaf45(X0,sk6))=X0|~ssList(X0)|~sQ22_spl)),
% 0.14/0.72 inference(resolution,[status(thm)],[f347,f2112])).
% 0.14/0.72 fof(f2288,definition,(
% 0.14/0.72 ![X0]: (sQ102_spl <=> (~ssList(X0)|app(sk6,skaf45(X0,sk6))=X0|~ssList(X0)))),
% 0.14/0.72 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.14/0.72 fof(f2291,plain,(
% 0.14/0.72 ~sQ13_spl|sQ102_spl|~sQ22_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f2286,f599,f2288,f955])).
% 0.14/0.72 fof(f2385,plain,(
% 0.14/0.72 ~ssList(sk3)|~ssList(sk5)|sk6=sk5|~sQ76_spl|~sQ22_spl),
% 0.14/0.72 inference(resolution,[status(thm)],[f1924,f1918])).
% 0.14/0.72 fof(f2391,plain,(
% 0.14/0.72 ~sQ15_spl|~sQ16_spl|sQ67_spl|~sQ76_spl|~sQ22_spl),
% 0.14/0.72 inference(split_clause,[status(thm)],[f2385,f632,f635,f1804,f1923,f955])).
% 0.14/0.72 fof(f2410,plain,(
% 0.14/0.72 sk6=sk3|~sQ76_spl|~sQ24_spl),
% 0.14/0.72 inference(forward_demodulation,[status(thm)],[f1924,f1173])).
% 0.14/0.72 fof(f2411,plain,(
% 0.14/0.72 $false|~sQ22_spl|sQ3_spl|~sQ76_spl|~sQ24_spl),
% 0.14/0.72 inference(forward_subsumption_resolution,[status(thm)],[f2410,f1245])).
% 0.14/0.72 fof(f2412,plain,(
% 0.14/0.72 ~sQ22_spl|sQ3_spl|~sQ76_spl|~sQ24_spl),
% 0.14/0.72 inference(contradiction_clause,[status(thm)],[f2411])).
% 0.14/0.72 fof(f2413,plain,(
% 0.14/0.72 $false),
% 0.14/0.72 inference(sat_refutation,[status(thm)],[f465,f479,f483,f597,f605,f607,f620,f638,f640,f642,f688,f690,f965,f974,f1228,f1268,f1272,f1274,f1391,f1399,f1433,f1446,f1489,f1496,f1503,f1510,f1517,f1524,f1531,f1538,f1545,f1642,f1747,f1751,f1789,f1796,f1800,f1816,f1820,f1823,f1827,f1872,f1876,f1880,f1886,f1892,f1896,f1926,f1954,f2004,f2037,f2041,f2045,f2132,f2139,f2283,f2291,f2391,f2412])).
% 0.14/0.72 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.73 % Elapsed time: 0.178413 seconds
% 0.14/0.73 % CPU time: 1.156032 seconds
% 0.14/0.73 % Total memory used: 133.000 MB
% 0.14/0.73 % Net memory used: 131.974 MB
%------------------------------------------------------------------------------