%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC327-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:48 PM UTC 2026
% Result : Unsatisfiable 0.14s 5.42s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 61
% Syntax : Number of formulae : 200 ( 25 unt; 32 def)
% Number of atoms : 673 ( 207 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 899 ( 426 ~; 441 |; 0 &)
% ( 32 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 33 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 149 ( 149 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [U,V] :
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [U,V] :
( nil = U
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [U,V] :
( nil = V
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,axiom,
! [U,V] :
( app(U,V) = nil
| ~ ssList(U)
| ~ ssList(V)
| nil != V
| nil != U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,axiom,
! [U,V,W] :
( app(app(W,V),U) = app(W,app(V,U))
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f150,axiom,
! [U,V,W] :
( V = W
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [U,V,W] :
( U = W
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,axiom,
! [U,V,W,X,Y] :
( V = W
| ~ ssList(Y)
| ~ equalelemsP(Y)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(X)
| app(U,cons(V,cons(W,X))) != Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f190,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,negated_conjecture,
ssList(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
app(sk3,sk5) = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
equalelemsP(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
! [A,B,C] :
( app(C,cons(A,nil)) != sk3
| ~ ssList(C)
| app(cons(A,nil),B) != sk5
| ~ ssList(B)
| ~ ssItem(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,negated_conjecture,
( nil != sk3
| nil = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
! [A] :
( nil = sk1
| ~ equalelemsP(sk1)
| ssItem(sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
! [A] :
( nil != sk2
| ~ equalelemsP(sk1)
| ssItem(sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
! [A] :
( nil = sk1
| ~ equalelemsP(sk1)
| ssList(sk7(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f200,negated_conjecture,
! [A] :
( nil = sk1
| ~ equalelemsP(sk1)
| app(cons(sk6(A),nil),sk7(A)) = A
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f201,negated_conjecture,
! [A] :
( nil = sk1
| ~ equalelemsP(sk1)
| ssList(sk8(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,negated_conjecture,
! [A] :
( nil = sk1
| ~ equalelemsP(sk1)
| app(sk8(A),cons(sk6(A),nil)) = sk1
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,negated_conjecture,
! [A] :
( nil != sk2
| ~ equalelemsP(sk1)
| ssList(sk7(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f204,negated_conjecture,
! [A] :
( nil != sk2
| ~ equalelemsP(sk1)
| app(cons(sk6(A),nil),sk7(A)) = A
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f205,negated_conjecture,
! [A] :
( nil != sk2
| ~ equalelemsP(sk1)
| ssList(sk8(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f206,negated_conjecture,
! [A] :
( nil != sk2
| ~ equalelemsP(sk1)
| app(sk8(A),cons(sk6(A),nil)) = sk1
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f214,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f280,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f281,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f292,plain,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f333,plain,
! [U] :
( nil = U
| ~ ssList(U)
| ! [V] :
( ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f334,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f333]) ).
fof(f335,plain,
! [V] :
( nil = V
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f336,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f368,plain,
! [X0,X1] :
( app(X0,X1) = nil
| ~ ssList(X0)
| ~ ssList(X1)
| nil != X1
| nil != X0 ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f375,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(f376,plain,
! [V,W] :
( V = W
| ~ ssList(W)
| ! [U] :
( ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f377,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != app(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f378,plain,
! [U,W] :
( U = W
| ~ ssList(W)
| ! [V] :
( ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f379,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f425,plain,
! [V,W] :
( V = W
| ! [Y] :
( ~ ssList(Y)
| ~ equalelemsP(Y)
| ~ ssItem(V)
| ~ ssItem(W)
| ! [U] :
( ~ ssList(U)
| ! [X] :
( ~ ssList(X)
| app(U,cons(V,cons(W,X))) != Y ) ) ) ),
inference(miniscoping,[status(thm)],[f180]) ).
fof(f426,plain,
! [X0,X1,X2,X3,X4] :
( X1 = X2
| ~ ssList(X4)
| ~ equalelemsP(X4)
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X3)
| app(X0,cons(X1,cons(X2,X3))) != X4 ),
inference(cnf_transformation,[status(thm)],[f425]) ).
fof(f437,plain,
ssList(sk1),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f441,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f442,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f443,plain,
ssList(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f444,plain,
app(sk3,sk5) = sk4,
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f445,plain,
equalelemsP(sk3),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f446,plain,
! [A,C] :
( app(C,cons(A,nil)) != sk3
| ~ ssList(C)
| ! [B] :
( app(cons(A,nil),B) != sk5
| ~ ssList(B)
| ~ ssItem(A) ) ),
inference(miniscoping,[status(thm)],[f195]) ).
fof(f447,plain,
! [X0,X1,X2] :
( app(X2,cons(X0,nil)) != sk3
| ~ ssList(X2)
| app(cons(X0,nil),X1) != sk5
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f446]) ).
fof(f448,plain,
( nil != sk3
| nil = sk4 ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f449,plain,
( nil = sk1
| ~ equalelemsP(sk1)
| ! [A] :
( ssItem(sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f197]) ).
fof(f450,plain,
! [X0] :
( nil = sk1
| ~ equalelemsP(sk1)
| ssItem(sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f449]) ).
fof(f451,plain,
( nil != sk2
| ~ equalelemsP(sk1)
| ! [A] :
( ssItem(sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f198]) ).
fof(f452,plain,
! [X0] :
( nil != sk2
| ~ equalelemsP(sk1)
| ssItem(sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f451]) ).
fof(f453,plain,
( nil = sk1
| ~ equalelemsP(sk1)
| ! [A] :
( ssList(sk7(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f199]) ).
fof(f454,plain,
! [X0] :
( nil = sk1
| ~ equalelemsP(sk1)
| ssList(sk7(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f453]) ).
fof(f455,plain,
( nil = sk1
| ~ equalelemsP(sk1)
| ! [A] :
( app(cons(sk6(A),nil),sk7(A)) = A
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f200]) ).
fof(f456,plain,
! [X0] :
( nil = sk1
| ~ equalelemsP(sk1)
| app(cons(sk6(X0),nil),sk7(X0)) = X0
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f455]) ).
fof(f457,plain,
( nil = sk1
| ~ equalelemsP(sk1)
| ! [A] :
( ssList(sk8(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f201]) ).
fof(f458,plain,
! [X0] :
( nil = sk1
| ~ equalelemsP(sk1)
| ssList(sk8(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f459,plain,
( nil = sk1
| ~ equalelemsP(sk1)
| ! [A] :
( app(sk8(A),cons(sk6(A),nil)) = sk1
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f202]) ).
fof(f460,plain,
! [X0] :
( nil = sk1
| ~ equalelemsP(sk1)
| app(sk8(X0),cons(sk6(X0),nil)) = sk1
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f459]) ).
fof(f461,plain,
( nil != sk2
| ~ equalelemsP(sk1)
| ! [A] :
( ssList(sk7(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f203]) ).
fof(f462,plain,
! [X0] :
( nil != sk2
| ~ equalelemsP(sk1)
| ssList(sk7(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f461]) ).
fof(f463,plain,
( nil != sk2
| ~ equalelemsP(sk1)
| ! [A] :
( app(cons(sk6(A),nil),sk7(A)) = A
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f204]) ).
fof(f464,plain,
! [X0] :
( nil != sk2
| ~ equalelemsP(sk1)
| app(cons(sk6(X0),nil),sk7(X0)) = X0
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f463]) ).
fof(f465,plain,
( nil != sk2
| ~ equalelemsP(sk1)
| ! [A] :
( ssList(sk8(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f205]) ).
fof(f466,plain,
! [X0] :
( nil != sk2
| ~ equalelemsP(sk1)
| ssList(sk8(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f465]) ).
fof(f467,plain,
( nil != sk2
| ~ equalelemsP(sk1)
| ! [A] :
( app(sk8(A),cons(sk6(A),nil)) = sk1
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f206]) ).
fof(f468,plain,
! [X0] :
( nil != sk2
| ~ equalelemsP(sk1)
| app(sk8(X0),cons(sk6(X0),nil)) = sk1
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f467]) ).
fof(f476,definition,
( sQ2_spl
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f477,plain,
( ~ sQ2_spl
| nil = sk4 ),
inference(component_clause,[status(thm)],[f476]) ).
fof(f479,definition,
( sQ3_spl
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f481,plain,
( sQ3_spl
| nil != sk3 ),
inference(component_clause,[status(thm)],[f479]) ).
fof(f482,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f448,f476,f479]) ).
fof(f483,definition,
! [X0] :
( sQ4_spl
<=> ( ssItem(sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f484,plain,
! [X0] :
( ~ sQ4_spl
| ssItem(sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f483]) ).
fof(f486,definition,
( sQ5_spl
<=> equalelemsP(sk1) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f488,plain,
( sQ5_spl
| ~ equalelemsP(sk1) ),
inference(component_clause,[status(thm)],[f486]) ).
fof(f489,definition,
( sQ6_spl
<=> nil = sk1 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f490,plain,
( ~ sQ6_spl
| nil = sk1 ),
inference(component_clause,[status(thm)],[f489]) ).
fof(f492,plain,
( sQ6_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f450,f483,f486,f489]) ).
fof(f493,definition,
( sQ7_spl
<=> nil = sk2 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f495,plain,
( sQ7_spl
| nil != sk2 ),
inference(component_clause,[status(thm)],[f493]) ).
fof(f496,plain,
( ~ sQ7_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f452,f483,f486,f493]) ).
fof(f497,definition,
! [X0] :
( sQ8_spl
<=> ( ssList(sk7(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f498,plain,
! [X0] :
( ~ sQ8_spl
| ssList(sk7(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f500,plain,
( sQ6_spl
| ~ sQ5_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f454,f497,f486,f489]) ).
fof(f501,definition,
! [X0] :
( sQ9_spl
<=> ( app(cons(sk6(X0),nil),sk7(X0)) = X0
| app(sk1,X0) != sk2
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f502,plain,
! [X0] :
( ~ sQ9_spl
| app(cons(sk6(X0),nil),sk7(X0)) = X0
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f501]) ).
fof(f504,plain,
( sQ6_spl
| ~ sQ5_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f456,f501,f486,f489]) ).
fof(f505,definition,
! [X0] :
( sQ10_spl
<=> ( ssList(sk8(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f506,plain,
! [X0] :
( ~ sQ10_spl
| ssList(sk8(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f505]) ).
fof(f508,plain,
( sQ6_spl
| ~ sQ5_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f458,f505,f486,f489]) ).
fof(f509,definition,
! [X0] :
( sQ11_spl
<=> ( app(sk8(X0),cons(sk6(X0),nil)) = sk1
| app(sk1,X0) != sk2
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f510,plain,
! [X0] :
( ~ sQ11_spl
| app(sk8(X0),cons(sk6(X0),nil)) = sk1
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f509]) ).
fof(f512,plain,
( sQ6_spl
| ~ sQ5_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f460,f509,f486,f489]) ).
fof(f513,plain,
( ~ sQ7_spl
| ~ sQ5_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f462,f497,f486,f493]) ).
fof(f514,plain,
( ~ sQ7_spl
| ~ sQ5_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f464,f501,f486,f493]) ).
fof(f515,plain,
( ~ sQ7_spl
| ~ sQ5_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f466,f505,f486,f493]) ).
fof(f516,plain,
( ~ sQ7_spl
| ~ sQ5_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f468,f509,f486,f493]) ).
fof(f529,plain,
app(sk1,sk5) = sk4,
inference(forward_demodulation,[status(thm)],[f442,f444]) ).
fof(f530,plain,
app(sk1,sk5) = sk2,
inference(forward_demodulation,[status(thm)],[f441,f529]) ).
fof(f531,plain,
( ssList(sk2)
| ~ ssList(sk1)
| ~ ssList(sk5) ),
inference(paramodulation,[status(thm)],[f530,f292]) ).
fof(f532,definition,
( sQ12_spl
<=> ssList(sk5) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f534,plain,
( sQ12_spl
| ~ ssList(sk5) ),
inference(component_clause,[status(thm)],[f532]) ).
fof(f535,definition,
( sQ13_spl
<=> ssList(sk1) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f537,plain,
( sQ13_spl
| ~ ssList(sk1) ),
inference(component_clause,[status(thm)],[f535]) ).
fof(f538,definition,
( sQ14_spl
<=> ssList(sk2) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f541,plain,
( sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f531,f532,f535,f538]) ).
fof(f542,plain,
equalelemsP(sk1),
inference(forward_demodulation,[status(thm)],[f442,f445]) ).
fof(f543,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f488,f542]) ).
fof(f544,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f543]) ).
fof(f545,plain,
( ~ sQ2_spl
| sk2 = nil ),
inference(backward_demodulation,[status(thm)],[f477,f441]) ).
fof(f548,plain,
( ~ sQ6_spl
| nil = sk3 ),
inference(backward_demodulation,[status(thm)],[f490,f442]) ).
fof(f550,plain,
( ~ sQ2_spl
| sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f545,f495]) ).
fof(f551,plain,
( ~ sQ2_spl
| sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f550]) ).
fof(f553,plain,
( ~ ssList(nil)
| nil = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f334,f281]) ).
fof(f555,definition,
( sQ15_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f557,plain,
( sQ15_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f555]) ).
fof(f558,definition,
( sQ16_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f561,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f553,f555,f558]) ).
fof(f563,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f557,f214]) ).
fof(f564,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f563]) ).
fof(f565,plain,
( sQ3_spl
| ~ sQ6_spl
| nil != nil ),
inference(forward_demodulation,[status(thm)],[f548,f481]) ).
fof(f566,plain,
( sQ3_spl
| ~ sQ6_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f565]) ).
fof(f567,plain,
( sQ3_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f566]) ).
fof(f595,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f534,f443]) ).
fof(f596,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f595]) ).
fof(f601,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X1)
| nil != X1
| nil != X0 ),
inference(resolution,[status(thm)],[f368,f336]) ).
fof(f607,definition,
! [X0] :
( sQ19_spl
<=> ( ~ ssList(X0)
| ~ ssList(X0)
| nil != X0 ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f608,plain,
! [X0] :
( ~ sQ19_spl
| ~ ssList(X0)
| ~ ssList(X0)
| nil != X0 ),
inference(component_clause,[status(thm)],[f607]) ).
fof(f610,definition,
! [X1] :
( sQ20_spl
<=> ( nil = X1
| ~ ssList(X1)
| ~ ssList(X1)
| nil != X1 ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f601,f607,f610]) ).
fof(f615,plain,
! [X0] :
( ~ sQ19_spl
| ~ ssList(X0)
| nil != X0 ),
inference(duplicate_literals_removal,[status(thm)],[f608]) ).
fof(f616,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f537,f437]) ).
fof(f617,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f616]) ).
fof(f627,definition,
( sQ21_spl
<=> ssList(sk8(sk5)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f662,plain,
! [X0] :
( ~ ssList(app(nil,X0))
| app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(nil,X0)) ),
inference(resolution,[status(thm)],[f377,f281]) ).
fof(f665,definition,
! [X0] :
( sQ28_spl
<=> ( ~ ssList(app(nil,X0))
| app(nil,X0) = X0
| ~ ssList(X0)
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f668,plain,
( ~ sQ15_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f662,f665,f555]) ).
fof(f678,plain,
! [X0] :
( ~ ssList(app(X0,nil))
| app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(app(X0,nil)) ),
inference(resolution,[status(thm)],[f379,f280]) ).
fof(f681,definition,
! [X0] :
( sQ31_spl
<=> ( ~ ssList(app(X0,nil))
| app(X0,nil) = X0
| ~ ssList(X0)
| ~ ssList(app(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f684,plain,
( ~ sQ15_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f678,f681,f555]) ).
fof(f689,plain,
! [X0] :
( X0 = sk1
| ~ ssList(sk1)
| ~ ssList(sk5)
| ~ ssList(X0)
| app(X0,sk5) != sk2 ),
inference(paramodulation,[status(thm)],[f530,f379]) ).
fof(f691,plain,
! [X0] :
( X0 = sk5
| ~ ssList(sk5)
| ~ ssList(sk1)
| ~ ssList(X0)
| app(sk1,X0) != sk2 ),
inference(paramodulation,[status(thm)],[f530,f377]) ).
fof(f693,plain,
! [X0] :
( app(sk2,X0) = app(sk1,app(sk5,X0))
| ~ ssList(sk1)
| ~ ssList(sk5)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f530,f375]) ).
fof(f698,definition,
! [X0] :
( sQ32_spl
<=> ( X0 = sk1
| ~ ssList(X0)
| app(X0,sk5) != sk2 ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f699,plain,
! [X0] :
( ~ sQ32_spl
| X0 = sk1
| ~ ssList(X0)
| app(X0,sk5) != sk2 ),
inference(component_clause,[status(thm)],[f698]) ).
fof(f701,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f689,f698,f532,f535]) ).
fof(f703,definition,
! [X0] :
( sQ33_spl
<=> ( X0 = sk5
| ~ ssList(X0)
| app(sk1,X0) != sk2 ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f704,plain,
! [X0] :
( ~ sQ33_spl
| X0 = sk5
| ~ ssList(X0)
| app(sk1,X0) != sk2 ),
inference(component_clause,[status(thm)],[f703]) ).
fof(f706,plain,
( ~ sQ12_spl
| ~ sQ13_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f691,f703,f535,f532]) ).
fof(f708,definition,
! [X0] :
( sQ34_spl
<=> ( app(sk2,X0) = app(sk1,app(sk5,X0))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f709,plain,
! [X0] :
( ~ sQ34_spl
| app(sk2,X0) = app(sk1,app(sk5,X0))
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f708]) ).
fof(f711,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f693,f708,f532,f535]) ).
fof(f716,plain,
( ~ sQ8_spl
| ssList(sk7(sk5))
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f498,f530]) ).
fof(f718,definition,
( sQ35_spl
<=> ssList(sk7(sk5)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f721,plain,
( ~ sQ8_spl
| sQ35_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f716,f532,f718,f497]) ).
fof(f722,definition,
( sQ36_spl
<=> sk2 = sk2 ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f724,plain,
( sQ36_spl
| sk2 != sk2 ),
inference(component_clause,[status(thm)],[f722]) ).
fof(f748,plain,
( ~ sQ19_spl
| nil != nil ),
inference(resolution,[status(thm)],[f615,f214]) ).
fof(f749,plain,
( ~ sQ19_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f748]) ).
fof(f750,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f749]) ).
fof(f764,plain,
( ~ sQ4_spl
| ssItem(sk6(sk5))
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f484,f530]) ).
fof(f766,definition,
( sQ40_spl
<=> ssItem(sk6(sk5)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f769,plain,
( ~ sQ4_spl
| sQ40_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f764,f532,f766,f483]) ).
fof(f778,plain,
! [X0,X1,X2] :
( ~ ssList(cons(X2,cons(X1,X0)))
| X2 = X1
| ~ ssList(cons(X2,cons(X1,X0)))
| ~ equalelemsP(cons(X2,cons(X1,X0)))
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f426,f281]) ).
fof(f786,definition,
! [X0,X1,X2] :
( sQ42_spl
<=> ( ~ ssList(cons(X2,cons(X1,X0)))
| X2 = X1
| ~ ssList(cons(X2,cons(X1,X0)))
| ~ equalelemsP(cons(X2,cons(X1,X0)))
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f789,plain,
( ~ sQ15_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f778,f786,f555]) ).
fof(f792,plain,
! [X0,X1,X2] :
( app(X2,cons(X0,nil)) != sk1
| ~ ssList(X2)
| app(cons(X0,nil),X1) != sk5
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(forward_demodulation,[status(thm)],[f442,f447]) ).
fof(f793,plain,
! [X0] :
( ~ sQ9_spl
| app(sk1,sk5) != sk2
| ~ ssList(sk5)
| app(X0,cons(sk6(sk5),nil)) != sk1
| ~ ssList(X0)
| ~ ssList(sk7(sk5))
| ~ ssItem(sk6(sk5)) ),
inference(resolution,[status(thm)],[f792,f502]) ).
fof(f794,definition,
! [X0] :
( sQ43_spl
<=> ( app(X0,cons(sk6(sk5),nil)) != sk1
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f795,plain,
! [X0] :
( ~ sQ43_spl
| app(X0,cons(sk6(sk5),nil)) != sk1
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f794]) ).
fof(f797,definition,
( sQ44_spl
<=> app(sk1,sk5) = sk2 ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f799,plain,
( sQ44_spl
| app(sk1,sk5) != sk2 ),
inference(component_clause,[status(thm)],[f797]) ).
fof(f800,plain,
( ~ sQ9_spl
| ~ sQ44_spl
| ~ sQ12_spl
| sQ43_spl
| ~ sQ35_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f793,f766,f718,f794,f532,f797,f501]) ).
fof(f801,plain,
( ~ sQ32_spl
| sk1 = sk1
| ~ ssList(sk1) ),
inference(resolution,[status(thm)],[f699,f530]) ).
fof(f803,definition,
( sQ45_spl
<=> sk1 = sk1 ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f806,plain,
( ~ sQ32_spl
| sQ45_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f801,f535,f803,f698]) ).
fof(f808,plain,
( ~ sQ33_spl
| sk5 = sk5
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f704,f530]) ).
fof(f810,definition,
( sQ46_spl
<=> sk5 = sk5 ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f813,plain,
( ~ sQ33_spl
| sQ46_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f808,f532,f810,f703]) ).
fof(f815,plain,
( sQ36_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f724]) ).
fof(f816,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f815]) ).
fof(f817,plain,
( ~ sQ10_spl
| ssList(sk8(sk5))
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f506,f530]) ).
fof(f819,plain,
( ~ sQ10_spl
| sQ21_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f817,f532,f627,f505]) ).
fof(f821,plain,
! [X0,X1,X2] :
( ~ sQ34_spl
| X0 = X1
| ~ ssList(app(sk1,app(sk5,cons(X0,cons(X1,X2)))))
| ~ equalelemsP(app(sk1,app(sk5,cons(X0,cons(X1,X2)))))
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(sk2)
| ~ ssList(X2)
| ~ ssList(cons(X0,cons(X1,X2))) ),
inference(resolution,[status(thm)],[f709,f426]) ).
fof(f822,definition,
! [X0,X1,X2] :
( sQ47_spl
<=> ( X0 = X1
| ~ ssList(app(sk1,app(sk5,cons(X0,cons(X1,X2)))))
| ~ equalelemsP(app(sk1,app(sk5,cons(X0,cons(X1,X2)))))
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(cons(X0,cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f825,plain,
( ~ sQ34_spl
| ~ sQ14_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f821,f822,f538,f708]) ).
fof(f899,plain,
( ~ sQ11_spl
| ~ sQ43_spl
| app(sk1,sk5) != sk2
| ~ ssList(sk5)
| ~ ssList(sk8(sk5)) ),
inference(resolution,[status(thm)],[f795,f510]) ).
fof(f900,plain,
( ~ sQ11_spl
| ~ sQ43_spl
| ~ sQ44_spl
| ~ sQ12_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f899,f627,f532,f797,f794,f509]) ).
fof(f901,plain,
( sQ44_spl
| sk2 != sk2 ),
inference(forward_demodulation,[status(thm)],[f530,f799]) ).
fof(f902,plain,
( sQ44_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f901]) ).
fof(f903,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f902]) ).
fof(f904,plain,
$false,
inference(sat_refutation,[status(thm)],[f482,f492,f496,f500,f504,f508,f512,f513,f514,f515,f516,f541,f544,f551,f561,f564,f567,f596,f613,f617,f668,f684,f701,f706,f711,f721,f750,f769,f789,f800,f806,f813,f816,f819,f825,f900,f903]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC327-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n006.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 08:16:03 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Drodi V4.1.1
% 0.14/5.42 % Refutation found
% 0.14/5.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/5.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/5.45 % Elapsed time: 0.068157 seconds
% 0.14/5.45 % CPU time: 0.223577 seconds
% 0.14/5.45 % Total memory used: 110.933 MB
% 0.14/5.45 % Net memory used: 110.696 MB
%------------------------------------------------------------------------------