%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC071-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : 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:30 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC071-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 07:56:17 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 0.13/0.52 % Refutation found
% 0.13/0.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.52 fof(f8,axiom,(
% 0.13/0.52 ssList(nil) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f13,axiom,(
% 0.13/0.52 (![U]: (ssList(skaf82(U)) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f14,axiom,(
% 0.13/0.52 (![U]: (ssList(skaf81(U)) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f15,axiom,(
% 0.13/0.52 (![U]: (ssList(skaf80(U)) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f18,axiom,(
% 0.13/0.52 (![U]: (ssList(skaf77(U)) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f19,axiom,(
% 0.13/0.52 (![U]: (ssList(skaf76(U)) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f20,axiom,(
% 0.13/0.52 (![U]: (ssList(skaf75(U)) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f22,axiom,(
% 0.13/0.52 (![U]: (ssList(skaf73(U)) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f23,axiom,(
% 0.13/0.52 (![U]: (ssList(skaf72(U)) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f24,axiom,(
% 0.13/0.52 (![U]: (ssList(skaf71(U)) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f27,axiom,(
% 0.13/0.52 (![U]: (ssList(skaf68(U)) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f28,axiom,(
% 0.13/0.52 (![U]: (ssList(skaf67(U)) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f56,axiom,(
% 0.13/0.52 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f57,axiom,(
% 0.13/0.52 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f73,axiom,(
% 0.13/0.52 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f74,axiom,(
% 0.13/0.52 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f80,axiom,(
% 0.13/0.52 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f85,axiom,(
% 0.13/0.52 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f98,axiom,(
% 0.13/0.52 (![U,V]: (( cons(U,V) != nil| ~ ssItem(U)| ~ ssList(V) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f100,axiom,(
% 0.13/0.52 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f127,axiom,(
% 0.13/0.52 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f152,axiom,(
% 0.13/0.52 (![U,V,W]: (( ~ segmentP(U,V)| ~ segmentP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| segmentP(U,W) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f158,axiom,(
% 0.13/0.52 (![U,V,W]: (( ~ memberP(app(U,V),W)| ~ ssList(V)| ~ ssList(U)| ~ ssItem(W)| memberP(V,W)| memberP(U,W) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f172,axiom,(
% 0.13/0.52 (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f173,axiom,(
% 0.13/0.52 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f186,negated_conjecture,(
% 0.13/0.52 ssList(sk1) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f187,negated_conjecture,(
% 0.13/0.52 ssList(sk2) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f190,negated_conjecture,(
% 0.13/0.52 sk2 = sk4 ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f191,negated_conjecture,(
% 0.13/0.52 sk1 = sk3 ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f192,negated_conjecture,(
% 0.13/0.52 (![A]: (( ~ ssList(A)| ~ neq(A,nil)| ~ segmentP(sk2,A)| ~ segmentP(sk1,A) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f193,negated_conjecture,(
% 0.13/0.52 ( nil != sk2| nil != sk1 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f194,negated_conjecture,(
% 0.13/0.52 ( ssItem(sk5)| nil = sk4 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f196,negated_conjecture,(
% 0.13/0.52 ( ssList(sk6)| nil = sk4 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f197,negated_conjecture,(
% 0.13/0.52 ( ssList(sk7)| nil = sk4 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f198,negated_conjecture,(
% 0.13/0.52 ( cons(sk5,nil) = sk3| nil = sk4 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f199,negated_conjecture,(
% 0.13/0.52 ( app(app(sk6,sk3),sk7) = sk4| nil = sk4 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f202,negated_conjecture,(
% 0.13/0.52 ( ssList(sk6)| nil = sk3 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f203,negated_conjecture,(
% 0.13/0.52 ( ssList(sk7)| nil = sk3 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f205,negated_conjecture,(
% 0.13/0.52 ( app(app(sk6,sk3),sk7) = sk4| nil = sk3 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f215,plain,(
% 0.13/0.52 ssList(nil)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.52 fof(f220,plain,(
% 0.13/0.52 ![X0]: (ssList(skaf82(X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f13])).
% 0.13/0.52 fof(f221,plain,(
% 0.13/0.52 ![X0]: (ssList(skaf81(X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f14])).
% 0.13/0.52 fof(f222,plain,(
% 0.13/0.52 ![X0]: (ssList(skaf80(X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.52 fof(f225,plain,(
% 0.13/0.52 ![X0]: (ssList(skaf77(X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f18])).
% 0.13/0.52 fof(f226,plain,(
% 0.13/0.52 ![X0]: (ssList(skaf76(X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/0.52 fof(f227,plain,(
% 0.13/0.52 ![X0]: (ssList(skaf75(X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f20])).
% 0.13/0.52 fof(f229,plain,(
% 0.13/0.52 ![X0]: (ssList(skaf73(X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f22])).
% 0.13/0.52 fof(f230,plain,(
% 0.13/0.52 ![X0]: (ssList(skaf72(X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f23])).
% 0.13/0.52 fof(f231,plain,(
% 0.13/0.52 ![X0]: (ssList(skaf71(X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f24])).
% 0.13/0.52 fof(f234,plain,(
% 0.13/0.52 ![X0]: (ssList(skaf68(X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f27])).
% 0.13/0.52 fof(f235,plain,(
% 0.13/0.52 ![X0]: (ssList(skaf67(X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f28])).
% 0.13/0.52 fof(f263,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f56])).
% 0.13/0.52 fof(f264,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f57])).
% 0.13/0.52 fof(f281,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f73])).
% 0.13/0.52 fof(f282,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f74])).
% 0.13/0.52 fof(f288,plain,(
% 0.13/0.52 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f80])).
% 0.13/0.52 fof(f293,plain,(
% 0.13/0.52 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f85])).
% 0.13/0.52 fof(f306,plain,(
% 0.13/0.52 ![V]: ((![U]: (~cons(U,V)=nil|~ssItem(U)))|~ssList(V))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f98])).
% 0.13/0.52 fof(f307,plain,(
% 0.13/0.52 ![X0,X1]: (~cons(X0,X1)=nil|~ssItem(X0)|~ssList(X1))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f306])).
% 0.13/0.52 fof(f310,plain,(
% 0.13/0.52 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f100])).
% 0.13/0.52 fof(f347,plain,(
% 0.13/0.52 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f127])).
% 0.13/0.52 fof(f381,plain,(
% 0.13/0.52 ![U,W]: (((![V]: (((~segmentP(U,V)|~segmentP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|segmentP(U,W))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f152])).
% 0.13/0.52 fof(f382,plain,(
% 0.13/0.52 ![X0,X1,X2]: (~segmentP(X0,X1)|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|segmentP(X0,X2))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f381])).
% 0.13/0.52 fof(f392,plain,(
% 0.13/0.52 ![U,W]: ((![V]: ((((~memberP(app(U,V),W)|~ssList(V))|~ssList(U))|~ssItem(W))|memberP(V,W)))|memberP(U,W))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f158])).
% 0.13/0.52 fof(f393,plain,(
% 0.13/0.52 ![X0,X1,X2]: (~memberP(app(X0,X1),X2)|~ssList(X1)|~ssList(X0)|~ssItem(X2)|memberP(X1,X2)|memberP(X0,X2))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f392])).
% 0.13/0.52 fof(f412,plain,(
% 0.13/0.52 ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f172])).
% 0.13/0.52 fof(f413,plain,(
% 0.13/0.52 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f173])).
% 0.13/0.52 fof(f414,plain,(
% 0.13/0.52 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f413])).
% 0.13/0.52 fof(f438,plain,(
% 0.13/0.52 ssList(sk1)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f186])).
% 0.13/0.52 fof(f439,plain,(
% 0.13/0.52 ssList(sk2)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f187])).
% 0.13/0.52 fof(f442,plain,(
% 0.13/0.52 sk2=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f190])).
% 0.13/0.52 fof(f443,plain,(
% 0.13/0.52 sk1=sk3),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f191])).
% 0.13/0.52 fof(f444,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f192])).
% 0.13/0.52 fof(f445,plain,(
% 0.13/0.52 ~nil=sk2|~nil=sk1),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f193])).
% 0.13/0.52 fof(f446,plain,(
% 0.13/0.52 ssItem(sk5)|nil=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f194])).
% 0.13/0.52 fof(f448,plain,(
% 0.13/0.52 ssList(sk6)|nil=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f196])).
% 0.13/0.52 fof(f449,plain,(
% 0.13/0.52 ssList(sk7)|nil=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f197])).
% 0.13/0.52 fof(f450,plain,(
% 0.13/0.52 cons(sk5,nil)=sk3|nil=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f198])).
% 0.13/0.52 fof(f451,plain,(
% 0.13/0.52 app(app(sk6,sk3),sk7)=sk4|nil=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f199])).
% 0.13/0.52 fof(f456,plain,(
% 0.13/0.52 ssList(sk6)|nil=sk3),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f202])).
% 0.13/0.52 fof(f457,plain,(
% 0.13/0.52 ssList(sk7)|nil=sk3),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f203])).
% 0.13/0.52 fof(f459,plain,(
% 0.13/0.52 app(app(sk6,sk3),sk7)=sk4|nil=sk3),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f205])).
% 0.13/0.52 fof(f471,definition,(
% 0.13/0.52 sQ2_spl <=> (nil=sk2)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f473,plain,(
% 0.13/0.52 ~nil=sk2|sQ2_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f471])).
% 0.13/0.52 fof(f474,definition,(
% 0.13/0.52 sQ3_spl <=> (nil=sk1)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f475,plain,(
% 0.13/0.52 nil=sk1|~sQ3_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f474])).
% 0.13/0.52 fof(f476,plain,(
% 0.13/0.52 ~nil=sk1|sQ3_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f474])).
% 0.13/0.52 fof(f477,plain,(
% 0.13/0.52 ~sQ2_spl|~sQ3_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f445,f471,f474])).
% 0.13/0.52 fof(f478,definition,(
% 0.13/0.52 sQ4_spl <=> (ssItem(sk5))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f481,definition,(
% 0.13/0.52 sQ5_spl <=> (nil=sk4)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f482,plain,(
% 0.13/0.52 nil=sk4|~sQ5_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f481])).
% 0.13/0.52 fof(f484,plain,(
% 0.13/0.52 sQ4_spl|sQ5_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f446,f478,f481])).
% 0.13/0.52 fof(f485,definition,(
% 0.13/0.52 sQ6_spl <=> (nil=sk3)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f486,plain,(
% 0.13/0.52 nil=sk3|~sQ6_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f485])).
% 0.13/0.52 fof(f487,plain,(
% 0.13/0.52 ~nil=sk3|sQ6_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f485])).
% 0.13/0.52 fof(f489,definition,(
% 0.13/0.52 sQ7_spl <=> (ssList(sk6))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f492,plain,(
% 0.13/0.52 sQ7_spl|sQ5_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f448,f489,f481])).
% 0.13/0.52 fof(f493,definition,(
% 0.13/0.52 sQ8_spl <=> (ssList(sk7))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f496,plain,(
% 0.13/0.52 sQ8_spl|sQ5_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f449,f493,f481])).
% 0.13/0.52 fof(f497,definition,(
% 0.13/0.52 sQ9_spl <=> (cons(sk5,nil)=sk3)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f498,plain,(
% 0.13/0.52 cons(sk5,nil)=sk3|~sQ9_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f497])).
% 0.13/0.52 fof(f500,plain,(
% 0.13/0.52 sQ9_spl|sQ5_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f450,f497,f481])).
% 0.13/0.52 fof(f501,definition,(
% 0.13/0.52 sQ10_spl <=> (app(app(sk6,sk3),sk7)=sk4)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f502,plain,(
% 0.13/0.52 app(app(sk6,sk3),sk7)=sk4|~sQ10_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f501])).
% 0.13/0.52 fof(f504,plain,(
% 0.13/0.52 sQ10_spl|sQ5_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f451,f501,f481])).
% 0.13/0.52 fof(f513,plain,(
% 0.13/0.52 sQ7_spl|sQ6_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f456,f489,f485])).
% 0.13/0.52 fof(f514,plain,(
% 0.13/0.52 sQ8_spl|sQ6_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f457,f493,f485])).
% 0.13/0.52 fof(f516,plain,(
% 0.13/0.52 sQ10_spl|sQ6_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f459,f501,f485])).
% 0.13/0.52 fof(f537,plain,(
% 0.13/0.52 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 0.13/0.52 inference(destructive_equality_resolution,[status(thm)],[f414])).
% 0.13/0.52 fof(f551,plain,(
% 0.13/0.52 nil=sk1|~sQ6_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f443,f486])).
% 0.13/0.52 fof(f566,plain,(
% 0.13/0.52 cons(sk5,sk1)=sk3|~sQ6_spl|~sQ9_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f551,f498])).
% 0.13/0.52 fof(f567,plain,(
% 0.13/0.52 cons(sk5,sk1)=sk1|~sQ6_spl|~sQ9_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f443,f566])).
% 0.13/0.52 fof(f568,plain,(
% 0.13/0.52 app(app(sk6,sk1),sk7)=sk4|~sQ10_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f443,f502])).
% 0.13/0.52 fof(f569,plain,(
% 0.13/0.52 ~sk1=sk1|~sQ6_spl|sQ3_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f551,f476])).
% 0.13/0.52 fof(f570,plain,(
% 0.13/0.52 $false|~sQ6_spl|sQ3_spl),
% 0.13/0.52 inference(trivial_equality_resolution,[status(thm)],[f569])).
% 0.13/0.52 fof(f571,plain,(
% 0.13/0.52 ~sQ6_spl|sQ3_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f570])).
% 0.13/0.52 fof(f573,plain,(
% 0.13/0.52 ~nil=sk1|sQ6_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f443,f487])).
% 0.13/0.52 fof(f574,plain,(
% 0.13/0.52 app(nil,nil)=nil),
% 0.13/0.52 inference(resolution,[status(thm)],[f281,f215])).
% 0.13/0.52 fof(f577,plain,(
% 0.13/0.52 ![X0]: (app(skaf82(X0),nil)=skaf82(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f281,f220])).
% 0.13/0.52 fof(f578,plain,(
% 0.13/0.52 app(sk2,nil)=sk2),
% 0.13/0.52 inference(resolution,[status(thm)],[f281,f439])).
% 0.13/0.52 fof(f579,plain,(
% 0.13/0.52 app(sk1,nil)=sk1),
% 0.13/0.52 inference(resolution,[status(thm)],[f281,f438])).
% 0.13/0.52 fof(f580,plain,(
% 0.13/0.52 ![X0]: (app(skaf81(X0),nil)=skaf81(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f221,f281])).
% 0.13/0.52 fof(f581,plain,(
% 0.13/0.52 ![X0]: (app(skaf80(X0),nil)=skaf80(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f222,f281])).
% 0.13/0.52 fof(f582,plain,(
% 0.13/0.52 app(app(sk6,sk1),sk7)=sk2|~sQ10_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f442,f568])).
% 0.13/0.52 fof(f583,plain,(
% 0.13/0.52 ![X0]: (app(nil,skaf80(X0))=skaf80(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f282,f222])).
% 0.13/0.52 fof(f584,plain,(
% 0.13/0.52 ![X0]: (app(nil,skaf81(X0))=skaf81(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f282,f221])).
% 0.13/0.52 fof(f588,plain,(
% 0.13/0.52 ![X0]: (app(nil,skaf82(X0))=skaf82(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f282,f220])).
% 0.13/0.52 fof(f589,plain,(
% 0.13/0.52 app(nil,sk2)=sk2),
% 0.13/0.52 inference(resolution,[status(thm)],[f282,f439])).
% 0.13/0.52 fof(f590,plain,(
% 0.13/0.52 app(nil,sk1)=sk1),
% 0.13/0.52 inference(resolution,[status(thm)],[f282,f438])).
% 0.13/0.52 fof(f591,plain,(
% 0.13/0.52 ![X0]: (app(nil,skaf77(X0))=skaf77(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f225,f282])).
% 0.13/0.52 fof(f592,plain,(
% 0.13/0.52 ![X0]: (app(skaf77(X0),nil)=skaf77(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f225,f281])).
% 0.13/0.52 fof(f593,plain,(
% 0.13/0.52 ![X0]: (app(nil,skaf76(X0))=skaf76(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f226,f282])).
% 0.13/0.52 fof(f594,plain,(
% 0.13/0.52 ![X0]: (app(skaf76(X0),nil)=skaf76(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f226,f281])).
% 0.13/0.52 fof(f595,plain,(
% 0.13/0.52 ![X0]: (app(nil,skaf75(X0))=skaf75(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f227,f282])).
% 0.13/0.52 fof(f596,plain,(
% 0.13/0.52 ![X0]: (app(skaf75(X0),nil)=skaf75(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f227,f281])).
% 0.13/0.52 fof(f597,plain,(
% 0.13/0.52 ![X0]: (app(nil,skaf73(X0))=skaf73(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f229,f282])).
% 0.13/0.52 fof(f598,plain,(
% 0.13/0.52 ![X0]: (app(skaf73(X0),nil)=skaf73(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f229,f281])).
% 0.13/0.52 fof(f599,plain,(
% 0.13/0.52 ![X0]: (app(nil,skaf72(X0))=skaf72(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f230,f282])).
% 0.13/0.52 fof(f600,plain,(
% 0.13/0.52 ![X0]: (app(skaf72(X0),nil)=skaf72(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f230,f281])).
% 0.13/0.52 fof(f601,plain,(
% 0.13/0.52 ![X0]: (app(nil,skaf71(X0))=skaf71(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f231,f282])).
% 0.13/0.52 fof(f602,plain,(
% 0.13/0.52 ![X0]: (app(skaf71(X0),nil)=skaf71(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f231,f281])).
% 0.13/0.52 fof(f603,plain,(
% 0.13/0.52 ![X0]: (app(nil,skaf68(X0))=skaf68(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f234,f282])).
% 0.13/0.52 fof(f604,plain,(
% 0.13/0.52 ![X0]: (app(skaf68(X0),nil)=skaf68(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f234,f281])).
% 0.13/0.52 fof(f605,plain,(
% 0.13/0.52 ![X0]: (app(nil,skaf67(X0))=skaf67(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f235,f282])).
% 0.13/0.52 fof(f606,plain,(
% 0.13/0.52 ![X0]: (app(skaf67(X0),nil)=skaf67(X0))),
% 0.13/0.52 inference(resolution,[status(thm)],[f235,f281])).
% 0.13/0.52 fof(f607,plain,(
% 0.13/0.52 ~ssList(nil)|nil=nil|~ssList(nil)),
% 0.13/0.52 inference(resolution,[status(thm)],[f288,f263])).
% 0.13/0.52 fof(f609,definition,(
% 0.13/0.52 sQ13_spl <=> (ssList(nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f611,plain,(
% 0.13/0.52 ~ssList(nil)|sQ13_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f609])).
% 0.13/0.52 fof(f612,definition,(
% 0.13/0.52 sQ14_spl <=> (nil=nil)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f615,plain,(
% 0.13/0.52 ~sQ13_spl|sQ14_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f607,f609,f612])).
% 0.13/0.52 fof(f617,plain,(
% 0.13/0.52 $false|sQ13_spl),
% 0.13/0.52 inference(forward_subsumption_resolution,[status(thm)],[f611,f215])).
% 0.13/0.52 fof(f618,plain,(
% 0.13/0.52 sQ13_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f617])).
% 0.13/0.52 fof(f622,plain,(
% 0.13/0.52 ![X0]: (~ssList(nil)|~ssList(skaf80(X0))|ssList(skaf80(X0)))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f581,f293])).
% 0.13/0.52 fof(f623,plain,(
% 0.13/0.52 ![X0]: (~ssList(nil)|~ssList(skaf81(X0))|ssList(skaf81(X0)))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f580,f293])).
% 0.13/0.52 fof(f624,plain,(
% 0.13/0.52 ![X0]: (~ssList(nil)|~ssList(skaf82(X0))|ssList(skaf82(X0)))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f577,f293])).
% 0.13/0.52 fof(f633,plain,(
% 0.13/0.52 ~ssList(sk7)|~ssList(app(sk6,sk1))|ssList(sk2)|~sQ10_spl),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f582,f293])).
% 0.13/0.52 fof(f636,definition,(
% 0.13/0.52 ![X0]: (sQ15_spl <=> (~ssList(skaf80(X0))|ssList(skaf80(X0))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f639,plain,(
% 0.13/0.52 ~sQ13_spl|sQ15_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f622,f609,f636])).
% 0.13/0.52 fof(f640,definition,(
% 0.13/0.52 ![X0]: (sQ16_spl <=> (~ssList(skaf81(X0))|ssList(skaf81(X0))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f643,plain,(
% 0.13/0.52 ~sQ13_spl|sQ16_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f623,f609,f640])).
% 0.13/0.52 fof(f644,definition,(
% 0.13/0.52 ![X0]: (sQ17_spl <=> (~ssList(skaf82(X0))|ssList(skaf82(X0))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f647,plain,(
% 0.13/0.52 ~sQ13_spl|sQ17_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f624,f609,f644])).
% 0.13/0.52 fof(f648,definition,(
% 0.13/0.52 sQ18_spl <=> (ssList(sk1))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f650,plain,(
% 0.13/0.52 ~ssList(sk1)|sQ18_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f648])).
% 0.13/0.52 fof(f652,definition,(
% 0.13/0.52 sQ19_spl <=> (ssList(sk2))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f662,definition,(
% 0.13/0.52 sQ20_spl <=> (ssList(app(sk6,sk1)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f664,plain,(
% 0.13/0.52 ~ssList(app(sk6,sk1))|sQ20_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f662])).
% 0.13/0.52 fof(f665,plain,(
% 0.13/0.52 ~sQ8_spl|~sQ20_spl|sQ19_spl|~sQ10_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f633,f493,f662,f652,f501])).
% 0.13/0.52 fof(f701,plain,(
% 0.13/0.52 ![X0,X1]: (~cons(X0,X1)=sk1|~ssItem(X0)|~ssList(X1)|~sQ6_spl)),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f551,f307])).
% 0.13/0.52 fof(f702,plain,(
% 0.13/0.52 ~ssItem(sk5)|~ssList(sk1)|~sQ9_spl|~sQ6_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f567,f701])).
% 0.13/0.52 fof(f705,plain,(
% 0.13/0.52 ~sQ4_spl|~sQ18_spl|~sQ9_spl|~sQ6_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f702,f478,f648,f497,f485])).
% 0.13/0.52 fof(f711,plain,(
% 0.13/0.52 $false|sQ18_spl),
% 0.13/0.52 inference(forward_subsumption_resolution,[status(thm)],[f650,f438])).
% 0.13/0.52 fof(f712,plain,(
% 0.13/0.52 sQ18_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f711])).
% 0.13/0.52 fof(f715,plain,(
% 0.13/0.52 ~ssList(sk1)|~ssList(sk6)|sQ20_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f664,f293])).
% 0.13/0.52 fof(f716,plain,(
% 0.13/0.52 ~sQ18_spl|~sQ7_spl|sQ20_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f715,f648,f489,f662])).
% 0.13/0.52 fof(f717,plain,(
% 0.13/0.52 nil=sk2|~sQ5_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f442,f482])).
% 0.13/0.52 fof(f718,plain,(
% 0.13/0.52 $false|sQ2_spl|~sQ5_spl),
% 0.13/0.52 inference(forward_subsumption_resolution,[status(thm)],[f717,f473])).
% 0.13/0.52 fof(f719,plain,(
% 0.13/0.52 sQ2_spl|~sQ5_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f718])).
% 0.13/0.52 fof(f758,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|~neq(X0,sk2)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~sQ5_spl)),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f717,f444])).
% 0.13/0.52 fof(f759,plain,(
% 0.13/0.52 ~ssList(sk2)|~neq(sk2,sk2)|~segmentP(sk1,sk2)|~ssList(sk2)|~sQ5_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f758,f264])).
% 0.13/0.52 fof(f761,definition,(
% 0.13/0.52 sQ22_spl <=> (neq(sk2,sk2))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f763,plain,(
% 0.13/0.52 ~neq(sk2,sk2)|sQ22_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f761])).
% 0.13/0.52 fof(f764,definition,(
% 0.13/0.52 sQ23_spl <=> (segmentP(sk1,sk2))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f767,plain,(
% 0.13/0.52 ~sQ19_spl|~sQ22_spl|~sQ23_spl|~sQ5_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f759,f652,f761,f764,f481])).
% 0.13/0.52 fof(f768,definition,(
% 0.13/0.52 sQ24_spl <=> (neq(sk1,sk2))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f770,plain,(
% 0.13/0.52 ~neq(sk1,sk2)|sQ24_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f768])).
% 0.13/0.52 fof(f775,plain,(
% 0.13/0.52 ~ssList(sk2)|~ssList(sk2)|sk2=sk2|sQ22_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f763,f310])).
% 0.13/0.52 fof(f776,definition,(
% 0.13/0.52 sQ26_spl <=> (sk2=sk2)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f779,plain,(
% 0.13/0.52 ~sQ19_spl|sQ26_spl|sQ22_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f775,f652,f776,f761])).
% 0.13/0.52 fof(f780,plain,(
% 0.13/0.52 ~ssList(sk2)|~ssList(sk1)|sk1=sk2|sQ24_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f770,f310])).
% 0.13/0.52 fof(f781,definition,(
% 0.13/0.52 sQ27_spl <=> (sk1=sk2)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f782,plain,(
% 0.13/0.52 sk1=sk2|~sQ27_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f781])).
% 0.13/0.52 fof(f784,plain,(
% 0.13/0.52 ~sQ19_spl|~sQ18_spl|sQ27_spl|sQ24_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f780,f652,f648,f781,f768])).
% 0.13/0.52 fof(f854,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk1,X0)|~segmentP(sk1,X0)|~sQ27_spl)),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f782,f444])).
% 0.13/0.52 fof(f855,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk1,X0)|~sQ27_spl)),
% 0.13/0.52 inference(duplicate_literals_removal,[status(thm)],[f854])).
% 0.13/0.52 fof(f856,plain,(
% 0.13/0.52 ~ssList(sk1)|~neq(sk1,nil)|~ssList(sk1)|~sQ27_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f855,f264])).
% 0.13/0.52 fof(f857,definition,(
% 0.13/0.52 sQ29_spl <=> (neq(sk1,nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f859,plain,(
% 0.13/0.52 ~neq(sk1,nil)|sQ29_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f857])).
% 0.13/0.52 fof(f860,plain,(
% 0.13/0.52 ~sQ18_spl|~sQ29_spl|~sQ27_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f856,f648,f857,f781])).
% 0.13/0.52 fof(f862,plain,(
% 0.13/0.52 ~ssList(nil)|~ssList(sk1)|sk1=nil|sQ29_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f859,f310])).
% 0.13/0.52 fof(f870,plain,(
% 0.13/0.52 ~sQ13_spl|~sQ18_spl|sQ3_spl|sQ29_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f862,f609,f648,f474,f857])).
% 0.13/0.52 fof(f871,plain,(
% 0.13/0.52 $false|sQ6_spl|~sQ3_spl),
% 0.13/0.52 inference(forward_subsumption_resolution,[status(thm)],[f475,f573])).
% 0.13/0.52 fof(f872,plain,(
% 0.13/0.52 sQ6_spl|~sQ3_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f871])).
% 0.13/0.52 fof(f945,plain,(
% 0.13/0.52 ~ssList(sk2)|~ssList(nil)|~neq(nil,nil)|~segmentP(sk1,nil)),
% 0.13/0.52 inference(resolution,[status(thm)],[f263,f444])).
% 0.13/0.52 fof(f946,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil)),
% 0.13/0.52 inference(resolution,[status(thm)],[f263,f347])).
% 0.13/0.52 fof(f947,definition,(
% 0.13/0.52 sQ36_spl <=> (neq(nil,nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f950,definition,(
% 0.13/0.52 sQ37_spl <=> (segmentP(sk1,nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f951,plain,(
% 0.13/0.52 segmentP(sk1,nil)|~sQ37_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f950])).
% 0.13/0.52 fof(f952,plain,(
% 0.13/0.52 ~segmentP(sk1,nil)|sQ37_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f950])).
% 0.13/0.52 fof(f953,plain,(
% 0.13/0.52 ~sQ19_spl|~sQ13_spl|~sQ36_spl|~sQ37_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f945,f652,f609,f947,f950])).
% 0.13/0.52 fof(f954,definition,(
% 0.13/0.52 ![X0]: (sQ38_spl <=> (~ssList(X0)|~segmentP(nil,X0)|~ssList(X0)|X0=nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f957,plain,(
% 0.13/0.52 sQ38_spl|~sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f946,f954,f609])).
% 0.13/0.52 fof(f963,plain,(
% 0.13/0.52 ~ssList(sk1)|sQ37_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f952,f263])).
% 0.13/0.52 fof(f964,plain,(
% 0.13/0.52 ~sQ18_spl|sQ37_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f963,f648,f950])).
% 0.13/0.52 fof(f965,plain,(
% 0.13/0.52 ~segmentP(nil,sk1)|~ssList(nil)|~ssList(sk1)|sk1=nil|~sQ37_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f951,f347])).
% 0.13/0.52 fof(f966,definition,(
% 0.13/0.52 sQ39_spl <=> (segmentP(nil,sk1))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f969,plain,(
% 0.13/0.52 ~sQ39_spl|~sQ13_spl|~sQ18_spl|sQ3_spl|~sQ37_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f965,f966,f609,f648,f474,f950])).
% 0.13/0.52 fof(f1485,plain,(
% 0.13/0.52 ![X0]: (~segmentP(X0,sk1)|~ssList(nil)|~ssList(sk1)|~ssList(X0)|segmentP(X0,nil)|~sQ37_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f382,f951])).
% 0.13/0.52 fof(f1486,plain,(
% 0.13/0.52 ![X0,X1]: (~segmentP(X0,X1)|~ssList(nil)|~ssList(X1)|~ssList(X0)|segmentP(X0,nil)|~ssList(X1))),
% 0.13/0.52 inference(resolution,[status(thm)],[f382,f263])).
% 0.13/0.52 fof(f1488,definition,(
% 0.13/0.52 ![X0]: (sQ48_spl <=> (~segmentP(X0,sk1)|~ssList(X0)|segmentP(X0,nil)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1491,plain,(
% 0.13/0.52 sQ48_spl|~sQ13_spl|~sQ18_spl|~sQ37_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1485,f1488,f609,f648,f950])).
% 0.13/0.52 fof(f1492,definition,(
% 0.13/0.52 ![X0,X1]: (sQ49_spl <=> (~segmentP(X0,X1)|~ssList(X1)|~ssList(X0)|segmentP(X0,nil)|~ssList(X1)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1495,plain,(
% 0.13/0.52 sQ49_spl|~sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1486,f1492,f609])).
% 0.13/0.52 fof(f1578,plain,(
% 0.13/0.52 ![X0]: (~ssList(skaf77(X0))|~ssList(nil)|ssList(skaf77(X0)))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f591,f293])).
% 0.13/0.52 fof(f1579,definition,(
% 0.13/0.52 ![X0]: (sQ50_spl <=> (~ssList(skaf77(X0))|ssList(skaf77(X0))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1582,plain,(
% 0.13/0.52 sQ50_spl|~sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1578,f1579,f609])).
% 0.13/0.52 fof(f1585,plain,(
% 0.13/0.52 ![X0]: (~ssList(skaf76(X0))|~ssList(nil)|ssList(skaf76(X0)))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f593,f293])).
% 0.13/0.52 fof(f1586,definition,(
% 0.13/0.52 ![X0]: (sQ51_spl <=> (~ssList(skaf76(X0))|ssList(skaf76(X0))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1589,plain,(
% 0.13/0.52 sQ51_spl|~sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1585,f1586,f609])).
% 0.13/0.52 fof(f1611,plain,(
% 0.13/0.52 ![X0,X1]: (~memberP(skaf76(X0),X1)|~ssList(nil)|~ssList(skaf76(X0))|~ssItem(X1)|memberP(nil,X1)|memberP(skaf76(X0),X1))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f594,f393])).
% 0.13/0.52 fof(f1612,plain,(
% 0.13/0.52 ![X0,X1]: (~memberP(skaf77(X0),X1)|~ssList(nil)|~ssList(skaf77(X0))|~ssItem(X1)|memberP(nil,X1)|memberP(skaf77(X0),X1))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f592,f393])).
% 0.13/0.52 fof(f1613,plain,(
% 0.13/0.52 ![X0]: (~memberP(sk1,X0)|~ssList(nil)|~ssList(sk1)|~ssItem(X0)|memberP(nil,X0)|memberP(sk1,X0))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f579,f393])).
% 0.13/0.52 fof(f1615,plain,(
% 0.13/0.52 ![X0]: (~memberP(sk2,X0)|~ssList(nil)|~ssList(sk2)|~ssItem(X0)|memberP(nil,X0)|memberP(sk2,X0))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f578,f393])).
% 0.13/0.52 fof(f1619,plain,(
% 0.13/0.52 ![X0,X1]: (~memberP(skaf82(X0),X1)|~ssList(skaf82(X0))|~ssList(nil)|~ssItem(X1)|memberP(skaf82(X0),X1)|memberP(nil,X1))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f588,f393])).
% 0.13/0.52 fof(f1620,plain,(
% 0.13/0.52 ![X0,X1]: (~memberP(skaf81(X0),X1)|~ssList(skaf81(X0))|~ssList(nil)|~ssItem(X1)|memberP(skaf81(X0),X1)|memberP(nil,X1))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f584,f393])).
% 0.13/0.52 fof(f1624,plain,(
% 0.13/0.52 ![X0]: (~memberP(nil,X0)|~ssList(nil)|~ssList(nil)|~ssItem(X0)|memberP(nil,X0)|memberP(nil,X0))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f574,f393])).
% 0.13/0.52 fof(f1627,definition,(
% 0.13/0.52 ![X0,X1]: (sQ52_spl <=> (~memberP(skaf76(X0),X1)|~ssList(skaf76(X0))|~ssItem(X1)|memberP(nil,X1)|memberP(skaf76(X0),X1)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1630,plain,(
% 0.13/0.52 sQ52_spl|~sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1611,f1627,f609])).
% 0.13/0.52 fof(f1631,definition,(
% 0.13/0.52 ![X0,X1]: (sQ53_spl <=> (~memberP(skaf77(X0),X1)|~ssList(skaf77(X0))|~ssItem(X1)|memberP(nil,X1)|memberP(skaf77(X0),X1)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1634,plain,(
% 0.13/0.52 sQ53_spl|~sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1612,f1631,f609])).
% 0.13/0.52 fof(f1635,definition,(
% 0.13/0.52 ![X0]: (sQ54_spl <=> (~memberP(sk1,X0)|~ssItem(X0)|memberP(nil,X0)|memberP(sk1,X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1638,plain,(
% 0.13/0.52 sQ54_spl|~sQ13_spl|~sQ18_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1613,f1635,f609,f648])).
% 0.13/0.52 fof(f1643,definition,(
% 0.13/0.52 ![X0]: (sQ56_spl <=> (~memberP(sk2,X0)|~ssItem(X0)|memberP(nil,X0)|memberP(sk2,X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1646,plain,(
% 0.13/0.52 sQ56_spl|~sQ13_spl|~sQ19_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1615,f1643,f609,f652])).
% 0.13/0.52 fof(f1653,definition,(
% 0.13/0.52 ![X0,X1]: (sQ58_spl <=> (~memberP(skaf82(X0),X1)|~ssList(skaf82(X0))|~ssItem(X1)|memberP(skaf82(X0),X1)|memberP(nil,X1)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1656,plain,(
% 0.13/0.52 sQ58_spl|~sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1619,f1653,f609])).
% 0.13/0.52 fof(f1657,definition,(
% 0.13/0.52 ![X0,X1]: (sQ59_spl <=> (~memberP(skaf81(X0),X1)|~ssList(skaf81(X0))|~ssItem(X1)|memberP(skaf81(X0),X1)|memberP(nil,X1)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1660,plain,(
% 0.13/0.52 sQ59_spl|~sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1620,f1657,f609])).
% 0.13/0.52 fof(f1664,definition,(
% 0.13/0.52 ![X0]: (sQ60_spl <=> (~memberP(nil,X0)|~ssItem(X0)|memberP(nil,X0)|memberP(nil,X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1667,plain,(
% 0.13/0.52 sQ60_spl|~sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1624,f1664,f609])).
% 0.13/0.52 fof(f1673,plain,(
% 0.13/0.52 ![X0,X1]: (~memberP(skaf75(X0),X1)|~ssList(skaf75(X0))|~ssList(nil)|~ssItem(X1)|memberP(skaf75(X0),X1)|memberP(nil,X1))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f595,f393])).
% 0.13/0.52 fof(f1674,plain,(
% 0.13/0.52 ![X0]: (~ssList(skaf75(X0))|~ssList(nil)|ssList(skaf75(X0)))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f595,f293])).
% 0.13/0.52 fof(f1675,definition,(
% 0.13/0.52 ![X0,X1]: (sQ62_spl <=> (~memberP(skaf75(X0),X1)|~ssList(skaf75(X0))|~ssItem(X1)|memberP(skaf75(X0),X1)|memberP(nil,X1)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1678,plain,(
% 0.13/0.52 sQ62_spl|~sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1673,f1675,f609])).
% 0.13/0.52 fof(f1679,definition,(
% 0.13/0.52 ![X0]: (sQ63_spl <=> (~ssList(skaf75(X0))|ssList(skaf75(X0))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1682,plain,(
% 0.13/0.52 sQ63_spl|~sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1674,f1679,f609])).
% 0.13/0.53 fof(f1687,plain,(
% 0.13/0.53 ![X0,X1]: (~memberP(skaf73(X0),X1)|~ssList(skaf73(X0))|~ssList(nil)|~ssItem(X1)|memberP(skaf73(X0),X1)|memberP(nil,X1))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f597,f393])).
% 0.13/0.53 fof(f1688,plain,(
% 0.13/0.53 ![X0]: (~ssList(skaf73(X0))|~ssList(nil)|ssList(skaf73(X0)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f597,f293])).
% 0.13/0.53 fof(f1689,definition,(
% 0.13/0.53 ![X0,X1]: (sQ64_spl <=> (~memberP(skaf73(X0),X1)|~ssList(skaf73(X0))|~ssItem(X1)|memberP(skaf73(X0),X1)|memberP(nil,X1)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f1692,plain,(
% 0.13/0.53 sQ64_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f1687,f1689,f609])).
% 0.13/0.53 fof(f1693,definition,(
% 0.13/0.53 ![X0]: (sQ65_spl <=> (~ssList(skaf73(X0))|ssList(skaf73(X0))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f1696,plain,(
% 0.13/0.53 sQ65_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f1688,f1693,f609])).
% 0.13/0.53 fof(f1701,plain,(
% 0.13/0.53 ![X0,X1]: (~memberP(skaf72(X0),X1)|~ssList(skaf72(X0))|~ssList(nil)|~ssItem(X1)|memberP(skaf72(X0),X1)|memberP(nil,X1))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f599,f393])).
% 0.13/0.53 fof(f1702,plain,(
% 0.13/0.53 ![X0]: (~ssList(skaf72(X0))|~ssList(nil)|ssList(skaf72(X0)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f599,f293])).
% 0.13/0.53 fof(f1703,definition,(
% 0.13/0.53 ![X0,X1]: (sQ66_spl <=> (~memberP(skaf72(X0),X1)|~ssList(skaf72(X0))|~ssItem(X1)|memberP(skaf72(X0),X1)|memberP(nil,X1)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f1706,plain,(
% 0.13/0.53 sQ66_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f1701,f1703,f609])).
% 0.13/0.53 fof(f1707,definition,(
% 0.13/0.53 ![X0]: (sQ67_spl <=> (~ssList(skaf72(X0))|ssList(skaf72(X0))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f1710,plain,(
% 0.13/0.53 sQ67_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f1702,f1707,f609])).
% 0.13/0.53 fof(f1715,plain,(
% 0.13/0.53 ![X0,X1]: (~memberP(skaf71(X0),X1)|~ssList(skaf71(X0))|~ssList(nil)|~ssItem(X1)|memberP(skaf71(X0),X1)|memberP(nil,X1))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f601,f393])).
% 0.13/0.53 fof(f1716,plain,(
% 0.13/0.53 ![X0]: (~ssList(skaf71(X0))|~ssList(nil)|ssList(skaf71(X0)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f601,f293])).
% 0.13/0.53 fof(f1717,definition,(
% 0.13/0.53 ![X0,X1]: (sQ68_spl <=> (~memberP(skaf71(X0),X1)|~ssList(skaf71(X0))|~ssItem(X1)|memberP(skaf71(X0),X1)|memberP(nil,X1)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f1720,plain,(
% 0.13/0.53 sQ68_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f1715,f1717,f609])).
% 0.13/0.53 fof(f1721,definition,(
% 0.13/0.53 ![X0]: (sQ69_spl <=> (~ssList(skaf71(X0))|ssList(skaf71(X0))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f1724,plain,(
% 0.13/0.53 sQ69_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f1716,f1721,f609])).
% 0.13/0.53 fof(f1729,plain,(
% 0.13/0.53 ![X0,X1]: (~memberP(skaf68(X0),X1)|~ssList(skaf68(X0))|~ssList(nil)|~ssItem(X1)|memberP(skaf68(X0),X1)|memberP(nil,X1))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f603,f393])).
% 0.13/0.53 fof(f1730,plain,(
% 0.13/0.53 ![X0]: (~ssList(skaf68(X0))|~ssList(nil)|ssList(skaf68(X0)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f603,f293])).
% 0.13/0.53 fof(f1731,definition,(
% 0.13/0.53 ![X0,X1]: (sQ70_spl <=> (~memberP(skaf68(X0),X1)|~ssList(skaf68(X0))|~ssItem(X1)|memberP(skaf68(X0),X1)|memberP(nil,X1)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f1734,plain,(
% 0.13/0.53 sQ70_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f1729,f1731,f609])).
% 0.13/0.53 fof(f1735,definition,(
% 0.13/0.53 ![X0]: (sQ71_spl <=> (~ssList(skaf68(X0))|ssList(skaf68(X0))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f1738,plain,(
% 0.13/0.53 sQ71_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f1730,f1735,f609])).
% 0.13/0.53 fof(f1780,plain,(
% 0.13/0.53 ![X0,X1]: (~memberP(skaf67(X0),X1)|~ssList(skaf67(X0))|~ssList(nil)|~ssItem(X1)|memberP(skaf67(X0),X1)|memberP(nil,X1))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f605,f393])).
% 0.13/0.53 fof(f1781,plain,(
% 0.13/0.53 ![X0]: (~ssList(skaf67(X0))|~ssList(nil)|ssList(skaf67(X0)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f605,f293])).
% 0.13/0.53 fof(f1782,definition,(
% 0.13/0.53 ![X0,X1]: (sQ72_spl <=> (~memberP(skaf67(X0),X1)|~ssList(skaf67(X0))|~ssItem(X1)|memberP(skaf67(X0),X1)|memberP(nil,X1)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f1785,plain,(
% 0.13/0.53 sQ72_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f1780,f1782,f609])).
% 0.13/0.53 fof(f1786,definition,(
% 0.13/0.53 ![X0]: (sQ73_spl <=> (~ssList(skaf67(X0))|ssList(skaf67(X0))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f1789,plain,(
% 0.13/0.53 sQ73_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f1781,f1786,f609])).
% 0.13/0.53 fof(f1794,plain,(
% 0.13/0.53 ![X0,X1]: (~memberP(skaf80(X0),X1)|~ssList(skaf80(X0))|~ssList(nil)|~ssItem(X1)|memberP(skaf80(X0),X1)|memberP(nil,X1))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f583,f393])).
% 0.13/0.53 fof(f1796,definition,(
% 0.13/0.53 ![X0,X1]: (sQ74_spl <=> (~memberP(skaf80(X0),X1)|~ssList(skaf80(X0))|~ssItem(X1)|memberP(skaf80(X0),X1)|memberP(nil,X1)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f1799,plain,(
% 0.13/0.53 sQ74_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f1794,f1796,f609])).
% 0.13/0.53 fof(f2004,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(sk1)|segmentP(app(app(X1,sk1),X0),nil)|~sQ37_spl)),
% 0.13/0.53 inference(resolution,[status(thm)],[f412,f951])).
% 0.13/0.53 fof(f2005,plain,(
% 0.13/0.53 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2))),
% 0.13/0.53 inference(resolution,[status(thm)],[f412,f263])).
% 0.13/0.53 fof(f2007,definition,(
% 0.13/0.53 ![X0,X1]: (sQ76_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2010,plain,(
% 0.13/0.53 sQ76_spl|~sQ13_spl|~sQ18_spl|~sQ37_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2004,f2007,f609,f648,f950])).
% 0.13/0.53 fof(f2011,definition,(
% 0.13/0.53 ![X0,X1,X2]: (sQ77_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),nil)|~ssList(X2)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2014,plain,(
% 0.13/0.53 sQ77_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2005,f2011,f609])).
% 0.13/0.53 fof(f2202,plain,(
% 0.13/0.53 ~ssList(sk7)|~ssList(sk6)|~ssList(sk1)|~ssList(sk2)|segmentP(app(app(sk6,sk1),sk7),sk1)|~sQ10_spl),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f582,f537])).
% 0.13/0.53 fof(f2203,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(skaf82(X1))|~ssList(nil)|~ssList(app(skaf82(X1),X0))|segmentP(app(app(skaf82(X1),nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f577,f537])).
% 0.13/0.53 fof(f2204,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(skaf81(X1))|~ssList(nil)|~ssList(app(skaf81(X1),X0))|segmentP(app(app(skaf81(X1),nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f580,f537])).
% 0.13/0.53 fof(f2205,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(skaf80(X1))|~ssList(nil)|~ssList(app(skaf80(X1),X0))|segmentP(app(app(skaf80(X1),nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f581,f537])).
% 0.13/0.53 fof(f2206,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(skaf67(X1))|~ssList(nil)|~ssList(app(skaf67(X1),X0))|segmentP(app(app(skaf67(X1),nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f606,f537])).
% 0.13/0.53 fof(f2207,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(skaf68(X1))|~ssList(nil)|~ssList(app(skaf68(X1),X0))|segmentP(app(app(skaf68(X1),nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f604,f537])).
% 0.13/0.53 fof(f2208,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(skaf71(X1))|~ssList(nil)|~ssList(app(skaf71(X1),X0))|segmentP(app(app(skaf71(X1),nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f602,f537])).
% 0.13/0.53 fof(f2209,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(skaf72(X1))|~ssList(nil)|~ssList(app(skaf72(X1),X0))|segmentP(app(app(skaf72(X1),nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f600,f537])).
% 0.13/0.53 fof(f2210,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(skaf73(X1))|~ssList(nil)|~ssList(app(skaf73(X1),X0))|segmentP(app(app(skaf73(X1),nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f598,f537])).
% 0.13/0.53 fof(f2211,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(skaf75(X1))|~ssList(nil)|~ssList(app(skaf75(X1),X0))|segmentP(app(app(skaf75(X1),nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f596,f537])).
% 0.13/0.53 fof(f2212,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(skaf76(X1))|~ssList(nil)|~ssList(app(skaf76(X1),X0))|segmentP(app(app(skaf76(X1),nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f594,f537])).
% 0.13/0.53 fof(f2213,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(skaf77(X1))|~ssList(nil)|~ssList(app(skaf77(X1),X0))|segmentP(app(app(skaf77(X1),nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f592,f537])).
% 0.13/0.53 fof(f2214,plain,(
% 0.13/0.53 ![X0]: (~ssList(X0)|~ssList(sk1)|~ssList(nil)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f579,f537])).
% 0.13/0.53 fof(f2216,plain,(
% 0.13/0.53 ![X0]: (~ssList(X0)|~ssList(sk2)|~ssList(nil)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f578,f537])).
% 0.13/0.53 fof(f2218,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf80(X1))|~ssList(app(skaf80(X1),X0))|segmentP(app(app(nil,skaf80(X1)),X0),skaf80(X1)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f583,f537])).
% 0.13/0.53 fof(f2219,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf67(X1))|~ssList(app(skaf67(X1),X0))|segmentP(app(app(nil,skaf67(X1)),X0),skaf67(X1)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f605,f537])).
% 0.13/0.53 fof(f2220,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf68(X1))|~ssList(app(skaf68(X1),X0))|segmentP(app(app(nil,skaf68(X1)),X0),skaf68(X1)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f603,f537])).
% 0.13/0.53 fof(f2221,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf71(X1))|~ssList(app(skaf71(X1),X0))|segmentP(app(app(nil,skaf71(X1)),X0),skaf71(X1)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f601,f537])).
% 0.13/0.53 fof(f2222,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf72(X1))|~ssList(app(skaf72(X1),X0))|segmentP(app(app(nil,skaf72(X1)),X0),skaf72(X1)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f599,f537])).
% 0.13/0.53 fof(f2223,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf73(X1))|~ssList(app(skaf73(X1),X0))|segmentP(app(app(nil,skaf73(X1)),X0),skaf73(X1)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f597,f537])).
% 0.13/0.53 fof(f2224,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf75(X1))|~ssList(app(skaf75(X1),X0))|segmentP(app(app(nil,skaf75(X1)),X0),skaf75(X1)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f595,f537])).
% 0.13/0.53 fof(f2225,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf76(X1))|~ssList(app(skaf76(X1),X0))|segmentP(app(app(nil,skaf76(X1)),X0),skaf76(X1)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f593,f537])).
% 0.13/0.53 fof(f2226,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf77(X1))|~ssList(app(skaf77(X1),X0))|segmentP(app(app(nil,skaf77(X1)),X0),skaf77(X1)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f591,f537])).
% 0.13/0.53 fof(f2227,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf82(X1))|~ssList(app(skaf82(X1),X0))|segmentP(app(app(nil,skaf82(X1)),X0),skaf82(X1)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f588,f537])).
% 0.13/0.53 fof(f2228,plain,(
% 0.13/0.53 ![X0,X1]: (~ssList(X0)|~ssList(nil)|~ssList(skaf81(X1))|~ssList(app(skaf81(X1),X0))|segmentP(app(app(nil,skaf81(X1)),X0),skaf81(X1)))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f584,f537])).
% 0.13/0.53 fof(f2229,plain,(
% 0.13/0.53 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f590,f537])).
% 0.13/0.53 fof(f2230,plain,(
% 0.13/0.53 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f589,f537])).
% 0.13/0.53 fof(f2232,plain,(
% 0.13/0.53 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(nil)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil))),
% 0.13/0.53 inference(paramodulation,[status(thm)],[f574,f537])).
% 0.13/0.53 fof(f2237,definition,(
% 0.13/0.53 sQ78_spl <=> (segmentP(app(app(sk6,sk1),sk7),sk1))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2238,plain,(
% 0.13/0.53 segmentP(app(app(sk6,sk1),sk7),sk1)|~sQ78_spl),
% 0.13/0.53 inference(component_clause,[status(thm)],[f2237])).
% 0.13/0.53 fof(f2240,plain,(
% 0.13/0.53 ~sQ8_spl|~sQ7_spl|~sQ18_spl|~sQ19_spl|sQ78_spl|~sQ10_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2202,f493,f489,f648,f652,f2237,f501])).
% 0.13/0.53 fof(f2241,definition,(
% 0.13/0.53 ![X0,X1]: (sQ79_spl <=> (~ssList(X0)|~ssList(skaf82(X1))|~ssList(app(skaf82(X1),X0))|segmentP(app(app(skaf82(X1),nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2244,plain,(
% 0.13/0.53 sQ79_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2203,f2241,f609])).
% 0.13/0.53 fof(f2245,definition,(
% 0.13/0.53 ![X0,X1]: (sQ80_spl <=> (~ssList(X0)|~ssList(skaf81(X1))|~ssList(app(skaf81(X1),X0))|segmentP(app(app(skaf81(X1),nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2248,plain,(
% 0.13/0.53 sQ80_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2204,f2245,f609])).
% 0.13/0.53 fof(f2249,definition,(
% 0.13/0.53 ![X0,X1]: (sQ81_spl <=> (~ssList(X0)|~ssList(skaf80(X1))|~ssList(app(skaf80(X1),X0))|segmentP(app(app(skaf80(X1),nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2252,plain,(
% 0.13/0.53 sQ81_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2205,f2249,f609])).
% 0.13/0.53 fof(f2253,definition,(
% 0.13/0.53 ![X0,X1]: (sQ82_spl <=> (~ssList(X0)|~ssList(skaf67(X1))|~ssList(app(skaf67(X1),X0))|segmentP(app(app(skaf67(X1),nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2256,plain,(
% 0.13/0.53 sQ82_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2206,f2253,f609])).
% 0.13/0.53 fof(f2257,definition,(
% 0.13/0.53 ![X0,X1]: (sQ83_spl <=> (~ssList(X0)|~ssList(skaf68(X1))|~ssList(app(skaf68(X1),X0))|segmentP(app(app(skaf68(X1),nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2260,plain,(
% 0.13/0.53 sQ83_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2207,f2257,f609])).
% 0.13/0.53 fof(f2261,definition,(
% 0.13/0.53 ![X0,X1]: (sQ84_spl <=> (~ssList(X0)|~ssList(skaf71(X1))|~ssList(app(skaf71(X1),X0))|segmentP(app(app(skaf71(X1),nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2264,plain,(
% 0.13/0.53 sQ84_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2208,f2261,f609])).
% 0.13/0.53 fof(f2265,definition,(
% 0.13/0.53 ![X0,X1]: (sQ85_spl <=> (~ssList(X0)|~ssList(skaf72(X1))|~ssList(app(skaf72(X1),X0))|segmentP(app(app(skaf72(X1),nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2268,plain,(
% 0.13/0.53 sQ85_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2209,f2265,f609])).
% 0.13/0.53 fof(f2269,definition,(
% 0.13/0.53 ![X0,X1]: (sQ86_spl <=> (~ssList(X0)|~ssList(skaf73(X1))|~ssList(app(skaf73(X1),X0))|segmentP(app(app(skaf73(X1),nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2272,plain,(
% 0.13/0.53 sQ86_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2210,f2269,f609])).
% 0.13/0.53 fof(f2273,definition,(
% 0.13/0.53 ![X0,X1]: (sQ87_spl <=> (~ssList(X0)|~ssList(skaf75(X1))|~ssList(app(skaf75(X1),X0))|segmentP(app(app(skaf75(X1),nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2276,plain,(
% 0.13/0.53 sQ87_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2211,f2273,f609])).
% 0.13/0.53 fof(f2277,definition,(
% 0.13/0.53 ![X0,X1]: (sQ88_spl <=> (~ssList(X0)|~ssList(skaf76(X1))|~ssList(app(skaf76(X1),X0))|segmentP(app(app(skaf76(X1),nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2280,plain,(
% 0.13/0.53 sQ88_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2212,f2277,f609])).
% 0.13/0.53 fof(f2281,definition,(
% 0.13/0.53 ![X0,X1]: (sQ89_spl <=> (~ssList(X0)|~ssList(skaf77(X1))|~ssList(app(skaf77(X1),X0))|segmentP(app(app(skaf77(X1),nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2284,plain,(
% 0.13/0.53 sQ89_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2213,f2281,f609])).
% 0.13/0.53 fof(f2285,definition,(
% 0.13/0.53 ![X0]: (sQ90_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(sk1,nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2288,plain,(
% 0.13/0.53 sQ90_spl|~sQ18_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2214,f2285,f648,f609])).
% 0.13/0.53 fof(f2293,definition,(
% 0.13/0.53 ![X0]: (sQ92_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(sk2,nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2296,plain,(
% 0.13/0.53 sQ92_spl|~sQ19_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2216,f2293,f652,f609])).
% 0.13/0.53 fof(f2301,definition,(
% 0.13/0.53 ![X0,X1]: (sQ94_spl <=> (~ssList(X0)|~ssList(skaf80(X1))|~ssList(app(skaf80(X1),X0))|segmentP(app(app(nil,skaf80(X1)),X0),skaf80(X1))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2304,plain,(
% 0.13/0.53 sQ94_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2218,f2301,f609])).
% 0.13/0.53 fof(f2305,definition,(
% 0.13/0.53 ![X0,X1]: (sQ95_spl <=> (~ssList(X0)|~ssList(skaf67(X1))|~ssList(app(skaf67(X1),X0))|segmentP(app(app(nil,skaf67(X1)),X0),skaf67(X1))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2308,plain,(
% 0.13/0.53 sQ95_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2219,f2305,f609])).
% 0.13/0.53 fof(f2309,definition,(
% 0.13/0.53 ![X0,X1]: (sQ96_spl <=> (~ssList(X0)|~ssList(skaf68(X1))|~ssList(app(skaf68(X1),X0))|segmentP(app(app(nil,skaf68(X1)),X0),skaf68(X1))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2312,plain,(
% 0.13/0.53 sQ96_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2220,f2309,f609])).
% 0.13/0.53 fof(f2313,definition,(
% 0.13/0.53 ![X0,X1]: (sQ97_spl <=> (~ssList(X0)|~ssList(skaf71(X1))|~ssList(app(skaf71(X1),X0))|segmentP(app(app(nil,skaf71(X1)),X0),skaf71(X1))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2316,plain,(
% 0.13/0.53 sQ97_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2221,f2313,f609])).
% 0.13/0.53 fof(f2317,definition,(
% 0.13/0.53 ![X0,X1]: (sQ98_spl <=> (~ssList(X0)|~ssList(skaf72(X1))|~ssList(app(skaf72(X1),X0))|segmentP(app(app(nil,skaf72(X1)),X0),skaf72(X1))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2320,plain,(
% 0.13/0.53 sQ98_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2222,f2317,f609])).
% 0.13/0.53 fof(f2321,definition,(
% 0.13/0.53 ![X0,X1]: (sQ99_spl <=> (~ssList(X0)|~ssList(skaf73(X1))|~ssList(app(skaf73(X1),X0))|segmentP(app(app(nil,skaf73(X1)),X0),skaf73(X1))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2324,plain,(
% 0.13/0.53 sQ99_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2223,f2321,f609])).
% 0.13/0.53 fof(f2325,definition,(
% 0.13/0.53 ![X0,X1]: (sQ100_spl <=> (~ssList(X0)|~ssList(skaf75(X1))|~ssList(app(skaf75(X1),X0))|segmentP(app(app(nil,skaf75(X1)),X0),skaf75(X1))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2328,plain,(
% 0.13/0.53 sQ100_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2224,f2325,f609])).
% 0.13/0.53 fof(f2329,definition,(
% 0.13/0.53 ![X0,X1]: (sQ101_spl <=> (~ssList(X0)|~ssList(skaf76(X1))|~ssList(app(skaf76(X1),X0))|segmentP(app(app(nil,skaf76(X1)),X0),skaf76(X1))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2332,plain,(
% 0.13/0.53 sQ101_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2225,f2329,f609])).
% 0.13/0.53 fof(f2333,definition,(
% 0.13/0.53 ![X0,X1]: (sQ102_spl <=> (~ssList(X0)|~ssList(skaf77(X1))|~ssList(app(skaf77(X1),X0))|segmentP(app(app(nil,skaf77(X1)),X0),skaf77(X1))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2336,plain,(
% 0.13/0.53 sQ102_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2226,f2333,f609])).
% 0.13/0.53 fof(f2337,definition,(
% 0.13/0.53 ![X0,X1]: (sQ103_spl <=> (~ssList(X0)|~ssList(skaf82(X1))|~ssList(app(skaf82(X1),X0))|segmentP(app(app(nil,skaf82(X1)),X0),skaf82(X1))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2340,plain,(
% 0.13/0.53 sQ103_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2227,f2337,f609])).
% 0.13/0.53 fof(f2341,definition,(
% 0.13/0.53 ![X0,X1]: (sQ104_spl <=> (~ssList(X0)|~ssList(skaf81(X1))|~ssList(app(skaf81(X1),X0))|segmentP(app(app(nil,skaf81(X1)),X0),skaf81(X1))))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2344,plain,(
% 0.13/0.53 sQ104_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2228,f2341,f609])).
% 0.13/0.53 fof(f2345,definition,(
% 0.13/0.53 ![X0]: (sQ105_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2348,plain,(
% 0.13/0.53 sQ105_spl|~sQ13_spl|~sQ18_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2229,f2345,f609,f648])).
% 0.13/0.53 fof(f2349,definition,(
% 0.13/0.53 ![X0]: (sQ106_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2352,plain,(
% 0.13/0.53 sQ106_spl|~sQ13_spl|~sQ19_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2230,f2349,f609,f652])).
% 0.13/0.53 fof(f2357,definition,(
% 0.13/0.53 ![X0]: (sQ108_spl <=> (~ssList(X0)|~ssList(app(nil,X0))|segmentP(app(app(nil,nil),X0),nil)))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2360,plain,(
% 0.13/0.53 sQ108_spl|~sQ13_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2232,f2357,f609])).
% 0.13/0.53 fof(f2411,plain,(
% 0.13/0.53 segmentP(sk2,sk1)|~sQ10_spl|~sQ78_spl),
% 0.13/0.53 inference(forward_demodulation,[status(thm)],[f582,f2238])).
% 0.13/0.53 fof(f2422,plain,(
% 0.13/0.53 ~ssList(sk1)|~neq(sk1,nil)|~segmentP(sk1,sk1)|~sQ10_spl|~sQ78_spl),
% 0.13/0.53 inference(resolution,[status(thm)],[f2411,f444])).
% 0.13/0.53 fof(f2426,definition,(
% 0.13/0.53 sQ112_spl <=> (segmentP(sk1,sk1))),
% 0.13/0.53 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.13/0.53 fof(f2428,plain,(
% 0.13/0.53 ~segmentP(sk1,sk1)|sQ112_spl),
% 0.13/0.53 inference(component_clause,[status(thm)],[f2426])).
% 0.13/0.53 fof(f2429,plain,(
% 0.13/0.53 ~sQ18_spl|~sQ29_spl|~sQ112_spl|~sQ10_spl|~sQ78_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2422,f648,f857,f2426,f501,f2237])).
% 0.13/0.53 fof(f2439,plain,(
% 0.13/0.53 ~ssList(sk1)|sQ112_spl),
% 0.13/0.53 inference(resolution,[status(thm)],[f2428,f264])).
% 0.13/0.53 fof(f2440,plain,(
% 0.13/0.53 ~sQ18_spl|sQ112_spl),
% 0.13/0.53 inference(split_clause,[status(thm)],[f2439,f648,f2426])).
% 0.13/0.53 fof(f2441,plain,(
% 0.13/0.53 $false),
% 0.13/0.53 inference(sat_refutation,[status(thm)],[f477,f484,f492,f496,f500,f504,f513,f514,f516,f571,f615,f618,f639,f643,f647,f665,f705,f712,f716,f719,f767,f779,f784,f860,f870,f872,f953,f957,f964,f969,f1491,f1495,f1582,f1589,f1630,f1634,f1638,f1646,f1656,f1660,f1667,f1678,f1682,f1692,f1696,f1706,f1710,f1720,f1724,f1734,f1738,f1785,f1789,f1799,f2010,f2014,f2240,f2244,f2248,f2252,f2256,f2260,f2264,f2268,f2272,f2276,f2280,f2284,f2288,f2296,f2304,f2308,f2312,f2316,f2320,f2324,f2328,f2332,f2336,f2340,f2344,f2348,f2352,f2360,f2429,f2440])).
% 0.13/0.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.20/0.55 % Elapsed time: 0.169156 seconds
% 0.20/0.55 % CPU time: 0.931092 seconds
% 0.20/0.55 % Total memory used: 128.320 MB
% 0.20/0.55 % Net memory used: 127.421 MB
%------------------------------------------------------------------------------