%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC253-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 : n013.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:31 PM UTC 2026
% Result : Unsatisfiable 62.12s 8.41s
% Output : CNFRefutation 62.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 62
% Syntax : Number of formulae : 226 ( 34 unt; 36 def)
% Number of atoms : 601 ( 117 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 685 ( 310 ~; 339 |; 0 &)
% ( 36 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 43 ( 41 usr; 37 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-2 aty)
% Number of variables : 111 ( 111 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] : ssList(skaf80(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(f53,axiom,
! [U,V] : ssList(skaf42(U,V)),
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(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(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(f115,axiom,
! [U,V] :
( ~ ssList(U)
| ~ ssList(V)
| ~ neq(U,V)
| U != V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,axiom,
! [U,V] :
( singletonP(V)
| ~ ssList(V)
| ~ ssItem(U)
| cons(U,nil) != V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,axiom,
! [U,V] :
( hd(app(V,U)) = hd(V)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f131,axiom,
! [U,V] :
( app(skaf46(U,V),V) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ rearsegP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f133,axiom,
! [U,V] :
( tl(app(V,U)) = app(tl(V),U)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f143,axiom,
! [U,V,W] :
( rearsegP(W,V)
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != W ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [U,V,W] :
( U = W
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(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)
| ~ singletonP(sk1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f205,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f212,plain,
! [X0] : ssList(skaf80(X0)),
inference(cnf_transformation,[status(thm)],[f15]) ).
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(f250,plain,
! [X0,X1] : ssList(skaf42(X0,X1)),
inference(cnf_transformation,[status(thm)],[f53]) ).
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(f283,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
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(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(f331,plain,
! [X0,X1] :
( hd(app(X1,X0)) = hd(X1)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f341,plain,
! [X0,X1] :
( app(skaf46(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f343,plain,
! [X0,X1] :
( tl(app(X1,X0)) = app(tl(X1),X0)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f355,plain,
! [V,W] :
( rearsegP(W,V)
| ~ ssList(W)
| ~ ssList(V)
| ! [U] :
( ~ ssList(U)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f143]) ).
fof(f356,plain,
! [X0,X1,X2] :
( rearsegP(X2,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f369,plain,
! [U,W] :
( U = W
| ~ ssList(W)
| ! [V] :
( ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f370,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
inference(cnf_transformation,[status(thm)],[f369]) ).
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)
| ~ 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
<=> ( 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
<=> singletonP(sk1) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f468,plain,
( ~ sQ3_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f440,f457,f460,f453]) ).
fof(f469,plain,
( ~ sQ3_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f441,f464,f453]) ).
fof(f477,plain,
! [X1] :
( ~ ssList(X1)
| ~ ssList(X1)
| ~ neq(X1,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f319]) ).
fof(f478,plain,
! [X0] :
( ~ ssList(X0)
| ~ neq(X0,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f477]) ).
fof(f479,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ~ ssList(cons(X0,nil))
| ~ ssItem(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f321]) ).
fof(f484,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f356]) ).
fof(f500,plain,
( sQ3_spl
| ~ neq(sk2,nil) ),
inference(forward_demodulation,[status(thm)],[f432,f455]) ).
fof(f501,plain,
( sQ3_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f500,f450]) ).
fof(f502,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f501]) ).
fof(f503,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(f504,plain,
! [X0,X1] :
( ~ sQ4_spl
| app(sk3,X1) != X0
| tl(sk2) != X1
| ~ ssList(X1)
| sk2 = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f432,f503]) ).
fof(f505,plain,
( ~ sQ4_spl
| ~ ssList(tl(sk2))
| sk2 = app(sk3,tl(sk2))
| ~ ssList(app(sk3,tl(sk2))) ),
inference(destructive_equality_resolution,[status(thm)],[f504]) ).
fof(f512,plain,
( ~ sQ4_spl
| ~ ssList(tl(sk2))
| sk2 = app(sk3,tl(sk2))
| ~ ssList(app(sk1,tl(sk2))) ),
inference(forward_demodulation,[status(thm)],[f433,f505]) ).
fof(f513,plain,
( ~ sQ4_spl
| ~ ssList(tl(sk2))
| sk2 = app(sk1,tl(sk2))
| ~ ssList(app(sk1,tl(sk2))) ),
inference(forward_demodulation,[status(thm)],[f433,f512]) ).
fof(f514,plain,
( ~ sQ4_spl
| ~ ssList(sk1)
| ~ ssList(tl(sk2))
| ~ ssList(tl(sk2))
| sk2 = app(sk1,tl(sk2)) ),
inference(resolution,[status(thm)],[f513,f283]) ).
fof(f515,definition,
( sQ7_spl
<=> sk2 = app(sk1,tl(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f516,plain,
( ~ sQ7_spl
| sk2 = app(sk1,tl(sk2)) ),
inference(component_clause,[status(thm)],[f515]) ).
fof(f518,definition,
( sQ8_spl
<=> ssList(tl(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f520,plain,
( sQ8_spl
| ~ ssList(tl(sk2)) ),
inference(component_clause,[status(thm)],[f518]) ).
fof(f521,definition,
( sQ9_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( sQ9_spl
| ~ ssList(sk1) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f524,plain,
( ~ sQ4_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f514,f515,f518,f521,f457]) ).
fof(f525,plain,
( sQ5_spl
| ~ neq(nil,sk2) ),
inference(forward_demodulation,[status(thm)],[f432,f462]) ).
fof(f526,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f523,f428]) ).
fof(f527,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f526]) ).
fof(f529,plain,
( sQ5_spl
| nil = sk2
| ~ ssList(nil)
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f525,f300]) ).
fof(f536,definition,
( sQ12_spl
<=> nil = sk2 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f537,plain,
( ~ sQ12_spl
| nil = sk2 ),
inference(component_clause,[status(thm)],[f536]) ).
fof(f540,definition,
( sQ13_spl
<=> ssList(sk2) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f542,plain,
( sQ13_spl
| ~ ssList(sk2) ),
inference(component_clause,[status(thm)],[f540]) ).
fof(f543,definition,
( sQ14_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f545,plain,
( sQ14_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f543]) ).
fof(f546,plain,
( sQ5_spl
| sQ12_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f529,f540,f543,f536,f460]) ).
fof(f551,plain,
( sQ8_spl
| nil = sk2
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f520,f273]) ).
fof(f552,plain,
( sQ8_spl
| sQ12_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f551,f540,f536,f518]) ).
fof(f559,plain,
( ~ sQ2_spl
| ~ sQ12_spl
| neq(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f537,f450]) ).
fof(f566,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f545,f205]) ).
fof(f567,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f566]) ).
fof(f571,plain,
( ~ sQ2_spl
| ~ sQ12_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f559,f478]) ).
fof(f572,plain,
( ~ sQ2_spl
| ~ sQ12_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f571,f543,f536,f449]) ).
fof(f573,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f542,f429]) ).
fof(f574,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f573]) ).
fof(f621,definition,
( sQ18_spl
<=> nil = sk1 ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f622,plain,
( ~ sQ18_spl
| nil = sk1 ),
inference(component_clause,[status(thm)],[f621]) ).
fof(f652,definition,
! [X1] :
( sQ23_spl
<=> ~ ssList(X1) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f653,plain,
! [X0] :
( ~ sQ23_spl
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f652]) ).
fof(f691,plain,
( ~ sQ7_spl
| tl(sk2) = app(tl(sk1),tl(sk2))
| nil = sk1
| ~ ssList(sk1)
| ~ ssList(tl(sk2)) ),
inference(paramodulation,[status(thm)],[f516,f343]) ).
fof(f692,definition,
( sQ29_spl
<=> tl(sk2) = app(tl(sk1),tl(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f693,plain,
( ~ sQ29_spl
| tl(sk2) = app(tl(sk1),tl(sk2)) ),
inference(component_clause,[status(thm)],[f692]) ).
fof(f695,plain,
( ~ sQ7_spl
| sQ29_spl
| sQ18_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f691,f518,f521,f621,f692,f515]) ).
fof(f698,plain,
( ~ sQ7_spl
| ~ sQ18_spl
| sk2 = app(nil,tl(sk2)) ),
inference(backward_demodulation,[status(thm)],[f622,f516]) ).
fof(f702,plain,
( ~ sQ7_spl
| ~ sQ18_spl
| sk2 = tl(sk2)
| ~ ssList(tl(sk2)) ),
inference(paramodulation,[status(thm)],[f698,f272]) ).
fof(f711,definition,
( sQ30_spl
<=> sk2 = tl(sk2) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f712,plain,
( ~ sQ30_spl
| sk2 = tl(sk2) ),
inference(component_clause,[status(thm)],[f711]) ).
fof(f714,plain,
( ~ sQ7_spl
| ~ sQ18_spl
| sQ30_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f702,f518,f711,f621,f515]) ).
fof(f734,plain,
( ~ sQ30_spl
| nil = sk2
| cons(hd(sk2),sk2) = sk2
| ~ ssList(sk2) ),
inference(paramodulation,[status(thm)],[f712,f304]) ).
fof(f736,definition,
( sQ34_spl
<=> cons(hd(sk2),sk2) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f737,plain,
( ~ sQ34_spl
| cons(hd(sk2),sk2) = sk2 ),
inference(component_clause,[status(thm)],[f736]) ).
fof(f739,plain,
( ~ sQ30_spl
| sQ12_spl
| sQ34_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f734,f540,f736,f536,f711]) ).
fof(f815,definition,
( sQ39_spl
<=> ssItem(hd(sk2)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f816,plain,
( ~ sQ39_spl
| ssItem(hd(sk2)) ),
inference(component_clause,[status(thm)],[f815]) ).
fof(f817,plain,
( sQ39_spl
| ~ ssItem(hd(sk2)) ),
inference(component_clause,[status(thm)],[f815]) ).
fof(f855,plain,
( sQ39_spl
| nil = sk2
| ~ ssList(sk2) ),
inference(resolution,[status(thm)],[f274,f817]) ).
fof(f856,plain,
( sQ39_spl
| sQ12_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f855,f540,f536,f815]) ).
fof(f873,definition,
( sQ41_spl
<=> ssList(tl(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f875,plain,
( sQ41_spl
| ~ ssList(tl(sk1)) ),
inference(component_clause,[status(thm)],[f873]) ).
fof(f881,definition,
( sQ43_spl
<=> nil = tl(sk1) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f882,plain,
( ~ sQ43_spl
| nil = tl(sk1) ),
inference(component_clause,[status(thm)],[f881]) ).
fof(f883,plain,
( sQ43_spl
| nil != tl(sk1) ),
inference(component_clause,[status(thm)],[f881]) ).
fof(f901,plain,
( sQ41_spl
| nil = sk1
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f875,f273]) ).
fof(f902,plain,
( sQ41_spl
| sQ18_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f901,f521,f621,f873]) ).
fof(f905,plain,
( ~ sQ43_spl
| nil = sk1
| cons(hd(sk1),nil) = sk1
| ~ ssList(sk1) ),
inference(paramodulation,[status(thm)],[f882,f304]) ).
fof(f911,definition,
( sQ48_spl
<=> cons(hd(sk1),nil) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f912,plain,
( ~ sQ48_spl
| cons(hd(sk1),nil) = sk1 ),
inference(component_clause,[status(thm)],[f911]) ).
fof(f914,plain,
( ~ sQ43_spl
| sQ18_spl
| sQ48_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f905,f521,f911,f621,f881]) ).
fof(f1135,plain,
( ~ sQ23_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f250,f653]) ).
fof(f1164,plain,
~ sQ23_spl,
inference(contradiction_clause,[status(thm)],[f1135]) ).
fof(f2003,plain,
! [X0,X1] :
( skaf46(app(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(skaf46(app(X0,X1),X1))
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ rearsegP(app(X0,X1),X1) ),
inference(resolution,[status(thm)],[f341,f370]) ).
fof(f2008,definition,
( sQ123_spl
<=> ssList(skaf46(sk2,sk2)) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f2010,plain,
( sQ123_spl
| ~ ssList(skaf46(sk2,sk2)) ),
inference(component_clause,[status(thm)],[f2008]) ).
fof(f2023,plain,
! [X0,X1] :
( skaf46(app(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(skaf46(app(X0,X1),X1))
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ rearsegP(app(X0,X1),X1) ),
inference(duplicate_literals_removal,[status(thm)],[f2003]) ).
fof(f2024,plain,
! [X0,X1] :
( skaf46(app(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(skaf46(app(X0,X1),X1))
| ~ ssList(X1)
| ~ rearsegP(app(X0,X1),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2023,f283]) ).
fof(f2037,plain,
( sQ123_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2010,f247]) ).
fof(f2038,plain,
sQ123_spl,
inference(contradiction_clause,[status(thm)],[f2037]) ).
fof(f2045,plain,
( ~ sQ7_spl
| hd(sk2) = hd(sk1)
| nil = sk1
| ~ ssList(sk1)
| ~ ssList(tl(sk2)) ),
inference(paramodulation,[status(thm)],[f516,f331]) ).
fof(f2062,definition,
( sQ129_spl
<=> hd(sk2) = hd(sk1) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f2063,plain,
( ~ sQ129_spl
| hd(sk2) = hd(sk1) ),
inference(component_clause,[status(thm)],[f2062]) ).
fof(f2065,plain,
( ~ sQ7_spl
| sQ129_spl
| sQ18_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2045,f518,f521,f621,f2062,f515]) ).
fof(f2663,definition,
( sQ179_spl
<=> ssList(skaf46(nil,sk2)) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f2665,plain,
( sQ179_spl
| ~ ssList(skaf46(nil,sk2)) ),
inference(component_clause,[status(thm)],[f2663]) ).
fof(f2673,plain,
( sQ179_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2665,f247]) ).
fof(f2674,plain,
sQ179_spl,
inference(contradiction_clause,[status(thm)],[f2673]) ).
fof(f2796,definition,
( sQ184_spl
<=> ssList(skaf46(sk2,tl(sk2))) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f2798,plain,
( sQ184_spl
| ~ ssList(skaf46(sk2,tl(sk2))) ),
inference(component_clause,[status(thm)],[f2796]) ).
fof(f2808,plain,
( sQ184_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2798,f247]) ).
fof(f2809,plain,
sQ184_spl,
inference(contradiction_clause,[status(thm)],[f2808]) ).
fof(f2815,definition,
( sQ187_spl
<=> ssList(skaf45(sk2,tl(nil))) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f2817,plain,
( sQ187_spl
| ~ ssList(skaf45(sk2,tl(nil))) ),
inference(component_clause,[status(thm)],[f2815]) ).
fof(f2825,plain,
( sQ187_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2817,f248]) ).
fof(f2826,plain,
sQ187_spl,
inference(contradiction_clause,[status(thm)],[f2825]) ).
fof(f2867,plain,
! [X0,X1] :
( skaf46(app(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(app(X0,X1),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2024,f247]) ).
fof(f2877,definition,
( sQ195_spl
<=> skaf46(tl(sk2),tl(sk2)) = nil ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f2878,plain,
( ~ sQ195_spl
| skaf46(tl(sk2),tl(sk2)) = nil ),
inference(component_clause,[status(thm)],[f2877]) ).
fof(f2889,definition,
( sQ197_spl
<=> app(nil,tl(sk2)) = tl(sk2) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f2890,plain,
( ~ sQ197_spl
| app(nil,tl(sk2)) = tl(sk2) ),
inference(component_clause,[status(thm)],[f2889]) ).
fof(f2891,plain,
( sQ197_spl
| app(nil,tl(sk2)) != tl(sk2) ),
inference(component_clause,[status(thm)],[f2889]) ).
fof(f2896,definition,
( sQ198_spl
<=> ssList(skaf46(sk1,tl(sk2))) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f2898,plain,
( sQ198_spl
| ~ ssList(skaf46(sk1,tl(sk2))) ),
inference(component_clause,[status(thm)],[f2896]) ).
fof(f2914,plain,
( sQ198_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2898,f247]) ).
fof(f2915,plain,
sQ198_spl,
inference(contradiction_clause,[status(thm)],[f2914]) ).
fof(f2923,definition,
( sQ203_spl
<=> ssList(skaf46(nil,tl(sk2))) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f2925,plain,
( sQ203_spl
| ~ ssList(skaf46(nil,tl(sk2))) ),
inference(component_clause,[status(thm)],[f2923]) ).
fof(f2935,plain,
( sQ203_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2925,f247]) ).
fof(f2936,plain,
sQ203_spl,
inference(contradiction_clause,[status(thm)],[f2935]) ).
fof(f2966,definition,
( sQ210_spl
<=> ssList(skaf45(sk2,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f2968,plain,
( sQ210_spl
| ~ ssList(skaf45(sk2,sk1)) ),
inference(component_clause,[status(thm)],[f2966]) ).
fof(f2977,plain,
( sQ210_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2968,f248]) ).
fof(f2978,plain,
sQ210_spl,
inference(contradiction_clause,[status(thm)],[f2977]) ).
fof(f3055,definition,
( sQ219_spl
<=> ssList(skaf80(nil)) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f3057,plain,
( sQ219_spl
| ~ ssList(skaf80(nil)) ),
inference(component_clause,[status(thm)],[f3055]) ).
fof(f3066,plain,
( sQ219_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3057,f212]) ).
fof(f3067,plain,
sQ219_spl,
inference(contradiction_clause,[status(thm)],[f3066]) ).
fof(f3068,plain,
! [X0,X1] :
( skaf46(app(X1,X0),X0) = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2867,f3069]) ).
fof(f3069,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f484,f283]) ).
fof(f3109,plain,
( ~ sQ39_spl
| ~ sQ129_spl
| ssItem(hd(sk1)) ),
inference(backward_demodulation,[status(thm)],[f2063,f816]) ).
fof(f3334,plain,
( ~ sQ197_spl
| skaf46(tl(sk2),tl(sk2)) = nil
| ~ ssList(nil)
| ~ ssList(tl(sk2)) ),
inference(paramodulation,[status(thm)],[f2890,f3068]) ).
fof(f3355,plain,
( ~ sQ197_spl
| sQ195_spl
| ~ sQ14_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3334,f518,f543,f2877,f2889]) ).
fof(f3602,plain,
( sQ197_spl
| ~ ssList(tl(sk2)) ),
inference(resolution,[status(thm)],[f2891,f272]) ).
fof(f3603,plain,
( sQ197_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3602,f518,f2889]) ).
fof(f3660,plain,
( ~ sQ29_spl
| skaf46(tl(sk2),tl(sk2)) = tl(sk1)
| ~ ssList(tl(sk1))
| ~ ssList(tl(sk2)) ),
inference(paramodulation,[status(thm)],[f693,f3068]) ).
fof(f3679,definition,
( sQ255_spl
<=> skaf46(tl(sk2),tl(sk2)) = tl(sk1) ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f3680,plain,
( ~ sQ255_spl
| skaf46(tl(sk2),tl(sk2)) = tl(sk1) ),
inference(component_clause,[status(thm)],[f3679]) ).
fof(f3682,plain,
( ~ sQ29_spl
| sQ255_spl
| ~ sQ41_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3660,f518,f873,f3679,f692]) ).
fof(f3709,plain,
( ~ sQ255_spl
| ~ sQ195_spl
| nil = tl(sk1) ),
inference(forward_demodulation,[status(thm)],[f2878,f3680]) ).
fof(f3710,plain,
( ~ sQ255_spl
| ~ sQ195_spl
| sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3709,f883]) ).
fof(f3711,plain,
( ~ sQ255_spl
| ~ sQ195_spl
| sQ43_spl ),
inference(contradiction_clause,[status(thm)],[f3710]) ).
fof(f3934,definition,
( sQ274_spl
<=> ssList(skaf45(sk2,nil)) ),
introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition]) ).
fof(f3936,plain,
( sQ274_spl
| ~ ssList(skaf45(sk2,nil)) ),
inference(component_clause,[status(thm)],[f3934]) ).
fof(f3941,definition,
( sQ276_spl
<=> ssList(skaf45(tl(sk2),nil)) ),
introduced(definition,[new_symbols(definition,[sQ276_spl])],[split_symbol_definition]) ).
fof(f3943,plain,
( sQ276_spl
| ~ ssList(skaf45(tl(sk2),nil)) ),
inference(component_clause,[status(thm)],[f3941]) ).
fof(f3949,plain,
( sQ274_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3936,f248]) ).
fof(f3950,plain,
sQ274_spl,
inference(contradiction_clause,[status(thm)],[f3949]) ).
fof(f3951,plain,
( sQ276_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3943,f248]) ).
fof(f3952,plain,
sQ276_spl,
inference(contradiction_clause,[status(thm)],[f3951]) ).
fof(f4225,definition,
( sQ310_spl
<=> ssItem(hd(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f4227,plain,
( sQ310_spl
| ~ ssItem(hd(sk1)) ),
inference(component_clause,[status(thm)],[f4225]) ).
fof(f4546,plain,
( ~ sQ48_spl
| singletonP(sk1)
| ~ ssList(cons(hd(sk1),nil))
| ~ ssItem(hd(sk1)) ),
inference(paramodulation,[status(thm)],[f912,f479]) ).
fof(f4555,definition,
( sQ347_spl
<=> ssList(cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ347_spl])],[split_symbol_definition]) ).
fof(f4557,plain,
( sQ347_spl
| ~ ssList(cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f4555]) ).
fof(f4569,plain,
( ~ sQ48_spl
| sQ6_spl
| ~ sQ347_spl
| ~ sQ310_spl ),
inference(split_clause,[status(thm)],[f4546,f4225,f4555,f464,f911]) ).
fof(f4590,plain,
( sQ310_spl
| ~ sQ39_spl
| ~ sQ129_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4227,f3109]) ).
fof(f4591,plain,
( sQ310_spl
| ~ sQ39_spl
| ~ sQ129_spl ),
inference(contradiction_clause,[status(thm)],[f4590]) ).
fof(f4592,plain,
( sQ347_spl
| ~ sQ48_spl
| ~ ssList(sk1) ),
inference(forward_demodulation,[status(thm)],[f912,f4557]) ).
fof(f4593,plain,
( sQ347_spl
| ~ sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4592,f428]) ).
fof(f4594,plain,
( sQ347_spl
| ~ sQ48_spl ),
inference(contradiction_clause,[status(thm)],[f4593]) ).
fof(f4949,plain,
( ~ sQ34_spl
| ~ ssList(sk2)
| ~ ssItem(hd(sk2)) ),
inference(resolution,[status(thm)],[f299,f737]) ).
fof(f4957,plain,
( ~ sQ34_spl
| ~ sQ13_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f4949,f815,f540,f736]) ).
fof(f4961,plain,
$false,
inference(sat_refutation,[status(thm)],[f452,f468,f469,f502,f524,f527,f546,f552,f567,f572,f574,f695,f714,f739,f856,f902,f914,f1164,f2038,f2065,f2674,f2809,f2826,f2915,f2936,f2978,f3067,f3355,f3603,f3682,f3711,f3950,f3952,f4569,f4591,f4594,f4957]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC253-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n013.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 08:08:05 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.46 % Drodi V4.1.1
% 62.12/8.41 % Refutation found
% 62.12/8.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 62.12/8.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 34.32/8.48 % Elapsed time: 8.031615 seconds
% 34.32/8.48 % CPU time: 63.041218 seconds
% 34.32/8.48 % Total memory used: 378.829 MB
% 34.32/8.48 % Net memory used: 353.227 MB
%------------------------------------------------------------------------------