%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC395-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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:41:04 PM UTC 2026
% Result : Unsatisfiable 21.47s 3.29s
% Output : CNFRefutation 21.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 71
% Syntax : Number of formulae : 260 ( 34 unt; 38 def)
% Number of atoms : 855 ( 128 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 1118 ( 523 ~; 557 |; 0 &)
% ( 38 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 46 ( 44 usr; 39 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-2 aty)
% Number of variables : 224 ( 224 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
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(f26,axiom,
! [U] : ssItem(skaf69(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [U,V] : ssList(skaf45(U,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [U,V] : ssList(skaf42(U,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [U,V] :
( ssItem(V)
| duplicatefreeP(U)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [U] :
( nil = U
| ssList(tl(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [U] :
( nil = U
| ssItem(hd(U))
| ~ ssList(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(f86,axiom,
! [U,V] :
( ssList(cons(U,V))
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [U,V] :
( V = U
| neq(V,U)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f102,axiom,
! [U,V] :
( V = U
| neq(V,U)
| ~ ssItem(V)
| ~ ssItem(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(f132,axiom,
! [U,V] :
( app(V,skaf45(U,V)) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,axiom,
! [U,V] :
( tl(app(V,U)) = app(tl(V),U)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,axiom,
! [U,V,W] :
( memberP(cons(V,W),U)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssList(W)
| U != V ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/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(f158,axiom,
! [U,V,W] :
( memberP(U,W)
| memberP(V,W)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(V)
| ~ memberP(app(U,V),W) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f179,axiom,
! [U,V,W,X,Y] :
( ~ ssList(Y)
| ~ duplicatefreeP(Y)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(X)
| app(app(U,cons(V,W)),cons(V,X)) != Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f187,negated_conjecture,
ssList(sk2),
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,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
memberP(sk1,sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
~ memberP(sk2,sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
( nil != sk4
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
! [A,B,C,D] :
( ~ neq(sk4,nil)
| ~ neq(nil,sk4)
| ~ neq(nil,sk4)
| hd(sk4) != D
| cons(D,nil) != C
| ~ ssItem(D)
| app(B,C) != A
| tl(sk4) != B
| ~ ssList(C)
| ~ ssList(B)
| sk3 = A
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f204,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f219,plain,
! [X0] : ssList(skaf72(X0)),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f220,plain,
! [X0] : ssList(skaf71(X0)),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f222,plain,
! [X0] : ssItem(skaf69(X0)),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f247,plain,
! [X0,X1] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f249,plain,
! [X0,X1] : ssList(skaf42(X0,X1)),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f267,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f268,plain,
( ! [V] : ssItem(V)
| ! [U] :
( duplicatefreeP(U)
| ~ ssList(U) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f269,plain,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f272,plain,
! [X0] :
( nil = X0
| ssList(tl(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f273,plain,
! [X0] :
( nil = X0
| ssItem(hd(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f282,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f283,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f299,plain,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f301,plain,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f303,plain,
! [X0] :
( nil = X0
| cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f341,plain,
! [X0,X1] :
( app(X1,skaf45(X0,X1)) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f342,plain,
! [X0,X1] :
( tl(app(X1,X0)) = app(tl(X1),X0)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f349,plain,
! [X0,X1,X2] :
( memberP(cons(X1,X2),X0)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f350,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(f352,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(f356,plain,
! [U,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f357,plain,
! [X0,X1,X2] :
( frontsegP(X2,X0)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f366,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f367,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f381,plain,
! [U,W] :
( memberP(U,W)
| ! [V] :
( memberP(V,W)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(V)
| ~ memberP(app(U,V),W) ) ),
inference(miniscoping,[status(thm)],[f158]) ).
fof(f382,plain,
! [X0,X1,X2] :
( memberP(X0,X2)
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ memberP(app(X0,X1),X2) ),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f387,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(f388,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)],[f387]) ).
fof(f413,plain,
! [Y] :
( ~ ssList(Y)
| ~ duplicatefreeP(Y)
| ! [V] :
( ~ ssItem(V)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| ! [X] :
( ~ ssList(X)
| app(app(U,cons(V,W)),cons(V,X)) != Y ) ) ) ) ),
inference(miniscoping,[status(thm)],[f179]) ).
fof(f414,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssList(X4)
| ~ duplicatefreeP(X4)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X3)
| app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4 ),
inference(cnf_transformation,[status(thm)],[f413]) ).
fof(f428,plain,
ssList(sk2),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f431,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f432,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f433,plain,
ssItem(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f434,plain,
memberP(sk1,sk5),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f435,plain,
~ memberP(sk2,sk5),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f436,plain,
( nil != sk4
| nil = sk3 ),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f437,plain,
( ~ neq(sk4,nil)
| ~ neq(nil,sk4)
| ~ neq(nil,sk4)
| ! [D] :
( hd(sk4) != D
| ! [C] :
( cons(D,nil) != C
| ~ ssItem(D)
| ! [A,B] :
( app(B,C) != A
| tl(sk4) != B
| ~ ssList(C)
| ~ ssList(B)
| sk3 = A
| ~ ssList(A) ) ) ) ),
inference(miniscoping,[status(thm)],[f196]) ).
fof(f438,plain,
! [X0,X1,X2,X3] :
( ~ neq(sk4,nil)
| ~ neq(nil,sk4)
| ~ neq(nil,sk4)
| hd(sk4) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk4) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk3 = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f437]) ).
fof(f439,definition,
! [X0] :
( sQ0_spl
<=> ( duplicatefreeP(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f440,plain,
! [X0] :
( ~ sQ0_spl
| duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f439]) ).
fof(f442,definition,
! [X1] :
( sQ1_spl
<=> ssItem(X1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f443,plain,
! [X0] :
( ~ sQ1_spl
| ssItem(X0) ),
inference(component_clause,[status(thm)],[f442]) ).
fof(f445,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f269,f439,f442]) ).
fof(f446,definition,
( sQ2_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f447,plain,
( ~ sQ2_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f449,definition,
( sQ3_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f451,plain,
( sQ3_spl
| nil != sk4 ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f436,f446,f449]) ).
fof(f453,definition,
! [X0,X1,X2,X3] :
( sQ4_spl
<=> ( hd(sk4) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk4) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk3 = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f454,plain,
! [X0,X1,X2,X3] :
( ~ sQ4_spl
| hd(sk4) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk4) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk3 = X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f453]) ).
fof(f456,definition,
( sQ5_spl
<=> neq(nil,sk4) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f458,plain,
( sQ5_spl
| ~ neq(nil,sk4) ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f459,definition,
( sQ6_spl
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f461,plain,
( sQ6_spl
| ~ neq(sk4,nil) ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f438,f453,f456,f459]) ).
fof(f475,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f349]) ).
fof(f476,plain,
! [X0,X1] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f475]) ).
fof(f478,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f357]) ).
fof(f485,plain,
! [X0,X1,X2,X3] :
( ~ ssList(app(app(X2,cons(X3,X1)),cons(X3,X0)))
| ~ duplicatefreeP(app(app(X2,cons(X3,X1)),cons(X3,X0)))
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f414]) ).
fof(f493,plain,
( sQ6_spl
| ~ neq(sk2,nil) ),
inference(forward_demodulation,[status(thm)],[f431,f461]) ).
fof(f496,plain,
( ~ sQ2_spl
| memberP(nil,sk5) ),
inference(backward_demodulation,[status(thm)],[f498,f434]) ).
fof(f498,plain,
( ~ sQ2_spl
| nil = sk1 ),
inference(forward_demodulation,[status(thm)],[f432,f447]) ).
fof(f499,plain,
( ~ sQ2_spl
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f496,f267]) ).
fof(f500,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f499,f433]) ).
fof(f501,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f500]) ).
fof(f502,plain,
( sQ3_spl
| nil != sk2 ),
inference(forward_demodulation,[status(thm)],[f431,f451]) ).
fof(f503,plain,
( sQ6_spl
| sk2 = nil
| ~ ssList(sk2)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f299,f493]) ).
fof(f506,definition,
( sQ7_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f508,plain,
( sQ7_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f506]) ).
fof(f509,definition,
( sQ8_spl
<=> ssList(sk2) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f511,plain,
( sQ8_spl
| ~ ssList(sk2) ),
inference(component_clause,[status(thm)],[f509]) ).
fof(f512,definition,
( sQ9_spl
<=> sk2 = nil ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f513,plain,
( ~ sQ9_spl
| sk2 = nil ),
inference(component_clause,[status(thm)],[f512]) ).
fof(f515,plain,
( sQ6_spl
| sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f503,f506,f509,f512,f459]) ).
fof(f516,plain,
( ~ sQ9_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f513,f502]) ).
fof(f517,plain,
( ~ sQ9_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f516]) ).
fof(f518,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f511,f428]) ).
fof(f519,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f518]) ).
fof(f520,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f508,f204]) ).
fof(f521,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f520]) ).
fof(f522,plain,
! [X0,X1,X2,X3] :
( ~ sQ4_spl
| hd(sk4) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk2) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk3 = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f431,f454]) ).
fof(f523,plain,
! [X0,X1,X2,X3] :
( ~ sQ4_spl
| hd(sk2) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk2) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk3 = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f431,f522]) ).
fof(f524,plain,
( ~ sQ4_spl
| ~ ssItem(hd(sk2))
| ~ ssList(cons(hd(sk2),nil))
| ~ ssList(tl(sk2))
| sk3 = app(tl(sk2),cons(hd(sk2),nil))
| ~ ssList(app(tl(sk2),cons(hd(sk2),nil))) ),
inference(destructive_equality_resolution,[status(thm)],[f523]) ).
fof(f525,plain,
( ~ sQ4_spl
| ~ ssItem(hd(sk2))
| ~ ssList(cons(hd(sk2),nil))
| ~ ssList(tl(sk2))
| sk3 = app(tl(sk2),cons(hd(sk2),nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[f524,f282]) ).
fof(f545,plain,
( ~ sQ4_spl
| ~ ssItem(hd(sk2))
| ~ ssList(cons(hd(sk2),nil))
| ~ ssList(tl(sk2))
| sk1 = app(tl(sk2),cons(hd(sk2),nil)) ),
inference(forward_demodulation,[status(thm)],[f432,f525]) ).
fof(f563,definition,
! [X1] :
( sQ15_spl
<=> ~ ssList(X1) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f564,plain,
! [X0] :
( ~ sQ15_spl
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f563]) ).
fof(f809,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(skaf45(app(X0,X1),X0))
| ~ ssList(app(X0,X1))
| ~ ssList(X0)
| ~ frontsegP(app(X0,X1),X0) ),
inference(resolution,[status(thm)],[f341,f367]) ).
fof(f813,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(skaf45(app(X0,X1),X0))
| ~ ssList(app(X0,X1))
| ~ ssList(X0)
| ~ frontsegP(app(X0,X1),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f809]) ).
fof(f814,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(skaf45(app(X0,X1),X0))
| ~ ssList(X0)
| ~ frontsegP(app(X0,X1),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f813,f282]) ).
fof(f902,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f478,f282]) ).
fof(f1063,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(skaf45(app(X0,X1),X0))
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f814,f902]) ).
fof(f1064,plain,
! [X0,X1] :
( skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1063,f247]) ).
fof(f1903,definition,
( sQ59_spl
<=> ssList(app(skaf71(nil),cons(skaf69(nil),skaf72(nil)))) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1904,plain,
( ~ sQ59_spl
| ssList(app(skaf71(nil),cons(skaf69(nil),skaf72(nil)))) ),
inference(component_clause,[status(thm)],[f1903]) ).
fof(f1905,plain,
( sQ59_spl
| ~ ssList(app(skaf71(nil),cons(skaf69(nil),skaf72(nil)))) ),
inference(component_clause,[status(thm)],[f1903]) ).
fof(f1999,plain,
( sQ59_spl
| ~ ssList(skaf71(nil))
| ~ ssList(cons(skaf69(nil),skaf72(nil))) ),
inference(resolution,[status(thm)],[f1905,f282]) ).
fof(f2000,definition,
( sQ75_spl
<=> ssList(cons(skaf69(nil),skaf72(nil))) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f2002,plain,
( sQ75_spl
| ~ ssList(cons(skaf69(nil),skaf72(nil))) ),
inference(component_clause,[status(thm)],[f2000]) ).
fof(f2003,definition,
( sQ76_spl
<=> ssList(skaf71(nil)) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f2005,plain,
( sQ76_spl
| ~ ssList(skaf71(nil)) ),
inference(component_clause,[status(thm)],[f2003]) ).
fof(f2006,plain,
( sQ59_spl
| ~ sQ76_spl
| ~ sQ75_spl ),
inference(split_clause,[status(thm)],[f1999,f2000,f2003,f1903]) ).
fof(f2007,plain,
( sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2005,f220]) ).
fof(f2008,plain,
sQ76_spl,
inference(contradiction_clause,[status(thm)],[f2007]) ).
fof(f2022,plain,
( sQ75_spl
| ~ ssList(skaf72(nil))
| ~ ssItem(skaf69(nil)) ),
inference(resolution,[status(thm)],[f2002,f283]) ).
fof(f2023,definition,
( sQ79_spl
<=> ssItem(skaf69(nil)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f2025,plain,
( sQ79_spl
| ~ ssItem(skaf69(nil)) ),
inference(component_clause,[status(thm)],[f2023]) ).
fof(f2026,definition,
( sQ80_spl
<=> ssList(skaf72(nil)) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f2028,plain,
( sQ80_spl
| ~ ssList(skaf72(nil)) ),
inference(component_clause,[status(thm)],[f2026]) ).
fof(f2029,plain,
( sQ75_spl
| ~ sQ80_spl
| ~ sQ79_spl ),
inference(split_clause,[status(thm)],[f2022,f2023,f2026,f2000]) ).
fof(f2030,plain,
( sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2028,f219]) ).
fof(f2031,plain,
sQ80_spl,
inference(contradiction_clause,[status(thm)],[f2030]) ).
fof(f2032,plain,
( sQ79_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2025,f222]) ).
fof(f2033,plain,
sQ79_spl,
inference(contradiction_clause,[status(thm)],[f2032]) ).
fof(f3100,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ ssList(app(app(X2,cons(X3,X1)),cons(X3,X0)))
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f485,f440]) ).
fof(f3101,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ ssList(app(X2,cons(X3,X1)))
| ~ ssList(cons(X3,X0))
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f3100,f282]) ).
fof(f3102,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ ssList(app(X2,cons(X3,X1)))
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3101,f283]) ).
fof(f3107,plain,
! [X0] :
( ~ sQ59_spl
| ~ sQ0_spl
| ~ ssItem(skaf69(nil))
| ~ ssList(skaf71(nil))
| ~ ssList(skaf72(nil))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f3102,f1904]) ).
fof(f3113,plain,
( ~ sQ59_spl
| ~ sQ0_spl
| ~ sQ79_spl
| ~ sQ76_spl
| ~ sQ80_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f3107,f563,f2026,f2003,f2023,f439,f1903]) ).
fof(f3119,plain,
( ~ sQ15_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f249,f564]) ).
fof(f3166,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f3119]) ).
fof(f3167,definition,
( sQ134_spl
<=> sk1 = app(tl(sk2),cons(hd(sk2),nil)) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f3168,plain,
( ~ sQ134_spl
| sk1 = app(tl(sk2),cons(hd(sk2),nil)) ),
inference(component_clause,[status(thm)],[f3167]) ).
fof(f3170,definition,
( sQ135_spl
<=> ssList(tl(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f3172,plain,
( sQ135_spl
| ~ ssList(tl(sk2)) ),
inference(component_clause,[status(thm)],[f3170]) ).
fof(f3173,definition,
( sQ136_spl
<=> ssList(cons(hd(sk2),nil)) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f3175,plain,
( sQ136_spl
| ~ ssList(cons(hd(sk2),nil)) ),
inference(component_clause,[status(thm)],[f3173]) ).
fof(f3176,definition,
( sQ137_spl
<=> ssItem(hd(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f3178,plain,
( sQ137_spl
| ~ ssItem(hd(sk2)) ),
inference(component_clause,[status(thm)],[f3176]) ).
fof(f3179,plain,
( ~ sQ4_spl
| ~ sQ137_spl
| ~ sQ136_spl
| ~ sQ135_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f545,f3167,f3170,f3173,f3176,f453]) ).
fof(f3181,plain,
( sQ5_spl
| ~ neq(nil,sk2) ),
inference(forward_demodulation,[status(thm)],[f431,f458]) ).
fof(f3182,plain,
( sQ5_spl
| nil = sk2
| ~ ssItem(nil)
| ~ ssItem(sk2) ),
inference(resolution,[status(thm)],[f3181,f301]) ).
fof(f3183,definition,
( sQ138_spl
<=> ssItem(sk2) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f3185,plain,
( sQ138_spl
| ~ ssItem(sk2) ),
inference(component_clause,[status(thm)],[f3183]) ).
fof(f3186,definition,
( sQ139_spl
<=> ssItem(nil) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f3188,plain,
( sQ139_spl
| ~ ssItem(nil) ),
inference(component_clause,[status(thm)],[f3186]) ).
fof(f3189,plain,
( sQ5_spl
| sQ9_spl
| ~ sQ139_spl
| ~ sQ138_spl ),
inference(split_clause,[status(thm)],[f3182,f3183,f3186,f512,f456]) ).
fof(f3194,plain,
( sQ137_spl
| nil = sk2
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f273,f3178]) ).
fof(f3195,plain,
( sQ137_spl
| sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3194,f509,f512,f3176]) ).
fof(f3253,plain,
! [X0] :
( ~ sQ1_spl
| ~ memberP(nil,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f267,f443]) ).
fof(f3255,plain,
( sQ138_spl
| ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3185,f443]) ).
fof(f3256,plain,
( sQ139_spl
| ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3188,f443]) ).
fof(f3302,plain,
( sQ138_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f3255]) ).
fof(f3303,plain,
( sQ139_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f3256]) ).
fof(f3310,plain,
! [X0,X1] :
( ~ sQ1_spl
| ssList(cons(X1,X0))
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f283,f443]) ).
fof(f3311,plain,
( sQ136_spl
| ~ sQ1_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f3310,f3175]) ).
fof(f3312,plain,
( sQ136_spl
| ~ sQ1_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f3311,f506,f442,f3173]) ).
fof(f3341,plain,
( ~ sQ134_spl
| ssList(sk1)
| ~ ssList(tl(sk2))
| ~ ssList(cons(hd(sk2),nil)) ),
inference(paramodulation,[status(thm)],[f3168,f282]) ).
fof(f3364,definition,
( sQ146_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f3367,plain,
( ~ sQ134_spl
| sQ146_spl
| ~ sQ135_spl
| ~ sQ136_spl ),
inference(split_clause,[status(thm)],[f3341,f3173,f3170,f3364,f3167]) ).
fof(f3376,plain,
( sQ135_spl
| nil = sk2
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f3172,f272]) ).
fof(f3377,plain,
( sQ135_spl
| sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3376,f509,f512,f3170]) ).
fof(f3403,plain,
! [X0,X1] :
( ~ sQ1_spl
| memberP(cons(X1,X0),X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f476,f443]) ).
fof(f3445,plain,
( ~ sQ134_spl
| skaf45(sk1,tl(sk2)) = cons(hd(sk2),nil)
| ~ ssList(cons(hd(sk2),nil))
| ~ ssList(tl(sk2)) ),
inference(paramodulation,[status(thm)],[f3168,f1064]) ).
fof(f3446,definition,
( sQ154_spl
<=> skaf45(sk1,tl(sk2)) = cons(hd(sk2),nil) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f3447,plain,
( ~ sQ154_spl
| skaf45(sk1,tl(sk2)) = cons(hd(sk2),nil) ),
inference(component_clause,[status(thm)],[f3446]) ).
fof(f3449,plain,
( ~ sQ134_spl
| sQ154_spl
| ~ sQ136_spl
| ~ sQ135_spl ),
inference(split_clause,[status(thm)],[f3445,f3170,f3173,f3446,f3167]) ).
fof(f3456,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| memberP(app(X2,X0),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f352,f443]) ).
fof(f3473,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| memberP(cons(X2,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f350,f443]) ).
fof(f3484,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| X2 = X0
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f388,f443]) ).
fof(f3494,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| memberP(X0,X2)
| memberP(X1,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ memberP(app(X0,X1),X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f382,f443]) ).
fof(f3524,plain,
( ~ sQ134_spl
| ~ sQ154_spl
| sk1 = app(tl(sk2),skaf45(sk1,tl(sk2))) ),
inference(backward_demodulation,[status(thm)],[f3447,f3168]) ).
fof(f3537,plain,
! [X0] :
( ~ sQ154_spl
| ~ sQ1_spl
| X0 = hd(sk2)
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssList(nil)
| ~ memberP(skaf45(sk1,tl(sk2)),X0) ),
inference(paramodulation,[status(thm)],[f3447,f3484]) ).
fof(f3549,plain,
( ~ sQ154_spl
| ~ sQ1_spl
| memberP(skaf45(sk1,tl(sk2)),hd(sk2))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f3447,f3403]) ).
fof(f3560,plain,
( ~ sQ154_spl
| ~ sQ1_spl
| ssList(skaf45(sk1,tl(sk2)))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f3447,f3310]) ).
fof(f3580,definition,
! [X0] :
( sQ167_spl
<=> ( X0 = hd(sk2)
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(skaf45(sk1,tl(sk2)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f3581,plain,
! [X0] :
( ~ sQ167_spl
| X0 = hd(sk2)
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(skaf45(sk1,tl(sk2)),X0) ),
inference(component_clause,[status(thm)],[f3580]) ).
fof(f3583,plain,
( ~ sQ154_spl
| ~ sQ1_spl
| ~ sQ7_spl
| sQ167_spl ),
inference(split_clause,[status(thm)],[f3537,f3580,f506,f442,f3446]) ).
fof(f3634,definition,
( sQ181_spl
<=> memberP(skaf45(sk1,tl(sk2)),hd(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f3635,plain,
( ~ sQ181_spl
| memberP(skaf45(sk1,tl(sk2)),hd(sk2)) ),
inference(component_clause,[status(thm)],[f3634]) ).
fof(f3637,plain,
( ~ sQ154_spl
| ~ sQ1_spl
| sQ181_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f3549,f506,f3634,f442,f3446]) ).
fof(f3678,definition,
( sQ192_spl
<=> ssList(skaf45(sk1,tl(sk2))) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f3681,plain,
( ~ sQ154_spl
| ~ sQ1_spl
| sQ192_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f3560,f506,f3678,f442,f3446]) ).
fof(f3707,plain,
! [X0] :
( ~ sQ167_spl
| ~ sQ1_spl
| X0 = hd(sk2)
| memberP(nil,X0)
| ~ memberP(skaf45(sk1,tl(sk2)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3581,f443]) ).
fof(f3800,plain,
( ~ sQ134_spl
| ~ sQ154_spl
| tl(app(sk2,skaf45(sk1,tl(sk2)))) = sk1
| nil = sk2
| ~ ssList(sk2)
| ~ ssList(skaf45(sk1,tl(sk2))) ),
inference(paramodulation,[status(thm)],[f3524,f342]) ).
fof(f3802,definition,
( sQ210_spl
<=> tl(app(sk2,skaf45(sk1,tl(sk2)))) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f3803,plain,
( ~ sQ210_spl
| tl(app(sk2,skaf45(sk1,tl(sk2)))) = sk1 ),
inference(component_clause,[status(thm)],[f3802]) ).
fof(f3805,plain,
( ~ sQ134_spl
| ~ sQ154_spl
| sQ210_spl
| sQ9_spl
| ~ sQ8_spl
| ~ sQ192_spl ),
inference(split_clause,[status(thm)],[f3800,f3678,f509,f512,f3802,f3446,f3167]) ).
fof(f3825,definition,
( sQ214_spl
<=> ssList(app(sk2,skaf45(sk1,tl(sk2)))) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f3827,plain,
( sQ214_spl
| ~ ssList(app(sk2,skaf45(sk1,tl(sk2)))) ),
inference(component_clause,[status(thm)],[f3825]) ).
fof(f3828,definition,
( sQ215_spl
<=> nil = app(sk2,skaf45(sk1,tl(sk2))) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f3829,plain,
( ~ sQ215_spl
| nil = app(sk2,skaf45(sk1,tl(sk2))) ),
inference(component_clause,[status(thm)],[f3828]) ).
fof(f3840,plain,
! [X0] :
( ~ sQ215_spl
| ~ sQ1_spl
| memberP(nil,X0)
| ~ ssList(sk2)
| ~ ssList(skaf45(sk1,tl(sk2)))
| ~ memberP(skaf45(sk1,tl(sk2)),X0) ),
inference(paramodulation,[status(thm)],[f3829,f3456]) ).
fof(f3868,definition,
! [X0] :
( sQ221_spl
<=> ( memberP(nil,X0)
| ~ memberP(skaf45(sk1,tl(sk2)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f3869,plain,
! [X0] :
( ~ sQ221_spl
| memberP(nil,X0)
| ~ memberP(skaf45(sk1,tl(sk2)),X0) ),
inference(component_clause,[status(thm)],[f3868]) ).
fof(f3871,plain,
( ~ sQ215_spl
| ~ sQ1_spl
| ~ sQ8_spl
| ~ sQ192_spl
| sQ221_spl ),
inference(split_clause,[status(thm)],[f3840,f3868,f3678,f509,f442,f3828]) ).
fof(f3897,plain,
! [X0] :
( ~ sQ167_spl
| ~ sQ1_spl
| X0 = hd(sk2)
| ~ memberP(skaf45(sk1,tl(sk2)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3707,f3253]) ).
fof(f3922,plain,
( sQ214_spl
| ~ ssList(sk2)
| ~ ssList(skaf45(sk1,tl(sk2))) ),
inference(resolution,[status(thm)],[f3827,f282]) ).
fof(f3923,plain,
( sQ214_spl
| ~ sQ8_spl
| ~ sQ192_spl ),
inference(split_clause,[status(thm)],[f3922,f3678,f509,f3825]) ).
fof(f3925,plain,
! [X0] :
( ~ sQ221_spl
| ~ sQ1_spl
| ~ memberP(skaf45(sk1,tl(sk2)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3869,f3253]) ).
fof(f3949,plain,
( ~ sQ181_spl
| ~ sQ221_spl
| ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3635,f3925]) ).
fof(f3951,plain,
( ~ sQ181_spl
| ~ sQ221_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f3949]) ).
fof(f4243,plain,
( ~ sQ210_spl
| nil = app(sk2,skaf45(sk1,tl(sk2)))
| cons(hd(app(sk2,skaf45(sk1,tl(sk2)))),sk1) = app(sk2,skaf45(sk1,tl(sk2)))
| ~ ssList(app(sk2,skaf45(sk1,tl(sk2)))) ),
inference(paramodulation,[status(thm)],[f3803,f303]) ).
fof(f4254,definition,
( sQ256_spl
<=> cons(hd(app(sk2,skaf45(sk1,tl(sk2)))),sk1) = app(sk2,skaf45(sk1,tl(sk2))) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f4255,plain,
( ~ sQ256_spl
| cons(hd(app(sk2,skaf45(sk1,tl(sk2)))),sk1) = app(sk2,skaf45(sk1,tl(sk2))) ),
inference(component_clause,[status(thm)],[f4254]) ).
fof(f4257,plain,
( ~ sQ210_spl
| sQ215_spl
| sQ256_spl
| ~ sQ214_spl ),
inference(split_clause,[status(thm)],[f4243,f3825,f4254,f3828,f3802]) ).
fof(f4272,plain,
! [X0] :
( ~ sQ256_spl
| ~ sQ1_spl
| memberP(app(sk2,skaf45(sk1,tl(sk2))),X0)
| ~ ssItem(X0)
| ~ ssList(sk1)
| ~ memberP(sk1,X0) ),
inference(paramodulation,[status(thm)],[f4255,f3473]) ).
fof(f4349,definition,
! [X0] :
( sQ271_spl
<=> ( memberP(app(sk2,skaf45(sk1,tl(sk2))),X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).
fof(f4350,plain,
! [X0] :
( ~ sQ271_spl
| memberP(app(sk2,skaf45(sk1,tl(sk2))),X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(component_clause,[status(thm)],[f4349]) ).
fof(f4352,plain,
( ~ sQ256_spl
| ~ sQ1_spl
| ~ sQ146_spl
| sQ271_spl ),
inference(split_clause,[status(thm)],[f4272,f4349,f3364,f442,f4254]) ).
fof(f4470,plain,
! [X0] :
( ~ sQ271_spl
| ~ sQ1_spl
| memberP(app(sk2,skaf45(sk1,tl(sk2))),X0)
| ~ memberP(sk1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4350,f443]) ).
fof(f4539,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ271_spl
| memberP(sk2,X0)
| memberP(skaf45(sk1,tl(sk2)),X0)
| ~ ssList(sk2)
| ~ ssList(skaf45(sk1,tl(sk2)))
| ~ memberP(sk1,X0) ),
inference(resolution,[status(thm)],[f4470,f3494]) ).
fof(f4540,definition,
! [X0] :
( sQ306_spl
<=> ( memberP(sk2,X0)
| memberP(skaf45(sk1,tl(sk2)),X0)
| ~ memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition]) ).
fof(f4541,plain,
! [X0] :
( ~ sQ306_spl
| memberP(sk2,X0)
| memberP(skaf45(sk1,tl(sk2)),X0)
| ~ memberP(sk1,X0) ),
inference(component_clause,[status(thm)],[f4540]) ).
fof(f4543,plain,
( ~ sQ1_spl
| ~ sQ271_spl
| ~ sQ8_spl
| ~ sQ192_spl
| sQ306_spl ),
inference(split_clause,[status(thm)],[f4539,f4540,f3678,f509,f4349,f442]) ).
fof(f4555,plain,
! [X0] :
( ~ sQ167_spl
| ~ sQ1_spl
| ~ sQ306_spl
| X0 = hd(sk2)
| memberP(sk2,X0)
| ~ memberP(sk1,X0) ),
inference(resolution,[status(thm)],[f4541,f3897]) ).
fof(f4557,plain,
( ~ sQ167_spl
| ~ sQ1_spl
| ~ sQ306_spl
| sk5 = hd(sk2)
| ~ memberP(sk1,sk5) ),
inference(resolution,[status(thm)],[f4555,f435]) ).
fof(f4558,definition,
( sQ309_spl
<=> memberP(sk1,sk5) ),
introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition]) ).
fof(f4560,plain,
( sQ309_spl
| ~ memberP(sk1,sk5) ),
inference(component_clause,[status(thm)],[f4558]) ).
fof(f4561,definition,
( sQ310_spl
<=> sk5 = hd(sk2) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f4562,plain,
( ~ sQ310_spl
| sk5 = hd(sk2) ),
inference(component_clause,[status(thm)],[f4561]) ).
fof(f4564,plain,
( ~ sQ167_spl
| ~ sQ1_spl
| ~ sQ306_spl
| sQ310_spl
| ~ sQ309_spl ),
inference(split_clause,[status(thm)],[f4557,f4558,f4561,f4540,f442,f3580]) ).
fof(f4565,plain,
( sQ309_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4560,f434]) ).
fof(f4566,plain,
sQ309_spl,
inference(contradiction_clause,[status(thm)],[f4565]) ).
fof(f4580,plain,
( ~ sQ310_spl
| nil = sk2
| cons(sk5,tl(sk2)) = sk2
| ~ ssList(sk2) ),
inference(paramodulation,[status(thm)],[f4562,f303]) ).
fof(f4590,definition,
( sQ311_spl
<=> cons(sk5,tl(sk2)) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ311_spl])],[split_symbol_definition]) ).
fof(f4591,plain,
( ~ sQ311_spl
| cons(sk5,tl(sk2)) = sk2 ),
inference(component_clause,[status(thm)],[f4590]) ).
fof(f4593,plain,
( ~ sQ310_spl
| sQ9_spl
| sQ311_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f4580,f509,f4590,f512,f4561]) ).
fof(f4630,plain,
( ~ sQ311_spl
| ~ sQ1_spl
| memberP(sk2,sk5)
| ~ ssList(tl(sk2)) ),
inference(paramodulation,[status(thm)],[f4591,f3403]) ).
fof(f4716,definition,
( sQ334_spl
<=> memberP(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ334_spl])],[split_symbol_definition]) ).
fof(f4717,plain,
( ~ sQ334_spl
| memberP(sk2,sk5) ),
inference(component_clause,[status(thm)],[f4716]) ).
fof(f4719,plain,
( ~ sQ311_spl
| ~ sQ1_spl
| sQ334_spl
| ~ sQ135_spl ),
inference(split_clause,[status(thm)],[f4630,f3170,f4716,f442,f4590]) ).
fof(f4794,plain,
( ~ sQ334_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4717,f435]) ).
fof(f4795,plain,
~ sQ334_spl,
inference(contradiction_clause,[status(thm)],[f4794]) ).
fof(f4796,plain,
$false,
inference(sat_refutation,[status(thm)],[f445,f452,f462,f501,f515,f517,f519,f521,f2006,f2008,f2029,f2031,f2033,f3113,f3166,f3179,f3189,f3195,f3302,f3303,f3312,f3367,f3377,f3449,f3583,f3637,f3681,f3805,f3871,f3923,f3951,f4257,f4352,f4543,f4564,f4566,f4593,f4719,f4795]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC395-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 08:23:29 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 21.47/3.29 % Refutation found
% 21.47/3.29 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 21.47/3.29 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 21.47/3.37 % Elapsed time: 2.991136 seconds
% 21.47/3.37 % CPU time: 23.195976 seconds
% 21.47/3.37 % Total memory used: 243.777 MB
% 21.47/3.37 % Net memory used: 232.385 MB
%------------------------------------------------------------------------------