%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC108-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 : n026.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:36 PM UTC 2026
% Result : Unsatisfiable 6.99s 1.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC108-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n026.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 07:58:37 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 6.99/1.42 % Refutation found
% 6.99/1.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.99/1.42 % SZS output start CNFRefutation for theBenchmark
% 6.99/1.42 fof(f8,axiom,(
% 6.99/1.42 ssList(nil) ),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f50,axiom,(
% 6.99/1.42 (![U,V]: (ssList(skaf46(U,V)) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f51,axiom,(
% 6.99/1.42 (![U,V]: (ssList(skaf45(U,V)) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f56,axiom,(
% 6.99/1.42 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f57,axiom,(
% 6.99/1.42 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f58,axiom,(
% 6.99/1.42 (![U]: (( ~ ssList(U)| rearsegP(U,nil) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f60,axiom,(
% 6.99/1.42 (![U]: (( ~ ssList(U)| frontsegP(U,nil) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f61,axiom,(
% 6.99/1.42 (![U]: (( ~ ssList(U)| frontsegP(U,U) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f73,axiom,(
% 6.99/1.42 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f74,axiom,(
% 6.99/1.42 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f80,axiom,(
% 6.99/1.42 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f82,axiom,(
% 6.99/1.42 (![U]: (( ~ rearsegP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f85,axiom,(
% 6.99/1.42 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f100,axiom,(
% 6.99/1.42 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f115,axiom,(
% 6.99/1.42 (![U,V]: (( U != V| ~ neq(U,V)| ~ ssList(V)| ~ ssList(U) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f127,axiom,(
% 6.99/1.42 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f128,axiom,(
% 6.99/1.42 (![U,V]: (( ~ rearsegP(U,V)| ~ rearsegP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f129,axiom,(
% 6.99/1.42 (![U,V]: (( ~ frontsegP(U,V)| ~ frontsegP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f131,axiom,(
% 6.99/1.42 (![U,V]: (( ~ rearsegP(U,V)| ~ ssList(V)| ~ ssList(U)| app(skaf46(U,V),V) = U ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f132,axiom,(
% 6.99/1.42 (![U,V]: (( ~ frontsegP(U,V)| ~ ssList(V)| ~ ssList(U)| app(V,skaf45(U,V)) = U ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f136,axiom,(
% 6.99/1.42 (![U,V,W]: (( ~ rearsegP(U,V)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| rearsegP(app(W,U),V) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f143,axiom,(
% 6.99/1.42 (![U,V,W]: (( app(U,V) != W| ~ ssList(U)| ~ ssList(V)| ~ ssList(W)| rearsegP(W,V) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f152,axiom,(
% 6.99/1.42 (![U,V,W]: (( ~ segmentP(U,V)| ~ segmentP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| segmentP(U,W) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f153,axiom,(
% 6.99/1.42 (![U,V,W]: (( ~ rearsegP(U,V)| ~ rearsegP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| rearsegP(U,W) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f172,axiom,(
% 6.99/1.42 (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f173,axiom,(
% 6.99/1.42 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f186,negated_conjecture,(
% 6.99/1.42 ssList(sk1) ),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f187,negated_conjecture,(
% 6.99/1.42 ssList(sk2) ),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f190,negated_conjecture,(
% 6.99/1.42 sk2 = sk4 ),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f191,negated_conjecture,(
% 6.99/1.42 sk1 = sk3 ),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f192,negated_conjecture,(
% 6.99/1.42 ( nil = sk2| neq(sk2,nil) ) ),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f193,negated_conjecture,(
% 6.99/1.42 ( nil = sk2| ~ neq(sk1,nil)| ~ segmentP(sk2,sk1) ) ),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f194,negated_conjecture,(
% 6.99/1.42 ( nil != sk1| neq(sk2,nil) ) ),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f196,negated_conjecture,(
% 6.99/1.42 ( nil = sk4| neq(sk3,nil) ) ),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f199,negated_conjecture,(
% 6.99/1.42 ( nil = sk3| rearsegP(sk4,sk3) ) ),
% 6.99/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.99/1.42 fof(f207,plain,(
% 6.99/1.42 ssList(nil)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f8])).
% 6.99/1.42 fof(f249,plain,(
% 6.99/1.42 ![X0,X1]: (ssList(skaf46(X0,X1)))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f50])).
% 6.99/1.42 fof(f250,plain,(
% 6.99/1.42 ![X0,X1]: (ssList(skaf45(X0,X1)))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f51])).
% 6.99/1.42 fof(f255,plain,(
% 6.99/1.42 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f56])).
% 6.99/1.42 fof(f256,plain,(
% 6.99/1.42 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f57])).
% 6.99/1.42 fof(f257,plain,(
% 6.99/1.42 ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f58])).
% 6.99/1.42 fof(f259,plain,(
% 6.99/1.42 ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f60])).
% 6.99/1.42 fof(f260,plain,(
% 6.99/1.42 ![X0]: (~ssList(X0)|frontsegP(X0,X0))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f61])).
% 6.99/1.42 fof(f273,plain,(
% 6.99/1.42 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f73])).
% 6.99/1.42 fof(f274,plain,(
% 6.99/1.42 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f74])).
% 6.99/1.42 fof(f280,plain,(
% 6.99/1.42 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f80])).
% 6.99/1.42 fof(f282,plain,(
% 6.99/1.42 ![X0]: (~rearsegP(nil,X0)|~ssList(X0)|nil=X0)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f82])).
% 6.99/1.42 fof(f285,plain,(
% 6.99/1.42 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f85])).
% 6.99/1.42 fof(f302,plain,(
% 6.99/1.42 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f100])).
% 6.99/1.42 fof(f320,plain,(
% 6.99/1.42 ![U]: ((![V]: ((~U=V|~neq(U,V))|~ssList(V)))|~ssList(U))),
% 6.99/1.42 inference(miniscoping,[status(thm)],[f115])).
% 6.99/1.42 fof(f321,plain,(
% 6.99/1.42 ![X0,X1]: (~X0=X1|~neq(X0,X1)|~ssList(X1)|~ssList(X0))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f320])).
% 6.99/1.42 fof(f339,plain,(
% 6.99/1.42 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f127])).
% 6.99/1.42 fof(f340,plain,(
% 6.99/1.42 ![X0,X1]: (~rearsegP(X0,X1)|~rearsegP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f128])).
% 6.99/1.42 fof(f341,plain,(
% 6.99/1.42 ![X0,X1]: (~frontsegP(X0,X1)|~frontsegP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f129])).
% 6.99/1.42 fof(f343,plain,(
% 6.99/1.42 ![X0,X1]: (~rearsegP(X0,X1)|~ssList(X1)|~ssList(X0)|app(skaf46(X0,X1),X1)=X0)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f131])).
% 6.99/1.42 fof(f344,plain,(
% 6.99/1.42 ![X0,X1]: (~frontsegP(X0,X1)|~ssList(X1)|~ssList(X0)|app(X1,skaf45(X0,X1))=X0)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f132])).
% 6.99/1.42 fof(f350,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~rearsegP(X0,X1)|~ssList(X2)|~ssList(X1)|~ssList(X0)|rearsegP(app(X2,X0),X1))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f136])).
% 6.99/1.42 fof(f357,plain,(
% 6.99/1.42 ![V,W]: ((((![U]: (~app(U,V)=W|~ssList(U)))|~ssList(V))|~ssList(W))|rearsegP(W,V))),
% 6.99/1.42 inference(miniscoping,[status(thm)],[f143])).
% 6.99/1.42 fof(f358,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~app(X0,X1)=X2|~ssList(X0)|~ssList(X1)|~ssList(X2)|rearsegP(X2,X1))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f357])).
% 6.99/1.42 fof(f373,plain,(
% 6.99/1.42 ![U,W]: (((![V]: (((~segmentP(U,V)|~segmentP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|segmentP(U,W))),
% 6.99/1.42 inference(miniscoping,[status(thm)],[f152])).
% 6.99/1.42 fof(f374,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~segmentP(X0,X1)|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|segmentP(X0,X2))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f373])).
% 6.99/1.42 fof(f375,plain,(
% 6.99/1.42 ![U,W]: (((![V]: (((~rearsegP(U,V)|~rearsegP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|rearsegP(U,W))),
% 6.99/1.42 inference(miniscoping,[status(thm)],[f153])).
% 6.99/1.42 fof(f376,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~rearsegP(X0,X1)|~rearsegP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|rearsegP(X0,X2))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f375])).
% 6.99/1.42 fof(f404,plain,(
% 6.99/1.42 ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f172])).
% 6.99/1.42 fof(f405,plain,(
% 6.99/1.42 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 6.99/1.42 inference(miniscoping,[status(thm)],[f173])).
% 6.99/1.42 fof(f406,plain,(
% 6.99/1.42 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f405])).
% 6.99/1.42 fof(f430,plain,(
% 6.99/1.42 ssList(sk1)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f186])).
% 6.99/1.42 fof(f431,plain,(
% 6.99/1.42 ssList(sk2)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f187])).
% 6.99/1.42 fof(f434,plain,(
% 6.99/1.42 sk2=sk4),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f190])).
% 6.99/1.42 fof(f435,plain,(
% 6.99/1.42 sk1=sk3),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f191])).
% 6.99/1.42 fof(f436,plain,(
% 6.99/1.42 nil=sk2|neq(sk2,nil)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f192])).
% 6.99/1.42 fof(f437,plain,(
% 6.99/1.42 nil=sk2|~neq(sk1,nil)|~segmentP(sk2,sk1)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f193])).
% 6.99/1.42 fof(f438,plain,(
% 6.99/1.42 ~nil=sk1|neq(sk2,nil)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f194])).
% 6.99/1.42 fof(f440,plain,(
% 6.99/1.42 nil=sk4|neq(sk3,nil)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f196])).
% 6.99/1.42 fof(f443,plain,(
% 6.99/1.42 nil=sk3|rearsegP(sk4,sk3)),
% 6.99/1.42 inference(cnf_transformation,[status(thm)],[f199])).
% 6.99/1.42 fof(f451,definition,(
% 6.99/1.42 sQ2_spl <=> (nil=sk2)),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f452,plain,(
% 6.99/1.42 nil=sk2|~sQ2_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f451])).
% 6.99/1.42 fof(f454,definition,(
% 6.99/1.42 sQ3_spl <=> (neq(sk2,nil))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f455,plain,(
% 6.99/1.42 neq(sk2,nil)|~sQ3_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f454])).
% 6.99/1.42 fof(f457,plain,(
% 6.99/1.42 sQ2_spl|sQ3_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f436,f451,f454])).
% 6.99/1.42 fof(f458,definition,(
% 6.99/1.42 sQ4_spl <=> (neq(sk1,nil))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f460,plain,(
% 6.99/1.42 ~neq(sk1,nil)|sQ4_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f458])).
% 6.99/1.42 fof(f461,definition,(
% 6.99/1.42 sQ5_spl <=> (segmentP(sk2,sk1))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f464,plain,(
% 6.99/1.42 sQ2_spl|~sQ4_spl|~sQ5_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f437,f451,f458,f461])).
% 6.99/1.42 fof(f465,definition,(
% 6.99/1.42 sQ6_spl <=> (nil=sk1)),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f466,plain,(
% 6.99/1.42 nil=sk1|~sQ6_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f465])).
% 6.99/1.42 fof(f467,plain,(
% 6.99/1.42 ~nil=sk1|sQ6_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f465])).
% 6.99/1.42 fof(f468,plain,(
% 6.99/1.42 ~sQ6_spl|sQ3_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f438,f465,f454])).
% 6.99/1.42 fof(f470,definition,(
% 6.99/1.42 sQ7_spl <=> (nil=sk4)),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f471,plain,(
% 6.99/1.42 nil=sk4|~sQ7_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f470])).
% 6.99/1.42 fof(f473,definition,(
% 6.99/1.42 sQ8_spl <=> (neq(sk3,nil))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f474,plain,(
% 6.99/1.42 neq(sk3,nil)|~sQ8_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f473])).
% 6.99/1.42 fof(f476,plain,(
% 6.99/1.42 sQ7_spl|sQ8_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f440,f470,f473])).
% 6.99/1.42 fof(f477,definition,(
% 6.99/1.42 sQ9_spl <=> (rearsegP(sk4,sk3))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f478,plain,(
% 6.99/1.42 rearsegP(sk4,sk3)|~sQ9_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f477])).
% 6.99/1.42 fof(f481,definition,(
% 6.99/1.42 sQ10_spl <=> (nil=sk3)),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f482,plain,(
% 6.99/1.42 nil=sk3|~sQ10_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f481])).
% 6.99/1.42 fof(f485,plain,(
% 6.99/1.42 sQ10_spl|sQ9_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f443,f481,f477])).
% 6.99/1.42 fof(f493,plain,(
% 6.99/1.42 ![X1]: (~neq(X1,X1)|~ssList(X1)|~ssList(X1))),
% 6.99/1.42 inference(destructive_equality_resolution,[status(thm)],[f321])).
% 6.99/1.42 fof(f494,plain,(
% 6.99/1.42 ![X0]: (~neq(X0,X0)|~ssList(X0))),
% 6.99/1.42 inference(duplicate_literals_removal,[status(thm)],[f493])).
% 6.99/1.42 fof(f500,plain,(
% 6.99/1.42 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(app(X0,X1))|rearsegP(app(X0,X1),X1))),
% 6.99/1.42 inference(destructive_equality_resolution,[status(thm)],[f358])).
% 6.99/1.42 fof(f504,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 6.99/1.42 inference(destructive_equality_resolution,[status(thm)],[f406])).
% 6.99/1.42 fof(f517,plain,(
% 6.99/1.42 sk1=nil|~sQ10_spl),
% 6.99/1.42 inference(backward_demodulation,[status(thm)],[f482,f435])).
% 6.99/1.42 fof(f518,plain,(
% 6.99/1.42 ~ssList(nil)|nil=nil|~ssList(nil)),
% 6.99/1.42 inference(resolution,[status(thm)],[f280,f255])).
% 6.99/1.42 fof(f519,plain,(
% 6.99/1.42 ![X0,X1]: (~ssList(X0)|nil=X0|~segmentP(nil,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|~ssList(nil))),
% 6.99/1.42 inference(resolution,[status(thm)],[f280,f374])).
% 6.99/1.42 fof(f521,definition,(
% 6.99/1.42 sQ11_spl <=> (ssList(nil))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f523,plain,(
% 6.99/1.42 ~ssList(nil)|sQ11_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f521])).
% 6.99/1.42 fof(f524,definition,(
% 6.99/1.42 sQ12_spl <=> (nil=nil)),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f527,plain,(
% 6.99/1.42 ~sQ11_spl|sQ12_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f518,f521,f524])).
% 6.99/1.42 fof(f528,definition,(
% 6.99/1.42 ![X0,X1]: (sQ13_spl <=> (~ssList(X0)|nil=X0|~segmentP(nil,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f529,plain,(
% 6.99/1.42 ![X0,X1]: (~ssList(X0)|nil=X0|~segmentP(nil,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|~sQ13_spl)),
% 6.99/1.42 inference(component_clause,[status(thm)],[f528])).
% 6.99/1.42 fof(f531,plain,(
% 6.99/1.42 sQ13_spl|~sQ11_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f519,f528,f521])).
% 6.99/1.42 fof(f533,plain,(
% 6.99/1.42 $false|sQ11_spl),
% 6.99/1.42 inference(forward_subsumption_resolution,[status(thm)],[f523,f207])).
% 6.99/1.42 fof(f534,plain,(
% 6.99/1.42 sQ11_spl),
% 6.99/1.42 inference(contradiction_clause,[status(thm)],[f533])).
% 6.99/1.42 fof(f535,plain,(
% 6.99/1.42 ![X0,X1]: (~ssList(X0)|nil=X0|~segmentP(nil,X1)|~segmentP(X1,X0)|~ssList(X1)|~sQ13_spl)),
% 6.99/1.42 inference(duplicate_literals_removal,[status(thm)],[f529])).
% 6.99/1.42 fof(f545,plain,(
% 6.99/1.42 sk2=nil|~sQ7_spl),
% 6.99/1.42 inference(backward_demodulation,[status(thm)],[f471,f434])).
% 6.99/1.42 fof(f547,plain,(
% 6.99/1.42 $false|sQ6_spl|~sQ10_spl),
% 6.99/1.42 inference(forward_subsumption_resolution,[status(thm)],[f517,f467])).
% 6.99/1.42 fof(f548,plain,(
% 6.99/1.42 sQ6_spl|~sQ10_spl),
% 6.99/1.42 inference(contradiction_clause,[status(thm)],[f547])).
% 6.99/1.42 fof(f551,plain,(
% 6.99/1.42 ![X0,X1]: (~ssList(X0)|nil=X0|~rearsegP(nil,X1)|~rearsegP(X1,X0)|~ssList(X0)|~ssList(X1)|~ssList(nil))),
% 6.99/1.42 inference(resolution,[status(thm)],[f282,f376])).
% 6.99/1.42 fof(f554,definition,(
% 6.99/1.42 ![X0,X1]: (sQ14_spl <=> (~ssList(X0)|nil=X0|~rearsegP(nil,X1)|~rearsegP(X1,X0)|~ssList(X0)|~ssList(X1)))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f555,plain,(
% 6.99/1.42 ![X0,X1]: (~ssList(X0)|nil=X0|~rearsegP(nil,X1)|~rearsegP(X1,X0)|~ssList(X0)|~ssList(X1)|~sQ14_spl)),
% 6.99/1.42 inference(component_clause,[status(thm)],[f554])).
% 6.99/1.42 fof(f557,plain,(
% 6.99/1.42 sQ14_spl|~sQ11_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f551,f554,f521])).
% 6.99/1.42 fof(f559,plain,(
% 6.99/1.42 ![X0,X1]: (~ssList(X0)|nil=X0|~rearsegP(nil,X1)|~rearsegP(X1,X0)|~ssList(X1)|~sQ14_spl)),
% 6.99/1.42 inference(duplicate_literals_removal,[status(thm)],[f555])).
% 6.99/1.42 fof(f560,plain,(
% 6.99/1.42 app(sk2,nil)=sk2),
% 6.99/1.42 inference(resolution,[status(thm)],[f273,f431])).
% 6.99/1.42 fof(f567,plain,(
% 6.99/1.42 app(nil,nil)=nil),
% 6.99/1.42 inference(resolution,[status(thm)],[f273,f207])).
% 6.99/1.42 fof(f568,plain,(
% 6.99/1.42 app(sk1,nil)=sk1),
% 6.99/1.42 inference(resolution,[status(thm)],[f273,f430])).
% 6.99/1.42 fof(f569,plain,(
% 6.99/1.42 ![X0]: (~rearsegP(nil,X0)|~ssList(sk2)|~ssList(X0)|~ssList(nil)|rearsegP(sk2,X0))),
% 6.99/1.42 inference(paramodulation,[status(thm)],[f560,f350])).
% 6.99/1.42 fof(f570,definition,(
% 6.99/1.42 ![X0]: (sQ15_spl <=> (~rearsegP(nil,X0)|~ssList(X0)|rearsegP(sk2,X0)))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f573,definition,(
% 6.99/1.42 sQ16_spl <=> (ssList(sk2))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f575,plain,(
% 6.99/1.42 ~ssList(sk2)|sQ16_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f573])).
% 6.99/1.42 fof(f576,plain,(
% 6.99/1.42 sQ15_spl|~sQ16_spl|~sQ11_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f569,f570,f573,f521])).
% 6.99/1.42 fof(f577,plain,(
% 6.99/1.42 ![X0]: (~rearsegP(nil,X0)|~ssList(nil)|~ssList(X0)|~ssList(nil)|rearsegP(nil,X0))),
% 6.99/1.42 inference(paramodulation,[status(thm)],[f567,f350])).
% 6.99/1.42 fof(f578,definition,(
% 6.99/1.42 ![X0]: (sQ17_spl <=> (~rearsegP(nil,X0)|~ssList(X0)|rearsegP(nil,X0)))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f581,plain,(
% 6.99/1.42 sQ17_spl|~sQ11_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f577,f578,f521])).
% 6.99/1.42 fof(f590,plain,(
% 6.99/1.42 ![X0]: (~rearsegP(nil,X0)|~ssList(sk1)|~ssList(X0)|~ssList(nil)|rearsegP(sk1,X0))),
% 6.99/1.42 inference(paramodulation,[status(thm)],[f568,f350])).
% 6.99/1.42 fof(f591,definition,(
% 6.99/1.42 ![X0]: (sQ18_spl <=> (~rearsegP(nil,X0)|~ssList(X0)|rearsegP(sk1,X0)))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f594,definition,(
% 6.99/1.42 sQ19_spl <=> (ssList(sk1))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f596,plain,(
% 6.99/1.42 ~ssList(sk1)|sQ19_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f594])).
% 6.99/1.42 fof(f597,plain,(
% 6.99/1.42 sQ18_spl|~sQ19_spl|~sQ11_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f590,f591,f594,f521])).
% 6.99/1.42 fof(f598,plain,(
% 6.99/1.42 rearsegP(sk2,sk3)|~sQ9_spl),
% 6.99/1.42 inference(backward_demodulation,[status(thm)],[f434,f478])).
% 6.99/1.42 fof(f609,plain,(
% 6.99/1.42 app(nil,sk2)=sk2),
% 6.99/1.42 inference(resolution,[status(thm)],[f274,f431])).
% 6.99/1.42 fof(f617,plain,(
% 6.99/1.42 ![X0]: (~rearsegP(sk2,X0)|~ssList(nil)|~ssList(X0)|~ssList(sk2)|rearsegP(sk2,X0))),
% 6.99/1.42 inference(paramodulation,[status(thm)],[f609,f350])).
% 6.99/1.42 fof(f618,definition,(
% 6.99/1.42 ![X0]: (sQ20_spl <=> (~rearsegP(sk2,X0)|~ssList(X0)|rearsegP(sk2,X0)))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f621,plain,(
% 6.99/1.42 sQ20_spl|~sQ11_spl|~sQ16_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f617,f618,f521,f573])).
% 6.99/1.42 fof(f622,plain,(
% 6.99/1.42 $false|sQ16_spl),
% 6.99/1.42 inference(forward_subsumption_resolution,[status(thm)],[f575,f431])).
% 6.99/1.42 fof(f623,plain,(
% 6.99/1.42 sQ16_spl),
% 6.99/1.42 inference(contradiction_clause,[status(thm)],[f622])).
% 6.99/1.42 fof(f642,plain,(
% 6.99/1.42 neq(nil,nil)|~sQ6_spl|~sQ8_spl),
% 6.99/1.42 inference(backward_demodulation,[status(thm)],[f643,f474])).
% 6.99/1.42 fof(f643,plain,(
% 6.99/1.42 nil=sk3|~sQ6_spl),
% 6.99/1.42 inference(forward_demodulation,[status(thm)],[f466,f435])).
% 6.99/1.42 fof(f646,plain,(
% 6.99/1.42 app(nil,sk1)=sk1),
% 6.99/1.42 inference(resolution,[status(thm)],[f430,f274])).
% 6.99/1.42 fof(f650,plain,(
% 6.99/1.42 nil=sk4|~sQ2_spl),
% 6.99/1.42 inference(backward_demodulation,[status(thm)],[f452,f434])).
% 6.99/1.42 fof(f656,plain,(
% 6.99/1.42 rearsegP(nil,sk3)|~sQ2_spl|~sQ9_spl),
% 6.99/1.42 inference(forward_demodulation,[status(thm)],[f452,f598])).
% 6.99/1.42 fof(f657,plain,(
% 6.99/1.42 ~ssList(sk3)|nil=sk3|~sQ2_spl|~sQ9_spl),
% 6.99/1.42 inference(resolution,[status(thm)],[f656,f282])).
% 6.99/1.42 fof(f658,definition,(
% 6.99/1.42 sQ21_spl <=> (ssList(sk3))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f660,plain,(
% 6.99/1.42 ~ssList(sk3)|sQ21_spl),
% 6.99/1.42 inference(component_clause,[status(thm)],[f658])).
% 6.99/1.42 fof(f661,plain,(
% 6.99/1.42 ~sQ21_spl|sQ10_spl|~sQ2_spl|~sQ9_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f657,f658,f481,f451,f477])).
% 6.99/1.42 fof(f670,plain,(
% 6.99/1.42 $false|sQ19_spl),
% 6.99/1.42 inference(forward_subsumption_resolution,[status(thm)],[f596,f430])).
% 6.99/1.42 fof(f671,plain,(
% 6.99/1.42 sQ19_spl),
% 6.99/1.42 inference(contradiction_clause,[status(thm)],[f670])).
% 6.99/1.42 fof(f672,plain,(
% 6.99/1.42 ![X0]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~ssList(X0))),
% 6.99/1.42 inference(resolution,[status(thm)],[f339,f255])).
% 6.99/1.42 fof(f673,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~segmentP(X0,X1)|~ssList(X0)|~ssList(X1)|X1=X0|~segmentP(X1,X2)|~segmentP(X2,X0)|~ssList(X0)|~ssList(X2)|~ssList(X1))),
% 6.99/1.42 inference(resolution,[status(thm)],[f339,f374])).
% 6.99/1.42 fof(f675,definition,(
% 6.99/1.42 ![X0]: (sQ23_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~ssList(X0)))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f678,plain,(
% 6.99/1.42 sQ23_spl|~sQ11_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f672,f675,f521])).
% 6.99/1.42 fof(f679,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~segmentP(X0,X1)|~ssList(X0)|~ssList(X1)|X1=X0|~segmentP(X1,X2)|~segmentP(X2,X0)|~ssList(X2))),
% 6.99/1.42 inference(duplicate_literals_removal,[status(thm)],[f673])).
% 6.99/1.42 fof(f681,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~rearsegP(X0,app(X1,X2))|~ssList(X0)|~ssList(app(X1,X2))|app(X1,X2)=X0|~rearsegP(X2,X0)|~ssList(X1)|~ssList(X0)|~ssList(X2))),
% 6.99/1.42 inference(resolution,[status(thm)],[f340,f350])).
% 6.99/1.42 fof(f682,plain,(
% 6.99/1.42 ![X0]: (~rearsegP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~ssList(X0))),
% 6.99/1.42 inference(resolution,[status(thm)],[f340,f257])).
% 6.99/1.42 fof(f683,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~rearsegP(X0,X1)|~ssList(X0)|~ssList(X1)|X1=X0|~rearsegP(X1,X2)|~rearsegP(X2,X0)|~ssList(X0)|~ssList(X2)|~ssList(X1))),
% 6.99/1.42 inference(resolution,[status(thm)],[f340,f376])).
% 6.99/1.42 fof(f685,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~rearsegP(X0,app(X1,X2))|~ssList(X0)|~ssList(app(X1,X2))|app(X1,X2)=X0|~rearsegP(X2,X0)|~ssList(X1)|~ssList(X2))),
% 6.99/1.42 inference(duplicate_literals_removal,[status(thm)],[f681])).
% 6.99/1.42 fof(f686,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~rearsegP(X0,app(X1,X2))|~ssList(X0)|app(X1,X2)=X0|~rearsegP(X2,X0)|~ssList(X1)|~ssList(X2))),
% 6.99/1.42 inference(forward_subsumption_resolution,[status(thm)],[f685,f285])).
% 6.99/1.42 fof(f687,definition,(
% 6.99/1.42 ![X0]: (sQ24_spl <=> (~rearsegP(nil,X0)|~ssList(X0)|X0=nil|~ssList(X0)))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f690,plain,(
% 6.99/1.42 sQ24_spl|~sQ11_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f682,f687,f521])).
% 6.99/1.42 fof(f691,plain,(
% 6.99/1.42 ![X0,X1,X2]: (~rearsegP(X0,X1)|~ssList(X0)|~ssList(X1)|X1=X0|~rearsegP(X1,X2)|~rearsegP(X2,X0)|~ssList(X2))),
% 6.99/1.42 inference(duplicate_literals_removal,[status(thm)],[f683])).
% 6.99/1.42 fof(f695,plain,(
% 6.99/1.42 ~ssList(nil)|~ssList(sk1)|sk1=nil|sQ4_spl),
% 6.99/1.42 inference(resolution,[status(thm)],[f460,f302])).
% 6.99/1.42 fof(f696,plain,(
% 6.99/1.42 ~sQ11_spl|~sQ19_spl|sQ6_spl|sQ4_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f695,f521,f594,f465,f458])).
% 6.99/1.42 fof(f706,plain,(
% 6.99/1.42 ![X0]: (~rearsegP(sk1,X0)|~ssList(nil)|~ssList(X0)|~ssList(sk1)|rearsegP(sk1,X0))),
% 6.99/1.42 inference(paramodulation,[status(thm)],[f646,f350])).
% 6.99/1.42 fof(f708,definition,(
% 6.99/1.42 ![X0]: (sQ25_spl <=> (~rearsegP(sk1,X0)|~ssList(X0)|rearsegP(sk1,X0)))),
% 6.99/1.42 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 6.99/1.42 fof(f711,plain,(
% 6.99/1.42 sQ25_spl|~sQ11_spl|~sQ19_spl),
% 6.99/1.42 inference(split_clause,[status(thm)],[f706,f708,f521,f594])).
% 6.99/1.42 fof(f734,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|rearsegP(app(X0,X1),X1))),
% 6.99/1.43 inference(forward_subsumption_resolution,[status(thm)],[f500,f285])).
% 6.99/1.43 fof(f735,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X1,app(X0,X1))|~ssList(X1)|~ssList(app(X0,X1))|app(X0,X1)=X1)),
% 6.99/1.43 inference(resolution,[status(thm)],[f734,f340])).
% 6.99/1.43 fof(f736,plain,(
% 6.99/1.43 ~ssList(sk2)|~ssList(nil)|rearsegP(sk2,nil)),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f560,f734])).
% 6.99/1.43 fof(f737,plain,(
% 6.99/1.43 ~ssList(sk1)|~ssList(nil)|rearsegP(sk1,nil)),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f568,f734])).
% 6.99/1.43 fof(f738,plain,(
% 6.99/1.43 ~ssList(nil)|~ssList(sk2)|rearsegP(sk2,sk2)),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f609,f734])).
% 6.99/1.43 fof(f739,plain,(
% 6.99/1.43 ~ssList(nil)|~ssList(sk1)|rearsegP(sk1,sk1)),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f646,f734])).
% 6.99/1.43 fof(f740,plain,(
% 6.99/1.43 ~ssList(nil)|~ssList(nil)|rearsegP(nil,nil)),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f567,f734])).
% 6.99/1.43 fof(f741,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X1,app(X0,X1))|~ssList(app(X0,X1))|app(X0,X1)=X1)),
% 6.99/1.43 inference(duplicate_literals_removal,[status(thm)],[f735])).
% 6.99/1.43 fof(f742,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X1,app(X0,X1))|app(X0,X1)=X1)),
% 6.99/1.43 inference(forward_subsumption_resolution,[status(thm)],[f741,f285])).
% 6.99/1.43 fof(f743,definition,(
% 6.99/1.43 sQ26_spl <=> (rearsegP(sk2,nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f744,plain,(
% 6.99/1.43 rearsegP(sk2,nil)|~sQ26_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f743])).
% 6.99/1.43 fof(f746,plain,(
% 6.99/1.43 ~sQ16_spl|~sQ11_spl|sQ26_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f736,f573,f521,f743])).
% 6.99/1.43 fof(f747,definition,(
% 6.99/1.43 sQ27_spl <=> (rearsegP(sk1,nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f748,plain,(
% 6.99/1.43 rearsegP(sk1,nil)|~sQ27_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f747])).
% 6.99/1.43 fof(f750,plain,(
% 6.99/1.43 ~sQ19_spl|~sQ11_spl|sQ27_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f737,f594,f521,f747])).
% 6.99/1.43 fof(f751,definition,(
% 6.99/1.43 sQ28_spl <=> (rearsegP(sk2,sk2))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f752,plain,(
% 6.99/1.43 rearsegP(sk2,sk2)|~sQ28_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f751])).
% 6.99/1.43 fof(f754,plain,(
% 6.99/1.43 ~sQ11_spl|~sQ16_spl|sQ28_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f738,f521,f573,f751])).
% 6.99/1.43 fof(f755,definition,(
% 6.99/1.43 sQ29_spl <=> (rearsegP(sk1,sk1))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f756,plain,(
% 6.99/1.43 rearsegP(sk1,sk1)|~sQ29_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f755])).
% 6.99/1.43 fof(f758,plain,(
% 6.99/1.43 ~sQ11_spl|~sQ19_spl|sQ29_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f739,f521,f594,f755])).
% 6.99/1.43 fof(f759,definition,(
% 6.99/1.43 sQ30_spl <=> (rearsegP(nil,nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f760,plain,(
% 6.99/1.43 rearsegP(nil,nil)|~sQ30_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f759])).
% 6.99/1.43 fof(f762,plain,(
% 6.99/1.43 ~sQ11_spl|sQ30_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f740,f521,f759])).
% 6.99/1.43 fof(f763,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2))),
% 6.99/1.43 inference(resolution,[status(thm)],[f404,f255])).
% 6.99/1.43 fof(f764,plain,(
% 6.99/1.43 ![X0,X1,X2,X3,X4]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|segmentP(app(app(X1,X3),X0),X2)|~segmentP(X3,X4)|~segmentP(X4,X2)|~ssList(X2)|~ssList(X4)|~ssList(X3))),
% 6.99/1.43 inference(resolution,[status(thm)],[f404,f374])).
% 6.99/1.43 fof(f765,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X2)|segmentP(app(app(X1,X2),X0),X2)|~ssList(X2))),
% 6.99/1.43 inference(resolution,[status(thm)],[f404,f256])).
% 6.99/1.43 fof(f766,definition,(
% 6.99/1.43 ![X0,X1,X2]: (sQ31_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f767,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2)|~sQ31_spl)),
% 6.99/1.43 inference(component_clause,[status(thm)],[f766])).
% 6.99/1.43 fof(f769,plain,(
% 6.99/1.43 sQ31_spl|~sQ11_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f763,f766,f521])).
% 6.99/1.43 fof(f770,plain,(
% 6.99/1.43 ![X0,X1,X2,X3,X4]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|segmentP(app(app(X1,X3),X0),X2)|~segmentP(X3,X4)|~segmentP(X4,X2)|~ssList(X4))),
% 6.99/1.43 inference(duplicate_literals_removal,[status(thm)],[f764])).
% 6.99/1.43 fof(f771,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),X2))),
% 6.99/1.43 inference(duplicate_literals_removal,[status(thm)],[f765])).
% 6.99/1.43 fof(f772,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~sQ31_spl)),
% 6.99/1.43 inference(duplicate_literals_removal,[status(thm)],[f767])).
% 6.99/1.43 fof(f773,plain,(
% 6.99/1.43 ~rearsegP(nil,sk2)|~ssList(nil)|~ssList(sk2)|sk2=nil|~sQ26_spl),
% 6.99/1.43 inference(resolution,[status(thm)],[f744,f340])).
% 6.99/1.43 fof(f774,definition,(
% 6.99/1.43 sQ32_spl <=> (rearsegP(nil,sk2))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f776,plain,(
% 6.99/1.43 ~rearsegP(nil,sk2)|sQ32_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f774])).
% 6.99/1.43 fof(f777,plain,(
% 6.99/1.43 ~sQ32_spl|~sQ11_spl|~sQ16_spl|sQ2_spl|~sQ26_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f773,f774,f521,f573,f451,f743])).
% 6.99/1.43 fof(f783,plain,(
% 6.99/1.43 ~rearsegP(sk2,sk2)|~ssList(sk2)|~ssList(sk2)|sk2=sk2|~sQ28_spl),
% 6.99/1.43 inference(resolution,[status(thm)],[f752,f340])).
% 6.99/1.43 fof(f784,definition,(
% 6.99/1.43 sQ34_spl <=> (sk2=sk2)),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f787,plain,(
% 6.99/1.43 ~sQ28_spl|~sQ16_spl|sQ34_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f783,f751,f573,f784])).
% 6.99/1.43 fof(f788,plain,(
% 6.99/1.43 ~rearsegP(sk1,sk1)|~ssList(sk1)|~ssList(sk1)|sk1=sk1|~sQ29_spl),
% 6.99/1.43 inference(resolution,[status(thm)],[f756,f340])).
% 6.99/1.43 fof(f789,definition,(
% 6.99/1.43 sQ35_spl <=> (sk1=sk1)),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f792,plain,(
% 6.99/1.43 ~sQ29_spl|~sQ19_spl|sQ35_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f788,f755,f594,f789])).
% 6.99/1.43 fof(f814,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|app(X0,X1)=X1|~rearsegP(X1,X2)|~rearsegP(X2,app(X0,X1))|~ssList(app(X0,X1))|~ssList(X2)|~ssList(X1))),
% 6.99/1.43 inference(resolution,[status(thm)],[f742,f376])).
% 6.99/1.43 fof(f817,plain,(
% 6.99/1.43 ~ssList(nil)|~ssList(sk2)|~rearsegP(sk2,sk2)|app(nil,sk2)=sk2),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f609,f742])).
% 6.99/1.43 fof(f818,plain,(
% 6.99/1.43 ~ssList(nil)|~ssList(sk1)|~rearsegP(sk1,sk1)|app(nil,sk1)=sk1),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f646,f742])).
% 6.99/1.43 fof(f819,plain,(
% 6.99/1.43 ~ssList(nil)|~ssList(nil)|~rearsegP(nil,nil)|app(nil,nil)=nil),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f567,f742])).
% 6.99/1.43 fof(f821,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|app(X0,X1)=X1|~rearsegP(X1,X2)|~rearsegP(X2,app(X0,X1))|~ssList(app(X0,X1))|~ssList(X2))),
% 6.99/1.43 inference(duplicate_literals_removal,[status(thm)],[f814])).
% 6.99/1.43 fof(f822,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|app(X0,X1)=X1|~rearsegP(X1,X2)|~rearsegP(X2,app(X0,X1))|~ssList(X2))),
% 6.99/1.43 inference(forward_subsumption_resolution,[status(thm)],[f821,f285])).
% 6.99/1.43 fof(f831,definition,(
% 6.99/1.43 sQ39_spl <=> (app(nil,sk2)=sk2)),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f834,plain,(
% 6.99/1.43 ~sQ11_spl|~sQ16_spl|~sQ28_spl|sQ39_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f817,f521,f573,f751,f831])).
% 6.99/1.43 fof(f835,definition,(
% 6.99/1.43 sQ40_spl <=> (app(nil,sk1)=sk1)),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f838,plain,(
% 6.99/1.43 ~sQ11_spl|~sQ19_spl|~sQ29_spl|sQ40_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f818,f521,f594,f755,f835])).
% 6.99/1.43 fof(f839,definition,(
% 6.99/1.43 sQ41_spl <=> (app(nil,nil)=nil)),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f842,plain,(
% 6.99/1.43 ~sQ11_spl|~sQ30_spl|sQ41_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f819,f521,f759,f839])).
% 6.99/1.43 fof(f850,plain,(
% 6.99/1.43 ![X0,X1,X2,X3,X4]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~ssList(nil)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X4,app(app(X1,X2),X0)),X3),nil)|~sQ31_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f772,f404])).
% 6.99/1.43 fof(f851,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~segmentP(nil,app(app(X1,X2),X0))|~ssList(nil)|~ssList(app(app(X1,X2),X0))|app(app(X1,X2),X0)=nil|~sQ31_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f772,f339])).
% 6.99/1.43 fof(f857,definition,(
% 6.99/1.43 ![X0,X1,X2,X3,X4]: (sQ43_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X4,app(app(X1,X2),X0)),X3),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f860,plain,(
% 6.99/1.43 sQ43_spl|~sQ11_spl|~sQ31_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f850,f857,f521,f766])).
% 6.99/1.43 fof(f861,definition,(
% 6.99/1.43 ![X0,X1,X2]: (sQ44_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~segmentP(nil,app(app(X1,X2),X0))|~ssList(app(app(X1,X2),X0))|app(app(X1,X2),X0)=nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f864,plain,(
% 6.99/1.43 sQ44_spl|~sQ11_spl|~sQ31_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f851,f861,f521,f766])).
% 6.99/1.43 fof(f865,definition,(
% 6.99/1.43 ![X0]: (sQ45_spl <=> (~ssList(X0)|segmentP(app(sk2,X0),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f866,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|segmentP(app(sk2,X0),nil)|~sQ45_spl)),
% 6.99/1.43 inference(component_clause,[status(thm)],[f865])).
% 6.99/1.43 fof(f869,definition,(
% 6.99/1.43 ![X0]: (sQ46_spl <=> (~ssList(X0)|segmentP(app(sk1,X0),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f870,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),nil)|~sQ46_spl)),
% 6.99/1.43 inference(component_clause,[status(thm)],[f869])).
% 6.99/1.43 fof(f875,definition,(
% 6.99/1.43 ![X0]: (sQ47_spl <=> (~ssList(X0)|segmentP(app(nil,X0),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f876,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|segmentP(app(nil,X0),nil)|~sQ47_spl)),
% 6.99/1.43 inference(component_clause,[status(thm)],[f875])).
% 6.99/1.43 fof(f880,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|~ssList(sk2)|~ssList(nil)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,nil),X0),nil))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f560,f504])).
% 6.99/1.43 fof(f881,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(nil)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f568,f504])).
% 6.99/1.43 fof(f882,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f609,f504])).
% 6.99/1.43 fof(f883,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f646,f504])).
% 6.99/1.43 fof(f884,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f567,f504])).
% 6.99/1.43 fof(f887,definition,(
% 6.99/1.43 ![X0]: (sQ48_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,nil),X0),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f890,plain,(
% 6.99/1.43 sQ48_spl|~sQ16_spl|~sQ11_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f880,f887,f573,f521])).
% 6.99/1.43 fof(f891,definition,(
% 6.99/1.43 ![X0]: (sQ49_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f894,plain,(
% 6.99/1.43 sQ49_spl|~sQ19_spl|~sQ11_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f881,f891,f594,f521])).
% 6.99/1.43 fof(f895,definition,(
% 6.99/1.43 ![X0]: (sQ50_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f898,plain,(
% 6.99/1.43 sQ50_spl|~sQ11_spl|~sQ16_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f882,f895,f521,f573])).
% 6.99/1.43 fof(f899,definition,(
% 6.99/1.43 ![X0]: (sQ51_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f902,plain,(
% 6.99/1.43 sQ51_spl|~sQ11_spl|~sQ19_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f883,f899,f521,f594])).
% 6.99/1.43 fof(f903,definition,(
% 6.99/1.43 ![X0]: (sQ52_spl <=> (~ssList(X0)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f906,plain,(
% 6.99/1.43 sQ52_spl|~sQ11_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f884,f903,f521])).
% 6.99/1.43 fof(f912,plain,(
% 6.99/1.43 ~rearsegP(nil,nil)|~sQ7_spl|sQ32_spl),
% 6.99/1.43 inference(backward_demodulation,[status(thm)],[f545,f776])).
% 6.99/1.43 fof(f919,plain,(
% 6.99/1.43 neq(nil,nil)|~sQ7_spl|~sQ3_spl),
% 6.99/1.43 inference(backward_demodulation,[status(thm)],[f545,f455])).
% 6.99/1.43 fof(f921,plain,(
% 6.99/1.43 $false|~sQ30_spl|~sQ7_spl|sQ32_spl),
% 6.99/1.43 inference(forward_subsumption_resolution,[status(thm)],[f912,f760])).
% 6.99/1.43 fof(f922,plain,(
% 6.99/1.43 ~sQ30_spl|~sQ7_spl|sQ32_spl),
% 6.99/1.43 inference(contradiction_clause,[status(thm)],[f921])).
% 6.99/1.43 fof(f923,plain,(
% 6.99/1.43 ~ssList(sk1)|sQ21_spl),
% 6.99/1.43 inference(forward_demodulation,[status(thm)],[f435,f660])).
% 6.99/1.43 fof(f924,plain,(
% 6.99/1.43 $false|sQ21_spl),
% 6.99/1.43 inference(forward_subsumption_resolution,[status(thm)],[f923,f430])).
% 6.99/1.43 fof(f925,plain,(
% 6.99/1.43 sQ21_spl),
% 6.99/1.43 inference(contradiction_clause,[status(thm)],[f924])).
% 6.99/1.43 fof(f927,plain,(
% 6.99/1.43 sQ7_spl|~sQ2_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f650,f470,f451])).
% 6.99/1.43 fof(f931,plain,(
% 6.99/1.43 rearsegP(sk2,sk1)|~sQ9_spl),
% 6.99/1.43 inference(forward_demodulation,[status(thm)],[f435,f598])).
% 6.99/1.43 fof(f994,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(nil)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),nil)|~sQ45_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f866,f404])).
% 6.99/1.43 fof(f995,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|~segmentP(nil,app(sk2,X0))|~ssList(nil)|~ssList(app(sk2,X0))|app(sk2,X0)=nil|~sQ45_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f866,f339])).
% 6.99/1.43 fof(f996,plain,(
% 6.99/1.43 ~ssList(nil)|segmentP(sk2,nil)|~sQ45_spl),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f560,f866])).
% 6.99/1.43 fof(f997,definition,(
% 6.99/1.43 ![X0,X1,X2]: (sQ56_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1000,plain,(
% 6.99/1.43 sQ56_spl|~sQ11_spl|~sQ45_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f994,f997,f521,f865])).
% 6.99/1.43 fof(f1001,definition,(
% 6.99/1.43 ![X0]: (sQ57_spl <=> (~ssList(X0)|~segmentP(nil,app(sk2,X0))|~ssList(app(sk2,X0))|app(sk2,X0)=nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1004,plain,(
% 6.99/1.43 sQ57_spl|~sQ11_spl|~sQ45_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f995,f1001,f521,f865])).
% 6.99/1.43 fof(f1005,definition,(
% 6.99/1.43 sQ58_spl <=> (segmentP(sk2,nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1006,plain,(
% 6.99/1.43 segmentP(sk2,nil)|~sQ58_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1005])).
% 6.99/1.43 fof(f1008,plain,(
% 6.99/1.43 ~sQ11_spl|sQ58_spl|~sQ45_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f996,f521,f1005,f865])).
% 6.99/1.43 fof(f1009,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(sk2)|segmentP(app(app(X1,sk2),X0),nil)|~sQ58_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f1006,f404])).
% 6.99/1.43 fof(f1011,definition,(
% 6.99/1.43 ![X0,X1]: (sQ59_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk2),X0),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1012,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk2),X0),nil)|~sQ59_spl)),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1011])).
% 6.99/1.43 fof(f1014,plain,(
% 6.99/1.43 sQ59_spl|~sQ11_spl|~sQ16_spl|~sQ58_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1009,f1011,f521,f573,f1005])).
% 6.99/1.43 fof(f1044,plain,(
% 6.99/1.43 ~ssList(nil)|~sQ7_spl|~sQ3_spl),
% 6.99/1.43 inference(resolution,[status(thm)],[f919,f494])).
% 6.99/1.43 fof(f1045,plain,(
% 6.99/1.43 ~sQ11_spl|~sQ7_spl|~sQ3_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1044,f521,f470,f454])).
% 6.99/1.43 fof(f1056,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(nil)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),nil)|~sQ46_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f870,f404])).
% 6.99/1.43 fof(f1057,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|~segmentP(nil,app(sk1,X0))|~ssList(nil)|~ssList(app(sk1,X0))|app(sk1,X0)=nil|~sQ46_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f870,f339])).
% 6.99/1.43 fof(f1058,plain,(
% 6.99/1.43 ~ssList(nil)|segmentP(sk1,nil)|~sQ46_spl),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f568,f870])).
% 6.99/1.43 fof(f1059,definition,(
% 6.99/1.43 ![X0,X1,X2]: (sQ63_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1062,plain,(
% 6.99/1.43 sQ63_spl|~sQ11_spl|~sQ46_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1056,f1059,f521,f869])).
% 6.99/1.43 fof(f1063,definition,(
% 6.99/1.43 ![X0]: (sQ64_spl <=> (~ssList(X0)|~segmentP(nil,app(sk1,X0))|~ssList(app(sk1,X0))|app(sk1,X0)=nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1066,plain,(
% 6.99/1.43 sQ64_spl|~sQ11_spl|~sQ46_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1057,f1063,f521,f869])).
% 6.99/1.43 fof(f1067,definition,(
% 6.99/1.43 sQ65_spl <=> (segmentP(sk1,nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1068,plain,(
% 6.99/1.43 segmentP(sk1,nil)|~sQ65_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1067])).
% 6.99/1.43 fof(f1070,plain,(
% 6.99/1.43 ~sQ11_spl|sQ65_spl|~sQ46_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1058,f521,f1067,f869])).
% 6.99/1.43 fof(f1071,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(sk1)|segmentP(app(app(X1,sk1),X0),nil)|~sQ65_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f1068,f404])).
% 6.99/1.43 fof(f1073,definition,(
% 6.99/1.43 ![X0,X1]: (sQ66_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1074,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),nil)|~sQ66_spl)),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1073])).
% 6.99/1.43 fof(f1076,plain,(
% 6.99/1.43 sQ66_spl|~sQ11_spl|~sQ19_spl|~sQ65_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1071,f1073,f521,f594,f1067])).
% 6.99/1.43 fof(f1081,plain,(
% 6.99/1.43 ~ssList(nil)|~sQ6_spl|~sQ8_spl),
% 6.99/1.43 inference(resolution,[status(thm)],[f642,f494])).
% 6.99/1.43 fof(f1082,plain,(
% 6.99/1.43 ~sQ11_spl|~sQ6_spl|~sQ8_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1081,f521,f465,f473])).
% 6.99/1.43 fof(f1098,plain,(
% 6.99/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(nil)|~ssList(app(app(X1,sk2),X0))|segmentP(app(app(X3,app(app(X1,sk2),X0)),X2),nil)|~sQ59_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f1012,f404])).
% 6.99/1.43 fof(f1099,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(nil,app(app(X1,sk2),X0))|~ssList(nil)|~ssList(app(app(X1,sk2),X0))|app(app(X1,sk2),X0)=nil|~sQ59_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f1012,f339])).
% 6.99/1.43 fof(f1101,definition,(
% 6.99/1.43 ![X0,X1,X2,X3]: (sQ68_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(app(app(X1,sk2),X0))|segmentP(app(app(X3,app(app(X1,sk2),X0)),X2),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1104,plain,(
% 6.99/1.43 sQ68_spl|~sQ11_spl|~sQ59_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1098,f1101,f521,f1011])).
% 6.99/1.43 fof(f1105,definition,(
% 6.99/1.43 ![X0,X1]: (sQ69_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(nil,app(app(X1,sk2),X0))|~ssList(app(app(X1,sk2),X0))|app(app(X1,sk2),X0)=nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1108,plain,(
% 6.99/1.43 sQ69_spl|~sQ11_spl|~sQ59_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1099,f1105,f521,f1011])).
% 6.99/1.43 fof(f1110,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(nil)|~ssList(app(nil,X0))|segmentP(app(app(X2,app(nil,X0)),X1),nil)|~sQ47_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f876,f404])).
% 6.99/1.43 fof(f1111,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|~segmentP(nil,app(nil,X0))|~ssList(nil)|~ssList(app(nil,X0))|app(nil,X0)=nil|~sQ47_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f876,f339])).
% 6.99/1.43 fof(f1114,plain,(
% 6.99/1.43 ~ssList(nil)|segmentP(nil,nil)|~sQ47_spl),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f567,f876])).
% 6.99/1.43 fof(f1115,definition,(
% 6.99/1.43 ![X0,X1,X2]: (sQ70_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(nil,X0))|segmentP(app(app(X2,app(nil,X0)),X1),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1118,plain,(
% 6.99/1.43 sQ70_spl|~sQ11_spl|~sQ47_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1110,f1115,f521,f875])).
% 6.99/1.43 fof(f1119,definition,(
% 6.99/1.43 ![X0]: (sQ71_spl <=> (~ssList(X0)|~segmentP(nil,app(nil,X0))|~ssList(app(nil,X0))|app(nil,X0)=nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1122,plain,(
% 6.99/1.43 sQ71_spl|~sQ11_spl|~sQ47_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1111,f1119,f521,f875])).
% 6.99/1.43 fof(f1125,definition,(
% 6.99/1.43 sQ72_spl <=> (segmentP(nil,nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1126,plain,(
% 6.99/1.43 segmentP(nil,nil)|~sQ72_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1125])).
% 6.99/1.43 fof(f1128,plain,(
% 6.99/1.43 ~sQ11_spl|sQ72_spl|~sQ47_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1114,f521,f1125,f875])).
% 6.99/1.43 fof(f1130,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(nil)|segmentP(app(app(X1,nil),X0),nil)|~sQ72_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f1126,f404])).
% 6.99/1.43 fof(f1133,definition,(
% 6.99/1.43 ![X0,X1]: (sQ73_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,nil),X0),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1134,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,nil),X0),nil)|~sQ73_spl)),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1133])).
% 6.99/1.43 fof(f1136,plain,(
% 6.99/1.43 sQ73_spl|~sQ11_spl|~sQ72_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1130,f1133,f521,f1125])).
% 6.99/1.43 fof(f1138,plain,(
% 6.99/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(nil)|~ssList(app(app(X1,sk1),X0))|segmentP(app(app(X3,app(app(X1,sk1),X0)),X2),nil)|~sQ66_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f1074,f404])).
% 6.99/1.43 fof(f1139,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(nil,app(app(X1,sk1),X0))|~ssList(nil)|~ssList(app(app(X1,sk1),X0))|app(app(X1,sk1),X0)=nil|~sQ66_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f1074,f339])).
% 6.99/1.43 fof(f1141,definition,(
% 6.99/1.43 ![X0,X1,X2,X3]: (sQ74_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(app(app(X1,sk1),X0))|segmentP(app(app(X3,app(app(X1,sk1),X0)),X2),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1144,plain,(
% 6.99/1.43 sQ74_spl|~sQ11_spl|~sQ66_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1138,f1141,f521,f1073])).
% 6.99/1.43 fof(f1145,definition,(
% 6.99/1.43 ![X0,X1]: (sQ75_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(nil,app(app(X1,sk1),X0))|~ssList(app(app(X1,sk1),X0))|app(app(X1,sk1),X0)=nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1148,plain,(
% 6.99/1.43 sQ75_spl|~sQ11_spl|~sQ66_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1139,f1145,f521,f1073])).
% 6.99/1.43 fof(f1150,plain,(
% 6.99/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(nil)|~ssList(app(app(X1,nil),X0))|segmentP(app(app(X3,app(app(X1,nil),X0)),X2),nil)|~sQ73_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f1134,f404])).
% 6.99/1.43 fof(f1151,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(nil,app(app(X1,nil),X0))|~ssList(nil)|~ssList(app(app(X1,nil),X0))|app(app(X1,nil),X0)=nil|~sQ73_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f1134,f339])).
% 6.99/1.43 fof(f1155,definition,(
% 6.99/1.43 ![X0,X1,X2,X3]: (sQ76_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(app(app(X1,nil),X0))|segmentP(app(app(X3,app(app(X1,nil),X0)),X2),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1158,plain,(
% 6.99/1.43 sQ76_spl|~sQ11_spl|~sQ73_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1150,f1155,f521,f1133])).
% 6.99/1.43 fof(f1159,definition,(
% 6.99/1.43 ![X0,X1]: (sQ77_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(nil,app(app(X1,nil),X0))|~ssList(app(app(X1,nil),X0))|app(app(X1,nil),X0)=nil))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1162,plain,(
% 6.99/1.43 sQ77_spl|~sQ11_spl|~sQ73_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1151,f1159,f521,f1133])).
% 6.99/1.43 fof(f1193,plain,(
% 6.99/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|app(X1,X2)=X0|~rearsegP(X2,X0)|~ssList(X1)|~ssList(X2)|~rearsegP(X0,X3)|~rearsegP(X3,app(X1,X2))|~ssList(app(X1,X2))|~ssList(X3)|~ssList(X0))),
% 6.99/1.43 inference(resolution,[status(thm)],[f686,f376])).
% 6.99/1.43 fof(f1195,plain,(
% 6.99/1.43 ![X0]: (~rearsegP(X0,sk2)|~ssList(X0)|app(sk2,nil)=X0|~rearsegP(nil,X0)|~ssList(sk2)|~ssList(nil))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f560,f686])).
% 6.99/1.43 fof(f1196,plain,(
% 6.99/1.43 ![X0]: (~rearsegP(X0,sk1)|~ssList(X0)|app(sk1,nil)=X0|~rearsegP(nil,X0)|~ssList(sk1)|~ssList(nil))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f568,f686])).
% 6.99/1.43 fof(f1197,plain,(
% 6.99/1.43 ![X0]: (~rearsegP(X0,sk2)|~ssList(X0)|app(nil,sk2)=X0|~rearsegP(sk2,X0)|~ssList(nil)|~ssList(sk2))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f609,f686])).
% 6.99/1.43 fof(f1198,plain,(
% 6.99/1.43 ![X0]: (~rearsegP(X0,sk1)|~ssList(X0)|app(nil,sk1)=X0|~rearsegP(sk1,X0)|~ssList(nil)|~ssList(sk1))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f646,f686])).
% 6.99/1.43 fof(f1199,plain,(
% 6.99/1.43 ![X0]: (~rearsegP(X0,nil)|~ssList(X0)|app(nil,nil)=X0|~rearsegP(nil,X0)|~ssList(nil)|~ssList(nil))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f567,f686])).
% 6.99/1.43 fof(f1202,plain,(
% 6.99/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|app(X1,X2)=X0|~rearsegP(X2,X0)|~ssList(X1)|~ssList(X2)|~rearsegP(X0,X3)|~rearsegP(X3,app(X1,X2))|~ssList(app(X1,X2))|~ssList(X3))),
% 6.99/1.43 inference(duplicate_literals_removal,[status(thm)],[f1193])).
% 6.99/1.43 fof(f1203,plain,(
% 6.99/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|app(X1,X2)=X0|~rearsegP(X2,X0)|~ssList(X1)|~ssList(X2)|~rearsegP(X0,X3)|~rearsegP(X3,app(X1,X2))|~ssList(X3))),
% 6.99/1.43 inference(forward_subsumption_resolution,[status(thm)],[f1202,f285])).
% 6.99/1.43 fof(f1204,definition,(
% 6.99/1.43 ![X0]: (sQ78_spl <=> (~rearsegP(X0,sk2)|~ssList(X0)|app(sk2,nil)=X0|~rearsegP(nil,X0)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1207,plain,(
% 6.99/1.43 sQ78_spl|~sQ16_spl|~sQ11_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1195,f1204,f573,f521])).
% 6.99/1.43 fof(f1208,definition,(
% 6.99/1.43 ![X0]: (sQ79_spl <=> (~rearsegP(X0,sk1)|~ssList(X0)|app(sk1,nil)=X0|~rearsegP(nil,X0)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1211,plain,(
% 6.99/1.43 sQ79_spl|~sQ19_spl|~sQ11_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1196,f1208,f594,f521])).
% 6.99/1.43 fof(f1212,definition,(
% 6.99/1.43 ![X0]: (sQ80_spl <=> (~rearsegP(X0,sk2)|~ssList(X0)|app(nil,sk2)=X0|~rearsegP(sk2,X0)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1215,plain,(
% 6.99/1.43 sQ80_spl|~sQ11_spl|~sQ16_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1197,f1212,f521,f573])).
% 6.99/1.43 fof(f1216,definition,(
% 6.99/1.43 ![X0]: (sQ81_spl <=> (~rearsegP(X0,sk1)|~ssList(X0)|app(nil,sk1)=X0|~rearsegP(sk1,X0)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1219,plain,(
% 6.99/1.43 sQ81_spl|~sQ11_spl|~sQ19_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1198,f1216,f521,f594])).
% 6.99/1.43 fof(f1220,definition,(
% 6.99/1.43 ![X0]: (sQ82_spl <=> (~rearsegP(X0,nil)|~ssList(X0)|app(nil,nil)=X0|~rearsegP(nil,X0)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1223,plain,(
% 6.99/1.43 sQ82_spl|~sQ11_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1199,f1220,f521])).
% 6.99/1.43 fof(f1231,plain,(
% 6.99/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|app(X0,X1)=X1|~rearsegP(X1,X2)|~ssList(X2)|~rearsegP(X2,X3)|~rearsegP(X3,app(X0,X1))|~ssList(app(X0,X1))|~ssList(X3)|~ssList(X2))),
% 6.99/1.43 inference(resolution,[status(thm)],[f822,f376])).
% 6.99/1.43 fof(f1240,plain,(
% 6.99/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|app(X0,X1)=X1|~rearsegP(X1,X2)|~ssList(X2)|~rearsegP(X2,X3)|~rearsegP(X3,app(X0,X1))|~ssList(app(X0,X1))|~ssList(X3))),
% 6.99/1.43 inference(duplicate_literals_removal,[status(thm)],[f1231])).
% 6.99/1.43 fof(f1241,plain,(
% 6.99/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|app(X0,X1)=X1|~rearsegP(X1,X2)|~ssList(X2)|~rearsegP(X2,X3)|~rearsegP(X3,app(X0,X1))|~ssList(X3))),
% 6.99/1.43 inference(forward_subsumption_resolution,[status(thm)],[f1240,f285])).
% 6.99/1.43 fof(f1261,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|app(sk2,nil)=X0|~rearsegP(nil,X0)|~ssList(sk2)|~ssList(nil)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f560,f1203])).
% 6.99/1.43 fof(f1262,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|app(sk1,nil)=X0|~rearsegP(nil,X0)|~ssList(sk1)|~ssList(nil)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f568,f1203])).
% 6.99/1.43 fof(f1263,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|app(nil,sk2)=X0|~rearsegP(sk2,X0)|~ssList(nil)|~ssList(sk2)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f609,f1203])).
% 6.99/1.43 fof(f1264,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|app(nil,sk1)=X0|~rearsegP(sk1,X0)|~ssList(nil)|~ssList(sk1)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f646,f1203])).
% 6.99/1.43 fof(f1265,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|app(nil,nil)=X0|~rearsegP(nil,X0)|~ssList(nil)|~ssList(nil)|~rearsegP(X0,X1)|~rearsegP(X1,nil)|~ssList(X1))),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f567,f1203])).
% 6.99/1.43 fof(f1271,definition,(
% 6.99/1.43 ![X0,X1]: (sQ86_spl <=> (~ssList(X0)|app(sk2,nil)=X0|~rearsegP(nil,X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1274,plain,(
% 6.99/1.43 sQ86_spl|~sQ16_spl|~sQ11_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1261,f1271,f573,f521])).
% 6.99/1.43 fof(f1275,definition,(
% 6.99/1.43 ![X0,X1]: (sQ87_spl <=> (~ssList(X0)|app(sk1,nil)=X0|~rearsegP(nil,X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1278,plain,(
% 6.99/1.43 sQ87_spl|~sQ19_spl|~sQ11_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1262,f1275,f594,f521])).
% 6.99/1.43 fof(f1279,definition,(
% 6.99/1.43 ![X0,X1]: (sQ88_spl <=> (~ssList(X0)|app(nil,sk2)=X0|~rearsegP(sk2,X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1282,plain,(
% 6.99/1.43 sQ88_spl|~sQ11_spl|~sQ16_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1263,f1279,f521,f573])).
% 6.99/1.43 fof(f1283,definition,(
% 6.99/1.43 ![X0,X1]: (sQ89_spl <=> (~ssList(X0)|app(nil,sk1)=X0|~rearsegP(sk1,X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1286,plain,(
% 6.99/1.43 sQ89_spl|~sQ11_spl|~sQ19_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1264,f1283,f521,f594])).
% 6.99/1.43 fof(f1287,definition,(
% 6.99/1.43 ![X0,X1]: (sQ90_spl <=> (~ssList(X0)|app(nil,nil)=X0|~rearsegP(nil,X0)|~rearsegP(X0,X1)|~rearsegP(X1,nil)|~ssList(X1)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1290,plain,(
% 6.99/1.43 sQ90_spl|~sQ11_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1265,f1287,f521])).
% 6.99/1.43 fof(f1331,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|nil=X0|~segmentP(nil,X0)|~ssList(nil)|~ssList(nil)|~sQ13_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f535,f255])).
% 6.99/1.43 fof(f1332,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|nil=X0|~segmentP(X1,X0)|~ssList(X1)|~segmentP(nil,X2)|~segmentP(X2,X1)|~ssList(X1)|~ssList(X2)|~ssList(nil)|~sQ13_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f535,f374])).
% 6.99/1.43 fof(f1334,definition,(
% 6.99/1.43 ![X0]: (sQ96_spl <=> (~ssList(X0)|nil=X0|~segmentP(nil,X0)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1338,plain,(
% 6.99/1.43 sQ96_spl|~sQ11_spl|~sQ13_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1331,f1334,f521,f528])).
% 6.99/1.43 fof(f1339,definition,(
% 6.99/1.43 ![X0,X1,X2]: (sQ97_spl <=> (~ssList(X0)|nil=X0|~segmentP(X1,X0)|~ssList(X1)|~segmentP(nil,X2)|~segmentP(X2,X1)|~ssList(X1)|~ssList(X2)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1342,plain,(
% 6.99/1.43 sQ97_spl|~sQ11_spl|~sQ13_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1332,f1339,f521,f528])).
% 6.99/1.43 fof(f1346,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|nil=X0|~rearsegP(nil,X0)|~ssList(nil)|~ssList(nil)|~sQ14_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f559,f257])).
% 6.99/1.43 fof(f1347,plain,(
% 6.99/1.43 ![X0,X1,X2]: (~ssList(X0)|nil=X0|~rearsegP(X1,X0)|~ssList(X1)|~rearsegP(nil,X2)|~rearsegP(X2,X1)|~ssList(X1)|~ssList(X2)|~ssList(nil)|~sQ14_spl)),
% 6.99/1.43 inference(resolution,[status(thm)],[f559,f376])).
% 6.99/1.43 fof(f1349,definition,(
% 6.99/1.43 ![X0]: (sQ98_spl <=> (~ssList(X0)|nil=X0|~rearsegP(nil,X0)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1353,plain,(
% 6.99/1.43 sQ98_spl|~sQ11_spl|~sQ14_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1346,f1349,f521,f554])).
% 6.99/1.43 fof(f1354,definition,(
% 6.99/1.43 ![X0,X1,X2]: (sQ99_spl <=> (~ssList(X0)|nil=X0|~rearsegP(X1,X0)|~ssList(X1)|~rearsegP(nil,X2)|~rearsegP(X2,X1)|~ssList(X1)|~ssList(X2)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1357,plain,(
% 6.99/1.43 sQ99_spl|~sQ11_spl|~sQ14_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1347,f1354,f521,f554])).
% 6.99/1.43 fof(f1478,plain,(
% 6.99/1.43 ~ssList(sk1)|~ssList(sk2)|app(skaf46(sk2,sk1),sk1)=sk2|~sQ9_spl),
% 6.99/1.43 inference(resolution,[status(thm)],[f343,f931])).
% 6.99/1.43 fof(f1479,plain,(
% 6.99/1.43 ~ssList(nil)|~ssList(sk2)|app(skaf46(sk2,nil),nil)=sk2|~sQ26_spl),
% 6.99/1.43 inference(resolution,[status(thm)],[f343,f744])).
% 6.99/1.43 fof(f1480,plain,(
% 6.99/1.43 ~ssList(sk2)|~ssList(sk2)|app(skaf46(sk2,sk2),sk2)=sk2|~sQ28_spl),
% 6.99/1.43 inference(resolution,[status(thm)],[f343,f752])).
% 6.99/1.43 fof(f1481,plain,(
% 6.99/1.43 ~ssList(nil)|~ssList(nil)|app(skaf46(nil,nil),nil)=nil|~sQ30_spl),
% 6.99/1.43 inference(resolution,[status(thm)],[f343,f760])).
% 6.99/1.43 fof(f1482,plain,(
% 6.99/1.43 ~ssList(sk1)|~ssList(sk1)|app(skaf46(sk1,sk1),sk1)=sk1|~sQ29_spl),
% 6.99/1.43 inference(resolution,[status(thm)],[f343,f756])).
% 6.99/1.43 fof(f1483,plain,(
% 6.99/1.43 ~ssList(nil)|~ssList(sk1)|app(skaf46(sk1,nil),nil)=sk1|~sQ27_spl),
% 6.99/1.43 inference(resolution,[status(thm)],[f343,f748])).
% 6.99/1.43 fof(f1486,plain,(
% 6.99/1.43 ![X0]: (~ssList(nil)|~ssList(X0)|app(skaf46(X0,nil),nil)=X0|~ssList(X0))),
% 6.99/1.43 inference(resolution,[status(thm)],[f343,f257])).
% 6.99/1.43 fof(f1489,definition,(
% 6.99/1.43 sQ106_spl <=> (app(skaf46(sk2,sk1),sk1)=sk2)),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1490,plain,(
% 6.99/1.43 app(skaf46(sk2,sk1),sk1)=sk2|~sQ106_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1489])).
% 6.99/1.43 fof(f1492,plain,(
% 6.99/1.43 ~sQ19_spl|~sQ16_spl|sQ106_spl|~sQ9_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1478,f594,f573,f1489,f477])).
% 6.99/1.43 fof(f1493,definition,(
% 6.99/1.43 sQ107_spl <=> (app(skaf46(sk2,nil),nil)=sk2)),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1494,plain,(
% 6.99/1.43 app(skaf46(sk2,nil),nil)=sk2|~sQ107_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1493])).
% 6.99/1.43 fof(f1496,plain,(
% 6.99/1.43 ~sQ11_spl|~sQ16_spl|sQ107_spl|~sQ26_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1479,f521,f573,f1493,f743])).
% 6.99/1.43 fof(f1497,definition,(
% 6.99/1.43 sQ108_spl <=> (app(skaf46(sk2,sk2),sk2)=sk2)),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1498,plain,(
% 6.99/1.43 app(skaf46(sk2,sk2),sk2)=sk2|~sQ108_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1497])).
% 6.99/1.43 fof(f1500,plain,(
% 6.99/1.43 ~sQ16_spl|sQ108_spl|~sQ28_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1480,f573,f1497,f751])).
% 6.99/1.43 fof(f1501,definition,(
% 6.99/1.43 sQ109_spl <=> (app(skaf46(nil,nil),nil)=nil)),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1502,plain,(
% 6.99/1.43 app(skaf46(nil,nil),nil)=nil|~sQ109_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1501])).
% 6.99/1.43 fof(f1504,plain,(
% 6.99/1.43 ~sQ11_spl|sQ109_spl|~sQ30_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1481,f521,f1501,f759])).
% 6.99/1.43 fof(f1505,definition,(
% 6.99/1.43 sQ110_spl <=> (app(skaf46(sk1,sk1),sk1)=sk1)),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1506,plain,(
% 6.99/1.43 app(skaf46(sk1,sk1),sk1)=sk1|~sQ110_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1505])).
% 6.99/1.43 fof(f1508,plain,(
% 6.99/1.43 ~sQ19_spl|sQ110_spl|~sQ29_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1482,f594,f1505,f755])).
% 6.99/1.43 fof(f1509,definition,(
% 6.99/1.43 sQ111_spl <=> (app(skaf46(sk1,nil),nil)=sk1)),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1510,plain,(
% 6.99/1.43 app(skaf46(sk1,nil),nil)=sk1|~sQ111_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1509])).
% 6.99/1.43 fof(f1512,plain,(
% 6.99/1.43 ~sQ11_spl|~sQ19_spl|sQ111_spl|~sQ27_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1483,f521,f594,f1509,f747])).
% 6.99/1.43 fof(f1517,definition,(
% 6.99/1.43 ![X0]: (sQ112_spl <=> (~ssList(X0)|app(skaf46(X0,nil),nil)=X0|~ssList(X0)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1520,plain,(
% 6.99/1.43 ~sQ11_spl|sQ112_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1486,f521,f1517])).
% 6.99/1.43 fof(f1560,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|app(skaf46(sk2,nil),nil)=X0|~rearsegP(nil,X0)|~ssList(skaf46(sk2,nil))|~ssList(nil)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)|~sQ107_spl)),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f1494,f1203])).
% 6.99/1.43 fof(f1562,plain,(
% 6.99/1.43 ![X0]: (~rearsegP(X0,sk2)|~ssList(X0)|app(skaf46(sk2,nil),nil)=X0|~rearsegP(nil,X0)|~ssList(skaf46(sk2,nil))|~ssList(nil)|~sQ107_spl)),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f1494,f686])).
% 6.99/1.43 fof(f1563,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|~ssList(skaf46(sk2,nil))|~ssList(nil)|~ssList(app(sk2,X0))|segmentP(app(app(skaf46(sk2,nil),nil),X0),nil)|~sQ107_spl)),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f1494,f504])).
% 6.99/1.43 fof(f1569,definition,(
% 6.99/1.43 sQ113_spl <=> (ssList(skaf46(sk2,nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1571,plain,(
% 6.99/1.43 ~ssList(skaf46(sk2,nil))|sQ113_spl),
% 6.99/1.43 inference(component_clause,[status(thm)],[f1569])).
% 6.99/1.43 fof(f1577,definition,(
% 6.99/1.43 ![X0,X1]: (sQ115_spl <=> (~ssList(X0)|app(skaf46(sk2,nil),nil)=X0|~rearsegP(nil,X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1580,plain,(
% 6.99/1.43 sQ115_spl|~sQ113_spl|~sQ11_spl|~sQ107_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1560,f1577,f1569,f521,f1493])).
% 6.99/1.43 fof(f1582,definition,(
% 6.99/1.43 ![X0]: (sQ116_spl <=> (~rearsegP(X0,sk2)|~ssList(X0)|app(skaf46(sk2,nil),nil)=X0|~rearsegP(nil,X0)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1585,plain,(
% 6.99/1.43 sQ116_spl|~sQ113_spl|~sQ11_spl|~sQ107_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1562,f1582,f1569,f521,f1493])).
% 6.99/1.43 fof(f1586,definition,(
% 6.99/1.43 ![X0]: (sQ117_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(skaf46(sk2,nil),nil),X0),nil)))),
% 6.99/1.43 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 6.99/1.43 fof(f1589,plain,(
% 6.99/1.43 sQ117_spl|~sQ113_spl|~sQ11_spl|~sQ107_spl),
% 6.99/1.43 inference(split_clause,[status(thm)],[f1563,f1586,f1569,f521,f1493])).
% 6.99/1.43 fof(f1595,plain,(
% 6.99/1.43 $false|sQ113_spl),
% 6.99/1.43 inference(forward_subsumption_resolution,[status(thm)],[f1571,f249])).
% 6.99/1.43 fof(f1596,plain,(
% 6.99/1.43 sQ113_spl),
% 6.99/1.43 inference(contradiction_clause,[status(thm)],[f1595])).
% 6.99/1.43 fof(f1602,plain,(
% 6.99/1.43 ![X0,X1]: (~ssList(X0)|app(skaf46(sk1,nil),nil)=X0|~rearsegP(nil,X0)|~ssList(skaf46(sk1,nil))|~ssList(nil)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)|~sQ111_spl)),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f1510,f1203])).
% 6.99/1.43 fof(f1604,plain,(
% 6.99/1.43 ![X0]: (~rearsegP(X0,sk1)|~ssList(X0)|app(skaf46(sk1,nil),nil)=X0|~rearsegP(nil,X0)|~ssList(skaf46(sk1,nil))|~ssList(nil)|~sQ111_spl)),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f1510,f686])).
% 6.99/1.43 fof(f1605,plain,(
% 6.99/1.43 ![X0]: (~ssList(X0)|~ssList(skaf46(sk1,nil))|~ssList(nil)|~ssList(app(sk1,X0))|segmentP(app(app(skaf46(sk1,nil),nil),X0),nil)|~sQ111_spl)),
% 6.99/1.43 inference(paramodulation,[status(thm)],[f1510,f504])).
% 6.99/1.43 fof(f1611,definition,(
% 4.89/1.43 sQ118_spl <=> (ssList(skaf46(sk1,nil)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1613,plain,(
% 4.89/1.43 ~ssList(skaf46(sk1,nil))|sQ118_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f1611])).
% 4.89/1.43 fof(f1619,definition,(
% 4.89/1.43 ![X0,X1]: (sQ120_spl <=> (~ssList(X0)|app(skaf46(sk1,nil),nil)=X0|~rearsegP(nil,X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1622,plain,(
% 4.89/1.43 sQ120_spl|~sQ118_spl|~sQ11_spl|~sQ111_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1602,f1619,f1611,f521,f1509])).
% 4.89/1.43 fof(f1624,definition,(
% 4.89/1.43 ![X0]: (sQ121_spl <=> (~rearsegP(X0,sk1)|~ssList(X0)|app(skaf46(sk1,nil),nil)=X0|~rearsegP(nil,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1627,plain,(
% 4.89/1.43 sQ121_spl|~sQ118_spl|~sQ11_spl|~sQ111_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1604,f1624,f1611,f521,f1509])).
% 4.89/1.43 fof(f1628,definition,(
% 4.89/1.43 ![X0]: (sQ122_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(skaf46(sk1,nil),nil),X0),nil)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1631,plain,(
% 4.89/1.43 sQ122_spl|~sQ118_spl|~sQ11_spl|~sQ111_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1605,f1628,f1611,f521,f1509])).
% 4.89/1.43 fof(f1637,plain,(
% 4.89/1.43 $false|sQ118_spl),
% 4.89/1.43 inference(forward_subsumption_resolution,[status(thm)],[f1613,f249])).
% 4.89/1.43 fof(f1638,plain,(
% 4.89/1.43 sQ118_spl),
% 4.89/1.43 inference(contradiction_clause,[status(thm)],[f1637])).
% 4.89/1.43 fof(f1652,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(X0)|app(skaf46(sk2,sk2),sk2)=X0|~rearsegP(sk2,X0)|~ssList(skaf46(sk2,sk2))|~ssList(sk2)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)|~sQ108_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f1498,f1203])).
% 4.89/1.43 fof(f1654,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk2)|~ssList(X0)|app(skaf46(sk2,sk2),sk2)=X0|~rearsegP(sk2,X0)|~ssList(skaf46(sk2,sk2))|~ssList(sk2)|~sQ108_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f1498,f686])).
% 4.89/1.43 fof(f1655,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(skaf46(sk2,sk2))|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(skaf46(sk2,sk2),sk2),X0),sk2)|~sQ108_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f1498,f504])).
% 4.89/1.43 fof(f1661,definition,(
% 4.89/1.43 sQ124_spl <=> (ssList(skaf46(sk2,sk2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1663,plain,(
% 4.89/1.43 ~ssList(skaf46(sk2,sk2))|sQ124_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f1661])).
% 4.89/1.43 fof(f1666,definition,(
% 4.89/1.43 ![X0,X1]: (sQ125_spl <=> (~ssList(X0)|app(skaf46(sk2,sk2),sk2)=X0|~rearsegP(sk2,X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1669,plain,(
% 4.89/1.43 sQ125_spl|~sQ124_spl|~sQ16_spl|~sQ108_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1652,f1666,f1661,f573,f1497])).
% 4.89/1.43 fof(f1671,definition,(
% 4.89/1.43 ![X0]: (sQ126_spl <=> (~rearsegP(X0,sk2)|~ssList(X0)|app(skaf46(sk2,sk2),sk2)=X0|~rearsegP(sk2,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1674,plain,(
% 4.89/1.43 sQ126_spl|~sQ124_spl|~sQ16_spl|~sQ108_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1654,f1671,f1661,f573,f1497])).
% 4.89/1.43 fof(f1675,definition,(
% 4.89/1.43 ![X0]: (sQ127_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(skaf46(sk2,sk2),sk2),X0),sk2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1678,plain,(
% 4.89/1.43 sQ127_spl|~sQ124_spl|~sQ16_spl|~sQ108_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1655,f1675,f1661,f573,f1497])).
% 4.89/1.43 fof(f1684,plain,(
% 4.89/1.43 $false|sQ124_spl),
% 4.89/1.43 inference(forward_subsumption_resolution,[status(thm)],[f1663,f249])).
% 4.89/1.43 fof(f1685,plain,(
% 4.89/1.43 sQ124_spl),
% 4.89/1.43 inference(contradiction_clause,[status(thm)],[f1684])).
% 4.89/1.43 fof(f1691,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(X0)|app(skaf46(sk1,sk1),sk1)=X0|~rearsegP(sk1,X0)|~ssList(skaf46(sk1,sk1))|~ssList(sk1)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)|~sQ110_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f1506,f1203])).
% 4.89/1.43 fof(f1693,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk1)|~ssList(X0)|app(skaf46(sk1,sk1),sk1)=X0|~rearsegP(sk1,X0)|~ssList(skaf46(sk1,sk1))|~ssList(sk1)|~sQ110_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f1506,f686])).
% 4.89/1.43 fof(f1694,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(skaf46(sk1,sk1))|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(skaf46(sk1,sk1),sk1),X0),sk1)|~sQ110_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f1506,f504])).
% 4.89/1.43 fof(f1700,definition,(
% 4.89/1.43 sQ128_spl <=> (ssList(skaf46(sk1,sk1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1702,plain,(
% 4.89/1.43 ~ssList(skaf46(sk1,sk1))|sQ128_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f1700])).
% 4.89/1.43 fof(f1705,definition,(
% 4.89/1.43 ![X0,X1]: (sQ129_spl <=> (~ssList(X0)|app(skaf46(sk1,sk1),sk1)=X0|~rearsegP(sk1,X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1708,plain,(
% 4.89/1.43 sQ129_spl|~sQ128_spl|~sQ19_spl|~sQ110_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1691,f1705,f1700,f594,f1505])).
% 4.89/1.43 fof(f1710,definition,(
% 4.89/1.43 ![X0]: (sQ130_spl <=> (~rearsegP(X0,sk1)|~ssList(X0)|app(skaf46(sk1,sk1),sk1)=X0|~rearsegP(sk1,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1713,plain,(
% 4.89/1.43 sQ130_spl|~sQ128_spl|~sQ19_spl|~sQ110_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1693,f1710,f1700,f594,f1505])).
% 4.89/1.43 fof(f1714,definition,(
% 4.89/1.43 ![X0]: (sQ131_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(skaf46(sk1,sk1),sk1),X0),sk1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1717,plain,(
% 4.89/1.43 sQ131_spl|~sQ128_spl|~sQ19_spl|~sQ110_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1694,f1714,f1700,f594,f1505])).
% 4.89/1.43 fof(f1723,plain,(
% 4.89/1.43 $false|sQ128_spl),
% 4.89/1.43 inference(forward_subsumption_resolution,[status(thm)],[f1702,f249])).
% 4.89/1.43 fof(f1724,plain,(
% 4.89/1.43 sQ128_spl),
% 4.89/1.43 inference(contradiction_clause,[status(thm)],[f1723])).
% 4.89/1.43 fof(f1730,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(X0)|app(skaf46(nil,nil),nil)=X0|~rearsegP(nil,X0)|~ssList(skaf46(nil,nil))|~ssList(nil)|~rearsegP(X0,X1)|~rearsegP(X1,nil)|~ssList(X1)|~sQ109_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f1502,f1203])).
% 4.89/1.43 fof(f1732,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,nil)|~ssList(X0)|app(skaf46(nil,nil),nil)=X0|~rearsegP(nil,X0)|~ssList(skaf46(nil,nil))|~ssList(nil)|~sQ109_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f1502,f686])).
% 4.89/1.43 fof(f1733,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(skaf46(nil,nil))|~ssList(nil)|~ssList(app(nil,X0))|segmentP(app(app(skaf46(nil,nil),nil),X0),nil)|~sQ109_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f1502,f504])).
% 4.89/1.43 fof(f1739,definition,(
% 4.89/1.43 sQ132_spl <=> (ssList(skaf46(nil,nil)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1741,plain,(
% 4.89/1.43 ~ssList(skaf46(nil,nil))|sQ132_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f1739])).
% 4.89/1.43 fof(f1744,definition,(
% 4.89/1.43 ![X0,X1]: (sQ133_spl <=> (~ssList(X0)|app(skaf46(nil,nil),nil)=X0|~rearsegP(nil,X0)|~rearsegP(X0,X1)|~rearsegP(X1,nil)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1747,plain,(
% 4.89/1.43 sQ133_spl|~sQ132_spl|~sQ11_spl|~sQ109_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1730,f1744,f1739,f521,f1501])).
% 4.89/1.43 fof(f1749,definition,(
% 4.89/1.43 ![X0]: (sQ134_spl <=> (~rearsegP(X0,nil)|~ssList(X0)|app(skaf46(nil,nil),nil)=X0|~rearsegP(nil,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1752,plain,(
% 4.89/1.43 sQ134_spl|~sQ132_spl|~sQ11_spl|~sQ109_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1732,f1749,f1739,f521,f1501])).
% 4.89/1.43 fof(f1753,definition,(
% 4.89/1.43 ![X0]: (sQ135_spl <=> (~ssList(X0)|~ssList(app(nil,X0))|segmentP(app(app(skaf46(nil,nil),nil),X0),nil)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1756,plain,(
% 4.89/1.43 sQ135_spl|~sQ132_spl|~sQ11_spl|~sQ109_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f1733,f1753,f1739,f521,f1501])).
% 4.89/1.43 fof(f1762,plain,(
% 4.89/1.43 $false|sQ132_spl),
% 4.89/1.43 inference(forward_subsumption_resolution,[status(thm)],[f1741,f249])).
% 4.89/1.43 fof(f1763,plain,(
% 4.89/1.43 sQ132_spl),
% 4.89/1.43 inference(contradiction_clause,[status(thm)],[f1762])).
% 4.89/1.43 fof(f1778,definition,(
% 4.89/1.43 sQ136_spl <=> (ssList(skaf46(sk2,sk1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f1780,plain,(
% 4.89/1.43 ~ssList(skaf46(sk2,sk1))|sQ136_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f1778])).
% 4.89/1.43 fof(f1813,plain,(
% 4.89/1.43 $false|sQ136_spl),
% 4.89/1.43 inference(forward_subsumption_resolution,[status(thm)],[f1780,f249])).
% 4.89/1.43 fof(f1814,plain,(
% 4.89/1.43 sQ136_spl),
% 4.89/1.43 inference(contradiction_clause,[status(thm)],[f1813])).
% 4.89/1.43 fof(f2049,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(X0)|app(X0,skaf45(X0,X0))=X0|~ssList(X0))),
% 4.89/1.43 inference(resolution,[status(thm)],[f344,f260])).
% 4.89/1.43 fof(f2050,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|app(X0,skaf45(X0,X0))=X0)),
% 4.89/1.43 inference(duplicate_literals_removal,[status(thm)],[f2049])).
% 4.89/1.43 fof(f2062,plain,(
% 4.89/1.43 app(sk2,skaf45(sk2,sk2))=sk2),
% 4.89/1.43 inference(resolution,[status(thm)],[f2050,f431])).
% 4.89/1.43 fof(f2067,plain,(
% 4.89/1.43 app(sk1,skaf45(sk1,sk1))=sk1),
% 4.89/1.43 inference(resolution,[status(thm)],[f2050,f430])).
% 4.89/1.43 fof(f2076,plain,(
% 4.89/1.43 app(nil,skaf45(nil,nil))=nil),
% 4.89/1.43 inference(resolution,[status(thm)],[f2050,f207])).
% 4.89/1.43 fof(f2078,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(sk2)|~ssList(skaf45(sk2,sk2))|app(sk2,skaf45(sk2,sk2))=skaf45(sk2,sk2)|~rearsegP(skaf45(sk2,sk2),X0)|~ssList(X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2062,f1241])).
% 4.89/1.43 fof(f2079,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(X0)|app(sk2,skaf45(sk2,sk2))=X0|~rearsegP(skaf45(sk2,sk2),X0)|~ssList(sk2)|~ssList(skaf45(sk2,sk2))|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2062,f1203])).
% 4.89/1.43 fof(f2080,plain,(
% 4.89/1.43 ![X0]: (~ssList(sk2)|~ssList(skaf45(sk2,sk2))|app(sk2,skaf45(sk2,sk2))=skaf45(sk2,sk2)|~rearsegP(skaf45(sk2,sk2),X0)|~rearsegP(X0,sk2)|~ssList(X0))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2062,f822])).
% 4.89/1.43 fof(f2081,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk2)|~ssList(X0)|app(sk2,skaf45(sk2,sk2))=X0|~rearsegP(skaf45(sk2,sk2),X0)|~ssList(sk2)|~ssList(skaf45(sk2,sk2)))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2062,f686])).
% 4.89/1.43 fof(f2082,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(sk2)|~ssList(skaf45(sk2,sk2))|~ssList(app(sk2,X0))|segmentP(app(app(sk2,skaf45(sk2,sk2)),X0),skaf45(sk2,sk2)))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2062,f504])).
% 4.89/1.43 fof(f2084,plain,(
% 4.89/1.43 ~ssList(sk2)|~ssList(skaf45(sk2,sk2))|~rearsegP(skaf45(sk2,sk2),sk2)|app(sk2,skaf45(sk2,sk2))=skaf45(sk2,sk2)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2062,f742])).
% 4.89/1.43 fof(f2085,plain,(
% 4.89/1.43 ~ssList(sk2)|~ssList(skaf45(sk2,sk2))|rearsegP(sk2,skaf45(sk2,sk2))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2062,f734])).
% 4.89/1.43 fof(f2087,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(skaf45(sk2,sk2),X0)|~ssList(sk2)|~ssList(X0)|~ssList(skaf45(sk2,sk2))|rearsegP(sk2,X0))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2062,f350])).
% 4.89/1.43 fof(f2088,definition,(
% 4.89/1.43 sQ154_spl <=> (ssList(skaf45(sk2,sk2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2090,plain,(
% 4.89/1.43 ~ssList(skaf45(sk2,sk2))|sQ154_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f2088])).
% 4.89/1.43 fof(f2092,definition,(
% 4.89/1.43 sQ155_spl <=> (app(sk2,skaf45(sk2,sk2))=skaf45(sk2,sk2))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2093,plain,(
% 4.89/1.43 app(sk2,skaf45(sk2,sk2))=skaf45(sk2,sk2)|~sQ155_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f2092])).
% 4.89/1.43 fof(f2095,definition,(
% 4.89/1.43 ![X0,X1]: (sQ156_spl <=> (~rearsegP(skaf45(sk2,sk2),X0)|~ssList(X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2098,plain,(
% 4.89/1.43 ~sQ16_spl|~sQ154_spl|sQ155_spl|sQ156_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2078,f573,f2088,f2092,f2095])).
% 4.89/1.43 fof(f2099,definition,(
% 4.89/1.43 ![X0,X1]: (sQ157_spl <=> (~ssList(X0)|app(sk2,skaf45(sk2,sk2))=X0|~rearsegP(skaf45(sk2,sk2),X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2102,plain,(
% 4.89/1.43 sQ157_spl|~sQ16_spl|~sQ154_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2079,f2099,f573,f2088])).
% 4.89/1.43 fof(f2103,definition,(
% 4.89/1.43 ![X0]: (sQ158_spl <=> (~rearsegP(skaf45(sk2,sk2),X0)|~rearsegP(X0,sk2)|~ssList(X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2106,plain,(
% 4.89/1.43 ~sQ16_spl|~sQ154_spl|sQ155_spl|sQ158_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2080,f573,f2088,f2092,f2103])).
% 4.89/1.43 fof(f2107,definition,(
% 4.89/1.43 ![X0]: (sQ159_spl <=> (~rearsegP(X0,sk2)|~ssList(X0)|app(sk2,skaf45(sk2,sk2))=X0|~rearsegP(skaf45(sk2,sk2),X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2110,plain,(
% 4.89/1.43 sQ159_spl|~sQ16_spl|~sQ154_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2081,f2107,f573,f2088])).
% 4.89/1.43 fof(f2111,definition,(
% 4.89/1.43 ![X0]: (sQ160_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,skaf45(sk2,sk2)),X0),skaf45(sk2,sk2))))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2114,plain,(
% 4.89/1.43 sQ160_spl|~sQ16_spl|~sQ154_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2082,f2111,f573,f2088])).
% 4.89/1.43 fof(f2116,definition,(
% 4.89/1.43 sQ161_spl <=> (rearsegP(skaf45(sk2,sk2),sk2))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2119,plain,(
% 4.89/1.43 ~sQ16_spl|~sQ154_spl|~sQ161_spl|sQ155_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2084,f573,f2088,f2116,f2092])).
% 4.89/1.43 fof(f2120,definition,(
% 4.89/1.43 sQ162_spl <=> (rearsegP(sk2,skaf45(sk2,sk2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2121,plain,(
% 4.89/1.43 rearsegP(sk2,skaf45(sk2,sk2))|~sQ162_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f2120])).
% 4.89/1.43 fof(f2123,plain,(
% 4.89/1.43 ~sQ16_spl|~sQ154_spl|sQ162_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2085,f573,f2088,f2120])).
% 4.89/1.43 fof(f2125,definition,(
% 4.89/1.43 ![X0]: (sQ163_spl <=> (~rearsegP(skaf45(sk2,sk2),X0)|~ssList(X0)|rearsegP(sk2,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2128,plain,(
% 4.89/1.43 sQ163_spl|~sQ16_spl|~sQ154_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2087,f2125,f573,f2088])).
% 4.89/1.43 fof(f2129,plain,(
% 4.89/1.43 $false|sQ154_spl),
% 4.89/1.43 inference(forward_subsumption_resolution,[status(thm)],[f2090,f250])).
% 4.89/1.43 fof(f2130,plain,(
% 4.89/1.43 sQ154_spl),
% 4.89/1.43 inference(contradiction_clause,[status(thm)],[f2129])).
% 4.89/1.43 fof(f2131,plain,(
% 4.89/1.43 sk2=skaf45(sk2,sk2)|~sQ155_spl),
% 4.89/1.43 inference(forward_demodulation,[status(thm)],[f2062,f2093])).
% 4.89/1.43 fof(f2135,plain,(
% 4.89/1.43 app(sk2,sk2)=sk2|~sQ155_spl),
% 4.89/1.43 inference(backward_demodulation,[status(thm)],[f2131,f2062])).
% 4.89/1.43 fof(f2140,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(X0)|app(sk2,sk2)=X0|~rearsegP(sk2,X0)|~ssList(sk2)|~ssList(sk2)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)|~sQ155_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2135,f1203])).
% 4.89/1.43 fof(f2142,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk2)|~ssList(X0)|app(sk2,sk2)=X0|~rearsegP(sk2,X0)|~ssList(sk2)|~ssList(sk2)|~sQ155_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2135,f686])).
% 4.89/1.43 fof(f2143,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(sk2)|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,sk2),X0),sk2)|~sQ155_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2135,f504])).
% 4.89/1.43 fof(f2145,plain,(
% 4.89/1.43 ~ssList(sk2)|~ssList(sk2)|~rearsegP(sk2,sk2)|app(sk2,sk2)=sk2|~sQ155_spl),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2135,f742])).
% 4.89/1.43 fof(f2151,definition,(
% 4.89/1.43 sQ164_spl <=> (app(sk2,sk2)=sk2)),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2155,definition,(
% 4.89/1.43 ![X0,X1]: (sQ165_spl <=> (~ssList(X0)|app(sk2,sk2)=X0|~rearsegP(sk2,X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2158,plain,(
% 4.89/1.43 sQ165_spl|~sQ16_spl|~sQ155_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2140,f2155,f573,f2092])).
% 4.89/1.43 fof(f2160,definition,(
% 4.89/1.43 ![X0]: (sQ166_spl <=> (~rearsegP(X0,sk2)|~ssList(X0)|app(sk2,sk2)=X0|~rearsegP(sk2,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2163,plain,(
% 4.89/1.43 sQ166_spl|~sQ16_spl|~sQ155_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2142,f2160,f573,f2092])).
% 4.89/1.43 fof(f2164,definition,(
% 4.89/1.43 ![X0]: (sQ167_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,sk2),X0),sk2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2167,plain,(
% 4.89/1.43 sQ167_spl|~sQ16_spl|~sQ155_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2143,f2164,f573,f2092])).
% 4.89/1.43 fof(f2169,plain,(
% 4.89/1.43 ~sQ16_spl|~sQ28_spl|sQ164_spl|~sQ155_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2145,f573,f751,f2151,f2092])).
% 4.89/1.43 fof(f2173,plain,(
% 4.89/1.43 ~ssList(skaf45(sk2,sk2))|~ssList(sk2)|app(skaf46(sk2,skaf45(sk2,sk2)),skaf45(sk2,sk2))=sk2|~sQ162_spl),
% 4.89/1.43 inference(resolution,[status(thm)],[f2121,f343])).
% 4.89/1.43 fof(f2174,plain,(
% 4.89/1.43 ~rearsegP(skaf45(sk2,sk2),sk2)|~ssList(skaf45(sk2,sk2))|~ssList(sk2)|sk2=skaf45(sk2,sk2)|~sQ162_spl),
% 4.89/1.43 inference(resolution,[status(thm)],[f2121,f340])).
% 4.89/1.43 fof(f2175,definition,(
% 4.89/1.43 sQ168_spl <=> (app(skaf46(sk2,skaf45(sk2,sk2)),skaf45(sk2,sk2))=sk2)),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2178,plain,(
% 4.89/1.43 ~sQ154_spl|~sQ16_spl|sQ168_spl|~sQ162_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2173,f2088,f573,f2175,f2120])).
% 4.89/1.43 fof(f2179,definition,(
% 4.89/1.43 sQ169_spl <=> (sk2=skaf45(sk2,sk2))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2182,plain,(
% 4.89/1.43 ~sQ161_spl|~sQ154_spl|~sQ16_spl|sQ169_spl|~sQ162_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2174,f2116,f2088,f573,f2179,f2120])).
% 4.89/1.43 fof(f2211,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(X0)|app(sk1,skaf45(sk1,sk1))=X0|~rearsegP(skaf45(sk1,sk1),X0)|~ssList(sk1)|~ssList(skaf45(sk1,sk1))|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2067,f1203])).
% 4.89/1.43 fof(f2213,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk1)|~ssList(X0)|app(sk1,skaf45(sk1,sk1))=X0|~rearsegP(skaf45(sk1,sk1),X0)|~ssList(sk1)|~ssList(skaf45(sk1,sk1)))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2067,f686])).
% 4.89/1.43 fof(f2214,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(skaf45(sk1,sk1))|~ssList(app(sk1,X0))|segmentP(app(app(sk1,skaf45(sk1,sk1)),X0),skaf45(sk1,sk1)))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2067,f504])).
% 4.89/1.43 fof(f2216,plain,(
% 4.89/1.43 ~ssList(sk1)|~ssList(skaf45(sk1,sk1))|~rearsegP(skaf45(sk1,sk1),sk1)|app(sk1,skaf45(sk1,sk1))=skaf45(sk1,sk1)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2067,f742])).
% 4.89/1.43 fof(f2217,plain,(
% 4.89/1.43 ~ssList(sk1)|~ssList(skaf45(sk1,sk1))|rearsegP(sk1,skaf45(sk1,sk1))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2067,f734])).
% 4.89/1.43 fof(f2219,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(skaf45(sk1,sk1),X0)|~ssList(sk1)|~ssList(X0)|~ssList(skaf45(sk1,sk1))|rearsegP(sk1,X0))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2067,f350])).
% 4.89/1.43 fof(f2220,definition,(
% 4.89/1.43 sQ170_spl <=> (ssList(skaf45(sk1,sk1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2222,plain,(
% 4.89/1.43 ~ssList(skaf45(sk1,sk1))|sQ170_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f2220])).
% 4.89/1.43 fof(f2224,definition,(
% 4.89/1.43 sQ171_spl <=> (app(sk1,skaf45(sk1,sk1))=skaf45(sk1,sk1))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2225,plain,(
% 4.89/1.43 app(sk1,skaf45(sk1,sk1))=skaf45(sk1,sk1)|~sQ171_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f2224])).
% 4.89/1.43 fof(f2231,definition,(
% 4.89/1.43 ![X0,X1]: (sQ173_spl <=> (~ssList(X0)|app(sk1,skaf45(sk1,sk1))=X0|~rearsegP(skaf45(sk1,sk1),X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2234,plain,(
% 4.89/1.43 sQ173_spl|~sQ19_spl|~sQ170_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2211,f2231,f594,f2220])).
% 4.89/1.43 fof(f2239,definition,(
% 4.89/1.43 ![X0]: (sQ175_spl <=> (~rearsegP(X0,sk1)|~ssList(X0)|app(sk1,skaf45(sk1,sk1))=X0|~rearsegP(skaf45(sk1,sk1),X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2242,plain,(
% 4.89/1.43 sQ175_spl|~sQ19_spl|~sQ170_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2213,f2239,f594,f2220])).
% 4.89/1.43 fof(f2243,definition,(
% 4.89/1.43 ![X0]: (sQ176_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,skaf45(sk1,sk1)),X0),skaf45(sk1,sk1))))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2246,plain,(
% 4.89/1.43 sQ176_spl|~sQ19_spl|~sQ170_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2214,f2243,f594,f2220])).
% 4.89/1.43 fof(f2248,definition,(
% 4.89/1.43 sQ177_spl <=> (rearsegP(skaf45(sk1,sk1),sk1))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2251,plain,(
% 4.89/1.43 ~sQ19_spl|~sQ170_spl|~sQ177_spl|sQ171_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2216,f594,f2220,f2248,f2224])).
% 4.89/1.43 fof(f2252,definition,(
% 4.89/1.43 sQ178_spl <=> (rearsegP(sk1,skaf45(sk1,sk1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2253,plain,(
% 4.89/1.43 rearsegP(sk1,skaf45(sk1,sk1))|~sQ178_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f2252])).
% 4.89/1.43 fof(f2255,plain,(
% 4.89/1.43 ~sQ19_spl|~sQ170_spl|sQ178_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2217,f594,f2220,f2252])).
% 4.89/1.43 fof(f2257,definition,(
% 4.89/1.43 ![X0]: (sQ179_spl <=> (~rearsegP(skaf45(sk1,sk1),X0)|~ssList(X0)|rearsegP(sk1,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2260,plain,(
% 4.89/1.43 sQ179_spl|~sQ19_spl|~sQ170_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2219,f2257,f594,f2220])).
% 4.89/1.43 fof(f2261,plain,(
% 4.89/1.43 $false|sQ170_spl),
% 4.89/1.43 inference(forward_subsumption_resolution,[status(thm)],[f2222,f250])).
% 4.89/1.43 fof(f2262,plain,(
% 4.89/1.43 sQ170_spl),
% 4.89/1.43 inference(contradiction_clause,[status(thm)],[f2261])).
% 4.89/1.43 fof(f2263,plain,(
% 4.89/1.43 sk1=skaf45(sk1,sk1)|~sQ171_spl),
% 4.89/1.43 inference(forward_demodulation,[status(thm)],[f2067,f2225])).
% 4.89/1.43 fof(f2267,plain,(
% 4.89/1.43 app(sk1,sk1)=sk1|~sQ171_spl),
% 4.89/1.43 inference(backward_demodulation,[status(thm)],[f2263,f2067])).
% 4.89/1.43 fof(f2373,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(X0)|app(sk1,sk1)=X0|~rearsegP(sk1,X0)|~ssList(sk1)|~ssList(sk1)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)|~sQ171_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2267,f1203])).
% 4.89/1.43 fof(f2375,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk1)|~ssList(X0)|app(sk1,sk1)=X0|~rearsegP(sk1,X0)|~ssList(sk1)|~ssList(sk1)|~sQ171_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2267,f686])).
% 4.89/1.43 fof(f2376,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,sk1),X0),sk1)|~sQ171_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2267,f504])).
% 4.89/1.43 fof(f2378,plain,(
% 4.89/1.43 ~ssList(sk1)|~ssList(sk1)|~rearsegP(sk1,sk1)|app(sk1,sk1)=sk1|~sQ171_spl),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2267,f742])).
% 4.89/1.43 fof(f2384,definition,(
% 4.89/1.43 sQ181_spl <=> (app(sk1,sk1)=sk1)),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2388,definition,(
% 4.89/1.43 ![X0,X1]: (sQ182_spl <=> (~ssList(X0)|app(sk1,sk1)=X0|~rearsegP(sk1,X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2391,plain,(
% 4.89/1.43 sQ182_spl|~sQ19_spl|~sQ171_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2373,f2388,f594,f2224])).
% 4.89/1.43 fof(f2393,definition,(
% 4.89/1.43 ![X0]: (sQ183_spl <=> (~rearsegP(X0,sk1)|~ssList(X0)|app(sk1,sk1)=X0|~rearsegP(sk1,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2396,plain,(
% 4.89/1.43 sQ183_spl|~sQ19_spl|~sQ171_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2375,f2393,f594,f2224])).
% 4.89/1.43 fof(f2397,definition,(
% 4.89/1.43 ![X0]: (sQ184_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,sk1),X0),sk1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2400,plain,(
% 4.89/1.43 sQ184_spl|~sQ19_spl|~sQ171_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2376,f2397,f594,f2224])).
% 4.89/1.43 fof(f2402,plain,(
% 4.89/1.43 ~sQ19_spl|~sQ29_spl|sQ181_spl|~sQ171_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2378,f594,f755,f2384,f2224])).
% 4.89/1.43 fof(f2450,plain,(
% 4.89/1.43 ~ssList(skaf45(sk1,sk1))|~ssList(sk1)|app(skaf46(sk1,skaf45(sk1,sk1)),skaf45(sk1,sk1))=sk1|~sQ178_spl),
% 4.89/1.43 inference(resolution,[status(thm)],[f2253,f343])).
% 4.89/1.43 fof(f2451,plain,(
% 4.89/1.43 ~rearsegP(skaf45(sk1,sk1),sk1)|~ssList(skaf45(sk1,sk1))|~ssList(sk1)|sk1=skaf45(sk1,sk1)|~sQ178_spl),
% 4.89/1.43 inference(resolution,[status(thm)],[f2253,f340])).
% 4.89/1.43 fof(f2452,definition,(
% 4.89/1.43 sQ185_spl <=> (app(skaf46(sk1,skaf45(sk1,sk1)),skaf45(sk1,sk1))=sk1)),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2455,plain,(
% 4.89/1.43 ~sQ170_spl|~sQ19_spl|sQ185_spl|~sQ178_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2450,f2220,f594,f2452,f2252])).
% 4.89/1.43 fof(f2456,definition,(
% 4.89/1.43 sQ186_spl <=> (sk1=skaf45(sk1,sk1))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2459,plain,(
% 4.89/1.43 ~sQ177_spl|~sQ170_spl|~sQ19_spl|sQ186_spl|~sQ178_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2451,f2248,f2220,f594,f2456,f2252])).
% 4.89/1.43 fof(f2469,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(X0)|app(nil,skaf45(nil,nil))=X0|~rearsegP(skaf45(nil,nil),X0)|~ssList(nil)|~ssList(skaf45(nil,nil))|~rearsegP(X0,X1)|~rearsegP(X1,nil)|~ssList(X1))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2076,f1203])).
% 4.89/1.43 fof(f2471,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,nil)|~ssList(X0)|app(nil,skaf45(nil,nil))=X0|~rearsegP(skaf45(nil,nil),X0)|~ssList(nil)|~ssList(skaf45(nil,nil)))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2076,f686])).
% 4.89/1.43 fof(f2472,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(skaf45(nil,nil))|~ssList(app(nil,X0))|segmentP(app(app(nil,skaf45(nil,nil)),X0),skaf45(nil,nil)))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2076,f504])).
% 4.89/1.43 fof(f2475,plain,(
% 4.89/1.43 ~ssList(nil)|~ssList(skaf45(nil,nil))|rearsegP(nil,skaf45(nil,nil))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2076,f734])).
% 4.89/1.43 fof(f2477,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(skaf45(nil,nil),X0)|~ssList(nil)|~ssList(X0)|~ssList(skaf45(nil,nil))|rearsegP(nil,X0))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2076,f350])).
% 4.89/1.43 fof(f2478,definition,(
% 4.89/1.43 sQ187_spl <=> (ssList(skaf45(nil,nil)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2480,plain,(
% 4.89/1.43 ~ssList(skaf45(nil,nil))|sQ187_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f2478])).
% 4.89/1.43 fof(f2489,definition,(
% 4.89/1.43 ![X0,X1]: (sQ190_spl <=> (~ssList(X0)|app(nil,skaf45(nil,nil))=X0|~rearsegP(skaf45(nil,nil),X0)|~rearsegP(X0,X1)|~rearsegP(X1,nil)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2492,plain,(
% 4.89/1.43 sQ190_spl|~sQ11_spl|~sQ187_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2469,f2489,f521,f2478])).
% 4.89/1.43 fof(f2497,definition,(
% 4.89/1.43 ![X0]: (sQ192_spl <=> (~rearsegP(X0,nil)|~ssList(X0)|app(nil,skaf45(nil,nil))=X0|~rearsegP(skaf45(nil,nil),X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2500,plain,(
% 4.89/1.43 sQ192_spl|~sQ11_spl|~sQ187_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2471,f2497,f521,f2478])).
% 4.89/1.43 fof(f2501,definition,(
% 4.89/1.43 ![X0]: (sQ193_spl <=> (~ssList(X0)|~ssList(app(nil,X0))|segmentP(app(app(nil,skaf45(nil,nil)),X0),skaf45(nil,nil))))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2504,plain,(
% 4.89/1.43 sQ193_spl|~sQ11_spl|~sQ187_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2472,f2501,f521,f2478])).
% 4.89/1.43 fof(f2510,definition,(
% 4.89/1.43 sQ195_spl <=> (rearsegP(nil,skaf45(nil,nil)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2513,plain,(
% 4.89/1.43 ~sQ11_spl|~sQ187_spl|sQ195_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2475,f521,f2478,f2510])).
% 4.89/1.43 fof(f2515,definition,(
% 4.89/1.43 ![X0]: (sQ196_spl <=> (~rearsegP(skaf45(nil,nil),X0)|~ssList(X0)|rearsegP(nil,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2518,plain,(
% 4.89/1.43 sQ196_spl|~sQ11_spl|~sQ187_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2477,f2515,f521,f2478])).
% 4.89/1.43 fof(f2519,plain,(
% 4.89/1.43 $false|sQ187_spl),
% 4.89/1.43 inference(forward_subsumption_resolution,[status(thm)],[f2480,f250])).
% 4.89/1.43 fof(f2520,plain,(
% 4.89/1.43 sQ187_spl),
% 4.89/1.43 inference(contradiction_clause,[status(thm)],[f2519])).
% 4.89/1.43 fof(f2647,plain,(
% 4.89/1.43 ![X0]: (~segmentP(X0,sk2)|~ssList(X0)|~ssList(sk2)|sk2=X0|~segmentP(nil,X0)|~ssList(nil)|~sQ58_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f1006])).
% 4.89/1.43 fof(f2649,plain,(
% 4.89/1.43 ![X0]: (~segmentP(X0,nil)|~ssList(X0)|~ssList(nil)|nil=X0|~segmentP(nil,X0)|~ssList(nil)|~sQ72_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f1126])).
% 4.89/1.43 fof(f2650,plain,(
% 4.89/1.43 ![X0]: (~segmentP(X0,sk1)|~ssList(X0)|~ssList(sk1)|sk1=X0|~segmentP(nil,X0)|~ssList(nil)|~sQ65_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f1068])).
% 4.89/1.43 fof(f2651,plain,(
% 4.89/1.43 ![X0,X1]: (~segmentP(X0,app(sk2,X1))|~ssList(X0)|~ssList(app(sk2,X1))|app(sk2,X1)=X0|~segmentP(nil,X0)|~ssList(nil)|~ssList(X1)|~sQ45_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f866])).
% 4.89/1.43 fof(f2652,plain,(
% 4.89/1.43 ![X0,X1]: (~segmentP(X0,app(nil,X1))|~ssList(X0)|~ssList(app(nil,X1))|app(nil,X1)=X0|~segmentP(nil,X0)|~ssList(nil)|~ssList(X1)|~sQ47_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f876])).
% 4.89/1.43 fof(f2653,plain,(
% 4.89/1.43 ![X0,X1]: (~segmentP(X0,app(sk1,X1))|~ssList(X0)|~ssList(app(sk1,X1))|app(sk1,X1)=X0|~segmentP(nil,X0)|~ssList(nil)|~ssList(X1)|~sQ46_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f870])).
% 4.89/1.43 fof(f2654,plain,(
% 4.89/1.43 ![X0,X1,X2]: (~segmentP(X0,app(app(X1,nil),X2))|~ssList(X0)|~ssList(app(app(X1,nil),X2))|app(app(X1,nil),X2)=X0|~segmentP(nil,X0)|~ssList(nil)|~ssList(X2)|~ssList(X1)|~sQ73_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f1134])).
% 4.89/1.43 fof(f2655,plain,(
% 4.89/1.43 ![X0,X1,X2]: (~segmentP(X0,app(app(X1,sk1),X2))|~ssList(X0)|~ssList(app(app(X1,sk1),X2))|app(app(X1,sk1),X2)=X0|~segmentP(nil,X0)|~ssList(nil)|~ssList(X2)|~ssList(X1)|~sQ66_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f1074])).
% 4.89/1.43 fof(f2656,plain,(
% 4.89/1.43 ![X0,X1,X2,X3]: (~segmentP(X0,app(app(X1,X2),X3))|~ssList(X0)|~ssList(app(app(X1,X2),X3))|app(app(X1,X2),X3)=X0|~segmentP(nil,X0)|~ssList(nil)|~ssList(X3)|~ssList(X1)|~ssList(X2)|~sQ31_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f772])).
% 4.89/1.43 fof(f2658,plain,(
% 4.89/1.43 ![X0,X1]: (~segmentP(X0,X1)|~ssList(X0)|~ssList(X1)|X1=X0|~segmentP(nil,X0)|~ssList(nil)|~ssList(X1))),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f255])).
% 4.89/1.43 fof(f2663,plain,(
% 4.89/1.43 ![X0]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~segmentP(X0,sk2)|~ssList(sk2)|~sQ58_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f1006])).
% 4.89/1.43 fof(f2665,plain,(
% 4.89/1.43 ![X0]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~segmentP(X0,sk1)|~ssList(sk1)|~sQ65_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f1068])).
% 4.89/1.43 fof(f2666,plain,(
% 4.89/1.43 ![X0,X1]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~segmentP(X0,app(sk2,X1))|~ssList(app(sk2,X1))|~ssList(X1)|~sQ45_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f866])).
% 4.89/1.43 fof(f2667,plain,(
% 4.89/1.43 ![X0,X1]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~segmentP(X0,app(nil,X1))|~ssList(app(nil,X1))|~ssList(X1)|~sQ47_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f876])).
% 4.89/1.43 fof(f2668,plain,(
% 4.89/1.43 ![X0,X1]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~segmentP(X0,app(sk1,X1))|~ssList(app(sk1,X1))|~ssList(X1)|~sQ46_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f870])).
% 4.89/1.43 fof(f2669,plain,(
% 4.89/1.43 ![X0,X1,X2]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~segmentP(X0,app(app(X1,nil),X2))|~ssList(app(app(X1,nil),X2))|~ssList(X2)|~ssList(X1)|~sQ73_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f1134])).
% 4.89/1.43 fof(f2670,plain,(
% 4.89/1.43 ![X0,X1,X2]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~segmentP(X0,app(app(X1,sk1),X2))|~ssList(app(app(X1,sk1),X2))|~ssList(X2)|~ssList(X1)|~sQ66_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f1074])).
% 4.89/1.43 fof(f2671,plain,(
% 4.89/1.43 ![X0,X1,X2,X3]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~segmentP(X0,app(app(X1,X2),X3))|~ssList(app(app(X1,X2),X3))|~ssList(X3)|~ssList(X1)|~ssList(X2)|~sQ31_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f772])).
% 4.89/1.43 fof(f2672,plain,(
% 4.89/1.43 ![X0,X1]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~segmentP(X0,X1)|~ssList(X1)|~ssList(X1))),
% 4.89/1.43 inference(resolution,[status(thm)],[f679,f255])).
% 4.89/1.43 fof(f2676,definition,(
% 4.89/1.43 ![X0]: (sQ197_spl <=> (~segmentP(X0,sk2)|~ssList(X0)|sk2=X0|~segmentP(nil,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2679,plain,(
% 4.89/1.43 sQ197_spl|~sQ16_spl|~sQ11_spl|~sQ58_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2647,f2676,f573,f521,f1005])).
% 4.89/1.43 fof(f2681,definition,(
% 4.89/1.43 ![X0]: (sQ198_spl <=> (~segmentP(X0,nil)|~ssList(X0)|nil=X0|~segmentP(nil,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2684,plain,(
% 4.89/1.43 sQ198_spl|~sQ11_spl|~sQ72_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2649,f2681,f521,f1125])).
% 4.89/1.43 fof(f2685,definition,(
% 4.89/1.43 ![X0]: (sQ199_spl <=> (~segmentP(X0,sk1)|~ssList(X0)|sk1=X0|~segmentP(nil,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2688,plain,(
% 4.89/1.43 sQ199_spl|~sQ19_spl|~sQ11_spl|~sQ65_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2650,f2685,f594,f521,f1067])).
% 4.89/1.43 fof(f2689,definition,(
% 4.89/1.43 ![X0,X1]: (sQ200_spl <=> (~segmentP(X0,app(sk2,X1))|~ssList(X0)|~ssList(app(sk2,X1))|app(sk2,X1)=X0|~segmentP(nil,X0)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2692,plain,(
% 4.89/1.43 sQ200_spl|~sQ11_spl|~sQ45_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2651,f2689,f521,f865])).
% 4.89/1.43 fof(f2693,definition,(
% 4.89/1.43 ![X0,X1]: (sQ201_spl <=> (~segmentP(X0,app(nil,X1))|~ssList(X0)|~ssList(app(nil,X1))|app(nil,X1)=X0|~segmentP(nil,X0)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2696,plain,(
% 4.89/1.43 sQ201_spl|~sQ11_spl|~sQ47_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2652,f2693,f521,f875])).
% 4.89/1.43 fof(f2697,definition,(
% 4.89/1.43 ![X0,X1]: (sQ202_spl <=> (~segmentP(X0,app(sk1,X1))|~ssList(X0)|~ssList(app(sk1,X1))|app(sk1,X1)=X0|~segmentP(nil,X0)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2700,plain,(
% 4.89/1.43 sQ202_spl|~sQ11_spl|~sQ46_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2653,f2697,f521,f869])).
% 4.89/1.43 fof(f2701,definition,(
% 4.89/1.43 ![X0,X1,X2]: (sQ203_spl <=> (~segmentP(X0,app(app(X1,nil),X2))|~ssList(X0)|~ssList(app(app(X1,nil),X2))|app(app(X1,nil),X2)=X0|~segmentP(nil,X0)|~ssList(X2)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2704,plain,(
% 4.89/1.43 sQ203_spl|~sQ11_spl|~sQ73_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2654,f2701,f521,f1133])).
% 4.89/1.43 fof(f2705,definition,(
% 4.89/1.43 ![X0,X1,X2]: (sQ204_spl <=> (~segmentP(X0,app(app(X1,sk1),X2))|~ssList(X0)|~ssList(app(app(X1,sk1),X2))|app(app(X1,sk1),X2)=X0|~segmentP(nil,X0)|~ssList(X2)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2708,plain,(
% 4.89/1.43 sQ204_spl|~sQ11_spl|~sQ66_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2655,f2705,f521,f1073])).
% 4.89/1.43 fof(f2709,definition,(
% 4.89/1.43 ![X0,X1,X2,X3]: (sQ205_spl <=> (~segmentP(X0,app(app(X1,X2),X3))|~ssList(X0)|~ssList(app(app(X1,X2),X3))|app(app(X1,X2),X3)=X0|~segmentP(nil,X0)|~ssList(X3)|~ssList(X1)|~ssList(X2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2712,plain,(
% 4.89/1.43 sQ205_spl|~sQ11_spl|~sQ31_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2656,f2709,f521,f766])).
% 4.89/1.43 fof(f2714,definition,(
% 4.89/1.43 ![X0,X1]: (sQ206_spl <=> (~segmentP(X0,X1)|~ssList(X0)|~ssList(X1)|X1=X0|~segmentP(nil,X0)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2717,plain,(
% 4.89/1.43 sQ206_spl|~sQ11_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2658,f2714,f521])).
% 4.89/1.43 fof(f2720,definition,(
% 4.89/1.43 ![X0]: (sQ207_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~segmentP(X0,sk2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2723,plain,(
% 4.89/1.43 sQ207_spl|~sQ11_spl|~sQ16_spl|~sQ58_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2663,f2720,f521,f573,f1005])).
% 4.89/1.43 fof(f2725,definition,(
% 4.89/1.43 ![X0]: (sQ208_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~segmentP(X0,sk1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2728,plain,(
% 4.89/1.43 sQ208_spl|~sQ11_spl|~sQ19_spl|~sQ65_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2665,f2725,f521,f594,f1067])).
% 4.89/1.43 fof(f2729,definition,(
% 4.89/1.43 ![X0,X1]: (sQ209_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~segmentP(X0,app(sk2,X1))|~ssList(app(sk2,X1))|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2732,plain,(
% 4.89/1.43 sQ209_spl|~sQ11_spl|~sQ45_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2666,f2729,f521,f865])).
% 4.89/1.43 fof(f2733,definition,(
% 4.89/1.43 ![X0,X1]: (sQ210_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~segmentP(X0,app(nil,X1))|~ssList(app(nil,X1))|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2736,plain,(
% 4.89/1.43 sQ210_spl|~sQ11_spl|~sQ47_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2667,f2733,f521,f875])).
% 4.89/1.43 fof(f2737,definition,(
% 4.89/1.43 ![X0,X1]: (sQ211_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~segmentP(X0,app(sk1,X1))|~ssList(app(sk1,X1))|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2740,plain,(
% 4.89/1.43 sQ211_spl|~sQ11_spl|~sQ46_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2668,f2737,f521,f869])).
% 4.89/1.43 fof(f2741,definition,(
% 4.89/1.43 ![X0,X1,X2]: (sQ212_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~segmentP(X0,app(app(X1,nil),X2))|~ssList(app(app(X1,nil),X2))|~ssList(X2)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2744,plain,(
% 4.89/1.43 sQ212_spl|~sQ11_spl|~sQ73_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2669,f2741,f521,f1133])).
% 4.89/1.43 fof(f2745,definition,(
% 4.89/1.43 ![X0,X1,X2]: (sQ213_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~segmentP(X0,app(app(X1,sk1),X2))|~ssList(app(app(X1,sk1),X2))|~ssList(X2)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2748,plain,(
% 4.89/1.43 sQ213_spl|~sQ11_spl|~sQ66_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2670,f2745,f521,f1073])).
% 4.89/1.43 fof(f2749,definition,(
% 4.89/1.43 ![X0,X1,X2,X3]: (sQ214_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~segmentP(X0,app(app(X1,X2),X3))|~ssList(app(app(X1,X2),X3))|~ssList(X3)|~ssList(X1)|~ssList(X2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2752,plain,(
% 4.89/1.43 sQ214_spl|~sQ11_spl|~sQ31_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2671,f2749,f521,f766])).
% 4.89/1.43 fof(f2753,definition,(
% 4.89/1.43 ![X0,X1]: (sQ215_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~segmentP(X0,X1)|~ssList(X1)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2756,plain,(
% 4.89/1.43 sQ215_spl|~sQ11_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2672,f2753,f521])).
% 4.89/1.43 fof(f2761,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk2)|~ssList(X0)|~ssList(sk2)|sk2=X0|~rearsegP(skaf45(sk2,sk2),X0)|~ssList(skaf45(sk2,sk2))|~sQ162_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f2121])).
% 4.89/1.43 fof(f2763,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk2)|~ssList(X0)|~ssList(sk2)|sk2=X0|~rearsegP(sk2,X0)|~ssList(sk2)|~sQ28_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f752])).
% 4.89/1.43 fof(f2764,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk2)|~ssList(X0)|~ssList(sk2)|sk2=X0|~rearsegP(nil,X0)|~ssList(nil)|~sQ26_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f744])).
% 4.89/1.43 fof(f2767,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,nil)|~ssList(X0)|~ssList(nil)|nil=X0|~rearsegP(nil,X0)|~ssList(nil)|~sQ30_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f760])).
% 4.89/1.43 fof(f2768,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk1)|~ssList(X0)|~ssList(sk1)|sk1=X0|~rearsegP(skaf45(sk1,sk1),X0)|~ssList(skaf45(sk1,sk1))|~sQ178_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f2253])).
% 4.89/1.43 fof(f2770,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk1)|~ssList(X0)|~ssList(sk1)|sk1=X0|~rearsegP(sk1,X0)|~ssList(sk1)|~sQ29_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f756])).
% 4.89/1.43 fof(f2771,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk1)|~ssList(X0)|~ssList(sk1)|sk1=X0|~rearsegP(nil,X0)|~ssList(nil)|~sQ27_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f748])).
% 4.89/1.43 fof(f2776,plain,(
% 4.89/1.43 ![X0,X1]: (~rearsegP(X0,X1)|~ssList(X0)|~ssList(X1)|X1=X0|~rearsegP(nil,X0)|~ssList(nil)|~ssList(X1))),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f257])).
% 4.89/1.43 fof(f2781,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(skaf45(sk2,sk2),X0)|~ssList(skaf45(sk2,sk2))|~ssList(X0)|X0=skaf45(sk2,sk2)|~rearsegP(X0,sk2)|~ssList(sk2)|~sQ162_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f2121])).
% 4.89/1.43 fof(f2783,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~rearsegP(X0,sk2)|~ssList(sk2)|~sQ26_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f744])).
% 4.89/1.43 fof(f2786,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(skaf45(sk1,sk1),X0)|~ssList(skaf45(sk1,sk1))|~ssList(X0)|X0=skaf45(sk1,sk1)|~rearsegP(X0,sk1)|~ssList(sk1)|~sQ178_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f2253])).
% 4.89/1.43 fof(f2788,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~rearsegP(X0,sk1)|~ssList(sk1)|~sQ27_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f748])).
% 4.89/1.43 fof(f2791,plain,(
% 4.89/1.43 ![X0,X1]: (~rearsegP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~rearsegP(X0,X1)|~ssList(X1)|~ssList(X1))),
% 4.89/1.43 inference(resolution,[status(thm)],[f691,f257])).
% 4.89/1.43 fof(f2795,definition,(
% 4.89/1.43 ![X0]: (sQ216_spl <=> (~rearsegP(X0,sk2)|~ssList(X0)|sk2=X0|~rearsegP(skaf45(sk2,sk2),X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2798,plain,(
% 4.89/1.43 sQ216_spl|~sQ16_spl|~sQ154_spl|~sQ162_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2761,f2795,f573,f2088,f2120])).
% 4.89/1.43 fof(f2800,definition,(
% 4.89/1.43 ![X0]: (sQ217_spl <=> (~rearsegP(X0,sk2)|~ssList(X0)|sk2=X0|~rearsegP(sk2,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2803,plain,(
% 4.89/1.43 sQ217_spl|~sQ16_spl|~sQ28_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2763,f2800,f573,f751])).
% 4.89/1.43 fof(f2804,definition,(
% 4.89/1.43 ![X0]: (sQ218_spl <=> (~rearsegP(X0,sk2)|~ssList(X0)|sk2=X0|~rearsegP(nil,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2807,plain,(
% 4.89/1.43 sQ218_spl|~sQ16_spl|~sQ11_spl|~sQ26_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2764,f2804,f573,f521,f743])).
% 4.89/1.43 fof(f2813,definition,(
% 4.89/1.43 ![X0]: (sQ220_spl <=> (~rearsegP(X0,nil)|~ssList(X0)|nil=X0|~rearsegP(nil,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2816,plain,(
% 4.89/1.43 sQ220_spl|~sQ11_spl|~sQ30_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2767,f2813,f521,f759])).
% 4.89/1.43 fof(f2817,definition,(
% 4.89/1.43 ![X0]: (sQ221_spl <=> (~rearsegP(X0,sk1)|~ssList(X0)|sk1=X0|~rearsegP(skaf45(sk1,sk1),X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2820,plain,(
% 4.89/1.43 sQ221_spl|~sQ19_spl|~sQ170_spl|~sQ178_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2768,f2817,f594,f2220,f2252])).
% 4.89/1.43 fof(f2822,definition,(
% 4.89/1.43 ![X0]: (sQ222_spl <=> (~rearsegP(X0,sk1)|~ssList(X0)|sk1=X0|~rearsegP(sk1,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2825,plain,(
% 4.89/1.43 sQ222_spl|~sQ19_spl|~sQ29_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2770,f2822,f594,f755])).
% 4.89/1.43 fof(f2826,definition,(
% 4.89/1.43 ![X0]: (sQ223_spl <=> (~rearsegP(X0,sk1)|~ssList(X0)|sk1=X0|~rearsegP(nil,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2829,plain,(
% 4.89/1.43 sQ223_spl|~sQ19_spl|~sQ11_spl|~sQ27_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2771,f2826,f594,f521,f747])).
% 4.89/1.43 fof(f2834,definition,(
% 4.89/1.43 ![X0,X1]: (sQ224_spl <=> (~rearsegP(X0,X1)|~ssList(X0)|~ssList(X1)|X1=X0|~rearsegP(nil,X0)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2837,plain,(
% 4.89/1.43 sQ224_spl|~sQ11_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2776,f2834,f521])).
% 4.89/1.43 fof(f2840,definition,(
% 4.89/1.43 ![X0]: (sQ225_spl <=> (~rearsegP(skaf45(sk2,sk2),X0)|~ssList(X0)|X0=skaf45(sk2,sk2)|~rearsegP(X0,sk2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2843,plain,(
% 4.89/1.43 sQ225_spl|~sQ154_spl|~sQ16_spl|~sQ162_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2781,f2840,f2088,f573,f2120])).
% 4.89/1.43 fof(f2845,definition,(
% 4.89/1.43 ![X0]: (sQ226_spl <=> (~rearsegP(nil,X0)|~ssList(X0)|X0=nil|~rearsegP(X0,sk2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2848,plain,(
% 4.89/1.43 sQ226_spl|~sQ11_spl|~sQ16_spl|~sQ26_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2783,f2845,f521,f573,f743])).
% 4.89/1.43 fof(f2854,definition,(
% 4.89/1.43 ![X0]: (sQ228_spl <=> (~rearsegP(skaf45(sk1,sk1),X0)|~ssList(X0)|X0=skaf45(sk1,sk1)|~rearsegP(X0,sk1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2857,plain,(
% 4.89/1.43 sQ228_spl|~sQ170_spl|~sQ19_spl|~sQ178_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2786,f2854,f2220,f594,f2252])).
% 4.89/1.43 fof(f2859,definition,(
% 4.89/1.43 ![X0]: (sQ229_spl <=> (~rearsegP(nil,X0)|~ssList(X0)|X0=nil|~rearsegP(X0,sk1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2862,plain,(
% 4.89/1.43 sQ229_spl|~sQ11_spl|~sQ19_spl|~sQ27_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2788,f2859,f521,f594,f747])).
% 4.89/1.43 fof(f2867,definition,(
% 4.89/1.43 ![X0,X1]: (sQ230_spl <=> (~rearsegP(nil,X0)|~ssList(X0)|X0=nil|~rearsegP(X0,X1)|~ssList(X1)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f2870,plain,(
% 4.89/1.43 sQ230_spl|~sQ11_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f2791,f2867,f521])).
% 4.89/1.43 fof(f3062,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(X0)|app(nil,skaf45(X0,nil))=X0)),
% 4.89/1.43 inference(resolution,[status(thm)],[f259,f344])).
% 4.89/1.43 fof(f3063,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~frontsegP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil)),
% 4.89/1.43 inference(resolution,[status(thm)],[f259,f341])).
% 4.89/1.43 fof(f3064,definition,(
% 4.89/1.43 ![X0]: (sQ231_spl <=> (~ssList(X0)|~ssList(X0)|app(nil,skaf45(X0,nil))=X0))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3065,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(X0)|app(nil,skaf45(X0,nil))=X0|~sQ231_spl)),
% 4.89/1.43 inference(component_clause,[status(thm)],[f3064])).
% 4.89/1.43 fof(f3067,plain,(
% 4.89/1.43 sQ231_spl|~sQ11_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3062,f3064,f521])).
% 4.89/1.43 fof(f3068,definition,(
% 4.89/1.43 ![X0]: (sQ232_spl <=> (~ssList(X0)|~frontsegP(nil,X0)|~ssList(X0)|X0=nil))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3071,plain,(
% 4.89/1.43 sQ232_spl|~sQ11_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3063,f3068,f521])).
% 4.89/1.43 fof(f3072,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|app(nil,skaf45(X0,nil))=X0|~sQ231_spl)),
% 4.89/1.43 inference(duplicate_literals_removal,[status(thm)],[f3065])).
% 4.89/1.43 fof(f3171,plain,(
% 4.89/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~segmentP(nil,X2)|~ssList(nil)|~ssList(X2)|X2=nil|~segmentP(X2,app(app(X1,sk2),X0))|~ssList(app(app(X1,sk2),X0))|~sQ59_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f1012,f679])).
% 4.89/1.43 fof(f3172,plain,(
% 4.89/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~segmentP(X2,app(app(X1,sk2),X0))|~ssList(X2)|~ssList(app(app(X1,sk2),X0))|app(app(X1,sk2),X0)=X2|~segmentP(nil,X2)|~ssList(nil)|~sQ59_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f1012,f679])).
% 4.89/1.43 fof(f3177,definition,(
% 4.89/1.43 ![X0,X1,X2]: (sQ233_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(nil,X2)|~ssList(X2)|X2=nil|~segmentP(X2,app(app(X1,sk2),X0))|~ssList(app(app(X1,sk2),X0))))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3180,plain,(
% 4.89/1.43 sQ233_spl|~sQ11_spl|~sQ59_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3171,f3177,f521,f1011])).
% 4.89/1.43 fof(f3181,definition,(
% 4.89/1.43 ![X0,X1,X2]: (sQ234_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(X2,app(app(X1,sk2),X0))|~ssList(X2)|~ssList(app(app(X1,sk2),X0))|app(app(X1,sk2),X0)=X2|~segmentP(nil,X2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3184,plain,(
% 4.89/1.43 sQ234_spl|~sQ11_spl|~sQ59_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3172,f3181,f521,f1011])).
% 4.89/1.43 fof(f3228,plain,(
% 4.89/1.43 app(nil,skaf45(sk2,nil))=sk2|~sQ231_spl),
% 4.89/1.43 inference(resolution,[status(thm)],[f3072,f431])).
% 4.89/1.43 fof(f3246,plain,(
% 4.89/1.43 app(nil,skaf45(sk1,nil))=sk1|~sQ231_spl),
% 4.89/1.43 inference(resolution,[status(thm)],[f3072,f430])).
% 4.89/1.43 fof(f3258,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(nil)|~ssList(skaf45(sk2,nil))|app(nil,skaf45(sk2,nil))=skaf45(sk2,nil)|~rearsegP(skaf45(sk2,nil),X0)|~ssList(X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3228,f1241])).
% 4.89/1.43 fof(f3259,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(X0)|app(nil,skaf45(sk2,nil))=X0|~rearsegP(skaf45(sk2,nil),X0)|~ssList(nil)|~ssList(skaf45(sk2,nil))|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3228,f1203])).
% 4.89/1.43 fof(f3260,plain,(
% 4.89/1.43 ![X0]: (~ssList(nil)|~ssList(skaf45(sk2,nil))|app(nil,skaf45(sk2,nil))=skaf45(sk2,nil)|~rearsegP(skaf45(sk2,nil),X0)|~rearsegP(X0,sk2)|~ssList(X0)|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3228,f822])).
% 4.89/1.43 fof(f3261,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk2)|~ssList(X0)|app(nil,skaf45(sk2,nil))=X0|~rearsegP(skaf45(sk2,nil),X0)|~ssList(nil)|~ssList(skaf45(sk2,nil))|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3228,f686])).
% 4.89/1.43 fof(f3262,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(skaf45(sk2,nil))|~ssList(app(sk2,X0))|segmentP(app(app(nil,skaf45(sk2,nil)),X0),skaf45(sk2,nil))|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3228,f504])).
% 4.89/1.43 fof(f3264,plain,(
% 4.89/1.43 ~ssList(nil)|~ssList(skaf45(sk2,nil))|~rearsegP(skaf45(sk2,nil),sk2)|app(nil,skaf45(sk2,nil))=skaf45(sk2,nil)|~sQ231_spl),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3228,f742])).
% 4.89/1.43 fof(f3265,plain,(
% 4.89/1.43 ~ssList(nil)|~ssList(skaf45(sk2,nil))|rearsegP(sk2,skaf45(sk2,nil))|~sQ231_spl),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3228,f734])).
% 4.89/1.43 fof(f3267,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(skaf45(sk2,nil),X0)|~ssList(nil)|~ssList(X0)|~ssList(skaf45(sk2,nil))|rearsegP(sk2,X0)|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3228,f350])).
% 4.89/1.43 fof(f3268,definition,(
% 4.89/1.43 sQ235_spl <=> (ssList(skaf45(sk2,nil)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3270,plain,(
% 4.89/1.43 ~ssList(skaf45(sk2,nil))|sQ235_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f3268])).
% 4.89/1.43 fof(f3272,definition,(
% 4.89/1.43 sQ236_spl <=> (app(nil,skaf45(sk2,nil))=skaf45(sk2,nil))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3275,definition,(
% 4.89/1.43 ![X0,X1]: (sQ237_spl <=> (~rearsegP(skaf45(sk2,nil),X0)|~ssList(X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3278,plain,(
% 4.89/1.43 ~sQ11_spl|~sQ235_spl|sQ236_spl|sQ237_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3258,f521,f3268,f3272,f3275,f3064])).
% 4.89/1.43 fof(f3279,definition,(
% 4.89/1.43 ![X0,X1]: (sQ238_spl <=> (~ssList(X0)|app(nil,skaf45(sk2,nil))=X0|~rearsegP(skaf45(sk2,nil),X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk2)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3282,plain,(
% 4.89/1.43 sQ238_spl|~sQ11_spl|~sQ235_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3259,f3279,f521,f3268,f3064])).
% 4.89/1.43 fof(f3283,definition,(
% 4.89/1.43 ![X0]: (sQ239_spl <=> (~rearsegP(skaf45(sk2,nil),X0)|~rearsegP(X0,sk2)|~ssList(X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3286,plain,(
% 4.89/1.43 ~sQ11_spl|~sQ235_spl|sQ236_spl|sQ239_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3260,f521,f3268,f3272,f3283,f3064])).
% 4.89/1.43 fof(f3287,definition,(
% 4.89/1.43 ![X0]: (sQ240_spl <=> (~rearsegP(X0,sk2)|~ssList(X0)|app(nil,skaf45(sk2,nil))=X0|~rearsegP(skaf45(sk2,nil),X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3290,plain,(
% 4.89/1.43 sQ240_spl|~sQ11_spl|~sQ235_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3261,f3287,f521,f3268,f3064])).
% 4.89/1.43 fof(f3291,definition,(
% 4.89/1.43 ![X0]: (sQ241_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(nil,skaf45(sk2,nil)),X0),skaf45(sk2,nil))))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3294,plain,(
% 4.89/1.43 sQ241_spl|~sQ11_spl|~sQ235_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3262,f3291,f521,f3268,f3064])).
% 4.89/1.43 fof(f3296,definition,(
% 4.89/1.43 sQ242_spl <=> (rearsegP(skaf45(sk2,nil),sk2))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3299,plain,(
% 4.89/1.43 ~sQ11_spl|~sQ235_spl|~sQ242_spl|sQ236_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3264,f521,f3268,f3296,f3272,f3064])).
% 4.89/1.43 fof(f3300,definition,(
% 4.89/1.43 sQ243_spl <=> (rearsegP(sk2,skaf45(sk2,nil)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3303,plain,(
% 4.89/1.43 ~sQ11_spl|~sQ235_spl|sQ243_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3265,f521,f3268,f3300,f3064])).
% 4.89/1.43 fof(f3305,definition,(
% 4.89/1.43 ![X0]: (sQ244_spl <=> (~rearsegP(skaf45(sk2,nil),X0)|~ssList(X0)|rearsegP(sk2,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3308,plain,(
% 4.89/1.43 sQ244_spl|~sQ11_spl|~sQ235_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3267,f3305,f521,f3268,f3064])).
% 4.89/1.43 fof(f3309,plain,(
% 4.89/1.43 $false|sQ235_spl),
% 4.89/1.43 inference(forward_subsumption_resolution,[status(thm)],[f3270,f250])).
% 4.89/1.43 fof(f3310,plain,(
% 4.89/1.43 sQ235_spl),
% 4.89/1.43 inference(contradiction_clause,[status(thm)],[f3309])).
% 4.89/1.43 fof(f3319,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(nil)|~ssList(skaf45(sk1,nil))|app(nil,skaf45(sk1,nil))=skaf45(sk1,nil)|~rearsegP(skaf45(sk1,nil),X0)|~ssList(X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3246,f1241])).
% 4.89/1.43 fof(f3320,plain,(
% 4.89/1.43 ![X0,X1]: (~ssList(X0)|app(nil,skaf45(sk1,nil))=X0|~rearsegP(skaf45(sk1,nil),X0)|~ssList(nil)|~ssList(skaf45(sk1,nil))|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3246,f1203])).
% 4.89/1.43 fof(f3321,plain,(
% 4.89/1.43 ![X0]: (~ssList(nil)|~ssList(skaf45(sk1,nil))|app(nil,skaf45(sk1,nil))=skaf45(sk1,nil)|~rearsegP(skaf45(sk1,nil),X0)|~rearsegP(X0,sk1)|~ssList(X0)|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3246,f822])).
% 4.89/1.43 fof(f3322,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(X0,sk1)|~ssList(X0)|app(nil,skaf45(sk1,nil))=X0|~rearsegP(skaf45(sk1,nil),X0)|~ssList(nil)|~ssList(skaf45(sk1,nil))|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3246,f686])).
% 4.89/1.43 fof(f3323,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(skaf45(sk1,nil))|~ssList(app(sk1,X0))|segmentP(app(app(nil,skaf45(sk1,nil)),X0),skaf45(sk1,nil))|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3246,f504])).
% 4.89/1.43 fof(f3325,plain,(
% 4.89/1.43 ~ssList(nil)|~ssList(skaf45(sk1,nil))|~rearsegP(skaf45(sk1,nil),sk1)|app(nil,skaf45(sk1,nil))=skaf45(sk1,nil)|~sQ231_spl),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3246,f742])).
% 4.89/1.43 fof(f3326,plain,(
% 4.89/1.43 ~ssList(nil)|~ssList(skaf45(sk1,nil))|rearsegP(sk1,skaf45(sk1,nil))|~sQ231_spl),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3246,f734])).
% 4.89/1.43 fof(f3328,plain,(
% 4.89/1.43 ![X0]: (~rearsegP(skaf45(sk1,nil),X0)|~ssList(nil)|~ssList(X0)|~ssList(skaf45(sk1,nil))|rearsegP(sk1,X0)|~sQ231_spl)),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f3246,f350])).
% 4.89/1.43 fof(f3329,definition,(
% 4.89/1.43 sQ245_spl <=> (ssList(skaf45(sk1,nil)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3331,plain,(
% 4.89/1.43 ~ssList(skaf45(sk1,nil))|sQ245_spl),
% 4.89/1.43 inference(component_clause,[status(thm)],[f3329])).
% 4.89/1.43 fof(f3333,definition,(
% 4.89/1.43 sQ246_spl <=> (app(nil,skaf45(sk1,nil))=skaf45(sk1,nil))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3336,definition,(
% 4.89/1.43 ![X0,X1]: (sQ247_spl <=> (~rearsegP(skaf45(sk1,nil),X0)|~ssList(X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3339,plain,(
% 4.89/1.43 ~sQ11_spl|~sQ245_spl|sQ246_spl|sQ247_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3319,f521,f3329,f3333,f3336,f3064])).
% 4.89/1.43 fof(f3340,definition,(
% 4.89/1.43 ![X0,X1]: (sQ248_spl <=> (~ssList(X0)|app(nil,skaf45(sk1,nil))=X0|~rearsegP(skaf45(sk1,nil),X0)|~rearsegP(X0,X1)|~rearsegP(X1,sk1)|~ssList(X1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3343,plain,(
% 4.89/1.43 sQ248_spl|~sQ11_spl|~sQ245_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3320,f3340,f521,f3329,f3064])).
% 4.89/1.43 fof(f3344,definition,(
% 4.89/1.43 ![X0]: (sQ249_spl <=> (~rearsegP(skaf45(sk1,nil),X0)|~rearsegP(X0,sk1)|~ssList(X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3347,plain,(
% 4.89/1.43 ~sQ11_spl|~sQ245_spl|sQ246_spl|sQ249_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3321,f521,f3329,f3333,f3344,f3064])).
% 4.89/1.43 fof(f3348,definition,(
% 4.89/1.43 ![X0]: (sQ250_spl <=> (~rearsegP(X0,sk1)|~ssList(X0)|app(nil,skaf45(sk1,nil))=X0|~rearsegP(skaf45(sk1,nil),X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3351,plain,(
% 4.89/1.43 sQ250_spl|~sQ11_spl|~sQ245_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3322,f3348,f521,f3329,f3064])).
% 4.89/1.43 fof(f3352,definition,(
% 4.89/1.43 ![X0]: (sQ251_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,skaf45(sk1,nil)),X0),skaf45(sk1,nil))))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3355,plain,(
% 4.89/1.43 sQ251_spl|~sQ11_spl|~sQ245_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3323,f3352,f521,f3329,f3064])).
% 4.89/1.43 fof(f3357,definition,(
% 4.89/1.43 sQ252_spl <=> (rearsegP(skaf45(sk1,nil),sk1))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3360,plain,(
% 4.89/1.43 ~sQ11_spl|~sQ245_spl|~sQ252_spl|sQ246_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3325,f521,f3329,f3357,f3333,f3064])).
% 4.89/1.43 fof(f3361,definition,(
% 4.89/1.43 sQ253_spl <=> (rearsegP(sk1,skaf45(sk1,nil)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3364,plain,(
% 4.89/1.43 ~sQ11_spl|~sQ245_spl|sQ253_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3326,f521,f3329,f3361,f3064])).
% 4.89/1.43 fof(f3366,definition,(
% 4.89/1.43 ![X0]: (sQ254_spl <=> (~rearsegP(skaf45(sk1,nil),X0)|~ssList(X0)|rearsegP(sk1,X0)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3369,plain,(
% 4.89/1.43 sQ254_spl|~sQ11_spl|~sQ245_spl|~sQ231_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3328,f3366,f521,f3329,f3064])).
% 4.89/1.43 fof(f3370,plain,(
% 4.89/1.43 $false|sQ245_spl),
% 4.89/1.43 inference(forward_subsumption_resolution,[status(thm)],[f3331,f250])).
% 4.89/1.43 fof(f3371,plain,(
% 4.89/1.43 sQ245_spl),
% 4.89/1.43 inference(contradiction_clause,[status(thm)],[f3370])).
% 4.89/1.43 fof(f3544,plain,(
% 4.89/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,sk2)|~ssList(sk2)|~sQ58_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f770,f1006])).
% 4.89/1.43 fof(f3545,plain,(
% 4.89/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,nil)|~ssList(nil)|~sQ72_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f770,f1126])).
% 4.89/1.43 fof(f3546,plain,(
% 4.89/1.43 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,sk1)|~ssList(sk1)|~sQ65_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f770,f1068])).
% 4.89/1.43 fof(f3547,plain,(
% 4.89/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(sk2,X3))|~ssList(app(sk2,X3))|~ssList(X3)|~sQ45_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f770,f866])).
% 4.89/1.43 fof(f3548,plain,(
% 4.89/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(nil,X3))|~ssList(app(nil,X3))|~ssList(X3)|~sQ47_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f770,f876])).
% 4.89/1.43 fof(f3549,plain,(
% 4.89/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(sk1,X3))|~ssList(app(sk1,X3))|~ssList(X3)|~sQ46_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f770,f870])).
% 4.89/1.43 fof(f3550,plain,(
% 4.89/1.43 ![X0,X1,X2,X3,X4]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(app(X3,sk2),X4))|~ssList(app(app(X3,sk2),X4))|~ssList(X4)|~ssList(X3)|~sQ59_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f770,f1012])).
% 4.89/1.43 fof(f3551,plain,(
% 4.89/1.43 ![X0,X1,X2,X3,X4]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(app(X3,nil),X4))|~ssList(app(app(X3,nil),X4))|~ssList(X4)|~ssList(X3)|~sQ73_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f770,f1134])).
% 4.89/1.43 fof(f3552,plain,(
% 4.89/1.43 ![X0,X1,X2,X3,X4]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(app(X3,sk1),X4))|~ssList(app(app(X3,sk1),X4))|~ssList(X4)|~ssList(X3)|~sQ66_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f770,f1074])).
% 4.89/1.43 fof(f3553,plain,(
% 4.89/1.43 ![X0,X1,X2,X3,X4,X5]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(app(X3,X4),X5))|~ssList(app(app(X3,X4),X5))|~ssList(X5)|~ssList(X3)|~ssList(X4)|~sQ31_spl)),
% 4.89/1.43 inference(resolution,[status(thm)],[f770,f772])).
% 4.89/1.43 fof(f3554,plain,(
% 4.89/1.43 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,X3)|~ssList(X3)|~ssList(X3))),
% 4.89/1.43 inference(resolution,[status(thm)],[f770,f255])).
% 4.89/1.43 fof(f3557,definition,(
% 4.89/1.43 ![X0,X1,X2]: (sQ255_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,sk2)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3560,plain,(
% 4.89/1.43 sQ255_spl|~sQ11_spl|~sQ16_spl|~sQ58_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3544,f3557,f521,f573,f1005])).
% 4.89/1.43 fof(f3561,definition,(
% 4.89/1.43 ![X0,X1,X2]: (sQ256_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,nil)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3564,plain,(
% 4.89/1.43 sQ256_spl|~sQ11_spl|~sQ72_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3545,f3561,f521,f1125])).
% 4.89/1.43 fof(f3565,definition,(
% 4.89/1.43 ![X0,X1,X2]: (sQ257_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,sk1)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3568,plain,(
% 4.89/1.43 sQ257_spl|~sQ11_spl|~sQ19_spl|~sQ65_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3546,f3565,f521,f594,f1067])).
% 4.89/1.43 fof(f3569,definition,(
% 4.89/1.43 ![X0,X1,X2,X3]: (sQ258_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(sk2,X3))|~ssList(app(sk2,X3))|~ssList(X3)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3572,plain,(
% 4.89/1.43 sQ258_spl|~sQ11_spl|~sQ45_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3547,f3569,f521,f865])).
% 4.89/1.43 fof(f3573,definition,(
% 4.89/1.43 ![X0,X1,X2,X3]: (sQ259_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(nil,X3))|~ssList(app(nil,X3))|~ssList(X3)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3576,plain,(
% 4.89/1.43 sQ259_spl|~sQ11_spl|~sQ47_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3548,f3573,f521,f875])).
% 4.89/1.43 fof(f3577,definition,(
% 4.89/1.43 ![X0,X1,X2,X3]: (sQ260_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(sk1,X3))|~ssList(app(sk1,X3))|~ssList(X3)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3580,plain,(
% 4.89/1.43 sQ260_spl|~sQ11_spl|~sQ46_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3549,f3577,f521,f869])).
% 4.89/1.43 fof(f3581,definition,(
% 4.89/1.43 ![X0,X1,X2,X3,X4]: (sQ261_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(app(X3,sk2),X4))|~ssList(app(app(X3,sk2),X4))|~ssList(X4)|~ssList(X3)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3584,plain,(
% 4.89/1.43 sQ261_spl|~sQ11_spl|~sQ59_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3550,f3581,f521,f1011])).
% 4.89/1.43 fof(f3585,definition,(
% 4.89/1.43 ![X0,X1,X2,X3,X4]: (sQ262_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(app(X3,nil),X4))|~ssList(app(app(X3,nil),X4))|~ssList(X4)|~ssList(X3)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3588,plain,(
% 4.89/1.43 sQ262_spl|~sQ11_spl|~sQ73_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3551,f3585,f521,f1133])).
% 4.89/1.43 fof(f3589,definition,(
% 4.89/1.43 ![X0,X1,X2,X3,X4]: (sQ263_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(app(X3,sk1),X4))|~ssList(app(app(X3,sk1),X4))|~ssList(X4)|~ssList(X3)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3592,plain,(
% 4.89/1.43 sQ263_spl|~sQ11_spl|~sQ66_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3552,f3589,f521,f1073])).
% 4.89/1.43 fof(f3593,definition,(
% 4.89/1.43 ![X0,X1,X2,X3,X4,X5]: (sQ264_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,app(app(X3,X4),X5))|~ssList(app(app(X3,X4),X5))|~ssList(X5)|~ssList(X3)|~ssList(X4)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3596,plain,(
% 4.89/1.43 sQ264_spl|~sQ11_spl|~sQ31_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3553,f3593,f521,f766])).
% 4.89/1.43 fof(f3597,definition,(
% 4.89/1.43 ![X0,X1,X2,X3]: (sQ265_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~segmentP(X2,X3)|~ssList(X3)|~ssList(X3)))),
% 4.89/1.43 introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition])).
% 4.89/1.43 fof(f3600,plain,(
% 4.89/1.43 sQ265_spl|~sQ11_spl),
% 4.89/1.43 inference(split_clause,[status(thm)],[f3554,f3597,f521])).
% 4.89/1.43 fof(f3611,plain,(
% 4.89/1.43 ![X0]: (~ssList(X0)|~ssList(sk2)|~ssList(skaf45(sk2,sk2))|segmentP(app(sk2,X0),skaf45(sk2,sk2)))),
% 4.89/1.43 inference(paramodulation,[status(thm)],[f2062,f771])).
% 4.89/1.44 fof(f3613,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|~ssList(skaf46(sk2,sk1))|~ssList(sk1)|segmentP(app(sk2,X0),sk1)|~sQ106_spl)),
% 4.89/1.44 inference(paramodulation,[status(thm)],[f1490,f771])).
% 4.89/1.44 fof(f3614,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|~ssList(skaf46(sk2,nil))|~ssList(nil)|segmentP(app(sk2,X0),nil)|~sQ107_spl)),
% 4.89/1.44 inference(paramodulation,[status(thm)],[f1494,f771])).
% 4.89/1.44 fof(f3615,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|~ssList(skaf46(sk2,sk2))|~ssList(sk2)|segmentP(app(sk2,X0),sk2)|~sQ108_spl)),
% 4.89/1.44 inference(paramodulation,[status(thm)],[f1498,f771])).
% 4.89/1.44 fof(f3617,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|~ssList(skaf46(sk1,sk1))|~ssList(sk1)|segmentP(app(sk1,X0),sk1)|~sQ110_spl)),
% 4.89/1.44 inference(paramodulation,[status(thm)],[f1506,f771])).
% 4.89/1.44 fof(f3618,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|~ssList(skaf46(sk1,nil))|~ssList(nil)|segmentP(app(sk1,X0),nil)|~sQ111_spl)),
% 4.89/1.44 inference(paramodulation,[status(thm)],[f1510,f771])).
% 4.89/1.44 fof(f3619,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(skaf45(sk1,sk1))|segmentP(app(sk1,X0),skaf45(sk1,sk1)))),
% 4.89/1.44 inference(paramodulation,[status(thm)],[f2067,f771])).
% 4.89/1.44 fof(f3623,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|segmentP(app(nil,X0),nil))),
% 4.89/1.44 inference(paramodulation,[status(thm)],[f567,f771])).
% 4.89/1.44 fof(f3637,definition,(
% 4.89/1.44 ![X0]: (sQ268_spl <=> (~ssList(X0)|segmentP(app(sk2,X0),skaf45(sk2,sk2))))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3640,plain,(
% 4.89/1.44 sQ268_spl|~sQ16_spl|~sQ154_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3611,f3637,f573,f2088])).
% 4.89/1.44 fof(f3642,definition,(
% 4.89/1.44 ![X0]: (sQ269_spl <=> (~ssList(X0)|segmentP(app(sk2,X0),sk1)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3643,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|segmentP(app(sk2,X0),sk1)|~sQ269_spl)),
% 4.89/1.44 inference(component_clause,[status(thm)],[f3642])).
% 4.89/1.44 fof(f3645,plain,(
% 4.89/1.44 sQ269_spl|~sQ136_spl|~sQ19_spl|~sQ106_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3613,f3642,f1778,f594,f1489])).
% 4.89/1.44 fof(f3646,plain,(
% 4.89/1.44 sQ45_spl|~sQ113_spl|~sQ11_spl|~sQ107_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3614,f865,f1569,f521,f1493])).
% 4.89/1.44 fof(f3647,definition,(
% 4.89/1.44 ![X0]: (sQ270_spl <=> (~ssList(X0)|segmentP(app(sk2,X0),sk2)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3648,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|segmentP(app(sk2,X0),sk2)|~sQ270_spl)),
% 4.89/1.44 inference(component_clause,[status(thm)],[f3647])).
% 4.89/1.44 fof(f3650,plain,(
% 4.89/1.44 sQ270_spl|~sQ124_spl|~sQ16_spl|~sQ108_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3615,f3647,f1661,f573,f1497])).
% 4.89/1.44 fof(f3652,definition,(
% 4.89/1.44 ![X0]: (sQ271_spl <=> (~ssList(X0)|segmentP(app(sk1,X0),sk1)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3653,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~sQ271_spl)),
% 4.89/1.44 inference(component_clause,[status(thm)],[f3652])).
% 4.89/1.44 fof(f3655,plain,(
% 4.89/1.44 sQ271_spl|~sQ128_spl|~sQ19_spl|~sQ110_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3617,f3652,f1700,f594,f1505])).
% 4.89/1.44 fof(f3656,plain,(
% 4.89/1.44 sQ46_spl|~sQ118_spl|~sQ11_spl|~sQ111_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3618,f869,f1611,f521,f1509])).
% 4.89/1.44 fof(f3657,definition,(
% 4.89/1.44 ![X0]: (sQ272_spl <=> (~ssList(X0)|segmentP(app(sk1,X0),skaf45(sk1,sk1))))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3660,plain,(
% 4.89/1.44 sQ272_spl|~sQ19_spl|~sQ170_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3619,f3657,f594,f2220])).
% 4.89/1.44 fof(f3664,plain,(
% 4.89/1.44 sQ47_spl|~sQ11_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3623,f875,f521])).
% 4.89/1.44 fof(f3665,plain,(
% 4.89/1.44 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk2)|~ssList(X3)|segmentP(app(app(X2,X3),X1),sk2)|~segmentP(X3,app(sk2,X0))|~ssList(app(sk2,X0))|~sQ270_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3648,f770])).
% 4.89/1.44 fof(f3666,plain,(
% 4.89/1.44 ![X0,X1]: (~ssList(X0)|~segmentP(sk2,X1)|~ssList(sk2)|~ssList(X1)|X1=sk2|~segmentP(X1,app(sk2,X0))|~ssList(app(sk2,X0))|~sQ270_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3648,f679])).
% 4.89/1.44 fof(f3667,plain,(
% 4.89/1.44 ![X0,X1]: (~ssList(X0)|~segmentP(X1,app(sk2,X0))|~ssList(X1)|~ssList(app(sk2,X0))|app(sk2,X0)=X1|~segmentP(sk2,X1)|~ssList(sk2)|~sQ270_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3648,f679])).
% 4.89/1.44 fof(f3668,plain,(
% 4.89/1.44 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),sk2)|~sQ270_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3648,f404])).
% 4.89/1.44 fof(f3669,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|~segmentP(sk2,app(sk2,X0))|~ssList(sk2)|~ssList(app(sk2,X0))|app(sk2,X0)=sk2|~sQ270_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3648,f339])).
% 4.89/1.44 fof(f3670,plain,(
% 4.89/1.44 ~ssList(skaf45(sk2,sk2))|segmentP(sk2,sk2)|~sQ270_spl),
% 4.89/1.44 inference(paramodulation,[status(thm)],[f2062,f3648])).
% 4.89/1.44 fof(f3672,definition,(
% 4.89/1.44 ![X0,X1,X2,X3]: (sQ273_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|segmentP(app(app(X2,X3),X1),sk2)|~segmentP(X3,app(sk2,X0))|~ssList(app(sk2,X0))))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3675,plain,(
% 4.89/1.44 sQ273_spl|~sQ16_spl|~sQ270_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3665,f3672,f573,f3647])).
% 4.89/1.44 fof(f3676,definition,(
% 4.89/1.44 ![X0,X1]: (sQ274_spl <=> (~ssList(X0)|~segmentP(sk2,X1)|~ssList(X1)|X1=sk2|~segmentP(X1,app(sk2,X0))|~ssList(app(sk2,X0))))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3679,plain,(
% 4.89/1.44 sQ274_spl|~sQ16_spl|~sQ270_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3666,f3676,f573,f3647])).
% 4.89/1.44 fof(f3680,definition,(
% 4.89/1.44 ![X0,X1]: (sQ275_spl <=> (~ssList(X0)|~segmentP(X1,app(sk2,X0))|~ssList(X1)|~ssList(app(sk2,X0))|app(sk2,X0)=X1|~segmentP(sk2,X1)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ275_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3683,plain,(
% 4.89/1.44 sQ275_spl|~sQ16_spl|~sQ270_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3667,f3680,f573,f3647])).
% 4.89/1.44 fof(f3684,definition,(
% 4.89/1.44 ![X0,X1,X2]: (sQ276_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),sk2)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ276_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3687,plain,(
% 4.89/1.44 sQ276_spl|~sQ16_spl|~sQ270_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3668,f3684,f573,f3647])).
% 4.89/1.44 fof(f3688,definition,(
% 4.89/1.44 ![X0]: (sQ277_spl <=> (~ssList(X0)|~segmentP(sk2,app(sk2,X0))|~ssList(app(sk2,X0))|app(sk2,X0)=sk2))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3691,plain,(
% 4.89/1.44 sQ277_spl|~sQ16_spl|~sQ270_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3669,f3688,f573,f3647])).
% 4.89/1.44 fof(f3692,definition,(
% 4.89/1.44 sQ278_spl <=> (segmentP(sk2,sk2))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3693,plain,(
% 4.89/1.44 segmentP(sk2,sk2)|~sQ278_spl),
% 4.89/1.44 inference(component_clause,[status(thm)],[f3692])).
% 4.89/1.44 fof(f3695,plain,(
% 4.89/1.44 ~sQ154_spl|sQ278_spl|~sQ270_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3670,f2088,f3692,f3647])).
% 4.89/1.44 fof(f3697,plain,(
% 4.89/1.44 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(sk2)|~ssList(X2)|segmentP(app(app(X1,X2),X0),sk2)|~segmentP(X2,sk2)|~ssList(sk2)|~sQ278_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3693,f770])).
% 4.89/1.44 fof(f3699,plain,(
% 4.89/1.44 ![X0]: (~segmentP(sk2,X0)|~ssList(sk2)|~ssList(X0)|X0=sk2|~segmentP(X0,sk2)|~ssList(sk2)|~sQ278_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3693,f679])).
% 4.89/1.44 fof(f3702,plain,(
% 4.89/1.44 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk2)|~ssList(sk2)|segmentP(app(app(X1,sk2),X0),sk2)|~sQ278_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3693,f404])).
% 4.89/1.44 fof(f3704,definition,(
% 4.89/1.44 ![X0,X1,X2]: (sQ279_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),sk2)|~segmentP(X2,sk2)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3707,plain,(
% 4.89/1.44 sQ279_spl|~sQ16_spl|~sQ278_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3697,f3704,f573,f3692])).
% 4.89/1.44 fof(f3709,definition,(
% 4.89/1.44 ![X0]: (sQ280_spl <=> (~segmentP(sk2,X0)|~ssList(X0)|X0=sk2|~segmentP(X0,sk2)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3712,plain,(
% 4.89/1.44 sQ280_spl|~sQ16_spl|~sQ278_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3699,f3709,f573,f3692])).
% 4.89/1.44 fof(f3715,definition,(
% 4.89/1.44 ![X0,X1]: (sQ281_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk2),X0),sk2)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ281_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3718,plain,(
% 4.89/1.44 sQ281_spl|~sQ16_spl|~sQ278_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3702,f3715,f573,f3692])).
% 4.89/1.44 fof(f3722,plain,(
% 4.89/1.44 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk1)|~ssList(X3)|segmentP(app(app(X2,X3),X1),sk1)|~segmentP(X3,app(sk1,X0))|~ssList(app(sk1,X0))|~sQ271_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3653,f770])).
% 4.89/1.44 fof(f3723,plain,(
% 4.89/1.44 ![X0,X1]: (~ssList(X0)|~segmentP(sk1,X1)|~ssList(sk1)|~ssList(X1)|X1=sk1|~segmentP(X1,app(sk1,X0))|~ssList(app(sk1,X0))|~sQ271_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3653,f679])).
% 4.89/1.44 fof(f3724,plain,(
% 4.89/1.44 ![X0,X1]: (~ssList(X0)|~segmentP(X1,app(sk1,X0))|~ssList(X1)|~ssList(app(sk1,X0))|app(sk1,X0)=X1|~segmentP(sk1,X1)|~ssList(sk1)|~sQ271_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3653,f679])).
% 4.89/1.44 fof(f3725,plain,(
% 4.89/1.44 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),sk1)|~sQ271_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3653,f404])).
% 4.89/1.44 fof(f3726,plain,(
% 4.89/1.44 ![X0]: (~ssList(X0)|~segmentP(sk1,app(sk1,X0))|~ssList(sk1)|~ssList(app(sk1,X0))|app(sk1,X0)=sk1|~sQ271_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3653,f339])).
% 4.89/1.44 fof(f3727,plain,(
% 4.89/1.44 ~ssList(skaf45(sk1,sk1))|segmentP(sk1,sk1)|~sQ271_spl),
% 4.89/1.44 inference(paramodulation,[status(thm)],[f2067,f3653])).
% 4.89/1.44 fof(f3729,definition,(
% 4.89/1.44 ![X0,X1,X2,X3]: (sQ282_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|segmentP(app(app(X2,X3),X1),sk1)|~segmentP(X3,app(sk1,X0))|~ssList(app(sk1,X0))))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3732,plain,(
% 4.89/1.44 sQ282_spl|~sQ19_spl|~sQ271_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3722,f3729,f594,f3652])).
% 4.89/1.44 fof(f3733,definition,(
% 4.89/1.44 ![X0,X1]: (sQ283_spl <=> (~ssList(X0)|~segmentP(sk1,X1)|~ssList(X1)|X1=sk1|~segmentP(X1,app(sk1,X0))|~ssList(app(sk1,X0))))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3736,plain,(
% 4.89/1.44 sQ283_spl|~sQ19_spl|~sQ271_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3723,f3733,f594,f3652])).
% 4.89/1.44 fof(f3737,definition,(
% 4.89/1.44 ![X0,X1]: (sQ284_spl <=> (~ssList(X0)|~segmentP(X1,app(sk1,X0))|~ssList(X1)|~ssList(app(sk1,X0))|app(sk1,X0)=X1|~segmentP(sk1,X1)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3740,plain,(
% 4.89/1.44 sQ284_spl|~sQ19_spl|~sQ271_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3724,f3737,f594,f3652])).
% 4.89/1.44 fof(f3741,definition,(
% 4.89/1.44 ![X0,X1,X2]: (sQ285_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),sk1)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3744,plain,(
% 4.89/1.44 sQ285_spl|~sQ19_spl|~sQ271_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3725,f3741,f594,f3652])).
% 4.89/1.44 fof(f3745,definition,(
% 4.89/1.44 ![X0]: (sQ286_spl <=> (~ssList(X0)|~segmentP(sk1,app(sk1,X0))|~ssList(app(sk1,X0))|app(sk1,X0)=sk1))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3748,plain,(
% 4.89/1.44 sQ286_spl|~sQ19_spl|~sQ271_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3726,f3745,f594,f3652])).
% 4.89/1.44 fof(f3749,definition,(
% 4.89/1.44 sQ287_spl <=> (segmentP(sk1,sk1))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ287_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3750,plain,(
% 4.89/1.44 segmentP(sk1,sk1)|~sQ287_spl),
% 4.89/1.44 inference(component_clause,[status(thm)],[f3749])).
% 4.89/1.44 fof(f3752,plain,(
% 4.89/1.44 ~sQ170_spl|sQ287_spl|~sQ271_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3727,f2220,f3749,f3652])).
% 4.89/1.44 fof(f3756,plain,(
% 4.89/1.44 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(sk1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),sk1)|~segmentP(X2,sk1)|~ssList(sk1)|~sQ287_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3750,f770])).
% 4.89/1.44 fof(f3758,plain,(
% 4.89/1.44 ![X0]: (~segmentP(sk1,X0)|~ssList(sk1)|~ssList(X0)|X0=sk1|~segmentP(X0,sk1)|~ssList(sk1)|~sQ287_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3750,f679])).
% 4.89/1.44 fof(f3761,plain,(
% 4.89/1.44 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk1)|~ssList(sk1)|segmentP(app(app(X1,sk1),X0),sk1)|~sQ287_spl)),
% 4.89/1.44 inference(resolution,[status(thm)],[f3750,f404])).
% 4.89/1.44 fof(f3765,definition,(
% 4.89/1.44 ![X0,X1,X2]: (sQ288_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),sk1)|~segmentP(X2,sk1)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ288_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3768,plain,(
% 4.89/1.44 sQ288_spl|~sQ19_spl|~sQ287_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3756,f3765,f594,f3749])).
% 4.89/1.44 fof(f3770,definition,(
% 4.89/1.44 ![X0]: (sQ289_spl <=> (~segmentP(sk1,X0)|~ssList(X0)|X0=sk1|~segmentP(X0,sk1)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3773,plain,(
% 4.89/1.44 sQ289_spl|~sQ19_spl|~sQ287_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3758,f3770,f594,f3749])).
% 4.89/1.44 fof(f3776,definition,(
% 4.89/1.44 ![X0,X1]: (sQ290_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),sk1)))),
% 4.89/1.44 introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition])).
% 4.89/1.44 fof(f3779,plain,(
% 4.89/1.44 sQ290_spl|~sQ19_spl|~sQ287_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3761,f3776,f594,f3749])).
% 4.89/1.44 fof(f3788,plain,(
% 4.89/1.44 ~ssList(skaf45(sk2,sk2))|segmentP(sk2,sk1)|~sQ269_spl),
% 4.89/1.44 inference(paramodulation,[status(thm)],[f2062,f3643])).
% 4.89/1.44 fof(f3810,plain,(
% 4.89/1.44 ~sQ154_spl|sQ5_spl|~sQ269_spl),
% 4.89/1.44 inference(split_clause,[status(thm)],[f3788,f2088,f461,f3642])).
% 4.89/1.44 fof(f3812,plain,(
% 4.89/1.44 $false),
% 4.89/1.44 inference(sat_refutation,[status(thm)],[f457,f464,f468,f476,f485,f527,f531,f534,f548,f557,f576,f581,f597,f621,f623,f661,f671,f678,f690,f696,f711,f746,f750,f754,f758,f762,f769,f777,f787,f792,f834,f838,f842,f860,f864,f890,f894,f898,f902,f906,f922,f925,f927,f1000,f1004,f1008,f1014,f1045,f1062,f1066,f1070,f1076,f1082,f1104,f1108,f1118,f1122,f1128,f1136,f1144,f1148,f1158,f1162,f1207,f1211,f1215,f1219,f1223,f1274,f1278,f1282,f1286,f1290,f1338,f1342,f1353,f1357,f1492,f1496,f1500,f1504,f1508,f1512,f1520,f1580,f1585,f1589,f1596,f1622,f1627,f1631,f1638,f1669,f1674,f1678,f1685,f1708,f1713,f1717,f1724,f1747,f1752,f1756,f1763,f1814,f2098,f2102,f2106,f2110,f2114,f2119,f2123,f2128,f2130,f2158,f2163,f2167,f2169,f2178,f2182,f2234,f2242,f2246,f2251,f2255,f2260,f2262,f2391,f2396,f2400,f2402,f2455,f2459,f2492,f2500,f2504,f2513,f2518,f2520,f2679,f2684,f2688,f2692,f2696,f2700,f2704,f2708,f2712,f2717,f2723,f2728,f2732,f2736,f2740,f2744,f2748,f2752,f2756,f2798,f2803,f2807,f2816,f2820,f2825,f2829,f2837,f2843,f2848,f2857,f2862,f2870,f3067,f3071,f3180,f3184,f3278,f3282,f3286,f3290,f3294,f3299,f3303,f3308,f3310,f3339,f3343,f3347,f3351,f3355,f3360,f3364,f3369,f3371,f3560,f3564,f3568,f3572,f3576,f3580,f3584,f3588,f3592,f3596,f3600,f3640,f3645,f3646,f3650,f3655,f3656,f3660,f3664,f3675,f3679,f3683,f3687,f3691,f3695,f3707,f3712,f3718,f3732,f3736,f3740,f3744,f3748,f3752,f3768,f3773,f3779,f3810])).
% 4.89/1.44 % SZS output end CNFRefutation for theBenchmark.p
% 4.89/1.45 % Elapsed time: 1.075509 seconds
% 4.89/1.45 % CPU time: 8.089757 seconds
% 4.89/1.45 % Total memory used: 192.658 MB
% 4.89/1.45 % Net memory used: 188.096 MB
%------------------------------------------------------------------------------