%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC169-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 : n007.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:14 PM UTC 2026
% Result : Unsatisfiable 25.04s 3.65s
% Output : CNFRefutation 25.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 83
% Syntax : Number of formulae : 295 ( 33 unt; 46 def)
% Number of atoms : 924 ( 142 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1182 ( 553 ~; 583 |; 0 &)
% ( 46 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 53 ( 51 usr; 47 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-2 aty)
% Number of variables : 169 ( 169 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
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(f51,axiom,
! [U,V] : ssList(skaf45(U,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [U] :
( frontsegP(U,nil)
| ~ 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(f74,axiom,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [U] :
( nil = U
| ssList(tl(U))
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(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(f102,axiom,
! [U,V] :
( V = U
| neq(V,U)
| ~ ssItem(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [U] :
( nil = U
| cons(hd(U),tl(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [U] :
( nil = U
| cons(skaf83(U),skaf82(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,axiom,
! [U,V] :
( hd(app(V,U)) = hd(V)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ frontsegP(V,U)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,axiom,
! [U,V,W] :
( frontsegP(app(U,W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,axiom,
! [U,V,W] :
( memberP(cons(V,W),U)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssList(W)
| U != V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,axiom,
! [U,V,W] :
( memberP(app(U,W),V)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [U,V,W] :
( memberP(app(W,U),V)
| ~ ssItem(V)
| ~ ssList(W)
| ~ ssList(U)
| ~ memberP(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f144,axiom,
! [U,V,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != W ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,axiom,
! [U,V,W] :
( app(app(W,V),U) = app(W,app(V,U))
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,axiom,
! [U,V,W] :
( W = U
| memberP(V,W)
| ~ ssItem(W)
| ~ ssItem(U)
| ~ ssList(V)
| ~ memberP(cons(U,V),W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f171,axiom,
! [U,V,W,X] :
( X = V
| ~ ssList(V)
| ~ ssList(X)
| ~ ssItem(U)
| ~ ssItem(W)
| cons(U,V) != cons(W,X) ),
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(f186,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
~ neq(sk5,sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
( nil = sk3
| ssItem(sk9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,negated_conjecture,
( nil = sk3
| cons(sk9,nil) = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f211,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f215,plain,
! [X0] : ssItem(skaf83(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f216,plain,
! [X0] : ssList(skaf82(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f254,plain,
! [X0,X1] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f263,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f274,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f278,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f279,plain,
! [X0] :
( nil = X0
| ssList(tl(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f289,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f290,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f301,plain,
! [X0,X1] :
( hd(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f302,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f98]) ).
fof(f303,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f308,plain,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f310,plain,
! [X0] :
( nil = X0
| cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f315,plain,
! [X0] :
( nil = X0
| cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f337,plain,
! [X0,X1] :
( hd(app(X1,X0)) = hd(X1)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f345,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f355,plain,
! [X0,X1,X2] :
( frontsegP(app(X0,X2),X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f356,plain,
! [X0,X1,X2] :
( memberP(cons(X1,X2),X0)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f358,plain,
! [X0,X1,X2] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f359,plain,
! [X0,X1,X2] :
( memberP(app(X2,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f363,plain,
! [U,W] :
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != W ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f364,plain,
! [X0,X1,X2] :
( frontsegP(X2,X0)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != X2 ),
inference(cnf_transformation,[status(thm)],[f363]) ).
fof(f372,plain,
! [X0,X1,X2] :
( app(app(X2,X1),X0) = app(X2,app(X1,X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f375,plain,
! [U,W] :
( U = W
| ~ ssList(W)
| ! [V] :
( ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f376,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f394,plain,
! [U,W] :
( W = U
| ! [V] :
( memberP(V,W)
| ~ ssItem(W)
| ~ ssItem(U)
| ~ ssList(V)
| ~ memberP(cons(U,V),W) ) ),
inference(miniscoping,[status(thm)],[f161]) ).
fof(f395,plain,
! [X0,X1,X2] :
( X2 = X0
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(cnf_transformation,[status(thm)],[f394]) ).
fof(f406,plain,
! [V,X] :
( X = V
| ~ ssList(V)
| ~ ssList(X)
| ! [U] :
( ~ ssItem(U)
| ! [W] :
( ~ ssItem(W)
| cons(U,V) != cons(W,X) ) ) ),
inference(miniscoping,[status(thm)],[f171]) ).
fof(f407,plain,
! [X0,X1,X2,X3] :
( X3 = X1
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssItem(X0)
| ~ ssItem(X2)
| cons(X0,X1) != cons(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f406]) ).
fof(f419,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(f434,plain,
ssList(sk1),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f439,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f440,plain,
ssItem(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f441,plain,
ssItem(sk6),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f442,plain,
ssList(sk7),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f443,plain,
ssList(sk8),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f444,plain,
app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = sk1,
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f445,plain,
~ neq(sk5,sk6),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f447,plain,
( nil = sk3
| ssItem(sk9) ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f450,plain,
( nil = sk3
| cons(sk9,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f459,definition,
( sQ2_spl
<=> ssItem(sk9) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f466,definition,
( sQ4_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( ~ sQ4_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,plain,
( sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f447,f459,f466]) ).
fof(f470,definition,
( sQ5_spl
<=> cons(sk9,nil) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( ~ sQ5_spl
| cons(sk9,nil) = sk3 ),
inference(component_clause,[status(thm)],[f470]) ).
fof(f478,plain,
( sQ4_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f450,f470,f466]) ).
fof(f492,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f356]) ).
fof(f493,plain,
! [X0,X1] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f492]) ).
fof(f495,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f364]) ).
fof(f500,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)],[f419]) ).
fof(f501,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)],[f500]) ).
fof(f510,plain,
( ssList(sk1)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(sk8) ),
inference(paramodulation,[status(thm)],[f444,f289]) ).
fof(f511,definition,
( sQ7_spl
<=> ssList(sk8) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f513,plain,
( sQ7_spl
| ~ ssList(sk8) ),
inference(component_clause,[status(thm)],[f511]) ).
fof(f514,definition,
( sQ8_spl
<=> ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f515,plain,
( ~ sQ8_spl
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(component_clause,[status(thm)],[f514]) ).
fof(f516,plain,
( sQ8_spl
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(component_clause,[status(thm)],[f514]) ).
fof(f517,definition,
( sQ9_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f520,plain,
( sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f510,f511,f514,f517]) ).
fof(f524,plain,
( ~ sQ4_spl
| app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = nil ),
inference(backward_demodulation,[status(thm)],[f526,f444]) ).
fof(f526,plain,
( ~ sQ4_spl
| nil = sk1 ),
inference(forward_demodulation,[status(thm)],[f439,f467]) ).
fof(f543,definition,
( sQ12_spl
<=> sk5 = sk6 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f544,plain,
( ~ sQ12_spl
| sk5 = sk6 ),
inference(component_clause,[status(thm)],[f543]) ).
fof(f547,plain,
( sk5 = sk6
| ~ ssItem(sk5)
| ~ ssItem(sk6) ),
inference(resolution,[status(thm)],[f308,f445]) ).
fof(f550,definition,
( sQ13_spl
<=> ssItem(sk6) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f552,plain,
( sQ13_spl
| ~ ssItem(sk6) ),
inference(component_clause,[status(thm)],[f550]) ).
fof(f553,definition,
( sQ14_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( sQ14_spl
| ~ ssItem(sk5) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f556,plain,
( sQ12_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f547,f550,f553,f543]) ).
fof(f557,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f555,f440]) ).
fof(f558,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f557]) ).
fof(f559,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f552,f441]) ).
fof(f560,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f559]) ).
fof(f563,definition,
( sQ15_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f565,plain,
( sQ15_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f563]) ).
fof(f571,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f565,f211]) ).
fof(f572,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f571]) ).
fof(f593,plain,
( ~ sQ4_spl
| ~ sQ12_spl
| app(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),sk8) = nil ),
inference(backward_demodulation,[status(thm)],[f544,f524]) ).
fof(f608,definition,
( sQ20_spl
<=> ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f610,plain,
( sQ20_spl
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f608]) ).
fof(f619,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f513,f443]) ).
fof(f620,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f619]) ).
fof(f621,plain,
( sQ8_spl
| ~ sQ12_spl
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
inference(forward_demodulation,[status(thm)],[f544,f516]) ).
fof(f679,plain,
( sQ8_spl
| ~ sQ12_spl
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[f621,f289]) ).
fof(f680,definition,
( sQ31_spl
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f682,plain,
( sQ31_spl
| ~ ssList(cons(sk5,nil)) ),
inference(component_clause,[status(thm)],[f680]) ).
fof(f683,definition,
( sQ32_spl
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f685,plain,
( sQ32_spl
| ~ ssList(app(sk7,cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f683]) ).
fof(f686,plain,
( sQ8_spl
| ~ sQ12_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f679,f680,f683,f543,f514]) ).
fof(f687,plain,
( sQ31_spl
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f682,f290]) ).
fof(f688,plain,
( sQ31_spl
| ~ sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f687,f553,f563,f680]) ).
fof(f689,plain,
( ~ sQ12_spl
| app(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),sk8) = sk1 ),
inference(forward_demodulation,[status(thm)],[f544,f444]) ).
fof(f690,plain,
( ~ sQ8_spl
| ~ sQ12_spl
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
inference(forward_demodulation,[status(thm)],[f544,f515]) ).
fof(f691,plain,
( ~ sQ12_spl
| sk1 = app(app(sk7,cons(sk5,nil)),app(cons(sk5,nil),sk8))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk8) ),
inference(paramodulation,[status(thm)],[f689,f372]) ).
fof(f699,plain,
! [X0] :
( ~ sQ12_spl
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssList(sk8)
| ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0) ),
inference(paramodulation,[status(thm)],[f689,f358]) ).
fof(f703,definition,
( sQ33_spl
<=> sk1 = app(app(sk7,cons(sk5,nil)),app(cons(sk5,nil),sk8)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f704,plain,
( ~ sQ33_spl
| sk1 = app(app(sk7,cons(sk5,nil)),app(cons(sk5,nil),sk8)) ),
inference(component_clause,[status(thm)],[f703]) ).
fof(f706,plain,
( ~ sQ12_spl
| sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f691,f511,f680,f683,f703,f543]) ).
fof(f729,definition,
! [X0] :
( sQ39_spl
<=> ( memberP(sk1,X0)
| ~ ssItem(X0)
| ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f730,plain,
! [X0] :
( ~ sQ39_spl
| memberP(sk1,X0)
| ~ ssItem(X0)
| ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0) ),
inference(component_clause,[status(thm)],[f729]) ).
fof(f732,plain,
( ~ sQ12_spl
| ~ sQ20_spl
| ~ sQ7_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f699,f729,f511,f608,f543]) ).
fof(f733,definition,
( sQ40_spl
<=> sk1 = nil ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f739,plain,
( sQ20_spl
| ~ sQ8_spl
| ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f610,f690]) ).
fof(f740,plain,
( sQ20_spl
| ~ sQ8_spl
| ~ sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f739]) ).
fof(f770,plain,
! [X0] :
( ~ sQ39_spl
| ~ ssItem(X0)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f730,f359]) ).
fof(f772,definition,
! [X0] :
( sQ46_spl
<=> ( ~ ssItem(X0)
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f773,plain,
! [X0] :
( ~ sQ46_spl
| ~ ssItem(X0)
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f772]) ).
fof(f775,plain,
( ~ sQ39_spl
| ~ sQ32_spl
| ~ sQ31_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f770,f772,f680,f683,f729]) ).
fof(f788,plain,
( ~ sQ5_spl
| cons(sk9,nil) = sk1 ),
inference(backward_demodulation,[status(thm)],[f439,f471]) ).
fof(f939,plain,
( sQ32_spl
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[f685,f289]) ).
fof(f940,definition,
( sQ61_spl
<=> ssList(sk7) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f942,plain,
( sQ61_spl
| ~ ssList(sk7) ),
inference(component_clause,[status(thm)],[f940]) ).
fof(f943,plain,
( sQ32_spl
| ~ sQ61_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f939,f680,f940,f683]) ).
fof(f944,plain,
( sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f942,f442]) ).
fof(f945,plain,
sQ61_spl,
inference(contradiction_clause,[status(thm)],[f944]) ).
fof(f947,plain,
! [X0] :
( ~ sQ46_spl
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk1,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f773]) ).
fof(f954,plain,
( ~ sQ46_spl
| ~ ssItem(sk5)
| ~ ssList(nil)
| memberP(sk1,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f947,f493]) ).
fof(f959,definition,
( sQ63_spl
<=> memberP(sk1,sk5) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f960,plain,
( ~ sQ63_spl
| memberP(sk1,sk5) ),
inference(component_clause,[status(thm)],[f959]) ).
fof(f962,plain,
( ~ sQ46_spl
| ~ sQ15_spl
| sQ63_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f954,f553,f959,f563,f772]) ).
fof(f1064,plain,
( ~ sQ5_spl
| hd(sk1) = sk9
| ~ ssList(nil)
| ~ ssItem(sk9) ),
inference(paramodulation,[status(thm)],[f788,f301]) ).
fof(f1071,plain,
! [X0] :
( ~ sQ5_spl
| X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk9)
| ~ ssList(nil)
| ~ memberP(sk1,X0) ),
inference(paramodulation,[status(thm)],[f788,f395]) ).
fof(f1102,definition,
( sQ74_spl
<=> hd(sk1) = sk9 ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1103,plain,
( ~ sQ74_spl
| hd(sk1) = sk9 ),
inference(component_clause,[status(thm)],[f1102]) ).
fof(f1105,plain,
( ~ sQ5_spl
| sQ74_spl
| ~ sQ15_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1064,f459,f563,f1102,f470]) ).
fof(f1124,definition,
! [X0] :
( sQ79_spl
<=> ( X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1125,plain,
! [X0] :
( ~ sQ79_spl
| X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(component_clause,[status(thm)],[f1124]) ).
fof(f1127,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ15_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1071,f1124,f563,f459,f470]) ).
fof(f1141,plain,
! [X0] :
( ~ sQ79_spl
| X0 = sk9
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1125,f274]) ).
fof(f1167,plain,
( ~ sQ63_spl
| ~ sQ79_spl
| sk5 = sk9
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1141,f960]) ).
fof(f1169,definition,
( sQ82_spl
<=> sk5 = sk9 ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1170,plain,
( ~ sQ82_spl
| sk5 = sk9 ),
inference(component_clause,[status(thm)],[f1169]) ).
fof(f1172,plain,
( ~ sQ63_spl
| ~ sQ79_spl
| sQ82_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1167,f553,f1169,f1124,f959]) ).
fof(f1386,plain,
( ~ sQ74_spl
| ~ sQ82_spl
| hd(sk1) = sk5 ),
inference(backward_demodulation,[status(thm)],[f1170,f1103]) ).
fof(f1387,plain,
( ~ sQ5_spl
| ~ sQ82_spl
| cons(sk5,nil) = sk1 ),
inference(backward_demodulation,[status(thm)],[f1170,f788]) ).
fof(f1412,plain,
( ~ sQ12_spl
| ~ sQ5_spl
| ~ sQ82_spl
| app(app(app(sk7,cons(sk5,nil)),sk1),sk8) = sk1 ),
inference(backward_demodulation,[status(thm)],[f1387,f689]) ).
fof(f1428,plain,
( ~ sQ5_spl
| ~ sQ82_spl
| ~ ssList(nil)
| ~ ssItem(sk5)
| sk1 != nil ),
inference(paramodulation,[status(thm)],[f1387,f303]) ).
fof(f1434,plain,
( ~ sQ12_spl
| ~ sQ5_spl
| ~ sQ82_spl
| app(app(app(sk7,sk1),sk1),sk8) = sk1 ),
inference(forward_demodulation,[status(thm)],[f1387,f1412]) ).
fof(f1460,plain,
( ~ sQ5_spl
| ~ sQ82_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f1428,f733,f553,f563,f1169,f470]) ).
fof(f1477,definition,
( sQ96_spl
<=> ssList(app(sk7,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1479,plain,
( sQ96_spl
| ~ ssList(app(sk7,sk1)) ),
inference(component_clause,[status(thm)],[f1477]) ).
fof(f1593,plain,
( ~ sQ33_spl
| ~ sQ5_spl
| ~ sQ82_spl
| sk1 = app(app(sk7,sk1),app(cons(sk5,nil),sk8)) ),
inference(forward_demodulation,[status(thm)],[f1387,f704]) ).
fof(f1594,plain,
( ~ sQ33_spl
| ~ sQ5_spl
| ~ sQ82_spl
| sk1 = app(app(sk7,sk1),app(sk1,sk8)) ),
inference(forward_demodulation,[status(thm)],[f1387,f1593]) ).
fof(f1595,plain,
( ~ sQ33_spl
| ~ sQ5_spl
| ~ sQ82_spl
| sk1 = app(sk7,app(sk1,app(sk1,sk8)))
| ~ ssList(sk7)
| ~ ssList(sk1)
| ~ ssList(app(sk1,sk8)) ),
inference(paramodulation,[status(thm)],[f1594,f372]) ).
fof(f1608,definition,
( sQ112_spl
<=> ssList(app(sk1,sk8)) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1610,plain,
( sQ112_spl
| ~ ssList(app(sk1,sk8)) ),
inference(component_clause,[status(thm)],[f1608]) ).
fof(f1611,definition,
( sQ113_spl
<=> sk1 = app(sk7,app(sk1,app(sk1,sk8))) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1612,plain,
( ~ sQ113_spl
| sk1 = app(sk7,app(sk1,app(sk1,sk8))) ),
inference(component_clause,[status(thm)],[f1611]) ).
fof(f1614,plain,
( ~ sQ33_spl
| ~ sQ5_spl
| ~ sQ82_spl
| sQ113_spl
| ~ sQ61_spl
| ~ sQ9_spl
| ~ sQ112_spl ),
inference(split_clause,[status(thm)],[f1595,f1608,f517,f940,f1611,f1169,f470,f703]) ).
fof(f1653,plain,
( sQ112_spl
| ~ ssList(sk1)
| ~ ssList(sk8) ),
inference(resolution,[status(thm)],[f1610,f289]) ).
fof(f1654,plain,
( sQ112_spl
| ~ sQ9_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1653,f511,f517,f1608]) ).
fof(f1682,definition,
( sQ124_spl
<=> ssList(app(sk1,app(sk1,sk8))) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1684,plain,
( sQ124_spl
| ~ ssList(app(sk1,app(sk1,sk8))) ),
inference(component_clause,[status(thm)],[f1682]) ).
fof(f1716,definition,
( sQ132_spl
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1717,plain,
( ~ sQ132_spl
| nil = sk7 ),
inference(component_clause,[status(thm)],[f1716]) ).
fof(f1721,plain,
( sQ124_spl
| ~ ssList(sk1)
| ~ ssList(app(sk1,sk8)) ),
inference(resolution,[status(thm)],[f1684,f289]) ).
fof(f1722,plain,
( sQ124_spl
| ~ sQ9_spl
| ~ sQ112_spl ),
inference(split_clause,[status(thm)],[f1721,f1608,f517,f1682]) ).
fof(f1825,definition,
( sQ145_spl
<=> app(sk7,sk1) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1826,plain,
( ~ sQ145_spl
| app(sk7,sk1) = sk1 ),
inference(component_clause,[status(thm)],[f1825]) ).
fof(f2083,plain,
! [X0,X1] :
( X1 = skaf82(cons(X0,X1))
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssItem(X0)
| nil = cons(X0,X1)
| ~ ssList(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f315,f407]) ).
fof(f2102,plain,
! [X0,X1] :
( X1 = skaf82(cons(X0,X1))
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssItem(X0)
| nil = cons(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2083,f290]) ).
fof(f2151,plain,
! [X0,X1] :
( X1 = skaf82(cons(X0,X1))
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2102,f303]) ).
fof(f2152,plain,
! [X0,X1] :
( X1 = skaf82(cons(X0,X1))
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f2151,f215]) ).
fof(f2154,plain,
! [X0,X1] :
( X1 = skaf82(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2152,f216]) ).
fof(f2182,plain,
( ~ sQ113_spl
| hd(sk1) = hd(sk7)
| nil = sk7
| ~ ssList(sk7)
| ~ ssList(app(sk1,app(sk1,sk8))) ),
inference(paramodulation,[status(thm)],[f1612,f337]) ).
fof(f2185,definition,
( sQ178_spl
<=> hd(sk1) = hd(sk7) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f2186,plain,
( ~ sQ178_spl
| hd(sk1) = hd(sk7) ),
inference(component_clause,[status(thm)],[f2185]) ).
fof(f2188,plain,
( ~ sQ113_spl
| sQ178_spl
| sQ132_spl
| ~ sQ61_spl
| ~ sQ124_spl ),
inference(split_clause,[status(thm)],[f2182,f1682,f940,f1716,f2185,f1611]) ).
fof(f2223,plain,
( ~ sQ12_spl
| ~ sQ5_spl
| ~ sQ82_spl
| ~ sQ132_spl
| app(app(app(nil,sk1),sk1),sk8) = sk1 ),
inference(backward_demodulation,[status(thm)],[f1717,f1434]) ).
fof(f2307,plain,
( ~ sQ178_spl
| ~ sQ74_spl
| ~ sQ82_spl
| sk5 = hd(sk7) ),
inference(forward_demodulation,[status(thm)],[f1386,f2186]) ).
fof(f2309,plain,
( ~ sQ178_spl
| ~ sQ74_spl
| ~ sQ82_spl
| nil = sk7
| cons(sk5,tl(sk7)) = sk7
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f2307,f310]) ).
fof(f2311,definition,
( sQ192_spl
<=> cons(sk5,tl(sk7)) = sk7 ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f2312,plain,
( ~ sQ192_spl
| cons(sk5,tl(sk7)) = sk7 ),
inference(component_clause,[status(thm)],[f2311]) ).
fof(f2314,plain,
( ~ sQ178_spl
| ~ sQ74_spl
| ~ sQ82_spl
| sQ132_spl
| sQ192_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f2309,f940,f2311,f1716,f1169,f1102,f2185]) ).
fof(f2465,definition,
( sQ195_spl
<=> memberP(nil,sk5) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f2466,plain,
( ~ sQ195_spl
| memberP(nil,sk5) ),
inference(component_clause,[status(thm)],[f2465]) ).
fof(f2558,plain,
( ~ sQ192_spl
| tl(sk7) = skaf82(sk7)
| ~ ssList(tl(sk7))
| ~ ssItem(sk5) ),
inference(paramodulation,[status(thm)],[f2312,f2154]) ).
fof(f2582,definition,
( sQ204_spl
<=> ssList(tl(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f2584,plain,
( sQ204_spl
| ~ ssList(tl(sk7)) ),
inference(component_clause,[status(thm)],[f2582]) ).
fof(f2599,definition,
( sQ209_spl
<=> tl(sk7) = skaf82(sk7) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f2600,plain,
( ~ sQ209_spl
| tl(sk7) = skaf82(sk7) ),
inference(component_clause,[status(thm)],[f2599]) ).
fof(f2602,plain,
( ~ sQ192_spl
| sQ209_spl
| ~ sQ204_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f2558,f553,f2582,f2599,f2311]) ).
fof(f2687,plain,
( sQ204_spl
| nil = sk7
| ~ ssList(sk7) ),
inference(resolution,[status(thm)],[f2584,f279]) ).
fof(f2688,plain,
( sQ204_spl
| sQ132_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f2687,f940,f1716,f2582]) ).
fof(f2749,plain,
( ~ sQ209_spl
| nil = sk7
| cons(hd(sk7),skaf82(sk7)) = sk7
| ~ ssList(sk7) ),
inference(paramodulation,[status(thm)],[f2600,f310]) ).
fof(f2751,definition,
( sQ230_spl
<=> cons(hd(sk7),skaf82(sk7)) = sk7 ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f2752,plain,
( ~ sQ230_spl
| cons(hd(sk7),skaf82(sk7)) = sk7 ),
inference(component_clause,[status(thm)],[f2751]) ).
fof(f2754,plain,
( ~ sQ209_spl
| sQ132_spl
| sQ230_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f2749,f940,f2751,f1716,f2599]) ).
fof(f2755,definition,
( sQ231_spl
<=> ssList(skaf82(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f2757,plain,
( sQ231_spl
| ~ ssList(skaf82(sk7)) ),
inference(component_clause,[status(thm)],[f2755]) ).
fof(f2759,plain,
( ~ sQ230_spl
| ~ sQ178_spl
| ~ sQ74_spl
| ~ sQ82_spl
| cons(sk5,skaf82(sk7)) = sk7 ),
inference(forward_demodulation,[status(thm)],[f2307,f2752]) ).
fof(f3486,plain,
( ~ sQ195_spl
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f274,f2466]) ).
fof(f3487,plain,
( ~ sQ195_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f3486,f553,f2465]) ).
fof(f3527,definition,
( sQ282_spl
<=> frontsegP(sk1,app(sk7,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f3528,plain,
( ~ sQ282_spl
| frontsegP(sk1,app(sk7,sk1)) ),
inference(component_clause,[status(thm)],[f3527]) ).
fof(f3549,plain,
! [X0,X1] :
( frontsegP(app(X1,X0),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f495,f289]) ).
fof(f4309,definition,
( sQ349_spl
<=> ssList(app(sk1,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition]) ).
fof(f4311,plain,
( sQ349_spl
| ~ ssList(app(sk1,sk1)) ),
inference(component_clause,[status(thm)],[f4309]) ).
fof(f4355,plain,
( ~ sQ33_spl
| ~ sQ5_spl
| ~ sQ82_spl
| frontsegP(sk1,app(sk7,sk1))
| ~ ssList(app(sk7,sk1))
| ~ ssList(app(sk1,sk8)) ),
inference(paramodulation,[status(thm)],[f1594,f3549]) ).
fof(f4360,plain,
( ~ sQ33_spl
| ~ sQ5_spl
| ~ sQ82_spl
| sQ282_spl
| ~ sQ96_spl
| ~ sQ112_spl ),
inference(split_clause,[status(thm)],[f4355,f1608,f1477,f3527,f1169,f470,f703]) ).
fof(f4453,plain,
( sQ349_spl
| ~ ssList(sk1)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f4311,f289]) ).
fof(f4454,plain,
( sQ349_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f4453,f517,f4309]) ).
fof(f4474,plain,
( sQ231_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2757,f216]) ).
fof(f4475,plain,
sQ231_spl,
inference(contradiction_clause,[status(thm)],[f4474]) ).
fof(f4560,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ82_spl
| frontsegP(cons(sk5,X0),sk1)
| ~ ssItem(sk5)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(X0,nil) ),
inference(paramodulation,[status(thm)],[f1387,f501]) ).
fof(f4579,definition,
! [X0] :
( sQ376_spl
<=> ( frontsegP(cons(sk5,X0),sk1)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ376_spl])],[split_symbol_definition]) ).
fof(f4580,plain,
! [X0] :
( ~ sQ376_spl
| frontsegP(cons(sk5,X0),sk1)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ),
inference(component_clause,[status(thm)],[f4579]) ).
fof(f4582,plain,
( ~ sQ5_spl
| ~ sQ82_spl
| ~ sQ14_spl
| ~ sQ15_spl
| sQ376_spl ),
inference(split_clause,[status(thm)],[f4560,f4579,f563,f553,f1169,f470]) ).
fof(f4583,plain,
! [X0] :
( ~ sQ376_spl
| frontsegP(cons(sk5,X0),sk1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4580,f263]) ).
fof(f5403,plain,
( sQ96_spl
| ~ ssList(sk7)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f1479,f289]) ).
fof(f5404,plain,
( sQ96_spl
| ~ sQ61_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f5403,f517,f940,f1477]) ).
fof(f5476,plain,
( ~ sQ63_spl
| ~ sQ4_spl
| ~ sQ12_spl
| memberP(nil,sk5) ),
inference(backward_demodulation,[status(thm)],[f5478,f960]) ).
fof(f5478,plain,
( ~ sQ4_spl
| ~ sQ12_spl
| sk1 = nil ),
inference(forward_demodulation,[status(thm)],[f689,f593]) ).
fof(f5494,plain,
( ~ sQ63_spl
| ~ sQ4_spl
| ~ sQ12_spl
| sQ195_spl ),
inference(split_clause,[status(thm)],[f5476,f2465,f543,f466,f959]) ).
fof(f6151,definition,
( sQ463_spl
<=> sk1 = app(nil,sk1) ),
introduced(definition,[new_symbols(definition,[sQ463_spl])],[split_symbol_definition]) ).
fof(f6152,plain,
( ~ sQ463_spl
| sk1 = app(nil,sk1) ),
inference(component_clause,[status(thm)],[f6151]) ).
fof(f6153,plain,
( sQ463_spl
| sk1 != app(nil,sk1) ),
inference(component_clause,[status(thm)],[f6151]) ).
fof(f6378,plain,
( ~ sQ12_spl
| ~ sQ5_spl
| ~ sQ82_spl
| ~ sQ132_spl
| ~ sQ463_spl
| app(app(sk1,sk1),sk8) = sk1 ),
inference(backward_demodulation,[status(thm)],[f6152,f2223]) ).
fof(f6399,plain,
! [X0] :
( ~ sQ463_spl
| X0 = nil
| ~ ssList(nil)
| ~ ssList(sk1)
| ~ ssList(X0)
| app(X0,sk1) != sk1 ),
inference(paramodulation,[status(thm)],[f6152,f376]) ).
fof(f6436,definition,
! [X0] :
( sQ490_spl
<=> ( X0 = nil
| ~ ssList(X0)
| app(X0,sk1) != sk1 ) ),
introduced(definition,[new_symbols(definition,[sQ490_spl])],[split_symbol_definition]) ).
fof(f6437,plain,
! [X0] :
( ~ sQ490_spl
| X0 = nil
| ~ ssList(X0)
| app(X0,sk1) != sk1 ),
inference(component_clause,[status(thm)],[f6436]) ).
fof(f6439,plain,
( ~ sQ463_spl
| ~ sQ15_spl
| ~ sQ9_spl
| sQ490_spl ),
inference(split_clause,[status(thm)],[f6399,f6436,f517,f563,f6151]) ).
fof(f6463,plain,
( ~ sQ12_spl
| ~ sQ5_spl
| ~ sQ82_spl
| ~ sQ132_spl
| ~ sQ463_spl
| frontsegP(sk1,app(sk1,sk1))
| ~ ssList(app(sk1,sk1))
| ~ ssList(sk8) ),
inference(paramodulation,[status(thm)],[f6378,f3549]) ).
fof(f6507,definition,
( sQ500_spl
<=> frontsegP(sk1,app(sk1,sk1)) ),
introduced(definition,[new_symbols(definition,[sQ500_spl])],[split_symbol_definition]) ).
fof(f6508,plain,
( ~ sQ500_spl
| frontsegP(sk1,app(sk1,sk1)) ),
inference(component_clause,[status(thm)],[f6507]) ).
fof(f6510,plain,
( ~ sQ12_spl
| ~ sQ5_spl
| ~ sQ82_spl
| ~ sQ132_spl
| ~ sQ463_spl
| sQ500_spl
| ~ sQ349_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f6463,f511,f4309,f6507,f6151,f1716,f1169,f470,f543]) ).
fof(f6559,plain,
( sQ463_spl
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f6153,f278]) ).
fof(f6560,plain,
( sQ463_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6559,f434]) ).
fof(f6561,plain,
sQ463_spl,
inference(contradiction_clause,[status(thm)],[f6560]) ).
fof(f6786,plain,
( ~ sQ500_spl
| sk1 = app(sk1,sk1)
| ~ ssList(sk1)
| ~ ssList(app(sk1,sk1))
| ~ frontsegP(app(sk1,sk1),sk1) ),
inference(resolution,[status(thm)],[f6508,f345]) ).
fof(f6787,definition,
( sQ514_spl
<=> frontsegP(app(sk1,sk1),sk1) ),
introduced(definition,[new_symbols(definition,[sQ514_spl])],[split_symbol_definition]) ).
fof(f6789,plain,
( sQ514_spl
| ~ frontsegP(app(sk1,sk1),sk1) ),
inference(component_clause,[status(thm)],[f6787]) ).
fof(f6790,definition,
( sQ515_spl
<=> sk1 = app(sk1,sk1) ),
introduced(definition,[new_symbols(definition,[sQ515_spl])],[split_symbol_definition]) ).
fof(f6791,plain,
( ~ sQ515_spl
| sk1 = app(sk1,sk1) ),
inference(component_clause,[status(thm)],[f6790]) ).
fof(f6793,plain,
( ~ sQ500_spl
| sQ515_spl
| ~ sQ9_spl
| ~ sQ349_spl
| ~ sQ514_spl ),
inference(split_clause,[status(thm)],[f6786,f6787,f4309,f517,f6790,f6507]) ).
fof(f6795,plain,
( sQ514_spl
| ~ ssList(sk1)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f6789,f3549]) ).
fof(f6797,plain,
( sQ514_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f6795,f517,f6787]) ).
fof(f6806,plain,
( ~ sQ490_spl
| ~ sQ515_spl
| sk1 = nil
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f6791,f6437]) ).
fof(f6829,plain,
( ~ sQ490_spl
| ~ sQ515_spl
| sQ40_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f6806,f517,f733,f6790,f6436]) ).
fof(f7053,definition,
( sQ526_spl
<=> ssList(skaf45(sk1,nil)) ),
introduced(definition,[new_symbols(definition,[sQ526_spl])],[split_symbol_definition]) ).
fof(f7055,plain,
( sQ526_spl
| ~ ssList(skaf45(sk1,nil)) ),
inference(component_clause,[status(thm)],[f7053]) ).
fof(f7065,plain,
( sQ526_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7055,f254]) ).
fof(f7066,plain,
sQ526_spl,
inference(contradiction_clause,[status(thm)],[f7065]) ).
fof(f7257,plain,
( ~ sQ282_spl
| sk1 = app(sk7,sk1)
| ~ ssList(sk1)
| ~ ssList(app(sk7,sk1))
| ~ frontsegP(app(sk7,sk1),sk1) ),
inference(resolution,[status(thm)],[f3528,f345]) ).
fof(f7258,definition,
( sQ541_spl
<=> frontsegP(app(sk7,sk1),sk1) ),
introduced(definition,[new_symbols(definition,[sQ541_spl])],[split_symbol_definition]) ).
fof(f7260,plain,
( sQ541_spl
| ~ frontsegP(app(sk7,sk1),sk1) ),
inference(component_clause,[status(thm)],[f7258]) ).
fof(f7261,plain,
( ~ sQ282_spl
| sQ145_spl
| ~ sQ9_spl
| ~ sQ96_spl
| ~ sQ541_spl ),
inference(split_clause,[status(thm)],[f7257,f7258,f1477,f517,f1825,f3527]) ).
fof(f7265,plain,
( sQ541_spl
| ~ ssList(sk7)
| ~ ssList(sk1)
| ~ ssList(sk1)
| ~ frontsegP(sk7,sk1) ),
inference(resolution,[status(thm)],[f7260,f355]) ).
fof(f7266,definition,
( sQ542_spl
<=> frontsegP(sk7,sk1) ),
introduced(definition,[new_symbols(definition,[sQ542_spl])],[split_symbol_definition]) ).
fof(f7269,plain,
( sQ541_spl
| ~ sQ61_spl
| ~ sQ9_spl
| ~ sQ542_spl ),
inference(split_clause,[status(thm)],[f7265,f7266,f517,f940,f7258]) ).
fof(f7346,plain,
( ~ sQ490_spl
| ~ sQ145_spl
| sk7 = nil
| ~ ssList(sk7) ),
inference(resolution,[status(thm)],[f1826,f6437]) ).
fof(f7368,plain,
( ~ sQ490_spl
| ~ sQ145_spl
| sQ132_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f7346,f940,f1716,f1825,f6436]) ).
fof(f7805,plain,
( ~ sQ230_spl
| ~ sQ178_spl
| ~ sQ74_spl
| ~ sQ82_spl
| ~ sQ376_spl
| frontsegP(sk7,sk1)
| ~ ssList(skaf82(sk7)) ),
inference(paramodulation,[status(thm)],[f2759,f4583]) ).
fof(f7816,plain,
( ~ sQ230_spl
| ~ sQ178_spl
| ~ sQ74_spl
| ~ sQ82_spl
| ~ sQ376_spl
| sQ542_spl
| ~ sQ231_spl ),
inference(split_clause,[status(thm)],[f7805,f2755,f7266,f4579,f1169,f1102,f2185,f2751]) ).
fof(f7818,plain,
$false,
inference(sat_refutation,[status(thm)],[f469,f478,f520,f556,f558,f560,f572,f620,f686,f688,f706,f732,f740,f775,f943,f945,f962,f1105,f1127,f1172,f1460,f1614,f1654,f1722,f2188,f2314,f2602,f2688,f2754,f3487,f4360,f4454,f4475,f4582,f5404,f5494,f6439,f6510,f6561,f6793,f6797,f6829,f7066,f7261,f7269,f7368,f7816]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC169-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.38 % Computer : n007.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Mon Sep 21 07:59:21 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 25.04/3.65 % Refutation found
% 25.04/3.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 25.04/3.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.03/3.72 % Elapsed time: 3.323987 seconds
% 4.03/3.72 % CPU time: 25.582852 seconds
% 4.03/3.72 % Total memory used: 256.400 MB
% 4.03/3.72 % Net memory used: 245.437 MB
%------------------------------------------------------------------------------