%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC120-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 : n012.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:02 PM UTC 2026
% Result : Unsatisfiable 284.52s 41.18s
% Output : CNFRefutation 284.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 99
% Syntax : Number of formulae : 366 ( 51 unt; 65 def)
% Number of atoms : 1059 ( 164 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1297 ( 604 ~; 628 |; 0 &)
% ( 65 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 73 ( 71 usr; 66 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-2 aty)
% Number of variables : 203 ( 203 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
duplicatefreeP(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [U] : ssItem(skaf83(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [U] : ssList(skaf82(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [U,V] : ssList(skaf46(U,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [U,V] : ssList(skaf45(U,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [U,V] :
( ssItem(V)
| duplicatefreeP(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(f75,axiom,
! [U] :
( nil = U
| ssList(tl(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [U] :
( nil = U
| ssItem(hd(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [U] :
( frontsegP(nil,U)
| ~ ssList(U)
| nil != 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(f96,axiom,
! [U,V] :
( tl(cons(U,V)) = 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(f104,axiom,
! [U] :
( nil = U
| cons(hd(U),tl(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [U] :
( nil = U
| cons(skaf83(U),skaf82(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,axiom,
! [U,V] :
( ~ ssList(U)
| ~ ssList(V)
| ~ neq(U,V)
| U != V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ frontsegP(V,U)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f132,axiom,
! [U,V] :
( app(V,skaf45(U,V)) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f137,axiom,
! [U,V,W] :
( frontsegP(app(U,W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(U,V) ),
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(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(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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f186,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f187,negated_conjecture,
ssList(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,negated_conjecture,
sk2 = 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,
( neq(sk2,nil)
| neq(sk2,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
! [A,B] :
( ~ neq(sk4,nil)
| ~ neq(nil,sk4)
| app(sk3,B) != A
| tl(sk4) != B
| ~ ssList(B)
| sk4 = A
| ~ ssList(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
( ~ neq(sk4,nil)
| ~ segmentP(sk2,sk1)
| ~ neq(sk1,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,plain,
duplicatefreeP(nil),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f205,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f209,plain,
! [X0] : ssItem(skaf83(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f210,plain,
! [X0] : ssList(skaf82(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f247,plain,
! [X0,X1] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f248,plain,
! [X0,X1] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f257,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f269,plain,
( ! [V] : ssItem(V)
| ! [U] :
( duplicatefreeP(U)
| ~ ssList(U) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f270,plain,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f272,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f273,plain,
! [X0] :
( nil = X0
| ssList(tl(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f274,plain,
! [X0] :
( nil = X0
| ssItem(hd(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f281,plain,
! [X0] :
( frontsegP(nil,X0)
| ~ ssList(X0)
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f283,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f284,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f294,plain,
! [X0,X1] :
( tl(cons(X0,X1)) = X1
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f298,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != V ) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f299,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != X1 ),
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f300,plain,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f304,plain,
! [X0] :
( nil = X0
| cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f309,plain,
! [X0] :
( nil = X0
| cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f318,plain,
! [U] :
( ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ neq(U,V)
| U != V ) ),
inference(miniscoping,[status(thm)],[f115]) ).
fof(f319,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ neq(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f339,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f342,plain,
! [X0,X1] :
( app(X1,skaf45(X0,X1)) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f349,plain,
! [X0,X1,X2] :
( frontsegP(app(X0,X2),X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f357,plain,
! [U,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f358,plain,
! [X0,X1,X2] :
( frontsegP(X2,X0)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f357]) ).
fof(f367,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f368,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f403,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(f404,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)],[f403]) ).
fof(f414,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(f415,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)],[f414]) ).
fof(f428,plain,
ssList(sk1),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f429,plain,
ssList(sk2),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f432,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f433,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f434,plain,
( neq(sk2,nil)
| neq(sk2,nil) ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f439,plain,
( ~ neq(sk4,nil)
| ~ neq(nil,sk4)
| ! [A,B] :
( app(sk3,B) != A
| tl(sk4) != B
| ~ ssList(B)
| sk4 = A
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f196]) ).
fof(f440,plain,
! [X0,X1] :
( ~ neq(sk4,nil)
| ~ neq(nil,sk4)
| app(sk3,X1) != X0
| tl(sk4) != X1
| ~ ssList(X1)
| sk4 = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f439]) ).
fof(f441,plain,
( ~ neq(sk4,nil)
| ~ segmentP(sk2,sk1)
| ~ neq(sk1,nil) ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f442,definition,
! [X0] :
( sQ0_spl
<=> ( duplicatefreeP(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f443,plain,
! [X0] :
( ~ sQ0_spl
| duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f442]) ).
fof(f445,definition,
! [X1] :
( sQ1_spl
<=> ssItem(X1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f446,plain,
! [X0] :
( ~ sQ1_spl
| ssItem(X0) ),
inference(component_clause,[status(thm)],[f445]) ).
fof(f448,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f270,f442,f445]) ).
fof(f449,definition,
( sQ2_spl
<=> neq(sk2,nil) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f450,plain,
( ~ sQ2_spl
| neq(sk2,nil) ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,plain,
sQ2_spl,
inference(split_clause,[status(thm)],[f434,f449]) ).
fof(f453,definition,
( sQ3_spl
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( sQ3_spl
| ~ neq(sk4,nil) ),
inference(component_clause,[status(thm)],[f453]) ).
fof(f457,definition,
! [X0,X1] :
( sQ4_spl
<=> ( app(sk3,X1) != X0
| tl(sk4) != X1
| ~ ssList(X1)
| sk4 = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f458,plain,
! [X0,X1] :
( ~ sQ4_spl
| app(sk3,X1) != X0
| tl(sk4) != X1
| ~ ssList(X1)
| sk4 = X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f457]) ).
fof(f460,definition,
( sQ5_spl
<=> neq(nil,sk4) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f462,plain,
( sQ5_spl
| ~ neq(nil,sk4) ),
inference(component_clause,[status(thm)],[f460]) ).
fof(f464,definition,
( sQ6_spl
<=> neq(sk1,nil) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( sQ6_spl
| ~ neq(sk1,nil) ),
inference(component_clause,[status(thm)],[f464]) ).
fof(f467,definition,
( sQ7_spl
<=> segmentP(sk2,sk1) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( ~ sQ3_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f440,f457,f460,f453]) ).
fof(f472,plain,
( ~ sQ3_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f441,f464,f467,f453]) ).
fof(f475,plain,
! [X1] :
( ~ ssList(X1)
| ~ ssList(X1)
| ~ neq(X1,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f319]) ).
fof(f476,plain,
! [X0] :
( ~ ssList(X0)
| ~ neq(X0,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f475]) ).
fof(f483,plain,
( sQ3_spl
| ~ neq(sk2,nil) ),
inference(backward_demodulation,[status(thm)],[f432,f455]) ).
fof(f485,plain,
( sQ3_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f483,f450]) ).
fof(f486,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f485]) ).
fof(f487,plain,
! [X0,X1] :
( ~ sQ4_spl
| app(sk3,X1) != X0
| tl(sk4) != X1
| ~ ssList(X1)
| sk2 = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f432,f458]) ).
fof(f488,plain,
! [X0,X1] :
( ~ sQ4_spl
| app(sk3,X1) != X0
| tl(sk2) != X1
| ~ ssList(X1)
| sk2 = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f432,f487]) ).
fof(f490,plain,
( sQ6_spl
| sk1 = nil
| ~ ssList(sk1)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f300,f466]) ).
fof(f493,definition,
( sQ8_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f495,plain,
( sQ8_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f493]) ).
fof(f496,definition,
( sQ9_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f498,plain,
( sQ9_spl
| ~ ssList(sk1) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f499,definition,
( sQ10_spl
<=> sk1 = nil ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f500,plain,
( ~ sQ10_spl
| sk1 = nil ),
inference(component_clause,[status(thm)],[f499]) ).
fof(f502,plain,
( sQ6_spl
| sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f490,f493,f496,f499,f464]) ).
fof(f503,plain,
( sQ5_spl
| ~ neq(nil,sk2) ),
inference(forward_demodulation,[status(thm)],[f432,f462]) ).
fof(f504,plain,
( sQ5_spl
| nil = sk2
| ~ ssList(nil)
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f503,f300]) ).
fof(f505,definition,
( sQ11_spl
<=> ssList(sk2) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f507,plain,
( sQ11_spl
| ~ ssList(sk2) ),
inference(component_clause,[status(thm)],[f505]) ).
fof(f508,definition,
( sQ12_spl
<=> nil = sk2 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f509,plain,
( ~ sQ12_spl
| nil = sk2 ),
inference(component_clause,[status(thm)],[f508]) ).
fof(f511,plain,
( sQ5_spl
| sQ12_spl
| ~ sQ8_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f504,f505,f493,f508,f460]) ).
fof(f512,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f495,f205]) ).
fof(f513,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f512]) ).
fof(f514,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f507,f429]) ).
fof(f515,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f514]) ).
fof(f538,plain,
( ~ sQ2_spl
| ~ sQ12_spl
| neq(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f509,f450]) ).
fof(f541,plain,
( ~ sQ2_spl
| ~ sQ12_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f538,f476]) ).
fof(f542,plain,
( ~ sQ2_spl
| ~ sQ12_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f541,f493,f508,f449]) ).
fof(f544,plain,
! [X0,X1] :
( ~ sQ4_spl
| app(sk1,X1) != X0
| tl(sk2) != X1
| ~ ssList(X1)
| sk2 = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f433,f488]) ).
fof(f549,plain,
! [X0] :
( ~ sQ4_spl
| tl(sk2) != X0
| ~ ssList(X0)
| sk2 = app(sk1,X0)
| ~ ssList(app(sk1,X0)) ),
inference(equality_resolution,[status(thm)],[f544]) ).
fof(f557,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f498,f428]) ).
fof(f558,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f557]) ).
fof(f742,plain,
! [X0] :
( ~ sQ4_spl
| ~ ssList(X0)
| ~ ssList(sk1)
| ~ frontsegP(X0,sk1)
| tl(sk2) != skaf45(X0,sk1)
| ~ ssList(skaf45(X0,sk1))
| sk2 = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f544,f342]) ).
fof(f752,definition,
! [X0] :
( sQ38_spl
<=> ( ~ ssList(X0)
| ~ frontsegP(X0,sk1)
| tl(sk2) != skaf45(X0,sk1)
| ~ ssList(skaf45(X0,sk1))
| sk2 = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f753,plain,
! [X0] :
( ~ sQ38_spl
| ~ ssList(X0)
| ~ frontsegP(X0,sk1)
| tl(sk2) != skaf45(X0,sk1)
| ~ ssList(skaf45(X0,sk1))
| sk2 = X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f752]) ).
fof(f755,plain,
( ~ sQ4_spl
| ~ sQ9_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f742,f752,f496,f457]) ).
fof(f757,plain,
! [X0] :
( ~ sQ38_spl
| ~ frontsegP(X0,sk1)
| tl(sk2) != skaf45(X0,sk1)
| ~ ssList(skaf45(X0,sk1))
| sk2 = X0
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f753]) ).
fof(f758,plain,
! [X0] :
( ~ sQ38_spl
| ~ frontsegP(X0,sk1)
| tl(sk2) != skaf45(X0,sk1)
| sk2 = X0
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f757,f248]) ).
fof(f759,plain,
! [X0] :
( ~ sQ4_spl
| tl(sk2) != X0
| ~ ssList(X0)
| sk2 = sk2
| ~ ssList(sk2)
| tl(sk2) != X0
| ~ ssList(X0)
| ~ ssList(app(sk1,X0)) ),
inference(resolution,[status(thm)],[f549,f544]) ).
fof(f760,definition,
! [X0] :
( sQ39_spl
<=> ( tl(sk2) != X0
| ~ ssList(X0)
| tl(sk2) != X0
| ~ ssList(X0)
| ~ ssList(app(sk1,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f761,plain,
! [X0] :
( ~ sQ39_spl
| tl(sk2) != X0
| ~ ssList(X0)
| tl(sk2) != X0
| ~ ssList(X0)
| ~ ssList(app(sk1,X0)) ),
inference(component_clause,[status(thm)],[f760]) ).
fof(f763,definition,
( sQ40_spl
<=> sk2 = sk2 ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f766,plain,
( ~ sQ4_spl
| sQ40_spl
| ~ sQ11_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f759,f760,f505,f763,f457]) ).
fof(f767,plain,
! [X0] :
( ~ sQ39_spl
| tl(sk2) != X0
| ~ ssList(X0)
| ~ ssList(app(sk1,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f761]) ).
fof(f775,plain,
( ~ sQ39_spl
| ~ ssList(tl(sk2))
| ~ ssList(app(sk1,tl(sk2))) ),
inference(equality_resolution,[status(thm)],[f767]) ).
fof(f779,definition,
( sQ42_spl
<=> ssList(tl(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f781,plain,
( sQ42_spl
| ~ ssList(tl(sk2)) ),
inference(component_clause,[status(thm)],[f779]) ).
fof(f798,definition,
( sQ47_spl
<=> ssList(app(nil,tl(sk2))) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f800,plain,
( sQ47_spl
| ~ ssList(app(nil,tl(sk2))) ),
inference(component_clause,[status(thm)],[f798]) ).
fof(f813,definition,
( sQ51_spl
<=> ssList(app(sk1,tl(sk2))) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f815,plain,
( sQ51_spl
| ~ ssList(app(sk1,tl(sk2))) ),
inference(component_clause,[status(thm)],[f813]) ).
fof(f816,plain,
( ~ sQ39_spl
| ~ sQ42_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f775,f813,f779,f760]) ).
fof(f817,plain,
( sQ42_spl
| nil = sk2
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f781,f273]) ).
fof(f818,plain,
( sQ42_spl
| sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f817,f505,f508,f779]) ).
fof(f824,definition,
( sQ52_spl
<=> duplicatefreeP(nil) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f826,plain,
( sQ52_spl
| ~ duplicatefreeP(nil) ),
inference(component_clause,[status(thm)],[f824]) ).
fof(f1167,plain,
! [X0,X1] :
( ~ ssList(app(X0,X1))
| ~ ssList(X0)
| ~ frontsegP(app(X0,X1),X0)
| skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(skaf45(app(X0,X1),X0)) ),
inference(resolution,[status(thm)],[f368,f342]) ).
fof(f1177,plain,
! [X0,X1] :
( ~ ssList(app(X0,X1))
| ~ frontsegP(app(X0,X1),X0)
| skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(skaf45(app(X0,X1),X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1167]) ).
fof(f1178,plain,
! [X0,X1] :
( ~ ssList(app(X0,X1))
| ~ frontsegP(app(X0,X1),X0)
| skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1177,f248]) ).
fof(f1934,plain,
( sQ51_spl
| ~ ssList(sk1)
| ~ ssList(tl(sk2)) ),
inference(resolution,[status(thm)],[f815,f283]) ).
fof(f1935,plain,
( sQ51_spl
| ~ sQ9_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f1934,f779,f496,f813]) ).
fof(f1938,plain,
( sQ47_spl
| ~ ssList(nil)
| ~ ssList(tl(sk2)) ),
inference(resolution,[status(thm)],[f800,f283]) ).
fof(f1939,plain,
( sQ47_spl
| ~ sQ8_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f1938,f779,f493,f798]) ).
fof(f2025,definition,
( sQ190_spl
<=> sk2 = tl(sk2) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f2026,plain,
( ~ sQ190_spl
| sk2 = tl(sk2) ),
inference(component_clause,[status(thm)],[f2025]) ).
fof(f2054,plain,
( ~ sQ190_spl
| nil = sk2
| cons(hd(sk2),sk2) = sk2
| ~ ssList(sk2) ),
inference(paramodulation,[status(thm)],[f2026,f304]) ).
fof(f2061,definition,
( sQ192_spl
<=> cons(hd(sk2),sk2) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f2062,plain,
( ~ sQ192_spl
| cons(hd(sk2),sk2) = sk2 ),
inference(component_clause,[status(thm)],[f2061]) ).
fof(f2064,plain,
( ~ sQ190_spl
| sQ12_spl
| sQ192_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2054,f505,f2061,f508,f2025]) ).
fof(f2084,definition,
( sQ194_spl
<=> ssItem(hd(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f2086,plain,
( sQ194_spl
| ~ ssItem(hd(sk2)) ),
inference(component_clause,[status(thm)],[f2084]) ).
fof(f2093,plain,
( sQ194_spl
| nil = sk2
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f2086,f274]) ).
fof(f2094,plain,
( sQ194_spl
| sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2093,f505,f508,f2084]) ).
fof(f2638,definition,
( sQ256_spl
<=> tl(sk2) = tl(sk2) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f2640,plain,
( sQ256_spl
| tl(sk2) != tl(sk2) ),
inference(component_clause,[status(thm)],[f2638]) ).
fof(f2793,definition,
( sQ268_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition]) ).
fof(f2795,plain,
( sQ268_spl
| ~ ssList(sk3) ),
inference(component_clause,[status(thm)],[f2793]) ).
fof(f2911,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ sQ10_spl
| app(nil,X1) != X0
| tl(sk2) != X1
| ~ ssList(X1)
| sk2 = X0
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f500,f544]) ).
fof(f3032,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ10_spl
| ~ ssList(X0)
| tl(sk2) != X0
| ~ ssList(X0)
| sk2 = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f2911,f272]) ).
fof(f3052,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ10_spl
| tl(sk2) != X0
| sk2 = X0
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3032]) ).
fof(f3103,definition,
( sQ304_spl
<=> frontsegP(nil,sk2) ),
introduced(definition,[new_symbols(definition,[sQ304_spl])],[split_symbol_definition]) ).
fof(f3105,plain,
( sQ304_spl
| ~ frontsegP(nil,sk2) ),
inference(component_clause,[status(thm)],[f3103]) ).
fof(f4537,plain,
( ~ sQ4_spl
| ~ sQ10_spl
| ~ ssList(tl(sk2))
| sk2 = app(nil,tl(sk2))
| ~ ssList(app(nil,tl(sk2))) ),
inference(resolution,[status(thm)],[f3052,f272]) ).
fof(f4573,definition,
( sQ442_spl
<=> sk2 = app(nil,tl(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ442_spl])],[split_symbol_definition]) ).
fof(f4574,plain,
( ~ sQ442_spl
| sk2 = app(nil,tl(sk2)) ),
inference(component_clause,[status(thm)],[f4573]) ).
fof(f4576,plain,
( ~ sQ4_spl
| ~ sQ10_spl
| ~ sQ42_spl
| sQ442_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f4537,f798,f4573,f779,f499,f457]) ).
fof(f4590,plain,
! [X0] :
( ~ sQ4_spl
| nil = app(sk1,X0)
| ~ ssList(app(sk1,X0))
| tl(sk2) != X0
| ~ ssList(X0)
| sk2 = cons(skaf83(app(sk1,X0)),skaf82(app(sk1,X0)))
| ~ ssList(cons(skaf83(app(sk1,X0)),skaf82(app(sk1,X0)))) ),
inference(resolution,[status(thm)],[f544,f309]) ).
fof(f4656,plain,
! [X0,X1] :
( ~ frontsegP(app(X0,X1),X0)
| skaf45(app(X0,X1),X0) = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1178,f283]) ).
fof(f5290,plain,
( ~ sQ38_spl
| ~ frontsegP(app(sk1,tl(sk2)),sk1)
| ~ ssList(tl(sk2))
| ~ ssList(sk1)
| ~ frontsegP(app(sk1,tl(sk2)),sk1)
| sk2 = app(sk1,tl(sk2))
| ~ ssList(app(sk1,tl(sk2))) ),
inference(resolution,[status(thm)],[f758,f4656]) ).
fof(f5291,definition,
( sQ495_spl
<=> sk2 = app(sk1,tl(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ495_spl])],[split_symbol_definition]) ).
fof(f5292,plain,
( ~ sQ495_spl
| sk2 = app(sk1,tl(sk2)) ),
inference(component_clause,[status(thm)],[f5291]) ).
fof(f5294,definition,
( sQ496_spl
<=> frontsegP(app(sk1,tl(sk2)),sk1) ),
introduced(definition,[new_symbols(definition,[sQ496_spl])],[split_symbol_definition]) ).
fof(f5296,plain,
( sQ496_spl
| ~ frontsegP(app(sk1,tl(sk2)),sk1) ),
inference(component_clause,[status(thm)],[f5294]) ).
fof(f5297,plain,
( ~ sQ38_spl
| ~ sQ42_spl
| ~ sQ9_spl
| ~ sQ496_spl
| sQ495_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f5290,f813,f5291,f5294,f496,f779,f752]) ).
fof(f5313,plain,
! [X0] :
( ~ sQ495_spl
| frontsegP(sk2,X0)
| ~ ssList(sk1)
| ~ ssList(X0)
| ~ ssList(tl(sk2))
| ~ frontsegP(sk1,X0) ),
inference(paramodulation,[status(thm)],[f5292,f349]) ).
fof(f5339,definition,
( sQ499_spl
<=> nil = app(sk1,tl(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ499_spl])],[split_symbol_definition]) ).
fof(f5340,plain,
( ~ sQ499_spl
| nil = app(sk1,tl(sk2)) ),
inference(component_clause,[status(thm)],[f5339]) ).
fof(f5354,definition,
( sQ503_spl
<=> sk2 = app(nil,sk2) ),
introduced(definition,[new_symbols(definition,[sQ503_spl])],[split_symbol_definition]) ).
fof(f5355,plain,
( ~ sQ503_spl
| sk2 = app(nil,sk2) ),
inference(component_clause,[status(thm)],[f5354]) ).
fof(f5356,plain,
( sQ503_spl
| sk2 != app(nil,sk2) ),
inference(component_clause,[status(thm)],[f5354]) ).
fof(f5379,definition,
! [X0] :
( sQ509_spl
<=> ( frontsegP(sk2,X0)
| ~ ssList(X0)
| ~ frontsegP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ509_spl])],[split_symbol_definition]) ).
fof(f5380,plain,
! [X0] :
( ~ sQ509_spl
| frontsegP(sk2,X0)
| ~ ssList(X0)
| ~ frontsegP(sk1,X0) ),
inference(component_clause,[status(thm)],[f5379]) ).
fof(f5382,plain,
( ~ sQ495_spl
| ~ sQ9_spl
| ~ sQ42_spl
| sQ509_spl ),
inference(split_clause,[status(thm)],[f5313,f5379,f779,f496,f5291]) ).
fof(f5885,plain,
( sQ503_spl
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f5356,f272]) ).
fof(f5886,plain,
( sQ503_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f5885,f505,f5354]) ).
fof(f6508,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[f358]) ).
fof(f6544,definition,
( sQ612_spl
<=> frontsegP(sk2,nil) ),
introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition]) ).
fof(f6545,plain,
( ~ sQ612_spl
| frontsegP(sk2,nil) ),
inference(component_clause,[status(thm)],[f6544]) ).
fof(f6572,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6508,f283]) ).
fof(f9519,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ0_spl
| ~ ssList(X4)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X3)
| app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4 ),
inference(forward_subsumption_resolution,[status(thm)],[f415,f443]) ).
fof(f10220,plain,
! [X0,X1,X2] :
( ~ sQ192_spl
| ~ sQ0_spl
| ~ ssList(X2)
| ~ ssItem(hd(sk2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(sk2)
| app(app(X0,cons(hd(sk2),X1)),sk2) != X2 ),
inference(paramodulation,[status(thm)],[f2062,f9519]) ).
fof(f10276,definition,
! [X0,X1,X2] :
( sQ831_spl
<=> ( ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(app(X0,cons(hd(sk2),X1)),sk2) != X2 ) ),
introduced(definition,[new_symbols(definition,[sQ831_spl])],[split_symbol_definition]) ).
fof(f10277,plain,
! [X0,X1,X2] :
( ~ sQ831_spl
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(app(X0,cons(hd(sk2),X1)),sk2) != X2 ),
inference(component_clause,[status(thm)],[f10276]) ).
fof(f10279,plain,
( ~ sQ192_spl
| ~ sQ0_spl
| ~ sQ194_spl
| ~ sQ11_spl
| sQ831_spl ),
inference(split_clause,[status(thm)],[f10220,f10276,f505,f2084,f442,f2061]) ).
fof(f10312,plain,
! [X0,X1] :
( ~ sQ192_spl
| ~ sQ831_spl
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(sk2)
| app(app(X0,sk2),sk2) != X1 ),
inference(paramodulation,[status(thm)],[f2062,f10277]) ).
fof(f10320,definition,
! [X0,X1] :
( sQ837_spl
<=> ( ~ ssList(X1)
| ~ ssList(X0)
| app(app(X0,sk2),sk2) != X1 ) ),
introduced(definition,[new_symbols(definition,[sQ837_spl])],[split_symbol_definition]) ).
fof(f10321,plain,
! [X0,X1] :
( ~ sQ837_spl
| ~ ssList(X1)
| ~ ssList(X0)
| app(app(X0,sk2),sk2) != X1 ),
inference(component_clause,[status(thm)],[f10320]) ).
fof(f10323,plain,
( ~ sQ192_spl
| ~ sQ831_spl
| ~ sQ11_spl
| sQ837_spl ),
inference(split_clause,[status(thm)],[f10312,f10320,f505,f10276,f2061]) ).
fof(f10336,plain,
! [X0] :
( ~ sQ837_spl
| ~ ssList(app(app(X0,sk2),sk2))
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[f10321]) ).
fof(f10500,plain,
! [X0] :
( ~ sQ837_spl
| ~ ssList(X0)
| ~ ssList(app(X0,sk2))
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f283,f10336]) ).
fof(f10507,definition,
! [X0] :
( sQ853_spl
<=> ( ~ ssList(X0)
| ~ ssList(app(X0,sk2)) ) ),
introduced(definition,[new_symbols(definition,[sQ853_spl])],[split_symbol_definition]) ).
fof(f10508,plain,
! [X0] :
( ~ sQ853_spl
| ~ ssList(X0)
| ~ ssList(app(X0,sk2)) ),
inference(component_clause,[status(thm)],[f10507]) ).
fof(f10510,plain,
( ~ sQ837_spl
| sQ853_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f10500,f505,f10507,f10320]) ).
fof(f10529,plain,
( ~ sQ503_spl
| ~ sQ853_spl
| ~ ssList(nil)
| ~ ssList(sk2) ),
inference(paramodulation,[status(thm)],[f5355,f10508]) ).
fof(f10532,plain,
( ~ sQ503_spl
| ~ sQ853_spl
| ~ sQ8_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f10529,f505,f493,f10507,f5354]) ).
fof(f10636,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ ssList(X1)
| cons(X0,X1) != X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f299,f446]) ).
fof(f10638,plain,
( ~ sQ192_spl
| ~ sQ1_spl
| ~ ssList(sk2)
| sk2 != sk2 ),
inference(paramodulation,[status(thm)],[f2062,f10636]) ).
fof(f10640,plain,
( ~ sQ192_spl
| ~ sQ1_spl
| ~ sQ11_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f10638,f763,f505,f445,f2061]) ).
fof(f10685,plain,
( sQ496_spl
| ~ ssList(sk1)
| ~ ssList(tl(sk2)) ),
inference(resolution,[status(thm)],[f5296,f6572]) ).
fof(f10686,plain,
( sQ496_spl
| ~ sQ9_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f10685,f779,f496,f5294]) ).
fof(f10688,plain,
( sQ256_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2640]) ).
fof(f10689,plain,
sQ256_spl,
inference(contradiction_clause,[status(thm)],[f10688]) ).
fof(f11627,plain,
( ~ sQ442_spl
| sk2 = tl(sk2)
| ~ ssList(tl(sk2)) ),
inference(paramodulation,[status(thm)],[f4574,f272]) ).
fof(f11644,plain,
( ~ sQ442_spl
| sQ190_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f11627,f779,f2025,f4573]) ).
fof(f14186,plain,
( ~ sQ612_spl
| sk2 = nil
| ~ ssList(sk2)
| ~ ssList(nil)
| ~ frontsegP(nil,sk2) ),
inference(resolution,[status(thm)],[f339,f6545]) ).
fof(f14199,plain,
( ~ sQ612_spl
| sQ12_spl
| ~ sQ11_spl
| ~ sQ8_spl
| ~ sQ304_spl ),
inference(split_clause,[status(thm)],[f14186,f3103,f493,f505,f508,f6544]) ).
fof(f15655,plain,
( ~ sQ495_spl
| ~ sQ4_spl
| nil = app(sk1,tl(sk2))
| ~ ssList(app(sk1,tl(sk2)))
| tl(sk2) != tl(sk2)
| ~ ssList(tl(sk2))
| sk2 = cons(skaf83(app(sk1,tl(sk2))),skaf82(sk2))
| ~ ssList(cons(skaf83(app(sk1,tl(sk2))),skaf82(app(sk1,tl(sk2))))) ),
inference(paramodulation,[status(thm)],[f5292,f4590]) ).
fof(f15658,definition,
( sQ1224_spl
<=> ssList(cons(skaf83(app(sk1,tl(sk2))),skaf82(app(sk1,tl(sk2))))) ),
introduced(definition,[new_symbols(definition,[sQ1224_spl])],[split_symbol_definition]) ).
fof(f15660,plain,
( sQ1224_spl
| ~ ssList(cons(skaf83(app(sk1,tl(sk2))),skaf82(app(sk1,tl(sk2))))) ),
inference(component_clause,[status(thm)],[f15658]) ).
fof(f15665,definition,
( sQ1226_spl
<=> sk2 = cons(skaf83(app(sk1,tl(sk2))),skaf82(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ1226_spl])],[split_symbol_definition]) ).
fof(f15666,plain,
( ~ sQ1226_spl
| sk2 = cons(skaf83(app(sk1,tl(sk2))),skaf82(sk2)) ),
inference(component_clause,[status(thm)],[f15665]) ).
fof(f15668,plain,
( ~ sQ495_spl
| ~ sQ4_spl
| sQ499_spl
| ~ sQ51_spl
| ~ sQ256_spl
| ~ sQ42_spl
| sQ1226_spl
| ~ sQ1224_spl ),
inference(split_clause,[status(thm)],[f15655,f15658,f15665,f779,f2638,f813,f5339,f457,f5291]) ).
fof(f15669,plain,
( sQ1224_spl
| ~ sQ495_spl
| ~ ssList(cons(skaf83(sk2),skaf82(app(sk1,tl(sk2))))) ),
inference(forward_demodulation,[status(thm)],[f5292,f15660]) ).
fof(f15670,plain,
( sQ1224_spl
| ~ sQ495_spl
| ~ ssList(cons(skaf83(sk2),skaf82(sk2))) ),
inference(forward_demodulation,[status(thm)],[f5292,f15669]) ).
fof(f16231,plain,
( ~ sQ499_spl
| frontsegP(nil,app(sk1,tl(sk2)))
| ~ ssList(app(sk1,tl(sk2))) ),
inference(resolution,[status(thm)],[f5340,f281]) ).
fof(f16283,definition,
( sQ1283_spl
<=> frontsegP(nil,app(sk1,tl(sk2))) ),
introduced(definition,[new_symbols(definition,[sQ1283_spl])],[split_symbol_definition]) ).
fof(f16284,plain,
( ~ sQ1283_spl
| frontsegP(nil,app(sk1,tl(sk2))) ),
inference(component_clause,[status(thm)],[f16283]) ).
fof(f16286,plain,
( ~ sQ499_spl
| sQ1283_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f16231,f813,f16283,f5339]) ).
fof(f17800,plain,
( ~ sQ1226_spl
| ~ sQ495_spl
| sk2 = cons(skaf83(sk2),skaf82(sk2)) ),
inference(forward_demodulation,[status(thm)],[f5292,f15666]) ).
fof(f18045,definition,
( sQ1460_spl
<=> ssList(skaf82(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ1460_spl])],[split_symbol_definition]) ).
fof(f18047,plain,
( sQ1460_spl
| ~ ssList(skaf82(sk2)) ),
inference(component_clause,[status(thm)],[f18045]) ).
fof(f18052,definition,
( sQ1462_spl
<=> ssItem(skaf83(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ1462_spl])],[split_symbol_definition]) ).
fof(f18054,plain,
( sQ1462_spl
| ~ ssItem(skaf83(sk2)) ),
inference(component_clause,[status(thm)],[f18052]) ).
fof(f18090,definition,
( sQ1471_spl
<=> tl(sk2) = skaf82(sk2) ),
introduced(definition,[new_symbols(definition,[sQ1471_spl])],[split_symbol_definition]) ).
fof(f18091,plain,
( ~ sQ1471_spl
| tl(sk2) = skaf82(sk2) ),
inference(component_clause,[status(thm)],[f18090]) ).
fof(f18110,plain,
( sQ1460_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18047,f210]) ).
fof(f18111,plain,
sQ1460_spl,
inference(contradiction_clause,[status(thm)],[f18110]) ).
fof(f18141,plain,
( ~ sQ495_spl
| ~ sQ1471_spl
| sk2 = app(sk1,skaf82(sk2)) ),
inference(backward_demodulation,[status(thm)],[f18091,f5292]) ).
fof(f18518,definition,
( sQ1502_spl
<=> skaf82(sk2) = skaf82(sk2) ),
introduced(definition,[new_symbols(definition,[sQ1502_spl])],[split_symbol_definition]) ).
fof(f18520,plain,
( sQ1502_spl
| skaf82(sk2) != skaf82(sk2) ),
inference(component_clause,[status(thm)],[f18518]) ).
fof(f19717,plain,
( ~ sQ509_spl
| ~ ssList(sk1)
| frontsegP(sk2,nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f5380,f257]) ).
fof(f19719,plain,
( ~ sQ509_spl
| ~ sQ9_spl
| sQ612_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f19717,f493,f6544,f496,f5379]) ).
fof(f21774,plain,
( sQ1224_spl
| ~ sQ495_spl
| ~ ssList(skaf82(sk2))
| ~ ssItem(skaf83(sk2)) ),
inference(resolution,[status(thm)],[f15670,f284]) ).
fof(f21775,plain,
( sQ1224_spl
| ~ sQ495_spl
| ~ sQ1460_spl
| ~ sQ1462_spl ),
inference(split_clause,[status(thm)],[f21774,f18052,f18045,f5291,f15658]) ).
fof(f21776,plain,
( sQ1462_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18054,f209]) ).
fof(f21777,plain,
sQ1462_spl,
inference(contradiction_clause,[status(thm)],[f21776]) ).
fof(f21867,plain,
( ~ sQ1283_spl
| ~ sQ495_spl
| frontsegP(nil,sk2) ),
inference(forward_demodulation,[status(thm)],[f5292,f16284]) ).
fof(f21868,plain,
( ~ sQ1283_spl
| ~ sQ495_spl
| sQ304_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21867,f3105]) ).
fof(f21869,plain,
( ~ sQ1283_spl
| ~ sQ495_spl
| sQ304_spl ),
inference(contradiction_clause,[status(thm)],[f21868]) ).
fof(f22308,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f826,f199]) ).
fof(f22309,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f22308]) ).
fof(f23518,plain,
( sQ1502_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f18520]) ).
fof(f23519,plain,
sQ1502_spl,
inference(contradiction_clause,[status(thm)],[f23518]) ).
fof(f24872,plain,
( sQ268_spl
| ~ ssList(sk1) ),
inference(forward_demodulation,[status(thm)],[f433,f2795]) ).
fof(f24873,plain,
( sQ268_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24872,f428]) ).
fof(f24874,plain,
sQ268_spl,
inference(contradiction_clause,[status(thm)],[f24873]) ).
fof(f24893,plain,
( ~ sQ1226_spl
| ~ sQ495_spl
| tl(sk2) = skaf82(sk2)
| ~ ssList(skaf82(sk2))
| ~ ssItem(skaf83(sk2)) ),
inference(paramodulation,[status(thm)],[f17800,f294]) ).
fof(f24900,plain,
( ~ sQ1226_spl
| ~ sQ495_spl
| sQ1471_spl
| ~ sQ1460_spl
| ~ sQ1462_spl ),
inference(split_clause,[status(thm)],[f24893,f18052,f18045,f18090,f5291,f15665]) ).
fof(f27818,definition,
( sQ2067_spl
<=> ssList(skaf45(sk2,skaf82(sk2))) ),
introduced(definition,[new_symbols(definition,[sQ2067_spl])],[split_symbol_definition]) ).
fof(f27820,plain,
( sQ2067_spl
| ~ ssList(skaf45(sk2,skaf82(sk2))) ),
inference(component_clause,[status(thm)],[f27818]) ).
fof(f27830,plain,
( sQ2067_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27820,f248]) ).
fof(f27831,plain,
sQ2067_spl,
inference(contradiction_clause,[status(thm)],[f27830]) ).
fof(f27922,definition,
( sQ2073_spl
<=> ssList(skaf82(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ2073_spl])],[split_symbol_definition]) ).
fof(f27924,plain,
( sQ2073_spl
| ~ ssList(skaf82(sk1)) ),
inference(component_clause,[status(thm)],[f27922]) ).
fof(f27960,plain,
( sQ2073_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27924,f210]) ).
fof(f27961,plain,
sQ2073_spl,
inference(contradiction_clause,[status(thm)],[f27960]) ).
fof(f28482,definition,
( sQ2113_spl
<=> ssList(skaf45(sk2,skaf45(nil,sk1))) ),
introduced(definition,[new_symbols(definition,[sQ2113_spl])],[split_symbol_definition]) ).
fof(f28484,plain,
( sQ2113_spl
| ~ ssList(skaf45(sk2,skaf45(nil,sk1))) ),
inference(component_clause,[status(thm)],[f28482]) ).
fof(f28495,plain,
( sQ2113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28484,f248]) ).
fof(f28496,plain,
sQ2113_spl,
inference(contradiction_clause,[status(thm)],[f28495]) ).
fof(f28751,definition,
( sQ2146_spl
<=> ssList(skaf45(sk1,skaf45(nil,sk1))) ),
introduced(definition,[new_symbols(definition,[sQ2146_spl])],[split_symbol_definition]) ).
fof(f28753,plain,
( sQ2146_spl
| ~ ssList(skaf45(sk1,skaf45(nil,sk1))) ),
inference(component_clause,[status(thm)],[f28751]) ).
fof(f28764,plain,
( sQ2146_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28753,f248]) ).
fof(f28765,plain,
sQ2146_spl,
inference(contradiction_clause,[status(thm)],[f28764]) ).
fof(f29581,definition,
( sQ2253_spl
<=> ssList(skaf45(nil,skaf45(sk2,skaf45(nil,sk1)))) ),
introduced(definition,[new_symbols(definition,[sQ2253_spl])],[split_symbol_definition]) ).
fof(f29583,plain,
( sQ2253_spl
| ~ ssList(skaf45(nil,skaf45(sk2,skaf45(nil,sk1)))) ),
inference(component_clause,[status(thm)],[f29581]) ).
fof(f29594,plain,
( sQ2253_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29583,f248]) ).
fof(f29595,plain,
sQ2253_spl,
inference(contradiction_clause,[status(thm)],[f29594]) ).
fof(f29622,definition,
( sQ2259_spl
<=> ssList(skaf45(nil,skaf45(sk1,skaf45(nil,sk1)))) ),
introduced(definition,[new_symbols(definition,[sQ2259_spl])],[split_symbol_definition]) ).
fof(f29624,plain,
( sQ2259_spl
| ~ ssList(skaf45(nil,skaf45(sk1,skaf45(nil,sk1)))) ),
inference(component_clause,[status(thm)],[f29622]) ).
fof(f29635,plain,
( sQ2259_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29624,f248]) ).
fof(f29636,plain,
sQ2259_spl,
inference(contradiction_clause,[status(thm)],[f29635]) ).
fof(f29689,definition,
( sQ2268_spl
<=> ssList(skaf46(sk1,nil)) ),
introduced(definition,[new_symbols(definition,[sQ2268_spl])],[split_symbol_definition]) ).
fof(f29691,plain,
( sQ2268_spl
| ~ ssList(skaf46(sk1,nil)) ),
inference(component_clause,[status(thm)],[f29689]) ).
fof(f29696,plain,
( sQ2268_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29691,f247]) ).
fof(f29697,plain,
sQ2268_spl,
inference(contradiction_clause,[status(thm)],[f29696]) ).
fof(f29748,definition,
( sQ2271_spl
<=> ssList(skaf46(sk1,sk2)) ),
introduced(definition,[new_symbols(definition,[sQ2271_spl])],[split_symbol_definition]) ).
fof(f29750,plain,
( sQ2271_spl
| ~ ssList(skaf46(sk1,sk2)) ),
inference(component_clause,[status(thm)],[f29748]) ).
fof(f29753,plain,
( sQ2271_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29750,f247]) ).
fof(f29754,plain,
sQ2271_spl,
inference(contradiction_clause,[status(thm)],[f29753]) ).
fof(f30217,definition,
( sQ2335_spl
<=> ssList(skaf45(sk2,skaf45(sk2,skaf45(nil,sk1)))) ),
introduced(definition,[new_symbols(definition,[sQ2335_spl])],[split_symbol_definition]) ).
fof(f30219,plain,
( sQ2335_spl
| ~ ssList(skaf45(sk2,skaf45(sk2,skaf45(nil,sk1)))) ),
inference(component_clause,[status(thm)],[f30217]) ).
fof(f30230,plain,
( sQ2335_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30219,f248]) ).
fof(f30231,plain,
sQ2335_spl,
inference(contradiction_clause,[status(thm)],[f30230]) ).
fof(f30437,definition,
( sQ2362_spl
<=> ssList(skaf45(sk2,skaf45(sk1,skaf45(nil,sk1)))) ),
introduced(definition,[new_symbols(definition,[sQ2362_spl])],[split_symbol_definition]) ).
fof(f30439,plain,
( sQ2362_spl
| ~ ssList(skaf45(sk2,skaf45(sk1,skaf45(nil,sk1)))) ),
inference(component_clause,[status(thm)],[f30437]) ).
fof(f30450,plain,
( sQ2362_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30439,f248]) ).
fof(f30451,plain,
sQ2362_spl,
inference(contradiction_clause,[status(thm)],[f30450]) ).
fof(f30960,definition,
( sQ2430_spl
<=> ssList(skaf45(sk1,nil)) ),
introduced(definition,[new_symbols(definition,[sQ2430_spl])],[split_symbol_definition]) ).
fof(f30962,plain,
( sQ2430_spl
| ~ ssList(skaf45(sk1,nil)) ),
inference(component_clause,[status(thm)],[f30960]) ).
fof(f30982,plain,
( sQ2430_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30962,f248]) ).
fof(f30983,plain,
sQ2430_spl,
inference(contradiction_clause,[status(thm)],[f30982]) ).
fof(f31343,definition,
! [X0,X1] :
( sQ2483_spl
<=> ( segmentP(X1,sk1)
| ~ ssList(X1)
| ~ ssList(X0)
| app(sk1,X0) != X1 ) ),
introduced(definition,[new_symbols(definition,[sQ2483_spl])],[split_symbol_definition]) ).
fof(f31344,plain,
! [X0,X1] :
( ~ sQ2483_spl
| segmentP(X1,sk1)
| ~ ssList(X1)
| ~ ssList(X0)
| app(sk1,X0) != X1 ),
inference(component_clause,[status(thm)],[f31343]) ).
fof(f31374,definition,
( sQ2487_spl
<=> ssList(skaf45(sk1,skaf45(sk1,skaf45(nil,sk1)))) ),
introduced(definition,[new_symbols(definition,[sQ2487_spl])],[split_symbol_definition]) ).
fof(f31376,plain,
( sQ2487_spl
| ~ ssList(skaf45(sk1,skaf45(sk1,skaf45(nil,sk1)))) ),
inference(component_clause,[status(thm)],[f31374]) ).
fof(f31387,plain,
( sQ2487_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31376,f248]) ).
fof(f31388,plain,
sQ2487_spl,
inference(contradiction_clause,[status(thm)],[f31387]) ).
fof(f31403,plain,
( ~ sQ495_spl
| ~ sQ1471_spl
| ~ sQ2483_spl
| segmentP(sk2,sk1)
| ~ ssList(sk2)
| ~ ssList(skaf82(sk2)) ),
inference(resolution,[status(thm)],[f31344,f18141]) ).
fof(f31427,plain,
( ~ sQ495_spl
| ~ sQ1471_spl
| ~ sQ2483_spl
| sQ7_spl
| ~ sQ11_spl
| ~ sQ1460_spl ),
inference(split_clause,[status(thm)],[f31403,f18045,f505,f467,f31343,f18090,f5291]) ).
fof(f31443,definition,
( sQ2493_spl
<=> ssList(skaf46(sk1,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ2493_spl])],[split_symbol_definition]) ).
fof(f31445,plain,
( sQ2493_spl
| ~ ssList(skaf46(sk1,sk1)) ),
inference(component_clause,[status(thm)],[f31443]) ).
fof(f31447,plain,
( sQ2493_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31445,f247]) ).
fof(f31448,plain,
sQ2493_spl,
inference(contradiction_clause,[status(thm)],[f31447]) ).
fof(f31942,definition,
( sQ2555_spl
<=> ssList(skaf45(sk1,skaf45(sk2,skaf45(nil,sk1)))) ),
introduced(definition,[new_symbols(definition,[sQ2555_spl])],[split_symbol_definition]) ).
fof(f31944,plain,
( sQ2555_spl
| ~ ssList(skaf45(sk1,skaf45(sk2,skaf45(nil,sk1)))) ),
inference(component_clause,[status(thm)],[f31942]) ).
fof(f31962,plain,
( sQ2555_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31944,f248]) ).
fof(f31963,plain,
sQ2555_spl,
inference(contradiction_clause,[status(thm)],[f31962]) ).
fof(f35850,definition,
( sQ3051_spl
<=> ssList(skaf45(nil,skaf45(nil,skaf45(sk2,skaf45(nil,sk1))))) ),
introduced(definition,[new_symbols(definition,[sQ3051_spl])],[split_symbol_definition]) ).
fof(f35852,plain,
( sQ3051_spl
| ~ ssList(skaf45(nil,skaf45(nil,skaf45(sk2,skaf45(nil,sk1))))) ),
inference(component_clause,[status(thm)],[f35850]) ).
fof(f35867,plain,
( sQ3051_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35852,f248]) ).
fof(f35868,plain,
sQ3051_spl,
inference(contradiction_clause,[status(thm)],[f35867]) ).
fof(f35892,definition,
( sQ3057_spl
<=> ssList(skaf45(nil,skaf45(nil,skaf45(sk1,skaf45(nil,sk1))))) ),
introduced(definition,[new_symbols(definition,[sQ3057_spl])],[split_symbol_definition]) ).
fof(f35894,plain,
( sQ3057_spl
| ~ ssList(skaf45(nil,skaf45(nil,skaf45(sk1,skaf45(nil,sk1))))) ),
inference(component_clause,[status(thm)],[f35892]) ).
fof(f35909,plain,
( sQ3057_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35894,f248]) ).
fof(f35910,plain,
sQ3057_spl,
inference(contradiction_clause,[status(thm)],[f35909]) ).
fof(f35935,definition,
( sQ3063_spl
<=> ssList(skaf45(nil,skaf45(sk2,skaf45(sk2,skaf45(nil,sk1))))) ),
introduced(definition,[new_symbols(definition,[sQ3063_spl])],[split_symbol_definition]) ).
fof(f35937,plain,
( sQ3063_spl
| ~ ssList(skaf45(nil,skaf45(sk2,skaf45(sk2,skaf45(nil,sk1))))) ),
inference(component_clause,[status(thm)],[f35935]) ).
fof(f35952,plain,
( sQ3063_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35937,f248]) ).
fof(f35953,plain,
sQ3063_spl,
inference(contradiction_clause,[status(thm)],[f35952]) ).
fof(f35977,definition,
( sQ3069_spl
<=> ssList(skaf45(nil,skaf45(sk2,skaf45(sk1,skaf45(nil,sk1))))) ),
introduced(definition,[new_symbols(definition,[sQ3069_spl])],[split_symbol_definition]) ).
fof(f35979,plain,
( sQ3069_spl
| ~ ssList(skaf45(nil,skaf45(sk2,skaf45(sk1,skaf45(nil,sk1))))) ),
inference(component_clause,[status(thm)],[f35977]) ).
fof(f35994,plain,
( sQ3069_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35979,f248]) ).
fof(f35995,plain,
sQ3069_spl,
inference(contradiction_clause,[status(thm)],[f35994]) ).
fof(f36019,definition,
( sQ3075_spl
<=> ssList(skaf45(nil,skaf45(sk1,skaf45(sk2,skaf45(nil,sk1))))) ),
introduced(definition,[new_symbols(definition,[sQ3075_spl])],[split_symbol_definition]) ).
fof(f36021,plain,
( sQ3075_spl
| ~ ssList(skaf45(nil,skaf45(sk1,skaf45(sk2,skaf45(nil,sk1))))) ),
inference(component_clause,[status(thm)],[f36019]) ).
fof(f36036,plain,
( sQ3075_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f36021,f248]) ).
fof(f36037,plain,
sQ3075_spl,
inference(contradiction_clause,[status(thm)],[f36036]) ).
fof(f36061,definition,
( sQ3081_spl
<=> ssList(skaf45(nil,skaf45(sk1,skaf45(sk1,skaf45(nil,sk1))))) ),
introduced(definition,[new_symbols(definition,[sQ3081_spl])],[split_symbol_definition]) ).
fof(f36063,plain,
( sQ3081_spl
| ~ ssList(skaf45(nil,skaf45(sk1,skaf45(sk1,skaf45(nil,sk1))))) ),
inference(component_clause,[status(thm)],[f36061]) ).
fof(f36078,plain,
( sQ3081_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f36063,f248]) ).
fof(f36079,plain,
sQ3081_spl,
inference(contradiction_clause,[status(thm)],[f36078]) ).
fof(f37072,definition,
( sQ3182_spl
<=> app(nil,sk1) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ3182_spl])],[split_symbol_definition]) ).
fof(f37073,plain,
( ~ sQ3182_spl
| app(nil,sk1) = sk1 ),
inference(component_clause,[status(thm)],[f37072]) ).
fof(f37074,plain,
( sQ3182_spl
| app(nil,sk1) != sk1 ),
inference(component_clause,[status(thm)],[f37072]) ).
fof(f37080,plain,
( sQ3182_spl
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f37074,f272]) ).
fof(f37081,plain,
( sQ3182_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f37080,f496,f37072]) ).
fof(f37148,plain,
! [X0,X1] :
( ~ sQ3182_spl
| segmentP(X1,sk1)
| ~ ssList(X1)
| ~ ssList(sk1)
| ~ ssList(nil)
| ~ ssList(X0)
| app(sk1,X0) != X1 ),
inference(paramodulation,[status(thm)],[f37073,f404]) ).
fof(f37251,plain,
( ~ sQ3182_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ2483_spl ),
inference(split_clause,[status(thm)],[f37148,f31343,f493,f496,f37072]) ).
fof(f37263,plain,
$false,
inference(sat_refutation,[status(thm)],[f448,f452,f471,f472,f486,f502,f511,f513,f515,f542,f558,f755,f766,f816,f818,f1935,f1939,f2064,f2094,f4576,f5297,f5382,f5886,f10279,f10323,f10510,f10532,f10640,f10686,f10689,f11644,f14199,f15668,f16286,f18111,f19719,f21775,f21777,f21869,f22309,f23519,f24874,f24900,f27831,f27961,f28496,f28765,f29595,f29636,f29697,f29754,f30231,f30451,f30983,f31388,f31427,f31448,f31963,f35868,f35910,f35953,f35995,f36037,f36079,f37081,f37251]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWC120-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/5.31 % Computer : n012.cluster.edu
% 0.03/5.31 % Model : x86_64 x86_64
% 0.03/5.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/5.31 % Memory : 8046.5625MB
% 0.03/5.31 % OS : Linux 6.8.0-71-generic
% 0.03/5.31 % CPULimit : 300
% 0.03/5.31 % WCLimit : 300
% 0.03/5.31 % DateTime : Mon Sep 21 07:56:57 UTC 2026
% 0.03/5.31 % CPUTime :
% 0.03/5.32 % Drodi V4.1.1
% 284.52/41.18 % Refutation found
% 284.52/41.18 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 284.52/41.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 13.80/41.31 % Elapsed time: 35.975202 seconds
% 13.80/41.31 % CPU time: 285.433126 seconds
% 13.80/41.31 % Total memory used: 919.348 MB
% 13.80/41.31 % Net memory used: 846.075 MB
%------------------------------------------------------------------------------