%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU321+2 : 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 : n010.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:51 PM UTC 2026
% Result : Theorem 102.49s 16.63s
% Output : CNFRefutation 102.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 6
% Syntax : Number of formulae : 68 ( 15 unt; 0 def)
% Number of atoms : 239 ( 20 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 279 ( 108 ~; 97 |; 53 &)
% ( 9 <=>; 10 =>; 0 <=; 2 <~>)
% Maximal formula depth : 11 ( 5 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 : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 103 ( 0 sgn 88 !; 15 ?; 22 :)
% Comments :
%------------------------------------------------------------------------------
fof(f73,axiom,
! [X0,X1] :
( ( empty(X0)
=> ( element(X1,X0)
<=> empty(X1) ) )
& ( ~ empty(X0)
=> ( element(X1,X0)
<=> in(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f93,axiom,
! [X0,X1,X2] :
( X2 = set_difference(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( ~ in(X3,X1)
& in(X3,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f98,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,X1) = set_difference(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_subset_1) ).
fof(f201,axiom,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ~ empty(the_carrier(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f264,conjecture,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,subset_complement(the_carrier(X0),X1))
<=> ~ in(X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l40_tops_1) ).
fof(f265,negated_conjecture,
~ ! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,subset_complement(the_carrier(X0),X1))
<=> ~ in(X2,X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f264]) ).
fof(f447,axiom,
! [X0,X1] :
( element(X0,powerset(X1))
<=> subset(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f591,plain,
? [X0] :
( one_sorted_str(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,powerset(the_carrier(X0)))
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,subset_complement(the_carrier(X0),X1))
<~> ~ in(X2,X1) ) ) ) ),
inference(ennf_transformation,[],[f265]) ).
fof(f592,plain,
? [X0] :
( one_sorted_str(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,powerset(the_carrier(X0)))
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,subset_complement(the_carrier(X0),X1))
<~> ~ in(X2,X1) ) ) ) ),
inference(flattening,[],[f591]) ).
fof(f871,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(the_carrier(X0)) ),
inference(ennf_transformation,[],[f201]) ).
fof(f872,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(the_carrier(X0)) ),
inference(flattening,[],[f871]) ).
fof(f875,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| subset_complement(X0,X1) = set_difference(X0,X1) ),
inference(ennf_transformation,[],[f98]) ).
fof(f897,plain,
! [X0,X1] :
( ( ~ empty(X0)
| ( element(X1,X0)
<=> empty(X1) ) )
& ( empty(X0)
| ( element(X1,X0)
<=> in(X1,X0) ) ) ),
inference(ennf_transformation,[],[f73]) ).
fof(f1137,plain,
? [X0] :
( one_sorted_str(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,powerset(the_carrier(X0)))
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,subset_complement(the_carrier(X0),X1))
| ~ in(X2,X1) )
& ( ~ in(X2,subset_complement(the_carrier(X0),X1))
| in(X2,X1) ) ) ) ),
inference(nnf_transformation,[],[f592]) ).
fof(f1138,plain,
? [X0] :
( one_sorted_str(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,powerset(the_carrier(X0)))
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,subset_complement(the_carrier(X0),X1))
| ~ in(X2,X1) )
& ( ~ in(X2,subset_complement(the_carrier(X0),X1))
| in(X2,X1) ) ) ) ),
inference(flattening,[],[f1137]) ).
fof(f1139,plain,
( one_sorted_str(sK46)
& ~ empty_carrier(sK46)
& element(sK47,powerset(the_carrier(sK46)))
& element(sK48,the_carrier(sK46))
& ( in(sK48,subset_complement(the_carrier(sK46),sK47))
| ~ in(sK48,sK47) )
& ( ~ in(sK48,subset_complement(the_carrier(sK46),sK47))
| in(sK48,sK47) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46,sK47,sK48]),skolemize(X0,sK46),skolemize(X1,sK47),skolemize(X2,sK48)],[f1138]) ).
fof(f1372,plain,
! [X0,X1] :
( ( ~ element(X0,powerset(X1))
| subset(X0,X1) )
& ( ~ subset(X0,X1)
| element(X0,powerset(X1)) ) ),
inference(nnf_transformation,[],[f447]) ).
fof(f1384,plain,
! [X0,X1,X2] :
( ( set_difference(X0,X1) != X2
| ! [X3] :
( ( ~ in(X3,X2)
| ( ~ in(X3,X1)
& in(X3,X0) ) )
& ( in(X3,X1)
| ~ in(X3,X0)
| in(X3,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| ( ~ in(X3,X1)
& in(X3,X0) ) )
& ( ~ in(X3,X2)
| in(X3,X1)
| ~ in(X3,X0) ) )
| X2 = set_difference(X0,X1) ) ),
inference(nnf_transformation,[],[f93]) ).
fof(f1385,plain,
! [X0,X1,X2] :
( ( set_difference(X0,X1) != X2
| ! [X3] :
( ( ~ in(X3,X2)
| ( ~ in(X3,X1)
& in(X3,X0) ) )
& ( in(X3,X1)
| ~ in(X3,X0)
| in(X3,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| ( ~ in(X3,X1)
& in(X3,X0) ) )
& ( ~ in(X3,X2)
| in(X3,X1)
| ~ in(X3,X0) ) )
| X2 = set_difference(X0,X1) ) ),
inference(flattening,[],[f1384]) ).
fof(f1386,plain,
! [X0,X1,X2] :
( ( set_difference(X0,X1) != X2
| ! [X4] :
( ( ~ in(X4,X2)
| ( ~ in(X4,X1)
& in(X4,X0) ) )
& ( in(X4,X1)
| ~ in(X4,X0)
| in(X4,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| ( ~ in(X3,X1)
& in(X3,X0) ) )
& ( ~ in(X3,X2)
| in(X3,X1)
| ~ in(X3,X0) ) )
| X2 = set_difference(X0,X1) ) ),
inference(rectify,[],[f1385]) ).
fof(f1387,plain,
! [X0,X1,X2] :
( ( set_difference(X0,X1) != X2
| ! [X4] :
( ( ~ in(X4,X2)
| ( ~ in(X4,X1)
& in(X4,X0) ) )
& ( in(X4,X1)
| ~ in(X4,X0)
| in(X4,X2) ) ) )
& ( ( ( in(sK194(X0,X1,X2),X2)
| ( ~ in(sK194(X0,X1,X2),X1)
& in(sK194(X0,X1,X2),X0) ) )
& ( ~ in(sK194(X0,X1,X2),X2)
| in(sK194(X0,X1,X2),X1)
| ~ in(sK194(X0,X1,X2),X0) ) )
| X2 = set_difference(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK194]),skolemize(X3,sK194(X0,X1,X2))],[f1386]) ).
fof(f1430,plain,
! [X0,X1] :
( ( ~ empty(X0)
| ( ( ~ element(X1,X0)
| empty(X1) )
& ( ~ empty(X1)
| element(X1,X0) ) ) )
& ( empty(X0)
| ( ( ~ element(X1,X0)
| in(X1,X0) )
& ( ~ in(X1,X0)
| element(X1,X0) ) ) ) ),
inference(nnf_transformation,[],[f897]) ).
fof(f1629,plain,
one_sorted_str(sK46),
inference(cnf_transformation,[],[f1139]) ).
fof(f1630,plain,
~ empty_carrier(sK46),
inference(cnf_transformation,[],[f1139]) ).
fof(f1631,plain,
element(sK47,powerset(the_carrier(sK46))),
inference(cnf_transformation,[],[f1139]) ).
fof(f1632,plain,
element(sK48,the_carrier(sK46)),
inference(cnf_transformation,[],[f1139]) ).
fof(f1633,plain,
( in(sK48,subset_complement(the_carrier(sK46),sK47))
| ~ in(sK48,sK47) ),
inference(cnf_transformation,[],[f1139]) ).
fof(f1634,plain,
( ~ in(sK48,subset_complement(the_carrier(sK46),sK47))
| in(sK48,sK47) ),
inference(cnf_transformation,[],[f1139]) ).
fof(f2199,plain,
! [X0,X1] :
( ~ element(X0,powerset(X1))
| subset(X0,X1) ),
inference(cnf_transformation,[],[f1372]) ).
fof(f2200,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f1372]) ).
fof(f2229,plain,
! [X2,X0,X1,X4] :
( set_difference(X0,X1) != X2
| ~ in(X4,X2)
| ~ in(X4,X1) ),
inference(cnf_transformation,[],[f1387]) ).
fof(f2231,plain,
! [X2,X0,X1,X4] :
( set_difference(X0,X1) != X2
| in(X4,X1)
| ~ in(X4,X0)
| in(X4,X2) ),
inference(cnf_transformation,[],[f1387]) ).
fof(f2247,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(the_carrier(X0)) ),
inference(cnf_transformation,[],[f872]) ).
fof(f2250,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| set_difference(X0,X1) = subset_complement(X0,X1) ),
inference(cnf_transformation,[],[f875]) ).
fof(f2341,plain,
! [X0,X1] :
( empty(X0)
| ~ element(X1,X0)
| in(X1,X0) ),
inference(cnf_transformation,[],[f1430]) ).
fof(f3294,plain,
! [X0,X1,X4] :
( in(X4,X1)
| ~ in(X4,X0)
| in(X4,set_difference(X0,X1)) ),
inference(equality_resolution,[],[f2231]) ).
fof(f3296,plain,
! [X0,X1,X4] :
( ~ in(X4,set_difference(X0,X1))
| ~ in(X4,X1) ),
inference(equality_resolution,[],[f2229]) ).
tcf(c_73,negated_conjecture,
( in(sK48,sK47)
| ~ in(sK48,subset_complement(the_carrier(sK46),sK47)) ),
inference(cnf_transformation,[],[f1634]) ).
tcf(c_74,negated_conjecture,
( in(sK48,subset_complement(the_carrier(sK46),sK47))
| ~ in(sK48,sK47) ),
inference(cnf_transformation,[],[f1633]) ).
tcf(c_75,negated_conjecture,
element(sK48,the_carrier(sK46)),
inference(cnf_transformation,[],[f1632]) ).
tcf(c_76,negated_conjecture,
element(sK47,powerset(the_carrier(sK46))),
inference(cnf_transformation,[],[f1631]) ).
tcf(c_77,negated_conjecture,
~ empty_carrier(sK46),
inference(cnf_transformation,[],[f1630]) ).
tcf(c_78,negated_conjecture,
one_sorted_str(sK46),
inference(cnf_transformation,[],[f1629]) ).
tcf(c_638,plain,
! [X0: $i,X1: $i] :
( element(X0,powerset(X1))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f2200]) ).
tcf(c_639,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f2199]) ).
tcf(c_671,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,X2)
| in(X0,set_difference(X1,X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f3294]) ).
tcf(c_673,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ in(X0,X2)
| ~ in(X0,set_difference(X1,X2)) ),
inference(cnf_transformation,[],[f3296]) ).
tcf(c_686,plain,
! [X0: $i] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ empty(the_carrier(X0)) ),
inference(cnf_transformation,[],[f2247]) ).
tcf(c_689,plain,
! [X0: $i,X1: $i] :
( ( set_difference(X1,X0) = subset_complement(X1,X0) )
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f2250]) ).
tcf(c_779,plain,
! [X0: $i,X1: $i] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[],[f2341]) ).
tcf(c_2382,plain,
! [X0: $i,X1: $i] :
( ( set_difference(X1,X0) = subset_complement(X1,X0) )
| ~ subset(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_638,c_689]) ).
tcf(c_22080,plain,
! [X0: $i] :
( ~ one_sorted_str(X0)
| ~ empty(the_carrier(X0))
| ( X0 != sK46 ) ),
inference(resolution_lifted,[status(thm)],[c_77,c_686]) ).
tcf(c_22081,plain,
( ~ one_sorted_str(sK46)
| ~ empty(the_carrier(sK46)) ),
inference(unflattening,[status(thm)],[c_22080]) ).
tcf(c_24267,plain,
! [X0: $i] :
( empty_carrier(X0)
| ~ empty(the_carrier(X0))
| ( X0 != sK46 ) ),
inference(resolution_lifted,[status(thm)],[c_78,c_686]) ).
tcf(c_24268,plain,
( empty_carrier(sK46)
| ~ empty(the_carrier(sK46)) ),
inference(unflattening,[status(thm)],[c_24267]) ).
tcf(c_24269,plain,
~ empty(the_carrier(sK46)),
inference(global_subsumption_just,[status(thm)],[c_24268,c_78,c_22081]) ).
tcf(c_44292,plain,
! [X0: $i,X1: $i] :
( ( set_difference(X1,X0) = subset_complement(X1,X0) )
| ~ subset(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_2382]) ).
tcf(c_108911,plain,
subset(sK47,the_carrier(sK46)),
inference(superposition,[status(thm)],[c_76,c_639]) ).
tcf(c_113756,plain,
( empty(the_carrier(sK46))
| in(sK48,the_carrier(sK46)) ),
inference(superposition,[status(thm)],[c_75,c_779]) ).
tcf(c_113827,plain,
in(sK48,the_carrier(sK46)),
inference(forward_subsumption_resolution,[status(thm)],[c_113756,c_24269]) ).
tcf(c_133382,plain,
! [X0: $i] :
( in(sK48,X0)
| in(sK48,set_difference(the_carrier(sK46),X0))
| ~ in(sK48,the_carrier(sK46)) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_147897,plain,
( in(sK48,sK47)
| in(sK48,set_difference(the_carrier(sK46),sK47))
| ~ in(sK48,the_carrier(sK46)) ),
inference(instantiation,[status(thm)],[c_133382]) ).
tcf(c_189499,plain,
set_difference(the_carrier(sK46),sK47) = subset_complement(the_carrier(sK46),sK47),
inference(superposition,[status(thm)],[c_108911,c_44292]) ).
tcf(c_189883,plain,
( in(sK48,set_difference(the_carrier(sK46),sK47))
| ~ in(sK48,sK47) ),
inference(demodulation,[status(thm)],[c_74,c_189499]) ).
tcf(c_189884,plain,
( in(sK48,sK47)
| ~ in(sK48,set_difference(the_carrier(sK46),sK47)) ),
inference(demodulation,[status(thm)],[c_73,c_189499]) ).
tcf(c_191135,plain,
in(sK48,set_difference(the_carrier(sK46),sK47)),
inference(global_subsumption_just,[status(thm)],[c_189883,c_113827,c_147897,c_189883]) ).
tcf(c_191155,plain,
~ in(sK48,sK47),
inference(superposition,[status(thm)],[c_191135,c_673]) ).
tcf(c_191181,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_191155,c_191135,c_189884]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU321+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n010.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 13:41:47 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.42 Running first-order theorem proving
% 0.14/0.42 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.44
% 0.14/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.44
% 0.14/0.44 % Detected problem language: tptp
% 0.14/0.46 % Proving...
% 102.49/16.63 % SZS status Started for theBenchmark.p
% 102.49/16.63 % SZS status Theorem for theBenchmark.p
% 102.49/16.63
% 102.49/16.63 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 102.49/16.63
% 102.49/16.63 % ------ iProver source info
% 102.49/16.63
% 102.49/16.63 % git: date: 2026-07-19 20:42:38 +0200
% 102.49/16.63 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 102.49/16.63 % git: non_committed_changes: false
% 102.49/16.63
% 102.49/16.63 % ------ Parsing...
% 102.49/16.63 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 102.49/16.63
% 102.49/16.63 % ------ Preprocessing... sup_sim: 96 sf_s rm: 76 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 30 sf_s rm: 19 0s sf_e pe_s pe_e %
% 102.49/16.63
% 102.49/16.63 % ------ Preprocessing... gs_s sp: 15 0s gs_e snvd_s sp: 0 0s snvd_e %
% 102.49/16.63
% 102.49/16.63 % ------ Preprocessing... sf_s rm: 3 0s sf_e sf_s rm: 0 0s sf_e
% 102.49/16.63 % ------ Proving...
% 102.49/16.63 % ------ Problem Properties
% 102.49/16.63
% 102.49/16.63 %
% 102.49/16.63 % clauses 1116
% 102.49/16.63 % conjectures 5
% 102.49/16.63 % EPR 165
% 102.49/16.63 % Horn 827
% 102.49/16.63 % unary 138
% 102.49/16.63 % binary 362
% 102.49/16.63 % lits 3309
% 102.49/16.63 % lits eq 475
% 102.49/16.63 % fd_pure 0
% 102.49/16.63 % fd_pseudo 0
% 102.49/16.63 % fd_cond 41
% 102.49/16.63 % fd_pseudo_cond 109
% 102.49/16.63 % AC symbols 0
% 102.49/16.63
% 102.49/16.63 % ------ Schedule dynamic 5 is on
% 102.49/16.63
% 102.49/16.63 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 102.49/16.63
% 102.49/16.63
% 102.49/16.63 % ------
% 102.49/16.63 % Current options:
% 102.49/16.63 % ------
% 102.49/16.63
% 102.49/16.63
% 102.49/16.63 %
% 102.49/16.63
% 102.49/16.63 % ------ Proving...
% 102.49/16.63 %
% 102.49/16.63
% 102.49/16.63 % SZS status Theorem for theBenchmark.p
% 102.49/16.63
% 102.49/16.63 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 102.49/16.63
% 102.49/16.63
%------------------------------------------------------------------------------