%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : SEU394+2 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n015.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.95s 3.59s
% Output : CNFRefutation 9.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 25
% Syntax : Number of clauses : 82 ( 65 unt; 9 nHn; 57 RR)
% Number of literals : 156 ( 34 equ; 76 neg)
% Maximal clause size : 12 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 3 con; 0-3 aty)
% Number of variables : 55 ( 19 sgn)
% Comments :
%------------------------------------------------------------------------------
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-mmxf0cjf/lgb.p',i_0_641) ).
cnf(i_0_3536,negated_conjecture,
one_sorted_str(esk525_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3536) ).
cnf(i_0_333,plain,
( identity_relation(the_carrier(X1)) = identity_on_carrier(X1)
| ~ one_sorted_str(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_333) ).
cnf(i_0_3853,lemma,
relation_rng(identity_relation(X1)) = X1,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3853) ).
cnf(i_0_3521,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-mmxf0cjf/lgb.p',i_0_3521) ).
cnf(i_0_615,plain,
poset_of_lattice(boole_lattice(X1)) = incl_POSet(powerset(X1)),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_615) ).
cnf(i_0_3588,lemma,
the_carrier(incl_POSet(X1)) = X1,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3588) ).
cnf(i_0_3854,lemma,
relation_dom(identity_relation(X1)) = X1,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3854) ).
cnf(i_0_3533,negated_conjecture,
upper_relstr_subset(esk526_0,incl_POSet(powerset(cast_as_carrier_subset(esk525_0)))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3533) ).
cnf(i_0_3534,negated_conjecture,
filtered_subset(esk526_0,incl_POSet(powerset(cast_as_carrier_subset(esk525_0)))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3534) ).
cnf(i_0_3531,negated_conjecture,
element(esk526_0,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(esk525_0)))))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3531) ).
cnf(i_0_3532,negated_conjecture,
proper_element(esk526_0,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(esk525_0)))))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3532) ).
cnf(i_0_3530,negated_conjecture,
filter_of_net_str(esk525_0,net_of_bool_filter(esk525_0,cast_as_carrier_subset(esk525_0),esk526_0)) != esk526_0,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3530) ).
cnf(i_0_3881,lemma,
( empty_carrier(X1)
| empty(X2)
| ~ rel_str(X1)
| ~ reflexive_relstr(X1)
| ~ transitive_relstr(X1)
| ~ antisymmetric_relstr(X1)
| ~ lower_bounded_relstr(X1)
| ~ filtered_subset(X2,X1)
| ~ upper_relstr_subset(X2,X1)
| ~ in(bottom_of_relstr(X1),X2)
| ~ element(X2,powerset(the_carrier(X1)))
| ~ proper_element(X2,powerset(the_carrier(X1))) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3881) ).
cnf(i_0_3859,plain,
( ~ empty(X1)
| ~ in(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3859) ).
cnf(i_0_3537,negated_conjecture,
~ empty_carrier(esk525_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3537) ).
cnf(i_0_1393,plain,
antisymmetric_relstr(incl_POSet(X1)),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_1393) ).
cnf(i_0_1394,plain,
transitive_relstr(incl_POSet(X1)),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_1394) ).
cnf(i_0_1395,plain,
reflexive_relstr(incl_POSet(X1)),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_1395) ).
cnf(i_0_940,plain,
rel_str(incl_POSet(X1)),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_940) ).
cnf(i_0_3568,lemma,
bottom_of_relstr(incl_POSet(powerset(X1))) = empty_set,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3568) ).
cnf(i_0_1459,plain,
lower_bounded_relstr(incl_POSet(powerset(X1))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_1459) ).
cnf(i_0_1467,plain,
~ empty_carrier(incl_POSet(powerset(X1))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_1467) ).
cnf(i_0_3535,negated_conjecture,
~ empty(esk526_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3535) ).
cnf(i_0_3836,lemma,
( set_difference(X1,unordered_pair(X2,X2)) = X1
| in(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-mmxf0cjf/lgb.p',i_0_3836) ).
cnf(c_0_3907,plain,
( cast_as_carrier_subset(X1) = the_carrier(X1)
| ~ one_sorted_str(X1) ),
i_0_641 ).
cnf(c_0_3908,negated_conjecture,
one_sorted_str(esk525_0),
i_0_3536 ).
cnf(c_0_3909,plain,
( identity_relation(the_carrier(X1)) = identity_on_carrier(X1)
| ~ one_sorted_str(X1) ),
i_0_333 ).
cnf(c_0_3910,negated_conjecture,
the_carrier(esk525_0) = cast_as_carrier_subset(esk525_0),
inference(spm,[status(thm)],[c_0_3907,c_0_3908]) ).
cnf(c_0_3911,lemma,
relation_rng(identity_relation(X1)) = X1,
i_0_3853 ).
cnf(c_0_3912,negated_conjecture,
identity_relation(cast_as_carrier_subset(esk525_0)) = identity_on_carrier(esk525_0),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3909,c_0_3908]),c_0_3910]) ).
cnf(c_0_3913,lemma,
cast_as_carrier_subset(esk525_0) = relation_rng(identity_on_carrier(esk525_0)),
inference(spm,[status(thm)],[c_0_3911,c_0_3912]) ).
cnf(c_0_3914,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_3521 ).
cnf(c_0_3915,plain,
poset_of_lattice(boole_lattice(X1)) = incl_POSet(powerset(X1)),
i_0_615 ).
cnf(c_0_3916,lemma,
the_carrier(incl_POSet(X1)) = X1,
i_0_3588 ).
cnf(c_0_3917,lemma,
relation_dom(identity_relation(X1)) = X1,
i_0_3854 ).
cnf(c_0_3918,negated_conjecture,
identity_relation(relation_rng(identity_on_carrier(esk525_0))) = identity_on_carrier(esk525_0),
inference(rw,[status(thm)],[c_0_3912,c_0_3913]) ).
cnf(c_0_3919,negated_conjecture,
upper_relstr_subset(esk526_0,incl_POSet(powerset(cast_as_carrier_subset(esk525_0)))),
i_0_3533 ).
cnf(c_0_3920,negated_conjecture,
filtered_subset(esk526_0,incl_POSet(powerset(cast_as_carrier_subset(esk525_0)))),
i_0_3534 ).
cnf(c_0_3921,negated_conjecture,
element(esk526_0,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(esk525_0)))))),
i_0_3531 ).
cnf(c_0_3922,negated_conjecture,
proper_element(esk526_0,powerset(the_carrier(incl_POSet(powerset(cast_as_carrier_subset(esk525_0)))))),
i_0_3532 ).
cnf(c_0_3923,negated_conjecture,
filter_of_net_str(esk525_0,net_of_bool_filter(esk525_0,cast_as_carrier_subset(esk525_0),esk526_0)) != esk526_0,
i_0_3530 ).
cnf(c_0_3924,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(X2)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ element(X2,powerset(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1)))))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3914,c_0_3915]),c_0_3915]),c_0_3915]) ).
cnf(c_0_3925,lemma,
the_carrier(poset_of_lattice(boole_lattice(X1))) = powerset(X1),
inference(spm,[status(thm)],[c_0_3916,c_0_3915]) ).
cnf(c_0_3926,lemma,
relation_rng(identity_on_carrier(esk525_0)) = relation_dom(identity_on_carrier(esk525_0)),
inference(spm,[status(thm)],[c_0_3917,c_0_3918]) ).
cnf(c_0_3927,negated_conjecture,
upper_relstr_subset(esk526_0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(esk525_0)))),
inference(rw,[status(thm)],[c_0_3919,c_0_3915]) ).
cnf(c_0_3928,negated_conjecture,
filtered_subset(esk526_0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(esk525_0)))),
inference(rw,[status(thm)],[c_0_3920,c_0_3915]) ).
cnf(c_0_3929,negated_conjecture,
element(esk526_0,powerset(powerset(cast_as_carrier_subset(esk525_0)))),
inference(rw,[status(thm)],[c_0_3921,c_0_3916]) ).
cnf(c_0_3930,lemma,
( empty_carrier(X1)
| empty(X2)
| ~ rel_str(X1)
| ~ reflexive_relstr(X1)
| ~ transitive_relstr(X1)
| ~ antisymmetric_relstr(X1)
| ~ lower_bounded_relstr(X1)
| ~ filtered_subset(X2,X1)
| ~ upper_relstr_subset(X2,X1)
| ~ in(bottom_of_relstr(X1),X2)
| ~ element(X2,powerset(the_carrier(X1)))
| ~ proper_element(X2,powerset(the_carrier(X1))) ),
i_0_3881 ).
cnf(c_0_3931,plain,
( ~ empty(X1)
| ~ in(X2,X1) ),
i_0_3859 ).
cnf(c_0_3932,negated_conjecture,
proper_element(esk526_0,powerset(powerset(cast_as_carrier_subset(esk525_0)))),
inference(rw,[status(thm)],[c_0_3922,c_0_3916]) ).
cnf(c_0_3933,negated_conjecture,
filter_of_net_str(esk525_0,net_of_bool_filter(esk525_0,relation_rng(identity_on_carrier(esk525_0)),esk526_0)) != esk526_0,
inference(rw,[status(thm)],[c_0_3923,c_0_3913]) ).
cnf(c_0_3934,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(X2)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ element(X2,powerset(powerset(cast_as_carrier_subset(X1)))) ),
inference(rw,[status(thm)],[c_0_3924,c_0_3925]) ).
cnf(c_0_3935,lemma,
cast_as_carrier_subset(esk525_0) = relation_dom(identity_on_carrier(esk525_0)),
inference(rw,[status(thm)],[c_0_3913,c_0_3926]) ).
cnf(c_0_3936,negated_conjecture,
~ empty_carrier(esk525_0),
i_0_3537 ).
cnf(c_0_3937,negated_conjecture,
upper_relstr_subset(esk526_0,poset_of_lattice(boole_lattice(relation_rng(identity_on_carrier(esk525_0))))),
inference(rw,[status(thm)],[c_0_3927,c_0_3913]) ).
cnf(c_0_3938,negated_conjecture,
filtered_subset(esk526_0,poset_of_lattice(boole_lattice(relation_rng(identity_on_carrier(esk525_0))))),
inference(rw,[status(thm)],[c_0_3928,c_0_3913]) ).
cnf(c_0_3939,negated_conjecture,
element(esk526_0,powerset(powerset(relation_rng(identity_on_carrier(esk525_0))))),
inference(rw,[status(thm)],[c_0_3929,c_0_3913]) ).
cnf(c_0_3940,lemma,
( empty_carrier(X1)
| ~ in(bottom_of_relstr(X1),X2)
| ~ lower_bounded_relstr(X1)
| ~ antisymmetric_relstr(X1)
| ~ transitive_relstr(X1)
| ~ reflexive_relstr(X1)
| ~ rel_str(X1)
| ~ upper_relstr_subset(X2,X1)
| ~ filtered_subset(X2,X1)
| ~ element(X2,powerset(the_carrier(X1)))
| ~ proper_element(X2,powerset(the_carrier(X1))) ),
inference(csr,[status(thm)],[c_0_3930,c_0_3931]) ).
cnf(c_0_3941,plain,
antisymmetric_relstr(incl_POSet(X1)),
i_0_1393 ).
cnf(c_0_3942,plain,
transitive_relstr(incl_POSet(X1)),
i_0_1394 ).
cnf(c_0_3943,plain,
reflexive_relstr(incl_POSet(X1)),
i_0_1395 ).
cnf(c_0_3944,plain,
rel_str(incl_POSet(X1)),
i_0_940 ).
cnf(c_0_3945,negated_conjecture,
proper_element(esk526_0,powerset(powerset(relation_rng(identity_on_carrier(esk525_0))))),
inference(rw,[status(thm)],[c_0_3932,c_0_3913]) ).
cnf(c_0_3946,lemma,
bottom_of_relstr(incl_POSet(powerset(X1))) = empty_set,
i_0_3568 ).
cnf(c_0_3947,plain,
lower_bounded_relstr(incl_POSet(powerset(X1))),
i_0_1459 ).
cnf(c_0_3948,plain,
~ empty_carrier(incl_POSet(powerset(X1))),
i_0_1467 ).
cnf(c_0_3949,negated_conjecture,
filter_of_net_str(esk525_0,net_of_bool_filter(esk525_0,relation_dom(identity_on_carrier(esk525_0)),esk526_0)) != esk526_0,
inference(rw,[status(thm)],[c_0_3933,c_0_3926]) ).
cnf(c_0_3950,lemma,
( filter_of_net_str(esk525_0,net_of_bool_filter(esk525_0,relation_dom(identity_on_carrier(esk525_0)),X1)) = set_difference(X1,unordered_pair(empty_set,empty_set))
| empty(X1)
| ~ upper_relstr_subset(X1,poset_of_lattice(boole_lattice(relation_dom(identity_on_carrier(esk525_0)))))
| ~ filtered_subset(X1,poset_of_lattice(boole_lattice(relation_dom(identity_on_carrier(esk525_0)))))
| ~ element(X1,powerset(powerset(relation_dom(identity_on_carrier(esk525_0))))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3934,c_0_3935]),c_0_3908])]),c_0_3936]) ).
cnf(c_0_3951,negated_conjecture,
upper_relstr_subset(esk526_0,poset_of_lattice(boole_lattice(relation_dom(identity_on_carrier(esk525_0))))),
inference(rw,[status(thm)],[c_0_3937,c_0_3926]) ).
cnf(c_0_3952,negated_conjecture,
filtered_subset(esk526_0,poset_of_lattice(boole_lattice(relation_dom(identity_on_carrier(esk525_0))))),
inference(rw,[status(thm)],[c_0_3938,c_0_3926]) ).
cnf(c_0_3953,negated_conjecture,
element(esk526_0,powerset(powerset(relation_dom(identity_on_carrier(esk525_0))))),
inference(rw,[status(thm)],[c_0_3939,c_0_3926]) ).
cnf(c_0_3954,negated_conjecture,
~ empty(esk526_0),
i_0_3535 ).
cnf(c_0_3955,lemma,
( empty_carrier(incl_POSet(X1))
| ~ in(bottom_of_relstr(incl_POSet(X1)),X2)
| ~ lower_bounded_relstr(incl_POSet(X1))
| ~ upper_relstr_subset(X2,incl_POSet(X1))
| ~ filtered_subset(X2,incl_POSet(X1))
| ~ element(X2,powerset(X1))
| ~ proper_element(X2,powerset(X1)) ),
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_3940,c_0_3916]),c_0_3941]),c_0_3942]),c_0_3943]),c_0_3944])]) ).
cnf(c_0_3956,negated_conjecture,
proper_element(esk526_0,powerset(powerset(relation_dom(identity_on_carrier(esk525_0))))),
inference(rw,[status(thm)],[c_0_3945,c_0_3926]) ).
cnf(c_0_3957,lemma,
bottom_of_relstr(poset_of_lattice(boole_lattice(X1))) = empty_set,
inference(rw,[status(thm)],[c_0_3946,c_0_3915]) ).
cnf(c_0_3958,plain,
lower_bounded_relstr(poset_of_lattice(boole_lattice(X1))),
inference(rw,[status(thm)],[c_0_3947,c_0_3915]) ).
cnf(c_0_3959,plain,
~ empty_carrier(poset_of_lattice(boole_lattice(X1))),
inference(rw,[status(thm)],[c_0_3948,c_0_3915]) ).
cnf(c_0_3960,negated_conjecture,
set_difference(esk526_0,unordered_pair(empty_set,empty_set)) != esk526_0,
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_3949,c_0_3950]),c_0_3951]),c_0_3952]),c_0_3953])]),c_0_3954]) ).
cnf(c_0_3961,lemma,
( set_difference(X1,unordered_pair(X2,X2)) = X1
| in(X2,X1) ),
i_0_3836 ).
cnf(c_0_3962,negated_conjecture,
~ in(empty_set,esk526_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(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3955,c_0_3956]),c_0_3915]),c_0_3915]),c_0_3957]),c_0_3915]),c_0_3958]),c_0_3915]),c_0_3951]),c_0_3915]),c_0_3952]),c_0_3953])]),c_0_3959]) ).
cnf(c_0_3963,lemma,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3960,c_0_3961]),c_0_3962]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU394+2 : TPTP v8.1.0. Released v3.3.0.
% 0.03/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.33 % Computer : n015.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Sun Jun 19 16:13:46 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.46 # ENIGMATIC: Selected SinE mode:
% 0.19/0.51 # Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.51 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.19/0.51 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.19/0.51 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 9.95/3.59 # ENIGMATIC: Solved by autoschedule-lgb:
% 9.95/3.59 # No SInE strategy applied
% 9.95/3.59 # Trying AutoSched0 for 150 seconds
% 9.95/3.59 # AutoSched0-Mode selected heuristic G_E___107_B42_F1_PI_SE_Q4_CS_SP_PS_S5PRR_S0Y
% 9.95/3.59 # and selection function SelectMaxLComplexAvoidPosPred.
% 9.95/3.59 #
% 9.95/3.59 # Preprocessing time : 0.044 s
% 9.95/3.59 # Presaturation interreduction done
% 9.95/3.59
% 9.95/3.59 # Proof found!
% 9.95/3.59 # SZS status Theorem
% 9.95/3.59 # SZS output start CNFRefutation
% See solution above
% 9.95/3.59 # Training examples: 0 positive, 0 negative
% 9.95/3.59
% 9.95/3.59 # -------------------------------------------------
% 9.95/3.59 # User time : 0.091 s
% 9.95/3.59 # System time : 0.015 s
% 9.95/3.59 # Total time : 0.106 s
% 9.95/3.59 # Maximum resident set size: 7296 pages
% 9.95/3.59
%------------------------------------------------------------------------------