%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC067-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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:39:50 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.41s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 89
% Syntax : Number of formulae : 291 ( 23 unt; 57 def)
% Number of atoms : 961 ( 163 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 1289 ( 619 ~; 613 |; 0 &)
% ( 57 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 65 ( 63 usr; 58 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 194 ( 194 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [U] :
( segmentP(U,nil)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [U] :
( segmentP(U,U)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [U,V] :
( ssItem(V)
| duplicatefreeP(U)
| ~ ssList(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(f79,axiom,
! [U] :
( segmentP(nil,U)
| ~ ssList(U)
| nil != U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,axiom,
! [U,V] :
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [U,V] :
( V = U
| neq(V,U)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,axiom,
! [U,V] :
( strictorderedP(cons(V,U))
| ~ ssItem(V)
| ~ ssList(U)
| nil != U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,axiom,
! [U,V] :
( ~ ssList(U)
| ~ ssList(V)
| ~ neq(U,V)
| U != V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(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(f127,axiom,
! [U,V] :
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ segmentP(V,U)
| ~ segmentP(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(f152,axiom,
! [U,V,W] :
( segmentP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ segmentP(V,W)
| ~ segmentP(U,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(f172,axiom,
! [U,V,W,X] :
( segmentP(app(app(X,U),W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(X)
| ~ ssList(W)
| ~ segmentP(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [U,V,W,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ~ ssList(U)
| ~ ssList(W)
| app(app(U,V),W) != X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f188,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
ssList(sk4),
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,
ssList(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
ssList(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
app(app(sk5,sk3),sk6) = sk4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
( nil != sk3
| nil = sk4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,negated_conjecture,
! [A] :
( ~ segmentP(sk1,A)
| ~ segmentP(sk2,A)
| ~ neq(A,nil)
| ~ ssList(A)
| nil = sk2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f201,negated_conjecture,
( neq(sk2,nil)
| nil != sk1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f210,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f258,plain,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f259,plain,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f274,plain,
( ! [V] : ssItem(V)
| ! [U] :
( duplicatefreeP(U)
| ~ ssList(U) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f275,plain,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f276,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f277,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f282,plain,
! [X0] :
( segmentP(nil,X0)
| ~ ssList(X0)
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f288,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f303,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != V ) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f304,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != X1 ),
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f305,plain,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f319,plain,
! [X0,X1] :
( strictorderedP(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0)
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f323,plain,
! [U] :
( ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ neq(U,V)
| U != V ) ),
inference(miniscoping,[status(thm)],[f115]) ).
fof(f324,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ neq(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f329,plain,
! [U] :
( nil = U
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f330,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f331,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f332,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f342,plain,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X0)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f371,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(f372,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f373,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f374,plain,
! [U,W] :
( U = W
| ~ ssList(W)
| ! [V] :
( ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f375,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f376,plain,
! [U,W] :
( segmentP(U,W)
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| ~ ssList(W)
| ~ segmentP(V,W)
| ~ segmentP(U,V) ) ),
inference(miniscoping,[status(thm)],[f152]) ).
fof(f377,plain,
! [X0,X1,X2] :
( segmentP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(X1,X2)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f386,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(f407,plain,
! [X0,X1,X2,X3] :
( segmentP(app(app(X3,X0),X2),X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f408,plain,
! [V,X] :
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ! [U] :
( ~ ssList(U)
| ! [W] :
( ~ ssList(W)
| app(app(U,V),W) != X ) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f409,plain,
! [X0,X1,X2,X3] :
( segmentP(X3,X1)
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| app(app(X0,X1),X2) != X3 ),
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f435,plain,
ssList(sk3),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f436,plain,
ssList(sk4),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f437,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f438,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f439,plain,
ssList(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f440,plain,
ssList(sk6),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f441,plain,
app(app(sk5,sk3),sk6) = sk4,
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f447,plain,
( nil != sk3
| nil = sk4 ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f449,plain,
! [X0] :
( ~ segmentP(sk1,X0)
| ~ segmentP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0)
| nil = sk2 ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f450,plain,
( neq(sk2,nil)
| nil != sk1 ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f452,definition,
! [X0] :
( sQ0_spl
<=> ( duplicatefreeP(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f453,plain,
! [X0] :
( ~ sQ0_spl
| duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f452]) ).
fof(f455,definition,
! [X1] :
( sQ1_spl
<=> ssItem(X1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f456,plain,
! [X0] :
( ~ sQ1_spl
| ssItem(X0) ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f458,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f275,f452,f455]) ).
fof(f459,definition,
( sQ2_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( ~ sQ2_spl
| nil = sk4 ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,definition,
( sQ3_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f464,plain,
( sQ3_spl
| nil != sk3 ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f447,f459,f462]) ).
fof(f466,definition,
( sQ4_spl
<=> nil = sk2 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( ~ sQ4_spl
| nil = sk2 ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,definition,
( sQ5_spl
<=> neq(sk2,nil) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f470,plain,
( ~ sQ5_spl
| neq(sk2,nil) ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f473,definition,
! [X0] :
( sQ6_spl
<=> ( ~ segmentP(sk1,X0)
| ~ segmentP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f474,plain,
! [X0] :
( ~ sQ6_spl
| ~ segmentP(sk1,X0)
| ~ segmentP(sk2,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f476,plain,
( sQ6_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f449,f466,f473]) ).
fof(f477,definition,
( sQ7_spl
<=> nil = sk1 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f479,plain,
( sQ7_spl
| nil != sk1 ),
inference(component_clause,[status(thm)],[f477]) ).
fof(f480,plain,
( sQ5_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f450,f477,f469]) ).
fof(f482,plain,
( segmentP(nil,nil)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f282]) ).
fof(f487,plain,
! [X0] :
( strictorderedP(cons(X0,nil))
| ~ ssItem(X0)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f319]) ).
fof(f489,plain,
! [X1] :
( ~ ssList(X1)
| ~ ssList(X1)
| ~ neq(X1,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f324]) ).
fof(f490,plain,
! [X0] :
( ~ ssList(X0)
| ~ neq(X0,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f489]) ).
fof(f500,plain,
! [X0,X1,X2] :
( segmentP(app(app(X1,X2),X0),X2)
| ~ ssList(app(app(X1,X2),X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f409]) ).
fof(f513,plain,
( sQ7_spl
| nil != sk3 ),
inference(forward_demodulation,[status(thm)],[f438,f479]) ).
fof(f517,plain,
( ~ sQ4_spl
| nil = sk4 ),
inference(forward_demodulation,[status(thm)],[f437,f467]) ).
fof(f540,definition,
( sQ8_spl
<=> ssList(sk4) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f548,plain,
( ~ sQ5_spl
| neq(sk4,nil) ),
inference(forward_demodulation,[status(thm)],[f437,f470]) ).
fof(f549,plain,
! [X0] :
( ~ sQ6_spl
| ~ segmentP(sk1,X0)
| ~ segmentP(sk4,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f437,f474]) ).
fof(f550,plain,
! [X0] :
( ~ sQ6_spl
| ~ segmentP(sk3,X0)
| ~ segmentP(sk4,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f438,f549]) ).
fof(f551,definition,
( sQ10_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f553,plain,
( sQ10_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f551]) ).
fof(f554,definition,
( sQ11_spl
<=> segmentP(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( ~ sQ11_spl
| segmentP(nil,nil) ),
inference(component_clause,[status(thm)],[f554]) ).
fof(f557,plain,
( sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f482,f551,f554]) ).
fof(f562,definition,
( sQ12_spl
<=> ssList(sk6) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f564,plain,
( sQ12_spl
| ~ ssList(sk6) ),
inference(component_clause,[status(thm)],[f562]) ).
fof(f565,definition,
( sQ13_spl
<=> ssList(app(sk5,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f567,plain,
( sQ13_spl
| ~ ssList(app(sk5,sk3)) ),
inference(component_clause,[status(thm)],[f565]) ).
fof(f569,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f564,f440]) ).
fof(f570,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f569]) ).
fof(f581,plain,
( sQ13_spl
| ~ ssList(sk5)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f567,f288]) ).
fof(f582,definition,
( sQ14_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f584,plain,
( sQ14_spl
| ~ ssList(sk3) ),
inference(component_clause,[status(thm)],[f582]) ).
fof(f585,definition,
( sQ15_spl
<=> ssList(sk5) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f587,plain,
( sQ15_spl
| ~ ssList(sk5) ),
inference(component_clause,[status(thm)],[f585]) ).
fof(f588,plain,
( sQ13_spl
| ~ sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f581,f582,f585,f565]) ).
fof(f589,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f584,f435]) ).
fof(f590,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f589]) ).
fof(f591,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f587,f439]) ).
fof(f592,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f591]) ).
fof(f594,plain,
( ~ sQ6_spl
| ~ ssList(sk3)
| ~ segmentP(sk4,sk3)
| ~ neq(sk3,nil)
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f550,f259]) ).
fof(f598,definition,
( sQ17_spl
<=> segmentP(sk3,sk4) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f599,plain,
( ~ sQ17_spl
| segmentP(sk3,sk4) ),
inference(component_clause,[status(thm)],[f598]) ).
fof(f600,plain,
( sQ17_spl
| ~ segmentP(sk3,sk4) ),
inference(component_clause,[status(thm)],[f598]) ).
fof(f602,definition,
( sQ18_spl
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f604,plain,
( sQ18_spl
| ~ neq(sk3,nil) ),
inference(component_clause,[status(thm)],[f602]) ).
fof(f605,definition,
( sQ19_spl
<=> segmentP(sk4,sk3) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f606,plain,
( ~ sQ19_spl
| segmentP(sk4,sk3) ),
inference(component_clause,[status(thm)],[f605]) ).
fof(f608,plain,
( ~ sQ6_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f594,f582,f602,f605,f473]) ).
fof(f609,plain,
( ~ sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f517,f459,f466]) ).
fof(f614,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| neq(sk4,sk4) ),
inference(backward_demodulation,[status(thm)],[f460,f548]) ).
fof(f625,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f614,f490]) ).
fof(f626,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f625,f436]) ).
fof(f627,plain,
( ~ sQ5_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f626]) ).
fof(f634,plain,
! [X0] :
( ~ sQ2_spl
| segmentP(X0,sk4)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f460,f258]) ).
fof(f635,plain,
( sQ17_spl
| ~ sQ2_spl
| ~ ssList(sk3) ),
inference(resolution,[status(thm)],[f634,f600]) ).
fof(f636,plain,
( sQ17_spl
| ~ sQ2_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f635,f582,f459,f598]) ).
fof(f638,plain,
( sQ18_spl
| sk3 = nil
| ~ ssList(sk3)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f305,f604]) ).
fof(f642,plain,
( sQ18_spl
| sQ3_spl
| ~ sQ14_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f638,f551,f582,f462,f602]) ).
fof(f644,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f553,f210]) ).
fof(f645,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f644]) ).
fof(f646,plain,
( sQ7_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f513,f462,f477]) ).
fof(f699,definition,
! [X0] :
( sQ23_spl
<=> ( strictorderedP(cons(X0,nil))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f702,plain,
( sQ23_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f487,f551,f699]) ).
fof(f712,definition,
( sQ25_spl
<=> segmentP(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f713,plain,
( ~ sQ25_spl
| segmentP(sk4,nil) ),
inference(component_clause,[status(thm)],[f712]) ).
fof(f714,plain,
( sQ25_spl
| ~ segmentP(sk4,nil) ),
inference(component_clause,[status(thm)],[f712]) ).
fof(f722,definition,
( sQ27_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f727,plain,
( sQ25_spl
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f714,f258]) ).
fof(f728,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f727,f436]) ).
fof(f729,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f728]) ).
fof(f738,plain,
( nil = sk6
| ~ ssList(app(sk5,sk3))
| ~ ssList(sk6)
| sk4 != nil ),
inference(paramodulation,[status(thm)],[f441,f332]) ).
fof(f741,definition,
( sQ28_spl
<=> nil = sk6 ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f742,plain,
( ~ sQ28_spl
| nil = sk6 ),
inference(component_clause,[status(thm)],[f741]) ).
fof(f744,plain,
( sQ28_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f738,f459,f562,f565,f741]) ).
fof(f770,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ ssList(X0)
| ~ ssList(X1)
| duplicatefreeP(app(X0,X1)) ),
inference(resolution,[status(thm)],[f453,f288]) ).
fof(f786,plain,
( ~ sQ0_spl
| ~ ssList(app(sk5,sk3))
| ~ ssList(sk6)
| duplicatefreeP(sk4) ),
inference(paramodulation,[status(thm)],[f441,f770]) ).
fof(f787,definition,
( sQ29_spl
<=> duplicatefreeP(sk4) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f790,plain,
( ~ sQ0_spl
| ~ sQ13_spl
| ~ sQ12_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f786,f787,f562,f565,f452]) ).
fof(f801,plain,
( ~ sQ11_spl
| nil = nil
| ~ ssList(nil)
| ~ ssList(nil)
| ~ segmentP(nil,nil) ),
inference(resolution,[status(thm)],[f342,f555]) ).
fof(f802,plain,
! [X0] :
( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ ssList(nil)
| ~ segmentP(nil,X0) ),
inference(resolution,[status(thm)],[f342,f258]) ).
fof(f808,plain,
( sQ27_spl
| ~ sQ10_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f801,f554,f551,f722]) ).
fof(f809,definition,
! [X0] :
( sQ32_spl
<=> ( ~ ssList(X0)
| X0 = nil
| ~ ssList(X0)
| ~ segmentP(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f812,plain,
( ~ sQ10_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f802,f809,f551]) ).
fof(f839,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ ssList(X1)
| cons(X0,X1) != X1 ),
inference(backward_subsumption_resolution,[status(thm)],[f304,f456]) ).
fof(f866,plain,
! [X0] :
( ~ ssList(app(nil,X0))
| app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(nil,X0)) ),
inference(resolution,[status(thm)],[f373,f277]) ).
fof(f868,plain,
! [X0] :
( sk6 = X0
| ~ ssList(X0)
| ~ ssList(app(sk5,sk3))
| ~ ssList(sk6)
| sk4 != app(app(sk5,sk3),X0) ),
inference(paramodulation,[status(thm)],[f441,f373]) ).
fof(f871,definition,
! [X0] :
( sQ37_spl
<=> ( ~ ssList(app(nil,X0))
| app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f874,plain,
( ~ sQ10_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f866,f871,f551]) ).
fof(f876,definition,
! [X0] :
( sQ38_spl
<=> ( sk6 = X0
| ~ ssList(X0)
| sk4 != app(app(sk5,sk3),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f877,plain,
! [X0] :
( ~ sQ38_spl
| sk6 = X0
| ~ ssList(X0)
| sk4 != app(app(sk5,sk3),X0) ),
inference(component_clause,[status(thm)],[f876]) ).
fof(f879,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f868,f876,f562,f565]) ).
fof(f889,plain,
( ~ sQ38_spl
| sk6 = sk6
| ~ ssList(sk6) ),
inference(resolution,[status(thm)],[f877,f441]) ).
fof(f891,definition,
( sQ41_spl
<=> sk6 = sk6 ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f894,plain,
( ~ sQ38_spl
| sQ41_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f889,f562,f891,f876]) ).
fof(f896,plain,
! [X0] :
( ~ ssList(app(X0,nil))
| app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(X0,nil)) ),
inference(resolution,[status(thm)],[f375,f276]) ).
fof(f898,plain,
! [X0] :
( app(sk5,sk3) = X0
| ~ ssList(X0)
| ~ ssList(sk6)
| ~ ssList(app(sk5,sk3))
| sk4 != app(X0,sk6) ),
inference(paramodulation,[status(thm)],[f441,f375]) ).
fof(f901,definition,
! [X0] :
( sQ42_spl
<=> ( ~ ssList(app(X0,nil))
| app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(app(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f904,plain,
( ~ sQ10_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f896,f901,f551]) ).
fof(f906,definition,
! [X0] :
( sQ43_spl
<=> ( app(sk5,sk3) = X0
| ~ ssList(X0)
| sk4 != app(X0,sk6) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f907,plain,
! [X0] :
( ~ sQ43_spl
| app(sk5,sk3) = X0
| ~ ssList(X0)
| sk4 != app(X0,sk6) ),
inference(component_clause,[status(thm)],[f906]) ).
fof(f909,plain,
( ~ sQ12_spl
| ~ sQ13_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f898,f906,f565,f562]) ).
fof(f913,plain,
! [X0] :
( ~ sQ43_spl
| sk5 = X0
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(sk5)
| ~ ssList(app(X0,sk3))
| sk4 != app(app(X0,sk3),sk6) ),
inference(resolution,[status(thm)],[f907,f375]) ).
fof(f914,plain,
! [X0] :
( ~ sQ43_spl
| sk3 = X0
| ~ ssList(X0)
| ~ ssList(sk5)
| ~ ssList(sk3)
| ~ ssList(app(sk5,X0))
| sk4 != app(app(sk5,X0),sk6) ),
inference(resolution,[status(thm)],[f907,f373]) ).
fof(f916,plain,
( ~ sQ43_spl
| nil = sk3
| ~ ssList(sk5)
| ~ ssList(sk3)
| ~ ssList(nil)
| sk4 != app(nil,sk6) ),
inference(resolution,[status(thm)],[f907,f332]) ).
fof(f917,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ43_spl
| ~ ssList(app(sk5,sk3))
| ~ ssList(cons(X0,app(sk5,sk3)))
| sk4 != app(cons(X0,app(sk5,sk3)),sk6) ),
inference(resolution,[status(thm)],[f907,f839]) ).
fof(f920,definition,
! [X0] :
( sQ44_spl
<=> ( sk5 = X0
| ~ ssList(X0)
| ~ ssList(app(X0,sk3))
| sk4 != app(app(X0,sk3),sk6) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f923,plain,
( ~ sQ43_spl
| ~ sQ14_spl
| ~ sQ15_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f913,f920,f585,f582,f906]) ).
fof(f924,definition,
! [X0] :
( sQ45_spl
<=> ( sk3 = X0
| ~ ssList(X0)
| ~ ssList(app(sk5,X0))
| sk4 != app(app(sk5,X0),sk6) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f925,plain,
! [X0] :
( ~ sQ45_spl
| sk3 = X0
| ~ ssList(X0)
| ~ ssList(app(sk5,X0))
| sk4 != app(app(sk5,X0),sk6) ),
inference(component_clause,[status(thm)],[f924]) ).
fof(f927,plain,
( ~ sQ43_spl
| ~ sQ15_spl
| ~ sQ14_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f914,f924,f582,f585,f906]) ).
fof(f928,definition,
( sQ46_spl
<=> sk4 = app(nil,sk6) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f931,definition,
( sQ47_spl
<=> nil = sk5 ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f935,plain,
( ~ sQ43_spl
| sQ3_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ10_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f916,f928,f551,f582,f585,f462,f906]) ).
fof(f936,definition,
! [X0] :
( sQ48_spl
<=> ( ~ ssList(cons(X0,app(sk5,sk3)))
| sk4 != app(cons(X0,app(sk5,sk3)),sk6) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f939,plain,
( ~ sQ1_spl
| ~ sQ43_spl
| ~ sQ13_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f917,f936,f565,f906,f455]) ).
fof(f942,plain,
( sk4 = app(sk5,app(sk3,sk6))
| ~ ssList(sk5)
| ~ ssList(sk3)
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f441,f371]) ).
fof(f943,plain,
! [X0] :
( app(sk4,X0) = app(app(sk5,sk3),app(sk6,X0))
| ~ ssList(app(sk5,sk3))
| ~ ssList(sk6)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f441,f371]) ).
fof(f944,definition,
( sQ49_spl
<=> sk4 = app(sk5,app(sk3,sk6)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f945,plain,
( ~ sQ49_spl
| sk4 = app(sk5,app(sk3,sk6)) ),
inference(component_clause,[status(thm)],[f944]) ).
fof(f947,plain,
( sQ49_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f942,f562,f582,f585,f944]) ).
fof(f948,definition,
! [X0] :
( sQ50_spl
<=> ( app(sk4,X0) = app(app(sk5,sk3),app(sk6,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f951,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f943,f948,f562,f565]) ).
fof(f952,plain,
! [X0] :
( ~ sQ25_spl
| segmentP(X0,nil)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ ssList(nil)
| ~ segmentP(X0,sk4) ),
inference(resolution,[status(thm)],[f377,f713]) ).
fof(f953,plain,
! [X0] :
( ~ sQ11_spl
| segmentP(X0,nil)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ segmentP(X0,nil) ),
inference(resolution,[status(thm)],[f377,f555]) ).
fof(f954,plain,
! [X0,X1] :
( ~ ssList(X1)
| segmentP(X0,nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ segmentP(X0,X1) ),
inference(resolution,[status(thm)],[f377,f258]) ).
fof(f956,definition,
! [X0] :
( sQ51_spl
<=> ( segmentP(X0,nil)
| ~ ssList(X0)
| ~ segmentP(X0,sk4) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f959,plain,
( ~ sQ25_spl
| ~ sQ8_spl
| ~ sQ10_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f952,f956,f551,f540,f712]) ).
fof(f960,definition,
! [X0] :
( sQ52_spl
<=> ( segmentP(X0,nil)
| ~ ssList(X0)
| ~ segmentP(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f963,plain,
( ~ sQ11_spl
| ~ sQ10_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f953,f960,f551,f554]) ).
fof(f964,definition,
! [X0,X1] :
( sQ53_spl
<=> ( ~ ssList(X1)
| segmentP(X0,nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f967,plain,
( ~ sQ10_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f954,f964,f551]) ).
fof(f969,plain,
! [X0] :
( ~ sQ49_spl
| app(sk4,X0) = app(sk5,app(app(sk3,sk6),X0))
| ~ ssList(sk5)
| ~ ssList(app(sk3,sk6))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f945,f371]) ).
fof(f970,plain,
! [X0] :
( ~ sQ49_spl
| X0 = sk5
| ~ ssList(sk5)
| ~ ssList(app(sk3,sk6))
| ~ ssList(X0)
| app(X0,app(sk3,sk6)) != sk4 ),
inference(paramodulation,[status(thm)],[f945,f375]) ).
fof(f972,plain,
! [X0] :
( ~ sQ49_spl
| X0 = app(sk3,sk6)
| ~ ssList(app(sk3,sk6))
| ~ ssList(sk5)
| ~ ssList(X0)
| app(sk5,X0) != sk4 ),
inference(paramodulation,[status(thm)],[f945,f373]) ).
fof(f974,plain,
( ~ sQ49_spl
| nil = sk5
| ~ ssList(sk5)
| ~ ssList(app(sk3,sk6))
| sk4 != nil ),
inference(paramodulation,[status(thm)],[f945,f330]) ).
fof(f976,plain,
( ~ sQ49_spl
| ssList(sk4)
| ~ ssList(sk5)
| ~ ssList(app(sk3,sk6)) ),
inference(paramodulation,[status(thm)],[f945,f288]) ).
fof(f977,definition,
! [X0] :
( sQ54_spl
<=> ( app(sk4,X0) = app(sk5,app(app(sk3,sk6),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f980,definition,
( sQ55_spl
<=> ssList(app(sk3,sk6)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f982,plain,
( sQ55_spl
| ~ ssList(app(sk3,sk6)) ),
inference(component_clause,[status(thm)],[f980]) ).
fof(f983,plain,
( ~ sQ49_spl
| ~ sQ15_spl
| ~ sQ55_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f969,f977,f980,f585,f944]) ).
fof(f984,definition,
! [X0] :
( sQ56_spl
<=> ( X0 = sk5
| ~ ssList(X0)
| app(X0,app(sk3,sk6)) != sk4 ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f985,plain,
! [X0] :
( ~ sQ56_spl
| X0 = sk5
| ~ ssList(X0)
| app(X0,app(sk3,sk6)) != sk4 ),
inference(component_clause,[status(thm)],[f984]) ).
fof(f987,plain,
( ~ sQ49_spl
| ~ sQ15_spl
| ~ sQ55_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f970,f984,f980,f585,f944]) ).
fof(f989,definition,
! [X0] :
( sQ57_spl
<=> ( X0 = app(sk3,sk6)
| ~ ssList(X0)
| app(sk5,X0) != sk4 ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f990,plain,
! [X0] :
( ~ sQ57_spl
| X0 = app(sk3,sk6)
| ~ ssList(X0)
| app(sk5,X0) != sk4 ),
inference(component_clause,[status(thm)],[f989]) ).
fof(f992,plain,
( ~ sQ49_spl
| ~ sQ55_spl
| ~ sQ15_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f972,f989,f585,f980,f944]) ).
fof(f994,plain,
( ~ sQ49_spl
| sQ47_spl
| ~ sQ15_spl
| ~ sQ55_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f974,f459,f980,f585,f931,f944]) ).
fof(f999,plain,
( ~ sQ49_spl
| sQ8_spl
| ~ sQ15_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f976,f980,f585,f540,f944]) ).
fof(f1000,plain,
( sQ55_spl
| ~ ssList(sk3)
| ~ ssList(sk6) ),
inference(resolution,[status(thm)],[f982,f288]) ).
fof(f1001,plain,
( sQ55_spl
| ~ sQ14_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1000,f562,f582,f980]) ).
fof(f1002,plain,
! [X0] :
( ~ sQ43_spl
| ~ ssList(cons(X0,app(sk5,sk3)))
| sk4 != app(cons(X0,app(sk5,sk3)),sk6)
| ~ ssList(app(sk5,sk3))
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f304,f907]) ).
fof(f1003,definition,
! [X0] :
( sQ59_spl
<=> ( ~ ssList(cons(X0,app(sk5,sk3)))
| sk4 != app(cons(X0,app(sk5,sk3)),sk6)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1006,plain,
( ~ sQ43_spl
| ~ sQ13_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1002,f1003,f565,f906]) ).
fof(f1019,plain,
! [X0] :
( ~ sQ49_spl
| cons(X0,sk4) = app(cons(X0,sk5),app(sk3,sk6))
| ~ ssList(app(sk3,sk6))
| ~ ssList(sk5)
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f945,f386]) ).
fof(f1020,plain,
! [X0] :
( cons(X0,sk4) = app(cons(X0,app(sk5,sk3)),sk6)
| ~ ssList(sk6)
| ~ ssList(app(sk5,sk3))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f441,f386]) ).
fof(f1021,definition,
! [X0] :
( sQ60_spl
<=> ( cons(X0,sk4) = app(cons(X0,sk5),app(sk3,sk6))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1024,plain,
( ~ sQ49_spl
| ~ sQ55_spl
| ~ sQ15_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1019,f1021,f585,f980,f944]) ).
fof(f1025,definition,
! [X0] :
( sQ61_spl
<=> ( cons(X0,sk4) = app(cons(X0,app(sk5,sk3)),sk6)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1028,plain,
( ~ sQ12_spl
| ~ sQ13_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f1020,f1025,f565,f562]) ).
fof(f1029,plain,
( ~ sQ49_spl
| ~ sQ56_spl
| sk5 = sk5
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f985,f945]) ).
fof(f1031,definition,
( sQ62_spl
<=> sk5 = sk5 ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1034,plain,
( ~ sQ49_spl
| ~ sQ56_spl
| sQ62_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1029,f585,f1031,f984,f944]) ).
fof(f1036,plain,
! [X0] :
( ~ sQ57_spl
| ~ ssList(app(sk3,sk6))
| ~ ssItem(X0)
| ~ ssList(cons(X0,app(sk3,sk6)))
| app(sk5,cons(X0,app(sk3,sk6))) != sk4 ),
inference(resolution,[status(thm)],[f990,f304]) ).
fof(f1037,plain,
! [X0] :
( ~ sQ57_spl
| X0 = sk3
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ ssList(app(X0,sk6))
| app(sk5,app(X0,sk6)) != sk4 ),
inference(resolution,[status(thm)],[f990,f375]) ).
fof(f1038,plain,
! [X0] :
( ~ sQ57_spl
| X0 = sk6
| ~ ssList(sk6)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(app(sk3,X0))
| app(sk5,app(sk3,X0)) != sk4 ),
inference(resolution,[status(thm)],[f990,f373]) ).
fof(f1043,definition,
! [X0] :
( sQ63_spl
<=> ( ~ ssItem(X0)
| ~ ssList(cons(X0,app(sk3,sk6)))
| app(sk5,cons(X0,app(sk3,sk6))) != sk4 ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1046,plain,
( ~ sQ57_spl
| ~ sQ55_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1036,f1043,f980,f989]) ).
fof(f1047,definition,
! [X0] :
( sQ64_spl
<=> ( X0 = sk3
| ~ ssList(X0)
| ~ ssList(app(X0,sk6))
| app(sk5,app(X0,sk6)) != sk4 ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1050,plain,
( ~ sQ57_spl
| ~ sQ14_spl
| ~ sQ12_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1037,f1047,f562,f582,f989]) ).
fof(f1051,definition,
! [X0] :
( sQ65_spl
<=> ( X0 = sk6
| ~ ssList(X0)
| ~ ssList(app(sk3,X0))
| app(sk5,app(sk3,X0)) != sk4 ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1054,plain,
( ~ sQ57_spl
| ~ sQ12_spl
| ~ sQ14_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1038,f1051,f582,f562,f989]) ).
fof(f1121,plain,
( ~ sQ45_spl
| sk3 = sk3
| ~ ssList(sk3)
| ~ ssList(app(sk5,sk3)) ),
inference(resolution,[status(thm)],[f925,f441]) ).
fof(f1124,definition,
( sQ69_spl
<=> sk3 = sk3 ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1127,plain,
( ~ sQ45_spl
| sQ69_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1121,f565,f582,f1124,f924]) ).
fof(f1180,plain,
( sQ3_spl
| ~ sQ28_spl
| sk6 != sk3 ),
inference(backward_demodulation,[status(thm)],[f742,f464]) ).
fof(f1246,plain,
( segmentP(sk4,sk3)
| ~ ssList(app(app(sk5,sk3),sk6))
| ~ ssList(sk3)
| ~ ssList(sk5)
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f441,f500]) ).
fof(f1247,plain,
! [X0] :
( segmentP(sk4,X0)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(sk5)
| ~ ssList(sk6)
| ~ segmentP(sk3,X0) ),
inference(paramodulation,[status(thm)],[f441,f407]) ).
fof(f1249,plain,
! [X0] :
( segmentP(app(sk4,X0),sk6)
| ~ ssList(app(app(app(sk5,sk3),sk6),X0))
| ~ ssList(sk6)
| ~ ssList(app(sk5,sk3))
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f441,f500]) ).
fof(f1250,plain,
! [X0,X1] :
( segmentP(app(sk4,X1),X0)
| ~ ssList(sk6)
| ~ ssList(X0)
| ~ ssList(app(sk5,sk3))
| ~ ssList(X1)
| ~ segmentP(sk6,X0) ),
inference(paramodulation,[status(thm)],[f441,f407]) ).
fof(f1259,definition,
( sQ74_spl
<=> ssList(app(app(sk5,sk3),sk6)) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1261,plain,
( sQ74_spl
| ~ ssList(app(app(sk5,sk3),sk6)) ),
inference(component_clause,[status(thm)],[f1259]) ).
fof(f1262,plain,
( sQ19_spl
| ~ sQ74_spl
| ~ sQ14_spl
| ~ sQ15_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1246,f562,f585,f582,f1259,f605]) ).
fof(f1263,definition,
! [X0] :
( sQ75_spl
<=> ( segmentP(sk4,X0)
| ~ ssList(X0)
| ~ segmentP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1266,plain,
( ~ sQ14_spl
| ~ sQ15_spl
| ~ sQ12_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f1247,f1263,f562,f585,f582]) ).
fof(f1268,definition,
! [X0] :
( sQ76_spl
<=> ( segmentP(app(sk4,X0),sk6)
| ~ ssList(app(app(app(sk5,sk3),sk6),X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1271,plain,
( ~ sQ12_spl
| ~ sQ13_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f1249,f1268,f565,f562]) ).
fof(f1272,definition,
! [X0,X1] :
( sQ77_spl
<=> ( segmentP(app(sk4,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ segmentP(sk6,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1275,plain,
( ~ sQ12_spl
| ~ sQ13_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f1250,f1272,f565,f562]) ).
fof(f1285,plain,
( sQ74_spl
| ~ ssList(sk4) ),
inference(forward_demodulation,[status(thm)],[f441,f1261]) ).
fof(f1286,plain,
( sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1285,f436]) ).
fof(f1287,plain,
sQ74_spl,
inference(contradiction_clause,[status(thm)],[f1286]) ).
fof(f1320,plain,
( ~ sQ28_spl
| ~ sQ2_spl
| sk4 = sk6 ),
inference(forward_demodulation,[status(thm)],[f460,f742]) ).
fof(f1394,plain,
( ~ sQ19_spl
| ~ sQ28_spl
| ~ sQ2_spl
| segmentP(sk6,sk3) ),
inference(forward_demodulation,[status(thm)],[f1320,f606]) ).
fof(f1404,definition,
( sQ83_spl
<=> sk6 = sk3 ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1405,plain,
( ~ sQ83_spl
| sk6 = sk3 ),
inference(component_clause,[status(thm)],[f1404]) ).
fof(f1408,plain,
( ~ sQ83_spl
| sQ3_spl
| ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1405,f1180]) ).
fof(f1409,plain,
( ~ sQ83_spl
| sQ3_spl
| ~ sQ28_spl ),
inference(contradiction_clause,[status(thm)],[f1408]) ).
fof(f1410,plain,
( ~ sQ17_spl
| ~ sQ28_spl
| ~ sQ2_spl
| segmentP(sk3,sk6) ),
inference(forward_demodulation,[status(thm)],[f1320,f599]) ).
fof(f1415,plain,
( ~ sQ17_spl
| ~ sQ28_spl
| ~ sQ2_spl
| sk3 = sk6
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ segmentP(sk6,sk3) ),
inference(resolution,[status(thm)],[f1410,f342]) ).
fof(f1420,definition,
( sQ85_spl
<=> segmentP(sk6,sk3) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1422,plain,
( sQ85_spl
| ~ segmentP(sk6,sk3) ),
inference(component_clause,[status(thm)],[f1420]) ).
fof(f1423,plain,
( ~ sQ17_spl
| ~ sQ28_spl
| ~ sQ2_spl
| sQ83_spl
| ~ sQ14_spl
| ~ sQ12_spl
| ~ sQ85_spl ),
inference(split_clause,[status(thm)],[f1415,f1420,f562,f582,f1404,f459,f741,f598]) ).
fof(f1424,plain,
( sQ85_spl
| ~ sQ19_spl
| ~ sQ28_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1422,f1394]) ).
fof(f1425,plain,
( sQ85_spl
| ~ sQ19_spl
| ~ sQ28_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1424]) ).
fof(f1426,plain,
$false,
inference(sat_refutation,[status(thm)],[f458,f465,f476,f480,f557,f570,f588,f590,f592,f608,f609,f627,f636,f642,f645,f646,f702,f729,f744,f790,f808,f812,f874,f879,f894,f904,f909,f923,f927,f935,f939,f947,f951,f959,f963,f967,f983,f987,f992,f994,f999,f1001,f1006,f1024,f1028,f1034,f1046,f1050,f1054,f1127,f1262,f1266,f1271,f1275,f1287,f1409,f1423,f1425]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC067-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 07:53:12 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.41 % Refutation found
% 0.12/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.45 % Elapsed time: 0.081341 seconds
% 0.12/0.45 % CPU time: 0.276638 seconds
% 0.12/0.45 % Total memory used: 111.677 MB
% 0.12/0.45 % Net memory used: 111.460 MB
%------------------------------------------------------------------------------