%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC198-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 : n004.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:50 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC198-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.34 % Computer : n004.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 08:04:19 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 0.13/0.38 % Refutation found
% 0.13/0.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.38 fof(f8,axiom,(
% 0.13/0.38 ssList(nil) ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f9,axiom,(
% 0.13/0.38 ssItem(skac3) ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f10,axiom,(
% 0.13/0.38 ssItem(skac2) ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f12,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf83(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f16,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf79(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f17,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf78(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f21,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf74(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f25,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf70(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f26,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf69(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f30,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf65(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f31,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf64(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f35,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf60(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f36,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf59(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f40,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf55(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f41,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf54(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f45,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf50(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f46,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf49(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f47,axiom,(
% 0.13/0.38 (![U]: (ssItem(skaf44(U)) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f56,axiom,(
% 0.13/0.38 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f62,axiom,(
% 0.13/0.38 (![U]: (( ~ ssItem(U)| leq(U,U) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f71,axiom,(
% 0.13/0.38 (![U]: (( ~ memberP(nil,U)| ~ ssItem(U) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f73,axiom,(
% 0.13/0.38 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f80,axiom,(
% 0.13/0.38 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f130,axiom,(
% 0.13/0.38 (![U,V]: (( ~ leq(U,V)| ~ leq(V,U)| ~ ssItem(U)| ~ ssItem(V)| V = U ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f139,axiom,(
% 0.13/0.38 (![U,V,W]: (( ~ memberP(U,V)| ~ ssList(U)| ~ ssItem(W)| ~ ssItem(V)| memberP(cons(W,U),V) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f140,axiom,(
% 0.13/0.38 (![U,V,W]: (( ~ memberP(U,V)| ~ ssList(W)| ~ ssList(U)| ~ ssItem(V)| memberP(app(U,W),V) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f141,axiom,(
% 0.13/0.38 (![U,V,W]: (( ~ memberP(U,V)| ~ ssList(U)| ~ ssList(W)| ~ ssItem(V)| memberP(app(W,U),V) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f156,axiom,(
% 0.13/0.38 (![U,V,W]: (( ~ leq(U,V)| ~ leq(V,W)| ~ ssItem(W)| ~ ssItem(V)| ~ ssItem(U)| leq(U,W) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f158,axiom,(
% 0.13/0.38 (![U,V,W]: (( ~ memberP(app(U,V),W)| ~ ssList(V)| ~ ssList(U)| ~ ssItem(W)| memberP(V,W)| memberP(U,W) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f161,axiom,(
% 0.13/0.38 (![U,V,W]: (( ~ memberP(cons(U,V),W)| ~ ssList(V)| ~ ssItem(U)| ~ ssItem(W)| memberP(V,W)| W = U ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f171,axiom,(
% 0.13/0.38 (![U,V,W,X]: (( cons(U,V) != cons(W,X)| ~ ssItem(W)| ~ ssItem(U)| ~ ssList(X)| ~ ssList(V)| X = V ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f188,negated_conjecture,(
% 0.13/0.38 ssList(sk3) ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f189,negated_conjecture,(
% 0.13/0.38 ssList(sk4) ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f191,negated_conjecture,(
% 0.13/0.38 sk1 = sk3 ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f192,negated_conjecture,(
% 0.13/0.38 (![A]: (( ~ ssItem(A)| ssItem(sk5(A)) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f193,negated_conjecture,(
% 0.13/0.38 (![A]: (( ~ ssItem(A)| memberP(sk1,sk5(A)) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f194,negated_conjecture,(
% 0.13/0.38 (![A]: (( ~ ssItem(A)| A != sk5(A) ) ))),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f195,negated_conjecture,(
% 0.13/0.38 ( ssItem(sk6)| nil = sk4 ) ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f196,negated_conjecture,(
% 0.13/0.38 ( ssItem(sk6)| nil = sk3 ) ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f197,negated_conjecture,(
% 0.13/0.38 ( cons(sk6,nil) = sk3| nil = sk4 ) ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f200,negated_conjecture,(
% 0.13/0.38 ( cons(sk6,nil) = sk3| nil = sk3 ) ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f210,plain,(
% 0.13/0.38 ssList(nil)),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.38 fof(f211,plain,(
% 0.13/0.38 ssItem(skac3)),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/0.38 fof(f212,plain,(
% 0.13/0.38 ssItem(skac2)),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.38 fof(f214,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf83(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/0.38 fof(f218,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf79(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f16])).
% 0.13/0.38 fof(f219,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf78(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.38 fof(f223,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf74(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f21])).
% 0.13/0.38 fof(f227,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf70(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/0.38 fof(f228,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf69(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f26])).
% 0.13/0.38 fof(f232,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf65(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f30])).
% 0.13/0.38 fof(f233,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf64(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f31])).
% 0.13/0.38 fof(f237,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf60(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f35])).
% 0.13/0.38 fof(f238,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf59(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f36])).
% 0.13/0.38 fof(f242,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf55(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f40])).
% 0.13/0.38 fof(f243,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf54(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f41])).
% 0.13/0.38 fof(f247,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf50(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f45])).
% 0.13/0.38 fof(f248,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf49(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f46])).
% 0.13/0.38 fof(f249,plain,(
% 0.13/0.38 ![X0]: (ssItem(skaf44(X0)))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f47])).
% 0.13/0.38 fof(f258,plain,(
% 0.13/0.38 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f56])).
% 0.13/0.38 fof(f264,plain,(
% 0.13/0.38 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/0.38 fof(f273,plain,(
% 0.13/0.38 ![X0]: (~memberP(nil,X0)|~ssItem(X0))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f71])).
% 0.13/0.38 fof(f276,plain,(
% 0.13/0.38 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f73])).
% 0.13/0.38 fof(f283,plain,(
% 0.13/0.38 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f80])).
% 0.13/0.38 fof(f345,plain,(
% 0.13/0.38 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|~ssItem(X0)|~ssItem(X1)|X1=X0)),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f130])).
% 0.13/0.38 fof(f356,plain,(
% 0.13/0.38 ![X0,X1,X2]: (~memberP(X0,X1)|~ssList(X0)|~ssItem(X2)|~ssItem(X1)|memberP(cons(X2,X0),X1))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f139])).
% 0.13/0.38 fof(f357,plain,(
% 0.13/0.38 ![X0,X1,X2]: (~memberP(X0,X1)|~ssList(X2)|~ssList(X0)|~ssItem(X1)|memberP(app(X0,X2),X1))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f140])).
% 0.13/0.38 fof(f358,plain,(
% 0.13/0.38 ![X0,X1,X2]: (~memberP(X0,X1)|~ssList(X0)|~ssList(X2)|~ssItem(X1)|memberP(app(X2,X0),X1))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f141])).
% 0.13/0.38 fof(f384,plain,(
% 0.13/0.38 ![U,W]: (((![V]: (((~leq(U,V)|~leq(V,W))|~ssItem(W))|~ssItem(V)))|~ssItem(U))|leq(U,W))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f156])).
% 0.13/0.38 fof(f385,plain,(
% 0.13/0.38 ![X0,X1,X2]: (~leq(X0,X1)|~leq(X1,X2)|~ssItem(X2)|~ssItem(X1)|~ssItem(X0)|leq(X0,X2))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f384])).
% 0.13/0.38 fof(f387,plain,(
% 0.13/0.38 ![U,W]: ((![V]: ((((~memberP(app(U,V),W)|~ssList(V))|~ssList(U))|~ssItem(W))|memberP(V,W)))|memberP(U,W))),
% 0.13/0.38 inference(miniscoping,[status(thm)],[f158])).
% 0.13/0.38 fof(f388,plain,(
% 0.13/0.38 ![X0,X1,X2]: (~memberP(app(X0,X1),X2)|~ssList(X1)|~ssList(X0)|~ssItem(X2)|memberP(X1,X2)|memberP(X0,X2))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f387])).
% 0.13/0.38 fof(f393,plain,(
% 0.13/0.38 ![U,W]: ((![V]: ((((~memberP(cons(U,V),W)|~ssList(V))|~ssItem(U))|~ssItem(W))|memberP(V,W)))|W=U)),
% 0.13/0.39 inference(miniscoping,[status(thm)],[f161])).
% 0.13/0.39 fof(f394,plain,(
% 0.13/0.39 ![X0,X1,X2]: (~memberP(cons(X0,X1),X2)|~ssList(X1)|~ssItem(X0)|~ssItem(X2)|memberP(X1,X2)|X2=X0)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f393])).
% 0.13/0.39 fof(f405,plain,(
% 0.13/0.39 ![V,X]: ((((![U]: ((![W]: (~cons(U,V)=cons(W,X)|~ssItem(W)))|~ssItem(U)))|~ssList(X))|~ssList(V))|X=V)),
% 0.13/0.39 inference(miniscoping,[status(thm)],[f171])).
% 0.13/0.39 fof(f406,plain,(
% 0.13/0.39 ![X0,X1,X2,X3]: (~cons(X0,X1)=cons(X2,X3)|~ssItem(X2)|~ssItem(X0)|~ssList(X3)|~ssList(X1)|X3=X1)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f405])).
% 0.13/0.39 fof(f435,plain,(
% 0.13/0.39 ssList(sk3)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f188])).
% 0.13/0.39 fof(f436,plain,(
% 0.13/0.39 ssList(sk4)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f189])).
% 0.13/0.39 fof(f438,plain,(
% 0.13/0.39 sk1=sk3),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f191])).
% 0.13/0.39 fof(f439,plain,(
% 0.13/0.39 ![X0]: (~ssItem(X0)|ssItem(sk5(X0)))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f192])).
% 0.13/0.39 fof(f440,plain,(
% 0.13/0.39 ![X0]: (~ssItem(X0)|memberP(sk1,sk5(X0)))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f193])).
% 0.13/0.39 fof(f441,plain,(
% 0.13/0.39 ![X0]: (~ssItem(X0)|~X0=sk5(X0))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f194])).
% 0.13/0.39 fof(f442,plain,(
% 0.13/0.39 ssItem(sk6)|nil=sk4),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f195])).
% 0.13/0.39 fof(f443,plain,(
% 0.13/0.39 ssItem(sk6)|nil=sk3),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f196])).
% 0.13/0.39 fof(f444,plain,(
% 0.13/0.39 cons(sk6,nil)=sk3|nil=sk4),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f197])).
% 0.13/0.39 fof(f448,plain,(
% 0.13/0.39 cons(sk6,nil)=sk3|nil=sk3),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f200])).
% 0.13/0.39 fof(f459,definition,(
% 0.13/0.39 sQ2_spl <=> (ssItem(sk6))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f460,plain,(
% 0.13/0.39 ssItem(sk6)|~sQ2_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f459])).
% 0.13/0.39 fof(f462,definition,(
% 0.13/0.39 sQ3_spl <=> (nil=sk4)),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f463,plain,(
% 0.13/0.39 nil=sk4|~sQ3_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f462])).
% 0.13/0.39 fof(f465,plain,(
% 0.13/0.39 sQ2_spl|sQ3_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f442,f459,f462])).
% 0.13/0.39 fof(f466,definition,(
% 0.13/0.39 sQ4_spl <=> (nil=sk3)),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f467,plain,(
% 0.13/0.39 nil=sk3|~sQ4_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f466])).
% 0.13/0.39 fof(f469,plain,(
% 0.13/0.39 sQ2_spl|sQ4_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f443,f459,f466])).
% 0.13/0.39 fof(f470,definition,(
% 0.13/0.39 sQ5_spl <=> (cons(sk6,nil)=sk3)),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f471,plain,(
% 0.13/0.39 cons(sk6,nil)=sk3|~sQ5_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f470])).
% 0.13/0.39 fof(f473,plain,(
% 0.13/0.39 sQ5_spl|sQ3_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f444,f470,f462])).
% 0.13/0.39 fof(f482,plain,(
% 0.13/0.39 sQ5_spl|sQ4_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f448,f470,f466])).
% 0.13/0.39 fof(f517,plain,(
% 0.13/0.39 sk4=sk3|~sQ3_spl|~sQ4_spl),
% 0.13/0.39 inference(backward_demodulation,[status(thm)],[f463,f467])).
% 0.13/0.39 fof(f518,plain,(
% 0.13/0.39 sk1=sk4|~sQ3_spl|~sQ4_spl),
% 0.13/0.39 inference(backward_demodulation,[status(thm)],[f517,f438])).
% 0.13/0.39 fof(f520,plain,(
% 0.13/0.39 ![X0]: (~memberP(sk4,X0)|~ssItem(X0)|~sQ3_spl)),
% 0.13/0.39 inference(forward_demodulation,[status(thm)],[f463,f273])).
% 0.13/0.39 fof(f521,plain,(
% 0.13/0.39 ![X0]: (~ssItem(X0)|memberP(sk4,sk5(X0))|~sQ3_spl|~sQ4_spl)),
% 0.13/0.39 inference(forward_demodulation,[status(thm)],[f518,f440])).
% 0.13/0.39 fof(f531,plain,(
% 0.13/0.39 memberP(sk4,sk5(skac3))|~sQ3_spl|~sQ4_spl),
% 0.13/0.39 inference(resolution,[status(thm)],[f211,f521])).
% 0.13/0.39 fof(f532,plain,(
% 0.13/0.39 ssItem(sk5(skac3))),
% 0.13/0.39 inference(resolution,[status(thm)],[f211,f439])).
% 0.13/0.39 fof(f533,plain,(
% 0.13/0.39 leq(skac3,skac3)),
% 0.13/0.39 inference(resolution,[status(thm)],[f211,f264])).
% 0.13/0.39 fof(f536,plain,(
% 0.13/0.39 ssItem(sk5(skac2))),
% 0.13/0.39 inference(resolution,[status(thm)],[f212,f439])).
% 0.13/0.39 fof(f537,plain,(
% 0.13/0.39 leq(skac2,skac2)),
% 0.13/0.39 inference(resolution,[status(thm)],[f212,f264])).
% 0.13/0.39 fof(f571,plain,(
% 0.13/0.39 ~ssItem(sk5(skac3))|~sQ4_spl|~sQ3_spl),
% 0.13/0.39 inference(resolution,[status(thm)],[f531,f520])).
% 0.13/0.39 fof(f572,plain,(
% 0.13/0.39 $false|~sQ4_spl|~sQ3_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f571,f532])).
% 0.13/0.39 fof(f573,plain,(
% 0.13/0.39 ~sQ4_spl|~sQ3_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f572])).
% 0.13/0.39 fof(f575,plain,(
% 0.13/0.39 ssItem(sk5(sk6))|~sQ2_spl),
% 0.13/0.39 inference(resolution,[status(thm)],[f460,f439])).
% 0.13/0.39 fof(f581,plain,(
% 0.13/0.39 ~leq(skac2,skac2)|~ssItem(skac2)|~ssItem(skac2)|skac2=skac2),
% 0.13/0.39 inference(resolution,[status(thm)],[f345,f537])).
% 0.13/0.39 fof(f582,plain,(
% 0.13/0.39 ~leq(skac3,skac3)|~ssItem(skac3)|~ssItem(skac3)|skac3=skac3),
% 0.13/0.39 inference(resolution,[status(thm)],[f345,f533])).
% 0.13/0.39 fof(f590,definition,(
% 0.13/0.39 sQ10_spl <=> (leq(skac2,skac2))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f592,plain,(
% 0.13/0.39 ~leq(skac2,skac2)|sQ10_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f590])).
% 0.13/0.39 fof(f593,definition,(
% 0.13/0.39 sQ11_spl <=> (ssItem(skac2))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f595,plain,(
% 0.13/0.39 ~ssItem(skac2)|sQ11_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f593])).
% 0.13/0.39 fof(f596,definition,(
% 0.13/0.39 sQ12_spl <=> (skac2=skac2)),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f599,plain,(
% 0.13/0.39 ~sQ10_spl|~sQ11_spl|sQ12_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f581,f590,f593,f596])).
% 0.13/0.39 fof(f600,definition,(
% 0.13/0.39 sQ13_spl <=> (leq(skac3,skac3))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f602,plain,(
% 0.13/0.39 ~leq(skac3,skac3)|sQ13_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f600])).
% 0.13/0.39 fof(f603,definition,(
% 0.13/0.39 sQ14_spl <=> (ssItem(skac3))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f605,plain,(
% 0.13/0.39 ~ssItem(skac3)|sQ14_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f603])).
% 0.13/0.39 fof(f606,definition,(
% 0.13/0.39 sQ15_spl <=> (skac3=skac3)),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f609,plain,(
% 0.13/0.39 ~sQ13_spl|~sQ14_spl|sQ15_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f582,f600,f603,f606])).
% 0.13/0.39 fof(f612,plain,(
% 0.13/0.39 $false|sQ14_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f605,f211])).
% 0.13/0.39 fof(f613,plain,(
% 0.13/0.39 sQ14_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f612])).
% 0.13/0.39 fof(f614,plain,(
% 0.13/0.39 $false|sQ13_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f602,f533])).
% 0.13/0.39 fof(f615,plain,(
% 0.13/0.39 sQ13_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f614])).
% 0.13/0.39 fof(f634,definition,(
% 0.13/0.39 sQ17_spl <=> (ssList(sk4))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f636,plain,(
% 0.13/0.39 ~ssList(sk4)|sQ17_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f634])).
% 0.13/0.39 fof(f638,plain,(
% 0.13/0.39 $false|sQ17_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f636,f436])).
% 0.13/0.39 fof(f639,plain,(
% 0.13/0.39 sQ17_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f638])).
% 0.13/0.39 fof(f770,plain,(
% 0.13/0.39 ![X0]: (~ssItem(X0)|memberP(sk3,sk5(X0)))),
% 0.13/0.39 inference(forward_demodulation,[status(thm)],[f438,f440])).
% 0.13/0.39 fof(f771,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf44(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f249])).
% 0.13/0.39 fof(f772,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf49(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f248])).
% 0.13/0.39 fof(f773,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf50(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f247])).
% 0.13/0.39 fof(f774,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf54(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f243])).
% 0.13/0.39 fof(f775,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf55(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f242])).
% 0.13/0.39 fof(f776,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf59(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f238])).
% 0.13/0.39 fof(f777,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf60(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f237])).
% 0.13/0.39 fof(f778,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf64(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f233])).
% 0.13/0.39 fof(f779,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf65(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f232])).
% 0.13/0.39 fof(f780,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf69(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f228])).
% 0.13/0.39 fof(f781,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf70(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f227])).
% 0.13/0.39 fof(f782,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf74(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f223])).
% 0.13/0.39 fof(f783,plain,(
% 0.13/0.39 memberP(sk3,sk5(sk6))|~sQ2_spl),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f460])).
% 0.13/0.39 fof(f805,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf78(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f219])).
% 0.13/0.39 fof(f806,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf79(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f218])).
% 0.13/0.39 fof(f807,plain,(
% 0.13/0.39 ![X0]: (memberP(sk3,sk5(skaf83(X0))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f214])).
% 0.13/0.39 fof(f808,plain,(
% 0.13/0.39 memberP(sk3,sk5(skac2))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f212])).
% 0.13/0.39 fof(f809,plain,(
% 0.13/0.39 memberP(sk3,sk5(skac3))),
% 0.13/0.39 inference(resolution,[status(thm)],[f770,f211])).
% 0.13/0.39 fof(f816,definition,(
% 0.13/0.39 sQ21_spl <=> (ssList(nil))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f818,plain,(
% 0.13/0.39 ~ssList(nil)|sQ21_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f816])).
% 0.13/0.39 fof(f820,plain,(
% 0.13/0.39 $false|sQ21_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f818,f210])).
% 0.13/0.39 fof(f821,plain,(
% 0.13/0.39 sQ21_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f820])).
% 0.13/0.39 fof(f837,plain,(
% 0.13/0.39 ![X0]: (~leq(X0,skac2)|~ssItem(skac2)|~ssItem(skac2)|~ssItem(X0)|leq(X0,skac2))),
% 0.13/0.39 inference(resolution,[status(thm)],[f385,f537])).
% 0.13/0.39 fof(f838,plain,(
% 0.13/0.39 ![X0]: (~leq(X0,skac3)|~ssItem(skac3)|~ssItem(skac3)|~ssItem(X0)|leq(X0,skac3))),
% 0.13/0.39 inference(resolution,[status(thm)],[f385,f533])).
% 0.13/0.39 fof(f846,definition,(
% 0.13/0.39 ![X0]: (sQ23_spl <=> (~leq(X0,skac2)|~ssItem(X0)|leq(X0,skac2)))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f849,plain,(
% 0.13/0.39 sQ23_spl|~sQ11_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f837,f846,f593])).
% 0.13/0.39 fof(f850,definition,(
% 0.13/0.39 ![X0]: (sQ24_spl <=> (~leq(X0,skac3)|~ssItem(X0)|leq(X0,skac3)))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f853,plain,(
% 0.13/0.39 sQ24_spl|~sQ14_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f838,f850,f603])).
% 0.13/0.39 fof(f857,plain,(
% 0.13/0.39 $false|sQ11_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f595,f212])).
% 0.13/0.39 fof(f858,plain,(
% 0.13/0.39 sQ11_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f857])).
% 0.13/0.39 fof(f859,plain,(
% 0.13/0.39 $false|sQ10_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f592,f537])).
% 0.13/0.39 fof(f860,plain,(
% 0.13/0.39 sQ10_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f859])).
% 0.13/0.39 fof(f943,plain,(
% 0.13/0.39 segmentP(nil,nil)),
% 0.13/0.39 inference(resolution,[status(thm)],[f258,f210])).
% 0.13/0.39 fof(f1011,definition,(
% 0.13/0.39 sQ26_spl <=> (ssList(sk3))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1013,plain,(
% 0.13/0.39 ~ssList(sk3)|sQ26_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f1011])).
% 0.13/0.39 fof(f1017,definition,(
% 0.13/0.39 sQ28_spl <=> (ssItem(sk5(sk6)))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1019,plain,(
% 0.13/0.39 ~ssItem(sk5(sk6))|sQ28_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f1017])).
% 0.13/0.39 fof(f1029,plain,(
% 0.13/0.39 $false|~sQ2_spl|sQ28_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1019,f575])).
% 0.13/0.39 fof(f1030,plain,(
% 0.13/0.39 ~sQ2_spl|sQ28_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f1029])).
% 0.13/0.39 fof(f1031,plain,(
% 0.13/0.39 $false|sQ26_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1013,f435])).
% 0.13/0.39 fof(f1032,plain,(
% 0.13/0.39 sQ26_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f1031])).
% 0.13/0.39 fof(f1033,plain,(
% 0.13/0.39 ![X0]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skac2))|memberP(app(X0,sk3),sk5(skac2)))),
% 0.13/0.39 inference(resolution,[status(thm)],[f808,f358])).
% 0.13/0.39 fof(f1034,plain,(
% 0.13/0.39 ![X0]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skac2))|memberP(app(sk3,X0),sk5(skac2)))),
% 0.13/0.39 inference(resolution,[status(thm)],[f808,f357])).
% 0.13/0.39 fof(f1035,plain,(
% 0.13/0.39 ![X0]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skac2))|memberP(cons(X0,sk3),sk5(skac2)))),
% 0.13/0.39 inference(resolution,[status(thm)],[f808,f356])).
% 0.13/0.39 fof(f1036,definition,(
% 0.13/0.39 ![X0]: (sQ31_spl <=> (~ssList(X0)|memberP(app(X0,sk3),sk5(skac2))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1039,definition,(
% 0.13/0.39 sQ32_spl <=> (ssItem(sk5(skac2)))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1041,plain,(
% 0.13/0.39 ~ssItem(sk5(skac2))|sQ32_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f1039])).
% 0.13/0.39 fof(f1042,plain,(
% 0.13/0.39 ~sQ26_spl|sQ31_spl|~sQ32_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f1033,f1011,f1036,f1039])).
% 0.13/0.39 fof(f1043,definition,(
% 0.13/0.39 ![X0]: (sQ33_spl <=> (~ssList(X0)|memberP(app(sk3,X0),sk5(skac2))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1046,plain,(
% 0.13/0.39 sQ33_spl|~sQ26_spl|~sQ32_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f1034,f1043,f1011,f1039])).
% 0.13/0.39 fof(f1047,definition,(
% 0.13/0.39 ![X0]: (sQ34_spl <=> (~ssItem(X0)|memberP(cons(X0,sk3),sk5(skac2))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1050,plain,(
% 0.13/0.39 ~sQ26_spl|sQ34_spl|~sQ32_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f1035,f1011,f1047,f1039])).
% 0.13/0.39 fof(f1051,plain,(
% 0.13/0.39 $false|sQ32_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1041,f536])).
% 0.13/0.39 fof(f1052,plain,(
% 0.13/0.39 sQ32_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f1051])).
% 0.13/0.39 fof(f1053,plain,(
% 0.13/0.39 ![X0]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skac3))|memberP(app(X0,sk3),sk5(skac3)))),
% 0.13/0.39 inference(resolution,[status(thm)],[f809,f358])).
% 0.13/0.39 fof(f1054,plain,(
% 0.13/0.39 ![X0]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skac3))|memberP(app(sk3,X0),sk5(skac3)))),
% 0.13/0.39 inference(resolution,[status(thm)],[f809,f357])).
% 0.13/0.39 fof(f1055,plain,(
% 0.13/0.39 ![X0]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skac3))|memberP(cons(X0,sk3),sk5(skac3)))),
% 0.13/0.39 inference(resolution,[status(thm)],[f809,f356])).
% 0.13/0.39 fof(f1056,definition,(
% 0.13/0.39 ![X0]: (sQ35_spl <=> (~ssList(X0)|memberP(app(X0,sk3),sk5(skac3))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1059,definition,(
% 0.13/0.39 sQ36_spl <=> (ssItem(sk5(skac3)))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1061,plain,(
% 0.13/0.39 ~ssItem(sk5(skac3))|sQ36_spl),
% 0.13/0.39 inference(component_clause,[status(thm)],[f1059])).
% 0.13/0.39 fof(f1062,plain,(
% 0.13/0.39 ~sQ26_spl|sQ35_spl|~sQ36_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f1053,f1011,f1056,f1059])).
% 0.13/0.39 fof(f1063,definition,(
% 0.13/0.39 ![X0]: (sQ37_spl <=> (~ssList(X0)|memberP(app(sk3,X0),sk5(skac3))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1066,plain,(
% 0.13/0.39 sQ37_spl|~sQ26_spl|~sQ36_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f1054,f1063,f1011,f1059])).
% 0.13/0.39 fof(f1067,definition,(
% 0.13/0.39 ![X0]: (sQ38_spl <=> (~ssItem(X0)|memberP(cons(X0,sk3),sk5(skac3))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1070,plain,(
% 0.13/0.39 ~sQ26_spl|sQ38_spl|~sQ36_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f1055,f1011,f1067,f1059])).
% 0.13/0.39 fof(f1071,plain,(
% 0.13/0.39 $false|sQ36_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1061,f532])).
% 0.13/0.39 fof(f1072,plain,(
% 0.13/0.39 sQ36_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f1071])).
% 0.13/0.39 fof(f1083,plain,(
% 0.13/0.39 ![X0]: (~memberP(sk3,X0)|~ssList(nil)|~ssItem(sk6)|~ssItem(X0)|memberP(nil,X0)|X0=sk6|~sQ5_spl)),
% 0.13/0.39 inference(paramodulation,[status(thm)],[f471,f394])).
% 0.13/0.39 fof(f1084,definition,(
% 0.13/0.39 ![X0]: (sQ39_spl <=> (~memberP(sk3,X0)|~ssItem(X0)|memberP(nil,X0)|X0=sk6))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1085,plain,(
% 0.13/0.39 ![X0]: (~memberP(sk3,X0)|~ssItem(X0)|memberP(nil,X0)|X0=sk6|~sQ39_spl)),
% 0.13/0.39 inference(component_clause,[status(thm)],[f1084])).
% 0.13/0.39 fof(f1087,plain,(
% 0.13/0.39 sQ39_spl|~sQ21_spl|~sQ2_spl|~sQ5_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f1083,f1084,f816,f459,f470])).
% 0.13/0.39 fof(f1088,plain,(
% 0.13/0.39 ![X0]: (~memberP(sk3,X0)|~ssItem(X0)|X0=sk6|~sQ39_spl)),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1085,f273])).
% 0.13/0.39 fof(f1253,plain,(
% 0.13/0.39 ![X0,X1]: (~ssItem(X0)|~ssItem(X0)|~ssList(X1)|~ssList(X1)|X1=X1)),
% 0.13/0.39 inference(equality_resolution,[status(thm)],[f406])).
% 0.13/0.39 fof(f1259,definition,(
% 0.13/0.39 ![X0]: (sQ44_spl <=> (~ssItem(X0)|~ssItem(X0)))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1260,plain,(
% 0.13/0.39 ![X0]: (~ssItem(X0)|~ssItem(X0)|~sQ44_spl)),
% 0.13/0.39 inference(component_clause,[status(thm)],[f1259])).
% 0.13/0.39 fof(f1262,definition,(
% 0.13/0.39 ![X1]: (sQ45_spl <=> (~ssList(X1)|~ssList(X1)|X1=X1))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f1265,plain,(
% 0.13/0.39 sQ44_spl|sQ45_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f1253,f1259,f1262])).
% 0.13/0.39 fof(f1266,plain,(
% 0.13/0.39 ![X0]: (~ssItem(X0)|~sQ44_spl)),
% 0.13/0.39 inference(duplicate_literals_removal,[status(thm)],[f1260])).
% 0.13/0.39 fof(f1273,plain,(
% 0.13/0.39 $false|~sQ44_spl),
% 0.13/0.39 inference(backward_subsumption_resolution,[status(thm)],[f249,f1266])).
% 0.13/0.39 fof(f1316,plain,(
% 0.13/0.39 ~sQ44_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f1273])).
% 0.13/0.39 fof(f1915,plain,(
% 0.13/0.39 app(nil,nil)=nil),
% 0.13/0.39 inference(resolution,[status(thm)],[f276,f210])).
% 0.13/0.39 fof(f1930,plain,(
% 0.13/0.39 app(sk3,nil)=sk3),
% 0.13/0.39 inference(resolution,[status(thm)],[f276,f435])).
% 0.13/0.39 fof(f1935,plain,(
% 0.13/0.39 app(sk4,nil)=sk4),
% 0.13/0.39 inference(resolution,[status(thm)],[f276,f436])).
% 0.13/0.39 fof(f2017,definition,(
% 0.13/0.39 sQ52_spl <=> (nil=nil)),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2065,plain,(
% 0.13/0.39 ![X0]: (~memberP(sk3,X0)|~ssList(nil)|~ssList(sk3)|~ssItem(X0)|memberP(nil,X0)|memberP(sk3,X0))),
% 0.13/0.39 inference(paramodulation,[status(thm)],[f1930,f388])).
% 0.13/0.39 fof(f2066,definition,(
% 0.13/0.39 ![X0]: (sQ59_spl <=> (~memberP(sk3,X0)|~ssItem(X0)|memberP(nil,X0)|memberP(sk3,X0)))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2069,plain,(
% 0.13/0.39 sQ59_spl|~sQ21_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2065,f2066,f816,f1011])).
% 0.13/0.39 fof(f2136,plain,(
% 0.13/0.39 ![X0]: (~memberP(nil,X0)|~ssList(nil)|~ssList(nil)|~ssItem(X0)|memberP(nil,X0)|memberP(nil,X0))),
% 0.13/0.39 inference(paramodulation,[status(thm)],[f1915,f388])).
% 0.13/0.39 fof(f2137,definition,(
% 0.13/0.39 ![X0]: (sQ62_spl <=> (~memberP(nil,X0)|~ssItem(X0)|memberP(nil,X0)|memberP(nil,X0)))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2140,plain,(
% 0.13/0.39 sQ62_spl|~sQ21_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2136,f2137,f816])).
% 0.13/0.39 fof(f2141,plain,(
% 0.13/0.39 ![X0]: (~memberP(sk4,X0)|~ssList(nil)|~ssList(sk4)|~ssItem(X0)|memberP(nil,X0)|memberP(sk4,X0))),
% 0.13/0.39 inference(paramodulation,[status(thm)],[f1935,f388])).
% 0.13/0.39 fof(f2142,definition,(
% 0.13/0.39 ![X0]: (sQ63_spl <=> (~memberP(sk4,X0)|~ssItem(X0)|memberP(nil,X0)|memberP(sk4,X0)))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2145,plain,(
% 0.13/0.39 sQ63_spl|~sQ21_spl|~sQ17_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2141,f2142,f816,f634])).
% 0.13/0.39 fof(f2440,plain,(
% 0.13/0.39 ~ssList(nil)|nil=nil),
% 0.13/0.39 inference(resolution,[status(thm)],[f283,f943])).
% 0.13/0.39 fof(f2441,plain,(
% 0.13/0.39 ~sQ21_spl|sQ52_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2440,f816,f2017])).
% 0.13/0.39 fof(f2555,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf44(X1)))|memberP(cons(X0,sk3),sk5(skaf44(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f771,f356])).
% 0.13/0.39 fof(f2556,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf44(X1)))|memberP(app(sk3,X0),sk5(skaf44(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f771,f357])).
% 0.13/0.39 fof(f2557,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf44(X1)))|memberP(app(X0,sk3),sk5(skaf44(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f771,f358])).
% 0.13/0.39 fof(f2558,definition,(
% 0.13/0.39 ![X0,X1]: (sQ79_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf44(X1)))|memberP(cons(X0,sk3),sk5(skaf44(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2561,plain,(
% 0.13/0.39 ~sQ26_spl|sQ79_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2555,f1011,f2558])).
% 0.13/0.39 fof(f2562,definition,(
% 0.13/0.39 ![X0,X1]: (sQ80_spl <=> (~ssList(X0)|~ssItem(sk5(skaf44(X1)))|memberP(app(sk3,X0),sk5(skaf44(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2565,plain,(
% 0.13/0.39 sQ80_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2556,f2562,f1011])).
% 0.13/0.39 fof(f2566,definition,(
% 0.13/0.39 ![X0,X1]: (sQ81_spl <=> (~ssList(X0)|~ssItem(sk5(skaf44(X1)))|memberP(app(X0,sk3),sk5(skaf44(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2569,plain,(
% 0.13/0.39 ~sQ26_spl|sQ81_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2557,f1011,f2566])).
% 0.13/0.39 fof(f2573,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf49(X1)))|memberP(cons(X0,sk3),sk5(skaf49(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f772,f356])).
% 0.13/0.39 fof(f2574,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf49(X1)))|memberP(app(sk3,X0),sk5(skaf49(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f772,f357])).
% 0.13/0.39 fof(f2575,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf49(X1)))|memberP(app(X0,sk3),sk5(skaf49(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f772,f358])).
% 0.13/0.39 fof(f2576,definition,(
% 0.13/0.39 ![X0,X1]: (sQ82_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf49(X1)))|memberP(cons(X0,sk3),sk5(skaf49(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2579,plain,(
% 0.13/0.39 ~sQ26_spl|sQ82_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2573,f1011,f2576])).
% 0.13/0.39 fof(f2580,definition,(
% 0.13/0.39 ![X0,X1]: (sQ83_spl <=> (~ssList(X0)|~ssItem(sk5(skaf49(X1)))|memberP(app(sk3,X0),sk5(skaf49(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2583,plain,(
% 0.13/0.39 sQ83_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2574,f2580,f1011])).
% 0.13/0.39 fof(f2584,definition,(
% 0.13/0.39 ![X0,X1]: (sQ84_spl <=> (~ssList(X0)|~ssItem(sk5(skaf49(X1)))|memberP(app(X0,sk3),sk5(skaf49(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2587,plain,(
% 0.13/0.39 ~sQ26_spl|sQ84_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2575,f1011,f2584])).
% 0.13/0.39 fof(f2591,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf50(X1)))|memberP(cons(X0,sk3),sk5(skaf50(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f773,f356])).
% 0.13/0.39 fof(f2592,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf50(X1)))|memberP(app(sk3,X0),sk5(skaf50(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f773,f357])).
% 0.13/0.39 fof(f2593,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf50(X1)))|memberP(app(X0,sk3),sk5(skaf50(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f773,f358])).
% 0.13/0.39 fof(f2594,definition,(
% 0.13/0.39 ![X0,X1]: (sQ85_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf50(X1)))|memberP(cons(X0,sk3),sk5(skaf50(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2597,plain,(
% 0.13/0.39 ~sQ26_spl|sQ85_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2591,f1011,f2594])).
% 0.13/0.39 fof(f2598,definition,(
% 0.13/0.39 ![X0,X1]: (sQ86_spl <=> (~ssList(X0)|~ssItem(sk5(skaf50(X1)))|memberP(app(sk3,X0),sk5(skaf50(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2601,plain,(
% 0.13/0.39 sQ86_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2592,f2598,f1011])).
% 0.13/0.39 fof(f2602,definition,(
% 0.13/0.39 ![X0,X1]: (sQ87_spl <=> (~ssList(X0)|~ssItem(sk5(skaf50(X1)))|memberP(app(X0,sk3),sk5(skaf50(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2605,plain,(
% 0.13/0.39 ~sQ26_spl|sQ87_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2593,f1011,f2602])).
% 0.13/0.39 fof(f2609,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf54(X1)))|memberP(cons(X0,sk3),sk5(skaf54(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f774,f356])).
% 0.13/0.39 fof(f2610,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf54(X1)))|memberP(app(sk3,X0),sk5(skaf54(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f774,f357])).
% 0.13/0.39 fof(f2611,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf54(X1)))|memberP(app(X0,sk3),sk5(skaf54(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f774,f358])).
% 0.13/0.39 fof(f2612,definition,(
% 0.13/0.39 ![X0,X1]: (sQ88_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf54(X1)))|memberP(cons(X0,sk3),sk5(skaf54(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2615,plain,(
% 0.13/0.39 ~sQ26_spl|sQ88_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2609,f1011,f2612])).
% 0.13/0.39 fof(f2616,definition,(
% 0.13/0.39 ![X0,X1]: (sQ89_spl <=> (~ssList(X0)|~ssItem(sk5(skaf54(X1)))|memberP(app(sk3,X0),sk5(skaf54(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2619,plain,(
% 0.13/0.39 sQ89_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2610,f2616,f1011])).
% 0.13/0.39 fof(f2620,definition,(
% 0.13/0.39 ![X0,X1]: (sQ90_spl <=> (~ssList(X0)|~ssItem(sk5(skaf54(X1)))|memberP(app(X0,sk3),sk5(skaf54(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2623,plain,(
% 0.13/0.39 ~sQ26_spl|sQ90_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2611,f1011,f2620])).
% 0.13/0.39 fof(f2627,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf55(X1)))|memberP(cons(X0,sk3),sk5(skaf55(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f775,f356])).
% 0.13/0.39 fof(f2628,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf55(X1)))|memberP(app(sk3,X0),sk5(skaf55(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f775,f357])).
% 0.13/0.39 fof(f2629,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf55(X1)))|memberP(app(X0,sk3),sk5(skaf55(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f775,f358])).
% 0.13/0.39 fof(f2630,definition,(
% 0.13/0.39 ![X0,X1]: (sQ91_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf55(X1)))|memberP(cons(X0,sk3),sk5(skaf55(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2633,plain,(
% 0.13/0.39 ~sQ26_spl|sQ91_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2627,f1011,f2630])).
% 0.13/0.39 fof(f2634,definition,(
% 0.13/0.39 ![X0,X1]: (sQ92_spl <=> (~ssList(X0)|~ssItem(sk5(skaf55(X1)))|memberP(app(sk3,X0),sk5(skaf55(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2637,plain,(
% 0.13/0.39 sQ92_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2628,f2634,f1011])).
% 0.13/0.39 fof(f2638,definition,(
% 0.13/0.39 ![X0,X1]: (sQ93_spl <=> (~ssList(X0)|~ssItem(sk5(skaf55(X1)))|memberP(app(X0,sk3),sk5(skaf55(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2641,plain,(
% 0.13/0.39 ~sQ26_spl|sQ93_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2629,f1011,f2638])).
% 0.13/0.39 fof(f2758,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf59(X1)))|memberP(cons(X0,sk3),sk5(skaf59(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f776,f356])).
% 0.13/0.39 fof(f2759,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf59(X1)))|memberP(app(sk3,X0),sk5(skaf59(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f776,f357])).
% 0.13/0.39 fof(f2760,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf59(X1)))|memberP(app(X0,sk3),sk5(skaf59(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f776,f358])).
% 0.13/0.39 fof(f2761,definition,(
% 0.13/0.39 ![X0,X1]: (sQ94_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf59(X1)))|memberP(cons(X0,sk3),sk5(skaf59(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2764,plain,(
% 0.13/0.39 ~sQ26_spl|sQ94_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2758,f1011,f2761])).
% 0.13/0.39 fof(f2765,definition,(
% 0.13/0.39 ![X0,X1]: (sQ95_spl <=> (~ssList(X0)|~ssItem(sk5(skaf59(X1)))|memberP(app(sk3,X0),sk5(skaf59(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2768,plain,(
% 0.13/0.39 sQ95_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2759,f2765,f1011])).
% 0.13/0.39 fof(f2769,definition,(
% 0.13/0.39 ![X0,X1]: (sQ96_spl <=> (~ssList(X0)|~ssItem(sk5(skaf59(X1)))|memberP(app(X0,sk3),sk5(skaf59(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2772,plain,(
% 0.13/0.39 ~sQ26_spl|sQ96_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2760,f1011,f2769])).
% 0.13/0.39 fof(f2776,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf60(X1)))|memberP(cons(X0,sk3),sk5(skaf60(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f777,f356])).
% 0.13/0.39 fof(f2777,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf60(X1)))|memberP(app(sk3,X0),sk5(skaf60(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f777,f357])).
% 0.13/0.39 fof(f2778,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf60(X1)))|memberP(app(X0,sk3),sk5(skaf60(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f777,f358])).
% 0.13/0.39 fof(f2779,definition,(
% 0.13/0.39 ![X0,X1]: (sQ97_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf60(X1)))|memberP(cons(X0,sk3),sk5(skaf60(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2782,plain,(
% 0.13/0.39 ~sQ26_spl|sQ97_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2776,f1011,f2779])).
% 0.13/0.39 fof(f2783,definition,(
% 0.13/0.39 ![X0,X1]: (sQ98_spl <=> (~ssList(X0)|~ssItem(sk5(skaf60(X1)))|memberP(app(sk3,X0),sk5(skaf60(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2786,plain,(
% 0.13/0.39 sQ98_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2777,f2783,f1011])).
% 0.13/0.39 fof(f2787,definition,(
% 0.13/0.39 ![X0,X1]: (sQ99_spl <=> (~ssList(X0)|~ssItem(sk5(skaf60(X1)))|memberP(app(X0,sk3),sk5(skaf60(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2790,plain,(
% 0.13/0.39 ~sQ26_spl|sQ99_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2778,f1011,f2787])).
% 0.13/0.39 fof(f2794,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf64(X1)))|memberP(cons(X0,sk3),sk5(skaf64(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f778,f356])).
% 0.13/0.39 fof(f2795,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf64(X1)))|memberP(app(sk3,X0),sk5(skaf64(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f778,f357])).
% 0.13/0.39 fof(f2796,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf64(X1)))|memberP(app(X0,sk3),sk5(skaf64(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f778,f358])).
% 0.13/0.39 fof(f2797,definition,(
% 0.13/0.39 ![X0,X1]: (sQ100_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf64(X1)))|memberP(cons(X0,sk3),sk5(skaf64(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2800,plain,(
% 0.13/0.39 ~sQ26_spl|sQ100_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2794,f1011,f2797])).
% 0.13/0.39 fof(f2801,definition,(
% 0.13/0.39 ![X0,X1]: (sQ101_spl <=> (~ssList(X0)|~ssItem(sk5(skaf64(X1)))|memberP(app(sk3,X0),sk5(skaf64(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2804,plain,(
% 0.13/0.39 sQ101_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2795,f2801,f1011])).
% 0.13/0.39 fof(f2805,definition,(
% 0.13/0.39 ![X0,X1]: (sQ102_spl <=> (~ssList(X0)|~ssItem(sk5(skaf64(X1)))|memberP(app(X0,sk3),sk5(skaf64(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2808,plain,(
% 0.13/0.39 ~sQ26_spl|sQ102_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2796,f1011,f2805])).
% 0.13/0.39 fof(f2812,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf65(X1)))|memberP(cons(X0,sk3),sk5(skaf65(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f779,f356])).
% 0.13/0.39 fof(f2813,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf65(X1)))|memberP(app(sk3,X0),sk5(skaf65(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f779,f357])).
% 0.13/0.39 fof(f2814,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf65(X1)))|memberP(app(X0,sk3),sk5(skaf65(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f779,f358])).
% 0.13/0.39 fof(f2815,definition,(
% 0.13/0.39 ![X0,X1]: (sQ103_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf65(X1)))|memberP(cons(X0,sk3),sk5(skaf65(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2818,plain,(
% 0.13/0.39 ~sQ26_spl|sQ103_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2812,f1011,f2815])).
% 0.13/0.39 fof(f2819,definition,(
% 0.13/0.39 ![X0,X1]: (sQ104_spl <=> (~ssList(X0)|~ssItem(sk5(skaf65(X1)))|memberP(app(sk3,X0),sk5(skaf65(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2822,plain,(
% 0.13/0.39 sQ104_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2813,f2819,f1011])).
% 0.13/0.39 fof(f2823,definition,(
% 0.13/0.39 ![X0,X1]: (sQ105_spl <=> (~ssList(X0)|~ssItem(sk5(skaf65(X1)))|memberP(app(X0,sk3),sk5(skaf65(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2826,plain,(
% 0.13/0.39 ~sQ26_spl|sQ105_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2814,f1011,f2823])).
% 0.13/0.39 fof(f2830,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf69(X1)))|memberP(cons(X0,sk3),sk5(skaf69(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f780,f356])).
% 0.13/0.39 fof(f2831,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf69(X1)))|memberP(app(sk3,X0),sk5(skaf69(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f780,f357])).
% 0.13/0.39 fof(f2832,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf69(X1)))|memberP(app(X0,sk3),sk5(skaf69(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f780,f358])).
% 0.13/0.39 fof(f2833,definition,(
% 0.13/0.39 ![X0,X1]: (sQ106_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf69(X1)))|memberP(cons(X0,sk3),sk5(skaf69(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2836,plain,(
% 0.13/0.39 ~sQ26_spl|sQ106_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2830,f1011,f2833])).
% 0.13/0.39 fof(f2837,definition,(
% 0.13/0.39 ![X0,X1]: (sQ107_spl <=> (~ssList(X0)|~ssItem(sk5(skaf69(X1)))|memberP(app(sk3,X0),sk5(skaf69(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2840,plain,(
% 0.13/0.39 sQ107_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2831,f2837,f1011])).
% 0.13/0.39 fof(f2841,definition,(
% 0.13/0.39 ![X0,X1]: (sQ108_spl <=> (~ssList(X0)|~ssItem(sk5(skaf69(X1)))|memberP(app(X0,sk3),sk5(skaf69(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2844,plain,(
% 0.13/0.39 ~sQ26_spl|sQ108_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2832,f1011,f2841])).
% 0.13/0.39 fof(f2881,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf70(X1)))|memberP(cons(X0,sk3),sk5(skaf70(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f781,f356])).
% 0.13/0.39 fof(f2882,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf70(X1)))|memberP(app(sk3,X0),sk5(skaf70(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f781,f357])).
% 0.13/0.39 fof(f2883,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf70(X1)))|memberP(app(X0,sk3),sk5(skaf70(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f781,f358])).
% 0.13/0.39 fof(f2884,definition,(
% 0.13/0.39 ![X0,X1]: (sQ109_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf70(X1)))|memberP(cons(X0,sk3),sk5(skaf70(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2887,plain,(
% 0.13/0.39 ~sQ26_spl|sQ109_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2881,f1011,f2884])).
% 0.13/0.39 fof(f2888,definition,(
% 0.13/0.39 ![X0,X1]: (sQ110_spl <=> (~ssList(X0)|~ssItem(sk5(skaf70(X1)))|memberP(app(sk3,X0),sk5(skaf70(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2891,plain,(
% 0.13/0.39 sQ110_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2882,f2888,f1011])).
% 0.13/0.39 fof(f2892,definition,(
% 0.13/0.39 ![X0,X1]: (sQ111_spl <=> (~ssList(X0)|~ssItem(sk5(skaf70(X1)))|memberP(app(X0,sk3),sk5(skaf70(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2895,plain,(
% 0.13/0.39 ~sQ26_spl|sQ111_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2883,f1011,f2892])).
% 0.13/0.39 fof(f2899,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf74(X1)))|memberP(cons(X0,sk3),sk5(skaf74(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f782,f356])).
% 0.13/0.39 fof(f2900,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf74(X1)))|memberP(app(sk3,X0),sk5(skaf74(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f782,f357])).
% 0.13/0.39 fof(f2901,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf74(X1)))|memberP(app(X0,sk3),sk5(skaf74(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f782,f358])).
% 0.13/0.39 fof(f2902,definition,(
% 0.13/0.39 ![X0,X1]: (sQ112_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf74(X1)))|memberP(cons(X0,sk3),sk5(skaf74(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2905,plain,(
% 0.13/0.39 ~sQ26_spl|sQ112_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2899,f1011,f2902])).
% 0.13/0.39 fof(f2906,definition,(
% 0.13/0.39 ![X0,X1]: (sQ113_spl <=> (~ssList(X0)|~ssItem(sk5(skaf74(X1)))|memberP(app(sk3,X0),sk5(skaf74(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2909,plain,(
% 0.13/0.39 sQ113_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2900,f2906,f1011])).
% 0.13/0.39 fof(f2910,definition,(
% 0.13/0.39 ![X0,X1]: (sQ114_spl <=> (~ssList(X0)|~ssItem(sk5(skaf74(X1)))|memberP(app(X0,sk3),sk5(skaf74(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2913,plain,(
% 0.13/0.39 ~sQ26_spl|sQ114_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2901,f1011,f2910])).
% 0.13/0.39 fof(f2917,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf78(X1)))|memberP(cons(X0,sk3),sk5(skaf78(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f805,f356])).
% 0.13/0.39 fof(f2918,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf78(X1)))|memberP(app(sk3,X0),sk5(skaf78(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f805,f357])).
% 0.13/0.39 fof(f2919,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf78(X1)))|memberP(app(X0,sk3),sk5(skaf78(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f805,f358])).
% 0.13/0.39 fof(f2920,definition,(
% 0.13/0.39 ![X0,X1]: (sQ115_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf78(X1)))|memberP(cons(X0,sk3),sk5(skaf78(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2923,plain,(
% 0.13/0.39 ~sQ26_spl|sQ115_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2917,f1011,f2920])).
% 0.13/0.39 fof(f2924,definition,(
% 0.13/0.39 ![X0,X1]: (sQ116_spl <=> (~ssList(X0)|~ssItem(sk5(skaf78(X1)))|memberP(app(sk3,X0),sk5(skaf78(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2927,plain,(
% 0.13/0.39 sQ116_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2918,f2924,f1011])).
% 0.13/0.39 fof(f2928,definition,(
% 0.13/0.39 ![X0,X1]: (sQ117_spl <=> (~ssList(X0)|~ssItem(sk5(skaf78(X1)))|memberP(app(X0,sk3),sk5(skaf78(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2931,plain,(
% 0.13/0.39 ~sQ26_spl|sQ117_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2919,f1011,f2928])).
% 0.13/0.39 fof(f2935,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf79(X1)))|memberP(cons(X0,sk3),sk5(skaf79(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f806,f356])).
% 0.13/0.39 fof(f2936,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf79(X1)))|memberP(app(sk3,X0),sk5(skaf79(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f806,f357])).
% 0.13/0.39 fof(f2937,plain,(
% 0.13/0.39 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf79(X1)))|memberP(app(X0,sk3),sk5(skaf79(X1))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f806,f358])).
% 0.13/0.39 fof(f2938,definition,(
% 0.13/0.39 ![X0,X1]: (sQ118_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf79(X1)))|memberP(cons(X0,sk3),sk5(skaf79(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2941,plain,(
% 0.13/0.39 ~sQ26_spl|sQ118_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2935,f1011,f2938])).
% 0.13/0.39 fof(f2942,definition,(
% 0.13/0.39 ![X0,X1]: (sQ119_spl <=> (~ssList(X0)|~ssItem(sk5(skaf79(X1)))|memberP(app(sk3,X0),sk5(skaf79(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f2945,plain,(
% 0.13/0.39 sQ119_spl|~sQ26_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f2936,f2942,f1011])).
% 0.13/0.39 fof(f2946,definition,(
% 0.13/0.39 ![X0,X1]: (sQ120_spl <=> (~ssList(X0)|~ssItem(sk5(skaf79(X1)))|memberP(app(X0,sk3),sk5(skaf79(X1)))))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f2949,plain,(
% 0.13/0.40 ~sQ26_spl|sQ120_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f2937,f1011,f2946])).
% 0.13/0.40 fof(f2953,plain,(
% 0.13/0.40 ![X0,X1]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5(skaf83(X1)))|memberP(cons(X0,sk3),sk5(skaf83(X1))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f807,f356])).
% 0.13/0.40 fof(f2954,plain,(
% 0.13/0.40 ![X0,X1]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5(skaf83(X1)))|memberP(app(sk3,X0),sk5(skaf83(X1))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f807,f357])).
% 0.13/0.40 fof(f2955,plain,(
% 0.13/0.40 ![X0,X1]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5(skaf83(X1)))|memberP(app(X0,sk3),sk5(skaf83(X1))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f807,f358])).
% 0.13/0.40 fof(f2956,definition,(
% 0.13/0.40 ![X0,X1]: (sQ121_spl <=> (~ssItem(X0)|~ssItem(sk5(skaf83(X1)))|memberP(cons(X0,sk3),sk5(skaf83(X1)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f2959,plain,(
% 0.13/0.40 ~sQ26_spl|sQ121_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f2953,f1011,f2956])).
% 0.13/0.40 fof(f2960,definition,(
% 0.13/0.40 ![X0,X1]: (sQ122_spl <=> (~ssList(X0)|~ssItem(sk5(skaf83(X1)))|memberP(app(sk3,X0),sk5(skaf83(X1)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f2963,plain,(
% 0.13/0.40 sQ122_spl|~sQ26_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f2954,f2960,f1011])).
% 0.13/0.40 fof(f2964,definition,(
% 0.13/0.40 ![X0,X1]: (sQ123_spl <=> (~ssList(X0)|~ssItem(sk5(skaf83(X1)))|memberP(app(X0,sk3),sk5(skaf83(X1)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f2967,plain,(
% 0.13/0.40 ~sQ26_spl|sQ123_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f2955,f1011,f2964])).
% 0.13/0.40 fof(f3672,plain,(
% 0.13/0.40 ~ssItem(sk5(sk6))|sk5(sk6)=sk6|~sQ39_spl|~sQ2_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f1088,f783])).
% 0.13/0.40 fof(f3696,definition,(
% 0.13/0.40 sQ168_spl <=> (sk5(sk6)=sk6)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f3697,plain,(
% 0.13/0.40 sk5(sk6)=sk6|~sQ168_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f3696])).
% 0.13/0.40 fof(f3699,plain,(
% 0.13/0.40 ~sQ28_spl|sQ168_spl|~sQ39_spl|~sQ2_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f3672,f1017,f3696,f1084,f459])).
% 0.13/0.40 fof(f3713,plain,(
% 0.13/0.40 ~ssItem(sk6)|~sQ168_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f3697,f441])).
% 0.13/0.40 fof(f3716,plain,(
% 0.13/0.40 $false|~sQ2_spl|~sQ168_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f3713,f460])).
% 0.13/0.40 fof(f3717,plain,(
% 0.13/0.40 ~sQ2_spl|~sQ168_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f3716])).
% 0.13/0.40 fof(f3718,plain,(
% 0.13/0.40 $false),
% 0.13/0.40 inference(sat_refutation,[status(thm)],[f465,f469,f473,f482,f573,f599,f609,f613,f615,f639,f821,f849,f853,f858,f860,f1030,f1032,f1042,f1046,f1050,f1052,f1062,f1066,f1070,f1072,f1087,f1265,f1316,f2069,f2140,f2145,f2441,f2561,f2565,f2569,f2579,f2583,f2587,f2597,f2601,f2605,f2615,f2619,f2623,f2633,f2637,f2641,f2764,f2768,f2772,f2782,f2786,f2790,f2800,f2804,f2808,f2818,f2822,f2826,f2836,f2840,f2844,f2887,f2891,f2895,f2905,f2909,f2913,f2923,f2927,f2931,f2941,f2945,f2949,f2959,f2963,f2967,f3699,f3717])).
% 0.13/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.42 % Elapsed time: 0.065079 seconds
% 0.13/0.42 % CPU time: 0.199767 seconds
% 0.13/0.42 % Total memory used: 34.111 MB
% 0.13/0.42 % Net memory used: 33.864 MB
%------------------------------------------------------------------------------