%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC382-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 : n015.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:01 PM UTC 2026
% Result : Unsatisfiable 204.64s 36.26s
% Output : CNFRefutation 62.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 82
% Syntax : Number of formulae : 327 ( 85 unt; 49 def)
% Number of atoms : 723 ( 146 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 769 ( 373 ~; 347 |; 0 &)
% ( 49 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 57 ( 55 usr; 50 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-2 aty)
% Number of variables : 135 ( 135 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
totalorderedP(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
ssItem(skac3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
ssItem(skac2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [U] : ssItem(skaf83(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [U] : ssList(skaf82(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [U] : ssItem(skaf70(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [U] : ssItem(skaf69(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [U] : ssItem(skaf65(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [U] : ssItem(skaf64(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [U,V] : ssList(skaf48(U,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(f96,axiom,
! [U,V] :
( tl(cons(U,V)) = V
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [U,V] :
( hd(cons(U,V)) = U
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != V ),
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(f109,axiom,
! [U] :
( nil = U
| cons(skaf83(U),skaf82(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f115,axiom,
! [U,V] :
( ~ ssList(U)
| ~ ssList(V)
| ~ neq(U,V)
| U != V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f116,axiom,
! [U,V] :
( singletonP(V)
| ~ ssList(V)
| ~ ssItem(U)
| cons(U,nil) != V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f120,axiom,
! [U,V] :
( app(cons(U,nil),V) = cons(U,V)
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [U,V,W,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ~ ssList(U)
| ~ ssList(W)
| app(app(U,V),W) != X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,negated_conjecture,
ssList(sk1),
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,
( neq(sk2,nil)
| neq(sk2,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
! [A,B] :
( ~ neq(sk4,nil)
| ~ neq(nil,sk4)
| hd(sk4) != B
| cons(B,nil) != A
| ~ ssItem(B)
| sk3 = A
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
( ~ neq(sk4,nil)
| ~ segmentP(sk2,sk1)
| ~ singletonP(sk1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f201,plain,
totalorderedP(nil),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f205,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f206,plain,
ssItem(skac3),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f207,plain,
ssItem(skac2),
inference(cnf_transformation,[status(thm)],[f10]) ).
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(f222,plain,
! [X0] : ssItem(skaf70(X0)),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f223,plain,
! [X0] : ssItem(skaf69(X0)),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f227,plain,
! [X0] : ssItem(skaf65(X0)),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f228,plain,
! [X0] : ssItem(skaf64(X0)),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f245,plain,
! [X0,X1] : ssList(skaf48(X0,X1)),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f271,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f272,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f274,plain,
! [X0] :
( nil = X0
| ssItem(hd(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
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(f295,plain,
! [X0,X1] :
( hd(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f296,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f98]) ).
fof(f297,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f296]) ).
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(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(f320,plain,
! [V] :
( singletonP(V)
| ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,nil) != V ) ),
inference(miniscoping,[status(thm)],[f116]) ).
fof(f321,plain,
! [X0,X1] :
( singletonP(X1)
| ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,nil) != X1 ),
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f328,plain,
! [X0,X1] :
( app(cons(X0,nil),X1) = cons(X0,X1)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
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(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)
| ! [B] :
( hd(sk4) != B
| ! [A] :
( cons(B,nil) != A
| ~ ssItem(B)
| sk3 = A
| ~ ssList(A) ) ) ),
inference(miniscoping,[status(thm)],[f196]) ).
fof(f440,plain,
! [X0,X1] :
( ~ neq(sk4,nil)
| ~ neq(nil,sk4)
| hd(sk4) != X1
| cons(X1,nil) != X0
| ~ ssItem(X1)
| sk3 = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f439]) ).
fof(f441,plain,
( ~ neq(sk4,nil)
| ~ segmentP(sk2,sk1)
| ~ singletonP(sk1) ),
inference(cnf_transformation,[status(thm)],[f197]) ).
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
<=> ( hd(sk4) != X1
| cons(X1,nil) != X0
| ~ ssItem(X1)
| sk3 = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f458,plain,
! [X0,X1] :
( ~ sQ4_spl
| hd(sk4) != X1
| cons(X1,nil) != X0
| ~ ssItem(X1)
| sk3 = 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
<=> singletonP(sk1) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
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(f480,plain,
! [X1] :
( ~ ssList(X1)
| ~ ssList(X1)
| ~ neq(X1,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f319]) ).
fof(f481,plain,
! [X0] :
( ~ ssList(X0)
| ~ neq(X0,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f480]) ).
fof(f482,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ~ ssList(cons(X0,nil))
| ~ ssItem(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f321]) ).
fof(f491,plain,
! [X0,X1,X2] :
( segmentP(app(app(X1,X2),X0),X2)
| ~ ssList(app(app(X1,X2),X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f404]) ).
fof(f504,plain,
( sQ3_spl
| ~ neq(sk2,nil) ),
inference(forward_demodulation,[status(thm)],[f432,f455]) ).
fof(f505,plain,
( sQ3_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f504,f450]) ).
fof(f506,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f505]) ).
fof(f507,plain,
! [X0,X1] :
( ~ sQ4_spl
| hd(sk4) != X1
| cons(X1,nil) != X0
| ~ ssItem(X1)
| sk1 = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f433,f458]) ).
fof(f508,plain,
! [X0,X1] :
( ~ sQ4_spl
| hd(sk2) != X1
| cons(X1,nil) != X0
| ~ ssItem(X1)
| sk1 = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f432,f507]) ).
fof(f509,plain,
( ~ sQ4_spl
| ~ ssItem(hd(sk2))
| sk1 = cons(hd(sk2),nil)
| ~ ssList(cons(hd(sk2),nil)) ),
inference(destructive_equality_resolution,[status(thm)],[f508]) ).
fof(f513,definition,
( sQ8_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f515,plain,
( sQ8_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f521,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f515,f205]) ).
fof(f522,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f521]) ).
fof(f523,plain,
( ~ sQ4_spl
| ~ ssItem(hd(sk2))
| sk1 = cons(hd(sk2),nil)
| ~ ssList(nil)
| ~ ssItem(hd(sk2)) ),
inference(resolution,[status(thm)],[f284,f509]) ).
fof(f524,definition,
( sQ10_spl
<=> ssItem(hd(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f525,plain,
( ~ sQ10_spl
| ssItem(hd(sk2)) ),
inference(component_clause,[status(thm)],[f524]) ).
fof(f526,plain,
( sQ10_spl
| ~ ssItem(hd(sk2)) ),
inference(component_clause,[status(thm)],[f524]) ).
fof(f527,definition,
( sQ11_spl
<=> sk1 = cons(hd(sk2),nil) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f528,plain,
( ~ sQ11_spl
| sk1 = cons(hd(sk2),nil) ),
inference(component_clause,[status(thm)],[f527]) ).
fof(f530,plain,
( ~ sQ4_spl
| sQ11_spl
| ~ sQ8_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f523,f524,f513,f527,f457]) ).
fof(f531,plain,
( sQ5_spl
| ~ neq(nil,sk2) ),
inference(forward_demodulation,[status(thm)],[f432,f462]) ).
fof(f533,definition,
( sQ12_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f537,plain,
( sQ10_spl
| nil = sk2
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f526,f274]) ).
fof(f538,definition,
( sQ13_spl
<=> ssList(sk2) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f540,plain,
( sQ13_spl
| ~ ssList(sk2) ),
inference(component_clause,[status(thm)],[f538]) ).
fof(f541,definition,
( sQ14_spl
<=> nil = sk2 ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f542,plain,
( ~ sQ14_spl
| nil = sk2 ),
inference(component_clause,[status(thm)],[f541]) ).
fof(f544,plain,
( sQ10_spl
| sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f537,f538,f541,f524]) ).
fof(f545,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f540,f429]) ).
fof(f546,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f545]) ).
fof(f549,plain,
! [X0,X1] :
( hd(cons(skaf83(X1),X0)) = skaf83(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f295,f209]) ).
fof(f555,plain,
! [X0,X1] :
( ~ ssList(X1)
| cons(skaf83(X0),X1) != nil ),
inference(resolution,[status(thm)],[f297,f209]) ).
fof(f565,definition,
( sQ15_spl
<=> ssList(cons(hd(sk2),nil)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f567,plain,
( sQ15_spl
| ~ ssList(cons(hd(sk2),nil)) ),
inference(component_clause,[status(thm)],[f565]) ).
fof(f576,plain,
! [X0] :
( ~ sQ10_spl
| ~ ssList(X0)
| cons(hd(sk2),X0) != X0 ),
inference(resolution,[status(thm)],[f299,f525]) ).
fof(f578,plain,
! [X0] :
( ~ ssList(X0)
| cons(skac3,X0) != X0 ),
inference(resolution,[status(thm)],[f299,f206]) ).
fof(f579,plain,
! [X0] :
( ~ ssList(X0)
| cons(skac2,X0) != X0 ),
inference(resolution,[status(thm)],[f299,f207]) ).
fof(f585,plain,
( sQ5_spl
| nil = sk2
| ~ ssList(nil)
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f531,f300]) ).
fof(f586,plain,
( sQ5_spl
| sQ14_spl
| ~ sQ8_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f585,f538,f513,f541,f460]) ).
fof(f591,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| neq(nil,nil) ),
inference(forward_demodulation,[status(thm)],[f542,f450]) ).
fof(f592,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f591,f481]) ).
fof(f593,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f592,f513,f541,f449]) ).
fof(f600,plain,
( ~ sQ11_spl
| singletonP(sk1)
| ~ ssList(cons(hd(sk2),nil))
| ~ ssItem(hd(sk2)) ),
inference(paramodulation,[status(thm)],[f528,f482]) ).
fof(f601,plain,
( ~ sQ11_spl
| sQ6_spl
| ~ sQ15_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f600,f524,f565,f464,f527]) ).
fof(f602,plain,
( sQ15_spl
| ~ sQ11_spl
| ~ ssList(sk1) ),
inference(forward_demodulation,[status(thm)],[f528,f567]) ).
fof(f603,plain,
( sQ15_spl
| ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f602,f428]) ).
fof(f604,plain,
( sQ15_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f603]) ).
fof(f613,plain,
cons(skac3,sk2) != sk2,
inference(resolution,[status(thm)],[f578,f429]) ).
fof(f627,plain,
cons(skac3,nil) != nil,
inference(resolution,[status(thm)],[f578,f205]) ).
fof(f670,plain,
( ~ sQ10_spl
| cons(hd(sk2),nil) != nil ),
inference(resolution,[status(thm)],[f576,f205]) ).
fof(f672,plain,
( ~ sQ10_spl
| ~ sQ11_spl
| sk1 != nil ),
inference(forward_demodulation,[status(thm)],[f528,f670]) ).
fof(f684,plain,
cons(skac2,sk2) != sk2,
inference(resolution,[status(thm)],[f579,f429]) ).
fof(f698,plain,
cons(skac2,nil) != nil,
inference(resolution,[status(thm)],[f579,f205]) ).
fof(f718,definition,
! [X1] :
( sQ20_spl
<=> ( ~ ssList(X1)
| ~ ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f719,plain,
! [X0] :
( ~ sQ20_spl
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f718]) ).
fof(f871,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[f271,f205]) ).
fof(f913,definition,
( sQ37_spl
<=> nil = sk1 ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f914,plain,
( ~ sQ37_spl
| nil = sk1 ),
inference(component_clause,[status(thm)],[f913]) ).
fof(f921,plain,
( ~ sQ37_spl
| ~ sQ10_spl
| ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f914,f672]) ).
fof(f922,plain,
( ~ sQ37_spl
| ~ sQ10_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f921]) ).
fof(f952,plain,
app(nil,sk1) = sk1,
inference(resolution,[status(thm)],[f272,f428]) ).
fof(f984,plain,
! [X0] :
( segmentP(app(app(nil,sk1),X0),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(sk1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f952,f491]) ).
fof(f987,definition,
! [X0] :
( sQ45_spl
<=> ( segmentP(app(app(nil,sk1),X0),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f988,plain,
! [X0] :
( ~ sQ45_spl
| segmentP(app(app(nil,sk1),X0),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f987]) ).
fof(f990,plain,
( ~ sQ12_spl
| ~ sQ8_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f984,f987,f513,f533]) ).
fof(f999,plain,
! [X0] :
( ~ sQ45_spl
| segmentP(app(sk1,X0),sk1)
| ~ ssList(app(sk1,X0))
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f952,f988]) ).
fof(f1438,plain,
! [X0] :
( tl(cons(skac3,X0)) = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f294,f206]) ).
fof(f1439,plain,
! [X0] :
( tl(cons(skac2,X0)) = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f294,f207]) ).
fof(f1545,plain,
! [X0,X1] : cons(skaf83(X0),skaf82(X1)) != nil,
inference(resolution,[status(thm)],[f555,f210]) ).
fof(f1832,plain,
( nil = sk2
| cons(skaf83(sk2),skaf82(sk2)) = sk2 ),
inference(resolution,[status(thm)],[f309,f429]) ).
fof(f1847,plain,
( nil = sk1
| cons(skaf83(sk1),skaf82(sk1)) = sk1 ),
inference(resolution,[status(thm)],[f309,f428]) ).
fof(f1849,definition,
( sQ67_spl
<=> cons(skaf83(sk2),skaf82(sk2)) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1850,plain,
( ~ sQ67_spl
| cons(skaf83(sk2),skaf82(sk2)) = sk2 ),
inference(component_clause,[status(thm)],[f1849]) ).
fof(f1852,plain,
( sQ14_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1832,f1849,f541]) ).
fof(f1857,definition,
( sQ69_spl
<=> cons(skaf83(sk1),skaf82(sk1)) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1858,plain,
( ~ sQ69_spl
| cons(skaf83(sk1),skaf82(sk1)) = sk1 ),
inference(component_clause,[status(thm)],[f1857]) ).
fof(f1860,plain,
( sQ37_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1847,f1857,f913]) ).
fof(f2014,plain,
( ~ sQ69_spl
| ssList(sk1)
| ~ ssList(skaf82(sk1))
| ~ ssItem(skaf83(sk1)) ),
inference(paramodulation,[status(thm)],[f1858,f284]) ).
fof(f2017,definition,
( sQ75_spl
<=> ssList(skaf82(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f2019,plain,
( sQ75_spl
| ~ ssList(skaf82(sk1)) ),
inference(component_clause,[status(thm)],[f2017]) ).
fof(f2024,definition,
( sQ77_spl
<=> ssItem(skaf83(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f2026,plain,
( sQ77_spl
| ~ ssItem(skaf83(sk1)) ),
inference(component_clause,[status(thm)],[f2024]) ).
fof(f2027,plain,
( ~ sQ69_spl
| sQ12_spl
| ~ sQ75_spl
| ~ sQ77_spl ),
inference(split_clause,[status(thm)],[f2014,f2024,f2017,f533,f1857]) ).
fof(f2033,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2019,f210]) ).
fof(f2034,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f2033]) ).
fof(f2035,plain,
( sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2026,f209]) ).
fof(f2036,plain,
sQ77_spl,
inference(contradiction_clause,[status(thm)],[f2035]) ).
fof(f2192,plain,
! [X0] :
( ~ sQ10_spl
| app(cons(hd(sk2),nil),X0) = cons(hd(sk2),X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f328,f525]) ).
fof(f2205,plain,
! [X0] :
( ~ sQ10_spl
| ~ sQ11_spl
| app(sk1,X0) = cons(hd(sk2),X0)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f528,f2192]) ).
fof(f2351,plain,
( ~ sQ67_spl
| hd(sk2) = skaf83(sk2)
| ~ ssList(skaf82(sk2)) ),
inference(paramodulation,[status(thm)],[f1850,f549]) ).
fof(f2355,definition,
( sQ83_spl
<=> ssList(skaf82(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f2357,plain,
( sQ83_spl
| ~ ssList(skaf82(sk2)) ),
inference(component_clause,[status(thm)],[f2355]) ).
fof(f2358,definition,
( sQ84_spl
<=> hd(sk2) = skaf83(sk2) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f2359,plain,
( ~ sQ84_spl
| hd(sk2) = skaf83(sk2) ),
inference(component_clause,[status(thm)],[f2358]) ).
fof(f2361,plain,
( ~ sQ67_spl
| sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f2351,f2355,f2358,f1849]) ).
fof(f2362,definition,
( sQ85_spl
<=> ssItem(skaf83(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f2364,plain,
( sQ85_spl
| ~ ssItem(skaf83(sk2)) ),
inference(component_clause,[status(thm)],[f2362]) ).
fof(f2371,plain,
( sQ83_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2357,f210]) ).
fof(f2372,plain,
sQ83_spl,
inference(contradiction_clause,[status(thm)],[f2371]) ).
fof(f2373,plain,
( sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2364,f209]) ).
fof(f2374,plain,
sQ85_spl,
inference(contradiction_clause,[status(thm)],[f2373]) ).
fof(f2429,plain,
( ~ sQ67_spl
| ~ sQ84_spl
| cons(hd(sk2),skaf82(sk2)) = sk2 ),
inference(backward_demodulation,[status(thm)],[f2359,f1850]) ).
fof(f3845,definition,
( sQ193_spl
<=> totalorderedP(nil) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f3847,plain,
( sQ193_spl
| ~ totalorderedP(nil) ),
inference(component_clause,[status(thm)],[f3845]) ).
fof(f5140,plain,
cons(skac2,sk1) != sk1,
inference(resolution,[status(thm)],[f428,f579]) ).
fof(f5142,plain,
cons(skac3,sk1) != sk1,
inference(resolution,[status(thm)],[f428,f578]) ).
fof(f6120,definition,
! [X0] :
( sQ310_spl
<=> ~ ssList(X0) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f6121,plain,
! [X0] :
( ~ sQ310_spl
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f6120]) ).
fof(f6130,plain,
( ~ sQ310_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f428,f6121]) ).
fof(f6162,plain,
~ sQ310_spl,
inference(contradiction_clause,[status(thm)],[f6130]) ).
fof(f6385,plain,
! [X0] :
( ~ ssItem(X0)
| cons(X0,sk2) != nil ),
inference(resolution,[status(thm)],[f297,f429]) ).
fof(f6386,plain,
! [X0] :
( ~ ssItem(X0)
| cons(X0,sk1) != nil ),
inference(resolution,[status(thm)],[f297,f428]) ).
fof(f9939,plain,
! [X0] :
( ssList(app(sk1,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f283,f428]) ).
fof(f10878,plain,
cons(skac2,sk2) != nil,
inference(resolution,[status(thm)],[f6385,f207]) ).
fof(f10879,plain,
cons(skac3,sk2) != nil,
inference(resolution,[status(thm)],[f6385,f206]) ).
fof(f10985,plain,
cons(skac2,sk1) != nil,
inference(resolution,[status(thm)],[f6386,f207]) ).
fof(f10986,plain,
cons(skac3,sk1) != nil,
inference(resolution,[status(thm)],[f6386,f206]) ).
fof(f12065,plain,
tl(cons(skac3,nil)) = nil,
inference(resolution,[status(thm)],[f1438,f205]) ).
fof(f12097,plain,
tl(cons(skac2,nil)) = nil,
inference(resolution,[status(thm)],[f1439,f205]) ).
fof(f12684,plain,
! [X0] :
( ~ sQ20_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f719]) ).
fof(f12685,plain,
( ~ sQ20_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f245,f12684]) ).
fof(f12716,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f12685]) ).
fof(f13184,plain,
! [X0] :
( ssList(cons(skac2,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f284,f207]) ).
fof(f13185,plain,
! [X0] :
( ssList(cons(skac3,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f284,f206]) ).
fof(f13261,definition,
( sQ681_spl
<=> ssList(cons(skac3,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ681_spl])],[split_symbol_definition]) ).
fof(f13263,plain,
( sQ681_spl
| ~ ssList(cons(skac3,sk1)) ),
inference(component_clause,[status(thm)],[f13261]) ).
fof(f13267,definition,
( sQ683_spl
<=> nil = cons(skac3,sk1) ),
introduced(definition,[new_symbols(definition,[sQ683_spl])],[split_symbol_definition]) ).
fof(f13268,plain,
( ~ sQ683_spl
| nil = cons(skac3,sk1) ),
inference(component_clause,[status(thm)],[f13267]) ).
fof(f13271,definition,
( sQ684_spl
<=> ssList(cons(skac3,sk2)) ),
introduced(definition,[new_symbols(definition,[sQ684_spl])],[split_symbol_definition]) ).
fof(f13273,plain,
( sQ684_spl
| ~ ssList(cons(skac3,sk2)) ),
inference(component_clause,[status(thm)],[f13271]) ).
fof(f13274,definition,
( sQ685_spl
<=> nil = cons(skac3,sk2) ),
introduced(definition,[new_symbols(definition,[sQ685_spl])],[split_symbol_definition]) ).
fof(f13275,plain,
( ~ sQ685_spl
| nil = cons(skac3,sk2) ),
inference(component_clause,[status(thm)],[f13274]) ).
fof(f13279,plain,
( sQ193_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3847,f201]) ).
fof(f13280,plain,
sQ193_spl,
inference(contradiction_clause,[status(thm)],[f13279]) ).
fof(f14324,definition,
( sQ688_spl
<=> ssList(cons(skac3,nil)) ),
introduced(definition,[new_symbols(definition,[sQ688_spl])],[split_symbol_definition]) ).
fof(f14326,plain,
( sQ688_spl
| ~ ssList(cons(skac3,nil)) ),
inference(component_clause,[status(thm)],[f14324]) ).
fof(f14327,definition,
( sQ689_spl
<=> nil = cons(skac3,nil) ),
introduced(definition,[new_symbols(definition,[sQ689_spl])],[split_symbol_definition]) ).
fof(f14328,plain,
( ~ sQ689_spl
| nil = cons(skac3,nil) ),
inference(component_clause,[status(thm)],[f14327]) ).
fof(f14660,definition,
( sQ695_spl
<=> ssItem(skaf65(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ695_spl])],[split_symbol_definition]) ).
fof(f14662,plain,
( sQ695_spl
| ~ ssItem(skaf65(sk2)) ),
inference(component_clause,[status(thm)],[f14660]) ).
fof(f14663,definition,
( sQ696_spl
<=> ssItem(skaf64(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ696_spl])],[split_symbol_definition]) ).
fof(f14665,plain,
( sQ696_spl
| ~ ssItem(skaf64(sk2)) ),
inference(component_clause,[status(thm)],[f14663]) ).
fof(f14686,plain,
( sQ696_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14665,f228]) ).
fof(f14687,plain,
sQ696_spl,
inference(contradiction_clause,[status(thm)],[f14686]) ).
fof(f14688,plain,
( sQ695_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14662,f227]) ).
fof(f14689,plain,
sQ695_spl,
inference(contradiction_clause,[status(thm)],[f14688]) ).
fof(f14773,definition,
( sQ702_spl
<=> ssList(cons(skac2,sk2)) ),
introduced(definition,[new_symbols(definition,[sQ702_spl])],[split_symbol_definition]) ).
fof(f14775,plain,
( sQ702_spl
| ~ ssList(cons(skac2,sk2)) ),
inference(component_clause,[status(thm)],[f14773]) ).
fof(f14779,definition,
( sQ704_spl
<=> nil = cons(skac2,sk2) ),
introduced(definition,[new_symbols(definition,[sQ704_spl])],[split_symbol_definition]) ).
fof(f14780,plain,
( ~ sQ704_spl
| nil = cons(skac2,sk2) ),
inference(component_clause,[status(thm)],[f14779]) ).
fof(f14793,plain,
( ~ sQ704_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14780,f10878]) ).
fof(f14794,plain,
~ sQ704_spl,
inference(contradiction_clause,[status(thm)],[f14793]) ).
fof(f14866,plain,
( ~ sQ685_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13275,f10879]) ).
fof(f14867,plain,
~ sQ685_spl,
inference(contradiction_clause,[status(thm)],[f14866]) ).
fof(f14868,plain,
( ~ sQ683_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13268,f10986]) ).
fof(f14869,plain,
~ sQ683_spl,
inference(contradiction_clause,[status(thm)],[f14868]) ).
fof(f14870,plain,
( ~ sQ689_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14328,f627]) ).
fof(f14871,plain,
~ sQ689_spl,
inference(contradiction_clause,[status(thm)],[f14870]) ).
fof(f14959,definition,
( sQ716_spl
<=> ssList(cons(skac2,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ716_spl])],[split_symbol_definition]) ).
fof(f14961,plain,
( sQ716_spl
| ~ ssList(cons(skac2,sk1)) ),
inference(component_clause,[status(thm)],[f14959]) ).
fof(f14962,definition,
( sQ717_spl
<=> nil = cons(skac2,sk1) ),
introduced(definition,[new_symbols(definition,[sQ717_spl])],[split_symbol_definition]) ).
fof(f14963,plain,
( ~ sQ717_spl
| nil = cons(skac2,sk1) ),
inference(component_clause,[status(thm)],[f14962]) ).
fof(f14971,plain,
( ~ sQ717_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14963,f10985]) ).
fof(f14972,plain,
~ sQ717_spl,
inference(contradiction_clause,[status(thm)],[f14971]) ).
fof(f16058,definition,
( sQ726_spl
<=> ssItem(skaf70(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ726_spl])],[split_symbol_definition]) ).
fof(f16060,plain,
( sQ726_spl
| ~ ssItem(skaf70(sk2)) ),
inference(component_clause,[status(thm)],[f16058]) ).
fof(f16061,definition,
( sQ727_spl
<=> ssItem(skaf69(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ727_spl])],[split_symbol_definition]) ).
fof(f16063,plain,
( sQ727_spl
| ~ ssItem(skaf69(sk2)) ),
inference(component_clause,[status(thm)],[f16061]) ).
fof(f16087,plain,
( sQ727_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16063,f223]) ).
fof(f16088,plain,
sQ727_spl,
inference(contradiction_clause,[status(thm)],[f16087]) ).
fof(f16089,plain,
( sQ726_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16060,f222]) ).
fof(f16090,plain,
sQ726_spl,
inference(contradiction_clause,[status(thm)],[f16089]) ).
fof(f17502,plain,
ssList(cons(skac2,sk1)),
inference(resolution,[status(thm)],[f13184,f428]) ).
fof(f17503,plain,
ssList(cons(skac2,sk2)),
inference(resolution,[status(thm)],[f13184,f429]) ).
fof(f17504,plain,
ssList(cons(skac2,nil)),
inference(resolution,[status(thm)],[f13184,f205]) ).
fof(f17505,plain,
( sQ716_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17502,f14961]) ).
fof(f17506,plain,
sQ716_spl,
inference(contradiction_clause,[status(thm)],[f17505]) ).
fof(f17507,plain,
( sQ702_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17503,f14775]) ).
fof(f17508,plain,
sQ702_spl,
inference(contradiction_clause,[status(thm)],[f17507]) ).
fof(f17625,definition,
( sQ783_spl
<=> cons(skaf83(tl(cons(skac2,nil))),skaf82(tl(cons(skac2,nil)))) = tl(cons(skac2,nil)) ),
introduced(definition,[new_symbols(definition,[sQ783_spl])],[split_symbol_definition]) ).
fof(f17626,plain,
( ~ sQ783_spl
| cons(skaf83(tl(cons(skac2,nil))),skaf82(tl(cons(skac2,nil)))) = tl(cons(skac2,nil)) ),
inference(component_clause,[status(thm)],[f17625]) ).
fof(f17631,definition,
( sQ785_spl
<=> nil = cons(skac2,nil) ),
introduced(definition,[new_symbols(definition,[sQ785_spl])],[split_symbol_definition]) ).
fof(f17632,plain,
( ~ sQ785_spl
| nil = cons(skac2,nil) ),
inference(component_clause,[status(thm)],[f17631]) ).
fof(f17689,plain,
( ~ sQ785_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17632,f698]) ).
fof(f17690,plain,
~ sQ785_spl,
inference(contradiction_clause,[status(thm)],[f17689]) ).
fof(f17697,plain,
( ~ sQ783_spl
| cons(skaf83(nil),skaf82(tl(cons(skac2,nil)))) = tl(cons(skac2,nil)) ),
inference(forward_demodulation,[status(thm)],[f12097,f17626]) ).
fof(f17698,plain,
( ~ sQ783_spl
| cons(skaf83(nil),skaf82(nil)) = tl(cons(skac2,nil)) ),
inference(forward_demodulation,[status(thm)],[f12097,f17697]) ).
fof(f17699,plain,
( ~ sQ783_spl
| cons(skaf83(nil),skaf82(nil)) = nil ),
inference(forward_demodulation,[status(thm)],[f12097,f17698]) ).
fof(f17700,plain,
( ~ sQ783_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17699,f1545]) ).
fof(f17701,plain,
~ sQ783_spl,
inference(contradiction_clause,[status(thm)],[f17700]) ).
fof(f17945,definition,
( sQ809_spl
<=> cons(skac2,sk1) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ809_spl])],[split_symbol_definition]) ).
fof(f17946,plain,
( ~ sQ809_spl
| cons(skac2,sk1) = sk1 ),
inference(component_clause,[status(thm)],[f17945]) ).
fof(f17996,plain,
( ~ sQ809_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17946,f5140]) ).
fof(f17997,plain,
~ sQ809_spl,
inference(contradiction_clause,[status(thm)],[f17996]) ).
fof(f18124,definition,
( sQ829_spl
<=> cons(skac2,sk2) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ829_spl])],[split_symbol_definition]) ).
fof(f18125,plain,
( ~ sQ829_spl
| cons(skac2,sk2) = sk2 ),
inference(component_clause,[status(thm)],[f18124]) ).
fof(f18168,plain,
( ~ sQ829_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18125,f684]) ).
fof(f18169,plain,
~ sQ829_spl,
inference(contradiction_clause,[status(thm)],[f18168]) ).
fof(f18195,definition,
( sQ840_spl
<=> ssList(cons(skac2,nil)) ),
introduced(definition,[new_symbols(definition,[sQ840_spl])],[split_symbol_definition]) ).
fof(f18197,plain,
( sQ840_spl
| ~ ssList(cons(skac2,nil)) ),
inference(component_clause,[status(thm)],[f18195]) ).
fof(f22291,plain,
ssList(cons(skac3,sk1)),
inference(resolution,[status(thm)],[f13185,f428]) ).
fof(f22292,plain,
ssList(cons(skac3,sk2)),
inference(resolution,[status(thm)],[f13185,f429]) ).
fof(f22293,plain,
ssList(cons(skac3,nil)),
inference(resolution,[status(thm)],[f13185,f205]) ).
fof(f22294,plain,
( sQ681_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22291,f13263]) ).
fof(f22295,plain,
sQ681_spl,
inference(contradiction_clause,[status(thm)],[f22294]) ).
fof(f22296,plain,
( sQ684_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22292,f13273]) ).
fof(f22297,plain,
sQ684_spl,
inference(contradiction_clause,[status(thm)],[f22296]) ).
fof(f22298,plain,
( sQ688_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22293,f14326]) ).
fof(f22299,plain,
sQ688_spl,
inference(contradiction_clause,[status(thm)],[f22298]) ).
fof(f22457,definition,
( sQ961_spl
<=> cons(skac3,sk1) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ961_spl])],[split_symbol_definition]) ).
fof(f22458,plain,
( ~ sQ961_spl
| cons(skac3,sk1) = sk1 ),
inference(component_clause,[status(thm)],[f22457]) ).
fof(f22508,plain,
( ~ sQ961_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22458,f5142]) ).
fof(f22509,plain,
~ sQ961_spl,
inference(contradiction_clause,[status(thm)],[f22508]) ).
fof(f22688,definition,
( sQ992_spl
<=> cons(skac3,sk2) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ992_spl])],[split_symbol_definition]) ).
fof(f22689,plain,
( ~ sQ992_spl
| cons(skac3,sk2) = sk2 ),
inference(component_clause,[status(thm)],[f22688]) ).
fof(f22732,plain,
( ~ sQ992_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22689,f613]) ).
fof(f22733,plain,
~ sQ992_spl,
inference(contradiction_clause,[status(thm)],[f22732]) ).
fof(f23440,definition,
( sQ1052_spl
<=> cons(skaf83(tl(cons(skac3,nil))),skaf82(tl(cons(skac3,nil)))) = tl(cons(skac3,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1052_spl])],[split_symbol_definition]) ).
fof(f23441,plain,
( ~ sQ1052_spl
| cons(skaf83(tl(cons(skac3,nil))),skaf82(tl(cons(skac3,nil)))) = tl(cons(skac3,nil)) ),
inference(component_clause,[status(thm)],[f23440]) ).
fof(f23510,plain,
( ~ sQ1052_spl
| cons(skaf83(nil),skaf82(tl(cons(skac3,nil)))) = tl(cons(skac3,nil)) ),
inference(forward_demodulation,[status(thm)],[f12065,f23441]) ).
fof(f23511,plain,
( ~ sQ1052_spl
| cons(skaf83(nil),skaf82(nil)) = tl(cons(skac3,nil)) ),
inference(forward_demodulation,[status(thm)],[f12065,f23510]) ).
fof(f23512,plain,
( ~ sQ1052_spl
| cons(skaf83(nil),skaf82(nil)) = nil ),
inference(forward_demodulation,[status(thm)],[f12065,f23511]) ).
fof(f23513,plain,
( ~ sQ1052_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23512,f1545]) ).
fof(f23514,plain,
~ sQ1052_spl,
inference(contradiction_clause,[status(thm)],[f23513]) ).
fof(f28937,definition,
! [X0] :
( sQ1209_spl
<=> ( ~ ssList(X0)
| app(X0,app(nil,nil)) != nil ) ),
introduced(definition,[new_symbols(definition,[sQ1209_spl])],[split_symbol_definition]) ).
fof(f28938,plain,
! [X0] :
( ~ sQ1209_spl
| ~ ssList(X0)
| app(X0,app(nil,nil)) != nil ),
inference(component_clause,[status(thm)],[f28937]) ).
fof(f28941,plain,
! [X0] :
( ~ sQ1209_spl
| ~ ssList(X0)
| app(X0,nil) != nil ),
inference(forward_demodulation,[status(thm)],[f871,f28938]) ).
fof(f31257,plain,
! [X0] :
( ~ sQ45_spl
| segmentP(app(sk1,X0),sk1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f999,f9939]) ).
fof(f31387,plain,
( sQ840_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18197,f17504]) ).
fof(f31388,plain,
sQ840_spl,
inference(contradiction_clause,[status(thm)],[f31387]) ).
fof(f36026,plain,
( ~ sQ1209_spl
| app(nil,nil) != nil ),
inference(resolution,[status(thm)],[f28941,f205]) ).
fof(f36056,plain,
( ~ sQ1209_spl
| nil != nil ),
inference(forward_demodulation,[status(thm)],[f871,f36026]) ).
fof(f36057,plain,
( ~ sQ1209_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f36056]) ).
fof(f36058,plain,
~ sQ1209_spl,
inference(contradiction_clause,[status(thm)],[f36057]) ).
fof(f37170,plain,
( ~ sQ67_spl
| ~ sQ84_spl
| ~ sQ10_spl
| ~ sQ11_spl
| app(sk1,skaf82(sk2)) = sk2
| ~ ssList(skaf82(sk2)) ),
inference(paramodulation,[status(thm)],[f2429,f2205]) ).
fof(f37176,definition,
( sQ1380_spl
<=> app(sk1,skaf82(sk2)) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ1380_spl])],[split_symbol_definition]) ).
fof(f37177,plain,
( ~ sQ1380_spl
| app(sk1,skaf82(sk2)) = sk2 ),
inference(component_clause,[status(thm)],[f37176]) ).
fof(f37179,plain,
( ~ sQ67_spl
| ~ sQ84_spl
| ~ sQ10_spl
| ~ sQ11_spl
| sQ1380_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f37170,f2355,f37176,f527,f524,f2358,f1849]) ).
fof(f39692,plain,
( ~ sQ1380_spl
| ~ sQ45_spl
| segmentP(sk2,sk1)
| ~ ssList(skaf82(sk2)) ),
inference(paramodulation,[status(thm)],[f37177,f31257]) ).
fof(f39703,plain,
( ~ sQ1380_spl
| ~ sQ45_spl
| sQ7_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f39692,f2355,f467,f987,f37176]) ).
fof(f39738,plain,
$false,
inference(sat_refutation,[status(thm)],[f452,f471,f472,f506,f522,f530,f544,f546,f586,f593,f601,f604,f922,f990,f1852,f1860,f2027,f2034,f2036,f2361,f2372,f2374,f6162,f12716,f13280,f14687,f14689,f14794,f14867,f14869,f14871,f14972,f16088,f16090,f17506,f17508,f17690,f17701,f17997,f18169,f22295,f22297,f22299,f22509,f22733,f23514,f31388,f36058,f37179,f39703]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC382-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/10.37 % Computer : n015.cluster.edu
% 0.08/10.37 % Model : x86_64 x86_64
% 0.08/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/10.37 % Memory : 8046.5625MB
% 0.08/10.37 % OS : Linux 6.8.0-71-generic
% 0.08/10.37 % CPULimit : 300
% 0.08/10.37 % WCLimit : 300
% 0.08/10.37 % DateTime : Mon Sep 21 08:23:32 UTC 2026
% 0.08/10.37 % CPUTime :
% 0.08/10.39 % Drodi V4.1.1
% 204.64/36.26 % Refutation found
% 204.64/36.26 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 204.64/36.26 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 62.88/36.40 % Elapsed time: 26.012357 seconds
% 62.88/36.40 % CPU time: 205.593091 seconds
% 62.88/36.40 % Total memory used: 649.432 MB
% 62.88/36.40 % Net memory used: 611.477 MB
%------------------------------------------------------------------------------