%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM629+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n003.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:26:18 PM UTC 2026
% Result : Theorem 15.18s 2.83s
% Output : CNFRefutation 15.18s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f275ERROR: Could not build tree for root c_39079ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f82,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( isCountable0(sdtlpdtrp0(xN,X0))
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3671) ).
fof(f111,axiom,
( sdtlpdtrp0(xe,xn) = xp
& aElementOf0(xn,szNzAzT0)
& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)
& aElementOf0(xn,szDzozmdt0(xd)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5309) ).
fof(f113,axiom,
( aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
& ! [X0] :
( aElementOf0(X0,xP)
=> aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5334) ).
fof(f114,axiom,
( xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))
& ! [X0] :
( aElementOf0(X0,xD)
<=> ( X0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& aElementOf0(X0,sdtlpdtrp0(xN,xn))
& aElement0(X0) ) )
& aSet0(xD)
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xn))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5585) ).
fof(f115,conjecture,
( aElementOf0(xP,slbdtsldtrb0(xD,xk))
| aSubsetOf0(xP,xD)
| ! [X0] :
( aElementOf0(X0,xP)
=> aElementOf0(X0,xD) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f116,negated_conjecture,
~ ( aElementOf0(xP,slbdtsldtrb0(xD,xk))
| aSubsetOf0(xP,xD)
| ! [X0] :
( aElementOf0(X0,xP)
=> aElementOf0(X0,xD) ) ),
inference(negated_conjecture,[status(cth)],[f115]) ).
fof(f132,plain,
( xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))
& ! [X1] :
( aElementOf0(X1,xD)
<=> ( szmzizndt0(sdtlpdtrp0(xN,xn)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xn))
& aElement0(X1) ) )
& aSet0(xD)
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xn))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0) ) ),
inference(rectify,[],[f114]) ).
fof(f147,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ( isCountable0(sdtlpdtrp0(xN,X0))
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ! [X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| aElementOf0(X1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,X0)) ) ),
inference(ennf_transformation,[],[f82]) ).
fof(f178,plain,
( aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
& ! [X0] :
( ~ aElementOf0(X0,xP)
| aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) ),
inference(ennf_transformation,[],[f113]) ).
fof(f179,plain,
( xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))
& ! [X1] :
( aElementOf0(X1,xD)
<=> ( szmzizndt0(sdtlpdtrp0(xN,xn)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xn))
& aElement0(X1) ) )
& aSet0(xD)
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xn))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0) ) ),
inference(ennf_transformation,[],[f132]) ).
fof(f180,plain,
( ~ aElementOf0(xP,slbdtsldtrb0(xD,xk))
& ~ aSubsetOf0(xP,xD)
& ? [X0] :
( aElementOf0(X0,xP)
& ~ aElementOf0(X0,xD) ) ),
inference(ennf_transformation,[],[f116]) ).
fof(f317,plain,
! [X0] :
( ~ sP5(X0)
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& sP4(X0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ),
inference(nnf_transformation,[],[f274]) ).
fof(f318,plain,
! [X0] :
( ~ sP5(X0)
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& sP4(X0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ),
inference(rectify,[],[f317]) ).
fof(f322,plain,
( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ( ( aElementOf0(sK35(X0),sdtlpdtrp0(xN,X0))
& ~ aElementOf0(sK35(X0),szNzAzT0) )
| ~ aSet0(sdtlpdtrp0(xN,X0)) ) )
| sP5(X0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(X1,sK35(X0))],[f275]) ).
fof(f393,plain,
( xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))
& ! [X1] :
( ( ~ aElementOf0(X1,xD)
| ( szmzizndt0(sdtlpdtrp0(xN,xn)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xn))
& aElement0(X1) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,xn)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xn))
| ~ aElement0(X1)
| aElementOf0(X1,xD) ) )
& aSet0(xD)
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xn))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0) ) ),
inference(nnf_transformation,[],[f179]) ).
fof(f394,plain,
( xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))
& ! [X1] :
( ( ~ aElementOf0(X1,xD)
| ( szmzizndt0(sdtlpdtrp0(xN,xn)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xn))
& aElement0(X1) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,xn)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xn))
| ~ aElement0(X1)
| aElementOf0(X1,xD) ) )
& aSet0(xD)
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xn))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0) ) ),
inference(flattening,[],[f393]) ).
fof(f395,plain,
( ~ aElementOf0(xP,slbdtsldtrb0(xD,xk))
& ~ aSubsetOf0(xP,xD)
& aElementOf0(sK54,xP)
& ~ aElementOf0(sK54,xD) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(X0,sK54)],[f180]) ).
fof(f498,plain,
! [X2,X0] :
( ~ sP5(X0)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(cnf_transformation,[],[f318]) ).
fof(f508,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| sP5(X0) ),
inference(cnf_transformation,[],[f322]) ).
fof(f509,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| aElementOf0(sK35(X0),sdtlpdtrp0(xN,X0))
| ~ aSet0(sdtlpdtrp0(xN,X0))
| sP5(X0) ),
inference(cnf_transformation,[],[f322]) ).
fof(f514,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| isCountable0(sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f147]) ).
fof(f515,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f723,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f111]) ).
fof(f729,plain,
! [X0] :
( ~ aElementOf0(X0,xP)
| aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
inference(cnf_transformation,[],[f178]) ).
fof(f730,plain,
xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),
inference(cnf_transformation,[],[f394]) ).
fof(f739,plain,
aElementOf0(sK54,xP),
inference(cnf_transformation,[],[f395]) ).
fof(f740,plain,
~ aElementOf0(sK54,xD),
inference(cnf_transformation,[],[f395]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ~ sP5(X1)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(X1))) ),
inference(cnf_transformation,[],[f498]) ).
tcf(c_122,plain,
! [X0: $i] :
( sP5(X0)
| aElementOf0(sK35(X0),sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSet0(sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f509]) ).
tcf(c_123,plain,
! [X0: $i] :
( sP5(X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ),
inference(cnf_transformation,[],[f508]) ).
tcf(c_126,plain,
! [X0: $i] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f515]) ).
tcf(c_127,plain,
! [X0: $i] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f514]) ).
tcf(c_335,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f723]) ).
tcf(c_338,plain,
! [X0: $i] :
( aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ aElementOf0(X0,xP) ),
inference(cnf_transformation,[],[f729]) ).
tcf(c_346,plain,
sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))) = xD,
inference(cnf_transformation,[],[f730]) ).
tcf(c_347,negated_conjecture,
~ aElementOf0(sK54,xD),
inference(cnf_transformation,[],[f740]) ).
tcf(c_348,negated_conjecture,
aElementOf0(sK54,xP),
inference(cnf_transformation,[],[f739]) ).
tcf(c_807,plain,
! [X0: $i] :
( sP5(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_122,c_127,c_126,c_123]) ).
tcf(c_6344,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X1)))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_807,c_111]) ).
tcf(c_6345,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(X1))) ),
inference(unflattening,[status(thm)],[c_6344]) ).
tcf(c_38546,plain,
! [X0: $i] :
( aElementOf0(X0,xD)
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
inference(superposition,[status(thm)],[c_346,c_6345]) ).
tcf(c_38555,plain,
! [X0: $i] :
( aElementOf0(X0,xD)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_38546,c_335]) ).
tcf(c_38781,plain,
! [X0: $i] :
( aElementOf0(X0,xD)
| ~ aElementOf0(X0,xP) ),
inference(superposition,[status(thm)],[c_338,c_38555]) ).
tcf(c_39077,plain,
aElementOf0(sK54,xD),
inference(superposition,[status(thm)],[c_348,c_38781]) ).
tcf(c_39079,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_39077,c_347]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM629+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.36 % Computer : n003.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 05:01:50 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.39 Running first-order theorem proving
% 0.08/0.39 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40
% 0.13/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.40
% 0.13/0.40 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 15.18/2.83 % SZS status Started for theBenchmark.p
% 15.18/2.83 % SZS status Theorem for theBenchmark.p
% 15.18/2.83
% 15.18/2.83 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 15.18/2.83
% 15.18/2.83 % ------ iProver source info
% 15.18/2.83
% 15.18/2.83 % git: date: 2026-07-19 20:42:38 +0200
% 15.18/2.83 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 15.18/2.83 % git: non_committed_changes: false
% 15.18/2.83
% 15.18/2.83 % ------ Parsing...
% 15.18/2.83 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 15.18/2.83
% 15.18/2.83 % ------ Preprocessing... sup_sim: 15 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 4 0s sf_e pe_s pe_e %
% 15.18/2.83
% 15.18/2.83 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 15.18/2.83
% 15.18/2.83 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 15.18/2.83 % ------ Proving...
% 15.18/2.83 % ------ Problem Properties
% 15.18/2.83
% 15.18/2.83 %
% 15.18/2.83 % clauses 372
% 15.18/2.83 % conjectures 4
% 15.18/2.83 % EPR 80
% 15.18/2.83 % Horn 304
% 15.18/2.83 % unary 70
% 15.18/2.83 % binary 103
% 15.18/2.83 % lits 1108
% 15.18/2.83 % lits eq 158
% 15.18/2.83 % fd_pure 0
% 15.18/2.83 % fd_pseudo 0
% 15.18/2.83 % fd_cond 10
% 15.18/2.83 % fd_pseudo_cond 33
% 15.18/2.83 % AC symbols 0
% 15.18/2.83
% 15.18/2.83 % ------ Schedule dynamic 5 is on
% 15.18/2.83
% 15.18/2.83 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 15.18/2.83
% 15.18/2.83
% 15.18/2.83 % ------
% 15.18/2.83 % Current options:
% 15.18/2.83 % ------
% 15.18/2.83
% 15.18/2.83
% 15.18/2.83 %
% 15.18/2.83
% 15.18/2.83 % ------ Proving...
% 15.18/2.83 %
% 15.18/2.83
% 15.18/2.83 % SZS status Theorem for theBenchmark.p
% 15.18/2.83
% 15.18/2.83 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 15.18/2.83
% 15.18/2.83
%------------------------------------------------------------------------------