%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG126+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n016.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 : Fri Sep 25 02:37:48 PM UTC 2026
% Result : Theorem 70.76s 9.40s
% Output : Proof 70.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 10
% Syntax : Number of formulae : 82 ( 52 unt; 0 def)
% Number of atoms : 300 ( 125 equ)
% Maximal formula atoms : 28 ( 3 avg)
% Number of connectives : 329 ( 111 ~; 85 |; 113 &)
% ( 9 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 15 con; 0-4 aty)
% Number of variables : 118 ( 2 sgn 58 !; 36 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f41,hypothesis,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& ! [W0] :
( aElementOf0(W0,xI)
<=> ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) ) )
& ! [W0] :
( aElementOf0(W0,slsdtgt0(xb))
<=> ? [W1] :
( sdtasdt0(xb,W1) = W0
& aElement0(W1) ) )
& ! [W0] :
( aElementOf0(W0,slsdtgt0(xa))
<=> ? [W1] :
( sdtasdt0(xa,W1) = W0
& aElement0(W1) ) )
& aIdeal0(xI)
& ! [W0] :
( aElementOf0(W0,xI)
=> ( ! [W1] :
( aElement0(W1)
=> aElementOf0(sdtasdt0(W1,W0),xI) )
& ! [W1] :
( aElementOf0(W1,xI)
=> aElementOf0(sdtpldt0(W0,W1),xI) ) ) )
& aSet0(xI) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2174) ).
fof(f41_nnf,plain,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& ! [W0] :
( ( ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) )
| aElementOf0(W0,xI) )
& ( ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) )
| ~ aElementOf0(W0,xI) ) )
& ! [W0] :
( ( ! [W1] :
( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1) )
| aElementOf0(W0,slsdtgt0(xb)) )
& ( ? [W1] :
( sdtasdt0(xb,W1) = W0
& aElement0(W1) )
| ~ aElementOf0(W0,slsdtgt0(xb)) ) )
& ! [W0] :
( ( ! [W1] :
( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1) )
| aElementOf0(W0,slsdtgt0(xa)) )
& ( ? [W1] :
( sdtasdt0(xa,W1) = W0
& aElement0(W1) )
| ~ aElementOf0(W0,slsdtgt0(xa)) ) )
& aIdeal0(xI)
& ! [W0] :
( ( ! [W1] :
( aElementOf0(sdtasdt0(W1,W0),xI)
| ~ aElement0(W1) )
& ! [W1] :
( aElementOf0(sdtpldt0(W0,W1),xI)
| ~ aElementOf0(W1,xI) ) )
| ~ aElementOf0(W0,xI) )
& aSet0(xI) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [W0,W1,W2] :
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& ( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa))
| aElementOf0(W0,xI) )
& ( ( sdtpldt0(sk25(W0),sk26(W0)) = W0
& aElementOf0(sk26(W0),slsdtgt0(xb))
& aElementOf0(sk25(W0),slsdtgt0(xa)) )
| ~ aElementOf0(W0,xI) )
& ( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1)
| aElementOf0(W0,slsdtgt0(xb)) )
& ( ( sdtasdt0(xb,sk24(W0)) = W0
& aElement0(sk24(W0)) )
| ~ aElementOf0(W0,slsdtgt0(xb)) )
& ( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1)
| aElementOf0(W0,slsdtgt0(xa)) )
& ( ( sdtasdt0(xa,sk23(W0)) = W0
& aElement0(sk23(W0)) )
| ~ aElementOf0(W0,slsdtgt0(xa)) )
& aIdeal0(xI)
& ( ( ( aElementOf0(sdtasdt0(W1,W0),xI)
| ~ aElement0(W1) )
& ( aElementOf0(sdtpldt0(W0,W1),xI)
| ~ aElementOf0(W1,xI) ) )
| ~ aElementOf0(W0,xI) )
& aSet0(xI) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk23,sk24,sk25,sk26])],[f41_nnf]) ).
cnf(c146,plain,
( aElementOf0(sdtasdt0(X1,X0),xI)
| ~ aElement0(X1)
| ~ aElementOf0(X0,xI) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(t161,plain,
ifeq(aElementOf0(X1,xI),true,ifeq(aElement0(X2),true,aElementOf0(sdtasdt0(X2,X1),xI),true),true) = true,
inference(equality_encoding,[status(esa)],[c146]) ).
cnf(t362,plain,
ifeq(aElementOf0(X1,xI),true,ifeq(aElement0(X2),true,aElementOf0(sdtasdt0(X2,X1),xI),true),true) = true,
inference(orient,[status(thm)],[t161]) ).
fof(f10,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulComm) ).
fof(f10_nnf,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c12,plain,
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t170,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,sdtasdt0(X1,X2),sdtasdt0(X2,X1)),sdtasdt0(X2,X1)) = sdtasdt0(X2,X1),
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t314,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,sdtasdt0(X1,X2),sdtasdt0(X2,X1)),sdtasdt0(X2,X1)) = sdtasdt0(X2,X1),
inference(orient,[status(thm)],[t170]) ).
fof(f46,hypothesis,
? [W0] :
( sdtasdt0(xu,W0) = xc
& aElement0(W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2744) ).
fof(f46_nnf,plain,
? [W0] :
( sdtasdt0(xu,W0) = xc
& aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
( sdtasdt0(xu,sk40) = xc
& aElement0(sk40) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk40])],[f46_nnf]) ).
cnf(c198,plain,
sdtasdt0(xu,sk40) = xc,
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(t67,plain,
sdtasdt0(xu,sk40) = xc,
inference(equality_encoding,[status(esa)],[c198]) ).
cnf(t3955,plain,
sdtasdt0(xu,sk40) = xc,
inference(orient,[status(thm)],[t67]) ).
cnf(t3956,plain,
sdtasdt0(sk40,xu) = ifeq(aElement0(xu),true,ifeq(aElement0(sk40),true,xc,sdtasdt0(sk40,xu)),sdtasdt0(sk40,xu)),
inference(cp,[status(thm)],[t314,t3955]) ).
fof(f19,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
fof(f19_nnf,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [W0,W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0)
| ~ aSet0(W0) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c25,plain,
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(hi22,axiom,
ifeq(aSet0(X0),true,ifeq(aElementOf0(X1,X0),true,aElement0(X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(c144,plain,
aSet0(xI),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(hi133,axiom,
aSet0(xI) = true,
inference(equality_encoding,[status(esa)],[c144]) ).
fof(f44,hypothesis,
( ! [W0] :
( ( W0 != sz00
& ( aElementOf0(W0,xI)
| ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) ) ) )
=> ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu)) )
& xu != sz00
& aElementOf0(xu,xI)
& ? [W0,W1] :
( sdtpldt0(W0,W1) = xu
& aElementOf0(W1,slsdtgt0(xb))
& aElementOf0(W0,slsdtgt0(xa)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2273) ).
fof(f44_nnf,plain,
( ! [W0] :
( ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu))
| W0 = sz00
| ( ~ aElementOf0(W0,xI)
& ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) ) ) )
& xu != sz00
& aElementOf0(xu,xI)
& ? [W0,W1] :
( sdtpldt0(W0,W1) = xu
& aElementOf0(W1,slsdtgt0(xb))
& aElementOf0(W0,slsdtgt0(xa)) ) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [W1,W2,W0] :
( ( ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu))
| W0 = sz00
| ( ~ aElementOf0(W0,xI)
& ( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) ) ) )
& xu != sz00
& aElementOf0(xu,xI)
& sdtpldt0(sk36,sk37) = xu
& aElementOf0(sk37,slsdtgt0(xb))
& aElementOf0(sk36,slsdtgt0(xa)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk36,sk37])],[f44_nnf]) ).
cnf(c185,plain,
aElementOf0(xu,xI),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(hi173,axiom,
aElementOf0(xu,xI) = true,
inference(equality_encoding,[status(esa)],[c185]) ).
cnf(t15,plain,
aElement0(xu) = true,
inference(hyper_resolution,[status(thm)],[hi22,hi133,hi173]) ).
cnf(t2572,plain,
aElement0(xu) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t15406,plain,
sdtasdt0(sk40,xu) = ifeq(true,true,ifeq(aElement0(sk40),true,xc,sdtasdt0(sk40,xu)),sdtasdt0(sk40,xu)),
inference(step,[status(thm)],[t3956,t2572]) ).
cnf(t94,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t94]) ).
cnf(t15407,plain,
sdtasdt0(sk40,xu) = ifeq(aElement0(sk40),true,xc,sdtasdt0(sk40,xu)),
inference(step,[status(thm)],[t15406,t256]) ).
cnf(c197,plain,
aElement0(sk40),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(t8,plain,
aElement0(sk40) = true,
inference(equality_encoding,[status(esa)],[c197]) ).
cnf(t1720,plain,
aElement0(sk40) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t15408,plain,
sdtasdt0(sk40,xu) = ifeq(true,true,xc,sdtasdt0(sk40,xu)),
inference(step,[status(thm)],[t15407,t1720]) ).
cnf(t15409,plain,
sdtasdt0(sk40,xu) = xc,
inference(step,[status(thm)],[t15408,t256]) ).
cnf(t10151,plain,
sdtasdt0(sk40,xu) = xc,
inference(orient,[status(thm)],[t15409]) ).
cnf(t10153,plain,
true = ifeq(aElementOf0(xu,xI),true,ifeq(aElement0(sk40),true,aElementOf0(xc,xI),true),true),
inference(cp,[status(thm)],[t362,t10151]) ).
cnf(t25,plain,
aElementOf0(xu,xI) = true,
inference(equality_encoding,[status(esa)],[c185]) ).
cnf(t4430,plain,
aElementOf0(xu,xI) = true,
inference(orient,[status(thm)],[t25]) ).
cnf(t15488,plain,
true = ifeq(true,true,ifeq(aElement0(sk40),true,aElementOf0(xc,xI),true),true),
inference(step,[status(thm)],[t10153,t4430]) ).
cnf(t15489,plain,
true = ifeq(aElement0(sk40),true,aElementOf0(xc,xI),true),
inference(step,[status(thm)],[t15488,t256]) ).
cnf(t15490,plain,
true = ifeq(true,true,aElementOf0(xc,xI),true),
inference(step,[status(thm)],[t15489,t1720]) ).
cnf(t15491,plain,
true = aElementOf0(xc,xI),
inference(step,[status(thm)],[t15490,t256]) ).
fof(f47,conjecture,
( ! [W0] :
( aElementOf0(W0,slsdtgt0(xa))
<=> ? [W1] :
( sdtasdt0(xa,W1) = W0
& aElement0(W1) ) )
=> ( ! [W0] :
( aElementOf0(W0,slsdtgt0(xb))
<=> ? [W1] :
( sdtasdt0(xb,W1) = W0
& aElement0(W1) ) )
=> ( aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
| ? [W0,W1] :
( sdtpldt0(W0,W1) = xc
& aElementOf0(W1,slsdtgt0(xb))
& aElementOf0(W0,slsdtgt0(xa)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f47_neg,negated_conjecture,
~ ( ! [W0] :
( aElementOf0(W0,slsdtgt0(xa))
<=> ? [W1] :
( sdtasdt0(xa,W1) = W0
& aElement0(W1) ) )
=> ( ! [W0] :
( aElementOf0(W0,slsdtgt0(xb))
<=> ? [W1] :
( sdtasdt0(xb,W1) = W0
& aElement0(W1) ) )
=> ( aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
| ? [W0,W1] :
( sdtpldt0(W0,W1) = xc
& aElementOf0(W1,slsdtgt0(xb))
& aElementOf0(W0,slsdtgt0(xa)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f47]) ).
fof(f47_nnf,plain,
( ~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
& ! [W0,W1] :
( sdtpldt0(W0,W1) != xc
| ~ aElementOf0(W1,slsdtgt0(xb))
| ~ aElementOf0(W0,slsdtgt0(xa)) )
& ! [W0] :
( ( ! [W1] :
( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1) )
| aElementOf0(W0,slsdtgt0(xb)) )
& ( ? [W1] :
( sdtasdt0(xb,W1) = W0
& aElement0(W1) )
| ~ aElementOf0(W0,slsdtgt0(xb)) ) )
& ! [W0] :
( ( ! [W1] :
( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1) )
| aElementOf0(W0,slsdtgt0(xa)) )
& ( ? [W1] :
( sdtasdt0(xa,W1) = W0
& aElement0(W1) )
| ~ aElementOf0(W0,slsdtgt0(xa)) ) ) ),
inference(nnf_transformation,[status(thm)],[f47_neg]) ).
fof(f47_sk,plain,
! [W0,W1] :
( ~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
& ( sdtpldt0(W0,W1) != xc
| ~ aElementOf0(W1,slsdtgt0(xb))
| ~ aElementOf0(W0,slsdtgt0(xa)) )
& ( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1)
| aElementOf0(W0,slsdtgt0(xb)) )
& ( ( sdtasdt0(xb,sk42(W0)) = W0
& aElement0(sk42(W0)) )
| ~ aElementOf0(W0,slsdtgt0(xb)) )
& ( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1)
| aElementOf0(W0,slsdtgt0(xa)) )
& ( ( sdtasdt0(xa,sk41(W0)) = W0
& aElement0(sk41(W0)) )
| ~ aElementOf0(W0,slsdtgt0(xa)) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk41,sk42])],[f47_nnf]) ).
cnf(c206,plain,
~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(t104,plain,
aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) = false,
inference(equality_encoding,[status(esa)],[c206]) ).
cnf(t4400,plain,
aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) = false,
inference(orient,[status(thm)],[t104]) ).
cnf(c158,plain,
xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(t99,plain,
sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) = xI,
inference(equality_encoding,[status(esa)],[c158]) ).
cnf(t5282,plain,
sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) = xI,
inference(orient,[status(thm)],[t99]) ).
cnf(t15289,plain,
aElementOf0(xc,xI) = false,
inference(step,[status(thm)],[t4400,t5282]) ).
cnf(t5305,plain,
aElementOf0(xc,xI) = false,
inference(rw,[status(thm)],[t15289]) ).
cnf(t14087,plain,
aElementOf0(xc,xI) = false,
inference(orient,[status(thm)],[t5305]) ).
cnf(t15492,plain,
true = false,
inference(step,[status(thm)],[t15491,t14087]) ).
cnf(t15265,plain,
false = true,
inference(orient,[status(thm)],[t15492]) ).
fof(f17,axiom,
sz10 != sz00,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mUnNeZr) ).
fof(f17_nnf,plain,
sz10 != sz00,
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
sz10 != sz00,
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c23,plain,
sz10 != sz00,
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
fof(f39,hypothesis,
( xb != sz00
| xa != sz00 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2110) ).
fof(f39_nnf,plain,
( xb != sz00
| xa != sz00 ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
( xb != sz00
| xa != sz00 ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c105,plain,
( xb != sz00
| xa != sz00 ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
fof(f43,hypothesis,
? [W0] :
( W0 != sz00
& aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
& ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) )
& ! [W1] :
( aElementOf0(W1,slsdtgt0(xb))
<=> ? [W2] :
( sdtasdt0(xb,W2) = W1
& aElement0(W2) ) )
& ! [W1] :
( aElementOf0(W1,slsdtgt0(xa))
<=> ? [W2] :
( sdtasdt0(xa,W2) = W1
& aElement0(W2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2228) ).
fof(f43_nnf,plain,
? [W0] :
( W0 != sz00
& aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
& ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) )
& ! [W1] :
( ( ! [W2] :
( sdtasdt0(xb,W2) != W1
| ~ aElement0(W2) )
| aElementOf0(W1,slsdtgt0(xb)) )
& ( ? [W2] :
( sdtasdt0(xb,W2) = W1
& aElement0(W2) )
| ~ aElementOf0(W1,slsdtgt0(xb)) ) )
& ! [W1] :
( ( ! [W2] :
( sdtasdt0(xa,W2) != W1
| ~ aElement0(W2) )
| aElementOf0(W1,slsdtgt0(xa)) )
& ( ? [W2] :
( sdtasdt0(xa,W2) = W1
& aElement0(W2) )
| ~ aElementOf0(W1,slsdtgt0(xa)) ) ) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [W1,W2] :
( sk31 != sz00
& aElementOf0(sk31,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
& sdtpldt0(sk34,sk35) = sk31
& aElementOf0(sk35,slsdtgt0(xb))
& aElementOf0(sk34,slsdtgt0(xa))
& ( sdtasdt0(xb,W2) != W1
| ~ aElement0(W2)
| aElementOf0(W1,slsdtgt0(xb)) )
& ( ( sdtasdt0(xb,sk33(W1)) = W1
& aElement0(sk33(W1)) )
| ~ aElementOf0(W1,slsdtgt0(xb)) )
& ( sdtasdt0(xa,W2) != W1
| ~ aElement0(W2)
| aElementOf0(W1,slsdtgt0(xa)) )
& ( ( sdtasdt0(xa,sk32(W1)) = W1
& aElement0(sk32(W1)) )
| ~ aElementOf0(W1,slsdtgt0(xa)) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk31,sk32,sk33,sk34,sk35])],[f43_nnf]) ).
cnf(c181,plain,
sk31 != sz00,
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(c186,plain,
xu != sz00,
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(c205,plain,
( sdtpldt0(X0,X1) != xc
| ~ aElementOf0(X1,slsdtgt0(xb))
| ~ aElementOf0(X0,slsdtgt0(xa)) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c23,c105,c181,c186,c205,c206]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t15265]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG126+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.37 % Computer : n016.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Thu Sep 24 08:27:28 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 70.76/9.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 70.76/9.40 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------