%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG112+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 : n019.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:41 AM UTC 2026
% Result : Theorem 55.22s 8.34s
% Output : CNFRefutation 55.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 4
% Syntax : Number of formulae : 47 ( 12 unt; 0 def)
% Number of atoms : 141 ( 67 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 160 ( 66 ~; 64 |; 26 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 36 ( 0 sgn 17 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__2174,axiom,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& aIdeal0(xI) ),
file('theBenchmark.p',m__2174) ).
fof(m__2228,axiom,
? [W0] :
( W0 != sz00
& aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) ),
file('theBenchmark.p',m__2228) ).
fof(m__2351,axiom,
! [W0] :
( ( W0 != sz00
& aElementOf0(W0,xI) )
=> ? [W1] :
( ! [W2] :
( ( W2 != sz00
& aElementOf0(W2,xI) )
=> ~ iLess0(sbrdtbr0(W2),sbrdtbr0(W1)) )
& W1 != sz00
& aElementOf0(W1,xI) ) ),
file('theBenchmark.p',m__2351) ).
fof(m__,conjecture,
? [W0] :
( ! [W1] :
( ( W1 != sz00
& aElementOf0(W1,xI) )
=> ~ iLess0(sbrdtbr0(W1),sbrdtbr0(W0)) )
& W0 != sz00
& aElementOf0(W0,xI) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ? [W0] :
( ! [W1] :
( ( W1 != sz00
& aElementOf0(W1,xI) )
=> ~ iLess0(sbrdtbr0(W1),sbrdtbr0(W0)) )
& W0 != sz00
& aElementOf0(W0,xI) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_153,plain,
sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) = xI,
inference(clausify,[status(thm)],[m__2174]) ).
fof(nnf_39,plain,
? [W0] :
( sz00 != W0
& aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) ),
inference(fof_nnf,[status(thm)],[m__2228]) ).
fof(sk_m__2228,plain,
( sz00 != sK0
& aElementOf0(sK0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(W0,sK0)],[nnf_39]) ).
cnf(c_158,plain,
aElementOf0(sK0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
inference(split_conjunct,[status(thm)],[sk_m__2228]) ).
cnf(c_159,plain,
aElementOf0(sK0,xI),
inference(paramod,[status(thm)],[c_153,c_158]) ).
cnf(c_160,plain,
sz00 != sK0,
inference(split_conjunct,[status(thm)],[sk_m__2228]) ).
cnf(c_161,plain,
sK0 != sz00,
inference(copy,[status(thm)],[c_160]) ).
fof(nnf_40,plain,
! [W0] :
( ? [W1] :
( ! [W2] :
( ~ iLess0(sbrdtbr0(W2),sbrdtbr0(W1))
| W2 = sz00
| ~ aElementOf0(W2,xI) )
& W1 != sz00
& aElementOf0(W1,xI) )
| sz00 = W0
| ~ aElementOf0(W0,xI) ),
inference(fof_nnf,[status(thm)],[m__2351]) ).
fof(sk_m__2351_sk,plain,
! [W0] :
( ( ! [W2] :
( ~ iLess0(sbrdtbr0(W2),sbrdtbr0(sK1(W0)))
| W2 = sz00
| ~ aElementOf0(W2,xI) )
& sK1(W0) != sz00
& aElementOf0(sK1(W0),xI) )
| sz00 = W0
| ~ aElementOf0(W0,xI) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(W1,sK1(W0))],[nnf_40]) ).
fof(sk_m__2351,plain,
( ! [VAR_0,VAR_1] :
( ~ iLess0(sbrdtbr0(VAR_1),sbrdtbr0(sK1(VAR_0)))
| VAR_1 = sz00
| ~ aElementOf0(VAR_1,xI)
| sz00 = VAR_0
| ~ aElementOf0(VAR_0,xI) )
& ! [VAR_0] :
( sK1(VAR_0) != sz00
| sz00 = VAR_0
| ~ aElementOf0(VAR_0,xI) )
& ! [VAR_0] :
( aElementOf0(sK1(VAR_0),xI)
| sz00 = VAR_0
| ~ aElementOf0(VAR_0,xI) ) ),
inference(cnf_transformation,[status(thm)],[sk_m__2351_sk]) ).
cnf(c_162,plain,
( aElementOf0(sK1(A),xI)
| sz00 = A
| ~ aElementOf0(A,xI) ),
inference(split_conjunct,[status(thm)],[sk_m__2351]) ).
cnf(c_163,plain,
( sK1(A) != sz00
| sz00 = A
| ~ aElementOf0(A,xI) ),
inference(split_conjunct,[status(thm)],[sk_m__2351]) ).
cnf(c_164,plain,
( ~ iLess0(sbrdtbr0(B),sbrdtbr0(sK1(A)))
| B = sz00
| ~ aElementOf0(B,xI)
| sz00 = A
| ~ aElementOf0(A,xI) ),
inference(split_conjunct,[status(thm)],[sk_m__2351]) ).
cnf(c_165,plain,
( ~ iLess0(sbrdtbr0(B),sbrdtbr0(sK1(A)))
| sz00 = B
| ~ aElementOf0(B,xI)
| sz00 = A
| ~ aElementOf0(A,xI) ),
inference(copy,[status(thm)],[c_164]) ).
fof(nnf_41,plain,
! [W0] :
( ? [W1] :
( iLess0(sbrdtbr0(W1),sbrdtbr0(W0))
& W1 != sz00
& aElementOf0(W1,xI) )
| sz00 = W0
| ~ aElementOf0(W0,xI) ),
inference(fof_nnf,[status(thm)],[m___neg]) ).
fof(sk_m___neg_sk,plain,
! [W0] :
( ( iLess0(sbrdtbr0(sK2(W0)),sbrdtbr0(W0))
& sK2(W0) != sz00
& aElementOf0(sK2(W0),xI) )
| sz00 = W0
| ~ aElementOf0(W0,xI) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(W1,sK2(W0))],[nnf_41]) ).
fof(sk_m___neg,plain,
( ! [VAR_0] :
( iLess0(sbrdtbr0(sK2(VAR_0)),sbrdtbr0(VAR_0))
| sz00 = VAR_0
| ~ aElementOf0(VAR_0,xI) )
& ! [VAR_0] :
( sK2(VAR_0) != sz00
| sz00 = VAR_0
| ~ aElementOf0(VAR_0,xI) )
& ! [VAR_0] :
( aElementOf0(sK2(VAR_0),xI)
| sz00 = VAR_0
| ~ aElementOf0(VAR_0,xI) ) ),
inference(cnf_transformation,[status(thm)],[sk_m___neg_sk]) ).
cnf(c_166,negated_conjecture,
( aElementOf0(sK2(A),xI)
| sz00 = A
| ~ aElementOf0(A,xI) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_167,negated_conjecture,
( sK2(A) != sz00
| sz00 = A
| ~ aElementOf0(A,xI) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_168,negated_conjecture,
( iLess0(sbrdtbr0(sK2(A)),sbrdtbr0(A))
| sz00 = A
| ~ aElementOf0(A,xI) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_43457,plain,
( aElementOf0(sK1(sK0),xI)
| sz00 = sK0 ),
inference(resolve,[status(thm)],[c_162,c_159]) ).
cnf(c_43458,plain,
( aElementOf0(sK1(sK0),xI)
| sK0 = sz00 ),
inference(copy,[status(thm)],[c_43457]) ).
cnf(c_884,plain,
aElementOf0(sK1(sK0),xI),
inference(resolve,[status(thm)],[c_161,c_43458]) ).
cnf(c_43459,plain,
( sK1(sK0) != sz00
| sz00 = sK0 ),
inference(resolve,[status(thm)],[c_163,c_159]) ).
cnf(c_43460,plain,
( sK1(sK0) != sz00
| sK0 = sz00 ),
inference(copy,[status(thm)],[c_43459]) ).
cnf(c_885,plain,
sK1(sK0) != sz00,
inference(resolve,[status(thm)],[c_161,c_43460]) ).
cnf(c_43461,plain,
( ~ iLess0(sbrdtbr0(A),sbrdtbr0(sK1(sK0)))
| sz00 = A
| ~ aElementOf0(A,xI)
| sz00 = sK0 ),
inference(resolve,[status(thm)],[c_165,c_159]) ).
cnf(c_43462,plain,
( ~ iLess0(sbrdtbr0(A),sbrdtbr0(sK1(sK0)))
| sz00 = A
| ~ aElementOf0(A,xI)
| sK0 = sz00 ),
inference(copy,[status(thm)],[c_43461]) ).
cnf(c_886,plain,
( ~ iLess0(sbrdtbr0(A),sbrdtbr0(sK1(sK0)))
| sz00 = A
| ~ aElementOf0(A,xI) ),
inference(resolve,[status(thm)],[c_161,c_43462]) ).
cnf(c_43463,negated_conjecture,
( iLess0(sbrdtbr0(sK2(sK1(sK0))),sbrdtbr0(sK1(sK0)))
| sz00 = sK1(sK0) ),
inference(resolve,[status(thm)],[c_884,c_168]) ).
cnf(c_43464,negated_conjecture,
( iLess0(sbrdtbr0(sK2(sK1(sK0))),sbrdtbr0(sK1(sK0)))
| sK1(sK0) = sz00 ),
inference(copy,[status(thm)],[c_43463]) ).
cnf(c_3818,negated_conjecture,
iLess0(sbrdtbr0(sK2(sK1(sK0))),sbrdtbr0(sK1(sK0))),
inference(resolve,[status(thm)],[c_885,c_43464]) ).
cnf(c_43465,negated_conjecture,
( sK2(sK1(sK0)) != sz00
| sz00 = sK1(sK0) ),
inference(resolve,[status(thm)],[c_884,c_167]) ).
cnf(c_43466,negated_conjecture,
( sK2(sK1(sK0)) != sz00
| sK1(sK0) = sz00 ),
inference(copy,[status(thm)],[c_43465]) ).
cnf(c_3819,negated_conjecture,
sK2(sK1(sK0)) != sz00,
inference(resolve,[status(thm)],[c_885,c_43466]) ).
cnf(c_43467,negated_conjecture,
( aElementOf0(sK2(sK1(sK0)),xI)
| sz00 = sK1(sK0) ),
inference(resolve,[status(thm)],[c_884,c_166]) ).
cnf(c_43468,negated_conjecture,
( aElementOf0(sK2(sK1(sK0)),xI)
| sK1(sK0) = sz00 ),
inference(copy,[status(thm)],[c_43467]) ).
cnf(c_3820,negated_conjecture,
aElementOf0(sK2(sK1(sK0)),xI),
inference(resolve,[status(thm)],[c_885,c_43468]) ).
cnf(c_43469,plain,
( ~ iLess0(sbrdtbr0(sK2(sK1(sK0))),sbrdtbr0(sK1(sK0)))
| sz00 = sK2(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_886,c_3820]) ).
cnf(c_43470,plain,
( ~ iLess0(sbrdtbr0(sK2(sK1(sK0))),sbrdtbr0(sK1(sK0)))
| sK2(sK1(sK0)) = sz00 ),
inference(copy,[status(thm)],[c_43469]) ).
cnf(c_43471,plain,
~ iLess0(sbrdtbr0(sK2(sK1(sK0))),sbrdtbr0(sK1(sK0))),
inference(resolve,[status(thm)],[c_3819,c_43470]) ).
cnf(c_43456,plain,
$false,
inference(resolve,[status(thm)],[c_3818,c_43471]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG112+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.36 % Computer : n019.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 : Sat Sep 26 06:08:19 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 571029 was started by sandbox on n019,
% 0.08/0.37 % Sat Sep 26 06:08:19 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.38
% 0.08/0.38 % From the command line: assign(max_seconds, 300).
% 55.22/8.34
% 55.22/8.34 % given #500 (W,wt=14): 17457 aElement0(sdtasdt0(xc,xb)). [resolve(659,a,1124,a)].
% 55.22/8.34
% 55.22/8.34 % given #1000 (W,wt=18): 24958 aElementOf0(A,sdtpldt1(xI,xI)) | sz00 != A. [resolve(402,c,21791,a),rewrite([337(9)]),unit_del(a,709)].
% 55.22/8.34
% 55.22/8.34 % given #1500 (T,wt=17): 37570 aDivisorOf0(sdtpldt0(xc,c1),sdtpldt0(xc,c1)). [back_unit_del(21124),unit_del(b,37503)].
% 55.22/8.34
% 55.22/8.34 % given #2000 (W,wt=15): 40740 aDivisorOf0(f16(xc,xa),sz00). [back_unit_del(7716),unit_del(b,40636)].
% 55.22/8.34
% 55.22/8.34 % given #2500 (T,wt=20): 8964 aDivisorOf0(f16(xa,xa),sz10) | -doDivides0(f16(xa,xa),sz10). [resolve(8928,a,468,b)].
% 55.22/8.34
% 55.22/8.34 % SZS status Theorem for theBenchmark
% 55.22/8.34
% 55.22/8.34 % Proof 1 at 5.71 (+ 1.92) seconds.
% 55.22/8.34 % Length of proof is 23.
% 55.22/8.34 % Level of proof is 5.
% 55.22/8.34 % Maximum clause weight is 33.000.
% 55.22/8.34 % Given clauses 2938.
% 55.22/8.34
% 55.22/8.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------