%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : RNG121+1 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:05:24 PM UTC 2026
% Result : Theorem 1.63s 1.83s
% Output : CNFRefutation 1.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 8
% Syntax : Number of formulae : 30 ( 9 unt; 0 def)
% Number of atoms : 164 ( 38 equ)
% Maximal formula atoms : 52 ( 5 avg)
% Number of connectives : 224 ( 90 ~; 98 |; 27 &)
% ( 4 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-4 aty)
% Number of variables : 55 ( 0 sgn 30 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mDefSSum,axiom,
! [X1,X2] :
( ( aSet0(X1)
& aSet0(X2) )
=> ! [X3] :
( X3 = sdtpldt1(X1,X2)
<=> ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
<=> ? [X5,X6] :
( aElementOf0(X5,X1)
& aElementOf0(X6,X2)
& sdtpldt0(X5,X6) = X4 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSSum) ).
fof(mAddZero,axiom,
! [X1] :
( aElement0(X1)
=> ( sdtpldt0(X1,sz00) = X1
& X1 = sdtpldt0(sz00,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddZero) ).
fof(mEOfElem,axiom,
! [X1] :
( aSet0(X1)
=> ! [X2] :
( aElementOf0(X2,X1)
=> aElement0(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mEOfElem) ).
fof(mDefPrIdeal,axiom,
! [X1] :
( aElement0(X1)
=> ! [X2] :
( X2 = slsdtgt0(X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ? [X4] :
( aElement0(X4)
& sdtasdt0(X1,X4) = X3 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefPrIdeal) ).
fof(m__2174,hypothesis,
( aIdeal0(xI)
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2174) ).
fof(m__2203,hypothesis,
( aElementOf0(sz00,slsdtgt0(xa))
& aElementOf0(xa,slsdtgt0(xa))
& aElementOf0(sz00,slsdtgt0(xb))
& aElementOf0(xb,slsdtgt0(xb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2203) ).
fof(m__2091,hypothesis,
( aElement0(xa)
& aElement0(xb) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2091) ).
fof(m__,conjecture,
aElementOf0(xb,xI),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(c_0_8,plain,
! [X126,X127,X128,X129,X132,X133,X134,X135,X137,X138] :
( ( aSet0(X128)
| X128 != sdtpldt1(X126,X127)
| ~ aSet0(X126)
| ~ aSet0(X127) )
& ( aElementOf0(esk3_4(X126,X127,X128,X129),X126)
| ~ aElementOf0(X129,X128)
| X128 != sdtpldt1(X126,X127)
| ~ aSet0(X126)
| ~ aSet0(X127) )
& ( aElementOf0(esk4_4(X126,X127,X128,X129),X127)
| ~ aElementOf0(X129,X128)
| X128 != sdtpldt1(X126,X127)
| ~ aSet0(X126)
| ~ aSet0(X127) )
& ( sdtpldt0(esk3_4(X126,X127,X128,X129),esk4_4(X126,X127,X128,X129)) = X129
| ~ aElementOf0(X129,X128)
| X128 != sdtpldt1(X126,X127)
| ~ aSet0(X126)
| ~ aSet0(X127) )
& ( ~ aElementOf0(X133,X126)
| ~ aElementOf0(X134,X127)
| sdtpldt0(X133,X134) != X132
| aElementOf0(X132,X128)
| X128 != sdtpldt1(X126,X127)
| ~ aSet0(X126)
| ~ aSet0(X127) )
& ( ~ aElementOf0(esk5_3(X126,X127,X135),X135)
| ~ aElementOf0(X137,X126)
| ~ aElementOf0(X138,X127)
| sdtpldt0(X137,X138) != esk5_3(X126,X127,X135)
| ~ aSet0(X135)
| X135 = sdtpldt1(X126,X127)
| ~ aSet0(X126)
| ~ aSet0(X127) )
& ( aElementOf0(esk6_3(X126,X127,X135),X126)
| aElementOf0(esk5_3(X126,X127,X135),X135)
| ~ aSet0(X135)
| X135 = sdtpldt1(X126,X127)
| ~ aSet0(X126)
| ~ aSet0(X127) )
& ( aElementOf0(esk7_3(X126,X127,X135),X127)
| aElementOf0(esk5_3(X126,X127,X135),X135)
| ~ aSet0(X135)
| X135 = sdtpldt1(X126,X127)
| ~ aSet0(X126)
| ~ aSet0(X127) )
& ( sdtpldt0(esk6_3(X126,X127,X135),esk7_3(X126,X127,X135)) = esk5_3(X126,X127,X135)
| aElementOf0(esk5_3(X126,X127,X135),X135)
| ~ aSet0(X135)
| X135 = sdtpldt1(X126,X127)
| ~ aSet0(X126)
| ~ aSet0(X127) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefSSum])])])])])]) ).
cnf(c_0_9,plain,
( aElementOf0(X5,X6)
| ~ aElementOf0(X1,X2)
| ~ aElementOf0(X3,X4)
| sdtpldt0(X1,X3) != X5
| X6 != sdtpldt1(X2,X4)
| ~ aSet0(X2)
| ~ aSet0(X4) ),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
fof(c_0_10,plain,
! [X105] :
( ( sdtpldt0(X105,sz00) = X105
| ~ aElement0(X105) )
& ( X105 = sdtpldt0(sz00,X105)
| ~ aElement0(X105) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mAddZero])])]) ).
fof(c_0_11,plain,
! [X120,X121] :
( ~ aSet0(X120)
| ~ aElementOf0(X121,X120)
| aElement0(X121) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEOfElem])])]) ).
cnf(c_0_12,plain,
( aElementOf0(sdtpldt0(X1,X2),sdtpldt1(X3,X4))
| ~ aElementOf0(X2,X4)
| ~ aElementOf0(X1,X3)
| ~ aSet0(X4)
| ~ aSet0(X3) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_9])]) ).
cnf(c_0_13,plain,
( X1 = sdtpldt0(sz00,X1)
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_14,plain,
( aElement0(X2)
| ~ aSet0(X1)
| ~ aElementOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
fof(c_0_15,plain,
! [X188,X189,X190,X192,X193,X194,X196] :
( ( aSet0(X189)
| X189 != slsdtgt0(X188)
| ~ aElement0(X188) )
& ( aElement0(esk18_3(X188,X189,X190))
| ~ aElementOf0(X190,X189)
| X189 != slsdtgt0(X188)
| ~ aElement0(X188) )
& ( sdtasdt0(X188,esk18_3(X188,X189,X190)) = X190
| ~ aElementOf0(X190,X189)
| X189 != slsdtgt0(X188)
| ~ aElement0(X188) )
& ( ~ aElement0(X193)
| sdtasdt0(X188,X193) != X192
| aElementOf0(X192,X189)
| X189 != slsdtgt0(X188)
| ~ aElement0(X188) )
& ( ~ aElementOf0(esk19_2(X188,X194),X194)
| ~ aElement0(X196)
| sdtasdt0(X188,X196) != esk19_2(X188,X194)
| ~ aSet0(X194)
| X194 = slsdtgt0(X188)
| ~ aElement0(X188) )
& ( aElement0(esk20_2(X188,X194))
| aElementOf0(esk19_2(X188,X194),X194)
| ~ aSet0(X194)
| X194 = slsdtgt0(X188)
| ~ aElement0(X188) )
& ( sdtasdt0(X188,esk20_2(X188,X194)) = esk19_2(X188,X194)
| aElementOf0(esk19_2(X188,X194),X194)
| ~ aSet0(X194)
| X194 = slsdtgt0(X188)
| ~ aElement0(X188) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[mDefPrIdeal])])])])])]) ).
cnf(c_0_16,plain,
( aElementOf0(X1,sdtpldt1(X2,X3))
| ~ aElementOf0(sz00,X2)
| ~ aElementOf0(X1,X3)
| ~ aSet0(X3)
| ~ aSet0(X2) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_12,c_0_13]),c_0_14]) ).
cnf(c_0_17,hypothesis,
xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)),
inference(split_conjunct,[status(thm)],[m__2174]) ).
cnf(c_0_18,hypothesis,
aElementOf0(sz00,slsdtgt0(xa)),
inference(split_conjunct,[status(thm)],[m__2203]) ).
cnf(c_0_19,plain,
( aSet0(X1)
| X1 != slsdtgt0(X2)
| ~ aElement0(X2) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_20,hypothesis,
( aElementOf0(X1,xI)
| ~ aElementOf0(X1,slsdtgt0(xb))
| ~ aSet0(slsdtgt0(xb))
| ~ aSet0(slsdtgt0(xa)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16,c_0_17]),c_0_18])]) ).
cnf(c_0_21,plain,
( aSet0(slsdtgt0(X1))
| ~ aElement0(X1) ),
inference(er,[status(thm)],[c_0_19]) ).
cnf(c_0_22,hypothesis,
aElement0(xb),
inference(split_conjunct,[status(thm)],[m__2091]) ).
cnf(c_0_23,hypothesis,
( aElementOf0(X1,xI)
| ~ aElementOf0(X1,slsdtgt0(xb))
| ~ aSet0(slsdtgt0(xa)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20,c_0_21]),c_0_22])]) ).
cnf(c_0_24,hypothesis,
aElement0(xa),
inference(split_conjunct,[status(thm)],[m__2091]) ).
fof(c_0_25,negated_conjecture,
~ aElementOf0(xb,xI),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[m__])]) ).
cnf(c_0_26,hypothesis,
( aElementOf0(X1,xI)
| ~ aElementOf0(X1,slsdtgt0(xb)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23,c_0_21]),c_0_24])]) ).
cnf(c_0_27,hypothesis,
aElementOf0(xb,slsdtgt0(xb)),
inference(split_conjunct,[status(thm)],[m__2203]) ).
cnf(c_0_28,negated_conjecture,
~ aElementOf0(xb,xI),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_29,hypothesis,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_26,c_0_27]),c_0_28]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : RNG121+1 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n009.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 01:51:11 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.33 % start to proof: theBenchmark
% 1.63/1.83 % Version : CSE_E---1.7
% 1.63/1.83 % Problem : theBenchmark.p
% 1.63/1.83 % SZS status Theorem for theBenchmark.p
% 1.63/1.83 % SZS output start CNFRefutation
% See solution above
% 1.63/1.84 % Total time : 1.371s
%------------------------------------------------------------------------------