%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC310-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 : n015.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:44 PM UTC 2026
% Result : Unsatisfiable 0.10s 0.42s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 79
% Syntax : Number of formulae : 271 ( 16 unt; 46 def)
% Number of atoms : 828 ( 189 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 1061 ( 504 ~; 511 |; 0 &)
% ( 46 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 54 ( 52 usr; 47 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-2 aty)
% Number of variables : 168 ( 168 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
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(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(f97,axiom,
! [U,V] :
( hd(cons(U,V)) = U
| ~ 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(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(f113,axiom,
! [U,V] :
( totalorderedP(cons(V,U))
| ~ ssItem(V)
| ~ ssList(U)
| nil != U ),
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(f120,axiom,
! [U,V] :
( app(cons(U,nil),V) = cons(U,V)
| ~ ssList(V)
| ~ ssItem(U) ),
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(f145,axiom,
! [U,V] :
( app(U,V) = nil
| ~ ssList(U)
| ~ ssList(V)
| nil != V
| nil != 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(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(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,
( nil != sk4
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
( ~ neq(sk4,nil)
| ssItem(sk5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
( ~ neq(sk4,nil)
| ssList(sk6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
( ~ neq(sk4,nil)
| app(cons(sk5,nil),sk6) = sk4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
( ~ neq(sk4,nil)
| app(sk6,cons(sk5,nil)) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
( neq(sk2,nil)
| nil = sk2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
! [A,B,C,D] :
( ~ neq(nil,sk2)
| ~ neq(nil,sk2)
| hd(sk2) != D
| cons(D,nil) != C
| ~ ssItem(D)
| app(B,C) != A
| tl(sk2) != B
| ~ ssList(C)
| ~ ssList(B)
| sk1 != A
| ~ ssList(A)
| nil = sk2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
( neq(sk2,nil)
| nil != sk1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f208,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f272,plain,
( ! [V] : ssItem(V)
| ! [U] :
( duplicatefreeP(U)
| ~ ssList(U) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f273,plain,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f274,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f275,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f277,plain,
! [X0] :
( nil = X0
| ssItem(hd(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f286,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f287,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f297,plain,
! [X0,X1] :
( tl(cons(X0,X1)) = X1
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f298,plain,
! [X0,X1] :
( hd(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f301,plain,
! [V] :
( ~ ssList(V)
| ! [U] :
( ~ ssItem(U)
| cons(U,V) != V ) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f302,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != X1 ),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f303,plain,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f317,plain,
! [X0,X1] :
( strictorderedP(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0)
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f318,plain,
! [X0,X1] :
( totalorderedP(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0)
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f329,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f330,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f331,plain,
! [X0,X1] :
( app(cons(X0,nil),X1) = cons(X0,X1)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f334,plain,
! [X0,X1] :
( hd(app(X1,X0)) = hd(X1)
| nil = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f362,plain,
! [X0,X1] :
( app(X0,X1) = nil
| ~ ssList(X0)
| ~ ssList(X1)
| nil != X1
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f370,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f371,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f372,plain,
! [U,W] :
( U = W
| ~ ssList(W)
| ! [V] :
( ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f373,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f384,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(f401,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(f402,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)],[f401]) ).
fof(f433,plain,
ssList(sk3),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f434,plain,
ssList(sk4),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f435,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f436,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f437,plain,
( nil != sk4
| nil = sk3 ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f438,plain,
( ~ neq(sk4,nil)
| ssItem(sk5) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f439,plain,
( ~ neq(sk4,nil)
| ssList(sk6) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f440,plain,
( ~ neq(sk4,nil)
| app(cons(sk5,nil),sk6) = sk4 ),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f441,plain,
( ~ neq(sk4,nil)
| app(sk6,cons(sk5,nil)) = sk3 ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f442,plain,
( neq(sk2,nil)
| nil = sk2 ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f443,plain,
( ~ neq(nil,sk2)
| ~ neq(nil,sk2)
| ! [D] :
( hd(sk2) != D
| ! [C] :
( cons(D,nil) != C
| ~ ssItem(D)
| ! [A,B] :
( app(B,C) != A
| tl(sk2) != B
| ~ ssList(C)
| ~ ssList(B)
| sk1 != A
| ~ ssList(A)
| nil = sk2 ) ) ) ),
inference(miniscoping,[status(thm)],[f198]) ).
fof(f444,plain,
! [X0,X1,X2,X3] :
( ~ neq(nil,sk2)
| ~ neq(nil,sk2)
| hd(sk2) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk2) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk1 != X0
| ~ ssList(X0)
| nil = sk2 ),
inference(cnf_transformation,[status(thm)],[f443]) ).
fof(f445,plain,
( neq(sk2,nil)
| nil != sk1 ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f448,definition,
! [X0] :
( sQ0_spl
<=> ( duplicatefreeP(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f449,plain,
! [X0] :
( ~ sQ0_spl
| duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f451,definition,
! [X1] :
( sQ1_spl
<=> ssItem(X1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f452,plain,
! [X0] :
( ~ sQ1_spl
| ssItem(X0) ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f273,f448,f451]) ).
fof(f455,definition,
( sQ2_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f456,plain,
( ~ sQ2_spl
| nil = sk3 ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f458,definition,
( sQ3_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( sQ3_spl
| nil != sk4 ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f437,f455,f458]) ).
fof(f462,definition,
( sQ4_spl
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f465,definition,
( sQ5_spl
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( sQ5_spl
| ~ neq(sk4,nil) ),
inference(component_clause,[status(thm)],[f465]) ).
fof(f468,plain,
( ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f438,f462,f465]) ).
fof(f469,definition,
( sQ6_spl
<=> ssList(sk6) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f470,plain,
( ~ sQ6_spl
| ssList(sk6) ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f472,plain,
( ~ sQ5_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f439,f469,f465]) ).
fof(f473,definition,
( sQ7_spl
<=> app(cons(sk5,nil),sk6) = sk4 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( ~ sQ7_spl
| app(cons(sk5,nil),sk6) = sk4 ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f476,plain,
( ~ sQ5_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f440,f473,f465]) ).
fof(f477,definition,
( sQ8_spl
<=> app(sk6,cons(sk5,nil)) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f478,plain,
( ~ sQ8_spl
| app(sk6,cons(sk5,nil)) = sk3 ),
inference(component_clause,[status(thm)],[f477]) ).
fof(f480,plain,
( ~ sQ5_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f441,f477,f465]) ).
fof(f481,definition,
( sQ9_spl
<=> nil = sk2 ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f482,plain,
( ~ sQ9_spl
| nil = sk2 ),
inference(component_clause,[status(thm)],[f481]) ).
fof(f484,definition,
( sQ10_spl
<=> neq(sk2,nil) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f485,plain,
( ~ sQ10_spl
| neq(sk2,nil) ),
inference(component_clause,[status(thm)],[f484]) ).
fof(f487,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f442,f481,f484]) ).
fof(f488,definition,
! [X0,X1,X2,X3] :
( sQ11_spl
<=> ( hd(sk2) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk2) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk1 != X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f489,plain,
! [X0,X1,X2,X3] :
( ~ sQ11_spl
| hd(sk2) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk2) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk1 != X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f488]) ).
fof(f491,definition,
( sQ12_spl
<=> neq(nil,sk2) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( sQ12_spl
| ~ neq(nil,sk2) ),
inference(component_clause,[status(thm)],[f491]) ).
fof(f494,plain,
( ~ sQ12_spl
| sQ11_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f444,f481,f488,f491]) ).
fof(f495,definition,
( sQ13_spl
<=> nil = sk1 ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f497,plain,
( sQ13_spl
| nil != sk1 ),
inference(component_clause,[status(thm)],[f495]) ).
fof(f498,plain,
( sQ10_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f445,f495,f484]) ).
fof(f505,plain,
! [X0] :
( strictorderedP(cons(X0,nil))
| ~ ssItem(X0)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f317]) ).
fof(f506,plain,
! [X0] :
( totalorderedP(cons(X0,nil))
| ~ ssItem(X0)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f318]) ).
fof(f516,plain,
( app(nil,nil) = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f362]) ).
fof(f517,plain,
( app(nil,nil) = nil
| ~ ssList(nil) ),
inference(duplicate_literals_removal,[status(thm)],[f516]) ).
fof(f531,plain,
( sQ13_spl
| nil != sk3 ),
inference(forward_demodulation,[status(thm)],[f436,f497]) ).
fof(f532,plain,
( sQ13_spl
| ~ sQ9_spl
| sk4 != sk3 ),
inference(backward_demodulation,[status(thm)],[f534,f531]) ).
fof(f534,plain,
( ~ sQ9_spl
| nil = sk4 ),
inference(forward_demodulation,[status(thm)],[f435,f482]) ).
fof(f537,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| sk4 = sk3 ),
inference(forward_demodulation,[status(thm)],[f534,f456]) ).
fof(f538,plain,
( sQ13_spl
| ~ sQ9_spl
| ~ sQ2_spl
| sk4 != sk4 ),
inference(forward_demodulation,[status(thm)],[f537,f532]) ).
fof(f539,plain,
( sQ13_spl
| ~ sQ9_spl
| ~ sQ2_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f538]) ).
fof(f540,plain,
( sQ13_spl
| ~ sQ9_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f539]) ).
fof(f541,plain,
( ~ sQ10_spl
| neq(sk4,nil) ),
inference(forward_demodulation,[status(thm)],[f435,f485]) ).
fof(f542,plain,
( sQ12_spl
| ~ neq(nil,sk4) ),
inference(forward_demodulation,[status(thm)],[f435,f493]) ).
fof(f543,plain,
! [X0,X1,X2,X3] :
( ~ sQ11_spl
| hd(sk2) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk4) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk1 != X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f435,f489]) ).
fof(f544,plain,
! [X0,X1,X2,X3] :
( ~ sQ11_spl
| hd(sk4) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sk4) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sk1 != X0
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f435,f543]) ).
fof(f545,plain,
( ~ sQ11_spl
| ~ ssItem(hd(sk4))
| app(tl(sk4),cons(hd(sk4),nil)) != sk1
| ~ ssList(cons(hd(sk4),nil))
| ~ ssList(tl(sk4))
| ~ ssList(sk1) ),
inference(destructive_equality_resolution,[status(thm)],[f544]) ).
fof(f547,plain,
( ~ sQ10_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f541,f467]) ).
fof(f548,plain,
( ~ sQ10_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f547]) ).
fof(f549,plain,
( ~ sQ9_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f534,f460]) ).
fof(f550,plain,
( ~ sQ9_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f549]) ).
fof(f569,definition,
( sQ14_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f571,plain,
( sQ14_spl
| ~ ssList(sk1) ),
inference(component_clause,[status(thm)],[f569]) ).
fof(f572,definition,
( sQ15_spl
<=> ssList(tl(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f574,plain,
( sQ15_spl
| ~ ssList(tl(sk4)) ),
inference(component_clause,[status(thm)],[f572]) ).
fof(f575,definition,
( sQ16_spl
<=> ssList(cons(hd(sk4),nil)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f577,plain,
( sQ16_spl
| ~ ssList(cons(hd(sk4),nil)) ),
inference(component_clause,[status(thm)],[f575]) ).
fof(f581,definition,
( sQ18_spl
<=> ssItem(hd(sk4)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f600,definition,
( sQ19_spl
<=> app(tl(sk4),cons(hd(sk4),nil)) = sk1 ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f602,plain,
( sQ19_spl
| app(tl(sk4),cons(hd(sk4),nil)) != sk1 ),
inference(component_clause,[status(thm)],[f600]) ).
fof(f603,plain,
( ~ sQ11_spl
| ~ sQ18_spl
| ~ sQ19_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f545,f569,f572,f575,f600,f581,f488]) ).
fof(f612,definition,
( sQ20_spl
<=> ssList(sk4) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f614,plain,
( sQ20_spl
| ~ ssList(sk4) ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f619,plain,
( sQ16_spl
| ~ sQ2_spl
| ~ ssList(cons(hd(sk4),sk3)) ),
inference(forward_demodulation,[status(thm)],[f456,f577]) ).
fof(f620,plain,
( sQ14_spl
| ~ ssList(sk3) ),
inference(forward_demodulation,[status(thm)],[f436,f571]) ).
fof(f621,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f620,f433]) ).
fof(f622,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f621]) ).
fof(f626,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f614,f434]) ).
fof(f627,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f626]) ).
fof(f633,definition,
( sQ22_spl
<=> ssList(cons(sk5,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f634,plain,
( ~ sQ22_spl
| ssList(cons(sk5,sk3)) ),
inference(component_clause,[status(thm)],[f633]) ).
fof(f635,plain,
( sQ22_spl
| ~ ssList(cons(sk5,sk3)) ),
inference(component_clause,[status(thm)],[f633]) ).
fof(f637,plain,
( sQ16_spl
| ~ sQ2_spl
| ~ ssList(sk3)
| ~ ssItem(hd(sk4)) ),
inference(resolution,[status(thm)],[f287,f619]) ).
fof(f638,definition,
( sQ23_spl
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f640,plain,
( sQ23_spl
| ~ ssList(sk3) ),
inference(component_clause,[status(thm)],[f638]) ).
fof(f641,plain,
( sQ16_spl
| ~ sQ2_spl
| ~ sQ23_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f637,f581,f638,f455,f575]) ).
fof(f642,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f640,f433]) ).
fof(f643,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f642]) ).
fof(f652,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ ssList(X0)
| ~ ssList(X1)
| duplicatefreeP(app(X0,X1)) ),
inference(resolution,[status(thm)],[f449,f286]) ).
fof(f696,plain,
( ~ sQ2_spl
| app(nil,nil) = nil
| ~ ssList(sk3) ),
inference(forward_demodulation,[status(thm)],[f456,f517]) ).
fof(f697,plain,
( ~ sQ2_spl
| app(sk3,nil) = nil
| ~ ssList(sk3) ),
inference(forward_demodulation,[status(thm)],[f456,f696]) ).
fof(f698,plain,
( ~ sQ2_spl
| app(sk3,sk3) = nil
| ~ ssList(sk3) ),
inference(forward_demodulation,[status(thm)],[f456,f697]) ).
fof(f699,plain,
( ~ sQ2_spl
| app(sk3,sk3) = sk3
| ~ ssList(sk3) ),
inference(forward_demodulation,[status(thm)],[f456,f698]) ).
fof(f710,plain,
( sQ22_spl
| ~ ssList(sk3)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f635,f287]) ).
fof(f711,plain,
( sQ22_spl
| ~ sQ23_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f710,f462,f638,f633]) ).
fof(f804,definition,
( sQ34_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f806,plain,
( sQ34_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f804]) ).
fof(f807,definition,
( sQ35_spl
<=> app(nil,nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f808,plain,
( ~ sQ35_spl
| app(nil,nil) = nil ),
inference(component_clause,[status(thm)],[f807]) ).
fof(f810,plain,
( sQ35_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f517,f804,f807]) ).
fof(f816,plain,
! [X0,X1] :
( ~ sQ1_spl
| ssList(cons(X1,X0))
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f287,f452]) ).
fof(f817,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ ssList(X1)
| cons(X0,X1) != X1 ),
inference(backward_subsumption_resolution,[status(thm)],[f302,f452]) ).
fof(f822,plain,
( sQ19_spl
| app(tl(sk4),cons(hd(sk4),nil)) != sk3 ),
inference(forward_demodulation,[status(thm)],[f436,f602]) ).
fof(f823,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f806,f208]) ).
fof(f824,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f823]) ).
fof(f830,definition,
( sQ36_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f836,plain,
( nil = nil
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f275,f330]) ).
fof(f838,plain,
( sQ36_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f836,f804,f830]) ).
fof(f852,plain,
( ~ sQ7_spl
| hd(sk4) = hd(cons(sk5,nil))
| nil = cons(sk5,nil)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk6) ),
inference(paramodulation,[status(thm)],[f474,f334]) ).
fof(f855,definition,
( sQ38_spl
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f856,plain,
( ~ sQ38_spl
| ssList(cons(sk5,nil)) ),
inference(component_clause,[status(thm)],[f855]) ).
fof(f857,plain,
( sQ38_spl
| ~ ssList(cons(sk5,nil)) ),
inference(component_clause,[status(thm)],[f855]) ).
fof(f858,definition,
( sQ39_spl
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f859,plain,
( ~ sQ39_spl
| nil = cons(sk5,nil) ),
inference(component_clause,[status(thm)],[f858]) ).
fof(f861,definition,
( sQ40_spl
<=> hd(sk4) = hd(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f862,plain,
( ~ sQ40_spl
| hd(sk4) = hd(cons(sk5,nil)) ),
inference(component_clause,[status(thm)],[f861]) ).
fof(f864,plain,
( ~ sQ7_spl
| sQ40_spl
| sQ39_spl
| ~ sQ38_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f852,f469,f855,f858,f861,f473]) ).
fof(f901,definition,
( sQ42_spl
<=> app(sk3,sk3) = sk3 ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f902,plain,
( ~ sQ42_spl
| app(sk3,sk3) = sk3 ),
inference(component_clause,[status(thm)],[f901]) ).
fof(f904,plain,
( ~ sQ2_spl
| sQ42_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f699,f638,f901,f455]) ).
fof(f908,plain,
( ~ sQ1_spl
| sQ38_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f857,f816]) ).
fof(f909,plain,
( ~ sQ1_spl
| sQ38_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f908,f804,f855,f451]) ).
fof(f910,plain,
! [X0,X1] :
( X0 = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[f371]) ).
fof(f911,definition,
! [X0] :
( sQ43_spl
<=> ( X0 = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f914,definition,
! [X1] :
( sQ44_spl
<=> ~ ssList(X1) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f915,plain,
! [X0] :
( ~ sQ44_spl
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f914]) ).
fof(f917,plain,
( sQ44_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f910,f911,f914]) ).
fof(f918,plain,
( ~ sQ44_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f208,f915]) ).
fof(f950,plain,
~ sQ44_spl,
inference(contradiction_clause,[status(thm)],[f918]) ).
fof(f971,plain,
! [X0] :
( ~ ssList(app(X0,nil))
| app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(X0,nil)) ),
inference(resolution,[status(thm)],[f373,f274]) ).
fof(f973,plain,
! [X0] :
( ~ sQ35_spl
| nil = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(nil)
| nil != app(X0,nil) ),
inference(paramodulation,[status(thm)],[f808,f373]) ).
fof(f975,plain,
! [X0] :
( ~ sQ42_spl
| sk3 = X0
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(sk3)
| sk3 != app(X0,sk3) ),
inference(paramodulation,[status(thm)],[f902,f373]) ).
fof(f980,definition,
! [X0] :
( sQ48_spl
<=> ( ~ ssList(app(X0,nil))
| app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(app(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f983,plain,
( ~ sQ34_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f971,f980,f804]) ).
fof(f985,definition,
! [X0] :
( sQ49_spl
<=> ( nil = X0
| ~ ssList(X0)
| nil != app(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f988,plain,
( ~ sQ35_spl
| ~ sQ34_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f973,f985,f804,f807]) ).
fof(f993,definition,
! [X0] :
( sQ51_spl
<=> ( sk3 = X0
| ~ ssList(X0)
| sk3 != app(X0,sk3) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f996,plain,
( ~ sQ42_spl
| ~ sQ23_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f975,f993,f638,f901]) ).
fof(f1002,plain,
! [X0] :
( ~ sQ35_spl
| cons(X0,nil) = app(cons(X0,nil),nil)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f808,f384]) ).
fof(f1004,definition,
! [X0] :
( sQ52_spl
<=> ( cons(X0,nil) = app(cons(X0,nil),nil)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1007,plain,
( ~ sQ35_spl
| ~ sQ34_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1002,f1004,f804,f807]) ).
fof(f1048,plain,
( ~ sQ35_spl
| ~ sQ0_spl
| ~ ssList(nil)
| ~ ssList(nil)
| duplicatefreeP(nil) ),
inference(paramodulation,[status(thm)],[f808,f652]) ).
fof(f1051,definition,
( sQ58_spl
<=> duplicatefreeP(nil) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1054,plain,
( ~ sQ35_spl
| ~ sQ0_spl
| ~ sQ34_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1048,f1051,f804,f448,f807]) ).
fof(f1056,plain,
! [X0,X1] :
( X0 = X0
| ~ ssList(X1)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X0) ),
inference(equality_resolution,[status(thm)],[f402]) ).
fof(f1057,definition,
! [X0] :
( sQ59_spl
<=> ( X0 = X0
| ~ ssItem(X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1060,definition,
! [X1] :
( sQ60_spl
<=> ( ~ ssList(X1)
| ~ ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1061,plain,
! [X0] :
( ~ sQ60_spl
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1060]) ).
fof(f1063,plain,
( sQ60_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1056,f1057,f1060]) ).
fof(f1064,plain,
! [X0] :
( ~ sQ60_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1061]) ).
fof(f1066,definition,
! [X0] :
( sQ61_spl
<=> ( ~ ssItem(X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1067,plain,
! [X0] :
( ~ sQ61_spl
| ~ ssItem(X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1066]) ).
fof(f1070,plain,
! [X0] :
( ~ sQ61_spl
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1067]) ).
fof(f1084,plain,
( ~ sQ22_spl
| ~ sQ60_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f634,f1064]) ).
fof(f1090,plain,
( ~ sQ22_spl
| ~ sQ60_spl ),
inference(contradiction_clause,[status(thm)],[f1084]) ).
fof(f1091,plain,
( ~ sQ61_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1070,f452]) ).
fof(f1092,plain,
( ~ sQ61_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1091]) ).
fof(f1102,plain,
( ~ sQ39_spl
| ~ sQ1_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f817,f859]) ).
fof(f1104,plain,
( ~ sQ39_spl
| ~ sQ1_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f1102,f804,f451,f858]) ).
fof(f1126,plain,
( ~ sQ40_spl
| nil = cons(sk5,nil)
| ssItem(hd(sk4))
| ~ ssList(cons(sk5,nil)) ),
inference(paramodulation,[status(thm)],[f862,f277]) ).
fof(f1127,plain,
( ~ sQ40_spl
| sQ39_spl
| sQ18_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f1126,f855,f581,f858,f861]) ).
fof(f1132,plain,
( sQ38_spl
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f287,f857]) ).
fof(f1133,plain,
( sQ38_spl
| ~ sQ34_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1132,f462,f804,f855]) ).
fof(f1137,plain,
( ~ sQ39_spl
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[f859,f302]) ).
fof(f1140,plain,
( ~ sQ39_spl
| ~ sQ34_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1137,f462,f804,f858]) ).
fof(f1165,plain,
( ~ sQ8_spl
| nil = cons(sk5,nil)
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| sk3 != nil ),
inference(paramodulation,[status(thm)],[f478,f330]) ).
fof(f1170,plain,
( ~ sQ8_spl
| sQ39_spl
| ~ sQ6_spl
| ~ sQ38_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1165,f455,f855,f469,f858,f477]) ).
fof(f1222,definition,
( sQ64_spl
<=> sk4 = cons(sk5,sk6) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1223,plain,
( ~ sQ64_spl
| sk4 = cons(sk5,sk6) ),
inference(component_clause,[status(thm)],[f1222]) ).
fof(f1228,plain,
( ~ sQ64_spl
| hd(sk4) = sk5
| ~ ssList(sk6)
| ~ ssItem(sk5) ),
inference(paramodulation,[status(thm)],[f1223,f298]) ).
fof(f1229,definition,
( sQ65_spl
<=> hd(sk4) = sk5 ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1230,plain,
( ~ sQ65_spl
| hd(sk4) = sk5 ),
inference(component_clause,[status(thm)],[f1229]) ).
fof(f1232,plain,
( ~ sQ64_spl
| sQ65_spl
| ~ sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1228,f462,f469,f1229,f1222]) ).
fof(f1234,plain,
( ~ sQ7_spl
| sk4 = cons(sk5,sk6)
| ~ ssList(sk6)
| ~ ssItem(sk5) ),
inference(paramodulation,[status(thm)],[f474,f331]) ).
fof(f1235,plain,
( ~ sQ7_spl
| sQ64_spl
| ~ sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1234,f462,f469,f1222,f473]) ).
fof(f1253,plain,
( ~ sQ64_spl
| tl(sk4) = sk6
| ~ ssList(sk6)
| ~ ssItem(sk5) ),
inference(paramodulation,[status(thm)],[f1223,f297]) ).
fof(f1254,definition,
( sQ69_spl
<=> tl(sk4) = sk6 ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1255,plain,
( ~ sQ69_spl
| tl(sk4) = sk6 ),
inference(component_clause,[status(thm)],[f1254]) ).
fof(f1257,plain,
( ~ sQ64_spl
| sQ69_spl
| ~ sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1253,f462,f469,f1254,f1222]) ).
fof(f1258,plain,
! [X0] :
( ~ ssList(app(nil,X0))
| app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(nil,X0)) ),
inference(resolution,[status(thm)],[f371,f275]) ).
fof(f1260,plain,
! [X0] :
( ~ sQ35_spl
| nil = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(nil)
| nil != app(nil,X0) ),
inference(paramodulation,[status(thm)],[f808,f371]) ).
fof(f1265,definition,
! [X0] :
( sQ70_spl
<=> ( ~ ssList(app(nil,X0))
| app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1268,plain,
( ~ sQ34_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1258,f1265,f804]) ).
fof(f1270,definition,
! [X0] :
( sQ71_spl
<=> ( nil = X0
| ~ ssList(X0)
| nil != app(nil,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1273,plain,
( ~ sQ35_spl
| ~ sQ34_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1260,f1270,f804,f807]) ).
fof(f1295,plain,
( sQ19_spl
| ~ sQ69_spl
| app(sk6,cons(hd(sk4),nil)) != sk3 ),
inference(forward_demodulation,[status(thm)],[f1255,f822]) ).
fof(f1296,plain,
( sQ19_spl
| ~ sQ69_spl
| ~ sQ65_spl
| app(sk6,cons(sk5,nil)) != sk3 ),
inference(forward_demodulation,[status(thm)],[f1230,f1295]) ).
fof(f1297,plain,
( sQ19_spl
| ~ sQ69_spl
| ~ sQ65_spl
| ~ sQ8_spl
| sk3 != sk3 ),
inference(forward_demodulation,[status(thm)],[f478,f1296]) ).
fof(f1298,plain,
( sQ19_spl
| ~ sQ69_spl
| ~ sQ65_spl
| ~ sQ8_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1297]) ).
fof(f1299,plain,
( sQ19_spl
| ~ sQ69_spl
| ~ sQ65_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f1298]) ).
fof(f1300,plain,
( sQ15_spl
| ~ sQ69_spl
| ~ ssList(sk6) ),
inference(forward_demodulation,[status(thm)],[f1255,f574]) ).
fof(f1301,plain,
( sQ15_spl
| ~ sQ69_spl
| ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1300,f470]) ).
fof(f1302,plain,
( sQ15_spl
| ~ sQ69_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f1301]) ).
fof(f1306,plain,
( sQ16_spl
| ~ sQ65_spl
| ~ ssList(cons(sk5,nil)) ),
inference(forward_demodulation,[status(thm)],[f1230,f577]) ).
fof(f1307,plain,
( sQ16_spl
| ~ sQ65_spl
| ~ sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1306,f856]) ).
fof(f1308,plain,
( sQ16_spl
| ~ sQ65_spl
| ~ sQ38_spl ),
inference(contradiction_clause,[status(thm)],[f1307]) ).
fof(f1766,definition,
! [X0] :
( sQ112_spl
<=> ( totalorderedP(cons(X0,nil))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1769,plain,
( sQ112_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f506,f804,f1766]) ).
fof(f1770,definition,
! [X0] :
( sQ113_spl
<=> ( strictorderedP(cons(X0,nil))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1773,plain,
( sQ113_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f505,f804,f1770]) ).
fof(f1776,plain,
( sQ12_spl
| nil = sk4
| ~ ssList(nil)
| ~ ssList(sk4) ),
inference(resolution,[status(thm)],[f542,f303]) ).
fof(f1778,plain,
( sQ12_spl
| sQ3_spl
| ~ sQ34_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f1776,f612,f804,f458,f491]) ).
fof(f1783,plain,
$false,
inference(sat_refutation,[status(thm)],[f454,f461,f468,f472,f476,f480,f487,f494,f498,f540,f548,f550,f603,f622,f627,f641,f643,f711,f810,f824,f838,f864,f904,f909,f917,f950,f983,f988,f996,f1007,f1054,f1063,f1090,f1092,f1104,f1127,f1133,f1140,f1170,f1232,f1235,f1257,f1268,f1273,f1299,f1302,f1308,f1769,f1773,f1778]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC310-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 08:18:05 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.42 % Refutation found
% 0.10/0.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.46 % Elapsed time: 0.075252 seconds
% 0.10/0.46 % CPU time: 0.279196 seconds
% 0.10/0.46 % Total memory used: 111.848 MB
% 0.10/0.46 % Net memory used: 111.556 MB
%------------------------------------------------------------------------------