%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC110-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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:41:37 PM UTC 2026
% Result : Unsatisfiable 0.15s 11.13s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC110-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/10.39 % Computer : n018.cluster.edu
% 0.12/10.39 % Model : x86_64 x86_64
% 0.12/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.39 % Memory : 8046.5625MB
% 0.12/10.39 % OS : Linux 6.8.0-71-generic
% 0.12/10.39 % CPULimit : 300
% 0.12/10.39 % WCLimit : 300
% 0.12/10.39 % DateTime : Mon Sep 21 07:58:39 UTC 2026
% 0.12/10.40 % CPUTime :
% 0.15/10.41 % Drodi V4.1.1
% 0.15/11.13 % Refutation found
% 0.15/11.13 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/11.13 % SZS output start CNFRefutation for theBenchmark
% 0.15/11.13 fof(f8,axiom,(
% 0.15/11.13 ssList(nil) ),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f36,axiom,(
% 0.15/11.13 (![U]: (ssItem(skaf59(U)) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f48,axiom,(
% 0.15/11.13 (![U,V]: (ssList(skaf48(U,V)) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f49,axiom,(
% 0.15/11.13 (![U,V]: (ssList(skaf47(U,V)) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f50,axiom,(
% 0.15/11.13 (![U,V]: (ssList(skaf46(U,V)) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f51,axiom,(
% 0.15/11.13 (![U,V]: (ssList(skaf45(U,V)) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f52,axiom,(
% 0.15/11.13 (![U,V]: (ssList(skaf43(U,V)) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f53,axiom,(
% 0.15/11.13 (![U,V]: (ssList(skaf42(U,V)) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f56,axiom,(
% 0.15/11.13 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f73,axiom,(
% 0.15/11.13 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f74,axiom,(
% 0.15/11.13 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f80,axiom,(
% 0.15/11.13 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f85,axiom,(
% 0.15/11.13 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f100,axiom,(
% 0.15/11.13 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f115,axiom,(
% 0.15/11.13 (![U,V]: (( U != V| ~ neq(U,V)| ~ ssList(V)| ~ ssList(U) ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f127,axiom,(
% 0.15/11.13 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f152,axiom,(
% 0.15/11.13 (![U,V,W]: (( ~ segmentP(U,V)| ~ segmentP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| segmentP(U,W) ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f171,axiom,(
% 0.15/11.13 (![U,V,W,X]: (( cons(U,V) != cons(W,X)| ~ ssItem(W)| ~ ssItem(U)| ~ ssList(X)| ~ ssList(V)| X = V ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f172,axiom,(
% 0.15/11.13 (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f173,axiom,(
% 0.15/11.13 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f186,negated_conjecture,(
% 0.15/11.13 ssList(sk1) ),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f187,negated_conjecture,(
% 0.15/11.13 ssList(sk2) ),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f190,negated_conjecture,(
% 0.15/11.13 sk2 = sk4 ),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f191,negated_conjecture,(
% 0.15/11.13 sk1 = sk3 ),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f192,negated_conjecture,(
% 0.15/11.13 ssList(sk5) ),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f193,negated_conjecture,(
% 0.15/11.13 app(sk3,sk5) = sk4 ),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f196,negated_conjecture,(
% 0.15/11.13 ( nil = sk4| nil != sk3 ) ),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f197,negated_conjecture,(
% 0.15/11.13 ( nil = sk2| neq(sk2,nil) ) ),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f198,negated_conjecture,(
% 0.15/11.13 ( nil = sk2| ~ neq(sk1,nil)| ~ segmentP(sk2,sk1) ) ),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f199,negated_conjecture,(
% 0.15/11.13 ( nil != sk1| neq(sk2,nil) ) ),
% 0.15/11.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/11.13 fof(f208,plain,(
% 0.15/11.13 ssList(nil)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f8])).
% 0.15/11.13 fof(f236,plain,(
% 0.15/11.13 ![X0]: (ssItem(skaf59(X0)))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/11.13 fof(f248,plain,(
% 0.15/11.13 ![X0,X1]: (ssList(skaf48(X0,X1)))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f48])).
% 0.15/11.13 fof(f249,plain,(
% 0.15/11.13 ![X0,X1]: (ssList(skaf47(X0,X1)))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f49])).
% 0.15/11.13 fof(f250,plain,(
% 0.15/11.13 ![X0,X1]: (ssList(skaf46(X0,X1)))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f50])).
% 0.15/11.13 fof(f251,plain,(
% 0.15/11.13 ![X0,X1]: (ssList(skaf45(X0,X1)))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f51])).
% 0.15/11.13 fof(f252,plain,(
% 0.15/11.13 ![X0,X1]: (ssList(skaf43(X0,X1)))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f52])).
% 0.15/11.13 fof(f253,plain,(
% 0.15/11.13 ![X0,X1]: (ssList(skaf42(X0,X1)))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f53])).
% 0.15/11.13 fof(f256,plain,(
% 0.15/11.13 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f56])).
% 0.15/11.13 fof(f274,plain,(
% 0.15/11.13 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f73])).
% 0.15/11.13 fof(f275,plain,(
% 0.15/11.13 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f74])).
% 0.15/11.13 fof(f281,plain,(
% 0.15/11.13 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/11.13 fof(f286,plain,(
% 0.15/11.13 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f85])).
% 0.15/11.13 fof(f303,plain,(
% 0.15/11.13 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f100])).
% 0.15/11.13 fof(f321,plain,(
% 0.15/11.13 ![U]: ((![V]: ((~U=V|~neq(U,V))|~ssList(V)))|~ssList(U))),
% 0.15/11.13 inference(miniscoping,[status(thm)],[f115])).
% 0.15/11.13 fof(f322,plain,(
% 0.15/11.13 ![X0,X1]: (~X0=X1|~neq(X0,X1)|~ssList(X1)|~ssList(X0))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f321])).
% 0.15/11.13 fof(f340,plain,(
% 0.15/11.13 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f127])).
% 0.15/11.13 fof(f374,plain,(
% 0.15/11.13 ![U,W]: (((![V]: (((~segmentP(U,V)|~segmentP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|segmentP(U,W))),
% 0.15/11.13 inference(miniscoping,[status(thm)],[f152])).
% 0.15/11.13 fof(f375,plain,(
% 0.15/11.13 ![X0,X1,X2]: (~segmentP(X0,X1)|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|segmentP(X0,X2))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f374])).
% 0.15/11.13 fof(f403,plain,(
% 0.15/11.13 ![V,X]: ((((![U]: ((![W]: (~cons(U,V)=cons(W,X)|~ssItem(W)))|~ssItem(U)))|~ssList(X))|~ssList(V))|X=V)),
% 0.15/11.13 inference(miniscoping,[status(thm)],[f171])).
% 0.15/11.13 fof(f404,plain,(
% 0.15/11.13 ![X0,X1,X2,X3]: (~cons(X0,X1)=cons(X2,X3)|~ssItem(X2)|~ssItem(X0)|~ssList(X3)|~ssList(X1)|X3=X1)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f403])).
% 0.15/11.13 fof(f405,plain,(
% 0.15/11.13 ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f172])).
% 0.15/11.13 fof(f406,plain,(
% 0.15/11.13 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 0.15/11.13 inference(miniscoping,[status(thm)],[f173])).
% 0.15/11.13 fof(f407,plain,(
% 0.15/11.13 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f406])).
% 0.15/11.13 fof(f431,plain,(
% 0.15/11.13 ssList(sk1)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f186])).
% 0.15/11.13 fof(f432,plain,(
% 0.15/11.13 ssList(sk2)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f187])).
% 0.15/11.13 fof(f435,plain,(
% 0.15/11.13 sk2=sk4),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f190])).
% 0.15/11.13 fof(f436,plain,(
% 0.15/11.13 sk1=sk3),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f191])).
% 0.15/11.13 fof(f437,plain,(
% 0.15/11.13 ssList(sk5)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f192])).
% 0.15/11.13 fof(f438,plain,(
% 0.15/11.13 app(sk3,sk5)=sk4),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f193])).
% 0.15/11.13 fof(f442,plain,(
% 0.15/11.13 nil=sk4|~nil=sk3),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f196])).
% 0.15/11.13 fof(f443,plain,(
% 0.15/11.13 nil=sk2|neq(sk2,nil)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f197])).
% 0.15/11.13 fof(f444,plain,(
% 0.15/11.13 nil=sk2|~neq(sk1,nil)|~segmentP(sk2,sk1)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f198])).
% 0.15/11.13 fof(f445,plain,(
% 0.15/11.13 ~nil=sk1|neq(sk2,nil)),
% 0.15/11.13 inference(cnf_transformation,[status(thm)],[f199])).
% 0.15/11.14 fof(f454,definition,(
% 0.15/11.14 sQ2_spl <=> (nil=sk4)),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f455,plain,(
% 0.15/11.14 nil=sk4|~sQ2_spl),
% 0.15/11.14 inference(component_clause,[status(thm)],[f454])).
% 0.15/11.14 fof(f457,definition,(
% 0.15/11.14 sQ3_spl <=> (nil=sk3)),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f459,plain,(
% 0.15/11.14 ~nil=sk3|sQ3_spl),
% 0.15/11.14 inference(component_clause,[status(thm)],[f457])).
% 0.15/11.14 fof(f460,plain,(
% 0.15/11.14 sQ2_spl|~sQ3_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f442,f454,f457])).
% 0.15/11.14 fof(f461,definition,(
% 0.15/11.14 sQ4_spl <=> (nil=sk2)),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f462,plain,(
% 0.15/11.14 nil=sk2|~sQ4_spl),
% 0.15/11.14 inference(component_clause,[status(thm)],[f461])).
% 0.15/11.14 fof(f464,definition,(
% 0.15/11.14 sQ5_spl <=> (neq(sk2,nil))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f465,plain,(
% 0.15/11.14 neq(sk2,nil)|~sQ5_spl),
% 0.15/11.14 inference(component_clause,[status(thm)],[f464])).
% 0.15/11.14 fof(f467,plain,(
% 0.15/11.14 sQ4_spl|sQ5_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f443,f461,f464])).
% 0.15/11.14 fof(f468,definition,(
% 0.15/11.14 sQ6_spl <=> (neq(sk1,nil))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f470,plain,(
% 0.15/11.14 ~neq(sk1,nil)|sQ6_spl),
% 0.15/11.14 inference(component_clause,[status(thm)],[f468])).
% 0.15/11.14 fof(f471,definition,(
% 0.15/11.14 sQ7_spl <=> (segmentP(sk2,sk1))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f474,plain,(
% 0.15/11.14 sQ4_spl|~sQ6_spl|~sQ7_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f444,f461,f468,f471])).
% 0.15/11.14 fof(f475,definition,(
% 0.15/11.14 sQ8_spl <=> (nil=sk1)),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f478,plain,(
% 0.15/11.14 ~sQ8_spl|sQ5_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f445,f475,f464])).
% 0.15/11.14 fof(f487,plain,(
% 0.15/11.14 ![X1]: (~neq(X1,X1)|~ssList(X1)|~ssList(X1))),
% 0.15/11.14 inference(destructive_equality_resolution,[status(thm)],[f322])).
% 0.15/11.14 fof(f488,plain,(
% 0.15/11.14 ![X0]: (~neq(X0,X0)|~ssList(X0))),
% 0.15/11.14 inference(duplicate_literals_removal,[status(thm)],[f487])).
% 0.15/11.14 fof(f498,plain,(
% 0.15/11.14 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 0.15/11.14 inference(destructive_equality_resolution,[status(thm)],[f407])).
% 0.15/11.14 fof(f509,plain,(
% 0.15/11.14 app(sk3,sk5)=sk2),
% 0.15/11.14 inference(backward_demodulation,[status(thm)],[f435,f438])).
% 0.15/11.14 fof(f513,plain,(
% 0.15/11.14 app(sk1,sk5)=sk2),
% 0.15/11.14 inference(forward_demodulation,[status(thm)],[f436,f509])).
% 0.15/11.14 fof(f514,plain,(
% 0.15/11.14 ![X0,X1]: (app(skaf43(X0,X1),nil)=skaf43(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f274,f252])).
% 0.15/11.14 fof(f515,plain,(
% 0.15/11.14 ![X0,X1]: (app(skaf45(X0,X1),nil)=skaf45(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f274,f251])).
% 0.15/11.14 fof(f516,plain,(
% 0.15/11.14 ![X0,X1]: (app(skaf46(X0,X1),nil)=skaf46(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f274,f250])).
% 0.15/11.14 fof(f517,plain,(
% 0.15/11.14 ![X0,X1]: (app(skaf47(X0,X1),nil)=skaf47(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f274,f249])).
% 0.15/11.14 fof(f518,plain,(
% 0.15/11.14 ![X0,X1]: (app(skaf48(X0,X1),nil)=skaf48(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f274,f248])).
% 0.15/11.14 fof(f519,plain,(
% 0.15/11.14 app(sk5,nil)=sk5),
% 0.15/11.14 inference(resolution,[status(thm)],[f274,f437])).
% 0.15/11.14 fof(f520,plain,(
% 0.15/11.14 app(nil,nil)=nil),
% 0.15/11.14 inference(resolution,[status(thm)],[f274,f208])).
% 0.15/11.14 fof(f521,plain,(
% 0.15/11.14 app(sk2,nil)=sk2),
% 0.15/11.14 inference(resolution,[status(thm)],[f274,f432])).
% 0.15/11.14 fof(f522,plain,(
% 0.15/11.14 app(sk1,nil)=sk1),
% 0.15/11.14 inference(resolution,[status(thm)],[f274,f431])).
% 0.15/11.14 fof(f523,plain,(
% 0.15/11.14 ![X0,X1]: (app(skaf42(X0,X1),nil)=skaf42(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f253,f274])).
% 0.15/11.14 fof(f535,plain,(
% 0.15/11.14 ![X0,X1]: (app(nil,skaf42(X0,X1))=skaf42(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f275,f253])).
% 0.15/11.14 fof(f536,plain,(
% 0.15/11.14 ![X0,X1]: (app(nil,skaf43(X0,X1))=skaf43(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f275,f252])).
% 0.15/11.14 fof(f537,plain,(
% 0.15/11.14 ![X0,X1]: (app(nil,skaf45(X0,X1))=skaf45(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f275,f251])).
% 0.15/11.14 fof(f538,plain,(
% 0.15/11.14 ![X0,X1]: (app(nil,skaf46(X0,X1))=skaf46(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f275,f250])).
% 0.15/11.14 fof(f539,plain,(
% 0.15/11.14 ![X0,X1]: (app(nil,skaf47(X0,X1))=skaf47(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f275,f249])).
% 0.15/11.14 fof(f540,plain,(
% 0.15/11.14 ![X0,X1]: (app(nil,skaf48(X0,X1))=skaf48(X0,X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f275,f248])).
% 0.15/11.14 fof(f541,plain,(
% 0.15/11.14 app(nil,sk5)=sk5),
% 0.15/11.14 inference(resolution,[status(thm)],[f275,f437])).
% 0.15/11.14 fof(f543,plain,(
% 0.15/11.14 app(nil,sk2)=sk2),
% 0.15/11.14 inference(resolution,[status(thm)],[f275,f432])).
% 0.15/11.14 fof(f544,plain,(
% 0.15/11.14 app(nil,sk1)=sk1),
% 0.15/11.14 inference(resolution,[status(thm)],[f275,f431])).
% 0.15/11.14 fof(f545,plain,(
% 0.15/11.14 ~ssList(nil)|nil=nil|~ssList(nil)),
% 0.15/11.14 inference(resolution,[status(thm)],[f281,f256])).
% 0.15/11.14 fof(f547,definition,(
% 0.15/11.14 sQ9_spl <=> (ssList(nil))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f549,plain,(
% 0.15/11.14 ~ssList(nil)|sQ9_spl),
% 0.15/11.14 inference(component_clause,[status(thm)],[f547])).
% 0.15/11.14 fof(f550,definition,(
% 0.15/11.14 sQ10_spl <=> (nil=nil)),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f553,plain,(
% 0.15/11.14 ~sQ9_spl|sQ10_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f545,f547,f550])).
% 0.15/11.14 fof(f555,plain,(
% 0.15/11.14 $false|sQ9_spl),
% 0.15/11.14 inference(forward_subsumption_resolution,[status(thm)],[f549,f208])).
% 0.15/11.14 fof(f556,plain,(
% 0.15/11.14 sQ9_spl),
% 0.15/11.14 inference(contradiction_clause,[status(thm)],[f555])).
% 0.15/11.14 fof(f583,plain,(
% 0.15/11.14 app(sk1,sk5)=nil|~sQ4_spl),
% 0.15/11.14 inference(backward_demodulation,[status(thm)],[f462,f513])).
% 0.15/11.14 fof(f584,plain,(
% 0.15/11.14 nil=sk4|~sQ4_spl),
% 0.15/11.14 inference(backward_demodulation,[status(thm)],[f462,f435])).
% 0.15/11.14 fof(f608,plain,(
% 0.15/11.14 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf42(X1,X2),X0)))),
% 0.15/11.14 inference(resolution,[status(thm)],[f286,f253])).
% 0.15/11.14 fof(f609,plain,(
% 0.15/11.14 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf43(X1,X2),X0)))),
% 0.15/11.14 inference(resolution,[status(thm)],[f286,f252])).
% 0.15/11.14 fof(f610,plain,(
% 0.15/11.14 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf45(X1,X2),X0)))),
% 0.15/11.14 inference(resolution,[status(thm)],[f286,f251])).
% 0.15/11.14 fof(f611,plain,(
% 0.15/11.14 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf46(X1,X2),X0)))),
% 0.15/11.14 inference(resolution,[status(thm)],[f286,f250])).
% 0.15/11.14 fof(f612,plain,(
% 0.15/11.14 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf47(X1,X2),X0)))),
% 0.15/11.14 inference(resolution,[status(thm)],[f286,f249])).
% 0.15/11.14 fof(f613,plain,(
% 0.15/11.14 ![X0,X1,X2]: (~ssList(X0)|ssList(app(skaf48(X1,X2),X0)))),
% 0.15/11.14 inference(resolution,[status(thm)],[f286,f248])).
% 0.15/11.14 fof(f614,plain,(
% 0.15/11.14 ![X0]: (~ssList(X0)|ssList(app(sk5,X0)))),
% 0.15/11.14 inference(resolution,[status(thm)],[f286,f437])).
% 0.15/11.14 fof(f616,plain,(
% 0.15/11.14 ![X0]: (~ssList(X0)|ssList(app(sk1,X0)))),
% 0.15/11.14 inference(resolution,[status(thm)],[f286,f431])).
% 0.15/11.14 fof(f619,plain,(
% 0.15/11.14 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(app(sk5,X0),X1)))),
% 0.15/11.14 inference(resolution,[status(thm)],[f614,f286])).
% 0.15/11.14 fof(f625,plain,(
% 0.15/11.14 ~ssList(nil)|ssList(sk5)),
% 0.15/11.14 inference(paramodulation,[status(thm)],[f519,f614])).
% 0.15/11.14 fof(f626,definition,(
% 0.15/11.14 sQ15_spl <=> (ssList(sk5))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f629,plain,(
% 0.15/11.14 ~sQ9_spl|sQ15_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f625,f547,f626])).
% 0.15/11.14 fof(f639,definition,(
% 0.15/11.14 sQ16_spl <=> (ssList(sk1))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f664,plain,(
% 0.15/11.14 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(app(sk1,X0),X1)))),
% 0.15/11.14 inference(resolution,[status(thm)],[f616,f286])).
% 0.15/11.14 fof(f671,plain,(
% 0.15/11.14 ~ssList(nil)|ssList(sk1)),
% 0.15/11.14 inference(paramodulation,[status(thm)],[f522,f616])).
% 0.15/11.14 fof(f673,plain,(
% 0.15/11.14 ~sQ9_spl|sQ16_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f671,f547,f639])).
% 0.15/11.14 fof(f674,plain,(
% 0.15/11.14 sk2=nil|~sQ2_spl),
% 0.15/11.14 inference(forward_demodulation,[status(thm)],[f455,f435])).
% 0.15/11.14 fof(f682,definition,(
% 0.15/11.14 sQ17_spl <=> (ssList(sk2))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f686,plain,(
% 0.15/11.14 ~ssList(sk5)|ssList(sk2)),
% 0.15/11.14 inference(paramodulation,[status(thm)],[f513,f616])).
% 0.15/11.14 fof(f687,plain,(
% 0.15/11.14 ~sQ15_spl|sQ17_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f686,f626,f682])).
% 0.15/11.14 fof(f729,plain,(
% 0.15/11.14 ![X0]: (~ssList(nil)|~ssList(X0)|ssList(app(sk5,X0)))),
% 0.15/11.14 inference(paramodulation,[status(thm)],[f519,f619])).
% 0.15/11.14 fof(f730,definition,(
% 0.15/11.14 ![X0]: (sQ19_spl <=> (~ssList(X0)|ssList(app(sk5,X0))))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f733,plain,(
% 0.15/11.14 ~sQ9_spl|sQ19_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f729,f547,f730])).
% 0.15/11.14 fof(f739,plain,(
% 0.15/11.14 neq(nil,nil)|~sQ2_spl|~sQ5_spl),
% 0.15/11.14 inference(backward_demodulation,[status(thm)],[f674,f465])).
% 0.15/11.14 fof(f746,plain,(
% 0.15/11.14 ~nil=sk1|sQ3_spl),
% 0.15/11.14 inference(forward_demodulation,[status(thm)],[f436,f459])).
% 0.15/11.14 fof(f769,plain,(
% 0.15/11.14 ~ssList(nil)|~ssList(sk1)|sk1=nil|sQ6_spl),
% 0.15/11.14 inference(resolution,[status(thm)],[f470,f303])).
% 0.15/11.14 fof(f770,plain,(
% 0.15/11.14 ~sQ9_spl|~sQ16_spl|sQ8_spl|sQ6_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f769,f547,f639,f475,f468])).
% 0.15/11.14 fof(f771,plain,(
% 0.15/11.14 ~sQ8_spl|sQ3_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f746,f475,f457])).
% 0.15/11.14 fof(f812,plain,(
% 0.15/11.14 ~ssList(nil)|~sQ2_spl|~sQ5_spl),
% 0.15/11.14 inference(resolution,[status(thm)],[f488,f739])).
% 0.15/11.14 fof(f814,plain,(
% 0.15/11.14 ~sQ9_spl|~sQ2_spl|~sQ5_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f812,f547,f454,f464])).
% 0.15/11.14 fof(f815,plain,(
% 0.15/11.14 sQ2_spl|~sQ4_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f584,f454,f461])).
% 0.15/11.14 fof(f925,plain,(
% 0.15/11.14 ![X0]: (~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~ssList(X0))),
% 0.15/11.14 inference(resolution,[status(thm)],[f340,f256])).
% 0.15/11.14 fof(f927,definition,(
% 0.15/11.14 ![X0]: (sQ28_spl <=> (~segmentP(nil,X0)|~ssList(X0)|X0=nil|~ssList(X0)))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f930,plain,(
% 0.15/11.14 sQ28_spl|~sQ9_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f925,f927,f547])).
% 0.15/11.14 fof(f1140,plain,(
% 0.15/11.14 ![X0]: (~ssList(nil)|~ssList(X0)|ssList(app(sk1,X0)))),
% 0.15/11.14 inference(paramodulation,[status(thm)],[f522,f664])).
% 0.15/11.14 fof(f1145,definition,(
% 0.15/11.14 ![X0]: (sQ30_spl <=> (~ssList(X0)|ssList(app(sk1,X0))))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f1148,plain,(
% 0.15/11.14 ~sQ9_spl|sQ30_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f1140,f547,f1145])).
% 0.15/11.14 fof(f1241,plain,(
% 0.15/11.14 ![X0,X1]: (~segmentP(X0,X1)|~ssList(nil)|~ssList(X1)|~ssList(X0)|segmentP(X0,nil)|~ssList(X1))),
% 0.15/11.14 inference(resolution,[status(thm)],[f375,f256])).
% 0.15/11.14 fof(f1243,definition,(
% 0.15/11.14 ![X0,X1]: (sQ31_spl <=> (~segmentP(X0,X1)|~ssList(X1)|~ssList(X0)|segmentP(X0,nil)|~ssList(X1)))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f1246,plain,(
% 0.15/11.14 sQ31_spl|~sQ9_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f1241,f1243,f547])).
% 0.15/11.14 fof(f1347,plain,(
% 0.15/11.14 ![X0,X1]: (~ssList(nil)|ssList(skaf42(X0,X1)))),
% 0.15/11.14 inference(paramodulation,[status(thm)],[f523,f608])).
% 0.15/11.14 fof(f1348,definition,(
% 0.15/11.14 ![X0,X1]: (sQ32_spl <=> (ssList(skaf42(X0,X1))))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.15/11.14 fof(f1351,plain,(
% 0.15/11.14 ~sQ9_spl|sQ32_spl),
% 0.15/11.14 inference(split_clause,[status(thm)],[f1347,f547,f1348])).
% 0.15/11.14 fof(f1368,plain,(
% 0.15/11.14 ![X0,X1]: (~ssList(nil)|ssList(skaf43(X0,X1)))),
% 0.15/11.14 inference(paramodulation,[status(thm)],[f514,f609])).
% 0.15/11.14 fof(f1369,definition,(
% 0.15/11.14 ![X0,X1]: (sQ33_spl <=> (ssList(skaf43(X0,X1))))),
% 0.15/11.14 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1372,plain,(
% 0.15/11.15 ~sQ9_spl|sQ33_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1368,f547,f1369])).
% 0.15/11.15 fof(f1389,plain,(
% 0.15/11.15 ![X0,X1]: (~ssList(nil)|ssList(skaf45(X0,X1)))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f515,f610])).
% 0.15/11.15 fof(f1390,definition,(
% 0.15/11.15 ![X0,X1]: (sQ34_spl <=> (ssList(skaf45(X0,X1))))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1393,plain,(
% 0.15/11.15 ~sQ9_spl|sQ34_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1389,f547,f1390])).
% 0.15/11.15 fof(f1528,plain,(
% 0.15/11.15 ![X0,X1]: (~ssItem(X0)|~ssItem(X0)|~ssList(X1)|~ssList(X1)|X1=X1)),
% 0.15/11.15 inference(equality_resolution,[status(thm)],[f404])).
% 0.15/11.15 fof(f1529,definition,(
% 0.15/11.15 ![X0]: (sQ38_spl <=> (~ssItem(X0)|~ssItem(X0)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1530,plain,(
% 0.15/11.15 ![X0]: (~ssItem(X0)|~ssItem(X0)|~sQ38_spl)),
% 0.15/11.15 inference(component_clause,[status(thm)],[f1529])).
% 0.15/11.15 fof(f1532,definition,(
% 0.15/11.15 ![X1]: (sQ39_spl <=> (~ssList(X1)|~ssList(X1)|X1=X1))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1535,plain,(
% 0.15/11.15 sQ38_spl|sQ39_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1528,f1529,f1532])).
% 0.15/11.15 fof(f1536,plain,(
% 0.15/11.15 ![X0]: (~ssItem(X0)|~sQ38_spl)),
% 0.15/11.15 inference(duplicate_literals_removal,[status(thm)],[f1530])).
% 0.15/11.15 fof(f1537,plain,(
% 0.15/11.15 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2))),
% 0.15/11.15 inference(resolution,[status(thm)],[f405,f256])).
% 0.15/11.15 fof(f1539,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ40_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1542,plain,(
% 0.15/11.15 sQ40_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1537,f1539,f547])).
% 0.15/11.15 fof(f1582,plain,(
% 0.15/11.15 $false|~sQ38_spl),
% 0.15/11.15 inference(forward_subsumption_resolution,[status(thm)],[f236,f1536])).
% 0.15/11.15 fof(f1583,plain,(
% 0.15/11.15 ~sQ38_spl),
% 0.15/11.15 inference(contradiction_clause,[status(thm)],[f1582])).
% 0.15/11.15 fof(f1633,plain,(
% 0.15/11.15 ![X0,X1]: (~ssList(X0)|~ssList(sk1)|~ssList(X1)|segmentP(app(app(sk1,X1),X0),X1)|~ssList(X1)|~ssList(X0))),
% 0.15/11.15 inference(resolution,[status(thm)],[f498,f664])).
% 0.15/11.15 fof(f1634,plain,(
% 0.15/11.15 ![X0,X1]: (~ssList(X0)|~ssList(sk5)|~ssList(X1)|segmentP(app(app(sk5,X1),X0),X1)|~ssList(X1)|~ssList(X0))),
% 0.15/11.15 inference(resolution,[status(thm)],[f498,f619])).
% 0.15/11.15 fof(f1635,plain,(
% 0.15/11.15 ![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))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f523,f498])).
% 0.15/11.15 fof(f1636,plain,(
% 0.15/11.15 ![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))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f518,f498])).
% 0.15/11.15 fof(f1637,plain,(
% 0.15/11.15 ![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))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f517,f498])).
% 0.15/11.15 fof(f1638,plain,(
% 0.15/11.15 ![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))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f516,f498])).
% 0.15/11.15 fof(f1639,plain,(
% 0.15/11.15 ![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))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f515,f498])).
% 0.15/11.15 fof(f1640,plain,(
% 0.15/11.15 ![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))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f514,f498])).
% 0.15/11.15 fof(f1641,plain,(
% 0.15/11.15 ![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)))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f540,f498])).
% 0.15/11.15 fof(f1642,plain,(
% 0.15/11.15 ![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)))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f539,f498])).
% 0.15/11.15 fof(f1643,plain,(
% 0.15/11.15 ![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)))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f538,f498])).
% 0.15/11.15 fof(f1644,plain,(
% 0.15/11.15 ![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)))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f537,f498])).
% 0.15/11.15 fof(f1645,plain,(
% 0.15/11.15 ![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)))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f536,f498])).
% 0.15/11.15 fof(f1646,plain,(
% 0.15/11.15 ![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)))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f535,f498])).
% 0.15/11.15 fof(f1647,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f544,f498])).
% 0.15/11.15 fof(f1648,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk5)|~ssList(app(sk5,X0))|segmentP(app(app(nil,sk5),X0),sk5))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f541,f498])).
% 0.15/11.15 fof(f1649,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f520,f498])).
% 0.15/11.15 fof(f1650,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(sk5)|~ssList(nil)|~ssList(app(sk5,X0))|segmentP(app(app(sk5,nil),X0),nil))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f519,f498])).
% 0.15/11.15 fof(f1652,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(nil)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f522,f498])).
% 0.15/11.15 fof(f1657,definition,(
% 0.15/11.15 ![X0,X1]: (sQ42_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(sk1,X1),X0),X1)|~ssList(X1)|~ssList(X0)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1660,plain,(
% 0.15/11.15 sQ42_spl|~sQ16_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1633,f1657,f639])).
% 0.15/11.15 fof(f1661,definition,(
% 0.15/11.15 ![X0,X1]: (sQ43_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(sk5,X1),X0),X1)|~ssList(X1)|~ssList(X0)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1664,plain,(
% 0.15/11.15 sQ43_spl|~sQ15_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1634,f1661,f626])).
% 0.15/11.15 fof(f1665,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ44_spl <=> (~ssList(X0)|~ssList(skaf42(X1,X2))|~ssList(app(skaf42(X1,X2),X0))|segmentP(app(app(skaf42(X1,X2),nil),X0),nil)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1668,plain,(
% 0.15/11.15 sQ44_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1635,f1665,f547])).
% 0.15/11.15 fof(f1669,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ45_spl <=> (~ssList(X0)|~ssList(skaf48(X1,X2))|~ssList(app(skaf48(X1,X2),X0))|segmentP(app(app(skaf48(X1,X2),nil),X0),nil)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1672,plain,(
% 0.15/11.15 sQ45_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1636,f1669,f547])).
% 0.15/11.15 fof(f1673,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ46_spl <=> (~ssList(X0)|~ssList(skaf47(X1,X2))|~ssList(app(skaf47(X1,X2),X0))|segmentP(app(app(skaf47(X1,X2),nil),X0),nil)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1676,plain,(
% 0.15/11.15 sQ46_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1637,f1673,f547])).
% 0.15/11.15 fof(f1677,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ47_spl <=> (~ssList(X0)|~ssList(skaf46(X1,X2))|~ssList(app(skaf46(X1,X2),X0))|segmentP(app(app(skaf46(X1,X2),nil),X0),nil)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1680,plain,(
% 0.15/11.15 sQ47_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1638,f1677,f547])).
% 0.15/11.15 fof(f1681,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ48_spl <=> (~ssList(X0)|~ssList(skaf45(X1,X2))|~ssList(app(skaf45(X1,X2),X0))|segmentP(app(app(skaf45(X1,X2),nil),X0),nil)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1684,plain,(
% 0.15/11.15 sQ48_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1639,f1681,f547])).
% 0.15/11.15 fof(f1685,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ49_spl <=> (~ssList(X0)|~ssList(skaf43(X1,X2))|~ssList(app(skaf43(X1,X2),X0))|segmentP(app(app(skaf43(X1,X2),nil),X0),nil)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1688,plain,(
% 0.15/11.15 sQ49_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1640,f1685,f547])).
% 0.15/11.15 fof(f1689,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ50_spl <=> (~ssList(X0)|~ssList(skaf48(X1,X2))|~ssList(app(skaf48(X1,X2),X0))|segmentP(app(app(nil,skaf48(X1,X2)),X0),skaf48(X1,X2))))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1692,plain,(
% 0.15/11.15 sQ50_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1641,f1689,f547])).
% 0.15/11.15 fof(f1693,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ51_spl <=> (~ssList(X0)|~ssList(skaf47(X1,X2))|~ssList(app(skaf47(X1,X2),X0))|segmentP(app(app(nil,skaf47(X1,X2)),X0),skaf47(X1,X2))))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1696,plain,(
% 0.15/11.15 sQ51_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1642,f1693,f547])).
% 0.15/11.15 fof(f1697,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ52_spl <=> (~ssList(X0)|~ssList(skaf46(X1,X2))|~ssList(app(skaf46(X1,X2),X0))|segmentP(app(app(nil,skaf46(X1,X2)),X0),skaf46(X1,X2))))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1700,plain,(
% 0.15/11.15 sQ52_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1643,f1697,f547])).
% 0.15/11.15 fof(f1701,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ53_spl <=> (~ssList(X0)|~ssList(skaf45(X1,X2))|~ssList(app(skaf45(X1,X2),X0))|segmentP(app(app(nil,skaf45(X1,X2)),X0),skaf45(X1,X2))))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1704,plain,(
% 0.15/11.15 sQ53_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1644,f1701,f547])).
% 0.15/11.15 fof(f1705,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ54_spl <=> (~ssList(X0)|~ssList(skaf43(X1,X2))|~ssList(app(skaf43(X1,X2),X0))|segmentP(app(app(nil,skaf43(X1,X2)),X0),skaf43(X1,X2))))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1708,plain,(
% 0.15/11.15 sQ54_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1645,f1705,f547])).
% 0.15/11.15 fof(f1709,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ55_spl <=> (~ssList(X0)|~ssList(skaf42(X1,X2))|~ssList(app(skaf42(X1,X2),X0))|segmentP(app(app(nil,skaf42(X1,X2)),X0),skaf42(X1,X2))))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1712,plain,(
% 0.15/11.15 sQ55_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1646,f1709,f547])).
% 0.15/11.15 fof(f1713,definition,(
% 0.15/11.15 ![X0]: (sQ56_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1714,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)|~sQ56_spl)),
% 0.15/11.15 inference(component_clause,[status(thm)],[f1713])).
% 0.15/11.15 fof(f1716,plain,(
% 0.15/11.15 sQ56_spl|~sQ9_spl|~sQ16_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1647,f1713,f547,f639])).
% 0.15/11.15 fof(f1717,definition,(
% 0.15/11.15 ![X0]: (sQ57_spl <=> (~ssList(X0)|~ssList(app(sk5,X0))|segmentP(app(app(nil,sk5),X0),sk5)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1718,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(app(sk5,X0))|segmentP(app(app(nil,sk5),X0),sk5)|~sQ57_spl)),
% 0.15/11.15 inference(component_clause,[status(thm)],[f1717])).
% 0.15/11.15 fof(f1720,plain,(
% 0.15/11.15 sQ57_spl|~sQ9_spl|~sQ15_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1648,f1717,f547,f626])).
% 0.15/11.15 fof(f1721,definition,(
% 0.15/11.15 ![X0]: (sQ58_spl <=> (~ssList(X0)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1724,plain,(
% 0.15/11.15 sQ58_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1649,f1721,f547])).
% 0.15/11.15 fof(f1725,definition,(
% 0.15/11.15 ![X0]: (sQ59_spl <=> (~ssList(X0)|~ssList(app(sk5,X0))|segmentP(app(app(sk5,nil),X0),nil)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1728,plain,(
% 0.15/11.15 sQ59_spl|~sQ15_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1650,f1725,f626,f547])).
% 0.15/11.15 fof(f1733,definition,(
% 0.15/11.15 ![X0]: (sQ61_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1736,plain,(
% 0.15/11.15 sQ61_spl|~sQ16_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1652,f1733,f639,f547])).
% 0.15/11.15 fof(f1738,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(app(sk5,X0))|segmentP(app(sk5,X0),sk5)|~sQ57_spl)),
% 0.15/11.15 inference(forward_demodulation,[status(thm)],[f541,f1718])).
% 0.15/11.15 fof(f1739,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|segmentP(app(sk5,X0),sk5)|~sQ57_spl)),
% 0.15/11.15 inference(forward_subsumption_resolution,[status(thm)],[f1738,f614])).
% 0.15/11.15 fof(f1742,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(sk1,X0),sk1)|~sQ56_spl)),
% 0.15/11.15 inference(forward_demodulation,[status(thm)],[f544,f1714])).
% 0.15/11.15 fof(f1743,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~sQ56_spl)),
% 0.15/11.15 inference(forward_subsumption_resolution,[status(thm)],[f1742,f616])).
% 0.15/11.15 fof(f1926,plain,(
% 0.15/11.15 ![X0,X1]: (~ssList(nil)|ssList(skaf46(X0,X1)))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f516,f611])).
% 0.15/11.15 fof(f1927,definition,(
% 0.15/11.15 ![X0,X1]: (sQ62_spl <=> (ssList(skaf46(X0,X1))))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1930,plain,(
% 0.15/11.15 ~sQ9_spl|sQ62_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1926,f547,f1927])).
% 0.15/11.15 fof(f1991,plain,(
% 0.15/11.15 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk5)|~ssList(app(sk5,X0))|segmentP(app(app(X2,app(sk5,X0)),X1),sk5)|~sQ57_spl)),
% 0.15/11.15 inference(resolution,[status(thm)],[f1739,f405])).
% 0.15/11.15 fof(f1992,plain,(
% 0.15/11.15 ![X0,X1]: (~ssList(X0)|~segmentP(X1,app(sk5,X0))|~ssList(sk5)|~ssList(app(sk5,X0))|~ssList(X1)|segmentP(X1,sk5)|~sQ57_spl)),
% 0.15/11.15 inference(resolution,[status(thm)],[f1739,f375])).
% 0.15/11.15 fof(f1993,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~segmentP(sk5,app(sk5,X0))|~ssList(sk5)|~ssList(app(sk5,X0))|app(sk5,X0)=sk5|~sQ57_spl)),
% 0.15/11.15 inference(resolution,[status(thm)],[f1739,f340])).
% 0.15/11.15 fof(f1994,plain,(
% 0.15/11.15 ~ssList(nil)|segmentP(sk5,sk5)|~sQ57_spl),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f519,f1739])).
% 0.15/11.15 fof(f1995,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ63_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk5,X0))|segmentP(app(app(X2,app(sk5,X0)),X1),sk5)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f1998,plain,(
% 0.15/11.15 sQ63_spl|~sQ15_spl|~sQ57_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1991,f1995,f626,f1717])).
% 0.15/11.15 fof(f1999,definition,(
% 0.15/11.15 ![X0,X1]: (sQ64_spl <=> (~ssList(X0)|~segmentP(X1,app(sk5,X0))|~ssList(app(sk5,X0))|~ssList(X1)|segmentP(X1,sk5)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2002,plain,(
% 0.15/11.15 sQ64_spl|~sQ15_spl|~sQ57_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1992,f1999,f626,f1717])).
% 0.15/11.15 fof(f2003,definition,(
% 0.15/11.15 ![X0]: (sQ65_spl <=> (~ssList(X0)|~segmentP(sk5,app(sk5,X0))|~ssList(app(sk5,X0))|app(sk5,X0)=sk5))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2006,plain,(
% 0.15/11.15 sQ65_spl|~sQ15_spl|~sQ57_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1993,f2003,f626,f1717])).
% 0.15/11.15 fof(f2007,definition,(
% 0.15/11.15 sQ66_spl <=> (segmentP(sk5,sk5))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2008,plain,(
% 0.15/11.15 segmentP(sk5,sk5)|~sQ66_spl),
% 0.15/11.15 inference(component_clause,[status(thm)],[f2007])).
% 0.15/11.15 fof(f2010,plain,(
% 0.15/11.15 ~sQ9_spl|sQ66_spl|~sQ57_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f1994,f547,f2007,f1717])).
% 0.15/11.15 fof(f2014,plain,(
% 0.15/11.15 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk5)|~ssList(sk5)|segmentP(app(app(X1,sk5),X0),sk5)|~sQ66_spl)),
% 0.15/11.15 inference(resolution,[status(thm)],[f2008,f405])).
% 0.15/11.15 fof(f2015,plain,(
% 0.15/11.15 ![X0]: (~segmentP(X0,sk5)|~ssList(sk5)|~ssList(sk5)|~ssList(X0)|segmentP(X0,sk5)|~sQ66_spl)),
% 0.15/11.15 inference(resolution,[status(thm)],[f2008,f375])).
% 0.15/11.15 fof(f2016,plain,(
% 0.15/11.15 ~segmentP(sk5,sk5)|~ssList(sk5)|~ssList(sk5)|sk5=sk5|~sQ66_spl),
% 0.15/11.15 inference(resolution,[status(thm)],[f2008,f340])).
% 0.15/11.15 fof(f2017,definition,(
% 0.15/11.15 ![X0,X1]: (sQ67_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk5),X0),sk5)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2020,plain,(
% 0.15/11.15 sQ67_spl|~sQ15_spl|~sQ66_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2014,f2017,f626,f2007])).
% 0.15/11.15 fof(f2021,definition,(
% 0.15/11.15 ![X0]: (sQ68_spl <=> (~segmentP(X0,sk5)|~ssList(X0)|segmentP(X0,sk5)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2024,plain,(
% 0.15/11.15 sQ68_spl|~sQ15_spl|~sQ66_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2015,f2021,f626,f2007])).
% 0.15/11.15 fof(f2025,definition,(
% 0.15/11.15 sQ69_spl <=> (sk5=sk5)),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2028,plain,(
% 0.15/11.15 ~sQ66_spl|~sQ15_spl|sQ69_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2016,f2007,f626,f2025])).
% 0.15/11.15 fof(f2051,plain,(
% 0.15/11.15 ![X0,X1]: (~ssList(nil)|ssList(skaf47(X0,X1)))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f517,f612])).
% 0.15/11.15 fof(f2052,definition,(
% 0.15/11.15 ![X0,X1]: (sQ70_spl <=> (ssList(skaf47(X0,X1))))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2055,plain,(
% 0.15/11.15 ~sQ9_spl|sQ70_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2051,f547,f2052])).
% 0.15/11.15 fof(f2076,plain,(
% 0.15/11.15 ![X0,X1]: (~ssList(nil)|ssList(skaf48(X0,X1)))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f518,f613])).
% 0.15/11.15 fof(f2077,definition,(
% 0.15/11.15 ![X0,X1]: (sQ71_spl <=> (ssList(skaf48(X0,X1))))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2080,plain,(
% 0.15/11.15 ~sQ9_spl|sQ71_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2076,f547,f2077])).
% 0.15/11.15 fof(f2081,plain,(
% 0.15/11.15 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),sk1)|~sQ56_spl)),
% 0.15/11.15 inference(resolution,[status(thm)],[f1743,f405])).
% 0.15/11.15 fof(f2082,plain,(
% 0.15/11.15 ![X0,X1]: (~ssList(X0)|~segmentP(X1,app(sk1,X0))|~ssList(sk1)|~ssList(app(sk1,X0))|~ssList(X1)|segmentP(X1,sk1)|~sQ56_spl)),
% 0.15/11.15 inference(resolution,[status(thm)],[f1743,f375])).
% 0.15/11.15 fof(f2083,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~segmentP(sk1,app(sk1,X0))|~ssList(sk1)|~ssList(app(sk1,X0))|app(sk1,X0)=sk1|~sQ56_spl)),
% 0.15/11.15 inference(resolution,[status(thm)],[f1743,f340])).
% 0.15/11.15 fof(f2084,plain,(
% 0.15/11.15 ~ssList(sk5)|segmentP(nil,sk1)|~sQ56_spl|~sQ4_spl),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f583,f1743])).
% 0.15/11.15 fof(f2085,plain,(
% 0.15/11.15 ~ssList(nil)|segmentP(sk1,sk1)|~sQ56_spl),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f522,f1743])).
% 0.15/11.15 fof(f2086,definition,(
% 0.15/11.15 ![X0,X1,X2]: (sQ72_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),sk1)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2089,plain,(
% 0.15/11.15 sQ72_spl|~sQ16_spl|~sQ56_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2081,f2086,f639,f1713])).
% 0.15/11.15 fof(f2090,definition,(
% 0.15/11.15 ![X0,X1]: (sQ73_spl <=> (~ssList(X0)|~segmentP(X1,app(sk1,X0))|~ssList(app(sk1,X0))|~ssList(X1)|segmentP(X1,sk1)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2093,plain,(
% 0.15/11.15 sQ73_spl|~sQ16_spl|~sQ56_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2082,f2090,f639,f1713])).
% 0.15/11.15 fof(f2094,definition,(
% 0.15/11.15 ![X0]: (sQ74_spl <=> (~ssList(X0)|~segmentP(sk1,app(sk1,X0))|~ssList(app(sk1,X0))|app(sk1,X0)=sk1))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2097,plain,(
% 0.15/11.15 sQ74_spl|~sQ16_spl|~sQ56_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2083,f2094,f639,f1713])).
% 0.15/11.15 fof(f2098,definition,(
% 0.15/11.15 sQ75_spl <=> (segmentP(nil,sk1))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2099,plain,(
% 0.15/11.15 segmentP(nil,sk1)|~sQ75_spl),
% 0.15/11.15 inference(component_clause,[status(thm)],[f2098])).
% 0.15/11.15 fof(f2101,plain,(
% 0.15/11.15 ~sQ15_spl|sQ75_spl|~sQ56_spl|~sQ4_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2084,f626,f2098,f1713,f461])).
% 0.15/11.15 fof(f2102,definition,(
% 0.15/11.15 sQ76_spl <=> (segmentP(sk1,sk1))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2103,plain,(
% 0.15/11.15 segmentP(sk1,sk1)|~sQ76_spl),
% 0.15/11.15 inference(component_clause,[status(thm)],[f2102])).
% 0.15/11.15 fof(f2105,plain,(
% 0.15/11.15 ~sQ9_spl|sQ76_spl|~sQ56_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2085,f547,f2102,f1713])).
% 0.15/11.15 fof(f2154,plain,(
% 0.15/11.15 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk1)|~ssList(sk1)|segmentP(app(app(X1,sk1),X0),sk1)|~sQ76_spl)),
% 0.15/11.15 inference(resolution,[status(thm)],[f2103,f405])).
% 0.15/11.15 fof(f2155,plain,(
% 0.15/11.15 ![X0]: (~segmentP(X0,sk1)|~ssList(sk1)|~ssList(sk1)|~ssList(X0)|segmentP(X0,sk1)|~sQ76_spl)),
% 0.15/11.15 inference(resolution,[status(thm)],[f2103,f375])).
% 0.15/11.15 fof(f2156,plain,(
% 0.15/11.15 ~segmentP(sk1,sk1)|~ssList(sk1)|~ssList(sk1)|sk1=sk1|~sQ76_spl),
% 0.15/11.15 inference(resolution,[status(thm)],[f2103,f340])).
% 0.15/11.15 fof(f2157,definition,(
% 0.15/11.15 ![X0,X1]: (sQ77_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),sk1)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2160,plain,(
% 0.15/11.15 sQ77_spl|~sQ16_spl|~sQ76_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2154,f2157,f639,f2102])).
% 0.15/11.15 fof(f2161,definition,(
% 0.15/11.15 ![X0]: (sQ78_spl <=> (~segmentP(X0,sk1)|~ssList(X0)|segmentP(X0,sk1)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2164,plain,(
% 0.15/11.15 sQ78_spl|~sQ16_spl|~sQ76_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2155,f2161,f639,f2102])).
% 0.15/11.15 fof(f2165,definition,(
% 0.15/11.15 sQ79_spl <=> (sk1=sk1)),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2168,plain,(
% 0.15/11.15 ~sQ76_spl|~sQ16_spl|sQ79_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2156,f2102,f639,f2165])).
% 0.15/11.15 fof(f2215,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f543,f498])).
% 0.15/11.15 fof(f2217,definition,(
% 0.15/11.15 ![X0]: (sQ80_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2220,plain,(
% 0.15/11.15 sQ80_spl|~sQ9_spl|~sQ17_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2215,f2217,f547,f682])).
% 0.15/11.15 fof(f2222,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(sk2)|~ssList(nil)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,nil),X0),nil))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f521,f498])).
% 0.15/11.15 fof(f2223,definition,(
% 0.15/11.15 ![X0]: (sQ81_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,nil),X0),nil)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2226,plain,(
% 0.15/11.15 sQ81_spl|~sQ17_spl|~sQ9_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2222,f2223,f682,f547])).
% 0.15/11.15 fof(f2228,plain,(
% 0.15/11.15 ~ssList(sk5)|segmentP(sk2,sk1)|~sQ56_spl),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f513,f1743])).
% 0.15/11.15 fof(f2229,plain,(
% 0.15/11.15 ![X0]: (~ssList(sk5)|~ssList(X0)|ssList(app(sk2,X0)))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f513,f664])).
% 0.15/11.15 fof(f2231,plain,(
% 0.15/11.15 ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(sk5)|~ssList(app(sk2,X0))|segmentP(app(app(sk1,sk5),X0),sk5))),
% 0.15/11.15 inference(paramodulation,[status(thm)],[f513,f498])).
% 0.15/11.15 fof(f2232,plain,(
% 0.15/11.15 ~sQ15_spl|sQ7_spl|~sQ56_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2228,f626,f471,f1713])).
% 0.15/11.15 fof(f2233,definition,(
% 0.15/11.15 ![X0]: (sQ82_spl <=> (~ssList(X0)|ssList(app(sk2,X0))))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2236,plain,(
% 0.15/11.15 ~sQ15_spl|sQ82_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2229,f626,f2233])).
% 0.15/11.15 fof(f2238,definition,(
% 0.15/11.15 ![X0]: (sQ83_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(sk1,sk5),X0),sk5)))),
% 0.15/11.15 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.15/11.15 fof(f2241,plain,(
% 0.15/11.15 sQ83_spl|~sQ16_spl|~sQ15_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2231,f2238,f639,f626])).
% 0.15/11.15 fof(f2245,plain,(
% 0.15/11.15 ~ssList(sk1)|nil=sk1|~sQ75_spl),
% 0.15/11.15 inference(resolution,[status(thm)],[f2099,f281])).
% 0.15/11.15 fof(f2249,plain,(
% 0.15/11.15 ~sQ16_spl|sQ8_spl|~sQ75_spl),
% 0.15/11.15 inference(split_clause,[status(thm)],[f2245,f639,f475,f2098])).
% 0.15/11.15 fof(f2262,plain,(
% 0.15/11.15 $false),
% 0.15/11.15 inference(sat_refutation,[status(thm)],[f460,f467,f474,f478,f553,f556,f629,f673,f687,f733,f770,f771,f814,f815,f930,f1148,f1246,f1351,f1372,f1393,f1535,f1542,f1583,f1660,f1664,f1668,f1672,f1676,f1680,f1684,f1688,f1692,f1696,f1700,f1704,f1708,f1712,f1716,f1720,f1724,f1728,f1736,f1930,f1998,f2002,f2006,f2010,f2020,f2024,f2028,f2055,f2080,f2089,f2093,f2097,f2101,f2105,f2160,f2164,f2168,f2220,f2226,f2232,f2236,f2241,f2249])).
% 0.15/11.15 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/11.17 % Elapsed time: 0.753790 seconds
% 0.15/11.17 % CPU time: 5.649041 seconds
% 0.15/11.17 % Total memory used: 175.819 MB
% 0.15/11.17 % Net memory used: 171.922 MB
%------------------------------------------------------------------------------