%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC065-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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:41:29 PM UTC 2026
% Result : Unsatisfiable 11.88s 1.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC065-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.35 % Computer : n002.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 07:55:01 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 11.88/1.95 % Refutation found
% 11.88/1.95 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 11.88/1.95 % SZS output start CNFRefutation for theBenchmark
% 11.88/1.95 fof(f8,axiom,(
% 11.88/1.95 ssList(nil) ),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f44,axiom,(
% 11.88/1.95 (![U]: (ssList(skaf51(U)) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f48,axiom,(
% 11.88/1.95 (![U,V]: (ssList(skaf48(U,V)) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f49,axiom,(
% 11.88/1.95 (![U,V]: (ssList(skaf47(U,V)) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f50,axiom,(
% 11.88/1.95 (![U,V]: (ssList(skaf46(U,V)) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f51,axiom,(
% 11.88/1.95 (![U,V]: (ssList(skaf45(U,V)) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f52,axiom,(
% 11.88/1.95 (![U,V]: (ssList(skaf43(U,V)) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f53,axiom,(
% 11.88/1.95 (![U,V]: (ssList(skaf42(U,V)) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f56,axiom,(
% 11.88/1.95 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f57,axiom,(
% 11.88/1.95 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f73,axiom,(
% 11.88/1.95 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f74,axiom,(
% 11.88/1.95 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f80,axiom,(
% 11.88/1.95 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f85,axiom,(
% 11.88/1.95 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f100,axiom,(
% 11.88/1.95 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f127,axiom,(
% 11.88/1.95 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f152,axiom,(
% 11.88/1.95 (![U,V,W]: (( ~ segmentP(U,V)| ~ segmentP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| segmentP(U,W) ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f172,axiom,(
% 11.88/1.95 (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f173,axiom,(
% 11.88/1.95 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f186,negated_conjecture,(
% 11.88/1.95 ssList(sk1) ),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f187,negated_conjecture,(
% 11.88/1.95 ssList(sk2) ),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f190,negated_conjecture,(
% 11.88/1.95 sk2 = sk4 ),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f191,negated_conjecture,(
% 11.88/1.95 sk1 = sk3 ),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f192,negated_conjecture,(
% 11.88/1.95 ssList(sk5) ),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f193,negated_conjecture,(
% 11.88/1.95 app(sk3,sk5) = sk4 ),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f196,negated_conjecture,(
% 11.88/1.95 ( nil = sk4| nil != sk3 ) ),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f197,negated_conjecture,(
% 11.88/1.95 ( nil = sk2| neq(sk2,nil) ) ),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f198,negated_conjecture,(
% 11.88/1.95 (![A]: (( nil = sk2| ~ ssList(A)| ~ neq(A,nil)| ~ segmentP(sk2,A)| ~ segmentP(sk1,A) ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f199,negated_conjecture,(
% 11.88/1.95 ( nil != sk1| neq(sk2,nil) ) ),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f200,negated_conjecture,(
% 11.88/1.95 (![A]: (( nil != sk1| ~ ssList(A)| ~ neq(A,nil)| ~ segmentP(sk2,A)| ~ segmentP(sk1,A) ) ))),
% 11.88/1.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.88/1.95 fof(f208,plain,(
% 11.88/1.95 ssList(nil)),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f8])).
% 11.88/1.95 fof(f244,plain,(
% 11.88/1.95 ![X0]: (ssList(skaf51(X0)))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f44])).
% 11.88/1.95 fof(f248,plain,(
% 11.88/1.95 ![X0,X1]: (ssList(skaf48(X0,X1)))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f48])).
% 11.88/1.95 fof(f249,plain,(
% 11.88/1.95 ![X0,X1]: (ssList(skaf47(X0,X1)))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f49])).
% 11.88/1.95 fof(f250,plain,(
% 11.88/1.95 ![X0,X1]: (ssList(skaf46(X0,X1)))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f50])).
% 11.88/1.95 fof(f251,plain,(
% 11.88/1.95 ![X0,X1]: (ssList(skaf45(X0,X1)))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f51])).
% 11.88/1.95 fof(f252,plain,(
% 11.88/1.95 ![X0,X1]: (ssList(skaf43(X0,X1)))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f52])).
% 11.88/1.95 fof(f253,plain,(
% 11.88/1.95 ![X0,X1]: (ssList(skaf42(X0,X1)))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f53])).
% 11.88/1.95 fof(f256,plain,(
% 11.88/1.95 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f56])).
% 11.88/1.95 fof(f257,plain,(
% 11.88/1.95 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f57])).
% 11.88/1.95 fof(f274,plain,(
% 11.88/1.95 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f73])).
% 11.88/1.95 fof(f275,plain,(
% 11.88/1.95 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f74])).
% 11.88/1.95 fof(f281,plain,(
% 11.88/1.95 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f80])).
% 11.88/1.95 fof(f286,plain,(
% 11.88/1.95 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f85])).
% 11.88/1.95 fof(f303,plain,(
% 11.88/1.95 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f100])).
% 11.88/1.95 fof(f340,plain,(
% 11.88/1.95 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f127])).
% 11.88/1.95 fof(f374,plain,(
% 11.88/1.95 ![U,W]: (((![V]: (((~segmentP(U,V)|~segmentP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|segmentP(U,W))),
% 11.88/1.95 inference(miniscoping,[status(thm)],[f152])).
% 11.88/1.95 fof(f375,plain,(
% 11.88/1.95 ![X0,X1,X2]: (~segmentP(X0,X1)|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|segmentP(X0,X2))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f374])).
% 11.88/1.95 fof(f405,plain,(
% 11.88/1.95 ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f172])).
% 11.88/1.95 fof(f406,plain,(
% 11.88/1.95 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 11.88/1.95 inference(miniscoping,[status(thm)],[f173])).
% 11.88/1.95 fof(f407,plain,(
% 11.88/1.95 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f406])).
% 11.88/1.95 fof(f431,plain,(
% 11.88/1.95 ssList(sk1)),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f186])).
% 11.88/1.95 fof(f432,plain,(
% 11.88/1.95 ssList(sk2)),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f187])).
% 11.88/1.95 fof(f435,plain,(
% 11.88/1.95 sk2=sk4),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f190])).
% 11.88/1.95 fof(f436,plain,(
% 11.88/1.95 sk1=sk3),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f191])).
% 11.88/1.95 fof(f437,plain,(
% 11.88/1.95 ssList(sk5)),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f192])).
% 11.88/1.95 fof(f438,plain,(
% 11.88/1.95 app(sk3,sk5)=sk4),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f193])).
% 11.88/1.95 fof(f442,plain,(
% 11.88/1.95 nil=sk4|~nil=sk3),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f196])).
% 11.88/1.95 fof(f443,plain,(
% 11.88/1.95 nil=sk2|neq(sk2,nil)),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f197])).
% 11.88/1.95 fof(f444,plain,(
% 11.88/1.95 ![X0]: (nil=sk2|~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f198])).
% 11.88/1.95 fof(f445,plain,(
% 11.88/1.95 ~nil=sk1|neq(sk2,nil)),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f199])).
% 11.88/1.95 fof(f446,plain,(
% 11.88/1.95 ![X0]: (~nil=sk1|~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 11.88/1.95 inference(cnf_transformation,[status(thm)],[f200])).
% 11.88/1.95 fof(f454,definition,(
% 11.88/1.95 sQ2_spl <=> (nil=sk4)),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f455,plain,(
% 11.88/1.95 nil=sk4|~sQ2_spl),
% 11.88/1.95 inference(component_clause,[status(thm)],[f454])).
% 11.88/1.95 fof(f457,definition,(
% 11.88/1.95 sQ3_spl <=> (nil=sk3)),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f459,plain,(
% 11.88/1.95 ~nil=sk3|sQ3_spl),
% 11.88/1.95 inference(component_clause,[status(thm)],[f457])).
% 11.88/1.95 fof(f460,plain,(
% 11.88/1.95 sQ2_spl|~sQ3_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f442,f454,f457])).
% 11.88/1.95 fof(f461,definition,(
% 11.88/1.95 sQ4_spl <=> (nil=sk2)),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f462,plain,(
% 11.88/1.95 nil=sk2|~sQ4_spl),
% 11.88/1.95 inference(component_clause,[status(thm)],[f461])).
% 11.88/1.95 fof(f464,definition,(
% 11.88/1.95 sQ5_spl <=> (neq(sk2,nil))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f465,plain,(
% 11.88/1.95 neq(sk2,nil)|~sQ5_spl),
% 11.88/1.95 inference(component_clause,[status(thm)],[f464])).
% 11.88/1.95 fof(f467,plain,(
% 11.88/1.95 sQ4_spl|sQ5_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f443,f461,f464])).
% 11.88/1.95 fof(f468,definition,(
% 11.88/1.95 ![X0]: (sQ6_spl <=> (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0)))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f469,plain,(
% 11.88/1.95 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~sQ6_spl)),
% 11.88/1.95 inference(component_clause,[status(thm)],[f468])).
% 11.88/1.95 fof(f471,plain,(
% 11.88/1.95 sQ4_spl|sQ6_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f444,f461,f468])).
% 11.88/1.95 fof(f472,definition,(
% 11.88/1.95 sQ7_spl <=> (nil=sk1)),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f473,plain,(
% 11.88/1.95 nil=sk1|~sQ7_spl),
% 11.88/1.95 inference(component_clause,[status(thm)],[f472])).
% 11.88/1.95 fof(f475,plain,(
% 11.88/1.95 ~sQ7_spl|sQ5_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f445,f472,f464])).
% 11.88/1.95 fof(f476,plain,(
% 11.88/1.95 ~sQ7_spl|sQ6_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f446,f472,f468])).
% 11.88/1.95 fof(f495,plain,(
% 11.88/1.95 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 11.88/1.95 inference(destructive_equality_resolution,[status(thm)],[f407])).
% 11.88/1.95 fof(f506,plain,(
% 11.88/1.95 app(sk3,sk5)=sk2),
% 11.88/1.95 inference(backward_demodulation,[status(thm)],[f435,f438])).
% 11.88/1.95 fof(f510,plain,(
% 11.88/1.95 app(sk1,sk5)=sk2),
% 11.88/1.95 inference(forward_demodulation,[status(thm)],[f436,f506])).
% 11.88/1.95 fof(f511,plain,(
% 11.88/1.95 ![X0,X1]: (app(skaf43(X0,X1),nil)=skaf43(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f274,f252])).
% 11.88/1.95 fof(f512,plain,(
% 11.88/1.95 ![X0,X1]: (app(skaf45(X0,X1),nil)=skaf45(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f274,f251])).
% 11.88/1.95 fof(f513,plain,(
% 11.88/1.95 ![X0,X1]: (app(skaf46(X0,X1),nil)=skaf46(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f274,f250])).
% 11.88/1.95 fof(f514,plain,(
% 11.88/1.95 ![X0,X1]: (app(skaf47(X0,X1),nil)=skaf47(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f274,f249])).
% 11.88/1.95 fof(f515,plain,(
% 11.88/1.95 ![X0,X1]: (app(skaf48(X0,X1),nil)=skaf48(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f274,f248])).
% 11.88/1.95 fof(f516,plain,(
% 11.88/1.95 app(sk5,nil)=sk5),
% 11.88/1.95 inference(resolution,[status(thm)],[f274,f437])).
% 11.88/1.95 fof(f517,plain,(
% 11.88/1.95 app(nil,nil)=nil),
% 11.88/1.95 inference(resolution,[status(thm)],[f274,f208])).
% 11.88/1.95 fof(f518,plain,(
% 11.88/1.95 app(sk2,nil)=sk2),
% 11.88/1.95 inference(resolution,[status(thm)],[f274,f432])).
% 11.88/1.95 fof(f519,plain,(
% 11.88/1.95 app(sk1,nil)=sk1),
% 11.88/1.95 inference(resolution,[status(thm)],[f274,f431])).
% 11.88/1.95 fof(f520,plain,(
% 11.88/1.95 ![X0,X1]: (app(skaf42(X0,X1),nil)=skaf42(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f253,f274])).
% 11.88/1.95 fof(f532,plain,(
% 11.88/1.95 ![X0,X1]: (app(nil,skaf42(X0,X1))=skaf42(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f275,f253])).
% 11.88/1.95 fof(f533,plain,(
% 11.88/1.95 ![X0,X1]: (app(nil,skaf43(X0,X1))=skaf43(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f275,f252])).
% 11.88/1.95 fof(f534,plain,(
% 11.88/1.95 ![X0,X1]: (app(nil,skaf45(X0,X1))=skaf45(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f275,f251])).
% 11.88/1.95 fof(f535,plain,(
% 11.88/1.95 ![X0,X1]: (app(nil,skaf46(X0,X1))=skaf46(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f275,f250])).
% 11.88/1.95 fof(f536,plain,(
% 11.88/1.95 ![X0,X1]: (app(nil,skaf47(X0,X1))=skaf47(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f275,f249])).
% 11.88/1.95 fof(f537,plain,(
% 11.88/1.95 ![X0,X1]: (app(nil,skaf48(X0,X1))=skaf48(X0,X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f275,f248])).
% 11.88/1.95 fof(f538,plain,(
% 11.88/1.95 app(nil,sk5)=sk5),
% 11.88/1.95 inference(resolution,[status(thm)],[f275,f437])).
% 11.88/1.95 fof(f540,plain,(
% 11.88/1.95 app(nil,sk2)=sk2),
% 11.88/1.95 inference(resolution,[status(thm)],[f275,f432])).
% 11.88/1.95 fof(f541,plain,(
% 11.88/1.95 app(nil,sk1)=sk1),
% 11.88/1.95 inference(resolution,[status(thm)],[f275,f431])).
% 11.88/1.95 fof(f542,plain,(
% 11.88/1.95 ~ssList(nil)|nil=nil|~ssList(nil)),
% 11.88/1.95 inference(resolution,[status(thm)],[f281,f256])).
% 11.88/1.95 fof(f544,definition,(
% 11.88/1.95 sQ8_spl <=> (ssList(nil))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f546,plain,(
% 11.88/1.95 ~ssList(nil)|sQ8_spl),
% 11.88/1.95 inference(component_clause,[status(thm)],[f544])).
% 11.88/1.95 fof(f547,definition,(
% 11.88/1.95 sQ9_spl <=> (nil=nil)),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f550,plain,(
% 11.88/1.95 ~sQ8_spl|sQ9_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f542,f544,f547])).
% 11.88/1.95 fof(f552,plain,(
% 11.88/1.95 $false|sQ8_spl),
% 11.88/1.95 inference(forward_subsumption_resolution,[status(thm)],[f546,f208])).
% 11.88/1.95 fof(f553,plain,(
% 11.88/1.95 sQ8_spl),
% 11.88/1.95 inference(contradiction_clause,[status(thm)],[f552])).
% 11.88/1.95 fof(f580,plain,(
% 11.88/1.95 app(sk1,sk5)=nil|~sQ4_spl),
% 11.88/1.95 inference(backward_demodulation,[status(thm)],[f462,f510])).
% 11.88/1.95 fof(f581,plain,(
% 11.88/1.95 nil=sk4|~sQ4_spl),
% 11.88/1.95 inference(backward_demodulation,[status(thm)],[f462,f435])).
% 11.88/1.95 fof(f605,plain,(
% 11.88/1.95 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf42(X1,X2),X0)))),
% 11.88/1.95 inference(resolution,[status(thm)],[f286,f253])).
% 11.88/1.95 fof(f606,plain,(
% 11.88/1.95 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf43(X1,X2),X0)))),
% 11.88/1.95 inference(resolution,[status(thm)],[f286,f252])).
% 11.88/1.95 fof(f607,plain,(
% 11.88/1.95 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf45(X1,X2),X0)))),
% 11.88/1.95 inference(resolution,[status(thm)],[f286,f251])).
% 11.88/1.95 fof(f608,plain,(
% 11.88/1.95 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf46(X1,X2),X0)))),
% 11.88/1.95 inference(resolution,[status(thm)],[f286,f250])).
% 11.88/1.95 fof(f609,plain,(
% 11.88/1.95 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf47(X1,X2),X0)))),
% 11.88/1.95 inference(resolution,[status(thm)],[f286,f249])).
% 11.88/1.95 fof(f610,plain,(
% 11.88/1.95 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf48(X1,X2),X0)))),
% 11.88/1.95 inference(resolution,[status(thm)],[f286,f248])).
% 11.88/1.95 fof(f611,plain,(
% 11.88/1.95 ![X0]: (~ssList(X0)|ssList(app(sk5,X0)))),
% 11.88/1.95 inference(resolution,[status(thm)],[f286,f437])).
% 11.88/1.95 fof(f613,plain,(
% 11.88/1.95 ![X0]: (~ssList(X0)|ssList(app(sk1,X0)))),
% 11.88/1.95 inference(resolution,[status(thm)],[f286,f431])).
% 11.88/1.95 fof(f616,plain,(
% 11.88/1.95 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(app(sk5,X0),X1)))),
% 11.88/1.95 inference(resolution,[status(thm)],[f611,f286])).
% 11.88/1.95 fof(f622,plain,(
% 11.88/1.95 ~ssList(nil)|ssList(sk5)),
% 11.88/1.95 inference(paramodulation,[status(thm)],[f516,f611])).
% 11.88/1.95 fof(f623,definition,(
% 11.88/1.95 sQ14_spl <=> (ssList(sk5))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f626,plain,(
% 11.88/1.95 ~sQ8_spl|sQ14_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f622,f544,f623])).
% 11.88/1.95 fof(f636,definition,(
% 11.88/1.95 sQ15_spl <=> (ssList(sk1))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f668,plain,(
% 11.88/1.95 ~ssList(nil)|ssList(sk1)),
% 11.88/1.95 inference(paramodulation,[status(thm)],[f519,f613])).
% 11.88/1.95 fof(f670,plain,(
% 11.88/1.95 ~sQ8_spl|sQ15_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f668,f544,f636])).
% 11.88/1.95 fof(f671,plain,(
% 11.88/1.95 sk2=nil|~sQ2_spl),
% 11.88/1.95 inference(forward_demodulation,[status(thm)],[f455,f435])).
% 11.88/1.95 fof(f672,plain,(
% 11.88/1.95 ![X0]: (~ssList(X0)|ssList(app(sk2,X0)))),
% 11.88/1.95 inference(resolution,[status(thm)],[f432,f286])).
% 11.88/1.95 fof(f679,definition,(
% 11.88/1.95 sQ16_spl <=> (ssList(sk2))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f683,plain,(
% 11.88/1.95 ~ssList(sk5)|ssList(sk2)),
% 11.88/1.95 inference(paramodulation,[status(thm)],[f510,f613])).
% 11.88/1.95 fof(f684,plain,(
% 11.88/1.95 ~sQ14_spl|sQ16_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f683,f623,f679])).
% 11.88/1.95 fof(f726,plain,(
% 11.88/1.95 ![X0]: (~ssList(nil)|~ssList(X0)|ssList(app(sk5,X0)))),
% 11.88/1.95 inference(paramodulation,[status(thm)],[f516,f616])).
% 11.88/1.95 fof(f727,definition,(
% 11.88/1.95 ![X0]: (sQ18_spl <=> (~ssList(X0)|ssList(app(sk5,X0))))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f730,plain,(
% 11.88/1.95 ~sQ8_spl|sQ18_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f726,f544,f727])).
% 11.88/1.95 fof(f731,plain,(
% 11.88/1.95 ~ssList(sk2)|~segmentP(sk2,sk2)|~segmentP(sk1,sk2)|~sQ6_spl|~sQ5_spl),
% 11.88/1.95 inference(resolution,[status(thm)],[f469,f465])).
% 11.88/1.95 fof(f732,plain,(
% 11.88/1.95 ![X0]: (~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~sQ6_spl)),
% 11.88/1.95 inference(resolution,[status(thm)],[f469,f303])).
% 11.88/1.95 fof(f733,definition,(
% 11.88/1.95 sQ19_spl <=> (segmentP(sk2,sk2))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f734,plain,(
% 11.88/1.95 segmentP(sk2,sk2)|~sQ19_spl),
% 11.88/1.95 inference(component_clause,[status(thm)],[f733])).
% 11.88/1.95 fof(f735,plain,(
% 11.88/1.95 ~segmentP(sk2,sk2)|sQ19_spl),
% 11.88/1.95 inference(component_clause,[status(thm)],[f733])).
% 11.88/1.95 fof(f736,definition,(
% 11.88/1.95 sQ20_spl <=> (segmentP(sk1,sk2))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f737,plain,(
% 11.88/1.95 segmentP(sk1,sk2)|~sQ20_spl),
% 11.88/1.95 inference(component_clause,[status(thm)],[f736])).
% 11.88/1.95 fof(f738,plain,(
% 11.88/1.95 ~segmentP(sk1,sk2)|sQ20_spl),
% 11.88/1.95 inference(component_clause,[status(thm)],[f736])).
% 11.88/1.95 fof(f739,plain,(
% 11.88/1.95 ~sQ16_spl|~sQ19_spl|~sQ20_spl|~sQ6_spl|~sQ5_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f731,f679,f733,f736,f468,f464])).
% 11.88/1.95 fof(f740,definition,(
% 11.88/1.95 ![X0]: (sQ21_spl <=> (~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~ssList(X0)|X0=nil))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f741,plain,(
% 11.88/1.95 ![X0]: (~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~ssList(X0)|X0=nil|~sQ21_spl)),
% 11.88/1.95 inference(component_clause,[status(thm)],[f740])).
% 11.88/1.95 fof(f743,plain,(
% 11.88/1.95 sQ21_spl|~sQ8_spl|~sQ6_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f732,f740,f544,f468])).
% 11.88/1.95 fof(f744,plain,(
% 11.88/1.95 ![X0]: (~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|X0=nil|~sQ21_spl)),
% 11.88/1.95 inference(duplicate_literals_removal,[status(thm)],[f741])).
% 11.88/1.95 fof(f854,plain,(
% 11.88/1.95 ~segmentP(sk1,nil)|~sQ2_spl|sQ20_spl),
% 11.88/1.95 inference(backward_demodulation,[status(thm)],[f671,f738])).
% 11.88/1.95 fof(f863,plain,(
% 11.88/1.95 ~ssList(sk1)|~sQ2_spl|sQ20_spl),
% 11.88/1.95 inference(resolution,[status(thm)],[f854,f256])).
% 11.88/1.95 fof(f864,plain,(
% 11.88/1.95 $false|~sQ2_spl|sQ20_spl),
% 11.88/1.95 inference(forward_subsumption_resolution,[status(thm)],[f863,f431])).
% 11.88/1.95 fof(f865,plain,(
% 11.88/1.95 ~sQ2_spl|sQ20_spl),
% 11.88/1.95 inference(contradiction_clause,[status(thm)],[f864])).
% 11.88/1.95 fof(f866,plain,(
% 11.88/1.95 ~nil=sk1|sQ3_spl),
% 11.88/1.95 inference(forward_demodulation,[status(thm)],[f436,f459])).
% 11.88/1.95 fof(f867,plain,(
% 11.88/1.95 sQ2_spl|~sQ4_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f581,f454,f461])).
% 11.88/1.95 fof(f874,plain,(
% 11.88/1.95 ~ssList(sk2)|sQ19_spl),
% 11.88/1.95 inference(resolution,[status(thm)],[f735,f257])).
% 11.88/1.95 fof(f875,plain,(
% 11.88/1.95 $false|sQ19_spl),
% 11.88/1.95 inference(forward_subsumption_resolution,[status(thm)],[f874,f432])).
% 11.88/1.95 fof(f876,plain,(
% 11.88/1.95 sQ19_spl),
% 11.88/1.95 inference(contradiction_clause,[status(thm)],[f875])).
% 11.88/1.95 fof(f970,plain,(
% 11.88/1.95 ~segmentP(sk2,sk2)|~ssList(sk2)|~ssList(sk2)|sk2=sk2|~sQ19_spl),
% 11.88/1.95 inference(resolution,[status(thm)],[f340,f734])).
% 11.88/1.95 fof(f972,plain,(
% 11.88/1.95 ![X0]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~ssList(X0))),
% 11.88/1.95 inference(resolution,[status(thm)],[f340,f256])).
% 11.88/1.95 fof(f974,definition,(
% 11.88/1.95 sQ27_spl <=> (sk2=sk2)),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f977,plain,(
% 11.88/1.95 ~sQ19_spl|~sQ16_spl|sQ27_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f970,f733,f679,f974])).
% 11.88/1.95 fof(f978,definition,(
% 11.88/1.95 sQ28_spl <=> (segmentP(sk2,sk1))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f979,plain,(
% 11.88/1.95 segmentP(sk2,sk1)|~sQ28_spl),
% 11.88/1.95 inference(component_clause,[status(thm)],[f978])).
% 11.88/1.95 fof(f985,definition,(
% 11.88/1.95 ![X0]: (sQ30_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~ssList(X0)))),
% 11.88/1.95 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 11.88/1.95 fof(f988,plain,(
% 11.88/1.95 sQ30_spl|~sQ8_spl),
% 11.88/1.95 inference(split_clause,[status(thm)],[f972,f985,f544])).
% 11.88/1.95 fof(f1114,plain,(
% 11.88/1.95 segmentP(sk1,nil)|~sQ4_spl|~sQ20_spl),
% 11.88/1.95 inference(backward_demodulation,[status(thm)],[f462,f737])).
% 11.88/1.95 fof(f1323,plain,(
% 11.88/1.95 ![X0]: (~segmentP(X0,sk2)|~ssList(sk2)|~ssList(sk2)|~ssList(X0)|segmentP(X0,sk2)|~sQ19_spl)),
% 11.88/1.95 inference(resolution,[status(thm)],[f375,f734])).
% 11.88/1.95 fof(f1324,plain,(
% 11.88/1.95 ![X0,X1]: (~segmentP(X0,X1)|~ssList(nil)|~ssList(X1)|~ssList(X0)|segmentP(X0,nil)|~ssList(X1))),
% 11.88/1.95 inference(resolution,[status(thm)],[f375,f256])).
% 11.88/1.95 fof(f1328,plain,(
% 11.88/1.95 ![X0,X1]: (~segmentP(nil,X0)|~segmentP(X0,X1)|~ssList(X1)|~ssList(X0)|~ssList(nil)|~ssList(X1)|nil=X1)),
% 11.88/1.96 inference(resolution,[status(thm)],[f375,f281])).
% 11.88/1.96 fof(f1331,definition,(
% 11.88/1.96 ![X0]: (sQ32_spl <=> (~segmentP(X0,sk2)|~ssList(X0)|segmentP(X0,sk2)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1334,plain,(
% 11.88/1.96 sQ32_spl|~sQ16_spl|~sQ19_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1323,f1331,f679,f733])).
% 11.88/1.96 fof(f1335,definition,(
% 11.88/1.96 ![X0,X1]: (sQ33_spl <=> (~segmentP(X0,X1)|~ssList(X1)|~ssList(X0)|segmentP(X0,nil)|~ssList(X1)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1338,plain,(
% 11.88/1.96 sQ33_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1324,f1335,f544])).
% 11.88/1.96 fof(f1344,definition,(
% 11.88/1.96 ![X0,X1]: (sQ35_spl <=> (~segmentP(nil,X0)|~segmentP(X0,X1)|~ssList(X1)|~ssList(X0)|~ssList(X1)|nil=X1))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1347,plain,(
% 11.88/1.96 sQ35_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1328,f1344,f544])).
% 11.88/1.96 fof(f1461,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(nil)|ssList(skaf42(X0,X1)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f520,f605])).
% 11.88/1.96 fof(f1462,definition,(
% 11.88/1.96 ![X0,X1]: (sQ36_spl <=> (ssList(skaf42(X0,X1))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1465,plain,(
% 11.88/1.96 ~sQ8_spl|sQ36_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1461,f544,f1462])).
% 11.88/1.96 fof(f1486,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(nil)|ssList(skaf43(X0,X1)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f511,f606])).
% 11.88/1.96 fof(f1487,definition,(
% 11.88/1.96 ![X0,X1]: (sQ37_spl <=> (ssList(skaf43(X0,X1))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1490,plain,(
% 11.88/1.96 ~sQ8_spl|sQ37_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1486,f544,f1487])).
% 11.88/1.96 fof(f1511,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(nil)|ssList(skaf45(X0,X1)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f512,f607])).
% 11.88/1.96 fof(f1512,definition,(
% 11.88/1.96 ![X0,X1]: (sQ38_spl <=> (ssList(skaf45(X0,X1))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1515,plain,(
% 11.88/1.96 ~sQ8_spl|sQ38_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1511,f544,f1512])).
% 11.88/1.96 fof(f1536,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(nil)|ssList(skaf46(X0,X1)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f513,f608])).
% 11.88/1.96 fof(f1537,definition,(
% 11.88/1.96 ![X0,X1]: (sQ39_spl <=> (ssList(skaf46(X0,X1))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1540,plain,(
% 11.88/1.96 ~sQ8_spl|sQ39_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1536,f544,f1537])).
% 11.88/1.96 fof(f1561,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(nil)|ssList(skaf47(X0,X1)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f514,f609])).
% 11.88/1.96 fof(f1562,definition,(
% 11.88/1.96 ![X0,X1]: (sQ40_spl <=> (ssList(skaf47(X0,X1))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1565,plain,(
% 11.88/1.96 ~sQ8_spl|sQ40_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1561,f544,f1562])).
% 11.88/1.96 fof(f1664,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(nil)|ssList(skaf48(X0,X1)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f515,f610])).
% 11.88/1.96 fof(f1665,definition,(
% 11.88/1.96 ![X0,X1]: (sQ41_spl <=> (ssList(skaf48(X0,X1))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1668,plain,(
% 11.88/1.96 ~sQ8_spl|sQ41_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1664,f544,f1665])).
% 11.88/1.96 fof(f1716,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk2)|~ssList(sk2)|segmentP(app(app(X1,sk2),X0),sk2)|~sQ19_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f405,f734])).
% 11.88/1.96 fof(f1717,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2))),
% 11.88/1.96 inference(resolution,[status(thm)],[f405,f256])).
% 11.88/1.96 fof(f1720,definition,(
% 11.88/1.96 ![X0,X1]: (sQ42_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk2),X0),sk2)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1723,plain,(
% 11.88/1.96 sQ42_spl|~sQ16_spl|~sQ19_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1716,f1720,f679,f733])).
% 11.88/1.96 fof(f1724,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ43_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1727,plain,(
% 11.88/1.96 sQ43_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1717,f1724,f544])).
% 11.88/1.96 fof(f1731,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(X0)|~ssList(sk5)|~ssList(X1)|segmentP(app(app(sk5,X1),X0),X1)|~ssList(X1)|~ssList(X0))),
% 11.88/1.96 inference(resolution,[status(thm)],[f495,f616])).
% 11.88/1.96 fof(f1732,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(sk2)|~ssList(nil)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,nil),X0),nil))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f518,f495])).
% 11.88/1.96 fof(f1733,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(skaf42(X1,X2))|~ssList(nil)|~ssList(app(skaf42(X1,X2),X0))|segmentP(app(app(skaf42(X1,X2),nil),X0),nil))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f520,f495])).
% 11.88/1.96 fof(f1734,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(skaf48(X1,X2))|~ssList(nil)|~ssList(app(skaf48(X1,X2),X0))|segmentP(app(app(skaf48(X1,X2),nil),X0),nil))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f515,f495])).
% 11.88/1.96 fof(f1735,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(skaf47(X1,X2))|~ssList(nil)|~ssList(app(skaf47(X1,X2),X0))|segmentP(app(app(skaf47(X1,X2),nil),X0),nil))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f514,f495])).
% 11.88/1.96 fof(f1736,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(skaf46(X1,X2))|~ssList(nil)|~ssList(app(skaf46(X1,X2),X0))|segmentP(app(app(skaf46(X1,X2),nil),X0),nil))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f513,f495])).
% 11.88/1.96 fof(f1737,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(skaf45(X1,X2))|~ssList(nil)|~ssList(app(skaf45(X1,X2),X0))|segmentP(app(app(skaf45(X1,X2),nil),X0),nil))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f512,f495])).
% 11.88/1.96 fof(f1738,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(skaf43(X1,X2))|~ssList(nil)|~ssList(app(skaf43(X1,X2),X0))|segmentP(app(app(skaf43(X1,X2),nil),X0),nil))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f511,f495])).
% 11.88/1.96 fof(f1739,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(nil)|~ssList(skaf48(X1,X2))|~ssList(app(skaf48(X1,X2),X0))|segmentP(app(app(nil,skaf48(X1,X2)),X0),skaf48(X1,X2)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f537,f495])).
% 11.88/1.96 fof(f1740,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(nil)|~ssList(skaf47(X1,X2))|~ssList(app(skaf47(X1,X2),X0))|segmentP(app(app(nil,skaf47(X1,X2)),X0),skaf47(X1,X2)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f536,f495])).
% 11.88/1.96 fof(f1741,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(nil)|~ssList(skaf46(X1,X2))|~ssList(app(skaf46(X1,X2),X0))|segmentP(app(app(nil,skaf46(X1,X2)),X0),skaf46(X1,X2)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f535,f495])).
% 11.88/1.96 fof(f1742,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(nil)|~ssList(skaf45(X1,X2))|~ssList(app(skaf45(X1,X2),X0))|segmentP(app(app(nil,skaf45(X1,X2)),X0),skaf45(X1,X2)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f534,f495])).
% 11.88/1.96 fof(f1743,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(nil)|~ssList(skaf43(X1,X2))|~ssList(app(skaf43(X1,X2),X0))|segmentP(app(app(nil,skaf43(X1,X2)),X0),skaf43(X1,X2)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f533,f495])).
% 11.88/1.96 fof(f1744,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f540,f495])).
% 11.88/1.96 fof(f1745,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(nil)|~ssList(skaf42(X1,X2))|~ssList(app(skaf42(X1,X2),X0))|segmentP(app(app(nil,skaf42(X1,X2)),X0),skaf42(X1,X2)))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f532,f495])).
% 11.88/1.96 fof(f1746,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f541,f495])).
% 11.88/1.96 fof(f1747,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk5)|~ssList(app(sk5,X0))|segmentP(app(app(nil,sk5),X0),sk5))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f538,f495])).
% 11.88/1.96 fof(f1748,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f517,f495])).
% 11.88/1.96 fof(f1749,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(sk5)|~ssList(nil)|~ssList(app(sk5,X0))|segmentP(app(app(sk5,nil),X0),nil))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f516,f495])).
% 11.88/1.96 fof(f1750,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(sk5)|~ssList(app(sk2,X0))|segmentP(app(app(sk1,sk5),X0),sk5))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f510,f495])).
% 11.88/1.96 fof(f1751,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(nil)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil))),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f519,f495])).
% 11.88/1.96 fof(f1752,definition,(
% 11.88/1.96 ![X0,X1]: (sQ44_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(sk5,X1),X0),X1)|~ssList(X1)|~ssList(X0)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1755,plain,(
% 11.88/1.96 sQ44_spl|~sQ14_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1731,f1752,f623])).
% 11.88/1.96 fof(f1756,definition,(
% 11.88/1.96 ![X0]: (sQ45_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,nil),X0),nil)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1759,plain,(
% 11.88/1.96 sQ45_spl|~sQ16_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1732,f1756,f679,f544])).
% 11.88/1.96 fof(f1760,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ46_spl <=> (~ssList(X0)|~ssList(skaf42(X1,X2))|~ssList(app(skaf42(X1,X2),X0))|segmentP(app(app(skaf42(X1,X2),nil),X0),nil)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1763,plain,(
% 11.88/1.96 sQ46_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1733,f1760,f544])).
% 11.88/1.96 fof(f1764,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ47_spl <=> (~ssList(X0)|~ssList(skaf48(X1,X2))|~ssList(app(skaf48(X1,X2),X0))|segmentP(app(app(skaf48(X1,X2),nil),X0),nil)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1767,plain,(
% 11.88/1.96 sQ47_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1734,f1764,f544])).
% 11.88/1.96 fof(f1768,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ48_spl <=> (~ssList(X0)|~ssList(skaf47(X1,X2))|~ssList(app(skaf47(X1,X2),X0))|segmentP(app(app(skaf47(X1,X2),nil),X0),nil)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1771,plain,(
% 11.88/1.96 sQ48_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1735,f1768,f544])).
% 11.88/1.96 fof(f1772,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ49_spl <=> (~ssList(X0)|~ssList(skaf46(X1,X2))|~ssList(app(skaf46(X1,X2),X0))|segmentP(app(app(skaf46(X1,X2),nil),X0),nil)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1775,plain,(
% 11.88/1.96 sQ49_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1736,f1772,f544])).
% 11.88/1.96 fof(f1776,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ50_spl <=> (~ssList(X0)|~ssList(skaf45(X1,X2))|~ssList(app(skaf45(X1,X2),X0))|segmentP(app(app(skaf45(X1,X2),nil),X0),nil)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1779,plain,(
% 11.88/1.96 sQ50_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1737,f1776,f544])).
% 11.88/1.96 fof(f1780,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ51_spl <=> (~ssList(X0)|~ssList(skaf43(X1,X2))|~ssList(app(skaf43(X1,X2),X0))|segmentP(app(app(skaf43(X1,X2),nil),X0),nil)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1783,plain,(
% 11.88/1.96 sQ51_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1738,f1780,f544])).
% 11.88/1.96 fof(f1784,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ52_spl <=> (~ssList(X0)|~ssList(skaf48(X1,X2))|~ssList(app(skaf48(X1,X2),X0))|segmentP(app(app(nil,skaf48(X1,X2)),X0),skaf48(X1,X2))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1787,plain,(
% 11.88/1.96 sQ52_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1739,f1784,f544])).
% 11.88/1.96 fof(f1788,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ53_spl <=> (~ssList(X0)|~ssList(skaf47(X1,X2))|~ssList(app(skaf47(X1,X2),X0))|segmentP(app(app(nil,skaf47(X1,X2)),X0),skaf47(X1,X2))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1791,plain,(
% 11.88/1.96 sQ53_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1740,f1788,f544])).
% 11.88/1.96 fof(f1792,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ54_spl <=> (~ssList(X0)|~ssList(skaf46(X1,X2))|~ssList(app(skaf46(X1,X2),X0))|segmentP(app(app(nil,skaf46(X1,X2)),X0),skaf46(X1,X2))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1795,plain,(
% 11.88/1.96 sQ54_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1741,f1792,f544])).
% 11.88/1.96 fof(f1796,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ55_spl <=> (~ssList(X0)|~ssList(skaf45(X1,X2))|~ssList(app(skaf45(X1,X2),X0))|segmentP(app(app(nil,skaf45(X1,X2)),X0),skaf45(X1,X2))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1799,plain,(
% 11.88/1.96 sQ55_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1742,f1796,f544])).
% 11.88/1.96 fof(f1800,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ56_spl <=> (~ssList(X0)|~ssList(skaf43(X1,X2))|~ssList(app(skaf43(X1,X2),X0))|segmentP(app(app(nil,skaf43(X1,X2)),X0),skaf43(X1,X2))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1803,plain,(
% 11.88/1.96 sQ56_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1743,f1800,f544])).
% 11.88/1.96 fof(f1804,definition,(
% 11.88/1.96 ![X0]: (sQ57_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1805,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2)|~sQ57_spl)),
% 11.88/1.96 inference(component_clause,[status(thm)],[f1804])).
% 11.88/1.96 fof(f1807,plain,(
% 11.88/1.96 sQ57_spl|~sQ8_spl|~sQ16_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1744,f1804,f544,f679])).
% 11.88/1.96 fof(f1808,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ58_spl <=> (~ssList(X0)|~ssList(skaf42(X1,X2))|~ssList(app(skaf42(X1,X2),X0))|segmentP(app(app(nil,skaf42(X1,X2)),X0),skaf42(X1,X2))))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1811,plain,(
% 11.88/1.96 sQ58_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1745,f1808,f544])).
% 11.88/1.96 fof(f1812,definition,(
% 11.88/1.96 ![X0]: (sQ59_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1813,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)|~sQ59_spl)),
% 11.88/1.96 inference(component_clause,[status(thm)],[f1812])).
% 11.88/1.96 fof(f1815,plain,(
% 11.88/1.96 sQ59_spl|~sQ8_spl|~sQ15_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1746,f1812,f544,f636])).
% 11.88/1.96 fof(f1816,definition,(
% 11.88/1.96 ![X0]: (sQ60_spl <=> (~ssList(X0)|~ssList(app(sk5,X0))|segmentP(app(app(nil,sk5),X0),sk5)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1817,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(app(sk5,X0))|segmentP(app(app(nil,sk5),X0),sk5)|~sQ60_spl)),
% 11.88/1.96 inference(component_clause,[status(thm)],[f1816])).
% 11.88/1.96 fof(f1819,plain,(
% 11.88/1.96 sQ60_spl|~sQ8_spl|~sQ14_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1747,f1816,f544,f623])).
% 11.88/1.96 fof(f1820,definition,(
% 11.88/1.96 ![X0]: (sQ61_spl <=> (~ssList(X0)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1823,plain,(
% 11.88/1.96 sQ61_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1748,f1820,f544])).
% 11.88/1.96 fof(f1824,definition,(
% 11.88/1.96 ![X0]: (sQ62_spl <=> (~ssList(X0)|~ssList(app(sk5,X0))|segmentP(app(app(sk5,nil),X0),nil)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1827,plain,(
% 11.88/1.96 sQ62_spl|~sQ14_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1749,f1824,f623,f544])).
% 11.88/1.96 fof(f1828,definition,(
% 11.88/1.96 ![X0]: (sQ63_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(sk1,sk5),X0),sk5)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1829,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(sk1,sk5),X0),sk5)|~sQ63_spl)),
% 11.88/1.96 inference(component_clause,[status(thm)],[f1828])).
% 11.88/1.96 fof(f1831,plain,(
% 11.88/1.96 sQ63_spl|~sQ15_spl|~sQ14_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1750,f1828,f636,f623])).
% 11.88/1.96 fof(f1832,definition,(
% 11.88/1.96 ![X0]: (sQ64_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1835,plain,(
% 11.88/1.96 sQ64_spl|~sQ15_spl|~sQ8_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1751,f1832,f636,f544])).
% 11.88/1.96 fof(f1837,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(sk2,X0),sk2)|~sQ57_spl)),
% 11.88/1.96 inference(forward_demodulation,[status(thm)],[f540,f1805])).
% 11.88/1.96 fof(f1838,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|segmentP(app(sk2,X0),sk2)|~sQ57_spl)),
% 11.88/1.96 inference(forward_subsumption_resolution,[status(thm)],[f1837,f672])).
% 11.88/1.96 fof(f1840,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(app(sk5,X0))|segmentP(app(sk5,X0),sk5)|~sQ60_spl)),
% 11.88/1.96 inference(forward_demodulation,[status(thm)],[f538,f1817])).
% 11.88/1.96 fof(f1841,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|segmentP(app(sk5,X0),sk5)|~sQ60_spl)),
% 11.88/1.96 inference(forward_subsumption_resolution,[status(thm)],[f1840,f611])).
% 11.88/1.96 fof(f1843,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(sk1,X0),sk1)|~sQ59_spl)),
% 11.88/1.96 inference(forward_demodulation,[status(thm)],[f541,f1813])).
% 11.88/1.96 fof(f1844,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~sQ59_spl)),
% 11.88/1.96 inference(forward_subsumption_resolution,[status(thm)],[f1843,f613])).
% 11.88/1.96 fof(f1845,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(sk2,X0),sk5)|~sQ63_spl)),
% 11.88/1.96 inference(forward_demodulation,[status(thm)],[f510,f1829])).
% 11.88/1.96 fof(f1846,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|segmentP(app(sk2,X0),sk5)|~sQ63_spl)),
% 11.88/1.96 inference(forward_subsumption_resolution,[status(thm)],[f1845,f672])).
% 11.88/1.96 fof(f1867,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),sk2)|~sQ57_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1838,f405])).
% 11.88/1.96 fof(f1868,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(X0)|~segmentP(X1,app(sk2,X0))|~ssList(sk2)|~ssList(app(sk2,X0))|~ssList(X1)|segmentP(X1,sk2)|~sQ57_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1838,f375])).
% 11.88/1.96 fof(f1869,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~segmentP(sk2,app(sk2,X0))|~ssList(sk2)|~ssList(app(sk2,X0))|app(sk2,X0)=sk2|~sQ57_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1838,f340])).
% 11.88/1.96 fof(f1871,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ65_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),sk2)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1874,plain,(
% 11.88/1.96 sQ65_spl|~sQ16_spl|~sQ57_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1867,f1871,f679,f1804])).
% 11.88/1.96 fof(f1875,definition,(
% 11.88/1.96 ![X0,X1]: (sQ66_spl <=> (~ssList(X0)|~segmentP(X1,app(sk2,X0))|~ssList(app(sk2,X0))|~ssList(X1)|segmentP(X1,sk2)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1878,plain,(
% 11.88/1.96 sQ66_spl|~sQ16_spl|~sQ57_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1868,f1875,f679,f1804])).
% 11.88/1.96 fof(f1879,definition,(
% 11.88/1.96 ![X0]: (sQ67_spl <=> (~ssList(X0)|~segmentP(sk2,app(sk2,X0))|~ssList(app(sk2,X0))|app(sk2,X0)=sk2))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1882,plain,(
% 11.88/1.96 sQ67_spl|~sQ16_spl|~sQ57_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1869,f1879,f679,f1804])).
% 11.88/1.96 fof(f1887,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk5)|~ssList(app(sk5,X0))|segmentP(app(app(X2,app(sk5,X0)),X1),sk5)|~sQ60_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1841,f405])).
% 11.88/1.96 fof(f1888,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(X0)|~segmentP(X1,app(sk5,X0))|~ssList(sk5)|~ssList(app(sk5,X0))|~ssList(X1)|segmentP(X1,sk5)|~sQ60_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1841,f375])).
% 11.88/1.96 fof(f1889,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~segmentP(sk5,app(sk5,X0))|~ssList(sk5)|~ssList(app(sk5,X0))|app(sk5,X0)=sk5|~sQ60_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1841,f340])).
% 11.88/1.96 fof(f1890,plain,(
% 11.88/1.96 ~ssList(nil)|segmentP(sk5,sk5)|~sQ60_spl),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f516,f1841])).
% 11.88/1.96 fof(f1891,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ68_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk5,X0))|segmentP(app(app(X2,app(sk5,X0)),X1),sk5)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1894,plain,(
% 11.88/1.96 sQ68_spl|~sQ14_spl|~sQ60_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1887,f1891,f623,f1816])).
% 11.88/1.96 fof(f1895,definition,(
% 11.88/1.96 ![X0,X1]: (sQ69_spl <=> (~ssList(X0)|~segmentP(X1,app(sk5,X0))|~ssList(app(sk5,X0))|~ssList(X1)|segmentP(X1,sk5)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1898,plain,(
% 11.88/1.96 sQ69_spl|~sQ14_spl|~sQ60_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1888,f1895,f623,f1816])).
% 11.88/1.96 fof(f1899,definition,(
% 11.88/1.96 ![X0]: (sQ70_spl <=> (~ssList(X0)|~segmentP(sk5,app(sk5,X0))|~ssList(app(sk5,X0))|app(sk5,X0)=sk5))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1902,plain,(
% 11.88/1.96 sQ70_spl|~sQ14_spl|~sQ60_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1889,f1899,f623,f1816])).
% 11.88/1.96 fof(f1903,definition,(
% 11.88/1.96 sQ71_spl <=> (segmentP(sk5,sk5))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1904,plain,(
% 11.88/1.96 segmentP(sk5,sk5)|~sQ71_spl),
% 11.88/1.96 inference(component_clause,[status(thm)],[f1903])).
% 11.88/1.96 fof(f1906,plain,(
% 11.88/1.96 ~sQ8_spl|sQ71_spl|~sQ60_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1890,f544,f1903,f1816])).
% 11.88/1.96 fof(f1910,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk5)|~ssList(sk5)|segmentP(app(app(X1,sk5),X0),sk5)|~sQ71_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1904,f405])).
% 11.88/1.96 fof(f1911,plain,(
% 11.88/1.96 ![X0]: (~segmentP(X0,sk5)|~ssList(sk5)|~ssList(sk5)|~ssList(X0)|segmentP(X0,sk5)|~sQ71_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1904,f375])).
% 11.88/1.96 fof(f1912,plain,(
% 11.88/1.96 ~segmentP(sk5,sk5)|~ssList(sk5)|~ssList(sk5)|sk5=sk5|~sQ71_spl),
% 11.88/1.96 inference(resolution,[status(thm)],[f1904,f340])).
% 11.88/1.96 fof(f1913,definition,(
% 11.88/1.96 ![X0,X1]: (sQ72_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk5),X0),sk5)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1916,plain,(
% 11.88/1.96 sQ72_spl|~sQ14_spl|~sQ71_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1910,f1913,f623,f1903])).
% 11.88/1.96 fof(f1917,definition,(
% 11.88/1.96 ![X0]: (sQ73_spl <=> (~segmentP(X0,sk5)|~ssList(X0)|segmentP(X0,sk5)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1920,plain,(
% 11.88/1.96 sQ73_spl|~sQ14_spl|~sQ71_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1911,f1917,f623,f1903])).
% 11.88/1.96 fof(f1921,definition,(
% 11.88/1.96 sQ74_spl <=> (sk5=sk5)),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1924,plain,(
% 11.88/1.96 ~sQ71_spl|~sQ14_spl|sQ74_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1912,f1903,f623,f1921])).
% 11.88/1.96 fof(f1925,plain,(
% 11.88/1.96 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),sk1)|~sQ59_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1844,f405])).
% 11.88/1.96 fof(f1926,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(X0)|~segmentP(X1,app(sk1,X0))|~ssList(sk1)|~ssList(app(sk1,X0))|~ssList(X1)|segmentP(X1,sk1)|~sQ59_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1844,f375])).
% 11.88/1.96 fof(f1927,plain,(
% 11.88/1.96 ![X0]: (~ssList(X0)|~segmentP(sk1,app(sk1,X0))|~ssList(sk1)|~ssList(app(sk1,X0))|app(sk1,X0)=sk1|~sQ59_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1844,f340])).
% 11.88/1.96 fof(f1928,plain,(
% 11.88/1.96 ~ssList(sk5)|segmentP(sk2,sk1)|~sQ59_spl),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f510,f1844])).
% 11.88/1.96 fof(f1929,plain,(
% 11.88/1.96 ~ssList(nil)|segmentP(sk1,sk1)|~sQ59_spl),
% 11.88/1.96 inference(paramodulation,[status(thm)],[f519,f1844])).
% 11.88/1.96 fof(f1930,definition,(
% 11.88/1.96 ![X0,X1,X2]: (sQ75_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),sk1)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1933,plain,(
% 11.88/1.96 sQ75_spl|~sQ15_spl|~sQ59_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1925,f1930,f636,f1812])).
% 11.88/1.96 fof(f1934,definition,(
% 11.88/1.96 ![X0,X1]: (sQ76_spl <=> (~ssList(X0)|~segmentP(X1,app(sk1,X0))|~ssList(app(sk1,X0))|~ssList(X1)|segmentP(X1,sk1)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1937,plain,(
% 11.88/1.96 sQ76_spl|~sQ15_spl|~sQ59_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1926,f1934,f636,f1812])).
% 11.88/1.96 fof(f1938,definition,(
% 11.88/1.96 ![X0]: (sQ77_spl <=> (~ssList(X0)|~segmentP(sk1,app(sk1,X0))|~ssList(app(sk1,X0))|app(sk1,X0)=sk1))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1941,plain,(
% 11.88/1.96 sQ77_spl|~sQ15_spl|~sQ59_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1927,f1938,f636,f1812])).
% 11.88/1.96 fof(f1942,plain,(
% 11.88/1.96 ~sQ14_spl|sQ28_spl|~sQ59_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1928,f623,f978,f1812])).
% 11.88/1.96 fof(f1943,definition,(
% 11.88/1.96 sQ78_spl <=> (segmentP(sk1,sk1))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1944,plain,(
% 11.88/1.96 segmentP(sk1,sk1)|~sQ78_spl),
% 11.88/1.96 inference(component_clause,[status(thm)],[f1943])).
% 11.88/1.96 fof(f1946,plain,(
% 11.88/1.96 ~sQ8_spl|sQ78_spl|~sQ59_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1929,f544,f1943,f1812])).
% 11.88/1.96 fof(f1950,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk1)|~ssList(sk1)|segmentP(app(app(X1,sk1),X0),sk1)|~sQ78_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1944,f405])).
% 11.88/1.96 fof(f1951,plain,(
% 11.88/1.96 ![X0]: (~segmentP(X0,sk1)|~ssList(sk1)|~ssList(sk1)|~ssList(X0)|segmentP(X0,sk1)|~sQ78_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f1944,f375])).
% 11.88/1.96 fof(f1952,plain,(
% 11.88/1.96 ~segmentP(sk1,sk1)|~ssList(sk1)|~ssList(sk1)|sk1=sk1|~sQ78_spl),
% 11.88/1.96 inference(resolution,[status(thm)],[f1944,f340])).
% 11.88/1.96 fof(f1953,definition,(
% 11.88/1.96 ![X0,X1]: (sQ79_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),sk1)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1956,plain,(
% 11.88/1.96 sQ79_spl|~sQ15_spl|~sQ78_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1950,f1953,f636,f1943])).
% 11.88/1.96 fof(f1957,definition,(
% 11.88/1.96 ![X0]: (sQ80_spl <=> (~segmentP(X0,sk1)|~ssList(X0)|segmentP(X0,sk1)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1960,plain,(
% 11.88/1.96 sQ80_spl|~sQ15_spl|~sQ78_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1951,f1957,f636,f1943])).
% 11.88/1.96 fof(f1961,definition,(
% 11.88/1.96 sQ81_spl <=> (sk1=sk1)),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1964,plain,(
% 11.88/1.96 ~sQ78_spl|~sQ15_spl|sQ81_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1952,f1943,f636,f1961])).
% 11.88/1.96 fof(f1965,plain,(
% 11.88/1.96 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk1)|~ssList(sk2)|segmentP(app(app(X1,sk2),X0),sk1)|~sQ28_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f979,f405])).
% 11.88/1.96 fof(f1966,plain,(
% 11.88/1.96 ![X0]: (~segmentP(X0,sk2)|~ssList(sk1)|~ssList(sk2)|~ssList(X0)|segmentP(X0,sk1)|~sQ28_spl)),
% 11.88/1.96 inference(resolution,[status(thm)],[f979,f375])).
% 11.88/1.96 fof(f1968,definition,(
% 11.88/1.96 ![X0,X1]: (sQ82_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk2),X0),sk1)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 11.88/1.96 fof(f1971,plain,(
% 11.88/1.96 sQ82_spl|~sQ15_spl|~sQ16_spl|~sQ28_spl),
% 11.88/1.96 inference(split_clause,[status(thm)],[f1965,f1968,f636,f679,f978])).
% 11.88/1.96 fof(f1972,definition,(
% 11.88/1.96 ![X0]: (sQ83_spl <=> (~segmentP(X0,sk2)|~ssList(X0)|segmentP(X0,sk1)))),
% 11.88/1.96 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f1975,plain,(
% 11.88/1.97 sQ83_spl|~sQ15_spl|~sQ16_spl|~sQ28_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f1966,f1972,f636,f679,f978])).
% 11.88/1.97 fof(f2021,plain,(
% 11.88/1.97 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk5)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),sk5)|~sQ63_spl)),
% 11.88/1.97 inference(resolution,[status(thm)],[f1846,f405])).
% 11.88/1.97 fof(f2022,plain,(
% 11.88/1.97 ![X0,X1]: (~ssList(X0)|~segmentP(X1,app(sk2,X0))|~ssList(sk5)|~ssList(app(sk2,X0))|~ssList(X1)|segmentP(X1,sk5)|~sQ63_spl)),
% 11.88/1.97 inference(resolution,[status(thm)],[f1846,f375])).
% 11.88/1.97 fof(f2023,plain,(
% 11.88/1.97 ![X0]: (~ssList(X0)|~segmentP(sk5,app(sk2,X0))|~ssList(sk5)|~ssList(app(sk2,X0))|app(sk2,X0)=sk5|~sQ63_spl)),
% 11.88/1.97 inference(resolution,[status(thm)],[f1846,f340])).
% 11.88/1.97 fof(f2024,plain,(
% 11.88/1.97 ~ssList(nil)|segmentP(sk2,sk5)|~sQ63_spl),
% 11.88/1.97 inference(paramodulation,[status(thm)],[f518,f1846])).
% 11.88/1.97 fof(f2025,definition,(
% 11.88/1.97 ![X0,X1,X2]: (sQ84_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk2,X0))|segmentP(app(app(X2,app(sk2,X0)),X1),sk5)))),
% 11.88/1.97 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f2028,plain,(
% 11.88/1.97 sQ84_spl|~sQ14_spl|~sQ63_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f2021,f2025,f623,f1828])).
% 11.88/1.97 fof(f2029,definition,(
% 11.88/1.97 ![X0,X1]: (sQ85_spl <=> (~ssList(X0)|~segmentP(X1,app(sk2,X0))|~ssList(app(sk2,X0))|~ssList(X1)|segmentP(X1,sk5)))),
% 11.88/1.97 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f2032,plain,(
% 11.88/1.97 sQ85_spl|~sQ14_spl|~sQ63_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f2022,f2029,f623,f1828])).
% 11.88/1.97 fof(f2033,definition,(
% 11.88/1.97 ![X0]: (sQ86_spl <=> (~ssList(X0)|~segmentP(sk5,app(sk2,X0))|~ssList(app(sk2,X0))|app(sk2,X0)=sk5))),
% 11.88/1.97 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f2036,plain,(
% 11.88/1.97 sQ86_spl|~sQ14_spl|~sQ63_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f2023,f2033,f623,f1828])).
% 11.88/1.97 fof(f2037,definition,(
% 11.88/1.97 sQ87_spl <=> (segmentP(sk2,sk5))),
% 11.88/1.97 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f2038,plain,(
% 11.88/1.97 segmentP(sk2,sk5)|~sQ87_spl),
% 11.88/1.97 inference(component_clause,[status(thm)],[f2037])).
% 11.88/1.97 fof(f2040,plain,(
% 11.88/1.97 ~sQ8_spl|sQ87_spl|~sQ63_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f2024,f544,f2037,f1828])).
% 11.88/1.97 fof(f2044,plain,(
% 11.88/1.97 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk5)|~ssList(sk2)|segmentP(app(app(X1,sk2),X0),sk5)|~sQ87_spl)),
% 11.88/1.97 inference(resolution,[status(thm)],[f2038,f405])).
% 11.88/1.97 fof(f2045,plain,(
% 11.88/1.97 ![X0]: (~segmentP(X0,sk2)|~ssList(sk5)|~ssList(sk2)|~ssList(X0)|segmentP(X0,sk5)|~sQ87_spl)),
% 11.88/1.97 inference(resolution,[status(thm)],[f2038,f375])).
% 11.88/1.97 fof(f2046,plain,(
% 11.88/1.97 ~segmentP(sk5,sk2)|~ssList(sk5)|~ssList(sk2)|sk2=sk5|~sQ87_spl),
% 11.88/1.97 inference(resolution,[status(thm)],[f2038,f340])).
% 11.88/1.97 fof(f2047,definition,(
% 11.88/1.97 ![X0,X1]: (sQ88_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk2),X0),sk5)))),
% 11.88/1.97 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f2050,plain,(
% 11.88/1.97 sQ88_spl|~sQ14_spl|~sQ16_spl|~sQ87_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f2044,f2047,f623,f679,f2037])).
% 11.88/1.97 fof(f2051,definition,(
% 11.88/1.97 ![X0]: (sQ89_spl <=> (~segmentP(X0,sk2)|~ssList(X0)|segmentP(X0,sk5)))),
% 11.88/1.97 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f2054,plain,(
% 11.88/1.97 sQ89_spl|~sQ14_spl|~sQ16_spl|~sQ87_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f2045,f2051,f623,f679,f2037])).
% 11.88/1.97 fof(f2055,definition,(
% 11.88/1.97 sQ90_spl <=> (segmentP(sk5,sk2))),
% 11.88/1.97 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f2057,plain,(
% 11.88/1.97 ~segmentP(sk5,sk2)|sQ90_spl),
% 11.88/1.97 inference(component_clause,[status(thm)],[f2055])).
% 11.88/1.97 fof(f2058,definition,(
% 11.88/1.97 sQ91_spl <=> (sk2=sk5)),
% 11.88/1.97 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f2061,plain,(
% 11.88/1.97 ~sQ90_spl|~sQ14_spl|~sQ16_spl|sQ91_spl|~sQ87_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f2046,f2055,f623,f679,f2058,f2037])).
% 11.88/1.97 fof(f2062,plain,(
% 11.88/1.97 ![X0]: (~segmentP(sk5,X0)|~segmentP(X0,sk2)|~ssList(sk2)|~ssList(X0)|~ssList(sk5)|sQ90_spl)),
% 11.88/1.97 inference(resolution,[status(thm)],[f2057,f375])).
% 11.88/1.97 fof(f2063,definition,(
% 11.88/1.97 ![X0]: (sQ92_spl <=> (~segmentP(sk5,X0)|~segmentP(X0,sk2)|~ssList(X0)))),
% 11.88/1.97 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f2066,plain,(
% 11.88/1.97 sQ92_spl|~sQ16_spl|~sQ14_spl|sQ90_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f2062,f2063,f679,f623,f2055])).
% 11.88/1.97 fof(f2796,definition,(
% 11.88/1.97 ![X0]: (sQ108_spl <=> (~ssList(X0)|~ssList(X0)))),
% 11.88/1.97 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f2797,plain,(
% 11.88/1.97 ![X0]: (~ssList(X0)|~ssList(X0)|~sQ108_spl)),
% 11.88/1.97 inference(component_clause,[status(thm)],[f2796])).
% 11.88/1.97 fof(f2803,plain,(
% 11.88/1.97 ![X0]: (~ssList(X0)|~sQ108_spl)),
% 11.88/1.97 inference(duplicate_literals_removal,[status(thm)],[f2797])).
% 11.88/1.97 fof(f2804,plain,(
% 11.88/1.97 $false|~sQ108_spl),
% 11.88/1.97 inference(backward_subsumption_resolution,[status(thm)],[f244,f2803])).
% 11.88/1.97 fof(f2835,plain,(
% 11.88/1.97 ~sQ108_spl),
% 11.88/1.97 inference(contradiction_clause,[status(thm)],[f2804])).
% 11.88/1.97 fof(f3217,plain,(
% 11.88/1.97 ~ssList(sk1)|~segmentP(sk2,sk1)|sk1=nil|~ssList(sk1)|~sQ21_spl),
% 11.88/1.97 inference(resolution,[status(thm)],[f744,f257])).
% 11.88/1.97 fof(f3223,plain,(
% 11.88/1.97 ~sQ15_spl|~sQ28_spl|sQ7_spl|~sQ21_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f3217,f636,f978,f472,f740])).
% 11.88/1.97 fof(f3224,plain,(
% 11.88/1.97 $false|sQ3_spl|~sQ7_spl),
% 11.88/1.97 inference(forward_subsumption_resolution,[status(thm)],[f473,f866])).
% 11.88/1.97 fof(f3225,plain,(
% 11.88/1.97 sQ3_spl|~sQ7_spl),
% 11.88/1.97 inference(contradiction_clause,[status(thm)],[f3224])).
% 11.88/1.97 fof(f3227,plain,(
% 11.88/1.97 ~ssList(sk5)|segmentP(nil,sk1)|~sQ59_spl|~sQ4_spl),
% 11.88/1.97 inference(paramodulation,[status(thm)],[f580,f1844])).
% 11.88/1.97 fof(f3229,definition,(
% 11.88/1.97 sQ111_spl <=> (segmentP(nil,sk1))),
% 11.88/1.97 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 11.88/1.97 fof(f3232,plain,(
% 11.88/1.97 ~sQ14_spl|sQ111_spl|~sQ59_spl|~sQ4_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f3227,f623,f3229,f1812,f461])).
% 11.88/1.97 fof(f4301,plain,(
% 11.88/1.97 ~segmentP(nil,sk1)|~ssList(nil)|~ssList(sk1)|sk1=nil|~sQ4_spl|~sQ20_spl),
% 11.88/1.97 inference(resolution,[status(thm)],[f340,f1114])).
% 11.88/1.97 fof(f4328,plain,(
% 11.88/1.97 ~sQ111_spl|~sQ8_spl|~sQ15_spl|sQ7_spl|~sQ4_spl|~sQ20_spl),
% 11.88/1.97 inference(split_clause,[status(thm)],[f4301,f3229,f544,f636,f472,f461,f736])).
% 11.88/1.97 fof(f4334,plain,(
% 11.88/1.97 $false),
% 11.88/1.97 inference(sat_refutation,[status(thm)],[f460,f467,f471,f475,f476,f550,f553,f626,f670,f684,f730,f739,f743,f865,f867,f876,f977,f988,f1334,f1338,f1347,f1465,f1490,f1515,f1540,f1565,f1668,f1723,f1727,f1755,f1759,f1763,f1767,f1771,f1775,f1779,f1783,f1787,f1791,f1795,f1799,f1803,f1807,f1811,f1815,f1819,f1823,f1827,f1831,f1835,f1874,f1878,f1882,f1894,f1898,f1902,f1906,f1916,f1920,f1924,f1933,f1937,f1941,f1942,f1946,f1956,f1960,f1964,f1971,f1975,f2028,f2032,f2036,f2040,f2050,f2054,f2061,f2066,f2835,f3223,f3225,f3232,f4328])).
% 11.88/1.97 % SZS output end CNFRefutation for theBenchmark.p
% 11.88/1.99 % Elapsed time: 1.615249 seconds
% 11.88/1.99 % CPU time: 12.367071 seconds
% 11.88/1.99 % Total memory used: 248.352 MB
% 11.88/1.99 % Net memory used: 239.900 MB
%------------------------------------------------------------------------------