%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU394+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 : Tue Sep 29 12:48:42 PM UTC 2026
% Result : Theorem 17.28s 3.39s
% Output : Refutation 18.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 11
% Syntax : Number of formulae : 73 ( 32 unt; 0 def)
% Number of atoms : 309 ( 35 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 410 ( 174 ~; 160 |; 64 &)
% ( 4 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 28 ( 26 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-3 aty)
% Number of variables : 62 ( 58 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f288,axiom,
! [X0] :
( strict_rel_str(boole_POSet(X0))
& rel_str(boole_POSet(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_yellow_1) ).
fof(f389,axiom,
! [X0] :
( ~ empty_carrier(boole_POSet(X0))
& strict_rel_str(boole_POSet(X0))
& reflexive_relstr(boole_POSet(X0))
& transitive_relstr(boole_POSet(X0))
& antisymmetric_relstr(boole_POSet(X0))
& lower_bounded_relstr(boole_POSet(X0))
& upper_bounded_relstr(boole_POSet(X0))
& bounded_relstr(boole_POSet(X0))
& up_complete_relstr(boole_POSet(X0))
& join_complete_relstr(boole_POSet(X0))
& ~ v1_yellow_3(boole_POSet(X0))
& distributive_relstr(boole_POSet(X0))
& heyting_relstr(boole_POSet(X0))
& complemented_relstr(boole_POSet(X0))
& boolean_relstr(boole_POSet(X0))
& with_suprema_relstr(boole_POSet(X0))
& with_infima_relstr(boole_POSet(X0))
& complete_relstr(boole_POSet(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_waybel_7) ).
fof(f708,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
=> set_difference(X1,singleton(empty_set)) = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t14_yellow19) ).
fof(f711,conjecture,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
=> X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_yellow19) ).
fof(f712,negated_conjecture,
~ ! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
=> X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
inference(negated_conjecture,[status(cth)],[f711]) ).
fof(f731,axiom,
! [X0] : bottom_of_relstr(boole_POSet(X0)) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_yellow_1) ).
fof(f741,axiom,
powerset(empty_set) = singleton(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_zfmisc_1) ).
fof(f848,axiom,
! [X0] : the_carrier(boole_POSet(X0)) = powerset(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_waybel_7) ).
fof(f879,axiom,
! [X0,X1] :
( set_difference(X0,singleton(X1)) = X0
<=> ~ in(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f881,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f892,axiom,
! [X0,X1] :
~ ( in(X0,X1)
& empty(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f904,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& reflexive_relstr(X0)
& transitive_relstr(X0)
& antisymmetric_relstr(X0)
& lower_bounded_relstr(X0)
& rel_str(X0) )
=> ! [X1] :
( ( ~ empty(X1)
& filtered_subset(X1,X0)
& upper_relstr_subset(X1,X0)
& element(X1,powerset(the_carrier(X0))) )
=> ( proper_element(X1,powerset(the_carrier(X0)))
<=> ~ in(bottom_of_relstr(X0),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_waybel_7) ).
fof(f1110,plain,
! [X0] :
( ! [X1] :
( set_difference(X1,singleton(empty_set)) = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))
| empty(X1)
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f708]) ).
fof(f1111,plain,
! [X0] :
( ! [X1] :
( set_difference(X1,singleton(empty_set)) = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))
| empty(X1)
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f1110]) ).
fof(f1114,plain,
? [X0] :
( ? [X1] :
( filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) != X1
& ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
& ~ empty_carrier(X0)
& one_sorted_str(X0) ),
inference(ennf_transformation,[],[f712]) ).
fof(f1115,plain,
? [X0] :
( ? [X1] :
( filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) != X1
& ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
& ~ empty_carrier(X0)
& one_sorted_str(X0) ),
inference(flattening,[],[f1114]) ).
fof(f1363,plain,
! [X0] :
( ! [X1] :
( ( proper_element(X1,powerset(the_carrier(X0)))
<=> ~ in(bottom_of_relstr(X0),X1) )
| empty(X1)
| ~ filtered_subset(X1,X0)
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0))) )
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ transitive_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f904]) ).
fof(f1364,plain,
! [X0] :
( ! [X1] :
( ( proper_element(X1,powerset(the_carrier(X0)))
<=> ~ in(bottom_of_relstr(X0),X1) )
| empty(X1)
| ~ filtered_subset(X1,X0)
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0))) )
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ transitive_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(flattening,[],[f1363]) ).
fof(f1381,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(ennf_transformation,[],[f892]) ).
fof(f2430,plain,
( sK207 != filter_of_net_str(sK206,net_of_bool_filter(sK206,cast_as_carrier_subset(sK206),sK207))
& ~ empty(sK207)
& filtered_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206)))
& upper_relstr_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206)))
& proper_element(sK207,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK206)))))
& element(sK207,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK206)))))
& ~ empty_carrier(sK206)
& one_sorted_str(sK206) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK206,sK207]),skolemize(X0,sK206),skolemize(X1,sK207)],[f1115]) ).
fof(f2517,plain,
! [X0,X1] :
( ( set_difference(X0,singleton(X1)) = X0
| in(X1,X0) )
& ( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ) ),
inference(nnf_transformation,[],[f879]) ).
fof(f2533,plain,
! [X0] :
( ! [X1] :
( ( ( proper_element(X1,powerset(the_carrier(X0)))
| in(bottom_of_relstr(X0),X1) )
& ( ~ in(bottom_of_relstr(X0),X1)
| ~ proper_element(X1,powerset(the_carrier(X0))) ) )
| empty(X1)
| ~ filtered_subset(X1,X0)
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0))) )
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ transitive_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(nnf_transformation,[],[f1364]) ).
fof(f3458,plain,
! [X0,X1] :
( set_difference(X1,singleton(empty_set)) = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))
| empty(X1)
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1111]) ).
fof(f3461,plain,
one_sorted_str(sK206),
inference(cnf_transformation,[],[f2430]) ).
fof(f3462,plain,
~ empty_carrier(sK206),
inference(cnf_transformation,[],[f2430]) ).
fof(f3463,plain,
element(sK207,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK206))))),
inference(cnf_transformation,[],[f2430]) ).
fof(f3464,plain,
proper_element(sK207,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK206))))),
inference(cnf_transformation,[],[f2430]) ).
fof(f3465,plain,
upper_relstr_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206))),
inference(cnf_transformation,[],[f2430]) ).
fof(f3466,plain,
filtered_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206))),
inference(cnf_transformation,[],[f2430]) ).
fof(f3467,plain,
~ empty(sK207),
inference(cnf_transformation,[],[f2430]) ).
fof(f3468,plain,
sK207 != filter_of_net_str(sK206,net_of_bool_filter(sK206,cast_as_carrier_subset(sK206),sK207)),
inference(cnf_transformation,[],[f2430]) ).
fof(f3505,plain,
! [X0] : empty_set = bottom_of_relstr(boole_POSet(X0)),
inference(cnf_transformation,[],[f731]) ).
fof(f3525,plain,
powerset(empty_set) = singleton(empty_set),
inference(cnf_transformation,[],[f741]) ).
fof(f3704,plain,
! [X0] : powerset(X0) = the_carrier(boole_POSet(X0)),
inference(cnf_transformation,[],[f848]) ).
fof(f3765,plain,
! [X0,X1] :
( set_difference(X0,singleton(X1)) = X0
| in(X1,X0) ),
inference(cnf_transformation,[],[f2517]) ).
fof(f3770,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f881]) ).
fof(f3803,plain,
! [X0,X1] :
( ~ in(bottom_of_relstr(X0),X1)
| ~ proper_element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ filtered_subset(X1,X0)
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ transitive_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f2533]) ).
fof(f3825,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(cnf_transformation,[],[f1381]) ).
fof(f4645,plain,
! [X0] : rel_str(boole_POSet(X0)),
inference(cnf_transformation,[],[f288]) ).
fof(f5683,plain,
! [X0] : lower_bounded_relstr(boole_POSet(X0)),
inference(cnf_transformation,[],[f389]) ).
fof(f5684,plain,
! [X0] : antisymmetric_relstr(boole_POSet(X0)),
inference(cnf_transformation,[],[f389]) ).
fof(f5685,plain,
! [X0] : transitive_relstr(boole_POSet(X0)),
inference(cnf_transformation,[],[f389]) ).
fof(f5686,plain,
! [X0] : reflexive_relstr(boole_POSet(X0)),
inference(cnf_transformation,[],[f389]) ).
fof(f5688,plain,
! [X0] : ~ empty_carrier(boole_POSet(X0)),
inference(cnf_transformation,[],[f389]) ).
fof(f6214,plain,
! [X0,X1] :
( filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) = set_difference(X1,unordered_pair(empty_set,empty_set))
| empty(X1)
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ element(X1,the_carrier(boole_POSet(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(definition_unfolding,[],[f3458,f3770,f3704]) ).
fof(f6217,plain,
proper_element(sK207,the_carrier(boole_POSet(the_carrier(boole_POSet(cast_as_carrier_subset(sK206)))))),
inference(definition_unfolding,[],[f3464,f3704]) ).
fof(f6218,plain,
element(sK207,the_carrier(boole_POSet(the_carrier(boole_POSet(cast_as_carrier_subset(sK206)))))),
inference(definition_unfolding,[],[f3463,f3704]) ).
fof(f6237,plain,
the_carrier(boole_POSet(empty_set)) = unordered_pair(empty_set,empty_set),
inference(definition_unfolding,[],[f3525,f3704,f3770]) ).
fof(f6313,plain,
! [X0,X1] :
( in(X1,X0)
| set_difference(X0,unordered_pair(X1,X1)) = X0 ),
inference(definition_unfolding,[],[f3765,f3770]) ).
fof(f6335,plain,
! [X0,X1] :
( ~ in(bottom_of_relstr(X0),X1)
| ~ proper_element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| empty(X1)
| ~ filtered_subset(X1,X0)
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ transitive_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(definition_unfolding,[],[f3803,f3704,f3704]) ).
fof(f7323,plain,
! [X0,X1] :
( ~ proper_element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| ~ in(bottom_of_relstr(X0),X1)
| ~ filtered_subset(X1,X0)
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ transitive_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(forward_subsumption_resolution,[],[f6335,f3825]) ).
fof(f7357,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(boole_POSet(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))))
| empty(X1)
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) = set_difference(X1,the_carrier(boole_POSet(empty_set)))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(forward_demodulation,[],[f6214,f6237]) ).
fof(f7550,plain,
( empty(sK207)
| ~ filtered_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206)))
| ~ upper_relstr_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206)))
| filter_of_net_str(sK206,net_of_bool_filter(sK206,cast_as_carrier_subset(sK206),sK207)) = set_difference(sK207,the_carrier(boole_POSet(empty_set)))
| empty_carrier(sK206)
| ~ one_sorted_str(sK206) ),
inference(resolution,[],[f6218,f7357]) ).
fof(f7551,plain,
( ~ filtered_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206)))
| ~ upper_relstr_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206)))
| filter_of_net_str(sK206,net_of_bool_filter(sK206,cast_as_carrier_subset(sK206),sK207)) = set_difference(sK207,the_carrier(boole_POSet(empty_set)))
| empty_carrier(sK206)
| ~ one_sorted_str(sK206) ),
inference(forward_subsumption_resolution,[],[f7550,f3467]) ).
fof(f7552,plain,
( ~ upper_relstr_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206)))
| filter_of_net_str(sK206,net_of_bool_filter(sK206,cast_as_carrier_subset(sK206),sK207)) = set_difference(sK207,the_carrier(boole_POSet(empty_set)))
| empty_carrier(sK206)
| ~ one_sorted_str(sK206) ),
inference(forward_subsumption_resolution,[],[f7551,f3466]) ).
fof(f7553,plain,
( filter_of_net_str(sK206,net_of_bool_filter(sK206,cast_as_carrier_subset(sK206),sK207)) = set_difference(sK207,the_carrier(boole_POSet(empty_set)))
| empty_carrier(sK206)
| ~ one_sorted_str(sK206) ),
inference(forward_subsumption_resolution,[],[f7552,f3465]) ).
fof(f7554,plain,
( filter_of_net_str(sK206,net_of_bool_filter(sK206,cast_as_carrier_subset(sK206),sK207)) = set_difference(sK207,the_carrier(boole_POSet(empty_set)))
| ~ one_sorted_str(sK206) ),
inference(forward_subsumption_resolution,[],[f7553,f3462]) ).
fof(f7555,plain,
filter_of_net_str(sK206,net_of_bool_filter(sK206,cast_as_carrier_subset(sK206),sK207)) = set_difference(sK207,the_carrier(boole_POSet(empty_set))),
inference(forward_subsumption_resolution,[],[f7554,f3461]) ).
fof(f7556,plain,
sK207 != set_difference(sK207,the_carrier(boole_POSet(empty_set))),
inference(superposition,[],[f3468,f7555]) ).
fof(f7600,plain,
( ~ in(bottom_of_relstr(boole_POSet(cast_as_carrier_subset(sK206))),sK207)
| ~ filtered_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206)))
| ~ upper_relstr_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206)))
| ~ element(sK207,the_carrier(boole_POSet(the_carrier(boole_POSet(cast_as_carrier_subset(sK206))))))
| empty_carrier(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ reflexive_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ transitive_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ antisymmetric_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ lower_bounded_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ rel_str(boole_POSet(cast_as_carrier_subset(sK206))) ),
inference(resolution,[],[f7323,f6217]) ).
fof(f7603,plain,
( ~ in(bottom_of_relstr(boole_POSet(cast_as_carrier_subset(sK206))),sK207)
| ~ upper_relstr_subset(sK207,boole_POSet(cast_as_carrier_subset(sK206)))
| ~ element(sK207,the_carrier(boole_POSet(the_carrier(boole_POSet(cast_as_carrier_subset(sK206))))))
| empty_carrier(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ reflexive_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ transitive_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ antisymmetric_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ lower_bounded_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ rel_str(boole_POSet(cast_as_carrier_subset(sK206))) ),
inference(forward_subsumption_resolution,[],[f7600,f3466]) ).
fof(f7604,plain,
( ~ in(bottom_of_relstr(boole_POSet(cast_as_carrier_subset(sK206))),sK207)
| ~ element(sK207,the_carrier(boole_POSet(the_carrier(boole_POSet(cast_as_carrier_subset(sK206))))))
| empty_carrier(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ reflexive_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ transitive_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ antisymmetric_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ lower_bounded_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ rel_str(boole_POSet(cast_as_carrier_subset(sK206))) ),
inference(forward_subsumption_resolution,[],[f7603,f3465]) ).
fof(f7605,plain,
( ~ in(bottom_of_relstr(boole_POSet(cast_as_carrier_subset(sK206))),sK207)
| empty_carrier(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ reflexive_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ transitive_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ antisymmetric_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ lower_bounded_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ rel_str(boole_POSet(cast_as_carrier_subset(sK206))) ),
inference(forward_subsumption_resolution,[],[f7604,f6218]) ).
fof(f7606,plain,
( ~ in(bottom_of_relstr(boole_POSet(cast_as_carrier_subset(sK206))),sK207)
| ~ reflexive_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ transitive_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ antisymmetric_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ lower_bounded_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ rel_str(boole_POSet(cast_as_carrier_subset(sK206))) ),
inference(forward_subsumption_resolution,[],[f7605,f5688]) ).
fof(f7607,plain,
( ~ in(bottom_of_relstr(boole_POSet(cast_as_carrier_subset(sK206))),sK207)
| ~ transitive_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ antisymmetric_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ lower_bounded_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ rel_str(boole_POSet(cast_as_carrier_subset(sK206))) ),
inference(forward_subsumption_resolution,[],[f7606,f5686]) ).
fof(f7608,plain,
( ~ in(bottom_of_relstr(boole_POSet(cast_as_carrier_subset(sK206))),sK207)
| ~ antisymmetric_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ lower_bounded_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ rel_str(boole_POSet(cast_as_carrier_subset(sK206))) ),
inference(forward_subsumption_resolution,[],[f7607,f5685]) ).
fof(f7609,plain,
( ~ in(bottom_of_relstr(boole_POSet(cast_as_carrier_subset(sK206))),sK207)
| ~ lower_bounded_relstr(boole_POSet(cast_as_carrier_subset(sK206)))
| ~ rel_str(boole_POSet(cast_as_carrier_subset(sK206))) ),
inference(forward_subsumption_resolution,[],[f7608,f5684]) ).
fof(f7610,plain,
( ~ in(bottom_of_relstr(boole_POSet(cast_as_carrier_subset(sK206))),sK207)
| ~ rel_str(boole_POSet(cast_as_carrier_subset(sK206))) ),
inference(forward_subsumption_resolution,[],[f7609,f5683]) ).
fof(f7611,plain,
~ in(bottom_of_relstr(boole_POSet(cast_as_carrier_subset(sK206))),sK207),
inference(forward_subsumption_resolution,[],[f7610,f4645]) ).
fof(f7612,plain,
~ in(empty_set,sK207),
inference(forward_demodulation,[],[f7611,f3505]) ).
fof(f12599,plain,
sK207 = set_difference(sK207,unordered_pair(empty_set,empty_set)),
inference(resolution,[],[f6313,f7612]) ).
fof(f12605,plain,
sK207 = set_difference(sK207,the_carrier(boole_POSet(empty_set))),
inference(forward_demodulation,[],[f12599,f6237]) ).
fof(f12610,plain,
$false,
inference(forward_subsumption_resolution,[],[f12605,f7556]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU394+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n002.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 05:08:07 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.90/2.64 % (4161047)Detected formulas, will run a generic FOF schedule.
% 11.90/2.64 % (4161056)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2851839280:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.90/2.64 % (4161056)Instruction limit reached!
% 11.90/2.64 % (4161056)------------------------------
% 11.90/2.64 % (4161056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.90/2.64 % (4161056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.90/2.64 % (4161056)CaDiCaL version: 2.1.3
% 11.90/2.64 % (4161056)Termination reason: Instruction limit
% 11.90/2.64 % (4161056)Termination phase: Saturation
% 11.90/2.64 % (4161056)Time elapsed: 0.040 s
% 11.90/2.64 % (4161056)Peak memory usage: 92 MB
% 11.90/2.64 % (4161056)Instructions burned: 122 (million)
% 11.90/2.64 % (4161057)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=979691089:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.90/2.64 % (4161054)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2954445090:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.90/2.64 % (4161055)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3206641145:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.90/2.64 % (4161053)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=714100680:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.90/2.64 % (4161058)dis-21_1_sil=8000:lcm=predicate:random_seed=254081420:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.90/2.64 % (4161052)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=251378161:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.90/2.64 % (4161055)Instruction limit reached!
% 11.90/2.64 % (4161055)------------------------------
% 11.90/2.64 % (4161055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.90/2.64 % (4161055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.90/2.64 % (4161055)CaDiCaL version: 2.1.3
% 11.90/2.64 % (4161055)Termination reason: Instruction limit
% 11.90/2.64 % (4161055)Termination phase: Blocked clause elimination
% 11.90/2.64 % (4161055)Time elapsed: 0.063 s
% 11.90/2.64 % (4161055)Peak memory usage: 90 MB
% 11.90/2.64 % (4161055)Instructions burned: 110 (million)
% 11.90/2.64 % (4161058)Instruction limit reached!
% 11.90/2.64 % (4161058)------------------------------
% 11.90/2.64 % (4161058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.90/2.64 % (4161058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.90/2.64 % (4161058)CaDiCaL version: 2.1.3
% 11.90/2.64 % (4161058)Termination reason: Instruction limit
% 11.90/2.64 % (4161058)Termination phase: Saturation
% 11.90/2.64 % (4161058)Time elapsed: 0.068 s
% 11.90/2.64 % (4161058)Peak memory usage: 92 MB
% 11.90/2.64 % (4161058)Instructions burned: 129 (million)
% 11.90/2.64 % (4161057)Instruction limit reached!
% 11.90/2.64 % (4161057)------------------------------
% 11.90/2.64 % (4161057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.90/2.64 % (4161057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.90/2.64 % (4161057)CaDiCaL version: 2.1.3
% 11.90/2.64 % (4161057)Termination reason: Instruction limit
% 11.90/2.64 % (4161057)Termination phase: Saturation
% 11.90/2.64 % (4161057)Time elapsed: 0.079 s
% 11.90/2.64 % (4161057)Peak memory usage: 92 MB
% 11.90/2.64 % (4161057)Instructions burned: 139 (million)
% 11.90/2.64 % (4161060)lrs+10_1_sil=8000:sp=occurrence:random_seed=2935765633:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.90/2.64 % (4161060)Instruction limit reached!
% 11.90/2.64 % (4161060)------------------------------
% 11.90/2.64 % (4161060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.90/2.64 % (4161060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.90/2.64 % (4161060)CaDiCaL version: 2.1.3
% 11.90/2.64 % (4161060)Termination reason: Instruction limit
% 11.90/2.64 % (4161060)Termination phase: Saturation
% 11.90/2.64 % (4161060)Time elapsed: 0.095 s
% 11.90/2.64 % (4161060)Peak memory usage: 95 MB
% 11.90/2.64 % (4161060)Instructions burned: 285 (million)
% 17.28/3.39 % (4161068)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2809637779:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 17.28/3.39 % (4161067)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2153220279:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 17.28/3.39 % (4161070)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1940701605:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 17.28/3.39 % (4161071)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4252432267:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 17.28/3.39 % (4161067)Instruction limit reached!
% 17.28/3.39 % (4161067)------------------------------
% 17.28/3.39 % (4161067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161067)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161067)Termination reason: Instruction limit
% 17.28/3.39 % (4161067)Termination phase: Saturation
% 17.28/3.39 % (4161067)Time elapsed: 0.092 s
% 17.28/3.39 % (4161067)Peak memory usage: 91 MB
% 17.28/3.39 % (4161067)Instructions burned: 158 (million)
% 17.28/3.39 % (4161070)Instruction limit reached!
% 17.28/3.39 % (4161070)------------------------------
% 17.28/3.39 % (4161070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161070)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161070)Termination reason: Instruction limit
% 17.28/3.39 % (4161070)Termination phase: Saturation
% 17.28/3.39 % (4161070)Time elapsed: 0.150 s
% 17.28/3.39 % (4161070)Peak memory usage: 94 MB
% 17.28/3.39 % (4161070)Instructions burned: 249 (million)
% 17.28/3.39 % (4161071)Instruction limit reached!
% 17.28/3.39 % (4161071)------------------------------
% 17.28/3.39 % (4161071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161071)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161071)Termination reason: Instruction limit
% 17.28/3.39 % (4161071)Termination phase: Saturation
% 17.28/3.39 % (4161071)Time elapsed: 0.093 s
% 17.28/3.39 % (4161071)Peak memory usage: 94 MB
% 17.28/3.39 % (4161071)Instructions burned: 296 (million)
% 17.28/3.39 % (4161068)Instruction limit reached!
% 17.28/3.39 % (4161068)------------------------------
% 17.28/3.39 % (4161068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161068)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161068)Termination reason: Instruction limit
% 17.28/3.39 % (4161068)Termination phase: Saturation
% 17.28/3.39 % (4161068)Time elapsed: 0.209 s
% 17.28/3.39 % (4161068)Peak memory usage: 96 MB
% 17.28/3.39 % (4161068)Instructions burned: 327 (million)
% 17.28/3.39 % (4161076)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1493942688:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 17.28/3.39 % (4161078)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2983022723:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 17.28/3.39 % (4161077)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1128983356:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 17.28/3.39 % (4161078)Instruction limit reached!
% 17.28/3.39 % (4161078)------------------------------
% 17.28/3.39 % (4161078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161078)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161078)Termination reason: Instruction limit
% 17.28/3.39 % (4161078)Termination phase: Blocked clause elimination
% 17.28/3.39 % (4161078)Time elapsed: 0.039 s
% 17.28/3.39 % (4161078)Peak memory usage: 91 MB
% 17.28/3.39 % (4161078)Instructions burned: 129 (million)
% 17.28/3.39 % (4161079)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4003967221:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 17.28/3.39 % (4161077)Instruction limit reached!
% 17.28/3.39 % (4161077)------------------------------
% 17.28/3.39 % (4161077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161077)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161077)Termination reason: Instruction limit
% 17.28/3.39 % (4161077)Termination phase: Saturation
% 17.28/3.39 % (4161077)Time elapsed: 0.063 s
% 17.28/3.39 % (4161077)Peak memory usage: 92 MB
% 17.28/3.39 % (4161077)Instructions burned: 114 (million)
% 17.28/3.39 % (4161083)lrs+10_1_sil=8000:sp=occurrence:random_seed=991805352:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 17.28/3.39 % (4161079)Instruction limit reached!
% 17.28/3.39 % (4161079)------------------------------
% 17.28/3.39 % (4161079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161079)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161079)Termination reason: Instruction limit
% 17.28/3.39 % (4161079)Termination phase: Saturation
% 17.28/3.39 % (4161079)Time elapsed: 0.057 s
% 17.28/3.39 % (4161079)Peak memory usage: 90 MB
% 17.28/3.39 % (4161079)Instructions burned: 114 (million)
% 17.28/3.39 % (4161085)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2937486506:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 17.28/3.39 % (4161087)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2772709341:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 17.28/3.39 % (4161083)Instruction limit reached!
% 17.28/3.39 % (4161083)------------------------------
% 17.28/3.39 % (4161083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161083)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161083)Termination reason: Instruction limit
% 17.28/3.39 % (4161083)Termination phase: Saturation
% 17.28/3.39 % (4161083)Time elapsed: 0.321 s
% 17.28/3.39 % (4161083)Peak memory usage: 106 MB
% 17.28/3.39 % (4161083)Instructions burned: 909 (million)
% 17.28/3.39 % (4161085)Instruction limit reached!
% 17.28/3.39 % (4161085)------------------------------
% 17.28/3.39 % (4161085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161085)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161085)Termination reason: Instruction limit
% 17.28/3.39 % (4161085)Termination phase: Saturation
% 17.28/3.39 % (4161085)Time elapsed: 0.269 s
% 17.28/3.39 % (4161085)Peak memory usage: 97 MB
% 17.28/3.39 % (4161085)Instructions burned: 437 (million)
% 17.28/3.39 % (4161090)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=310558236:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 17.28/3.39 % (4161090)Instruction limit reached!
% 17.28/3.39 % (4161090)------------------------------
% 17.28/3.39 % (4161090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161090)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161090)Termination reason: Instruction limit
% 17.28/3.39 % (4161090)Termination phase: Property scanning
% 17.28/3.39 % (4161090)Time elapsed: 0.038 s
% 17.28/3.39 % (4161090)Peak memory usage: 90 MB
% 17.28/3.39 % (4161090)Instructions burned: 138 (million)
% 17.28/3.39 % (4161091)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2296058093:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 17.28/3.39 % (4161093)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1919173532:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 17.28/3.39 % (4161091)Instruction limit reached!
% 17.28/3.39 % (4161091)------------------------------
% 17.28/3.39 % (4161091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161091)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161091)Termination reason: Instruction limit
% 17.28/3.39 % (4161091)Termination phase: Saturation
% 17.28/3.39 % (4161091)Time elapsed: 0.355 s
% 17.28/3.39 % (4161091)Peak memory usage: 103 MB
% 17.28/3.39 % (4161091)Instructions burned: 593 (million)
% 17.28/3.39 % (4161097)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3802085229:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 17.28/3.39 % (4161097)Instruction limit reached!
% 17.28/3.39 % (4161097)------------------------------
% 17.28/3.39 % (4161097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161097)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161097)Termination reason: Instruction limit
% 17.28/3.39 % (4161097)Termination phase: Saturation
% 17.28/3.39 % (4161097)Time elapsed: 0.072 s
% 17.28/3.39 % (4161097)Peak memory usage: 92 MB
% 17.28/3.39 % (4161097)Instructions burned: 125 (million)
% 17.28/3.39 % (4161099)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=811079176:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 17.28/3.39 % (4161099)Instruction limit reached!
% 17.28/3.39 % (4161099)------------------------------
% 17.28/3.39 % (4161099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161099)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161099)Termination reason: Instruction limit
% 17.28/3.39 % (4161099)Termination phase: Saturation
% 17.28/3.39 % (4161099)Time elapsed: 0.069 s
% 17.28/3.39 % (4161099)Peak memory usage: 92 MB
% 17.28/3.39 % (4161099)Instructions burned: 134 (million)
% 17.28/3.39 % (4161076)Instruction limit reached!
% 17.28/3.39 % (4161076)------------------------------
% 17.28/3.39 % (4161076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161076)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161076)Termination reason: Instruction limit
% 17.28/3.39 % (4161076)Termination phase: Saturation
% 17.28/3.39 % (4161076)Time elapsed: 1.482 s
% 17.28/3.39 % (4161076)Peak memory usage: 172 MB
% 17.28/3.39 % (4161076)Instructions burned: 2351 (million)
% 17.28/3.39 % (4161101)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=69008240:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 17.28/3.39 % (4161102)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2846137048:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi)
% 17.28/3.39 % (4161101)Instruction limit reached!
% 17.28/3.39 % (4161101)------------------------------
% 17.28/3.39 % (4161101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161101)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161101)Termination reason: Instruction limit
% 17.28/3.39 % (4161101)Termination phase: Saturation
% 17.28/3.39 % (4161101)Time elapsed: 0.071 s
% 17.28/3.39 % (4161101)Peak memory usage: 92 MB
% 17.28/3.39 % (4161101)Instructions burned: 141 (million)
% 17.28/3.39 % (4161093)First to succeed.
% 17.28/3.39 % (4161093)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4161047"
% 17.28/3.39 % (4161105)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=45350412:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi)
% 17.28/3.39 % (4161102)Instruction limit reached!
% 17.28/3.39 % (4161102)------------------------------
% 17.28/3.39 % (4161102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.28/3.39 % (4161102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.28/3.39 % (4161102)CaDiCaL version: 2.1.3
% 17.28/3.39 % (4161102)Termination reason: Instruction limit
% 17.28/3.39 % (4161102)Termination phase: Saturation
% 17.28/3.39 % (4161102)Time elapsed: 0.246 s
% 17.28/3.39 % (4161102)Peak memory usage: 96 MB
% 17.28/3.39 % (4161102)Instructions burned: 431 (million)
% 17.28/3.39 % (4161093)Refutation found. Thanks to Tanya!
% 17.28/3.39 % SZS status Theorem for theBenchmark
% 17.28/3.39 % SZS output start Proof for theBenchmark
% See solution above
% 18.12/3.48 % (4161093)------------------------------
% 18.12/3.48 % (4161093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.12/3.48 % (4161093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.12/3.48 % (4161093)CaDiCaL version: 2.1.3
% 18.12/3.48 % (4161093)Termination reason: Refutation
% 18.12/3.48 % (4161093)Time elapsed: 1.045 s
% 18.12/3.48 % (4161093)Peak memory usage: 168 MB
% 18.12/3.48 % (4161093)Instructions burned: 3147 (million)
% 18.12/3.48 % (4161093)------------------------------
% 18.12/3.48 % (4161093)------------------------------
% 18.12/3.48 % (4161047)Success in time 2.531 s
% 18.12/3.48 % Vampire exiting
%------------------------------------------------------------------------------