%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC284-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:40:38 PM UTC 2026
% Result : Unsatisfiable 1.29s 0.69s
% Output : CNFRefutation 1.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 89
% Syntax : Number of formulae : 292 ( 24 unt; 55 def)
% Number of atoms : 973 ( 140 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 1303 ( 622 ~; 626 |; 0 &)
% ( 55 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 64 ( 62 usr; 56 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 190 ( 190 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [U] :
( leq(U,U)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [U,V] :
( ssList(cons(U,V))
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [U,V] :
( V = U
| neq(V,U)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [U,V] :
( nil = U
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [U,V] :
( nil = V
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,axiom,
! [U,V,W] :
( memberP(cons(W,U),V)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ ssList(U)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f140,axiom,
! [U,V,W] :
( memberP(app(U,W),V)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [U,V,W] :
( memberP(app(W,U),V)
| ~ ssItem(V)
| ~ ssList(W)
| ~ ssList(U)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f143,axiom,
! [U,V,W] :
( rearsegP(W,V)
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != W ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,axiom,
! [U,V,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != W ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [U,V,W] :
( U = W
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,axiom,
! [U,V,W] :
( W = U
| memberP(V,W)
| ~ ssItem(W)
| ~ ssItem(U)
| ~ ssList(V)
| ~ memberP(cons(U,V),W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f175,axiom,
! [U,V,W,X] :
( memberP(X,V)
| ~ ssList(X)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| app(U,cons(V,W)) != X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
ssList(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
app(app(sk6,cons(sk5,nil)),sk7) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
ssItem(sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
( memberP(sk7,sk8)
| memberP(sk6,sk8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
( ~ leq(sk5,sk8)
| memberP(sk6,sk8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,negated_conjecture,
( ~ leq(sk5,sk8)
| ~ leq(sk8,sk5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f201,negated_conjecture,
( nil != sk4
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f202,negated_conjecture,
( ~ neq(sk4,nil)
| ssItem(sk9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f203,negated_conjecture,
( ~ neq(sk4,nil)
| cons(sk9,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f212,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f266,plain,
! [X0] :
( leq(X0,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f275,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f278,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f279,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f290,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f291,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f305,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != V ) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f306,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != X1 ),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f307,plain,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f331,plain,
! [U] :
( nil = U
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f332,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f333,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f334,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f333]) ).
fof(f358,plain,
! [X0,X1,X2] :
( memberP(cons(X2,X0),X1)
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f359,plain,
! [X0,X1,X2] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f360,plain,
! [X0,X1,X2] :
( memberP(app(X2,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f362,plain,
! [V,W] :
( rearsegP(W,V)
| ~ ssList(W)
| ~ ssList(V)
| ! [U] :
( ~ ssList(U)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f143]) ).
fof(f363,plain,
! [X0,X1,X2] :
( rearsegP(X2,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f364,plain,
! [U,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f365,plain,
! [X0,X1,X2] :
( frontsegP(X2,X0)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f373,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(f374,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f375,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f376,plain,
! [U,W] :
( U = W
| ~ ssList(W)
| ! [V] :
( ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f377,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f395,plain,
! [U,W] :
( W = U
| ! [V] :
( memberP(V,W)
| ~ ssItem(W)
| ~ ssItem(U)
| ~ ssList(V)
| ~ memberP(cons(U,V),W) ) ),
inference(miniscoping,[status(thm)],[f161]) ).
fof(f396,plain,
! [X0,X1,X2] :
( X2 = X0
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(cnf_transformation,[status(thm)],[f395]) ).
fof(f414,plain,
! [V,X] :
( memberP(X,V)
| ~ ssList(X)
| ~ ssItem(V)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| app(U,cons(V,W)) != X ) ) ),
inference(miniscoping,[status(thm)],[f175]) ).
fof(f415,plain,
! [X0,X1,X2,X3] :
( memberP(X3,X1)
| ~ ssList(X3)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| app(X0,cons(X1,X2)) != X3 ),
inference(cnf_transformation,[status(thm)],[f414]) ).
fof(f438,plain,
ssList(sk4),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f440,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f441,plain,
ssItem(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f442,plain,
ssList(sk6),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f443,plain,
ssList(sk7),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f444,plain,
app(app(sk6,cons(sk5,nil)),sk7) = sk1,
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f445,plain,
ssItem(sk8),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f446,plain,
( memberP(sk7,sk8)
| memberP(sk6,sk8) ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f447,plain,
( ~ leq(sk5,sk8)
| memberP(sk6,sk8) ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f449,plain,
( ~ leq(sk5,sk8)
| ~ leq(sk8,sk5) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f450,plain,
( nil != sk4
| nil = sk3 ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f451,plain,
( ~ neq(sk4,nil)
| ssItem(sk9) ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f452,plain,
( ~ neq(sk4,nil)
| cons(sk9,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f461,definition,
( sQ2_spl
<=> memberP(sk6,sk8) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f462,plain,
( ~ sQ2_spl
| memberP(sk6,sk8) ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f464,definition,
( sQ3_spl
<=> memberP(sk7,sk8) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f465,plain,
( ~ sQ3_spl
| memberP(sk7,sk8) ),
inference(component_clause,[status(thm)],[f464]) ).
fof(f467,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f446,f461,f464]) ).
fof(f468,definition,
( sQ4_spl
<=> leq(sk5,sk8) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( ~ sQ4_spl
| leq(sk5,sk8) ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f470,plain,
( sQ4_spl
| ~ leq(sk5,sk8) ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f471,plain,
( ~ sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f447,f461,f468]) ).
fof(f472,definition,
( sQ5_spl
<=> leq(sk8,sk5) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( sQ5_spl
| ~ leq(sk8,sk5) ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f476,plain,
( ~ sQ4_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f449,f472,f468]) ).
fof(f477,definition,
( sQ6_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f478,plain,
( ~ sQ6_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f477]) ).
fof(f480,definition,
( sQ7_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f483,plain,
( ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f450,f477,f480]) ).
fof(f484,definition,
( sQ8_spl
<=> ssItem(sk9) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f487,definition,
( sQ9_spl
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f489,plain,
( sQ9_spl
| ~ neq(sk4,nil) ),
inference(component_clause,[status(thm)],[f487]) ).
fof(f490,plain,
( ~ sQ9_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f451,f484,f487]) ).
fof(f491,definition,
( sQ10_spl
<=> cons(sk9,nil) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f492,plain,
( ~ sQ10_spl
| cons(sk9,nil) = sk3 ),
inference(component_clause,[status(thm)],[f491]) ).
fof(f494,plain,
( ~ sQ9_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f452,f491,f487]) ).
fof(f513,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f363]) ).
fof(f514,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f513,f290]) ).
fof(f515,plain,
! [X1,X0] :
( frontsegP(app(X0,X1),X0)
| ~ ssList(app(X0,X1))
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f365]) ).
fof(f516,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f515,f290]) ).
fof(f520,plain,
! [X0,X1,X2] :
( memberP(app(X1,cons(X2,X0)),X2)
| ~ ssList(app(X1,cons(X2,X0)))
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f415]) ).
fof(f532,plain,
app(app(sk6,cons(sk5,nil)),sk7) = sk3,
inference(forward_demodulation,[status(thm)],[f440,f444]) ).
fof(f559,plain,
! [X0] :
( ~ sQ6_spl
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(backward_demodulation,[status(thm)],[f478,f275]) ).
fof(f588,definition,
( sQ12_spl
<=> ssList(sk7) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f590,plain,
( sQ12_spl
| ~ ssList(sk7) ),
inference(component_clause,[status(thm)],[f588]) ).
fof(f594,definition,
( sQ14_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f598,plain,
( sQ9_spl
| sk4 = nil
| ~ ssList(sk4)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f307,f489]) ).
fof(f601,definition,
( sQ15_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f603,plain,
( sQ15_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f601]) ).
fof(f604,definition,
( sQ16_spl
<=> ssList(sk4) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f606,plain,
( sQ16_spl
| ~ ssList(sk4) ),
inference(component_clause,[status(thm)],[f604]) ).
fof(f607,plain,
( sQ9_spl
| sQ7_spl
| ~ sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f598,f601,f604,f480,f487]) ).
fof(f608,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f606,f438]) ).
fof(f609,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f608]) ).
fof(f610,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f603,f212]) ).
fof(f611,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f610]) ).
fof(f696,plain,
( ssList(sk3)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f532,f290]) ).
fof(f697,definition,
( sQ20_spl
<=> ssList(app(sk6,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f699,plain,
( sQ20_spl
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f697]) ).
fof(f700,plain,
( sQ14_spl
| ~ sQ20_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f696,f588,f697,f594]) ).
fof(f701,plain,
( rearsegP(sk3,sk7)
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(paramodulation,[status(thm)],[f532,f514]) ).
fof(f702,definition,
( sQ21_spl
<=> rearsegP(sk3,sk7) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f705,plain,
( sQ21_spl
| ~ sQ12_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f701,f697,f588,f702]) ).
fof(f706,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f590,f443]) ).
fof(f707,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f706]) ).
fof(f708,plain,
( sQ20_spl
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[f699,f290]) ).
fof(f709,definition,
( sQ22_spl
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f711,plain,
( sQ22_spl
| ~ ssList(cons(sk5,nil)) ),
inference(component_clause,[status(thm)],[f709]) ).
fof(f712,definition,
( sQ23_spl
<=> ssList(sk6) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f714,plain,
( sQ23_spl
| ~ ssList(sk6) ),
inference(component_clause,[status(thm)],[f712]) ).
fof(f715,plain,
( sQ20_spl
| ~ sQ23_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f708,f709,f712,f697]) ).
fof(f716,plain,
( sQ22_spl
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f711,f291]) ).
fof(f717,definition,
( sQ24_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f719,plain,
( sQ24_spl
| ~ ssItem(sk5) ),
inference(component_clause,[status(thm)],[f717]) ).
fof(f720,plain,
( sQ22_spl
| ~ sQ15_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f716,f717,f601,f709]) ).
fof(f721,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f719,f441]) ).
fof(f722,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f721]) ).
fof(f723,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f714,f442]) ).
fof(f724,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f723]) ).
fof(f725,plain,
( frontsegP(sk3,app(sk6,cons(sk5,nil)))
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f532,f516]) ).
fof(f726,definition,
( sQ25_spl
<=> frontsegP(sk3,app(sk6,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f729,plain,
( sQ25_spl
| ~ sQ20_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f725,f588,f697,f726]) ).
fof(f730,plain,
( ~ ssList(nil)
| nil = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f332,f279]) ).
fof(f733,definition,
( sQ26_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f736,plain,
( sQ26_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f730,f601,f733]) ).
fof(f744,plain,
( nil = sk7
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| sk3 != nil ),
inference(paramodulation,[status(thm)],[f532,f334]) ).
fof(f747,definition,
( sQ28_spl
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f748,plain,
( ~ sQ28_spl
| nil = sk7 ),
inference(component_clause,[status(thm)],[f747]) ).
fof(f750,plain,
( sQ28_spl
| ~ sQ20_spl
| ~ sQ12_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f744,f477,f588,f697,f747]) ).
fof(f864,plain,
( ~ sQ6_spl
| ~ sQ28_spl
| sk7 = sk3 ),
inference(forward_demodulation,[status(thm)],[f748,f478]) ).
fof(f873,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ28_spl
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(forward_demodulation,[status(thm)],[f864,f559]) ).
fof(f1029,plain,
! [X0] :
( ~ ssList(app(nil,X0))
| app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(nil,X0)) ),
inference(resolution,[status(thm)],[f375,f279]) ).
fof(f1034,definition,
! [X0] :
( sQ36_spl
<=> ( ~ ssList(app(nil,X0))
| app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1037,plain,
( ~ sQ15_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1029,f1034,f601]) ).
fof(f1054,plain,
( sk3 = app(sk6,app(cons(sk5,nil),sk7))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f532,f373]) ).
fof(f1055,plain,
! [X0] :
( X0 = sk7
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(X0)
| app(app(sk6,cons(sk5,nil)),X0) != sk3 ),
inference(paramodulation,[status(thm)],[f532,f375]) ).
fof(f1057,plain,
! [X0] :
( app(sk3,X0) = app(app(sk6,cons(sk5,nil)),app(sk7,X0))
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f532,f373]) ).
fof(f1061,definition,
( sQ40_spl
<=> sk3 = app(sk6,app(cons(sk5,nil),sk7)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1062,plain,
( ~ sQ40_spl
| sk3 = app(sk6,app(cons(sk5,nil),sk7)) ),
inference(component_clause,[status(thm)],[f1061]) ).
fof(f1064,plain,
( sQ40_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1054,f588,f709,f712,f1061]) ).
fof(f1065,definition,
! [X0] :
( sQ41_spl
<=> ( X0 = sk7
| ~ ssList(X0)
| app(app(sk6,cons(sk5,nil)),X0) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1066,plain,
! [X0] :
( ~ sQ41_spl
| X0 = sk7
| ~ ssList(X0)
| app(app(sk6,cons(sk5,nil)),X0) != sk3 ),
inference(component_clause,[status(thm)],[f1065]) ).
fof(f1068,plain,
( ~ sQ12_spl
| ~ sQ20_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f1055,f1065,f697,f588]) ).
fof(f1070,definition,
! [X0] :
( sQ42_spl
<=> ( app(sk3,X0) = app(app(sk6,cons(sk5,nil)),app(sk7,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1073,plain,
( ~ sQ20_spl
| ~ sQ12_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f1057,f1070,f588,f697]) ).
fof(f1100,plain,
! [X0] :
( ~ ssList(app(X0,nil))
| app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(X0,nil)) ),
inference(resolution,[status(thm)],[f377,f278]) ).
fof(f1102,plain,
! [X0] :
( app(sk6,cons(sk5,nil)) = X0
| ~ ssList(X0)
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil)))
| sk3 != app(X0,sk7) ),
inference(paramodulation,[status(thm)],[f532,f377]) ).
fof(f1107,definition,
! [X0] :
( sQ43_spl
<=> ( ~ ssList(app(X0,nil))
| app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(app(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1110,plain,
( ~ sQ15_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f1100,f1107,f601]) ).
fof(f1112,definition,
! [X0] :
( sQ44_spl
<=> ( app(sk6,cons(sk5,nil)) = X0
| ~ ssList(X0)
| sk3 != app(X0,sk7) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1113,plain,
! [X0] :
( ~ sQ44_spl
| app(sk6,cons(sk5,nil)) = X0
| ~ ssList(X0)
| sk3 != app(X0,sk7) ),
inference(component_clause,[status(thm)],[f1112]) ).
fof(f1115,plain,
( ~ sQ12_spl
| ~ sQ20_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1102,f1112,f697,f588]) ).
fof(f1139,plain,
! [X0] :
( ~ sQ40_spl
| X0 = sk6
| ~ ssList(sk6)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ ssList(X0)
| app(X0,app(cons(sk5,nil),sk7)) != sk3 ),
inference(paramodulation,[status(thm)],[f1062,f377]) ).
fof(f1142,plain,
! [X0] :
( ~ sQ40_spl
| X0 = app(cons(sk5,nil),sk7)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ ssList(sk6)
| ~ ssList(X0)
| app(sk6,X0) != sk3 ),
inference(paramodulation,[status(thm)],[f1062,f375]) ).
fof(f1144,plain,
! [X0] :
( ~ sQ40_spl
| app(sk3,X0) = app(sk6,app(app(cons(sk5,nil),sk7),X0))
| ~ ssList(sk6)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1062,f373]) ).
fof(f1145,plain,
( ~ sQ40_spl
| frontsegP(sk3,sk6)
| ~ ssList(sk6)
| ~ ssList(app(cons(sk5,nil),sk7)) ),
inference(paramodulation,[status(thm)],[f1062,f516]) ).
fof(f1146,plain,
( ~ sQ40_spl
| rearsegP(sk3,app(cons(sk5,nil),sk7))
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f1062,f514]) ).
fof(f1148,definition,
( sQ46_spl
<=> ssList(app(cons(sk5,nil),sk7)) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1150,plain,
( sQ46_spl
| ~ ssList(app(cons(sk5,nil),sk7)) ),
inference(component_clause,[status(thm)],[f1148]) ).
fof(f1155,definition,
! [X0] :
( sQ48_spl
<=> ( X0 = sk6
| ~ ssList(X0)
| app(X0,app(cons(sk5,nil),sk7)) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1156,plain,
! [X0] :
( ~ sQ48_spl
| X0 = sk6
| ~ ssList(X0)
| app(X0,app(cons(sk5,nil),sk7)) != sk3 ),
inference(component_clause,[status(thm)],[f1155]) ).
fof(f1158,plain,
( ~ sQ40_spl
| ~ sQ23_spl
| ~ sQ46_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1139,f1155,f1148,f712,f1061]) ).
fof(f1161,definition,
! [X0] :
( sQ49_spl
<=> ( X0 = app(cons(sk5,nil),sk7)
| ~ ssList(X0)
| app(sk6,X0) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1162,plain,
! [X0] :
( ~ sQ49_spl
| X0 = app(cons(sk5,nil),sk7)
| ~ ssList(X0)
| app(sk6,X0) != sk3 ),
inference(component_clause,[status(thm)],[f1161]) ).
fof(f1164,plain,
( ~ sQ40_spl
| ~ sQ46_spl
| ~ sQ23_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f1142,f1161,f712,f1148,f1061]) ).
fof(f1166,definition,
! [X0] :
( sQ50_spl
<=> ( app(sk3,X0) = app(sk6,app(app(cons(sk5,nil),sk7),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1169,plain,
( ~ sQ40_spl
| ~ sQ23_spl
| ~ sQ46_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f1144,f1166,f1148,f712,f1061]) ).
fof(f1170,definition,
( sQ51_spl
<=> frontsegP(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1173,plain,
( ~ sQ40_spl
| sQ51_spl
| ~ sQ23_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f1145,f1148,f712,f1170,f1061]) ).
fof(f1174,definition,
( sQ52_spl
<=> rearsegP(sk3,app(cons(sk5,nil),sk7)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1177,plain,
( ~ sQ40_spl
| sQ52_spl
| ~ sQ46_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f1146,f712,f1148,f1174,f1061]) ).
fof(f1179,plain,
( sQ46_spl
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(resolution,[status(thm)],[f1150,f290]) ).
fof(f1180,plain,
( sQ46_spl
| ~ sQ22_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1179,f588,f709,f1148]) ).
fof(f1181,plain,
( ~ sQ41_spl
| sk7 = sk7
| ~ ssList(sk7) ),
inference(resolution,[status(thm)],[f1066,f532]) ).
fof(f1183,definition,
( sQ53_spl
<=> sk7 = sk7 ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1186,plain,
( ~ sQ41_spl
| sQ53_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1181,f588,f1183,f1065]) ).
fof(f1215,plain,
! [X0] :
( ~ sQ40_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(sk6)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ memberP(app(cons(sk5,nil),sk7),X0) ),
inference(paramodulation,[status(thm)],[f1062,f360]) ).
fof(f1216,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| ~ memberP(sk7,X0) ),
inference(paramodulation,[status(thm)],[f532,f360]) ).
fof(f1218,definition,
! [X0] :
( sQ56_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(cons(sk5,nil),sk7),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1219,plain,
! [X0] :
( ~ sQ56_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(cons(sk5,nil),sk7),X0) ),
inference(component_clause,[status(thm)],[f1218]) ).
fof(f1221,plain,
( ~ sQ40_spl
| ~ sQ23_spl
| ~ sQ46_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1215,f1218,f1148,f712,f1061]) ).
fof(f1222,definition,
! [X0] :
( sQ57_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1223,plain,
! [X0] :
( ~ sQ57_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(component_clause,[status(thm)],[f1222]) ).
fof(f1225,plain,
( ~ sQ20_spl
| ~ sQ12_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1216,f1222,f588,f697]) ).
fof(f1227,plain,
! [X0] :
( ~ sQ40_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(sk6)
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ memberP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f1062,f359]) ).
fof(f1228,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7)
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ),
inference(paramodulation,[status(thm)],[f532,f359]) ).
fof(f1230,definition,
! [X0] :
( sQ58_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1231,plain,
! [X0] :
( ~ sQ58_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk6,X0) ),
inference(component_clause,[status(thm)],[f1230]) ).
fof(f1233,plain,
( ~ sQ40_spl
| ~ sQ23_spl
| ~ sQ46_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1227,f1230,f1148,f712,f1061]) ).
fof(f1234,definition,
! [X0] :
( sQ59_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1235,plain,
! [X0] :
( ~ sQ59_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ),
inference(component_clause,[status(thm)],[f1234]) ).
fof(f1237,plain,
( ~ sQ20_spl
| ~ sQ12_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1228,f1234,f588,f697]) ).
fof(f1239,plain,
( ~ sQ2_spl
| ~ sQ58_spl
| memberP(sk3,sk8)
| ~ ssItem(sk8) ),
inference(resolution,[status(thm)],[f1231,f462]) ).
fof(f1240,definition,
( sQ60_spl
<=> ssItem(sk8) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1242,plain,
( sQ60_spl
| ~ ssItem(sk8) ),
inference(component_clause,[status(thm)],[f1240]) ).
fof(f1243,definition,
( sQ61_spl
<=> memberP(sk3,sk8) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1244,plain,
( ~ sQ61_spl
| memberP(sk3,sk8) ),
inference(component_clause,[status(thm)],[f1243]) ).
fof(f1246,plain,
( ~ sQ2_spl
| ~ sQ58_spl
| sQ61_spl
| ~ sQ60_spl ),
inference(split_clause,[status(thm)],[f1239,f1240,f1243,f1230,f461]) ).
fof(f1247,plain,
( ~ sQ57_spl
| ~ sQ3_spl
| memberP(sk3,sk8)
| ~ ssItem(sk8) ),
inference(resolution,[status(thm)],[f465,f1223]) ).
fof(f1248,plain,
( ~ sQ57_spl
| ~ sQ3_spl
| sQ61_spl
| ~ sQ60_spl ),
inference(split_clause,[status(thm)],[f1247,f1240,f1243,f464,f1222]) ).
fof(f1249,plain,
( sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1242,f445]) ).
fof(f1250,plain,
sQ60_spl,
inference(contradiction_clause,[status(thm)],[f1249]) ).
fof(f1316,plain,
! [X0] :
( ~ sQ44_spl
| sk6 = X0
| ~ ssList(X0)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk6)
| ~ ssList(app(X0,cons(sk5,nil)))
| sk3 != app(app(X0,cons(sk5,nil)),sk7) ),
inference(resolution,[status(thm)],[f1113,f377]) ).
fof(f1317,plain,
! [X0] :
( ~ sQ44_spl
| cons(sk5,nil) = X0
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(app(sk6,X0))
| sk3 != app(app(sk6,X0),sk7) ),
inference(resolution,[status(thm)],[f1113,f375]) ).
fof(f1318,plain,
! [X0] :
( ~ sQ44_spl
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssItem(X0)
| ~ ssList(cons(X0,app(sk6,cons(sk5,nil))))
| sk3 != app(cons(X0,app(sk6,cons(sk5,nil))),sk7) ),
inference(resolution,[status(thm)],[f1113,f306]) ).
fof(f1329,definition,
! [X0] :
( sQ67_spl
<=> ( sk6 = X0
| ~ ssList(X0)
| ~ ssList(app(X0,cons(sk5,nil)))
| sk3 != app(app(X0,cons(sk5,nil)),sk7) ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1332,plain,
( ~ sQ44_spl
| ~ sQ22_spl
| ~ sQ23_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1316,f1329,f712,f709,f1112]) ).
fof(f1333,definition,
! [X0] :
( sQ68_spl
<=> ( cons(sk5,nil) = X0
| ~ ssList(X0)
| ~ ssList(app(sk6,X0))
| sk3 != app(app(sk6,X0),sk7) ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1336,plain,
( ~ sQ44_spl
| ~ sQ23_spl
| ~ sQ22_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1317,f1333,f709,f712,f1112]) ).
fof(f1337,definition,
! [X0] :
( sQ69_spl
<=> ( ~ ssItem(X0)
| ~ ssList(cons(X0,app(sk6,cons(sk5,nil))))
| sk3 != app(cons(X0,app(sk6,cons(sk5,nil))),sk7) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1340,plain,
( ~ sQ44_spl
| ~ sQ20_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1318,f1337,f697,f1112]) ).
fof(f1343,plain,
( ~ sQ40_spl
| ~ sQ48_spl
| sk6 = sk6
| ~ ssList(sk6) ),
inference(resolution,[status(thm)],[f1156,f1062]) ).
fof(f1345,definition,
( sQ70_spl
<=> sk6 = sk6 ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1348,plain,
( ~ sQ40_spl
| ~ sQ48_spl
| sQ70_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f1343,f712,f1345,f1155,f1061]) ).
fof(f1355,plain,
! [X0] :
( ~ sQ49_spl
| ~ ssList(app(cons(sk5,nil),sk7))
| ~ ssItem(X0)
| ~ ssList(cons(X0,app(cons(sk5,nil),sk7)))
| app(sk6,cons(X0,app(cons(sk5,nil),sk7))) != sk3 ),
inference(resolution,[status(thm)],[f1162,f306]) ).
fof(f1356,plain,
! [X0] :
( ~ sQ49_spl
| X0 = cons(sk5,nil)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7)
| ~ ssList(X0)
| ~ ssList(app(X0,sk7))
| app(sk6,app(X0,sk7)) != sk3 ),
inference(resolution,[status(thm)],[f1162,f377]) ).
fof(f1357,plain,
! [X0] :
( ~ sQ49_spl
| X0 = sk7
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(X0)
| ~ ssList(app(cons(sk5,nil),X0))
| app(sk6,app(cons(sk5,nil),X0)) != sk3 ),
inference(resolution,[status(thm)],[f1162,f375]) ).
fof(f1362,definition,
! [X0] :
( sQ71_spl
<=> ( ~ ssItem(X0)
| ~ ssList(cons(X0,app(cons(sk5,nil),sk7)))
| app(sk6,cons(X0,app(cons(sk5,nil),sk7))) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1365,plain,
( ~ sQ49_spl
| ~ sQ46_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1355,f1362,f1148,f1161]) ).
fof(f1366,definition,
! [X0] :
( sQ72_spl
<=> ( X0 = cons(sk5,nil)
| ~ ssList(X0)
| ~ ssList(app(X0,sk7))
| app(sk6,app(X0,sk7)) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1369,plain,
( ~ sQ49_spl
| ~ sQ22_spl
| ~ sQ12_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f1356,f1366,f588,f709,f1161]) ).
fof(f1370,definition,
! [X0] :
( sQ73_spl
<=> ( X0 = sk7
| ~ ssList(X0)
| ~ ssList(app(cons(sk5,nil),X0))
| app(sk6,app(cons(sk5,nil),X0)) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1373,plain,
( ~ sQ49_spl
| ~ sQ12_spl
| ~ sQ22_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f1357,f1370,f709,f588,f1161]) ).
fof(f1382,plain,
! [X0] :
( ~ sQ56_spl
| ~ ssItem(X0)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7)
| ~ memberP(sk7,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1219,f360]) ).
fof(f1383,definition,
! [X0] :
( sQ75_spl
<=> ( ~ ssItem(X0)
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1384,plain,
! [X0] :
( ~ sQ75_spl
| ~ ssItem(X0)
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1383]) ).
fof(f1387,definition,
! [X0] :
( sQ76_spl
<=> ( ~ ssItem(X0)
| ~ memberP(sk7,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1390,plain,
( ~ sQ56_spl
| ~ sQ22_spl
| ~ sQ12_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f1382,f1387,f588,f709,f1218]) ).
fof(f1391,plain,
! [X0] :
( ~ sQ75_spl
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1384]) ).
fof(f1393,plain,
! [X0] :
( ~ sQ75_spl
| ~ ssItem(X0)
| ~ ssItem(sk5)
| ~ ssList(nil)
| ~ memberP(nil,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1391,f358]) ).
fof(f1395,definition,
! [X0] :
( sQ77_spl
<=> ( ~ ssItem(X0)
| ~ memberP(nil,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1398,plain,
( ~ sQ75_spl
| ~ sQ24_spl
| ~ sQ15_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f1393,f1395,f601,f717,f1383]) ).
fof(f1399,definition,
( sQ78_spl
<=> memberP(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1400,plain,
( ~ sQ78_spl
| memberP(sk3,sk5) ),
inference(component_clause,[status(thm)],[f1399]) ).
fof(f1404,plain,
( ~ sQ59_spl
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssItem(sk5)
| ~ ssList(sk6)
| ~ ssList(nil)
| memberP(sk3,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1235,f520]) ).
fof(f1405,plain,
! [X0] :
( ~ sQ59_spl
| ~ ssItem(X0)
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ memberP(sk6,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1235,f359]) ).
fof(f1406,plain,
! [X0] :
( ~ sQ59_spl
| ~ ssItem(X0)
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1235,f360]) ).
fof(f1407,plain,
( ~ sQ59_spl
| ~ sQ20_spl
| ~ sQ23_spl
| ~ sQ15_spl
| sQ78_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1404,f717,f1399,f601,f712,f697,f1234]) ).
fof(f1408,definition,
! [X0] :
( sQ79_spl
<=> ( ~ ssItem(X0)
| ~ memberP(sk6,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1411,plain,
( ~ sQ59_spl
| ~ sQ23_spl
| ~ sQ22_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1405,f1408,f709,f712,f1234]) ).
fof(f1412,plain,
( ~ sQ59_spl
| ~ sQ23_spl
| ~ sQ22_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f1406,f1383,f709,f712,f1234]) ).
fof(f1438,plain,
! [X0] :
( ~ sQ10_spl
| X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk9)
| ~ ssList(nil)
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f492,f396]) ).
fof(f1439,definition,
! [X0] :
( sQ84_spl
<=> ( X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1440,plain,
! [X0] :
( ~ sQ84_spl
| X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(component_clause,[status(thm)],[f1439]) ).
fof(f1442,plain,
( ~ sQ10_spl
| ~ sQ8_spl
| ~ sQ15_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f1438,f1439,f601,f484,f491]) ).
fof(f1443,plain,
! [X0] :
( ~ sQ84_spl
| X0 = sk9
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1440,f275]) ).
fof(f1444,plain,
( ~ sQ78_spl
| ~ sQ84_spl
| sk5 = sk9
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1443,f1400]) ).
fof(f1445,plain,
( ~ sQ61_spl
| ~ sQ84_spl
| sk8 = sk9
| ~ ssItem(sk8) ),
inference(resolution,[status(thm)],[f1443,f1244]) ).
fof(f1447,definition,
( sQ85_spl
<=> sk5 = sk9 ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1448,plain,
( ~ sQ85_spl
| sk5 = sk9 ),
inference(component_clause,[status(thm)],[f1447]) ).
fof(f1450,plain,
( ~ sQ78_spl
| ~ sQ84_spl
| sQ85_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1444,f717,f1447,f1439,f1399]) ).
fof(f1451,definition,
( sQ86_spl
<=> sk8 = sk9 ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1452,plain,
( ~ sQ86_spl
| sk8 = sk9 ),
inference(component_clause,[status(thm)],[f1451]) ).
fof(f1454,plain,
( ~ sQ61_spl
| ~ sQ84_spl
| sQ86_spl
| ~ sQ60_spl ),
inference(split_clause,[status(thm)],[f1445,f1240,f1451,f1439,f1243]) ).
fof(f1536,plain,
( ~ sQ78_spl
| ~ sQ6_spl
| ~ sQ28_spl
| memberP(sk7,sk5) ),
inference(backward_demodulation,[status(thm)],[f864,f1400]) ).
fof(f1847,plain,
( ~ sQ78_spl
| ~ sQ6_spl
| ~ sQ28_spl
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f873,f1536]) ).
fof(f1849,plain,
( ~ sQ78_spl
| ~ sQ6_spl
| ~ sQ28_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1847,f717,f747,f477,f1399]) ).
fof(f1851,plain,
( sQ4_spl
| ~ sQ85_spl
| ~ leq(sk9,sk8) ),
inference(backward_demodulation,[status(thm)],[f1448,f470]) ).
fof(f2025,plain,
( sQ4_spl
| ~ sQ85_spl
| ~ sQ86_spl
| ~ leq(sk9,sk9) ),
inference(forward_demodulation,[status(thm)],[f1452,f1851]) ).
fof(f2084,plain,
( sQ4_spl
| ~ sQ85_spl
| ~ sQ86_spl
| ~ ssItem(sk9) ),
inference(resolution,[status(thm)],[f2025,f266]) ).
fof(f2085,plain,
( sQ4_spl
| ~ sQ85_spl
| ~ sQ86_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2084,f484,f1451,f1447,f468]) ).
fof(f2086,plain,
( sQ5_spl
| ~ sQ86_spl
| ~ leq(sk9,sk5) ),
inference(forward_demodulation,[status(thm)],[f1452,f474]) ).
fof(f2087,plain,
( sQ5_spl
| ~ sQ86_spl
| ~ sQ85_spl
| ~ leq(sk9,sk9) ),
inference(forward_demodulation,[status(thm)],[f1448,f2086]) ).
fof(f2089,plain,
( ~ sQ4_spl
| ~ sQ85_spl
| leq(sk9,sk8) ),
inference(forward_demodulation,[status(thm)],[f1448,f469]) ).
fof(f2090,plain,
( ~ sQ4_spl
| ~ sQ85_spl
| ~ sQ86_spl
| leq(sk9,sk9) ),
inference(forward_demodulation,[status(thm)],[f1452,f2089]) ).
fof(f2091,plain,
( ~ sQ4_spl
| ~ sQ85_spl
| ~ sQ86_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2090,f2087]) ).
fof(f2092,plain,
( ~ sQ4_spl
| ~ sQ85_spl
| ~ sQ86_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f2091]) ).
fof(f2093,plain,
$false,
inference(sat_refutation,[status(thm)],[f467,f471,f476,f483,f490,f494,f607,f609,f611,f700,f705,f707,f715,f720,f722,f724,f729,f736,f750,f1037,f1064,f1068,f1073,f1110,f1115,f1158,f1164,f1169,f1173,f1177,f1180,f1186,f1221,f1225,f1233,f1237,f1246,f1248,f1250,f1332,f1336,f1340,f1348,f1365,f1369,f1373,f1390,f1398,f1407,f1411,f1412,f1442,f1450,f1454,f1849,f2085,f2092]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC284-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n006.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 08:11:57 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 1.29/0.69 % Refutation found
% 1.29/0.69 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.29/0.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.29/0.72 % Elapsed time: 0.338623 seconds
% 1.29/0.72 % CPU time: 2.427988 seconds
% 1.29/0.72 % Total memory used: 151.609 MB
% 1.29/0.72 % Net memory used: 149.368 MB
%------------------------------------------------------------------------------