%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG108+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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:40 AM UTC 2026
% Result : Theorem 1.64s 0.66s
% Output : CNFRefutation 1.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 8
% Syntax : Number of formulae : 60 ( 26 unt; 0 def)
% Number of atoms : 338 ( 86 equ)
% Maximal formula atoms : 127 ( 5 avg)
% Number of connectives : 451 ( 173 ~; 166 |; 106 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 41 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 104 ( 0 sgn 57 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mMulUnit,axiom,
! [W0] :
( aElement0(W0)
=> ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
file('theBenchmark.p',mMulUnit) ).
fof(mMulZero,axiom,
! [W0] :
( aElement0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('theBenchmark.p',mMulZero) ).
fof(mDefPrIdeal,axiom,
! [W0] :
( aElement0(W0)
=> ! [W1] :
( W1 = slsdtgt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) ) )
& aSet0(W1) ) ) ),
file('theBenchmark.p',mDefPrIdeal) ).
fof(m__2091,axiom,
( aElement0(xb)
& aElement0(xa) ),
file('theBenchmark.p',m__2091) ).
fof(m__2129,axiom,
( aGcdOfAnd0(xc,xa,xb)
& ! [W0] :
( ( ( aDivisorOf0(W0,xb)
| doDivides0(W0,xb)
| ? [W1] :
( sdtasdt0(W0,W1) = xb
& aElement0(W1) ) )
& ( aDivisorOf0(W0,xa)
| ( ( doDivides0(W0,xa)
| ? [W1] :
( sdtasdt0(W0,W1) = xa
& aElement0(W1) ) )
& aElement0(W0) ) ) )
=> ( doDivides0(W0,xc)
& ? [W1] :
( sdtasdt0(W0,W1) = xc
& aElement0(W1) ) ) )
& aDivisorOf0(xc,xb)
& doDivides0(xc,xb)
& ? [W0] :
( sdtasdt0(xc,W0) = xb
& aElement0(W0) )
& aElement0(xc)
& aDivisorOf0(xc,xa)
& doDivides0(xc,xa)
& ? [W0] :
( sdtasdt0(xc,W0) = xa
& aElement0(W0) )
& aElement0(xc) ),
file('theBenchmark.p',m__2129) ).
fof(m__,conjecture,
( ( aElementOf0(xb,slsdtgt0(xb))
| ? [W0] :
( sdtasdt0(xb,W0) = xb
& aElement0(W0) ) )
& ( aElementOf0(sz00,slsdtgt0(xb))
| ? [W0] :
( sdtasdt0(xb,W0) = sz00
& aElement0(W0) ) )
& ( aElementOf0(xa,slsdtgt0(xa))
| ? [W0] :
( sdtasdt0(xa,W0) = xa
& aElement0(W0) ) )
& ( aElementOf0(sz00,slsdtgt0(xa))
| ? [W0] :
( sdtasdt0(xa,W0) = sz00
& aElement0(W0) ) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( ( aElementOf0(xb,slsdtgt0(xb))
| ? [W0] :
( sdtasdt0(xb,W0) = xb
& aElement0(W0) ) )
& ( aElementOf0(sz00,slsdtgt0(xb))
| ? [W0] :
( sdtasdt0(xb,W0) = sz00
& aElement0(W0) ) )
& ( aElementOf0(xa,slsdtgt0(xa))
| ? [W0] :
( sdtasdt0(xa,W0) = xa
& aElement0(W0) ) )
& ( aElementOf0(sz00,slsdtgt0(xa))
| ? [W0] :
( sdtasdt0(xa,W0) = sz00
& aElement0(W0) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_72,negated_conjecture,
( ~ aElementOf0(xb,slsdtgt0(xb))
| ~ aElementOf0(sz00,slsdtgt0(xb))
| ~ aElementOf0(xa,slsdtgt0(xa))
| ~ aElementOf0(sz00,slsdtgt0(xa)) ),
inference(clausify,[status(thm)],[m___neg]) ).
fof(nnf_37,plain,
( aGcdOfAnd0(xc,xa,xb)
& ! [W0] :
( ( doDivides0(W0,xc)
& ? [W1] :
( sdtasdt0(W0,W1) = xc
& aElement0(W1) ) )
| ( ~ aDivisorOf0(W0,xb)
& ~ doDivides0(W0,xb)
& ! [X2] :
( sdtasdt0(W0,X2) != xb
| ~ aElement0(X2) ) )
| ( ~ aDivisorOf0(W0,xa)
& ( ( ~ doDivides0(W0,xa)
& ! [X1] :
( sdtasdt0(W0,X1) != xa
| ~ aElement0(X1) ) )
| ~ aElement0(W0) ) ) )
& aDivisorOf0(xc,xb)
& doDivides0(xc,xb)
& ? [X0] :
( sdtasdt0(xc,X0) = xb
& aElement0(X0) )
& aElement0(xc)
& aDivisorOf0(xc,xa)
& doDivides0(xc,xa)
& ? [X3] :
( sdtasdt0(xc,X3) = xa
& aElement0(X3) )
& aElement0(xc) ),
inference(fof_nnf,[status(thm)],[m__2129]) ).
fof(sk_m__2129_sk,plain,
( aGcdOfAnd0(xc,xa,xb)
& ! [W0] :
( ( doDivides0(W0,xc)
& sdtasdt0(W0,sK2(W0)) = xc
& aElement0(sK2(W0)) )
| ( ~ aDivisorOf0(W0,xb)
& ~ doDivides0(W0,xb)
& ! [X2] :
( sdtasdt0(W0,X2) != xb
| ~ aElement0(X2) ) )
| ( ~ aDivisorOf0(W0,xa)
& ( ( ~ doDivides0(W0,xa)
& ! [X1] :
( sdtasdt0(W0,X1) != xa
| ~ aElement0(X1) ) )
| ~ aElement0(W0) ) ) )
& aDivisorOf0(xc,xb)
& doDivides0(xc,xb)
& sdtasdt0(xc,sK0) = xb
& aElement0(sK0)
& aElement0(xc)
& aDivisorOf0(xc,xa)
& doDivides0(xc,xa)
& sdtasdt0(xc,sK1) = xa
& aElement0(sK1)
& aElement0(xc) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0,sK2]),skolemize(X3,sK1),skolemize(X0,sK0),skolemize(W1,sK2(W0))],[nnf_37]) ).
fof(sk_m__2129,plain,
( aGcdOfAnd0(xc,xa,xb)
& ! [VAR_0] :
( doDivides0(VAR_0,xc)
| ~ aDivisorOf0(VAR_0,xb)
| ~ aDivisorOf0(VAR_0,xa) )
& ! [VAR_0] :
( sdtasdt0(VAR_0,sK2(VAR_0)) = xc
| ~ aDivisorOf0(VAR_0,xb)
| ~ aDivisorOf0(VAR_0,xa) )
& ! [VAR_0] :
( aElement0(sK2(VAR_0))
| ~ aDivisorOf0(VAR_0,xb)
| ~ aDivisorOf0(VAR_0,xa) )
& ! [VAR_0] :
( doDivides0(VAR_0,xc)
| ~ doDivides0(VAR_0,xb)
| ~ aDivisorOf0(VAR_0,xa) )
& ! [VAR_0] :
( sdtasdt0(VAR_0,sK2(VAR_0)) = xc
| ~ doDivides0(VAR_0,xb)
| ~ aDivisorOf0(VAR_0,xa) )
& ! [VAR_0] :
( aElement0(sK2(VAR_0))
| ~ doDivides0(VAR_0,xb)
| ~ aDivisorOf0(VAR_0,xa) )
& ! [VAR_0,VAR_1] :
( doDivides0(VAR_0,xc)
| sdtasdt0(VAR_0,VAR_1) != xb
| ~ aElement0(VAR_1)
| ~ aDivisorOf0(VAR_0,xa) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(VAR_0,sK2(VAR_0)) = xc
| sdtasdt0(VAR_0,VAR_1) != xb
| ~ aElement0(VAR_1)
| ~ aDivisorOf0(VAR_0,xa) )
& ! [VAR_0,VAR_1] :
( aElement0(sK2(VAR_0))
| sdtasdt0(VAR_0,VAR_1) != xb
| ~ aElement0(VAR_1)
| ~ aDivisorOf0(VAR_0,xa) )
& ! [VAR_0] :
( doDivides0(VAR_0,xc)
| ~ aDivisorOf0(VAR_0,xb)
| ~ doDivides0(VAR_0,xa)
| ~ aElement0(VAR_0) )
& ! [VAR_0] :
( sdtasdt0(VAR_0,sK2(VAR_0)) = xc
| ~ aDivisorOf0(VAR_0,xb)
| ~ doDivides0(VAR_0,xa)
| ~ aElement0(VAR_0) )
& ! [VAR_0] :
( aElement0(sK2(VAR_0))
| ~ aDivisorOf0(VAR_0,xb)
| ~ doDivides0(VAR_0,xa)
| ~ aElement0(VAR_0) )
& ! [VAR_0] :
( doDivides0(VAR_0,xc)
| ~ doDivides0(VAR_0,xb)
| ~ doDivides0(VAR_0,xa)
| ~ aElement0(VAR_0) )
& ! [VAR_0] :
( sdtasdt0(VAR_0,sK2(VAR_0)) = xc
| ~ doDivides0(VAR_0,xb)
| ~ doDivides0(VAR_0,xa)
| ~ aElement0(VAR_0) )
& ! [VAR_0] :
( aElement0(sK2(VAR_0))
| ~ doDivides0(VAR_0,xb)
| ~ doDivides0(VAR_0,xa)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( doDivides0(VAR_0,xc)
| sdtasdt0(VAR_0,VAR_1) != xb
| ~ aElement0(VAR_1)
| ~ doDivides0(VAR_0,xa)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(VAR_0,sK2(VAR_0)) = xc
| sdtasdt0(VAR_0,VAR_1) != xb
| ~ aElement0(VAR_1)
| ~ doDivides0(VAR_0,xa)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aElement0(sK2(VAR_0))
| sdtasdt0(VAR_0,VAR_1) != xb
| ~ aElement0(VAR_1)
| ~ doDivides0(VAR_0,xa)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( doDivides0(VAR_0,xc)
| ~ aDivisorOf0(VAR_0,xb)
| sdtasdt0(VAR_0,VAR_1) != xa
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(VAR_0,sK2(VAR_0)) = xc
| ~ aDivisorOf0(VAR_0,xb)
| sdtasdt0(VAR_0,VAR_1) != xa
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aElement0(sK2(VAR_0))
| ~ aDivisorOf0(VAR_0,xb)
| sdtasdt0(VAR_0,VAR_1) != xa
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( doDivides0(VAR_0,xc)
| ~ doDivides0(VAR_0,xb)
| sdtasdt0(VAR_0,VAR_1) != xa
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(VAR_0,sK2(VAR_0)) = xc
| ~ doDivides0(VAR_0,xb)
| sdtasdt0(VAR_0,VAR_1) != xa
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aElement0(sK2(VAR_0))
| ~ doDivides0(VAR_0,xb)
| sdtasdt0(VAR_0,VAR_1) != xa
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( doDivides0(VAR_0,xc)
| sdtasdt0(VAR_0,VAR_2) != xb
| ~ aElement0(VAR_2)
| sdtasdt0(VAR_0,VAR_1) != xa
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sdtasdt0(VAR_0,sK2(VAR_0)) = xc
| sdtasdt0(VAR_0,VAR_2) != xb
| ~ aElement0(VAR_2)
| sdtasdt0(VAR_0,VAR_1) != xa
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElement0(sK2(VAR_0))
| sdtasdt0(VAR_0,VAR_2) != xb
| ~ aElement0(VAR_2)
| sdtasdt0(VAR_0,VAR_1) != xa
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& aDivisorOf0(xc,xb)
& doDivides0(xc,xb)
& sdtasdt0(xc,sK0) = xb
& aElement0(sK0)
& aDivisorOf0(xc,xa)
& doDivides0(xc,xa)
& sdtasdt0(xc,sK1) = xa
& aElement0(sK1)
& aElement0(xc) ),
inference(cnf_transformation,[status(thm)],[sk_m__2129_sk]) ).
cnf(c_132,plain,
sdtasdt0(xc,sK0) = xb,
inference(split_conjunct,[status(thm)],[sk_m__2129]) ).
cnf(c_133,plain,
xb = sdtasdt0(xc,sK0),
inference(copy,[status(thm)],[c_132]) ).
cnf(c_137,plain,
sdtasdt0(xc,sK1) = xa,
inference(split_conjunct,[status(thm)],[sk_m__2129]) ).
cnf(c_138,plain,
xa = sdtasdt0(xc,sK1),
inference(copy,[status(thm)],[c_137]) ).
cnf(c_143,plain,
aElement0(xb),
inference(clausify,[status(thm)],[m__2091]) ).
cnf(c_144,plain,
aElement0(sdtasdt0(xc,sK0)),
inference(paramod,[status(thm)],[c_133,c_143]) ).
cnf(c_145,plain,
aElement0(xa),
inference(clausify,[status(thm)],[m__2091]) ).
cnf(c_146,plain,
aElement0(sdtasdt0(xc,sK1)),
inference(paramod,[status(thm)],[c_138,c_145]) ).
cnf(c_152,plain,
( sdtasdt0(A,D) != C
| ~ aElement0(D)
| aElementOf0(C,B)
| slsdtgt0(A) != B
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mDefPrIdeal]) ).
cnf(c_206,plain,
( sdtasdt0(A,sz00) = sz00
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulZero]) ).
cnf(c_214,plain,
( sdtasdt0(A,sz10) = A
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulUnit]) ).
fof(mSortsC_01,axiom,
aElement0(sz10),
file('theBenchmark.p',mSortsC_01) ).
cnf(c_226,plain,
aElement0(sz10),
inference(clausify,[status(thm)],[mSortsC_01]) ).
fof(mSortsC,axiom,
aElement0(sz00),
file('theBenchmark.p',mSortsC) ).
cnf(c_227,plain,
aElement0(sz00),
inference(clausify,[status(thm)],[mSortsC]) ).
cnf(c_2981,negated_conjecture,
( ~ aElementOf0(xb,slsdtgt0(xb))
| ~ aElementOf0(sz00,slsdtgt0(xb))
| ~ aElementOf0(xa,slsdtgt0(xa))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(paramod,[status(thm)],[c_138,c_72]) ).
cnf(c_2982,negated_conjecture,
( ~ aElementOf0(xb,slsdtgt0(xb))
| ~ aElementOf0(sz00,slsdtgt0(xb))
| ~ aElementOf0(sdtasdt0(xc,sK1),slsdtgt0(xa))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(paramod,[status(thm)],[c_138,c_2981]) ).
cnf(c_2983,negated_conjecture,
( ~ aElementOf0(xb,slsdtgt0(xb))
| ~ aElementOf0(sz00,slsdtgt0(xb))
| ~ aElementOf0(sdtasdt0(xc,sK1),slsdtgt0(sdtasdt0(xc,sK1)))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(paramod,[status(thm)],[c_138,c_2982]) ).
cnf(c_2984,negated_conjecture,
( ~ aElementOf0(xb,slsdtgt0(xb))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK0)))
| ~ aElementOf0(sdtasdt0(xc,sK1),slsdtgt0(sdtasdt0(xc,sK1)))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(paramod,[status(thm)],[c_133,c_2983]) ).
cnf(c_2985,negated_conjecture,
( ~ aElementOf0(sdtasdt0(xc,sK0),slsdtgt0(xb))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK0)))
| ~ aElementOf0(sdtasdt0(xc,sK1),slsdtgt0(sdtasdt0(xc,sK1)))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(paramod,[status(thm)],[c_133,c_2984]) ).
cnf(c_336,negated_conjecture,
( ~ aElementOf0(sdtasdt0(xc,sK0),slsdtgt0(sdtasdt0(xc,sK0)))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK0)))
| ~ aElementOf0(sdtasdt0(xc,sK1),slsdtgt0(sdtasdt0(xc,sK1)))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(paramod,[status(thm)],[c_133,c_2985]) ).
cnf(c_739,plain,
sdtasdt0(sdtasdt0(xc,sK1),sz00) = sz00,
inference(resolve,[status(thm)],[c_206,c_146]) ).
cnf(c_740,plain,
sdtasdt0(sdtasdt0(xc,sK0),sz00) = sz00,
inference(resolve,[status(thm)],[c_206,c_144]) ).
cnf(c_1141,plain,
sdtasdt0(sdtasdt0(xc,sK1),sz10) = sdtasdt0(xc,sK1),
inference(resolve,[status(thm)],[c_214,c_146]) ).
cnf(c_1142,plain,
sdtasdt0(sdtasdt0(xc,sK0),sz10) = sdtasdt0(xc,sK0),
inference(resolve,[status(thm)],[c_214,c_144]) ).
cnf(c_2986,plain,
( sdtasdt0(sdtasdt0(xc,sK1),C) != B
| ~ aElement0(C)
| aElementOf0(B,A)
| slsdtgt0(sdtasdt0(xc,sK1)) != A ),
inference(resolve,[status(thm)],[c_152,c_146]) ).
cnf(c_2987,plain,
( sdtasdt0(sdtasdt0(xc,sK1),B) != A
| ~ aElement0(B)
| aElementOf0(A,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(xxres,[status(thm)],[c_2986]) ).
cnf(c_2988,plain,
( sdtasdt0(sdtasdt0(xc,sK1),sz10) != A
| aElementOf0(A,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(resolve,[status(thm)],[c_2987,c_226]) ).
cnf(c_2989,plain,
aElementOf0(sdtasdt0(sdtasdt0(xc,sK1),sz10),slsdtgt0(sdtasdt0(xc,sK1))),
inference(xxres,[status(thm)],[c_2988]) ).
cnf(c_2563,plain,
aElementOf0(sdtasdt0(xc,sK1),slsdtgt0(sdtasdt0(xc,sK1))),
inference(paramod,[status(thm)],[c_1141,c_2989]) ).
cnf(c_2990,plain,
( sdtasdt0(sdtasdt0(xc,sK0),C) != B
| ~ aElement0(C)
| aElementOf0(B,A)
| slsdtgt0(sdtasdt0(xc,sK0)) != A ),
inference(resolve,[status(thm)],[c_152,c_144]) ).
cnf(c_2991,plain,
( sdtasdt0(sdtasdt0(xc,sK0),B) != A
| ~ aElement0(B)
| aElementOf0(A,slsdtgt0(sdtasdt0(xc,sK0))) ),
inference(xxres,[status(thm)],[c_2990]) ).
cnf(c_2992,plain,
( sdtasdt0(sdtasdt0(xc,sK0),sz10) != A
| aElementOf0(A,slsdtgt0(sdtasdt0(xc,sK0))) ),
inference(resolve,[status(thm)],[c_2991,c_226]) ).
cnf(c_2993,plain,
aElementOf0(sdtasdt0(sdtasdt0(xc,sK0),sz10),slsdtgt0(sdtasdt0(xc,sK0))),
inference(xxres,[status(thm)],[c_2992]) ).
cnf(c_2564,plain,
aElementOf0(sdtasdt0(xc,sK0),slsdtgt0(sdtasdt0(xc,sK0))),
inference(paramod,[status(thm)],[c_1142,c_2993]) ).
cnf(c_2994,negated_conjecture,
( ~ aElementOf0(sdtasdt0(xc,sK0),slsdtgt0(sdtasdt0(xc,sK0)))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK0)))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(resolve,[status(thm)],[c_2563,c_336]) ).
cnf(c_2751,negated_conjecture,
( ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK0)))
| ~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(resolve,[status(thm)],[c_2564,c_2994]) ).
cnf(c_2995,plain,
( sdtasdt0(sdtasdt0(xc,sK1),C) != B
| ~ aElement0(C)
| aElementOf0(B,A)
| slsdtgt0(sdtasdt0(xc,sK1)) != A ),
inference(resolve,[status(thm)],[c_152,c_146]) ).
cnf(c_2996,plain,
( sdtasdt0(sdtasdt0(xc,sK1),B) != A
| ~ aElement0(B)
| aElementOf0(A,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(xxres,[status(thm)],[c_2995]) ).
cnf(c_2997,plain,
( sdtasdt0(sdtasdt0(xc,sK1),sz00) != A
| aElementOf0(A,slsdtgt0(sdtasdt0(xc,sK1))) ),
inference(resolve,[status(thm)],[c_2996,c_227]) ).
cnf(c_2998,plain,
aElementOf0(sdtasdt0(sdtasdt0(xc,sK1),sz00),slsdtgt0(sdtasdt0(xc,sK1))),
inference(xxres,[status(thm)],[c_2997]) ).
cnf(c_2957,plain,
aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK1))),
inference(paramod,[status(thm)],[c_739,c_2998]) ).
cnf(c_2999,plain,
( sdtasdt0(sdtasdt0(xc,sK0),C) != B
| ~ aElement0(C)
| aElementOf0(B,A)
| slsdtgt0(sdtasdt0(xc,sK0)) != A ),
inference(resolve,[status(thm)],[c_152,c_144]) ).
cnf(c_3000,plain,
( sdtasdt0(sdtasdt0(xc,sK0),B) != A
| ~ aElement0(B)
| aElementOf0(A,slsdtgt0(sdtasdt0(xc,sK0))) ),
inference(xxres,[status(thm)],[c_2999]) ).
cnf(c_3001,plain,
( sdtasdt0(sdtasdt0(xc,sK0),sz00) != A
| aElementOf0(A,slsdtgt0(sdtasdt0(xc,sK0))) ),
inference(resolve,[status(thm)],[c_3000,c_227]) ).
cnf(c_3002,plain,
aElementOf0(sdtasdt0(sdtasdt0(xc,sK0),sz00),slsdtgt0(sdtasdt0(xc,sK0))),
inference(xxres,[status(thm)],[c_3001]) ).
cnf(c_2958,plain,
aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK0))),
inference(paramod,[status(thm)],[c_740,c_3002]) ).
cnf(c_3003,negated_conjecture,
~ aElementOf0(sz00,slsdtgt0(sdtasdt0(xc,sK0))),
inference(resolve,[status(thm)],[c_2957,c_2751]) ).
cnf(c_2980,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_2958,c_3003]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG108+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n019.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 06:07:18 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.38 % Process 567187 was started by sandbox2 on n019,
% 0.09/0.38 % Sat Sep 26 06:07:18 2026
% 0.09/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.39
% 0.09/0.39 % From the command line: assign(max_seconds, 300).
% 1.64/0.66
% 1.64/0.66 % SZS status Theorem for theBenchmark
% 1.64/0.66
% 1.64/0.66 % Proof 1 at 0.18 (+ 0.06) seconds.
% 1.64/0.66 % Length of proof is 31.
% 1.64/0.66 % Level of proof is 7.
% 1.64/0.66 % Maximum clause weight is 43.000.
% 1.64/0.66 % Given clauses 93.
% 1.64/0.66
% 1.64/0.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------