%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC343-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 : n007.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:51 PM UTC 2026
% Result : Unsatisfiable 0.15s 0.55s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 21
% Syntax : Number of formulae : 128 ( 19 unt; 0 def)
% Number of atoms : 514 ( 220 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 754 ( 368 ~; 386 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% Number of variables : 102 ( 102 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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,
strictorderedP(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
! [A,B,C,D] :
( ~ lt(C,A)
| app(D,cons(C,nil)) != sk3
| ~ ssList(D)
| ~ ssItem(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
| ~ strictorderedP(sk1)
| ssItem(sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
! [A] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
! [A] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk7(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f200,negated_conjecture,
! [A] :
( nil = sk1
| ~ strictorderedP(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
| ~ strictorderedP(sk1)
| ssItem(sk8(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,negated_conjecture,
! [A] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk9(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,negated_conjecture,
! [A] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(sk9(A),cons(sk8(A),nil)) = sk1
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f204,negated_conjecture,
! [A] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk8(A),sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f205,negated_conjecture,
! [A] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk7(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f206,negated_conjecture,
! [A] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk6(A),nil),sk7(A)) = A
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f207,negated_conjecture,
! [A] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk8(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f208,negated_conjecture,
! [A] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk9(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f209,negated_conjecture,
! [A] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(sk9(A),cons(sk8(A),nil)) = sk1
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f210,negated_conjecture,
! [A] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk8(A),sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f445,plain,
sk2 = sk4,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f446,plain,
sk1 = sk3,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f447,plain,
ssList(sk5),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f448,plain,
app(sk3,sk5) = sk4,
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f449,plain,
strictorderedP(sk3),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f450,plain,
! [A,C] :
( ~ lt(C,A)
| ! [D] :
( app(D,cons(C,nil)) != sk3
| ~ ssList(D)
| ~ ssItem(C)
| ! [B] :
( app(cons(A,nil),B) != sk5
| ~ ssList(B)
| ~ ssItem(A) ) ) ),
inference(miniscoping,[status(thm)],[f195]) ).
fof(f451,plain,
! [X0,X1,X2,X3] :
( ~ lt(X2,X0)
| app(X3,cons(X2,nil)) != sk3
| ~ ssList(X3)
| ~ ssItem(X2)
| app(cons(X0,nil),X1) != sk5
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f452,plain,
( nil != sk3
| nil = sk4 ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f453,plain,
( nil = sk1
| ~ strictorderedP(sk1)
| ! [A] :
( ssItem(sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f197]) ).
fof(f454,plain,
! [X0] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f453]) ).
fof(f455,plain,
( nil != sk2
| ~ strictorderedP(sk1)
| ! [A] :
( ssItem(sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f198]) ).
fof(f456,plain,
! [X0] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f455]) ).
fof(f457,plain,
( nil = sk1
| ~ strictorderedP(sk1)
| ! [A] :
( ssList(sk7(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f199]) ).
fof(f458,plain,
! [X0] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk7(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f459,plain,
( nil = sk1
| ~ strictorderedP(sk1)
| ! [A] :
( app(cons(sk6(A),nil),sk7(A)) = A
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f200]) ).
fof(f460,plain,
! [X0] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk6(X0),nil),sk7(X0)) = X0
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f459]) ).
fof(f461,plain,
( nil = sk1
| ~ strictorderedP(sk1)
| ! [A] :
( ssItem(sk8(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f201]) ).
fof(f462,plain,
! [X0] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk8(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f461]) ).
fof(f463,plain,
( nil = sk1
| ~ strictorderedP(sk1)
| ! [A] :
( ssList(sk9(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f202]) ).
fof(f464,plain,
! [X0] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk9(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f463]) ).
fof(f465,plain,
( nil = sk1
| ~ strictorderedP(sk1)
| ! [A] :
( app(sk9(A),cons(sk8(A),nil)) = sk1
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f203]) ).
fof(f466,plain,
! [X0] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(sk9(X0),cons(sk8(X0),nil)) = sk1
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f465]) ).
fof(f467,plain,
( nil = sk1
| ~ strictorderedP(sk1)
| ! [A] :
( lt(sk8(A),sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f204]) ).
fof(f468,plain,
! [X0] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk8(X0),sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f467]) ).
fof(f469,plain,
( nil != sk2
| ~ strictorderedP(sk1)
| ! [A] :
( ssList(sk7(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f205]) ).
fof(f470,plain,
! [X0] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk7(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f469]) ).
fof(f471,plain,
( nil != sk2
| ~ strictorderedP(sk1)
| ! [A] :
( app(cons(sk6(A),nil),sk7(A)) = A
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f206]) ).
fof(f472,plain,
! [X0] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk6(X0),nil),sk7(X0)) = X0
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f471]) ).
fof(f473,plain,
( nil != sk2
| ~ strictorderedP(sk1)
| ! [A] :
( ssItem(sk8(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f207]) ).
fof(f474,plain,
! [X0] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk8(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f473]) ).
fof(f475,plain,
( nil != sk2
| ~ strictorderedP(sk1)
| ! [A] :
( ssList(sk9(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f208]) ).
fof(f476,plain,
! [X0] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk9(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f477,plain,
( nil != sk2
| ~ strictorderedP(sk1)
| ! [A] :
( app(sk9(A),cons(sk8(A),nil)) = sk1
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f209]) ).
fof(f478,plain,
! [X0] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(sk9(X0),cons(sk8(X0),nil)) = sk1
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f477]) ).
fof(f479,plain,
( nil != sk2
| ~ strictorderedP(sk1)
| ! [A] :
( lt(sk8(A),sk6(A))
| app(sk1,A) != sk2
| ~ ssList(A) ) ),
inference(miniscoping,[status(thm)],[f210]) ).
fof(f480,plain,
! [X0] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk8(X0),sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f479]) ).
fof(f514,plain,
app(sk1,sk5) = sk4,
inference(forward_demodulation,[status(thm)],[f446,f448]) ).
fof(f515,plain,
app(sk1,sk5) = sk2,
inference(forward_demodulation,[status(thm)],[f445,f514]) ).
fof(f516,plain,
strictorderedP(sk1),
inference(forward_demodulation,[status(thm)],[f446,f449]) ).
fof(f517,plain,
! [X0,X1,X2,X3] :
( ~ lt(X2,X0)
| app(X3,cons(X2,nil)) != sk1
| ~ ssList(X3)
| ~ ssItem(X2)
| app(cons(X0,nil),X1) != sk5
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(forward_demodulation,[status(thm)],[f446,f451]) ).
fof(f518,plain,
( nil != sk3
| nil = sk2 ),
inference(forward_demodulation,[status(thm)],[f445,f452]) ).
fof(f519,plain,
( nil != sk1
| nil = sk2 ),
inference(forward_demodulation,[status(thm)],[f446,f518]) ).
fof(f520,plain,
! [X0] :
( nil = sk1
| ssItem(sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f454,f516]) ).
fof(f521,plain,
! [X0] :
( nil != sk2
| ssItem(sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f456,f516]) ).
fof(f522,plain,
! [X0] :
( nil = sk1
| ssList(sk7(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f458,f516]) ).
fof(f523,plain,
! [X0] :
( nil = sk1
| app(cons(sk6(X0),nil),sk7(X0)) = X0
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f460,f516]) ).
fof(f524,plain,
! [X0] :
( nil = sk1
| ssItem(sk8(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f462,f516]) ).
fof(f525,plain,
! [X0] :
( nil = sk1
| ssList(sk9(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f464,f516]) ).
fof(f526,plain,
! [X0] :
( nil = sk1
| app(sk9(X0),cons(sk8(X0),nil)) = sk1
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f466,f516]) ).
fof(f527,plain,
! [X0] :
( nil = sk1
| lt(sk8(X0),sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f468,f516]) ).
fof(f528,plain,
! [X0] :
( nil != sk2
| ssList(sk7(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f470,f516]) ).
fof(f529,plain,
! [X0] :
( nil != sk2
| app(cons(sk6(X0),nil),sk7(X0)) = X0
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f472,f516]) ).
fof(f530,plain,
! [X0] :
( nil != sk2
| ssItem(sk8(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f474,f516]) ).
fof(f531,plain,
! [X0] :
( nil != sk2
| ssList(sk9(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f476,f516]) ).
fof(f532,plain,
! [X0] :
( nil != sk2
| app(sk9(X0),cons(sk8(X0),nil)) = sk1
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f478,f516]) ).
fof(f533,plain,
! [X0] :
( nil != sk2
| lt(sk8(X0),sk6(X0))
| app(sk1,X0) != sk2
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f480,f516]) ).
fof(f551,plain,
( nil = sk1
| lt(sk8(sk5),sk6(sk5))
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f515,f527]) ).
fof(f552,plain,
( nil = sk1
| ssList(sk9(sk5))
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f515,f525]) ).
fof(f554,plain,
( nil = sk1
| ssList(sk7(sk5))
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f515,f522]) ).
fof(f555,plain,
( nil = sk1
| ssItem(sk6(sk5))
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f515,f520]) ).
fof(f565,plain,
( nil = sk1
| lt(sk8(sk5),sk6(sk5)) ),
inference(forward_subsumption_resolution,[status(thm)],[f551,f447]) ).
fof(f566,plain,
( nil = sk1
| ssList(sk9(sk5)) ),
inference(forward_subsumption_resolution,[status(thm)],[f552,f447]) ).
fof(f568,plain,
( nil = sk1
| ssList(sk7(sk5)) ),
inference(forward_subsumption_resolution,[status(thm)],[f554,f447]) ).
fof(f569,plain,
( nil = sk1
| ssItem(sk6(sk5)) ),
inference(forward_subsumption_resolution,[status(thm)],[f555,f447]) ).
fof(f581,plain,
! [X0,X1] :
( nil = sk1
| app(sk1,sk5) != sk2
| ~ ssList(sk5)
| ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssList(sk7(sk5))
| ~ ssItem(sk6(sk5)) ),
inference(resolution,[status(thm)],[f517,f523]) ).
fof(f582,plain,
! [X0,X1] :
( nil = sk1
| sk2 != sk2
| ~ ssList(sk5)
| ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssList(sk7(sk5))
| ~ ssItem(sk6(sk5)) ),
inference(forward_demodulation,[status(thm)],[f515,f581]) ).
fof(f583,plain,
! [X0,X1] :
( nil = sk1
| ~ ssList(sk5)
| ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssList(sk7(sk5))
| ~ ssItem(sk6(sk5)) ),
inference(trivial_equality_resolution,[status(thm)],[f582]) ).
fof(f584,plain,
! [X0,X1] :
( nil = sk1
| ~ ssList(sk5)
| ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssList(sk7(sk5)) ),
inference(forward_subsumption_resolution,[status(thm)],[f583,f569]) ).
fof(f603,plain,
( nil != sk2
| ssItem(sk6(sk5))
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f521,f515]) ).
fof(f605,plain,
( nil != sk2
| ssItem(sk6(sk5)) ),
inference(forward_subsumption_resolution,[status(thm)],[f603,f447]) ).
fof(f607,plain,
( nil != sk2
| ssList(sk7(sk5))
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f528,f515]) ).
fof(f609,plain,
( nil != sk2
| ssList(sk7(sk5)) ),
inference(forward_subsumption_resolution,[status(thm)],[f607,f447]) ).
fof(f611,plain,
! [X0,X1] :
( ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssList(sk7(sk5))
| ~ ssItem(sk6(sk5))
| nil != sk2
| app(sk1,sk5) != sk2
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f529,f517]) ).
fof(f612,plain,
! [X0,X1] :
( ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssList(sk7(sk5))
| ~ ssItem(sk6(sk5))
| nil != sk2
| sk2 != sk2
| ~ ssList(sk5) ),
inference(forward_demodulation,[status(thm)],[f515,f611]) ).
fof(f613,plain,
! [X0,X1] :
( ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssList(sk7(sk5))
| ~ ssItem(sk6(sk5))
| nil != sk2
| ~ ssList(sk5) ),
inference(trivial_equality_resolution,[status(thm)],[f612]) ).
fof(f614,plain,
! [X0,X1] :
( ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssList(sk7(sk5))
| ~ ssItem(sk6(sk5))
| nil != sk2 ),
inference(forward_subsumption_resolution,[status(thm)],[f613,f447]) ).
fof(f619,plain,
( nil != sk2
| ssList(sk9(sk5))
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f531,f515]) ).
fof(f621,plain,
( nil != sk2
| ssList(sk9(sk5)) ),
inference(forward_subsumption_resolution,[status(thm)],[f619,f447]) ).
fof(f623,plain,
( nil != sk1
| ssItem(sk6(sk5)) ),
inference(resolution,[status(thm)],[f605,f519]) ).
fof(f624,plain,
! [X0,X1] :
( ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssList(sk7(sk5))
| nil != sk2 ),
inference(backward_subsumption_resolution,[status(thm)],[f614,f625]) ).
fof(f625,plain,
ssItem(sk6(sk5)),
inference(forward_subsumption_resolution,[status(thm)],[f623,f569]) ).
fof(f626,plain,
! [X0,X1] :
( ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0)
| nil != sk2 ),
inference(forward_subsumption_resolution,[status(thm)],[f624,f609]) ).
fof(f627,plain,
( nil != sk1
| ssList(sk7(sk5)) ),
inference(resolution,[status(thm)],[f609,f519]) ).
fof(f628,plain,
! [X0,X1] :
( nil = sk1
| ~ ssList(sk5)
| ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f584,f629]) ).
fof(f629,plain,
ssList(sk7(sk5)),
inference(forward_subsumption_resolution,[status(thm)],[f627,f568]) ).
fof(f630,plain,
! [X0,X1] :
( nil = sk1
| ~ lt(X0,sk6(sk5))
| app(X1,cons(X0,nil)) != sk1
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f628,f447]) ).
fof(f634,plain,
( nil != sk1
| ssList(sk9(sk5)) ),
inference(resolution,[status(thm)],[f621,f519]) ).
fof(f635,plain,
ssList(sk9(sk5)),
inference(forward_subsumption_resolution,[status(thm)],[f634,f566]) ).
fof(f637,plain,
( nil != sk2
| lt(sk8(sk5),sk6(sk5))
| ~ ssList(sk5) ),
inference(resolution,[status(thm)],[f533,f515]) ).
fof(f639,plain,
( nil != sk2
| lt(sk8(sk5),sk6(sk5)) ),
inference(forward_subsumption_resolution,[status(thm)],[f637,f447]) ).
fof(f641,plain,
( nil != sk1
| lt(sk8(sk5),sk6(sk5)) ),
inference(resolution,[status(thm)],[f639,f519]) ).
fof(f642,plain,
lt(sk8(sk5),sk6(sk5)),
inference(forward_subsumption_resolution,[status(thm)],[f641,f565]) ).
fof(f643,plain,
! [X0] :
( nil != sk2
| app(sk1,X0) != sk2
| ~ ssList(X0)
| ~ lt(sk8(X0),sk6(sk5))
| ~ ssList(sk9(X0))
| ~ ssItem(sk8(X0))
| nil != sk2 ),
inference(resolution,[status(thm)],[f626,f532]) ).
fof(f645,plain,
! [X0] :
( app(sk1,X0) != sk2
| ~ ssList(X0)
| ~ lt(sk8(X0),sk6(sk5))
| ~ ssList(sk9(X0))
| ~ ssItem(sk8(X0))
| nil != sk2 ),
inference(duplicate_literals_removal,[status(thm)],[f643]) ).
fof(f646,plain,
! [X0] :
( app(sk1,X0) != sk2
| ~ ssList(X0)
| ~ lt(sk8(X0),sk6(sk5))
| ~ ssList(sk9(X0))
| nil != sk2 ),
inference(forward_subsumption_resolution,[status(thm)],[f645,f530]) ).
fof(f648,plain,
! [X0] :
( nil = sk1
| app(sk1,X0) != sk2
| ~ ssList(X0)
| nil = sk1
| ~ lt(sk8(X0),sk6(sk5))
| ~ ssList(sk9(X0))
| ~ ssItem(sk8(X0)) ),
inference(resolution,[status(thm)],[f630,f526]) ).
fof(f649,plain,
! [X0] :
( app(sk1,X0) != sk2
| ~ ssList(X0)
| nil = sk1
| ~ lt(sk8(X0),sk6(sk5))
| ~ ssList(sk9(X0))
| ~ ssItem(sk8(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f648]) ).
fof(f650,plain,
! [X0] :
( app(sk1,X0) != sk2
| ~ ssList(X0)
| nil = sk1
| ~ lt(sk8(X0),sk6(sk5))
| ~ ssList(sk9(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f649,f524]) ).
fof(f651,plain,
( ~ ssList(sk5)
| ~ lt(sk8(sk5),sk6(sk5))
| ~ ssList(sk9(sk5))
| nil != sk2 ),
inference(resolution,[status(thm)],[f646,f515]) ).
fof(f653,plain,
( ~ ssList(sk5)
| ~ lt(sk8(sk5),sk6(sk5))
| nil != sk2 ),
inference(forward_subsumption_resolution,[status(thm)],[f651,f635]) ).
fof(f655,plain,
( ~ ssList(sk5)
| nil = sk1
| ~ lt(sk8(sk5),sk6(sk5))
| ~ ssList(sk9(sk5)) ),
inference(resolution,[status(thm)],[f650,f515]) ).
fof(f657,plain,
( ~ ssList(sk5)
| nil = sk1
| ~ lt(sk8(sk5),sk6(sk5)) ),
inference(forward_subsumption_resolution,[status(thm)],[f655,f635]) ).
fof(f659,plain,
( nil != sk1
| ~ ssList(sk5)
| ~ lt(sk8(sk5),sk6(sk5)) ),
inference(resolution,[status(thm)],[f653,f519]) ).
fof(f661,plain,
( ~ ssList(sk5)
| ~ lt(sk8(sk5),sk6(sk5)) ),
inference(backward_subsumption_resolution,[status(thm)],[f657,f662]) ).
fof(f662,plain,
( nil != sk1
| ~ ssList(sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[f659,f642]) ).
fof(f665,plain,
~ ssList(sk5),
inference(forward_subsumption_resolution,[status(thm)],[f661,f642]) ).
fof(f666,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f447,f665]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC343-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n007.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 08:15:20 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.45 % Drodi V4.1.1
% 0.15/0.55 % Refutation found
% 0.15/0.55 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/0.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.58 % Elapsed time: 0.137703 seconds
% 0.15/0.58 % CPU time: 0.747739 seconds
% 0.15/0.58 % Total memory used: 118.344 MB
% 0.15/0.58 % Net memory used: 117.786 MB
%------------------------------------------------------------------------------