%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PUZ133+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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.16s 16.06s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 28
% Syntax : Number of formulae : 124 ( 12 unt; 19 def)
% Number of atoms : 421 ( 86 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 533 ( 236 ~; 224 |; 42 &)
% ( 23 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 24 ( 22 usr; 22 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 124 ( 120 !; 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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f4,conjecture,
( ( ! [I] : q(I) = p(perm(I))
& queens_p )
=> queens_q ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [J,I] : minus(I,J) = minus(perm(J),perm(I)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y,Z] :
( ( le(Y,Z)
& le(X,Y) )
=> le(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X] : le(X,s(X)),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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(f17,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(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(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)],[f17]) ).
fof(f19,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)],[f18]) ).
fof(f20,plain,
( queens_q
| le(s(n0),sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f21,plain,
( queens_q
| le(sK0_skl,n) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f22,plain,
( queens_q
| le(s(sK0_skl),sK1_skl) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f23,plain,
( queens_q
| le(sK1_skl,n) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f24,plain,
( queens_q
| le(s(perm(sK1_skl)),perm(sK0_skl))
| ~ le(s(sK0_skl),sK1_skl) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f26,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)],[f19]) ).
fof(f27,plain,
( ~ queens_q
& ! [I] : q(I) = p(perm(I))
& queens_p ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f28,plain,
queens_p,
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f29,plain,
! [X0] : q(X0) = p(perm(X0)),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f30,plain,
~ queens_q,
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f31,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(f32,plain,
! [X0] :
( le(s(n0),perm(X0))
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f33,plain,
! [X0] :
( le(perm(X0),n)
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f34,plain,
! [X0,X1] : minus(X0,X1) = minus(perm(X1),perm(X0)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f35,plain,
! [X,Y,Z] :
( le(X,Z)
| ~ le(Y,Z)
| ~ le(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f36,plain,
! [X,Z] :
( le(X,Z)
| ! [Y] :
( ~ le(Y,Z)
| ~ le(X,Y) ) ),
inference(miniscoping,[status(thm)],[f35]) ).
fof(f37,plain,
! [X0,X1,X2] :
( le(X0,X2)
| ~ le(X1,X2)
| ~ le(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f38,plain,
! [X0] : le(X0,s(X0)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f39,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(f40,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)],[f39]) ).
fof(f41,plain,
! [X0,X1,X2,X3] :
( minus(X0,X2) = minus(X3,X1)
| plus(X0,X1) != plus(X2,X3) ),
inference(cnf_transformation,[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)],[f40]) ).
fof(f43,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(f44,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)],[f43]) ).
fof(f45,plain,
! [X0,X1,X2,X3] :
( minus(X0,X2) = minus(X1,X3)
| minus(X0,X1) != minus(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f47,definition,
( sQ0_spl
<=> queens_p ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f49,plain,
( sQ0_spl
| ~ queens_p ),
inference(component_clause,[status(thm)],[f47]) ).
fof(f50,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(f51,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)],[f50]) ).
fof(f53,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f13,f47,f50]) ).
fof(f54,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(f55,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)],[f54]) ).
fof(f57,plain,
( sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f14,f47,f54]) ).
fof(f58,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(f59,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)],[f58]) ).
fof(f61,plain,
( sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f15,f47,f58]) ).
fof(f62,definition,
( sQ4_spl
<=> le(s(n0),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f63,plain,
( ~ sQ4_spl
| le(s(n0),sK0_skl) ),
inference(component_clause,[status(thm)],[f62]) ).
fof(f65,definition,
( sQ5_spl
<=> queens_q ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f66,plain,
( ~ sQ5_spl
| queens_q ),
inference(component_clause,[status(thm)],[f65]) ).
fof(f68,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f20,f62,f65]) ).
fof(f69,definition,
( sQ6_spl
<=> le(sK0_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f72,plain,
( sQ5_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f21,f69,f65]) ).
fof(f73,definition,
( sQ7_spl
<=> le(s(sK0_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f74,plain,
( ~ sQ7_spl
| le(s(sK0_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f73]) ).
fof(f76,plain,
( sQ5_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f22,f73,f65]) ).
fof(f77,definition,
( sQ8_spl
<=> le(sK1_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f80,plain,
( sQ5_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f23,f77,f65]) ).
fof(f81,definition,
( sQ9_spl
<=> le(s(perm(sK1_skl)),perm(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f84,plain,
( sQ5_spl
| sQ9_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f24,f73,f81,f65]) ).
fof(f86,definition,
( sQ10_spl
<=> q(sK0_skl) = q(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f87,plain,
( ~ sQ10_spl
| q(sK0_skl) = q(sK1_skl) ),
inference(component_clause,[status(thm)],[f86]) ).
fof(f89,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(f90,plain,
( ~ sQ11_spl
| plus(q(sK0_skl),sK0_skl) = plus(q(sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f89]) ).
fof(f92,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(f93,plain,
( ~ sQ12_spl
| minus(q(sK0_skl),sK0_skl) = minus(q(sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f92]) ).
fof(f95,plain,
( sQ5_spl
| sQ12_spl
| sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f26,f86,f89,f92,f65]) ).
fof(f96,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f49,f28]) ).
fof(f97,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f96]) ).
fof(f99,plain,
! [X0,X1] :
( ~ sQ1_spl
| p(X0) != q(X1)
| ~ le(perm(X1),n)
| ~ le(s(X0),perm(X1))
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(paramodulation,[status(thm)],[f29,f51]) ).
fof(f103,plain,
! [X0,X1] :
( ~ sQ1_spl
| q(X0) != q(X1)
| ~ le(perm(X1),n)
| ~ le(s(perm(X0)),perm(X1))
| ~ le(perm(X0),n)
| ~ le(s(n0),perm(X0)) ),
inference(paramodulation,[status(thm)],[f29,f99]) ).
fof(f106,plain,
! [X0,X1] :
( ~ sQ2_spl
| plus(p(X0),X0) != plus(q(X1),perm(X1))
| ~ le(perm(X1),n)
| ~ le(s(X0),perm(X1))
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(paramodulation,[status(thm)],[f29,f55]) ).
fof(f109,plain,
! [X0,X1] :
( ~ sQ3_spl
| minus(q(X0),perm(X0)) != minus(p(X1),X1)
| ~ le(X1,n)
| ~ le(s(perm(X0)),X1)
| ~ le(perm(X0),n)
| ~ le(s(n0),perm(X0)) ),
inference(paramodulation,[status(thm)],[f29,f59]) ).
fof(f118,plain,
! [X0,X1] :
( ~ sQ2_spl
| plus(q(X0),perm(X0)) != plus(q(X1),perm(X1))
| ~ le(perm(X1),n)
| ~ le(s(perm(X0)),perm(X1))
| ~ le(perm(X0),n)
| ~ le(s(n0),perm(X0)) ),
inference(paramodulation,[status(thm)],[f29,f106]) ).
fof(f122,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f66,f30]) ).
fof(f123,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f122]) ).
fof(f137,plain,
! [X0] :
( ~ sQ7_spl
| le(X0,sK1_skl)
| ~ le(X0,s(sK0_skl)) ),
inference(resolution,[status(thm)],[f37,f74]) ).
fof(f158,plain,
( ~ sQ4_spl
| le(perm(sK0_skl),n)
| ~ le(sK0_skl,n) ),
inference(resolution,[status(thm)],[f33,f63]) ).
fof(f165,definition,
( sQ19_spl
<=> le(perm(sK0_skl),n) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f168,plain,
( ~ sQ4_spl
| sQ19_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f158,f69,f165,f62]) ).
fof(f180,plain,
( ~ sQ7_spl
| le(sK0_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f137,f38]) ).
fof(f182,plain,
! [X0] :
( ~ sQ7_spl
| le(X0,sK1_skl)
| ~ le(X0,sK0_skl) ),
inference(resolution,[status(thm)],[f180,f37]) ).
fof(f183,plain,
( ~ sQ4_spl
| ~ sQ7_spl
| le(s(n0),sK1_skl) ),
inference(resolution,[status(thm)],[f182,f63]) ).
fof(f184,plain,
( ~ sQ4_spl
| ~ sQ7_spl
| le(perm(sK1_skl),n)
| ~ le(sK1_skl,n) ),
inference(resolution,[status(thm)],[f183,f33]) ).
fof(f188,definition,
( sQ21_spl
<=> le(perm(sK1_skl),n) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f191,plain,
( ~ sQ4_spl
| ~ sQ7_spl
| sQ21_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f184,f77,f188,f73,f62]) ).
fof(f240,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ le(perm(X0),n)
| ~ le(s(perm(X1)),perm(X0))
| ~ le(perm(X1),n)
| ~ le(s(n0),perm(X1))
| minus(q(X0),q(X1)) != minus(perm(X1),perm(X0)) ),
inference(resolution,[status(thm)],[f42,f118]) ).
fof(f246,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ le(perm(X0),n)
| ~ le(s(perm(X1)),perm(X0))
| ~ le(perm(X1),n)
| ~ le(s(n0),perm(X1))
| minus(q(X0),q(X1)) != minus(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f34,f240]) ).
fof(f247,plain,
( ~ sQ12_spl
| minus(q(sK0_skl),q(sK1_skl)) = minus(sK0_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f45,f93]) ).
fof(f256,plain,
! [X0,X1,X2,X3] :
( minus(X0,perm(X3)) = minus(X1,perm(X2))
| minus(X0,X1) != minus(X2,X3) ),
inference(paramodulation,[status(thm)],[f34,f45]) ).
fof(f286,definition,
( sQ24_spl
<=> le(s(n0),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f288,plain,
( sQ24_spl
| ~ le(s(n0),sK1_skl) ),
inference(component_clause,[status(thm)],[f286]) ).
fof(f290,plain,
( sQ24_spl
| ~ sQ4_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f288,f183]) ).
fof(f291,plain,
( sQ24_spl
| ~ sQ4_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f290]) ).
fof(f856,definition,
( sQ44_spl
<=> perm(perm(p(perm(s(n))))) = perm(perm(q(s(n)))) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f858,plain,
( sQ44_spl
| perm(perm(p(perm(s(n))))) != perm(perm(q(s(n)))) ),
inference(component_clause,[status(thm)],[f856]) ).
fof(f893,plain,
( sQ44_spl
| perm(perm(q(s(n)))) != perm(perm(q(s(n)))) ),
inference(forward_demodulation,[status(thm)],[f29,f858]) ).
fof(f894,plain,
( sQ44_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f893]) ).
fof(f895,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f894]) ).
fof(f898,plain,
( ~ sQ2_spl
| ~ sQ12_spl
| ~ le(perm(sK0_skl),n)
| ~ le(s(perm(sK1_skl)),perm(sK0_skl))
| ~ le(perm(sK1_skl),n)
| ~ le(s(n0),perm(sK1_skl)) ),
inference(resolution,[status(thm)],[f247,f246]) ).
fof(f909,definition,
( sQ50_spl
<=> le(s(n0),perm(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f911,plain,
( sQ50_spl
| ~ le(s(n0),perm(sK1_skl)) ),
inference(component_clause,[status(thm)],[f909]) ).
fof(f912,plain,
( ~ sQ2_spl
| ~ sQ12_spl
| ~ sQ19_spl
| ~ sQ9_spl
| ~ sQ21_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f898,f909,f188,f81,f165,f92,f54]) ).
fof(f923,plain,
( ~ sQ1_spl
| ~ sQ10_spl
| ~ le(perm(sK0_skl),n)
| ~ le(s(perm(sK1_skl)),perm(sK0_skl))
| ~ le(perm(sK1_skl),n)
| ~ le(s(n0),perm(sK1_skl)) ),
inference(resolution,[status(thm)],[f87,f103]) ).
fof(f945,plain,
( ~ sQ1_spl
| ~ sQ10_spl
| ~ sQ19_spl
| ~ sQ9_spl
| ~ sQ21_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f923,f909,f188,f81,f165,f86,f50]) ).
fof(f1026,plain,
( sQ50_spl
| ~ le(sK1_skl,n)
| ~ le(s(n0),sK1_skl) ),
inference(resolution,[status(thm)],[f911,f32]) ).
fof(f1027,plain,
( sQ50_spl
| ~ sQ8_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1026,f286,f77,f909]) ).
fof(f1060,plain,
( ~ sQ11_spl
| minus(q(sK1_skl),q(sK0_skl)) = minus(sK0_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f90,f41]) ).
fof(f1180,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ le(perm(X1),n)
| ~ le(s(perm(X0)),perm(X1))
| ~ le(perm(X0),n)
| ~ le(s(n0),perm(X0))
| minus(q(X0),p(perm(X1))) != minus(X1,X0) ),
inference(resolution,[status(thm)],[f256,f109]) ).
fof(f1217,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ le(perm(X1),n)
| ~ le(s(perm(X0)),perm(X1))
| ~ le(perm(X0),n)
| ~ le(s(n0),perm(X0))
| minus(q(X0),q(X1)) != minus(X1,X0) ),
inference(forward_demodulation,[status(thm)],[f29,f1180]) ).
fof(f1601,definition,
! [X0] :
( sQ116_spl
<=> perm(X0) != perm(X0) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1602,plain,
! [X0] :
( ~ sQ116_spl
| perm(X0) != perm(X0) ),
inference(component_clause,[status(thm)],[f1601]) ).
fof(f1608,plain,
( ~ sQ116_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1602]) ).
fof(f1609,plain,
~ sQ116_spl,
inference(contradiction_clause,[status(thm)],[f1608]) ).
fof(f3499,plain,
( ~ sQ11_spl
| ~ sQ3_spl
| ~ le(perm(sK0_skl),n)
| ~ le(s(perm(sK1_skl)),perm(sK0_skl))
| ~ le(perm(sK1_skl),n)
| ~ le(s(n0),perm(sK1_skl)) ),
inference(resolution,[status(thm)],[f1217,f1060]) ).
fof(f3516,plain,
( ~ sQ11_spl
| ~ sQ3_spl
| ~ sQ19_spl
| ~ sQ9_spl
| ~ sQ21_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f3499,f909,f188,f81,f165,f58,f89]) ).
fof(f3541,plain,
$false,
inference(sat_refutation,[status(thm)],[f53,f57,f61,f68,f72,f76,f80,f84,f95,f97,f123,f168,f191,f291,f895,f912,f945,f1027,f1609,f3516]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ133+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/15.38 % Computer : n010.cluster.edu
% 0.10/15.38 % Model : x86_64 x86_64
% 0.10/15.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/15.38 % Memory : 8046.5625MB
% 0.10/15.38 % OS : Linux 6.8.0-71-generic
% 0.10/15.38 % CPULimit : 300
% 0.10/15.38 % WCLimit : 300
% 0.10/15.38 % DateTime : Mon Sep 21 03:52:40 UTC 2026
% 0.10/15.39 % CPUTime :
% 0.16/15.40 % Drodi V4.1.1
% 0.16/16.06 % Refutation found
% 0.16/16.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/16.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.16/16.09 % Elapsed time: 0.688037 seconds
% 0.16/16.09 % CPU time: 5.240367 seconds
% 0.16/16.09 % Total memory used: 150.672 MB
% 0.16/16.09 % Net memory used: 142.551 MB
%------------------------------------------------------------------------------