%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC022-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 : n009.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:39:37 PM UTC 2026
% Result : Unsatisfiable 18.90s 2.91s
% Output : CNFRefutation 19.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 67
% Syntax : Number of formulae : 245 ( 55 unt; 38 def)
% Number of atoms : 580 ( 83 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 637 ( 302 ~; 297 |; 0 &)
% ( 38 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 47 ( 45 usr; 39 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-2 aty)
% Number of variables : 98 ( 98 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
strictorderedP(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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(f47,axiom,
! [U] : ssItem(skaf44(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [U] :
( frontsegP(U,U)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [U] :
( nil = U
| ssList(tl(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [U] :
( nil = U
| ssItem(hd(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [U,V] :
( ssList(cons(U,V))
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(f104,axiom,
! [U] :
( nil = U
| cons(hd(U),tl(U)) = U
| ~ 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(f178,axiom,
! [U,V,W,X] :
( frontsegP(cons(W,U),cons(X,V))
| ~ ssItem(W)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(V)
| W != X
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
ssList(sk4),
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] :
( ~ neq(sk4,nil)
| ~ frontsegP(sk1,A)
| ~ frontsegP(sk2,A)
| ~ neq(A,nil)
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,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(f200,plain,
strictorderedP(nil),
inference(cnf_transformation,[status(thm)],[f3]) ).
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(f244,plain,
! [X0] : ssItem(skaf44(X0)),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f257,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f258,plain,
! [X0] :
( frontsegP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f268,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
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(f284,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
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(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(f413,plain,
! [X0,X1,X2,X3] :
( frontsegP(cons(X2,X0),cons(X3,X1))
| ~ ssItem(X2)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X1)
| X2 != X3
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f430,plain,
ssList(sk3),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f431,plain,
ssList(sk4),
inference(cnf_transformation,[status(thm)],[f189]) ).
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(f440,plain,
( ~ neq(sk4,nil)
| ! [A] :
( ~ frontsegP(sk1,A)
| ~ frontsegP(sk2,A)
| ~ neq(A,nil)
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f196]) ).
fof(f441,plain,
! [X0] :
( ~ neq(sk4,nil)
| ~ frontsegP(sk1,X0)
| ~ frontsegP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f440]) ).
fof(f442,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)],[f197]) ).
fof(f443,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)],[f442]) ).
fof(f451,definition,
( sQ2_spl
<=> neq(sk2,nil) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f452,plain,
( ~ sQ2_spl
| neq(sk2,nil) ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,plain,
sQ2_spl,
inference(split_clause,[status(thm)],[f434,f451]) ).
fof(f455,definition,
( sQ3_spl
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( sQ3_spl
| ~ neq(sk4,nil) ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f459,definition,
! [X0] :
( sQ4_spl
<=> ( ~ frontsegP(sk1,X0)
| ~ frontsegP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f460,plain,
! [X0] :
( ~ sQ4_spl
| ~ frontsegP(sk1,X0)
| ~ frontsegP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f463,definition,
! [X0,X1] :
( sQ5_spl
<=> ( hd(sk4) != X1
| cons(X1,nil) != X0
| ~ ssItem(X1)
| sk3 = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f464,plain,
! [X0,X1] :
( ~ sQ5_spl
| hd(sk4) != X1
| cons(X1,nil) != X0
| ~ ssItem(X1)
| sk3 = X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f466,definition,
( sQ6_spl
<=> neq(nil,sk4) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f468,plain,
( sQ6_spl
| ~ neq(nil,sk4) ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f470,plain,
( ~ sQ3_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f441,f459,f455]) ).
fof(f471,plain,
( ~ sQ3_spl
| ~ sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f443,f463,f466,f455]) ).
fof(f479,plain,
! [X1] :
( ~ ssList(X1)
| ~ ssList(X1)
| ~ neq(X1,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f319]) ).
fof(f480,plain,
! [X0] :
( ~ ssList(X0)
| ~ neq(X0,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f479]) ).
fof(f492,plain,
! [X0,X1,X3] :
( frontsegP(cons(X3,X0),cons(X3,X1))
| ~ ssItem(X3)
| ~ ssItem(X3)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f413]) ).
fof(f493,plain,
! [X0,X1,X2] :
( frontsegP(cons(X2,X0),cons(X2,X1))
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f492]) ).
fof(f503,plain,
( ~ sQ2_spl
| neq(sk4,nil) ),
inference(forward_demodulation,[status(thm)],[f432,f452]) ).
fof(f504,plain,
( sQ3_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f457,f503]) ).
fof(f505,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f504]) ).
fof(f506,plain,
( ~ sQ5_spl
| ~ ssItem(hd(sk4))
| sk3 = cons(hd(sk4),nil)
| ~ ssList(cons(hd(sk4),nil)) ),
inference(destructive_equality_resolution,[status(thm)],[f464]) ).
fof(f511,plain,
! [X0] :
( ~ sQ4_spl
| ~ frontsegP(sk1,X0)
| ~ frontsegP(sk4,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f432,f460]) ).
fof(f512,plain,
! [X0] :
( ~ sQ4_spl
| ~ frontsegP(sk3,X0)
| ~ frontsegP(sk4,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f433,f511]) ).
fof(f514,definition,
( sQ7_spl
<=> ssList(sk4) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f516,plain,
( sQ7_spl
| ~ ssList(sk4) ),
inference(component_clause,[status(thm)],[f514]) ).
fof(f526,definition,
( sQ10_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f528,plain,
( sQ10_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f526]) ).
fof(f534,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f528,f205]) ).
fof(f535,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f534]) ).
fof(f537,plain,
! [X0] :
( ~ ssList(X0)
| cons(skac2,X0) != X0 ),
inference(resolution,[status(thm)],[f299,f207]) ).
fof(f538,plain,
! [X0] :
( ~ ssList(X0)
| cons(skac3,X0) != X0 ),
inference(resolution,[status(thm)],[f299,f206]) ).
fof(f543,plain,
cons(skac2,nil) != nil,
inference(resolution,[status(thm)],[f537,f205]) ).
fof(f546,plain,
( ~ sQ5_spl
| ~ ssItem(hd(sk4))
| sk3 = cons(hd(sk4),nil)
| ~ ssList(nil)
| ~ ssItem(hd(sk4)) ),
inference(resolution,[status(thm)],[f284,f506]) ).
fof(f548,definition,
( sQ12_spl
<=> ssItem(hd(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f549,plain,
( ~ sQ12_spl
| ssItem(hd(sk4)) ),
inference(component_clause,[status(thm)],[f548]) ).
fof(f550,plain,
( sQ12_spl
| ~ ssItem(hd(sk4)) ),
inference(component_clause,[status(thm)],[f548]) ).
fof(f551,definition,
( sQ13_spl
<=> sk3 = cons(hd(sk4),nil) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f552,plain,
( ~ sQ13_spl
| sk3 = cons(hd(sk4),nil) ),
inference(component_clause,[status(thm)],[f551]) ).
fof(f554,plain,
( ~ sQ5_spl
| sQ13_spl
| ~ sQ10_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f546,f548,f526,f551,f463]) ).
fof(f586,plain,
( sQ12_spl
| nil = sk4
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f550,f274]) ).
fof(f587,definition,
( sQ14_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f588,plain,
( ~ sQ14_spl
| nil = sk4 ),
inference(component_clause,[status(thm)],[f587]) ).
fof(f590,plain,
( sQ12_spl
| sQ14_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f586,f514,f587,f548]) ).
fof(f591,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f516,f431]) ).
fof(f592,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f591]) ).
fof(f607,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| neq(sk4,sk4) ),
inference(backward_demodulation,[status(thm)],[f588,f503]) ).
fof(f683,plain,
( sQ6_spl
| nil = sk4
| ~ ssList(nil)
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f468,f300]) ).
fof(f684,plain,
( sQ6_spl
| sQ14_spl
| ~ sQ10_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f683,f514,f526,f587,f466]) ).
fof(f687,plain,
! [X0] :
( ~ sQ12_spl
| ~ ssList(X0)
| cons(hd(sk4),X0) != X0 ),
inference(resolution,[status(thm)],[f549,f299]) ).
fof(f699,definition,
( sQ21_spl
<=> ssItem(skac2) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f701,plain,
( sQ21_spl
| ~ ssItem(skac2) ),
inference(component_clause,[status(thm)],[f699]) ).
fof(f703,definition,
( sQ22_spl
<=> ssItem(skac3) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f705,plain,
( sQ22_spl
| ~ ssItem(skac3) ),
inference(component_clause,[status(thm)],[f703]) ).
fof(f721,definition,
( sQ23_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f742,definition,
( sQ25_spl
<=> frontsegP(sk4,sk3) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f754,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f607,f480]) ).
fof(f755,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f754,f514,f587,f451]) ).
fof(f759,plain,
( ~ sQ4_spl
| ~ ssList(sk3)
| ~ frontsegP(sk4,sk3)
| ~ neq(sk3,nil)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f512,f258]) ).
fof(f760,definition,
( sQ26_spl
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f762,plain,
( sQ26_spl
| ~ neq(sk3,nil) ),
inference(component_clause,[status(thm)],[f760]) ).
fof(f763,plain,
( ~ sQ4_spl
| ~ sQ25_spl
| ~ sQ26_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f759,f721,f760,f742,f459]) ).
fof(f870,definition,
! [X1] :
( sQ42_spl
<=> ( ~ ssList(X1)
| ~ ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f871,plain,
! [X0] :
( ~ sQ42_spl
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f870]) ).
fof(f987,plain,
( ~ sQ12_spl
| cons(hd(sk4),nil) != nil ),
inference(resolution,[status(thm)],[f687,f205]) ).
fof(f1018,plain,
( ~ sQ12_spl
| ~ sQ13_spl
| sk3 != nil ),
inference(forward_demodulation,[status(thm)],[f552,f987]) ).
fof(f1036,plain,
cons(skac3,nil) != nil,
inference(resolution,[status(thm)],[f538,f205]) ).
fof(f1185,definition,
( sQ67_spl
<=> sk3 = nil ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1186,plain,
( ~ sQ67_spl
| sk3 = nil ),
inference(component_clause,[status(thm)],[f1185]) ).
fof(f1278,plain,
! [X0] :
( ~ sQ13_spl
| frontsegP(cons(hd(sk4),X0),sk3)
| ~ ssItem(hd(sk4))
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(X0,nil) ),
inference(paramodulation,[status(thm)],[f552,f493]) ).
fof(f1299,definition,
! [X0] :
( sQ75_spl
<=> ( frontsegP(cons(hd(sk4),X0),sk3)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1300,plain,
! [X0] :
( ~ sQ75_spl
| frontsegP(cons(hd(sk4),X0),sk3)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ),
inference(component_clause,[status(thm)],[f1299]) ).
fof(f1302,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ10_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f1278,f1299,f526,f548,f551]) ).
fof(f1303,plain,
! [X0] :
( ~ sQ75_spl
| frontsegP(cons(hd(sk4),X0),sk3)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1300,f257]) ).
fof(f1321,plain,
! [X0] :
( ~ ssList(X0)
| cons(skac2,X0) != nil ),
inference(resolution,[status(thm)],[f297,f207]) ).
fof(f1322,plain,
! [X0] :
( ~ ssList(X0)
| cons(skac3,X0) != nil ),
inference(resolution,[status(thm)],[f297,f206]) ).
fof(f1495,plain,
( ~ sQ67_spl
| ~ sQ12_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1186,f1018]) ).
fof(f1496,plain,
( ~ sQ67_spl
| ~ sQ12_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f1495]) ).
fof(f1955,plain,
( nil = sk4
| cons(hd(sk4),tl(sk4)) = sk4 ),
inference(resolution,[status(thm)],[f304,f431]) ).
fof(f1962,definition,
( sQ89_spl
<=> cons(hd(sk4),tl(sk4)) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1963,plain,
( ~ sQ89_spl
| cons(hd(sk4),tl(sk4)) = sk4 ),
inference(component_clause,[status(thm)],[f1962]) ).
fof(f1965,plain,
( sQ14_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f1955,f1962,f587]) ).
fof(f2219,definition,
( sQ102_spl
<=> ssList(tl(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f2221,plain,
( sQ102_spl
| ~ ssList(tl(sk4)) ),
inference(component_clause,[status(thm)],[f2219]) ).
fof(f2259,plain,
( sQ102_spl
| nil = sk4
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f2221,f273]) ).
fof(f2260,plain,
( sQ102_spl
| sQ14_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f2259,f514,f587,f2219]) ).
fof(f2569,plain,
( nil = sk3
| cons(skaf83(sk3),skaf82(sk3)) = sk3 ),
inference(resolution,[status(thm)],[f309,f430]) ).
fof(f2583,definition,
( sQ164_spl
<=> cons(skaf83(sk3),skaf82(sk3)) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f2584,plain,
( ~ sQ164_spl
| cons(skaf83(sk3),skaf82(sk3)) = sk3 ),
inference(component_clause,[status(thm)],[f2583]) ).
fof(f2586,plain,
( sQ67_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f2569,f2583,f1185]) ).
fof(f2633,plain,
( ~ sQ164_spl
| ssList(sk3)
| ~ ssList(skaf82(sk3))
| ~ ssItem(skaf83(sk3)) ),
inference(paramodulation,[status(thm)],[f2584,f284]) ).
fof(f2634,definition,
( sQ165_spl
<=> ssList(skaf82(sk3)) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f2636,plain,
( sQ165_spl
| ~ ssList(skaf82(sk3)) ),
inference(component_clause,[status(thm)],[f2634]) ).
fof(f2641,definition,
( sQ167_spl
<=> ssItem(skaf83(sk3)) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f2643,plain,
( sQ167_spl
| ~ ssItem(skaf83(sk3)) ),
inference(component_clause,[status(thm)],[f2641]) ).
fof(f2681,plain,
( ~ sQ164_spl
| sQ23_spl
| ~ sQ165_spl
| ~ sQ167_spl ),
inference(split_clause,[status(thm)],[f2633,f2641,f2634,f721,f2583]) ).
fof(f2682,plain,
( sQ165_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2636,f210]) ).
fof(f2683,plain,
sQ165_spl,
inference(contradiction_clause,[status(thm)],[f2682]) ).
fof(f2684,plain,
( sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2643,f209]) ).
fof(f2685,plain,
sQ167_spl,
inference(contradiction_clause,[status(thm)],[f2684]) ).
fof(f2938,definition,
( sQ221_spl
<=> ssList(skaf82(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f2940,plain,
( sQ221_spl
| ~ ssList(skaf82(sk4)) ),
inference(component_clause,[status(thm)],[f2938]) ).
fof(f2945,definition,
( sQ223_spl
<=> ssItem(skaf83(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f2947,plain,
( sQ223_spl
| ~ ssItem(skaf83(sk4)) ),
inference(component_clause,[status(thm)],[f2945]) ).
fof(f2983,plain,
( sQ221_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2940,f210]) ).
fof(f2984,plain,
sQ221_spl,
inference(contradiction_clause,[status(thm)],[f2983]) ).
fof(f2985,plain,
( sQ223_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2947,f209]) ).
fof(f2986,plain,
sQ223_spl,
inference(contradiction_clause,[status(thm)],[f2985]) ).
fof(f3033,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f701,f207]) ).
fof(f3034,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f3033]) ).
fof(f3401,plain,
( sQ26_spl
| sk3 = nil
| ~ ssList(sk3)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f762,f300]) ).
fof(f3406,plain,
( sQ26_spl
| sQ67_spl
| ~ sQ23_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f3401,f526,f721,f1185,f760]) ).
fof(f3876,definition,
( sQ305_spl
<=> nil = cons(skac2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition]) ).
fof(f3877,plain,
( ~ sQ305_spl
| nil = cons(skac2,sk3) ),
inference(component_clause,[status(thm)],[f3876]) ).
fof(f3902,definition,
( sQ308_spl
<=> totalorderedP(nil) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f3904,plain,
( sQ308_spl
| ~ totalorderedP(nil) ),
inference(component_clause,[status(thm)],[f3902]) ).
fof(f3909,definition,
( sQ310_spl
<=> strictorderedP(nil) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f3911,plain,
( sQ310_spl
| ~ strictorderedP(nil) ),
inference(component_clause,[status(thm)],[f3909]) ).
fof(f3995,plain,
( sQ308_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3904,f201]) ).
fof(f3996,plain,
sQ308_spl,
inference(contradiction_clause,[status(thm)],[f3995]) ).
fof(f4058,plain,
! [X0] :
( ~ sQ42_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f871]) ).
fof(f4059,plain,
( ~ sQ42_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f430,f4058]) ).
fof(f4092,plain,
~ sQ42_spl,
inference(contradiction_clause,[status(thm)],[f4059]) ).
fof(f4212,plain,
cons(skac2,sk3) != nil,
inference(resolution,[status(thm)],[f1321,f430]) ).
fof(f4413,plain,
( sQ310_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3911,f200]) ).
fof(f4414,plain,
sQ310_spl,
inference(contradiction_clause,[status(thm)],[f4413]) ).
fof(f4426,plain,
( ~ sQ305_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3877,f4212]) ).
fof(f4427,plain,
~ sQ305_spl,
inference(contradiction_clause,[status(thm)],[f4426]) ).
fof(f4651,definition,
( sQ359_spl
<=> ssList(cons(skac3,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition]) ).
fof(f4653,plain,
( sQ359_spl
| ~ ssList(cons(skac3,sk3)) ),
inference(component_clause,[status(thm)],[f4651]) ).
fof(f4654,definition,
( sQ360_spl
<=> nil = cons(skac3,sk3) ),
introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition]) ).
fof(f4655,plain,
( ~ sQ360_spl
| nil = cons(skac3,sk3) ),
inference(component_clause,[status(thm)],[f4654]) ).
fof(f4658,definition,
( sQ361_spl
<=> ssList(cons(skac3,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition]) ).
fof(f4660,plain,
( sQ361_spl
| ~ ssList(cons(skac3,sk4)) ),
inference(component_clause,[status(thm)],[f4658]) ).
fof(f4979,definition,
( sQ363_spl
<=> memberP(nil,skac3) ),
introduced(definition,[new_symbols(definition,[sQ363_spl])],[split_symbol_definition]) ).
fof(f4980,plain,
( ~ sQ363_spl
| memberP(nil,skac3) ),
inference(component_clause,[status(thm)],[f4979]) ).
fof(f5008,plain,
( ~ sQ363_spl
| ~ ssItem(skac3) ),
inference(resolution,[status(thm)],[f4980,f268]) ).
fof(f5012,plain,
( ~ sQ363_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5008,f206]) ).
fof(f5013,plain,
~ sQ363_spl,
inference(contradiction_clause,[status(thm)],[f5012]) ).
fof(f5014,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f705,f206]) ).
fof(f5015,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f5014]) ).
fof(f5575,plain,
cons(skac3,sk3) != nil,
inference(resolution,[status(thm)],[f1322,f430]) ).
fof(f6043,definition,
( sQ427_spl
<=> nil = cons(skac2,nil) ),
introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition]) ).
fof(f6044,plain,
( ~ sQ427_spl
| nil = cons(skac2,nil) ),
inference(component_clause,[status(thm)],[f6043]) ).
fof(f6048,definition,
( sQ428_spl
<=> ssList(cons(skac3,nil)) ),
introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition]) ).
fof(f6050,plain,
( sQ428_spl
| ~ ssList(cons(skac3,nil)) ),
inference(component_clause,[status(thm)],[f6048]) ).
fof(f6051,definition,
( sQ429_spl
<=> nil = cons(skac3,nil) ),
introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition]) ).
fof(f6052,plain,
( ~ sQ429_spl
| nil = cons(skac3,nil) ),
inference(component_clause,[status(thm)],[f6051]) ).
fof(f6287,definition,
( sQ443_spl
<=> ssItem(skaf44(sk3)) ),
introduced(definition,[new_symbols(definition,[sQ443_spl])],[split_symbol_definition]) ).
fof(f6289,plain,
( sQ443_spl
| ~ ssItem(skaf44(sk3)) ),
inference(component_clause,[status(thm)],[f6287]) ).
fof(f6368,plain,
( sQ443_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6289,f244]) ).
fof(f6369,plain,
sQ443_spl,
inference(contradiction_clause,[status(thm)],[f6368]) ).
fof(f7338,plain,
! [X0] :
( ssList(cons(skac3,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f284,f206]) ).
fof(f7545,plain,
! [X0] :
( ssList(app(sk3,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f283,f430]) ).
fof(f7576,plain,
! [X0] :
( ssList(app(sk4,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f283,f431]) ).
fof(f8864,plain,
ssList(cons(skac3,sk3)),
inference(resolution,[status(thm)],[f7338,f430]) ).
fof(f8896,plain,
ssList(cons(skac3,sk4)),
inference(resolution,[status(thm)],[f7338,f431]) ).
fof(f8897,plain,
ssList(cons(skac3,nil)),
inference(resolution,[status(thm)],[f7338,f205]) ).
fof(f8963,plain,
( ~ sQ360_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4655,f5575]) ).
fof(f8964,plain,
~ sQ360_spl,
inference(contradiction_clause,[status(thm)],[f8963]) ).
fof(f9099,plain,
( ~ sQ429_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6052,f1036]) ).
fof(f9100,plain,
~ sQ429_spl,
inference(contradiction_clause,[status(thm)],[f9099]) ).
fof(f11095,definition,
( sQ577_spl
<=> ssList(app(sk3,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ577_spl])],[split_symbol_definition]) ).
fof(f11097,plain,
( sQ577_spl
| ~ ssList(app(sk3,sk3)) ),
inference(component_clause,[status(thm)],[f11095]) ).
fof(f11110,plain,
( sQ577_spl
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f11097,f7545]) ).
fof(f11111,plain,
( sQ577_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11110,f430]) ).
fof(f11112,plain,
sQ577_spl,
inference(contradiction_clause,[status(thm)],[f11111]) ).
fof(f11700,definition,
( sQ622_spl
<=> ssList(app(sk4,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ622_spl])],[split_symbol_definition]) ).
fof(f11702,plain,
( sQ622_spl
| ~ ssList(app(sk4,sk3)) ),
inference(component_clause,[status(thm)],[f11700]) ).
fof(f11848,plain,
( sQ622_spl
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f11702,f7576]) ).
fof(f11849,plain,
( sQ622_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11848,f430]) ).
fof(f11850,plain,
sQ622_spl,
inference(contradiction_clause,[status(thm)],[f11849]) ).
fof(f13673,plain,
( sQ361_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4660,f8896]) ).
fof(f13674,plain,
sQ361_spl,
inference(contradiction_clause,[status(thm)],[f13673]) ).
fof(f13675,plain,
( sQ359_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4653,f8864]) ).
fof(f13676,plain,
sQ359_spl,
inference(contradiction_clause,[status(thm)],[f13675]) ).
fof(f13677,plain,
( sQ428_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6050,f8897]) ).
fof(f13678,plain,
sQ428_spl,
inference(contradiction_clause,[status(thm)],[f13677]) ).
fof(f13679,plain,
( ~ sQ427_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6044,f543]) ).
fof(f13680,plain,
~ sQ427_spl,
inference(contradiction_clause,[status(thm)],[f13679]) ).
fof(f18614,plain,
( ~ sQ89_spl
| ~ sQ75_spl
| frontsegP(sk4,sk3)
| ~ ssList(tl(sk4)) ),
inference(paramodulation,[status(thm)],[f1963,f1303]) ).
fof(f18650,plain,
( ~ sQ89_spl
| ~ sQ75_spl
| sQ25_spl
| ~ sQ102_spl ),
inference(split_clause,[status(thm)],[f18614,f2219,f742,f1299,f1962]) ).
fof(f18651,plain,
$false,
inference(sat_refutation,[status(thm)],[f454,f470,f471,f505,f535,f554,f590,f592,f684,f755,f763,f1302,f1496,f1965,f2260,f2586,f2681,f2683,f2685,f2984,f2986,f3034,f3406,f3996,f4092,f4414,f4427,f5013,f5015,f6369,f8964,f9100,f11112,f11850,f13674,f13676,f13678,f13680,f18650]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC022-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n009.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 07:49:58 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 18.90/2.91 % Refutation found
% 18.90/2.91 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 18.90/2.91 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 19.66/2.97 % Elapsed time: 2.594022 seconds
% 19.66/2.97 % CPU time: 20.050378 seconds
% 19.66/2.97 % Total memory used: 247.795 MB
% 19.66/2.97 % Net memory used: 240.185 MB
%------------------------------------------------------------------------------