%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : SEU395+2 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Tue Jul 19 08:41:51 EDT 2022
% Result : Theorem 9.32s 3.54s
% Output : CNFRefutation 9.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 25
% Syntax : Number of clauses : 88 ( 42 unt; 32 nHn; 84 RR)
% Number of literals : 307 ( 17 equ; 166 neg)
% Maximal clause size : 10 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 80 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_998,plain,
( one_sorted_str(X1)
| ~ top_str(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_998) ).
cnf(i_0_3568,negated_conjecture,
top_str(esk529_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3568) ).
cnf(i_0_641,plain,
( cast_as_carrier_subset(X1) = the_carrier(X1)
| ~ one_sorted_str(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_641) ).
cnf(i_0_3563,negated_conjecture,
element(esk530_0,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(esk529_0)))))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3563) ).
cnf(i_0_3591,lemma,
the_carrier(incl_POSet(X1)) = X1,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3591) ).
cnf(i_0_3564,negated_conjecture,
proper_element(esk530_0,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(esk529_0)))))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3564) ).
cnf(i_0_951,plain,
( empty_carrier(X1)
| empty(X2)
| empty(X3)
| net_str(net_of_bool_filter(X1,X3,X2),X1)
| ~ one_sorted_str(X1)
| ~ element(X3,powerset(the_carrier(X1)))
| ~ filtered_subset(X2,incl_POSet(powerset(X3)))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(X3)))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(X3))))) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_951) ).
cnf(i_0_3565,negated_conjecture,
upper_relstr_subset(esk530_0,incl_POSet(powerset(cast_as_carrier_subset(esk529_0)))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3565) ).
cnf(i_0_3566,negated_conjecture,
filtered_subset(esk530_0,incl_POSet(powerset(cast_as_carrier_subset(esk529_0)))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3566) ).
cnf(i_0_1212,plain,
( empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ empty(cast_as_carrier_subset(X1)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_1212) ).
cnf(i_0_3570,negated_conjecture,
~ empty_carrier(esk529_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3570) ).
cnf(i_0_1363,plain,
( empty_carrier(X1)
| empty(X2)
| empty(X3)
| transitive_relstr(net_of_bool_filter(X1,X3,X2))
| ~ one_sorted_str(X1)
| ~ element(X3,powerset(the_carrier(X1)))
| ~ filtered_subset(X2,incl_POSet(powerset(X3)))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(X3)))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(X3))))) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_1363) ).
cnf(i_0_953,plain,
( empty_carrier(X1)
| empty(X2)
| empty(X3)
| ~ one_sorted_str(X1)
| ~ empty_carrier(net_of_bool_filter(X1,X3,X2))
| ~ element(X3,powerset(the_carrier(X1)))
| ~ filtered_subset(X2,incl_POSet(powerset(X3)))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(X3)))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(X3))))) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_953) ).
cnf(i_0_1388,plain,
( empty_carrier(X1)
| empty(X2)
| empty(X3)
| directed_relstr(net_of_bool_filter(X1,X3,X2))
| ~ one_sorted_str(X1)
| ~ element(X3,powerset(the_carrier(X1)))
| ~ filtered_subset(X2,incl_POSet(powerset(X3)))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(X3)))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(X3)))))
| ~ proper_element(X2,powerset(the_carrier(incl_POSet(powerset(X3))))) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_1388) ).
cnf(i_0_3567,negated_conjecture,
~ empty(esk530_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3567) ).
cnf(i_0_936,plain,
element(X1,powerset(X1)),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_936) ).
cnf(i_0_3520,lemma,
( filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) = set_difference(X2,unordered_pair(empty_set,empty_set))
| empty_carrier(X1)
| empty(X2)
| ~ one_sorted_str(X1)
| ~ filtered_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(X1)))))) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3520) ).
cnf(i_0_3592,lemma,
unordered_pair(empty_set,empty_set) = powerset(empty_set),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3592) ).
cnf(i_0_3507,lemma,
( empty_carrier(X1)
| empty_carrier(X2)
| is_a_convergence_point_of_set(X2,filter_of_net_str(X2,X1),X3)
| ~ transitive_relstr(X1)
| ~ topological_space(X2)
| ~ top_str(X2)
| ~ directed_relstr(X1)
| ~ net_str(X1,X2)
| ~ element(X3,the_carrier(X2))
| ~ in(X3,lim_points_of_net(X2,X1)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3507) ).
cnf(i_0_3569,negated_conjecture,
topological_space(esk529_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3569) ).
cnf(i_0_3560,negated_conjecture,
( is_a_convergence_point_of_set(esk529_0,esk530_0,esk531_0)
| in(esk531_0,lim_points_of_net(esk529_0,net_of_bool_filter(esk529_0,cast_as_carrier_subset(esk529_0),esk530_0))) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3560) ).
cnf(i_0_3529,lemma,
( filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) = X2
| empty_carrier(X1)
| empty(X2)
| ~ one_sorted_str(X1)
| ~ filtered_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(X1))))))
| ~ proper_element(X2,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(X1)))))) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3529) ).
cnf(i_0_3562,negated_conjecture,
element(esk531_0,the_carrier(esk529_0)),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3562) ).
cnf(i_0_3506,lemma,
( empty_carrier(X1)
| empty_carrier(X2)
| in(X3,lim_points_of_net(X2,X1))
| ~ transitive_relstr(X1)
| ~ topological_space(X2)
| ~ top_str(X2)
| ~ directed_relstr(X1)
| ~ net_str(X1,X2)
| ~ element(X3,the_carrier(X2))
| ~ is_a_convergence_point_of_set(X2,filter_of_net_str(X2,X1),X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3506) ).
cnf(i_0_3561,negated_conjecture,
( ~ is_a_convergence_point_of_set(esk529_0,esk530_0,esk531_0)
| ~ in(esk531_0,lim_points_of_net(esk529_0,net_of_bool_filter(esk529_0,cast_as_carrier_subset(esk529_0),esk530_0))) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-iqr2rp31/lgb.p',i_0_3561) ).
cnf(c_0_3618,plain,
( one_sorted_str(X1)
| ~ top_str(X1) ),
i_0_998 ).
cnf(c_0_3619,negated_conjecture,
top_str(esk529_0),
i_0_3568 ).
cnf(c_0_3620,plain,
( cast_as_carrier_subset(X1) = the_carrier(X1)
| ~ one_sorted_str(X1) ),
i_0_641 ).
cnf(c_0_3621,negated_conjecture,
one_sorted_str(esk529_0),
inference(spm,[status(thm)],[c_0_3618,c_0_3619]) ).
cnf(c_0_3622,negated_conjecture,
element(esk530_0,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(esk529_0)))))),
i_0_3563 ).
cnf(c_0_3623,lemma,
the_carrier(incl_POSet(X1)) = X1,
i_0_3591 ).
cnf(c_0_3624,negated_conjecture,
proper_element(esk530_0,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(esk529_0)))))),
i_0_3564 ).
cnf(c_0_3625,plain,
( empty_carrier(X1)
| empty(X2)
| empty(X3)
| net_str(net_of_bool_filter(X1,X3,X2),X1)
| ~ one_sorted_str(X1)
| ~ element(X3,powerset(the_carrier(X1)))
| ~ filtered_subset(X2,incl_POSet(powerset(X3)))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(X3)))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(X3))))) ),
i_0_951 ).
cnf(c_0_3626,negated_conjecture,
upper_relstr_subset(esk530_0,incl_POSet(powerset(cast_as_carrier_subset(esk529_0)))),
i_0_3565 ).
cnf(c_0_3627,negated_conjecture,
cast_as_carrier_subset(esk529_0) = the_carrier(esk529_0),
inference(spm,[status(thm)],[c_0_3620,c_0_3621]) ).
cnf(c_0_3628,negated_conjecture,
filtered_subset(esk530_0,incl_POSet(powerset(cast_as_carrier_subset(esk529_0)))),
i_0_3566 ).
cnf(c_0_3629,negated_conjecture,
element(esk530_0,powerset(powerset(cast_as_carrier_subset(esk529_0)))),
inference(rw,[status(thm)],[c_0_3622,c_0_3623]) ).
cnf(c_0_3630,plain,
( empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ empty(cast_as_carrier_subset(X1)) ),
i_0_1212 ).
cnf(c_0_3631,negated_conjecture,
~ empty_carrier(esk529_0),
i_0_3570 ).
cnf(c_0_3632,plain,
( empty_carrier(X1)
| empty(X2)
| empty(X3)
| transitive_relstr(net_of_bool_filter(X1,X3,X2))
| ~ one_sorted_str(X1)
| ~ element(X3,powerset(the_carrier(X1)))
| ~ filtered_subset(X2,incl_POSet(powerset(X3)))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(X3)))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(X3))))) ),
i_0_1363 ).
cnf(c_0_3633,plain,
( empty_carrier(X1)
| empty(X2)
| empty(X3)
| ~ one_sorted_str(X1)
| ~ empty_carrier(net_of_bool_filter(X1,X3,X2))
| ~ element(X3,powerset(the_carrier(X1)))
| ~ filtered_subset(X2,incl_POSet(powerset(X3)))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(X3)))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(X3))))) ),
i_0_953 ).
cnf(c_0_3634,plain,
( empty_carrier(X1)
| empty(X2)
| empty(X3)
| directed_relstr(net_of_bool_filter(X1,X3,X2))
| ~ one_sorted_str(X1)
| ~ element(X3,powerset(the_carrier(X1)))
| ~ filtered_subset(X2,incl_POSet(powerset(X3)))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(X3)))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(X3)))))
| ~ proper_element(X2,powerset(the_carrier(incl_POSet(powerset(X3))))) ),
i_0_1388 ).
cnf(c_0_3635,negated_conjecture,
proper_element(esk530_0,powerset(powerset(cast_as_carrier_subset(esk529_0)))),
inference(rw,[status(thm)],[c_0_3624,c_0_3623]) ).
cnf(c_0_3636,plain,
( net_str(net_of_bool_filter(X1,X2,X3),X1)
| empty(X3)
| empty(X2)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X3,incl_POSet(powerset(X2)))
| ~ filtered_subset(X3,incl_POSet(powerset(X2)))
| ~ element(X2,powerset(the_carrier(X1)))
| ~ element(X3,powerset(powerset(X2))) ),
inference(rw,[status(thm)],[c_0_3625,c_0_3623]) ).
cnf(c_0_3637,negated_conjecture,
upper_relstr_subset(esk530_0,incl_POSet(powerset(the_carrier(esk529_0)))),
inference(rw,[status(thm)],[c_0_3626,c_0_3627]) ).
cnf(c_0_3638,negated_conjecture,
filtered_subset(esk530_0,incl_POSet(powerset(the_carrier(esk529_0)))),
inference(rw,[status(thm)],[c_0_3628,c_0_3627]) ).
cnf(c_0_3639,negated_conjecture,
element(esk530_0,powerset(powerset(the_carrier(esk529_0)))),
inference(rw,[status(thm)],[c_0_3629,c_0_3627]) ).
cnf(c_0_3640,plain,
~ empty(the_carrier(esk529_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3630,c_0_3627]),c_0_3621])]),c_0_3631]) ).
cnf(c_0_3641,negated_conjecture,
~ empty(esk530_0),
i_0_3567 ).
cnf(c_0_3642,plain,
( transitive_relstr(net_of_bool_filter(X1,X2,X3))
| empty(X3)
| empty(X2)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X3,incl_POSet(powerset(X2)))
| ~ filtered_subset(X3,incl_POSet(powerset(X2)))
| ~ element(X2,powerset(the_carrier(X1)))
| ~ element(X3,powerset(powerset(X2))) ),
inference(rw,[status(thm)],[c_0_3632,c_0_3623]) ).
cnf(c_0_3643,plain,
( empty(X1)
| empty(X2)
| empty_carrier(X3)
| ~ one_sorted_str(X3)
| ~ empty_carrier(net_of_bool_filter(X3,X2,X1))
| ~ upper_relstr_subset(X1,incl_POSet(powerset(X2)))
| ~ filtered_subset(X1,incl_POSet(powerset(X2)))
| ~ element(X2,powerset(the_carrier(X3)))
| ~ element(X1,powerset(powerset(X2))) ),
inference(rw,[status(thm)],[c_0_3633,c_0_3623]) ).
cnf(c_0_3644,plain,
( directed_relstr(net_of_bool_filter(X1,X2,X3))
| empty(X3)
| empty(X2)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X3,incl_POSet(powerset(X2)))
| ~ filtered_subset(X3,incl_POSet(powerset(X2)))
| ~ element(X2,powerset(the_carrier(X1)))
| ~ element(X3,powerset(powerset(X2)))
| ~ proper_element(X3,powerset(powerset(X2))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3634,c_0_3623]),c_0_3623]) ).
cnf(c_0_3645,negated_conjecture,
proper_element(esk530_0,powerset(powerset(the_carrier(esk529_0)))),
inference(rw,[status(thm)],[c_0_3635,c_0_3627]) ).
cnf(c_0_3646,negated_conjecture,
( net_str(net_of_bool_filter(X1,the_carrier(esk529_0),esk530_0),X1)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(the_carrier(esk529_0),powerset(the_carrier(X1))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3636,c_0_3637]),c_0_3638]),c_0_3639])]),c_0_3640]),c_0_3641]) ).
cnf(c_0_3647,plain,
element(X1,powerset(X1)),
i_0_936 ).
cnf(c_0_3648,negated_conjecture,
( transitive_relstr(net_of_bool_filter(X1,the_carrier(esk529_0),esk530_0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(the_carrier(esk529_0),powerset(the_carrier(X1))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3642,c_0_3637]),c_0_3638]),c_0_3639])]),c_0_3640]),c_0_3641]) ).
cnf(c_0_3649,negated_conjecture,
( empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ empty_carrier(net_of_bool_filter(X1,the_carrier(esk529_0),esk530_0))
| ~ element(the_carrier(esk529_0),powerset(the_carrier(X1))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3643,c_0_3637]),c_0_3638]),c_0_3639])]),c_0_3640]),c_0_3641]) ).
cnf(c_0_3650,negated_conjecture,
( directed_relstr(net_of_bool_filter(X1,the_carrier(esk529_0),esk530_0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(the_carrier(esk529_0),powerset(the_carrier(X1))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3644,c_0_3645]),c_0_3637]),c_0_3638]),c_0_3639])]),c_0_3640]),c_0_3641]) ).
cnf(c_0_3651,lemma,
( filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) = set_difference(X2,unordered_pair(empty_set,empty_set))
| empty_carrier(X1)
| empty(X2)
| ~ one_sorted_str(X1)
| ~ filtered_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(X1)))))) ),
i_0_3520 ).
cnf(c_0_3652,lemma,
unordered_pair(empty_set,empty_set) = powerset(empty_set),
i_0_3592 ).
cnf(c_0_3653,lemma,
( empty_carrier(X1)
| empty_carrier(X2)
| is_a_convergence_point_of_set(X2,filter_of_net_str(X2,X1),X3)
| ~ transitive_relstr(X1)
| ~ topological_space(X2)
| ~ top_str(X2)
| ~ directed_relstr(X1)
| ~ net_str(X1,X2)
| ~ element(X3,the_carrier(X2))
| ~ in(X3,lim_points_of_net(X2,X1)) ),
i_0_3507 ).
cnf(c_0_3654,plain,
net_str(net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0),esk529_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3646,c_0_3647]),c_0_3621])]),c_0_3631]) ).
cnf(c_0_3655,negated_conjecture,
topological_space(esk529_0),
i_0_3569 ).
cnf(c_0_3656,plain,
transitive_relstr(net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3648,c_0_3647]),c_0_3621])]),c_0_3631]) ).
cnf(c_0_3657,plain,
~ empty_carrier(net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3649,c_0_3647]),c_0_3621])]),c_0_3631]) ).
cnf(c_0_3658,plain,
directed_relstr(net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3650,c_0_3647]),c_0_3621])]),c_0_3631]) ).
cnf(c_0_3659,negated_conjecture,
( is_a_convergence_point_of_set(esk529_0,esk530_0,esk531_0)
| in(esk531_0,lim_points_of_net(esk529_0,net_of_bool_filter(esk529_0,cast_as_carrier_subset(esk529_0),esk530_0))) ),
i_0_3560 ).
cnf(c_0_3660,lemma,
( filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) = set_difference(X2,powerset(empty_set))
| empty(X2)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ filtered_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ element(X2,powerset(powerset(cast_as_carrier_subset(X1)))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3651,c_0_3652]),c_0_3623]) ).
cnf(c_0_3661,lemma,
( filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) = X2
| empty_carrier(X1)
| empty(X2)
| ~ one_sorted_str(X1)
| ~ filtered_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ upper_relstr_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ element(X2,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(X1))))))
| ~ proper_element(X2,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(X1)))))) ),
i_0_3529 ).
cnf(c_0_3662,lemma,
( is_a_convergence_point_of_set(esk529_0,filter_of_net_str(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)),X1)
| ~ element(X1,the_carrier(esk529_0))
| ~ in(X1,lim_points_of_net(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3653,c_0_3654]),c_0_3619]),c_0_3655]),c_0_3656])]),c_0_3631]),c_0_3657]),c_0_3658])]) ).
cnf(c_0_3663,negated_conjecture,
( in(esk531_0,lim_points_of_net(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)))
| is_a_convergence_point_of_set(esk529_0,esk530_0,esk531_0) ),
inference(rw,[status(thm)],[c_0_3659,c_0_3627]) ).
cnf(c_0_3664,negated_conjecture,
element(esk531_0,the_carrier(esk529_0)),
i_0_3562 ).
cnf(c_0_3665,negated_conjecture,
( filter_of_net_str(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),X1)) = set_difference(X1,powerset(empty_set))
| empty(X1)
| ~ upper_relstr_subset(X1,incl_POSet(powerset(the_carrier(esk529_0))))
| ~ filtered_subset(X1,incl_POSet(powerset(the_carrier(esk529_0))))
| ~ element(X1,powerset(powerset(the_carrier(esk529_0)))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3660,c_0_3627]),c_0_3621])]),c_0_3631]) ).
cnf(c_0_3666,lemma,
( filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) = X2
| empty(X2)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ filtered_subset(X2,incl_POSet(powerset(cast_as_carrier_subset(X1))))
| ~ element(X2,powerset(powerset(cast_as_carrier_subset(X1))))
| ~ proper_element(X2,powerset(powerset(cast_as_carrier_subset(X1)))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3661,c_0_3623]),c_0_3623]) ).
cnf(c_0_3667,lemma,
( empty_carrier(X1)
| empty_carrier(X2)
| in(X3,lim_points_of_net(X2,X1))
| ~ transitive_relstr(X1)
| ~ topological_space(X2)
| ~ top_str(X2)
| ~ directed_relstr(X1)
| ~ net_str(X1,X2)
| ~ element(X3,the_carrier(X2))
| ~ is_a_convergence_point_of_set(X2,filter_of_net_str(X2,X1),X3) ),
i_0_3506 ).
cnf(c_0_3668,negated_conjecture,
( is_a_convergence_point_of_set(esk529_0,filter_of_net_str(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)),esk531_0)
| is_a_convergence_point_of_set(esk529_0,esk530_0,esk531_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3662,c_0_3663]),c_0_3664])]) ).
cnf(c_0_3669,negated_conjecture,
filter_of_net_str(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)) = set_difference(esk530_0,powerset(empty_set)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3665,c_0_3637]),c_0_3638]),c_0_3639])]),c_0_3641]) ).
cnf(c_0_3670,negated_conjecture,
( filter_of_net_str(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),X1)) = X1
| empty(X1)
| ~ upper_relstr_subset(X1,incl_POSet(powerset(the_carrier(esk529_0))))
| ~ filtered_subset(X1,incl_POSet(powerset(the_carrier(esk529_0))))
| ~ element(X1,powerset(powerset(the_carrier(esk529_0))))
| ~ proper_element(X1,powerset(powerset(the_carrier(esk529_0)))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3666,c_0_3627]),c_0_3621])]),c_0_3631]) ).
cnf(c_0_3671,lemma,
( in(X1,lim_points_of_net(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)))
| ~ element(X1,the_carrier(esk529_0))
| ~ is_a_convergence_point_of_set(esk529_0,filter_of_net_str(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)),X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3667,c_0_3654]),c_0_3619]),c_0_3655]),c_0_3656])]),c_0_3631]),c_0_3657]),c_0_3658])]) ).
cnf(c_0_3672,negated_conjecture,
( ~ is_a_convergence_point_of_set(esk529_0,esk530_0,esk531_0)
| ~ in(esk531_0,lim_points_of_net(esk529_0,net_of_bool_filter(esk529_0,cast_as_carrier_subset(esk529_0),esk530_0))) ),
i_0_3561 ).
cnf(c_0_3673,negated_conjecture,
( is_a_convergence_point_of_set(esk529_0,set_difference(esk530_0,powerset(empty_set)),esk531_0)
| is_a_convergence_point_of_set(esk529_0,esk530_0,esk531_0) ),
inference(rw,[status(thm)],[c_0_3668,c_0_3669]) ).
cnf(c_0_3674,negated_conjecture,
set_difference(esk530_0,powerset(empty_set)) = esk530_0,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3670,c_0_3645]),c_0_3669]),c_0_3637]),c_0_3638]),c_0_3639])]),c_0_3641]) ).
cnf(c_0_3675,lemma,
( in(X1,lim_points_of_net(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)))
| ~ element(X1,the_carrier(esk529_0))
| ~ is_a_convergence_point_of_set(esk529_0,set_difference(esk530_0,powerset(empty_set)),X1) ),
inference(rw,[status(thm)],[c_0_3671,c_0_3669]) ).
cnf(c_0_3676,negated_conjecture,
( ~ in(esk531_0,lim_points_of_net(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)))
| ~ is_a_convergence_point_of_set(esk529_0,esk530_0,esk531_0) ),
inference(rw,[status(thm)],[c_0_3672,c_0_3627]) ).
cnf(c_0_3677,negated_conjecture,
is_a_convergence_point_of_set(esk529_0,esk530_0,esk531_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3673,c_0_3674])]) ).
cnf(c_0_3678,lemma,
( in(X1,lim_points_of_net(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0)))
| ~ element(X1,the_carrier(esk529_0))
| ~ is_a_convergence_point_of_set(esk529_0,esk530_0,X1) ),
inference(rw,[status(thm)],[c_0_3675,c_0_3674]) ).
cnf(c_0_3679,negated_conjecture,
~ in(esk531_0,lim_points_of_net(esk529_0,net_of_bool_filter(esk529_0,the_carrier(esk529_0),esk530_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3676,c_0_3677])]) ).
cnf(c_0_3680,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3678,c_0_3677]),c_0_3664])]),c_0_3679]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SEU395+2 : TPTP v8.1.0. Released v3.3.0.
% 0.10/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jun 20 07:57:50 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.46 # ENIGMATIC: Selected SinE mode:
% 0.19/0.52 # Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.52 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.19/0.52 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.19/0.52 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 9.32/3.54 # ENIGMATIC: Solved by autoschedule-lgb:
% 9.32/3.54 # No SInE strategy applied
% 9.32/3.54 # Trying AutoSched0 for 150 seconds
% 9.32/3.54 # AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_S4d
% 9.32/3.54 # and selection function SelectCQIPrecWNTNp.
% 9.32/3.54 #
% 9.32/3.54 # Preprocessing time : 0.017 s
% 9.32/3.54 # Presaturation interreduction done
% 9.32/3.54
% 9.32/3.54 # Proof found!
% 9.32/3.54 # SZS status Theorem
% 9.32/3.54 # SZS output start CNFRefutation
% See solution above
% 9.32/3.54 # Training examples: 0 positive, 0 negative
% 9.32/3.54
% 9.32/3.54 # -------------------------------------------------
% 9.32/3.54 # User time : 0.043 s
% 9.32/3.54 # System time : 0.006 s
% 9.32/3.54 # Total time : 0.049 s
% 9.32/3.54 # Maximum resident set size: 7288 pages
% 9.32/3.54
%------------------------------------------------------------------------------