%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC330-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 : n006.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:10 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC330-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.08/0.54 % Computer : n006.cluster.edu
% 0.08/0.54 % Model : x86_64 x86_64
% 0.08/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.54 % Memory : 8046.5625MB
% 0.08/0.54 % OS : Linux 6.8.0-71-generic
% 0.08/0.54 % CPULimit : 300
% 0.08/0.54 % WCLimit : 300
% 0.08/0.54 % DateTime : Mon Sep 21 08:16:13 UTC 2026
% 0.08/0.54 % CPUTime :
% 0.13/0.56 % Drodi V4.1.1
% 0.13/0.69 % Refutation found
% 0.13/0.69 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.69 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.69 fof(f1,axiom,(
% 0.13/0.69 equalelemsP(nil) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f8,axiom,(
% 0.13/0.69 ssList(nil) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f9,axiom,(
% 0.13/0.69 ssItem(skac3) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f10,axiom,(
% 0.13/0.69 ssItem(skac2) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f13,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf82(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f14,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf81(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f15,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf80(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f18,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf77(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f19,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf76(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f20,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf75(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f22,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf73(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f23,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf72(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f24,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf71(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f27,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf68(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f28,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf67(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f29,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf66(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f32,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf63(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f33,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf62(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f34,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf61(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f37,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf58(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f38,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf57(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f39,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf56(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f42,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf53(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f43,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf52(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f44,axiom,(
% 0.13/0.69 (![U]: (ssList(skaf51(U)) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f55,axiom,(
% 0.13/0.69 (![U]: (( ~ ssItem(U)| geq(U,U) ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f56,axiom,(
% 0.13/0.69 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f57,axiom,(
% 0.13/0.69 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f62,axiom,(
% 0.13/0.69 (![U]: (( ~ ssItem(U)| leq(U,U) ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f64,axiom,(
% 0.13/0.69 (![U]: (( ~ ssItem(U)| equalelemsP(cons(U,nil)) ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f80,axiom,(
% 0.13/0.69 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f81,axiom,(
% 0.13/0.69 (![U]: (( nil != U| ~ ssList(U)| rearsegP(nil,U) ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f83,axiom,(
% 0.13/0.69 (![U]: (( nil != U| ~ ssList(U)| frontsegP(nil,U) ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f107,axiom,(
% 0.13/0.69 (![U,V]: (( ~ geq(U,V)| ~ ssItem(V)| ~ ssItem(U)| leq(V,U) ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f108,axiom,(
% 0.13/0.69 (![U,V]: (( ~ leq(U,V)| ~ ssItem(U)| ~ ssItem(V)| geq(V,U) ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f127,axiom,(
% 0.13/0.69 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f145,axiom,(
% 0.13/0.69 (![U,V]: (( nil != U| nil != V| ~ ssList(V)| ~ ssList(U)| app(U,V) = nil ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f150,axiom,(
% 0.13/0.69 (![U,V,W]: (( app(U,V) != app(U,W)| ~ ssList(V)| ~ ssList(U)| ~ ssList(W)| V = W ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f152,axiom,(
% 0.13/0.69 (![U,V,W]: (( ~ segmentP(U,V)| ~ segmentP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| segmentP(U,W) ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f170,axiom,(
% 0.13/0.69 (![U,V,W,X]: (( cons(U,V) != cons(W,X)| ~ ssItem(W)| ~ ssItem(U)| ~ ssList(X)| ~ ssList(V)| U = W ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f173,axiom,(
% 0.13/0.69 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f188,negated_conjecture,(
% 0.13/0.69 ssList(sk3) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f189,negated_conjecture,(
% 0.13/0.69 ssList(sk4) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f190,negated_conjecture,(
% 0.13/0.69 sk2 = sk4 ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f191,negated_conjecture,(
% 0.13/0.69 sk1 = sk3 ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f193,negated_conjecture,(
% 0.13/0.69 ( ssItem(sk5)| nil = sk3 ) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f200,negated_conjecture,(
% 0.13/0.69 ( ssList(sk6)| nil = sk3 ) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f201,negated_conjecture,(
% 0.13/0.69 ( ssList(sk7)| nil = sk3 ) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f202,negated_conjecture,(
% 0.13/0.69 ( cons(sk5,nil) = sk3| nil = sk3 ) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f203,negated_conjecture,(
% 0.13/0.69 ( app(app(sk6,sk3),sk7) = sk4| nil = sk3 ) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f206,negated_conjecture,(
% 0.13/0.69 ( ~ segmentP(sk2,sk1)| ~ equalelemsP(sk1) ) ),
% 0.13/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f207,plain,(
% 0.13/0.69 equalelemsP(nil)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f214,plain,(
% 0.13/0.69 ssList(nil)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.69 fof(f215,plain,(
% 0.13/0.69 ssItem(skac3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/0.69 fof(f216,plain,(
% 0.13/0.69 ssItem(skac2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.69 fof(f219,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf82(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f13])).
% 0.13/0.69 fof(f220,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf81(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f14])).
% 0.13/0.69 fof(f221,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf80(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.69 fof(f224,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf77(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f18])).
% 0.13/0.69 fof(f225,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf76(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/0.69 fof(f226,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf75(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f20])).
% 0.13/0.69 fof(f228,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf73(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f22])).
% 0.13/0.69 fof(f229,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf72(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f23])).
% 0.13/0.69 fof(f230,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf71(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f24])).
% 0.13/0.69 fof(f233,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf68(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f27])).
% 0.13/0.69 fof(f234,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf67(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f28])).
% 0.13/0.69 fof(f235,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf66(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.69 fof(f238,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf63(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f32])).
% 0.13/0.69 fof(f239,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf62(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f33])).
% 0.13/0.69 fof(f240,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf61(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f34])).
% 0.13/0.69 fof(f243,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf58(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f37])).
% 0.13/0.69 fof(f244,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf57(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f38])).
% 0.13/0.69 fof(f245,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf56(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f39])).
% 0.13/0.69 fof(f248,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf53(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f42])).
% 0.13/0.69 fof(f249,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf52(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f43])).
% 0.13/0.69 fof(f250,plain,(
% 0.13/0.69 ![X0]: (ssList(skaf51(X0)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.69 fof(f261,plain,(
% 0.13/0.69 ![X0]: (~ssItem(X0)|geq(X0,X0))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f55])).
% 0.13/0.69 fof(f262,plain,(
% 0.13/0.69 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f56])).
% 0.13/0.69 fof(f263,plain,(
% 0.13/0.69 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f57])).
% 0.13/0.69 fof(f268,plain,(
% 0.13/0.69 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/0.69 fof(f270,plain,(
% 0.13/0.69 ![X0]: (~ssItem(X0)|equalelemsP(cons(X0,nil)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f64])).
% 0.13/0.69 fof(f287,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f80])).
% 0.13/0.69 fof(f288,plain,(
% 0.13/0.69 ![X0]: (~nil=X0|~ssList(X0)|rearsegP(nil,X0))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f81])).
% 0.13/0.69 fof(f290,plain,(
% 0.13/0.69 ![X0]: (~nil=X0|~ssList(X0)|frontsegP(nil,X0))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f83])).
% 0.13/0.69 fof(f316,plain,(
% 0.13/0.69 ![X0,X1]: (~geq(X0,X1)|~ssItem(X1)|~ssItem(X0)|leq(X1,X0))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.69 fof(f317,plain,(
% 0.13/0.69 ![X0,X1]: (~leq(X0,X1)|~ssItem(X0)|~ssItem(X1)|geq(X1,X0))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f108])).
% 0.13/0.69 fof(f346,plain,(
% 0.13/0.69 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f127])).
% 0.13/0.69 fof(f368,plain,(
% 0.13/0.69 ![X0,X1]: (~nil=X0|~nil=X1|~ssList(X1)|~ssList(X0)|app(X0,X1)=nil)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f145])).
% 0.13/0.69 fof(f376,plain,(
% 0.13/0.69 ![V,W]: (((![U]: ((~app(U,V)=app(U,W)|~ssList(V))|~ssList(U)))|~ssList(W))|V=W)),
% 0.13/0.69 inference(miniscoping,[status(thm)],[f150])).
% 0.13/0.69 fof(f377,plain,(
% 0.13/0.69 ![X0,X1,X2]: (~app(X0,X1)=app(X0,X2)|~ssList(X1)|~ssList(X0)|~ssList(X2)|X1=X2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f376])).
% 0.13/0.69 fof(f380,plain,(
% 0.13/0.69 ![U,W]: (((![V]: (((~segmentP(U,V)|~segmentP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|segmentP(U,W))),
% 0.13/0.69 inference(miniscoping,[status(thm)],[f152])).
% 0.13/0.69 fof(f381,plain,(
% 0.13/0.69 ![X0,X1,X2]: (~segmentP(X0,X1)|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|segmentP(X0,X2))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f380])).
% 0.13/0.69 fof(f407,plain,(
% 0.13/0.69 ![U,W]: ((![V]: ((![X]: (((~cons(U,V)=cons(W,X)|~ssItem(W))|~ssItem(U))|~ssList(X)))|~ssList(V)))|U=W)),
% 0.13/0.69 inference(miniscoping,[status(thm)],[f170])).
% 0.13/0.69 fof(f408,plain,(
% 0.13/0.69 ![X0,X1,X2,X3]: (~cons(X0,X1)=cons(X2,X3)|~ssItem(X2)|~ssItem(X0)|~ssList(X3)|~ssList(X1)|X0=X2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f407])).
% 0.13/0.69 fof(f412,plain,(
% 0.13/0.69 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 0.13/0.69 inference(miniscoping,[status(thm)],[f173])).
% 0.13/0.69 fof(f413,plain,(
% 0.13/0.69 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f412])).
% 0.13/0.69 fof(f439,plain,(
% 0.13/0.69 ssList(sk3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f188])).
% 0.13/0.69 fof(f440,plain,(
% 0.13/0.69 ssList(sk4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f189])).
% 0.13/0.69 fof(f441,plain,(
% 0.13/0.69 sk2=sk4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f190])).
% 0.13/0.69 fof(f442,plain,(
% 0.13/0.69 sk1=sk3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f191])).
% 0.13/0.69 fof(f444,plain,(
% 0.13/0.69 ssItem(sk5)|nil=sk3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f193])).
% 0.13/0.69 fof(f453,plain,(
% 0.13/0.69 ssList(sk6)|nil=sk3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f200])).
% 0.13/0.69 fof(f454,plain,(
% 0.13/0.69 ssList(sk7)|nil=sk3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f201])).
% 0.13/0.69 fof(f455,plain,(
% 0.13/0.69 cons(sk5,nil)=sk3|nil=sk3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f202])).
% 0.13/0.69 fof(f456,plain,(
% 0.13/0.69 app(app(sk6,sk3),sk7)=sk4|nil=sk3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f203])).
% 0.13/0.69 fof(f461,plain,(
% 0.13/0.69 ~segmentP(sk2,sk1)|~equalelemsP(sk1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f206])).
% 0.13/0.69 fof(f469,definition,(
% 0.13/0.69 sQ2_spl <=> (ssItem(sk5))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f470,plain,(
% 0.13/0.69 ssItem(sk5)|~sQ2_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f469])).
% 0.13/0.69 fof(f476,definition,(
% 0.13/0.69 sQ4_spl <=> (nil=sk3)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f477,plain,(
% 0.13/0.69 nil=sk3|~sQ4_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f476])).
% 0.13/0.69 fof(f479,plain,(
% 0.13/0.69 sQ2_spl|sQ4_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f444,f469,f476])).
% 0.13/0.69 fof(f480,definition,(
% 0.13/0.69 sQ5_spl <=> (ssList(sk6))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f484,definition,(
% 0.13/0.69 sQ6_spl <=> (ssList(sk7))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f488,definition,(
% 0.13/0.69 sQ7_spl <=> (cons(sk5,nil)=sk3)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f489,plain,(
% 0.13/0.69 cons(sk5,nil)=sk3|~sQ7_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f488])).
% 0.13/0.69 fof(f492,definition,(
% 0.13/0.69 sQ8_spl <=> (app(app(sk6,sk3),sk7)=sk4)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f493,plain,(
% 0.13/0.69 app(app(sk6,sk3),sk7)=sk4|~sQ8_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f492])).
% 0.13/0.69 fof(f504,plain,(
% 0.13/0.69 sQ5_spl|sQ4_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f453,f480,f476])).
% 0.13/0.69 fof(f505,plain,(
% 0.13/0.69 sQ6_spl|sQ4_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f454,f484,f476])).
% 0.13/0.69 fof(f506,plain,(
% 0.13/0.69 sQ7_spl|sQ4_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f455,f488,f476])).
% 0.13/0.69 fof(f507,plain,(
% 0.13/0.69 sQ8_spl|sQ4_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f456,f492,f476])).
% 0.13/0.69 fof(f510,definition,(
% 0.13/0.69 sQ11_spl <=> (segmentP(sk2,sk1))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f512,plain,(
% 0.13/0.69 ~segmentP(sk2,sk1)|sQ11_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f510])).
% 0.13/0.69 fof(f513,definition,(
% 0.13/0.69 sQ12_spl <=> (equalelemsP(sk1))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f515,plain,(
% 0.13/0.69 ~equalelemsP(sk1)|sQ12_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f513])).
% 0.13/0.69 fof(f516,plain,(
% 0.13/0.69 ~sQ11_spl|~sQ12_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f461,f510,f513])).
% 0.13/0.69 fof(f518,plain,(
% 0.13/0.69 ~ssList(nil)|rearsegP(nil,nil)),
% 0.13/0.69 inference(destructive_equality_resolution,[status(thm)],[f288])).
% 0.13/0.69 fof(f519,plain,(
% 0.13/0.69 ~ssList(nil)|frontsegP(nil,nil)),
% 0.13/0.69 inference(destructive_equality_resolution,[status(thm)],[f290])).
% 0.13/0.69 fof(f533,plain,(
% 0.13/0.69 ~ssList(nil)|~ssList(nil)|app(nil,nil)=nil),
% 0.13/0.69 inference(destructive_equality_resolution,[status(thm)],[f368])).
% 0.13/0.69 fof(f534,plain,(
% 0.13/0.69 ~ssList(nil)|app(nil,nil)=nil),
% 0.13/0.69 inference(duplicate_literals_removal,[status(thm)],[f533])).
% 0.13/0.69 fof(f535,plain,(
% 0.13/0.69 ![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.69 inference(destructive_equality_resolution,[status(thm)],[f413])).
% 0.13/0.69 fof(f549,plain,(
% 0.13/0.69 equalelemsP(sk3)|~sQ4_spl),
% 0.13/0.69 inference(backward_demodulation,[status(thm)],[f477,f207])).
% 0.13/0.69 fof(f554,plain,(
% 0.13/0.69 ~segmentP(sk4,sk1)|sQ11_spl),
% 0.13/0.69 inference(forward_demodulation,[status(thm)],[f441,f512])).
% 0.13/0.69 fof(f556,plain,(
% 0.13/0.69 segmentP(sk4,sk4)),
% 0.13/0.69 inference(resolution,[status(thm)],[f263,f440])).
% 0.13/0.69 fof(f559,plain,(
% 0.13/0.69 segmentP(sk4,nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f262,f440])).
% 0.13/0.69 fof(f564,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf82(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f219,f262])).
% 0.13/0.69 fof(f566,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf81(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f220,f262])).
% 0.13/0.69 fof(f568,plain,(
% 0.13/0.69 ~equalelemsP(sk3)|sQ12_spl),
% 0.13/0.69 inference(backward_demodulation,[status(thm)],[f442,f515])).
% 0.13/0.69 fof(f569,plain,(
% 0.13/0.69 $false|~sQ4_spl|sQ12_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f568,f549])).
% 0.13/0.69 fof(f570,plain,(
% 0.13/0.69 ~sQ4_spl|sQ12_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f569])).
% 0.13/0.69 fof(f571,plain,(
% 0.13/0.69 ~segmentP(sk4,sk3)|sQ11_spl),
% 0.13/0.69 inference(forward_demodulation,[status(thm)],[f442,f554])).
% 0.13/0.69 fof(f573,plain,(
% 0.13/0.69 segmentP(sk3,sk3)),
% 0.13/0.69 inference(resolution,[status(thm)],[f439,f263])).
% 0.13/0.69 fof(f574,plain,(
% 0.13/0.69 segmentP(nil,nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f214,f262])).
% 0.13/0.69 fof(f577,plain,(
% 0.13/0.69 equalelemsP(cons(sk5,nil))|~sQ2_spl),
% 0.13/0.69 inference(resolution,[status(thm)],[f270,f470])).
% 0.13/0.69 fof(f580,plain,(
% 0.13/0.69 equalelemsP(sk3)|~sQ7_spl|~sQ2_spl),
% 0.13/0.69 inference(forward_demodulation,[status(thm)],[f489,f577])).
% 0.13/0.69 fof(f581,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf80(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f221,f262])).
% 0.13/0.69 fof(f585,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf77(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f224,f262])).
% 0.13/0.69 fof(f587,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf76(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f225,f262])).
% 0.13/0.69 fof(f589,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf75(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f226,f262])).
% 0.13/0.69 fof(f592,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf73(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f228,f262])).
% 0.13/0.69 fof(f594,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf72(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f229,f262])).
% 0.13/0.69 fof(f596,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf71(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f230,f262])).
% 0.13/0.69 fof(f600,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf68(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f233,f262])).
% 0.13/0.69 fof(f602,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf67(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f234,f262])).
% 0.13/0.69 fof(f604,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf66(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f235,f262])).
% 0.13/0.69 fof(f644,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf63(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f238,f262])).
% 0.13/0.69 fof(f648,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf62(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f239,f262])).
% 0.13/0.69 fof(f652,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf61(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f240,f262])).
% 0.13/0.69 fof(f658,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf58(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f243,f262])).
% 0.13/0.69 fof(f662,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf57(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f244,f262])).
% 0.13/0.69 fof(f666,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf56(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f245,f262])).
% 0.13/0.69 fof(f672,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf53(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f248,f262])).
% 0.13/0.69 fof(f676,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf52(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f249,f262])).
% 0.13/0.69 fof(f680,plain,(
% 0.13/0.69 ![X0]: (segmentP(skaf51(X0),nil))),
% 0.13/0.69 inference(resolution,[status(thm)],[f250,f262])).
% 0.13/0.69 fof(f693,plain,(
% 0.13/0.69 ~ssList(nil)|nil=nil),
% 0.13/0.69 inference(resolution,[status(thm)],[f287,f574])).
% 0.13/0.69 fof(f694,definition,(
% 0.13/0.69 sQ13_spl <=> (ssList(nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f696,plain,(
% 0.13/0.69 ~ssList(nil)|sQ13_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f694])).
% 0.13/0.69 fof(f697,definition,(
% 0.13/0.69 sQ14_spl <=> (nil=nil)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f700,plain,(
% 0.13/0.69 ~sQ13_spl|sQ14_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f693,f694,f697])).
% 0.13/0.69 fof(f701,plain,(
% 0.13/0.69 $false|sQ13_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f696,f214])).
% 0.13/0.69 fof(f702,plain,(
% 0.13/0.69 sQ13_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f701])).
% 0.13/0.69 fof(f771,plain,(
% 0.13/0.69 segmentP(sk4,sk3)|~sQ4_spl),
% 0.13/0.69 inference(backward_demodulation,[status(thm)],[f477,f559])).
% 0.13/0.69 fof(f782,plain,(
% 0.13/0.69 $false|sQ11_spl|~sQ4_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f771,f571])).
% 0.13/0.69 fof(f783,plain,(
% 0.13/0.69 sQ11_spl|~sQ4_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f782])).
% 0.13/0.69 fof(f810,plain,(
% 0.13/0.69 geq(skac2,skac2)),
% 0.13/0.69 inference(resolution,[status(thm)],[f261,f216])).
% 0.13/0.69 fof(f811,plain,(
% 0.13/0.69 geq(skac3,skac3)),
% 0.13/0.69 inference(resolution,[status(thm)],[f261,f215])).
% 0.13/0.69 fof(f1010,plain,(
% 0.13/0.69 leq(skac2,skac2)),
% 0.13/0.69 inference(resolution,[status(thm)],[f268,f216])).
% 0.13/0.69 fof(f1011,plain,(
% 0.13/0.69 leq(skac3,skac3)),
% 0.13/0.69 inference(resolution,[status(thm)],[f268,f215])).
% 0.13/0.69 fof(f1088,definition,(
% 0.13/0.69 sQ15_spl <=> (ssList(sk3))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1090,plain,(
% 0.13/0.69 ~ssList(sk3)|sQ15_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f1088])).
% 0.13/0.69 fof(f1096,definition,(
% 0.13/0.69 sQ17_spl <=> (ssList(sk4))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1098,plain,(
% 0.13/0.69 ~ssList(sk4)|sQ17_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f1096])).
% 0.13/0.69 fof(f1252,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf82(X0))|~ssList(nil)|~ssList(skaf82(X0))|skaf82(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f564])).
% 0.13/0.69 fof(f1254,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf81(X0))|~ssList(nil)|~ssList(skaf81(X0))|skaf81(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f566])).
% 0.13/0.69 fof(f1256,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf80(X0))|~ssList(nil)|~ssList(skaf80(X0))|skaf80(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f581])).
% 0.13/0.69 fof(f1258,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf77(X0))|~ssList(nil)|~ssList(skaf77(X0))|skaf77(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f585])).
% 0.13/0.69 fof(f1260,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf76(X0))|~ssList(nil)|~ssList(skaf76(X0))|skaf76(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f587])).
% 0.13/0.69 fof(f1262,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf75(X0))|~ssList(nil)|~ssList(skaf75(X0))|skaf75(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f589])).
% 0.13/0.69 fof(f1264,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf73(X0))|~ssList(nil)|~ssList(skaf73(X0))|skaf73(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f592])).
% 0.13/0.69 fof(f1266,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf72(X0))|~ssList(nil)|~ssList(skaf72(X0))|skaf72(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f594])).
% 0.13/0.69 fof(f1267,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf71(X0))|~ssList(nil)|~ssList(skaf71(X0))|skaf71(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f596])).
% 0.13/0.69 fof(f1268,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf68(X0))|~ssList(nil)|~ssList(skaf68(X0))|skaf68(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f600])).
% 0.13/0.69 fof(f1269,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf67(X0))|~ssList(nil)|~ssList(skaf67(X0))|skaf67(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f602])).
% 0.13/0.69 fof(f1270,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf66(X0))|~ssList(nil)|~ssList(skaf66(X0))|skaf66(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f604])).
% 0.13/0.69 fof(f1271,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf63(X0))|~ssList(nil)|~ssList(skaf63(X0))|skaf63(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f644])).
% 0.13/0.69 fof(f1272,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf62(X0))|~ssList(nil)|~ssList(skaf62(X0))|skaf62(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f648])).
% 0.13/0.69 fof(f1273,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf61(X0))|~ssList(nil)|~ssList(skaf61(X0))|skaf61(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f652])).
% 0.13/0.69 fof(f1274,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf58(X0))|~ssList(nil)|~ssList(skaf58(X0))|skaf58(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f658])).
% 0.13/0.69 fof(f1275,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf57(X0))|~ssList(nil)|~ssList(skaf57(X0))|skaf57(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f662])).
% 0.13/0.69 fof(f1276,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf56(X0))|~ssList(nil)|~ssList(skaf56(X0))|skaf56(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f666])).
% 0.13/0.69 fof(f1277,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf53(X0))|~ssList(nil)|~ssList(skaf53(X0))|skaf53(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f672])).
% 0.13/0.69 fof(f1278,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf52(X0))|~ssList(nil)|~ssList(skaf52(X0))|skaf52(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f676])).
% 0.13/0.69 fof(f1279,plain,(
% 0.13/0.69 ![X0]: (~segmentP(nil,skaf51(X0))|~ssList(nil)|~ssList(skaf51(X0))|skaf51(X0)=nil)),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f680])).
% 0.13/0.69 fof(f1282,plain,(
% 0.13/0.69 ~segmentP(sk3,sk3)|~ssList(sk3)|~ssList(sk3)|sk3=sk3),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f573])).
% 0.13/0.69 fof(f1288,plain,(
% 0.13/0.69 ~segmentP(sk4,sk4)|~ssList(sk4)|~ssList(sk4)|sk4=sk4),
% 0.13/0.69 inference(resolution,[status(thm)],[f346,f556])).
% 0.13/0.69 fof(f1289,definition,(
% 0.13/0.69 ![X0]: (sQ21_spl <=> (~segmentP(nil,skaf82(X0))|~ssList(skaf82(X0))|skaf82(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1292,plain,(
% 0.13/0.69 sQ21_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1252,f1289,f694])).
% 0.13/0.69 fof(f1293,definition,(
% 0.13/0.69 ![X0]: (sQ22_spl <=> (~segmentP(nil,skaf81(X0))|~ssList(skaf81(X0))|skaf81(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1296,plain,(
% 0.13/0.69 sQ22_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1254,f1293,f694])).
% 0.13/0.69 fof(f1297,definition,(
% 0.13/0.69 ![X0]: (sQ23_spl <=> (~segmentP(nil,skaf80(X0))|~ssList(skaf80(X0))|skaf80(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1300,plain,(
% 0.13/0.69 sQ23_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1256,f1297,f694])).
% 0.13/0.69 fof(f1301,definition,(
% 0.13/0.69 ![X0]: (sQ24_spl <=> (~segmentP(nil,skaf77(X0))|~ssList(skaf77(X0))|skaf77(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1304,plain,(
% 0.13/0.69 sQ24_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1258,f1301,f694])).
% 0.13/0.69 fof(f1305,definition,(
% 0.13/0.69 ![X0]: (sQ25_spl <=> (~segmentP(nil,skaf76(X0))|~ssList(skaf76(X0))|skaf76(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1308,plain,(
% 0.13/0.69 sQ25_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1260,f1305,f694])).
% 0.13/0.69 fof(f1309,definition,(
% 0.13/0.69 ![X0]: (sQ26_spl <=> (~segmentP(nil,skaf75(X0))|~ssList(skaf75(X0))|skaf75(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1312,plain,(
% 0.13/0.69 sQ26_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1262,f1309,f694])).
% 0.13/0.69 fof(f1313,definition,(
% 0.13/0.69 ![X0]: (sQ27_spl <=> (~segmentP(nil,skaf73(X0))|~ssList(skaf73(X0))|skaf73(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1316,plain,(
% 0.13/0.69 sQ27_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1264,f1313,f694])).
% 0.13/0.69 fof(f1317,definition,(
% 0.13/0.69 ![X0]: (sQ28_spl <=> (~segmentP(nil,skaf72(X0))|~ssList(skaf72(X0))|skaf72(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1320,plain,(
% 0.13/0.69 sQ28_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1266,f1317,f694])).
% 0.13/0.69 fof(f1321,definition,(
% 0.13/0.69 ![X0]: (sQ29_spl <=> (~segmentP(nil,skaf71(X0))|~ssList(skaf71(X0))|skaf71(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1324,plain,(
% 0.13/0.69 sQ29_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1267,f1321,f694])).
% 0.13/0.69 fof(f1325,definition,(
% 0.13/0.69 ![X0]: (sQ30_spl <=> (~segmentP(nil,skaf68(X0))|~ssList(skaf68(X0))|skaf68(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1328,plain,(
% 0.13/0.69 sQ30_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1268,f1325,f694])).
% 0.13/0.69 fof(f1329,definition,(
% 0.13/0.69 ![X0]: (sQ31_spl <=> (~segmentP(nil,skaf67(X0))|~ssList(skaf67(X0))|skaf67(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1332,plain,(
% 0.13/0.69 sQ31_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1269,f1329,f694])).
% 0.13/0.69 fof(f1333,definition,(
% 0.13/0.69 ![X0]: (sQ32_spl <=> (~segmentP(nil,skaf66(X0))|~ssList(skaf66(X0))|skaf66(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1336,plain,(
% 0.13/0.69 sQ32_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1270,f1333,f694])).
% 0.13/0.69 fof(f1337,definition,(
% 0.13/0.69 ![X0]: (sQ33_spl <=> (~segmentP(nil,skaf63(X0))|~ssList(skaf63(X0))|skaf63(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1340,plain,(
% 0.13/0.69 sQ33_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1271,f1337,f694])).
% 0.13/0.69 fof(f1341,definition,(
% 0.13/0.69 ![X0]: (sQ34_spl <=> (~segmentP(nil,skaf62(X0))|~ssList(skaf62(X0))|skaf62(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1344,plain,(
% 0.13/0.69 sQ34_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1272,f1341,f694])).
% 0.13/0.69 fof(f1345,definition,(
% 0.13/0.69 ![X0]: (sQ35_spl <=> (~segmentP(nil,skaf61(X0))|~ssList(skaf61(X0))|skaf61(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1348,plain,(
% 0.13/0.69 sQ35_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1273,f1345,f694])).
% 0.13/0.69 fof(f1349,definition,(
% 0.13/0.69 ![X0]: (sQ36_spl <=> (~segmentP(nil,skaf58(X0))|~ssList(skaf58(X0))|skaf58(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1352,plain,(
% 0.13/0.69 sQ36_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1274,f1349,f694])).
% 0.13/0.69 fof(f1353,definition,(
% 0.13/0.69 ![X0]: (sQ37_spl <=> (~segmentP(nil,skaf57(X0))|~ssList(skaf57(X0))|skaf57(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1356,plain,(
% 0.13/0.69 sQ37_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1275,f1353,f694])).
% 0.13/0.69 fof(f1357,definition,(
% 0.13/0.69 ![X0]: (sQ38_spl <=> (~segmentP(nil,skaf56(X0))|~ssList(skaf56(X0))|skaf56(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1360,plain,(
% 0.13/0.69 sQ38_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1276,f1357,f694])).
% 0.13/0.69 fof(f1361,definition,(
% 0.13/0.69 ![X0]: (sQ39_spl <=> (~segmentP(nil,skaf53(X0))|~ssList(skaf53(X0))|skaf53(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1364,plain,(
% 0.13/0.69 sQ39_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1277,f1361,f694])).
% 0.13/0.69 fof(f1365,definition,(
% 0.13/0.69 ![X0]: (sQ40_spl <=> (~segmentP(nil,skaf52(X0))|~ssList(skaf52(X0))|skaf52(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1368,plain,(
% 0.13/0.69 sQ40_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1278,f1365,f694])).
% 0.13/0.69 fof(f1369,definition,(
% 0.13/0.69 ![X0]: (sQ41_spl <=> (~segmentP(nil,skaf51(X0))|~ssList(skaf51(X0))|skaf51(X0)=nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1372,plain,(
% 0.13/0.69 sQ41_spl|~sQ13_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1279,f1369,f694])).
% 0.13/0.69 fof(f1381,definition,(
% 0.13/0.69 sQ44_spl <=> (segmentP(sk3,sk3))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1383,plain,(
% 0.13/0.69 ~segmentP(sk3,sk3)|sQ44_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f1381])).
% 0.13/0.69 fof(f1384,definition,(
% 0.13/0.69 sQ45_spl <=> (sk3=sk3)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1387,plain,(
% 0.13/0.69 ~sQ44_spl|~sQ15_spl|sQ45_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1282,f1381,f1088,f1384])).
% 0.13/0.69 fof(f1414,definition,(
% 0.13/0.69 sQ53_spl <=> (segmentP(sk4,sk4))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1416,plain,(
% 0.13/0.69 ~segmentP(sk4,sk4)|sQ53_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f1414])).
% 0.13/0.69 fof(f1417,definition,(
% 0.13/0.69 sQ54_spl <=> (sk4=sk4)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f1420,plain,(
% 0.13/0.69 ~sQ53_spl|~sQ17_spl|sQ54_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f1288,f1414,f1096,f1417])).
% 0.13/0.69 fof(f1421,plain,(
% 0.13/0.69 $false|sQ15_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1090,f439])).
% 0.13/0.69 fof(f1422,plain,(
% 0.13/0.69 sQ15_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f1421])).
% 0.13/0.69 fof(f1423,plain,(
% 0.13/0.69 $false|sQ17_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1098,f440])).
% 0.13/0.69 fof(f1424,plain,(
% 0.13/0.69 sQ17_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f1423])).
% 0.13/0.69 fof(f1450,plain,(
% 0.13/0.69 $false|sQ44_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1383,f573])).
% 0.13/0.69 fof(f1451,plain,(
% 0.13/0.69 sQ44_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f1450])).
% 0.13/0.69 fof(f1452,plain,(
% 0.13/0.69 $false|sQ53_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1416,f556])).
% 0.13/0.69 fof(f1453,plain,(
% 0.13/0.69 sQ53_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f1452])).
% 0.13/0.69 fof(f2237,plain,(
% 0.13/0.69 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(X0)|X0=X0)),
% 0.13/0.69 inference(equality_resolution,[status(thm)],[f377])).
% 0.13/0.69 fof(f2251,definition,(
% 0.13/0.69 ![X0]: (sQ99_spl <=> (~ssList(X0)|~ssList(X0)|X0=X0))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f2254,definition,(
% 0.13/0.69 ![X1]: (sQ100_spl <=> (~ssList(X1)))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f2255,plain,(
% 0.13/0.69 ![X0]: (~ssList(X0)|~sQ100_spl)),
% 0.13/0.69 inference(component_clause,[status(thm)],[f2254])).
% 0.13/0.69 fof(f2257,plain,(
% 0.13/0.69 sQ99_spl|sQ100_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f2237,f2251,f2254])).
% 0.13/0.69 fof(f2455,plain,(
% 0.13/0.69 ![X0]: (~segmentP(X0,sk3)|~ssList(sk3)|~ssList(sk3)|~ssList(X0)|segmentP(X0,sk3))),
% 0.13/0.69 inference(resolution,[status(thm)],[f381,f573])).
% 0.13/0.69 fof(f2457,plain,(
% 0.13/0.69 ![X0]: (~segmentP(X0,sk4)|~ssList(sk4)|~ssList(sk4)|~ssList(X0)|segmentP(X0,sk4))),
% 0.13/0.69 inference(resolution,[status(thm)],[f381,f556])).
% 0.13/0.69 fof(f2490,definition,(
% 0.13/0.69 ![X0]: (sQ129_spl <=> (~segmentP(X0,sk3)|~ssList(X0)|segmentP(X0,sk3)))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f2493,plain,(
% 0.13/0.69 sQ129_spl|~sQ15_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f2455,f2490,f1088])).
% 0.13/0.69 fof(f2498,definition,(
% 0.13/0.69 ![X0]: (sQ131_spl <=> (~segmentP(X0,sk4)|~ssList(X0)|segmentP(X0,sk4)))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f2501,plain,(
% 0.13/0.69 sQ131_spl|~sQ17_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f2457,f2498,f1096])).
% 0.13/0.69 fof(f2557,definition,(
% 0.13/0.69 sQ145_spl <=> (app(nil,nil)=nil)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f2560,plain,(
% 0.13/0.69 ~sQ13_spl|sQ145_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f534,f694,f2557])).
% 0.13/0.69 fof(f2561,definition,(
% 0.13/0.69 sQ146_spl <=> (frontsegP(nil,nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f2564,plain,(
% 0.13/0.69 ~sQ13_spl|sQ146_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f519,f694,f2561])).
% 0.13/0.69 fof(f2565,definition,(
% 0.13/0.69 sQ147_spl <=> (rearsegP(nil,nil))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f2568,plain,(
% 0.13/0.69 ~sQ13_spl|sQ147_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f518,f694,f2565])).
% 0.13/0.69 fof(f3018,plain,(
% 0.13/0.69 $false|~sQ100_spl),
% 0.13/0.69 inference(backward_subsumption_resolution,[status(thm)],[f214,f2255])).
% 0.13/0.69 fof(f3051,plain,(
% 0.13/0.69 ~sQ100_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f3018])).
% 0.13/0.69 fof(f3052,plain,(
% 0.13/0.69 ![X0,X1]: (~ssItem(X0)|~ssItem(X0)|~ssList(X1)|~ssList(X1)|X0=X0)),
% 0.13/0.69 inference(equality_resolution,[status(thm)],[f408])).
% 0.13/0.69 fof(f3053,definition,(
% 0.13/0.69 ![X0]: (sQ160_spl <=> (~ssItem(X0)|~ssItem(X0)|X0=X0))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f3056,definition,(
% 0.13/0.69 ![X1]: (sQ161_spl <=> (~ssList(X1)|~ssList(X1)))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f3057,plain,(
% 0.13/0.69 ![X0]: (~ssList(X0)|~ssList(X0)|~sQ161_spl)),
% 0.13/0.69 inference(component_clause,[status(thm)],[f3056])).
% 0.13/0.69 fof(f3059,plain,(
% 0.13/0.69 sQ160_spl|sQ161_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f3052,f3053,f3056])).
% 0.13/0.69 fof(f3060,plain,(
% 0.13/0.69 ![X0]: (~ssList(X0)|~sQ161_spl)),
% 0.13/0.69 inference(duplicate_literals_removal,[status(thm)],[f3057])).
% 0.13/0.69 fof(f3098,plain,(
% 0.13/0.69 $false|~sQ161_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f440,f3060])).
% 0.13/0.69 fof(f3099,plain,(
% 0.13/0.69 ~sQ161_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f3098])).
% 0.13/0.69 fof(f3158,plain,(
% 0.13/0.69 ~ssItem(skac3)|~ssItem(skac3)|leq(skac3,skac3)),
% 0.13/0.69 inference(resolution,[status(thm)],[f316,f811])).
% 0.13/0.69 fof(f3159,plain,(
% 0.13/0.69 ~ssItem(skac2)|~ssItem(skac2)|leq(skac2,skac2)),
% 0.13/0.69 inference(resolution,[status(thm)],[f316,f810])).
% 0.13/0.69 fof(f3161,definition,(
% 0.13/0.69 sQ167_spl <=> (ssItem(skac3))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f3163,plain,(
% 0.13/0.69 ~ssItem(skac3)|sQ167_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f3161])).
% 0.13/0.69 fof(f3164,definition,(
% 0.13/0.69 sQ168_spl <=> (leq(skac3,skac3))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f3167,plain,(
% 0.13/0.69 ~sQ167_spl|sQ168_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f3158,f3161,f3164])).
% 0.13/0.69 fof(f3168,definition,(
% 0.13/0.69 sQ169_spl <=> (ssItem(skac2))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f3170,plain,(
% 0.13/0.69 ~ssItem(skac2)|sQ169_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f3168])).
% 0.13/0.69 fof(f3171,definition,(
% 0.13/0.69 sQ170_spl <=> (leq(skac2,skac2))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f3174,plain,(
% 0.13/0.69 ~sQ169_spl|sQ170_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f3159,f3168,f3171])).
% 0.13/0.69 fof(f3179,plain,(
% 0.13/0.69 $false|sQ169_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f3170,f216])).
% 0.13/0.69 fof(f3180,plain,(
% 0.13/0.69 sQ169_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f3179])).
% 0.13/0.69 fof(f3181,plain,(
% 0.13/0.69 $false|sQ167_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f3163,f215])).
% 0.13/0.69 fof(f3182,plain,(
% 0.13/0.69 sQ167_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f3181])).
% 0.13/0.69 fof(f3183,plain,(
% 0.13/0.69 ~ssItem(skac3)|~ssItem(skac3)|geq(skac3,skac3)),
% 0.13/0.69 inference(resolution,[status(thm)],[f317,f1011])).
% 0.13/0.69 fof(f3184,plain,(
% 0.13/0.69 ~ssItem(skac2)|~ssItem(skac2)|geq(skac2,skac2)),
% 0.13/0.69 inference(resolution,[status(thm)],[f317,f1010])).
% 0.13/0.69 fof(f3186,definition,(
% 0.13/0.69 sQ172_spl <=> (geq(skac3,skac3))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f3189,plain,(
% 0.13/0.69 ~sQ167_spl|sQ172_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f3183,f3161,f3186])).
% 0.13/0.69 fof(f3190,definition,(
% 0.13/0.69 sQ173_spl <=> (geq(skac2,skac2))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f3193,plain,(
% 0.13/0.69 ~sQ169_spl|sQ173_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f3184,f3168,f3190])).
% 0.13/0.69 fof(f3232,plain,(
% 0.13/0.69 ~ssList(sk7)|~ssList(sk6)|~ssList(sk3)|~ssList(sk4)|segmentP(app(app(sk6,sk3),sk7),sk3)|~sQ8_spl),
% 0.13/0.69 inference(paramodulation,[status(thm)],[f493,f535])).
% 0.13/0.69 fof(f3234,definition,(
% 0.13/0.69 sQ181_spl <=> (segmentP(app(app(sk6,sk3),sk7),sk3))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f3235,plain,(
% 0.13/0.69 segmentP(app(app(sk6,sk3),sk7),sk3)|~sQ181_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f3234])).
% 0.13/0.69 fof(f3237,plain,(
% 0.13/0.69 ~sQ6_spl|~sQ5_spl|~sQ15_spl|~sQ17_spl|sQ181_spl|~sQ8_spl),
% 0.13/0.69 inference(split_clause,[status(thm)],[f3232,f484,f480,f1088,f1096,f3234,f492])).
% 0.13/0.69 fof(f3242,plain,(
% 0.13/0.69 segmentP(sk4,sk3)|~sQ8_spl|~sQ181_spl),
% 0.13/0.69 inference(forward_demodulation,[status(thm)],[f493,f3235])).
% 0.13/0.69 fof(f3243,plain,(
% 0.13/0.69 $false|sQ11_spl|~sQ8_spl|~sQ181_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f3242,f571])).
% 0.13/0.69 fof(f3244,plain,(
% 0.13/0.69 sQ11_spl|~sQ8_spl|~sQ181_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f3243])).
% 0.13/0.69 fof(f3247,plain,(
% 0.13/0.69 $false|~sQ7_spl|~sQ2_spl|sQ12_spl),
% 0.13/0.69 inference(forward_subsumption_resolution,[status(thm)],[f568,f580])).
% 0.13/0.69 fof(f3248,plain,(
% 0.13/0.69 ~sQ7_spl|~sQ2_spl|sQ12_spl),
% 0.13/0.69 inference(contradiction_clause,[status(thm)],[f3247])).
% 0.13/0.69 fof(f3249,plain,(
% 0.13/0.69 $false),
% 0.13/0.69 inference(sat_refutation,[status(thm)],[f479,f504,f505,f506,f507,f516,f570,f700,f702,f783,f1292,f1296,f1300,f1304,f1308,f1312,f1316,f1320,f1324,f1328,f1332,f1336,f1340,f1344,f1348,f1352,f1356,f1360,f1364,f1368,f1372,f1387,f1420,f1422,f1424,f1451,f1453,f2257,f2493,f2501,f2560,f2564,f2568,f3051,f3059,f3099,f3167,f3174,f3180,f3182,f3189,f3193,f3237,f3244,f3248])).
% 0.13/0.69 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.69 % Elapsed time: 0.145439 seconds
% 0.13/0.69 % CPU time: 0.856782 seconds
% 0.13/0.69 % Total memory used: 126.031 MB
% 0.13/0.69 % Net memory used: 125.052 MB
%------------------------------------------------------------------------------