%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU308+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 : 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:56:35 PM UTC 2026
% Result : Theorem 3.69s 6.19s
% Output : CNFRefutation 3.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 44 ( 13 unt; 0 def)
% Number of atoms : 87 ( 26 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 78 ( 35 ~; 28 |; 6 &)
% ( 1 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 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 : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 54 ( 0 sgn 52 !; 2 ?; 16 :)
% Comments :
%------------------------------------------------------------------------------
fof(f94,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(f130,axiom,
! [X0] :
( one_sorted_str(X0)
=> element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_pre_topc) ).
fof(f291,axiom,
! [X0,X1,X2] :
( ( element(X2,powerset(X0))
& element(X1,powerset(X0)) )
=> subset_difference(X0,X1,X2) = set_difference(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_subset_1) ).
fof(f337,axiom,
! [X0] :
( one_sorted_str(X0)
=> cast_as_carrier_subset(X0) = the_carrier(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f361,conjecture,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t17_pre_topc) ).
fof(f362,negated_conjecture,
~ ! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1) ) ),
inference(negated_conjecture,[status(cth)],[f361]) ).
fof(f424,axiom,
! [X0,X1] :
( element(X0,powerset(X1))
<=> subset(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f636,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| subset_complement(X0,X1) = set_difference(X0,X1) ),
inference(ennf_transformation,[],[f94]) ).
fof(f665,plain,
! [X0] :
( ~ one_sorted_str(X0)
| element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
inference(ennf_transformation,[],[f130]) ).
fof(f783,plain,
! [X0,X1,X2] :
( ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| subset_difference(X0,X1,X2) = set_difference(X1,X2) ),
inference(ennf_transformation,[],[f291]) ).
fof(f784,plain,
! [X0,X1,X2] :
( ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| subset_difference(X0,X1,X2) = set_difference(X1,X2) ),
inference(flattening,[],[f783]) ).
fof(f848,plain,
! [X0] :
( ~ one_sorted_str(X0)
| cast_as_carrier_subset(X0) = the_carrier(X0) ),
inference(ennf_transformation,[],[f337]) ).
fof(f882,plain,
? [X0] :
( one_sorted_str(X0)
& ? [X1] :
( element(X1,powerset(the_carrier(X0)))
& subset_complement(the_carrier(X0),X1) != subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1) ) ),
inference(ennf_transformation,[],[f362]) ).
fof(f1510,plain,
( one_sorted_str(sK332)
& element(sK333,powerset(the_carrier(sK332)))
& subset_complement(the_carrier(sK332),sK333) != subset_difference(the_carrier(sK332),cast_as_carrier_subset(sK332),sK333) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK332,sK333]),skolemize(X0,sK332),skolemize(X1,sK333)],[f882]) ).
fof(f1537,plain,
! [X0,X1] :
( ( ~ element(X0,powerset(X1))
| subset(X0,X1) )
& ( ~ subset(X0,X1)
| element(X0,powerset(X1)) ) ),
inference(nnf_transformation,[],[f424]) ).
fof(f1878,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| set_difference(X0,X1) = subset_complement(X0,X1) ),
inference(cnf_transformation,[],[f636]) ).
fof(f1953,plain,
! [X0] :
( ~ one_sorted_str(X0)
| element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f665]) ).
fof(f2252,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| subset_difference(X0,X1,X2) = set_difference(X1,X2) ),
inference(cnf_transformation,[],[f784]) ).
fof(f2591,plain,
! [X0] :
( ~ one_sorted_str(X0)
| the_carrier(X0) = cast_as_carrier_subset(X0) ),
inference(cnf_transformation,[],[f848]) ).
fof(f2627,plain,
one_sorted_str(sK332),
inference(cnf_transformation,[],[f1510]) ).
fof(f2628,plain,
element(sK333,powerset(the_carrier(sK332))),
inference(cnf_transformation,[],[f1510]) ).
fof(f2629,plain,
subset_complement(the_carrier(sK332),sK333) != subset_difference(the_carrier(sK332),cast_as_carrier_subset(sK332),sK333),
inference(cnf_transformation,[],[f1510]) ).
fof(f2726,plain,
! [X0,X1] :
( ~ element(X0,powerset(X1))
| subset(X0,X1) ),
inference(cnf_transformation,[],[f1537]) ).
fof(f2727,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f1537]) ).
tcf(c_351,plain,
! [X0: $i,X1: $i] :
( ( set_difference(X1,X0) = subset_complement(X1,X0) )
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f1878]) ).
tcf(c_425,plain,
! [X0: $i] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1953]) ).
tcf(c_724,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( subset_difference(X1,X0,X2) = set_difference(X0,X2) )
| ~ element(X2,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f2252]) ).
tcf(c_1063,plain,
! [X0: $i] :
( ( the_carrier(X0) = cast_as_carrier_subset(X0) )
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f2591]) ).
tcf(c_1099,negated_conjecture,
subset_difference(the_carrier(sK332),cast_as_carrier_subset(sK332),sK333) != subset_complement(the_carrier(sK332),sK333),
inference(cnf_transformation,[],[f2629]) ).
tcf(c_1100,negated_conjecture,
element(sK333,powerset(the_carrier(sK332))),
inference(cnf_transformation,[],[f2628]) ).
tcf(c_1101,negated_conjecture,
one_sorted_str(sK332),
inference(cnf_transformation,[],[f2627]) ).
tcf(c_1198,plain,
! [X0: $i,X1: $i] :
( element(X0,powerset(X1))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f2727]) ).
tcf(c_1199,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f2726]) ).
tcf(c_1505,plain,
! [X0: $i] :
( subset(cast_as_carrier_subset(X0),the_carrier(X0))
| ~ one_sorted_str(X0) ),
inference(superposition,[status(thm)],[c_425,c_1199]) ).
tcf(c_1512,plain,
the_carrier(sK332) = cast_as_carrier_subset(sK332),
inference(superposition,[status(thm)],[c_1101,c_1063]) ).
tcf(c_1570,plain,
set_difference(the_carrier(sK332),sK333) = subset_complement(the_carrier(sK332),sK333),
inference(superposition,[status(thm)],[c_1100,c_351]) ).
tcf(c_1571,plain,
subset_difference(the_carrier(sK332),cast_as_carrier_subset(sK332),sK333) != set_difference(the_carrier(sK332),sK333),
inference(demodulation,[status(thm)],[c_1099,c_1570]) ).
tcf(c_1687,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( subset_difference(X1,X2,X0) = set_difference(X2,X0) )
| ~ subset(X2,X1)
| ~ element(X0,powerset(X1)) ),
inference(superposition,[status(thm)],[c_1198,c_724]) ).
tcf(c_1729,plain,
( subset(the_carrier(sK332),the_carrier(sK332))
| ~ one_sorted_str(sK332) ),
inference(superposition,[status(thm)],[c_1512,c_1505]) ).
tcf(c_1970,plain,
subset_difference(the_carrier(sK332),the_carrier(sK332),sK333) != set_difference(the_carrier(sK332),sK333),
inference(light_normalisation,[status(thm)],[c_1571,c_1512]) ).
tcf(c_2284,plain,
! [X0: $i] :
( ( subset_difference(the_carrier(sK332),X0,sK333) = set_difference(X0,sK333) )
| ~ subset(X0,the_carrier(sK332)) ),
inference(superposition,[status(thm)],[c_1100,c_1687]) ).
tcf(c_2411,plain,
subset(the_carrier(sK332),the_carrier(sK332)),
inference(global_subsumption_just,[status(thm)],[c_1729,c_1101,c_1729]) ).
tcf(c_4575,plain,
subset_difference(the_carrier(sK332),the_carrier(sK332),sK333) = set_difference(the_carrier(sK332),sK333),
inference(superposition,[status(thm)],[c_2411,c_2284]) ).
tcf(c_4578,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_1970,c_4575]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU308+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.09/5.37 % Computer : n003.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Thu Sep 24 13:40:28 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/5.41 Running first-order theorem proving
% 0.13/5.41 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/5.42
% 0.13/5.42 % ======== iProver multi-core TPTP/SMT =========
% 0.13/5.42
% 0.13/5.42 % Detected problem language: tptp
% 0.13/5.43 % Proving...
% 3.69/6.19 % SZS status Started for theBenchmark.p
% 3.69/6.19 % SZS status Theorem for theBenchmark.p
% 3.69/6.19
% 3.69/6.19 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.69/6.19
% 3.69/6.19 % ------ iProver source info
% 3.69/6.19
% 3.69/6.19 % git: date: 2026-07-19 20:42:38 +0200
% 3.69/6.19 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.69/6.19 % git: non_committed_changes: false
% 3.69/6.19
% 3.69/6.19 % ------ Parsing...
% 3.69/6.19 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 3.69/6.19 % ------ Proving...
% 3.69/6.19 % ------ Problem Properties
% 3.69/6.19
% 3.69/6.19 %
% 3.69/6.19 % clauses 1275
% 3.69/6.19 % conjectures 3
% 3.69/6.19 % EPR 225
% 3.69/6.19 % Horn 986
% 3.69/6.19 % unary 182
% 3.69/6.19 % binary 415
% 3.69/6.19 % lits 3736
% 3.69/6.19 % lits eq 501
% 3.69/6.19 % fd_pure 0
% 3.69/6.19 % fd_pseudo 0
% 3.69/6.19 % fd_cond 45
% 3.69/6.19 % fd_pseudo_cond 117
% 3.69/6.19 % AC symbols 0
% 3.69/6.19
% 3.69/6.19 % ------ Input Options Time Limit: Unbounded
% 3.69/6.19
% 3.69/6.19
% 3.69/6.19 % ------
% 3.69/6.19 % Current options:
% 3.69/6.19 % ------
% 3.69/6.19
% 3.69/6.19
% 3.69/6.19 %
% 3.69/6.19
% 3.69/6.19 % ------ Proving...
% 3.69/6.19 %
% 3.69/6.19
% 3.69/6.19 % SZS status Theorem for theBenchmark.p
% 3.69/6.19
% 3.69/6.19 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.69/6.20
% 3.69/6.20
%------------------------------------------------------------------------------