%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC396-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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:41:04 PM UTC 2026
% Result : Unsatisfiable 54.73s 12.46s
% Output : CNFRefutation 48.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 76
% Syntax : Number of formulae : 275 ( 36 unt; 44 def)
% Number of atoms : 827 ( 171 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 1011 ( 459 ~; 508 |; 0 &)
% ( 44 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 50 ( 48 usr; 45 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-2 aty)
% Number of variables : 145 ( 145 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [U] : ssItem(skaf83(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [U] : ssList(skaf82(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [U,V] : ssList(skaf46(U,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [U,V] : ssList(skaf45(U,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,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(f86,axiom,
! [U,V] :
( ssList(cons(U,V))
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,axiom,
! [U,V] :
( tl(cons(U,V)) = V
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != nil ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [U,V] :
( V = U
| neq(V,U)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [U] :
( nil = U
| cons(hd(U),tl(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [U] :
( nil = U
| cons(skaf83(U),skaf82(U)) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [U,V] :
( nil = U
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
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(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(f138,axiom,
! [U,V,W] :
( memberP(cons(V,W),U)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssList(W)
| U != V ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f170,axiom,
! [U,V,W,X] :
( U = W
| ~ ssList(V)
| ~ ssList(X)
| ~ ssItem(U)
| ~ ssItem(W)
| cons(U,V) != cons(W,X) ),
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,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
memberP(sk1,sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
~ memberP(sk2,sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
( nil != sk4
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
! [A,B,C,D] :
( ~ neq(nil,sk3)
| ~ neq(nil,sk3)
| hd(sk3) != D
| cons(D,nil) != C
| ~ ssItem(D)
| app(B,C) != A
| tl(sk3) != B
| ~ ssList(C)
| ~ ssList(B)
| sk4 = A
| ~ ssList(A)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f205,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f209,plain,
! [X0] : ssItem(skaf83(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f210,plain,
! [X0] : ssList(skaf82(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f247,plain,
! [X0,X1] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f248,plain,
! [X0,X1] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(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(f294,plain,
! [X0,X1] :
( tl(cons(X0,X1)) = X1
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
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(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(f324,plain,
! [U] :
( nil = U
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f325,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f331,plain,
! [X0,X1] :
( hd(app(X1,X0)) = hd(X1)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
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(f350,plain,
! [X0,X1,X2] :
( memberP(cons(X1,X2),X0)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f352,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(f353,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(f388,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(f389,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)],[f388]) ).
fof(f398,plain,
! [U,W] :
( U = W
| ! [V] :
( ~ ssList(V)
| ! [X] :
( ~ ssList(X)
| ~ ssItem(U)
| ~ ssItem(W)
| cons(U,V) != cons(W,X) ) ) ),
inference(miniscoping,[status(thm)],[f170]) ).
fof(f399,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssItem(X0)
| ~ ssItem(X2)
| cons(X0,X1) != cons(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f398]) ).
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,
ssItem(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f435,plain,
memberP(sk1,sk5),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f436,plain,
~ memberP(sk2,sk5),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f437,plain,
( nil != sk4
| nil = sk3 ),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f439,plain,
( ~ neq(nil,sk3)
| ~ neq(nil,sk3)
| ! [D] :
( hd(sk3) != D
| ! [C] :
( cons(D,nil) != C
| ~ ssItem(D)
| ! [A,B] :
( app(B,C) != A
| tl(sk3) != B
| ~ ssList(C)
| ~ ssList(B)
| sk4 = A
| ~ ssList(A)
| ~ neq(sk4,nil) ) ) ) ),
inference(miniscoping,[status(thm)],[f197]) ).
fof(f440,plain,
! [X0,X1,X2,X3] :
( ~ neq(nil,sk3)
| ~ neq(nil,sk3)
| hd(sk3) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk3) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk4 = X0
| ~ ssList(X0)
| ~ neq(sk4,nil) ),
inference(cnf_transformation,[status(thm)],[f439]) ).
fof(f448,definition,
( sQ2_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( ~ sQ2_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f450,plain,
( sQ2_spl
| nil != sk3 ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f451,definition,
( sQ3_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f453,plain,
( sQ3_spl
| nil != sk4 ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f437,f448,f451]) ).
fof(f455,definition,
( sQ4_spl
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( sQ4_spl
| ~ neq(sk4,nil) ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f462,definition,
! [X0,X1,X2,X3] :
( sQ6_spl
<=> ( hd(sk3) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk3) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk4 = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f463,plain,
! [X0,X1,X2,X3] :
( ~ sQ6_spl
| hd(sk3) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk3) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk4 = X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,definition,
( sQ7_spl
<=> neq(nil,sk3) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( sQ7_spl
| ~ neq(nil,sk3) ),
inference(component_clause,[status(thm)],[f465]) ).
fof(f468,plain,
( ~ sQ7_spl
| sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f440,f455,f462,f465]) ).
fof(f481,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f350]) ).
fof(f482,plain,
! [X0,X1] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f481]) ).
fof(f499,plain,
( sQ4_spl
| ~ neq(sk2,nil) ),
inference(forward_demodulation,[status(thm)],[f432,f457]) ).
fof(f502,plain,
( ~ sQ2_spl
| memberP(nil,sk5) ),
inference(backward_demodulation,[status(thm)],[f504,f435]) ).
fof(f504,plain,
( ~ sQ2_spl
| nil = sk1 ),
inference(forward_demodulation,[status(thm)],[f433,f449]) ).
fof(f505,plain,
( ~ sQ2_spl
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f502,f268]) ).
fof(f506,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f505,f434]) ).
fof(f507,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f506]) ).
fof(f508,plain,
( sQ3_spl
| nil != sk2 ),
inference(forward_demodulation,[status(thm)],[f432,f453]) ).
fof(f509,plain,
( sQ4_spl
| sk2 = nil
| ~ ssList(sk2)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f300,f499]) ).
fof(f512,definition,
( sQ8_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f514,plain,
( sQ8_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f512]) ).
fof(f515,definition,
( sQ9_spl
<=> ssList(sk2) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f517,plain,
( sQ9_spl
| ~ ssList(sk2) ),
inference(component_clause,[status(thm)],[f515]) ).
fof(f518,definition,
( sQ10_spl
<=> sk2 = nil ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f519,plain,
( ~ sQ10_spl
| sk2 = nil ),
inference(component_clause,[status(thm)],[f518]) ).
fof(f521,plain,
( sQ4_spl
| sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f509,f512,f515,f518,f455]) ).
fof(f522,plain,
( ~ sQ10_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f519,f508]) ).
fof(f523,plain,
( ~ sQ10_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f522]) ).
fof(f524,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f514,f205]) ).
fof(f525,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f524]) ).
fof(f526,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f517,f429]) ).
fof(f527,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f526]) ).
fof(f528,plain,
! [X0,X1,X2,X3] :
( ~ sQ6_spl
| hd(sk3) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk3) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk2 = X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f432,f463]) ).
fof(f529,plain,
( ~ sQ6_spl
| ~ ssItem(hd(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(tl(sk3))
| sk2 = app(tl(sk3),cons(hd(sk3),nil))
| ~ ssList(app(tl(sk3),cons(hd(sk3),nil))) ),
inference(destructive_equality_resolution,[status(thm)],[f528]) ).
fof(f530,plain,
( ~ sQ6_spl
| ~ ssItem(hd(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(tl(sk3))
| sk2 = app(tl(sk3),cons(hd(sk3),nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[f529,f283]) ).
fof(f546,plain,
( sQ2_spl
| nil != sk1 ),
inference(forward_demodulation,[status(thm)],[f433,f450]) ).
fof(f547,plain,
( ~ sQ6_spl
| ~ ssItem(hd(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(tl(sk3))
| sk2 = app(tl(sk1),cons(hd(sk3),nil)) ),
inference(forward_demodulation,[status(thm)],[f433,f530]) ).
fof(f548,plain,
( ~ sQ6_spl
| ~ ssItem(hd(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(tl(sk3))
| sk2 = app(tl(sk1),cons(hd(sk1),nil)) ),
inference(forward_demodulation,[status(thm)],[f433,f547]) ).
fof(f549,plain,
( ~ sQ6_spl
| ~ ssItem(hd(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(tl(sk1))
| sk2 = app(tl(sk1),cons(hd(sk1),nil)) ),
inference(forward_demodulation,[status(thm)],[f433,f548]) ).
fof(f550,plain,
( ~ sQ6_spl
| ~ ssItem(hd(sk3))
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(tl(sk1))
| sk2 = app(tl(sk1),cons(hd(sk1),nil)) ),
inference(forward_demodulation,[status(thm)],[f433,f549]) ).
fof(f551,plain,
( ~ sQ6_spl
| ~ ssItem(hd(sk1))
| ~ ssList(cons(hd(sk1),nil))
| ~ ssList(tl(sk1))
| sk2 = app(tl(sk1),cons(hd(sk1),nil)) ),
inference(forward_demodulation,[status(thm)],[f433,f550]) ).
fof(f718,plain,
! [X0,X1] :
( skaf83(cons(X0,X1)) = X0
| ~ 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)],[f309,f399]) ).
fof(f723,plain,
! [X0,X1] :
( skaf83(cons(X0,X1)) = X0
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssItem(X0)
| nil = cons(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f718,f284]) ).
fof(f877,plain,
! [X0,X1] :
( skaf83(cons(X0,X1)) = X0
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(skaf83(cons(X0,X1)))
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f723,f297]) ).
fof(f878,plain,
! [X0,X1] :
( skaf83(cons(X0,X1)) = X0
| ~ ssList(skaf82(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f877,f209]) ).
fof(f879,plain,
! [X0,X1] :
( skaf83(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f878,f210]) ).
fof(f3033,definition,
( sQ144_spl
<=> sk2 = app(tl(sk1),cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f3034,plain,
( ~ sQ144_spl
| sk2 = app(tl(sk1),cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f3033]) ).
fof(f3036,definition,
( sQ145_spl
<=> ssList(tl(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f3038,plain,
( sQ145_spl
| ~ ssList(tl(sk1)) ),
inference(component_clause,[status(thm)],[f3036]) ).
fof(f3039,definition,
( sQ146_spl
<=> ssList(cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f3041,plain,
( sQ146_spl
| ~ ssList(cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f3039]) ).
fof(f3042,definition,
( sQ147_spl
<=> ssItem(hd(sk1)) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f3044,plain,
( sQ147_spl
| ~ ssItem(hd(sk1)) ),
inference(component_clause,[status(thm)],[f3042]) ).
fof(f3045,plain,
( ~ sQ6_spl
| ~ sQ147_spl
| ~ sQ146_spl
| ~ sQ145_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f551,f3033,f3036,f3039,f3042,f462]) ).
fof(f3046,plain,
( sQ7_spl
| ~ neq(nil,sk1) ),
inference(forward_demodulation,[status(thm)],[f433,f467]) ).
fof(f3047,plain,
( sQ7_spl
| nil = sk1
| ~ ssList(nil)
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f3046,f300]) ).
fof(f3048,definition,
( sQ148_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f3050,plain,
( sQ148_spl
| ~ ssList(sk1) ),
inference(component_clause,[status(thm)],[f3048]) ).
fof(f3051,definition,
( sQ149_spl
<=> nil = sk1 ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f3052,plain,
( ~ sQ149_spl
| nil = sk1 ),
inference(component_clause,[status(thm)],[f3051]) ).
fof(f3054,plain,
( sQ7_spl
| sQ149_spl
| ~ sQ8_spl
| ~ sQ148_spl ),
inference(split_clause,[status(thm)],[f3047,f3048,f512,f3051,f465]) ).
fof(f3055,plain,
( ~ sQ149_spl
| sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3052,f546]) ).
fof(f3056,plain,
( ~ sQ149_spl
| sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f3055]) ).
fof(f3057,plain,
( sQ148_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3050,f428]) ).
fof(f3058,plain,
sQ148_spl,
inference(contradiction_clause,[status(thm)],[f3057]) ).
fof(f3063,plain,
( sQ147_spl
| nil = sk1
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f274,f3044]) ).
fof(f3064,plain,
( sQ147_spl
| sQ149_spl
| ~ sQ148_spl ),
inference(split_clause,[status(thm)],[f3063,f3048,f3051,f3042]) ).
fof(f3097,plain,
( sQ146_spl
| ~ ssList(nil)
| ~ ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f284,f3041]) ).
fof(f3099,plain,
( sQ146_spl
| ~ sQ8_spl
| ~ sQ147_spl ),
inference(split_clause,[status(thm)],[f3097,f3042,f512,f3039]) ).
fof(f3101,plain,
( ~ sQ144_spl
| tl(app(sk1,cons(hd(sk1),nil))) = sk2
| nil = sk1
| ~ ssList(sk1)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f3034,f343]) ).
fof(f3140,definition,
( sQ150_spl
<=> tl(app(sk1,cons(hd(sk1),nil))) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f3141,plain,
( ~ sQ150_spl
| tl(app(sk1,cons(hd(sk1),nil))) = sk2 ),
inference(component_clause,[status(thm)],[f3140]) ).
fof(f3143,plain,
( ~ sQ144_spl
| sQ150_spl
| sQ149_spl
| ~ sQ148_spl
| ~ sQ146_spl ),
inference(split_clause,[status(thm)],[f3101,f3039,f3048,f3051,f3140,f3033]) ).
fof(f3290,definition,
( sQ188_spl
<=> nil = cons(hd(sk1),nil) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f3291,plain,
( ~ sQ188_spl
| nil = cons(hd(sk1),nil) ),
inference(component_clause,[status(thm)],[f3290]) ).
fof(f3296,plain,
( sQ145_spl
| nil = sk1
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f3038,f273]) ).
fof(f3297,plain,
( sQ145_spl
| sQ149_spl
| ~ sQ148_spl ),
inference(split_clause,[status(thm)],[f3296,f3048,f3051,f3036]) ).
fof(f3504,definition,
( sQ208_spl
<=> ssList(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f3506,plain,
( sQ208_spl
| ~ ssList(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f3504]) ).
fof(f3507,definition,
( sQ209_spl
<=> nil = app(sk1,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f3508,plain,
( ~ sQ209_spl
| nil = app(sk1,cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f3507]) ).
fof(f3588,plain,
! [X0] :
( ~ sQ144_spl
| memberP(sk2,X0)
| ~ ssItem(X0)
| ~ ssList(tl(sk1))
| ~ ssList(cons(hd(sk1),nil))
| ~ memberP(cons(hd(sk1),nil),X0) ),
inference(paramodulation,[status(thm)],[f3034,f353]) ).
fof(f3598,definition,
! [X0] :
( sQ219_spl
<=> ( memberP(sk2,X0)
| ~ ssItem(X0)
| ~ memberP(cons(hd(sk1),nil),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f3599,plain,
! [X0] :
( ~ sQ219_spl
| memberP(sk2,X0)
| ~ ssItem(X0)
| ~ memberP(cons(hd(sk1),nil),X0) ),
inference(component_clause,[status(thm)],[f3598]) ).
fof(f3601,plain,
( ~ sQ144_spl
| ~ sQ145_spl
| ~ sQ146_spl
| sQ219_spl ),
inference(split_clause,[status(thm)],[f3588,f3598,f3039,f3036,f3033]) ).
fof(f4041,definition,
( sQ269_spl
<=> memberP(sk1,sk5) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f4043,plain,
( sQ269_spl
| ~ memberP(sk1,sk5) ),
inference(component_clause,[status(thm)],[f4041]) ).
fof(f4044,definition,
( sQ270_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).
fof(f4046,plain,
( sQ270_spl
| ~ ssItem(sk5) ),
inference(component_clause,[status(thm)],[f4044]) ).
fof(f4049,plain,
( sQ269_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4043,f435]) ).
fof(f4050,plain,
sQ269_spl,
inference(contradiction_clause,[status(thm)],[f4049]) ).
fof(f5149,plain,
( ~ sQ209_spl
| nil = sk1
| ~ ssList(sk1)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(resolution,[status(thm)],[f3508,f325]) ).
fof(f5168,plain,
( ~ sQ209_spl
| sQ149_spl
| ~ sQ148_spl
| ~ sQ146_spl ),
inference(split_clause,[status(thm)],[f5149,f3039,f3048,f3051,f3507]) ).
fof(f5337,plain,
( sQ208_spl
| ~ ssList(sk1)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(resolution,[status(thm)],[f3506,f283]) ).
fof(f5338,plain,
( sQ208_spl
| ~ sQ148_spl
| ~ sQ146_spl ),
inference(split_clause,[status(thm)],[f5337,f3039,f3048,f3504]) ).
fof(f5356,plain,
( ~ sQ150_spl
| nil = app(sk1,cons(hd(sk1),nil))
| cons(hd(app(sk1,cons(hd(sk1),nil))),sk2) = app(sk1,cons(hd(sk1),nil))
| ~ ssList(app(sk1,cons(hd(sk1),nil))) ),
inference(paramodulation,[status(thm)],[f3141,f304]) ).
fof(f5359,definition,
( sQ381_spl
<=> cons(hd(app(sk1,cons(hd(sk1),nil))),sk2) = app(sk1,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ381_spl])],[split_symbol_definition]) ).
fof(f5360,plain,
( ~ sQ381_spl
| cons(hd(app(sk1,cons(hd(sk1),nil))),sk2) = app(sk1,cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f5359]) ).
fof(f5362,plain,
( ~ sQ150_spl
| sQ209_spl
| sQ381_spl
| ~ sQ208_spl ),
inference(split_clause,[status(thm)],[f5356,f3504,f5359,f3507,f3140]) ).
fof(f5551,plain,
( ~ sQ381_spl
| skaf83(app(sk1,cons(hd(sk1),nil))) = hd(app(sk1,cons(hd(sk1),nil)))
| ~ ssList(sk2)
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(paramodulation,[status(thm)],[f5360,f879]) ).
fof(f5565,definition,
( sQ397_spl
<=> ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
introduced(definition,[new_symbols(definition,[sQ397_spl])],[split_symbol_definition]) ).
fof(f5567,plain,
( sQ397_spl
| ~ ssItem(hd(app(sk1,cons(hd(sk1),nil)))) ),
inference(component_clause,[status(thm)],[f5565]) ).
fof(f5569,definition,
( sQ398_spl
<=> skaf83(app(sk1,cons(hd(sk1),nil))) = hd(app(sk1,cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ398_spl])],[split_symbol_definition]) ).
fof(f5570,plain,
( ~ sQ398_spl
| skaf83(app(sk1,cons(hd(sk1),nil))) = hd(app(sk1,cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f5569]) ).
fof(f5572,plain,
( ~ sQ381_spl
| sQ398_spl
| ~ sQ9_spl
| ~ sQ397_spl ),
inference(split_clause,[status(thm)],[f5551,f5565,f515,f5569,f5359]) ).
fof(f5636,plain,
( sQ397_spl
| nil = app(sk1,cons(hd(sk1),nil))
| ~ ssList(app(sk1,cons(hd(sk1),nil))) ),
inference(resolution,[status(thm)],[f5567,f274]) ).
fof(f5637,plain,
( sQ397_spl
| sQ209_spl
| ~ sQ208_spl ),
inference(split_clause,[status(thm)],[f5636,f3504,f3507,f5565]) ).
fof(f5673,definition,
( sQ417_spl
<=> hd(app(sk1,cons(hd(sk1),nil))) = hd(sk1) ),
introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition]) ).
fof(f5674,plain,
( ~ sQ417_spl
| hd(app(sk1,cons(hd(sk1),nil))) = hd(sk1) ),
inference(component_clause,[status(thm)],[f5673]) ).
fof(f5874,plain,
( ~ sQ417_spl
| nil = app(sk1,cons(hd(sk1),nil))
| cons(hd(sk1),tl(app(sk1,cons(hd(sk1),nil)))) = app(sk1,cons(hd(sk1),nil))
| ~ ssList(app(sk1,cons(hd(sk1),nil))) ),
inference(paramodulation,[status(thm)],[f5674,f304]) ).
fof(f5887,definition,
( sQ438_spl
<=> cons(hd(sk1),tl(app(sk1,cons(hd(sk1),nil)))) = app(sk1,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ438_spl])],[split_symbol_definition]) ).
fof(f5888,plain,
( ~ sQ438_spl
| cons(hd(sk1),tl(app(sk1,cons(hd(sk1),nil)))) = app(sk1,cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f5887]) ).
fof(f5890,plain,
( ~ sQ417_spl
| sQ209_spl
| sQ438_spl
| ~ sQ208_spl ),
inference(split_clause,[status(thm)],[f5874,f3504,f5887,f3507,f5673]) ).
fof(f5897,plain,
( ~ sQ438_spl
| ~ sQ150_spl
| cons(hd(sk1),sk2) = app(sk1,cons(hd(sk1),nil)) ),
inference(forward_demodulation,[status(thm)],[f3141,f5888]) ).
fof(f6067,plain,
! [X0] :
( ~ sQ438_spl
| ~ sQ150_spl
| memberP(cons(hd(sk1),sk2),X0)
| ~ ssItem(X0)
| ~ ssList(sk1)
| ~ ssList(cons(hd(sk1),nil))
| ~ memberP(sk1,X0) ),
inference(paramodulation,[status(thm)],[f5897,f352]) ).
fof(f6101,definition,
! [X0] :
( sQ461_spl
<=> ( memberP(cons(hd(sk1),sk2),X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ461_spl])],[split_symbol_definition]) ).
fof(f6102,plain,
! [X0] :
( ~ sQ461_spl
| memberP(cons(hd(sk1),sk2),X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(component_clause,[status(thm)],[f6101]) ).
fof(f6104,plain,
( ~ sQ438_spl
| ~ sQ150_spl
| ~ sQ148_spl
| ~ sQ146_spl
| sQ461_spl ),
inference(split_clause,[status(thm)],[f6067,f6101,f3039,f3048,f3140,f5887]) ).
fof(f6441,definition,
( sQ509_spl
<=> skaf83(cons(hd(sk1),nil)) = hd(sk1) ),
introduced(definition,[new_symbols(definition,[sQ509_spl])],[split_symbol_definition]) ).
fof(f6442,plain,
( ~ sQ509_spl
| skaf83(cons(hd(sk1),nil)) = hd(sk1) ),
inference(component_clause,[status(thm)],[f6441]) ).
fof(f6454,definition,
( sQ512_spl
<=> hd(cons(hd(sk1),nil)) = hd(sk1) ),
introduced(definition,[new_symbols(definition,[sQ512_spl])],[split_symbol_definition]) ).
fof(f6455,plain,
( ~ sQ512_spl
| hd(cons(hd(sk1),nil)) = hd(sk1) ),
inference(component_clause,[status(thm)],[f6454]) ).
fof(f6517,plain,
( ~ sQ512_spl
| nil = cons(hd(sk1),nil)
| cons(hd(sk1),tl(cons(hd(sk1),nil))) = cons(hd(sk1),nil)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f6455,f304]) ).
fof(f6527,definition,
( sQ520_spl
<=> cons(hd(sk1),tl(cons(hd(sk1),nil))) = cons(hd(sk1),nil) ),
introduced(definition,[new_symbols(definition,[sQ520_spl])],[split_symbol_definition]) ).
fof(f6528,plain,
( ~ sQ520_spl
| cons(hd(sk1),tl(cons(hd(sk1),nil))) = cons(hd(sk1),nil) ),
inference(component_clause,[status(thm)],[f6527]) ).
fof(f6530,plain,
( ~ sQ512_spl
| sQ188_spl
| sQ520_spl
| ~ sQ146_spl ),
inference(split_clause,[status(thm)],[f6517,f3039,f6527,f3290,f6454]) ).
fof(f6568,definition,
( sQ525_spl
<=> sk5 = hd(sk1) ),
introduced(definition,[new_symbols(definition,[sQ525_spl])],[split_symbol_definition]) ).
fof(f6569,plain,
( ~ sQ525_spl
| sk5 = hd(sk1) ),
inference(component_clause,[status(thm)],[f6568]) ).
fof(f6572,plain,
( sQ270_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4046,f434]) ).
fof(f6573,plain,
sQ270_spl,
inference(contradiction_clause,[status(thm)],[f6572]) ).
fof(f7218,plain,
! [X0] :
( ~ sQ461_spl
| X0 = hd(sk1)
| memberP(sk2,X0)
| ~ ssItem(X0)
| ~ ssItem(hd(sk1))
| ~ ssList(sk2)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(resolution,[status(thm)],[f6102,f389]) ).
fof(f7219,definition,
! [X0] :
( sQ564_spl
<=> ( X0 = hd(sk1)
| memberP(sk2,X0)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ564_spl])],[split_symbol_definition]) ).
fof(f7220,plain,
! [X0] :
( ~ sQ564_spl
| X0 = hd(sk1)
| memberP(sk2,X0)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(component_clause,[status(thm)],[f7219]) ).
fof(f7222,plain,
( ~ sQ461_spl
| ~ sQ147_spl
| ~ sQ9_spl
| sQ564_spl ),
inference(split_clause,[status(thm)],[f7218,f7219,f515,f3042,f6101]) ).
fof(f7223,plain,
! [X0] :
( ~ sQ564_spl
| X0 = hd(sk1)
| memberP(sk2,X0)
| ~ ssItem(X0)
| ~ memberP(sk1,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f7220]) ).
fof(f7224,plain,
( ~ sQ564_spl
| sk5 = hd(sk1)
| ~ ssItem(sk5)
| ~ memberP(sk1,sk5) ),
inference(resolution,[status(thm)],[f7223,f436]) ).
fof(f7226,plain,
( ~ sQ564_spl
| sQ525_spl
| ~ sQ270_spl
| ~ sQ269_spl ),
inference(split_clause,[status(thm)],[f7224,f4041,f4044,f6568,f7219]) ).
fof(f7378,definition,
( sQ584_spl
<=> ssItem(hd(cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ584_spl])],[split_symbol_definition]) ).
fof(f7380,plain,
( sQ584_spl
| ~ ssItem(hd(cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f7378]) ).
fof(f7443,plain,
( sQ584_spl
| nil = cons(hd(sk1),nil)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(resolution,[status(thm)],[f7380,f274]) ).
fof(f7444,plain,
( sQ584_spl
| sQ188_spl
| ~ sQ146_spl ),
inference(split_clause,[status(thm)],[f7443,f3039,f3290,f7378]) ).
fof(f7531,definition,
( sQ606_spl
<=> ssItem(skaf83(cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ606_spl])],[split_symbol_definition]) ).
fof(f7533,plain,
( sQ606_spl
| ~ ssItem(skaf83(cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f7531]) ).
fof(f7628,definition,
( sQ615_spl
<=> memberP(cons(hd(sk1),nil),skaf83(cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition]) ).
fof(f7629,plain,
( ~ sQ615_spl
| memberP(cons(hd(sk1),nil),skaf83(cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f7628]) ).
fof(f7630,plain,
( sQ615_spl
| ~ memberP(cons(hd(sk1),nil),skaf83(cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f7628]) ).
fof(f7658,plain,
( sQ606_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7533,f209]) ).
fof(f7659,plain,
sQ606_spl,
inference(contradiction_clause,[status(thm)],[f7658]) ).
fof(f7660,plain,
( ~ sQ219_spl
| ~ sQ615_spl
| memberP(sk2,skaf83(cons(hd(sk1),nil)))
| ~ ssItem(skaf83(cons(hd(sk1),nil))) ),
inference(resolution,[status(thm)],[f7629,f3599]) ).
fof(f7662,definition,
( sQ620_spl
<=> memberP(sk2,skaf83(cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition]) ).
fof(f7663,plain,
( ~ sQ620_spl
| memberP(sk2,skaf83(cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f7662]) ).
fof(f7665,plain,
( ~ sQ219_spl
| ~ sQ615_spl
| sQ620_spl
| ~ sQ606_spl ),
inference(split_clause,[status(thm)],[f7660,f7531,f7662,f7628,f3598]) ).
fof(f7720,plain,
( ~ sQ188_spl
| ~ ssList(nil)
| ~ ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f3291,f297]) ).
fof(f7747,plain,
( ~ sQ188_spl
| ~ sQ8_spl
| ~ sQ147_spl ),
inference(split_clause,[status(thm)],[f7720,f3042,f512,f3290]) ).
fof(f7895,plain,
( sQ615_spl
| ~ sQ509_spl
| ~ memberP(cons(hd(sk1),nil),hd(sk1)) ),
inference(forward_demodulation,[status(thm)],[f6442,f7630]) ).
fof(f7896,plain,
( sQ615_spl
| ~ sQ509_spl
| ~ ssItem(hd(sk1))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f7895,f482]) ).
fof(f7898,plain,
( sQ615_spl
| ~ sQ509_spl
| ~ sQ147_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f7896,f512,f3042,f6441,f7628]) ).
fof(f7935,definition,
( sQ631_spl
<=> ssList(tl(cons(hd(sk1),nil))) ),
introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition]) ).
fof(f7937,plain,
( sQ631_spl
| ~ ssList(tl(cons(hd(sk1),nil))) ),
inference(component_clause,[status(thm)],[f7935]) ).
fof(f7940,plain,
( sQ631_spl
| nil = cons(hd(sk1),nil)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(resolution,[status(thm)],[f7937,f273]) ).
fof(f7941,plain,
( sQ631_spl
| sQ188_spl
| ~ sQ146_spl ),
inference(split_clause,[status(thm)],[f7940,f3039,f3290,f7935]) ).
fof(f8863,plain,
( ~ sQ520_spl
| skaf83(cons(hd(sk1),nil)) = hd(sk1)
| ~ ssList(tl(cons(hd(sk1),nil)))
| ~ ssItem(hd(sk1)) ),
inference(paramodulation,[status(thm)],[f6528,f879]) ).
fof(f8877,definition,
( sQ744_spl
<=> nil = tl(cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ744_spl])],[split_symbol_definition]) ).
fof(f8878,plain,
( ~ sQ744_spl
| nil = tl(cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f8877]) ).
fof(f8879,plain,
( sQ744_spl
| nil != tl(cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f8877]) ).
fof(f8954,plain,
( ~ sQ520_spl
| sQ509_spl
| ~ sQ631_spl
| ~ sQ147_spl ),
inference(split_clause,[status(thm)],[f8863,f3042,f7935,f6441,f6527]) ).
fof(f8990,plain,
( ~ sQ744_spl
| nil = cons(hd(sk1),nil)
| cons(hd(cons(hd(sk1),nil)),nil) = cons(hd(sk1),nil)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f8878,f304]) ).
fof(f8997,definition,
( sQ769_spl
<=> cons(hd(cons(hd(sk1),nil)),nil) = cons(hd(sk1),nil) ),
introduced(definition,[new_symbols(definition,[sQ769_spl])],[split_symbol_definition]) ).
fof(f8998,plain,
( ~ sQ769_spl
| cons(hd(cons(hd(sk1),nil)),nil) = cons(hd(sk1),nil) ),
inference(component_clause,[status(thm)],[f8997]) ).
fof(f9000,plain,
( ~ sQ744_spl
| sQ188_spl
| sQ769_spl
| ~ sQ146_spl ),
inference(split_clause,[status(thm)],[f8990,f3039,f8997,f3290,f8877]) ).
fof(f9062,plain,
( ~ sQ769_spl
| hd(cons(hd(sk1),nil)) = hd(sk1)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssItem(hd(cons(hd(sk1),nil)))
| ~ ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f8998,f399]) ).
fof(f9107,plain,
( ~ sQ769_spl
| sQ512_spl
| ~ sQ8_spl
| ~ sQ584_spl
| ~ sQ147_spl ),
inference(split_clause,[status(thm)],[f9062,f3042,f7378,f512,f6454,f8997]) ).
fof(f9229,plain,
( sQ744_spl
| ~ ssList(nil)
| ~ ssItem(hd(sk1)) ),
inference(resolution,[status(thm)],[f8879,f294]) ).
fof(f9230,plain,
( sQ744_spl
| ~ sQ8_spl
| ~ sQ147_spl ),
inference(split_clause,[status(thm)],[f9229,f3042,f512,f8877]) ).
fof(f9324,plain,
( ~ sQ620_spl
| ~ sQ509_spl
| memberP(sk2,hd(sk1)) ),
inference(forward_demodulation,[status(thm)],[f6442,f7663]) ).
fof(f9964,definition,
( sQ843_spl
<=> skaf83(app(sk1,cons(hd(sk1),nil))) = hd(sk1) ),
introduced(definition,[new_symbols(definition,[sQ843_spl])],[split_symbol_definition]) ).
fof(f9965,plain,
( ~ sQ843_spl
| skaf83(app(sk1,cons(hd(sk1),nil))) = hd(sk1) ),
inference(component_clause,[status(thm)],[f9964]) ).
fof(f9972,plain,
( ~ sQ398_spl
| ~ sQ843_spl
| hd(sk1) = hd(app(sk1,cons(hd(sk1),nil))) ),
inference(backward_demodulation,[status(thm)],[f9965,f5570]) ).
fof(f9974,plain,
( ~ sQ398_spl
| ~ sQ843_spl
| sQ417_spl ),
inference(split_clause,[status(thm)],[f9972,f5673,f9964,f5569]) ).
fof(f10036,plain,
( ~ sQ620_spl
| ~ sQ509_spl
| ~ sQ525_spl
| memberP(sk2,sk5) ),
inference(backward_demodulation,[status(thm)],[f6569,f9324]) ).
fof(f10099,plain,
( ~ sQ620_spl
| ~ sQ509_spl
| ~ sQ525_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10036,f436]) ).
fof(f10100,plain,
( ~ sQ620_spl
| ~ sQ509_spl
| ~ sQ525_spl ),
inference(contradiction_clause,[status(thm)],[f10099]) ).
fof(f10102,definition,
( sQ845_spl
<=> ssList(skaf46(sk2,sk2)) ),
introduced(definition,[new_symbols(definition,[sQ845_spl])],[split_symbol_definition]) ).
fof(f10104,plain,
( sQ845_spl
| ~ ssList(skaf46(sk2,sk2)) ),
inference(component_clause,[status(thm)],[f10102]) ).
fof(f10106,plain,
( sQ845_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10104,f247]) ).
fof(f10107,plain,
sQ845_spl,
inference(contradiction_clause,[status(thm)],[f10106]) ).
fof(f10469,definition,
( sQ864_spl
<=> ssList(skaf45(cons(hd(sk1),sk2),sk1)) ),
introduced(definition,[new_symbols(definition,[sQ864_spl])],[split_symbol_definition]) ).
fof(f10471,plain,
( sQ864_spl
| ~ ssList(skaf45(cons(hd(sk1),sk2),sk1)) ),
inference(component_clause,[status(thm)],[f10469]) ).
fof(f10473,plain,
( sQ864_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10471,f248]) ).
fof(f10474,plain,
sQ864_spl,
inference(contradiction_clause,[status(thm)],[f10473]) ).
fof(f10644,definition,
( sQ887_spl
<=> app(sk1,cons(hd(sk1),nil)) = app(sk1,cons(hd(sk1),nil)) ),
introduced(definition,[new_symbols(definition,[sQ887_spl])],[split_symbol_definition]) ).
fof(f10646,plain,
( sQ887_spl
| app(sk1,cons(hd(sk1),nil)) != app(sk1,cons(hd(sk1),nil)) ),
inference(component_clause,[status(thm)],[f10644]) ).
fof(f10648,plain,
( sQ887_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10646]) ).
fof(f10649,plain,
sQ887_spl,
inference(contradiction_clause,[status(thm)],[f10648]) ).
fof(f11296,definition,
( sQ957_spl
<=> ssList(skaf46(nil,sk2)) ),
introduced(definition,[new_symbols(definition,[sQ957_spl])],[split_symbol_definition]) ).
fof(f11298,plain,
( sQ957_spl
| ~ ssList(skaf46(nil,sk2)) ),
inference(component_clause,[status(thm)],[f11296]) ).
fof(f11300,plain,
( sQ957_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11298,f247]) ).
fof(f11301,plain,
sQ957_spl,
inference(contradiction_clause,[status(thm)],[f11300]) ).
fof(f11480,plain,
( ~ sQ398_spl
| skaf83(app(sk1,cons(hd(sk1),nil))) = hd(sk1)
| nil = sk1
| ~ ssList(sk1)
| ~ ssList(cons(hd(sk1),nil)) ),
inference(paramodulation,[status(thm)],[f5570,f331]) ).
fof(f11486,plain,
( ~ sQ398_spl
| sQ843_spl
| sQ149_spl
| ~ sQ148_spl
| ~ sQ146_spl ),
inference(split_clause,[status(thm)],[f11480,f3039,f3048,f3051,f9964,f5569]) ).
fof(f11488,plain,
$false,
inference(sat_refutation,[status(thm)],[f454,f468,f507,f521,f523,f525,f527,f3045,f3054,f3056,f3058,f3064,f3099,f3143,f3297,f3601,f4050,f5168,f5338,f5362,f5572,f5637,f5890,f6104,f6530,f6573,f7222,f7226,f7444,f7659,f7665,f7747,f7898,f7941,f8954,f9000,f9107,f9230,f9974,f10100,f10107,f10474,f10649,f11301,f11486]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC396-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.37 % Computer : n002.cluster.edu
% 0.08/5.37 % Model : x86_64 x86_64
% 0.08/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.37 % Memory : 8046.5625MB
% 0.08/5.37 % OS : Linux 6.8.0-71-generic
% 0.08/5.37 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Mon Sep 21 08:23:55 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.08/5.39 % Drodi V4.1.1
% 54.73/12.46 % Refutation found
% 54.73/12.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 54.73/12.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.39/12.54 % Elapsed time: 7.149961 seconds
% 8.39/12.54 % CPU time: 56.100234 seconds
% 8.39/12.54 % Total memory used: 391.724 MB
% 8.39/12.54 % Net memory used: 372.991 MB
%------------------------------------------------------------------------------