%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC330-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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:40:49 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.63s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 111
% Syntax : Number of formulae : 331 ( 73 unt; 62 def)
% Number of atoms : 822 ( 161 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 883 ( 392 ~; 429 |; 0 &)
% ( 62 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 68 ( 66 usr; 63 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 8 con; 0-2 aty)
% Number of variables : 206 ( 206 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
equalelemsP(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [U] : ssList(skaf82(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [U] : ssList(skaf81(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] : ssList(skaf80(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [U] : ssList(skaf77(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [U] : ssList(skaf76(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [U] : ssList(skaf75(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [U] : ssList(skaf73(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [U] : ssList(skaf72(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [U] : ssList(skaf71(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [U] : ssList(skaf68(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [U] : ssList(skaf67(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [U] : ssList(skaf66(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [U] : ssList(skaf63(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [U] : ssList(skaf62(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [U] : ssList(skaf61(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [U] : ssList(skaf58(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [U] : ssList(skaf57(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [U] : ssList(skaf56(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [U] : ssList(skaf53(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [U] :
( segmentP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [U] :
( segmentP(U,U)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [U] :
( equalelemsP(cons(U,nil))
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [U] :
( nil = U
| ~ ssList(U)
| ~ segmentP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [U] :
( nil = U
| cons(hd(U),tl(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [U] :
( nil = U
| cons(skaf83(U),skaf82(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [U,V] :
( nil = U
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [U,V] :
( nil = V
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ segmentP(V,U)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,axiom,
! [U,V] :
( app(U,V) = nil
| ~ ssList(U)
| ~ ssList(V)
| nil != V
| nil != U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,axiom,
! [U,V,W] :
( app(app(W,V),U) = app(W,app(V,U))
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f150,axiom,
! [U,V,W] :
( V = W
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,axiom,
! [U,V,W] :
( segmentP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ segmentP(V,W)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [U,V,W,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ~ ssList(U)
| ~ ssList(W)
| app(app(U,V),W) != X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f190,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
( nil = sk4
| ssItem(sk5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
( nil = sk3
| ssItem(sk5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
( nil = sk4
| cons(sk5,nil) = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f200,negated_conjecture,
( nil = sk3
| ssList(sk6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f201,negated_conjecture,
( nil = sk3
| ssList(sk7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,negated_conjecture,
( nil = sk3
| cons(sk5,nil) = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,negated_conjecture,
( nil = sk3
| app(app(sk6,sk3),sk7) = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f206,negated_conjecture,
( ~ equalelemsP(sk1)
| ~ segmentP(sk2,sk1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f207,plain,
equalelemsP(nil),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f214,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f219,plain,
! [X0] : ssList(skaf82(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f220,plain,
! [X0] : ssList(skaf81(X0)),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f221,plain,
! [X0] : ssList(skaf80(X0)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f224,plain,
! [X0] : ssList(skaf77(X0)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f225,plain,
! [X0] : ssList(skaf76(X0)),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f226,plain,
! [X0] : ssList(skaf75(X0)),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f228,plain,
! [X0] : ssList(skaf73(X0)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f229,plain,
! [X0] : ssList(skaf72(X0)),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f230,plain,
! [X0] : ssList(skaf71(X0)),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f233,plain,
! [X0] : ssList(skaf68(X0)),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f234,plain,
! [X0] : ssList(skaf67(X0)),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f235,plain,
! [X0] : ssList(skaf66(X0)),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f238,plain,
! [X0] : ssList(skaf63(X0)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f239,plain,
! [X0] : ssList(skaf62(X0)),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f240,plain,
! [X0] : ssList(skaf61(X0)),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f243,plain,
! [X0] : ssList(skaf58(X0)),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f244,plain,
! [X0] : ssList(skaf57(X0)),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f245,plain,
! [X0] : ssList(skaf56(X0)),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f248,plain,
! [X0] : ssList(skaf53(X0)),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f262,plain,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f263,plain,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f270,plain,
! [X0] :
( equalelemsP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f281,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f287,plain,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ segmentP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f292,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f313,plain,
! [X0] :
( nil = X0
| cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f318,plain,
! [X0] :
( nil = X0
| cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f333,plain,
! [U] :
( nil = U
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f334,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f333]) ).
fof(f335,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f336,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f346,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X0)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f368,plain,
! [X0,X1] :
( app(X0,X1) = nil
| ~ ssList(X0)
| ~ ssList(X1)
| nil != X1
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f375,plain,
! [X0,X1,X2] :
( app(app(X2,X1),X0) = app(X2,app(X1,X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f376,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f377,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f380,plain,
! [U,W] :
( segmentP(U,W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ ssList(W)
| ~ segmentP(V,W)
| ~ segmentP(U,V) ) ),
inference(miniscoping,[status(thm)],[f152]) ).
fof(f381,plain,
! [X0,X1,X2] :
( segmentP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(X1,X2)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f412,plain,
! [V,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| app(app(U,V),W) != X ) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f413,plain,
! [X0,X1,X2,X3] :
( segmentP(X3,X1)
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| app(app(X0,X1),X2) != X3 ),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f439,plain,
ssList(sk3),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f440,plain,
ssList(sk4),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f441,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f442,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f443,plain,
( nil = sk4
| ssItem(sk5) ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f444,plain,
( nil = sk3
| ssItem(sk5) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f447,plain,
( nil = sk4
| cons(sk5,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f453,plain,
( nil = sk3
| ssList(sk6) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f454,plain,
( nil = sk3
| ssList(sk7) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f455,plain,
( nil = sk3
| cons(sk5,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f456,plain,
( nil = sk3
| app(app(sk6,sk3),sk7) = sk4 ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f461,plain,
( ~ equalelemsP(sk1)
| ~ segmentP(sk2,sk1) ),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f469,definition,
( sQ2_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f472,definition,
( sQ3_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f473,plain,
( ~ sQ3_spl
| nil = sk4 ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f475,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f443,f469,f472]) ).
fof(f476,definition,
( sQ4_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f477,plain,
( ~ sQ4_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f476]) ).
fof(f479,plain,
( sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f444,f469,f476]) ).
fof(f480,definition,
( sQ5_spl
<=> ssList(sk6) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f481,plain,
( ~ sQ5_spl
| ssList(sk6) ),
inference(component_clause,[status(thm)],[f480]) ).
fof(f484,definition,
( sQ6_spl
<=> ssList(sk7) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f485,plain,
( ~ sQ6_spl
| ssList(sk7) ),
inference(component_clause,[status(thm)],[f484]) ).
fof(f488,definition,
( sQ7_spl
<=> cons(sk5,nil) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f489,plain,
( ~ sQ7_spl
| cons(sk5,nil) = sk3 ),
inference(component_clause,[status(thm)],[f488]) ).
fof(f491,plain,
( sQ3_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f447,f488,f472]) ).
fof(f492,definition,
( sQ8_spl
<=> app(app(sk6,sk3),sk7) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( ~ sQ8_spl
| app(app(sk6,sk3),sk7) = sk4 ),
inference(component_clause,[status(thm)],[f492]) ).
fof(f504,plain,
( sQ4_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f453,f480,f476]) ).
fof(f505,plain,
( sQ4_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f454,f484,f476]) ).
fof(f506,plain,
( sQ4_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f455,f488,f476]) ).
fof(f507,plain,
( sQ4_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f456,f492,f476]) ).
fof(f510,definition,
( sQ11_spl
<=> segmentP(sk2,sk1) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f512,plain,
( sQ11_spl
| ~ segmentP(sk2,sk1) ),
inference(component_clause,[status(thm)],[f510]) ).
fof(f513,definition,
( sQ12_spl
<=> equalelemsP(sk1) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f515,plain,
( sQ12_spl
| ~ equalelemsP(sk1) ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,plain,
( ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f461,f510,f513]) ).
fof(f533,plain,
( app(nil,nil) = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f368]) ).
fof(f534,plain,
( app(nil,nil) = nil
| ~ ssList(nil) ),
inference(duplicate_literals_removal,[status(thm)],[f533]) ).
fof(f535,plain,
! [X0,X1,X2] :
( segmentP(app(app(X1,X2),X0),X2)
| ~ ssList(app(app(X1,X2),X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f413]) ).
fof(f549,plain,
( ~ sQ4_spl
| equalelemsP(sk3) ),
inference(backward_demodulation,[status(thm)],[f477,f207]) ).
fof(f563,plain,
( sQ11_spl
| ~ segmentP(sk4,sk1) ),
inference(forward_demodulation,[status(thm)],[f441,f512]) ).
fof(f570,plain,
( sQ12_spl
| ~ equalelemsP(sk3) ),
inference(backward_demodulation,[status(thm)],[f442,f515]) ).
fof(f571,plain,
( sQ12_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f570,f549]) ).
fof(f572,plain,
( sQ12_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f571]) ).
fof(f573,plain,
( sQ11_spl
| ~ segmentP(sk4,sk3) ),
inference(forward_demodulation,[status(thm)],[f442,f563]) ).
fof(f574,plain,
( ~ sQ7_spl
| equalelemsP(sk3)
| ~ ssItem(sk5) ),
inference(paramodulation,[status(thm)],[f489,f270]) ).
fof(f575,definition,
( sQ13_spl
<=> equalelemsP(sk3) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f576,plain,
( ~ sQ13_spl
| equalelemsP(sk3) ),
inference(component_clause,[status(thm)],[f575]) ).
fof(f578,plain,
( ~ sQ7_spl
| sQ13_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f574,f469,f575,f488]) ).
fof(f613,plain,
! [X0] :
( ~ sQ4_spl
| segmentP(X0,sk3)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f477,f262]) ).
fof(f614,plain,
( sQ11_spl
| ~ sQ4_spl
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f613,f573]) ).
fof(f615,plain,
( sQ11_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f614,f440]) ).
fof(f616,plain,
( sQ11_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f615]) ).
fof(f618,plain,
! [X0] : app(nil,skaf61(X0)) = skaf61(X0),
inference(resolution,[status(thm)],[f281,f240]) ).
fof(f619,plain,
! [X0] : app(nil,skaf62(X0)) = skaf62(X0),
inference(resolution,[status(thm)],[f281,f239]) ).
fof(f620,plain,
! [X0] : app(nil,skaf63(X0)) = skaf63(X0),
inference(resolution,[status(thm)],[f281,f238]) ).
fof(f621,plain,
! [X0] : app(nil,skaf66(X0)) = skaf66(X0),
inference(resolution,[status(thm)],[f281,f235]) ).
fof(f622,plain,
! [X0] : app(nil,skaf67(X0)) = skaf67(X0),
inference(resolution,[status(thm)],[f281,f234]) ).
fof(f623,plain,
! [X0] : app(nil,skaf68(X0)) = skaf68(X0),
inference(resolution,[status(thm)],[f281,f233]) ).
fof(f624,plain,
! [X0] : app(nil,skaf71(X0)) = skaf71(X0),
inference(resolution,[status(thm)],[f281,f230]) ).
fof(f625,plain,
! [X0] : app(nil,skaf72(X0)) = skaf72(X0),
inference(resolution,[status(thm)],[f281,f229]) ).
fof(f626,plain,
! [X0] : app(nil,skaf73(X0)) = skaf73(X0),
inference(resolution,[status(thm)],[f281,f228]) ).
fof(f627,plain,
! [X0] : app(nil,skaf75(X0)) = skaf75(X0),
inference(resolution,[status(thm)],[f281,f226]) ).
fof(f628,plain,
! [X0] : app(nil,skaf76(X0)) = skaf76(X0),
inference(resolution,[status(thm)],[f281,f225]) ).
fof(f629,plain,
! [X0] : app(nil,skaf77(X0)) = skaf77(X0),
inference(resolution,[status(thm)],[f281,f224]) ).
fof(f633,plain,
! [X0] : app(nil,skaf80(X0)) = skaf80(X0),
inference(resolution,[status(thm)],[f281,f221]) ).
fof(f634,plain,
! [X0] : app(nil,skaf81(X0)) = skaf81(X0),
inference(resolution,[status(thm)],[f281,f220]) ).
fof(f635,plain,
! [X0] : app(nil,skaf82(X0)) = skaf82(X0),
inference(resolution,[status(thm)],[f281,f219]) ).
fof(f637,plain,
! [X0] : app(nil,skaf58(X0)) = skaf58(X0),
inference(resolution,[status(thm)],[f243,f281]) ).
fof(f638,plain,
! [X0] : app(nil,skaf57(X0)) = skaf57(X0),
inference(resolution,[status(thm)],[f244,f281]) ).
fof(f639,plain,
! [X0] : app(nil,skaf56(X0)) = skaf56(X0),
inference(resolution,[status(thm)],[f245,f281]) ).
fof(f640,plain,
! [X0] : app(nil,skaf53(X0)) = skaf53(X0),
inference(resolution,[status(thm)],[f248,f281]) ).
fof(f671,plain,
( ~ ssList(nil)
| nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f287,f262]) ).
fof(f673,definition,
( sQ14_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f675,plain,
( sQ14_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f673]) ).
fof(f676,definition,
( sQ15_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f679,plain,
( sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f671,f673,f676]) ).
fof(f681,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f675,f214]) ).
fof(f682,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f681]) ).
fof(f689,plain,
! [X0] :
( ssList(skaf61(X0))
| ~ ssList(nil)
| ~ ssList(skaf61(X0)) ),
inference(paramodulation,[status(thm)],[f618,f292]) ).
fof(f695,plain,
( ~ sQ8_spl
| ssList(sk4)
| ~ ssList(app(sk6,sk3))
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f493,f292]) ).
fof(f696,definition,
( sQ16_spl
<=> ssList(sk4) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f702,definition,
( sQ17_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f704,plain,
( sQ17_spl
| ~ ssList(sk3) ),
inference(component_clause,[status(thm)],[f702]) ).
fof(f706,definition,
! [X0] :
( sQ18_spl
<=> ( ssList(skaf61(X0))
| ~ ssList(skaf61(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f709,plain,
( ~ sQ14_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f689,f706,f673]) ).
fof(f715,definition,
( sQ19_spl
<=> ssList(app(sk6,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f716,plain,
( ~ sQ19_spl
| ssList(app(sk6,sk3)) ),
inference(component_clause,[status(thm)],[f715]) ).
fof(f717,plain,
( sQ19_spl
| ~ ssList(app(sk6,sk3)) ),
inference(component_clause,[status(thm)],[f715]) ).
fof(f718,plain,
( ~ sQ8_spl
| sQ16_spl
| ~ sQ19_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f695,f484,f715,f696,f492]) ).
fof(f731,plain,
( sQ19_spl
| ~ ssList(sk6)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f717,f292]) ).
fof(f732,plain,
( sQ19_spl
| ~ sQ5_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f731,f702,f480,f715]) ).
fof(f733,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f704,f439]) ).
fof(f734,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f733]) ).
fof(f737,plain,
! [X0] :
( ~ sQ3_spl
| sk4 = X0
| ~ ssList(X0)
| ~ segmentP(nil,X0) ),
inference(backward_demodulation,[status(thm)],[f473,f287]) ).
fof(f760,plain,
! [X0] :
( ~ sQ3_spl
| segmentP(X0,sk4)
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f473,f262]) ).
fof(f764,plain,
! [X0] :
( ~ sQ3_spl
| sk4 = X0
| ~ ssList(X0)
| ~ segmentP(sk4,X0) ),
inference(forward_demodulation,[status(thm)],[f473,f737]) ).
fof(f995,plain,
! [X0] :
( ~ sQ6_spl
| nil = X0
| ~ ssList(X0)
| app(X0,sk7) != nil ),
inference(resolution,[status(thm)],[f334,f485]) ).
fof(f1009,plain,
! [X0] :
( ~ sQ19_spl
| nil = app(sk6,sk3)
| ~ ssList(X0)
| app(X0,app(sk6,sk3)) != nil ),
inference(resolution,[status(thm)],[f336,f716]) ).
fof(f1030,plain,
! [X0] :
( ~ sQ6_spl
| nil = sk7
| ~ ssList(X0)
| app(X0,sk7) != nil ),
inference(resolution,[status(thm)],[f336,f485]) ).
fof(f1031,plain,
! [X0] :
( ~ sQ5_spl
| nil = sk6
| ~ ssList(X0)
| app(X0,sk6) != nil ),
inference(resolution,[status(thm)],[f336,f481]) ).
fof(f1040,definition,
! [X0] :
( sQ28_spl
<=> ( ~ ssList(X0)
| app(X0,app(sk6,sk3)) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1043,definition,
( sQ29_spl
<=> nil = app(sk6,sk3) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1044,plain,
( ~ sQ29_spl
| nil = app(sk6,sk3) ),
inference(component_clause,[status(thm)],[f1043]) ).
fof(f1046,plain,
( ~ sQ19_spl
| sQ29_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f1009,f1040,f1043,f715]) ).
fof(f1051,definition,
! [X0] :
( sQ31_spl
<=> ( ~ ssList(X0)
| app(X0,sk7) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1054,definition,
( sQ32_spl
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f1055,plain,
( ~ sQ32_spl
| nil = sk7 ),
inference(component_clause,[status(thm)],[f1054]) ).
fof(f1057,plain,
( ~ sQ6_spl
| sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f1030,f1051,f1054,f484]) ).
fof(f1058,definition,
! [X0] :
( sQ33_spl
<=> ( ~ ssList(X0)
| app(X0,sk6) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1061,definition,
( sQ34_spl
<=> nil = sk6 ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1062,plain,
( ~ sQ34_spl
| nil = sk6 ),
inference(component_clause,[status(thm)],[f1061]) ).
fof(f1064,plain,
( ~ sQ5_spl
| sQ34_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f1031,f1058,f1061,f480]) ).
fof(f1109,plain,
( ~ sQ3_spl
| ~ ssList(sk4)
| sk4 = sk4
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f764,f263]) ).
fof(f1110,definition,
( sQ36_spl
<=> sk4 = sk4 ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1113,plain,
( ~ sQ3_spl
| sQ36_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f1109,f696,f1110,f472]) ).
fof(f1119,plain,
! [X0] :
( ~ sQ3_spl
| ~ ssList(X0)
| X0 = sk4
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ segmentP(sk4,X0) ),
inference(resolution,[status(thm)],[f346,f760]) ).
fof(f1121,definition,
! [X0] :
( sQ37_spl
<=> ( ~ ssList(X0)
| X0 = sk4
| ~ ssList(X0)
| ~ segmentP(sk4,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1124,plain,
( ~ sQ3_spl
| ~ sQ16_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f1119,f1121,f696,f472]) ).
fof(f1127,plain,
! [X0] :
( X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(nil,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f262,f346]) ).
fof(f1128,definition,
! [X0] :
( sQ38_spl
<=> ( X0 = nil
| ~ ssList(X0)
| ~ segmentP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1131,plain,
( ~ sQ14_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f1127,f1128,f673]) ).
fof(f1315,plain,
! [X0] :
( ssList(skaf62(X0))
| ~ ssList(nil)
| ~ ssList(skaf62(X0)) ),
inference(paramodulation,[status(thm)],[f619,f292]) ).
fof(f1316,definition,
! [X0] :
( sQ41_spl
<=> ( ssList(skaf62(X0))
| ~ ssList(skaf62(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1319,plain,
( ~ sQ14_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f1315,f1316,f673]) ).
fof(f1320,plain,
! [X0] :
( ssList(skaf63(X0))
| ~ ssList(nil)
| ~ ssList(skaf63(X0)) ),
inference(paramodulation,[status(thm)],[f620,f292]) ).
fof(f1321,definition,
! [X0] :
( sQ42_spl
<=> ( ssList(skaf63(X0))
| ~ ssList(skaf63(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1324,plain,
( ~ sQ14_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f1320,f1321,f673]) ).
fof(f1325,plain,
! [X0] :
( ssList(skaf66(X0))
| ~ ssList(nil)
| ~ ssList(skaf66(X0)) ),
inference(paramodulation,[status(thm)],[f621,f292]) ).
fof(f1326,definition,
! [X0] :
( sQ43_spl
<=> ( ssList(skaf66(X0))
| ~ ssList(skaf66(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1329,plain,
( ~ sQ14_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f1325,f1326,f673]) ).
fof(f1330,plain,
! [X0] :
( ssList(skaf67(X0))
| ~ ssList(nil)
| ~ ssList(skaf67(X0)) ),
inference(paramodulation,[status(thm)],[f622,f292]) ).
fof(f1331,definition,
! [X0] :
( sQ44_spl
<=> ( ssList(skaf67(X0))
| ~ ssList(skaf67(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1334,plain,
( ~ sQ14_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1330,f1331,f673]) ).
fof(f1335,plain,
! [X0] :
( ssList(skaf68(X0))
| ~ ssList(nil)
| ~ ssList(skaf68(X0)) ),
inference(paramodulation,[status(thm)],[f623,f292]) ).
fof(f1336,definition,
! [X0] :
( sQ45_spl
<=> ( ssList(skaf68(X0))
| ~ ssList(skaf68(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1339,plain,
( ~ sQ14_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f1335,f1336,f673]) ).
fof(f1340,plain,
! [X0] :
( ssList(skaf71(X0))
| ~ ssList(nil)
| ~ ssList(skaf71(X0)) ),
inference(paramodulation,[status(thm)],[f624,f292]) ).
fof(f1341,definition,
! [X0] :
( sQ46_spl
<=> ( ssList(skaf71(X0))
| ~ ssList(skaf71(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1344,plain,
( ~ sQ14_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f1340,f1341,f673]) ).
fof(f1367,plain,
! [X0] :
( ssList(skaf72(X0))
| ~ ssList(nil)
| ~ ssList(skaf72(X0)) ),
inference(paramodulation,[status(thm)],[f625,f292]) ).
fof(f1368,definition,
! [X0] :
( sQ49_spl
<=> ( ssList(skaf72(X0))
| ~ ssList(skaf72(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1371,plain,
( ~ sQ14_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f1367,f1368,f673]) ).
fof(f1372,plain,
! [X0] :
( ssList(skaf73(X0))
| ~ ssList(nil)
| ~ ssList(skaf73(X0)) ),
inference(paramodulation,[status(thm)],[f626,f292]) ).
fof(f1373,definition,
! [X0] :
( sQ50_spl
<=> ( ssList(skaf73(X0))
| ~ ssList(skaf73(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1376,plain,
( ~ sQ14_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f1372,f1373,f673]) ).
fof(f1377,plain,
! [X0] :
( ssList(skaf75(X0))
| ~ ssList(nil)
| ~ ssList(skaf75(X0)) ),
inference(paramodulation,[status(thm)],[f627,f292]) ).
fof(f1378,definition,
! [X0] :
( sQ51_spl
<=> ( ssList(skaf75(X0))
| ~ ssList(skaf75(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1381,plain,
( ~ sQ14_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1377,f1378,f673]) ).
fof(f1382,plain,
! [X0] :
( ssList(skaf76(X0))
| ~ ssList(nil)
| ~ ssList(skaf76(X0)) ),
inference(paramodulation,[status(thm)],[f628,f292]) ).
fof(f1383,definition,
! [X0] :
( sQ52_spl
<=> ( ssList(skaf76(X0))
| ~ ssList(skaf76(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1386,plain,
( ~ sQ14_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1382,f1383,f673]) ).
fof(f1387,plain,
! [X0] :
( ssList(skaf77(X0))
| ~ ssList(nil)
| ~ ssList(skaf77(X0)) ),
inference(paramodulation,[status(thm)],[f629,f292]) ).
fof(f1388,definition,
! [X0] :
( sQ53_spl
<=> ( ssList(skaf77(X0))
| ~ ssList(skaf77(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1391,plain,
( ~ sQ14_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f1387,f1388,f673]) ).
fof(f1392,plain,
! [X0] :
( ssList(skaf80(X0))
| ~ ssList(nil)
| ~ ssList(skaf80(X0)) ),
inference(paramodulation,[status(thm)],[f633,f292]) ).
fof(f1393,definition,
! [X0] :
( sQ54_spl
<=> ( ssList(skaf80(X0))
| ~ ssList(skaf80(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1396,plain,
( ~ sQ14_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1392,f1393,f673]) ).
fof(f1397,plain,
! [X0] :
( ssList(skaf81(X0))
| ~ ssList(nil)
| ~ ssList(skaf81(X0)) ),
inference(paramodulation,[status(thm)],[f634,f292]) ).
fof(f1398,definition,
! [X0] :
( sQ55_spl
<=> ( ssList(skaf81(X0))
| ~ ssList(skaf81(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1401,plain,
( ~ sQ14_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1397,f1398,f673]) ).
fof(f1402,plain,
! [X0] :
( ssList(skaf82(X0))
| ~ ssList(nil)
| ~ ssList(skaf82(X0)) ),
inference(paramodulation,[status(thm)],[f635,f292]) ).
fof(f1403,definition,
! [X0] :
( sQ56_spl
<=> ( ssList(skaf82(X0))
| ~ ssList(skaf82(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1406,plain,
( ~ sQ14_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1402,f1403,f673]) ).
fof(f1407,plain,
! [X0] :
( ssList(skaf58(X0))
| ~ ssList(nil)
| ~ ssList(skaf58(X0)) ),
inference(paramodulation,[status(thm)],[f637,f292]) ).
fof(f1408,definition,
! [X0] :
( sQ57_spl
<=> ( ssList(skaf58(X0))
| ~ ssList(skaf58(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1411,plain,
( ~ sQ14_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1407,f1408,f673]) ).
fof(f1412,plain,
! [X0] :
( ssList(skaf57(X0))
| ~ ssList(nil)
| ~ ssList(skaf57(X0)) ),
inference(paramodulation,[status(thm)],[f638,f292]) ).
fof(f1413,definition,
! [X0] :
( sQ58_spl
<=> ( ssList(skaf57(X0))
| ~ ssList(skaf57(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1416,plain,
( ~ sQ14_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1412,f1413,f673]) ).
fof(f1417,plain,
! [X0] :
( ssList(skaf56(X0))
| ~ ssList(nil)
| ~ ssList(skaf56(X0)) ),
inference(paramodulation,[status(thm)],[f639,f292]) ).
fof(f1418,definition,
! [X0] :
( sQ59_spl
<=> ( ssList(skaf56(X0))
| ~ ssList(skaf56(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1421,plain,
( ~ sQ14_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1417,f1418,f673]) ).
fof(f1422,plain,
! [X0] :
( ssList(skaf53(X0))
| ~ ssList(nil)
| ~ ssList(skaf53(X0)) ),
inference(paramodulation,[status(thm)],[f640,f292]) ).
fof(f1423,definition,
! [X0] :
( sQ60_spl
<=> ( ssList(skaf53(X0))
| ~ ssList(skaf53(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1426,plain,
( ~ sQ14_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1422,f1423,f673]) ).
fof(f1456,plain,
( ~ sQ6_spl
| nil = sk7
| app(sk7,sk7) != nil ),
inference(resolution,[status(thm)],[f995,f485]) ).
fof(f1457,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| nil = sk6
| app(sk6,sk7) != nil ),
inference(resolution,[status(thm)],[f995,f481]) ).
fof(f1474,definition,
( sQ64_spl
<=> app(sk7,sk7) = nil ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1477,plain,
( ~ sQ6_spl
| sQ32_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f1456,f1474,f1054,f484]) ).
fof(f1478,definition,
( sQ65_spl
<=> app(sk6,sk7) = nil ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1481,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| sQ34_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f1457,f1478,f1061,f484,f480]) ).
fof(f1545,plain,
( ~ sQ34_spl
| ~ sQ32_spl
| nil = sk7 ),
inference(backward_demodulation,[status(thm)],[f1553,f1062]) ).
fof(f1553,plain,
( ~ sQ32_spl
| ~ sQ34_spl
| sk6 = sk7 ),
inference(forward_demodulation,[status(thm)],[f1062,f1055]) ).
fof(f1566,plain,
( ~ sQ34_spl
| ~ sQ32_spl
| app(nil,nil) = sk7
| ~ ssList(nil) ),
inference(backward_demodulation,[status(thm)],[f1545,f534]) ).
fof(f1567,definition,
( sQ67_spl
<=> app(nil,nil) = sk7 ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1568,plain,
( ~ sQ67_spl
| app(nil,nil) = sk7 ),
inference(component_clause,[status(thm)],[f1567]) ).
fof(f1570,plain,
( ~ sQ34_spl
| ~ sQ32_spl
| sQ67_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1566,f673,f1567,f1054,f1061]) ).
fof(f1571,definition,
( sQ68_spl
<=> app(nil,nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1574,plain,
( sQ68_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f534,f673,f1571]) ).
fof(f1581,plain,
! [X0] :
( ~ sQ29_spl
| app(nil,X0) = app(sk6,app(sk3,X0))
| ~ ssList(sk6)
| ~ ssList(sk3)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1044,f375]) ).
fof(f1583,definition,
! [X0] :
( sQ69_spl
<=> ( app(nil,X0) = app(sk6,app(sk3,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1586,plain,
( ~ sQ29_spl
| ~ sQ5_spl
| ~ sQ17_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1581,f1583,f702,f480,f1043]) ).
fof(f1588,plain,
! [X0] :
( ~ sQ67_spl
| app(sk7,X0) = app(nil,app(nil,X0))
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1568,f375]) ).
fof(f1590,definition,
! [X0] :
( sQ70_spl
<=> ( app(sk7,X0) = app(nil,app(nil,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1593,plain,
( ~ sQ67_spl
| ~ sQ14_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1588,f1590,f673,f1567]) ).
fof(f1598,plain,
! [X0,X1] :
( X0 = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[f377]) ).
fof(f1599,definition,
! [X0] :
( sQ71_spl
<=> ( X0 = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1602,definition,
! [X1] :
( sQ72_spl
<=> ~ ssList(X1) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1603,plain,
! [X0] :
( ~ sQ72_spl
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1602]) ).
fof(f1605,plain,
( sQ72_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1598,f1599,f1602]) ).
fof(f1622,plain,
( ~ sQ72_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f214,f1603]) ).
fof(f1655,plain,
~ sQ72_spl,
inference(contradiction_clause,[status(thm)],[f1622]) ).
fof(f1675,plain,
( sQ12_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f570,f576]) ).
fof(f1676,plain,
( sQ12_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f1675]) ).
fof(f1712,plain,
! [X0,X1] :
( segmentP(X1,nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(X1,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f262,f381]) ).
fof(f1713,definition,
! [X0,X1] :
( sQ74_spl
<=> ( segmentP(X1,nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1716,plain,
( ~ sQ14_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f1712,f1713,f673]) ).
fof(f1796,plain,
( ~ sQ6_spl
| nil = sk7
| cons(hd(sk7),tl(sk7)) = sk7 ),
inference(resolution,[status(thm)],[f313,f485]) ).
fof(f1798,plain,
( ~ sQ5_spl
| nil = sk6
| cons(hd(sk6),tl(sk6)) = sk6 ),
inference(resolution,[status(thm)],[f313,f481]) ).
fof(f1804,definition,
( sQ86_spl
<=> cons(hd(sk7),tl(sk7)) = sk7 ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1807,plain,
( ~ sQ6_spl
| sQ32_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f1796,f1804,f1054,f484]) ).
fof(f1812,definition,
( sQ88_spl
<=> cons(hd(sk6),tl(sk6)) = sk6 ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1815,plain,
( ~ sQ5_spl
| sQ34_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f1798,f1812,f1061,f480]) ).
fof(f1821,plain,
! [X0] :
( ~ sQ32_spl
| segmentP(X0,sk7)
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f1055,f262]) ).
fof(f1881,plain,
! [X0,X1] :
( ~ sQ32_spl
| segmentP(X1,sk7)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(sk7)
| ~ segmentP(X1,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1821,f381]) ).
fof(f1882,definition,
! [X0,X1] :
( sQ90_spl
<=> ( segmentP(X1,sk7)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1885,plain,
( ~ sQ32_spl
| ~ sQ6_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f1881,f1882,f484,f1054]) ).
fof(f1920,plain,
! [X0] :
( ~ sQ34_spl
| sk6 = X0
| cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f1062,f318]) ).
fof(f1943,plain,
( ~ sQ34_spl
| sk6 = sk4
| cons(skaf83(sk4),skaf82(sk4)) = sk4 ),
inference(resolution,[status(thm)],[f1920,f440]) ).
fof(f1944,plain,
( ~ sQ6_spl
| ~ sQ34_spl
| sk6 = sk7
| cons(skaf83(sk7),skaf82(sk7)) = sk7 ),
inference(resolution,[status(thm)],[f1920,f485]) ).
fof(f1945,plain,
( ~ sQ34_spl
| sk6 = sk3
| cons(skaf83(sk3),skaf82(sk3)) = sk3 ),
inference(resolution,[status(thm)],[f1920,f439]) ).
fof(f1954,definition,
( sQ93_spl
<=> cons(skaf83(sk4),skaf82(sk4)) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1957,definition,
( sQ94_spl
<=> sk6 = sk4 ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1960,plain,
( ~ sQ34_spl
| sQ94_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f1943,f1954,f1957,f1061]) ).
fof(f1961,definition,
( sQ95_spl
<=> cons(skaf83(sk7),skaf82(sk7)) = sk7 ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1964,definition,
( sQ96_spl
<=> sk6 = sk7 ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1967,plain,
( ~ sQ6_spl
| ~ sQ34_spl
| sQ96_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f1944,f1961,f1964,f1061,f484]) ).
fof(f1968,definition,
( sQ97_spl
<=> cons(skaf83(sk3),skaf82(sk3)) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1971,definition,
( sQ98_spl
<=> sk6 = sk3 ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1974,plain,
( ~ sQ34_spl
| sQ98_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f1945,f1968,f1971,f1061]) ).
fof(f2016,plain,
( ~ sQ8_spl
| segmentP(app(app(sk6,sk3),sk7),sk3)
| ~ ssList(sk4)
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f493,f535]) ).
fof(f2018,definition,
( sQ102_spl
<=> segmentP(app(app(sk6,sk3),sk7),sk3) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f2019,plain,
( ~ sQ102_spl
| segmentP(app(app(sk6,sk3),sk7),sk3) ),
inference(component_clause,[status(thm)],[f2018]) ).
fof(f2021,plain,
( ~ sQ8_spl
| sQ102_spl
| ~ sQ16_spl
| ~ sQ17_spl
| ~ sQ5_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2016,f484,f480,f702,f696,f2018,f492]) ).
fof(f2026,plain,
( ~ sQ102_spl
| ~ sQ8_spl
| segmentP(sk4,sk3) ),
inference(forward_demodulation,[status(thm)],[f493,f2019]) ).
fof(f2027,plain,
( ~ sQ102_spl
| ~ sQ8_spl
| sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2026,f573]) ).
fof(f2028,plain,
( ~ sQ102_spl
| ~ sQ8_spl
| sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f2027]) ).
fof(f2029,plain,
$false,
inference(sat_refutation,[status(thm)],[f475,f479,f491,f504,f505,f506,f507,f516,f572,f578,f616,f679,f682,f709,f718,f732,f734,f1046,f1057,f1064,f1113,f1124,f1131,f1319,f1324,f1329,f1334,f1339,f1344,f1371,f1376,f1381,f1386,f1391,f1396,f1401,f1406,f1411,f1416,f1421,f1426,f1477,f1481,f1570,f1574,f1586,f1593,f1605,f1655,f1676,f1716,f1807,f1815,f1885,f1960,f1967,f1974,f2021,f2028]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC330-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.58 % Computer : n006.cluster.edu
% 0.11/0.58 % Model : x86_64 x86_64
% 0.11/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.58 % Memory : 8046.5625MB
% 0.11/0.58 % OS : Linux 6.8.0-71-generic
% 0.11/0.58 % CPULimit : 300
% 0.11/0.58 % WCLimit : 300
% 0.11/0.58 % DateTime : Mon Sep 21 08:16:13 UTC 2026
% 0.11/0.59 % CPUTime :
% 0.11/0.60 % Drodi V4.1.1
% 0.14/0.63 % Refutation found
% 0.14/0.63 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.66 % Elapsed time: 0.067806 seconds
% 0.14/0.66 % CPU time: 0.250584 seconds
% 0.14/0.66 % Total memory used: 55.058 MB
% 0.14/0.66 % Net memory used: 54.890 MB
%------------------------------------------------------------------------------