%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC067-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:29 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC067-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n003.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 07:54:45 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 0.14/0.57 % Refutation found
% 0.14/0.57 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.57 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.57 fof(f8,axiom,(
% 0.14/0.57 ssList(nil) ),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f13,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf82(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f14,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf81(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f15,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf80(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f18,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf77(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f19,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf76(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f20,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf75(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f22,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf73(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f23,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf72(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f24,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf71(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f27,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf68(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f28,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf67(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f29,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf66(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f32,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf63(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f33,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf62(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f34,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf61(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f37,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf58(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f38,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf57(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f39,axiom,(
% 0.14/0.57 (![U]: (ssList(skaf56(U)) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f56,axiom,(
% 0.14/0.57 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f57,axiom,(
% 0.14/0.57 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f73,axiom,(
% 0.14/0.57 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f74,axiom,(
% 0.14/0.57 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f79,axiom,(
% 0.14/0.57 (![U]: (( nil != U| ~ ssList(U)| segmentP(nil,U) ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f80,axiom,(
% 0.14/0.57 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f85,axiom,(
% 0.14/0.57 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f100,axiom,(
% 0.14/0.57 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f115,axiom,(
% 0.14/0.57 (![U,V]: (( U != V| ~ neq(U,V)| ~ ssList(V)| ~ ssList(U) ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f119,axiom,(
% 0.14/0.57 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = V ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f127,axiom,(
% 0.14/0.57 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f149,axiom,(
% 0.14/0.57 (![U,V,W]: (( ~ ssList(U)| ~ ssList(V)| ~ ssList(W)| app(app(W,V),U) = app(W,app(V,U)) ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f152,axiom,(
% 0.14/0.57 (![U,V,W]: (( ~ segmentP(U,V)| ~ segmentP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| segmentP(U,W) ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f172,axiom,(
% 0.14/0.57 (![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.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f173,axiom,(
% 0.14/0.57 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f186,negated_conjecture,(
% 0.14/0.57 ssList(sk1) ),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f189,negated_conjecture,(
% 0.14/0.57 ssList(sk4) ),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f190,negated_conjecture,(
% 0.14/0.57 sk2 = sk4 ),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f191,negated_conjecture,(
% 0.14/0.57 sk1 = sk3 ),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f192,negated_conjecture,(
% 0.14/0.57 ssList(sk5) ),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f193,negated_conjecture,(
% 0.14/0.57 ssList(sk6) ),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f194,negated_conjecture,(
% 0.14/0.57 app(app(sk5,sk3),sk6) = sk4 ),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f198,negated_conjecture,(
% 0.14/0.57 ( nil = sk4| nil != sk3 ) ),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f199,negated_conjecture,(
% 0.14/0.57 ( nil = sk2| neq(sk2,nil) ) ),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f200,negated_conjecture,(
% 0.14/0.57 (![A]: (( nil = sk2| ~ ssList(A)| ~ neq(A,nil)| ~ segmentP(sk2,A)| ~ segmentP(sk1,A) ) ))),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f201,negated_conjecture,(
% 0.14/0.57 ( nil != sk1| neq(sk2,nil) ) ),
% 0.14/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.57 fof(f210,plain,(
% 0.14/0.57 ssList(nil)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.57 fof(f215,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf82(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/0.57 fof(f216,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf81(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f14])).
% 0.14/0.57 fof(f217,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf80(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f15])).
% 0.14/0.57 fof(f220,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf77(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f18])).
% 0.14/0.57 fof(f221,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf76(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f19])).
% 0.14/0.57 fof(f222,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf75(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f20])).
% 0.14/0.57 fof(f224,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf73(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/0.57 fof(f225,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf72(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f23])).
% 0.14/0.57 fof(f226,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf71(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f24])).
% 0.14/0.57 fof(f229,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf68(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f27])).
% 0.14/0.57 fof(f230,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf67(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f28])).
% 0.14/0.57 fof(f231,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf66(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f29])).
% 0.14/0.57 fof(f234,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf63(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f32])).
% 0.14/0.57 fof(f235,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf62(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f33])).
% 0.14/0.57 fof(f236,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf61(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f34])).
% 0.14/0.57 fof(f239,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf58(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f37])).
% 0.14/0.57 fof(f240,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf57(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f38])).
% 0.14/0.57 fof(f241,plain,(
% 0.14/0.57 ![X0]: (ssList(skaf56(X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f39])).
% 0.14/0.57 fof(f258,plain,(
% 0.14/0.57 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f56])).
% 0.14/0.57 fof(f259,plain,(
% 0.14/0.57 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f57])).
% 0.14/0.57 fof(f276,plain,(
% 0.14/0.57 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/0.57 fof(f277,plain,(
% 0.14/0.57 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f74])).
% 0.14/0.57 fof(f282,plain,(
% 0.14/0.57 ![X0]: (~nil=X0|~ssList(X0)|segmentP(nil,X0))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f79])).
% 0.14/0.57 fof(f283,plain,(
% 0.14/0.57 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f80])).
% 0.14/0.57 fof(f288,plain,(
% 0.14/0.57 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f85])).
% 0.14/0.57 fof(f305,plain,(
% 0.14/0.57 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f100])).
% 0.14/0.57 fof(f323,plain,(
% 0.14/0.57 ![U]: ((![V]: ((~U=V|~neq(U,V))|~ssList(V)))|~ssList(U))),
% 0.14/0.57 inference(miniscoping,[status(thm)],[f115])).
% 0.14/0.57 fof(f324,plain,(
% 0.14/0.57 ![X0,X1]: (~X0=X1|~neq(X0,X1)|~ssList(X1)|~ssList(X0))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f323])).
% 0.14/0.57 fof(f331,plain,(
% 0.14/0.57 ![V]: ((![U]: ((~app(U,V)=nil|~ssList(V))|~ssList(U)))|nil=V)),
% 0.14/0.57 inference(miniscoping,[status(thm)],[f119])).
% 0.14/0.57 fof(f332,plain,(
% 0.14/0.57 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X1)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f331])).
% 0.14/0.57 fof(f342,plain,(
% 0.14/0.57 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f127])).
% 0.14/0.57 fof(f371,plain,(
% 0.14/0.57 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|app(app(X2,X1),X0)=app(X2,app(X1,X0)))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f149])).
% 0.14/0.57 fof(f376,plain,(
% 0.14/0.57 ![U,W]: (((![V]: (((~segmentP(U,V)|~segmentP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|segmentP(U,W))),
% 0.14/0.57 inference(miniscoping,[status(thm)],[f152])).
% 0.14/0.57 fof(f377,plain,(
% 0.14/0.57 ![X0,X1,X2]: (~segmentP(X0,X1)|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|segmentP(X0,X2))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f376])).
% 0.14/0.57 fof(f407,plain,(
% 0.14/0.57 ![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.57 inference(cnf_transformation,[status(thm)],[f172])).
% 0.14/0.57 fof(f408,plain,(
% 0.14/0.57 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 0.14/0.57 inference(miniscoping,[status(thm)],[f173])).
% 0.14/0.57 fof(f409,plain,(
% 0.14/0.57 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f408])).
% 0.14/0.57 fof(f433,plain,(
% 0.14/0.57 ssList(sk1)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f186])).
% 0.14/0.57 fof(f436,plain,(
% 0.14/0.57 ssList(sk4)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f189])).
% 0.14/0.57 fof(f437,plain,(
% 0.14/0.57 sk2=sk4),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f190])).
% 0.14/0.57 fof(f438,plain,(
% 0.14/0.57 sk1=sk3),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f191])).
% 0.14/0.57 fof(f439,plain,(
% 0.14/0.57 ssList(sk5)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f192])).
% 0.14/0.57 fof(f440,plain,(
% 0.14/0.57 ssList(sk6)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f193])).
% 0.14/0.57 fof(f441,plain,(
% 0.14/0.57 app(app(sk5,sk3),sk6)=sk4),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f194])).
% 0.14/0.57 fof(f447,plain,(
% 0.14/0.57 nil=sk4|~nil=sk3),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f198])).
% 0.14/0.57 fof(f448,plain,(
% 0.14/0.57 nil=sk2|neq(sk2,nil)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f199])).
% 0.14/0.57 fof(f449,plain,(
% 0.14/0.57 ![X0]: (nil=sk2|~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f200])).
% 0.14/0.57 fof(f450,plain,(
% 0.14/0.57 ~nil=sk1|neq(sk2,nil)),
% 0.14/0.57 inference(cnf_transformation,[status(thm)],[f201])).
% 0.14/0.57 fof(f459,definition,(
% 0.14/0.57 sQ2_spl <=> (nil=sk4)),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f460,plain,(
% 0.14/0.57 nil=sk4|~sQ2_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f459])).
% 0.14/0.57 fof(f461,plain,(
% 0.14/0.57 ~nil=sk4|sQ2_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f459])).
% 0.14/0.57 fof(f462,definition,(
% 0.14/0.57 sQ3_spl <=> (nil=sk3)),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f464,plain,(
% 0.14/0.57 ~nil=sk3|sQ3_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f462])).
% 0.14/0.57 fof(f465,plain,(
% 0.14/0.57 sQ2_spl|~sQ3_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f447,f459,f462])).
% 0.14/0.57 fof(f466,definition,(
% 0.14/0.57 sQ4_spl <=> (nil=sk2)),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f467,plain,(
% 0.14/0.57 nil=sk2|~sQ4_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f466])).
% 0.14/0.57 fof(f469,definition,(
% 0.14/0.57 sQ5_spl <=> (neq(sk2,nil))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f470,plain,(
% 0.14/0.57 neq(sk2,nil)|~sQ5_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f469])).
% 0.14/0.57 fof(f472,plain,(
% 0.14/0.57 sQ4_spl|sQ5_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f448,f466,f469])).
% 0.14/0.57 fof(f473,definition,(
% 0.14/0.57 ![X0]: (sQ6_spl <=> (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f474,plain,(
% 0.14/0.57 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~sQ6_spl)),
% 0.14/0.57 inference(component_clause,[status(thm)],[f473])).
% 0.14/0.57 fof(f476,plain,(
% 0.14/0.57 sQ4_spl|sQ6_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f449,f466,f473])).
% 0.14/0.57 fof(f477,definition,(
% 0.14/0.57 sQ7_spl <=> (nil=sk1)),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f478,plain,(
% 0.14/0.57 nil=sk1|~sQ7_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f477])).
% 0.14/0.57 fof(f479,plain,(
% 0.14/0.57 ~nil=sk1|sQ7_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f477])).
% 0.14/0.57 fof(f480,plain,(
% 0.14/0.57 ~sQ7_spl|sQ5_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f450,f477,f469])).
% 0.14/0.57 fof(f482,plain,(
% 0.14/0.57 ~ssList(nil)|segmentP(nil,nil)),
% 0.14/0.57 inference(destructive_equality_resolution,[status(thm)],[f282])).
% 0.14/0.57 fof(f489,plain,(
% 0.14/0.57 ![X1]: (~neq(X1,X1)|~ssList(X1)|~ssList(X1))),
% 0.14/0.57 inference(destructive_equality_resolution,[status(thm)],[f324])).
% 0.14/0.57 fof(f490,plain,(
% 0.14/0.57 ![X0]: (~neq(X0,X0)|~ssList(X0))),
% 0.14/0.57 inference(duplicate_literals_removal,[status(thm)],[f489])).
% 0.14/0.57 fof(f500,plain,(
% 0.14/0.57 ![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.57 inference(destructive_equality_resolution,[status(thm)],[f409])).
% 0.14/0.57 fof(f525,plain,(
% 0.14/0.57 nil=sk4|~sQ4_spl),
% 0.14/0.57 inference(forward_demodulation,[status(thm)],[f437,f467])).
% 0.14/0.57 fof(f526,plain,(
% 0.14/0.57 app(app(sk5,sk1),sk6)=sk4),
% 0.14/0.57 inference(forward_demodulation,[status(thm)],[f438,f441])).
% 0.14/0.57 fof(f579,definition,(
% 0.14/0.57 sQ8_spl <=> (ssList(sk4))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f587,plain,(
% 0.14/0.57 neq(sk4,nil)|~sQ5_spl),
% 0.14/0.57 inference(forward_demodulation,[status(thm)],[f437,f470])).
% 0.14/0.57 fof(f588,plain,(
% 0.14/0.57 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk4,X0)|~segmentP(sk1,X0)|~sQ6_spl)),
% 0.14/0.57 inference(forward_demodulation,[status(thm)],[f437,f474])).
% 0.14/0.57 fof(f589,definition,(
% 0.14/0.57 sQ10_spl <=> (ssList(nil))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f591,plain,(
% 0.14/0.57 ~ssList(nil)|sQ10_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f589])).
% 0.14/0.57 fof(f592,definition,(
% 0.14/0.57 sQ11_spl <=> (segmentP(nil,nil))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f593,plain,(
% 0.14/0.57 segmentP(nil,nil)|~sQ11_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f592])).
% 0.14/0.57 fof(f595,plain,(
% 0.14/0.57 ~sQ10_spl|sQ11_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f482,f589,f592])).
% 0.14/0.57 fof(f598,plain,(
% 0.14/0.57 ~ssList(sk6)|~ssList(app(sk5,sk1))|ssList(sk4)),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f526,f288])).
% 0.14/0.57 fof(f599,definition,(
% 0.14/0.57 sQ12_spl <=> (ssList(sk6))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f601,plain,(
% 0.14/0.57 ~ssList(sk6)|sQ12_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f599])).
% 0.14/0.57 fof(f602,definition,(
% 0.14/0.57 sQ13_spl <=> (ssList(app(sk5,sk1)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f603,plain,(
% 0.14/0.57 ssList(app(sk5,sk1))|~sQ13_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f602])).
% 0.14/0.57 fof(f604,plain,(
% 0.14/0.57 ~ssList(app(sk5,sk1))|sQ13_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f602])).
% 0.14/0.57 fof(f605,plain,(
% 0.14/0.57 ~sQ12_spl|~sQ13_spl|sQ8_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f598,f599,f602,f579])).
% 0.14/0.57 fof(f606,plain,(
% 0.14/0.57 $false|sQ12_spl),
% 0.14/0.57 inference(forward_subsumption_resolution,[status(thm)],[f601,f440])).
% 0.14/0.57 fof(f607,plain,(
% 0.14/0.57 sQ12_spl),
% 0.14/0.57 inference(contradiction_clause,[status(thm)],[f606])).
% 0.14/0.57 fof(f616,plain,(
% 0.14/0.57 neq(sk4,sk4)|~sQ2_spl|~sQ5_spl),
% 0.14/0.57 inference(forward_demodulation,[status(thm)],[f460,f587])).
% 0.14/0.57 fof(f618,plain,(
% 0.14/0.57 ~ssList(sk4)|~sQ2_spl|~sQ5_spl),
% 0.14/0.57 inference(resolution,[status(thm)],[f616,f490])).
% 0.14/0.57 fof(f619,plain,(
% 0.14/0.57 $false|~sQ2_spl|~sQ5_spl),
% 0.14/0.57 inference(forward_subsumption_resolution,[status(thm)],[f618,f436])).
% 0.14/0.57 fof(f620,plain,(
% 0.14/0.57 ~sQ2_spl|~sQ5_spl),
% 0.14/0.57 inference(contradiction_clause,[status(thm)],[f619])).
% 0.14/0.57 fof(f621,plain,(
% 0.14/0.57 ~nil=sk1|sQ3_spl),
% 0.14/0.57 inference(forward_demodulation,[status(thm)],[f438,f464])).
% 0.14/0.57 fof(f632,plain,(
% 0.14/0.57 ~ssList(sk1)|~ssList(sk5)|sQ13_spl),
% 0.14/0.57 inference(resolution,[status(thm)],[f604,f288])).
% 0.14/0.57 fof(f633,definition,(
% 0.14/0.57 sQ14_spl <=> (ssList(sk1))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f635,plain,(
% 0.14/0.57 ~ssList(sk1)|sQ14_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f633])).
% 0.14/0.57 fof(f636,definition,(
% 0.14/0.57 sQ15_spl <=> (ssList(sk5))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f638,plain,(
% 0.14/0.57 ~ssList(sk5)|sQ15_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f636])).
% 0.14/0.57 fof(f639,plain,(
% 0.14/0.57 ~sQ14_spl|~sQ15_spl|sQ13_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f632,f633,f636,f602])).
% 0.14/0.57 fof(f640,plain,(
% 0.14/0.57 $false|sQ14_spl),
% 0.14/0.57 inference(forward_subsumption_resolution,[status(thm)],[f635,f433])).
% 0.14/0.57 fof(f641,plain,(
% 0.14/0.57 sQ14_spl),
% 0.14/0.57 inference(contradiction_clause,[status(thm)],[f640])).
% 0.14/0.57 fof(f642,plain,(
% 0.14/0.57 $false|sQ15_spl),
% 0.14/0.57 inference(forward_subsumption_resolution,[status(thm)],[f638,f439])).
% 0.14/0.57 fof(f643,plain,(
% 0.14/0.57 sQ15_spl),
% 0.14/0.57 inference(contradiction_clause,[status(thm)],[f642])).
% 0.14/0.57 fof(f644,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf56(X0))=skaf56(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f241])).
% 0.14/0.57 fof(f645,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf57(X0))=skaf57(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f240])).
% 0.14/0.57 fof(f646,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf58(X0))=skaf58(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f239])).
% 0.14/0.57 fof(f648,plain,(
% 0.14/0.57 app(nil,nil)=nil),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f210])).
% 0.14/0.57 fof(f649,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf61(X0))=skaf61(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f236])).
% 0.14/0.57 fof(f650,plain,(
% 0.14/0.57 app(nil,app(sk5,sk1))=app(sk5,sk1)|~sQ13_spl),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f603])).
% 0.14/0.57 fof(f652,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf62(X0))=skaf62(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f235])).
% 0.14/0.57 fof(f653,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf63(X0))=skaf63(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f234])).
% 0.14/0.57 fof(f654,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf66(X0))=skaf66(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f231])).
% 0.14/0.57 fof(f655,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf67(X0))=skaf67(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f230])).
% 0.14/0.57 fof(f656,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf68(X0))=skaf68(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f229])).
% 0.14/0.57 fof(f657,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf71(X0))=skaf71(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f226])).
% 0.14/0.57 fof(f658,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf72(X0))=skaf72(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f225])).
% 0.14/0.57 fof(f659,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf73(X0))=skaf73(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f224])).
% 0.14/0.57 fof(f660,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf75(X0))=skaf75(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f222])).
% 0.14/0.57 fof(f661,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf76(X0))=skaf76(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f221])).
% 0.14/0.57 fof(f662,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf77(X0))=skaf77(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f220])).
% 0.14/0.57 fof(f663,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf80(X0))=skaf80(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f217])).
% 0.14/0.57 fof(f664,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf81(X0))=skaf81(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f216])).
% 0.14/0.57 fof(f665,plain,(
% 0.14/0.57 ![X0]: (app(nil,skaf82(X0))=skaf82(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f215])).
% 0.14/0.57 fof(f666,plain,(
% 0.14/0.57 app(nil,sk6)=sk6),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f440])).
% 0.14/0.57 fof(f667,plain,(
% 0.14/0.57 app(nil,sk5)=sk5),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f439])).
% 0.14/0.57 fof(f668,plain,(
% 0.14/0.57 app(nil,sk4)=sk4),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f436])).
% 0.14/0.57 fof(f669,plain,(
% 0.14/0.57 app(nil,sk1)=sk1),
% 0.14/0.57 inference(resolution,[status(thm)],[f277,f433])).
% 0.14/0.57 fof(f711,plain,(
% 0.14/0.57 ~ssList(sk1)|~neq(sk1,nil)|~segmentP(sk4,sk1)|~ssList(sk1)|~sQ6_spl),
% 0.14/0.57 inference(resolution,[status(thm)],[f588,f259])).
% 0.14/0.57 fof(f730,definition,(
% 0.14/0.57 sQ21_spl <=> (neq(sk1,nil))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f732,plain,(
% 0.14/0.57 ~neq(sk1,nil)|sQ21_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f730])).
% 0.14/0.57 fof(f733,definition,(
% 0.14/0.57 sQ22_spl <=> (segmentP(sk4,sk1))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f735,plain,(
% 0.14/0.57 ~segmentP(sk4,sk1)|sQ22_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f733])).
% 0.14/0.57 fof(f736,plain,(
% 0.14/0.57 ~sQ14_spl|~sQ21_spl|~sQ22_spl|~sQ6_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f711,f633,f730,f733,f473])).
% 0.14/0.57 fof(f813,plain,(
% 0.14/0.57 ~sk4=sk4|~sQ4_spl|sQ2_spl),
% 0.14/0.57 inference(forward_demodulation,[status(thm)],[f525,f461])).
% 0.14/0.57 fof(f814,plain,(
% 0.14/0.57 $false|~sQ4_spl|sQ2_spl),
% 0.14/0.57 inference(trivial_equality_resolution,[status(thm)],[f813])).
% 0.14/0.57 fof(f815,plain,(
% 0.14/0.57 ~sQ4_spl|sQ2_spl),
% 0.14/0.57 inference(contradiction_clause,[status(thm)],[f814])).
% 0.14/0.57 fof(f818,plain,(
% 0.14/0.57 $false|sQ10_spl),
% 0.14/0.57 inference(forward_subsumption_resolution,[status(thm)],[f591,f210])).
% 0.14/0.57 fof(f819,plain,(
% 0.14/0.57 sQ10_spl),
% 0.14/0.57 inference(contradiction_clause,[status(thm)],[f818])).
% 0.14/0.57 fof(f825,plain,(
% 0.14/0.57 ~sk4=nil|~ssList(sk6)|~ssList(app(sk5,sk1))|nil=sk6),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f526,f332])).
% 0.14/0.57 fof(f826,definition,(
% 0.14/0.57 sQ25_spl <=> (nil=sk6)),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f827,plain,(
% 0.14/0.57 nil=sk6|~sQ25_spl),
% 0.14/0.57 inference(component_clause,[status(thm)],[f826])).
% 0.14/0.57 fof(f829,plain,(
% 0.14/0.57 ~sQ2_spl|~sQ12_spl|~sQ13_spl|sQ25_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f825,f459,f599,f602,f826])).
% 0.14/0.57 fof(f831,plain,(
% 0.14/0.57 ~ssList(nil)|~ssList(sk1)|sk1=nil|sQ21_spl),
% 0.14/0.57 inference(resolution,[status(thm)],[f732,f305])).
% 0.14/0.57 fof(f839,plain,(
% 0.14/0.57 ~sQ10_spl|~sQ14_spl|sQ7_spl|sQ21_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f831,f589,f633,f477,f730])).
% 0.14/0.57 fof(f840,plain,(
% 0.14/0.57 $false|sQ3_spl|~sQ7_spl),
% 0.14/0.57 inference(forward_subsumption_resolution,[status(thm)],[f478,f621])).
% 0.14/0.57 fof(f841,plain,(
% 0.14/0.57 sQ3_spl|~sQ7_spl),
% 0.14/0.57 inference(contradiction_clause,[status(thm)],[f840])).
% 0.14/0.57 fof(f844,definition,(
% 0.14/0.57 sQ28_spl <=> (nil=nil)),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f923,plain,(
% 0.14/0.57 app(app(sk5,sk1),nil)=app(sk5,sk1)|~sQ13_spl),
% 0.14/0.57 inference(resolution,[status(thm)],[f276,f603])).
% 0.14/0.57 fof(f939,plain,(
% 0.14/0.57 app(sk6,nil)=sk6),
% 0.14/0.57 inference(resolution,[status(thm)],[f276,f440])).
% 0.14/0.57 fof(f940,plain,(
% 0.14/0.57 app(sk5,nil)=sk5),
% 0.14/0.57 inference(resolution,[status(thm)],[f276,f439])).
% 0.14/0.57 fof(f941,plain,(
% 0.14/0.57 app(sk4,nil)=sk4),
% 0.14/0.57 inference(resolution,[status(thm)],[f276,f436])).
% 0.14/0.57 fof(f942,plain,(
% 0.14/0.57 app(sk1,nil)=sk1),
% 0.14/0.57 inference(resolution,[status(thm)],[f276,f433])).
% 0.14/0.57 fof(f1027,plain,(
% 0.14/0.57 ~segmentP(nil,nil)|~ssList(nil)|~ssList(nil)|nil=nil|~sQ11_spl),
% 0.14/0.57 inference(resolution,[status(thm)],[f342,f593])).
% 0.14/0.57 fof(f1028,plain,(
% 0.14/0.57 ![X0]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~ssList(X0))),
% 0.14/0.57 inference(resolution,[status(thm)],[f342,f258])).
% 0.14/0.57 fof(f1030,plain,(
% 0.14/0.57 ~sQ11_spl|~sQ10_spl|sQ28_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1027,f592,f589,f844])).
% 0.14/0.57 fof(f1031,definition,(
% 0.14/0.57 ![X0]: (sQ32_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~ssList(X0)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1034,plain,(
% 0.14/0.57 sQ32_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1028,f1031,f589])).
% 0.14/0.57 fof(f1113,plain,(
% 0.14/0.57 ![X0]: (~skaf56(X0)=nil|~ssList(skaf56(X0))|~ssList(nil)|nil=skaf56(X0))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f644,f332])).
% 0.14/0.57 fof(f1115,plain,(
% 0.14/0.57 ![X0]: (~ssList(skaf56(X0))|~ssList(nil)|ssList(skaf56(X0)))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f644,f288])).
% 0.14/0.57 fof(f1116,definition,(
% 0.14/0.57 ![X0]: (sQ34_spl <=> (~skaf56(X0)=nil|~ssList(skaf56(X0))|nil=skaf56(X0)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1119,plain,(
% 0.14/0.57 sQ34_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1113,f1116,f589])).
% 0.14/0.57 fof(f1124,definition,(
% 0.14/0.57 ![X0]: (sQ36_spl <=> (~ssList(skaf56(X0))|ssList(skaf56(X0))))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1127,plain,(
% 0.14/0.57 sQ36_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1115,f1124,f589])).
% 0.14/0.57 fof(f1128,plain,(
% 0.14/0.57 ![X0]: (~skaf57(X0)=nil|~ssList(skaf57(X0))|~ssList(nil)|nil=skaf57(X0))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f645,f332])).
% 0.14/0.57 fof(f1130,plain,(
% 0.14/0.57 ![X0]: (~ssList(skaf57(X0))|~ssList(nil)|ssList(skaf57(X0)))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f645,f288])).
% 0.14/0.57 fof(f1131,definition,(
% 0.14/0.57 ![X0]: (sQ37_spl <=> (~skaf57(X0)=nil|~ssList(skaf57(X0))|nil=skaf57(X0)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1134,plain,(
% 0.14/0.57 sQ37_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1128,f1131,f589])).
% 0.14/0.57 fof(f1139,definition,(
% 0.14/0.57 ![X0]: (sQ39_spl <=> (~ssList(skaf57(X0))|ssList(skaf57(X0))))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1142,plain,(
% 0.14/0.57 sQ39_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1130,f1139,f589])).
% 0.14/0.57 fof(f1143,plain,(
% 0.14/0.57 ![X0]: (~skaf58(X0)=nil|~ssList(skaf58(X0))|~ssList(nil)|nil=skaf58(X0))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f646,f332])).
% 0.14/0.57 fof(f1145,plain,(
% 0.14/0.57 ![X0]: (~ssList(skaf58(X0))|~ssList(nil)|ssList(skaf58(X0)))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f646,f288])).
% 0.14/0.57 fof(f1146,definition,(
% 0.14/0.57 ![X0]: (sQ40_spl <=> (~skaf58(X0)=nil|~ssList(skaf58(X0))|nil=skaf58(X0)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1149,plain,(
% 0.14/0.57 sQ40_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1143,f1146,f589])).
% 0.14/0.57 fof(f1154,definition,(
% 0.14/0.57 ![X0]: (sQ42_spl <=> (~ssList(skaf58(X0))|ssList(skaf58(X0))))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1157,plain,(
% 0.14/0.57 sQ42_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1145,f1154,f589])).
% 0.14/0.57 fof(f1158,plain,(
% 0.14/0.57 ![X0]: (~skaf61(X0)=nil|~ssList(skaf61(X0))|~ssList(nil)|nil=skaf61(X0))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f649,f332])).
% 0.14/0.57 fof(f1160,plain,(
% 0.14/0.57 ![X0]: (~ssList(skaf61(X0))|~ssList(nil)|ssList(skaf61(X0)))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f649,f288])).
% 0.14/0.57 fof(f1161,definition,(
% 0.14/0.57 ![X0]: (sQ43_spl <=> (~skaf61(X0)=nil|~ssList(skaf61(X0))|nil=skaf61(X0)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1164,plain,(
% 0.14/0.57 sQ43_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1158,f1161,f589])).
% 0.14/0.57 fof(f1169,definition,(
% 0.14/0.57 ![X0]: (sQ45_spl <=> (~ssList(skaf61(X0))|ssList(skaf61(X0))))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1172,plain,(
% 0.14/0.57 sQ45_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1160,f1169,f589])).
% 0.14/0.57 fof(f1173,plain,(
% 0.14/0.57 ![X0]: (~skaf62(X0)=nil|~ssList(skaf62(X0))|~ssList(nil)|nil=skaf62(X0))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f652,f332])).
% 0.14/0.57 fof(f1175,plain,(
% 0.14/0.57 ![X0]: (~ssList(skaf62(X0))|~ssList(nil)|ssList(skaf62(X0)))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f652,f288])).
% 0.14/0.57 fof(f1176,definition,(
% 0.14/0.57 ![X0]: (sQ46_spl <=> (~skaf62(X0)=nil|~ssList(skaf62(X0))|nil=skaf62(X0)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1179,plain,(
% 0.14/0.57 sQ46_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1173,f1176,f589])).
% 0.14/0.57 fof(f1184,definition,(
% 0.14/0.57 ![X0]: (sQ48_spl <=> (~ssList(skaf62(X0))|ssList(skaf62(X0))))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1187,plain,(
% 0.14/0.57 sQ48_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1175,f1184,f589])).
% 0.14/0.57 fof(f1252,plain,(
% 0.14/0.57 ![X0]: (~ssList(X0)|app(app(sk6,sk6),X0)=app(sk6,app(sk6,X0)))),
% 0.14/0.57 inference(resolution,[status(thm)],[f371,f440])).
% 0.14/0.57 fof(f1297,plain,(
% 0.14/0.57 ![X0]: (~skaf63(X0)=nil|~ssList(skaf63(X0))|~ssList(nil)|nil=skaf63(X0))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f653,f332])).
% 0.14/0.57 fof(f1299,plain,(
% 0.14/0.57 ![X0]: (~ssList(skaf63(X0))|~ssList(nil)|ssList(skaf63(X0)))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f653,f288])).
% 0.14/0.57 fof(f1300,definition,(
% 0.14/0.57 ![X0]: (sQ49_spl <=> (~skaf63(X0)=nil|~ssList(skaf63(X0))|nil=skaf63(X0)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1303,plain,(
% 0.14/0.57 sQ49_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1297,f1300,f589])).
% 0.14/0.57 fof(f1308,definition,(
% 0.14/0.57 ![X0]: (sQ51_spl <=> (~ssList(skaf63(X0))|ssList(skaf63(X0))))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1311,plain,(
% 0.14/0.57 sQ51_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1299,f1308,f589])).
% 0.14/0.57 fof(f1312,plain,(
% 0.14/0.57 ![X0]: (~skaf66(X0)=nil|~ssList(skaf66(X0))|~ssList(nil)|nil=skaf66(X0))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f654,f332])).
% 0.14/0.57 fof(f1314,plain,(
% 0.14/0.57 ![X0]: (~ssList(skaf66(X0))|~ssList(nil)|ssList(skaf66(X0)))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f654,f288])).
% 0.14/0.57 fof(f1315,definition,(
% 0.14/0.57 ![X0]: (sQ52_spl <=> (~skaf66(X0)=nil|~ssList(skaf66(X0))|nil=skaf66(X0)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1318,plain,(
% 0.14/0.57 sQ52_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1312,f1315,f589])).
% 0.14/0.57 fof(f1323,definition,(
% 0.14/0.57 ![X0]: (sQ54_spl <=> (~ssList(skaf66(X0))|ssList(skaf66(X0))))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1326,plain,(
% 0.14/0.57 sQ54_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1314,f1323,f589])).
% 0.14/0.57 fof(f1327,plain,(
% 0.14/0.57 ![X0]: (~skaf67(X0)=nil|~ssList(skaf67(X0))|~ssList(nil)|nil=skaf67(X0))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f655,f332])).
% 0.14/0.57 fof(f1329,plain,(
% 0.14/0.57 ![X0]: (~ssList(skaf67(X0))|~ssList(nil)|ssList(skaf67(X0)))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f655,f288])).
% 0.14/0.57 fof(f1330,definition,(
% 0.14/0.57 ![X0]: (sQ55_spl <=> (~skaf67(X0)=nil|~ssList(skaf67(X0))|nil=skaf67(X0)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1333,plain,(
% 0.14/0.57 sQ55_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1327,f1330,f589])).
% 0.14/0.57 fof(f1338,definition,(
% 0.14/0.57 ![X0]: (sQ57_spl <=> (~ssList(skaf67(X0))|ssList(skaf67(X0))))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1341,plain,(
% 0.14/0.57 sQ57_spl|~sQ10_spl),
% 0.14/0.57 inference(split_clause,[status(thm)],[f1329,f1338,f589])).
% 0.14/0.57 fof(f1342,plain,(
% 0.14/0.57 ![X0]: (~skaf68(X0)=nil|~ssList(skaf68(X0))|~ssList(nil)|nil=skaf68(X0))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f656,f332])).
% 0.14/0.57 fof(f1344,plain,(
% 0.14/0.57 ![X0]: (~ssList(skaf68(X0))|~ssList(nil)|ssList(skaf68(X0)))),
% 0.14/0.57 inference(paramodulation,[status(thm)],[f656,f288])).
% 0.14/0.57 fof(f1345,definition,(
% 0.14/0.57 ![X0]: (sQ58_spl <=> (~skaf68(X0)=nil|~ssList(skaf68(X0))|nil=skaf68(X0)))),
% 0.14/0.57 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.14/0.57 fof(f1348,plain,(
% 0.14/0.57 sQ58_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1342,f1345,f589])).
% 0.14/0.58 fof(f1353,definition,(
% 0.14/0.58 ![X0]: (sQ60_spl <=> (~ssList(skaf68(X0))|ssList(skaf68(X0))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1356,plain,(
% 0.14/0.58 sQ60_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1344,f1353,f589])).
% 0.14/0.58 fof(f1357,plain,(
% 0.14/0.58 ![X0]: (~skaf71(X0)=nil|~ssList(skaf71(X0))|~ssList(nil)|nil=skaf71(X0))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f657,f332])).
% 0.14/0.58 fof(f1359,plain,(
% 0.14/0.58 ![X0]: (~ssList(skaf71(X0))|~ssList(nil)|ssList(skaf71(X0)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f657,f288])).
% 0.14/0.58 fof(f1360,definition,(
% 0.14/0.58 ![X0]: (sQ61_spl <=> (~skaf71(X0)=nil|~ssList(skaf71(X0))|nil=skaf71(X0)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1363,plain,(
% 0.14/0.58 sQ61_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1357,f1360,f589])).
% 0.14/0.58 fof(f1368,definition,(
% 0.14/0.58 ![X0]: (sQ63_spl <=> (~ssList(skaf71(X0))|ssList(skaf71(X0))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1371,plain,(
% 0.14/0.58 sQ63_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1359,f1368,f589])).
% 0.14/0.58 fof(f1372,plain,(
% 0.14/0.58 ![X0]: (~skaf72(X0)=nil|~ssList(skaf72(X0))|~ssList(nil)|nil=skaf72(X0))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f658,f332])).
% 0.14/0.58 fof(f1374,plain,(
% 0.14/0.58 ![X0]: (~ssList(skaf72(X0))|~ssList(nil)|ssList(skaf72(X0)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f658,f288])).
% 0.14/0.58 fof(f1375,definition,(
% 0.14/0.58 ![X0]: (sQ64_spl <=> (~skaf72(X0)=nil|~ssList(skaf72(X0))|nil=skaf72(X0)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1378,plain,(
% 0.14/0.58 sQ64_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1372,f1375,f589])).
% 0.14/0.58 fof(f1383,definition,(
% 0.14/0.58 ![X0]: (sQ66_spl <=> (~ssList(skaf72(X0))|ssList(skaf72(X0))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1386,plain,(
% 0.14/0.58 sQ66_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1374,f1383,f589])).
% 0.14/0.58 fof(f1387,plain,(
% 0.14/0.58 ![X0]: (~skaf73(X0)=nil|~ssList(skaf73(X0))|~ssList(nil)|nil=skaf73(X0))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f659,f332])).
% 0.14/0.58 fof(f1389,plain,(
% 0.14/0.58 ![X0]: (~ssList(skaf73(X0))|~ssList(nil)|ssList(skaf73(X0)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f659,f288])).
% 0.14/0.58 fof(f1390,definition,(
% 0.14/0.58 ![X0]: (sQ67_spl <=> (~skaf73(X0)=nil|~ssList(skaf73(X0))|nil=skaf73(X0)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1393,plain,(
% 0.14/0.58 sQ67_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1387,f1390,f589])).
% 0.14/0.58 fof(f1398,definition,(
% 0.14/0.58 ![X0]: (sQ69_spl <=> (~ssList(skaf73(X0))|ssList(skaf73(X0))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1401,plain,(
% 0.14/0.58 sQ69_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1389,f1398,f589])).
% 0.14/0.58 fof(f1402,plain,(
% 0.14/0.58 ![X0]: (~skaf75(X0)=nil|~ssList(skaf75(X0))|~ssList(nil)|nil=skaf75(X0))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f660,f332])).
% 0.14/0.58 fof(f1404,plain,(
% 0.14/0.58 ![X0]: (~ssList(skaf75(X0))|~ssList(nil)|ssList(skaf75(X0)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f660,f288])).
% 0.14/0.58 fof(f1405,definition,(
% 0.14/0.58 ![X0]: (sQ70_spl <=> (~skaf75(X0)=nil|~ssList(skaf75(X0))|nil=skaf75(X0)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1408,plain,(
% 0.14/0.58 sQ70_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1402,f1405,f589])).
% 0.14/0.58 fof(f1413,definition,(
% 0.14/0.58 ![X0]: (sQ72_spl <=> (~ssList(skaf75(X0))|ssList(skaf75(X0))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1416,plain,(
% 0.14/0.58 sQ72_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1404,f1413,f589])).
% 0.14/0.58 fof(f1428,plain,(
% 0.14/0.58 app(app(sk6,sk6),nil)=app(sk6,app(sk6,nil))),
% 0.14/0.58 inference(resolution,[status(thm)],[f1252,f210])).
% 0.14/0.58 fof(f1459,plain,(
% 0.14/0.58 app(app(sk6,sk6),sk6)=app(sk6,app(sk6,sk6))),
% 0.14/0.58 inference(resolution,[status(thm)],[f1252,f440])).
% 0.14/0.58 fof(f1463,plain,(
% 0.14/0.58 app(app(sk6,sk6),nil)=app(sk6,sk6)),
% 0.14/0.58 inference(forward_demodulation,[status(thm)],[f939,f1428])).
% 0.14/0.58 fof(f1470,definition,(
% 0.14/0.58 sQ74_spl <=> (ssList(app(sk6,sk6)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1472,plain,(
% 0.14/0.58 ~ssList(app(sk6,sk6))|sQ74_spl),
% 0.14/0.58 inference(component_clause,[status(thm)],[f1470])).
% 0.14/0.58 fof(f1478,plain,(
% 0.14/0.58 ~ssList(sk6)|~ssList(app(sk6,sk6))|ssList(app(sk6,app(sk6,sk6)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f1459,f288])).
% 0.14/0.58 fof(f1484,definition,(
% 0.14/0.58 sQ76_spl <=> (ssList(app(sk6,app(sk6,sk6))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1487,plain,(
% 0.14/0.58 ~sQ12_spl|~sQ74_spl|sQ76_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1478,f599,f1470,f1484])).
% 0.14/0.58 fof(f1526,plain,(
% 0.14/0.58 ~ssList(sk6)|~ssList(sk6)|sQ74_spl),
% 0.14/0.58 inference(resolution,[status(thm)],[f1472,f288])).
% 0.14/0.58 fof(f1527,plain,(
% 0.14/0.58 ~sQ12_spl|sQ74_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1526,f599,f1470])).
% 0.14/0.58 fof(f1540,plain,(
% 0.14/0.58 ![X0]: (~skaf76(X0)=nil|~ssList(skaf76(X0))|~ssList(nil)|nil=skaf76(X0))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f661,f332])).
% 0.14/0.58 fof(f1542,plain,(
% 0.14/0.58 ![X0]: (~ssList(skaf76(X0))|~ssList(nil)|ssList(skaf76(X0)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f661,f288])).
% 0.14/0.58 fof(f1543,definition,(
% 0.14/0.58 ![X0]: (sQ77_spl <=> (~skaf76(X0)=nil|~ssList(skaf76(X0))|nil=skaf76(X0)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1546,plain,(
% 0.14/0.58 sQ77_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1540,f1543,f589])).
% 0.14/0.58 fof(f1551,definition,(
% 0.14/0.58 ![X0]: (sQ79_spl <=> (~ssList(skaf76(X0))|ssList(skaf76(X0))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1554,plain,(
% 0.14/0.58 sQ79_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1542,f1551,f589])).
% 0.14/0.58 fof(f1555,plain,(
% 0.14/0.58 ![X0]: (~skaf77(X0)=nil|~ssList(skaf77(X0))|~ssList(nil)|nil=skaf77(X0))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f662,f332])).
% 0.14/0.58 fof(f1557,plain,(
% 0.14/0.58 ![X0]: (~ssList(skaf77(X0))|~ssList(nil)|ssList(skaf77(X0)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f662,f288])).
% 0.14/0.58 fof(f1558,definition,(
% 0.14/0.58 ![X0]: (sQ80_spl <=> (~skaf77(X0)=nil|~ssList(skaf77(X0))|nil=skaf77(X0)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1561,plain,(
% 0.14/0.58 sQ80_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1555,f1558,f589])).
% 0.14/0.58 fof(f1566,definition,(
% 0.14/0.58 ![X0]: (sQ82_spl <=> (~ssList(skaf77(X0))|ssList(skaf77(X0))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1569,plain,(
% 0.14/0.58 sQ82_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1557,f1566,f589])).
% 0.14/0.58 fof(f1570,plain,(
% 0.14/0.58 ![X0]: (~skaf80(X0)=nil|~ssList(skaf80(X0))|~ssList(nil)|nil=skaf80(X0))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f663,f332])).
% 0.14/0.58 fof(f1572,plain,(
% 0.14/0.58 ![X0]: (~ssList(skaf80(X0))|~ssList(nil)|ssList(skaf80(X0)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f663,f288])).
% 0.14/0.58 fof(f1573,definition,(
% 0.14/0.58 ![X0]: (sQ83_spl <=> (~skaf80(X0)=nil|~ssList(skaf80(X0))|nil=skaf80(X0)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1576,plain,(
% 0.14/0.58 sQ83_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1570,f1573,f589])).
% 0.14/0.58 fof(f1581,definition,(
% 0.14/0.58 ![X0]: (sQ85_spl <=> (~ssList(skaf80(X0))|ssList(skaf80(X0))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1584,plain,(
% 0.14/0.58 sQ85_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1572,f1581,f589])).
% 0.14/0.58 fof(f1734,plain,(
% 0.14/0.58 ![X0]: (~skaf81(X0)=nil|~ssList(skaf81(X0))|~ssList(nil)|nil=skaf81(X0))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f664,f332])).
% 0.14/0.58 fof(f1736,plain,(
% 0.14/0.58 ![X0]: (~ssList(skaf81(X0))|~ssList(nil)|ssList(skaf81(X0)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f664,f288])).
% 0.14/0.58 fof(f1737,definition,(
% 0.14/0.58 ![X0]: (sQ86_spl <=> (~skaf81(X0)=nil|~ssList(skaf81(X0))|nil=skaf81(X0)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1740,plain,(
% 0.14/0.58 sQ86_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1734,f1737,f589])).
% 0.14/0.58 fof(f1745,definition,(
% 0.14/0.58 ![X0]: (sQ88_spl <=> (~ssList(skaf81(X0))|ssList(skaf81(X0))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1748,plain,(
% 0.14/0.58 sQ88_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1736,f1745,f589])).
% 0.14/0.58 fof(f1749,plain,(
% 0.14/0.58 ![X0]: (~skaf82(X0)=nil|~ssList(skaf82(X0))|~ssList(nil)|nil=skaf82(X0))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f665,f332])).
% 0.14/0.58 fof(f1751,plain,(
% 0.14/0.58 ![X0]: (~ssList(skaf82(X0))|~ssList(nil)|ssList(skaf82(X0)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f665,f288])).
% 0.14/0.58 fof(f1752,definition,(
% 0.14/0.58 ![X0]: (sQ89_spl <=> (~skaf82(X0)=nil|~ssList(skaf82(X0))|nil=skaf82(X0)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1755,plain,(
% 0.14/0.58 sQ89_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1749,f1752,f589])).
% 0.14/0.58 fof(f1760,definition,(
% 0.14/0.58 ![X0]: (sQ91_spl <=> (~ssList(skaf82(X0))|ssList(skaf82(X0))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1763,plain,(
% 0.14/0.58 sQ91_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1751,f1760,f589])).
% 0.14/0.58 fof(f1915,plain,(
% 0.14/0.58 ![X0]: (~segmentP(X0,nil)|~ssList(nil)|~ssList(nil)|~ssList(X0)|segmentP(X0,nil)|~sQ11_spl)),
% 0.14/0.58 inference(resolution,[status(thm)],[f377,f593])).
% 0.14/0.58 fof(f1916,plain,(
% 0.14/0.58 ![X0,X1]: (~segmentP(X0,X1)|~ssList(nil)|~ssList(X1)|~ssList(X0)|segmentP(X0,nil)|~ssList(X1))),
% 0.14/0.58 inference(resolution,[status(thm)],[f377,f258])).
% 0.14/0.58 fof(f1918,definition,(
% 0.14/0.58 ![X0]: (sQ92_spl <=> (~segmentP(X0,nil)|~ssList(X0)|segmentP(X0,nil)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1921,plain,(
% 0.14/0.58 sQ92_spl|~sQ10_spl|~sQ11_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1915,f1918,f589,f592])).
% 0.14/0.58 fof(f1922,definition,(
% 0.14/0.58 ![X0,X1]: (sQ93_spl <=> (~segmentP(X0,X1)|~ssList(X1)|~ssList(X0)|segmentP(X0,nil)|~ssList(X1)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f1925,plain,(
% 0.14/0.58 sQ93_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f1916,f1922,f589])).
% 0.14/0.58 fof(f2529,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(nil)|segmentP(app(app(X1,nil),X0),nil)|~sQ11_spl)),
% 0.14/0.58 inference(resolution,[status(thm)],[f407,f593])).
% 0.14/0.58 fof(f2530,plain,(
% 0.14/0.58 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2))),
% 0.14/0.58 inference(resolution,[status(thm)],[f407,f258])).
% 0.14/0.58 fof(f2532,definition,(
% 0.14/0.58 ![X0,X1]: (sQ101_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,nil),X0),nil)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2535,plain,(
% 0.14/0.58 sQ101_spl|~sQ10_spl|~sQ11_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2529,f2532,f589,f592])).
% 0.14/0.58 fof(f2536,definition,(
% 0.14/0.58 ![X0,X1,X2]: (sQ102_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2539,plain,(
% 0.14/0.58 sQ102_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2530,f2536,f589])).
% 0.14/0.58 fof(f2543,plain,(
% 0.14/0.58 ~ssList(sk6)|~ssList(sk6)|~ssList(sk6)|~ssList(app(sk6,app(sk6,sk6)))|segmentP(app(app(sk6,sk6),sk6),sk6)),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f1459,f500])).
% 0.14/0.58 fof(f2544,plain,(
% 0.14/0.58 ~ssList(nil)|~ssList(sk6)|~ssList(sk6)|~ssList(app(sk6,sk6))|segmentP(app(app(sk6,sk6),nil),sk6)),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f1463,f500])).
% 0.14/0.58 fof(f2545,plain,(
% 0.14/0.58 ~ssList(nil)|~ssList(sk5)|~ssList(sk1)|~ssList(app(sk5,sk1))|segmentP(app(app(sk5,sk1),nil),sk1)|~sQ13_spl),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f923,f500])).
% 0.14/0.58 fof(f2546,plain,(
% 0.14/0.58 ~ssList(sk6)|~ssList(sk5)|~ssList(sk1)|~ssList(sk4)|segmentP(app(app(sk5,sk1),sk6),sk1)),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f526,f500])).
% 0.14/0.58 fof(f2547,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(nil)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f942,f500])).
% 0.14/0.58 fof(f2548,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(sk4)|~ssList(nil)|~ssList(app(sk4,X0))|segmentP(app(app(sk4,nil),X0),nil))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f941,f500])).
% 0.14/0.58 fof(f2549,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(sk5)|~ssList(nil)|~ssList(app(sk5,X0))|segmentP(app(app(sk5,nil),X0),nil))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f940,f500])).
% 0.14/0.58 fof(f2550,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(sk6)|~ssList(nil)|~ssList(app(sk6,X0))|segmentP(app(app(sk6,nil),X0),nil))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f939,f500])).
% 0.14/0.58 fof(f2551,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf82(X1))|~ssList(app(skaf82(X1),X0))|segmentP(app(app(nil,skaf82(X1)),X0),skaf82(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f665,f500])).
% 0.14/0.58 fof(f2552,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf81(X1))|~ssList(app(skaf81(X1),X0))|segmentP(app(app(nil,skaf81(X1)),X0),skaf81(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f664,f500])).
% 0.14/0.58 fof(f2553,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf80(X1))|~ssList(app(skaf80(X1),X0))|segmentP(app(app(nil,skaf80(X1)),X0),skaf80(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f663,f500])).
% 0.14/0.58 fof(f2554,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf77(X1))|~ssList(app(skaf77(X1),X0))|segmentP(app(app(nil,skaf77(X1)),X0),skaf77(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f662,f500])).
% 0.14/0.58 fof(f2555,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf76(X1))|~ssList(app(skaf76(X1),X0))|segmentP(app(app(nil,skaf76(X1)),X0),skaf76(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f661,f500])).
% 0.14/0.58 fof(f2556,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf75(X1))|~ssList(app(skaf75(X1),X0))|segmentP(app(app(nil,skaf75(X1)),X0),skaf75(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f660,f500])).
% 0.14/0.58 fof(f2557,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf73(X1))|~ssList(app(skaf73(X1),X0))|segmentP(app(app(nil,skaf73(X1)),X0),skaf73(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f659,f500])).
% 0.14/0.58 fof(f2558,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf72(X1))|~ssList(app(skaf72(X1),X0))|segmentP(app(app(nil,skaf72(X1)),X0),skaf72(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f658,f500])).
% 0.14/0.58 fof(f2559,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf71(X1))|~ssList(app(skaf71(X1),X0))|segmentP(app(app(nil,skaf71(X1)),X0),skaf71(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f657,f500])).
% 0.14/0.58 fof(f2560,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf68(X1))|~ssList(app(skaf68(X1),X0))|segmentP(app(app(nil,skaf68(X1)),X0),skaf68(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f656,f500])).
% 0.14/0.58 fof(f2561,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf67(X1))|~ssList(app(skaf67(X1),X0))|segmentP(app(app(nil,skaf67(X1)),X0),skaf67(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f655,f500])).
% 0.14/0.58 fof(f2562,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf66(X1))|~ssList(app(skaf66(X1),X0))|segmentP(app(app(nil,skaf66(X1)),X0),skaf66(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f654,f500])).
% 0.14/0.58 fof(f2563,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf63(X1))|~ssList(app(skaf63(X1),X0))|segmentP(app(app(nil,skaf63(X1)),X0),skaf63(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f653,f500])).
% 0.14/0.58 fof(f2564,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf62(X1))|~ssList(app(skaf62(X1),X0))|segmentP(app(app(nil,skaf62(X1)),X0),skaf62(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f652,f500])).
% 0.14/0.58 fof(f2565,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf61(X1))|~ssList(app(skaf61(X1),X0))|segmentP(app(app(nil,skaf61(X1)),X0),skaf61(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f649,f500])).
% 0.14/0.58 fof(f2566,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf58(X1))|~ssList(app(skaf58(X1),X0))|segmentP(app(app(nil,skaf58(X1)),X0),skaf58(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f646,f500])).
% 0.14/0.58 fof(f2567,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf57(X1))|~ssList(app(skaf57(X1),X0))|segmentP(app(app(nil,skaf57(X1)),X0),skaf57(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f645,f500])).
% 0.14/0.58 fof(f2568,plain,(
% 0.14/0.58 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf56(X1))|~ssList(app(skaf56(X1),X0))|segmentP(app(app(nil,skaf56(X1)),X0),skaf56(X1)))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f644,f500])).
% 0.14/0.58 fof(f2569,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(app(sk5,sk1))|~ssList(app(app(sk5,sk1),X0))|segmentP(app(app(nil,app(sk5,sk1)),X0),app(sk5,sk1))|~sQ13_spl)),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f650,f500])).
% 0.14/0.58 fof(f2570,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f648,f500])).
% 0.14/0.58 fof(f2571,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk6)|~ssList(app(sk6,X0))|segmentP(app(app(nil,sk6),X0),sk6))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f666,f500])).
% 0.14/0.58 fof(f2572,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk5)|~ssList(app(sk5,X0))|segmentP(app(app(nil,sk5),X0),sk5))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f667,f500])).
% 0.14/0.58 fof(f2573,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk4)|~ssList(app(sk4,X0))|segmentP(app(app(nil,sk4),X0),sk4))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f668,f500])).
% 0.14/0.58 fof(f2574,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f669,f500])).
% 0.14/0.58 fof(f2575,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(app(sk6,sk6))|~ssList(sk6)|~ssList(app(app(sk6,app(sk6,sk6)),X0))|segmentP(app(app(app(sk6,sk6),sk6),X0),sk6))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f1459,f500])).
% 0.14/0.58 fof(f2576,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(app(sk6,sk6))|~ssList(nil)|~ssList(app(app(sk6,sk6),X0))|segmentP(app(app(app(sk6,sk6),nil),X0),nil))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f1463,f500])).
% 0.14/0.58 fof(f2577,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(app(sk5,sk1))|~ssList(nil)|~ssList(app(app(sk5,sk1),X0))|segmentP(app(app(app(sk5,sk1),nil),X0),nil)|~sQ13_spl)),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f923,f500])).
% 0.14/0.58 fof(f2578,plain,(
% 0.14/0.58 ![X0]: (~ssList(X0)|~ssList(app(sk5,sk1))|~ssList(sk6)|~ssList(app(sk4,X0))|segmentP(app(app(app(sk5,sk1),sk6),X0),sk6))),
% 0.14/0.58 inference(paramodulation,[status(thm)],[f526,f500])).
% 0.14/0.58 fof(f2581,definition,(
% 0.14/0.58 sQ103_spl <=> (segmentP(app(app(sk6,sk6),sk6),sk6))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2584,plain,(
% 0.14/0.58 ~sQ12_spl|~sQ76_spl|sQ103_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2543,f599,f1484,f2581])).
% 0.14/0.58 fof(f2585,definition,(
% 0.14/0.58 sQ104_spl <=> (segmentP(app(app(sk6,sk6),nil),sk6))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2588,plain,(
% 0.14/0.58 ~sQ10_spl|~sQ12_spl|~sQ74_spl|sQ104_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2544,f589,f599,f1470,f2585])).
% 0.14/0.58 fof(f2589,definition,(
% 0.14/0.58 sQ105_spl <=> (segmentP(app(app(sk5,sk1),nil),sk1))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2592,plain,(
% 0.14/0.58 ~sQ10_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|sQ105_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2545,f589,f636,f633,f602,f2589])).
% 0.14/0.58 fof(f2593,definition,(
% 0.14/0.58 sQ106_spl <=> (segmentP(app(app(sk5,sk1),sk6),sk1))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2594,plain,(
% 0.14/0.58 segmentP(app(app(sk5,sk1),sk6),sk1)|~sQ106_spl),
% 0.14/0.58 inference(component_clause,[status(thm)],[f2593])).
% 0.14/0.58 fof(f2596,plain,(
% 0.14/0.58 ~sQ12_spl|~sQ15_spl|~sQ14_spl|~sQ8_spl|sQ106_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2546,f599,f636,f633,f579,f2593])).
% 0.14/0.58 fof(f2597,definition,(
% 0.14/0.58 ![X0]: (sQ107_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2600,plain,(
% 0.14/0.58 sQ107_spl|~sQ14_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2547,f2597,f633,f589])).
% 0.14/0.58 fof(f2601,definition,(
% 0.14/0.58 ![X0]: (sQ108_spl <=> (~ssList(X0)|~ssList(app(sk4,X0))|segmentP(app(app(sk4,nil),X0),nil)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2604,plain,(
% 0.14/0.58 sQ108_spl|~sQ8_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2548,f2601,f579,f589])).
% 0.14/0.58 fof(f2605,definition,(
% 0.14/0.58 ![X0]: (sQ109_spl <=> (~ssList(X0)|~ssList(app(sk5,X0))|segmentP(app(app(sk5,nil),X0),nil)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2608,plain,(
% 0.14/0.58 sQ109_spl|~sQ15_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2549,f2605,f636,f589])).
% 0.14/0.58 fof(f2609,definition,(
% 0.14/0.58 ![X0]: (sQ110_spl <=> (~ssList(X0)|~ssList(app(sk6,X0))|segmentP(app(app(sk6,nil),X0),nil)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2612,plain,(
% 0.14/0.58 sQ110_spl|~sQ12_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2550,f2609,f599,f589])).
% 0.14/0.58 fof(f2613,definition,(
% 0.14/0.58 ![X0,X1]: (sQ111_spl <=> (~ssList(X0)|~ssList(skaf82(X1))|~ssList(app(skaf82(X1),X0))|segmentP(app(app(nil,skaf82(X1)),X0),skaf82(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2616,plain,(
% 0.14/0.58 sQ111_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2551,f2613,f589])).
% 0.14/0.58 fof(f2617,definition,(
% 0.14/0.58 ![X0,X1]: (sQ112_spl <=> (~ssList(X0)|~ssList(skaf81(X1))|~ssList(app(skaf81(X1),X0))|segmentP(app(app(nil,skaf81(X1)),X0),skaf81(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2620,plain,(
% 0.14/0.58 sQ112_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2552,f2617,f589])).
% 0.14/0.58 fof(f2621,definition,(
% 0.14/0.58 ![X0,X1]: (sQ113_spl <=> (~ssList(X0)|~ssList(skaf80(X1))|~ssList(app(skaf80(X1),X0))|segmentP(app(app(nil,skaf80(X1)),X0),skaf80(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2624,plain,(
% 0.14/0.58 sQ113_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2553,f2621,f589])).
% 0.14/0.58 fof(f2625,definition,(
% 0.14/0.58 ![X0,X1]: (sQ114_spl <=> (~ssList(X0)|~ssList(skaf77(X1))|~ssList(app(skaf77(X1),X0))|segmentP(app(app(nil,skaf77(X1)),X0),skaf77(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2628,plain,(
% 0.14/0.58 sQ114_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2554,f2625,f589])).
% 0.14/0.58 fof(f2629,definition,(
% 0.14/0.58 ![X0,X1]: (sQ115_spl <=> (~ssList(X0)|~ssList(skaf76(X1))|~ssList(app(skaf76(X1),X0))|segmentP(app(app(nil,skaf76(X1)),X0),skaf76(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2632,plain,(
% 0.14/0.58 sQ115_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2555,f2629,f589])).
% 0.14/0.58 fof(f2633,definition,(
% 0.14/0.58 ![X0,X1]: (sQ116_spl <=> (~ssList(X0)|~ssList(skaf75(X1))|~ssList(app(skaf75(X1),X0))|segmentP(app(app(nil,skaf75(X1)),X0),skaf75(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2636,plain,(
% 0.14/0.58 sQ116_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2556,f2633,f589])).
% 0.14/0.58 fof(f2637,definition,(
% 0.14/0.58 ![X0,X1]: (sQ117_spl <=> (~ssList(X0)|~ssList(skaf73(X1))|~ssList(app(skaf73(X1),X0))|segmentP(app(app(nil,skaf73(X1)),X0),skaf73(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2640,plain,(
% 0.14/0.58 sQ117_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2557,f2637,f589])).
% 0.14/0.58 fof(f2641,definition,(
% 0.14/0.58 ![X0,X1]: (sQ118_spl <=> (~ssList(X0)|~ssList(skaf72(X1))|~ssList(app(skaf72(X1),X0))|segmentP(app(app(nil,skaf72(X1)),X0),skaf72(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2644,plain,(
% 0.14/0.58 sQ118_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2558,f2641,f589])).
% 0.14/0.58 fof(f2645,definition,(
% 0.14/0.58 ![X0,X1]: (sQ119_spl <=> (~ssList(X0)|~ssList(skaf71(X1))|~ssList(app(skaf71(X1),X0))|segmentP(app(app(nil,skaf71(X1)),X0),skaf71(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2648,plain,(
% 0.14/0.58 sQ119_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2559,f2645,f589])).
% 0.14/0.58 fof(f2649,definition,(
% 0.14/0.58 ![X0,X1]: (sQ120_spl <=> (~ssList(X0)|~ssList(skaf68(X1))|~ssList(app(skaf68(X1),X0))|segmentP(app(app(nil,skaf68(X1)),X0),skaf68(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2652,plain,(
% 0.14/0.58 sQ120_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2560,f2649,f589])).
% 0.14/0.58 fof(f2653,definition,(
% 0.14/0.58 ![X0,X1]: (sQ121_spl <=> (~ssList(X0)|~ssList(skaf67(X1))|~ssList(app(skaf67(X1),X0))|segmentP(app(app(nil,skaf67(X1)),X0),skaf67(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2656,plain,(
% 0.14/0.58 sQ121_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2561,f2653,f589])).
% 0.14/0.58 fof(f2657,definition,(
% 0.14/0.58 ![X0,X1]: (sQ122_spl <=> (~ssList(X0)|~ssList(skaf66(X1))|~ssList(app(skaf66(X1),X0))|segmentP(app(app(nil,skaf66(X1)),X0),skaf66(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2660,plain,(
% 0.14/0.58 sQ122_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2562,f2657,f589])).
% 0.14/0.58 fof(f2661,definition,(
% 0.14/0.58 ![X0,X1]: (sQ123_spl <=> (~ssList(X0)|~ssList(skaf63(X1))|~ssList(app(skaf63(X1),X0))|segmentP(app(app(nil,skaf63(X1)),X0),skaf63(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2664,plain,(
% 0.14/0.58 sQ123_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2563,f2661,f589])).
% 0.14/0.58 fof(f2665,definition,(
% 0.14/0.58 ![X0,X1]: (sQ124_spl <=> (~ssList(X0)|~ssList(skaf62(X1))|~ssList(app(skaf62(X1),X0))|segmentP(app(app(nil,skaf62(X1)),X0),skaf62(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2668,plain,(
% 0.14/0.58 sQ124_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2564,f2665,f589])).
% 0.14/0.58 fof(f2669,definition,(
% 0.14/0.58 ![X0,X1]: (sQ125_spl <=> (~ssList(X0)|~ssList(skaf61(X1))|~ssList(app(skaf61(X1),X0))|segmentP(app(app(nil,skaf61(X1)),X0),skaf61(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2672,plain,(
% 0.14/0.58 sQ125_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2565,f2669,f589])).
% 0.14/0.58 fof(f2673,definition,(
% 0.14/0.58 ![X0,X1]: (sQ126_spl <=> (~ssList(X0)|~ssList(skaf58(X1))|~ssList(app(skaf58(X1),X0))|segmentP(app(app(nil,skaf58(X1)),X0),skaf58(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2676,plain,(
% 0.14/0.58 sQ126_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2566,f2673,f589])).
% 0.14/0.58 fof(f2677,definition,(
% 0.14/0.58 ![X0,X1]: (sQ127_spl <=> (~ssList(X0)|~ssList(skaf57(X1))|~ssList(app(skaf57(X1),X0))|segmentP(app(app(nil,skaf57(X1)),X0),skaf57(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2680,plain,(
% 0.14/0.58 sQ127_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2567,f2677,f589])).
% 0.14/0.58 fof(f2681,definition,(
% 0.14/0.58 ![X0,X1]: (sQ128_spl <=> (~ssList(X0)|~ssList(skaf56(X1))|~ssList(app(skaf56(X1),X0))|segmentP(app(app(nil,skaf56(X1)),X0),skaf56(X1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2684,plain,(
% 0.14/0.58 sQ128_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2568,f2681,f589])).
% 0.14/0.58 fof(f2685,definition,(
% 0.14/0.58 ![X0]: (sQ129_spl <=> (~ssList(X0)|~ssList(app(app(sk5,sk1),X0))|segmentP(app(app(nil,app(sk5,sk1)),X0),app(sk5,sk1))))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2688,plain,(
% 0.14/0.58 sQ129_spl|~sQ10_spl|~sQ13_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2569,f2685,f589,f602])).
% 0.14/0.58 fof(f2689,definition,(
% 0.14/0.58 ![X0]: (sQ130_spl <=> (~ssList(X0)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2692,plain,(
% 0.14/0.58 sQ130_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2570,f2689,f589])).
% 0.14/0.58 fof(f2693,definition,(
% 0.14/0.58 ![X0]: (sQ131_spl <=> (~ssList(X0)|~ssList(app(sk6,X0))|segmentP(app(app(nil,sk6),X0),sk6)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2696,plain,(
% 0.14/0.58 sQ131_spl|~sQ10_spl|~sQ12_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2571,f2693,f589,f599])).
% 0.14/0.58 fof(f2697,definition,(
% 0.14/0.58 ![X0]: (sQ132_spl <=> (~ssList(X0)|~ssList(app(sk5,X0))|segmentP(app(app(nil,sk5),X0),sk5)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2700,plain,(
% 0.14/0.58 sQ132_spl|~sQ10_spl|~sQ15_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2572,f2697,f589,f636])).
% 0.14/0.58 fof(f2701,definition,(
% 0.14/0.58 ![X0]: (sQ133_spl <=> (~ssList(X0)|~ssList(app(sk4,X0))|segmentP(app(app(nil,sk4),X0),sk4)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2704,plain,(
% 0.14/0.58 sQ133_spl|~sQ10_spl|~sQ8_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2573,f2701,f589,f579])).
% 0.14/0.58 fof(f2705,definition,(
% 0.14/0.58 ![X0]: (sQ134_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2708,plain,(
% 0.14/0.58 sQ134_spl|~sQ10_spl|~sQ14_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2574,f2705,f589,f633])).
% 0.14/0.58 fof(f2709,definition,(
% 0.14/0.58 ![X0]: (sQ135_spl <=> (~ssList(X0)|~ssList(app(app(sk6,app(sk6,sk6)),X0))|segmentP(app(app(app(sk6,sk6),sk6),X0),sk6)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2712,plain,(
% 0.14/0.58 sQ135_spl|~sQ74_spl|~sQ12_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2575,f2709,f1470,f599])).
% 0.14/0.58 fof(f2713,definition,(
% 0.14/0.58 ![X0]: (sQ136_spl <=> (~ssList(X0)|~ssList(app(app(sk6,sk6),X0))|segmentP(app(app(app(sk6,sk6),nil),X0),nil)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2716,plain,(
% 0.14/0.58 sQ136_spl|~sQ74_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2576,f2713,f1470,f589])).
% 0.14/0.58 fof(f2717,definition,(
% 0.14/0.58 ![X0]: (sQ137_spl <=> (~ssList(X0)|~ssList(app(app(sk5,sk1),X0))|segmentP(app(app(app(sk5,sk1),nil),X0),nil)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2720,plain,(
% 0.14/0.58 sQ137_spl|~sQ13_spl|~sQ10_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2577,f2717,f602,f589])).
% 0.14/0.58 fof(f2721,definition,(
% 0.14/0.58 ![X0]: (sQ138_spl <=> (~ssList(X0)|~ssList(app(sk4,X0))|segmentP(app(app(app(sk5,sk1),sk6),X0),sk6)))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f2724,plain,(
% 0.14/0.58 sQ138_spl|~sQ13_spl|~sQ12_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f2578,f2721,f602,f599])).
% 0.14/0.58 fof(f2731,plain,(
% 0.14/0.58 segmentP(sk4,sk1)|~sQ106_spl),
% 0.14/0.58 inference(forward_demodulation,[status(thm)],[f526,f2594])).
% 0.14/0.58 fof(f2732,plain,(
% 0.14/0.58 $false|sQ22_spl|~sQ106_spl),
% 0.14/0.58 inference(forward_subsumption_resolution,[status(thm)],[f2731,f735])).
% 0.14/0.58 fof(f2733,plain,(
% 0.14/0.58 sQ22_spl|~sQ106_spl),
% 0.14/0.58 inference(contradiction_clause,[status(thm)],[f2732])).
% 0.14/0.58 fof(f2903,plain,(
% 0.14/0.58 sk6=sk4|~sQ25_spl|~sQ4_spl),
% 0.14/0.58 inference(backward_demodulation,[status(thm)],[f827,f525])).
% 0.14/0.58 fof(f2904,plain,(
% 0.14/0.58 ![X0]: (~segmentP(sk6,X0)|~ssList(X0)|nil=X0|~sQ25_spl)),
% 0.14/0.58 inference(forward_demodulation,[status(thm)],[f827,f283])).
% 0.14/0.58 fof(f2905,plain,(
% 0.14/0.58 ![X0]: (~segmentP(sk6,X0)|~ssList(X0)|sk6=X0|~sQ25_spl)),
% 0.14/0.58 inference(forward_demodulation,[status(thm)],[f827,f2904])).
% 0.14/0.58 fof(f2911,plain,(
% 0.14/0.58 ~sk6=sk1|~sQ25_spl|sQ7_spl),
% 0.14/0.58 inference(forward_demodulation,[status(thm)],[f827,f479])).
% 0.14/0.58 fof(f3027,definition,(
% 0.14/0.58 sQ151_spl <=> (sk6=sk1)),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f3028,plain,(
% 0.14/0.58 sk6=sk1|~sQ151_spl),
% 0.14/0.58 inference(component_clause,[status(thm)],[f3027])).
% 0.14/0.58 fof(f3032,plain,(
% 0.14/0.58 segmentP(sk6,sk1)|~sQ25_spl|~sQ4_spl|~sQ106_spl),
% 0.14/0.58 inference(forward_demodulation,[status(thm)],[f2903,f2731])).
% 0.14/0.58 fof(f3033,plain,(
% 0.14/0.58 ~ssList(sk1)|sk6=sk1|~sQ4_spl|~sQ106_spl|~sQ25_spl),
% 0.14/0.58 inference(resolution,[status(thm)],[f3032,f2905])).
% 0.14/0.58 fof(f3037,plain,(
% 0.14/0.58 ~sQ14_spl|sQ151_spl|~sQ4_spl|~sQ106_spl|~sQ25_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f3033,f633,f3027,f466,f2593,f826])).
% 0.14/0.58 fof(f3050,plain,(
% 0.14/0.58 $false|~sQ25_spl|sQ7_spl|~sQ151_spl),
% 0.14/0.58 inference(forward_subsumption_resolution,[status(thm)],[f3028,f2911])).
% 0.14/0.58 fof(f3051,plain,(
% 0.14/0.58 ~sQ25_spl|sQ7_spl|~sQ151_spl),
% 0.14/0.58 inference(contradiction_clause,[status(thm)],[f3050])).
% 0.14/0.58 fof(f3052,plain,(
% 0.14/0.58 $false),
% 0.14/0.58 inference(sat_refutation,[status(thm)],[f465,f472,f476,f480,f595,f605,f607,f620,f639,f641,f643,f736,f815,f819,f829,f839,f841,f1030,f1034,f1119,f1127,f1134,f1142,f1149,f1157,f1164,f1172,f1179,f1187,f1303,f1311,f1318,f1326,f1333,f1341,f1348,f1356,f1363,f1371,f1378,f1386,f1393,f1401,f1408,f1416,f1487,f1527,f1546,f1554,f1561,f1569,f1576,f1584,f1740,f1748,f1755,f1763,f1921,f1925,f2535,f2539,f2584,f2588,f2592,f2596,f2600,f2604,f2608,f2612,f2616,f2620,f2624,f2628,f2632,f2636,f2640,f2644,f2648,f2652,f2656,f2660,f2664,f2668,f2672,f2676,f2680,f2684,f2688,f2692,f2696,f2700,f2704,f2708,f2712,f2716,f2720,f2724,f2733,f3037,f3051])).
% 0.14/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.74/0.59 % Elapsed time: 0.215041 seconds
% 0.74/0.59 % CPU time: 1.372485 seconds
% 0.74/0.59 % Total memory used: 132.598 MB
% 0.74/0.59 % Net memory used: 131.520 MB
%------------------------------------------------------------------------------