Drodi-SAT---4.1.1.UNS-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : SWC058-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p

% Computer : n014.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:28 PM UTC 2026

% Result   : Unsatisfiable 0.13s 0.56s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWC058-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36  % Computer : n014.cluster.edu
% 0.09/0.36  % Model    : x86_64 x86_64
% 0.09/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36  % Memory   : 8046.5625MB
% 0.09/0.36  % OS       : Linux 6.8.0-71-generic
% 0.09/0.36  % CPULimit : 300
% 0.09/0.36  % WCLimit  : 300
% 0.09/0.36  % DateTime : Mon Sep 21 07:52:04 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 0.13/0.38  % Drodi V4.1.1
% 0.13/0.56  % Refutation found
% 0.13/0.56  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.56  % SZS output start CNFRefutation for theBenchmark
% 0.13/0.56  fof(f8,axiom,(
% 0.13/0.56    ssList(nil) ),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f50,axiom,(
% 0.13/0.56    (![U,V]: (ssList(skaf46(U,V)) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f56,axiom,(
% 0.13/0.56    (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f57,axiom,(
% 0.13/0.56    (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f58,axiom,(
% 0.13/0.56    (![U]: (( ~ ssList(U)| rearsegP(U,nil) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f73,axiom,(
% 0.13/0.56    (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f74,axiom,(
% 0.13/0.56    (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f80,axiom,(
% 0.13/0.56    (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f82,axiom,(
% 0.13/0.56    (![U]: (( ~ rearsegP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f85,axiom,(
% 0.13/0.56    (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f127,axiom,(
% 0.13/0.56    (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f128,axiom,(
% 0.13/0.56    (![U,V]: (( ~ rearsegP(U,V)| ~ rearsegP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f131,axiom,(
% 0.13/0.56    (![U,V]: (( ~ rearsegP(U,V)| ~ ssList(V)| ~ ssList(U)| app(skaf46(U,V),V) = U ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f136,axiom,(
% 0.13/0.56    (![U,V,W]: (( ~ rearsegP(U,V)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| rearsegP(app(W,U),V) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f143,axiom,(
% 0.13/0.56    (![U,V,W]: (( app(U,V) != W| ~ ssList(U)| ~ ssList(V)| ~ ssList(W)| rearsegP(W,V) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f152,axiom,(
% 0.13/0.56    (![U,V,W]: (( ~ segmentP(U,V)| ~ segmentP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| segmentP(U,W) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f153,axiom,(
% 0.13/0.56    (![U,V,W]: (( ~ rearsegP(U,V)| ~ rearsegP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| rearsegP(U,W) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f172,axiom,(
% 0.13/0.56    (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f173,axiom,(
% 0.13/0.56    (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f186,negated_conjecture,(
% 0.13/0.56    ssList(sk1) ),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f187,negated_conjecture,(
% 0.13/0.56    ssList(sk2) ),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f190,negated_conjecture,(
% 0.13/0.56    sk2 = sk4 ),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f191,negated_conjecture,(
% 0.13/0.56    sk1 = sk3 ),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f193,negated_conjecture,(
% 0.13/0.56    (![A]: (( nil = sk2| ~ ssList(A)| ~ neq(A,nil)| ~ segmentP(sk2,A)| ~ segmentP(sk1,A) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f194,negated_conjecture,(
% 0.13/0.56    ( nil != sk1| neq(sk2,nil) ) ),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f195,negated_conjecture,(
% 0.13/0.56    (![A]: (( nil != sk1| ~ ssList(A)| ~ neq(A,nil)| ~ segmentP(sk2,A)| ~ segmentP(sk1,A) ) ))),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f196,negated_conjecture,(
% 0.13/0.56    ( nil = sk4| neq(sk3,nil) ) ),
% 0.13/0.56    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.56  fof(f197,negated_conjecture,(
% 0.13/0.57    ( nil = sk4| rearsegP(sk4,sk3) ) ),
% 0.13/0.57    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.57  fof(f198,negated_conjecture,(
% 0.13/0.57    ( nil = sk3| neq(sk3,nil) ) ),
% 0.13/0.57    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.57  fof(f199,negated_conjecture,(
% 0.13/0.57    ( nil = sk3| rearsegP(sk4,sk3) ) ),
% 0.13/0.57    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.57  fof(f207,plain,(
% 0.13/0.57    ssList(nil)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.57  fof(f249,plain,(
% 0.13/0.57    ![X0,X1]: (ssList(skaf46(X0,X1)))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f50])).
% 0.13/0.57  fof(f255,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f56])).
% 0.13/0.57  fof(f256,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f57])).
% 0.13/0.57  fof(f257,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|rearsegP(X0,nil))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f58])).
% 0.13/0.57  fof(f273,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f73])).
% 0.13/0.57  fof(f274,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f74])).
% 0.13/0.57  fof(f280,plain,(
% 0.13/0.57    ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f80])).
% 0.13/0.57  fof(f282,plain,(
% 0.13/0.57    ![X0]: (~rearsegP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f82])).
% 0.13/0.57  fof(f285,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f85])).
% 0.13/0.57  fof(f339,plain,(
% 0.13/0.57    ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f127])).
% 0.13/0.57  fof(f340,plain,(
% 0.13/0.57    ![X0,X1]: (~rearsegP(X0,X1)|~rearsegP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f128])).
% 0.13/0.57  fof(f343,plain,(
% 0.13/0.57    ![X0,X1]: (~rearsegP(X0,X1)|~ssList(X1)|~ssList(X0)|app(skaf46(X0,X1),X1)=X0)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f131])).
% 0.13/0.57  fof(f350,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~rearsegP(X0,X1)|~ssList(X2)|~ssList(X1)|~ssList(X0)|rearsegP(app(X2,X0),X1))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f136])).
% 0.13/0.57  fof(f357,plain,(
% 0.13/0.57    ![V,W]: ((((![U]: (~app(U,V)=W|~ssList(U)))|~ssList(V))|~ssList(W))|rearsegP(W,V))),
% 0.13/0.57    inference(miniscoping,[status(thm)],[f143])).
% 0.13/0.57  fof(f358,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~app(X0,X1)=X2|~ssList(X0)|~ssList(X1)|~ssList(X2)|rearsegP(X2,X1))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f357])).
% 0.13/0.57  fof(f373,plain,(
% 0.13/0.57    ![U,W]: (((![V]: (((~segmentP(U,V)|~segmentP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|segmentP(U,W))),
% 0.13/0.57    inference(miniscoping,[status(thm)],[f152])).
% 0.13/0.57  fof(f374,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~segmentP(X0,X1)|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|segmentP(X0,X2))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f373])).
% 0.13/0.57  fof(f375,plain,(
% 0.13/0.57    ![U,W]: (((![V]: (((~rearsegP(U,V)|~rearsegP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|rearsegP(U,W))),
% 0.13/0.57    inference(miniscoping,[status(thm)],[f153])).
% 0.13/0.57  fof(f376,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~rearsegP(X0,X1)|~rearsegP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|rearsegP(X0,X2))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f375])).
% 0.13/0.57  fof(f404,plain,(
% 0.13/0.57    ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f172])).
% 0.13/0.57  fof(f405,plain,(
% 0.13/0.57    ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 0.13/0.57    inference(miniscoping,[status(thm)],[f173])).
% 0.13/0.57  fof(f406,plain,(
% 0.13/0.57    ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f405])).
% 0.13/0.57  fof(f430,plain,(
% 0.13/0.57    ssList(sk1)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f186])).
% 0.13/0.57  fof(f431,plain,(
% 0.13/0.57    ssList(sk2)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f187])).
% 0.13/0.57  fof(f434,plain,(
% 0.13/0.57    sk2=sk4),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f190])).
% 0.13/0.57  fof(f435,plain,(
% 0.13/0.57    sk1=sk3),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f191])).
% 0.13/0.57  fof(f437,plain,(
% 0.13/0.57    ![X0]: (nil=sk2|~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f193])).
% 0.13/0.57  fof(f438,plain,(
% 0.13/0.57    ~nil=sk1|neq(sk2,nil)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f194])).
% 0.13/0.57  fof(f439,plain,(
% 0.13/0.57    ![X0]: (~nil=sk1|~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f195])).
% 0.13/0.57  fof(f440,plain,(
% 0.13/0.57    nil=sk4|neq(sk3,nil)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f196])).
% 0.13/0.57  fof(f441,plain,(
% 0.13/0.57    nil=sk4|rearsegP(sk4,sk3)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f197])).
% 0.13/0.57  fof(f442,plain,(
% 0.13/0.57    nil=sk3|neq(sk3,nil)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f198])).
% 0.13/0.57  fof(f443,plain,(
% 0.13/0.57    nil=sk3|rearsegP(sk4,sk3)),
% 0.13/0.57    inference(cnf_transformation,[status(thm)],[f199])).
% 0.13/0.57  fof(f451,definition,(
% 0.13/0.57    sQ2_spl <=> (nil=sk2)),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f452,plain,(
% 0.13/0.57    nil=sk2|~sQ2_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f451])).
% 0.13/0.57  fof(f454,definition,(
% 0.13/0.57    sQ3_spl <=> (neq(sk2,nil))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f455,plain,(
% 0.13/0.57    neq(sk2,nil)|~sQ3_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f454])).
% 0.13/0.57  fof(f458,definition,(
% 0.13/0.57    ![X0]: (sQ4_spl <=> (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f459,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~sQ4_spl)),
% 0.13/0.57    inference(component_clause,[status(thm)],[f458])).
% 0.13/0.57  fof(f461,plain,(
% 0.13/0.57    sQ2_spl|sQ4_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f437,f451,f458])).
% 0.13/0.57  fof(f462,definition,(
% 0.13/0.57    sQ5_spl <=> (nil=sk1)),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f464,plain,(
% 0.13/0.57    ~nil=sk1|sQ5_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f462])).
% 0.13/0.57  fof(f465,plain,(
% 0.13/0.57    ~sQ5_spl|sQ3_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f438,f462,f454])).
% 0.13/0.57  fof(f466,plain,(
% 0.13/0.57    ~sQ5_spl|sQ4_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f439,f462,f458])).
% 0.13/0.57  fof(f467,definition,(
% 0.13/0.57    sQ6_spl <=> (nil=sk4)),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f468,plain,(
% 0.13/0.57    nil=sk4|~sQ6_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f467])).
% 0.13/0.57  fof(f470,definition,(
% 0.13/0.57    sQ7_spl <=> (neq(sk3,nil))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f471,plain,(
% 0.13/0.57    neq(sk3,nil)|~sQ7_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f470])).
% 0.13/0.57  fof(f473,plain,(
% 0.13/0.57    sQ6_spl|sQ7_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f440,f467,f470])).
% 0.13/0.57  fof(f474,definition,(
% 0.13/0.57    sQ8_spl <=> (rearsegP(sk4,sk3))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f475,plain,(
% 0.13/0.57    rearsegP(sk4,sk3)|~sQ8_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f474])).
% 0.13/0.57  fof(f477,plain,(
% 0.13/0.57    sQ6_spl|sQ8_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f441,f467,f474])).
% 0.13/0.57  fof(f478,definition,(
% 0.13/0.57    sQ9_spl <=> (nil=sk3)),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f479,plain,(
% 0.13/0.57    nil=sk3|~sQ9_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f478])).
% 0.13/0.57  fof(f481,plain,(
% 0.13/0.57    sQ9_spl|sQ7_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f442,f478,f470])).
% 0.13/0.57  fof(f482,plain,(
% 0.13/0.57    sQ9_spl|sQ8_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f443,f478,f474])).
% 0.13/0.57  fof(f497,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(app(X0,X1))|rearsegP(app(X0,X1),X1))),
% 0.13/0.57    inference(destructive_equality_resolution,[status(thm)],[f358])).
% 0.13/0.57  fof(f501,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 0.13/0.57    inference(destructive_equality_resolution,[status(thm)],[f406])).
% 0.13/0.57  fof(f514,plain,(
% 0.13/0.57    sk1=nil|~sQ9_spl),
% 0.13/0.57    inference(backward_demodulation,[status(thm)],[f479,f435])).
% 0.13/0.57  fof(f515,plain,(
% 0.13/0.57    ~ssList(nil)|nil=nil|~ssList(nil)),
% 0.13/0.57    inference(resolution,[status(thm)],[f280,f255])).
% 0.13/0.57  fof(f516,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|nil=X0|~segmentP(nil,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|~ssList(nil))),
% 0.13/0.57    inference(resolution,[status(thm)],[f280,f374])).
% 0.13/0.57  fof(f518,definition,(
% 0.13/0.57    sQ10_spl <=> (ssList(nil))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f520,plain,(
% 0.13/0.57    ~ssList(nil)|sQ10_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f518])).
% 0.13/0.57  fof(f521,definition,(
% 0.13/0.57    sQ11_spl <=> (nil=nil)),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f524,plain,(
% 0.13/0.57    ~sQ10_spl|sQ11_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f515,f518,f521])).
% 0.13/0.57  fof(f525,definition,(
% 0.13/0.57    ![X0,X1]: (sQ12_spl <=> (~ssList(X0)|nil=X0|~segmentP(nil,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f526,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|nil=X0|~segmentP(nil,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|~sQ12_spl)),
% 0.13/0.57    inference(component_clause,[status(thm)],[f525])).
% 0.13/0.57  fof(f528,plain,(
% 0.13/0.57    sQ12_spl|~sQ10_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f516,f525,f518])).
% 0.13/0.57  fof(f530,plain,(
% 0.13/0.57    $false|sQ10_spl),
% 0.13/0.57    inference(forward_subsumption_resolution,[status(thm)],[f520,f207])).
% 0.13/0.57  fof(f531,plain,(
% 0.13/0.57    sQ10_spl),
% 0.13/0.57    inference(contradiction_clause,[status(thm)],[f530])).
% 0.13/0.57  fof(f532,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|nil=X0|~segmentP(nil,X1)|~segmentP(X1,X0)|~ssList(X1)|~sQ12_spl)),
% 0.13/0.57    inference(duplicate_literals_removal,[status(thm)],[f526])).
% 0.13/0.57  fof(f544,plain,(
% 0.13/0.57    $false|sQ5_spl|~sQ9_spl),
% 0.13/0.57    inference(forward_subsumption_resolution,[status(thm)],[f514,f464])).
% 0.13/0.57  fof(f545,plain,(
% 0.13/0.57    sQ5_spl|~sQ9_spl),
% 0.13/0.57    inference(contradiction_clause,[status(thm)],[f544])).
% 0.13/0.57  fof(f548,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|nil=X0|~rearsegP(nil,X1)|~rearsegP(X1,X0)|~ssList(X0)|~ssList(X1)|~ssList(nil))),
% 0.13/0.57    inference(resolution,[status(thm)],[f282,f376])).
% 0.13/0.57  fof(f551,definition,(
% 0.13/0.57    ![X0,X1]: (sQ13_spl <=> (~ssList(X0)|nil=X0|~rearsegP(nil,X1)|~rearsegP(X1,X0)|~ssList(X0)|~ssList(X1)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f552,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|nil=X0|~rearsegP(nil,X1)|~rearsegP(X1,X0)|~ssList(X0)|~ssList(X1)|~sQ13_spl)),
% 0.13/0.57    inference(component_clause,[status(thm)],[f551])).
% 0.13/0.57  fof(f554,plain,(
% 0.13/0.57    sQ13_spl|~sQ10_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f548,f551,f518])).
% 0.13/0.57  fof(f556,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|nil=X0|~rearsegP(nil,X1)|~rearsegP(X1,X0)|~ssList(X1)|~sQ13_spl)),
% 0.13/0.57    inference(duplicate_literals_removal,[status(thm)],[f552])).
% 0.13/0.57  fof(f557,plain,(
% 0.13/0.57    app(sk2,nil)=sk2),
% 0.13/0.57    inference(resolution,[status(thm)],[f273,f431])).
% 0.13/0.57  fof(f564,plain,(
% 0.13/0.57    app(nil,nil)=nil),
% 0.13/0.57    inference(resolution,[status(thm)],[f273,f207])).
% 0.13/0.57  fof(f565,plain,(
% 0.13/0.57    app(sk1,nil)=sk1),
% 0.13/0.57    inference(resolution,[status(thm)],[f273,f430])).
% 0.13/0.57  fof(f566,plain,(
% 0.13/0.57    ![X0]: (~rearsegP(nil,X0)|~ssList(sk2)|~ssList(X0)|~ssList(nil)|rearsegP(sk2,X0))),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f557,f350])).
% 0.13/0.57  fof(f567,definition,(
% 0.13/0.57    ![X0]: (sQ14_spl <=> (~rearsegP(nil,X0)|~ssList(X0)|rearsegP(sk2,X0)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f570,definition,(
% 0.13/0.57    sQ15_spl <=> (ssList(sk2))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f572,plain,(
% 0.13/0.57    ~ssList(sk2)|sQ15_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f570])).
% 0.13/0.57  fof(f573,plain,(
% 0.13/0.57    sQ14_spl|~sQ15_spl|~sQ10_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f566,f567,f570,f518])).
% 0.13/0.57  fof(f574,plain,(
% 0.13/0.57    ![X0]: (~rearsegP(nil,X0)|~ssList(nil)|~ssList(X0)|~ssList(nil)|rearsegP(nil,X0))),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f564,f350])).
% 0.13/0.57  fof(f575,definition,(
% 0.13/0.57    ![X0]: (sQ16_spl <=> (~rearsegP(nil,X0)|~ssList(X0)|rearsegP(nil,X0)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f578,plain,(
% 0.13/0.57    sQ16_spl|~sQ10_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f574,f575,f518])).
% 0.13/0.57  fof(f579,plain,(
% 0.13/0.57    ![X0]: (~rearsegP(nil,X0)|~ssList(sk1)|~ssList(X0)|~ssList(nil)|rearsegP(sk1,X0))),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f565,f350])).
% 0.13/0.57  fof(f580,definition,(
% 0.13/0.57    ![X0]: (sQ17_spl <=> (~rearsegP(nil,X0)|~ssList(X0)|rearsegP(sk1,X0)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f583,definition,(
% 0.13/0.57    sQ18_spl <=> (ssList(sk1))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f585,plain,(
% 0.13/0.57    ~ssList(sk1)|sQ18_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f583])).
% 0.13/0.57  fof(f586,plain,(
% 0.13/0.57    sQ17_spl|~sQ18_spl|~sQ10_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f579,f580,f583,f518])).
% 0.13/0.57  fof(f596,plain,(
% 0.13/0.57    ~ssList(sk2)|~segmentP(sk2,sk2)|~segmentP(sk1,sk2)|~sQ4_spl|~sQ3_spl),
% 0.13/0.57    inference(resolution,[status(thm)],[f459,f455])).
% 0.13/0.57  fof(f597,definition,(
% 0.13/0.57    sQ19_spl <=> (ssList(sk3))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f599,plain,(
% 0.13/0.57    ~ssList(sk3)|sQ19_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f597])).
% 0.13/0.57  fof(f607,definition,(
% 0.13/0.57    sQ22_spl <=> (segmentP(sk2,sk2))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f608,plain,(
% 0.13/0.57    segmentP(sk2,sk2)|~sQ22_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f607])).
% 0.13/0.57  fof(f609,plain,(
% 0.13/0.57    ~segmentP(sk2,sk2)|sQ22_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f607])).
% 0.13/0.57  fof(f610,definition,(
% 0.13/0.57    sQ23_spl <=> (segmentP(sk1,sk2))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f612,plain,(
% 0.13/0.57    ~segmentP(sk1,sk2)|sQ23_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f610])).
% 0.13/0.57  fof(f613,plain,(
% 0.13/0.57    ~sQ15_spl|~sQ22_spl|~sQ23_spl|~sQ4_spl|~sQ3_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f596,f570,f607,f610,f458,f454])).
% 0.13/0.57  fof(f614,plain,(
% 0.13/0.57    $false|sQ15_spl),
% 0.13/0.57    inference(forward_subsumption_resolution,[status(thm)],[f572,f431])).
% 0.13/0.57  fof(f615,plain,(
% 0.13/0.57    sQ15_spl),
% 0.13/0.57    inference(contradiction_clause,[status(thm)],[f614])).
% 0.13/0.57  fof(f621,plain,(
% 0.13/0.57    $false|sQ18_spl),
% 0.13/0.57    inference(forward_subsumption_resolution,[status(thm)],[f585,f430])).
% 0.13/0.57  fof(f622,plain,(
% 0.13/0.57    sQ18_spl),
% 0.13/0.57    inference(contradiction_clause,[status(thm)],[f621])).
% 0.13/0.57  fof(f624,plain,(
% 0.13/0.57    ~ssList(sk2)|sQ22_spl),
% 0.13/0.57    inference(resolution,[status(thm)],[f609,f256])).
% 0.13/0.57  fof(f629,plain,(
% 0.13/0.57    ~sQ15_spl|sQ22_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f624,f570,f607])).
% 0.13/0.57  fof(f644,plain,(
% 0.13/0.57    app(nil,sk2)=sk2),
% 0.13/0.57    inference(resolution,[status(thm)],[f274,f431])).
% 0.13/0.57  fof(f652,plain,(
% 0.13/0.57    app(nil,sk1)=sk1),
% 0.13/0.57    inference(resolution,[status(thm)],[f274,f430])).
% 0.13/0.57  fof(f653,plain,(
% 0.13/0.57    ![X0]: (~rearsegP(sk2,X0)|~ssList(nil)|~ssList(X0)|~ssList(sk2)|rearsegP(sk2,X0))),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f644,f350])).
% 0.13/0.57  fof(f654,definition,(
% 0.13/0.57    ![X0]: (sQ28_spl <=> (~rearsegP(sk2,X0)|~ssList(X0)|rearsegP(sk2,X0)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f657,plain,(
% 0.13/0.57    sQ28_spl|~sQ10_spl|~sQ15_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f653,f654,f518,f570])).
% 0.13/0.57  fof(f658,plain,(
% 0.13/0.57    ![X0]: (~rearsegP(sk1,X0)|~ssList(nil)|~ssList(X0)|~ssList(sk1)|rearsegP(sk1,X0))),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f652,f350])).
% 0.13/0.57  fof(f659,definition,(
% 0.13/0.57    ![X0]: (sQ29_spl <=> (~rearsegP(sk1,X0)|~ssList(X0)|rearsegP(sk1,X0)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f662,plain,(
% 0.13/0.57    sQ29_spl|~sQ10_spl|~sQ18_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f658,f659,f518,f583])).
% 0.13/0.57  fof(f670,plain,(
% 0.13/0.57    rearsegP(sk2,sk3)|~sQ8_spl),
% 0.13/0.57    inference(backward_demodulation,[status(thm)],[f434,f475])).
% 0.13/0.57  fof(f671,plain,(
% 0.13/0.57    rearsegP(sk2,sk1)|~sQ8_spl),
% 0.13/0.57    inference(backward_demodulation,[status(thm)],[f435,f670])).
% 0.13/0.57  fof(f672,plain,(
% 0.13/0.57    neq(sk1,nil)|~sQ7_spl),
% 0.13/0.57    inference(backward_demodulation,[status(thm)],[f435,f471])).
% 0.13/0.57  fof(f673,plain,(
% 0.13/0.57    sk2=nil|~sQ6_spl),
% 0.13/0.57    inference(backward_demodulation,[status(thm)],[f468,f434])).
% 0.13/0.57  fof(f675,plain,(
% 0.13/0.57    ![X0]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~ssList(X0))),
% 0.13/0.57    inference(resolution,[status(thm)],[f339,f255])).
% 0.13/0.57  fof(f678,definition,(
% 0.13/0.57    sQ30_spl <=> (sk2=sk2)),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f682,definition,(
% 0.13/0.57    ![X0]: (sQ31_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~ssList(X0)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f685,plain,(
% 0.13/0.57    sQ31_spl|~sQ10_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f675,f682,f518])).
% 0.13/0.57  fof(f690,plain,(
% 0.13/0.57    ![X0]: (~rearsegP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~ssList(X0))),
% 0.13/0.57    inference(resolution,[status(thm)],[f340,f257])).
% 0.13/0.57  fof(f701,definition,(
% 0.13/0.57    ![X0]: (sQ34_spl <=> (~rearsegP(nil,X0)|~ssList(X0)|X0=nil|~ssList(X0)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f704,plain,(
% 0.13/0.57    sQ34_spl|~sQ10_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f690,f701,f518])).
% 0.13/0.57  fof(f749,definition,(
% 0.13/0.57    sQ36_spl <=> (rearsegP(sk1,nil))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f750,plain,(
% 0.13/0.57    rearsegP(sk1,nil)|~sQ36_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f749])).
% 0.13/0.57  fof(f751,plain,(
% 0.13/0.57    ~rearsegP(sk1,nil)|sQ36_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f749])).
% 0.13/0.57  fof(f754,plain,(
% 0.13/0.57    ~ssList(sk1)|sQ36_spl),
% 0.13/0.57    inference(resolution,[status(thm)],[f751,f257])).
% 0.13/0.57  fof(f756,plain,(
% 0.13/0.57    ~sQ18_spl|sQ36_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f754,f583,f749])).
% 0.13/0.57  fof(f762,plain,(
% 0.13/0.57    rearsegP(nil,sk1)|~sQ2_spl|~sQ8_spl),
% 0.13/0.57    inference(forward_demodulation,[status(thm)],[f452,f671])).
% 0.13/0.57  fof(f764,plain,(
% 0.13/0.57    ~rearsegP(sk1,nil)|~ssList(sk1)|~ssList(nil)|nil=sk1|~sQ2_spl|~sQ8_spl),
% 0.13/0.57    inference(resolution,[status(thm)],[f762,f340])).
% 0.13/0.57  fof(f766,plain,(
% 0.13/0.57    ~sQ36_spl|~sQ18_spl|~sQ10_spl|sQ5_spl|~sQ2_spl|~sQ8_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f764,f749,f583,f518,f462,f451,f474])).
% 0.13/0.57  fof(f768,plain,(
% 0.13/0.57    ~segmentP(sk1,nil)|~sQ2_spl|sQ23_spl),
% 0.13/0.57    inference(forward_demodulation,[status(thm)],[f452,f612])).
% 0.13/0.57  fof(f769,plain,(
% 0.13/0.57    ~ssList(sk1)|~sQ2_spl|sQ23_spl),
% 0.13/0.57    inference(resolution,[status(thm)],[f768,f255])).
% 0.13/0.57  fof(f771,plain,(
% 0.13/0.57    ~sQ18_spl|~sQ2_spl|sQ23_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f769,f583,f451,f610])).
% 0.13/0.57  fof(f776,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|rearsegP(app(X0,X1),X1))),
% 0.13/0.57    inference(forward_subsumption_resolution,[status(thm)],[f497,f285])).
% 0.13/0.57  fof(f777,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X1,app(X0,X1))|~ssList(X1)|~ssList(app(X0,X1))|app(X0,X1)=X1)),
% 0.13/0.57    inference(resolution,[status(thm)],[f776,f340])).
% 0.13/0.57  fof(f779,plain,(
% 0.13/0.57    ~ssList(nil)|~ssList(sk1)|rearsegP(sk1,sk1)),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f652,f776])).
% 0.13/0.57  fof(f780,plain,(
% 0.13/0.57    ~ssList(nil)|~ssList(nil)|rearsegP(nil,nil)),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f564,f776])).
% 0.13/0.57  fof(f781,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X1,app(X0,X1))|~ssList(app(X0,X1))|app(X0,X1)=X1)),
% 0.13/0.57    inference(duplicate_literals_removal,[status(thm)],[f777])).
% 0.13/0.57  fof(f782,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~rearsegP(X1,app(X0,X1))|app(X0,X1)=X1)),
% 0.13/0.57    inference(forward_subsumption_resolution,[status(thm)],[f781,f285])).
% 0.13/0.57  fof(f784,definition,(
% 0.13/0.57    sQ39_spl <=> (rearsegP(sk1,sk1))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f785,plain,(
% 0.13/0.57    rearsegP(sk1,sk1)|~sQ39_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f784])).
% 0.13/0.57  fof(f787,plain,(
% 0.13/0.57    ~sQ10_spl|~sQ18_spl|sQ39_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f779,f518,f583,f784])).
% 0.13/0.57  fof(f788,definition,(
% 0.13/0.57    sQ40_spl <=> (rearsegP(nil,nil))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f789,plain,(
% 0.13/0.57    rearsegP(nil,nil)|~sQ40_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f788])).
% 0.13/0.57  fof(f791,plain,(
% 0.13/0.57    ~sQ10_spl|sQ40_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f780,f518,f788])).
% 0.13/0.57  fof(f792,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2))),
% 0.13/0.57    inference(resolution,[status(thm)],[f404,f255])).
% 0.13/0.57  fof(f795,definition,(
% 0.13/0.57    ![X0,X1,X2]: (sQ41_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f796,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2)|~sQ41_spl)),
% 0.13/0.57    inference(component_clause,[status(thm)],[f795])).
% 0.13/0.57  fof(f798,plain,(
% 0.13/0.57    sQ41_spl|~sQ10_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f792,f795,f518])).
% 0.13/0.57  fof(f801,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~sQ41_spl)),
% 0.13/0.57    inference(duplicate_literals_removal,[status(thm)],[f796])).
% 0.13/0.57  fof(f805,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk2)|~ssList(sk2)|segmentP(app(app(X1,sk2),X0),sk2)|~sQ22_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f608,f404])).
% 0.13/0.57  fof(f807,definition,(
% 0.13/0.57    ![X0,X1]: (sQ42_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk2),X0),sk2)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f808,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk2),X0),sk2)|~sQ42_spl)),
% 0.13/0.57    inference(component_clause,[status(thm)],[f807])).
% 0.13/0.57  fof(f810,plain,(
% 0.13/0.57    sQ42_spl|~sQ15_spl|~sQ22_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f805,f807,f570,f607])).
% 0.13/0.57  fof(f831,plain,(
% 0.13/0.57    ~rearsegP(sk1,sk1)|~ssList(sk1)|~ssList(sk1)|sk1=sk1|~sQ39_spl),
% 0.13/0.57    inference(resolution,[status(thm)],[f785,f340])).
% 0.13/0.57  fof(f832,definition,(
% 0.13/0.57    sQ44_spl <=> (sk1=sk1)),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f835,plain,(
% 0.13/0.57    ~sQ39_spl|~sQ18_spl|sQ44_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f831,f784,f583,f832])).
% 0.13/0.57  fof(f836,plain,(
% 0.13/0.57    ~ssList(nil)|~ssList(sk2)|rearsegP(sk2,sk2)),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f644,f776])).
% 0.13/0.57  fof(f839,definition,(
% 0.13/0.57    sQ45_spl <=> (rearsegP(sk2,sk2))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f840,plain,(
% 0.13/0.57    rearsegP(sk2,sk2)|~sQ45_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f839])).
% 0.13/0.57  fof(f842,plain,(
% 0.13/0.57    ~sQ10_spl|~sQ15_spl|sQ45_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f836,f518,f570,f839])).
% 0.13/0.57  fof(f849,plain,(
% 0.13/0.57    ~rearsegP(sk2,sk2)|~ssList(sk2)|~ssList(sk2)|sk2=sk2|~sQ45_spl),
% 0.13/0.57    inference(resolution,[status(thm)],[f840,f340])).
% 0.13/0.57  fof(f850,plain,(
% 0.13/0.57    ~sQ45_spl|~sQ15_spl|sQ30_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f849,f839,f570,f678])).
% 0.13/0.57  fof(f851,plain,(
% 0.13/0.57    ~ssList(sk2)|~ssList(nil)|rearsegP(sk2,nil)),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f557,f776])).
% 0.13/0.57  fof(f854,definition,(
% 0.13/0.57    sQ46_spl <=> (rearsegP(sk2,nil))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f855,plain,(
% 0.13/0.57    rearsegP(sk2,nil)|~sQ46_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f854])).
% 0.13/0.57  fof(f857,plain,(
% 0.13/0.57    ~sQ15_spl|~sQ10_spl|sQ46_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f851,f570,f518,f854])).
% 0.13/0.57  fof(f866,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~ssList(sk2)|~ssList(nil)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,nil),X0),nil))),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f557,f501])).
% 0.13/0.57  fof(f867,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(nil)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil))),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f565,f501])).
% 0.13/0.57  fof(f868,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2))),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f644,f501])).
% 0.13/0.57  fof(f869,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1))),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f652,f501])).
% 0.13/0.57  fof(f870,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil))),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f564,f501])).
% 0.13/0.57  fof(f873,definition,(
% 0.13/0.57    ![X0]: (sQ48_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,nil),X0),nil)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f876,plain,(
% 0.13/0.57    sQ48_spl|~sQ15_spl|~sQ10_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f866,f873,f570,f518])).
% 0.13/0.57  fof(f877,definition,(
% 0.13/0.57    ![X0]: (sQ49_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f880,plain,(
% 0.13/0.57    sQ49_spl|~sQ18_spl|~sQ10_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f867,f877,f583,f518])).
% 0.13/0.57  fof(f881,definition,(
% 0.13/0.57    ![X0]: (sQ50_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f884,plain,(
% 0.13/0.57    sQ50_spl|~sQ10_spl|~sQ15_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f868,f881,f518,f570])).
% 0.13/0.57  fof(f885,definition,(
% 0.13/0.57    ![X0]: (sQ51_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f888,plain,(
% 0.13/0.57    sQ51_spl|~sQ10_spl|~sQ18_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f869,f885,f518,f583])).
% 0.13/0.57  fof(f889,definition,(
% 0.13/0.57    ![X0]: (sQ52_spl <=> (~ssList(X0)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f892,plain,(
% 0.13/0.57    sQ52_spl|~sQ10_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f870,f889,f518])).
% 0.13/0.57  fof(f923,plain,(
% 0.13/0.57    sQ2_spl|~sQ6_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f673,f451,f467])).
% 0.13/0.57  fof(f969,plain,(
% 0.13/0.57    ~ssList(sk1)|~segmentP(sk2,sk1)|~segmentP(sk1,sk1)|~sQ7_spl|~sQ4_spl),
% 0.13/0.57    inference(resolution,[status(thm)],[f672,f459])).
% 0.13/0.57  fof(f970,definition,(
% 0.13/0.57    sQ59_spl <=> (segmentP(sk2,sk1))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f973,definition,(
% 0.13/0.57    sQ60_spl <=> (segmentP(sk1,sk1))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f974,plain,(
% 0.13/0.57    segmentP(sk1,sk1)|~sQ60_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f973])).
% 0.13/0.57  fof(f975,plain,(
% 0.13/0.57    ~segmentP(sk1,sk1)|sQ60_spl),
% 0.13/0.57    inference(component_clause,[status(thm)],[f973])).
% 0.13/0.57  fof(f976,plain,(
% 0.13/0.57    ~sQ18_spl|~sQ59_spl|~sQ60_spl|~sQ7_spl|~sQ4_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f969,f583,f970,f973,f470,f458])).
% 0.13/0.57  fof(f983,plain,(
% 0.13/0.57    ~ssList(sk1)|sQ60_spl),
% 0.13/0.57    inference(resolution,[status(thm)],[f975,f256])).
% 0.13/0.57  fof(f988,plain,(
% 0.13/0.57    ~sQ18_spl|sQ60_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f983,f583,f973])).
% 0.13/0.57  fof(f989,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk1)|~ssList(sk1)|segmentP(app(app(X1,sk1),X0),sk1)|~sQ60_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f974,f404])).
% 0.13/0.57  fof(f991,definition,(
% 0.13/0.57    ![X0,X1]: (sQ63_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),sk1)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f992,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),sk1)|~sQ63_spl)),
% 0.13/0.57    inference(component_clause,[status(thm)],[f991])).
% 0.13/0.57  fof(f994,plain,(
% 0.13/0.57    sQ63_spl|~sQ18_spl|~sQ60_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f989,f991,f583,f973])).
% 0.13/0.57  fof(f1028,plain,(
% 0.13/0.57    ~ssList(nil)|~ssList(sk1)|~rearsegP(sk1,sk1)|app(nil,sk1)=sk1),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f652,f782])).
% 0.13/0.57  fof(f1029,plain,(
% 0.13/0.57    ~ssList(nil)|~ssList(sk2)|~rearsegP(sk2,sk2)|app(nil,sk2)=sk2),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f644,f782])).
% 0.13/0.57  fof(f1030,plain,(
% 0.13/0.57    ~ssList(nil)|~ssList(nil)|~rearsegP(nil,nil)|app(nil,nil)=nil),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f564,f782])).
% 0.13/0.57  fof(f1042,definition,(
% 0.13/0.57    sQ66_spl <=> (app(nil,sk1)=sk1)),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1045,plain,(
% 0.13/0.57    ~sQ10_spl|~sQ18_spl|~sQ39_spl|sQ66_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1028,f518,f583,f784,f1042])).
% 0.13/0.57  fof(f1046,definition,(
% 0.13/0.57    sQ67_spl <=> (app(nil,sk2)=sk2)),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1049,plain,(
% 0.13/0.57    ~sQ10_spl|~sQ15_spl|~sQ45_spl|sQ67_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1029,f518,f570,f839,f1046])).
% 0.13/0.57  fof(f1050,definition,(
% 0.13/0.57    sQ68_spl <=> (app(nil,nil)=nil)),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1053,plain,(
% 0.13/0.57    ~sQ10_spl|~sQ40_spl|sQ68_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1030,f518,f788,f1050])).
% 0.13/0.57  fof(f1054,plain,(
% 0.13/0.57    ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(sk2)|~ssList(app(app(X1,sk2),X0))|segmentP(app(app(X3,app(app(X1,sk2),X0)),X2),sk2)|~sQ42_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f808,f404])).
% 0.13/0.57  fof(f1055,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(sk2,app(app(X1,sk2),X0))|~ssList(sk2)|~ssList(app(app(X1,sk2),X0))|app(app(X1,sk2),X0)=sk2|~sQ42_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f808,f339])).
% 0.13/0.57  fof(f1056,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~ssList(nil)|segmentP(app(sk2,X0),sk2)|~sQ42_spl)),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f644,f808])).
% 0.13/0.57  fof(f1057,definition,(
% 0.13/0.57    ![X0,X1,X2,X3]: (sQ69_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),sk2)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1058,plain,(
% 0.13/0.57    ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(app(app(X1,sk2),X0))|segmentP(app(app(X3,app(app(X1,sk2),X0)),X2),sk2)|~sQ69_spl)),
% 0.13/0.57    inference(component_clause,[status(thm)],[f1057])).
% 0.13/0.57  fof(f1060,plain,(
% 0.13/0.57    sQ69_spl|~sQ15_spl|~sQ42_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1054,f1057,f570,f807])).
% 0.13/0.57  fof(f1061,definition,(
% 0.13/0.57    ![X0,X1]: (sQ70_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(sk2,app(app(X1,sk2),X0))|~ssList(app(app(X1,sk2),X0))|app(app(X1,sk2),X0)=sk2))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1064,plain,(
% 0.13/0.57    sQ70_spl|~sQ15_spl|~sQ42_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1055,f1061,f570,f807])).
% 0.13/0.57  fof(f1065,definition,(
% 0.13/0.57    ![X0]: (sQ71_spl <=> (~ssList(X0)|segmentP(app(sk2,X0),sk2)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1066,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|segmentP(app(sk2,X0),sk2)|~sQ71_spl)),
% 0.13/0.57    inference(component_clause,[status(thm)],[f1065])).
% 0.13/0.57  fof(f1068,plain,(
% 0.13/0.57    sQ71_spl|~sQ10_spl|~sQ42_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1056,f1065,f518,f807])).
% 0.13/0.57  fof(f1069,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),sk2)|~sQ71_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f1066,f404])).
% 0.13/0.57  fof(f1070,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~segmentP(sk2,app(sk2,X0))|~ssList(sk2)|~ssList(app(sk2,X0))|app(sk2,X0)=sk2|~sQ71_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f1066,f339])).
% 0.13/0.57  fof(f1072,definition,(
% 0.13/0.57    ![X0,X1,X2]: (sQ72_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),sk2)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1075,plain,(
% 0.13/0.57    sQ72_spl|~sQ15_spl|~sQ71_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1069,f1072,f570,f1065])).
% 0.13/0.57  fof(f1076,definition,(
% 0.13/0.57    ![X0]: (sQ73_spl <=> (~ssList(X0)|~segmentP(sk2,app(sk2,X0))|~ssList(app(sk2,X0))|app(sk2,X0)=sk2))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1079,plain,(
% 0.13/0.57    sQ73_spl|~sQ15_spl|~sQ71_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1070,f1076,f570,f1065])).
% 0.13/0.57  fof(f1081,plain,(
% 0.13/0.57    ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(sk1)|~ssList(app(app(X1,sk1),X0))|segmentP(app(app(X3,app(app(X1,sk1),X0)),X2),sk1)|~sQ63_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f992,f404])).
% 0.13/0.57  fof(f1082,plain,(
% 0.13/0.57    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(sk1,app(app(X1,sk1),X0))|~ssList(sk1)|~ssList(app(app(X1,sk1),X0))|app(app(X1,sk1),X0)=sk1|~sQ63_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f992,f339])).
% 0.13/0.57  fof(f1083,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~ssList(nil)|segmentP(app(sk1,X0),sk1)|~sQ63_spl)),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f652,f992])).
% 0.13/0.57  fof(f1084,definition,(
% 0.13/0.57    ![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),sk1)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1087,plain,(
% 0.13/0.57    sQ74_spl|~sQ18_spl|~sQ63_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1081,f1084,f583,f991])).
% 0.13/0.57  fof(f1088,definition,(
% 0.13/0.57    ![X0,X1]: (sQ75_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(sk1,app(app(X1,sk1),X0))|~ssList(app(app(X1,sk1),X0))|app(app(X1,sk1),X0)=sk1))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1091,plain,(
% 0.13/0.57    sQ75_spl|~sQ18_spl|~sQ63_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1082,f1088,f583,f991])).
% 0.13/0.57  fof(f1092,definition,(
% 0.13/0.57    ![X0]: (sQ76_spl <=> (~ssList(X0)|segmentP(app(sk1,X0),sk1)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1093,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~sQ76_spl)),
% 0.13/0.57    inference(component_clause,[status(thm)],[f1092])).
% 0.13/0.57  fof(f1095,plain,(
% 0.13/0.57    sQ76_spl|~sQ10_spl|~sQ63_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1083,f1092,f518,f991])).
% 0.13/0.57  fof(f1097,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),sk1)|~sQ76_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f1093,f404])).
% 0.13/0.57  fof(f1098,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~segmentP(sk1,app(sk1,X0))|~ssList(sk1)|~ssList(app(sk1,X0))|app(sk1,X0)=sk1|~sQ76_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f1093,f339])).
% 0.13/0.57  fof(f1100,definition,(
% 0.13/0.57    ![X0,X1,X2]: (sQ77_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),sk1)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1103,plain,(
% 0.13/0.57    sQ77_spl|~sQ18_spl|~sQ76_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1097,f1100,f583,f1092])).
% 0.13/0.57  fof(f1104,definition,(
% 0.13/0.57    ![X0]: (sQ78_spl <=> (~ssList(X0)|~segmentP(sk1,app(sk1,X0))|~ssList(app(sk1,X0))|app(sk1,X0)=sk1))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1107,plain,(
% 0.13/0.57    sQ78_spl|~sQ18_spl|~sQ76_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1098,f1104,f583,f1092])).
% 0.13/0.57  fof(f1129,plain,(
% 0.13/0.57    ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|segmentP(app(app(X3,app(app(X1,sk2),X0)),X2),sk2)|~ssList(X0)|~ssList(app(X1,sk2))|~sQ69_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f1058,f285])).
% 0.13/0.57  fof(f1130,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~ssList(X0)|~ssList(nil)|~ssList(X1)|~ssList(X2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(app(nil,sk2),X0)),X1),sk2)|~sQ69_spl)),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f644,f1058])).
% 0.13/0.57  fof(f1131,plain,(
% 0.13/0.57    ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|segmentP(app(app(X3,app(app(X1,sk2),X0)),X2),sk2)|~ssList(app(X1,sk2))|~sQ69_spl)),
% 0.13/0.57    inference(duplicate_literals_removal,[status(thm)],[f1129])).
% 0.13/0.57  fof(f1132,definition,(
% 0.13/0.57    ![X0,X1,X2]: (sQ79_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(app(nil,sk2),X0)),X1),sk2)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1135,plain,(
% 0.13/0.57    sQ79_spl|~sQ10_spl|~sQ69_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1130,f1132,f518,f1057])).
% 0.13/0.57  fof(f1137,plain,(
% 0.13/0.57    ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|segmentP(app(app(X3,app(app(X1,sk2),X0)),X2),sk2)|~ssList(sk2)|~ssList(X1)|~sQ69_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f1131,f285])).
% 0.13/0.57  fof(f1138,plain,(
% 0.13/0.57    ![X0,X1,X2]: (~ssList(X0)|~ssList(nil)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X2,app(app(nil,sk2),X0)),X1),sk2)|~ssList(sk2)|~sQ69_spl)),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f644,f1131])).
% 0.13/0.57  fof(f1139,definition,(
% 0.13/0.57    ![X0,X1,X2,X3]: (sQ80_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|segmentP(app(app(X3,app(app(X1,sk2),X0)),X2),sk2)|~ssList(X1)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1142,plain,(
% 0.13/0.57    sQ80_spl|~sQ15_spl|~sQ69_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1137,f1139,f570,f1057])).
% 0.13/0.57  fof(f1143,definition,(
% 0.13/0.57    ![X0,X1,X2]: (sQ81_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X2,app(app(nil,sk2),X0)),X1),sk2)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1146,plain,(
% 0.13/0.57    sQ81_spl|~sQ10_spl|~sQ15_spl|~sQ69_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1138,f1143,f518,f570,f1057])).
% 0.13/0.57  fof(f1149,plain,(
% 0.13/0.57    ~ssList(sk1)|sQ19_spl),
% 0.13/0.57    inference(forward_demodulation,[status(thm)],[f435,f599])).
% 0.13/0.57  fof(f1150,plain,(
% 0.13/0.57    $false|sQ19_spl),
% 0.13/0.57    inference(forward_subsumption_resolution,[status(thm)],[f1149,f430])).
% 0.13/0.57  fof(f1151,plain,(
% 0.13/0.57    sQ19_spl),
% 0.13/0.57    inference(contradiction_clause,[status(thm)],[f1150])).
% 0.13/0.57  fof(f1156,plain,(
% 0.13/0.57    ![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)|~sQ41_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f801,f404])).
% 0.13/0.57  fof(f1157,plain,(
% 0.13/0.57    ![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|~sQ41_spl)),
% 0.13/0.57    inference(resolution,[status(thm)],[f801,f339])).
% 0.13/0.57  fof(f1158,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(nil)|segmentP(app(sk1,X0),nil)|~sQ41_spl)),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f565,f801])).
% 0.13/0.57  fof(f1159,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~ssList(sk2)|~ssList(nil)|segmentP(app(sk2,X0),nil)|~sQ41_spl)),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f557,f801])).
% 0.13/0.57  fof(f1162,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|segmentP(app(nil,X0),nil)|~sQ41_spl)),
% 0.13/0.57    inference(paramodulation,[status(thm)],[f564,f801])).
% 0.13/0.57  fof(f1163,definition,(
% 0.13/0.57    ![X0,X1,X2,X3,X4]: (sQ82_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)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1166,plain,(
% 0.13/0.57    sQ82_spl|~sQ10_spl|~sQ41_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1156,f1163,f518,f795])).
% 0.13/0.57  fof(f1167,definition,(
% 0.13/0.57    ![X0,X1,X2]: (sQ83_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))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1170,plain,(
% 0.13/0.57    sQ83_spl|~sQ10_spl|~sQ41_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1157,f1167,f518,f795])).
% 0.13/0.57  fof(f1171,definition,(
% 0.13/0.57    ![X0]: (sQ84_spl <=> (~ssList(X0)|segmentP(app(sk1,X0),nil)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1172,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),nil)|~sQ84_spl)),
% 0.13/0.57    inference(component_clause,[status(thm)],[f1171])).
% 0.13/0.57  fof(f1174,plain,(
% 0.13/0.57    sQ84_spl|~sQ18_spl|~sQ10_spl|~sQ41_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1158,f1171,f583,f518,f795])).
% 0.13/0.57  fof(f1175,definition,(
% 0.13/0.57    ![X0]: (sQ85_spl <=> (~ssList(X0)|segmentP(app(sk2,X0),nil)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.13/0.57  fof(f1176,plain,(
% 0.13/0.57    ![X0]: (~ssList(X0)|segmentP(app(sk2,X0),nil)|~sQ85_spl)),
% 0.13/0.57    inference(component_clause,[status(thm)],[f1175])).
% 0.13/0.57  fof(f1178,plain,(
% 0.13/0.57    sQ85_spl|~sQ15_spl|~sQ10_spl|~sQ41_spl),
% 0.13/0.57    inference(split_clause,[status(thm)],[f1159,f1175,f570,f518,f795])).
% 0.13/0.57  fof(f1181,definition,(
% 0.13/0.57    ![X0]: (sQ86_spl <=> (~ssList(X0)|segmentP(app(nil,X0),nil)))),
% 0.13/0.57    introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1182,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|segmentP(app(nil,X0),nil)|~sQ86_spl)),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1181])).
% 0.13/0.58  fof(f1184,plain,(
% 0.13/0.58    sQ86_spl|~sQ10_spl|~sQ41_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1162,f1181,f518,f795])).
% 0.13/0.58  fof(f1185,plain,(
% 0.13/0.58    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(nil)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),nil)|~sQ84_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f1172,f404])).
% 0.13/0.58  fof(f1186,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|~segmentP(nil,app(sk1,X0))|~ssList(nil)|~ssList(app(sk1,X0))|app(sk1,X0)=nil|~sQ84_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f1172,f339])).
% 0.13/0.58  fof(f1187,plain,(
% 0.13/0.58    ~ssList(nil)|segmentP(sk1,nil)|~sQ84_spl),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f565,f1172])).
% 0.13/0.58  fof(f1188,definition,(
% 0.13/0.58    ![X0,X1,X2]: (sQ87_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1191,plain,(
% 0.13/0.58    sQ87_spl|~sQ10_spl|~sQ84_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1185,f1188,f518,f1171])).
% 0.13/0.58  fof(f1192,definition,(
% 0.13/0.58    ![X0]: (sQ88_spl <=> (~ssList(X0)|~segmentP(nil,app(sk1,X0))|~ssList(app(sk1,X0))|app(sk1,X0)=nil))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1195,plain,(
% 0.13/0.58    sQ88_spl|~sQ10_spl|~sQ84_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1186,f1192,f518,f1171])).
% 0.13/0.58  fof(f1196,definition,(
% 0.13/0.58    sQ89_spl <=> (segmentP(sk1,nil))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1197,plain,(
% 0.13/0.58    segmentP(sk1,nil)|~sQ89_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1196])).
% 0.13/0.58  fof(f1199,plain,(
% 0.13/0.58    ~sQ10_spl|sQ89_spl|~sQ84_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1187,f518,f1196,f1171])).
% 0.13/0.58  fof(f1200,plain,(
% 0.13/0.58    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(sk1)|segmentP(app(app(X1,sk1),X0),nil)|~sQ89_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f1197,f404])).
% 0.13/0.58  fof(f1202,definition,(
% 0.13/0.58    ![X0,X1]: (sQ90_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1205,plain,(
% 0.13/0.58    sQ90_spl|~sQ10_spl|~sQ18_spl|~sQ89_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1200,f1202,f518,f583,f1196])).
% 0.13/0.58  fof(f1215,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|nil=X0|~segmentP(nil,X0)|~ssList(nil)|~ssList(nil)|~sQ12_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f532,f255])).
% 0.13/0.58  fof(f1216,plain,(
% 0.13/0.58    ![X0,X1,X2]: (~ssList(X0)|nil=X0|~segmentP(X1,X0)|~ssList(X1)|~segmentP(nil,X2)|~segmentP(X2,X1)|~ssList(X1)|~ssList(X2)|~ssList(nil)|~sQ12_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f532,f374])).
% 0.13/0.58  fof(f1218,definition,(
% 0.13/0.58    ![X0]: (sQ93_spl <=> (~ssList(X0)|nil=X0|~segmentP(nil,X0)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1221,plain,(
% 0.13/0.58    sQ93_spl|~sQ10_spl|~sQ12_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1215,f1218,f518,f525])).
% 0.13/0.58  fof(f1222,definition,(
% 0.13/0.58    ![X0,X1,X2]: (sQ94_spl <=> (~ssList(X0)|nil=X0|~segmentP(X1,X0)|~ssList(X1)|~segmentP(nil,X2)|~segmentP(X2,X1)|~ssList(X1)|~ssList(X2)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1225,plain,(
% 0.13/0.58    sQ94_spl|~sQ10_spl|~sQ12_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1216,f1222,f518,f525])).
% 0.13/0.58  fof(f1229,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|nil=X0|~rearsegP(nil,X0)|~ssList(nil)|~ssList(nil)|~sQ13_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f556,f257])).
% 0.13/0.58  fof(f1230,plain,(
% 0.13/0.58    ![X0,X1,X2]: (~ssList(X0)|nil=X0|~rearsegP(X1,X0)|~ssList(X1)|~rearsegP(nil,X2)|~rearsegP(X2,X1)|~ssList(X1)|~ssList(X2)|~ssList(nil)|~sQ13_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f556,f376])).
% 0.13/0.58  fof(f1232,definition,(
% 0.13/0.58    ![X0]: (sQ95_spl <=> (~ssList(X0)|nil=X0|~rearsegP(nil,X0)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1236,plain,(
% 0.13/0.58    sQ95_spl|~sQ10_spl|~sQ13_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1229,f1232,f518,f551])).
% 0.13/0.58  fof(f1237,definition,(
% 0.13/0.58    ![X0,X1,X2]: (sQ96_spl <=> (~ssList(X0)|nil=X0|~rearsegP(X1,X0)|~ssList(X1)|~rearsegP(nil,X2)|~rearsegP(X2,X1)|~ssList(X1)|~ssList(X2)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1240,plain,(
% 0.13/0.58    sQ96_spl|~sQ10_spl|~sQ13_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1230,f1237,f518,f551])).
% 0.13/0.58  fof(f1243,plain,(
% 0.13/0.58    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(nil)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),nil)|~sQ85_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f1176,f404])).
% 0.13/0.58  fof(f1244,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|~segmentP(nil,app(sk2,X0))|~ssList(nil)|~ssList(app(sk2,X0))|app(sk2,X0)=nil|~sQ85_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f1176,f339])).
% 0.13/0.58  fof(f1245,plain,(
% 0.13/0.58    ~ssList(nil)|segmentP(sk2,nil)|~sQ85_spl),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f557,f1176])).
% 0.13/0.58  fof(f1246,definition,(
% 0.13/0.58    ![X0,X1,X2]: (sQ97_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1249,plain,(
% 0.13/0.58    sQ97_spl|~sQ10_spl|~sQ85_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1243,f1246,f518,f1175])).
% 0.13/0.58  fof(f1250,definition,(
% 0.13/0.58    ![X0]: (sQ98_spl <=> (~ssList(X0)|~segmentP(nil,app(sk2,X0))|~ssList(app(sk2,X0))|app(sk2,X0)=nil))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1253,plain,(
% 0.13/0.58    sQ98_spl|~sQ10_spl|~sQ85_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1244,f1250,f518,f1175])).
% 0.13/0.58  fof(f1254,definition,(
% 0.13/0.58    sQ99_spl <=> (segmentP(sk2,nil))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1255,plain,(
% 0.13/0.58    segmentP(sk2,nil)|~sQ99_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1254])).
% 0.13/0.58  fof(f1257,plain,(
% 0.13/0.58    ~sQ10_spl|sQ99_spl|~sQ85_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1245,f518,f1254,f1175])).
% 0.13/0.58  fof(f1258,plain,(
% 0.13/0.58    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(sk2)|segmentP(app(app(X1,sk2),X0),nil)|~sQ99_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f1255,f404])).
% 0.13/0.58  fof(f1260,definition,(
% 0.13/0.58    ![X0,X1]: (sQ100_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk2),X0),nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1263,plain,(
% 0.13/0.58    sQ100_spl|~sQ10_spl|~sQ15_spl|~sQ99_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1258,f1260,f518,f570,f1254])).
% 0.13/0.58  fof(f1270,plain,(
% 0.13/0.58    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(nil)|~ssList(app(nil,X0))|segmentP(app(app(X2,app(nil,X0)),X1),nil)|~sQ86_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f1182,f404])).
% 0.13/0.58  fof(f1271,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|~segmentP(nil,app(nil,X0))|~ssList(nil)|~ssList(app(nil,X0))|app(nil,X0)=nil|~sQ86_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f1182,f339])).
% 0.13/0.58  fof(f1274,plain,(
% 0.13/0.58    ~ssList(nil)|segmentP(nil,nil)|~sQ86_spl),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f564,f1182])).
% 0.13/0.58  fof(f1275,definition,(
% 0.13/0.58    ![X0,X1,X2]: (sQ102_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(nil,X0))|segmentP(app(app(X2,app(nil,X0)),X1),nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1278,plain,(
% 0.13/0.58    sQ102_spl|~sQ10_spl|~sQ86_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1270,f1275,f518,f1181])).
% 0.13/0.58  fof(f1279,definition,(
% 0.13/0.58    ![X0]: (sQ103_spl <=> (~ssList(X0)|~segmentP(nil,app(nil,X0))|~ssList(app(nil,X0))|app(nil,X0)=nil))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1282,plain,(
% 0.13/0.58    sQ103_spl|~sQ10_spl|~sQ86_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1271,f1279,f518,f1181])).
% 0.13/0.58  fof(f1285,definition,(
% 0.13/0.58    sQ104_spl <=> (segmentP(nil,nil))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1286,plain,(
% 0.13/0.58    segmentP(nil,nil)|~sQ104_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1285])).
% 0.13/0.58  fof(f1288,plain,(
% 0.13/0.58    ~sQ10_spl|sQ104_spl|~sQ86_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1274,f518,f1285,f1181])).
% 0.13/0.58  fof(f1291,plain,(
% 0.13/0.58    ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(nil)|segmentP(app(app(X1,nil),X0),nil)|~sQ104_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f1286,f404])).
% 0.13/0.58  fof(f1295,definition,(
% 0.13/0.58    ![X0,X1]: (sQ105_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,nil),X0),nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1298,plain,(
% 0.13/0.58    sQ105_spl|~sQ10_spl|~sQ104_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1291,f1295,f518,f1285])).
% 0.13/0.58  fof(f1300,plain,(
% 0.13/0.58    ~ssList(nil)|~ssList(sk1)|app(skaf46(sk1,nil),nil)=sk1|~sQ36_spl),
% 0.13/0.58    inference(resolution,[status(thm)],[f343,f750])).
% 0.13/0.58  fof(f1301,plain,(
% 0.13/0.58    ~ssList(sk1)|~ssList(sk1)|app(skaf46(sk1,sk1),sk1)=sk1|~sQ39_spl),
% 0.13/0.58    inference(resolution,[status(thm)],[f343,f785])).
% 0.13/0.58  fof(f1302,plain,(
% 0.13/0.58    ~ssList(nil)|~ssList(nil)|app(skaf46(nil,nil),nil)=nil|~sQ40_spl),
% 0.13/0.58    inference(resolution,[status(thm)],[f343,f789])).
% 0.13/0.58  fof(f1303,plain,(
% 0.13/0.58    ~ssList(sk1)|~ssList(sk2)|app(skaf46(sk2,sk1),sk1)=sk2|~sQ8_spl),
% 0.13/0.58    inference(resolution,[status(thm)],[f343,f671])).
% 0.13/0.58  fof(f1304,plain,(
% 0.13/0.58    ~ssList(nil)|~ssList(sk2)|app(skaf46(sk2,nil),nil)=sk2|~sQ46_spl),
% 0.13/0.58    inference(resolution,[status(thm)],[f343,f855])).
% 0.13/0.58  fof(f1305,plain,(
% 0.13/0.58    ~ssList(sk2)|~ssList(sk2)|app(skaf46(sk2,sk2),sk2)=sk2|~sQ45_spl),
% 0.13/0.58    inference(resolution,[status(thm)],[f343,f840])).
% 0.13/0.58  fof(f1308,plain,(
% 0.13/0.58    ![X0]: (~ssList(nil)|~ssList(X0)|app(skaf46(X0,nil),nil)=X0|~ssList(X0))),
% 0.13/0.58    inference(resolution,[status(thm)],[f343,f257])).
% 0.13/0.58  fof(f1311,definition,(
% 0.13/0.58    sQ106_spl <=> (app(skaf46(sk1,nil),nil)=sk1)),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1312,plain,(
% 0.13/0.58    app(skaf46(sk1,nil),nil)=sk1|~sQ106_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1311])).
% 0.13/0.58  fof(f1314,plain,(
% 0.13/0.58    ~sQ10_spl|~sQ18_spl|sQ106_spl|~sQ36_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1300,f518,f583,f1311,f749])).
% 0.13/0.58  fof(f1315,definition,(
% 0.13/0.58    sQ107_spl <=> (app(skaf46(sk1,sk1),sk1)=sk1)),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1316,plain,(
% 0.13/0.58    app(skaf46(sk1,sk1),sk1)=sk1|~sQ107_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1315])).
% 0.13/0.58  fof(f1318,plain,(
% 0.13/0.58    ~sQ18_spl|sQ107_spl|~sQ39_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1301,f583,f1315,f784])).
% 0.13/0.58  fof(f1319,definition,(
% 0.13/0.58    sQ108_spl <=> (app(skaf46(nil,nil),nil)=nil)),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1320,plain,(
% 0.13/0.58    app(skaf46(nil,nil),nil)=nil|~sQ108_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1319])).
% 0.13/0.58  fof(f1322,plain,(
% 0.13/0.58    ~sQ10_spl|sQ108_spl|~sQ40_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1302,f518,f1319,f788])).
% 0.13/0.58  fof(f1323,definition,(
% 0.13/0.58    sQ109_spl <=> (app(skaf46(sk2,sk1),sk1)=sk2)),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1324,plain,(
% 0.13/0.58    app(skaf46(sk2,sk1),sk1)=sk2|~sQ109_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1323])).
% 0.13/0.58  fof(f1326,plain,(
% 0.13/0.58    ~sQ18_spl|~sQ15_spl|sQ109_spl|~sQ8_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1303,f583,f570,f1323,f474])).
% 0.13/0.58  fof(f1327,definition,(
% 0.13/0.58    sQ110_spl <=> (app(skaf46(sk2,nil),nil)=sk2)),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1328,plain,(
% 0.13/0.58    app(skaf46(sk2,nil),nil)=sk2|~sQ110_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1327])).
% 0.13/0.58  fof(f1330,plain,(
% 0.13/0.58    ~sQ10_spl|~sQ15_spl|sQ110_spl|~sQ46_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1304,f518,f570,f1327,f854])).
% 0.13/0.58  fof(f1331,definition,(
% 0.13/0.58    sQ111_spl <=> (app(skaf46(sk2,sk2),sk2)=sk2)),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1332,plain,(
% 0.13/0.58    app(skaf46(sk2,sk2),sk2)=sk2|~sQ111_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1331])).
% 0.13/0.58  fof(f1334,plain,(
% 0.13/0.58    ~sQ15_spl|sQ111_spl|~sQ45_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1305,f570,f1331,f839])).
% 0.13/0.58  fof(f1339,definition,(
% 0.13/0.58    ![X0]: (sQ112_spl <=> (~ssList(X0)|app(skaf46(X0,nil),nil)=X0|~ssList(X0)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1342,plain,(
% 0.13/0.58    ~sQ10_spl|sQ112_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1308,f518,f1339])).
% 0.13/0.58  fof(f1362,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|~ssList(skaf46(sk1,sk1))|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(skaf46(sk1,sk1),sk1),X0),sk1)|~sQ107_spl)),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f1316,f501])).
% 0.13/0.58  fof(f1366,definition,(
% 0.13/0.58    sQ113_spl <=> (ssList(skaf46(sk1,sk1)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1368,plain,(
% 0.13/0.58    ~ssList(skaf46(sk1,sk1))|sQ113_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1366])).
% 0.13/0.58  fof(f1372,definition,(
% 0.13/0.58    ![X0]: (sQ114_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(skaf46(sk1,sk1),sk1),X0),sk1)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1375,plain,(
% 0.13/0.58    sQ114_spl|~sQ113_spl|~sQ18_spl|~sQ107_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1362,f1372,f1366,f583,f1315])).
% 0.13/0.58  fof(f1379,plain,(
% 0.13/0.58    $false|sQ113_spl),
% 0.13/0.58    inference(forward_subsumption_resolution,[status(thm)],[f1368,f249])).
% 0.13/0.58  fof(f1380,plain,(
% 0.13/0.58    sQ113_spl),
% 0.13/0.58    inference(contradiction_clause,[status(thm)],[f1379])).
% 0.13/0.58  fof(f1382,plain,(
% 0.13/0.58    ![X0,X1,X2]: (~ssList(X0)|~ssList(skaf46(sk2,sk2))|~ssList(X1)|~ssList(X2)|segmentP(app(app(X2,app(app(skaf46(sk2,sk2),sk2),X0)),X1),sk2)|~ssList(sk2)|~sQ69_spl|~sQ111_spl)),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f1332,f1131])).
% 0.13/0.58  fof(f1383,plain,(
% 0.13/0.58    ![X0,X1,X2]: (~ssList(X0)|~ssList(skaf46(sk2,sk2))|~ssList(X1)|~ssList(X2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(app(skaf46(sk2,sk2),sk2),X0)),X1),sk2)|~sQ69_spl|~sQ111_spl)),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f1332,f1058])).
% 0.13/0.58  fof(f1387,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|~ssList(skaf46(sk2,sk2))|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(skaf46(sk2,sk2),sk2),X0),sk2)|~sQ111_spl)),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f1332,f501])).
% 0.13/0.58  fof(f1391,definition,(
% 0.13/0.58    ![X0,X1,X2]: (sQ115_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X2,app(app(skaf46(sk2,sk2),sk2),X0)),X1),sk2)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1394,definition,(
% 0.13/0.58    sQ116_spl <=> (ssList(skaf46(sk2,sk2)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1396,plain,(
% 0.13/0.58    ~ssList(skaf46(sk2,sk2))|sQ116_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1394])).
% 0.13/0.58  fof(f1397,plain,(
% 0.13/0.58    sQ115_spl|~sQ116_spl|~sQ15_spl|~sQ69_spl|~sQ111_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1382,f1391,f1394,f570,f1057,f1331])).
% 0.13/0.58  fof(f1398,definition,(
% 0.13/0.58    ![X0,X1,X2]: (sQ117_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(app(skaf46(sk2,sk2),sk2),X0)),X1),sk2)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1401,plain,(
% 0.13/0.58    sQ117_spl|~sQ116_spl|~sQ69_spl|~sQ111_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1383,f1398,f1394,f1057,f1331])).
% 0.13/0.58  fof(f1405,definition,(
% 0.13/0.58    ![X0]: (sQ118_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(skaf46(sk2,sk2),sk2),X0),sk2)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1408,plain,(
% 0.13/0.58    sQ118_spl|~sQ116_spl|~sQ15_spl|~sQ111_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1387,f1405,f1394,f570,f1331])).
% 0.13/0.58  fof(f1412,plain,(
% 0.13/0.58    $false|sQ116_spl),
% 0.13/0.58    inference(forward_subsumption_resolution,[status(thm)],[f1396,f249])).
% 0.13/0.58  fof(f1413,plain,(
% 0.13/0.58    sQ116_spl),
% 0.13/0.58    inference(contradiction_clause,[status(thm)],[f1412])).
% 0.13/0.58  fof(f1584,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|~ssList(skaf46(nil,nil))|~ssList(nil)|~ssList(app(nil,X0))|segmentP(app(app(skaf46(nil,nil),nil),X0),nil)|~sQ108_spl)),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f1320,f501])).
% 0.13/0.58  fof(f1588,definition,(
% 0.13/0.58    sQ125_spl <=> (ssList(skaf46(nil,nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1590,plain,(
% 0.13/0.58    ~ssList(skaf46(nil,nil))|sQ125_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1588])).
% 0.13/0.58  fof(f1593,definition,(
% 0.13/0.58    ![X0]: (sQ126_spl <=> (~ssList(X0)|~ssList(app(nil,X0))|segmentP(app(app(skaf46(nil,nil),nil),X0),nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1596,plain,(
% 0.13/0.58    sQ126_spl|~sQ125_spl|~sQ10_spl|~sQ108_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1584,f1593,f1588,f518,f1319])).
% 0.13/0.58  fof(f1600,plain,(
% 0.13/0.58    $false|sQ125_spl),
% 0.13/0.58    inference(forward_subsumption_resolution,[status(thm)],[f1590,f249])).
% 0.13/0.58  fof(f1601,plain,(
% 0.13/0.58    sQ125_spl),
% 0.13/0.58    inference(contradiction_clause,[status(thm)],[f1600])).
% 0.13/0.58  fof(f1605,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|~ssList(skaf46(sk2,nil))|~ssList(nil)|~ssList(app(sk2,X0))|segmentP(app(app(skaf46(sk2,nil),nil),X0),nil)|~sQ110_spl)),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f1328,f501])).
% 0.13/0.58  fof(f1609,definition,(
% 0.13/0.58    sQ127_spl <=> (ssList(skaf46(sk2,nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1611,plain,(
% 0.13/0.58    ~ssList(skaf46(sk2,nil))|sQ127_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1609])).
% 0.13/0.58  fof(f1617,definition,(
% 0.13/0.58    ![X0]: (sQ129_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(skaf46(sk2,nil),nil),X0),nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1620,plain,(
% 0.13/0.58    sQ129_spl|~sQ127_spl|~sQ10_spl|~sQ110_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1605,f1617,f1609,f518,f1327])).
% 0.13/0.58  fof(f1624,plain,(
% 0.13/0.58    $false|sQ127_spl),
% 0.13/0.58    inference(forward_subsumption_resolution,[status(thm)],[f1611,f249])).
% 0.13/0.58  fof(f1625,plain,(
% 0.13/0.58    sQ127_spl),
% 0.13/0.58    inference(contradiction_clause,[status(thm)],[f1624])).
% 0.13/0.58  fof(f1629,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|~ssList(skaf46(sk1,nil))|~ssList(nil)|~ssList(app(sk1,X0))|segmentP(app(app(skaf46(sk1,nil),nil),X0),nil)|~sQ106_spl)),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f1312,f501])).
% 0.13/0.58  fof(f1633,definition,(
% 0.13/0.58    sQ130_spl <=> (ssList(skaf46(sk1,nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1635,plain,(
% 0.13/0.58    ~ssList(skaf46(sk1,nil))|sQ130_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1633])).
% 0.13/0.58  fof(f1641,definition,(
% 0.13/0.58    ![X0]: (sQ132_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(skaf46(sk1,nil),nil),X0),nil)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1644,plain,(
% 0.13/0.58    sQ132_spl|~sQ130_spl|~sQ10_spl|~sQ106_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1629,f1641,f1633,f518,f1311])).
% 0.13/0.58  fof(f1648,plain,(
% 0.13/0.58    $false|sQ130_spl),
% 0.13/0.58    inference(forward_subsumption_resolution,[status(thm)],[f1635,f249])).
% 0.13/0.58  fof(f1649,plain,(
% 0.13/0.58    sQ130_spl),
% 0.13/0.58    inference(contradiction_clause,[status(thm)],[f1648])).
% 0.13/0.58  fof(f1651,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|~ssList(skaf46(sk2,sk1))|segmentP(app(sk2,X0),sk1)|~sQ63_spl|~sQ109_spl)),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f1324,f992])).
% 0.13/0.58  fof(f1654,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|~ssList(skaf46(sk2,sk1))|~ssList(sk1)|~ssList(app(sk2,X0))|segmentP(app(app(skaf46(sk2,sk1),sk1),X0),sk1)|~sQ109_spl)),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f1324,f501])).
% 0.13/0.58  fof(f1655,plain,(
% 0.13/0.58    ~ssList(skaf46(sk2,sk1))|~ssList(sk1)|rearsegP(sk2,sk1)|~sQ109_spl),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f1324,f776])).
% 0.13/0.58  fof(f1657,plain,(
% 0.13/0.58    ![X0]: (~rearsegP(sk1,X0)|~ssList(skaf46(sk2,sk1))|~ssList(X0)|~ssList(sk1)|rearsegP(sk2,X0)|~sQ109_spl)),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f1324,f350])).
% 0.13/0.58  fof(f1658,definition,(
% 0.13/0.58    ![X0]: (sQ133_spl <=> (~ssList(X0)|segmentP(app(sk2,X0),sk1)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1659,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|segmentP(app(sk2,X0),sk1)|~sQ133_spl)),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1658])).
% 0.13/0.58  fof(f1661,definition,(
% 0.13/0.58    sQ134_spl <=> (ssList(skaf46(sk2,sk1)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1663,plain,(
% 0.13/0.58    ~ssList(skaf46(sk2,sk1))|sQ134_spl),
% 0.13/0.58    inference(component_clause,[status(thm)],[f1661])).
% 0.13/0.58  fof(f1664,plain,(
% 0.13/0.58    sQ133_spl|~sQ134_spl|~sQ63_spl|~sQ109_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1651,f1658,f1661,f991,f1323])).
% 0.13/0.58  fof(f1670,definition,(
% 0.13/0.58    ![X0]: (sQ136_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(skaf46(sk2,sk1),sk1),X0),sk1)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1673,plain,(
% 0.13/0.58    sQ136_spl|~sQ134_spl|~sQ18_spl|~sQ109_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1654,f1670,f1661,f583,f1323])).
% 0.13/0.58  fof(f1674,definition,(
% 0.13/0.58    sQ137_spl <=> (rearsegP(sk2,sk1))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1677,plain,(
% 0.13/0.58    ~sQ134_spl|~sQ18_spl|sQ137_spl|~sQ109_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1655,f1661,f583,f1674,f1323])).
% 0.13/0.58  fof(f1679,definition,(
% 0.13/0.58    ![X0]: (sQ138_spl <=> (~rearsegP(sk1,X0)|~ssList(X0)|rearsegP(sk2,X0)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1682,plain,(
% 0.13/0.58    sQ138_spl|~sQ134_spl|~sQ18_spl|~sQ109_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1657,f1679,f1661,f583,f1323])).
% 0.13/0.58  fof(f1683,plain,(
% 0.13/0.58    $false|sQ134_spl),
% 0.13/0.58    inference(forward_subsumption_resolution,[status(thm)],[f1663,f249])).
% 0.13/0.58  fof(f1684,plain,(
% 0.13/0.58    sQ134_spl),
% 0.13/0.58    inference(contradiction_clause,[status(thm)],[f1683])).
% 0.13/0.58  fof(f1724,plain,(
% 0.13/0.58    ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk1)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),sk1)|~sQ133_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f1659,f404])).
% 0.13/0.58  fof(f1725,plain,(
% 0.13/0.58    ![X0]: (~ssList(X0)|~segmentP(sk1,app(sk2,X0))|~ssList(sk1)|~ssList(app(sk2,X0))|app(sk2,X0)=sk1|~sQ133_spl)),
% 0.13/0.58    inference(resolution,[status(thm)],[f1659,f339])).
% 0.13/0.58  fof(f1726,plain,(
% 0.13/0.58    ~ssList(nil)|segmentP(sk2,sk1)|~sQ133_spl),
% 0.13/0.58    inference(paramodulation,[status(thm)],[f557,f1659])).
% 0.13/0.58  fof(f1727,definition,(
% 0.13/0.58    ![X0,X1,X2]: (sQ139_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),sk1)))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1730,plain,(
% 0.13/0.58    sQ139_spl|~sQ18_spl|~sQ133_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1724,f1727,f583,f1658])).
% 0.13/0.58  fof(f1731,definition,(
% 0.13/0.58    ![X0]: (sQ140_spl <=> (~ssList(X0)|~segmentP(sk1,app(sk2,X0))|~ssList(app(sk2,X0))|app(sk2,X0)=sk1))),
% 0.13/0.58    introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 0.13/0.58  fof(f1734,plain,(
% 0.13/0.58    sQ140_spl|~sQ18_spl|~sQ133_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1725,f1731,f583,f1658])).
% 0.13/0.58  fof(f1735,plain,(
% 0.13/0.58    ~sQ10_spl|sQ59_spl|~sQ133_spl),
% 0.13/0.58    inference(split_clause,[status(thm)],[f1726,f518,f970,f1658])).
% 0.13/0.58  fof(f1736,plain,(
% 0.13/0.58    $false),
% 0.13/0.58    inference(sat_refutation,[status(thm)],[f461,f465,f466,f473,f477,f481,f482,f524,f528,f531,f545,f554,f573,f578,f586,f613,f615,f622,f629,f657,f662,f685,f704,f756,f766,f771,f787,f791,f798,f810,f835,f842,f850,f857,f876,f880,f884,f888,f892,f923,f976,f988,f994,f1045,f1049,f1053,f1060,f1064,f1068,f1075,f1079,f1087,f1091,f1095,f1103,f1107,f1135,f1142,f1146,f1151,f1166,f1170,f1174,f1178,f1184,f1191,f1195,f1199,f1205,f1221,f1225,f1236,f1240,f1249,f1253,f1257,f1263,f1278,f1282,f1288,f1298,f1314,f1318,f1322,f1326,f1330,f1334,f1342,f1375,f1380,f1397,f1401,f1408,f1413,f1596,f1601,f1620,f1625,f1644,f1649,f1664,f1673,f1677,f1682,f1684,f1730,f1734,f1735])).
% 0.13/0.58  % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.59  % Elapsed time: 0.215987 seconds
% 0.13/0.59  % CPU time: 1.451199 seconds
% 0.13/0.59  % Total memory used: 127.383 MB
% 0.13/0.59  % Net memory used: 126.056 MB
%------------------------------------------------------------------------------