%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM633+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.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:20:35 PM UTC 2026
% Result : Theorem 29.70s 4.86s
% Output : Proof 29.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 5
% Syntax : Number of formulae : 46 ( 10 unt; 0 def)
% Number of atoms : 275 ( 49 equ)
% Maximal formula atoms : 32 ( 5 avg)
% Number of connectives : 328 ( 99 ~; 92 |; 115 &)
% ( 3 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 9 con; 0-2 aty)
% Number of variables : 65 ( 0 sgn 39 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f97,hypothesis,
( aSubsetOf0(xO,xS)
& ! [W0] :
( aElementOf0(W0,xO)
=> aElementOf0(W0,xS) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4998) ).
fof(f97_nnf,plain,
( aSubsetOf0(xO,xS)
& ! [W0] :
( aElementOf0(W0,xS)
| ~ aElementOf0(W0,xO) ) ),
inference(nnf_transformation,[status(thm)],[f97]) ).
fof(f97_sk,plain,
! [W0] :
( aSubsetOf0(xO,xS)
& ( aElementOf0(W0,xS)
| ~ aElementOf0(W0,xO) ) ),
inference(skolemisation,[status(esa)],[f97_nnf]) ).
cnf(c1052,plain,
( aElementOf0(X0,xS)
| ~ aElementOf0(X0,xO) ),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
fof(f93,hypothesis,
( ! [W0] :
( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
<=> ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) ) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(szDzizrdt0(xd),xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4854) ).
fof(f93_nnf,plain,
( ! [W0] :
( ( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(szDzizrdt0(xd),xT) ),
inference(nnf_transformation,[status(thm)],[f93]) ).
fof(f93_sk,plain,
! [W0] :
( ( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(szDzizrdt0(xd),xT) ),
inference(skolemisation,[status(esa)],[f93_nnf]) ).
cnf(c1028,plain,
aElementOf0(szDzizrdt0(xd),xT),
inference(cnf_transformation,[status(esa)],[f93_sk]) ).
fof(f98,conjecture,
( ! [W0] :
( ( aElementOf0(W0,slbdtsldtrb0(xO,xK))
| ( sbrdtbr0(W0) = xK
& ( aSubsetOf0(W0,xO)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xO) )
& aSet0(W0) ) ) ) )
=> ( sdtlpdtrp0(xc,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xc))
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSubsetOf0(W0,szNzAzT0)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,szNzAzT0) )
& ~ ( W0 = slcrc0
| ~ ? [W1] : aElementOf0(W1,W0) ) ) )
=> ? [W0] :
( ? [W1] :
( ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xK))
& sbrdtbr0(W2) = xK
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W2)
=> aElementOf0(W3,W1) )
& aSet0(W2) )
=> sdtlpdtrp0(xc,W2) = W0 )
& isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,xS) )
& aSet0(W1) ) ) )
& aElementOf0(W0,xT) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f98_neg,negated_conjecture,
~ ( ! [W0] :
( ( aElementOf0(W0,slbdtsldtrb0(xO,xK))
| ( sbrdtbr0(W0) = xK
& ( aSubsetOf0(W0,xO)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xO) )
& aSet0(W0) ) ) ) )
=> ( sdtlpdtrp0(xc,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xc))
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSubsetOf0(W0,szNzAzT0)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,szNzAzT0) )
& ~ ( W0 = slcrc0
| ~ ? [W1] : aElementOf0(W1,W0) ) ) )
=> ? [W0] :
( ? [W1] :
( ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xK))
& sbrdtbr0(W2) = xK
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W2)
=> aElementOf0(W3,W1) )
& aSet0(W2) )
=> sdtlpdtrp0(xc,W2) = W0 )
& isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,xS) )
& aSet0(W1) ) ) )
& aElementOf0(W0,xT) ) ),
inference(negated_conjecture,[status(cth)],[f98]) ).
fof(f98_nnf,plain,
( ! [W0] :
( ! [W1] :
( ? [W2] :
( sdtlpdtrp0(xc,W2) != W0
& aElementOf0(W2,slbdtsldtrb0(W1,xK))
& sbrdtbr0(W2) = xK
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W1)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) ) )
| ~ aElementOf0(W0,xT) )
& ! [W0] :
( ( sdtlpdtrp0(xc,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xc))
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSubsetOf0(W0,szNzAzT0)
& ! [W1] :
( aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W1,W0) )
& W0 != slcrc0
& ? [W1] : aElementOf0(W1,W0) )
| ( ~ aElementOf0(W0,slbdtsldtrb0(xO,xK))
& ( sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xO)
& ( ? [W1] :
( ~ aElementOf0(W1,xO)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) ) ) ) ),
inference(nnf_transformation,[status(thm)],[f98_neg]) ).
fof(f98_sk,plain,
! [W0,W1,W3] :
( ( ( sdtlpdtrp0(xc,sk49(W0,W1)) != W0
& aElementOf0(sk49(W0,W1),slbdtsldtrb0(W1,xK))
& sbrdtbr0(sk49(W0,W1)) = xK
& aSubsetOf0(sk49(W0,W1),W1)
& ( aElementOf0(W3,W1)
| ~ aElementOf0(W3,sk49(W0,W1)) )
& aSet0(sk49(W0,W1)) )
| ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ( ~ aElementOf0(sk48(W0,W1),xS)
& aElementOf0(sk48(W0,W1),W1) )
| ~ aSet0(W1) ) )
| ~ aElementOf0(W0,xT) )
& ( ( sdtlpdtrp0(xc,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xc))
& aSubsetOf0(W0,xS)
& ( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSubsetOf0(W0,xS)
& ( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSubsetOf0(W0,szNzAzT0)
& ( aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W1,W0) )
& W0 != slcrc0
& aElementOf0(sk47(W0),W0) )
| ( ~ aElementOf0(W0,slbdtsldtrb0(xO,xK))
& ( sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xO)
& ( ( ~ aElementOf0(sk46(W0),xO)
& aElementOf0(sk46(W0),W0) )
| ~ aSet0(W0) ) ) ) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk46,sk47,sk48,sk49])],[f98_nnf]) ).
cnf(c1099,plain,
( sdtlpdtrp0(xc,sk49(X0,X1)) != X0
| ~ isCountable0(X1)
| aElementOf0(sk48(X0,X1),X1)
| ~ aSet0(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
cnf(p974,plain,
( sdtlpdtrp0(xc,sk49(szDzizrdt0(xd),X0)) != szDzizrdt0(xd)
| ~ isCountable0(X0)
| aElementOf0(sk48(szDzizrdt0(xd),X0),X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[c1028,c1099]) ).
fof(f94,hypothesis,
( xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [W0] :
( aElementOf0(W0,xO)
<=> ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
& ! [W0] :
( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
<=> ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) ) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSet0(xO) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4891) ).
fof(f94_nnf,plain,
( xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [W0] :
( ( ! [W1] :
( sdtlpdtrp0(xe,W1) != W0
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| aElementOf0(W0,xO) )
& ( ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| ~ aElementOf0(W0,xO) ) )
& ! [W0] :
( ( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSet0(xO) ),
inference(nnf_transformation,[status(thm)],[f94]) ).
fof(f94_sk,plain,
! [W0,W1] :
( xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ( sdtlpdtrp0(xe,W1) != W0
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| aElementOf0(W0,xO) )
& ( ( sdtlpdtrp0(xe,sk44(W0)) = W0
& aElementOf0(sk44(W0),sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| ~ aElementOf0(W0,xO) )
& ( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSet0(xO) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk44])],[f94_nnf]) ).
cnf(c1033,plain,
aSet0(xO),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(p1097,plain,
( sdtlpdtrp0(xc,sk49(szDzizrdt0(xd),xO)) != szDzizrdt0(xd)
| ~ isCountable0(xO)
| aElementOf0(sk48(szDzizrdt0(xd),xO),xO) ),
inference(resolution,[status(thm)],[p974,c1033]) ).
fof(f95,hypothesis,
( isCountable0(xO)
& aSet0(xO) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4908) ).
fof(f95_nnf,plain,
( isCountable0(xO)
& aSet0(xO) ),
inference(nnf_transformation,[status(thm)],[f95]) ).
fof(f95_sk,plain,
( isCountable0(xO)
& aSet0(xO) ),
inference(skolemisation,[status(esa)],[f95_nnf]) ).
cnf(c1043,plain,
isCountable0(xO),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1105,plain,
( sdtlpdtrp0(xc,sk49(szDzizrdt0(xd),xO)) != szDzizrdt0(xd)
| aElementOf0(sk48(szDzizrdt0(xd),xO),xO) ),
inference(resolution,[status(thm)],[p1097,c1043]) ).
cnf(c1098,plain,
( aElementOf0(sk49(X0,X1),slbdtsldtrb0(X1,xK))
| ~ isCountable0(X1)
| aElementOf0(sk48(X0,X1),X1)
| ~ aSet0(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
cnf(p975,plain,
( aElementOf0(sk49(szDzizrdt0(xd),X0),slbdtsldtrb0(X0,xK))
| ~ isCountable0(X0)
| aElementOf0(sk48(szDzizrdt0(xd),X0),X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[c1028,c1098]) ).
cnf(p1082,plain,
( aElementOf0(sk49(szDzizrdt0(xd),xO),slbdtsldtrb0(xO,xK))
| ~ isCountable0(xO)
| aElementOf0(sk48(szDzizrdt0(xd),xO),xO) ),
inference(resolution,[status(thm)],[p975,c1033]) ).
cnf(p1088,plain,
( aElementOf0(sk49(szDzizrdt0(xd),xO),slbdtsldtrb0(xO,xK))
| aElementOf0(sk48(szDzizrdt0(xd),xO),xO) ),
inference(resolution,[status(thm)],[p1082,c1043]) ).
cnf(c1093,plain,
( sdtlpdtrp0(xc,X0) = szDzizrdt0(xd)
| ~ aElementOf0(X0,slbdtsldtrb0(xO,xK)) ),
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
cnf(p1089,plain,
( sdtlpdtrp0(xc,sk49(szDzizrdt0(xd),xO)) = szDzizrdt0(xd)
| aElementOf0(sk48(szDzizrdt0(xd),xO),xO) ),
inference(resolution,[status(thm)],[p1088,c1093]) ).
cnf(p1106,plain,
( aElementOf0(sk48(szDzizrdt0(xd),xO),xO)
| aElementOf0(sk48(szDzizrdt0(xd),xO),xO) ),
inference(resolution,[status(thm)],[p1105,p1089]) ).
cnf(p1107,plain,
aElementOf0(sk48(szDzizrdt0(xd),xO),xO),
inference(factoring,[status(thm)],[p1106]) ).
cnf(p1459,plain,
aElementOf0(sk48(szDzizrdt0(xd),xO),xS),
inference(resolution,[status(thm)],[c1052,p1107]) ).
cnf(c1110,plain,
( aElementOf0(sk49(X0,X1),slbdtsldtrb0(X1,xK))
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,xS)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
cnf(p967,plain,
( aElementOf0(sk49(szDzizrdt0(xd),X0),slbdtsldtrb0(X0,xK))
| ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xS) ),
inference(resolution,[status(thm)],[c1028,c1110]) ).
cnf(c1053,plain,
aSubsetOf0(xO,xS),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
cnf(p1173,plain,
( aElementOf0(sk49(szDzizrdt0(xd),xO),slbdtsldtrb0(xO,xK))
| ~ isCountable0(xO) ),
inference(resolution,[status(thm)],[p967,c1053]) ).
cnf(p1186,plain,
aElementOf0(sk49(szDzizrdt0(xd),xO),slbdtsldtrb0(xO,xK)),
inference(resolution,[status(thm)],[p1173,c1043]) ).
cnf(p1187,plain,
sdtlpdtrp0(xc,sk49(szDzizrdt0(xd),xO)) = szDzizrdt0(xd),
inference(resolution,[status(thm)],[p1186,c1093]) ).
cnf(c1105,plain,
( sdtlpdtrp0(xc,sk49(X0,X1)) != X0
| ~ isCountable0(X1)
| ~ aElementOf0(sk48(X0,X1),xS)
| ~ aSet0(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
cnf(p1067,plain,
( sdtlpdtrp0(xc,sk49(szDzizrdt0(xd),X0)) != szDzizrdt0(xd)
| ~ isCountable0(X0)
| ~ aElementOf0(sk48(szDzizrdt0(xd),X0),xS)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[c1105,c1028]) ).
cnf(p1071,plain,
( sdtlpdtrp0(xc,sk49(szDzizrdt0(xd),xO)) != szDzizrdt0(xd)
| ~ isCountable0(xO)
| ~ aElementOf0(sk48(szDzizrdt0(xd),xO),xS) ),
inference(resolution,[status(thm)],[p1067,c1033]) ).
cnf(p1188,plain,
( szDzizrdt0(xd) != szDzizrdt0(xd)
| ~ isCountable0(xO)
| ~ aElementOf0(sk48(szDzizrdt0(xd),xO),xS) ),
inference(demodulation,[status(thm)],[p1187,p1071]) ).
cnf(p1214,plain,
( ~ isCountable0(xO)
| ~ aElementOf0(sk48(szDzizrdt0(xd),xO),xS) ),
inference(equality_resolution,[status(thm)],[p1188]) ).
cnf(p1460,plain,
~ isCountable0(xO),
inference(resolution,[status(thm)],[p1459,p1214]) ).
cnf(p1462,plain,
$false,
inference(resolution,[status(thm)],[p1460,c1043]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM633+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n014.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 05:01:03 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 29.70/4.86 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.70/4.86 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------