%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM588+3 : 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 : n004.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:17:29 AM UTC 2026
% Result : Theorem 41.44s 6.59s
% Output : CNFRefutation 41.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 1
% Syntax : Number of formulae : 12 ( 5 unt; 0 def)
% Number of atoms : 195 ( 21 equ)
% Maximal formula atoms : 42 ( 16 avg)
% Number of connectives : 240 ( 57 ~; 46 |; 113 &)
% ( 4 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 10 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 50 ( 0 sgn 44 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__,conjecture,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( ( isCountable0(W1)
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(W1)
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
=> ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xk))
& sbrdtbr0(W2) = xk
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W2)
=> aElementOf0(W3,W1) )
& aSet0(W2) )
=> ( ( ! [W3] :
( aElementOf0(W3,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
=> ( ( ! [W3] :
( aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W3 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W3,sdtlpdtrp0(xN,W0))
& aElement0(W3) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
=> ( aElementOf0(W2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
| aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ! [W3] :
( aElementOf0(W3,W2)
=> aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) ) ) ) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( ( isCountable0(W1)
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(W1)
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
=> ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xk))
& sbrdtbr0(W2) = xk
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W2)
=> aElementOf0(W3,W1) )
& aSet0(W2) )
=> ( ( ! [W3] :
( aElementOf0(W3,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
=> ( ( ! [W3] :
( aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W3 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W3,sdtlpdtrp0(xN,W0))
& aElement0(W3) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
=> ( aElementOf0(W2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
| aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ! [W3] :
( aElementOf0(W3,W2)
=> aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(nnf_82,plain,
? [W0] :
( ? [W1] :
( ? [W2] :
( ~ aElementOf0(W2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
& ~ aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ? [W3] :
( ~ aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(W3,W2) )
& ! [X5] :
( ( szmzizndt0(sdtlpdtrp0(xN,W0)) = X5
| ~ aElementOf0(X5,sdtlpdtrp0(xN,W0))
| ~ aElement0(X5)
| aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,W0)) != X5
& aElementOf0(X5,sdtlpdtrp0(xN,W0))
& aElement0(X5) )
| ~ aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [X4] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),X4)
| ~ aElementOf0(X4,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))
& aElementOf0(W2,slbdtsldtrb0(W1,xk))
& sbrdtbr0(W2) = xk
& aSubsetOf0(W2,W1)
& ! [X3] :
( aElementOf0(X3,W1)
| ~ aElementOf0(X3,W2) )
& aSet0(W2) )
& isCountable0(W1)
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(X2,W1) )
& aSet0(W1)
& ! [X1] :
( ( szmzizndt0(sdtlpdtrp0(xN,W0)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,W0))
| ~ aElement0(X1)
| aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,W0)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,W0))
& aElement0(X1) )
| ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [X0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),X0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
& aElementOf0(W0,szNzAzT0) ),
inference(fof_nnf,[status(thm)],[m___neg]) ).
fof(sk_m___neg_sk,plain,
( ~ aElementOf0(sK2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))),xk))
& ~ aSubsetOf0(sK2,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
& ~ aElementOf0(sK3,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
& aElementOf0(sK3,sK2)
& ! [X5] :
( ( szmzizndt0(sdtlpdtrp0(xN,sK1)) = X5
| ~ aElementOf0(X5,sdtlpdtrp0(xN,sK1))
| ~ aElement0(X5)
| aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,sK1)) != X5
& aElementOf0(X5,sdtlpdtrp0(xN,sK1))
& aElement0(X5) )
| ~ aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
& ! [X4] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,sK1)),X4)
| ~ aElementOf0(X4,sdtlpdtrp0(xN,sK1)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK1)),sdtlpdtrp0(xN,sK1))
& aElementOf0(sK2,slbdtsldtrb0(sK0,xk))
& sbrdtbr0(sK2) = xk
& aSubsetOf0(sK2,sK0)
& ! [X3] :
( aElementOf0(X3,sK0)
| ~ aElementOf0(X3,sK2) )
& aSet0(sK2)
& isCountable0(sK0)
& aSubsetOf0(sK0,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
| ~ aElementOf0(X2,sK0) )
& aSet0(sK0)
& ! [X1] :
( ( szmzizndt0(sdtlpdtrp0(xN,sK1)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,sK1))
| ~ aElement0(X1)
| aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,sK1)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,sK1))
& aElement0(X1) )
| ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
& ! [X0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,sK1)),X0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,sK1)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK1)),sdtlpdtrp0(xN,sK1))
& aElementOf0(sK1,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0,sK2,sK3]),skolemize(W0,sK1),skolemize(W1,sK0),skolemize(W2,sK2),skolemize(W3,sK3)],[nnf_82]) ).
fof(sk_m___neg,plain,
( ~ aElementOf0(sK2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))),xk))
& ~ aSubsetOf0(sK2,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
& ~ aElementOf0(sK3,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
& aElementOf0(sK3,sK2)
& ! [VAR_0] :
( szmzizndt0(sdtlpdtrp0(xN,sK1)) = VAR_0
| ~ aElementOf0(VAR_0,sdtlpdtrp0(xN,sK1))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) )
& ! [VAR_0] :
( szmzizndt0(sdtlpdtrp0(xN,sK1)) != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) )
& ! [VAR_0] :
( aElementOf0(VAR_0,sdtlpdtrp0(xN,sK1))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) )
& ! [VAR_0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,sK1)),VAR_0)
| ~ aElementOf0(VAR_0,sdtlpdtrp0(xN,sK1)) )
& aElementOf0(sK2,slbdtsldtrb0(sK0,xk))
& sbrdtbr0(sK2) = xk
& aSubsetOf0(sK2,sK0)
& ! [VAR_0] :
( aElementOf0(VAR_0,sK0)
| ~ aElementOf0(VAR_0,sK2) )
& aSet0(sK2)
& isCountable0(sK0)
& aSubsetOf0(sK0,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
& ! [VAR_0] :
( aElementOf0(VAR_0,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
| ~ aElementOf0(VAR_0,sK0) )
& aSet0(sK0)
& ! [VAR_0] :
( szmzizndt0(sdtlpdtrp0(xN,sK1)) = VAR_0
| ~ aElementOf0(VAR_0,sdtlpdtrp0(xN,sK1))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) )
& ! [VAR_0] :
( szmzizndt0(sdtlpdtrp0(xN,sK1)) != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) )
& ! [VAR_0] :
( aElementOf0(VAR_0,sdtlpdtrp0(xN,sK1))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
& ! [VAR_0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,sK1)),VAR_0)
| ~ aElementOf0(VAR_0,sdtlpdtrp0(xN,sK1)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK1)),sdtlpdtrp0(xN,sK1))
& aElementOf0(sK1,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[sk_m___neg_sk]) ).
cnf(c_854,negated_conjecture,
( aElementOf0(A,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1))))
| ~ aElementOf0(A,sK0) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_858,negated_conjecture,
( aElementOf0(A,sK0)
| ~ aElementOf0(A,sK2) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_862,negated_conjecture,
aElementOf0(sK3,sK2),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_863,negated_conjecture,
~ aElementOf0(sK3,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_6792,plain,
aElementOf0(sK3,sK0),
inference(resolve,[status(thm)],[c_862,c_858]) ).
cnf(c_7073,negated_conjecture,
aElementOf0(sK3,sdtmndt0(sdtlpdtrp0(xN,sK1),szmzizndt0(sdtlpdtrp0(xN,sK1)))),
inference(resolve,[status(thm)],[c_6792,c_854]) ).
cnf(c_7072,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_863,c_7073]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM588+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n004.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sat Sep 26 03:21:06 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.34 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.34 % Process 700121 was started by sandbox2 on n004,
% 0.07/0.34 % Sat Sep 26 03:21:06 2026
% 0.07/0.34 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.21/0.49
% 0.21/0.49 % From the command line: assign(max_seconds, 300).
% 41.44/6.59
% 41.44/6.59 % given #500 (I,wt=41): 891 szDzozmdt0(A) != slbdtsldtrb0(B,C) | -aElementOf0(C,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(A) | -aElementOf0(f26(C,B,A),xT) | -iLess0(C,xK) | aElementOf0(f27(C,B,A),xT). [resolve(83,a,101,e)].
% 41.44/6.59
% 41.44/6.59 % given #1000 (I,wt=64): 1727 -aSet0(f23(A,B,C)) | -aElementOf0(f24(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(f23(A,B,C),szDzozmdt0(C)) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(f26(A,B,C),xT) | -iLess0(A,xK) | isCountable0(f28(A,B,C)). [resolve(276,a,97,e)].
% 41.44/6.59
% 41.44/6.59 % given #1500 (I,wt=81): 2448 -aSet0(f23(A,B,C)) | -aElementOf0(f24(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(D,f23(A,B,C)) | aElementOf0(D,B) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | aElementOf0(f22(A,B),B) | -isCountable0(B) | -aFunction0(C) | -aElementOf0(f26(A,B,C),xT) | -iLess0(A,xK) | -aElementOf0(E,slbdtsldtrb0(f28(A,B,C),A)) | f27(A,B,C) = sdtlpdtrp0(C,E). [copy(2447),flip(n)].
% 41.44/6.59
% 41.44/6.59 % given #2000 (I,wt=74): 3171 -aSet0(f23(A,B,C)) | aElementOf0(f24(A,B,C),f23(A,B,C)) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(D,f23(A,B,C)) | aElementOf0(D,B) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | -aElementOf0(f22(A,B),szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aSubsetOf0(sdtlcdtrc0(C,szDzozmdt0(C)),xT) | -iLess0(A,xK) | aSubsetOf0(f28(A,B,C),B). [resolve(281,a,152,f)].
% 41.44/6.59
% 41.44/6.59 % given #2500 (I,wt=87): 3809 -aSubsetOf0(f23(A,B,C),B) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(f23(A,B,C),szDzozmdt0(C)) | -aElementOf0(A,szNzAzT0) | -aSet0(B) | -aElementOf0(f22(A,B),szNzAzT0) | -isCountable0(B) | -aFunction0(C) | -aSubsetOf0(sdtlcdtrc0(C,szDzozmdt0(C)),xT) | -iLess0(A,xK) | -aSet0(f23(A,B,C)) | aElementOf0(f29(A,B,C,f23(A,B,C)),f23(A,B,C)) | f27(A,B,C) = sdtlpdtrp0(C,f23(A,B,C)). [factor(1237,b,m)].
% 41.44/6.59
% 41.44/6.59 % given #3000 (I,wt=134): 4316 -aSet0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | -aElementOf0(f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))) | sbrdtbr0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) != A | aSubsetOf0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(A,szNzAzT0) | -aSet0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),szNzAzT0) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | sdtlpdtrp0(B,f25(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B))) = f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B) | -iLess0(A,xK) | aSubsetOf0(f28(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))). [factor(2131,b,j)].
% 41.44/6.59
% 41.44/6.59 % given #3500 (I,wt=89): 4837 -aSet0(f23(A,B,C)) | aElementOf0(f24(A,B,C),f23(A,B,C)) | sbrdtbr0(f23(A,B,C)) != A | -aElementOf0(f23(A,B,C),szDzozmdt0(C)) | -aElementOf0(A,szNzAzT0) | -aSubsetOf0(B,szNzAzT0) | -isCountable0(B) | -aFunction0(C) | aElementOf0(f26(A,B,C),sdtlcdtrc0(C,szDzozmdt0(C))) | -iLess0(A,xK) | aElementOf0(f29(A,B,C,f23(A,B,C)),f23(A,B,C)) | f27(A,B,C) = sdtlpdtrp0(C,f23(A,B,C)). [factor(2558,a,k),merge(l)].
% 41.44/6.59
% 41.44/6.59 % given #4000 (I,wt=125): 5355 -aSet0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | aElementOf0(f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | sbrdtbr0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) != A | -aElementOf0(C,f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | aElementOf0(C,sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(A,szNzAzT0) | -aSet0(sdtlcdtrc0(B,szDzozmdt0(B))) | aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),sdtlcdtrc0(B,szDzozmdt0(B))) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | -aElementOf0(D,szDzozmdt0(B)) | f22(A,sdtlcdtrc0(B,szDzozmdt0(B))) != sdtlpdtrp0(B,D) | -iLess0(A,xK) | aElementOf0(f27(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),xT). [factor(3304,h,k),flip(l)].
% 41.44/6.59
% 41.44/6.59 % given #4500 (I,wt=137): 5858 -aSet0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | -aElementOf0(f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B),sdtlcdtrc0(B,szDzozmdt0(B))) | sbrdtbr0(f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) != A | -aElementOf0(C,f23(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)) | aElementOf0(C,sdtlcdtrc0(B,szDzozmdt0(B))) | -aElementOf0(A,szNzAzT0) | -aSet0(sdtlcdtrc0(B,szDzozmdt0(B))) | aElementOf0(f22(A,sdtlcdtrc0(B,szDzozmdt0(B))),sdtlcdtrc0(B,szDzozmdt0(B))) | -isCountable0(sdtlcdtrc0(B,szDzozmdt0(B))) | -aFunction0(B) | sdtlpdtrp0(B,f25(A,sdtlcdtrc0(B,szDzozmdt0(B)),B,f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B))) = f24(A,sdtlcdtrc0(B,szDzozmdt0(B)),B) | -iLess0(A,xK) | -aElementOf0(C,f28(A,sdtlcdtrc0(B,szDzozmdt0(B)),B)). [factor(4765,e,n)].
% 41.44/6.59
% 41.44/6.59 % SZS status Theorem for theBenchmark
% 41.44/6.59
% 41.44/6.59 % Proof 1 at 5.66 (+ 0.28) seconds.
% 41.44/6.59 % Length of proof is 7.
% 41.44/6.59 % Level of proof is 3.
% 41.44/6.59 % Maximum clause weight is 33.000.
% 41.44/6.59 % Given clauses 4814.
% 41.44/6.59
% 41.44/6.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------