%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PUZ133+2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 : Sun Sep 27 08:23:22 AM UTC 2026
% Result : Theorem 0.79s 0.56s
% Output : CNFRefutation 0.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 9
% Syntax : Number of formulae : 105 ( 37 unt; 0 def)
% Number of atoms : 292 ( 117 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 328 ( 141 ~; 143 |; 33 &)
% ( 3 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 6 ( 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 : 97 ( 0 sgn 21 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(queens_p,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('theBenchmark.p',queens_p) ).
fof(queens_q,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('theBenchmark.p',queens_q) ).
fof(permutation_range,axiom,
! [I] :
( ( le(I,n)
& le(s(n0),I) )
=> ( le(perm(I),n)
& le(s(n0),perm(I)) ) ),
file('theBenchmark.p',permutation_range) ).
fof(permutation_another_one,axiom,
! [J,I] : minus(I,J) = minus(perm(J),perm(I)),
file('theBenchmark.p',permutation_another_one) ).
fof(le_trans,axiom,
! [X,Y,Z] :
( ( le(Y,Z)
& le(X,Y) )
=> le(X,Z) ),
file('theBenchmark.p',le_trans) ).
fof(succ_le,axiom,
! [X] : le(X,s(X)),
file('theBenchmark.p',succ_le) ).
fof(plus1,axiom,
! [I,J,K,L] :
( plus(I,J) = plus(K,L)
<=> minus(I,K) = minus(L,J) ),
file('theBenchmark.p',plus1) ).
fof(minus1,axiom,
! [I,J,K,L] :
( minus(I,J) = minus(K,L)
<=> minus(I,K) = minus(J,L) ),
file('theBenchmark.p',minus1) ).
fof(queens_sym,conjecture,
( ( ! [I] : q(I) = p(perm(I))
& queens_p )
=> queens_q ),
file('theBenchmark.p',queens_sym) ).
fof(queens_sym_neg,negated_conjecture,
~ ( ( ! [I] : q(I) = p(perm(I))
& queens_p )
=> queens_q ),
inference(assume_negation,[status(cth)],[queens_sym]) ).
cnf(c_11,plain,
( p(B) != p(A)
| ~ le(B,n)
| ~ le(s(A),B)
| ~ le(A,n)
| ~ le(s(n0),A)
| ~ queens_p ),
inference(clausify,[status(thm)],[queens_p]) ).
cnf(c_12,plain,
( plus(p(B),B) != plus(p(A),A)
| ~ le(B,n)
| ~ le(s(A),B)
| ~ le(A,n)
| ~ le(s(n0),A)
| ~ queens_p ),
inference(clausify,[status(thm)],[queens_p]) ).
cnf(c_13,plain,
( minus(p(B),B) != minus(p(A),A)
| ~ le(B,n)
| ~ le(s(A),B)
| ~ le(A,n)
| ~ le(s(n0),A)
| ~ queens_p ),
inference(clausify,[status(thm)],[queens_p]) ).
fof(nnf_3,plain,
( queens_q
| ? [I,J] :
( ( minus(q(J),J) = minus(q(I),I)
| plus(q(J),J) = plus(q(I),I)
| q(J) = q(I) )
& ( ~ 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(fof_nnf,[status(thm)],[queens_q]) ).
fof(sk_queens_q_sk,plain,
( queens_q
| ( ( minus(q(sK1),sK1) = minus(q(sK0),sK0)
| plus(q(sK1),sK1) = plus(q(sK0),sK0)
| q(sK1) = q(sK0) )
& ( ~ 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(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(I,sK0),skolemize(J,sK1)],[nnf_3]) ).
fof(sk_queens_q,plain,
( ( queens_q
| minus(q(sK1),sK1) = minus(q(sK0),sK0)
| plus(q(sK1),sK1) = plus(q(sK0),sK0)
| q(sK1) = q(sK0) )
& ( queens_q
| le(s(perm(sK1)),perm(sK0))
| ~ le(s(sK0),sK1) )
& ( queens_q
| le(sK1,n) )
& ( queens_q
| le(s(sK0),sK1) )
& ( queens_q
| le(sK0,n) )
& ( queens_q
| le(s(n0),sK0) ) ),
inference(cnf_transformation,[status(thm)],[sk_queens_q_sk]) ).
cnf(c_16,plain,
( queens_q
| le(s(n0),sK0) ),
inference(split_conjunct,[status(thm)],[sk_queens_q]) ).
cnf(c_17,plain,
( queens_q
| le(sK0,n) ),
inference(split_conjunct,[status(thm)],[sk_queens_q]) ).
cnf(c_18,plain,
( queens_q
| le(s(sK0),sK1) ),
inference(split_conjunct,[status(thm)],[sk_queens_q]) ).
cnf(c_19,plain,
( queens_q
| le(sK1,n) ),
inference(split_conjunct,[status(thm)],[sk_queens_q]) ).
cnf(c_20,plain,
( queens_q
| le(s(perm(sK1)),perm(sK0))
| ~ le(s(sK0),sK1) ),
inference(split_conjunct,[status(thm)],[sk_queens_q]) ).
cnf(c_21,plain,
( queens_q
| minus(q(sK1),sK1) = minus(q(sK0),sK0)
| plus(q(sK1),sK1) = plus(q(sK0),sK0)
| q(sK1) = q(sK0) ),
inference(split_conjunct,[status(thm)],[sk_queens_q]) ).
cnf(c_22,plain,
( le(s(n0),perm(A))
| ~ le(A,n)
| ~ le(s(n0),A) ),
inference(clausify,[status(thm)],[permutation_range]) ).
cnf(c_23,plain,
( le(perm(A),n)
| ~ le(A,n)
| ~ le(s(n0),A) ),
inference(clausify,[status(thm)],[permutation_range]) ).
cnf(c_24,plain,
minus(perm(A),perm(B)) = minus(B,A),
inference(clausify,[status(thm)],[permutation_another_one]) ).
cnf(c_25,plain,
( le(A,C)
| ~ le(B,C)
| ~ le(A,B) ),
inference(clausify,[status(thm)],[le_trans]) ).
cnf(c_26,plain,
le(A,s(A)),
inference(clausify,[status(thm)],[succ_le]) ).
cnf(c_27,plain,
( minus(B,D) = minus(C,A)
| plus(A,B) != plus(C,D) ),
inference(clausify,[status(thm)],[plus1]) ).
cnf(c_28,plain,
( minus(B,D) != minus(C,A)
| plus(A,B) = plus(C,D) ),
inference(clausify,[status(thm)],[plus1]) ).
cnf(c_29,plain,
( minus(D,B) = minus(C,A)
| minus(A,B) != minus(C,D) ),
inference(clausify,[status(thm)],[minus1]) ).
cnf(c_30,negated_conjecture,
queens_p,
inference(clausify,[status(thm)],[queens_sym_neg]) ).
cnf(c_31,negated_conjecture,
q(A) = p(perm(A)),
inference(clausify,[status(thm)],[queens_sym_neg]) ).
cnf(c_32,negated_conjecture,
~ queens_q,
inference(clausify,[status(thm)],[queens_sym_neg]) ).
cnf(c_38,negated_conjecture,
( minus(p(B),B) != minus(p(A),A)
| ~ le(B,n)
| ~ le(s(A),B)
| ~ le(A,n)
| ~ le(s(n0),A) ),
inference(resolve,[status(thm)],[c_30,c_13]) ).
cnf(c_39,negated_conjecture,
( plus(p(B),B) != plus(p(A),A)
| ~ le(B,n)
| ~ le(s(A),B)
| ~ le(A,n)
| ~ le(s(n0),A) ),
inference(resolve,[status(thm)],[c_30,c_12]) ).
cnf(c_40,negated_conjecture,
( p(B) != p(A)
| ~ le(B,n)
| ~ le(s(A),B)
| ~ le(A,n)
| ~ le(s(n0),A) ),
inference(resolve,[status(thm)],[c_30,c_11]) ).
cnf(c_654,plain,
( queens_q
| minus(q(sK1),sK1) = minus(q(sK0),sK0)
| plus(q(sK1),sK1) = plus(q(sK0),sK0)
| p(perm(sK1)) = q(sK0) ),
inference(paramod,[status(thm)],[c_31,c_21]) ).
cnf(c_655,plain,
( queens_q
| minus(q(sK1),sK1) = minus(q(sK0),sK0)
| plus(q(sK1),sK1) = plus(q(sK0),sK0)
| p(perm(sK1)) = p(perm(sK0)) ),
inference(paramod,[status(thm)],[c_31,c_654]) ).
cnf(c_656,plain,
( queens_q
| minus(q(sK1),sK1) = minus(q(sK0),sK0)
| plus(p(perm(sK1)),sK1) = plus(q(sK0),sK0)
| p(perm(sK1)) = p(perm(sK0)) ),
inference(paramod,[status(thm)],[c_31,c_655]) ).
cnf(c_657,plain,
( queens_q
| minus(q(sK1),sK1) = minus(q(sK0),sK0)
| plus(p(perm(sK1)),sK1) = plus(p(perm(sK0)),sK0)
| p(perm(sK1)) = p(perm(sK0)) ),
inference(paramod,[status(thm)],[c_31,c_656]) ).
cnf(c_658,plain,
( queens_q
| minus(p(perm(sK1)),sK1) = minus(q(sK0),sK0)
| plus(p(perm(sK1)),sK1) = plus(p(perm(sK0)),sK0)
| p(perm(sK1)) = p(perm(sK0)) ),
inference(paramod,[status(thm)],[c_31,c_657]) ).
cnf(c_659,plain,
( queens_q
| minus(p(perm(sK1)),sK1) = minus(p(perm(sK0)),sK0)
| plus(p(perm(sK1)),sK1) = plus(p(perm(sK0)),sK0)
| p(perm(sK1)) = p(perm(sK0)) ),
inference(paramod,[status(thm)],[c_31,c_658]) ).
cnf(c_41,negated_conjecture,
( minus(p(perm(sK1)),sK1) = minus(p(perm(sK0)),sK0)
| plus(p(perm(sK1)),sK1) = plus(p(perm(sK0)),sK0)
| p(perm(sK1)) = p(perm(sK0)) ),
inference(resolve,[status(thm)],[c_32,c_659]) ).
cnf(c_42,negated_conjecture,
( le(s(perm(sK1)),perm(sK0))
| ~ le(s(sK0),sK1) ),
inference(resolve,[status(thm)],[c_32,c_20]) ).
cnf(c_43,negated_conjecture,
le(sK1,n),
inference(resolve,[status(thm)],[c_32,c_19]) ).
cnf(c_44,negated_conjecture,
le(s(sK0),sK1),
inference(resolve,[status(thm)],[c_32,c_18]) ).
cnf(c_45,negated_conjecture,
le(sK0,n),
inference(resolve,[status(thm)],[c_32,c_17]) ).
cnf(c_46,negated_conjecture,
le(s(n0),sK0),
inference(resolve,[status(thm)],[c_32,c_16]) ).
cnf(c_47,negated_conjecture,
le(s(perm(sK1)),perm(sK0)),
inference(resolve,[status(thm)],[c_44,c_42]) ).
cnf(c_57,plain,
plus(A,B) = plus(B,A),
inference(xxres,[status(thm)],[c_28]) ).
cnf(c_59,plain,
( minus(B,D) != minus(A,C)
| plus(perm(A),B) = plus(perm(C),D) ),
inference(paramod,[status(thm)],[c_24,c_28]) ).
cnf(c_660,negated_conjecture,
( minus(p(perm(sK1)),sK1) = minus(p(perm(sK0)),sK0)
| plus(sK1,p(perm(sK1))) = plus(p(perm(sK0)),sK0)
| p(perm(sK1)) = p(perm(sK0)) ),
inference(paramod,[status(thm)],[c_57,c_41]) ).
cnf(c_60,negated_conjecture,
( minus(p(perm(sK1)),sK1) = minus(p(perm(sK0)),sK0)
| plus(sK1,p(perm(sK1))) = plus(sK0,p(perm(sK0)))
| p(perm(sK1)) = p(perm(sK0)) ),
inference(paramod,[status(thm)],[c_57,c_660]) ).
cnf(c_661,negated_conjecture,
( plus(B,p(B)) != plus(p(A),A)
| ~ le(B,n)
| ~ le(s(A),B)
| ~ le(A,n)
| ~ le(s(n0),A) ),
inference(paramod,[status(thm)],[c_57,c_39]) ).
cnf(c_61,negated_conjecture,
( plus(B,p(B)) != plus(A,p(A))
| ~ le(B,n)
| ~ le(s(A),B)
| ~ le(A,n)
| ~ le(s(n0),A) ),
inference(paramod,[status(thm)],[c_57,c_661]) ).
cnf(c_63,plain,
minus(A,perm(B)) = minus(B,perm(A)),
inference(resolve,[status(thm)],[c_29,c_24]) ).
cnf(c_65,plain,
( minus(D,perm(A)) = minus(C,perm(B))
| minus(A,B) != minus(C,D) ),
inference(paramod,[status(thm)],[c_24,c_29]) ).
cnf(c_662,plain,
( le(A,B)
| ~ le(s(A),B) ),
inference(resolve,[status(thm)],[c_25,c_26]) ).
cnf(c_79,plain,
le(sK0,sK1),
inference(resolve,[status(thm)],[c_662,c_44]) ).
cnf(c_663,plain,
( le(perm(sK0),n)
| ~ le(sK0,n) ),
inference(resolve,[status(thm)],[c_46,c_23]) ).
cnf(c_90,plain,
le(perm(sK0),n),
inference(resolve,[status(thm)],[c_45,c_663]) ).
cnf(c_664,plain,
( p(perm(sK0)) != p(perm(sK1))
| ~ le(perm(sK0),n)
| ~ le(perm(sK1),n)
| ~ le(s(n0),perm(sK1)) ),
inference(resolve,[status(thm)],[c_47,c_40]) ).
cnf(c_665,plain,
( p(perm(sK1)) != p(perm(sK0))
| ~ le(perm(sK0),n)
| ~ le(perm(sK1),n)
| ~ le(s(n0),perm(sK1)) ),
inference(copy,[status(thm)],[c_664]) ).
cnf(c_99,plain,
( p(perm(sK1)) != p(perm(sK0))
| ~ le(perm(sK1),n)
| ~ le(s(n0),perm(sK1)) ),
inference(resolve,[status(thm)],[c_90,c_665]) ).
cnf(c_666,plain,
( minus(p(perm(sK0)),perm(sK0)) != minus(p(perm(sK1)),perm(sK1))
| ~ le(perm(sK0),n)
| ~ le(perm(sK1),n)
| ~ le(s(n0),perm(sK1)) ),
inference(resolve,[status(thm)],[c_47,c_38]) ).
cnf(c_667,plain,
( minus(sK0,perm(p(perm(sK0)))) != minus(p(perm(sK1)),perm(sK1))
| ~ le(perm(sK0),n)
| ~ le(perm(sK1),n)
| ~ le(s(n0),perm(sK1)) ),
inference(paramod,[status(thm)],[c_63,c_666]) ).
cnf(c_668,plain,
( minus(sK0,perm(p(perm(sK0)))) != minus(sK1,perm(p(perm(sK1))))
| ~ le(perm(sK0),n)
| ~ le(perm(sK1),n)
| ~ le(s(n0),perm(sK1)) ),
inference(paramod,[status(thm)],[c_63,c_667]) ).
cnf(c_669,plain,
( minus(sK1,perm(p(perm(sK1)))) != minus(sK0,perm(p(perm(sK0))))
| ~ le(perm(sK0),n)
| ~ le(perm(sK1),n)
| ~ le(s(n0),perm(sK1)) ),
inference(copy,[status(thm)],[c_668]) ).
cnf(c_100,plain,
( minus(sK1,perm(p(perm(sK1)))) != minus(sK0,perm(p(perm(sK0))))
| ~ le(perm(sK1),n)
| ~ le(s(n0),perm(sK1)) ),
inference(resolve,[status(thm)],[c_90,c_669]) ).
cnf(c_670,plain,
( le(s(n0),A)
| ~ le(sK0,A) ),
inference(resolve,[status(thm)],[c_25,c_46]) ).
cnf(c_118,plain,
le(s(n0),sK1),
inference(resolve,[status(thm)],[c_670,c_79]) ).
cnf(c_671,plain,
( le(perm(sK1),n)
| ~ le(sK1,n) ),
inference(resolve,[status(thm)],[c_118,c_23]) ).
cnf(c_183,plain,
le(perm(sK1),n),
inference(resolve,[status(thm)],[c_43,c_671]) ).
cnf(c_672,plain,
( le(s(n0),perm(sK1))
| ~ le(sK1,n) ),
inference(resolve,[status(thm)],[c_118,c_22]) ).
cnf(c_184,plain,
le(s(n0),perm(sK1)),
inference(resolve,[status(thm)],[c_43,c_672]) ).
cnf(c_673,plain,
( minus(sK1,perm(p(perm(sK1)))) != minus(sK0,perm(p(perm(sK0))))
| ~ le(perm(sK1),n) ),
inference(resolve,[status(thm)],[c_184,c_100]) ).
cnf(c_186,plain,
minus(sK1,perm(p(perm(sK1)))) != minus(sK0,perm(p(perm(sK0)))),
inference(resolve,[status(thm)],[c_183,c_673]) ).
cnf(c_674,plain,
( p(perm(sK1)) != p(perm(sK0))
| ~ le(perm(sK1),n) ),
inference(resolve,[status(thm)],[c_184,c_99]) ).
cnf(c_187,plain,
p(perm(sK1)) != p(perm(sK0)),
inference(resolve,[status(thm)],[c_183,c_674]) ).
cnf(c_188,negated_conjecture,
( minus(p(perm(sK1)),sK1) = minus(p(perm(sK0)),sK0)
| plus(sK1,p(perm(sK1))) = plus(sK0,p(perm(sK0))) ),
inference(resolve,[status(thm)],[c_187,c_60]) ).
cnf(c_354,plain,
( minus(A,D) = minus(C,B)
| plus(A,B) != plus(C,D) ),
inference(paramod,[status(thm)],[c_57,c_27]) ).
cnf(c_675,plain,
( plus(perm(sK0),p(perm(sK0))) != plus(perm(sK1),p(perm(sK1)))
| ~ le(perm(sK0),n)
| ~ le(perm(sK1),n)
| ~ le(s(n0),perm(sK1)) ),
inference(resolve,[status(thm)],[c_61,c_47]) ).
cnf(c_676,plain,
( plus(perm(sK1),p(perm(sK1))) != plus(perm(sK0),p(perm(sK0)))
| ~ le(perm(sK0),n)
| ~ le(perm(sK1),n)
| ~ le(s(n0),perm(sK1)) ),
inference(copy,[status(thm)],[c_675]) ).
cnf(c_677,plain,
( plus(perm(sK1),p(perm(sK1))) != plus(perm(sK0),p(perm(sK0)))
| ~ le(perm(sK0),n)
| ~ le(perm(sK1),n) ),
inference(resolve,[status(thm)],[c_184,c_676]) ).
cnf(c_678,plain,
( plus(perm(sK1),p(perm(sK1))) != plus(perm(sK0),p(perm(sK0)))
| ~ le(perm(sK0),n) ),
inference(resolve,[status(thm)],[c_183,c_677]) ).
cnf(c_384,plain,
plus(perm(sK1),p(perm(sK1))) != plus(perm(sK0),p(perm(sK0))),
inference(resolve,[status(thm)],[c_90,c_678]) ).
cnf(c_393,plain,
minus(A,perm(perm(B))) = minus(A,B),
inference(paramod,[status(thm)],[c_63,c_24]) ).
cnf(c_679,plain,
( minus(perm(C),perm(A)) = minus(perm(D),perm(B))
| minus(A,B) != minus(C,D) ),
inference(paramod,[status(thm)],[c_24,c_65]) ).
cnf(c_680,plain,
( minus(A,C) = minus(perm(D),perm(B))
| minus(A,B) != minus(C,D) ),
inference(paramod,[status(thm)],[c_24,c_679]) ).
cnf(c_419,plain,
( minus(A,C) = minus(B,D)
| minus(A,B) != minus(C,D) ),
inference(paramod,[status(thm)],[c_24,c_680]) ).
cnf(c_559,plain,
minus(p(perm(sK1)),p(perm(sK0))) != minus(sK1,sK0),
inference(resolve,[status(thm)],[c_59,c_384]) ).
cnf(c_681,plain,
minus(sK1,sK0) != minus(p(perm(sK1)),p(perm(sK0))),
inference(copy,[status(thm)],[c_559]) ).
cnf(c_682,plain,
minus(p(perm(sK0)),sK0) != minus(p(perm(sK1)),sK1),
inference(resolve,[status(thm)],[c_29,c_681]) ).
cnf(c_586,plain,
minus(p(perm(sK1)),sK1) != minus(p(perm(sK0)),sK0),
inference(copy,[status(thm)],[c_682]) ).
cnf(c_587,negated_conjecture,
plus(sK1,p(perm(sK1))) = plus(sK0,p(perm(sK0))),
inference(resolve,[status(thm)],[c_586,c_188]) ).
cnf(c_606,plain,
( minus(A,C) = minus(D,B)
| plus(A,B) != plus(C,D) ),
inference(paramod,[status(thm)],[c_57,c_354]) ).
cnf(c_683,plain,
minus(sK1,sK0) != minus(perm(p(perm(sK1))),perm(p(perm(sK0)))),
inference(resolve,[status(thm)],[c_419,c_186]) ).
cnf(c_684,plain,
minus(sK1,sK0) != minus(p(perm(sK0)),perm(perm(p(perm(sK1))))),
inference(paramod,[status(thm)],[c_63,c_683]) ).
cnf(c_685,plain,
minus(sK1,sK0) != minus(p(perm(sK0)),p(perm(sK1))),
inference(paramod,[status(thm)],[c_393,c_684]) ).
cnf(c_651,plain,
minus(p(perm(sK0)),p(perm(sK1))) != minus(sK1,sK0),
inference(copy,[status(thm)],[c_685]) ).
cnf(c_686,plain,
plus(p(perm(sK0)),sK0) != plus(p(perm(sK1)),sK1),
inference(resolve,[status(thm)],[c_606,c_651]) ).
cnf(c_687,plain,
plus(sK0,p(perm(sK0))) != plus(p(perm(sK1)),sK1),
inference(paramod,[status(thm)],[c_57,c_686]) ).
cnf(c_688,plain,
plus(sK0,p(perm(sK0))) != plus(sK1,p(perm(sK1))),
inference(paramod,[status(thm)],[c_57,c_687]) ).
cnf(c_689,plain,
plus(sK0,p(perm(sK0))) != plus(sK0,p(perm(sK0))),
inference(paramod,[status(thm)],[c_587,c_688]) ).
cnf(c_653,plain,
$false,
inference(copy,[status(thm)],[c_689]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ133+2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n014.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sat Sep 26 05:18:33 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.38 % Process 2228333 was started by sandbox2 on n014,
% 0.12/0.38 % Sat Sep 26 05:18:33 2026
% 0.12/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.38
% 0.12/0.38 % From the command line: assign(max_seconds, 300).
% 0.79/0.56
% 0.79/0.56 % SZS status Theorem for theBenchmark
% 0.79/0.56
% 0.79/0.56 % Proof 1 at 0.13 (+ 0.04) seconds.
% 0.79/0.56 % Length of proof is 65.
% 0.79/0.56 % Level of proof is 10.
% 0.79/0.56 % Maximum clause weight is 49.000.
% 0.79/0.56 % Given clauses 311.
% 0.79/0.56
% 0.79/0.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------