%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM586+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n008.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:07 PM UTC 2026
% Result : Theorem 4.36s 1.74s
% Output : CNFRefutation 4.36s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f243ERROR: Could not build tree for root c_27408ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f87,axiom,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4200) ).
fof(f88,axiom,
( aElementOf0(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))))
& ? [X0] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),X0) = xx
& aElementOf0(X0,szDzozmdt0(sdtlpdtrp0(xC,xi))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4200_02) ).
fof(f344,plain,
! [X0] :
( ~ sP16(X0)
| ! [X3] :
( ( sbrdtbr0(X3) != xk
| ( ~ aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ( ? [X5] :
( aElementOf0(X5,X3)
& ~ aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| ~ aSet0(X3) ) )
| aElementOf0(X3,szDzozmdt0(sdtlpdtrp0(xC,X0))) )
& ( ~ aElementOf0(X3,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| ( sbrdtbr0(X3) = xk
& aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,X3)
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(X3) ) ) ) ),
inference(nnf_transformation,[],[f243]) ).
fof(f345,plain,
! [X0] :
( ~ sP16(X0)
| ! [X1] :
( ( sbrdtbr0(X1) != xk
| ( ~ aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ( ? [X3] :
( aElementOf0(X3,X1)
& ~ aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| ~ aSet0(X1) ) )
| aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0))) )
& ( ~ aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| ( sbrdtbr0(X1) = xk
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(X1) ) ) ) ),
inference(rectify,[],[f344]) ).
fof(f346,plain,
! [X0] :
( ~ sP16(X0)
| ! [X1] :
( ( sbrdtbr0(X1) != xk
| ( ~ aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ( ( aElementOf0(sK51(X0,X1),X1)
& ~ aElementOf0(sK51(X0,X1),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| ~ aSet0(X1) ) )
| aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0))) )
& ( ~ aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| ( sbrdtbr0(X1) = xk
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(X1) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(X3,sK51(X0,X1))],[f345]) ).
fof(f356,plain,
( aElementOf0(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))))
& xx = sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK53)
& aElementOf0(sK53,szDzozmdt0(sdtlpdtrp0(xC,xi))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53]),skolemize(X0,sK53)],[f88]) ).
fof(f360,plain,
! [X0] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),X0) != xx
| ( ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& sP18
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ~ aElementOf0(X0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))
& ( sbrdtbr0(X0) != xk
| ( ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ( ? [X1] :
( aElementOf0(X1,X0)
& ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
| ~ aSet0(X0) ) ) ) ) ),
inference(rectify,[],[f247]) ).
fof(f361,plain,
! [X0] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),X0) != xx
| ( ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& sP18
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ~ aElementOf0(X0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))
& ( sbrdtbr0(X0) != xk
| ( ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ( ( aElementOf0(sK54(X0),X0)
& ~ aElementOf0(sK54(X0),sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
| ~ aSet0(X0) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(X1,sK54(X0))],[f360]) ).
fof(f622,plain,
! [X0,X1] :
( ~ sP16(X0)
| ~ aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| sbrdtbr0(X1) = xk ),
inference(cnf_transformation,[],[f346]) ).
fof(f623,plain,
! [X0,X1] :
( ~ sP16(X0)
| ~ aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(cnf_transformation,[],[f346]) ).
fof(f647,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sP16(X0) ),
inference(cnf_transformation,[],[f245]) ).
fof(f655,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[],[f87]) ).
fof(f657,plain,
xx = sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK53),
inference(cnf_transformation,[],[f356]) ).
fof(f658,plain,
aElementOf0(sK53,szDzozmdt0(sdtlpdtrp0(xC,xi))),
inference(cnf_transformation,[],[f356]) ).
fof(f668,plain,
! [X0] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),X0) != xx
| sbrdtbr0(X0) != xk
| ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(cnf_transformation,[],[f361]) ).
tcf(c_308,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ~ sP16(X1)
| ~ aElementOf0(X0,szDzozmdt0(sdtlpdtrp0(xC,X1))) ),
inference(cnf_transformation,[],[f623]) ).
tcf(c_309,plain,
! [X0: $i,X1: $i] :
( ( sbrdtbr0(X0) = xk )
| ~ sP16(X1)
| ~ aElementOf0(X0,szDzozmdt0(sdtlpdtrp0(xC,X1))) ),
inference(cnf_transformation,[],[f622]) ).
tcf(c_339,plain,
! [X0: $i] :
( sP16(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f647]) ).
tcf(c_342,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[],[f655]) ).
tcf(c_343,plain,
aElementOf0(sK53,szDzozmdt0(sdtlpdtrp0(xC,xi))),
inference(cnf_transformation,[],[f658]) ).
tcf(c_344,plain,
sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK53) = xx,
inference(cnf_transformation,[],[f657]) ).
tcf(c_352,negated_conjecture,
! [X0: $i] :
( ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( sbrdtbr0(X0) != xk )
| ( sdtlpdtrp0(sdtlpdtrp0(xC,xi),X0) != xx ) ),
inference(cnf_transformation,[],[f668]) ).
tcf(c_5148,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sbrdtbr0(X2) = xk )
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_309,c_339]) ).
tcf(c_5149,plain,
! [X0: $i,X1: $i] :
( ( sbrdtbr0(X0) = xk )
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szDzozmdt0(sdtlpdtrp0(xC,X1))) ),
inference(unflattening,[status(thm)],[c_5148]) ).
tcf(c_5160,plain,
! [X0: $i,X1: $i,X2: $i] :
( aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_308,c_339]) ).
tcf(c_5161,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szDzozmdt0(sdtlpdtrp0(xC,X1))) ),
inference(unflattening,[status(thm)],[c_5160]) ).
tcf(c_21686,definition,
iPr_def_12 = sdtlpdtrp0(xC,xi),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_21687,definition,
iPr_def_13 = sdtlpdtrp0(xN,xi),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_21688,definition,
iPr_def_14 = szmzizndt0(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_21689,definition,
iPr_def_15 = sdtmndt0(iPr_def_13,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_21698,negated_conjecture,
! [X0: $i] :
( ~ aSubsetOf0(X0,iPr_def_15)
| ( sbrdtbr0(X0) != xk )
| ( sdtlpdtrp0(iPr_def_12,X0) != xx ) ),
inference(demodulation,[status(thm)],[c_352]) ).
tcf(c_26001,plain,
aElementOf0(sK53,szDzozmdt0(iPr_def_12)),
inference(light_normalisation,[status(thm)],[c_343,c_21686]) ).
tcf(c_26166,plain,
sdtlpdtrp0(iPr_def_12,sK53) = xx,
inference(light_normalisation,[status(thm)],[c_344,c_21686]) ).
tcf(c_26169,plain,
( ~ aSubsetOf0(sK53,iPr_def_15)
| ( sbrdtbr0(sK53) != xk ) ),
inference(superposition,[status(thm)],[c_26166,c_21698]) ).
tcf(c_26483,plain,
! [X0: $i] :
( ( sbrdtbr0(X0) = xk )
| ~ aElementOf0(xi,szNzAzT0)
| ~ aElementOf0(X0,szDzozmdt0(iPr_def_12)) ),
inference(superposition,[status(thm)],[c_21686,c_5149]) ).
tcf(c_26484,plain,
! [X0: $i] :
( ( sbrdtbr0(X0) = xk )
| ~ aElementOf0(X0,szDzozmdt0(iPr_def_12)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_26483,c_342]) ).
tcf(c_26632,plain,
! [X0: $i] :
( aSubsetOf0(X0,sdtmndt0(iPr_def_13,szmzizndt0(iPr_def_13)))
| ~ aElementOf0(xi,szNzAzT0)
| ~ aElementOf0(X0,szDzozmdt0(sdtlpdtrp0(xC,xi))) ),
inference(superposition,[status(thm)],[c_21687,c_5161]) ).
tcf(c_26634,plain,
! [X0: $i] :
( aSubsetOf0(X0,iPr_def_15)
| ~ aElementOf0(xi,szNzAzT0)
| ~ aElementOf0(X0,szDzozmdt0(iPr_def_12)) ),
inference(light_normalisation,[status(thm)],[c_26632,c_21686,c_21688,c_21689]) ).
tcf(c_26635,plain,
! [X0: $i] :
( aSubsetOf0(X0,iPr_def_15)
| ~ aElementOf0(X0,szDzozmdt0(iPr_def_12)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_26634,c_342]) ).
tcf(c_26749,plain,
aSubsetOf0(sK53,iPr_def_15),
inference(superposition,[status(thm)],[c_26001,c_26635]) ).
tcf(c_26753,plain,
sbrdtbr0(sK53) != xk,
inference(backward_subsumption_resolution,[status(thm)],[c_26169,c_26749]) ).
tcf(c_27407,plain,
sbrdtbr0(sK53) = xk,
inference(superposition,[status(thm)],[c_26001,c_26484]) ).
tcf(c_27408,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_27407,c_26753]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM586+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n008.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 04:47:24 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.41
% 0.14/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.41
% 0.14/0.41 % Detected problem language: tptp
% 0.14/0.43 % Proving...
% 4.36/1.74 % SZS status Started for theBenchmark.p
% 4.36/1.74 % SZS status Theorem for theBenchmark.p
% 4.36/1.74
% 4.36/1.74 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.36/1.74
% 4.36/1.74 % ------ iProver source info
% 4.36/1.74
% 4.36/1.74 % git: date: 2026-07-19 20:42:38 +0200
% 4.36/1.74 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.36/1.74 % git: non_committed_changes: false
% 4.36/1.74
% 4.36/1.74 % ------ Parsing...
% 4.36/1.74 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.36/1.74
% 4.36/1.74 % ------ Preprocessing... sup_sim: 1 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: 2 0s sf_e pe_s pe_e %
% 4.36/1.74
% 4.36/1.74 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 4.36/1.74
% 4.36/1.74 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 4.36/1.74 % ------ Proving...
% 4.36/1.74 % ------ Problem Properties
% 4.36/1.74
% 4.36/1.74 %
% 4.36/1.74 % clauses 292
% 4.36/1.74 % conjectures 10
% 4.36/1.74 % EPR 50
% 4.36/1.74 % Horn 225
% 4.36/1.74 % unary 36
% 4.36/1.74 % binary 65
% 4.36/1.74 % lits 963
% 4.36/1.74 % lits eq 143
% 4.36/1.74 % fd_pure 0
% 4.36/1.74 % fd_pseudo 0
% 4.36/1.74 % fd_cond 11
% 4.36/1.74 % fd_pseudo_cond 37
% 4.36/1.74 % AC symbols 0
% 4.36/1.74
% 4.36/1.74 % ------ Schedule dynamic 5 is on
% 4.36/1.74
% 4.36/1.74 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 4.36/1.74
% 4.36/1.74
% 4.36/1.74 % ------
% 4.36/1.74 % Current options:
% 4.36/1.74 % ------
% 4.36/1.74
% 4.36/1.74
% 4.36/1.74 %
% 4.36/1.74
% 4.36/1.74 % ------ Proving...
% 4.36/1.74 %
% 4.36/1.74
% 4.36/1.74 % SZS status Theorem for theBenchmark.p
% 4.36/1.74
% 4.36/1.74 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.36/1.74
% 4.36/1.74
%------------------------------------------------------------------------------