%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PUZ133+2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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:00:09 PM UTC 2026
% Result : Theorem 0.11s 0.46s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 32
% Syntax : Number of formulae : 144 ( 13 unt; 23 def)
% Number of atoms : 429 ( 97 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 488 ( 203 ~; 208 |; 42 &)
% ( 27 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 28 ( 26 usr; 26 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 100 ( 96 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( queens_p
=> ! [I,J] :
( ( le(J,n)
& le(s(I),J)
& le(I,n)
& le(s(n0),I) )
=> ( minus(p(I),I) != minus(p(J),J)
& plus(p(I),I) != plus(p(J),J)
& p(I) != p(J) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
( ! [I,J] :
( ( ( le(s(I),J)
<=> le(s(perm(J)),perm(I)) )
& le(J,n)
& le(s(I),J)
& le(I,n)
& le(s(n0),I) )
=> ( minus(q(I),I) != minus(q(J),J)
& plus(q(I),I) != plus(q(J),J)
& q(I) != q(J) ) )
=> queens_q ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,conjecture,
( ( ! [I] : q(I) = p(perm(I))
& queens_p )
=> queens_q ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
~ ( ( ! [I] : q(I) = p(perm(I))
& queens_p )
=> queens_q ),
inference(negated_conjecture,[status(cth)],[f4]) ).
fof(f6,axiom,
! [I] :
( ( le(I,n)
& le(s(n0),I) )
=> ( le(perm(I),n)
& le(s(n0),perm(I)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [J,I] : minus(I,J) = minus(perm(J),perm(I)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y,Z] :
( ( le(Y,Z)
& le(X,Y) )
=> le(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X] : le(X,s(X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [I,J,K,L] :
( plus(I,J) = plus(K,L)
<=> minus(I,K) = minus(L,J) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [I,J,K,L] :
( minus(I,J) = minus(K,L)
<=> minus(I,K) = minus(J,L) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,plain,
( ! [I,J] :
( ( minus(p(I),I) != minus(p(J),J)
& plus(p(I),I) != plus(p(J),J)
& p(I) != p(J) )
| ~ le(J,n)
| ~ le(s(I),J)
| ~ le(I,n)
| ~ le(s(n0),I) )
| ~ queens_p ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f13,plain,
! [X0,X1] :
( p(X0) != p(X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0)
| ~ queens_p ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f14,plain,
! [X0,X1] :
( plus(p(X0),X0) != plus(p(X1),X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0)
| ~ queens_p ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f15,plain,
! [X0,X1] :
( minus(p(X0),X0) != minus(p(X1),X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0)
| ~ queens_p ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f18,plain,
( queens_q
| ? [I,J] :
( ( minus(q(I),I) = minus(q(J),J)
| plus(q(I),I) = plus(q(J),J)
| q(I) = q(J) )
& ( le(s(I),J)
<=> le(s(perm(J)),perm(I)) )
& le(J,n)
& le(s(I),J)
& le(I,n)
& le(s(n0),I) ) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f19,plain,
( queens_q
| ? [I,J] :
( ( minus(q(I),I) = minus(q(J),J)
| plus(q(I),I) = plus(q(J),J)
| q(I) = q(J) )
& ( ~ le(s(perm(J)),perm(I))
| le(s(I),J) )
& ( le(s(perm(J)),perm(I))
| ~ le(s(I),J) )
& le(J,n)
& le(s(I),J)
& le(I,n)
& le(s(n0),I) ) ),
inference(NNF_transformation,[status(thm)],[f18]) ).
fof(f20,plain,
( queens_q
| ( ( minus(q(sK0_skl),sK0_skl) = minus(q(sK1_skl),sK1_skl)
| plus(q(sK0_skl),sK0_skl) = plus(q(sK1_skl),sK1_skl)
| q(sK0_skl) = q(sK1_skl) )
& ( ~ le(s(perm(sK1_skl)),perm(sK0_skl))
| le(s(sK0_skl),sK1_skl) )
& ( le(s(perm(sK1_skl)),perm(sK0_skl))
| ~ le(s(sK0_skl),sK1_skl) )
& le(sK1_skl,n)
& le(s(sK0_skl),sK1_skl)
& le(sK0_skl,n)
& le(s(n0),sK0_skl) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(I,sK0_skl),skolemize(J,sK1_skl)],[f19]) ).
fof(f21,plain,
( queens_q
| le(s(n0),sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f22,plain,
( queens_q
| le(sK0_skl,n) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f23,plain,
( queens_q
| le(s(sK0_skl),sK1_skl) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f24,plain,
( queens_q
| le(sK1_skl,n) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f25,plain,
( queens_q
| le(s(perm(sK1_skl)),perm(sK0_skl))
| ~ le(s(sK0_skl),sK1_skl) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f27,plain,
( queens_q
| minus(q(sK0_skl),sK0_skl) = minus(q(sK1_skl),sK1_skl)
| plus(q(sK0_skl),sK0_skl) = plus(q(sK1_skl),sK1_skl)
| q(sK0_skl) = q(sK1_skl) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f28,plain,
( ~ queens_q
& ! [I] : q(I) = p(perm(I))
& queens_p ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f29,plain,
queens_p,
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f30,plain,
! [X0] : q(X0) = p(perm(X0)),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f31,plain,
~ queens_q,
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f32,plain,
! [I] :
( ( le(perm(I),n)
& le(s(n0),perm(I)) )
| ~ le(I,n)
| ~ le(s(n0),I) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f33,plain,
! [X0] :
( le(s(n0),perm(X0))
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f34,plain,
! [X0] :
( le(perm(X0),n)
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f35,plain,
! [X0,X1] : minus(X0,X1) = minus(perm(X1),perm(X0)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f36,plain,
! [X,Y,Z] :
( le(X,Z)
| ~ le(Y,Z)
| ~ le(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f37,plain,
! [X,Z] :
( le(X,Z)
| ! [Y] :
( ~ le(Y,Z)
| ~ le(X,Y) ) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f38,plain,
! [X0,X1,X2] :
( le(X0,X2)
| ~ le(X1,X2)
| ~ le(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f39,plain,
! [X0] : le(X0,s(X0)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f40,plain,
! [I,J,K,L] :
( ( minus(I,K) != minus(L,J)
| plus(I,J) = plus(K,L) )
& ( minus(I,K) = minus(L,J)
| plus(I,J) != plus(K,L) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f41,plain,
( ! [I,J,K,L] :
( minus(I,K) != minus(L,J)
| plus(I,J) = plus(K,L) )
& ! [I,J,K,L] :
( minus(I,K) = minus(L,J)
| plus(I,J) != plus(K,L) ) ),
inference(miniscoping,[status(thm)],[f40]) ).
fof(f42,plain,
! [X0,X1,X2,X3] :
( minus(X0,X2) = minus(X3,X1)
| plus(X0,X1) != plus(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f43,plain,
! [X0,X1,X2,X3] :
( minus(X0,X2) != minus(X3,X1)
| plus(X0,X1) = plus(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f44,plain,
! [I,J,K,L] :
( ( minus(I,K) != minus(J,L)
| minus(I,J) = minus(K,L) )
& ( minus(I,K) = minus(J,L)
| minus(I,J) != minus(K,L) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f45,plain,
( ! [I,J,K,L] :
( minus(I,K) != minus(J,L)
| minus(I,J) = minus(K,L) )
& ! [I,J,K,L] :
( minus(I,K) = minus(J,L)
| minus(I,J) != minus(K,L) ) ),
inference(miniscoping,[status(thm)],[f44]) ).
fof(f46,plain,
! [X0,X1,X2,X3] :
( minus(X0,X2) = minus(X1,X3)
| minus(X0,X1) != minus(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f48,definition,
( sQ0_spl
<=> queens_p ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f50,plain,
( sQ0_spl
| ~ queens_p ),
inference(component_clause,[status(thm)],[f48]) ).
fof(f51,definition,
! [X0,X1] :
( sQ1_spl
<=> ( p(X0) != p(X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f52,plain,
! [X0,X1] :
( ~ sQ1_spl
| p(X0) != p(X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(component_clause,[status(thm)],[f51]) ).
fof(f54,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f13,f48,f51]) ).
fof(f55,definition,
! [X0,X1] :
( sQ2_spl
<=> ( plus(p(X0),X0) != plus(p(X1),X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f56,plain,
! [X0,X1] :
( ~ sQ2_spl
| plus(p(X0),X0) != plus(p(X1),X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(component_clause,[status(thm)],[f55]) ).
fof(f58,plain,
( sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f14,f48,f55]) ).
fof(f59,definition,
! [X0,X1] :
( sQ3_spl
<=> ( minus(p(X0),X0) != minus(p(X1),X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f60,plain,
! [X0,X1] :
( ~ sQ3_spl
| minus(p(X0),X0) != minus(p(X1),X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(component_clause,[status(thm)],[f59]) ).
fof(f62,plain,
( sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f15,f48,f59]) ).
fof(f63,definition,
( sQ4_spl
<=> le(s(n0),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f64,plain,
( ~ sQ4_spl
| le(s(n0),sK0_skl) ),
inference(component_clause,[status(thm)],[f63]) ).
fof(f66,definition,
( sQ5_spl
<=> queens_q ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f67,plain,
( ~ sQ5_spl
| queens_q ),
inference(component_clause,[status(thm)],[f66]) ).
fof(f69,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f21,f63,f66]) ).
fof(f70,definition,
( sQ6_spl
<=> le(sK0_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f73,plain,
( sQ5_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f22,f70,f66]) ).
fof(f74,definition,
( sQ7_spl
<=> le(s(sK0_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f75,plain,
( ~ sQ7_spl
| le(s(sK0_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f74]) ).
fof(f77,plain,
( sQ5_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f23,f74,f66]) ).
fof(f78,definition,
( sQ8_spl
<=> le(sK1_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f81,plain,
( sQ5_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f24,f78,f66]) ).
fof(f82,definition,
( sQ9_spl
<=> le(s(perm(sK1_skl)),perm(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f83,plain,
( ~ sQ9_spl
| le(s(perm(sK1_skl)),perm(sK0_skl)) ),
inference(component_clause,[status(thm)],[f82]) ).
fof(f85,plain,
( sQ5_spl
| sQ9_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f25,f74,f82,f66]) ).
fof(f87,definition,
( sQ10_spl
<=> q(sK0_skl) = q(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f88,plain,
( ~ sQ10_spl
| q(sK0_skl) = q(sK1_skl) ),
inference(component_clause,[status(thm)],[f87]) ).
fof(f90,definition,
( sQ11_spl
<=> plus(q(sK0_skl),sK0_skl) = plus(q(sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f91,plain,
( ~ sQ11_spl
| plus(q(sK0_skl),sK0_skl) = plus(q(sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f90]) ).
fof(f93,definition,
( sQ12_spl
<=> minus(q(sK0_skl),sK0_skl) = minus(q(sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f94,plain,
( ~ sQ12_spl
| minus(q(sK0_skl),sK0_skl) = minus(q(sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f93]) ).
fof(f96,plain,
( sQ5_spl
| sQ12_spl
| sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f27,f87,f90,f93,f66]) ).
fof(f97,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f67,f31]) ).
fof(f98,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f97]) ).
fof(f99,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f50,f29]) ).
fof(f100,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f99]) ).
fof(f104,plain,
( ~ sQ9_spl
| ~ sQ1_spl
| p(perm(sK1_skl)) != p(perm(sK0_skl))
| ~ le(perm(sK0_skl),n)
| ~ le(perm(sK1_skl),n)
| ~ le(s(n0),perm(sK1_skl)) ),
inference(resolution,[status(thm)],[f52,f83]) ).
fof(f122,definition,
( sQ16_spl
<=> le(s(n0),perm(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f124,plain,
( sQ16_spl
| ~ le(s(n0),perm(sK1_skl)) ),
inference(component_clause,[status(thm)],[f122]) ).
fof(f125,definition,
( sQ17_spl
<=> le(perm(sK1_skl),n) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f127,plain,
( sQ17_spl
| ~ le(perm(sK1_skl),n) ),
inference(component_clause,[status(thm)],[f125]) ).
fof(f128,definition,
( sQ18_spl
<=> le(perm(sK0_skl),n) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f130,plain,
( sQ18_spl
| ~ le(perm(sK0_skl),n) ),
inference(component_clause,[status(thm)],[f128]) ).
fof(f131,definition,
( sQ19_spl
<=> p(perm(sK1_skl)) = p(perm(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f133,plain,
( sQ19_spl
| p(perm(sK1_skl)) != p(perm(sK0_skl)) ),
inference(component_clause,[status(thm)],[f131]) ).
fof(f134,plain,
( ~ sQ9_spl
| ~ sQ1_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f104,f122,f125,f128,f131,f51,f82]) ).
fof(f155,plain,
( sQ19_spl
| q(sK1_skl) != p(perm(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f30,f133]) ).
fof(f156,plain,
( sQ19_spl
| q(sK1_skl) != q(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f30,f155]) ).
fof(f162,definition,
( sQ26_spl
<=> le(s(n0),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f164,plain,
( sQ26_spl
| ~ le(s(n0),sK1_skl) ),
inference(component_clause,[status(thm)],[f162]) ).
fof(f179,plain,
( sQ18_spl
| ~ le(sK0_skl,n)
| ~ le(s(n0),sK0_skl) ),
inference(resolution,[status(thm)],[f130,f34]) ).
fof(f180,plain,
( sQ18_spl
| ~ sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f179,f63,f70,f128]) ).
fof(f181,plain,
( sQ17_spl
| ~ le(sK1_skl,n)
| ~ le(s(n0),sK1_skl) ),
inference(resolution,[status(thm)],[f127,f34]) ).
fof(f182,plain,
( sQ17_spl
| ~ sQ8_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f181,f162,f78,f125]) ).
fof(f186,plain,
( ~ sQ9_spl
| ~ sQ2_spl
| plus(p(perm(sK1_skl)),perm(sK1_skl)) != plus(p(perm(sK0_skl)),perm(sK0_skl))
| ~ le(perm(sK0_skl),n)
| ~ le(perm(sK1_skl),n)
| ~ le(s(n0),perm(sK1_skl)) ),
inference(resolution,[status(thm)],[f56,f83]) ).
fof(f201,definition,
( sQ31_spl
<=> plus(p(perm(sK1_skl)),perm(sK1_skl)) = plus(p(perm(sK0_skl)),perm(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f203,plain,
( sQ31_spl
| plus(p(perm(sK1_skl)),perm(sK1_skl)) != plus(p(perm(sK0_skl)),perm(sK0_skl)) ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f204,plain,
( ~ sQ9_spl
| ~ sQ2_spl
| ~ sQ31_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f186,f122,f125,f128,f201,f55,f82]) ).
fof(f219,plain,
( sQ31_spl
| plus(q(sK1_skl),perm(sK1_skl)) != plus(p(perm(sK0_skl)),perm(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f30,f203]) ).
fof(f220,plain,
( sQ31_spl
| plus(q(sK1_skl),perm(sK1_skl)) != plus(q(sK0_skl),perm(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f30,f219]) ).
fof(f243,plain,
( ~ sQ9_spl
| ~ sQ3_spl
| minus(p(perm(sK1_skl)),perm(sK1_skl)) != minus(p(perm(sK0_skl)),perm(sK0_skl))
| ~ le(perm(sK0_skl),n)
| ~ le(perm(sK1_skl),n)
| ~ le(s(n0),perm(sK1_skl)) ),
inference(resolution,[status(thm)],[f60,f83]) ).
fof(f258,definition,
( sQ40_spl
<=> minus(p(perm(sK1_skl)),perm(sK1_skl)) = minus(p(perm(sK0_skl)),perm(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f260,plain,
( sQ40_spl
| minus(p(perm(sK1_skl)),perm(sK1_skl)) != minus(p(perm(sK0_skl)),perm(sK0_skl)) ),
inference(component_clause,[status(thm)],[f258]) ).
fof(f261,plain,
( ~ sQ9_spl
| ~ sQ3_spl
| ~ sQ40_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f243,f122,f125,f128,f258,f59,f82]) ).
fof(f276,plain,
( sQ40_spl
| minus(q(sK1_skl),perm(sK1_skl)) != minus(p(perm(sK0_skl)),perm(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f30,f260]) ).
fof(f277,plain,
( sQ40_spl
| minus(q(sK1_skl),perm(sK1_skl)) != minus(q(sK0_skl),perm(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f30,f276]) ).
fof(f297,plain,
( sQ16_spl
| ~ le(sK1_skl,n)
| ~ le(s(n0),sK1_skl) ),
inference(resolution,[status(thm)],[f124,f33]) ).
fof(f298,plain,
( sQ16_spl
| ~ sQ8_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f297,f162,f78,f122]) ).
fof(f358,plain,
! [X0] :
( sQ26_spl
| ~ le(X0,sK1_skl)
| ~ le(s(n0),X0) ),
inference(resolution,[status(thm)],[f38,f164]) ).
fof(f374,definition,
( sQ56_spl
<=> minus(p(n0),n0) = minus(p(n0),n0) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f376,plain,
( sQ56_spl
| minus(p(n0),n0) != minus(p(n0),n0) ),
inference(component_clause,[status(thm)],[f374]) ).
fof(f378,definition,
( sQ57_spl
<=> plus(p(n0),n0) = plus(p(n0),n0) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f380,plain,
( sQ57_spl
| plus(p(n0),n0) != plus(p(n0),n0) ),
inference(component_clause,[status(thm)],[f378]) ).
fof(f382,definition,
( sQ58_spl
<=> p(n0) = p(n0) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f384,plain,
( sQ58_spl
| p(n0) != p(n0) ),
inference(component_clause,[status(thm)],[f382]) ).
fof(f389,plain,
( sQ58_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f384]) ).
fof(f390,plain,
sQ58_spl,
inference(contradiction_clause,[status(thm)],[f389]) ).
fof(f391,plain,
( sQ57_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f380]) ).
fof(f392,plain,
sQ57_spl,
inference(contradiction_clause,[status(thm)],[f391]) ).
fof(f393,plain,
( sQ56_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f376]) ).
fof(f394,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f393]) ).
fof(f427,plain,
( sQ31_spl
| minus(q(sK1_skl),q(sK0_skl)) != minus(perm(sK0_skl),perm(sK1_skl)) ),
inference(resolution,[status(thm)],[f43,f220]) ).
fof(f435,plain,
( sQ31_spl
| minus(q(sK1_skl),q(sK0_skl)) != minus(sK1_skl,sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f35,f427]) ).
fof(f443,plain,
( sQ40_spl
| minus(q(sK1_skl),q(sK0_skl)) != minus(perm(sK1_skl),perm(sK0_skl)) ),
inference(resolution,[status(thm)],[f46,f277]) ).
fof(f455,plain,
( sQ40_spl
| minus(q(sK1_skl),q(sK0_skl)) != minus(sK0_skl,sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f35,f443]) ).
fof(f458,plain,
( ~ sQ4_spl
| sQ26_spl
| ~ le(sK0_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f358,f64]) ).
fof(f461,plain,
! [X0] :
( ~ sQ4_spl
| sQ26_spl
| ~ le(X0,sK1_skl)
| ~ le(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f458,f38]) ).
fof(f464,plain,
( ~ sQ4_spl
| sQ26_spl
| ~ le(s(sK0_skl),sK1_skl) ),
inference(resolution,[status(thm)],[f461,f39]) ).
fof(f468,plain,
( ~ sQ4_spl
| sQ26_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f464,f75]) ).
fof(f469,plain,
( ~ sQ4_spl
| sQ26_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f468]) ).
fof(f721,plain,
( sQ31_spl
| minus(q(sK1_skl),sK1_skl) != minus(q(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f435,f46]) ).
fof(f725,plain,
( sQ31_spl
| ~ sQ12_spl
| minus(q(sK0_skl),sK0_skl) != minus(q(sK0_skl),sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f94,f721]) ).
fof(f726,plain,
( sQ31_spl
| ~ sQ12_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f725]) ).
fof(f727,plain,
( sQ31_spl
| ~ sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f726]) ).
fof(f728,plain,
( ~ sQ10_spl
| sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f88,f156]) ).
fof(f729,plain,
( ~ sQ10_spl
| sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f728]) ).
fof(f735,plain,
( sQ40_spl
| plus(q(sK1_skl),sK1_skl) != plus(q(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f455,f42]) ).
fof(f738,plain,
( sQ40_spl
| ~ sQ11_spl
| plus(q(sK0_skl),sK0_skl) != plus(q(sK0_skl),sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f91,f735]) ).
fof(f739,plain,
( sQ40_spl
| ~ sQ11_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f738]) ).
fof(f740,plain,
( sQ40_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f739]) ).
fof(f741,plain,
$false,
inference(sat_refutation,[status(thm)],[f54,f58,f62,f69,f73,f77,f81,f85,f96,f98,f100,f134,f180,f182,f204,f261,f298,f390,f392,f394,f469,f727,f729,f740]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ133+2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n001.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 21 03:57:28 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.40 % Drodi V4.1.1
% 0.11/0.46 % Refutation found
% 0.11/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.11/0.49 % Elapsed time: 0.096557 seconds
% 0.11/0.49 % CPU time: 0.454388 seconds
% 0.11/0.49 % Total memory used: 106.200 MB
% 0.11/0.49 % Net memory used: 105.272 MB
%------------------------------------------------------------------------------