%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC392-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : 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:42:21 PM UTC 2026
% Result : Unsatisfiable 0.12s 5.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC392-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.55 % Computer : n004.cluster.edu
% 0.09/5.55 % Model : x86_64 x86_64
% 0.09/5.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.55 % Memory : 8046.5625MB
% 0.09/5.55 % OS : Linux 6.8.0-71-generic
% 0.09/5.55 % CPULimit : 300
% 0.09/5.55 % WCLimit : 300
% 0.09/5.55 % DateTime : Mon Sep 21 08:20:57 UTC 2026
% 0.09/5.55 % CPUTime :
% 0.09/5.57 % Drodi V4.1.1
% 0.12/5.61 % Refutation found
% 0.12/5.61 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/5.61 % SZS output start CNFRefutation for theBenchmark
% 0.12/5.61 fof(f8,axiom,(
% 0.12/5.61 ssList(nil) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f9,axiom,(
% 0.12/5.61 ssItem(skac3) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f10,axiom,(
% 0.12/5.61 ssItem(skac2) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f47,axiom,(
% 0.12/5.61 (![U]: (ssItem(skaf44(U)) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f56,axiom,(
% 0.12/5.61 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f62,axiom,(
% 0.12/5.61 (![U]: (( ~ ssItem(U)| leq(U,U) ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f71,axiom,(
% 0.12/5.61 (![U]: (( ~ memberP(nil,U)| ~ ssItem(U) ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f73,axiom,(
% 0.12/5.61 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f74,axiom,(
% 0.12/5.61 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f75,axiom,(
% 0.12/5.61 (![U]: (( ~ ssList(U)| ssList(tl(U))| nil = U ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f76,axiom,(
% 0.12/5.61 (![U]: (( ~ ssList(U)| ssItem(hd(U))| nil = U ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f80,axiom,(
% 0.12/5.61 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f86,axiom,(
% 0.12/5.61 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f98,axiom,(
% 0.12/5.61 (![U,V]: (( cons(U,V) != nil| ~ ssItem(U)| ~ ssList(V) ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f99,axiom,(
% 0.12/5.61 (![U,V]: (( cons(U,V) != V| ~ ssItem(U)| ~ ssList(V) ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f130,axiom,(
% 0.12/5.61 (![U,V]: (( ~ leq(U,V)| ~ leq(V,U)| ~ ssItem(U)| ~ ssItem(V)| V = U ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f139,axiom,(
% 0.12/5.61 (![U,V,W]: (( ~ memberP(U,V)| ~ ssList(U)| ~ ssItem(W)| ~ ssItem(V)| memberP(cons(W,U),V) ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f140,axiom,(
% 0.12/5.61 (![U,V,W]: (( ~ memberP(U,V)| ~ ssList(W)| ~ ssList(U)| ~ ssItem(V)| memberP(app(U,W),V) ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f141,axiom,(
% 0.12/5.61 (![U,V,W]: (( ~ memberP(U,V)| ~ ssList(U)| ~ ssList(W)| ~ ssItem(V)| memberP(app(W,U),V) ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f156,axiom,(
% 0.12/5.61 (![U,V,W]: (( ~ leq(U,V)| ~ leq(V,W)| ~ ssItem(W)| ~ ssItem(V)| ~ ssItem(U)| leq(U,W) ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f158,axiom,(
% 0.12/5.61 (![U,V,W]: (( ~ memberP(app(U,V),W)| ~ ssList(V)| ~ ssList(U)| ~ ssItem(W)| memberP(V,W)| memberP(U,W) ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f161,axiom,(
% 0.12/5.61 (![U,V,W]: (( ~ memberP(cons(U,V),W)| ~ ssList(V)| ~ ssItem(U)| ~ ssItem(W)| memberP(V,W)| W = U ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f171,axiom,(
% 0.12/5.61 (![U,V,W,X]: (( cons(U,V) != cons(W,X)| ~ ssItem(W)| ~ ssItem(U)| ~ ssList(X)| ~ ssList(V)| X = V ) ))),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f188,negated_conjecture,(
% 0.12/5.61 ssList(sk3) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f189,negated_conjecture,(
% 0.12/5.61 ssList(sk4) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f190,negated_conjecture,(
% 0.12/5.61 sk2 = sk4 ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f191,negated_conjecture,(
% 0.12/5.61 sk1 = sk3 ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f192,negated_conjecture,(
% 0.12/5.61 ssItem(sk5) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f193,negated_conjecture,(
% 0.12/5.61 memberP(sk1,sk5) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f194,negated_conjecture,(
% 0.12/5.61 ~ memberP(sk2,sk5) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f195,negated_conjecture,(
% 0.12/5.61 ( ssItem(sk6)| nil = sk4 ) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f196,negated_conjecture,(
% 0.12/5.61 ( ssItem(sk6)| nil = sk3 ) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f197,negated_conjecture,(
% 0.12/5.61 ( cons(sk6,nil) = sk3| nil = sk4 ) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f200,negated_conjecture,(
% 0.12/5.61 ( cons(sk6,nil) = sk3| nil = sk3 ) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f201,negated_conjecture,(
% 0.12/5.61 ( memberP(sk4,sk6)| nil = sk3 ) ),
% 0.12/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/5.61 fof(f210,plain,(
% 0.12/5.61 ssList(nil)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/5.61 fof(f211,plain,(
% 0.12/5.61 ssItem(skac3)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/5.61 fof(f212,plain,(
% 0.12/5.61 ssItem(skac2)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f10])).
% 0.12/5.61 fof(f249,plain,(
% 0.12/5.61 ![X0]: (ssItem(skaf44(X0)))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f47])).
% 0.12/5.61 fof(f258,plain,(
% 0.12/5.61 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f56])).
% 0.12/5.61 fof(f264,plain,(
% 0.12/5.61 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f62])).
% 0.12/5.61 fof(f273,plain,(
% 0.12/5.61 ![X0]: (~memberP(nil,X0)|~ssItem(X0))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/5.61 fof(f276,plain,(
% 0.12/5.61 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f73])).
% 0.12/5.61 fof(f277,plain,(
% 0.12/5.61 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f74])).
% 0.12/5.61 fof(f278,plain,(
% 0.12/5.61 ![X0]: (~ssList(X0)|ssList(tl(X0))|nil=X0)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f75])).
% 0.12/5.61 fof(f279,plain,(
% 0.12/5.61 ![X0]: (~ssList(X0)|ssItem(hd(X0))|nil=X0)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f76])).
% 0.12/5.61 fof(f283,plain,(
% 0.12/5.61 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f80])).
% 0.12/5.61 fof(f289,plain,(
% 0.12/5.61 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f86])).
% 0.12/5.61 fof(f301,plain,(
% 0.12/5.61 ![V]: ((![U]: (~cons(U,V)=nil|~ssItem(U)))|~ssList(V))),
% 0.12/5.61 inference(miniscoping,[status(thm)],[f98])).
% 0.12/5.61 fof(f302,plain,(
% 0.12/5.61 ![X0,X1]: (~cons(X0,X1)=nil|~ssItem(X0)|~ssList(X1))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f301])).
% 0.12/5.61 fof(f303,plain,(
% 0.12/5.61 ![V]: ((![U]: (~cons(U,V)=V|~ssItem(U)))|~ssList(V))),
% 0.12/5.61 inference(miniscoping,[status(thm)],[f99])).
% 0.12/5.61 fof(f304,plain,(
% 0.12/5.61 ![X0,X1]: (~cons(X0,X1)=X1|~ssItem(X0)|~ssList(X1))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f303])).
% 0.12/5.61 fof(f345,plain,(
% 0.12/5.61 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|~ssItem(X0)|~ssItem(X1)|X1=X0)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f130])).
% 0.12/5.61 fof(f356,plain,(
% 0.12/5.61 ![X0,X1,X2]: (~memberP(X0,X1)|~ssList(X0)|~ssItem(X2)|~ssItem(X1)|memberP(cons(X2,X0),X1))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f139])).
% 0.12/5.61 fof(f357,plain,(
% 0.12/5.61 ![X0,X1,X2]: (~memberP(X0,X1)|~ssList(X2)|~ssList(X0)|~ssItem(X1)|memberP(app(X0,X2),X1))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f140])).
% 0.12/5.61 fof(f358,plain,(
% 0.12/5.61 ![X0,X1,X2]: (~memberP(X0,X1)|~ssList(X0)|~ssList(X2)|~ssItem(X1)|memberP(app(X2,X0),X1))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f141])).
% 0.12/5.61 fof(f384,plain,(
% 0.12/5.61 ![U,W]: (((![V]: (((~leq(U,V)|~leq(V,W))|~ssItem(W))|~ssItem(V)))|~ssItem(U))|leq(U,W))),
% 0.12/5.61 inference(miniscoping,[status(thm)],[f156])).
% 0.12/5.61 fof(f385,plain,(
% 0.12/5.61 ![X0,X1,X2]: (~leq(X0,X1)|~leq(X1,X2)|~ssItem(X2)|~ssItem(X1)|~ssItem(X0)|leq(X0,X2))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f384])).
% 0.12/5.61 fof(f387,plain,(
% 0.12/5.61 ![U,W]: ((![V]: ((((~memberP(app(U,V),W)|~ssList(V))|~ssList(U))|~ssItem(W))|memberP(V,W)))|memberP(U,W))),
% 0.12/5.61 inference(miniscoping,[status(thm)],[f158])).
% 0.12/5.61 fof(f388,plain,(
% 0.12/5.61 ![X0,X1,X2]: (~memberP(app(X0,X1),X2)|~ssList(X1)|~ssList(X0)|~ssItem(X2)|memberP(X1,X2)|memberP(X0,X2))),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f387])).
% 0.12/5.61 fof(f393,plain,(
% 0.12/5.61 ![U,W]: ((![V]: ((((~memberP(cons(U,V),W)|~ssList(V))|~ssItem(U))|~ssItem(W))|memberP(V,W)))|W=U)),
% 0.12/5.61 inference(miniscoping,[status(thm)],[f161])).
% 0.12/5.61 fof(f394,plain,(
% 0.12/5.61 ![X0,X1,X2]: (~memberP(cons(X0,X1),X2)|~ssList(X1)|~ssItem(X0)|~ssItem(X2)|memberP(X1,X2)|X2=X0)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f393])).
% 0.12/5.61 fof(f405,plain,(
% 0.12/5.61 ![V,X]: ((((![U]: ((![W]: (~cons(U,V)=cons(W,X)|~ssItem(W)))|~ssItem(U)))|~ssList(X))|~ssList(V))|X=V)),
% 0.12/5.61 inference(miniscoping,[status(thm)],[f171])).
% 0.12/5.61 fof(f406,plain,(
% 0.12/5.61 ![X0,X1,X2,X3]: (~cons(X0,X1)=cons(X2,X3)|~ssItem(X2)|~ssItem(X0)|~ssList(X3)|~ssList(X1)|X3=X1)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f405])).
% 0.12/5.61 fof(f435,plain,(
% 0.12/5.61 ssList(sk3)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f188])).
% 0.12/5.61 fof(f436,plain,(
% 0.12/5.61 ssList(sk4)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f189])).
% 0.12/5.61 fof(f437,plain,(
% 0.12/5.61 sk2=sk4),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f190])).
% 0.12/5.61 fof(f438,plain,(
% 0.12/5.61 sk1=sk3),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f191])).
% 0.12/5.61 fof(f439,plain,(
% 0.12/5.61 ssItem(sk5)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f192])).
% 0.12/5.61 fof(f440,plain,(
% 0.12/5.61 memberP(sk1,sk5)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f193])).
% 0.12/5.61 fof(f441,plain,(
% 0.12/5.61 ~memberP(sk2,sk5)),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f194])).
% 0.12/5.61 fof(f442,plain,(
% 0.12/5.61 ssItem(sk6)|nil=sk4),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f195])).
% 0.12/5.61 fof(f443,plain,(
% 0.12/5.61 ssItem(sk6)|nil=sk3),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f196])).
% 0.12/5.61 fof(f444,plain,(
% 0.12/5.61 cons(sk6,nil)=sk3|nil=sk4),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f197])).
% 0.12/5.61 fof(f448,plain,(
% 0.12/5.61 cons(sk6,nil)=sk3|nil=sk3),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f200])).
% 0.12/5.61 fof(f449,plain,(
% 0.12/5.61 memberP(sk4,sk6)|nil=sk3),
% 0.12/5.61 inference(cnf_transformation,[status(thm)],[f201])).
% 0.12/5.61 fof(f459,definition,(
% 0.12/5.61 sQ2_spl <=> (ssItem(sk6))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f460,plain,(
% 0.12/5.61 ssItem(sk6)|~sQ2_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f459])).
% 0.12/5.61 fof(f462,definition,(
% 0.12/5.61 sQ3_spl <=> (nil=sk4)),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f463,plain,(
% 0.12/5.61 nil=sk4|~sQ3_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f462])).
% 0.12/5.61 fof(f465,plain,(
% 0.12/5.61 sQ2_spl|sQ3_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f442,f459,f462])).
% 0.12/5.61 fof(f466,definition,(
% 0.12/5.61 sQ4_spl <=> (nil=sk3)),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f467,plain,(
% 0.12/5.61 nil=sk3|~sQ4_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f466])).
% 0.12/5.61 fof(f469,plain,(
% 0.12/5.61 sQ2_spl|sQ4_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f443,f459,f466])).
% 0.12/5.61 fof(f470,definition,(
% 0.12/5.61 sQ5_spl <=> (cons(sk6,nil)=sk3)),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f471,plain,(
% 0.12/5.61 cons(sk6,nil)=sk3|~sQ5_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f470])).
% 0.12/5.61 fof(f473,plain,(
% 0.12/5.61 sQ5_spl|sQ3_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f444,f470,f462])).
% 0.12/5.61 fof(f474,definition,(
% 0.12/5.61 sQ6_spl <=> (memberP(sk4,sk6))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f475,plain,(
% 0.12/5.61 memberP(sk4,sk6)|~sQ6_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f474])).
% 0.12/5.61 fof(f482,plain,(
% 0.12/5.61 sQ5_spl|sQ4_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f448,f470,f466])).
% 0.12/5.61 fof(f483,plain,(
% 0.12/5.61 sQ6_spl|sQ4_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f449,f474,f466])).
% 0.12/5.61 fof(f517,plain,(
% 0.12/5.61 sk4=sk3|~sQ3_spl|~sQ4_spl),
% 0.12/5.61 inference(backward_demodulation,[status(thm)],[f463,f467])).
% 0.12/5.61 fof(f518,plain,(
% 0.12/5.61 sk1=sk4|~sQ3_spl|~sQ4_spl),
% 0.12/5.61 inference(backward_demodulation,[status(thm)],[f517,f438])).
% 0.12/5.61 fof(f520,plain,(
% 0.12/5.61 memberP(sk4,sk5)|~sQ3_spl|~sQ4_spl),
% 0.12/5.61 inference(forward_demodulation,[status(thm)],[f518,f440])).
% 0.12/5.61 fof(f521,plain,(
% 0.12/5.61 ~memberP(sk4,sk5)),
% 0.12/5.61 inference(forward_demodulation,[status(thm)],[f437,f441])).
% 0.12/5.61 fof(f522,plain,(
% 0.12/5.61 $false|~sQ3_spl|~sQ4_spl),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f521,f520])).
% 0.12/5.61 fof(f523,plain,(
% 0.12/5.61 ~sQ3_spl|~sQ4_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f522])).
% 0.12/5.61 fof(f524,plain,(
% 0.12/5.61 leq(sk6,sk6)|~sQ2_spl),
% 0.12/5.61 inference(resolution,[status(thm)],[f264,f460])).
% 0.12/5.61 fof(f525,plain,(
% 0.12/5.61 leq(sk5,sk5)),
% 0.12/5.61 inference(resolution,[status(thm)],[f264,f439])).
% 0.12/5.61 fof(f526,plain,(
% 0.12/5.61 leq(skac3,skac3)),
% 0.12/5.61 inference(resolution,[status(thm)],[f211,f264])).
% 0.12/5.61 fof(f527,plain,(
% 0.12/5.61 leq(skac2,skac2)),
% 0.12/5.61 inference(resolution,[status(thm)],[f212,f264])).
% 0.12/5.61 fof(f529,plain,(
% 0.12/5.61 memberP(sk3,sk5)),
% 0.12/5.61 inference(forward_demodulation,[status(thm)],[f438,f440])).
% 0.12/5.61 fof(f530,plain,(
% 0.12/5.61 ~sk3=nil|~ssItem(sk6)|~ssList(nil)|~sQ5_spl),
% 0.12/5.61 inference(paramodulation,[status(thm)],[f471,f304])).
% 0.12/5.61 fof(f531,definition,(
% 0.12/5.61 sQ8_spl <=> (ssList(nil))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f533,plain,(
% 0.12/5.61 ~ssList(nil)|sQ8_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f531])).
% 0.12/5.61 fof(f534,plain,(
% 0.12/5.61 ~sQ4_spl|~sQ2_spl|~sQ8_spl|~sQ5_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f530,f466,f459,f531,f470])).
% 0.12/5.61 fof(f548,plain,(
% 0.12/5.61 ![X0]: (~ssList(X0)|ssList(cons(skac2,X0)))),
% 0.12/5.61 inference(resolution,[status(thm)],[f289,f212])).
% 0.12/5.61 fof(f550,plain,(
% 0.12/5.61 ![X0]: (~ssList(X0)|ssList(cons(sk6,X0))|~sQ2_spl)),
% 0.12/5.61 inference(resolution,[status(thm)],[f289,f460])).
% 0.12/5.61 fof(f551,plain,(
% 0.12/5.61 ![X0]: (~ssList(X0)|ssList(cons(sk5,X0)))),
% 0.12/5.61 inference(resolution,[status(thm)],[f289,f439])).
% 0.12/5.61 fof(f568,definition,(
% 0.12/5.61 sQ10_spl <=> (ssList(sk4))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f570,plain,(
% 0.12/5.61 ~ssList(sk4)|sQ10_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f568])).
% 0.12/5.61 fof(f579,definition,(
% 0.12/5.61 sQ11_spl <=> (sk6=sk6)),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f583,plain,(
% 0.12/5.61 ssList(cons(skac2,nil))),
% 0.12/5.61 inference(resolution,[status(thm)],[f548,f210])).
% 0.12/5.61 fof(f596,plain,(
% 0.12/5.61 ssList(cons(skac2,sk3))),
% 0.12/5.61 inference(resolution,[status(thm)],[f548,f435])).
% 0.12/5.61 fof(f597,plain,(
% 0.12/5.61 ssList(cons(skac2,sk4))),
% 0.12/5.61 inference(resolution,[status(thm)],[f548,f436])).
% 0.12/5.61 fof(f606,plain,(
% 0.12/5.61 ~leq(skac2,skac2)|~ssItem(skac2)|~ssItem(skac2)|skac2=skac2),
% 0.12/5.61 inference(resolution,[status(thm)],[f345,f527])).
% 0.12/5.61 fof(f607,plain,(
% 0.12/5.61 ~leq(skac3,skac3)|~ssItem(skac3)|~ssItem(skac3)|skac3=skac3),
% 0.12/5.61 inference(resolution,[status(thm)],[f345,f526])).
% 0.12/5.61 fof(f608,plain,(
% 0.12/5.61 ~leq(sk5,sk5)|~ssItem(sk5)|~ssItem(sk5)|sk5=sk5),
% 0.12/5.61 inference(resolution,[status(thm)],[f345,f525])).
% 0.12/5.61 fof(f609,plain,(
% 0.12/5.61 ~leq(sk6,sk6)|~ssItem(sk6)|~ssItem(sk6)|sk6=sk6|~sQ2_spl),
% 0.12/5.61 inference(resolution,[status(thm)],[f345,f524])).
% 0.12/5.61 fof(f610,definition,(
% 0.12/5.61 sQ12_spl <=> (leq(skac2,skac2))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f612,plain,(
% 0.12/5.61 ~leq(skac2,skac2)|sQ12_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f610])).
% 0.12/5.61 fof(f613,definition,(
% 0.12/5.61 sQ13_spl <=> (ssItem(skac2))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f615,plain,(
% 0.12/5.61 ~ssItem(skac2)|sQ13_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f613])).
% 0.12/5.61 fof(f616,definition,(
% 0.12/5.61 sQ14_spl <=> (skac2=skac2)),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f619,plain,(
% 0.12/5.61 ~sQ12_spl|~sQ13_spl|sQ14_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f606,f610,f613,f616])).
% 0.12/5.61 fof(f620,definition,(
% 0.12/5.61 sQ15_spl <=> (leq(skac3,skac3))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f622,plain,(
% 0.12/5.61 ~leq(skac3,skac3)|sQ15_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f620])).
% 0.12/5.61 fof(f623,definition,(
% 0.12/5.61 sQ16_spl <=> (ssItem(skac3))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f625,plain,(
% 0.12/5.61 ~ssItem(skac3)|sQ16_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f623])).
% 0.12/5.61 fof(f626,definition,(
% 0.12/5.61 sQ17_spl <=> (skac3=skac3)),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f629,plain,(
% 0.12/5.61 ~sQ15_spl|~sQ16_spl|sQ17_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f607,f620,f623,f626])).
% 0.12/5.61 fof(f630,definition,(
% 0.12/5.61 sQ18_spl <=> (leq(sk5,sk5))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f632,plain,(
% 0.12/5.61 ~leq(sk5,sk5)|sQ18_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f630])).
% 0.12/5.61 fof(f633,definition,(
% 0.12/5.61 sQ19_spl <=> (ssItem(sk5))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f635,plain,(
% 0.12/5.61 ~ssItem(sk5)|sQ19_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f633])).
% 0.12/5.61 fof(f636,definition,(
% 0.12/5.61 sQ20_spl <=> (sk5=sk5)),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f639,plain,(
% 0.12/5.61 ~sQ18_spl|~sQ19_spl|sQ20_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f608,f630,f633,f636])).
% 0.12/5.61 fof(f640,definition,(
% 0.12/5.61 sQ21_spl <=> (leq(sk6,sk6))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f642,plain,(
% 0.12/5.61 ~leq(sk6,sk6)|sQ21_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f640])).
% 0.12/5.61 fof(f643,plain,(
% 0.12/5.61 ~sQ21_spl|~sQ2_spl|sQ11_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f609,f640,f459,f579])).
% 0.12/5.61 fof(f644,plain,(
% 0.12/5.61 $false|~sQ2_spl|sQ21_spl),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f642,f524])).
% 0.12/5.61 fof(f645,plain,(
% 0.12/5.61 ~sQ2_spl|sQ21_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f644])).
% 0.12/5.61 fof(f646,plain,(
% 0.12/5.61 $false|sQ19_spl),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f635,f439])).
% 0.12/5.61 fof(f647,plain,(
% 0.12/5.61 sQ19_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f646])).
% 0.12/5.61 fof(f648,plain,(
% 0.12/5.61 $false|sQ18_spl),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f632,f525])).
% 0.12/5.61 fof(f649,plain,(
% 0.12/5.61 sQ18_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f648])).
% 0.12/5.61 fof(f650,plain,(
% 0.12/5.61 $false|sQ16_spl),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f625,f211])).
% 0.12/5.61 fof(f651,plain,(
% 0.12/5.61 sQ16_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f650])).
% 0.12/5.61 fof(f652,plain,(
% 0.12/5.61 $false|sQ15_spl),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f622,f526])).
% 0.12/5.61 fof(f653,plain,(
% 0.12/5.61 sQ15_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f652])).
% 0.12/5.61 fof(f715,plain,(
% 0.12/5.61 ssList(cons(sk6,sk3))|~sQ2_spl),
% 0.12/5.61 inference(resolution,[status(thm)],[f550,f435])).
% 0.12/5.61 fof(f716,plain,(
% 0.12/5.61 ssList(cons(sk6,sk4))|~sQ2_spl),
% 0.12/5.61 inference(resolution,[status(thm)],[f550,f436])).
% 0.12/5.61 fof(f739,plain,(
% 0.12/5.61 ssList(cons(sk5,nil))),
% 0.12/5.61 inference(resolution,[status(thm)],[f551,f210])).
% 0.12/5.61 fof(f752,plain,(
% 0.12/5.61 ssList(cons(sk5,sk3))),
% 0.12/5.61 inference(resolution,[status(thm)],[f551,f435])).
% 0.12/5.61 fof(f753,plain,(
% 0.12/5.61 ssList(cons(sk5,sk4))),
% 0.12/5.61 inference(resolution,[status(thm)],[f551,f436])).
% 0.12/5.61 fof(f782,plain,(
% 0.12/5.61 ![X0]: (~ssList(sk3)|~ssItem(X0)|~ssItem(sk5)|memberP(cons(X0,sk3),sk5))),
% 0.12/5.61 inference(resolution,[status(thm)],[f356,f529])).
% 0.12/5.61 fof(f784,definition,(
% 0.12/5.61 sQ22_spl <=> (ssList(sk3))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f786,plain,(
% 0.12/5.61 ~ssList(sk3)|sQ22_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f784])).
% 0.12/5.61 fof(f787,definition,(
% 0.12/5.61 ![X0]: (sQ23_spl <=> (~ssItem(X0)|memberP(cons(X0,sk3),sk5)))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f790,plain,(
% 0.12/5.61 ~sQ22_spl|sQ23_spl|~sQ19_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f782,f784,f787,f633])).
% 0.12/5.61 fof(f795,plain,(
% 0.12/5.61 $false|sQ10_spl),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f570,f436])).
% 0.12/5.61 fof(f796,plain,(
% 0.12/5.61 sQ10_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f795])).
% 0.12/5.61 fof(f797,plain,(
% 0.12/5.61 $false|sQ22_spl),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f786,f435])).
% 0.12/5.61 fof(f798,plain,(
% 0.12/5.61 sQ22_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f797])).
% 0.12/5.61 fof(f799,plain,(
% 0.12/5.61 ![X0]: (~ssList(X0)|~ssList(sk3)|~ssItem(sk5)|memberP(app(sk3,X0),sk5))),
% 0.12/5.61 inference(resolution,[status(thm)],[f357,f529])).
% 0.12/5.61 fof(f801,definition,(
% 0.12/5.61 ![X0]: (sQ25_spl <=> (~ssList(X0)|memberP(app(sk3,X0),sk5)))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f804,plain,(
% 0.12/5.61 sQ25_spl|~sQ22_spl|~sQ19_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f799,f801,f784,f633])).
% 0.12/5.61 fof(f943,plain,(
% 0.12/5.61 segmentP(nil,nil)),
% 0.12/5.61 inference(resolution,[status(thm)],[f258,f210])).
% 0.12/5.61 fof(f1024,plain,(
% 0.12/5.61 ![X0]: (~ssList(sk3)|~ssList(X0)|~ssItem(sk5)|memberP(app(X0,sk3),sk5))),
% 0.12/5.61 inference(resolution,[status(thm)],[f358,f529])).
% 0.12/5.61 fof(f1026,definition,(
% 0.12/5.61 ![X0]: (sQ27_spl <=> (~ssList(X0)|memberP(app(X0,sk3),sk5)))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f1029,plain,(
% 0.12/5.61 ~sQ22_spl|sQ27_spl|~sQ19_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f1024,f784,f1026,f633])).
% 0.12/5.61 fof(f1049,plain,(
% 0.12/5.61 ![X0]: (~leq(X0,skac2)|~ssItem(skac2)|~ssItem(skac2)|~ssItem(X0)|leq(X0,skac2))),
% 0.12/5.61 inference(resolution,[status(thm)],[f385,f527])).
% 0.12/5.61 fof(f1050,plain,(
% 0.12/5.61 ![X0]: (~leq(X0,skac3)|~ssItem(skac3)|~ssItem(skac3)|~ssItem(X0)|leq(X0,skac3))),
% 0.12/5.61 inference(resolution,[status(thm)],[f385,f526])).
% 0.12/5.61 fof(f1051,plain,(
% 0.12/5.61 ![X0]: (~leq(X0,sk5)|~ssItem(sk5)|~ssItem(sk5)|~ssItem(X0)|leq(X0,sk5))),
% 0.12/5.61 inference(resolution,[status(thm)],[f385,f525])).
% 0.12/5.61 fof(f1052,plain,(
% 0.12/5.61 ![X0]: (~leq(X0,sk6)|~ssItem(sk6)|~ssItem(sk6)|~ssItem(X0)|leq(X0,sk6)|~sQ2_spl)),
% 0.12/5.61 inference(resolution,[status(thm)],[f385,f524])).
% 0.12/5.61 fof(f1057,definition,(
% 0.12/5.61 ![X0]: (sQ29_spl <=> (~leq(X0,skac2)|~ssItem(X0)|leq(X0,skac2)))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f1060,plain,(
% 0.12/5.61 sQ29_spl|~sQ13_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f1049,f1057,f613])).
% 0.12/5.61 fof(f1061,definition,(
% 0.12/5.61 ![X0]: (sQ30_spl <=> (~leq(X0,skac3)|~ssItem(X0)|leq(X0,skac3)))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f1064,plain,(
% 0.12/5.61 sQ30_spl|~sQ16_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f1050,f1061,f623])).
% 0.12/5.61 fof(f1065,definition,(
% 0.12/5.61 ![X0]: (sQ31_spl <=> (~leq(X0,sk5)|~ssItem(X0)|leq(X0,sk5)))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f1068,plain,(
% 0.12/5.61 sQ31_spl|~sQ19_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f1051,f1065,f633])).
% 0.12/5.61 fof(f1069,definition,(
% 0.12/5.61 ![X0]: (sQ32_spl <=> (~leq(X0,sk6)|~ssItem(X0)|leq(X0,sk6)))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f1072,plain,(
% 0.12/5.61 sQ32_spl|~sQ2_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f1052,f1069,f459])).
% 0.12/5.61 fof(f1080,plain,(
% 0.12/5.61 $false|sQ13_spl),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f615,f212])).
% 0.12/5.61 fof(f1081,plain,(
% 0.12/5.61 sQ13_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f1080])).
% 0.12/5.61 fof(f1083,plain,(
% 0.12/5.61 $false|sQ12_spl),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f612,f527])).
% 0.12/5.61 fof(f1084,plain,(
% 0.12/5.61 sQ12_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f1083])).
% 0.12/5.61 fof(f1230,plain,(
% 0.12/5.61 ![X0]: (~memberP(sk3,X0)|~ssList(nil)|~ssItem(sk6)|~ssItem(X0)|memberP(nil,X0)|X0=sk6|~sQ5_spl)),
% 0.12/5.61 inference(paramodulation,[status(thm)],[f471,f394])).
% 0.12/5.61 fof(f1231,definition,(
% 0.12/5.61 ![X0]: (sQ34_spl <=> (~memberP(sk3,X0)|~ssItem(X0)|memberP(nil,X0)|X0=sk6))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f1232,plain,(
% 0.12/5.61 ![X0]: (~memberP(sk3,X0)|~ssItem(X0)|memberP(nil,X0)|X0=sk6|~sQ34_spl)),
% 0.12/5.61 inference(component_clause,[status(thm)],[f1231])).
% 0.12/5.61 fof(f1234,plain,(
% 0.12/5.61 sQ34_spl|~sQ8_spl|~sQ2_spl|~sQ5_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f1230,f1231,f531,f459,f470])).
% 0.12/5.61 fof(f1235,plain,(
% 0.12/5.61 $false|sQ8_spl),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f533,f210])).
% 0.12/5.61 fof(f1236,plain,(
% 0.12/5.61 sQ8_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f1235])).
% 0.12/5.61 fof(f1237,plain,(
% 0.12/5.61 ![X0]: (~memberP(sk3,X0)|~ssItem(X0)|X0=sk6|~sQ34_spl)),
% 0.12/5.61 inference(forward_subsumption_resolution,[status(thm)],[f1232,f273])).
% 0.12/5.61 fof(f1455,plain,(
% 0.12/5.61 ![X0,X1]: (~ssItem(X0)|~ssItem(X0)|~ssList(X1)|~ssList(X1)|X1=X1)),
% 0.12/5.61 inference(equality_resolution,[status(thm)],[f406])).
% 0.12/5.61 fof(f1461,definition,(
% 0.12/5.61 ![X0]: (sQ39_spl <=> (~ssItem(X0)|~ssItem(X0)))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f1462,plain,(
% 0.12/5.61 ![X0]: (~ssItem(X0)|~ssItem(X0)|~sQ39_spl)),
% 0.12/5.61 inference(component_clause,[status(thm)],[f1461])).
% 0.12/5.61 fof(f1464,definition,(
% 0.12/5.61 ![X1]: (sQ40_spl <=> (~ssList(X1)|~ssList(X1)|X1=X1))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f1467,plain,(
% 0.12/5.61 sQ39_spl|sQ40_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f1455,f1461,f1464])).
% 0.12/5.61 fof(f1468,plain,(
% 0.12/5.61 ![X0]: (~ssItem(X0)|~sQ39_spl)),
% 0.12/5.61 inference(duplicate_literals_removal,[status(thm)],[f1462])).
% 0.12/5.61 fof(f1469,plain,(
% 0.12/5.61 $false|~sQ39_spl),
% 0.12/5.61 inference(backward_subsumption_resolution,[status(thm)],[f249,f1468])).
% 0.12/5.61 fof(f1488,plain,(
% 0.12/5.61 ~sQ39_spl),
% 0.12/5.61 inference(contradiction_clause,[status(thm)],[f1469])).
% 0.12/5.61 fof(f1731,plain,(
% 0.12/5.61 app(nil,nil)=nil),
% 0.12/5.61 inference(resolution,[status(thm)],[f276,f210])).
% 0.12/5.61 fof(f1745,plain,(
% 0.12/5.61 app(sk4,nil)=sk4),
% 0.12/5.61 inference(resolution,[status(thm)],[f276,f436])).
% 0.12/5.61 fof(f1929,plain,(
% 0.12/5.61 app(nil,sk3)=sk3),
% 0.12/5.61 inference(resolution,[status(thm)],[f277,f435])).
% 0.12/5.61 fof(f1946,plain,(
% 0.12/5.61 ssList(tl(cons(sk5,sk4)))|nil=cons(sk5,sk4)),
% 0.12/5.61 inference(resolution,[status(thm)],[f278,f753])).
% 0.12/5.61 fof(f1947,plain,(
% 0.12/5.61 ssList(tl(cons(sk5,sk3)))|nil=cons(sk5,sk3)),
% 0.12/5.61 inference(resolution,[status(thm)],[f278,f752])).
% 0.12/5.61 fof(f1948,plain,(
% 0.12/5.61 ssList(tl(cons(sk5,nil)))|nil=cons(sk5,nil)),
% 0.12/5.61 inference(resolution,[status(thm)],[f278,f739])).
% 0.12/5.61 fof(f1959,plain,(
% 0.12/5.61 ssList(tl(cons(sk6,sk4)))|nil=cons(sk6,sk4)|~sQ2_spl),
% 0.12/5.61 inference(resolution,[status(thm)],[f278,f716])).
% 0.12/5.61 fof(f1960,plain,(
% 0.12/5.61 ssList(tl(cons(sk6,sk3)))|nil=cons(sk6,sk3)|~sQ2_spl),
% 0.12/5.61 inference(resolution,[status(thm)],[f278,f715])).
% 0.12/5.61 fof(f1979,plain,(
% 0.12/5.61 ssList(tl(cons(skac2,sk4)))|nil=cons(skac2,sk4)),
% 0.12/5.61 inference(resolution,[status(thm)],[f278,f597])).
% 0.12/5.61 fof(f1980,plain,(
% 0.12/5.61 ssList(tl(cons(skac2,sk3)))|nil=cons(skac2,sk3)),
% 0.12/5.61 inference(resolution,[status(thm)],[f278,f596])).
% 0.12/5.61 fof(f1981,plain,(
% 0.12/5.61 ssList(tl(cons(skac2,nil)))|nil=cons(skac2,nil)),
% 0.12/5.61 inference(resolution,[status(thm)],[f278,f583])).
% 0.12/5.61 fof(f1997,definition,(
% 0.12/5.61 sQ42_spl <=> (ssList(tl(cons(sk5,sk4))))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f2000,definition,(
% 0.12/5.61 sQ43_spl <=> (nil=cons(sk5,sk4))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f2001,plain,(
% 0.12/5.61 nil=cons(sk5,sk4)|~sQ43_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f2000])).
% 0.12/5.61 fof(f2003,plain,(
% 0.12/5.61 sQ42_spl|sQ43_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f1946,f1997,f2000])).
% 0.12/5.61 fof(f2004,definition,(
% 0.12/5.61 sQ44_spl <=> (ssList(tl(cons(sk5,sk3))))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f2007,definition,(
% 0.12/5.61 sQ45_spl <=> (nil=cons(sk5,sk3))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f2008,plain,(
% 0.12/5.61 nil=cons(sk5,sk3)|~sQ45_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f2007])).
% 0.12/5.61 fof(f2010,plain,(
% 0.12/5.61 sQ44_spl|sQ45_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f1947,f2004,f2007])).
% 0.12/5.61 fof(f2011,definition,(
% 0.12/5.61 sQ46_spl <=> (ssList(tl(cons(sk5,nil))))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f2014,definition,(
% 0.12/5.61 sQ47_spl <=> (nil=cons(sk5,nil))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f2015,plain,(
% 0.12/5.61 nil=cons(sk5,nil)|~sQ47_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f2014])).
% 0.12/5.61 fof(f2017,plain,(
% 0.12/5.61 sQ46_spl|sQ47_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f1948,f2011,f2014])).
% 0.12/5.61 fof(f2018,definition,(
% 0.12/5.61 sQ48_spl <=> (ssList(tl(cons(sk6,sk4))))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f2021,definition,(
% 0.12/5.61 sQ49_spl <=> (nil=cons(sk6,sk4))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f2022,plain,(
% 0.12/5.61 nil=cons(sk6,sk4)|~sQ49_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f2021])).
% 0.12/5.61 fof(f2024,plain,(
% 0.12/5.61 sQ48_spl|sQ49_spl|~sQ2_spl),
% 0.12/5.61 inference(split_clause,[status(thm)],[f1959,f2018,f2021,f459])).
% 0.12/5.61 fof(f2025,definition,(
% 0.12/5.61 sQ50_spl <=> (ssList(tl(cons(sk6,sk3))))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f2028,definition,(
% 0.12/5.61 sQ51_spl <=> (nil=cons(sk6,sk3))),
% 0.12/5.61 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.12/5.61 fof(f2029,plain,(
% 0.12/5.61 nil=cons(sk6,sk3)|~sQ51_spl),
% 0.12/5.61 inference(component_clause,[status(thm)],[f2028])).
% 0.12/5.61 fof(f2031,plain,(
% 0.12/5.61 sQ50_spl|sQ51_spl|~sQ2_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f1960,f2025,f2028,f459])).
% 0.12/5.62 fof(f2032,definition,(
% 0.12/5.62 sQ52_spl <=> (ssList(tl(cons(skac2,sk4))))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2035,definition,(
% 0.12/5.62 sQ53_spl <=> (nil=cons(skac2,sk4))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2036,plain,(
% 0.12/5.62 nil=cons(skac2,sk4)|~sQ53_spl),
% 0.12/5.62 inference(component_clause,[status(thm)],[f2035])).
% 0.12/5.62 fof(f2038,plain,(
% 0.12/5.62 sQ52_spl|sQ53_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f1979,f2032,f2035])).
% 0.12/5.62 fof(f2039,definition,(
% 0.12/5.62 sQ54_spl <=> (ssList(tl(cons(skac2,sk3))))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2042,definition,(
% 0.12/5.62 sQ55_spl <=> (nil=cons(skac2,sk3))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2043,plain,(
% 0.12/5.62 nil=cons(skac2,sk3)|~sQ55_spl),
% 0.12/5.62 inference(component_clause,[status(thm)],[f2042])).
% 0.12/5.62 fof(f2045,plain,(
% 0.12/5.62 sQ54_spl|sQ55_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f1980,f2039,f2042])).
% 0.12/5.62 fof(f2046,definition,(
% 0.12/5.62 sQ56_spl <=> (ssList(tl(cons(skac2,nil))))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2049,definition,(
% 0.12/5.62 sQ57_spl <=> (nil=cons(skac2,nil))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2050,plain,(
% 0.12/5.62 nil=cons(skac2,nil)|~sQ57_spl),
% 0.12/5.62 inference(component_clause,[status(thm)],[f2049])).
% 0.12/5.62 fof(f2052,plain,(
% 0.12/5.62 sQ56_spl|sQ57_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f1981,f2046,f2049])).
% 0.12/5.62 fof(f2056,definition,(
% 0.12/5.62 sQ59_spl <=> (nil=nil)),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2083,plain,(
% 0.12/5.62 ssItem(hd(cons(sk5,sk4)))|nil=cons(sk5,sk4)),
% 0.12/5.62 inference(resolution,[status(thm)],[f279,f753])).
% 0.12/5.62 fof(f2084,plain,(
% 0.12/5.62 ssItem(hd(cons(sk5,sk3)))|nil=cons(sk5,sk3)),
% 0.12/5.62 inference(resolution,[status(thm)],[f279,f752])).
% 0.12/5.62 fof(f2085,plain,(
% 0.12/5.62 ssItem(hd(cons(sk5,nil)))|nil=cons(sk5,nil)),
% 0.12/5.62 inference(resolution,[status(thm)],[f279,f739])).
% 0.12/5.62 fof(f2096,plain,(
% 0.12/5.62 ssItem(hd(cons(sk6,sk4)))|nil=cons(sk6,sk4)|~sQ2_spl),
% 0.12/5.62 inference(resolution,[status(thm)],[f279,f716])).
% 0.12/5.62 fof(f2097,plain,(
% 0.12/5.62 ssItem(hd(cons(sk6,sk3)))|nil=cons(sk6,sk3)|~sQ2_spl),
% 0.12/5.62 inference(resolution,[status(thm)],[f279,f715])).
% 0.12/5.62 fof(f2116,plain,(
% 0.12/5.62 ssItem(hd(cons(skac2,sk4)))|nil=cons(skac2,sk4)),
% 0.12/5.62 inference(resolution,[status(thm)],[f279,f597])).
% 0.12/5.62 fof(f2117,plain,(
% 0.12/5.62 ssItem(hd(cons(skac2,sk3)))|nil=cons(skac2,sk3)),
% 0.12/5.62 inference(resolution,[status(thm)],[f279,f596])).
% 0.12/5.62 fof(f2118,plain,(
% 0.12/5.62 ssItem(hd(cons(skac2,nil)))|nil=cons(skac2,nil)),
% 0.12/5.62 inference(resolution,[status(thm)],[f279,f583])).
% 0.12/5.62 fof(f2134,definition,(
% 0.12/5.62 sQ62_spl <=> (ssItem(hd(cons(sk5,sk4))))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2137,plain,(
% 0.12/5.62 sQ62_spl|sQ43_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2083,f2134,f2000])).
% 0.12/5.62 fof(f2138,definition,(
% 0.12/5.62 sQ63_spl <=> (ssItem(hd(cons(sk5,sk3))))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2141,plain,(
% 0.12/5.62 sQ63_spl|sQ45_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2084,f2138,f2007])).
% 0.12/5.62 fof(f2142,definition,(
% 0.12/5.62 sQ64_spl <=> (ssItem(hd(cons(sk5,nil))))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2145,plain,(
% 0.12/5.62 sQ64_spl|sQ47_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2085,f2142,f2014])).
% 0.12/5.62 fof(f2146,definition,(
% 0.12/5.62 sQ65_spl <=> (ssItem(hd(cons(sk6,sk4))))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2149,plain,(
% 0.12/5.62 sQ65_spl|sQ49_spl|~sQ2_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2096,f2146,f2021,f459])).
% 0.12/5.62 fof(f2150,definition,(
% 0.12/5.62 sQ66_spl <=> (ssItem(hd(cons(sk6,sk3))))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2153,plain,(
% 0.12/5.62 sQ66_spl|sQ51_spl|~sQ2_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2097,f2150,f2028,f459])).
% 0.12/5.62 fof(f2154,definition,(
% 0.12/5.62 sQ67_spl <=> (ssItem(hd(cons(skac2,sk4))))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2157,plain,(
% 0.12/5.62 sQ67_spl|sQ53_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2116,f2154,f2035])).
% 0.12/5.62 fof(f2158,definition,(
% 0.12/5.62 sQ68_spl <=> (ssItem(hd(cons(skac2,sk3))))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2161,plain,(
% 0.12/5.62 sQ68_spl|sQ55_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2117,f2158,f2042])).
% 0.12/5.62 fof(f2162,definition,(
% 0.12/5.62 sQ69_spl <=> (ssItem(hd(cons(skac2,nil))))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2165,plain,(
% 0.12/5.62 sQ69_spl|sQ57_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2118,f2162,f2049])).
% 0.12/5.62 fof(f2317,plain,(
% 0.12/5.62 ~ssItem(sk6)|~ssList(sk4)|~sQ49_spl),
% 0.12/5.62 inference(resolution,[status(thm)],[f2022,f302])).
% 0.12/5.62 fof(f2324,plain,(
% 0.12/5.62 ~sQ2_spl|~sQ10_spl|~sQ49_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2317,f459,f568,f2021])).
% 0.12/5.62 fof(f2377,plain,(
% 0.12/5.62 ![X0]: (~memberP(sk4,X0)|~ssList(nil)|~ssList(sk4)|~ssItem(X0)|memberP(nil,X0)|memberP(sk4,X0))),
% 0.12/5.62 inference(paramodulation,[status(thm)],[f1745,f388])).
% 0.12/5.62 fof(f2379,plain,(
% 0.12/5.62 ![X0]: (~memberP(sk3,X0)|~ssList(sk3)|~ssList(nil)|~ssItem(X0)|memberP(sk3,X0)|memberP(nil,X0))),
% 0.12/5.62 inference(paramodulation,[status(thm)],[f1929,f388])).
% 0.12/5.62 fof(f2380,plain,(
% 0.12/5.62 ![X0]: (~memberP(nil,X0)|~ssList(nil)|~ssList(nil)|~ssItem(X0)|memberP(nil,X0)|memberP(nil,X0))),
% 0.12/5.62 inference(paramodulation,[status(thm)],[f1731,f388])).
% 0.12/5.62 fof(f2382,definition,(
% 0.12/5.62 ![X0]: (sQ85_spl <=> (~memberP(sk4,X0)|~ssItem(X0)|memberP(nil,X0)|memberP(sk4,X0)))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2385,plain,(
% 0.12/5.62 sQ85_spl|~sQ8_spl|~sQ10_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2377,f2382,f531,f568])).
% 0.12/5.62 fof(f2387,definition,(
% 0.12/5.62 ![X0]: (sQ86_spl <=> (~memberP(sk3,X0)|~ssItem(X0)|memberP(sk3,X0)|memberP(nil,X0)))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2390,plain,(
% 0.12/5.62 sQ86_spl|~sQ22_spl|~sQ8_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2379,f2387,f784,f531])).
% 0.12/5.62 fof(f2391,definition,(
% 0.12/5.62 ![X0]: (sQ87_spl <=> (~memberP(nil,X0)|~ssItem(X0)|memberP(nil,X0)|memberP(nil,X0)))),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f2394,plain,(
% 0.12/5.62 sQ87_spl|~sQ8_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2380,f2391,f531])).
% 0.12/5.62 fof(f2398,plain,(
% 0.12/5.62 ~ssItem(sk6)|~ssList(sk3)|~sQ51_spl),
% 0.12/5.62 inference(resolution,[status(thm)],[f2029,f302])).
% 0.12/5.62 fof(f2406,plain,(
% 0.12/5.62 ~sQ2_spl|~sQ22_spl|~sQ51_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2398,f459,f784,f2028])).
% 0.12/5.62 fof(f2425,plain,(
% 0.12/5.62 ~ssItem(skac2)|~ssList(sk3)|~sQ55_spl),
% 0.12/5.62 inference(resolution,[status(thm)],[f2043,f302])).
% 0.12/5.62 fof(f2433,plain,(
% 0.12/5.62 ~sQ13_spl|~sQ22_spl|~sQ55_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2425,f613,f784,f2042])).
% 0.12/5.62 fof(f2452,plain,(
% 0.12/5.62 ~ssItem(skac2)|~ssList(sk4)|~sQ53_spl),
% 0.12/5.62 inference(resolution,[status(thm)],[f2036,f302])).
% 0.12/5.62 fof(f2460,plain,(
% 0.12/5.62 ~sQ13_spl|~sQ10_spl|~sQ53_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2452,f613,f568,f2035])).
% 0.12/5.62 fof(f2482,plain,(
% 0.12/5.62 ~ssItem(sk5)|~ssList(nil)|~sQ47_spl),
% 0.12/5.62 inference(resolution,[status(thm)],[f2015,f302])).
% 0.12/5.62 fof(f2490,plain,(
% 0.12/5.62 ~sQ19_spl|~sQ8_spl|~sQ47_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2482,f633,f531,f2014])).
% 0.12/5.62 fof(f2512,plain,(
% 0.12/5.62 ~ssItem(sk5)|~ssList(sk3)|~sQ45_spl),
% 0.12/5.62 inference(resolution,[status(thm)],[f2008,f302])).
% 0.12/5.62 fof(f2520,plain,(
% 0.12/5.62 ~sQ19_spl|~sQ22_spl|~sQ45_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2512,f633,f784,f2007])).
% 0.12/5.62 fof(f2597,plain,(
% 0.12/5.62 ~ssItem(skac2)|~ssList(nil)|~sQ57_spl),
% 0.12/5.62 inference(resolution,[status(thm)],[f2050,f302])).
% 0.12/5.62 fof(f2605,plain,(
% 0.12/5.62 ~sQ13_spl|~sQ8_spl|~sQ57_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2597,f613,f531,f2049])).
% 0.12/5.62 fof(f2621,plain,(
% 0.12/5.62 ~ssItem(sk5)|~ssList(sk4)|~sQ43_spl),
% 0.12/5.62 inference(resolution,[status(thm)],[f2001,f302])).
% 0.12/5.62 fof(f2629,plain,(
% 0.12/5.62 ~sQ19_spl|~sQ10_spl|~sQ43_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2621,f633,f568,f2000])).
% 0.12/5.62 fof(f2700,plain,(
% 0.12/5.62 ~ssList(nil)|nil=nil),
% 0.12/5.62 inference(resolution,[status(thm)],[f283,f943])).
% 0.12/5.62 fof(f2701,plain,(
% 0.12/5.62 ~sQ8_spl|sQ59_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f2700,f531,f2056])).
% 0.12/5.62 fof(f3746,plain,(
% 0.12/5.62 ~ssItem(sk5)|sk5=sk6|~sQ34_spl),
% 0.12/5.62 inference(resolution,[status(thm)],[f1237,f529])).
% 0.12/5.62 fof(f3747,definition,(
% 0.12/5.62 sQ140_spl <=> (sk5=sk6)),
% 0.12/5.62 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 0.12/5.62 fof(f3748,plain,(
% 0.12/5.62 sk5=sk6|~sQ140_spl),
% 0.12/5.62 inference(component_clause,[status(thm)],[f3747])).
% 0.12/5.62 fof(f3750,plain,(
% 0.12/5.62 ~sQ19_spl|sQ140_spl|~sQ34_spl),
% 0.12/5.62 inference(split_clause,[status(thm)],[f3746,f633,f3747,f1231])).
% 0.12/5.62 fof(f3782,plain,(
% 0.12/5.62 ~memberP(sk4,sk6)|~sQ140_spl),
% 0.12/5.62 inference(backward_demodulation,[status(thm)],[f3748,f521])).
% 0.12/5.62 fof(f3794,plain,(
% 0.12/5.62 $false|~sQ6_spl|~sQ140_spl),
% 0.12/5.62 inference(forward_subsumption_resolution,[status(thm)],[f3782,f475])).
% 0.12/5.62 fof(f3795,plain,(
% 0.12/5.62 ~sQ6_spl|~sQ140_spl),
% 0.12/5.62 inference(contradiction_clause,[status(thm)],[f3794])).
% 0.12/5.62 fof(f3796,plain,(
% 0.12/5.62 $false),
% 0.12/5.62 inference(sat_refutation,[status(thm)],[f465,f469,f473,f482,f483,f523,f534,f619,f629,f639,f643,f645,f647,f649,f651,f653,f790,f796,f798,f804,f1029,f1060,f1064,f1068,f1072,f1081,f1084,f1234,f1236,f1467,f1488,f2003,f2010,f2017,f2024,f2031,f2038,f2045,f2052,f2137,f2141,f2145,f2149,f2153,f2157,f2161,f2165,f2324,f2385,f2390,f2394,f2406,f2433,f2460,f2490,f2520,f2605,f2629,f2701,f3750,f3795])).
% 0.12/5.62 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/5.65 % Elapsed time: 0.079037 seconds
% 0.12/5.65 % CPU time: 0.304219 seconds
% 0.12/5.65 % Total memory used: 113.000 MB
% 0.12/5.65 % Net memory used: 112.605 MB
%------------------------------------------------------------------------------