%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU326+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n001.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:56:55 PM UTC 2026
% Result : Theorem 2.20s 1.39s
% Output : CNFRefutation 2.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 10
% Syntax : Number of formulae : 60 ( 20 unt; 3 def)
% Number of atoms : 153 ( 66 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 111 ( 48 ~; 37 |; 20 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 12 ( 10 usr; 4 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 46 ( 0 sgn 43 !; 3 ?; 12 :)
% Comments :
%------------------------------------------------------------------------------
fof(f19,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> element(complements_of_subsets(X0,X1),powerset(powerset(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_setfam_1) ).
fof(f23,axiom,
( v5_membered(empty_set)
& v4_membered(empty_set)
& v3_membered(empty_set)
& v2_membered(empty_set)
& v1_membered(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_membered) ).
fof(f24,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> complements_of_subsets(X0,complements_of_subsets(X0,X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k7_setfam_1) ).
fof(f27,axiom,
! [X0] :
? [X1] :
( empty(X1)
& element(X1,powerset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_subset_1) ).
fof(f29,conjecture,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ( ~ ( X1 = empty_set
& complements_of_subsets(X0,X1) != empty_set )
& ~ ( complements_of_subsets(X0,X1) = empty_set
& X1 != empty_set ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_tops_2) ).
fof(f30,negated_conjecture,
~ ! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ( ~ ( X1 = empty_set
& complements_of_subsets(X0,X1) != empty_set )
& ~ ( complements_of_subsets(X0,X1) = empty_set
& X1 != empty_set ) ) ),
inference(negated_conjecture,[status(cth)],[f29]) ).
fof(f34,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ~ ( complements_of_subsets(X0,X1) = empty_set
& X1 != empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t46_setfam_1) ).
fof(f37,axiom,
! [X0] :
( empty(X0)
=> X0 = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
fof(f68,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| element(complements_of_subsets(X0,X1),powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f19]) ).
fof(f69,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| complements_of_subsets(X0,complements_of_subsets(X0,X1)) = X1 ),
inference(ennf_transformation,[],[f24]) ).
fof(f71,plain,
? [X0,X1] :
( element(X1,powerset(powerset(X0)))
& ( ( X1 = empty_set
& complements_of_subsets(X0,X1) != empty_set )
| ( complements_of_subsets(X0,X1) = empty_set
& X1 != empty_set ) ) ),
inference(ennf_transformation,[],[f30]) ).
fof(f76,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| complements_of_subsets(X0,X1) != empty_set
| empty_set = X1 ),
inference(ennf_transformation,[],[f34]) ).
fof(f77,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| complements_of_subsets(X0,X1) != empty_set
| empty_set = X1 ),
inference(flattening,[],[f76]) ).
fof(f81,plain,
! [X0] :
( ~ empty(X0)
| X0 = empty_set ),
inference(ennf_transformation,[],[f37]) ).
fof(f87,plain,
! [X0] :
( empty(sK3(X0))
& element(sK3(X0),powerset(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X1,sK3(X0))],[f27]) ).
fof(f88,plain,
( element(sK5,powerset(powerset(sK4)))
& ( ( empty_set = sK5
& empty_set != complements_of_subsets(sK4,sK5) )
| ( empty_set = complements_of_subsets(sK4,sK5)
& empty_set != sK5 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X0,sK4),skolemize(X1,sK5)],[f71]) ).
fof(f114,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| element(complements_of_subsets(X0,X1),powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f68]) ).
fof(f122,plain,
empty(empty_set),
inference(cnf_transformation,[],[f23]) ).
fof(f123,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| complements_of_subsets(X0,complements_of_subsets(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f69]) ).
fof(f132,plain,
! [X0] : empty(sK3(X0)),
inference(cnf_transformation,[],[f87]) ).
fof(f133,plain,
! [X0] : element(sK3(X0),powerset(X0)),
inference(cnf_transformation,[],[f87]) ).
fof(f135,plain,
element(sK5,powerset(powerset(sK4))),
inference(cnf_transformation,[],[f88]) ).
fof(f136,plain,
( empty_set = sK5
| empty_set = complements_of_subsets(sK4,sK5) ),
inference(cnf_transformation,[],[f88]) ).
fof(f139,plain,
( empty_set != complements_of_subsets(sK4,sK5)
| empty_set != sK5 ),
inference(cnf_transformation,[],[f88]) ).
fof(f143,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| complements_of_subsets(X0,X1) != empty_set
| empty_set = X1 ),
inference(cnf_transformation,[],[f77]) ).
fof(f146,plain,
! [X0] :
( ~ empty(X0)
| empty_set = X0 ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( element(complements_of_subsets(X1,X0),powerset(powerset(X1)))
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_77,plain,
empty(empty_set),
inference(cnf_transformation,[],[f122]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i] :
( ( complements_of_subsets(X1,complements_of_subsets(X1,X0)) = X0 )
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[],[f123]) ).
tcf(c_92,plain,
! [X0: $i] : element(sK3(X0),powerset(X0)),
inference(cnf_transformation,[],[f133]) ).
tcf(c_93,plain,
! [X0: $i] : empty(sK3(X0)),
inference(cnf_transformation,[],[f132]) ).
tcf(c_95,negated_conjecture,
( ( empty_set != sK5 )
| ( complements_of_subsets(sK4,sK5) != empty_set ) ),
inference(cnf_transformation,[],[f139]) ).
tcf(c_96,negated_conjecture,
( ( empty_set = sK5 )
| ( complements_of_subsets(sK4,sK5) = empty_set ) ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_97,negated_conjecture,
element(sK5,powerset(powerset(sK4))),
inference(cnf_transformation,[],[f135]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i] :
( ( X1 = empty_set )
| ~ element(X1,powerset(powerset(X0)))
| ( complements_of_subsets(X0,X1) != empty_set ) ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_104,plain,
! [X0: $i] :
( ( X0 = empty_set )
| ~ empty(X0) ),
inference(cnf_transformation,[],[f146]) ).
tcf(c_944,definition,
iPr_def_10 = powerset(sK4),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_945,definition,
iPr_def_11 = powerset(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_946,definition,
iPr_def_12 = complements_of_subsets(sK4,sK5),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_947,negated_conjecture,
element(sK5,iPr_def_11),
inference(demodulation,[status(thm)],[c_97,c_944,c_945]) ).
tcf(c_948,negated_conjecture,
( ( iPr_def_12 = empty_set )
| ( empty_set = sK5 ) ),
inference(demodulation,[status(thm)],[c_96,c_946]) ).
tcf(c_949,negated_conjecture,
( ( iPr_def_12 != empty_set )
| ( empty_set != sK5 ) ),
inference(demodulation,[status(thm)],[c_95]) ).
tcf(c_1412,plain,
( ( empty_set = iPr_def_12 )
| ( complements_of_subsets(sK4,empty_set) = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_948,c_946]) ).
tcf(c_1445,plain,
! [X0: $i] : sK3(X0) = empty_set,
inference(superposition,[status(thm)],[c_93,c_104]) ).
tcf(c_1446,plain,
! [X0: $i] : element(empty_set,powerset(X0)),
inference(demodulation,[status(thm)],[c_92,c_1445]) ).
tcf(c_1556,plain,
( ( iPr_def_12 = empty_set )
| ~ empty(iPr_def_12) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_1598,plain,
( element(iPr_def_12,powerset(powerset(sK4)))
| ~ element(sK5,powerset(powerset(sK4))) ),
inference(superposition,[status(thm)],[c_946,c_74]) ).
tcf(c_1605,plain,
( element(iPr_def_12,iPr_def_11)
| ~ element(sK5,iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_1598,c_944,c_945]) ).
tcf(c_1606,plain,
element(iPr_def_12,iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_1605,c_947]) ).
tcf(c_1679,plain,
! [X0: $i] : complements_of_subsets(X0,complements_of_subsets(X0,empty_set)) = empty_set,
inference(superposition,[status(thm)],[c_1446,c_83]) ).
tcf(c_1716,plain,
( ( empty_set = sK5 )
| ~ element(sK5,powerset(powerset(sK4)))
| ( empty_set != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_946,c_101]) ).
tcf(c_1718,plain,
( ( empty_set = sK5 )
| ~ element(sK5,iPr_def_11)
| ( empty_set != iPr_def_12 ) ),
inference(light_normalisation,[status(thm)],[c_1716,c_944,c_945]) ).
tcf(c_1719,plain,
( ( empty_set = sK5 )
| ( empty_set != iPr_def_12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1718,c_947]) ).
tcf(c_1767,plain,
( ( empty_set = iPr_def_12 )
| ( complements_of_subsets(sK4,iPr_def_12) = empty_set ) ),
inference(superposition,[status(thm)],[c_1412,c_1679]) ).
tcf(c_1781,plain,
( ( empty_set = iPr_def_12 )
| ~ element(iPr_def_12,powerset(powerset(sK4))) ),
inference(superposition,[status(thm)],[c_1767,c_101]) ).
tcf(c_1782,plain,
( ( empty_set = iPr_def_12 )
| ~ element(iPr_def_12,iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_1781,c_944,c_945]) ).
tcf(c_1783,plain,
empty_set = iPr_def_12,
inference(forward_subsumption_resolution,[status(thm)],[c_1782,c_1606]) ).
tcf(c_1784,plain,
empty_set = sK5,
inference(backward_subsumption_resolution,[status(thm)],[c_1719,c_1783]) ).
tcf(c_1800,plain,
empty(iPr_def_12),
inference(demodulation,[status(thm)],[c_77,c_1783]) ).
tcf(c_1819,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_1784,c_1800,c_1556,c_949]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU326+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.58 % Computer : n001.cluster.edu
% 0.13/0.58 % Model : x86_64 x86_64
% 0.13/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.58 % Memory : 8046.5625MB
% 0.13/0.58 % OS : Linux 6.8.0-71-generic
% 0.13/0.58 % CPULimit : 300
% 0.13/0.58 % WCLimit : 300
% 0.13/0.58 % DateTime : Thu Sep 24 13:48:24 UTC 2026
% 0.13/0.59 % CPUTime :
% 0.13/0.59 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.62 Running first-order theorem proving
% 0.13/0.62 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.13/0.64
% 0.13/0.64 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.64
% 0.13/0.64 % Detected problem language: tptp
% 0.16/0.65 % Proving...
% 2.20/1.39 % SZS status Started for theBenchmark.p
% 2.20/1.39 % SZS status Theorem for theBenchmark.p
% 2.20/1.39
% 2.20/1.39 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.20/1.39
% 2.20/1.39 % ------ iProver source info
% 2.20/1.39
% 2.20/1.39 % git: date: 2026-07-19 20:42:38 +0200
% 2.20/1.39 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.20/1.39 % git: non_committed_changes: false
% 2.20/1.39
% 2.20/1.39 % ------ Parsing...
% 2.20/1.39 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.20/1.39
% 2.20/1.39 % ------ Preprocessing... sup_sim: 0 sf_s rm: 40 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 6 0s sf_e pe_s pe_e %
% 2.20/1.39
% 2.20/1.39 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.20/1.39
% 2.20/1.39 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 2.20/1.39 % ------ Proving...
% 2.20/1.39 % ------ Problem Properties
% 2.20/1.39
% 2.20/1.39 %
% 2.20/1.39 % clauses 26
% 2.20/1.39 % conjectures 3
% 2.20/1.39 % EPR 11
% 2.20/1.39 % Horn 23
% 2.20/1.39 % unary 11
% 2.20/1.39 % binary 10
% 2.20/1.39 % lits 46
% 2.20/1.39 % lits eq 12
% 2.20/1.39 % fd_pure 0
% 2.20/1.39 % fd_pseudo 0
% 2.20/1.39 % fd_cond 2
% 2.20/1.39 % fd_pseudo_cond 1
% 2.20/1.39 % AC symbols 0
% 2.20/1.39
% 2.20/1.39 % ------ Schedule dynamic 5 is on
% 2.20/1.39
% 2.20/1.39 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 2.20/1.39
% 2.20/1.39
% 2.20/1.39 % ------
% 2.20/1.39 % Current options:
% 2.20/1.39 % ------
% 2.20/1.39
% 2.20/1.39
% 2.20/1.39 %
% 2.20/1.39
% 2.20/1.39 % ------ Proving...
% 2.20/1.39 %
% 2.20/1.39
% 2.20/1.39 % SZS status Theorem for theBenchmark.p
% 2.20/1.39
% 2.20/1.39 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.20/1.39
% 2.20/1.39
%------------------------------------------------------------------------------