%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PUZ133+2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.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 : Fri Sep 25 02:32:08 PM UTC 2026
% Result : Theorem 154.08s 22.62s
% Output : Proof 154.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 9
% Syntax : Number of formulae : 117 ( 16 unt; 0 def)
% Number of atoms : 376 ( 124 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 416 ( 157 ~; 206 |; 42 &)
% ( 3 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 3 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 121 ( 0 sgn 57 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [I,J,K,L] :
( plus(I,J) = plus(K,L)
<=> minus(I,K) = minus(L,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1) ).
fof(f8_nnf,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)],[f8]) ).
fof(f8_sk,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(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c20,plain,
( minus(X0,X2) != minus(X3,X1)
| plus(X0,X1) = plus(X2,X3) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p101,plain,
plus(X0,X1) = plus(X1,X0),
inference(equality_resolution,[status(thm)],[c20]) ).
fof(f2,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',queens_q) ).
fof(f2_nnf,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)],[f2]) ).
fof(f2_sk,plain,
( queens_q
| ( ( minus(q(sk0),sk0) = minus(q(sk1),sk1)
| plus(q(sk0),sk0) = plus(q(sk1),sk1)
| q(sk0) = q(sk1) )
& ( ~ le(s(perm(sk1)),perm(sk0))
| le(s(sk0),sk1) )
& ( le(s(perm(sk1)),perm(sk0))
| ~ le(s(sk0),sk1) )
& le(sk1,n)
& le(s(sk0),sk1)
& le(sk0,n)
& le(s(n0),sk0) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f2_nnf]) ).
cnf(c10,plain,
( queens_q
| minus(q(sk0),sk0) = minus(q(sk1),sk1)
| plus(q(sk0),sk0) = plus(q(sk1),sk1)
| q(sk0) = q(sk1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p102,plain,
( queens_q
| minus(q(sk0),sk0) = minus(q(sk1),sk1)
| plus(sk0,q(sk0)) = plus(sk1,q(sk1))
| q(sk0) = q(sk1) ),
inference(demodulation,[status(thm)],[p101,c10]) ).
fof(f9,axiom,
! [I,J,K,L] :
( minus(I,J) = minus(K,L)
<=> minus(I,K) = minus(J,L) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minus1) ).
fof(f9_nnf,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)],[f9]) ).
fof(f9_sk,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(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c21,plain,
( minus(X0,X2) = minus(X1,X3)
| minus(X0,X1) != minus(X2,X3) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p243,plain,
( minus(q(sk0),q(sk1)) = minus(sk0,sk1)
| queens_q
| plus(sk0,q(sk0)) = plus(sk1,q(sk1))
| q(sk0) = q(sk1) ),
inference(resolution,[status(thm)],[p102,c21]) ).
fof(f5,axiom,
! [J,I] : minus(I,J) = minus(perm(J),perm(I)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',permutation_another_one) ).
fof(f5_nnf,plain,
! [J,I] : minus(I,J) = minus(perm(J),perm(I)),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [I,J] : minus(I,J) = minus(perm(J),perm(I)),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c16,plain,
minus(X1,X0) = minus(perm(X0),perm(X1)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p114,plain,
( minus(X0,X2) != minus(X1,X3)
| plus(X0,perm(X1)) = plus(X2,perm(X3)) ),
inference(superposition,[status(thm)],[c16,c20]) ).
cnf(p853,plain,
( plus(perm(sk0),q(sk0)) = plus(perm(sk1),q(sk1))
| queens_q
| plus(sk0,q(sk0)) = plus(sk1,q(sk1))
| q(sk0) = q(sk1) ),
inference(resolution,[status(thm)],[p243,p114]) ).
fof(f3,conjecture,
( ( ! [I] : q(I) = p(perm(I))
& queens_p )
=> queens_q ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',queens_sym) ).
fof(f3_neg,negated_conjecture,
~ ( ( ! [I] : q(I) = p(perm(I))
& queens_p )
=> queens_q ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f3_nnf,plain,
( ~ queens_q
& ! [I] : q(I) = p(perm(I))
& queens_p ),
inference(nnf_transformation,[status(thm)],[f3_neg]) ).
fof(f3_sk,plain,
! [I] :
( ~ queens_q
& q(I) = p(perm(I))
& queens_p ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c12,plain,
q(X0) = p(perm(X0)),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
fof(f6,axiom,
! [X,Y,Z] :
( ( le(Y,Z)
& le(X,Y) )
=> le(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',le_trans) ).
fof(f6_nnf,plain,
! [X,Y,Z] :
( le(X,Z)
| ~ le(Y,Z)
| ~ le(X,Y) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y,Z] :
( le(X,Z)
| ~ le(Y,Z)
| ~ le(X,Y) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c17,plain,
( le(X0,X2)
| ~ le(X1,X2)
| ~ le(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(c4,plain,
( queens_q
| le(s(n0),sk0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p83,plain,
( queens_q
| le(s(n0),X0)
| ~ le(sk0,X0) ),
inference(resolution,[status(thm)],[c17,c4]) ).
fof(f7,axiom,
! [X] : le(X,s(X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_le) ).
fof(f7_nnf,plain,
! [X] : le(X,s(X)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X] : le(X,s(X)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c18,plain,
le(X0,s(X0)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p80,plain,
( le(X0,X1)
| ~ le(s(X0),X1) ),
inference(resolution,[status(thm)],[c17,c18]) ).
cnf(c6,plain,
( queens_q
| le(s(sk0),sk1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p87,plain,
( queens_q
| le(sk0,sk1) ),
inference(resolution,[status(thm)],[p80,c6]) ).
cnf(p191,plain,
( queens_q
| queens_q
| le(s(n0),sk1) ),
inference(resolution,[status(thm)],[p83,p87]) ).
cnf(p267,plain,
( queens_q
| le(s(n0),sk1) ),
inference(factoring,[status(thm)],[p191]) ).
fof(f4,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',permutation_range) ).
fof(f4_nnf,plain,
! [I] :
( ( le(perm(I),n)
& le(s(n0),perm(I)) )
| ~ le(I,n)
| ~ le(s(n0),I) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [I] :
( ( le(perm(I),n)
& le(s(n0),perm(I)) )
| ~ le(I,n)
| ~ le(s(n0),I) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c14,plain,
( le(s(n0),perm(X0))
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p272,plain,
( le(s(n0),perm(sk1))
| ~ le(sk1,n)
| queens_q ),
inference(resolution,[status(thm)],[p267,c14]) ).
cnf(c7,plain,
( queens_q
| le(sk1,n) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p1053,plain,
( queens_q
| le(s(n0),perm(sk1))
| queens_q ),
inference(resolution,[status(thm)],[p272,c7]) ).
cnf(p1054,plain,
( le(s(n0),perm(sk1))
| queens_q ),
inference(factoring,[status(thm)],[p1053]) ).
fof(f0,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',queens_p) ).
fof(f0_nnf,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(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,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(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c1,plain,
( 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(esa)],[f0_sk]) ).
cnf(c11,plain,
queens_p,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p37,plain,
( plus(p(X0),X0) != plus(p(X1),X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(resolution,[status(thm)],[c1,c11]) ).
cnf(p103,plain,
( plus(X0,p(X0)) != plus(X1,p(X1))
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(demodulation,[status(thm)],[p101,p37]) ).
cnf(p1063,plain,
( plus(perm(sk1),p(perm(sk1))) != plus(X0,p(X0))
| ~ le(X0,n)
| ~ le(s(perm(sk1)),X0)
| ~ le(perm(sk1),n)
| queens_q ),
inference(resolution,[status(thm)],[p1054,p103]) ).
cnf(c8,plain,
( queens_q
| le(s(perm(sk1)),perm(sk0))
| ~ le(s(sk0),sk1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p59,plain,
( queens_q
| queens_q
| le(s(perm(sk1)),perm(sk0)) ),
inference(resolution,[status(thm)],[c8,c6]) ).
cnf(p137,plain,
( queens_q
| le(s(perm(sk1)),perm(sk0)) ),
inference(factoring,[status(thm)],[p59]) ).
cnf(p154,plain,
( le(perm(sk1),perm(sk0))
| queens_q ),
inference(resolution,[status(thm)],[p137,p80]) ).
cnf(p155,plain,
( le(perm(sk1),X0)
| ~ le(perm(sk0),X0)
| queens_q ),
inference(resolution,[status(thm)],[p154,c17]) ).
cnf(c15,plain,
( le(perm(X0),n)
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p77,plain,
( queens_q
| le(perm(sk0),n)
| ~ le(sk0,n) ),
inference(resolution,[status(thm)],[c15,c4]) ).
cnf(c5,plain,
( queens_q
| le(sk0,n) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p168,plain,
( queens_q
| queens_q
| le(perm(sk0),n) ),
inference(resolution,[status(thm)],[p77,c5]) ).
cnf(p169,plain,
( queens_q
| le(perm(sk0),n) ),
inference(factoring,[status(thm)],[p168]) ).
cnf(p483,plain,
( queens_q
| le(perm(sk1),n)
| queens_q ),
inference(resolution,[status(thm)],[p155,p169]) ).
cnf(p491,plain,
( le(perm(sk1),n)
| queens_q ),
inference(factoring,[status(thm)],[p483]) ).
cnf(p1169,plain,
( queens_q
| plus(perm(sk1),p(perm(sk1))) != plus(X0,p(X0))
| ~ le(X0,n)
| ~ le(s(perm(sk1)),X0)
| queens_q ),
inference(resolution,[status(thm)],[p1063,p491]) ).
cnf(p1170,plain,
( plus(perm(sk1),p(perm(sk1))) != plus(X0,p(X0))
| ~ le(X0,n)
| ~ le(s(perm(sk1)),X0)
| queens_q ),
inference(factoring,[status(thm)],[p1169]) ).
cnf(p1175,plain,
( queens_q
| plus(perm(sk1),p(perm(sk1))) != plus(perm(sk0),p(perm(sk0)))
| ~ le(perm(sk0),n)
| queens_q ),
inference(resolution,[status(thm)],[p1170,p137]) ).
cnf(p1189,plain,
( plus(perm(sk1),p(perm(sk1))) != plus(perm(sk0),p(perm(sk0)))
| ~ le(perm(sk0),n)
| queens_q ),
inference(factoring,[status(thm)],[p1175]) ).
cnf(p1190,plain,
( queens_q
| plus(perm(sk1),p(perm(sk1))) != plus(perm(sk0),p(perm(sk0)))
| queens_q ),
inference(resolution,[status(thm)],[p1189,p169]) ).
cnf(p1197,plain,
( plus(perm(sk1),p(perm(sk1))) != plus(perm(sk0),p(perm(sk0)))
| queens_q ),
inference(factoring,[status(thm)],[p1190]) ).
cnf(p1198,plain,
( plus(perm(sk1),q(sk1)) != plus(perm(sk0),p(perm(sk0)))
| queens_q ),
inference(superposition,[status(thm)],[c12,p1197]) ).
cnf(p1200,plain,
( plus(perm(sk1),q(sk1)) != plus(perm(sk0),q(sk0))
| queens_q ),
inference(superposition,[status(thm)],[c12,p1198]) ).
cnf(p3196,plain,
( plus(perm(sk0),q(sk0)) != plus(perm(sk0),q(sk0))
| queens_q
| queens_q
| plus(sk0,q(sk0)) = plus(sk1,q(sk1))
| q(sk0) = q(sk1) ),
inference(superposition,[status(thm)],[p853,p1200]) ).
cnf(p3211,plain,
( plus(perm(sk0),q(sk0)) != plus(perm(sk0),q(sk0))
| queens_q
| plus(sk0,q(sk0)) = plus(sk1,q(sk1))
| q(sk0) = q(sk1) ),
inference(factoring,[status(thm)],[p3196]) ).
cnf(p3212,plain,
( queens_q
| plus(sk0,q(sk0)) = plus(sk1,q(sk1))
| q(sk0) = q(sk1) ),
inference(equality_resolution,[status(thm)],[p3211]) ).
cnf(c19,plain,
( minus(X0,X2) = minus(X3,X1)
| plus(X0,X1) != plus(X2,X3) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p3213,plain,
( minus(sk0,sk1) = minus(q(sk1),q(sk0))
| queens_q
| q(sk0) = q(sk1) ),
inference(resolution,[status(thm)],[p3212,c19]) ).
cnf(p115,plain,
minus(X0,perm(X1)) = minus(X1,perm(X0)),
inference(resolution,[status(thm)],[c21,c16]) ).
cnf(p303,plain,
minus(X0,perm(perm(X1))) = minus(X0,X1),
inference(superposition,[status(thm)],[c16,p115]) ).
cnf(p3252,plain,
( minus(q(sk1),q(sk0)) = minus(sk0,sk1)
| queens_q
| q(sk0) = q(sk1) ),
inference(superposition,[status(thm)],[p3213,p303]) ).
cnf(p117,plain,
( minus(X0,perm(X3)) = minus(X1,perm(X2))
| minus(X0,X1) != minus(X2,X3) ),
inference(superposition,[status(thm)],[c16,c21]) ).
cnf(p3511,plain,
( minus(sk1,perm(q(sk1))) = minus(sk0,perm(q(sk0)))
| queens_q
| q(sk0) = q(sk1) ),
inference(resolution,[status(thm)],[p3252,p117]) ).
cnf(c2,plain,
( 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(esa)],[f0_sk]) ).
cnf(p40,plain,
( minus(p(X0),X0) != minus(p(X1),X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(resolution,[status(thm)],[c2,c11]) ).
cnf(p1057,plain,
( minus(sk1,perm(p(perm(sk1)))) != minus(p(X0),X0)
| ~ le(X0,n)
| ~ le(s(perm(sk1)),X0)
| ~ le(perm(sk1),n)
| queens_q ),
inference(resolution,[status(thm)],[p1054,p40]) ).
cnf(p1131,plain,
( queens_q
| minus(sk1,perm(p(perm(sk1)))) != minus(p(X0),X0)
| ~ le(X0,n)
| ~ le(s(perm(sk1)),X0)
| queens_q ),
inference(resolution,[status(thm)],[p1057,p491]) ).
cnf(p1132,plain,
( minus(sk1,perm(p(perm(sk1)))) != minus(p(X0),X0)
| ~ le(X0,n)
| ~ le(s(perm(sk1)),X0)
| queens_q ),
inference(factoring,[status(thm)],[p1131]) ).
cnf(p1137,plain,
( queens_q
| minus(sk1,perm(p(perm(sk1)))) != minus(sk0,perm(p(perm(sk0))))
| ~ le(perm(sk0),n)
| queens_q ),
inference(resolution,[status(thm)],[p1132,p137]) ).
cnf(p1149,plain,
( minus(sk1,perm(p(perm(sk1)))) != minus(sk0,perm(p(perm(sk0))))
| ~ le(perm(sk0),n)
| queens_q ),
inference(factoring,[status(thm)],[p1137]) ).
cnf(p1150,plain,
( queens_q
| minus(sk1,perm(p(perm(sk1)))) != minus(sk0,perm(p(perm(sk0))))
| queens_q ),
inference(resolution,[status(thm)],[p1149,p169]) ).
cnf(p1151,plain,
( minus(sk1,perm(p(perm(sk1)))) != minus(sk0,perm(p(perm(sk0))))
| queens_q ),
inference(factoring,[status(thm)],[p1150]) ).
cnf(p1155,plain,
( minus(sk1,perm(q(sk1))) != minus(sk0,perm(p(perm(sk0))))
| queens_q ),
inference(superposition,[status(thm)],[c12,p1151]) ).
cnf(p1157,plain,
( minus(sk1,perm(q(sk1))) != minus(sk0,perm(q(sk0)))
| queens_q ),
inference(superposition,[status(thm)],[c12,p1155]) ).
cnf(p3730,plain,
( queens_q
| queens_q
| q(sk0) = q(sk1) ),
inference(resolution,[status(thm)],[p3511,p1157]) ).
cnf(p3731,plain,
( queens_q
| q(sk0) = q(sk1) ),
inference(factoring,[status(thm)],[p3730]) ).
cnf(p3732,plain,
( q(sk0) = p(perm(sk1))
| queens_q ),
inference(superposition,[status(thm)],[p3731,c12]) ).
cnf(p3739,plain,
( q(sk1) = q(sk0)
| queens_q ),
inference(superposition,[status(thm)],[p3732,c12]) ).
cnf(c0,plain,
( p(X0) != p(X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0)
| ~ queens_p ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p27,plain,
( p(X0) != p(X1)
| ~ le(X1,n)
| ~ le(s(X0),X1)
| ~ le(X0,n)
| ~ le(s(n0),X0) ),
inference(resolution,[status(thm)],[c0,c11]) ).
cnf(p1055,plain,
( p(perm(sk1)) != p(X0)
| ~ le(X0,n)
| ~ le(s(perm(sk1)),X0)
| ~ le(perm(sk1),n)
| queens_q ),
inference(resolution,[status(thm)],[p1054,p27]) ).
cnf(p1072,plain,
( queens_q
| p(perm(sk1)) != p(X0)
| ~ le(X0,n)
| ~ le(s(perm(sk1)),X0)
| queens_q ),
inference(resolution,[status(thm)],[p1055,p491]) ).
cnf(p1073,plain,
( p(perm(sk1)) != p(X0)
| ~ le(X0,n)
| ~ le(s(perm(sk1)),X0)
| queens_q ),
inference(factoring,[status(thm)],[p1072]) ).
cnf(p1078,plain,
( queens_q
| p(perm(sk1)) != p(perm(sk0))
| ~ le(perm(sk0),n)
| queens_q ),
inference(resolution,[status(thm)],[p1073,p137]) ).
cnf(p1090,plain,
( p(perm(sk1)) != p(perm(sk0))
| ~ le(perm(sk0),n)
| queens_q ),
inference(factoring,[status(thm)],[p1078]) ).
cnf(p1091,plain,
( queens_q
| p(perm(sk1)) != p(perm(sk0))
| queens_q ),
inference(resolution,[status(thm)],[p1090,p169]) ).
cnf(p1100,plain,
( p(perm(sk1)) != p(perm(sk0))
| queens_q ),
inference(factoring,[status(thm)],[p1091]) ).
cnf(p1101,plain,
( q(sk1) != p(perm(sk0))
| queens_q ),
inference(superposition,[status(thm)],[c12,p1100]) ).
cnf(p1103,plain,
( q(sk1) != q(sk0)
| queens_q ),
inference(superposition,[status(thm)],[c12,p1101]) ).
cnf(p3740,plain,
( queens_q
| queens_q ),
inference(resolution,[status(thm)],[p3739,p1103]) ).
cnf(p3741,plain,
queens_q,
inference(factoring,[status(thm)],[p3740]) ).
cnf(c13,plain,
~ queens_q,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p3742,plain,
$false,
inference(resolution,[status(thm)],[p3741,c13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ133+2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n008.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 07:00:25 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 154.08/22.62 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 154.08/22.62 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------