%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PUZ133+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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.13s 0.99s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 10
% Syntax : Number of formulae : 105 ( 33 unt; 0 def)
% Number of atoms : 296 ( 115 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 323 ( 132 ~; 147 |; 33 &)
% ( 3 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 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 : 102 ( 0 sgn 22 !; 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(permutation,axiom,
! [I] : perm(I) = minus(s(n),I),
file('theBenchmark.p',permutation) ).
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]) ).
cnf(c_14,plain,
perm(A) = minus(s(n),A),
inference(clausify,[status(thm)],[permutation]) ).
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_15,plain,
( queens_q
| le(s(n0),sK0) ),
inference(split_conjunct,[status(thm)],[sk_queens_q]) ).
cnf(c_16,plain,
( queens_q
| le(sK0,n) ),
inference(split_conjunct,[status(thm)],[sk_queens_q]) ).
cnf(c_17,plain,
( queens_q
| le(s(sK0),sK1) ),
inference(split_conjunct,[status(thm)],[sk_queens_q]) ).
cnf(c_18,plain,
( queens_q
| le(sK1,n) ),
inference(split_conjunct,[status(thm)],[sk_queens_q]) ).
cnf(c_19,plain,
( queens_q
| le(s(perm(sK1)),perm(sK0))
| ~ le(s(sK0),sK1) ),
inference(split_conjunct,[status(thm)],[sk_queens_q]) ).
cnf(c_753,plain,
( queens_q
| le(s(minus(s(n),sK1)),perm(sK0))
| ~ le(s(sK0),sK1) ),
inference(paramod,[status(thm)],[c_14,c_19]) ).
cnf(c_20,plain,
( queens_q
| le(s(minus(s(n),sK1)),minus(s(n),sK0))
| ~ le(s(sK0),sK1) ),
inference(paramod,[status(thm)],[c_14,c_753]) ).
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(s(n0),minus(s(n),A))
| ~ le(A,n)
| ~ le(s(n0),A) ),
inference(paramod,[status(thm)],[c_14,c_22]) ).
cnf(c_24,plain,
( le(perm(A),n)
| ~ le(A,n)
| ~ le(s(n0),A) ),
inference(clausify,[status(thm)],[permutation_range]) ).
cnf(c_25,plain,
( le(minus(s(n),A),n)
| ~ le(A,n)
| ~ le(s(n0),A) ),
inference(paramod,[status(thm)],[c_14,c_24]) ).
cnf(c_26,plain,
minus(perm(A),perm(B)) = minus(B,A),
inference(clausify,[status(thm)],[permutation_another_one]) ).
cnf(c_754,plain,
minus(minus(s(n),A),perm(B)) = minus(B,A),
inference(paramod,[status(thm)],[c_14,c_26]) ).
cnf(c_27,plain,
minus(minus(s(n),A),minus(s(n),B)) = minus(B,A),
inference(paramod,[status(thm)],[c_14,c_754]) ).
cnf(c_28,plain,
( le(A,C)
| ~ le(B,C)
| ~ le(A,B) ),
inference(clausify,[status(thm)],[le_trans]) ).
cnf(c_29,plain,
le(A,s(A)),
inference(clausify,[status(thm)],[succ_le]) ).
cnf(c_30,plain,
( minus(B,D) = minus(C,A)
| plus(A,B) != plus(C,D) ),
inference(clausify,[status(thm)],[plus1]) ).
cnf(c_31,plain,
( minus(B,D) != minus(C,A)
| plus(A,B) = plus(C,D) ),
inference(clausify,[status(thm)],[plus1]) ).
cnf(c_32,plain,
( minus(D,B) = minus(C,A)
| minus(A,B) != minus(C,D) ),
inference(clausify,[status(thm)],[minus1]) ).
cnf(c_33,negated_conjecture,
queens_p,
inference(clausify,[status(thm)],[queens_sym_neg]) ).
cnf(c_34,negated_conjecture,
q(A) = p(perm(A)),
inference(clausify,[status(thm)],[queens_sym_neg]) ).
cnf(c_35,negated_conjecture,
q(A) = p(minus(s(n),A)),
inference(paramod,[status(thm)],[c_14,c_34]) ).
cnf(c_36,negated_conjecture,
~ queens_q,
inference(clausify,[status(thm)],[queens_sym_neg]) ).
cnf(c_42,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_33,c_13]) ).
cnf(c_43,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_33,c_12]) ).
cnf(c_44,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_33,c_11]) ).
cnf(c_755,plain,
( queens_q
| minus(q(sK1),sK1) = minus(q(sK0),sK0)
| plus(q(sK1),sK1) = plus(q(sK0),sK0)
| p(minus(s(n),sK1)) = q(sK0) ),
inference(paramod,[status(thm)],[c_35,c_21]) ).
cnf(c_756,plain,
( queens_q
| minus(q(sK1),sK1) = minus(q(sK0),sK0)
| plus(q(sK1),sK1) = plus(q(sK0),sK0)
| p(minus(s(n),sK1)) = p(minus(s(n),sK0)) ),
inference(paramod,[status(thm)],[c_35,c_755]) ).
cnf(c_757,plain,
( queens_q
| minus(q(sK1),sK1) = minus(q(sK0),sK0)
| plus(p(minus(s(n),sK1)),sK1) = plus(q(sK0),sK0)
| p(minus(s(n),sK1)) = p(minus(s(n),sK0)) ),
inference(paramod,[status(thm)],[c_35,c_756]) ).
cnf(c_758,plain,
( queens_q
| minus(q(sK1),sK1) = minus(q(sK0),sK0)
| plus(p(minus(s(n),sK1)),sK1) = plus(p(minus(s(n),sK0)),sK0)
| p(minus(s(n),sK1)) = p(minus(s(n),sK0)) ),
inference(paramod,[status(thm)],[c_35,c_757]) ).
cnf(c_759,plain,
( queens_q
| minus(p(minus(s(n),sK1)),sK1) = minus(q(sK0),sK0)
| plus(p(minus(s(n),sK1)),sK1) = plus(p(minus(s(n),sK0)),sK0)
| p(minus(s(n),sK1)) = p(minus(s(n),sK0)) ),
inference(paramod,[status(thm)],[c_35,c_758]) ).
cnf(c_760,plain,
( queens_q
| minus(p(minus(s(n),sK1)),sK1) = minus(p(minus(s(n),sK0)),sK0)
| plus(p(minus(s(n),sK1)),sK1) = plus(p(minus(s(n),sK0)),sK0)
| p(minus(s(n),sK1)) = p(minus(s(n),sK0)) ),
inference(paramod,[status(thm)],[c_35,c_759]) ).
cnf(c_45,negated_conjecture,
( minus(p(minus(s(n),sK1)),sK1) = minus(p(minus(s(n),sK0)),sK0)
| plus(p(minus(s(n),sK1)),sK1) = plus(p(minus(s(n),sK0)),sK0)
| p(minus(s(n),sK1)) = p(minus(s(n),sK0)) ),
inference(resolve,[status(thm)],[c_36,c_760]) ).
cnf(c_46,negated_conjecture,
( le(s(minus(s(n),sK1)),minus(s(n),sK0))
| ~ le(s(sK0),sK1) ),
inference(resolve,[status(thm)],[c_36,c_20]) ).
cnf(c_47,negated_conjecture,
le(sK1,n),
inference(resolve,[status(thm)],[c_36,c_18]) ).
cnf(c_48,negated_conjecture,
le(s(sK0),sK1),
inference(resolve,[status(thm)],[c_36,c_17]) ).
cnf(c_49,negated_conjecture,
le(sK0,n),
inference(resolve,[status(thm)],[c_36,c_16]) ).
cnf(c_50,negated_conjecture,
le(s(n0),sK0),
inference(resolve,[status(thm)],[c_36,c_15]) ).
cnf(c_51,negated_conjecture,
le(s(minus(s(n),sK1)),minus(s(n),sK0)),
inference(resolve,[status(thm)],[c_48,c_46]) ).
cnf(c_60,plain,
plus(A,B) = plus(B,A),
inference(xxres,[status(thm)],[c_31]) ).
cnf(c_62,plain,
( minus(B,D) != minus(A,C)
| plus(minus(s(n),A),B) = plus(minus(s(n),C),D) ),
inference(paramod,[status(thm)],[c_27,c_31]) ).
cnf(c_761,negated_conjecture,
( minus(p(minus(s(n),sK1)),sK1) = minus(p(minus(s(n),sK0)),sK0)
| plus(sK1,p(minus(s(n),sK1))) = plus(p(minus(s(n),sK0)),sK0)
| p(minus(s(n),sK1)) = p(minus(s(n),sK0)) ),
inference(paramod,[status(thm)],[c_60,c_45]) ).
cnf(c_63,negated_conjecture,
( minus(p(minus(s(n),sK1)),sK1) = minus(p(minus(s(n),sK0)),sK0)
| plus(sK1,p(minus(s(n),sK1))) = plus(sK0,p(minus(s(n),sK0)))
| p(minus(s(n),sK1)) = p(minus(s(n),sK0)) ),
inference(paramod,[status(thm)],[c_60,c_761]) ).
cnf(c_762,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_60,c_43]) ).
cnf(c_64,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_60,c_762]) ).
cnf(c_68,plain,
( minus(D,minus(s(n),A)) = minus(C,minus(s(n),B))
| minus(A,B) != minus(C,D) ),
inference(paramod,[status(thm)],[c_27,c_32]) ).
cnf(c_763,plain,
( le(A,B)
| ~ le(s(A),B) ),
inference(resolve,[status(thm)],[c_28,c_29]) ).
cnf(c_82,plain,
le(sK0,sK1),
inference(resolve,[status(thm)],[c_763,c_48]) ).
cnf(c_764,plain,
( le(minus(s(n),sK0),n)
| ~ le(sK0,n) ),
inference(resolve,[status(thm)],[c_50,c_25]) ).
cnf(c_93,plain,
le(minus(s(n),sK0),n),
inference(resolve,[status(thm)],[c_49,c_764]) ).
cnf(c_765,plain,
( p(minus(s(n),sK0)) != p(minus(s(n),sK1))
| ~ le(minus(s(n),sK0),n)
| ~ le(minus(s(n),sK1),n)
| ~ le(s(n0),minus(s(n),sK1)) ),
inference(resolve,[status(thm)],[c_51,c_44]) ).
cnf(c_766,plain,
( p(minus(s(n),sK1)) != p(minus(s(n),sK0))
| ~ le(minus(s(n),sK0),n)
| ~ le(minus(s(n),sK1),n)
| ~ le(s(n0),minus(s(n),sK1)) ),
inference(copy,[status(thm)],[c_765]) ).
cnf(c_101,plain,
( p(minus(s(n),sK1)) != p(minus(s(n),sK0))
| ~ le(minus(s(n),sK1),n)
| ~ le(s(n0),minus(s(n),sK1)) ),
inference(resolve,[status(thm)],[c_93,c_766]) ).
cnf(c_767,plain,
( minus(p(minus(s(n),sK0)),minus(s(n),sK0)) != minus(p(minus(s(n),sK1)),minus(s(n),sK1))
| ~ le(minus(s(n),sK0),n)
| ~ le(minus(s(n),sK1),n)
| ~ le(s(n0),minus(s(n),sK1)) ),
inference(resolve,[status(thm)],[c_51,c_42]) ).
cnf(c_768,plain,
( minus(p(minus(s(n),sK1)),minus(s(n),sK1)) != minus(p(minus(s(n),sK0)),minus(s(n),sK0))
| ~ le(minus(s(n),sK0),n)
| ~ le(minus(s(n),sK1),n)
| ~ le(s(n0),minus(s(n),sK1)) ),
inference(copy,[status(thm)],[c_767]) ).
cnf(c_102,plain,
( minus(p(minus(s(n),sK1)),minus(s(n),sK1)) != minus(p(minus(s(n),sK0)),minus(s(n),sK0))
| ~ le(minus(s(n),sK1),n)
| ~ le(s(n0),minus(s(n),sK1)) ),
inference(resolve,[status(thm)],[c_93,c_768]) ).
cnf(c_769,plain,
( le(s(n0),A)
| ~ le(sK0,A) ),
inference(resolve,[status(thm)],[c_28,c_50]) ).
cnf(c_120,plain,
le(s(n0),sK1),
inference(resolve,[status(thm)],[c_769,c_82]) ).
cnf(c_770,plain,
( le(minus(s(n),sK1),n)
| ~ le(sK1,n) ),
inference(resolve,[status(thm)],[c_120,c_25]) ).
cnf(c_176,plain,
le(minus(s(n),sK1),n),
inference(resolve,[status(thm)],[c_47,c_770]) ).
cnf(c_771,plain,
( le(s(n0),minus(s(n),sK1))
| ~ le(sK1,n) ),
inference(resolve,[status(thm)],[c_120,c_23]) ).
cnf(c_177,plain,
le(s(n0),minus(s(n),sK1)),
inference(resolve,[status(thm)],[c_47,c_771]) ).
cnf(c_772,plain,
( minus(p(minus(s(n),sK1)),minus(s(n),sK1)) != minus(p(minus(s(n),sK0)),minus(s(n),sK0))
| ~ le(minus(s(n),sK1),n) ),
inference(resolve,[status(thm)],[c_177,c_102]) ).
cnf(c_178,plain,
minus(p(minus(s(n),sK1)),minus(s(n),sK1)) != minus(p(minus(s(n),sK0)),minus(s(n),sK0)),
inference(resolve,[status(thm)],[c_176,c_772]) ).
cnf(c_773,plain,
( p(minus(s(n),sK1)) != p(minus(s(n),sK0))
| ~ le(minus(s(n),sK1),n) ),
inference(resolve,[status(thm)],[c_177,c_101]) ).
cnf(c_179,plain,
p(minus(s(n),sK1)) != p(minus(s(n),sK0)),
inference(resolve,[status(thm)],[c_176,c_773]) ).
cnf(c_180,negated_conjecture,
( minus(p(minus(s(n),sK1)),sK1) = minus(p(minus(s(n),sK0)),sK0)
| plus(sK1,p(minus(s(n),sK1))) = plus(sK0,p(minus(s(n),sK0))) ),
inference(resolve,[status(thm)],[c_179,c_63]) ).
cnf(c_276,plain,
( minus(A,D) = minus(C,B)
| plus(A,B) != plus(C,D) ),
inference(paramod,[status(thm)],[c_60,c_30]) ).
cnf(c_774,plain,
( plus(minus(s(n),sK0),p(minus(s(n),sK0))) != plus(minus(s(n),sK1),p(minus(s(n),sK1)))
| ~ le(minus(s(n),sK0),n)
| ~ le(minus(s(n),sK1),n)
| ~ le(s(n0),minus(s(n),sK1)) ),
inference(resolve,[status(thm)],[c_64,c_51]) ).
cnf(c_775,plain,
( plus(minus(s(n),sK1),p(minus(s(n),sK1))) != plus(minus(s(n),sK0),p(minus(s(n),sK0)))
| ~ le(minus(s(n),sK0),n)
| ~ le(minus(s(n),sK1),n)
| ~ le(s(n0),minus(s(n),sK1)) ),
inference(copy,[status(thm)],[c_774]) ).
cnf(c_776,plain,
( plus(minus(s(n),sK1),p(minus(s(n),sK1))) != plus(minus(s(n),sK0),p(minus(s(n),sK0)))
| ~ le(minus(s(n),sK0),n)
| ~ le(minus(s(n),sK1),n) ),
inference(resolve,[status(thm)],[c_177,c_775]) ).
cnf(c_777,plain,
( plus(minus(s(n),sK1),p(minus(s(n),sK1))) != plus(minus(s(n),sK0),p(minus(s(n),sK0)))
| ~ le(minus(s(n),sK0),n) ),
inference(resolve,[status(thm)],[c_176,c_776]) ).
cnf(c_309,plain,
plus(minus(s(n),sK1),p(minus(s(n),sK1))) != plus(minus(s(n),sK0),p(minus(s(n),sK0))),
inference(resolve,[status(thm)],[c_93,c_777]) ).
cnf(c_778,plain,
( minus(minus(s(n),C),minus(s(n),A)) = minus(minus(s(n),D),minus(s(n),B))
| minus(A,B) != minus(C,D) ),
inference(paramod,[status(thm)],[c_27,c_68]) ).
cnf(c_779,plain,
( minus(A,C) = minus(minus(s(n),D),minus(s(n),B))
| minus(A,B) != minus(C,D) ),
inference(paramod,[status(thm)],[c_27,c_778]) ).
cnf(c_393,plain,
( minus(A,C) = minus(B,D)
| minus(A,B) != minus(C,D) ),
inference(paramod,[status(thm)],[c_27,c_779]) ).
cnf(c_471,plain,
( minus(A,C) = minus(D,B)
| plus(A,B) != plus(C,D) ),
inference(paramod,[status(thm)],[c_60,c_276]) ).
cnf(c_780,plain,
minus(sK1,sK0) != minus(p(minus(s(n),sK0)),p(minus(s(n),sK1))),
inference(resolve,[status(thm)],[c_68,c_178]) ).
cnf(c_582,plain,
minus(p(minus(s(n),sK0)),p(minus(s(n),sK1))) != minus(sK1,sK0),
inference(copy,[status(thm)],[c_780]) ).
cnf(c_781,plain,
( minus(sK1,sK0) = minus(p(minus(s(n),sK0)),p(minus(s(n),sK1)))
| minus(p(minus(s(n),sK1)),sK1) = minus(p(minus(s(n),sK0)),sK0) ),
inference(resolve,[status(thm)],[c_180,c_471]) ).
cnf(c_782,plain,
( minus(p(minus(s(n),sK0)),p(minus(s(n),sK1))) = minus(sK1,sK0)
| minus(p(minus(s(n),sK1)),sK1) = minus(p(minus(s(n),sK0)),sK0) ),
inference(copy,[status(thm)],[c_781]) ).
cnf(c_601,plain,
minus(p(minus(s(n),sK1)),sK1) = minus(p(minus(s(n),sK0)),sK0),
inference(resolve,[status(thm)],[c_582,c_782]) ).
cnf(c_749,plain,
minus(p(minus(s(n),sK1)),p(minus(s(n),sK0))) != minus(sK1,sK0),
inference(resolve,[status(thm)],[c_62,c_309]) ).
cnf(c_783,plain,
minus(p(minus(s(n),sK1)),sK1) != minus(p(minus(s(n),sK0)),sK0),
inference(resolve,[status(thm)],[c_393,c_749]) ).
cnf(c_784,plain,
minus(p(minus(s(n),sK0)),sK0) != minus(p(minus(s(n),sK0)),sK0),
inference(paramod,[status(thm)],[c_601,c_783]) ).
cnf(c_752,plain,
$false,
inference(copy,[status(thm)],[c_784]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ133+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.56 % Computer : n026.cluster.edu
% 0.07/0.56 % Model : x86_64 x86_64
% 0.07/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.56 % Memory : 8046.5625MB
% 0.07/0.56 % OS : Linux 6.8.0-71-generic
% 0.07/0.56 % CPULimit : 300
% 0.07/0.56 % WCLimit : 300
% 0.07/0.56 % DateTime : Sat Sep 26 05:21:28 UTC 2026
% 0.07/0.57 % CPUTime :
% 0.07/0.57 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.57 % Process 160949 was started by sandbox on n026,
% 0.07/0.57 % Sat Sep 26 05:21:28 2026
% 0.07/0.57 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/0.58
% 0.07/0.58 % From the command line: assign(max_seconds, 300).
% 0.13/0.99
% 0.13/0.99 % SZS status Theorem for theBenchmark
% 0.13/0.99
% 0.13/0.99 % Proof 1 at 0.24 (+ 0.08) seconds.
% 0.13/0.99 % Length of proof is 69.
% 0.13/0.99 % Level of proof is 9.
% 0.13/0.99 % Maximum clause weight is 69.000.
% 0.13/0.99 % Given clauses 369.
% 0.13/0.99
% 0.13/0.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------