%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG114+4 : 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 : n026.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 29.76s 4.29s
% Output : CNFRefutation 29.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 4
% Syntax : Number of formulae : 32 ( 11 unt; 0 def)
% Number of atoms : 249 ( 77 equ)
% Maximal formula atoms : 33 ( 7 avg)
% Number of connectives : 322 ( 105 ~; 87 |; 121 &)
% ( 5 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 10 con; 0-2 aty)
% Number of variables : 109 ( 0 sgn 73 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__2174,axiom,
( 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('theBenchmark.p',m__2174) ).
fof(m__2228,axiom,
? [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('theBenchmark.p',m__2228) ).
fof(m__2273,axiom,
( ! [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('theBenchmark.p',m__2273) ).
fof(m__,conjecture,
? [W0,W1] :
( xu = sdtpldt0(sdtasdt0(xa,W0),sdtasdt0(xb,W1))
& aElement0(W1)
& aElement0(W0) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ? [W0,W1] :
( xu = sdtpldt0(sdtasdt0(xa,W0),sdtasdt0(xb,W1))
& aElement0(W1)
& aElement0(W0) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(nnf_38,plain,
( sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) = xI
& ! [W0] :
( ( ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) )
| aElementOf0(W0,xI) )
& ( ? [X9,X10] :
( sdtpldt0(X9,X10) = W0
& aElementOf0(X10,slsdtgt0(xb))
& aElementOf0(X9,slsdtgt0(xa)) )
| ~ aElementOf0(W0,xI) ) )
& ! [X6] :
( ( ! [X8] :
( sdtasdt0(xb,X8) != X6
| ~ aElement0(X8) )
| aElementOf0(X6,slsdtgt0(xb)) )
& ( ? [X7] :
( sdtasdt0(xb,X7) = X6
& aElement0(X7) )
| ~ aElementOf0(X6,slsdtgt0(xb)) ) )
& ! [X3] :
( ( ! [X5] :
( sdtasdt0(xa,X5) != X3
| ~ aElement0(X5) )
| aElementOf0(X3,slsdtgt0(xa)) )
& ( ? [X4] :
( sdtasdt0(xa,X4) = X3
& aElement0(X4) )
| ~ aElementOf0(X3,slsdtgt0(xa)) ) )
& aIdeal0(xI)
& ! [X0] :
( ( ! [X2] :
( aElementOf0(sdtasdt0(X2,X0),xI)
| ~ aElement0(X2) )
& ! [X1] :
( aElementOf0(sdtpldt0(X0,X1),xI)
| ~ aElementOf0(X1,xI) ) )
| ~ aElementOf0(X0,xI) )
& aSet0(xI) ),
inference(fof_nnf,[status(thm)],[m__2174]) ).
fof(sk_m__2174_sk,plain,
( sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) = xI
& ! [W0] :
( ( ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) )
| aElementOf0(W0,xI) )
& ( ( sdtpldt0(sK5(W0),sK6(W0)) = W0
& aElementOf0(sK6(W0),slsdtgt0(xb))
& aElementOf0(sK5(W0),slsdtgt0(xa)) )
| ~ aElementOf0(W0,xI) ) )
& ! [X6] :
( ( ! [X8] :
( sdtasdt0(xb,X8) != X6
| ~ aElement0(X8) )
| aElementOf0(X6,slsdtgt0(xb)) )
& ( ( sdtasdt0(xb,sK0(X6)) = X6
& aElement0(sK0(X6)) )
| ~ aElementOf0(X6,slsdtgt0(xb)) ) )
& ! [X3] :
( ( ! [X5] :
( sdtasdt0(xa,X5) != X3
| ~ aElement0(X5) )
| aElementOf0(X3,slsdtgt0(xa)) )
& ( ( sdtasdt0(xa,sK4(X3)) = X3
& aElement0(sK4(X3)) )
| ~ aElementOf0(X3,slsdtgt0(xa)) ) )
& aIdeal0(xI)
& ! [X0] :
( ( ! [X2] :
( aElementOf0(sdtasdt0(X2,X0),xI)
| ~ aElement0(X2) )
& ! [X1] :
( aElementOf0(sdtpldt0(X0,X1),xI)
| ~ aElementOf0(X1,xI) ) )
| ~ aElementOf0(X0,xI) )
& aSet0(xI) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK0,sK5,sK6]),skolemize(X4,sK4(X3)),skolemize(X7,sK0(X6)),skolemize(X9,sK5(W0)),skolemize(X10,sK6(W0))],[nnf_38]) ).
fof(sk_m__2174,plain,
( sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) = xI
& ! [VAR_0,VAR_1,VAR_2] :
( sdtpldt0(VAR_1,VAR_2) != VAR_0
| ~ aElementOf0(VAR_2,slsdtgt0(xb))
| ~ aElementOf0(VAR_1,slsdtgt0(xa))
| aElementOf0(VAR_0,xI) )
& ! [VAR_0] :
( sdtpldt0(sK5(VAR_0),sK6(VAR_0)) = VAR_0
| ~ aElementOf0(VAR_0,xI) )
& ! [VAR_0] :
( aElementOf0(sK6(VAR_0),slsdtgt0(xb))
| ~ aElementOf0(VAR_0,xI) )
& ! [VAR_0] :
( aElementOf0(sK5(VAR_0),slsdtgt0(xa))
| ~ aElementOf0(VAR_0,xI) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(xb,VAR_1) != VAR_0
| ~ aElement0(VAR_1)
| aElementOf0(VAR_0,slsdtgt0(xb)) )
& ! [VAR_0] :
( sdtasdt0(xb,sK0(VAR_0)) = VAR_0
| ~ aElementOf0(VAR_0,slsdtgt0(xb)) )
& ! [VAR_0] :
( aElement0(sK0(VAR_0))
| ~ aElementOf0(VAR_0,slsdtgt0(xb)) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(xa,VAR_1) != VAR_0
| ~ aElement0(VAR_1)
| aElementOf0(VAR_0,slsdtgt0(xa)) )
& ! [VAR_0] :
( sdtasdt0(xa,sK4(VAR_0)) = VAR_0
| ~ aElementOf0(VAR_0,slsdtgt0(xa)) )
& ! [VAR_0] :
( aElement0(sK4(VAR_0))
| ~ aElementOf0(VAR_0,slsdtgt0(xa)) )
& aIdeal0(xI)
& ! [VAR_0,VAR_1] :
( aElementOf0(sdtasdt0(VAR_1,VAR_0),xI)
| ~ aElement0(VAR_1)
| ~ aElementOf0(VAR_0,xI) )
& ! [VAR_0,VAR_1] :
( aElementOf0(sdtpldt0(VAR_0,VAR_1),xI)
| ~ aElementOf0(VAR_1,xI)
| ~ aElementOf0(VAR_0,xI) )
& aSet0(xI) ),
inference(cnf_transformation,[status(thm)],[sk_m__2174_sk]) ).
cnf(c_197,plain,
( aElement0(sK0(A))
| ~ aElementOf0(A,slsdtgt0(xb)) ),
inference(split_conjunct,[status(thm)],[sk_m__2174]) ).
cnf(c_198,plain,
( sdtasdt0(xb,sK0(A)) = A
| ~ aElementOf0(A,slsdtgt0(xb)) ),
inference(split_conjunct,[status(thm)],[sk_m__2174]) ).
fof(nnf_40,plain,
? [W0] :
( sz00 != W0
& aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
& ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) )
& ! [X9] :
( ( ! [X10] :
( sdtasdt0(xb,X10) != X9
| ~ aElement0(X10) )
| aElementOf0(X9,slsdtgt0(xb)) )
& ( ? [X6] :
( sdtasdt0(xb,X6) = X9
& aElement0(X6) )
| ~ aElementOf0(X9,slsdtgt0(xb)) ) )
& ! [X8] :
( ( ! [X7] :
( sdtasdt0(xa,X7) != X8
| ~ aElement0(X7) )
| aElementOf0(X8,slsdtgt0(xa)) )
& ( ? [X3] :
( sdtasdt0(xa,X3) = X8
& aElement0(X3) )
| ~ aElementOf0(X8,slsdtgt0(xa)) ) ) ),
inference(fof_nnf,[status(thm)],[m__2228]) ).
fof(sk_m__2228_sk,plain,
( sz00 != sK10
& aElementOf0(sK10,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
& sdtpldt0(sK8,sK9) = sK10
& aElementOf0(sK9,slsdtgt0(xb))
& aElementOf0(sK8,slsdtgt0(xa))
& ! [X9] :
( ( ! [X10] :
( sdtasdt0(xb,X10) != X9
| ~ aElement0(X10) )
| aElementOf0(X9,slsdtgt0(xb)) )
& ( ( sdtasdt0(xb,sK7(X9)) = X9
& aElement0(sK7(X9)) )
| ~ aElementOf0(X9,slsdtgt0(xb)) ) )
& ! [X8] :
( ( ! [X7] :
( sdtasdt0(xa,X7) != X8
| ~ aElement0(X7) )
| aElementOf0(X8,slsdtgt0(xa)) )
& ( ( sdtasdt0(xa,sK1(X8)) = X8
& aElement0(sK1(X8)) )
| ~ aElementOf0(X8,slsdtgt0(xa)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK7,sK8,sK9,sK10]),skolemize(W0,sK10),skolemize(X3,sK1(X8)),skolemize(X6,sK7(X9)),skolemize(W1,sK8),skolemize(W2,sK9)],[nnf_40]) ).
fof(sk_m__2228,plain,
( sz00 != sK10
& aElementOf0(sK10,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
& sdtpldt0(sK8,sK9) = sK10
& aElementOf0(sK9,slsdtgt0(xb))
& aElementOf0(sK8,slsdtgt0(xa))
& ! [VAR_0,VAR_1] :
( sdtasdt0(xb,VAR_1) != VAR_0
| ~ aElement0(VAR_1)
| aElementOf0(VAR_0,slsdtgt0(xb)) )
& ! [VAR_0] :
( sdtasdt0(xb,sK7(VAR_0)) = VAR_0
| ~ aElementOf0(VAR_0,slsdtgt0(xb)) )
& ! [VAR_0] :
( aElement0(sK7(VAR_0))
| ~ aElementOf0(VAR_0,slsdtgt0(xb)) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(xa,VAR_1) != VAR_0
| ~ aElement0(VAR_1)
| aElementOf0(VAR_0,slsdtgt0(xa)) )
& ! [VAR_0] :
( sdtasdt0(xa,sK1(VAR_0)) = VAR_0
| ~ aElementOf0(VAR_0,slsdtgt0(xa)) )
& ! [VAR_0] :
( aElement0(sK1(VAR_0))
| ~ aElementOf0(VAR_0,slsdtgt0(xa)) ) ),
inference(cnf_transformation,[status(thm)],[sk_m__2228_sk]) ).
cnf(c_217,plain,
( aElement0(sK1(A))
| ~ aElementOf0(A,slsdtgt0(xa)) ),
inference(split_conjunct,[status(thm)],[sk_m__2228]) ).
cnf(c_218,plain,
( sdtasdt0(xa,sK1(A)) = A
| ~ aElementOf0(A,slsdtgt0(xa)) ),
inference(split_conjunct,[status(thm)],[sk_m__2228]) ).
fof(nnf_41,plain,
( ! [W0] :
( ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu))
| sz00 = W0
| ( ~ aElementOf0(W0,xI)
& ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) ) ) )
& xu != sz00
& aElementOf0(xu,xI)
& ? [X9,X10] :
( sdtpldt0(X9,X10) = xu
& aElementOf0(X10,slsdtgt0(xb))
& aElementOf0(X9,slsdtgt0(xa)) ) ),
inference(fof_nnf,[status(thm)],[m__2273]) ).
fof(sk_m__2273_sk,plain,
( ! [W0] :
( ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu))
| sz00 = W0
| ( ~ aElementOf0(W0,xI)
& ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) ) ) )
& xu != sz00
& aElementOf0(xu,xI)
& sdtpldt0(sK2,sK3) = xu
& aElementOf0(sK3,slsdtgt0(xb))
& aElementOf0(sK2,slsdtgt0(xa)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X9,sK2),skolemize(X10,sK3)],[nnf_41]) ).
fof(sk_m__2273,plain,
( ! [VAR_0] :
( ~ iLess0(sbrdtbr0(VAR_0),sbrdtbr0(xu))
| sz00 = VAR_0
| ~ aElementOf0(VAR_0,xI) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ iLess0(sbrdtbr0(VAR_2),sbrdtbr0(xu))
| sz00 = VAR_2
| sdtpldt0(VAR_0,VAR_1) != VAR_2
| ~ aElementOf0(VAR_1,slsdtgt0(xb))
| ~ aElementOf0(VAR_0,slsdtgt0(xa)) )
& xu != sz00
& aElementOf0(xu,xI)
& sdtpldt0(sK2,sK3) = xu
& aElementOf0(sK3,slsdtgt0(xb))
& aElementOf0(sK2,slsdtgt0(xa)) ),
inference(cnf_transformation,[status(thm)],[sk_m__2273_sk]) ).
cnf(c_227,plain,
aElementOf0(sK2,slsdtgt0(xa)),
inference(split_conjunct,[status(thm)],[sk_m__2273]) ).
cnf(c_228,plain,
aElementOf0(sK3,slsdtgt0(xb)),
inference(split_conjunct,[status(thm)],[sk_m__2273]) ).
cnf(c_229,plain,
sdtpldt0(sK2,sK3) = xu,
inference(split_conjunct,[status(thm)],[sk_m__2273]) ).
cnf(c_243,negated_conjecture,
( sdtpldt0(sdtasdt0(xa,A),sdtasdt0(xb,B)) != xu
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_1619,plain,
sdtasdt0(xa,sK1(sK2)) = sK2,
inference(resolve,[status(thm)],[c_227,c_218]) ).
cnf(c_1620,plain,
aElement0(sK1(sK2)),
inference(resolve,[status(thm)],[c_227,c_217]) ).
cnf(c_1663,plain,
sdtasdt0(xb,sK0(sK3)) = sK3,
inference(resolve,[status(thm)],[c_228,c_198]) ).
cnf(c_1664,plain,
aElement0(sK0(sK3)),
inference(resolve,[status(thm)],[c_228,c_197]) ).
cnf(c_15848,negated_conjecture,
( sdtpldt0(sdtasdt0(xa,sK1(sK2)),sdtasdt0(xb,A)) != xu
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1620,c_243]) ).
cnf(c_6767,negated_conjecture,
( sdtpldt0(sK2,sdtasdt0(xb,A)) != xu
| ~ aElement0(A) ),
inference(paramod,[status(thm)],[c_1619,c_15848]) ).
cnf(c_15849,plain,
sdtpldt0(sK2,sdtasdt0(xb,sK0(sK3))) != xu,
inference(resolve,[status(thm)],[c_6767,c_1664]) ).
cnf(c_15850,plain,
sdtpldt0(sK2,sK3) != xu,
inference(paramod,[status(thm)],[c_1663,c_15849]) ).
cnf(c_15851,plain,
xu != xu,
inference(paramod,[status(thm)],[c_229,c_15850]) ).
cnf(c_15847,plain,
$false,
inference(copy,[status(thm)],[c_15851]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG114+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n026.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 06:11:24 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 270572 was started by sandbox on n026,
% 0.09/0.36 % Sat Sep 26 06:11:24 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/0.38
% 0.14/0.38 % From the command line: assign(max_seconds, 300).
% 29.76/4.29
% 29.76/4.29 % given #500 (T,wt=4): 1790 aElement0(sdtpldt0(sz10,sz10)). [resolve(259,a,69,a)].
% 29.76/4.29
% 29.76/4.29 % SZS status Theorem for theBenchmark
% 29.76/4.29
% 29.76/4.29 % Proof 1 at 2.77 (+ 0.90) seconds.
% 29.76/4.29 % Length of proof is 18.
% 29.76/4.29 % Level of proof is 4.
% 29.76/4.29 % Maximum clause weight is 13.000.
% 29.76/4.29 % Given clauses 901.
% 29.76/4.29
% 29.76/4.29 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------