%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC109-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 : n009.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:36 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC109-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.36 % Computer : n009.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8046.5625MB
% 0.13/0.36 % OS : Linux 6.8.0-71-generic
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Mon Sep 21 07:55:58 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 0.13/0.52 % Refutation found
% 0.13/0.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.52 fof(f8,axiom,(
% 0.13/0.52 ssList(nil) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f56,axiom,(
% 0.13/0.52 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f73,axiom,(
% 0.13/0.52 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f74,axiom,(
% 0.13/0.52 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f79,axiom,(
% 0.13/0.52 (![U]: (( nil != U| ~ ssList(U)| segmentP(nil,U) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f80,axiom,(
% 0.13/0.52 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f86,axiom,(
% 0.13/0.52 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f98,axiom,(
% 0.13/0.52 (![U,V]: (( cons(U,V) != nil| ~ ssItem(U)| ~ ssList(V) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f100,axiom,(
% 0.13/0.52 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f115,axiom,(
% 0.13/0.52 (![U,V]: (( U != V| ~ neq(U,V)| ~ ssList(V)| ~ ssList(U) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f119,axiom,(
% 0.13/0.52 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = V ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f127,axiom,(
% 0.13/0.52 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f140,axiom,(
% 0.13/0.52 (![U,V,W]: (( ~ memberP(U,V)| ~ ssList(W)| ~ ssList(U)| ~ ssItem(V)| memberP(app(U,W),V) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f141,axiom,(
% 0.13/0.52 (![U,V,W]: (( ~ memberP(U,V)| ~ ssList(U)| ~ ssList(W)| ~ ssItem(V)| memberP(app(W,U),V) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f145,axiom,(
% 0.13/0.52 (![U,V]: (( nil != U| nil != V| ~ ssList(V)| ~ ssList(U)| app(U,V) = nil ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f150,axiom,(
% 0.13/0.52 (![U,V,W]: (( app(U,V) != app(U,W)| ~ ssList(V)| ~ ssList(U)| ~ ssList(W)| V = W ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f151,axiom,(
% 0.13/0.52 (![U,V,W]: (( app(U,V) != app(W,V)| ~ ssList(U)| ~ ssList(V)| ~ ssList(W)| U = W ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f152,axiom,(
% 0.13/0.52 (![U,V,W]: (( ~ segmentP(U,V)| ~ segmentP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| segmentP(U,W) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f158,axiom,(
% 0.13/0.52 (![U,V,W]: (( ~ memberP(app(U,V),W)| ~ ssList(V)| ~ ssList(U)| ~ ssItem(W)| memberP(V,W)| memberP(U,W) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f173,axiom,(
% 0.13/0.52 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f186,negated_conjecture,(
% 0.13/0.52 ssList(sk1) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f187,negated_conjecture,(
% 0.13/0.52 ssList(sk2) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f190,negated_conjecture,(
% 0.13/0.52 sk2 = sk4 ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f191,negated_conjecture,(
% 0.13/0.52 sk1 = sk3 ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f192,negated_conjecture,(
% 0.13/0.52 ( ssItem(sk5)| nil = sk4 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f193,negated_conjecture,(
% 0.13/0.52 ( ssItem(sk5)| nil = sk3 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f194,negated_conjecture,(
% 0.13/0.52 ( ssList(sk6)| nil = sk4 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f195,negated_conjecture,(
% 0.13/0.52 ( ssList(sk7)| nil = sk4 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f196,negated_conjecture,(
% 0.13/0.52 ( cons(sk5,nil) = sk3| nil = sk4 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f197,negated_conjecture,(
% 0.13/0.52 ( app(app(sk6,sk3),sk7) = sk4| nil = sk4 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f200,negated_conjecture,(
% 0.13/0.52 ( ssList(sk6)| nil = sk3 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f201,negated_conjecture,(
% 0.13/0.52 ( ssList(sk7)| nil = sk3 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f202,negated_conjecture,(
% 0.13/0.52 ( cons(sk5,nil) = sk3| nil = sk3 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f203,negated_conjecture,(
% 0.13/0.52 ( app(app(sk6,sk3),sk7) = sk4| nil = sk3 ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f206,negated_conjecture,(
% 0.13/0.52 ( nil = sk2| neq(sk2,nil) ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f207,negated_conjecture,(
% 0.13/0.52 ( nil = sk2| ~ neq(sk1,nil)| ~ segmentP(sk2,sk1) ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f208,negated_conjecture,(
% 0.13/0.52 ( nil != sk1| neq(sk2,nil) ) ),
% 0.13/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f217,plain,(
% 0.13/0.52 ssList(nil)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.52 fof(f265,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f56])).
% 0.13/0.52 fof(f283,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f73])).
% 0.13/0.52 fof(f284,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f74])).
% 0.13/0.52 fof(f289,plain,(
% 0.13/0.52 ![X0]: (~nil=X0|~ssList(X0)|segmentP(nil,X0))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f79])).
% 0.13/0.52 fof(f290,plain,(
% 0.13/0.52 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f80])).
% 0.13/0.52 fof(f296,plain,(
% 0.13/0.52 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f86])).
% 0.13/0.52 fof(f308,plain,(
% 0.13/0.52 ![V]: ((![U]: (~cons(U,V)=nil|~ssItem(U)))|~ssList(V))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f98])).
% 0.13/0.52 fof(f309,plain,(
% 0.13/0.52 ![X0,X1]: (~cons(X0,X1)=nil|~ssItem(X0)|~ssList(X1))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f308])).
% 0.13/0.52 fof(f312,plain,(
% 0.13/0.52 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f100])).
% 0.13/0.52 fof(f330,plain,(
% 0.13/0.52 ![U]: ((![V]: ((~U=V|~neq(U,V))|~ssList(V)))|~ssList(U))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f115])).
% 0.13/0.52 fof(f331,plain,(
% 0.13/0.52 ![X0,X1]: (~X0=X1|~neq(X0,X1)|~ssList(X1)|~ssList(X0))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f330])).
% 0.13/0.52 fof(f338,plain,(
% 0.13/0.52 ![V]: ((![U]: ((~app(U,V)=nil|~ssList(V))|~ssList(U)))|nil=V)),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f119])).
% 0.13/0.52 fof(f339,plain,(
% 0.13/0.52 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X1)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f338])).
% 0.13/0.52 fof(f349,plain,(
% 0.13/0.52 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f127])).
% 0.13/0.52 fof(f364,plain,(
% 0.13/0.52 ![X0,X1,X2]: (~memberP(X0,X1)|~ssList(X2)|~ssList(X0)|~ssItem(X1)|memberP(app(X0,X2),X1))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f140])).
% 0.13/0.52 fof(f365,plain,(
% 0.13/0.52 ![X0,X1,X2]: (~memberP(X0,X1)|~ssList(X0)|~ssList(X2)|~ssItem(X1)|memberP(app(X2,X0),X1))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f141])).
% 0.13/0.52 fof(f371,plain,(
% 0.13/0.52 ![X0,X1]: (~nil=X0|~nil=X1|~ssList(X1)|~ssList(X0)|app(X0,X1)=nil)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f145])).
% 0.13/0.52 fof(f379,plain,(
% 0.13/0.52 ![V,W]: (((![U]: ((~app(U,V)=app(U,W)|~ssList(V))|~ssList(U)))|~ssList(W))|V=W)),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f150])).
% 0.13/0.52 fof(f380,plain,(
% 0.13/0.52 ![X0,X1,X2]: (~app(X0,X1)=app(X0,X2)|~ssList(X1)|~ssList(X0)|~ssList(X2)|X1=X2)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f379])).
% 0.13/0.52 fof(f381,plain,(
% 0.13/0.52 ![U,W]: (((![V]: ((~app(U,V)=app(W,V)|~ssList(U))|~ssList(V)))|~ssList(W))|U=W)),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f151])).
% 0.13/0.52 fof(f382,plain,(
% 0.13/0.52 ![X0,X1,X2]: (~app(X0,X1)=app(X2,X1)|~ssList(X0)|~ssList(X1)|~ssList(X2)|X0=X2)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f381])).
% 0.13/0.52 fof(f383,plain,(
% 0.13/0.52 ![U,W]: (((![V]: (((~segmentP(U,V)|~segmentP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|segmentP(U,W))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f152])).
% 0.13/0.52 fof(f384,plain,(
% 0.13/0.52 ![X0,X1,X2]: (~segmentP(X0,X1)|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|segmentP(X0,X2))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f383])).
% 0.13/0.52 fof(f394,plain,(
% 0.13/0.52 ![U,W]: ((![V]: ((((~memberP(app(U,V),W)|~ssList(V))|~ssList(U))|~ssItem(W))|memberP(V,W)))|memberP(U,W))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f158])).
% 0.13/0.52 fof(f395,plain,(
% 0.13/0.52 ![X0,X1,X2]: (~memberP(app(X0,X1),X2)|~ssList(X1)|~ssList(X0)|~ssItem(X2)|memberP(X1,X2)|memberP(X0,X2))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f394])).
% 0.13/0.52 fof(f415,plain,(
% 0.13/0.52 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f173])).
% 0.13/0.52 fof(f416,plain,(
% 0.13/0.52 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f415])).
% 0.13/0.52 fof(f440,plain,(
% 0.13/0.52 ssList(sk1)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f186])).
% 0.13/0.52 fof(f441,plain,(
% 0.13/0.52 ssList(sk2)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f187])).
% 0.13/0.52 fof(f444,plain,(
% 0.13/0.52 sk2=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f190])).
% 0.13/0.52 fof(f445,plain,(
% 0.13/0.52 sk1=sk3),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f191])).
% 0.13/0.52 fof(f446,plain,(
% 0.13/0.52 ssItem(sk5)|nil=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f192])).
% 0.13/0.52 fof(f447,plain,(
% 0.13/0.52 ssItem(sk5)|nil=sk3),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f193])).
% 0.13/0.52 fof(f448,plain,(
% 0.13/0.52 ssList(sk6)|nil=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f194])).
% 0.13/0.52 fof(f449,plain,(
% 0.13/0.52 ssList(sk7)|nil=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f195])).
% 0.13/0.52 fof(f450,plain,(
% 0.13/0.52 cons(sk5,nil)=sk3|nil=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f196])).
% 0.13/0.52 fof(f451,plain,(
% 0.13/0.52 app(app(sk6,sk3),sk7)=sk4|nil=sk4),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f197])).
% 0.13/0.52 fof(f456,plain,(
% 0.13/0.52 ssList(sk6)|nil=sk3),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f200])).
% 0.13/0.52 fof(f457,plain,(
% 0.13/0.52 ssList(sk7)|nil=sk3),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f201])).
% 0.13/0.52 fof(f458,plain,(
% 0.13/0.52 cons(sk5,nil)=sk3|nil=sk3),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f202])).
% 0.13/0.52 fof(f459,plain,(
% 0.13/0.52 app(app(sk6,sk3),sk7)=sk4|nil=sk3),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f203])).
% 0.13/0.52 fof(f464,plain,(
% 0.13/0.52 nil=sk2|neq(sk2,nil)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f206])).
% 0.13/0.52 fof(f465,plain,(
% 0.13/0.52 nil=sk2|~neq(sk1,nil)|~segmentP(sk2,sk1)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f207])).
% 0.13/0.52 fof(f466,plain,(
% 0.13/0.52 ~nil=sk1|neq(sk2,nil)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f208])).
% 0.13/0.52 fof(f475,definition,(
% 0.13/0.52 sQ2_spl <=> (ssItem(sk5))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f476,plain,(
% 0.13/0.52 ssItem(sk5)|~sQ2_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f475])).
% 0.13/0.52 fof(f478,definition,(
% 0.13/0.52 sQ3_spl <=> (nil=sk4)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f479,plain,(
% 0.13/0.52 nil=sk4|~sQ3_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f478])).
% 0.13/0.52 fof(f481,plain,(
% 0.13/0.52 sQ2_spl|sQ3_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f446,f475,f478])).
% 0.13/0.52 fof(f482,definition,(
% 0.13/0.52 sQ4_spl <=> (nil=sk3)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f483,plain,(
% 0.13/0.52 nil=sk3|~sQ4_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f482])).
% 0.13/0.52 fof(f484,plain,(
% 0.13/0.52 ~nil=sk3|sQ4_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f482])).
% 0.13/0.52 fof(f485,plain,(
% 0.13/0.52 sQ2_spl|sQ4_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f447,f475,f482])).
% 0.13/0.52 fof(f486,definition,(
% 0.13/0.52 sQ5_spl <=> (ssList(sk6))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f489,plain,(
% 0.13/0.52 sQ5_spl|sQ3_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f448,f486,f478])).
% 0.13/0.52 fof(f490,definition,(
% 0.13/0.52 sQ6_spl <=> (ssList(sk7))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f493,plain,(
% 0.13/0.52 sQ6_spl|sQ3_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f449,f490,f478])).
% 0.13/0.52 fof(f494,definition,(
% 0.13/0.52 sQ7_spl <=> (cons(sk5,nil)=sk3)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f495,plain,(
% 0.13/0.52 cons(sk5,nil)=sk3|~sQ7_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f494])).
% 0.13/0.52 fof(f497,plain,(
% 0.13/0.52 sQ7_spl|sQ3_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f450,f494,f478])).
% 0.13/0.52 fof(f498,definition,(
% 0.13/0.52 sQ8_spl <=> (app(app(sk6,sk3),sk7)=sk4)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f499,plain,(
% 0.13/0.52 app(app(sk6,sk3),sk7)=sk4|~sQ8_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f498])).
% 0.13/0.52 fof(f501,plain,(
% 0.13/0.52 sQ8_spl|sQ3_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f451,f498,f478])).
% 0.13/0.52 fof(f510,plain,(
% 0.13/0.52 sQ5_spl|sQ4_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f456,f486,f482])).
% 0.13/0.52 fof(f511,plain,(
% 0.13/0.52 sQ6_spl|sQ4_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f457,f490,f482])).
% 0.13/0.52 fof(f512,plain,(
% 0.13/0.52 sQ7_spl|sQ4_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f458,f494,f482])).
% 0.13/0.52 fof(f513,plain,(
% 0.13/0.52 sQ8_spl|sQ4_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f459,f498,f482])).
% 0.13/0.52 fof(f516,definition,(
% 0.13/0.52 sQ11_spl <=> (nil=sk2)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f517,plain,(
% 0.13/0.52 nil=sk2|~sQ11_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f516])).
% 0.13/0.52 fof(f518,plain,(
% 0.13/0.52 ~nil=sk2|sQ11_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f516])).
% 0.13/0.52 fof(f519,definition,(
% 0.13/0.52 sQ12_spl <=> (neq(sk2,nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f520,plain,(
% 0.13/0.52 neq(sk2,nil)|~sQ12_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f519])).
% 0.13/0.52 fof(f522,plain,(
% 0.13/0.52 sQ11_spl|sQ12_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f464,f516,f519])).
% 0.13/0.52 fof(f523,definition,(
% 0.13/0.52 sQ13_spl <=> (neq(sk1,nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f525,plain,(
% 0.13/0.52 ~neq(sk1,nil)|sQ13_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f523])).
% 0.13/0.52 fof(f526,definition,(
% 0.13/0.52 sQ14_spl <=> (segmentP(sk2,sk1))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f528,plain,(
% 0.13/0.52 ~segmentP(sk2,sk1)|sQ14_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f526])).
% 0.13/0.52 fof(f529,plain,(
% 0.13/0.52 sQ11_spl|~sQ13_spl|~sQ14_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f465,f516,f523,f526])).
% 0.13/0.52 fof(f530,definition,(
% 0.13/0.52 sQ15_spl <=> (nil=sk1)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f532,plain,(
% 0.13/0.52 ~nil=sk1|sQ15_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f530])).
% 0.13/0.52 fof(f533,plain,(
% 0.13/0.52 ~sQ15_spl|sQ12_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f466,f530,f519])).
% 0.13/0.52 fof(f535,plain,(
% 0.13/0.52 ~ssList(nil)|segmentP(nil,nil)),
% 0.13/0.52 inference(destructive_equality_resolution,[status(thm)],[f289])).
% 0.13/0.52 fof(f542,plain,(
% 0.13/0.52 ![X1]: (~neq(X1,X1)|~ssList(X1)|~ssList(X1))),
% 0.13/0.52 inference(destructive_equality_resolution,[status(thm)],[f331])).
% 0.13/0.52 fof(f543,plain,(
% 0.13/0.52 ![X0]: (~neq(X0,X0)|~ssList(X0))),
% 0.13/0.52 inference(duplicate_literals_removal,[status(thm)],[f542])).
% 0.13/0.52 fof(f551,plain,(
% 0.13/0.52 ~ssList(nil)|~ssList(nil)|app(nil,nil)=nil),
% 0.13/0.52 inference(destructive_equality_resolution,[status(thm)],[f371])).
% 0.13/0.52 fof(f552,plain,(
% 0.13/0.52 ~ssList(nil)|app(nil,nil)=nil),
% 0.13/0.52 inference(duplicate_literals_removal,[status(thm)],[f551])).
% 0.13/0.52 fof(f553,plain,(
% 0.13/0.52 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 0.13/0.52 inference(destructive_equality_resolution,[status(thm)],[f416])).
% 0.13/0.52 fof(f567,plain,(
% 0.13/0.52 nil=sk1|~sQ4_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f445,f483])).
% 0.13/0.52 fof(f568,plain,(
% 0.13/0.52 sk2=sk1|~sQ4_spl|~sQ3_spl),
% 0.13/0.52 inference(backward_demodulation,[status(thm)],[f569,f444])).
% 0.13/0.52 fof(f569,plain,(
% 0.13/0.52 sk1=sk4|~sQ4_spl|~sQ3_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f567,f479])).
% 0.13/0.52 fof(f570,plain,(
% 0.13/0.52 ~sk1=sk1|~sQ4_spl|sQ15_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f567,f532])).
% 0.13/0.52 fof(f571,plain,(
% 0.13/0.52 $false|~sQ4_spl|sQ15_spl),
% 0.13/0.52 inference(trivial_equality_resolution,[status(thm)],[f570])).
% 0.13/0.52 fof(f572,plain,(
% 0.13/0.52 ~sQ4_spl|sQ15_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f571])).
% 0.13/0.52 fof(f573,plain,(
% 0.13/0.52 cons(sk5,nil)=sk1|~sQ7_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f445,f495])).
% 0.13/0.52 fof(f574,plain,(
% 0.13/0.52 app(app(sk6,sk1),sk7)=sk4|~sQ8_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f445,f499])).
% 0.13/0.52 fof(f575,plain,(
% 0.13/0.52 ~nil=sk1|sQ4_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f445,f484])).
% 0.13/0.52 fof(f587,plain,(
% 0.13/0.52 ~sk2=sk1|~sQ11_spl|sQ4_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f517,f575])).
% 0.13/0.52 fof(f589,plain,(
% 0.13/0.52 neq(sk2,sk2)|~sQ11_spl|~sQ12_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f517,f520])).
% 0.13/0.52 fof(f590,plain,(
% 0.13/0.52 cons(sk5,sk2)=sk1|~sQ11_spl|~sQ7_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f517,f573])).
% 0.13/0.52 fof(f591,plain,(
% 0.13/0.52 app(app(sk6,sk1),sk7)=sk2|~sQ8_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f444,f574])).
% 0.13/0.52 fof(f592,plain,(
% 0.13/0.52 ~ssList(sk2)|~sQ11_spl|~sQ12_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f543,f589])).
% 0.13/0.52 fof(f593,plain,(
% 0.13/0.52 $false|~sQ11_spl|~sQ12_spl),
% 0.13/0.52 inference(forward_subsumption_resolution,[status(thm)],[f592,f441])).
% 0.13/0.52 fof(f594,plain,(
% 0.13/0.52 ~sQ11_spl|~sQ12_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f593])).
% 0.13/0.52 fof(f624,plain,(
% 0.13/0.52 ~sk1=sk2|~sQ4_spl|sQ11_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f567,f518])).
% 0.13/0.52 fof(f625,plain,(
% 0.13/0.52 ~sk1=sk1|~sQ3_spl|~sQ4_spl|sQ11_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f568,f624])).
% 0.13/0.52 fof(f626,plain,(
% 0.13/0.52 $false|~sQ3_spl|~sQ4_spl|sQ11_spl),
% 0.13/0.52 inference(trivial_equality_resolution,[status(thm)],[f625])).
% 0.13/0.52 fof(f627,plain,(
% 0.13/0.52 ~sQ3_spl|~sQ4_spl|sQ11_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f626])).
% 0.13/0.52 fof(f636,definition,(
% 0.13/0.52 sQ16_spl <=> (ssList(sk2))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f638,plain,(
% 0.13/0.52 ~ssList(sk2)|sQ16_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f636])).
% 0.13/0.52 fof(f643,plain,(
% 0.13/0.52 $false|sQ16_spl),
% 0.13/0.52 inference(forward_subsumption_resolution,[status(thm)],[f638,f441])).
% 0.13/0.52 fof(f644,plain,(
% 0.13/0.52 sQ16_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f643])).
% 0.13/0.52 fof(f655,plain,(
% 0.13/0.52 ~ssItem(sk5)|~ssList(sk2)|ssList(sk1)|~sQ11_spl|~sQ7_spl),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f590,f296])).
% 0.13/0.52 fof(f656,definition,(
% 0.13/0.52 sQ18_spl <=> (ssList(sk1))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f659,plain,(
% 0.13/0.52 ~sQ2_spl|~sQ16_spl|sQ18_spl|~sQ11_spl|~sQ7_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f655,f475,f636,f656,f516,f494])).
% 0.13/0.52 fof(f661,definition,(
% 0.13/0.52 sQ19_spl <=> (ssList(nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f663,plain,(
% 0.13/0.52 ~ssList(nil)|sQ19_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f661])).
% 0.13/0.52 fof(f664,definition,(
% 0.13/0.52 sQ20_spl <=> (segmentP(nil,nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f665,plain,(
% 0.13/0.52 segmentP(nil,nil)|~sQ20_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f664])).
% 0.13/0.52 fof(f667,plain,(
% 0.13/0.52 ~sQ19_spl|sQ20_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f535,f661,f664])).
% 0.13/0.52 fof(f668,plain,(
% 0.13/0.52 ~ssItem(sk5)|~ssList(nil)|ssList(sk1)|~sQ7_spl),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f573,f296])).
% 0.13/0.52 fof(f669,plain,(
% 0.13/0.52 ~sQ2_spl|~sQ19_spl|sQ18_spl|~sQ7_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f668,f475,f661,f656,f494])).
% 0.13/0.52 fof(f670,plain,(
% 0.13/0.52 $false|sQ19_spl),
% 0.13/0.52 inference(forward_subsumption_resolution,[status(thm)],[f663,f217])).
% 0.13/0.52 fof(f671,plain,(
% 0.13/0.52 sQ19_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f670])).
% 0.13/0.52 fof(f674,plain,(
% 0.13/0.52 ![X0]: (~cons(sk5,X0)=nil|~ssList(X0)|~sQ2_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f309,f476])).
% 0.13/0.52 fof(f737,plain,(
% 0.13/0.52 app(nil,nil)=nil),
% 0.13/0.52 inference(resolution,[status(thm)],[f284,f217])).
% 0.13/0.52 fof(f744,plain,(
% 0.13/0.52 app(nil,sk2)=sk2),
% 0.13/0.52 inference(resolution,[status(thm)],[f284,f441])).
% 0.13/0.52 fof(f753,plain,(
% 0.13/0.52 app(nil,sk1)=sk1),
% 0.13/0.52 inference(resolution,[status(thm)],[f284,f440])).
% 0.13/0.52 fof(f758,plain,(
% 0.13/0.52 ~ssList(nil)|~ssList(sk1)|sk1=nil|sQ13_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f312,f525])).
% 0.13/0.52 fof(f761,plain,(
% 0.13/0.52 ~sQ19_spl|~sQ18_spl|sQ15_spl|sQ13_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f758,f661,f656,f530,f523])).
% 0.13/0.52 fof(f816,plain,(
% 0.13/0.52 app(sk2,nil)=sk2),
% 0.13/0.52 inference(resolution,[status(thm)],[f283,f441])).
% 0.13/0.52 fof(f825,plain,(
% 0.13/0.52 app(sk1,nil)=sk1),
% 0.13/0.52 inference(resolution,[status(thm)],[f283,f440])).
% 0.13/0.52 fof(f925,plain,(
% 0.13/0.52 ~cons(sk5,nil)=nil|~sQ2_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f674,f217])).
% 0.13/0.52 fof(f942,plain,(
% 0.13/0.52 ~sk1=nil|~sQ7_spl|~sQ2_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f573,f925])).
% 0.13/0.52 fof(f1001,plain,(
% 0.13/0.52 ![X0]: (~app(X0,sk2)=nil|~ssList(X0)|nil=sk2)),
% 0.13/0.52 inference(resolution,[status(thm)],[f339,f441])).
% 0.13/0.52 fof(f1014,definition,(
% 0.13/0.52 sQ23_spl <=> (nil=nil)),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1019,definition,(
% 0.13/0.52 ![X0]: (sQ24_spl <=> (~app(X0,sk2)=nil|~ssList(X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1022,plain,(
% 0.13/0.52 sQ24_spl|sQ11_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1001,f1019,f516])).
% 0.13/0.52 fof(f1111,plain,(
% 0.13/0.52 ~sQ15_spl|~sQ7_spl|~sQ2_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f942,f530,f494,f475])).
% 0.13/0.52 fof(f1157,definition,(
% 0.13/0.52 ![X0]: (sQ38_spl <=> (~memberP(nil,X0)|~ssItem(X0)|memberP(sk1,X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1171,plain,(
% 0.13/0.52 app(nil,nil)=nil),
% 0.13/0.52 inference(forward_subsumption_resolution,[status(thm)],[f552,f217])).
% 0.13/0.52 fof(f1172,plain,(
% 0.13/0.52 ![X0]: (~memberP(nil,X0)|~ssList(nil)|~ssList(nil)|~ssItem(X0)|memberP(nil,X0))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f1171,f365])).
% 0.13/0.52 fof(f1175,definition,(
% 0.13/0.52 ![X0]: (sQ41_spl <=> (~memberP(nil,X0)|~ssItem(X0)|memberP(nil,X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1178,plain,(
% 0.13/0.52 sQ41_spl|~sQ19_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1172,f1175,f661])).
% 0.13/0.52 fof(f1190,plain,(
% 0.13/0.52 ![X0]: (~memberP(nil,X0)|~ssList(nil)|~ssList(sk1)|~ssItem(X0)|memberP(sk1,X0))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f825,f365])).
% 0.13/0.52 fof(f1191,plain,(
% 0.13/0.52 ![X0]: (~memberP(sk1,X0)|~ssList(nil)|~ssList(sk1)|~ssItem(X0)|memberP(sk1,X0))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f825,f364])).
% 0.13/0.52 fof(f1193,plain,(
% 0.13/0.52 sQ38_spl|~sQ19_spl|~sQ18_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1190,f1157,f661,f656])).
% 0.13/0.52 fof(f1194,definition,(
% 0.13/0.52 ![X0]: (sQ43_spl <=> (~memberP(sk1,X0)|~ssItem(X0)|memberP(sk1,X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1197,plain,(
% 0.13/0.52 sQ43_spl|~sQ19_spl|~sQ18_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1191,f1194,f661,f656])).
% 0.13/0.52 fof(f1223,plain,(
% 0.13/0.52 ![X0]: (~memberP(nil,X0)|~ssList(nil)|~ssList(sk2)|~ssItem(X0)|memberP(sk2,X0))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f816,f365])).
% 0.13/0.52 fof(f1224,plain,(
% 0.13/0.52 ![X0]: (~memberP(sk2,X0)|~ssList(nil)|~ssList(sk2)|~ssItem(X0)|memberP(sk2,X0))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f816,f364])).
% 0.13/0.52 fof(f1226,definition,(
% 0.13/0.52 ![X0]: (sQ48_spl <=> (~memberP(nil,X0)|~ssItem(X0)|memberP(sk2,X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1229,plain,(
% 0.13/0.52 sQ48_spl|~sQ19_spl|~sQ16_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1223,f1226,f661,f636])).
% 0.13/0.52 fof(f1230,definition,(
% 0.13/0.52 ![X0]: (sQ49_spl <=> (~memberP(sk2,X0)|~ssItem(X0)|memberP(sk2,X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1233,plain,(
% 0.13/0.52 sQ49_spl|~sQ19_spl|~sQ16_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1224,f1230,f661,f636])).
% 0.13/0.52 fof(f1341,plain,(
% 0.13/0.52 ![X0]: (~sk2=app(sk2,X0)|~ssList(nil)|~ssList(sk2)|~ssList(X0)|nil=X0)),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f816,f380])).
% 0.13/0.52 fof(f1344,plain,(
% 0.13/0.52 ![X0]: (~sk1=app(sk1,X0)|~ssList(nil)|~ssList(sk1)|~ssList(X0)|nil=X0)),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f825,f380])).
% 0.13/0.52 fof(f1345,plain,(
% 0.13/0.52 ![X0]: (~nil=app(nil,X0)|~ssList(nil)|~ssList(nil)|~ssList(X0)|nil=X0)),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f1171,f380])).
% 0.13/0.52 fof(f1354,definition,(
% 0.13/0.52 ![X0]: (sQ50_spl <=> (~sk2=app(sk2,X0)|~ssList(X0)|nil=X0))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1357,plain,(
% 0.13/0.52 sQ50_spl|~sQ19_spl|~sQ16_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1341,f1354,f661,f636])).
% 0.13/0.52 fof(f1366,definition,(
% 0.13/0.52 ![X0]: (sQ53_spl <=> (~sk1=app(sk1,X0)|~ssList(X0)|nil=X0))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1369,plain,(
% 0.13/0.52 sQ53_spl|~sQ19_spl|~sQ18_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1344,f1366,f661,f656])).
% 0.13/0.52 fof(f1370,definition,(
% 0.13/0.52 ![X0]: (sQ54_spl <=> (~nil=app(nil,X0)|~ssList(X0)|nil=X0))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1373,plain,(
% 0.13/0.52 sQ54_spl|~sQ19_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1345,f1370,f661])).
% 0.13/0.52 fof(f1391,plain,(
% 0.13/0.52 ![X0]: (~app(nil,X0)=sk1|~ssList(X0)|~ssList(nil)|~ssList(sk1)|X0=sk1)),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f753,f380])).
% 0.13/0.52 fof(f1396,definition,(
% 0.13/0.52 ![X0]: (sQ58_spl <=> (~app(nil,X0)=sk1|~ssList(X0)|X0=sk1))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1399,plain,(
% 0.13/0.52 sQ58_spl|~sQ19_spl|~sQ18_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1391,f1396,f661,f656])).
% 0.13/0.52 fof(f1609,plain,(
% 0.13/0.52 ![X0]: (~app(X0,sk2)=sk2|~ssList(X0)|~ssList(sk2)|~ssList(nil)|X0=nil)),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f744,f382])).
% 0.13/0.52 fof(f1611,plain,(
% 0.13/0.52 ![X0]: (~app(nil,X0)=sk2|~ssList(X0)|~ssList(nil)|~ssList(sk2)|X0=sk2)),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f744,f380])).
% 0.13/0.52 fof(f1616,definition,(
% 0.13/0.52 ![X0]: (sQ71_spl <=> (~app(X0,sk2)=sk2|~ssList(X0)|X0=nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1619,plain,(
% 0.13/0.52 sQ71_spl|~sQ16_spl|~sQ19_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1609,f1616,f636,f661])).
% 0.13/0.52 fof(f1621,definition,(
% 0.13/0.52 ![X0]: (sQ72_spl <=> (~app(nil,X0)=sk2|~ssList(X0)|X0=sk2))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1624,plain,(
% 0.13/0.52 sQ72_spl|~sQ19_spl|~sQ16_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1611,f1621,f661,f636])).
% 0.13/0.52 fof(f1636,plain,(
% 0.13/0.52 ![X0]: (~segmentP(X0,nil)|~ssList(nil)|~ssList(nil)|~ssList(X0)|segmentP(X0,nil)|~sQ20_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f665,f384])).
% 0.13/0.52 fof(f1637,plain,(
% 0.13/0.52 ~segmentP(nil,nil)|~ssList(nil)|~ssList(nil)|nil=nil|~sQ20_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f665,f349])).
% 0.13/0.52 fof(f1638,definition,(
% 0.13/0.52 ![X0]: (sQ73_spl <=> (~segmentP(X0,nil)|~ssList(X0)|segmentP(X0,nil)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1641,plain,(
% 0.13/0.52 sQ73_spl|~sQ19_spl|~sQ20_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1636,f1638,f661,f664])).
% 0.13/0.52 fof(f1642,plain,(
% 0.13/0.52 ~sQ20_spl|~sQ19_spl|sQ23_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1637,f664,f661,f1014])).
% 0.13/0.52 fof(f1643,plain,(
% 0.13/0.52 ![X0]: (~app(X0,nil)=nil|~ssList(X0)|~ssList(nil)|~ssList(nil)|X0=nil)),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f737,f382])).
% 0.13/0.52 fof(f1650,definition,(
% 0.13/0.52 ![X0]: (sQ74_spl <=> (~app(X0,nil)=nil|~ssList(X0)|X0=nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1653,plain,(
% 0.13/0.52 sQ74_spl|~sQ19_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1643,f1650,f661])).
% 0.13/0.52 fof(f1660,plain,(
% 0.13/0.52 ![X0,X1]: (~ssList(X0)|~segmentP(X1,X0)|~ssList(nil)|~ssList(X0)|~ssList(X1)|segmentP(X1,nil))),
% 0.13/0.52 inference(resolution,[status(thm)],[f265,f384])).
% 0.13/0.52 fof(f1661,plain,(
% 0.13/0.52 ![X0]: (~ssList(X0)|~segmentP(nil,X0)|~ssList(nil)|~ssList(X0)|X0=nil)),
% 0.13/0.52 inference(resolution,[status(thm)],[f265,f349])).
% 0.13/0.52 fof(f1662,definition,(
% 0.13/0.52 ![X0,X1]: (sQ75_spl <=> (~ssList(X0)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|segmentP(X1,nil)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1665,plain,(
% 0.13/0.52 sQ75_spl|~sQ19_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1660,f1662,f661])).
% 0.13/0.52 fof(f1666,definition,(
% 0.13/0.52 ![X0]: (sQ76_spl <=> (~ssList(X0)|~segmentP(nil,X0)|~ssList(X0)|X0=nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1669,plain,(
% 0.13/0.52 sQ76_spl|~sQ19_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1661,f1666,f661])).
% 0.13/0.52 fof(f1674,plain,(
% 0.13/0.52 ![X0]: (~memberP(nil,X0)|~ssList(nil)|~ssList(nil)|~ssItem(X0)|memberP(nil,X0)|memberP(nil,X0))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f737,f395])).
% 0.13/0.52 fof(f1675,plain,(
% 0.13/0.52 ![X0]: (~memberP(sk2,X0)|~ssList(sk2)|~ssList(nil)|~ssItem(X0)|memberP(sk2,X0)|memberP(nil,X0))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f744,f395])).
% 0.13/0.52 fof(f1676,definition,(
% 0.13/0.52 ![X0]: (sQ77_spl <=> (~memberP(nil,X0)|~ssItem(X0)|memberP(nil,X0)|memberP(nil,X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1679,plain,(
% 0.13/0.52 sQ77_spl|~sQ19_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1674,f1676,f661])).
% 0.13/0.52 fof(f1680,definition,(
% 0.13/0.52 ![X0]: (sQ78_spl <=> (~memberP(sk2,X0)|~ssItem(X0)|memberP(sk2,X0)|memberP(nil,X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1683,plain,(
% 0.13/0.52 sQ78_spl|~sQ16_spl|~sQ19_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1675,f1680,f636,f661])).
% 0.13/0.52 fof(f1787,plain,(
% 0.13/0.52 ![X0]: (~memberP(sk1,X0)|~ssList(sk1)|~ssList(nil)|~ssItem(X0)|memberP(sk1,X0)|memberP(nil,X0))),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f753,f395])).
% 0.13/0.52 fof(f1788,plain,(
% 0.13/0.52 ![X0]: (~app(X0,sk1)=sk1|~ssList(X0)|~ssList(sk1)|~ssList(nil)|X0=nil)),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f753,f382])).
% 0.13/0.52 fof(f1795,definition,(
% 0.13/0.52 ![X0]: (sQ84_spl <=> (~memberP(sk1,X0)|~ssItem(X0)|memberP(sk1,X0)|memberP(nil,X0)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1798,plain,(
% 0.13/0.52 sQ84_spl|~sQ18_spl|~sQ19_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1787,f1795,f656,f661])).
% 0.13/0.52 fof(f1799,definition,(
% 0.13/0.52 ![X0]: (sQ85_spl <=> (~app(X0,sk1)=sk1|~ssList(X0)|X0=nil))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1802,plain,(
% 0.13/0.52 sQ85_spl|~sQ18_spl|~sQ19_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1788,f1799,f656,f661])).
% 0.13/0.52 fof(f1810,plain,(
% 0.13/0.52 ![X0]: (~app(X0,nil)=sk2|~ssList(X0)|~ssList(nil)|~ssList(sk2)|X0=sk2)),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f816,f382])).
% 0.13/0.52 fof(f1818,definition,(
% 0.13/0.52 ![X0]: (sQ86_spl <=> (~app(X0,nil)=sk2|~ssList(X0)|X0=sk2))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1821,plain,(
% 0.13/0.52 sQ86_spl|~sQ19_spl|~sQ16_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1810,f1818,f661,f636])).
% 0.13/0.52 fof(f1867,plain,(
% 0.13/0.52 ![X0]: (~app(X0,nil)=sk1|~ssList(X0)|~ssList(nil)|~ssList(sk1)|X0=sk1)),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f825,f382])).
% 0.13/0.52 fof(f1875,definition,(
% 0.13/0.52 ![X0]: (sQ89_spl <=> (~app(X0,nil)=sk1|~ssList(X0)|X0=sk1))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f1878,plain,(
% 0.13/0.52 sQ89_spl|~sQ19_spl|~sQ18_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1867,f1875,f661,f656])).
% 0.13/0.52 fof(f1996,plain,(
% 0.13/0.52 ~ssList(sk7)|~ssList(sk6)|~ssList(sk1)|~ssList(sk2)|segmentP(app(app(sk6,sk1),sk7),sk1)|~sQ8_spl),
% 0.13/0.52 inference(paramodulation,[status(thm)],[f591,f553])).
% 0.13/0.52 fof(f2000,definition,(
% 0.13/0.52 sQ96_spl <=> (segmentP(app(app(sk6,sk1),sk7),sk1))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f2001,plain,(
% 0.13/0.52 segmentP(app(app(sk6,sk1),sk7),sk1)|~sQ96_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f2000])).
% 0.13/0.52 fof(f2003,plain,(
% 0.13/0.52 ~sQ6_spl|~sQ5_spl|~sQ18_spl|~sQ16_spl|sQ96_spl|~sQ8_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f1996,f490,f486,f656,f636,f2000,f498])).
% 0.13/0.52 fof(f2008,plain,(
% 0.13/0.52 segmentP(sk2,sk1)|~sQ8_spl|~sQ96_spl),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f591,f2001])).
% 0.13/0.52 fof(f2009,plain,(
% 0.13/0.52 $false|sQ14_spl|~sQ8_spl|~sQ96_spl),
% 0.13/0.52 inference(forward_subsumption_resolution,[status(thm)],[f2008,f528])).
% 0.13/0.52 fof(f2010,plain,(
% 0.13/0.52 sQ14_spl|~sQ8_spl|~sQ96_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f2009])).
% 0.13/0.52 fof(f2056,plain,(
% 0.13/0.52 ![X0]: (~segmentP(sk2,X0)|~ssList(X0)|nil=X0|~sQ11_spl)),
% 0.13/0.52 inference(forward_demodulation,[status(thm)],[f517,f290])).
% 0.13/0.52 fof(f2057,plain,(
% 0.86/0.53 ![X0]: (~segmentP(sk2,X0)|~ssList(X0)|sk2=X0|~sQ11_spl)),
% 0.86/0.53 inference(forward_demodulation,[status(thm)],[f517,f2056])).
% 0.86/0.53 fof(f2084,plain,(
% 0.86/0.53 ~ssList(sk1)|sk2=sk1|~sQ8_spl|~sQ96_spl|~sQ11_spl),
% 0.86/0.53 inference(resolution,[status(thm)],[f2008,f2057])).
% 0.86/0.53 fof(f2088,definition,(
% 0.86/0.53 sQ101_spl <=> (sk2=sk1)),
% 0.86/0.53 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.86/0.53 fof(f2089,plain,(
% 0.86/0.53 sk2=sk1|~sQ101_spl),
% 0.86/0.53 inference(component_clause,[status(thm)],[f2088])).
% 0.86/0.53 fof(f2091,plain,(
% 0.86/0.53 ~sQ18_spl|sQ101_spl|~sQ8_spl|~sQ96_spl|~sQ11_spl),
% 0.86/0.53 inference(split_clause,[status(thm)],[f2084,f656,f2088,f498,f2000,f516])).
% 0.86/0.53 fof(f2104,plain,(
% 0.86/0.53 $false|~sQ11_spl|sQ4_spl|~sQ101_spl),
% 0.86/0.53 inference(forward_subsumption_resolution,[status(thm)],[f2089,f587])).
% 0.86/0.53 fof(f2105,plain,(
% 0.86/0.53 ~sQ11_spl|sQ4_spl|~sQ101_spl),
% 0.86/0.53 inference(contradiction_clause,[status(thm)],[f2104])).
% 0.86/0.53 fof(f2106,plain,(
% 0.86/0.53 $false),
% 0.86/0.53 inference(sat_refutation,[status(thm)],[f481,f485,f489,f493,f497,f501,f510,f511,f512,f513,f522,f529,f533,f572,f594,f627,f644,f659,f667,f669,f671,f761,f1022,f1111,f1178,f1193,f1197,f1229,f1233,f1357,f1369,f1373,f1399,f1619,f1624,f1641,f1642,f1653,f1665,f1669,f1679,f1683,f1798,f1802,f1821,f1878,f2003,f2010,f2091,f2105])).
% 0.86/0.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.86/0.54 % Elapsed time: 0.166336 seconds
% 0.86/0.54 % CPU time: 1.047664 seconds
% 0.86/0.54 % Total memory used: 131.514 MB
% 0.86/0.54 % Net memory used: 130.627 MB
%------------------------------------------------------------------------------