%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU367+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 : n020.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:57:14 PM UTC 2026
% Result : Theorem 126.97s 18.01s
% Output : CNFRefutation 126.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 11
% Syntax : Number of formulae : 160 ( 21 unt; 0 def)
% Number of atoms : 774 ( 59 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 998 ( 384 ~; 490 |; 93 &)
% ( 11 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 5 con; 0-4 aty)
% Number of variables : 367 ( 0 sgn 340 !; 27 ?; 161 :)
% Comments :
%------------------------------------------------------------------------------
fof(f57,axiom,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( net_str(X1,X0)
& ~ empty_carrier(X1) )
=> ! [X2] :
( is_eventually_in(X0,X1,X2)
<=> ? [X3] :
( ! [X4] :
( element(X4,the_carrier(X1))
=> ( related(X1,X3,X4)
=> in(apply_netmap(X0,X1,X4),X2) ) )
& element(X3,the_carrier(X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_waybel_0) ).
fof(f62,axiom,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( net_str(X1,X0)
& ~ empty_carrier(X1) )
=> ! [X2] :
( is_often_in(X0,X1,X2)
<=> ! [X3] :
( element(X3,the_carrier(X1))
=> ? [X4] :
( in(apply_netmap(X0,X1,X4),X2)
& related(X1,X3,X4)
& element(X4,the_carrier(X1)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d12_waybel_0) ).
fof(f121,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f123,axiom,
! [X0,X1,X2] :
( X2 = set_intersection2(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X1)
& in(X3,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f173,axiom,
! [X0,X1] :
( ( latt_str(X0)
& ~ empty_carrier(X0) )
=> element(join_of_latt_set(X0,X1),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k15_lattice3) ).
fof(f438,axiom,
! [X0] : identity_as_relation_of(X0) = identity_relation(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_partfun1) ).
fof(f610,axiom,
! [X0,X1] :
( in(X1,X0)
=> apply(identity_relation(X0),X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t35_funct_1) ).
fof(f613,axiom,
! [X0,X1] :
( set_difference(X0,X1) = empty_set
<=> subset(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t37_xboole_1) ).
fof(f619,axiom,
! [X0] : set_difference(X0,empty_set) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_boole) ).
fof(f647,axiom,
! [X0,X1] : set_difference(X0,set_difference(X0,X1)) = set_intersection2(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f702,conjecture,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( net_str(X1,X0)
& ~ empty_carrier(X1) )
=> ! [X2,X3] :
( subset(X2,X3)
=> ( ( is_often_in(X0,X1,X2)
=> is_often_in(X0,X1,X3) )
& ( is_eventually_in(X0,X1,X2)
=> is_eventually_in(X0,X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_waybel_0) ).
fof(f703,negated_conjecture,
~ ! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( net_str(X1,X0)
& ~ empty_carrier(X1) )
=> ! [X2,X3] :
( subset(X2,X3)
=> ( ( is_often_in(X0,X1,X2)
=> is_often_in(X0,X1,X3) )
& ( is_eventually_in(X0,X1,X2)
=> is_eventually_in(X0,X1,X3) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f702]) ).
fof(f1001,plain,
! [X0,X1] :
( ~ in(X1,X0)
| apply(identity_relation(X0),X1) = X1 ),
inference(ennf_transformation,[],[f610]) ).
fof(f1093,plain,
? [X0] :
( one_sorted_str(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( net_str(X1,X0)
& ~ empty_carrier(X1)
& ? [X2,X3] :
( subset(X2,X3)
& ( ( is_often_in(X0,X1,X2)
& ~ is_often_in(X0,X1,X3) )
| ( is_eventually_in(X0,X1,X2)
& ~ is_eventually_in(X0,X1,X3) ) ) ) ) ),
inference(ennf_transformation,[],[f703]) ).
fof(f1094,plain,
? [X0] :
( one_sorted_str(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( net_str(X1,X0)
& ~ empty_carrier(X1)
& ? [X2,X3] :
( subset(X2,X3)
& ( ( is_often_in(X0,X1,X2)
& ~ is_often_in(X0,X1,X3) )
| ( is_eventually_in(X0,X1,X2)
& ~ is_eventually_in(X0,X1,X3) ) ) ) ) ),
inference(flattening,[],[f1093]) ).
fof(f1144,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( ~ in(X2,X0)
| in(X2,X1) ) ),
inference(ennf_transformation,[],[f121]) ).
fof(f1353,plain,
! [X0,X1] :
( ~ latt_str(X0)
| empty_carrier(X0)
| element(join_of_latt_set(X0,X1),the_carrier(X0)) ),
inference(ennf_transformation,[],[f173]) ).
fof(f1354,plain,
! [X0,X1] :
( ~ latt_str(X0)
| empty_carrier(X0)
| element(join_of_latt_set(X0,X1),the_carrier(X0)) ),
inference(flattening,[],[f1353]) ).
fof(f1415,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( is_eventually_in(X0,X1,X2)
<=> ? [X3] :
( ! [X4] :
( ~ element(X4,the_carrier(X1))
| ~ related(X1,X3,X4)
| in(apply_netmap(X0,X1,X4),X2) )
& element(X3,the_carrier(X1)) ) ) ) ),
inference(ennf_transformation,[],[f57]) ).
fof(f1416,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( is_eventually_in(X0,X1,X2)
<=> ? [X3] :
( ! [X4] :
( ~ element(X4,the_carrier(X1))
| ~ related(X1,X3,X4)
| in(apply_netmap(X0,X1,X4),X2) )
& element(X3,the_carrier(X1)) ) ) ) ),
inference(flattening,[],[f1415]) ).
fof(f1417,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( is_often_in(X0,X1,X2)
<=> ! [X3] :
( ~ element(X3,the_carrier(X1))
| ? [X4] :
( in(apply_netmap(X0,X1,X4),X2)
& related(X1,X3,X4)
& element(X4,the_carrier(X1)) ) ) ) ) ),
inference(ennf_transformation,[],[f62]) ).
fof(f1418,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( is_often_in(X0,X1,X2)
<=> ! [X3] :
( ~ element(X3,the_carrier(X1))
| ? [X4] :
( in(apply_netmap(X0,X1,X4),X2)
& related(X1,X3,X4)
& element(X4,the_carrier(X1)) ) ) ) ) ),
inference(flattening,[],[f1417]) ).
fof(f1828,plain,
! [X0,X1] :
( ( empty_set != set_difference(X0,X1)
| subset(X0,X1) )
& ( ~ subset(X0,X1)
| set_difference(X0,X1) = empty_set ) ),
inference(nnf_transformation,[],[f613]) ).
fof(f1870,plain,
( one_sorted_str(sK205)
& ~ empty_carrier(sK205)
& net_str(sK206,sK205)
& ~ empty_carrier(sK206)
& subset(sK207,sK208)
& ( ( is_often_in(sK205,sK206,sK207)
& ~ is_often_in(sK205,sK206,sK208) )
| ( is_eventually_in(sK205,sK206,sK207)
& ~ is_eventually_in(sK205,sK206,sK208) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK205,sK206,sK207,sK208]),skolemize(X0,sK205),skolemize(X1,sK206),skolemize(X2,sK207),skolemize(X3,sK208)],[f1094]) ).
fof(f1934,plain,
! [X0,X1] :
( ( ~ subset(X0,X1)
| ! [X2] :
( ~ in(X2,X0)
| in(X2,X1) ) )
& ( ? [X2] :
( in(X2,X0)
& ~ in(X2,X1) )
| subset(X0,X1) ) ),
inference(nnf_transformation,[],[f1144]) ).
fof(f1935,plain,
! [X0,X1] :
( ( ~ subset(X0,X1)
| ! [X3] :
( ~ in(X3,X0)
| in(X3,X1) ) )
& ( ? [X2] :
( in(X2,X0)
& ~ in(X2,X1) )
| subset(X0,X1) ) ),
inference(rectify,[],[f1934]) ).
fof(f1936,plain,
! [X0,X1] :
( ( ~ subset(X0,X1)
| ! [X3] :
( ~ in(X3,X0)
| in(X3,X1) ) )
& ( ( in(sK257(X0,X1),X0)
& ~ in(sK257(X0,X1),X1) )
| subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK257]),skolemize(X2,sK257(X0,X1))],[f1935]) ).
fof(f2102,plain,
! [X0,X1,X2] :
( ( set_intersection2(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_intersection2(X0,X1) ) ),
inference(nnf_transformation,[],[f123]) ).
fof(f2103,plain,
! [X0,X1,X2] :
( ( set_intersection2(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_intersection2(X0,X1) ) ),
inference(flattening,[],[f2102]) ).
fof(f2104,plain,
! [X0,X1,X2] :
( ( set_intersection2(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_intersection2(X0,X1) ) ),
inference(rectify,[],[f2103]) ).
fof(f2105,plain,
! [X0,X1,X2] :
( ( set_intersection2(X0,X1) != X2
| ! [X4] :
( ( ~ in(X4,X2)
| ( in(X4,X1)
& in(X4,X0) ) )
& ( ~ in(X4,X1)
| ~ in(X4,X0)
| in(X4,X2) ) ) )
& ( ( ( in(sK418(X0,X1,X2),X2)
| ( in(sK418(X0,X1,X2),X1)
& in(sK418(X0,X1,X2),X0) ) )
& ( ~ in(sK418(X0,X1,X2),X2)
| ~ in(sK418(X0,X1,X2),X1)
| ~ in(sK418(X0,X1,X2),X0) ) )
| X2 = set_intersection2(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK418]),skolemize(X3,sK418(X0,X1,X2))],[f2104]) ).
fof(f2238,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( ( ~ is_eventually_in(X0,X1,X2)
| ? [X3] :
( ! [X4] :
( ~ element(X4,the_carrier(X1))
| ~ related(X1,X3,X4)
| in(apply_netmap(X0,X1,X4),X2) )
& element(X3,the_carrier(X1)) ) )
& ( ! [X3] :
( ? [X4] :
( element(X4,the_carrier(X1))
& related(X1,X3,X4)
& ~ in(apply_netmap(X0,X1,X4),X2) )
| ~ element(X3,the_carrier(X1)) )
| is_eventually_in(X0,X1,X2) ) ) ) ),
inference(nnf_transformation,[],[f1416]) ).
fof(f2239,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( ( ~ is_eventually_in(X0,X1,X2)
| ? [X5] :
( ! [X6] :
( ~ element(X6,the_carrier(X1))
| ~ related(X1,X5,X6)
| in(apply_netmap(X0,X1,X6),X2) )
& element(X5,the_carrier(X1)) ) )
& ( ! [X3] :
( ? [X4] :
( element(X4,the_carrier(X1))
& related(X1,X3,X4)
& ~ in(apply_netmap(X0,X1,X4),X2) )
| ~ element(X3,the_carrier(X1)) )
| is_eventually_in(X0,X1,X2) ) ) ) ),
inference(rectify,[],[f2238]) ).
fof(f2240,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( ( ~ is_eventually_in(X0,X1,X2)
| ( ! [X6] :
( ~ element(X6,the_carrier(X1))
| ~ related(X1,sK488(X0,X1,X2),X6)
| in(apply_netmap(X0,X1,X6),X2) )
& element(sK488(X0,X1,X2),the_carrier(X1)) ) )
& ( ! [X3] :
( ( element(sK487(X0,X1,X2,X3),the_carrier(X1))
& related(X1,X3,sK487(X0,X1,X2,X3))
& ~ in(apply_netmap(X0,X1,sK487(X0,X1,X2,X3)),X2) )
| ~ element(X3,the_carrier(X1)) )
| is_eventually_in(X0,X1,X2) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK487,sK488]),skolemize(X4,sK487(X0,X1,X2,X3)),skolemize(X5,sK488(X0,X1,X2))],[f2239]) ).
fof(f2241,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( ( ~ is_often_in(X0,X1,X2)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| ? [X4] :
( in(apply_netmap(X0,X1,X4),X2)
& related(X1,X3,X4)
& element(X4,the_carrier(X1)) ) ) )
& ( ? [X3] :
( element(X3,the_carrier(X1))
& ! [X4] :
( ~ in(apply_netmap(X0,X1,X4),X2)
| ~ related(X1,X3,X4)
| ~ element(X4,the_carrier(X1)) ) )
| is_often_in(X0,X1,X2) ) ) ) ),
inference(nnf_transformation,[],[f1418]) ).
fof(f2242,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( ( ~ is_often_in(X0,X1,X2)
| ! [X5] :
( ~ element(X5,the_carrier(X1))
| ? [X6] :
( in(apply_netmap(X0,X1,X6),X2)
& related(X1,X5,X6)
& element(X6,the_carrier(X1)) ) ) )
& ( ? [X3] :
( element(X3,the_carrier(X1))
& ! [X4] :
( ~ in(apply_netmap(X0,X1,X4),X2)
| ~ related(X1,X3,X4)
| ~ element(X4,the_carrier(X1)) ) )
| is_often_in(X0,X1,X2) ) ) ) ),
inference(rectify,[],[f2241]) ).
fof(f2243,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( ( ~ is_often_in(X0,X1,X2)
| ! [X5] :
( ~ element(X5,the_carrier(X1))
| ( in(apply_netmap(X0,X1,sK490(X0,X1,X2,X5)),X2)
& related(X1,X5,sK490(X0,X1,X2,X5))
& element(sK490(X0,X1,X2,X5),the_carrier(X1)) ) ) )
& ( ( element(sK489(X0,X1,X2),the_carrier(X1))
& ! [X4] :
( ~ in(apply_netmap(X0,X1,X4),X2)
| ~ related(X1,sK489(X0,X1,X2),X4)
| ~ element(X4,the_carrier(X1)) ) )
| is_often_in(X0,X1,X2) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK489,sK490]),skolemize(X3,sK489(X0,X1,X2)),skolemize(X6,sK490(X0,X1,X2,X5))],[f2242]) ).
fof(f2754,plain,
! [X0,X1] :
( ~ in(X1,X0)
| apply(identity_relation(X0),X1) = X1 ),
inference(cnf_transformation,[],[f1001]) ).
fof(f2759,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| empty_set = set_difference(X0,X1) ),
inference(cnf_transformation,[],[f1828]) ).
fof(f2810,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1)),
inference(cnf_transformation,[],[f647]) ).
fof(f2892,plain,
one_sorted_str(sK205),
inference(cnf_transformation,[],[f1870]) ).
fof(f2893,plain,
~ empty_carrier(sK205),
inference(cnf_transformation,[],[f1870]) ).
fof(f2894,plain,
net_str(sK206,sK205),
inference(cnf_transformation,[],[f1870]) ).
fof(f2895,plain,
~ empty_carrier(sK206),
inference(cnf_transformation,[],[f1870]) ).
fof(f2896,plain,
subset(sK207,sK208),
inference(cnf_transformation,[],[f1870]) ).
fof(f2897,plain,
( is_often_in(sK205,sK206,sK207)
| is_eventually_in(sK205,sK206,sK207) ),
inference(cnf_transformation,[],[f1870]) ).
fof(f2898,plain,
( ~ is_often_in(sK205,sK206,sK208)
| is_eventually_in(sK205,sK206,sK207) ),
inference(cnf_transformation,[],[f1870]) ).
fof(f2899,plain,
( is_often_in(sK205,sK206,sK207)
| ~ is_eventually_in(sK205,sK206,sK208) ),
inference(cnf_transformation,[],[f1870]) ).
fof(f2900,plain,
( ~ is_often_in(sK205,sK206,sK208)
| ~ is_eventually_in(sK205,sK206,sK208) ),
inference(cnf_transformation,[],[f1870]) ).
fof(f3046,plain,
! [X3,X0,X1] :
( ~ subset(X0,X1)
| ~ in(X3,X0)
| in(X3,X1) ),
inference(cnf_transformation,[],[f1936]) ).
fof(f3071,plain,
! [X0] : set_difference(X0,empty_set) = X0,
inference(cnf_transformation,[],[f619]) ).
fof(f3461,plain,
! [X2,X0,X1,X4] :
( set_intersection2(X0,X1) != X2
| ~ in(X4,X2)
| in(X4,X1) ),
inference(cnf_transformation,[],[f2105]) ).
fof(f3691,plain,
! [X0,X1] :
( ~ latt_str(X0)
| empty_carrier(X0)
| element(join_of_latt_set(X0,X1),the_carrier(X0)) ),
inference(cnf_transformation,[],[f1354]) ).
fof(f3810,plain,
! [X2,X0,X1,X6] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ is_eventually_in(X0,X1,X2)
| ~ element(X6,the_carrier(X1))
| ~ related(X1,sK488(X0,X1,X2),X6)
| in(apply_netmap(X0,X1,X6),X2) ),
inference(cnf_transformation,[],[f2240]) ).
fof(f3811,plain,
! [X2,X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ is_eventually_in(X0,X1,X2)
| element(sK488(X0,X1,X2),the_carrier(X1)) ),
inference(cnf_transformation,[],[f2240]) ).
fof(f3812,plain,
! [X2,X3,X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| element(sK487(X0,X1,X2,X3),the_carrier(X1))
| ~ element(X3,the_carrier(X1))
| is_eventually_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f2240]) ).
fof(f3813,plain,
! [X2,X3,X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| related(X1,X3,sK487(X0,X1,X2,X3))
| ~ element(X3,the_carrier(X1))
| is_eventually_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f2240]) ).
fof(f3814,plain,
! [X2,X3,X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ in(apply_netmap(X0,X1,sK487(X0,X1,X2,X3)),X2)
| ~ element(X3,the_carrier(X1))
| is_eventually_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f2240]) ).
fof(f3815,plain,
! [X2,X0,X1,X5] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ is_often_in(X0,X1,X2)
| ~ element(X5,the_carrier(X1))
| in(apply_netmap(X0,X1,sK490(X0,X1,X2,X5)),X2) ),
inference(cnf_transformation,[],[f2243]) ).
fof(f3816,plain,
! [X2,X0,X1,X5] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ is_often_in(X0,X1,X2)
| ~ element(X5,the_carrier(X1))
| related(X1,X5,sK490(X0,X1,X2,X5)) ),
inference(cnf_transformation,[],[f2243]) ).
fof(f3817,plain,
! [X2,X0,X1,X5] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ is_often_in(X0,X1,X2)
| ~ element(X5,the_carrier(X1))
| element(sK490(X0,X1,X2,X5),the_carrier(X1)) ),
inference(cnf_transformation,[],[f2243]) ).
fof(f3818,plain,
! [X2,X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| element(sK489(X0,X1,X2),the_carrier(X1))
| is_often_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f2243]) ).
fof(f3819,plain,
! [X2,X0,X1,X4] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ in(apply_netmap(X0,X1,X4),X2)
| ~ related(X1,sK489(X0,X1,X2),X4)
| ~ element(X4,the_carrier(X1))
| is_often_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f2243]) ).
fof(f4005,plain,
! [X0] : identity_relation(X0) = identity_as_relation_of(X0),
inference(cnf_transformation,[],[f438]) ).
fof(f4221,plain,
! [X0,X1] :
( ~ in(X1,X0)
| apply(identity_as_relation_of(X0),X1) = X1 ),
inference(definition_unfolding,[],[f2754,f4005]) ).
fof(f4386,plain,
! [X2,X0,X1,X4] :
( set_difference(X0,set_difference(X0,X1)) != X2
| ~ in(X4,X2)
| in(X4,X1) ),
inference(definition_unfolding,[],[f3461,f2810]) ).
fof(f4682,plain,
! [X0,X1,X4] :
( ~ in(X4,set_difference(X0,set_difference(X0,X1)))
| in(X4,X1) ),
inference(equality_resolution,[],[f4386]) ).
tcf(c_519,plain,
! [X0: $i,X1: $i] :
( ( apply(identity_as_relation_of(X1),X0) = X0 )
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f4221]) ).
tcf(c_523,plain,
! [X0: $i,X1: $i] :
( ( set_difference(X0,X1) = empty_set )
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f2759]) ).
tcf(c_655,negated_conjecture,
( ~ is_often_in(sK205,sK206,sK208)
| ~ is_eventually_in(sK205,sK206,sK208) ),
inference(cnf_transformation,[],[f2900]) ).
tcf(c_656,negated_conjecture,
( is_often_in(sK205,sK206,sK207)
| ~ is_eventually_in(sK205,sK206,sK208) ),
inference(cnf_transformation,[],[f2899]) ).
tcf(c_657,negated_conjecture,
( is_eventually_in(sK205,sK206,sK207)
| ~ is_often_in(sK205,sK206,sK208) ),
inference(cnf_transformation,[],[f2898]) ).
tcf(c_658,negated_conjecture,
( is_often_in(sK205,sK206,sK207)
| is_eventually_in(sK205,sK206,sK207) ),
inference(cnf_transformation,[],[f2897]) ).
tcf(c_659,negated_conjecture,
subset(sK207,sK208),
inference(cnf_transformation,[],[f2896]) ).
tcf(c_660,negated_conjecture,
~ empty_carrier(sK206),
inference(cnf_transformation,[],[f2895]) ).
tcf(c_661,negated_conjecture,
net_str(sK206,sK205),
inference(cnf_transformation,[],[f2894]) ).
tcf(c_662,negated_conjecture,
~ empty_carrier(sK205),
inference(cnf_transformation,[],[f2893]) ).
tcf(c_663,negated_conjecture,
one_sorted_str(sK205),
inference(cnf_transformation,[],[f2892]) ).
tcf(c_808,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,X2)
| ~ subset(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f3046]) ).
tcf(c_831,plain,
! [X0: $i] : set_difference(X0,empty_set) = X0,
inference(cnf_transformation,[],[f3071]) ).
tcf(c_1225,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,X2)
| ~ in(X0,set_difference(X1,set_difference(X1,X2))) ),
inference(cnf_transformation,[],[f4682]) ).
tcf(c_1450,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X0)
| element(join_of_latt_set(X0,X1),the_carrier(X0))
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f3691]) ).
tcf(c_1567,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| is_eventually_in(X0,X1,X2)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| ~ element(X3,the_carrier(X1))
| ~ in(apply_netmap(X0,X1,sK487(X0,X1,X2,X3)),X2) ),
inference(cnf_transformation,[],[f3814]) ).
tcf(c_1568,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| is_eventually_in(X2,X1,X3)
| related(X1,X0,sK487(X2,X1,X3,X0))
| ~ one_sorted_str(X2)
| ~ net_str(X1,X2)
| ~ element(X0,the_carrier(X1)) ),
inference(cnf_transformation,[],[f3813]) ).
tcf(c_1569,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| is_eventually_in(X2,X1,X3)
| element(sK487(X2,X1,X3,X0),the_carrier(X1))
| ~ one_sorted_str(X2)
| ~ net_str(X1,X2)
| ~ element(X0,the_carrier(X1)) ),
inference(cnf_transformation,[],[f3812]) ).
tcf(c_1570,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| element(sK488(X0,X1,X2),the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| ~ is_eventually_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f3811]) ).
tcf(c_1571,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| in(apply_netmap(X1,X0,X3),X2)
| ~ one_sorted_str(X1)
| ~ net_str(X0,X1)
| ~ element(X3,the_carrier(X0))
| ~ is_eventually_in(X1,X0,X2)
| ~ related(X0,sK488(X1,X0,X2),X3) ),
inference(cnf_transformation,[],[f3810]) ).
tcf(c_1572,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| is_often_in(X1,X0,X2)
| ~ one_sorted_str(X1)
| ~ net_str(X0,X1)
| ~ element(X3,the_carrier(X0))
| ~ in(apply_netmap(X1,X0,X3),X2)
| ~ related(X0,sK489(X1,X0,X2),X3) ),
inference(cnf_transformation,[],[f3819]) ).
tcf(c_1573,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| is_often_in(X1,X0,X2)
| element(sK489(X1,X0,X2),the_carrier(X0))
| ~ one_sorted_str(X1)
| ~ net_str(X0,X1) ),
inference(cnf_transformation,[],[f3818]) ).
tcf(c_1574,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| element(sK490(X0,X1,X2,X3),the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| ~ element(X3,the_carrier(X1))
| ~ is_often_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f3817]) ).
tcf(c_1575,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| related(X1,X3,sK490(X0,X1,X2,X3))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| ~ element(X3,the_carrier(X1))
| ~ is_often_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f3816]) ).
tcf(c_1576,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| in(apply_netmap(X0,X1,sK490(X0,X1,X2,X3)),X2)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| ~ element(X3,the_carrier(X1))
| ~ is_often_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f3815]) ).
tcf(c_3833,plain,
( ~ is_often_in(sK205,sK206,sK208)
| ~ is_eventually_in(sK205,sK206,sK208) ),
inference(prop_impl_just,[status(thm)],[c_655]) ).
tcf(c_3839,plain,
( is_eventually_in(sK205,sK206,sK207)
| ~ is_often_in(sK205,sK206,sK208) ),
inference(prop_impl_just,[status(thm)],[c_657]) ).
tcf(c_46250,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| is_often_in(X0,X1,X2)
| element(sK489(X0,X1,X2),the_carrier(X1))
| ~ one_sorted_str(X0)
| ( X1 != sK206 )
| ( X0 != sK205 ) ),
inference(resolution_lifted,[status(thm)],[c_661,c_1573]) ).
tcf(c_46251,plain,
! [X0: $i] :
( empty_carrier(sK206)
| empty_carrier(sK205)
| is_often_in(sK205,sK206,X0)
| element(sK489(sK205,sK206,X0),the_carrier(sK206))
| ~ one_sorted_str(sK205) ),
inference(unflattening,[status(thm)],[c_46250]) ).
tcf(c_46253,plain,
! [X0: $i] :
( is_often_in(sK205,sK206,X0)
| element(sK489(sK205,sK206,X0),the_carrier(sK206)) ),
inference(global_subsumption_just,[status(thm)],[c_46251,c_663,c_662,c_660,c_46251]) ).
tcf(c_46262,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| is_often_in(X0,X1,X2)
| ~ one_sorted_str(X0)
| ~ element(X3,the_carrier(X1))
| ~ in(apply_netmap(X0,X1,X3),X2)
| ~ related(X1,sK489(X0,X1,X2),X3)
| ( X1 != sK206 )
| ( X0 != sK205 ) ),
inference(resolution_lifted,[status(thm)],[c_661,c_1572]) ).
tcf(c_46263,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK206)
| empty_carrier(sK205)
| is_often_in(sK205,sK206,X0)
| ~ one_sorted_str(sK205)
| ~ element(X1,the_carrier(sK206))
| ~ in(apply_netmap(sK205,sK206,X1),X0)
| ~ related(sK206,sK489(sK205,sK206,X0),X1) ),
inference(unflattening,[status(thm)],[c_46262]) ).
tcf(c_46265,plain,
! [X0: $i,X1: $i] :
( is_often_in(sK205,sK206,X0)
| ~ related(sK206,sK489(sK205,sK206,X0),X1)
| ~ in(apply_netmap(sK205,sK206,X1),X0)
| ~ element(X1,the_carrier(sK206)) ),
inference(global_subsumption_just,[status(thm)],[c_46263,c_663,c_662,c_660,c_46263]) ).
tcf(c_46266,plain,
! [X0: $i,X1: $i] :
( is_often_in(sK205,sK206,X0)
| ~ element(X1,the_carrier(sK206))
| ~ in(apply_netmap(sK205,sK206,X1),X0)
| ~ related(sK206,sK489(sK205,sK206,X0),X1) ),
inference(renaming,[status(thm)],[c_46265]) ).
tcf(c_46280,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| in(apply_netmap(X0,X1,X3),X2)
| ~ one_sorted_str(X0)
| ~ element(X3,the_carrier(X1))
| ~ is_eventually_in(X0,X1,X2)
| ~ related(X1,sK488(X0,X1,X2),X3)
| ( X1 != sK206 )
| ( X0 != sK205 ) ),
inference(resolution_lifted,[status(thm)],[c_661,c_1571]) ).
tcf(c_46281,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK206)
| empty_carrier(sK205)
| in(apply_netmap(sK205,sK206,X1),X0)
| ~ one_sorted_str(sK205)
| ~ is_eventually_in(sK205,sK206,X0)
| ~ element(X1,the_carrier(sK206))
| ~ related(sK206,sK488(sK205,sK206,X0),X1) ),
inference(unflattening,[status(thm)],[c_46280]) ).
tcf(c_46283,plain,
! [X0: $i,X1: $i] :
( in(apply_netmap(sK205,sK206,X1),X0)
| ~ related(sK206,sK488(sK205,sK206,X0),X1)
| ~ element(X1,the_carrier(sK206))
| ~ is_eventually_in(sK205,sK206,X0) ),
inference(global_subsumption_just,[status(thm)],[c_46281,c_663,c_662,c_660,c_46281]) ).
tcf(c_46284,plain,
! [X0: $i,X1: $i] :
( in(apply_netmap(sK205,sK206,X1),X0)
| ~ is_eventually_in(sK205,sK206,X0)
| ~ element(X1,the_carrier(sK206))
| ~ related(sK206,sK488(sK205,sK206,X0),X1) ),
inference(renaming,[status(thm)],[c_46283]) ).
tcf(c_46305,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| in(apply_netmap(X0,X1,sK490(X0,X1,X2,X3)),X2)
| ~ one_sorted_str(X0)
| ~ element(X3,the_carrier(X1))
| ~ is_often_in(X0,X1,X2)
| ( X1 != sK206 )
| ( X0 != sK205 ) ),
inference(resolution_lifted,[status(thm)],[c_661,c_1576]) ).
tcf(c_46306,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK206)
| empty_carrier(sK205)
| in(apply_netmap(sK205,sK206,sK490(sK205,sK206,X1,X0)),X1)
| ~ one_sorted_str(sK205)
| ~ is_often_in(sK205,sK206,X1)
| ~ element(X0,the_carrier(sK206)) ),
inference(unflattening,[status(thm)],[c_46305]) ).
tcf(c_46308,plain,
! [X0: $i,X1: $i] :
( in(apply_netmap(sK205,sK206,sK490(sK205,sK206,X1,X0)),X1)
| ~ element(X0,the_carrier(sK206))
| ~ is_often_in(sK205,sK206,X1) ),
inference(global_subsumption_just,[status(thm)],[c_46306,c_663,c_662,c_660,c_46306]) ).
tcf(c_46309,plain,
! [X0: $i,X1: $i] :
( in(apply_netmap(sK205,sK206,sK490(sK205,sK206,X1,X0)),X1)
| ~ is_often_in(sK205,sK206,X1)
| ~ element(X0,the_carrier(sK206)) ),
inference(renaming,[status(thm)],[c_46308]) ).
tcf(c_46320,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| related(X1,X3,sK490(X0,X1,X2,X3))
| ~ one_sorted_str(X0)
| ~ element(X3,the_carrier(X1))
| ~ is_often_in(X0,X1,X2)
| ( X1 != sK206 )
| ( X0 != sK205 ) ),
inference(resolution_lifted,[status(thm)],[c_661,c_1575]) ).
tcf(c_46321,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK206)
| empty_carrier(sK205)
| related(sK206,X0,sK490(sK205,sK206,X1,X0))
| ~ one_sorted_str(sK205)
| ~ is_often_in(sK205,sK206,X1)
| ~ element(X0,the_carrier(sK206)) ),
inference(unflattening,[status(thm)],[c_46320]) ).
tcf(c_46323,plain,
! [X0: $i,X1: $i] :
( related(sK206,X0,sK490(sK205,sK206,X1,X0))
| ~ element(X0,the_carrier(sK206))
| ~ is_often_in(sK205,sK206,X1) ),
inference(global_subsumption_just,[status(thm)],[c_46321,c_663,c_662,c_660,c_46321]) ).
tcf(c_46324,plain,
! [X0: $i,X1: $i] :
( related(sK206,X0,sK490(sK205,sK206,X1,X0))
| ~ is_often_in(sK205,sK206,X1)
| ~ element(X0,the_carrier(sK206)) ),
inference(renaming,[status(thm)],[c_46323]) ).
tcf(c_46335,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| element(sK490(X0,X1,X2,X3),the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ element(X3,the_carrier(X1))
| ~ is_often_in(X0,X1,X2)
| ( X1 != sK206 )
| ( X0 != sK205 ) ),
inference(resolution_lifted,[status(thm)],[c_661,c_1574]) ).
tcf(c_46336,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK206)
| empty_carrier(sK205)
| element(sK490(sK205,sK206,X1,X0),the_carrier(sK206))
| ~ one_sorted_str(sK205)
| ~ is_often_in(sK205,sK206,X1)
| ~ element(X0,the_carrier(sK206)) ),
inference(unflattening,[status(thm)],[c_46335]) ).
tcf(c_46338,plain,
! [X0: $i,X1: $i] :
( element(sK490(sK205,sK206,X1,X0),the_carrier(sK206))
| ~ element(X0,the_carrier(sK206))
| ~ is_often_in(sK205,sK206,X1) ),
inference(global_subsumption_just,[status(thm)],[c_46336,c_663,c_662,c_660,c_46336]) ).
tcf(c_46339,plain,
! [X0: $i,X1: $i] :
( element(sK490(sK205,sK206,X1,X0),the_carrier(sK206))
| ~ is_often_in(sK205,sK206,X1)
| ~ element(X0,the_carrier(sK206)) ),
inference(renaming,[status(thm)],[c_46338]) ).
tcf(c_46350,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| element(sK488(X0,X1,X2),the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ is_eventually_in(X0,X1,X2)
| ( X1 != sK206 )
| ( X0 != sK205 ) ),
inference(resolution_lifted,[status(thm)],[c_661,c_1570]) ).
tcf(c_46351,plain,
! [X0: $i] :
( empty_carrier(sK206)
| empty_carrier(sK205)
| element(sK488(sK205,sK206,X0),the_carrier(sK206))
| ~ one_sorted_str(sK205)
| ~ is_eventually_in(sK205,sK206,X0) ),
inference(unflattening,[status(thm)],[c_46350]) ).
tcf(c_46362,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| is_eventually_in(X0,X1,X2)
| ~ one_sorted_str(X0)
| ~ element(X3,the_carrier(X1))
| ~ in(apply_netmap(X0,X1,sK487(X0,X1,X2,X3)),X2)
| ( X1 != sK206 )
| ( X0 != sK205 ) ),
inference(resolution_lifted,[status(thm)],[c_661,c_1567]) ).
tcf(c_46363,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK206)
| empty_carrier(sK205)
| is_eventually_in(sK205,sK206,X0)
| ~ one_sorted_str(sK205)
| ~ element(X1,the_carrier(sK206))
| ~ in(apply_netmap(sK205,sK206,sK487(sK205,sK206,X0,X1)),X0) ),
inference(unflattening,[status(thm)],[c_46362]) ).
tcf(c_46365,plain,
! [X0: $i,X1: $i] :
( is_eventually_in(sK205,sK206,X0)
| ~ in(apply_netmap(sK205,sK206,sK487(sK205,sK206,X0,X1)),X0)
| ~ element(X1,the_carrier(sK206)) ),
inference(global_subsumption_just,[status(thm)],[c_46363,c_663,c_662,c_660,c_46363]) ).
tcf(c_46366,plain,
! [X0: $i,X1: $i] :
( is_eventually_in(sK205,sK206,X0)
| ~ element(X1,the_carrier(sK206))
| ~ in(apply_netmap(sK205,sK206,sK487(sK205,sK206,X0,X1)),X0) ),
inference(renaming,[status(thm)],[c_46365]) ).
tcf(c_46389,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| is_eventually_in(X0,X1,X3)
| element(sK487(X0,X1,X3,X2),the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ element(X2,the_carrier(X1))
| ( X1 != sK206 )
| ( X0 != sK205 ) ),
inference(resolution_lifted,[status(thm)],[c_661,c_1569]) ).
tcf(c_46390,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK206)
| empty_carrier(sK205)
| is_eventually_in(sK205,sK206,X1)
| element(sK487(sK205,sK206,X1,X0),the_carrier(sK206))
| ~ one_sorted_str(sK205)
| ~ element(X0,the_carrier(sK206)) ),
inference(unflattening,[status(thm)],[c_46389]) ).
tcf(c_46392,plain,
! [X0: $i,X1: $i] :
( is_eventually_in(sK205,sK206,X1)
| element(sK487(sK205,sK206,X1,X0),the_carrier(sK206))
| ~ element(X0,the_carrier(sK206)) ),
inference(global_subsumption_just,[status(thm)],[c_46390,c_663,c_662,c_660,c_46390]) ).
tcf(c_46404,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| is_eventually_in(X0,X1,X3)
| related(X1,X2,sK487(X0,X1,X3,X2))
| ~ one_sorted_str(X0)
| ~ element(X2,the_carrier(X1))
| ( X1 != sK206 )
| ( X0 != sK205 ) ),
inference(resolution_lifted,[status(thm)],[c_661,c_1568]) ).
tcf(c_46405,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK206)
| empty_carrier(sK205)
| is_eventually_in(sK205,sK206,X1)
| related(sK206,X0,sK487(sK205,sK206,X1,X0))
| ~ one_sorted_str(sK205)
| ~ element(X0,the_carrier(sK206)) ),
inference(unflattening,[status(thm)],[c_46404]) ).
tcf(c_46407,plain,
! [X0: $i,X1: $i] :
( is_eventually_in(sK205,sK206,X1)
| related(sK206,X0,sK487(sK205,sK206,X1,X0))
| ~ element(X0,the_carrier(sK206)) ),
inference(global_subsumption_just,[status(thm)],[c_46405,c_663,c_662,c_660,c_46405]) ).
tcf(c_69768,plain,
! [X0: $i] :
( is_eventually_in(sK205,sK206,sK207)
| element(sK489(sK205,sK206,X0),the_carrier(sK206))
| ( sK206 != sK206 )
| ( sK205 != sK205 )
| ( X0 != sK208 ) ),
inference(resolution_lifted,[status(thm)],[c_3839,c_46253]) ).
tcf(c_69769,plain,
( is_eventually_in(sK205,sK206,sK207)
| element(sK489(sK205,sK206,sK208),the_carrier(sK206)) ),
inference(unflattening,[status(thm)],[c_69768]) ).
tcf(c_69791,plain,
! [X0: $i] :
( element(sK489(sK205,sK206,X0),the_carrier(sK206))
| ~ is_eventually_in(sK205,sK206,sK208)
| ( sK206 != sK206 )
| ( sK205 != sK205 )
| ( X0 != sK208 ) ),
inference(resolution_lifted,[status(thm)],[c_3833,c_46253]) ).
tcf(c_69792,plain,
( element(sK489(sK205,sK206,sK208),the_carrier(sK206))
| ~ is_eventually_in(sK205,sK206,sK208) ),
inference(unflattening,[status(thm)],[c_69791]) ).
tcf(c_98531,plain,
! [X0: $i] :
( element(sK488(sK205,sK206,X0),the_carrier(sK206))
| ~ is_eventually_in(sK205,sK206,X0) ),
inference(prop_impl_just,[status(thm)],[c_663,c_662,c_660,c_46351]) ).
tcf(c_209309,plain,
! [X0: $i,X1: $i] :
( is_often_in(sK205,sK206,X1)
| ~ is_often_in(sK205,sK206,X0)
| ~ element(sK489(sK205,sK206,X1),the_carrier(sK206))
| ~ element(sK490(sK205,sK206,X0,sK489(sK205,sK206,X1)),the_carrier(sK206))
| ~ in(apply_netmap(sK205,sK206,sK490(sK205,sK206,X0,sK489(sK205,sK206,X1))),X1) ),
inference(superposition,[status(thm)],[c_46324,c_46266]) ).
tcf(c_209385,plain,
! [X0: $i,X1: $i] :
( is_often_in(sK205,sK206,X1)
| ~ is_often_in(sK205,sK206,X0)
| ~ element(sK489(sK205,sK206,X1),the_carrier(sK206))
| ~ in(apply_netmap(sK205,sK206,sK490(sK205,sK206,X0,sK489(sK205,sK206,X1))),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_209309,c_46339]) ).
tcf(c_219297,plain,
! [X0: $i] :
( is_eventually_in(sK205,sK206,sK208)
| element(sK487(sK205,sK206,sK208,X0),the_carrier(sK206))
| ~ element(X0,the_carrier(sK206)) ),
inference(instantiation,[status(thm)],[c_46392]) ).
tcf(c_219321,plain,
! [X0: $i] :
( is_eventually_in(sK205,sK206,sK208)
| ~ element(X0,the_carrier(sK206))
| ~ in(apply_netmap(sK205,sK206,sK487(sK205,sK206,sK208,X0)),sK208) ),
inference(instantiation,[status(thm)],[c_46366]) ).
tcf(c_219336,plain,
! [X0: $i] :
( is_eventually_in(sK205,sK206,sK208)
| related(sK206,X0,sK487(sK205,sK206,sK208,X0))
| ~ element(X0,the_carrier(sK206)) ),
inference(instantiation,[status(thm)],[c_46407]) ).
tcf(c_225020,plain,
( element(sK488(sK205,sK206,sK207),the_carrier(sK206))
| ~ is_eventually_in(sK205,sK206,sK207) ),
inference(instantiation,[status(thm)],[c_98531]) ).
tcf(c_228942,plain,
set_difference(sK207,sK208) = empty_set,
inference(superposition,[status(thm)],[c_659,c_523]) ).
tcf(c_231393,plain,
( is_eventually_in(sK205,sK206,sK208)
| element(sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207)),the_carrier(sK206))
| ~ element(sK488(sK205,sK206,sK207),the_carrier(sK206)) ),
inference(instantiation,[status(thm)],[c_219297]) ).
tcf(c_231401,plain,
( is_eventually_in(sK205,sK206,sK208)
| ~ element(sK488(sK205,sK206,sK207),the_carrier(sK206))
| ~ in(apply_netmap(sK205,sK206,sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207))),sK208) ),
inference(instantiation,[status(thm)],[c_219321]) ).
tcf(c_238501,plain,
! [X0: $i,X1: $i] :
( ( apply(identity_as_relation_of(X1),apply_netmap(sK205,sK206,sK490(sK205,sK206,X1,X0))) = apply_netmap(sK205,sK206,sK490(sK205,sK206,X1,X0)) )
| ~ is_often_in(sK205,sK206,X1)
| ~ element(X0,the_carrier(sK206)) ),
inference(superposition,[status(thm)],[c_46309,c_519]) ).
tcf(c_238760,plain,
( is_eventually_in(sK205,sK206,sK208)
| related(sK206,sK488(sK205,sK206,sK207),sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207)))
| ~ element(sK488(sK205,sK206,sK207),the_carrier(sK206)) ),
inference(instantiation,[status(thm)],[c_219336]) ).
tcf(c_243017,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(apply_netmap(sK205,sK206,sK490(sK205,sK206,set_difference(X0,set_difference(X0,X1)),X2)),X1)
| ~ element(X2,the_carrier(sK206))
| ~ is_often_in(sK205,sK206,set_difference(X0,set_difference(X0,X1))) ),
inference(superposition,[status(thm)],[c_46309,c_1225]) ).
tcf(c_243413,plain,
! [X0: $i] :
( in(apply_netmap(sK205,sK206,sK490(sK205,sK206,set_difference(sK207,empty_set),X0)),sK208)
| ~ element(X0,the_carrier(sK206))
| ~ is_often_in(sK205,sK206,set_difference(sK207,set_difference(sK207,sK208))) ),
inference(superposition,[status(thm)],[c_228942,c_243017]) ).
tcf(c_243451,plain,
! [X0: $i] :
( in(apply_netmap(sK205,sK206,sK490(sK205,sK206,set_difference(sK207,empty_set),X0)),sK208)
| ~ element(X0,the_carrier(sK206))
| ~ is_often_in(sK205,sK206,set_difference(sK207,empty_set)) ),
inference(light_normalisation,[status(thm)],[c_243413,c_228942]) ).
tcf(c_243618,plain,
! [X0: $i] :
( in(apply_netmap(sK205,sK206,sK490(sK205,sK206,sK207,X0)),sK208)
| ~ is_often_in(sK205,sK206,sK207)
| ~ element(X0,the_carrier(sK206)) ),
inference(demodulation,[status(thm)],[c_243451,c_831]) ).
tcf(c_243638,plain,
( is_often_in(sK205,sK206,sK208)
| ~ is_often_in(sK205,sK206,sK207)
| ~ element(sK489(sK205,sK206,sK208),the_carrier(sK206)) ),
inference(superposition,[status(thm)],[c_243618,c_209385]) ).
tcf(c_245083,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK206)
| ( apply(identity_as_relation_of(X0),apply_netmap(sK205,sK206,sK490(sK205,sK206,X0,join_of_latt_set(sK206,X1)))) = apply_netmap(sK205,sK206,sK490(sK205,sK206,X0,join_of_latt_set(sK206,X1))) )
| ~ latt_str(sK206)
| ~ is_often_in(sK205,sK206,X0) ),
inference(superposition,[status(thm)],[c_1450,c_238501]) ).
tcf(c_245105,plain,
! [X0: $i,X1: $i] :
( ( apply(identity_as_relation_of(X0),apply_netmap(sK205,sK206,sK490(sK205,sK206,X0,join_of_latt_set(sK206,X1)))) = apply_netmap(sK205,sK206,sK490(sK205,sK206,X0,join_of_latt_set(sK206,X1))) )
| ~ latt_str(sK206)
| ~ is_often_in(sK205,sK206,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_245083,c_660]) ).
tcf(c_245284,plain,
! [X0: $i] :
( is_eventually_in(sK205,sK206,sK207)
| ( apply(identity_as_relation_of(sK207),apply_netmap(sK205,sK206,sK490(sK205,sK206,sK207,join_of_latt_set(sK206,X0)))) = apply_netmap(sK205,sK206,sK490(sK205,sK206,sK207,join_of_latt_set(sK206,X0))) )
| ~ latt_str(sK206) ),
inference(superposition,[status(thm)],[c_658,c_245105]) ).
tcf(c_245304,plain,
is_eventually_in(sK205,sK206,sK207),
inference(global_subsumption_just,[status(thm)],[c_245284,c_658,c_657,c_69769,c_243638]) ).
tcf(c_247193,plain,
! [X0: $i] :
( in(apply_netmap(sK205,sK206,sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207))),X0)
| ~ is_eventually_in(sK205,sK206,X0)
| ~ element(sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207)),the_carrier(sK206))
| ~ related(sK206,sK488(sK205,sK206,X0),sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207))) ),
inference(instantiation,[status(thm)],[c_46284]) ).
tcf(c_247714,negated_conjecture,
~ is_eventually_in(sK205,sK206,sK208),
inference(global_subsumption_just,[status(thm)],[c_656,c_656,c_655,c_69792,c_243638]) ).
tcf(c_260936,plain,
( in(apply_netmap(sK205,sK206,sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207))),sK207)
| ~ is_eventually_in(sK205,sK206,sK207)
| ~ element(sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207)),the_carrier(sK206))
| ~ related(sK206,sK488(sK205,sK206,sK207),sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207))) ),
inference(instantiation,[status(thm)],[c_247193]) ).
tcf(c_272994,plain,
! [X0: $i] :
( in(apply_netmap(sK205,sK206,sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207))),X0)
| ~ subset(sK207,X0)
| ~ in(apply_netmap(sK205,sK206,sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207))),sK207) ),
inference(instantiation,[status(thm)],[c_808]) ).
tcf(c_286728,plain,
( in(apply_netmap(sK205,sK206,sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207))),sK208)
| ~ subset(sK207,sK208)
| ~ in(apply_netmap(sK205,sK206,sK487(sK205,sK206,sK208,sK488(sK205,sK206,sK207))),sK207) ),
inference(instantiation,[status(thm)],[c_272994]) ).
tcf(c_286729,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_286728,c_260936,c_247714,c_245304,c_238760,c_231401,c_231393,c_225020,c_659]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU367+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.10/0.37 % Computer : n020.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 13:53:04 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 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.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 126.97/18.01 % SZS status Started for theBenchmark.p
% 126.97/18.01 % SZS status Theorem for theBenchmark.p
% 126.97/18.01
% 126.97/18.01 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 126.97/18.01
% 126.97/18.01 % ------ iProver source info
% 126.97/18.01
% 126.97/18.01 % git: date: 2026-07-19 20:42:38 +0200
% 126.97/18.01 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 126.97/18.01 % git: non_committed_changes: false
% 126.97/18.01
% 126.97/18.01 % ------ Parsing...
% 126.97/18.01 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 126.97/18.01
% 126.97/18.01 % ------ Preprocessing... sup_sim: 109 sf_s rm: 76 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sup_sim: 30 sf_s rm: 23 0s sf_e pe_s pe:1:0s pe_e %
% 126.97/18.01
% 126.97/18.01 % ------ Preprocessing... gs_s sp: 16 0s gs_e snvd_s sp: 0 0s snvd_e %
% 126.97/18.01
% 126.97/18.01 % ------ Preprocessing... sf_s rm: 5 0s sf_e sf_s rm: 0 0s sf_e
% 126.97/18.01 % ------ Proving...
% 126.97/18.01 % ------ Problem Properties
% 126.97/18.01
% 126.97/18.01 %
% 126.97/18.01 % clauses 1607
% 126.97/18.01 % conjectures 8
% 126.97/18.01 % EPR 211
% 126.97/18.01 % Horn 1147
% 126.97/18.01 % unary 190
% 126.97/18.01 % binary 428
% 126.97/18.01 % lits 5219
% 126.97/18.01 % lits eq 635
% 126.97/18.01 % fd_pure 0
% 126.97/18.01 % fd_pseudo 0
% 126.97/18.01 % fd_cond 46
% 126.97/18.01 % fd_pseudo_cond 143
% 126.97/18.01 % AC symbols 0
% 126.97/18.01
% 126.97/18.01 % ------ Schedule dynamic 5 is on
% 126.97/18.01
% 126.97/18.01 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 126.97/18.01
% 126.97/18.01
% 126.97/18.01 % ------
% 126.97/18.01 % Current options:
% 126.97/18.01 % ------
% 126.97/18.01
% 126.97/18.01
% 126.97/18.01 %
% 126.97/18.01
% 126.97/18.01 % ------ Proving...
% 126.97/18.01 %
% 126.97/18.01
% 126.97/18.01 % SZS status Theorem for theBenchmark.p
% 126.97/18.01
% 126.97/18.01 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 126.97/18.01
% 126.97/18.01
%------------------------------------------------------------------------------