%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU326+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n016.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:56 PM UTC 2026
% Result : Theorem 1.07s 1.74s
% Output : CNFRefutation 1.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 6
% Syntax : Number of formulae : 54 ( 8 unt; 0 def)
% Number of atoms : 198 ( 60 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 255 ( 111 ~; 98 |; 33 &)
% ( 5 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 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 : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 103 ( 0 sgn 96 !; 7 ?; 23 :)
% Comments :
%------------------------------------------------------------------------------
fof(f68,axiom,
! [X0] :
( X0 = empty_set
<=> ! [X1] : ~ in(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f116,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ! [X2] :
( element(X2,powerset(powerset(X0)))
=> ( X2 = complements_of_subsets(X0,X1)
<=> ! [X3] :
( element(X3,powerset(X0))
=> ( in(X3,X2)
<=> in(subset_complement(X0,X3),X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_setfam_1) ).
fof(f167,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> element(complements_of_subsets(X0,X1),powerset(powerset(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_setfam_1) ).
fof(f360,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/sandbox2/benchmark/theBenchmark.p',t10_tops_2) ).
fof(f361,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)],[f360]) ).
fof(f476,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ~ ( complements_of_subsets(X0,X1) = empty_set
& X1 != empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t46_setfam_1) ).
fof(f485,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X2))
& in(X0,X1) )
=> element(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f708,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| ! [X2] :
( ~ element(X2,powerset(powerset(X0)))
| ( X2 = complements_of_subsets(X0,X1)
<=> ! [X3] :
( ~ element(X3,powerset(X0))
| ( in(X3,X2)
<=> in(subset_complement(X0,X3),X1) ) ) ) ) ),
inference(ennf_transformation,[],[f116]) ).
fof(f742,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| element(complements_of_subsets(X0,X1),powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f167]) ).
fof(f936,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,[],[f361]) ).
fof(f1076,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| empty_set != complements_of_subsets(X0,X1)
| empty_set = X1 ),
inference(ennf_transformation,[],[f476]) ).
fof(f1077,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| empty_set != complements_of_subsets(X0,X1)
| empty_set = X1 ),
inference(flattening,[],[f1076]) ).
fof(f1088,plain,
! [X0,X1,X2] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(ennf_transformation,[],[f485]) ).
fof(f1089,plain,
! [X0,X1,X2] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(flattening,[],[f1088]) ).
fof(f1304,plain,
! [X0] :
( ( empty_set != X0
| ! [X1] : ~ in(X1,X0) )
& ( ? [X1] : in(X1,X0)
| X0 = empty_set ) ),
inference(nnf_transformation,[],[f68]) ).
fof(f1305,plain,
! [X0] :
( ( empty_set != X0
| ! [X2] : ~ in(X2,X0) )
& ( ? [X1] : in(X1,X0)
| X0 = empty_set ) ),
inference(rectify,[],[f1304]) ).
fof(f1306,plain,
! [X0] :
( ( empty_set != X0
| ! [X2] : ~ in(X2,X0) )
& ( in(sK83(X0),X0)
| X0 = empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK83]),skolemize(X1,sK83(X0))],[f1305]) ).
fof(f1413,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| ! [X2] :
( ~ element(X2,powerset(powerset(X0)))
| ( ( complements_of_subsets(X0,X1) != X2
| ! [X3] :
( ~ element(X3,powerset(X0))
| ( ( ~ in(X3,X2)
| in(subset_complement(X0,X3),X1) )
& ( ~ in(subset_complement(X0,X3),X1)
| in(X3,X2) ) ) ) )
& ( ? [X3] :
( element(X3,powerset(X0))
& ( in(X3,X2)
| in(subset_complement(X0,X3),X1) )
& ( ~ in(X3,X2)
| ~ in(subset_complement(X0,X3),X1) ) )
| X2 = complements_of_subsets(X0,X1) ) ) ) ),
inference(nnf_transformation,[],[f708]) ).
fof(f1414,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| ! [X2] :
( ~ element(X2,powerset(powerset(X0)))
| ( ( complements_of_subsets(X0,X1) != X2
| ! [X3] :
( ~ element(X3,powerset(X0))
| ( ( ~ in(X3,X2)
| in(subset_complement(X0,X3),X1) )
& ( ~ in(subset_complement(X0,X3),X1)
| in(X3,X2) ) ) ) )
& ( ? [X3] :
( element(X3,powerset(X0))
& ( in(X3,X2)
| in(subset_complement(X0,X3),X1) )
& ( ~ in(X3,X2)
| ~ in(subset_complement(X0,X3),X1) ) )
| X2 = complements_of_subsets(X0,X1) ) ) ) ),
inference(flattening,[],[f1413]) ).
fof(f1415,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| ! [X2] :
( ~ element(X2,powerset(powerset(X0)))
| ( ( complements_of_subsets(X0,X1) != X2
| ! [X4] :
( ~ element(X4,powerset(X0))
| ( ( ~ in(X4,X2)
| in(subset_complement(X0,X4),X1) )
& ( ~ in(subset_complement(X0,X4),X1)
| in(X4,X2) ) ) ) )
& ( ? [X3] :
( element(X3,powerset(X0))
& ( in(X3,X2)
| in(subset_complement(X0,X3),X1) )
& ( ~ in(X3,X2)
| ~ in(subset_complement(X0,X3),X1) ) )
| X2 = complements_of_subsets(X0,X1) ) ) ) ),
inference(rectify,[],[f1414]) ).
fof(f1416,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| ! [X2] :
( ~ element(X2,powerset(powerset(X0)))
| ( ( complements_of_subsets(X0,X1) != X2
| ! [X4] :
( ~ element(X4,powerset(X0))
| ( ( ~ in(X4,X2)
| in(subset_complement(X0,X4),X1) )
& ( ~ in(subset_complement(X0,X4),X1)
| in(X4,X2) ) ) ) )
& ( ( element(sK141(X0,X1,X2),powerset(X0))
& ( in(sK141(X0,X1,X2),X2)
| in(subset_complement(X0,sK141(X0,X1,X2)),X1) )
& ( ~ in(sK141(X0,X1,X2),X2)
| ~ in(subset_complement(X0,sK141(X0,X1,X2)),X1) ) )
| X2 = complements_of_subsets(X0,X1) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK141]),skolemize(X3,sK141(X0,X1,X2))],[f1415]) ).
fof(f1674,plain,
( element(sK365,powerset(powerset(sK364)))
& ( ( empty_set = sK365
& empty_set != complements_of_subsets(sK364,sK365) )
| ( empty_set = complements_of_subsets(sK364,sK365)
& empty_set != sK365 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK364,sK365]),skolemize(X0,sK364),skolemize(X1,sK365)],[f936]) ).
fof(f1959,plain,
! [X2,X0] :
( empty_set != X0
| ~ in(X2,X0) ),
inference(cnf_transformation,[],[f1306]) ).
fof(f1960,plain,
! [X0] :
( in(sK83(X0),X0)
| empty_set = X0 ),
inference(cnf_transformation,[],[f1306]) ).
fof(f2158,plain,
! [X2,X0,X1,X4] :
( ~ element(X1,powerset(powerset(X0)))
| ~ element(X2,powerset(powerset(X0)))
| complements_of_subsets(X0,X1) != X2
| ~ element(X4,powerset(X0))
| ~ in(X4,X2)
| in(subset_complement(X0,X4),X1) ),
inference(cnf_transformation,[],[f1416]) ).
fof(f2190,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| element(complements_of_subsets(X0,X1),powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f742]) ).
fof(f2873,plain,
element(sK365,powerset(powerset(sK364))),
inference(cnf_transformation,[],[f1674]) ).
fof(f2874,plain,
( empty_set = sK365
| empty_set = complements_of_subsets(sK364,sK365) ),
inference(cnf_transformation,[],[f1674]) ).
fof(f2877,plain,
( empty_set != complements_of_subsets(sK364,sK365)
| empty_set != sK365 ),
inference(cnf_transformation,[],[f1674]) ).
fof(f3065,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| empty_set != complements_of_subsets(X0,X1)
| empty_set = X1 ),
inference(cnf_transformation,[],[f1077]) ).
fof(f3074,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(cnf_transformation,[],[f1089]) ).
fof(f3590,plain,
! [X2] : ~ in(X2,empty_set),
inference(equality_resolution,[],[f1959]) ).
fof(f3644,plain,
! [X0,X1,X4] :
( ~ element(X1,powerset(powerset(X0)))
| ~ element(complements_of_subsets(X0,X1),powerset(powerset(X0)))
| ~ element(X4,powerset(X0))
| ~ in(X4,complements_of_subsets(X0,X1))
| in(subset_complement(X0,X4),X1) ),
inference(equality_resolution,[],[f2158]) ).
tcf(c_248,plain,
! [X0: $i] :
( in(sK83(X0),X0)
| ( X0 = empty_set ) ),
inference(cnf_transformation,[],[f1960]) ).
tcf(c_249,plain,
! [X0: $i] : ~ in(X0,empty_set),
inference(cnf_transformation,[],[f3590]) ).
tcf(c_450,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(subset_complement(X0,X2),X1)
| ~ element(X2,powerset(X0))
| ~ element(X1,powerset(powerset(X0)))
| ~ in(X2,complements_of_subsets(X0,X1))
| ~ element(complements_of_subsets(X0,X1),powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f3644]) ).
tcf(c_478,plain,
! [X0: $i,X1: $i] :
( element(complements_of_subsets(X1,X0),powerset(powerset(X1)))
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[],[f2190]) ).
tcf(c_1161,negated_conjecture,
( ( empty_set != sK365 )
| ( complements_of_subsets(sK364,sK365) != empty_set ) ),
inference(cnf_transformation,[],[f2877]) ).
tcf(c_1162,negated_conjecture,
( ( empty_set = sK365 )
| ( complements_of_subsets(sK364,sK365) = empty_set ) ),
inference(cnf_transformation,[],[f2874]) ).
tcf(c_1163,negated_conjecture,
element(sK365,powerset(powerset(sK364))),
inference(cnf_transformation,[],[f2873]) ).
tcf(c_1351,plain,
! [X0: $i,X1: $i] :
( ( X1 = empty_set )
| ~ element(X1,powerset(powerset(X0)))
| ( complements_of_subsets(X0,X1) != empty_set ) ),
inference(cnf_transformation,[],[f3065]) ).
tcf(c_1359,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(X2,X1)
| ~ in(X2,X0)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f3074]) ).
tcf(c_1645,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(X0,powerset(X1))
| ~ element(X2,powerset(powerset(X1)))
| ~ in(X0,complements_of_subsets(X1,X2)) ),
inference(superposition,[status(thm)],[c_478,c_1359]) ).
tcf(c_1672,plain,
( ( empty_set = sK365 )
| ~ element(sK365,powerset(powerset(sK364))) ),
inference(superposition,[status(thm)],[c_1162,c_1351]) ).
tcf(c_1687,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(subset_complement(X1,X0),X2)
| ~ element(X0,powerset(X1))
| ~ element(X2,powerset(powerset(X1)))
| ~ in(X0,complements_of_subsets(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_450,c_478]) ).
tcf(c_1702,plain,
! [X0: $i] :
( in(subset_complement(sK364,X0),sK365)
| ~ element(X0,powerset(sK364))
| ~ in(X0,complements_of_subsets(sK364,sK365)) ),
inference(superposition,[status(thm)],[c_1163,c_1687]) ).
tcf(c_1806,plain,
! [X0: $i] :
( element(X0,powerset(sK364))
| ~ in(X0,complements_of_subsets(sK364,sK365)) ),
inference(superposition,[status(thm)],[c_1163,c_1645]) ).
tcf(c_1879,plain,
empty_set = sK365,
inference(global_subsumption_just,[status(thm)],[c_1672,c_1163,c_1672]) ).
tcf(c_1882,plain,
( ( empty_set != sK365 )
| ( complements_of_subsets(sK364,empty_set) != empty_set ) ),
inference(superposition,[status(thm)],[c_1879,c_1161]) ).
tcf(c_1948,plain,
! [X0: $i] :
( in(subset_complement(sK364,X0),sK365)
| ~ in(X0,complements_of_subsets(sK364,sK365)) ),
inference(global_subsumption_just,[status(thm)],[c_1702,c_1702,c_1806]) ).
tcf(c_1953,plain,
! [X0: $i] :
( in(subset_complement(sK364,X0),empty_set)
| ~ in(X0,complements_of_subsets(sK364,empty_set)) ),
inference(light_normalisation,[status(thm)],[c_1948,c_1879]) ).
tcf(c_1956,plain,
! [X0: $i] : ~ in(X0,complements_of_subsets(sK364,empty_set)),
inference(forward_subsumption_resolution,[status(thm)],[c_1953,c_249]) ).
tcf(c_1957,plain,
complements_of_subsets(sK364,empty_set) = empty_set,
inference(superposition,[status(thm)],[c_248,c_1956]) ).
tcf(c_1960,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_1957,c_1882,c_1672,c_1163]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU326+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.37 % Computer : n016.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Thu Sep 24 13:47:28 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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.12/0.42
% 0.12/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.42
% 0.12/0.42 % Detected problem language: tptp
% 0.12/0.44 % Proving...
% 1.07/1.74 % SZS status Started for theBenchmark.p
% 1.07/1.74 % SZS status Theorem for theBenchmark.p
% 1.07/1.74
% 1.07/1.74 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.07/1.74
% 1.07/1.74 % ------ iProver source info
% 1.07/1.74
% 1.07/1.74 % git: date: 2026-07-19 20:42:38 +0200
% 1.07/1.74 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.07/1.74 % git: non_committed_changes: false
% 1.07/1.74
% 1.07/1.74 % ------ Parsing...
% 1.07/1.74 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 1.07/1.74 % ------ Proving...
% 1.07/1.74 % ------ Problem Properties
% 1.07/1.74
% 1.07/1.74 %
% 1.07/1.74 % clauses 1411
% 1.07/1.74 % conjectures 3
% 1.07/1.74 % EPR 228
% 1.07/1.74 % Horn 1088
% 1.07/1.74 % unary 181
% 1.07/1.74 % binary 451
% 1.07/1.74 % lits 4282
% 1.07/1.74 % lits eq 529
% 1.07/1.74 % fd_pure 0
% 1.07/1.74 % fd_pseudo 0
% 1.07/1.74 % fd_cond 45
% 1.07/1.74 % fd_pseudo_cond 118
% 1.07/1.74 % AC symbols 0
% 1.07/1.74
% 1.07/1.74 % ------ Input Options Time Limit: Unbounded
% 1.07/1.74
% 1.07/1.74
% 1.07/1.74 % ------
% 1.07/1.74 % Current options:
% 1.07/1.74 % ------
% 1.07/1.74
% 1.07/1.74
% 1.07/1.74 %
% 1.07/1.74
% 1.07/1.74 % ------ Proving...
% 1.07/1.74 %
% 1.07/1.74
% 1.07/1.74 % SZS status Theorem for theBenchmark.p
% 1.07/1.74
% 1.07/1.74 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.07/1.74
% 1.07/1.74
%------------------------------------------------------------------------------