%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC192-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 : n026.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:20 PM UTC 2026
% Result : Unsatisfiable 0.02s 0.43s
% Output : CNFRefutation 0.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 86
% Syntax : Number of formulae : 280 ( 28 unt; 55 def)
% Number of atoms : 937 ( 148 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 1247 ( 590 ~; 602 |; 0 &)
% ( 55 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 60 ( 58 usr; 56 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 174 ( 174 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U] :
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(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(f99,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != V ),
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(f119,axiom,
! [U,V] :
( nil = V
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
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(f139,axiom,
! [U,V,W] :
( memberP(cons(W,U),V)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ ssList(U)
| ~ memberP(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(f149,axiom,
! [U,V,W] :
( app(app(W,V),U) = app(W,app(V,U))
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f150,axiom,
! [U,V,W] :
( V = W
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [U,V,W] :
( U = W
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f157,axiom,
! [U,V,W] :
( cons(U,app(V,W)) = app(cons(U,V),W)
| ~ ssList(W)
| ~ ssList(V)
| ~ ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f158,axiom,
! [U,V,W] :
( memberP(U,W)
| memberP(V,W)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(V)
| ~ memberP(app(U,V),W) ),
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(f188,negated_conjecture,
ssList(sk3),
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,
ssItem(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
sk5 != sk6,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
( nil = sk4
| ssItem(sk9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
( nil = sk3
| ssItem(sk9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,negated_conjecture,
( nil = sk4
| cons(sk9,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f202,negated_conjecture,
( nil = sk3
| cons(sk9,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f211,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f274,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f277,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f278,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
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(f304,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != V ) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f305,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != X1 ),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f330,plain,
! [U] :
( nil = U
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f331,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f332,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f333,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f332]) ).
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(f357,plain,
! [X0,X1,X2] :
( memberP(cons(X2,X0),X1)
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
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(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(f373,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f374,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f373]) ).
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(f387,plain,
! [X0,X1,X2] :
( cons(X0,app(X1,X2)) = app(cons(X0,X1),X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f388,plain,
! [U,W] :
( memberP(U,W)
| ! [V] :
( memberP(V,W)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(V)
| ~ memberP(app(U,V),W) ) ),
inference(miniscoping,[status(thm)],[f158]) ).
fof(f389,plain,
! [X0,X1,X2] :
( memberP(X0,X2)
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ memberP(app(X0,X1),X2) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
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(f436,plain,
ssList(sk3),
inference(cnf_transformation,[status(thm)],[f188]) ).
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,
sk5 != sk6,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f446,plain,
( nil = sk4
| ssItem(sk9) ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f447,plain,
( nil = sk3
| ssItem(sk9) ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f448,plain,
( nil = sk4
| cons(sk9,nil) = sk3 ),
inference(cnf_transformation,[status(thm)],[f200]) ).
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(f462,definition,
( sQ3_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f463,plain,
( ~ sQ3_spl
| nil = sk4 ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f446,f459,f462]) ).
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(f473,plain,
( sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f448,f470,f462]) ).
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(f512,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| nil = sk4 ),
inference(backward_demodulation,[status(thm)],[f515,f467]) ).
fof(f515,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| sk3 = sk4 ),
inference(forward_demodulation,[status(thm)],[f467,f463]) ).
fof(f516,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ3_spl
| ~ ssItem(X0)
| ~ memberP(sk4,X0) ),
inference(forward_demodulation,[status(thm)],[f512,f274]) ).
fof(f531,definition,
( sQ7_spl
<=> ssList(sk8) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f533,plain,
( sQ7_spl
| ~ ssList(sk8) ),
inference(component_clause,[status(thm)],[f531]) ).
fof(f541,plain,
( ~ sQ5_spl
| ~ ssList(nil)
| ~ ssItem(sk9)
| sk3 != nil ),
inference(paramodulation,[status(thm)],[f471,f305]) ).
fof(f542,definition,
( sQ10_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f544,plain,
( sQ10_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f545,plain,
( ~ sQ5_spl
| ~ sQ10_spl
| ~ sQ2_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f541,f466,f459,f542,f470]) ).
fof(f560,definition,
( sQ11_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f585,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f544,f211]) ).
fof(f586,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f585]) ).
fof(f591,plain,
( ~ ssList(nil)
| nil = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f331,f278]) ).
fof(f592,definition,
( sQ13_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f595,plain,
( sQ13_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f591,f542,f592]) ).
fof(f598,plain,
app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = sk3,
inference(forward_demodulation,[status(thm)],[f439,f444]) ).
fof(f599,plain,
( nil = sk8
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(sk8)
| sk3 != nil ),
inference(paramodulation,[status(thm)],[f598,f333]) ).
fof(f602,definition,
( sQ14_spl
<=> ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f604,plain,
( sQ14_spl
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(component_clause,[status(thm)],[f602]) ).
fof(f605,definition,
( sQ15_spl
<=> nil = sk8 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f606,plain,
( ~ sQ15_spl
| nil = sk8 ),
inference(component_clause,[status(thm)],[f605]) ).
fof(f608,plain,
( sQ15_spl
| ~ sQ14_spl
| ~ sQ7_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f599,f466,f531,f602,f605]) ).
fof(f635,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f533,f443]) ).
fof(f636,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f635]) ).
fof(f660,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| sk1 = sk4 ),
inference(backward_demodulation,[status(thm)],[f515,f439]) ).
fof(f739,plain,
! [X0,X1] :
( X0 = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[f374]) ).
fof(f745,definition,
! [X0] :
( sQ25_spl
<=> ( X0 = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f748,definition,
! [X1] :
( sQ26_spl
<=> ~ ssList(X1) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f749,plain,
! [X0] :
( ~ sQ26_spl
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f748]) ).
fof(f751,plain,
( sQ26_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f739,f745,f748]) ).
fof(f769,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| sk3 = sk4 ),
inference(forward_demodulation,[status(thm)],[f439,f660]) ).
fof(f770,plain,
( sk3 = app(app(sk7,cons(sk5,nil)),app(cons(sk6,nil),sk8))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| ~ ssList(sk8) ),
inference(paramodulation,[status(thm)],[f598,f372]) ).
fof(f771,plain,
! [X0] :
( X0 = app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(sk8)
| ~ ssList(X0)
| app(X0,sk8) != sk3 ),
inference(paramodulation,[status(thm)],[f598,f376]) ).
fof(f773,plain,
! [X0] :
( X0 = sk8
| ~ ssList(sk8)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) != sk3 ),
inference(paramodulation,[status(thm)],[f598,f374]) ).
fof(f775,plain,
! [X0] :
( app(sk3,X0) = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),app(sk8,X0))
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(sk8)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f598,f372]) ).
fof(f776,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(sk8)
| ~ memberP(sk8,X0) ),
inference(paramodulation,[status(thm)],[f598,f359]) ).
fof(f777,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(sk8)
| ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) ),
inference(paramodulation,[status(thm)],[f598,f358]) ).
fof(f779,definition,
( sQ28_spl
<=> ssList(cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f781,plain,
( sQ28_spl
| ~ ssList(cons(sk6,nil)) ),
inference(component_clause,[status(thm)],[f779]) ).
fof(f782,definition,
( sQ29_spl
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f784,plain,
( sQ29_spl
| ~ ssList(app(sk7,cons(sk5,nil))) ),
inference(component_clause,[status(thm)],[f782]) ).
fof(f785,definition,
( sQ30_spl
<=> sk3 = app(app(sk7,cons(sk5,nil)),app(cons(sk6,nil),sk8)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f786,plain,
( ~ sQ30_spl
| sk3 = app(app(sk7,cons(sk5,nil)),app(cons(sk6,nil),sk8)) ),
inference(component_clause,[status(thm)],[f785]) ).
fof(f788,plain,
( sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f770,f531,f779,f782,f785]) ).
fof(f789,definition,
! [X0] :
( sQ31_spl
<=> ( X0 = app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| ~ ssList(X0)
| app(X0,sk8) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f790,plain,
! [X0] :
( ~ sQ31_spl
| X0 = app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| ~ ssList(X0)
| app(X0,sk8) != sk3 ),
inference(component_clause,[status(thm)],[f789]) ).
fof(f792,plain,
( ~ sQ14_spl
| ~ sQ7_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f771,f789,f531,f602]) ).
fof(f794,definition,
! [X0] :
( sQ32_spl
<=> ( X0 = sk8
| ~ ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f797,plain,
( ~ sQ7_spl
| ~ sQ14_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f773,f794,f602,f531]) ).
fof(f799,definition,
! [X0] :
( sQ33_spl
<=> ( app(sk3,X0) = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),app(sk8,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f802,plain,
( ~ sQ14_spl
| ~ sQ7_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f775,f799,f531,f602]) ).
fof(f803,definition,
! [X0] :
( sQ34_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk8,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f806,plain,
( ~ sQ14_spl
| ~ sQ7_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f776,f803,f531,f602]) ).
fof(f807,definition,
! [X0] :
( sQ35_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f810,plain,
( ~ sQ14_spl
| ~ sQ7_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f777,f807,f531,f602]) ).
fof(f858,definition,
( sQ38_spl
<=> sk3 = sk3 ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f860,plain,
( sQ38_spl
| sk3 != sk3 ),
inference(component_clause,[status(thm)],[f858]) ).
fof(f862,plain,
( sQ38_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f860]) ).
fof(f863,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f862]) ).
fof(f865,plain,
! [X0] :
( memberP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0)
| memberP(sk8,X0)
| ~ ssItem(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(sk8)
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f598,f389]) ).
fof(f866,plain,
! [X0] :
( cons(X0,sk3) = app(cons(X0,app(app(sk7,cons(sk5,nil)),cons(sk6,nil))),sk8)
| ~ ssList(sk8)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f598,f387]) ).
fof(f876,definition,
! [X0] :
( sQ39_spl
<=> ( memberP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0)
| memberP(sk8,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f879,plain,
( ~ sQ14_spl
| ~ sQ7_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f865,f876,f531,f602]) ).
fof(f880,definition,
! [X0] :
( sQ40_spl
<=> ( cons(X0,sk3) = app(cons(X0,app(app(sk7,cons(sk5,nil)),cons(sk6,nil))),sk8)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f883,plain,
( ~ sQ7_spl
| ~ sQ14_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f866,f880,f602,f531]) ).
fof(f892,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(X0,nil))
| ~ ssList(app(X0,nil)) ),
inference(resolution,[status(thm)],[f277,f376]) ).
fof(f896,definition,
! [X0] :
( sQ41_spl
<=> ( app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(app(X0,nil))
| ~ ssList(app(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f899,plain,
( ~ sQ10_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f892,f896,f542]) ).
fof(f904,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(nil,X0))
| ~ ssList(app(nil,X0)) ),
inference(resolution,[status(thm)],[f278,f374]) ).
fof(f906,definition,
! [X0] :
( sQ42_spl
<=> ( app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(app(nil,X0))
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f909,plain,
( ~ sQ10_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f904,f906,f542]) ).
fof(f920,plain,
( ~ sQ26_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f436,f749]) ).
fof(f952,plain,
~ sQ26_spl,
inference(contradiction_clause,[status(thm)],[f920]) ).
fof(f964,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ15_spl
| sk8 = sk4 ),
inference(forward_demodulation,[status(thm)],[f606,f512]) ).
fof(f967,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| sk3 = sk8 ),
inference(forward_demodulation,[status(thm)],[f964,f769]) ).
fof(f1133,plain,
( sQ14_spl
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil)) ),
inference(resolution,[status(thm)],[f604,f289]) ).
fof(f1134,plain,
( sQ14_spl
| ~ sQ29_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f1133,f779,f782,f602]) ).
fof(f1135,plain,
( sQ28_spl
| ~ ssList(nil)
| ~ ssItem(sk6) ),
inference(resolution,[status(thm)],[f781,f290]) ).
fof(f1136,definition,
( sQ47_spl
<=> ssItem(sk6) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1138,plain,
( sQ47_spl
| ~ ssItem(sk6) ),
inference(component_clause,[status(thm)],[f1136]) ).
fof(f1139,plain,
( sQ28_spl
| ~ sQ10_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f1135,f1136,f542,f779]) ).
fof(f1140,plain,
( sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1138,f441]) ).
fof(f1141,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f1140]) ).
fof(f1142,plain,
( sQ29_spl
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[f784,f289]) ).
fof(f1143,definition,
( sQ48_spl
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1145,plain,
( sQ48_spl
| ~ ssList(cons(sk5,nil)) ),
inference(component_clause,[status(thm)],[f1143]) ).
fof(f1146,definition,
( sQ49_spl
<=> ssList(sk7) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1148,plain,
( sQ49_spl
| ~ ssList(sk7) ),
inference(component_clause,[status(thm)],[f1146]) ).
fof(f1149,plain,
( sQ29_spl
| ~ sQ49_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f1142,f1143,f1146,f782]) ).
fof(f1150,plain,
( sQ48_spl
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1145,f290]) ).
fof(f1151,definition,
( sQ50_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1153,plain,
( sQ50_spl
| ~ ssItem(sk5) ),
inference(component_clause,[status(thm)],[f1151]) ).
fof(f1154,plain,
( sQ48_spl
| ~ sQ10_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f1150,f1151,f542,f1143]) ).
fof(f1155,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1148,f442]) ).
fof(f1156,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f1155]) ).
fof(f1157,plain,
( sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1153,f440]) ).
fof(f1158,plain,
sQ50_spl,
inference(contradiction_clause,[status(thm)],[f1157]) ).
fof(f1216,plain,
( ~ sQ30_spl
| sk3 = app(sk7,app(cons(sk5,nil),app(cons(sk6,nil),sk8)))
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(app(cons(sk6,nil),sk8)) ),
inference(paramodulation,[status(thm)],[f786,f372]) ).
fof(f1217,plain,
! [X0] :
( ~ sQ30_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(app(cons(sk6,nil),sk8))
| ~ memberP(app(sk7,cons(sk5,nil)),X0) ),
inference(paramodulation,[status(thm)],[f786,f358]) ).
fof(f1218,plain,
! [X0] :
( ~ sQ30_spl
| app(sk3,X0) = app(app(sk7,cons(sk5,nil)),app(app(cons(sk6,nil),sk8),X0))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(app(cons(sk6,nil),sk8))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f786,f372]) ).
fof(f1219,plain,
! [X0] :
( ~ sQ30_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(app(cons(sk6,nil),sk8))
| ~ memberP(app(cons(sk6,nil),sk8),X0) ),
inference(paramodulation,[status(thm)],[f786,f359]) ).
fof(f1220,plain,
! [X0] :
( ~ sQ30_spl
| X0 = app(cons(sk6,nil),sk8)
| ~ ssList(app(cons(sk6,nil),sk8))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(X0)
| app(app(sk7,cons(sk5,nil)),X0) != sk3 ),
inference(paramodulation,[status(thm)],[f786,f374]) ).
fof(f1222,plain,
! [X0] :
( ~ sQ30_spl
| X0 = app(sk7,cons(sk5,nil))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(app(cons(sk6,nil),sk8))
| ~ ssList(X0)
| app(X0,app(cons(sk6,nil),sk8)) != sk3 ),
inference(paramodulation,[status(thm)],[f786,f376]) ).
fof(f1224,plain,
! [X0] :
( ~ sQ30_spl
| cons(X0,sk3) = app(cons(X0,app(sk7,cons(sk5,nil))),app(cons(sk6,nil),sk8))
| ~ ssList(app(cons(sk6,nil),sk8))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f786,f387]) ).
fof(f1225,plain,
! [X0] :
( ~ sQ30_spl
| memberP(app(sk7,cons(sk5,nil)),X0)
| memberP(app(cons(sk6,nil),sk8),X0)
| ~ ssItem(X0)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(app(cons(sk6,nil),sk8))
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f786,f389]) ).
fof(f1227,plain,
( ~ sQ30_spl
| ssList(sk3)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(app(cons(sk6,nil),sk8)) ),
inference(paramodulation,[status(thm)],[f786,f289]) ).
fof(f1230,definition,
( sQ52_spl
<=> ssList(app(cons(sk6,nil),sk8)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1232,plain,
( sQ52_spl
| ~ ssList(app(cons(sk6,nil),sk8)) ),
inference(component_clause,[status(thm)],[f1230]) ).
fof(f1233,definition,
( sQ53_spl
<=> sk3 = app(sk7,app(cons(sk5,nil),app(cons(sk6,nil),sk8))) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1236,plain,
( ~ sQ30_spl
| sQ53_spl
| ~ sQ49_spl
| ~ sQ48_spl
| ~ sQ52_spl ),
inference(split_clause,[status(thm)],[f1216,f1230,f1143,f1146,f1233,f785]) ).
fof(f1237,definition,
! [X0] :
( sQ54_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(sk7,cons(sk5,nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1238,plain,
! [X0] :
( ~ sQ54_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(sk7,cons(sk5,nil)),X0) ),
inference(component_clause,[status(thm)],[f1237]) ).
fof(f1240,plain,
( ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ52_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1217,f1237,f1230,f782,f785]) ).
fof(f1241,definition,
! [X0] :
( sQ55_spl
<=> ( app(sk3,X0) = app(app(sk7,cons(sk5,nil)),app(app(cons(sk6,nil),sk8),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1244,plain,
( ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ52_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1218,f1241,f1230,f782,f785]) ).
fof(f1245,definition,
! [X0] :
( sQ56_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(cons(sk6,nil),sk8),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1246,plain,
! [X0] :
( ~ sQ56_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(cons(sk6,nil),sk8),X0) ),
inference(component_clause,[status(thm)],[f1245]) ).
fof(f1248,plain,
( ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ52_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1219,f1245,f1230,f782,f785]) ).
fof(f1249,definition,
! [X0] :
( sQ57_spl
<=> ( X0 = app(cons(sk6,nil),sk8)
| ~ ssList(X0)
| app(app(sk7,cons(sk5,nil)),X0) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1252,plain,
( ~ sQ30_spl
| ~ sQ52_spl
| ~ sQ29_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1220,f1249,f782,f1230,f785]) ).
fof(f1254,definition,
! [X0] :
( sQ58_spl
<=> ( X0 = app(sk7,cons(sk5,nil))
| ~ ssList(X0)
| app(X0,app(cons(sk6,nil),sk8)) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1257,plain,
( ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ52_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1222,f1254,f1230,f782,f785]) ).
fof(f1259,definition,
! [X0] :
( sQ59_spl
<=> ( cons(X0,sk3) = app(cons(X0,app(sk7,cons(sk5,nil))),app(cons(sk6,nil),sk8))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1262,plain,
( ~ sQ30_spl
| ~ sQ52_spl
| ~ sQ29_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1224,f1259,f782,f1230,f785]) ).
fof(f1263,definition,
! [X0] :
( sQ60_spl
<=> ( memberP(app(sk7,cons(sk5,nil)),X0)
| memberP(app(cons(sk6,nil),sk8),X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1266,plain,
( ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ52_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1225,f1263,f1230,f782,f785]) ).
fof(f1268,plain,
( ~ sQ30_spl
| sQ11_spl
| ~ sQ29_spl
| ~ sQ52_spl ),
inference(split_clause,[status(thm)],[f1227,f1230,f782,f560,f785]) ).
fof(f1269,definition,
( sQ61_spl
<=> nil = app(sk7,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1277,plain,
( sQ52_spl
| ~ ssList(cons(sk6,nil))
| ~ ssList(sk8) ),
inference(resolution,[status(thm)],[f1232,f289]) ).
fof(f1278,plain,
( sQ52_spl
| ~ sQ28_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1277,f531,f779,f1230]) ).
fof(f1279,plain,
! [X0] :
( ~ sQ54_spl
| ~ ssItem(X0)
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ memberP(sk7,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1238,f358]) ).
fof(f1280,plain,
! [X0] :
( ~ sQ54_spl
| ~ ssItem(X0)
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1238,f359]) ).
fof(f1281,definition,
! [X0] :
( sQ63_spl
<=> ( ~ ssItem(X0)
| ~ memberP(sk7,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1284,plain,
( ~ sQ54_spl
| ~ sQ49_spl
| ~ sQ48_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1279,f1281,f1143,f1146,f1237]) ).
fof(f1285,definition,
! [X0] :
( sQ64_spl
<=> ( ~ ssItem(X0)
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1286,plain,
! [X0] :
( ~ sQ64_spl
| ~ ssItem(X0)
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1285]) ).
fof(f1288,plain,
( ~ sQ54_spl
| ~ sQ49_spl
| ~ sQ48_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1280,f1285,f1143,f1146,f1237]) ).
fof(f1290,plain,
! [X0] :
( ~ sQ64_spl
| ~ memberP(cons(sk5,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1286]) ).
fof(f1291,plain,
! [X0] :
( ~ sQ31_spl
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssItem(X0)
| ~ ssList(cons(X0,app(app(sk7,cons(sk5,nil)),cons(sk6,nil))))
| app(cons(X0,app(app(sk7,cons(sk5,nil)),cons(sk6,nil))),sk8) != sk3 ),
inference(resolution,[status(thm)],[f790,f305]) ).
fof(f1292,plain,
! [X0] :
( ~ sQ31_spl
| X0 = cons(sk6,nil)
| ~ ssList(cons(sk6,nil))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),X0))
| app(app(app(sk7,cons(sk5,nil)),X0),sk8) != sk3 ),
inference(resolution,[status(thm)],[f790,f374]) ).
fof(f1293,plain,
! [X0] :
( ~ sQ31_spl
| X0 = app(sk7,cons(sk5,nil))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| ~ ssList(X0)
| ~ ssList(app(X0,cons(sk6,nil)))
| app(app(X0,cons(sk6,nil)),sk8) != sk3 ),
inference(resolution,[status(thm)],[f790,f376]) ).
fof(f1296,plain,
( ~ sQ31_spl
| nil = app(sk7,cons(sk5,nil))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| ~ ssList(nil)
| app(nil,sk8) != sk3 ),
inference(resolution,[status(thm)],[f790,f331]) ).
fof(f1297,plain,
( ~ sQ31_spl
| nil = cons(sk6,nil)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| ~ ssList(nil)
| app(nil,sk8) != sk3 ),
inference(resolution,[status(thm)],[f790,f333]) ).
fof(f1298,definition,
! [X0] :
( sQ65_spl
<=> ( ~ ssItem(X0)
| ~ ssList(cons(X0,app(app(sk7,cons(sk5,nil)),cons(sk6,nil))))
| app(cons(X0,app(app(sk7,cons(sk5,nil)),cons(sk6,nil))),sk8) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1301,plain,
( ~ sQ31_spl
| ~ sQ14_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1291,f1298,f602,f789]) ).
fof(f1302,definition,
! [X0] :
( sQ66_spl
<=> ( X0 = cons(sk6,nil)
| ~ ssList(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),X0))
| app(app(app(sk7,cons(sk5,nil)),X0),sk8) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1305,plain,
( ~ sQ31_spl
| ~ sQ28_spl
| ~ sQ29_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f1292,f1302,f782,f779,f789]) ).
fof(f1306,definition,
! [X0] :
( sQ67_spl
<=> ( X0 = app(sk7,cons(sk5,nil))
| ~ ssList(X0)
| ~ ssList(app(X0,cons(sk6,nil)))
| app(app(X0,cons(sk6,nil)),sk8) != sk3 ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1309,plain,
( ~ sQ31_spl
| ~ sQ29_spl
| ~ sQ28_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1293,f1306,f779,f782,f789]) ).
fof(f1312,definition,
( sQ68_spl
<=> app(nil,sk8) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1315,plain,
( ~ sQ31_spl
| sQ61_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ10_spl
| ~ sQ68_spl ),
inference(split_clause,[status(thm)],[f1296,f1312,f542,f779,f782,f1269,f789]) ).
fof(f1316,definition,
( sQ69_spl
<=> nil = cons(sk6,nil) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1319,plain,
( ~ sQ31_spl
| sQ69_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ10_spl
| ~ sQ68_spl ),
inference(split_clause,[status(thm)],[f1297,f1312,f542,f779,f782,f1316,f789]) ).
fof(f1320,plain,
( ~ sQ64_spl
| ~ ssItem(sk5)
| ~ ssList(nil)
| memberP(sk3,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1290,f493]) ).
fof(f1321,definition,
( sQ70_spl
<=> memberP(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1322,plain,
( ~ sQ70_spl
| memberP(sk3,sk5) ),
inference(component_clause,[status(thm)],[f1321]) ).
fof(f1324,plain,
( ~ sQ64_spl
| ~ sQ10_spl
| sQ70_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f1320,f1151,f1321,f542,f1285]) ).
fof(f1325,plain,
! [X0] :
( ~ sQ64_spl
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ ssItem(sk5)
| ~ ssList(nil)
| ~ memberP(nil,X0) ),
inference(resolution,[status(thm)],[f357,f1290]) ).
fof(f1327,definition,
! [X0] :
( sQ71_spl
<=> ( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ memberP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1330,plain,
( ~ sQ64_spl
| ~ sQ50_spl
| ~ sQ10_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1325,f1327,f542,f1151,f1285]) ).
fof(f1333,plain,
! [X0] :
( ~ sQ56_spl
| ~ ssItem(X0)
| ~ ssList(cons(sk6,nil))
| ~ ssList(sk8)
| ~ memberP(cons(sk6,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1246,f358]) ).
fof(f1334,plain,
! [X0] :
( ~ sQ56_spl
| ~ ssItem(X0)
| ~ ssList(cons(sk6,nil))
| ~ ssList(sk8)
| ~ memberP(sk8,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1246,f359]) ).
fof(f1335,definition,
! [X0] :
( sQ72_spl
<=> ( ~ ssItem(X0)
| ~ memberP(cons(sk6,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1336,plain,
! [X0] :
( ~ sQ72_spl
| ~ ssItem(X0)
| ~ memberP(cons(sk6,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1335]) ).
fof(f1338,plain,
( ~ sQ56_spl
| ~ sQ28_spl
| ~ sQ7_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f1333,f1335,f531,f779,f1245]) ).
fof(f1339,definition,
! [X0] :
( sQ73_spl
<=> ( ~ ssItem(X0)
| ~ memberP(sk8,X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1342,plain,
( ~ sQ56_spl
| ~ sQ28_spl
| ~ sQ7_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f1334,f1339,f531,f779,f1245]) ).
fof(f1343,plain,
! [X0] :
( ~ sQ72_spl
| ~ memberP(cons(sk6,nil),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1336]) ).
fof(f1346,plain,
( ~ sQ72_spl
| ~ ssItem(sk6)
| ~ ssList(nil)
| memberP(sk3,sk6)
| ~ ssItem(sk6) ),
inference(resolution,[status(thm)],[f1343,f493]) ).
fof(f1348,definition,
( sQ74_spl
<=> memberP(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1349,plain,
( ~ sQ74_spl
| memberP(sk3,sk6) ),
inference(component_clause,[status(thm)],[f1348]) ).
fof(f1351,plain,
( ~ sQ72_spl
| ~ sQ10_spl
| sQ74_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f1346,f1136,f1348,f542,f1335]) ).
fof(f1379,plain,
! [X0] :
( ~ sQ5_spl
| X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ ssItem(sk9)
| ~ ssList(nil)
| ~ memberP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f471,f395]) ).
fof(f1380,definition,
! [X0] :
( sQ78_spl
<=> ( X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1381,plain,
! [X0] :
( ~ sQ78_spl
| X0 = sk9
| memberP(nil,X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(component_clause,[status(thm)],[f1380]) ).
fof(f1383,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ10_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f1379,f1380,f542,f459,f470]) ).
fof(f1384,plain,
! [X0] :
( ~ sQ78_spl
| X0 = sk9
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1381,f274]) ).
fof(f1385,plain,
( ~ sQ74_spl
| ~ sQ78_spl
| sk6 = sk9
| ~ ssItem(sk6) ),
inference(resolution,[status(thm)],[f1384,f1349]) ).
fof(f1386,plain,
( ~ sQ70_spl
| ~ sQ78_spl
| sk5 = sk9
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1384,f1322]) ).
fof(f1388,definition,
( sQ79_spl
<=> sk6 = sk9 ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1389,plain,
( ~ sQ79_spl
| sk6 = sk9 ),
inference(component_clause,[status(thm)],[f1388]) ).
fof(f1391,plain,
( ~ sQ74_spl
| ~ sQ78_spl
| sQ79_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f1385,f1136,f1388,f1380,f1348]) ).
fof(f1392,definition,
( sQ80_spl
<=> sk5 = sk9 ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1393,plain,
( ~ sQ80_spl
| sk5 = sk9 ),
inference(component_clause,[status(thm)],[f1392]) ).
fof(f1395,plain,
( ~ sQ70_spl
| ~ sQ78_spl
| sQ80_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f1386,f1151,f1392,f1380,f1321]) ).
fof(f1410,plain,
( ~ sQ79_spl
| sk5 != sk9 ),
inference(backward_demodulation,[status(thm)],[f1389,f445]) ).
fof(f1427,plain,
( ~ sQ79_spl
| ~ sQ80_spl
| sk9 != sk9 ),
inference(forward_demodulation,[status(thm)],[f1393,f1410]) ).
fof(f1428,plain,
( ~ sQ79_spl
| ~ sQ80_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1427]) ).
fof(f1429,plain,
( ~ sQ79_spl
| ~ sQ80_spl ),
inference(contradiction_clause,[status(thm)],[f1428]) ).
fof(f1655,definition,
( sQ107_spl
<=> sk8 = sk8 ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1657,plain,
( sQ107_spl
| sk8 != sk8 ),
inference(component_clause,[status(thm)],[f1655]) ).
fof(f1659,plain,
( sQ107_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1657]) ).
fof(f1660,plain,
sQ107_spl,
inference(contradiction_clause,[status(thm)],[f1659]) ).
fof(f1702,plain,
( ~ sQ70_spl
| ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| memberP(sk8,sk5) ),
inference(forward_demodulation,[status(thm)],[f967,f1322]) ).
fof(f1743,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ15_spl
| ~ ssItem(X0)
| ~ memberP(sk8,X0) ),
inference(forward_demodulation,[status(thm)],[f964,f516]) ).
fof(f1745,plain,
( ~ sQ70_spl
| ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f1743,f1702]) ).
fof(f1747,plain,
( ~ sQ70_spl
| ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f1745,f1151,f605,f466,f462,f1321]) ).
fof(f1749,plain,
$false,
inference(sat_refutation,[status(thm)],[f465,f469,f473,f478,f545,f586,f595,f608,f636,f751,f788,f792,f797,f802,f806,f810,f863,f879,f883,f899,f909,f952,f1134,f1139,f1141,f1149,f1154,f1156,f1158,f1236,f1240,f1244,f1248,f1252,f1257,f1262,f1266,f1268,f1278,f1284,f1288,f1301,f1305,f1309,f1315,f1319,f1324,f1330,f1338,f1342,f1351,f1383,f1391,f1395,f1429,f1660,f1747]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC192-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n026.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 08:05:52 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.38 % Drodi V4.1.1
% 0.02/0.43 % Refutation found
% 0.02/0.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.02/0.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.02/0.46 % Elapsed time: 0.091706 seconds
% 0.02/0.46 % CPU time: 0.393140 seconds
% 0.02/0.46 % Total memory used: 115.242 MB
% 0.02/0.46 % Net memory used: 114.835 MB
%------------------------------------------------------------------------------