%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG126+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:26:43 AM UTC 2026
% Result : Theorem 108.21s 15.18s
% Output : CNFRefutation 108.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 12
% Syntax : Number of formulae : 56 ( 25 unt; 0 def)
% Number of atoms : 146 ( 21 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 150 ( 60 ~; 54 |; 21 &)
% ( 4 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% Number of variables : 52 ( 0 sgn 30 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mMulComm,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ),
file('theBenchmark.p',mMulComm) ).
fof(mEOfElem,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('theBenchmark.p',mEOfElem) ).
fof(mDefIdeal,axiom,
! [W0] :
( aIdeal0(W0)
<=> ( ! [W1] :
( aElementOf0(W1,W0)
=> ( ! [W2] :
( aElement0(W2)
=> aElementOf0(sdtasdt0(W2,W1),W0) )
& ! [W2] :
( aElementOf0(W2,W0)
=> aElementOf0(sdtpldt0(W1,W2),W0) ) ) )
& aSet0(W0) ) ),
file('theBenchmark.p',mDefIdeal) ).
fof(mDefDiv,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> ( doDivides0(W0,W1)
<=> ? [W2] :
( sdtasdt0(W0,W2) = W1
& aElement0(W2) ) ) ),
file('theBenchmark.p',mDefDiv) ).
fof(mDefDvs,axiom,
! [W0] :
( aElement0(W0)
=> ! [W1] :
( aDivisorOf0(W1,W0)
<=> ( doDivides0(W1,W0)
& aElement0(W1) ) ) ),
file('theBenchmark.p',mDefDvs) ).
fof(mDefGCD,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> ! [W2] :
( aGcdOfAnd0(W2,W0,W1)
<=> ( ! [W3] :
( ( aDivisorOf0(W3,W1)
& aDivisorOf0(W3,W0) )
=> doDivides0(W3,W2) )
& aDivisorOf0(W2,W1)
& aDivisorOf0(W2,W0) ) ) ),
file('theBenchmark.p',mDefGCD) ).
fof(m__2091,axiom,
( aElement0(xb)
& aElement0(xa) ),
file('theBenchmark.p',m__2091) ).
fof(m__2174,axiom,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& aIdeal0(xI) ),
file('theBenchmark.p',m__2174) ).
fof(m__2273,axiom,
( ! [W0] :
( ( W0 != sz00
& aElementOf0(W0,xI) )
=> ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu)) )
& xu != sz00
& aElementOf0(xu,xI) ),
file('theBenchmark.p',m__2273) ).
fof(m__,conjecture,
aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
inference(assume_negation,[status(cth)],[m__]) ).
fof(m__2129,axiom,
aGcdOfAnd0(xc,xa,xb),
file('theBenchmark.p',m__2129) ).
cnf(c_55,plain,
aGcdOfAnd0(xc,xa,xb),
inference(clausify,[status(thm)],[m__2129]) ).
cnf(c_56,plain,
( aDivisorOf0(C,B)
| ~ aGcdOfAnd0(C,A,B)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mDefGCD]) ).
cnf(c_59,plain,
( aDivisorOf0(xc,xb)
| ~ aElement0(xb)
| ~ aElement0(xa) ),
inference(resolve,[status(thm)],[c_56,c_55]) ).
cnf(c_78,plain,
( sdtasdt0(B,A) = sdtasdt0(A,B)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulComm]) ).
cnf(c_93,plain,
( aElement0(B)
| ~ aElementOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mEOfElem]) ).
cnf(c_115,plain,
( aSet0(A)
| ~ aIdeal0(A) ),
inference(clausify,[status(thm)],[mDefIdeal]) ).
cnf(c_117,plain,
( aElementOf0(sdtasdt0(C,B),A)
| ~ aElement0(C)
| ~ aElementOf0(B,A)
| ~ aIdeal0(A) ),
inference(clausify,[status(thm)],[mDefIdeal]) ).
fof(nnf_30,plain,
! [W0,W1] :
( ( ( ! [W2] :
( sdtasdt0(W0,W2) != W1
| ~ aElement0(W2) )
| doDivides0(W0,W1) )
& ( ? [X0] :
( sdtasdt0(W0,X0) = W1
& aElement0(X0) )
| ~ doDivides0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(fof_nnf,[status(thm)],[mDefDiv]) ).
fof(sk_mDefDiv_sk,plain,
! [W0,W1] :
( ( ( ! [W2] :
( sdtasdt0(W0,W2) != W1
| ~ aElement0(W2) )
| doDivides0(W0,W1) )
& ( ( sdtasdt0(W0,sK0(W0,W1)) = W1
& aElement0(sK0(W0,W1)) )
| ~ doDivides0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0(W0,W1))],[nnf_30]) ).
fof(sk_mDefDiv,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( sdtasdt0(VAR_0,VAR_2) != VAR_1
| ~ aElement0(VAR_2)
| doDivides0(VAR_0,VAR_1)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(VAR_0,sK0(VAR_0,VAR_1)) = VAR_1
| ~ doDivides0(VAR_0,VAR_1)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aElement0(sK0(VAR_0,VAR_1))
| ~ doDivides0(VAR_0,VAR_1)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mDefDiv_sk]) ).
cnf(c_135,plain,
( aElement0(sK0(A,B))
| ~ doDivides0(A,B)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefDiv]) ).
cnf(c_136,plain,
( sdtasdt0(A,sK0(A,B)) = B
| ~ doDivides0(A,B)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefDiv]) ).
cnf(c_138,plain,
( aElement0(B)
| ~ aDivisorOf0(B,A)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mDefDvs]) ).
cnf(c_150,plain,
aElement0(xa),
inference(clausify,[status(thm)],[m__2091]) ).
cnf(c_151,plain,
aElement0(xb),
inference(clausify,[status(thm)],[m__2091]) ).
cnf(c_153,plain,
aIdeal0(xI),
inference(clausify,[status(thm)],[m__2174]) ).
cnf(c_154,plain,
sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) = xI,
inference(clausify,[status(thm)],[m__2174]) ).
cnf(c_162,plain,
aElementOf0(xu,xI),
inference(clausify,[status(thm)],[m__2273]) ).
fof(m__2744,axiom,
doDivides0(xu,xc),
file('theBenchmark.p',m__2744) ).
cnf(c_167,plain,
doDivides0(xu,xc),
inference(clausify,[status(thm)],[m__2744]) ).
cnf(c_168,negated_conjecture,
~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_169,negated_conjecture,
~ aElementOf0(xc,xI),
inference(paramod,[status(thm)],[c_154,c_168]) ).
cnf(c_24641,plain,
( aDivisorOf0(xc,xb)
| ~ aElement0(xb) ),
inference(resolve,[status(thm)],[c_150,c_59]) ).
cnf(c_251,plain,
aDivisorOf0(xc,xb),
inference(resolve,[status(thm)],[c_151,c_24641]) ).
cnf(c_709,plain,
aSet0(xI),
inference(resolve,[status(thm)],[c_153,c_115]) ).
cnf(c_24642,plain,
( aElementOf0(sdtasdt0(A,xu),xI)
| ~ aElement0(A)
| ~ aIdeal0(xI) ),
inference(resolve,[status(thm)],[c_162,c_117]) ).
cnf(c_893,plain,
( aElementOf0(sdtasdt0(A,xu),xI)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_153,c_24642]) ).
cnf(c_24643,plain,
( aElement0(xu)
| ~ aSet0(xI) ),
inference(resolve,[status(thm)],[c_162,c_93]) ).
cnf(c_907,plain,
aElement0(xu),
inference(resolve,[status(thm)],[c_709,c_24643]) ).
cnf(c_24644,plain,
( sdtasdt0(xu,sK0(xu,xc)) = xc
| ~ aElement0(xc)
| ~ aElement0(xu) ),
inference(resolve,[status(thm)],[c_167,c_136]) ).
cnf(c_969,plain,
( sdtasdt0(xu,sK0(xu,xc)) = xc
| ~ aElement0(xc) ),
inference(resolve,[status(thm)],[c_907,c_24644]) ).
cnf(c_24645,plain,
( aElement0(sK0(xu,xc))
| ~ aElement0(xc)
| ~ aElement0(xu) ),
inference(resolve,[status(thm)],[c_167,c_135]) ).
cnf(c_970,plain,
( aElement0(sK0(xu,xc))
| ~ aElement0(xc) ),
inference(resolve,[status(thm)],[c_907,c_24645]) ).
cnf(c_24646,plain,
( aElement0(xc)
| ~ aElement0(xb) ),
inference(resolve,[status(thm)],[c_251,c_138]) ).
cnf(c_1220,plain,
aElement0(xc),
inference(resolve,[status(thm)],[c_151,c_24646]) ).
cnf(c_1233,plain,
aElement0(sK0(xu,xc)),
inference(resolve,[status(thm)],[c_1220,c_970]) ).
cnf(c_1234,plain,
sdtasdt0(xu,sK0(xu,xc)) = xc,
inference(resolve,[status(thm)],[c_1220,c_969]) ).
cnf(c_1720,plain,
( sdtasdt0(xu,A) = sdtasdt0(A,xu)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_907,c_78]) ).
cnf(c_23605,plain,
aElementOf0(sdtasdt0(sK0(xu,xc),xu),xI),
inference(resolve,[status(thm)],[c_893,c_1233]) ).
cnf(c_24647,plain,
sdtasdt0(xu,sK0(xu,xc)) = sdtasdt0(sK0(xu,xc),xu),
inference(resolve,[status(thm)],[c_1720,c_1233]) ).
cnf(c_24648,plain,
xc = sdtasdt0(sK0(xu,xc),xu),
inference(paramod,[status(thm)],[c_1234,c_24647]) ).
cnf(c_24636,plain,
sdtasdt0(sK0(xu,xc),xu) = xc,
inference(copy,[status(thm)],[c_24648]) ).
cnf(c_24649,plain,
aElementOf0(xc,xI),
inference(paramod,[status(thm)],[c_24636,c_23605]) ).
cnf(c_24640,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_169,c_24649]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG126+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n015.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 06:15:28 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 3300402 was started by sandbox on n015,
% 0.08/0.36 % Sat Sep 26 06:15:28 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 108.21/15.18
% 108.21/15.18 % given #500 (W,wt=15): 10440 f16(sz10,xc) = xc. [resolve(10075,a,81,a),rewrite([10074(5)]),flip(a)].
% 108.21/15.18
% 108.21/15.18 % given #1000 (W,wt=18): 9604 doDivides0(xa,smndt0(xb)) | smndt0(xb) != xa. [resolve(9557,a,663,a),flip(b)].
% 108.21/15.18
% 108.21/15.18 % SZS status Theorem for theBenchmark
% 108.21/15.18
% 108.21/15.18 % Proof 1 at 4.76 (+ 1.75) seconds.
% 108.21/15.18 % Length of proof is 41.
% 108.21/15.18 % Level of proof is 7.
% 108.21/15.18 % Maximum clause weight is 29.000.
% 108.21/15.18 % Given clauses 1410.
% 108.21/15.18
% 108.21/15.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------