%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC354-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 : n001.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:14 PM UTC 2026
% Result : Unsatisfiable 131.79s 17.08s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC354-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.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 08:23:58 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 131.79/17.08 % Refutation found
% 131.79/17.08 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 131.79/17.08 % SZS output start CNFRefutation for theBenchmark
% 131.79/17.08 fof(f3,axiom,(
% 131.79/17.08 strictorderedP(nil) ),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f8,axiom,(
% 131.79/17.08 ssList(nil) ),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f12,axiom,(
% 131.79/17.08 (![U]: (ssItem(skaf83(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f13,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf82(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f14,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf81(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f15,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf80(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f18,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf77(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f19,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf76(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f20,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf75(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f22,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf73(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f23,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf72(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f24,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf71(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f25,axiom,(
% 131.79/17.08 (![U]: (ssItem(skaf70(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f26,axiom,(
% 131.79/17.08 (![U]: (ssItem(skaf69(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f27,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf68(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f28,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf67(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f29,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf66(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f32,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf63(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f33,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf62(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f34,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf61(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f36,axiom,(
% 131.79/17.08 (![U]: (ssItem(skaf59(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f37,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf58(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f38,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf57(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f39,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf56(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f42,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf53(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f43,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf52(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f44,axiom,(
% 131.79/17.08 (![U]: (ssList(skaf51(U)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f50,axiom,(
% 131.79/17.08 (![U,V]: (ssList(skaf46(U,V)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f51,axiom,(
% 131.79/17.08 (![U,V]: (ssList(skaf45(U,V)) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f54,axiom,(
% 131.79/17.08 skac3 != skac2 ),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f56,axiom,(
% 131.79/17.08 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f59,axiom,(
% 131.79/17.08 (![U]: (( ~ ssList(U)| rearsegP(U,U) ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f61,axiom,(
% 131.79/17.08 (![U]: (( ~ ssList(U)| frontsegP(U,U) ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f73,axiom,(
% 131.79/17.08 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f74,axiom,(
% 131.79/17.08 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f75,axiom,(
% 131.79/17.08 (![U]: (( ~ ssList(U)| ssList(tl(U))| nil = U ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f76,axiom,(
% 131.79/17.08 (![U]: (( ~ ssList(U)| ssItem(hd(U))| nil = U ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f85,axiom,(
% 131.79/17.08 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f86,axiom,(
% 131.79/17.08 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f97,axiom,(
% 131.79/17.08 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| hd(cons(U,V)) = U ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f98,axiom,(
% 131.79/17.08 (![U,V]: (( cons(U,V) != nil| ~ ssItem(U)| ~ ssList(V) ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f100,axiom,(
% 131.79/17.08 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f104,axiom,(
% 131.79/17.08 (![U]: (( ~ ssList(U)| cons(hd(U),tl(U)) = U| nil = U ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f115,axiom,(
% 131.79/17.08 (![U,V]: (( U != V| ~ neq(U,V)| ~ ssList(V)| ~ ssList(U) ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f120,axiom,(
% 131.79/17.08 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| app(cons(U,nil),V) = cons(U,V) ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f131,axiom,(
% 131.79/17.08 (![U,V]: (( ~ rearsegP(U,V)| ~ ssList(V)| ~ ssList(U)| app(skaf46(U,V),V) = U ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f132,axiom,(
% 131.79/17.08 (![U,V]: (( ~ frontsegP(U,V)| ~ ssList(V)| ~ ssList(U)| app(V,skaf45(U,V)) = U ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f173,axiom,(
% 131.79/17.08 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f186,negated_conjecture,(
% 131.79/17.08 ssList(sk1) ),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f187,negated_conjecture,(
% 131.79/17.08 ssList(sk2) ),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f190,negated_conjecture,(
% 131.79/17.08 sk2 = sk4 ),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f191,negated_conjecture,(
% 131.79/17.08 sk1 = sk3 ),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f192,negated_conjecture,(
% 131.79/17.08 ( neq(sk2,nil)| neq(sk2,nil) ) ),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f196,negated_conjecture,(
% 131.79/17.08 (![A,B]: (( ~ ssList(A)| sk3 = A| ~ ssItem(B)| cons(B,nil) != A| hd(sk4) != B| ~ neq(nil,sk4)| ~ neq(sk4,nil) ) ))),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f197,negated_conjecture,(
% 131.79/17.08 ( ~ segmentP(sk2,sk1)| ~ neq(sk4,nil) ) ),
% 131.79/17.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 131.79/17.08 fof(f200,plain,(
% 131.79/17.08 strictorderedP(nil)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f3])).
% 131.79/17.08 fof(f205,plain,(
% 131.79/17.08 ssList(nil)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f8])).
% 131.79/17.08 fof(f209,plain,(
% 131.79/17.08 ![X0]: (ssItem(skaf83(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f12])).
% 131.79/17.08 fof(f210,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf82(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f13])).
% 131.79/17.08 fof(f211,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf81(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f14])).
% 131.79/17.08 fof(f212,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf80(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f15])).
% 131.79/17.08 fof(f215,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf77(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f18])).
% 131.79/17.08 fof(f216,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf76(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f19])).
% 131.79/17.08 fof(f217,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf75(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f20])).
% 131.79/17.08 fof(f219,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf73(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f22])).
% 131.79/17.08 fof(f220,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf72(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f23])).
% 131.79/17.08 fof(f221,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf71(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f24])).
% 131.79/17.08 fof(f222,plain,(
% 131.79/17.08 ![X0]: (ssItem(skaf70(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f25])).
% 131.79/17.08 fof(f223,plain,(
% 131.79/17.08 ![X0]: (ssItem(skaf69(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f26])).
% 131.79/17.08 fof(f224,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf68(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f27])).
% 131.79/17.08 fof(f225,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf67(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f28])).
% 131.79/17.08 fof(f226,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf66(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f29])).
% 131.79/17.08 fof(f229,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf63(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f32])).
% 131.79/17.08 fof(f230,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf62(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f33])).
% 131.79/17.08 fof(f231,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf61(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f34])).
% 131.79/17.08 fof(f233,plain,(
% 131.79/17.08 ![X0]: (ssItem(skaf59(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f36])).
% 131.79/17.08 fof(f234,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf58(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f37])).
% 131.79/17.08 fof(f235,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf57(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f38])).
% 131.79/17.08 fof(f236,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf56(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f39])).
% 131.79/17.08 fof(f239,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf53(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f42])).
% 131.79/17.08 fof(f240,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf52(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f43])).
% 131.79/17.08 fof(f241,plain,(
% 131.79/17.08 ![X0]: (ssList(skaf51(X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f44])).
% 131.79/17.08 fof(f247,plain,(
% 131.79/17.08 ![X0,X1]: (ssList(skaf46(X0,X1)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f50])).
% 131.79/17.08 fof(f248,plain,(
% 131.79/17.08 ![X0,X1]: (ssList(skaf45(X0,X1)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f51])).
% 131.79/17.08 fof(f251,plain,(
% 131.79/17.08 ~skac3=skac2),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f54])).
% 131.79/17.08 fof(f253,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f56])).
% 131.79/17.08 fof(f256,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|rearsegP(X0,X0))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f59])).
% 131.79/17.08 fof(f258,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|frontsegP(X0,X0))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f61])).
% 131.79/17.08 fof(f271,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f73])).
% 131.79/17.08 fof(f272,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f74])).
% 131.79/17.08 fof(f273,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|ssList(tl(X0))|nil=X0)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f75])).
% 131.79/17.08 fof(f274,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|ssItem(hd(X0))|nil=X0)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f76])).
% 131.79/17.08 fof(f283,plain,(
% 131.79/17.08 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f85])).
% 131.79/17.08 fof(f284,plain,(
% 131.79/17.08 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f86])).
% 131.79/17.08 fof(f295,plain,(
% 131.79/17.08 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|hd(cons(X0,X1))=X0)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f97])).
% 131.79/17.08 fof(f296,plain,(
% 131.79/17.08 ![V]: ((![U]: (~cons(U,V)=nil|~ssItem(U)))|~ssList(V))),
% 131.79/17.08 inference(miniscoping,[status(thm)],[f98])).
% 131.79/17.08 fof(f297,plain,(
% 131.79/17.08 ![X0,X1]: (~cons(X0,X1)=nil|~ssItem(X0)|~ssList(X1))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f296])).
% 131.79/17.08 fof(f300,plain,(
% 131.79/17.08 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f100])).
% 131.79/17.08 fof(f304,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|cons(hd(X0),tl(X0))=X0|nil=X0)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f104])).
% 131.79/17.08 fof(f318,plain,(
% 131.79/17.08 ![U]: ((![V]: ((~U=V|~neq(U,V))|~ssList(V)))|~ssList(U))),
% 131.79/17.08 inference(miniscoping,[status(thm)],[f115])).
% 131.79/17.08 fof(f319,plain,(
% 131.79/17.08 ![X0,X1]: (~X0=X1|~neq(X0,X1)|~ssList(X1)|~ssList(X0))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f318])).
% 131.79/17.08 fof(f328,plain,(
% 131.79/17.08 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(cons(X0,nil),X1)=cons(X0,X1))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f120])).
% 131.79/17.08 fof(f341,plain,(
% 131.79/17.08 ![X0,X1]: (~rearsegP(X0,X1)|~ssList(X1)|~ssList(X0)|app(skaf46(X0,X1),X1)=X0)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f131])).
% 131.79/17.08 fof(f342,plain,(
% 131.79/17.08 ![X0,X1]: (~frontsegP(X0,X1)|~ssList(X1)|~ssList(X0)|app(X1,skaf45(X0,X1))=X0)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f132])).
% 131.79/17.08 fof(f403,plain,(
% 131.79/17.08 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 131.79/17.08 inference(miniscoping,[status(thm)],[f173])).
% 131.79/17.08 fof(f404,plain,(
% 131.79/17.08 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f403])).
% 131.79/17.08 fof(f428,plain,(
% 131.79/17.08 ssList(sk1)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f186])).
% 131.79/17.08 fof(f429,plain,(
% 131.79/17.08 ssList(sk2)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f187])).
% 131.79/17.08 fof(f432,plain,(
% 131.79/17.08 sk2=sk4),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f190])).
% 131.79/17.08 fof(f433,plain,(
% 131.79/17.08 sk1=sk3),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f191])).
% 131.79/17.08 fof(f434,plain,(
% 131.79/17.08 neq(sk2,nil)|neq(sk2,nil)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f192])).
% 131.79/17.08 fof(f439,plain,(
% 131.79/17.08 ((![B]: ((![A]: (((~ssList(A)|sk3=A)|~ssItem(B))|~cons(B,nil)=A))|~hd(sk4)=B))|~neq(nil,sk4))|~neq(sk4,nil)),
% 131.79/17.08 inference(miniscoping,[status(thm)],[f196])).
% 131.79/17.08 fof(f440,plain,(
% 131.79/17.08 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1|~neq(nil,sk4)|~neq(sk4,nil))),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f439])).
% 131.79/17.08 fof(f441,plain,(
% 131.79/17.08 ~segmentP(sk2,sk1)|~neq(sk4,nil)),
% 131.79/17.08 inference(cnf_transformation,[status(thm)],[f197])).
% 131.79/17.08 fof(f449,definition,(
% 131.79/17.08 sQ2_spl <=> (neq(sk2,nil))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f450,plain,(
% 131.79/17.08 neq(sk2,nil)|~sQ2_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f449])).
% 131.79/17.08 fof(f452,plain,(
% 131.79/17.08 sQ2_spl),
% 131.79/17.08 inference(split_clause,[status(thm)],[f434,f449])).
% 131.79/17.08 fof(f453,definition,(
% 131.79/17.08 sQ3_spl <=> (neq(sk4,nil))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f455,plain,(
% 131.79/17.08 ~neq(sk4,nil)|sQ3_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f453])).
% 131.79/17.08 fof(f457,definition,(
% 131.79/17.08 ![X0,X1]: (sQ4_spl <=> (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f458,plain,(
% 131.79/17.08 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1|~sQ4_spl)),
% 131.79/17.08 inference(component_clause,[status(thm)],[f457])).
% 131.79/17.08 fof(f460,definition,(
% 131.79/17.08 sQ5_spl <=> (neq(nil,sk4))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f462,plain,(
% 131.79/17.08 ~neq(nil,sk4)|sQ5_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f460])).
% 131.79/17.08 fof(f464,definition,(
% 131.79/17.08 sQ6_spl <=> (segmentP(sk2,sk1))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f468,plain,(
% 131.79/17.08 sQ4_spl|~sQ5_spl|~sQ3_spl),
% 131.79/17.08 inference(split_clause,[status(thm)],[f440,f457,f460,f453])).
% 131.79/17.08 fof(f469,plain,(
% 131.79/17.08 ~sQ6_spl|~sQ3_spl),
% 131.79/17.08 inference(split_clause,[status(thm)],[f441,f464,f453])).
% 131.79/17.08 fof(f477,plain,(
% 131.79/17.08 ![X1]: (~neq(X1,X1)|~ssList(X1)|~ssList(X1))),
% 131.79/17.08 inference(destructive_equality_resolution,[status(thm)],[f319])).
% 131.79/17.08 fof(f478,plain,(
% 131.79/17.08 ![X0]: (~neq(X0,X0)|~ssList(X0))),
% 131.79/17.08 inference(duplicate_literals_removal,[status(thm)],[f477])).
% 131.79/17.08 fof(f488,plain,(
% 131.79/17.08 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 131.79/17.08 inference(destructive_equality_resolution,[status(thm)],[f404])).
% 131.79/17.08 fof(f499,plain,(
% 131.79/17.08 ~neq(sk2,nil)|sQ3_spl),
% 131.79/17.08 inference(backward_demodulation,[status(thm)],[f432,f455])).
% 131.79/17.08 fof(f501,plain,(
% 131.79/17.08 $false|~sQ2_spl|sQ3_spl),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f499,f450])).
% 131.79/17.08 fof(f502,plain,(
% 131.79/17.08 ~sQ2_spl|sQ3_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f501])).
% 131.79/17.08 fof(f503,plain,(
% 131.79/17.08 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk2)=X1|~sQ4_spl)),
% 131.79/17.08 inference(forward_demodulation,[status(thm)],[f432,f458])).
% 131.79/17.08 fof(f504,plain,(
% 131.79/17.08 ~ssList(cons(hd(sk2),nil))|sk3=cons(hd(sk2),nil)|~ssItem(hd(sk2))|~sQ4_spl),
% 131.79/17.08 inference(destructive_equality_resolution,[status(thm)],[f503])).
% 131.79/17.08 fof(f519,plain,(
% 131.79/17.08 ~ssList(cons(hd(sk2),nil))|sk1=cons(hd(sk2),nil)|~ssItem(hd(sk2))|~sQ4_spl),
% 131.79/17.08 inference(forward_demodulation,[status(thm)],[f433,f504])).
% 131.79/17.08 fof(f520,plain,(
% 131.79/17.08 ~ssList(cons(hd(sk2),nil))|sk1=cons(hd(sk2),nil)|~ssList(sk2)|nil=sk2|~sQ4_spl),
% 131.79/17.08 inference(resolution,[status(thm)],[f519,f274])).
% 131.79/17.08 fof(f521,definition,(
% 131.79/17.08 sQ7_spl <=> (ssList(cons(hd(sk2),nil)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f523,plain,(
% 131.79/17.08 ~ssList(cons(hd(sk2),nil))|sQ7_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f521])).
% 131.79/17.08 fof(f524,definition,(
% 131.79/17.08 sQ8_spl <=> (sk1=cons(hd(sk2),nil))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f525,plain,(
% 131.79/17.08 sk1=cons(hd(sk2),nil)|~sQ8_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f524])).
% 131.79/17.08 fof(f527,definition,(
% 131.79/17.08 sQ9_spl <=> (ssList(sk2))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f529,plain,(
% 131.79/17.08 ~ssList(sk2)|sQ9_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f527])).
% 131.79/17.08 fof(f530,definition,(
% 131.79/17.08 sQ10_spl <=> (nil=sk2)),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f531,plain,(
% 131.79/17.08 nil=sk2|~sQ10_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f530])).
% 131.79/17.08 fof(f533,plain,(
% 131.79/17.08 ~sQ7_spl|sQ8_spl|~sQ9_spl|sQ10_spl|~sQ4_spl),
% 131.79/17.08 inference(split_clause,[status(thm)],[f520,f521,f524,f527,f530,f457])).
% 131.79/17.08 fof(f534,plain,(
% 131.79/17.08 ~neq(nil,sk2)|sQ5_spl),
% 131.79/17.08 inference(forward_demodulation,[status(thm)],[f432,f462])).
% 131.79/17.08 fof(f539,definition,(
% 131.79/17.08 sQ11_spl <=> (ssList(nil))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f541,plain,(
% 131.79/17.08 ~ssList(nil)|sQ11_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f539])).
% 131.79/17.08 fof(f547,plain,(
% 131.79/17.08 $false|sQ11_spl),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f541,f205])).
% 131.79/17.08 fof(f548,plain,(
% 131.79/17.08 sQ11_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f547])).
% 131.79/17.08 fof(f556,plain,(
% 131.79/17.08 app(nil,nil)=nil),
% 131.79/17.08 inference(resolution,[status(thm)],[f271,f205])).
% 131.79/17.08 fof(f557,plain,(
% 131.79/17.08 app(sk2,nil)=sk2),
% 131.79/17.08 inference(resolution,[status(thm)],[f271,f429])).
% 131.79/17.08 fof(f558,plain,(
% 131.79/17.08 app(sk1,nil)=sk1),
% 131.79/17.08 inference(resolution,[status(thm)],[f271,f428])).
% 131.79/17.08 fof(f568,plain,(
% 131.79/17.08 app(nil,sk1)=sk1),
% 131.79/17.08 inference(resolution,[status(thm)],[f272,f428])).
% 131.79/17.08 fof(f583,plain,(
% 131.79/17.08 neq(nil,nil)|~sQ10_spl|~sQ2_spl),
% 131.79/17.08 inference(backward_demodulation,[status(thm)],[f531,f450])).
% 131.79/17.08 fof(f589,definition,(
% 131.79/17.08 sQ13_spl <=> (ssItem(hd(sk2)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f590,plain,(
% 131.79/17.08 ssItem(hd(sk2))|~sQ13_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f589])).
% 131.79/17.08 fof(f601,plain,(
% 131.79/17.08 ~ssList(sk2)|~ssList(nil)|nil=sk2|sQ5_spl),
% 131.79/17.08 inference(resolution,[status(thm)],[f534,f300])).
% 131.79/17.08 fof(f609,plain,(
% 131.79/17.08 ~sQ9_spl|~sQ11_spl|sQ10_spl|sQ5_spl),
% 131.79/17.08 inference(split_clause,[status(thm)],[f601,f527,f539,f530,f460])).
% 131.79/17.08 fof(f610,plain,(
% 131.79/17.08 $false|sQ9_spl),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f529,f429])).
% 131.79/17.08 fof(f611,plain,(
% 131.79/17.08 sQ9_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f610])).
% 131.79/17.08 fof(f613,plain,(
% 131.79/17.08 ![X0,X1]: (~cons(skaf83(X0),X1)=nil|~ssList(X1))),
% 131.79/17.08 inference(resolution,[status(thm)],[f209,f297])).
% 131.79/17.08 fof(f643,definition,(
% 131.79/17.08 sQ16_spl <=> (ssList(sk1))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f681,plain,(
% 131.79/17.08 ~ssList(nil)|~sQ10_spl|~sQ2_spl),
% 131.79/17.08 inference(resolution,[status(thm)],[f583,f478])).
% 131.79/17.08 fof(f682,plain,(
% 131.79/17.08 ~sQ11_spl|~sQ10_spl|~sQ2_spl),
% 131.79/17.08 inference(split_clause,[status(thm)],[f681,f539,f530,f449])).
% 131.79/17.08 fof(f727,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|hd(cons(hd(sk2),X0))=hd(sk2)|~sQ13_spl)),
% 131.79/17.08 inference(resolution,[status(thm)],[f590,f295])).
% 131.79/17.08 fof(f786,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|ssList(app(sk2,X0)))),
% 131.79/17.08 inference(resolution,[status(thm)],[f283,f429])).
% 131.79/17.08 fof(f795,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|ssList(app(sk1,X0)))),
% 131.79/17.08 inference(resolution,[status(thm)],[f283,f428])).
% 131.79/17.08 fof(f1133,plain,(
% 131.79/17.08 hd(cons(hd(sk2),nil))=hd(sk2)|~sQ13_spl),
% 131.79/17.08 inference(resolution,[status(thm)],[f727,f205])).
% 131.79/17.08 fof(f1204,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1))),
% 131.79/17.08 inference(paramodulation,[status(thm)],[f568,f488])).
% 131.79/17.08 fof(f1218,definition,(
% 131.79/17.08 ![X0]: (sQ36_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f1219,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)|~sQ36_spl)),
% 131.79/17.08 inference(component_clause,[status(thm)],[f1218])).
% 131.79/17.08 fof(f1221,plain,(
% 131.79/17.08 sQ36_spl|~sQ11_spl|~sQ16_spl),
% 131.79/17.08 inference(split_clause,[status(thm)],[f1204,f1218,f539,f643])).
% 131.79/17.08 fof(f1227,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(sk1,X0),sk1)|~sQ36_spl)),
% 131.79/17.08 inference(forward_demodulation,[status(thm)],[f568,f1219])).
% 131.79/17.08 fof(f1228,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~sQ36_spl)),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f1227,f795])).
% 131.79/17.08 fof(f1288,definition,(
% 131.79/17.08 sQ42_spl <=> (strictorderedP(nil))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f1290,plain,(
% 131.79/17.08 ~strictorderedP(nil)|sQ42_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f1288])).
% 131.79/17.08 fof(f1468,plain,(
% 131.79/17.08 ~ssItem(hd(sk2))|~ssList(nil)|sQ7_spl),
% 131.79/17.08 inference(resolution,[status(thm)],[f523,f284])).
% 131.79/17.08 fof(f1469,plain,(
% 131.79/17.08 ~sQ13_spl|~sQ11_spl|sQ7_spl),
% 131.79/17.08 inference(split_clause,[status(thm)],[f1468,f589,f539,f521])).
% 131.79/17.08 fof(f1777,plain,(
% 131.79/17.08 ~ssItem(hd(sk2))|~ssList(nil)|ssList(sk1)|~sQ8_spl),
% 131.79/17.08 inference(paramodulation,[status(thm)],[f525,f284])).
% 131.79/17.08 fof(f1807,plain,(
% 131.79/17.08 ~sQ13_spl|~sQ11_spl|sQ16_spl|~sQ8_spl),
% 131.79/17.08 inference(split_clause,[status(thm)],[f1777,f589,f539,f643,f524])).
% 131.79/17.08 fof(f2154,plain,(
% 131.79/17.08 sk1=cons(hd(sk1),nil)|~sQ13_spl|~sQ8_spl),
% 131.79/17.08 inference(backward_demodulation,[status(thm)],[f2155,f525])).
% 131.79/17.08 fof(f2155,plain,(
% 131.79/17.08 hd(sk1)=hd(sk2)|~sQ8_spl|~sQ13_spl),
% 131.79/17.08 inference(forward_demodulation,[status(thm)],[f525,f1133])).
% 131.79/17.08 fof(f2248,definition,(
% 131.79/17.08 ![X0]: (sQ79_spl <=> (~ssList(X0)|~ssList(X0)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f2249,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|~ssList(X0)|~sQ79_spl)),
% 131.79/17.08 inference(component_clause,[status(thm)],[f2248])).
% 131.79/17.08 fof(f2255,plain,(
% 131.79/17.08 ssItem(hd(sk1))|~sQ8_spl|~sQ13_spl),
% 131.79/17.08 inference(forward_demodulation,[status(thm)],[f2155,f590])).
% 131.79/17.08 fof(f2487,definition,(
% 131.79/17.08 ![X0]: (sQ85_spl <=> (~ssItem(X0)|~ssItem(X0)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f2488,plain,(
% 131.79/17.08 ![X0]: (~ssItem(X0)|~ssItem(X0)|~sQ85_spl)),
% 131.79/17.08 inference(component_clause,[status(thm)],[f2487])).
% 131.79/17.08 fof(f2494,plain,(
% 131.79/17.08 ![X0]: (~ssItem(X0)|~sQ85_spl)),
% 131.79/17.08 inference(duplicate_literals_removal,[status(thm)],[f2488])).
% 131.79/17.08 fof(f2495,plain,(
% 131.79/17.08 $false|~sQ85_spl),
% 131.79/17.08 inference(backward_subsumption_resolution,[status(thm)],[f233,f2494])).
% 131.79/17.08 fof(f2499,plain,(
% 131.79/17.08 ~sQ85_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f2495])).
% 131.79/17.08 fof(f5053,plain,(
% 131.79/17.08 cons(hd(sk2),tl(sk2))=sk2|nil=sk2),
% 131.79/17.08 inference(resolution,[status(thm)],[f304,f429])).
% 131.79/17.08 fof(f5065,definition,(
% 131.79/17.08 sQ141_spl <=> (cons(hd(sk2),tl(sk2))=sk2)),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f5066,plain,(
% 131.79/17.08 cons(hd(sk2),tl(sk2))=sk2|~sQ141_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f5065])).
% 131.79/17.08 fof(f5068,plain,(
% 131.79/17.08 sQ141_spl|sQ10_spl),
% 131.79/17.08 inference(split_clause,[status(thm)],[f5053,f5065,f530])).
% 131.79/17.08 fof(f5073,plain,(
% 131.79/17.08 cons(hd(sk1),tl(sk2))=sk2|~sQ8_spl|~sQ13_spl|~sQ141_spl),
% 131.79/17.08 inference(forward_demodulation,[status(thm)],[f2155,f5066])).
% 131.79/17.08 fof(f5143,definition,(
% 131.79/17.08 sQ145_spl <=> (cons(skaf83(nil),skaf82(nil))=nil)),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f5144,plain,(
% 131.79/17.08 cons(skaf83(nil),skaf82(nil))=nil|~sQ145_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f5143])).
% 131.79/17.08 fof(f5159,definition,(
% 131.79/17.08 sQ147_spl <=> (ssList(tl(sk2)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f5160,plain,(
% 131.79/17.08 ssList(tl(sk2))|~sQ147_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f5159])).
% 131.79/17.08 fof(f5181,definition,(
% 131.79/17.08 sQ152_spl <=> (ssList(skaf82(sk1)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f5183,plain,(
% 131.79/17.08 ~ssList(skaf82(sk1))|sQ152_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f5181])).
% 131.79/17.08 fof(f5185,definition,(
% 131.79/17.08 sQ153_spl <=> (ssItem(skaf83(sk1)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f5187,plain,(
% 131.79/17.08 ~ssItem(skaf83(sk1))|sQ153_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f5185])).
% 131.79/17.08 fof(f5192,plain,(
% 131.79/17.08 $false|sQ152_spl),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f5183,f210])).
% 131.79/17.08 fof(f5193,plain,(
% 131.79/17.08 sQ152_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f5192])).
% 131.79/17.08 fof(f5196,definition,(
% 131.79/17.08 sQ155_spl <=> (ssList(skaf82(sk2)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f5198,plain,(
% 131.79/17.08 ~ssList(skaf82(sk2))|sQ155_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f5196])).
% 131.79/17.08 fof(f5200,definition,(
% 131.79/17.08 sQ156_spl <=> (ssItem(skaf83(sk2)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f5202,plain,(
% 131.79/17.08 ~ssItem(skaf83(sk2))|sQ156_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f5200])).
% 131.79/17.08 fof(f5207,plain,(
% 131.79/17.08 $false|sQ155_spl),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f5198,f210])).
% 131.79/17.08 fof(f5208,plain,(
% 131.79/17.08 sQ155_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f5207])).
% 131.79/17.08 fof(f5209,plain,(
% 131.79/17.08 ~ssList(skaf82(nil))|~sQ145_spl),
% 131.79/17.08 inference(resolution,[status(thm)],[f5144,f613])).
% 131.79/17.08 fof(f5212,plain,(
% 131.79/17.08 $false|~sQ145_spl),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f5209,f210])).
% 131.79/17.08 fof(f5213,plain,(
% 131.79/17.08 ~sQ145_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f5212])).
% 131.79/17.08 fof(f6168,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|~sQ79_spl)),
% 131.79/17.08 inference(duplicate_literals_removal,[status(thm)],[f2249])).
% 131.79/17.08 fof(f6202,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|~ssList(X0)|app(skaf46(X0,X0),X0)=X0|~ssList(X0))),
% 131.79/17.08 inference(resolution,[status(thm)],[f341,f256])).
% 131.79/17.08 fof(f6207,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|app(skaf46(X0,X0),X0)=X0)),
% 131.79/17.08 inference(duplicate_literals_removal,[status(thm)],[f6202])).
% 131.79/17.08 fof(f6210,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|~ssList(X0)|app(X0,skaf45(X0,X0))=X0|~ssList(X0))),
% 131.79/17.08 inference(resolution,[status(thm)],[f342,f258])).
% 131.79/17.08 fof(f6215,plain,(
% 131.79/17.08 ![X0]: (~ssList(X0)|app(X0,skaf45(X0,X0))=X0)),
% 131.79/17.08 inference(duplicate_literals_removal,[status(thm)],[f6210])).
% 131.79/17.08 fof(f6346,plain,(
% 131.79/17.08 $false|~sQ79_spl),
% 131.79/17.08 inference(backward_subsumption_resolution,[status(thm)],[f428,f6168])).
% 131.79/17.08 fof(f6383,plain,(
% 131.79/17.08 ~sQ79_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f6346])).
% 131.79/17.08 fof(f6669,definition,(
% 131.79/17.08 sQ203_spl <=> (ssList(app(sk1,nil)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f6671,plain,(
% 131.79/17.08 ~ssList(app(sk1,nil))|sQ203_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f6669])).
% 131.79/17.08 fof(f6676,definition,(
% 131.79/17.08 sQ205_spl <=> (ssList(app(sk2,nil)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f6678,plain,(
% 131.79/17.08 ~ssList(app(sk2,nil))|sQ205_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f6676])).
% 131.79/17.08 fof(f6691,definition,(
% 131.79/17.08 sQ209_spl <=> (ssList(app(nil,nil)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f6693,plain,(
% 131.79/17.08 ~ssList(app(nil,nil))|sQ209_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f6691])).
% 131.79/17.08 fof(f6698,plain,(
% 131.79/17.08 ~ssList(sk1)|sQ203_spl),
% 131.79/17.08 inference(forward_demodulation,[status(thm)],[f558,f6671])).
% 131.79/17.08 fof(f6699,plain,(
% 131.79/17.08 $false|sQ203_spl),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f6698,f428])).
% 131.79/17.08 fof(f6700,plain,(
% 131.79/17.08 sQ203_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f6699])).
% 131.79/17.08 fof(f6701,plain,(
% 131.79/17.08 ~ssList(sk2)|sQ205_spl),
% 131.79/17.08 inference(forward_demodulation,[status(thm)],[f557,f6678])).
% 131.79/17.08 fof(f6702,plain,(
% 131.79/17.08 $false|sQ205_spl),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f6701,f429])).
% 131.79/17.08 fof(f6703,plain,(
% 131.79/17.08 sQ205_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f6702])).
% 131.79/17.08 fof(f6704,plain,(
% 131.79/17.08 ~ssList(nil)|sQ209_spl),
% 131.79/17.08 inference(forward_demodulation,[status(thm)],[f556,f6693])).
% 131.79/17.08 fof(f6705,plain,(
% 131.79/17.08 $false|sQ209_spl),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f6704,f205])).
% 131.79/17.08 fof(f6706,plain,(
% 131.79/17.08 sQ209_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f6705])).
% 131.79/17.08 fof(f7190,plain,(
% 131.79/17.08 app(skaf46(nil,nil),nil)=nil),
% 131.79/17.08 inference(resolution,[status(thm)],[f6207,f205])).
% 131.79/17.08 fof(f7191,plain,(
% 131.79/17.08 app(skaf46(sk2,sk2),sk2)=sk2),
% 131.79/17.08 inference(resolution,[status(thm)],[f6207,f429])).
% 131.79/17.08 fof(f7192,plain,(
% 131.79/17.08 app(skaf46(sk1,sk1),sk1)=sk1),
% 131.79/17.08 inference(resolution,[status(thm)],[f6207,f428])).
% 131.79/17.08 fof(f7214,plain,(
% 131.79/17.08 app(nil,skaf45(nil,nil))=nil),
% 131.79/17.08 inference(resolution,[status(thm)],[f6215,f205])).
% 131.79/17.08 fof(f7215,plain,(
% 131.79/17.08 app(sk2,skaf45(sk2,sk2))=sk2),
% 131.79/17.08 inference(resolution,[status(thm)],[f6215,f429])).
% 131.79/17.08 fof(f7216,plain,(
% 131.79/17.08 app(sk1,skaf45(sk1,sk1))=sk1),
% 131.79/17.08 inference(resolution,[status(thm)],[f6215,f428])).
% 131.79/17.08 fof(f7446,definition,(
% 131.79/17.08 sQ234_spl <=> (ssList(skaf46(sk2,sk2)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f7448,plain,(
% 131.79/17.08 ~ssList(skaf46(sk2,sk2))|sQ234_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f7446])).
% 131.79/17.08 fof(f7455,definition,(
% 131.79/17.08 sQ236_spl <=> (ssList(app(skaf46(sk2,sk2),sk2)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f7457,plain,(
% 131.79/17.08 ~ssList(app(skaf46(sk2,sk2),sk2))|sQ236_spl),
% 131.79/17.08 inference(component_clause,[status(thm)],[f7455])).
% 131.79/17.08 fof(f7463,plain,(
% 131.79/17.08 $false|sQ234_spl),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f7448,f247])).
% 131.79/17.08 fof(f7464,plain,(
% 131.79/17.08 sQ234_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f7463])).
% 131.79/17.08 fof(f7465,plain,(
% 131.79/17.08 ~ssList(sk2)|sQ236_spl),
% 131.79/17.08 inference(forward_demodulation,[status(thm)],[f7191,f7457])).
% 131.79/17.08 fof(f7466,plain,(
% 131.79/17.08 $false|sQ236_spl),
% 131.79/17.08 inference(forward_subsumption_resolution,[status(thm)],[f7465,f429])).
% 131.79/17.08 fof(f7467,plain,(
% 131.79/17.08 sQ236_spl),
% 131.79/17.08 inference(contradiction_clause,[status(thm)],[f7466])).
% 131.79/17.08 fof(f7480,definition,(
% 131.79/17.08 sQ239_spl <=> (ssList(skaf46(sk1,sk1)))),
% 131.79/17.08 introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition])).
% 131.79/17.08 fof(f7482,plain,(
% 131.79/17.09 ~ssList(skaf46(sk1,sk1))|sQ239_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f7480])).
% 131.79/17.09 fof(f7489,definition,(
% 131.79/17.09 sQ241_spl <=> (ssList(app(skaf46(sk1,sk1),sk1)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f7491,plain,(
% 131.79/17.09 ~ssList(app(skaf46(sk1,sk1),sk1))|sQ241_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f7489])).
% 131.79/17.09 fof(f7497,plain,(
% 131.79/17.09 $false|sQ239_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f7482,f247])).
% 131.79/17.09 fof(f7498,plain,(
% 131.79/17.09 sQ239_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f7497])).
% 131.79/17.09 fof(f7499,plain,(
% 131.79/17.09 ~ssList(sk1)|sQ241_spl),
% 131.79/17.09 inference(forward_demodulation,[status(thm)],[f7192,f7491])).
% 131.79/17.09 fof(f7500,plain,(
% 131.79/17.09 $false|sQ241_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f7499,f428])).
% 131.79/17.09 fof(f7501,plain,(
% 131.79/17.09 sQ241_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f7500])).
% 131.79/17.09 fof(f7514,definition,(
% 131.79/17.09 sQ244_spl <=> (ssList(skaf46(nil,nil)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f7516,plain,(
% 131.79/17.09 ~ssList(skaf46(nil,nil))|sQ244_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f7514])).
% 131.79/17.09 fof(f7523,definition,(
% 131.79/17.09 sQ246_spl <=> (ssList(app(skaf46(nil,nil),nil)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f7525,plain,(
% 131.79/17.09 ~ssList(app(skaf46(nil,nil),nil))|sQ246_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f7523])).
% 131.79/17.09 fof(f7531,plain,(
% 131.79/17.09 $false|sQ244_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f7516,f247])).
% 131.79/17.09 fof(f7532,plain,(
% 131.79/17.09 sQ244_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f7531])).
% 131.79/17.09 fof(f7533,plain,(
% 131.79/17.09 ~ssList(nil)|sQ246_spl),
% 131.79/17.09 inference(forward_demodulation,[status(thm)],[f7190,f7525])).
% 131.79/17.09 fof(f7534,plain,(
% 131.79/17.09 $false|sQ246_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f7533,f205])).
% 131.79/17.09 fof(f7535,plain,(
% 131.79/17.09 sQ246_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f7534])).
% 131.79/17.09 fof(f7545,definition,(
% 131.79/17.09 sQ248_spl <=> (ssList(skaf45(nil,nil)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f7547,plain,(
% 131.79/17.09 ~ssList(skaf45(nil,nil))|sQ248_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f7545])).
% 131.79/17.09 fof(f7561,definition,(
% 131.79/17.09 sQ252_spl <=> (ssList(app(nil,skaf45(nil,nil))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f7563,plain,(
% 131.79/17.09 ~ssList(app(nil,skaf45(nil,nil)))|sQ252_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f7561])).
% 131.79/17.09 fof(f7569,plain,(
% 131.79/17.09 $false|sQ248_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f7547,f248])).
% 131.79/17.09 fof(f7570,plain,(
% 131.79/17.09 sQ248_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f7569])).
% 131.79/17.09 fof(f7571,plain,(
% 131.79/17.09 ~ssList(nil)|sQ252_spl),
% 131.79/17.09 inference(forward_demodulation,[status(thm)],[f7214,f7563])).
% 131.79/17.09 fof(f7572,plain,(
% 131.79/17.09 $false|sQ252_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f7571,f205])).
% 131.79/17.09 fof(f7573,plain,(
% 131.79/17.09 sQ252_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f7572])).
% 131.79/17.09 fof(f7584,definition,(
% 131.79/17.09 sQ254_spl <=> (ssList(skaf45(sk2,sk2)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f7586,plain,(
% 131.79/17.09 ~ssList(skaf45(sk2,sk2))|sQ254_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f7584])).
% 131.79/17.09 fof(f7601,definition,(
% 131.79/17.09 sQ258_spl <=> (ssList(app(sk2,skaf45(sk2,sk2))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f7603,plain,(
% 131.79/17.09 ~ssList(app(sk2,skaf45(sk2,sk2)))|sQ258_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f7601])).
% 131.79/17.09 fof(f7609,plain,(
% 131.79/17.09 $false|sQ254_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f7586,f248])).
% 131.79/17.09 fof(f7610,plain,(
% 131.79/17.09 sQ254_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f7609])).
% 131.79/17.09 fof(f7611,plain,(
% 131.79/17.09 ~ssList(sk2)|sQ258_spl),
% 131.79/17.09 inference(forward_demodulation,[status(thm)],[f7215,f7603])).
% 131.79/17.09 fof(f7612,plain,(
% 131.79/17.09 $false|sQ258_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f7611,f429])).
% 131.79/17.09 fof(f7613,plain,(
% 131.79/17.09 sQ258_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f7612])).
% 131.79/17.09 fof(f7624,definition,(
% 131.79/17.09 sQ260_spl <=> (ssList(skaf45(sk1,sk1)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f7626,plain,(
% 131.79/17.09 ~ssList(skaf45(sk1,sk1))|sQ260_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f7624])).
% 131.79/17.09 fof(f7641,definition,(
% 131.79/17.09 sQ264_spl <=> (ssList(app(sk1,skaf45(sk1,sk1))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f7643,plain,(
% 131.79/17.09 ~ssList(app(sk1,skaf45(sk1,sk1)))|sQ264_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f7641])).
% 131.79/17.09 fof(f7649,plain,(
% 131.79/17.09 $false|sQ260_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f7626,f248])).
% 131.79/17.09 fof(f7650,plain,(
% 131.79/17.09 sQ260_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f7649])).
% 131.79/17.09 fof(f7651,plain,(
% 131.79/17.09 ~ssList(sk1)|sQ264_spl),
% 131.79/17.09 inference(forward_demodulation,[status(thm)],[f7216,f7643])).
% 131.79/17.09 fof(f7652,plain,(
% 131.79/17.09 $false|sQ264_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f7651,f428])).
% 131.79/17.09 fof(f7653,plain,(
% 131.79/17.09 sQ264_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f7652])).
% 131.79/17.09 fof(f7671,definition,(
% 131.79/17.09 sQ267_spl <=> (segmentP(sk1,nil))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f7673,plain,(
% 131.79/17.09 ~segmentP(sk1,nil)|sQ267_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f7671])).
% 131.79/17.09 fof(f7682,plain,(
% 131.79/17.09 ~ssList(sk1)|sQ267_spl),
% 131.79/17.09 inference(resolution,[status(thm)],[f7673,f253])).
% 131.79/17.09 fof(f7684,plain,(
% 131.79/17.09 $false|sQ267_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f7682,f428])).
% 131.79/17.09 fof(f7685,plain,(
% 131.79/17.09 sQ267_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f7684])).
% 131.79/17.09 fof(f10127,definition,(
% 131.79/17.09 sQ379_spl <=> (skac2=skac3)),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ379_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f10128,plain,(
% 131.79/17.09 skac2=skac3|~sQ379_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f10127])).
% 131.79/17.09 fof(f10135,plain,(
% 131.79/17.09 $false|~sQ379_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f10128,f251])).
% 131.79/17.09 fof(f10136,plain,(
% 131.79/17.09 ~sQ379_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f10135])).
% 131.79/17.09 fof(f12388,plain,(
% 131.79/17.09 ssList(tl(sk2))|nil=sk2),
% 131.79/17.09 inference(resolution,[status(thm)],[f273,f429])).
% 131.79/17.09 fof(f12399,plain,(
% 131.79/17.09 sQ147_spl|sQ10_spl),
% 131.79/17.09 inference(split_clause,[status(thm)],[f12388,f5159,f530])).
% 131.79/17.09 fof(f12404,plain,(
% 131.79/17.09 $false|sQ42_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f1290,f200])).
% 131.79/17.09 fof(f12405,plain,(
% 131.79/17.09 sQ42_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f12404])).
% 131.79/17.09 fof(f15981,definition,(
% 131.79/17.09 sQ458_spl <=> (ssList(skaf46(sk2,nil)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ458_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f15983,plain,(
% 131.79/17.09 ~ssList(skaf46(sk2,nil))|sQ458_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f15981])).
% 131.79/17.09 fof(f15987,plain,(
% 131.79/17.09 $false|sQ458_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f15983,f247])).
% 131.79/17.09 fof(f15988,plain,(
% 131.79/17.09 sQ458_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f15987])).
% 131.79/17.09 fof(f15994,definition,(
% 131.79/17.09 sQ459_spl <=> (ssList(skaf46(sk1,nil)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ459_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f15996,plain,(
% 131.79/17.09 ~ssList(skaf46(sk1,nil))|sQ459_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f15994])).
% 131.79/17.09 fof(f16000,plain,(
% 131.79/17.09 $false|sQ459_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f15996,f247])).
% 131.79/17.09 fof(f16001,plain,(
% 131.79/17.09 sQ459_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f16000])).
% 131.79/17.09 fof(f16090,definition,(
% 131.79/17.09 sQ460_spl <=> (ssList(skaf45(sk2,nil)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ460_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f16092,plain,(
% 131.79/17.09 ~ssList(skaf45(sk2,nil))|sQ460_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f16090])).
% 131.79/17.09 fof(f16104,plain,(
% 131.79/17.09 $false|sQ460_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f16092,f248])).
% 131.79/17.09 fof(f16105,plain,(
% 131.79/17.09 sQ460_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f16104])).
% 131.79/17.09 fof(f16112,definition,(
% 131.79/17.09 sQ463_spl <=> (ssList(skaf45(sk1,nil)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ463_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f16114,plain,(
% 131.79/17.09 ~ssList(skaf45(sk1,nil))|sQ463_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f16112])).
% 131.79/17.09 fof(f16126,plain,(
% 131.79/17.09 $false|sQ463_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f16114,f248])).
% 131.79/17.09 fof(f16127,plain,(
% 131.79/17.09 sQ463_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f16126])).
% 131.79/17.09 fof(f16318,definition,(
% 131.79/17.09 ![X0]: (sQ477_spl <=> (~app(X0,sk2)=app(X0,sk2)|~ssList(X0)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ477_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f16319,plain,(
% 131.79/17.09 ![X0]: (~app(X0,sk2)=app(X0,sk2)|~ssList(X0)|~sQ477_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f16318])).
% 131.79/17.09 fof(f16329,plain,(
% 131.79/17.09 ![X0]: (~ssList(X0)|~sQ477_spl)),
% 131.79/17.09 inference(trivial_equality_resolution,[status(thm)],[f16319])).
% 131.79/17.09 fof(f16330,plain,(
% 131.79/17.09 $false|~sQ477_spl),
% 131.79/17.09 inference(backward_subsumption_resolution,[status(thm)],[f210,f16329])).
% 131.79/17.09 fof(f16390,plain,(
% 131.79/17.09 ~sQ477_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f16330])).
% 131.79/17.09 fof(f16439,definition,(
% 131.79/17.09 ![X0]: (sQ484_spl <=> (~app(X0,sk1)=app(X0,sk1)|~ssList(X0)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ484_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f16440,plain,(
% 131.79/17.09 ![X0]: (~app(X0,sk1)=app(X0,sk1)|~ssList(X0)|~sQ484_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f16439])).
% 131.79/17.09 fof(f16448,plain,(
% 131.79/17.09 ![X0]: (~ssList(X0)|~sQ484_spl)),
% 131.79/17.09 inference(trivial_equality_resolution,[status(thm)],[f16440])).
% 131.79/17.09 fof(f16449,plain,(
% 131.79/17.09 $false|~sQ484_spl),
% 131.79/17.09 inference(backward_subsumption_resolution,[status(thm)],[f247,f16448])).
% 131.79/17.09 fof(f16457,plain,(
% 131.79/17.09 ~sQ484_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f16449])).
% 131.79/17.09 fof(f16863,plain,(
% 131.79/17.09 ssList(app(sk2,sk2))),
% 131.79/17.09 inference(resolution,[status(thm)],[f786,f429])).
% 131.79/17.09 fof(f16864,plain,(
% 131.79/17.09 ssList(app(sk2,sk1))),
% 131.79/17.09 inference(resolution,[status(thm)],[f786,f428])).
% 131.79/17.09 fof(f22155,plain,(
% 131.79/17.09 ![X0]: (~ssList(X0)|app(cons(hd(sk1),nil),X0)=cons(hd(sk1),X0)|~sQ8_spl|~sQ13_spl)),
% 131.79/17.09 inference(resolution,[status(thm)],[f328,f2255])).
% 131.79/17.09 fof(f22158,plain,(
% 131.79/17.09 ![X0]: (~ssList(X0)|app(sk1,X0)=cons(hd(sk1),X0)|~sQ8_spl|~sQ13_spl)),
% 131.79/17.09 inference(forward_demodulation,[status(thm)],[f2154,f22155])).
% 131.79/17.09 fof(f22638,definition,(
% 131.79/17.09 sQ662_spl <=> (ssItem(skaf70(sk2)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ662_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f22640,plain,(
% 131.79/17.09 ~ssItem(skaf70(sk2))|sQ662_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f22638])).
% 131.79/17.09 fof(f22641,definition,(
% 131.79/17.09 sQ663_spl <=> (ssItem(skaf69(sk2)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ663_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f22643,plain,(
% 131.79/17.09 ~ssItem(skaf69(sk2))|sQ663_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f22641])).
% 131.79/17.09 fof(f22709,plain,(
% 131.79/17.09 $false|sQ662_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f22640,f222])).
% 131.79/17.09 fof(f22710,plain,(
% 131.79/17.09 sQ662_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f22709])).
% 131.79/17.09 fof(f22711,plain,(
% 131.79/17.09 $false|sQ663_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f22643,f223])).
% 131.79/17.09 fof(f22712,plain,(
% 131.79/17.09 sQ663_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f22711])).
% 131.79/17.09 fof(f30247,plain,(
% 131.79/17.09 ssItem(hd(sk2))|nil=sk2),
% 131.79/17.09 inference(resolution,[status(thm)],[f274,f429])).
% 131.79/17.09 fof(f30250,plain,(
% 131.79/17.09 sQ13_spl|sQ10_spl),
% 131.79/17.09 inference(split_clause,[status(thm)],[f30247,f589,f530])).
% 131.79/17.09 fof(f34242,plain,(
% 131.79/17.09 $false|sQ153_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f5187,f209])).
% 131.79/17.09 fof(f34243,plain,(
% 131.79/17.09 sQ153_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f34242])).
% 131.79/17.09 fof(f37172,plain,(
% 131.79/17.09 $false|sQ156_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f5202,f209])).
% 131.79/17.09 fof(f37173,plain,(
% 131.79/17.09 sQ156_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f37172])).
% 131.79/17.09 fof(f40567,definition,(
% 131.79/17.09 sQ1323_spl <=> (ssList(app(sk2,sk2)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1323_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f40569,plain,(
% 131.79/17.09 ~ssList(app(sk2,sk2))|sQ1323_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f40567])).
% 131.79/17.09 fof(f40575,plain,(
% 131.79/17.09 $false|sQ1323_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f40569,f16863])).
% 131.79/17.09 fof(f40576,plain,(
% 131.79/17.09 sQ1323_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f40575])).
% 131.79/17.09 fof(f40938,definition,(
% 131.79/17.09 sQ1346_spl <=> (ssList(app(sk2,sk1)))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1346_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f40940,plain,(
% 131.79/17.09 ~ssList(app(sk2,sk1))|sQ1346_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f40938])).
% 131.79/17.09 fof(f40946,plain,(
% 131.79/17.09 $false|sQ1346_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f40940,f16864])).
% 131.79/17.09 fof(f40947,plain,(
% 131.79/17.09 sQ1346_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f40946])).
% 131.79/17.09 fof(f41737,definition,(
% 131.79/17.09 sQ1379_spl <=> (app(nil,nil)=nil)),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1379_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f41739,plain,(
% 131.79/17.09 ~app(nil,nil)=nil|sQ1379_spl),
% 131.79/17.09 inference(component_clause,[status(thm)],[f41737])).
% 131.79/17.09 fof(f41743,plain,(
% 131.79/17.09 ~nil=nil|sQ1379_spl),
% 131.79/17.09 inference(forward_demodulation,[status(thm)],[f556,f41739])).
% 131.79/17.09 fof(f41744,plain,(
% 131.79/17.09 $false|sQ1379_spl),
% 131.79/17.09 inference(trivial_equality_resolution,[status(thm)],[f41743])).
% 131.79/17.09 fof(f41745,plain,(
% 131.79/17.09 sQ1379_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f41744])).
% 131.79/17.09 fof(f44762,definition,(
% 131.79/17.09 ![X0]: (sQ1656_spl <=> (~ssList(skaf73(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1656_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f44763,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf73(X0))|~sQ1656_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f44762])).
% 131.79/17.09 fof(f44770,plain,(
% 131.79/17.09 $false|~sQ1656_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f44763,f219])).
% 131.79/17.09 fof(f44771,plain,(
% 131.79/17.09 ~sQ1656_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f44770])).
% 131.79/17.09 fof(f44777,definition,(
% 131.79/17.09 ![X0]: (sQ1657_spl <=> (~ssList(skaf75(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1657_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f44778,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf75(X0))|~sQ1657_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f44777])).
% 131.79/17.09 fof(f44785,plain,(
% 131.79/17.09 $false|~sQ1657_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f44778,f217])).
% 131.79/17.09 fof(f44786,plain,(
% 131.79/17.09 ~sQ1657_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f44785])).
% 131.79/17.09 fof(f45440,definition,(
% 131.79/17.09 ![X0]: (sQ1678_spl <=> (~ssList(skaf76(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1678_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45441,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf76(X0))|~sQ1678_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45440])).
% 131.79/17.09 fof(f45448,plain,(
% 131.79/17.09 $false|~sQ1678_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45441,f216])).
% 131.79/17.09 fof(f45449,plain,(
% 131.79/17.09 ~sQ1678_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45448])).
% 131.79/17.09 fof(f45455,definition,(
% 131.79/17.09 ![X0]: (sQ1679_spl <=> (~ssList(skaf77(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1679_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45456,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf77(X0))|~sQ1679_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45455])).
% 131.79/17.09 fof(f45463,plain,(
% 131.79/17.09 $false|~sQ1679_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45456,f215])).
% 131.79/17.09 fof(f45464,plain,(
% 131.79/17.09 ~sQ1679_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45463])).
% 131.79/17.09 fof(f45470,definition,(
% 131.79/17.09 ![X0]: (sQ1680_spl <=> (~ssList(skaf80(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1680_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45471,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf80(X0))|~sQ1680_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45470])).
% 131.79/17.09 fof(f45478,plain,(
% 131.79/17.09 $false|~sQ1680_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45471,f212])).
% 131.79/17.09 fof(f45479,plain,(
% 131.79/17.09 ~sQ1680_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45478])).
% 131.79/17.09 fof(f45485,definition,(
% 131.79/17.09 ![X0]: (sQ1681_spl <=> (~ssList(skaf81(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1681_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45486,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf81(X0))|~sQ1681_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45485])).
% 131.79/17.09 fof(f45493,plain,(
% 131.79/17.09 $false|~sQ1681_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45486,f211])).
% 131.79/17.09 fof(f45494,plain,(
% 131.79/17.09 ~sQ1681_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45493])).
% 131.79/17.09 fof(f45554,definition,(
% 131.79/17.09 ![X0]: (sQ1682_spl <=> (~ssList(skaf82(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1682_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45555,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf82(X0))|~sQ1682_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45554])).
% 131.79/17.09 fof(f45562,plain,(
% 131.79/17.09 $false|~sQ1682_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45555,f210])).
% 131.79/17.09 fof(f45563,plain,(
% 131.79/17.09 ~sQ1682_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45562])).
% 131.79/17.09 fof(f45569,definition,(
% 131.79/17.09 ![X0]: (sQ1683_spl <=> (~ssList(skaf72(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1683_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45570,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf72(X0))|~sQ1683_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45569])).
% 131.79/17.09 fof(f45577,plain,(
% 131.79/17.09 $false|~sQ1683_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45570,f220])).
% 131.79/17.09 fof(f45578,plain,(
% 131.79/17.09 ~sQ1683_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45577])).
% 131.79/17.09 fof(f45618,definition,(
% 131.79/17.09 ![X0]: (sQ1687_spl <=> (~ssList(skaf71(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1687_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45619,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf71(X0))|~sQ1687_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45618])).
% 131.79/17.09 fof(f45626,plain,(
% 131.79/17.09 $false|~sQ1687_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45619,f221])).
% 131.79/17.09 fof(f45627,plain,(
% 131.79/17.09 ~sQ1687_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45626])).
% 131.79/17.09 fof(f45633,definition,(
% 131.79/17.09 ![X0]: (sQ1688_spl <=> (~ssList(skaf51(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1688_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45634,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf51(X0))|~sQ1688_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45633])).
% 131.79/17.09 fof(f45641,plain,(
% 131.79/17.09 $false|~sQ1688_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45634,f241])).
% 131.79/17.09 fof(f45642,plain,(
% 131.79/17.09 ~sQ1688_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45641])).
% 131.79/17.09 fof(f45648,definition,(
% 131.79/17.09 ![X0]: (sQ1689_spl <=> (~ssList(skaf52(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1689_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45649,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf52(X0))|~sQ1689_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45648])).
% 131.79/17.09 fof(f45656,plain,(
% 131.79/17.09 $false|~sQ1689_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45649,f240])).
% 131.79/17.09 fof(f45657,plain,(
% 131.79/17.09 ~sQ1689_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45656])).
% 131.79/17.09 fof(f45895,definition,(
% 131.79/17.09 ![X0]: (sQ1690_spl <=> (~ssList(skaf53(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1690_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45896,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf53(X0))|~sQ1690_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45895])).
% 131.79/17.09 fof(f45903,plain,(
% 131.79/17.09 $false|~sQ1690_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45896,f239])).
% 131.79/17.09 fof(f45904,plain,(
% 131.79/17.09 ~sQ1690_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45903])).
% 131.79/17.09 fof(f45910,definition,(
% 131.79/17.09 ![X0]: (sQ1691_spl <=> (~ssList(skaf56(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1691_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45911,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf56(X0))|~sQ1691_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45910])).
% 131.79/17.09 fof(f45918,plain,(
% 131.79/17.09 $false|~sQ1691_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45911,f236])).
% 131.79/17.09 fof(f45919,plain,(
% 131.79/17.09 ~sQ1691_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45918])).
% 131.79/17.09 fof(f45925,definition,(
% 131.79/17.09 ![X0]: (sQ1692_spl <=> (~ssList(skaf57(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1692_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45926,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf57(X0))|~sQ1692_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45925])).
% 131.79/17.09 fof(f45933,plain,(
% 131.79/17.09 $false|~sQ1692_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45926,f235])).
% 131.79/17.09 fof(f45934,plain,(
% 131.79/17.09 ~sQ1692_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45933])).
% 131.79/17.09 fof(f45940,definition,(
% 131.79/17.09 ![X0]: (sQ1693_spl <=> (~ssList(skaf58(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1693_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45941,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf58(X0))|~sQ1693_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45940])).
% 131.79/17.09 fof(f45948,plain,(
% 131.79/17.09 $false|~sQ1693_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45941,f234])).
% 131.79/17.09 fof(f45949,plain,(
% 131.79/17.09 ~sQ1693_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45948])).
% 131.79/17.09 fof(f45955,definition,(
% 131.79/17.09 ![X0]: (sQ1694_spl <=> (~ssList(skaf61(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1694_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45956,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf61(X0))|~sQ1694_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45955])).
% 131.79/17.09 fof(f45963,plain,(
% 131.79/17.09 $false|~sQ1694_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45956,f231])).
% 131.79/17.09 fof(f45964,plain,(
% 131.79/17.09 ~sQ1694_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45963])).
% 131.79/17.09 fof(f45970,definition,(
% 131.79/17.09 ![X0]: (sQ1695_spl <=> (~ssList(skaf62(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1695_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f45971,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf62(X0))|~sQ1695_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f45970])).
% 131.79/17.09 fof(f45978,plain,(
% 131.79/17.09 $false|~sQ1695_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f45971,f230])).
% 131.79/17.09 fof(f45979,plain,(
% 131.79/17.09 ~sQ1695_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f45978])).
% 131.79/17.09 fof(f46949,definition,(
% 131.79/17.09 ![X0]: (sQ1776_spl <=> (~ssList(skaf63(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1776_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f46950,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf63(X0))|~sQ1776_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f46949])).
% 131.79/17.09 fof(f46957,plain,(
% 131.79/17.09 $false|~sQ1776_spl),
% 131.79/17.09 inference(forward_subsumption_resolution,[status(thm)],[f46950,f229])).
% 131.79/17.09 fof(f46958,plain,(
% 131.79/17.09 ~sQ1776_spl),
% 131.79/17.09 inference(contradiction_clause,[status(thm)],[f46957])).
% 131.79/17.09 fof(f46964,definition,(
% 131.79/17.09 ![X0]: (sQ1777_spl <=> (~ssList(skaf66(X0))))),
% 131.79/17.09 introduced(definition,[new_symbols(definition,[sQ1777_spl])],[split_symbol_definition])).
% 131.79/17.09 fof(f46965,plain,(
% 131.79/17.09 ![X0]: (~ssList(skaf66(X0))|~sQ1777_spl)),
% 131.79/17.09 inference(component_clause,[status(thm)],[f46964])).
% 128.46/17.12 fof(f46972,plain,(
% 128.46/17.12 $false|~sQ1777_spl),
% 128.46/17.12 inference(forward_subsumption_resolution,[status(thm)],[f46965,f226])).
% 128.46/17.12 fof(f46973,plain,(
% 128.46/17.12 ~sQ1777_spl),
% 128.46/17.12 inference(contradiction_clause,[status(thm)],[f46972])).
% 128.46/17.12 fof(f46979,definition,(
% 128.46/17.12 ![X0]: (sQ1778_spl <=> (~ssList(skaf67(X0))))),
% 128.46/17.12 introduced(definition,[new_symbols(definition,[sQ1778_spl])],[split_symbol_definition])).
% 128.46/17.12 fof(f46980,plain,(
% 128.46/17.12 ![X0]: (~ssList(skaf67(X0))|~sQ1778_spl)),
% 128.46/17.12 inference(component_clause,[status(thm)],[f46979])).
% 128.46/17.12 fof(f46987,plain,(
% 128.46/17.12 $false|~sQ1778_spl),
% 128.46/17.12 inference(forward_subsumption_resolution,[status(thm)],[f46980,f225])).
% 128.46/17.12 fof(f46988,plain,(
% 128.46/17.12 ~sQ1778_spl),
% 128.46/17.12 inference(contradiction_clause,[status(thm)],[f46987])).
% 128.46/17.12 fof(f46994,definition,(
% 128.46/17.12 ![X0]: (sQ1779_spl <=> (~ssList(skaf68(X0))))),
% 128.46/17.12 introduced(definition,[new_symbols(definition,[sQ1779_spl])],[split_symbol_definition])).
% 128.46/17.12 fof(f46995,plain,(
% 128.46/17.12 ![X0]: (~ssList(skaf68(X0))|~sQ1779_spl)),
% 128.46/17.12 inference(component_clause,[status(thm)],[f46994])).
% 128.46/17.12 fof(f47002,plain,(
% 128.46/17.12 $false|~sQ1779_spl),
% 128.46/17.12 inference(forward_subsumption_resolution,[status(thm)],[f46995,f224])).
% 128.46/17.12 fof(f47003,plain,(
% 128.46/17.12 ~sQ1779_spl),
% 128.46/17.12 inference(contradiction_clause,[status(thm)],[f47002])).
% 128.46/17.12 fof(f47402,plain,(
% 128.46/17.12 app(sk1,tl(sk2))=cons(hd(sk1),tl(sk2))|~sQ8_spl|~sQ13_spl|~sQ147_spl),
% 128.46/17.12 inference(resolution,[status(thm)],[f22158,f5160])).
% 128.46/17.12 fof(f47409,plain,(
% 128.46/17.12 app(sk1,tl(sk2))=sk2|~sQ141_spl|~sQ8_spl|~sQ13_spl|~sQ147_spl),
% 128.46/17.12 inference(forward_demodulation,[status(thm)],[f5073,f47402])).
% 128.46/17.12 fof(f47436,plain,(
% 128.46/17.12 ~ssList(tl(sk2))|segmentP(sk2,sk1)|~sQ36_spl|~sQ141_spl|~sQ8_spl|~sQ13_spl|~sQ147_spl),
% 128.46/17.12 inference(paramodulation,[status(thm)],[f47409,f1228])).
% 128.46/17.12 fof(f47443,plain,(
% 128.46/17.12 ~sQ147_spl|sQ6_spl|~sQ36_spl|~sQ141_spl|~sQ8_spl|~sQ13_spl),
% 128.46/17.12 inference(split_clause,[status(thm)],[f47436,f5159,f464,f1218,f5065,f524,f589])).
% 128.46/17.12 fof(f47450,plain,(
% 128.46/17.12 $false),
% 128.46/17.12 inference(sat_refutation,[status(thm)],[f452,f468,f469,f502,f533,f548,f609,f611,f682,f1221,f1469,f1807,f2499,f5068,f5193,f5208,f5213,f6383,f6700,f6703,f6706,f7464,f7467,f7498,f7501,f7532,f7535,f7570,f7573,f7610,f7613,f7650,f7653,f7685,f10136,f12399,f12405,f15988,f16001,f16105,f16127,f16390,f16457,f22710,f22712,f30250,f34243,f37173,f40576,f40947,f41745,f44771,f44786,f45449,f45464,f45479,f45494,f45563,f45578,f45627,f45642,f45657,f45904,f45919,f45934,f45949,f45964,f45979,f46958,f46973,f46988,f47003,f47443])).
% 128.46/17.12 % SZS output end CNFRefutation for theBenchmark.p
% 29.04/17.24 % Elapsed time: 16.864669 seconds
% 29.04/17.24 % CPU time: 133.459928 seconds
% 29.04/17.24 % Total memory used: 1.164 GB
% 29.04/17.24 % Net memory used: 1.100 GB
%------------------------------------------------------------------------------