%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX035+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /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 : Sun Sep 27 09:16:06 AM UTC 2026
% Result : Theorem 285.62s 37.84s
% Output : CNFRefutation 285.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 7
% Syntax : Number of formulae : 44 ( 13 unt; 0 def)
% Number of atoms : 102 ( 26 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 96 ( 38 ~; 36 |; 12 &)
% ( 4 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 66 ( 0 sgn 26 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(id15,axiom,
! [Xx1,Xx2,Xx3] :
( times_succeeds(Xx1,Xx2,Xx3)
<=> ( ( Xx3 = '0'
& Xx1 = '0' )
| ? [Xx4,Xx5] :
( plus_succeeds(Xx2,Xx5,Xx3)
& times_succeeds(Xx4,Xx2,Xx5)
& Xx1 = s(Xx4) ) ) ),
file('theBenchmark.p',id15) ).
fof(id27,axiom,
! [Xx1] :
( nat_succeeds(Xx1)
<=> ( Xx1 = '0'
| ? [Xx2] :
( nat_succeeds(Xx2)
& Xx1 = s(Xx2) ) ) ),
file('theBenchmark.p',id27) ).
fof('(@+)/2',axiom,
! [Xx,Xy,Xz] :
( nat_succeeds(Xx)
=> ( '@+'(Xx,Xy) = Xz
<=> plus_succeeds(Xx,Xy,Xz) ) ),
file('theBenchmark.p','(@+)/2') ).
fof('(@*)/2',axiom,
! [Xx,Xy,Xz] :
( ( nat_succeeds(Xy)
& nat_succeeds(Xx) )
=> ( '@*'(Xx,Xy) = Xz
<=> times_succeeds(Xx,Xy,Xz) ) ),
file('theBenchmark.p','(@*)/2') ).
fof('lemma-(plus:existence)',axiom,
! [Xx,Xy] :
( nat_succeeds(Xx)
=> ? [Xz] : plus_succeeds(Xx,Xy,Xz) ),
file('theBenchmark.p','lemma-(plus:existence)') ).
fof('lemma-(times:existence)',axiom,
! [Xx,Xy] :
( ( nat_succeeds(Xy)
& nat_succeeds(Xx) )
=> ? [Xz] : times_succeeds(Xx,Xy,Xz) ),
file('theBenchmark.p','lemma-(times:existence)') ).
fof('corollary-(times:successor)',conjecture,
! [Xx,Xy] :
( ( nat_succeeds(Xy)
& nat_succeeds(Xx) )
=> '@*'(s(Xx),Xy) = '@+'(Xy,'@*'(Xx,Xy)) ),
file('theBenchmark.p','corollary-(times:successor)') ).
fof('corollary-(times:successor)_neg',negated_conjecture,
~ ! [Xx,Xy] :
( ( nat_succeeds(Xy)
& nat_succeeds(Xx) )
=> '@*'(s(Xx),Xy) = '@+'(Xy,'@*'(Xx,Xy)) ),
inference(assume_negation,[status(cth)],['corollary-(times:successor)']) ).
cnf(c_89,plain,
( ~ plus_succeeds(B,E,C)
| ~ times_succeeds(D,B,E)
| s(D) != A
| times_succeeds(A,B,C) ),
inference(clausify,[status(thm)],[id15]) ).
cnf(c_194,plain,
( ~ nat_succeeds(B)
| s(B) != A
| nat_succeeds(A) ),
inference(clausify,[status(thm)],[id27]) ).
cnf(c_208,plain,
( ~ plus_succeeds(A,B,C)
| '@+'(A,B) = C
| ~ nat_succeeds(A) ),
inference(clausify,[status(thm)],['(@+)/2']) ).
cnf(c_210,plain,
( ~ times_succeeds(A,B,C)
| '@*'(A,B) = C
| ~ nat_succeeds(B)
| ~ nat_succeeds(A) ),
inference(clausify,[status(thm)],['(@*)/2']) ).
fof(nnf_42,plain,
! [Xx,Xy] :
( ? [Xz] : plus_succeeds(Xx,Xy,Xz)
| ~ nat_succeeds(Xx) ),
inference(fof_nnf,[status(thm)],['lemma-(plus:existence)']) ).
fof('sk_lemma-(plus:existence)',plain,
! [Xx,Xy] :
( plus_succeeds(Xx,Xy,sK0(Xx,Xy))
| ~ nat_succeeds(Xx) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(Xz,sK0(Xx,Xy))],[nnf_42]) ).
cnf(c_222,plain,
( plus_succeeds(A,B,sK0(A,B))
| ~ nat_succeeds(A) ),
inference(split_conjunct,[status(thm)],['sk_lemma-(plus:existence)']) ).
fof(nnf_57,plain,
! [Xx,Xy] :
( ? [Xz] : times_succeeds(Xx,Xy,Xz)
| ~ nat_succeeds(Xy)
| ~ nat_succeeds(Xx) ),
inference(fof_nnf,[status(thm)],['lemma-(times:existence)']) ).
fof('sk_lemma-(times:existence)',plain,
! [Xx,Xy] :
( times_succeeds(Xx,Xy,sK1(Xx,Xy))
| ~ nat_succeeds(Xy)
| ~ nat_succeeds(Xx) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(Xz,sK1(Xx,Xy))],[nnf_57]) ).
cnf(c_237,plain,
( times_succeeds(A,B,sK1(A,B))
| ~ nat_succeeds(B)
| ~ nat_succeeds(A) ),
inference(split_conjunct,[status(thm)],['sk_lemma-(times:existence)']) ).
fof(nnf_61,plain,
? [Xx,Xy] :
( '@*'(s(Xx),Xy) != '@+'(Xy,'@*'(Xx,Xy))
& nat_succeeds(Xy)
& nat_succeeds(Xx) ),
inference(fof_nnf,[status(thm)],['corollary-(times:successor)_neg']) ).
fof('sk_corollary-(times:successor)_neg',plain,
( '@*'(s(sK2),sK3) != '@+'(sK3,'@*'(sK2,sK3))
& nat_succeeds(sK3)
& nat_succeeds(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(Xx,sK2),skolemize(Xy,sK3)],[nnf_61]) ).
cnf(c_245,negated_conjecture,
nat_succeeds(sK2),
inference(split_conjunct,[status(thm)],['sk_corollary-(times:successor)_neg']) ).
cnf(c_246,negated_conjecture,
nat_succeeds(sK3),
inference(split_conjunct,[status(thm)],['sk_corollary-(times:successor)_neg']) ).
cnf(c_247,negated_conjecture,
'@*'(s(sK2),sK3) != '@+'(sK3,'@*'(sK2,sK3)),
inference(split_conjunct,[status(thm)],['sk_corollary-(times:successor)_neg']) ).
cnf(c_282,plain,
( ~ plus_succeeds(B,D,C)
| ~ times_succeeds(A,B,D)
| times_succeeds(s(A),B,C) ),
inference(xxres,[status(thm)],[c_89]) ).
cnf(c_421,plain,
( ~ nat_succeeds(A)
| nat_succeeds(s(A)) ),
inference(xxres,[status(thm)],[c_194]) ).
cnf(c_452,plain,
( times_succeeds(sK2,A,sK1(sK2,A))
| ~ nat_succeeds(A) ),
inference(resolve,[status(thm)],[c_245,c_237]) ).
cnf(c_520,plain,
plus_succeeds(sK3,A,sK0(sK3,A)),
inference(resolve,[status(thm)],[c_246,c_222]) ).
cnf(c_527,plain,
( ~ times_succeeds(A,sK3,B)
| '@*'(A,sK3) = B
| ~ nat_succeeds(A) ),
inference(resolve,[status(thm)],[c_246,c_210]) ).
cnf(c_962,plain,
nat_succeeds(s(sK2)),
inference(resolve,[status(thm)],[c_421,c_245]) ).
cnf(c_22050,plain,
( '@+'(sK3,A) = sK0(sK3,A)
| ~ nat_succeeds(sK3) ),
inference(resolve,[status(thm)],[c_520,c_208]) ).
cnf(c_22051,plain,
( sK0(sK3,A) = '@+'(sK3,A)
| ~ nat_succeeds(sK3) ),
inference(copy,[status(thm)],[c_22050]) ).
cnf(c_1578,negated_conjecture,
sK0(sK3,A) = '@+'(sK3,A),
inference(resolve,[status(thm)],[c_246,c_22051]) ).
cnf(c_1591,plain,
plus_succeeds(sK3,A,'@+'(sK3,A)),
inference(paramod,[status(thm)],[c_1578,c_520]) ).
cnf(c_2404,plain,
times_succeeds(sK2,sK3,sK1(sK2,sK3)),
inference(resolve,[status(thm)],[c_452,c_246]) ).
cnf(c_22052,plain,
( '@*'(sK2,sK3) = sK1(sK2,sK3)
| ~ nat_succeeds(sK3)
| ~ nat_succeeds(sK2) ),
inference(resolve,[status(thm)],[c_2404,c_210]) ).
cnf(c_22053,plain,
( sK1(sK2,sK3) = '@*'(sK2,sK3)
| ~ nat_succeeds(sK3)
| ~ nat_succeeds(sK2) ),
inference(copy,[status(thm)],[c_22052]) ).
cnf(c_22054,negated_conjecture,
( sK1(sK2,sK3) = '@*'(sK2,sK3)
| ~ nat_succeeds(sK3) ),
inference(resolve,[status(thm)],[c_245,c_22053]) ).
cnf(c_2527,negated_conjecture,
sK1(sK2,sK3) = '@*'(sK2,sK3),
inference(resolve,[status(thm)],[c_246,c_22054]) ).
cnf(c_2539,plain,
times_succeeds(sK2,sK3,'@*'(sK2,sK3)),
inference(paramod,[status(thm)],[c_2527,c_2404]) ).
cnf(c_10603,plain,
( ~ plus_succeeds(sK3,'@*'(sK2,sK3),A)
| times_succeeds(s(sK2),sK3,A) ),
inference(resolve,[status(thm)],[c_282,c_2539]) ).
cnf(c_10616,plain,
times_succeeds(s(sK2),sK3,'@+'(sK3,'@*'(sK2,sK3))),
inference(resolve,[status(thm)],[c_10603,c_1591]) ).
cnf(c_22055,plain,
( '@*'(s(sK2),sK3) = '@+'(sK3,'@*'(sK2,sK3))
| ~ nat_succeeds(s(sK2)) ),
inference(resolve,[status(thm)],[c_10616,c_527]) ).
cnf(c_22056,plain,
'@*'(s(sK2),sK3) = '@+'(sK3,'@*'(sK2,sK3)),
inference(resolve,[status(thm)],[c_962,c_22055]) ).
cnf(c_22049,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_247,c_22056]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX035+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.39 % Computer : n001.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sat Sep 26 16:49:28 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.40 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.40 % Process 2239873 was started by sandbox2 on n001,
% 0.13/0.40 % Sat Sep 26 16:49:28 2026
% 0.13/0.40 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.41
% 0.18/0.41 % From the command line: assign(max_seconds, 300).
% 285.62/37.84
% 285.62/37.84 % given #500 (T,wt=17): 1578 f31(c5,A) = @+(c5,A). [resolve(520,a,208,c),flip(b),unit_del(a,246)].
% 285.62/37.84
% 285.62/37.84 % given #1000 (T,wt=19): 4212 plus_succeeds(0,A,s(c4)) | s(c4) != A. [resolve(1268,b,311,a),flip(b)].
% 285.62/37.84
% 285.62/37.84 % given #1500 (W,wt=21): 8572 times_succeeds(@*(c4,c4),0,0) | @*(c4,c4) != 0. [resolve(2024,b,287,a),flip(b)].
% 285.62/37.84
% 285.62/37.84 % given #2000 (W,wt=14): 11042 c5 = 0 | @<_succeeds(A,c5) | 0 != A. [resolve(535,a,173,c)].
% 285.62/37.84
% 285.62/37.84 % given #2500 (F,wt=23): 14200 -nat_fails(@+(c4,@+(c5,c5))). [resolve(1364,a,75,a)].
% 285.62/37.84
% 285.62/37.84 % given #3000 (T,wt=23): 7243 times_terminates(c5,@+(c5,@*(c4,c5)),A). [resolve(2549,a,507,a)].
% 285.62/37.84
% 285.62/37.84 % given #3500 (T,wt=23): 17927 plus_fails(c5,A,f28(c5)) | plus_succeeds(s(c5),A,c5) | c5 = 0. [resolve(10674,a,535,a)].
% 285.62/37.84
% 285.62/37.84 % given #4000 (T,wt=24): 4042 times_terminates(s(@+(c5,c5)),@*(c5,c4),A). [resolve(959,a,2319,a)].
% 285.62/37.84
% 285.62/37.84 % given #4500 (T,wt=24): 10345 plus_terminates(A,B,@+(@*(c5,c4),s(c4))). [resolve(8084,a,214,a)].
% 285.62/37.84
% 285.62/37.84 % SZS status Theorem for theBenchmark
% 285.62/37.84
% 285.62/37.84 % Proof 1 at 4.00 (+ 0.92) seconds.
% 285.62/37.84 % Length of proof is 30.
% 285.62/37.84 % Level of proof is 8.
% 285.62/37.84 % Maximum clause weight is 26.000.
% 285.62/37.84 % Given clauses 4518.
% 285.62/37.84
% 285.62/37.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------