%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU363+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 : n012.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:33 PM UTC 2026
% Result : Theorem 41.56s 6.59s
% Output : Refutation 42.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 40
% Syntax : Number of formulae : 209 ( 73 unt; 25 def)
% Number of atoms : 570 ( 45 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 615 ( 254 ~; 246 |; 59 &)
% ( 30 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 24 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 8 con; 0-2 aty)
% Number of variables : 153 ( 0 sgn 141 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [X0,X1,X2] :
( element(X2,powerset(cartesian_product2(X0,X1)))
=> relation(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f43,axiom,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f67,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1] :
( subrelstr(X1,X0)
=> ( full_subrelstr(X1,X0)
<=> the_InternalRel(X1) = relation_restriction_as_relation_of(the_InternalRel(X0),the_carrier(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d14_yellow_0) ).
fof(f137,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f161,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( related(X0,X1,X2)
<=> in(ordered_pair(X1,X2),the_InternalRel(X0)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_orders_2) ).
fof(f246,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1] :
( subrelstr(X1,X0)
=> rel_str(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
fof(f247,axiom,
! [X0,X1,X2] :
( relation_of2_as_subset(X2,X0,X1)
=> element(X2,powerset(cartesian_product2(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f249,axiom,
! [X0] :
( rel_str(X0)
=> relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_orders_2) ).
fof(f413,axiom,
! [X0] : k1_pcomps_1(X0) = powerset(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_pcomps_1) ).
fof(f414,axiom,
! [X0,X1] :
( relation(X0)
=> relation_restriction_as_relation_of(X0,X1) = relation_restriction(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_toler_1) ).
fof(f483,axiom,
! [X0,X1,X2,X3] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
<=> ( in(X0,X2)
& in(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t106_zfmisc_1) ).
fof(f520,axiom,
! [X0,X1,X2] :
( relation(X2)
=> ( in(X0,relation_restriction(X2,X1))
<=> ( in(X0,X2)
& in(X0,cartesian_product2(X1,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_wellord1) ).
fof(f656,conjecture,
! [X0] :
( rel_str(X0)
=> ! [X1] :
( ( full_subrelstr(X1,X0)
& subrelstr(X1,X0) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ! [X3] :
( element(X3,the_carrier(X0))
=> ! [X4] :
( element(X4,the_carrier(X1))
=> ! [X5] :
( element(X5,the_carrier(X1))
=> ( ( X4 = X2
& X5 = X3
& related(X0,X2,X3)
& in(X4,the_carrier(X1))
& in(X5,the_carrier(X1)) )
=> related(X1,X4,X5) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t61_yellow_0) ).
fof(f657,negated_conjecture,
~ ! [X0] :
( rel_str(X0)
=> ! [X1] :
( ( full_subrelstr(X1,X0)
& subrelstr(X1,X0) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ! [X3] :
( element(X3,the_carrier(X0))
=> ! [X4] :
( element(X4,the_carrier(X1))
=> ! [X5] :
( element(X5,the_carrier(X1))
=> ( ( X4 = X2
& X5 = X3
& related(X0,X2,X3)
& in(X4,the_carrier(X1))
& in(X5,the_carrier(X1)) )
=> related(X1,X4,X5) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f656]) ).
fof(f664,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f790,plain,
! [X0,X1,X2] :
( relation(X2)
| ~ element(X2,powerset(cartesian_product2(X0,X1))) ),
inference(ennf_transformation,[],[f25]) ).
fof(f848,plain,
! [X0] :
( ! [X1] :
( ( full_subrelstr(X1,X0)
<=> the_InternalRel(X1) = relation_restriction_as_relation_of(the_InternalRel(X0),the_carrier(X1)) )
| ~ subrelstr(X1,X0) )
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f67]) ).
fof(f958,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( related(X0,X1,X2)
<=> in(ordered_pair(X1,X2),the_InternalRel(X0)) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f161]) ).
fof(f1037,plain,
! [X0] :
( ! [X1] :
( rel_str(X1)
| ~ subrelstr(X1,X0) )
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f246]) ).
fof(f1038,plain,
! [X0,X1,X2] :
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(ennf_transformation,[],[f247]) ).
fof(f1040,plain,
! [X0] :
( relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f249]) ).
fof(f1190,plain,
! [X0,X1] :
( relation_restriction_as_relation_of(X0,X1) = relation_restriction(X0,X1)
| ~ relation(X0) ),
inference(ennf_transformation,[],[f414]) ).
fof(f1352,plain,
! [X0,X1,X2] :
( ( in(X0,relation_restriction(X2,X1))
<=> ( in(X0,X2)
& in(X0,cartesian_product2(X1,X1)) ) )
| ~ relation(X2) ),
inference(ennf_transformation,[],[f520]) ).
fof(f1532,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ~ related(X1,X4,X5)
& X4 = X2
& X5 = X3
& related(X0,X2,X3)
& in(X4,the_carrier(X1))
& in(X5,the_carrier(X1))
& element(X5,the_carrier(X1)) )
& element(X4,the_carrier(X1)) )
& element(X3,the_carrier(X0)) )
& element(X2,the_carrier(X0)) )
& full_subrelstr(X1,X0)
& subrelstr(X1,X0) )
& rel_str(X0) ),
inference(ennf_transformation,[],[f657]) ).
fof(f1533,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ~ related(X1,X4,X5)
& X4 = X2
& X5 = X3
& related(X0,X2,X3)
& in(X4,the_carrier(X1))
& in(X5,the_carrier(X1))
& element(X5,the_carrier(X1)) )
& element(X4,the_carrier(X1)) )
& element(X3,the_carrier(X0)) )
& element(X2,the_carrier(X0)) )
& full_subrelstr(X1,X0)
& subrelstr(X1,X0) )
& rel_str(X0) ),
inference(flattening,[],[f1532]) ).
fof(f1713,plain,
! [X0] :
( ! [X1] :
( ( ( full_subrelstr(X1,X0)
| the_InternalRel(X1) != relation_restriction_as_relation_of(the_InternalRel(X0),the_carrier(X1)) )
& ( the_InternalRel(X1) = relation_restriction_as_relation_of(the_InternalRel(X0),the_carrier(X1))
| ~ full_subrelstr(X1,X0) ) )
| ~ subrelstr(X1,X0) )
| ~ rel_str(X0) ),
inference(nnf_transformation,[],[f848]) ).
fof(f1922,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( related(X0,X1,X2)
| ~ in(ordered_pair(X1,X2),the_InternalRel(X0)) )
& ( in(ordered_pair(X1,X2),the_InternalRel(X0))
| ~ related(X0,X1,X2) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(nnf_transformation,[],[f958]) ).
fof(f2259,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(nnf_transformation,[],[f483]) ).
fof(f2260,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(flattening,[],[f2259]) ).
fof(f2278,plain,
! [X0,X1,X2] :
( ( ( in(X0,relation_restriction(X2,X1))
| ~ in(X0,X2)
| ~ in(X0,cartesian_product2(X1,X1)) )
& ( ( in(X0,X2)
& in(X0,cartesian_product2(X1,X1)) )
| ~ in(X0,relation_restriction(X2,X1)) ) )
| ~ relation(X2) ),
inference(nnf_transformation,[],[f1352]) ).
fof(f2279,plain,
! [X0,X1,X2] :
( ( ( in(X0,relation_restriction(X2,X1))
| ~ in(X0,X2)
| ~ in(X0,cartesian_product2(X1,X1)) )
& ( ( in(X0,X2)
& in(X0,cartesian_product2(X1,X1)) )
| ~ in(X0,relation_restriction(X2,X1)) ) )
| ~ relation(X2) ),
inference(flattening,[],[f2278]) ).
fof(f2346,plain,
( ~ related(sK518,sK521,sK522)
& sK519 = sK521
& sK520 = sK522
& related(sK517,sK519,sK520)
& in(sK521,the_carrier(sK518))
& in(sK522,the_carrier(sK518))
& element(sK522,the_carrier(sK518))
& element(sK521,the_carrier(sK518))
& element(sK520,the_carrier(sK517))
& element(sK519,the_carrier(sK517))
& full_subrelstr(sK518,sK517)
& subrelstr(sK518,sK517)
& rel_str(sK517) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK517,sK518,sK519,sK520,sK521,sK522]),skolemize(X0,sK517),skolemize(X1,sK518),skolemize(X2,sK519),skolemize(X3,sK520),skolemize(X4,sK521),skolemize(X5,sK522)],[f1533]) ).
fof(f2406,plain,
! [X2,X0,X1] :
( relation(X2)
| ~ element(X2,powerset(cartesian_product2(X0,X1))) ),
inference(cnf_transformation,[],[f790]) ).
fof(f2453,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f43]) ).
fof(f2541,plain,
! [X0,X1] :
( ~ full_subrelstr(X1,X0)
| the_InternalRel(X1) = relation_restriction_as_relation_of(the_InternalRel(X0),the_carrier(X1))
| ~ subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1713]) ).
fof(f2811,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f137]) ).
fof(f2920,plain,
! [X2,X0,X1] :
( in(ordered_pair(X1,X2),the_InternalRel(X0))
| ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1922]) ).
fof(f2921,plain,
! [X2,X0,X1] :
( related(X0,X1,X2)
| ~ in(ordered_pair(X1,X2),the_InternalRel(X0))
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1922]) ).
fof(f3001,plain,
! [X0,X1] :
( rel_str(X1)
| ~ subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1037]) ).
fof(f3002,plain,
! [X2,X0,X1] :
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[],[f1038]) ).
fof(f3006,plain,
! [X0] :
( relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1040]) ).
fof(f3416,plain,
! [X0] : powerset(X0) = k1_pcomps_1(X0),
inference(cnf_transformation,[],[f413]) ).
fof(f3417,plain,
! [X0,X1] :
( relation_restriction(X0,X1) = relation_restriction_as_relation_of(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1190]) ).
fof(f3930,plain,
! [X2,X3,X0,X1] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) ),
inference(cnf_transformation,[],[f2260]) ).
fof(f3994,plain,
! [X2,X0,X1] :
( in(X0,relation_restriction(X2,X1))
| ~ in(X0,X2)
| ~ in(X0,cartesian_product2(X1,X1))
| ~ relation(X2) ),
inference(cnf_transformation,[],[f2279]) ).
fof(f4232,plain,
rel_str(sK517),
inference(cnf_transformation,[],[f2346]) ).
fof(f4233,plain,
subrelstr(sK518,sK517),
inference(cnf_transformation,[],[f2346]) ).
fof(f4234,plain,
full_subrelstr(sK518,sK517),
inference(cnf_transformation,[],[f2346]) ).
fof(f4235,plain,
element(sK519,the_carrier(sK517)),
inference(cnf_transformation,[],[f2346]) ).
fof(f4236,plain,
element(sK520,the_carrier(sK517)),
inference(cnf_transformation,[],[f2346]) ).
fof(f4237,plain,
element(sK521,the_carrier(sK518)),
inference(cnf_transformation,[],[f2346]) ).
fof(f4238,plain,
element(sK522,the_carrier(sK518)),
inference(cnf_transformation,[],[f2346]) ).
fof(f4239,plain,
in(sK522,the_carrier(sK518)),
inference(cnf_transformation,[],[f2346]) ).
fof(f4240,plain,
in(sK521,the_carrier(sK518)),
inference(cnf_transformation,[],[f2346]) ).
fof(f4241,plain,
related(sK517,sK519,sK520),
inference(cnf_transformation,[],[f2346]) ).
fof(f4242,plain,
sK520 = sK522,
inference(cnf_transformation,[],[f2346]) ).
fof(f4243,plain,
sK519 = sK521,
inference(cnf_transformation,[],[f2346]) ).
fof(f4244,plain,
~ related(sK518,sK521,sK522),
inference(cnf_transformation,[],[f2346]) ).
fof(f4257,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f664]) ).
fof(f4312,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f2811,f4257]) ).
fof(f4324,plain,
! [X2,X0,X1] :
( relation(X2)
| ~ element(X2,k1_pcomps_1(cartesian_product2(X0,X1))) ),
inference(definition_unfolding,[],[f2406,f3416]) ).
fof(f4493,plain,
! [X2,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X1,X2),unordered_pair(X1,X1)),the_InternalRel(X0))
| related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(definition_unfolding,[],[f2921,f4312]) ).
fof(f4494,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(X1,X2),unordered_pair(X1,X1)),the_InternalRel(X0))
| ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(definition_unfolding,[],[f2920,f4312]) ).
fof(f4512,plain,
! [X2,X0,X1] :
( element(X2,k1_pcomps_1(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(definition_unfolding,[],[f3002,f3416]) ).
fof(f4885,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) ),
inference(definition_unfolding,[],[f3930,f4312]) ).
fof(f4990,plain,
related(sK517,sK521,sK522),
inference(definition_unfolding,[],[f4241,f4243,f4242]) ).
fof(f4991,plain,
element(sK522,the_carrier(sK517)),
inference(definition_unfolding,[],[f4236,f4242]) ).
fof(f4992,plain,
element(sK521,the_carrier(sK517)),
inference(definition_unfolding,[],[f4235,f4243]) ).
fof(f5283,definition,
sF527 = the_carrier(sK518),
introduced(definition,[new_symbols(definition,[sF527])],[function_definition]) ).
fof(f5284,plain,
the_carrier(sK518) = sF527,
inference(reorient_equations,[],[f5283]) ).
fof(f5285,plain,
in(sK521,sF527),
inference(definition_folding,[],[f4240,f5284]) ).
fof(f5286,plain,
in(sK522,sF527),
inference(definition_folding,[],[f4239,f5284]) ).
fof(f5287,plain,
element(sK522,sF527),
inference(definition_folding,[],[f4238,f5284]) ).
fof(f5288,plain,
element(sK521,sF527),
inference(definition_folding,[],[f4237,f5284]) ).
fof(f5289,definition,
sF528 = the_carrier(sK517),
introduced(definition,[new_symbols(definition,[sF528])],[function_definition]) ).
fof(f5290,plain,
the_carrier(sK517) = sF528,
inference(reorient_equations,[],[f5289]) ).
fof(f5291,plain,
element(sK522,sF528),
inference(definition_folding,[],[f4991,f5290]) ).
fof(f5292,plain,
element(sK521,sF528),
inference(definition_folding,[],[f4992,f5290]) ).
fof(f5315,definition,
( spl529_1
<=> rel_str(sK517) ),
introduced(definition,[new_symbols(definition,[spl529_1])],[avatar_definition]) ).
fof(f5317,plain,
( rel_str(sK517)
| ~ spl529_1 ),
inference(avatar_component_clause,[],[f5315]) ).
fof(f5318,plain,
spl529_1,
inference(avatar_split_clause,[],[f4232,f5315]) ).
fof(f5320,definition,
( spl529_2
<=> subrelstr(sK518,sK517) ),
introduced(definition,[new_symbols(definition,[spl529_2])],[avatar_definition]) ).
fof(f5322,plain,
( subrelstr(sK518,sK517)
| ~ spl529_2 ),
inference(avatar_component_clause,[],[f5320]) ).
fof(f5323,plain,
spl529_2,
inference(avatar_split_clause,[],[f4233,f5320]) ).
fof(f5325,definition,
( spl529_3
<=> full_subrelstr(sK518,sK517) ),
introduced(definition,[new_symbols(definition,[spl529_3])],[avatar_definition]) ).
fof(f5327,plain,
( full_subrelstr(sK518,sK517)
| ~ spl529_3 ),
inference(avatar_component_clause,[],[f5325]) ).
fof(f5328,plain,
spl529_3,
inference(avatar_split_clause,[],[f4234,f5325]) ).
fof(f5330,definition,
( spl529_4
<=> element(sK521,sF528) ),
introduced(definition,[new_symbols(definition,[spl529_4])],[avatar_definition]) ).
fof(f5332,plain,
( element(sK521,sF528)
| ~ spl529_4 ),
inference(avatar_component_clause,[],[f5330]) ).
fof(f5333,plain,
spl529_4,
inference(avatar_split_clause,[],[f5292,f5330]) ).
fof(f5335,definition,
( spl529_5
<=> element(sK522,sF528) ),
introduced(definition,[new_symbols(definition,[spl529_5])],[avatar_definition]) ).
fof(f5337,plain,
( element(sK522,sF528)
| ~ spl529_5 ),
inference(avatar_component_clause,[],[f5335]) ).
fof(f5338,plain,
spl529_5,
inference(avatar_split_clause,[],[f5291,f5335]) ).
fof(f5340,definition,
( spl529_6
<=> element(sK521,sF527) ),
introduced(definition,[new_symbols(definition,[spl529_6])],[avatar_definition]) ).
fof(f5342,plain,
( element(sK521,sF527)
| ~ spl529_6 ),
inference(avatar_component_clause,[],[f5340]) ).
fof(f5343,plain,
spl529_6,
inference(avatar_split_clause,[],[f5288,f5340]) ).
fof(f5345,definition,
( spl529_7
<=> element(sK522,sF527) ),
introduced(definition,[new_symbols(definition,[spl529_7])],[avatar_definition]) ).
fof(f5347,plain,
( element(sK522,sF527)
| ~ spl529_7 ),
inference(avatar_component_clause,[],[f5345]) ).
fof(f5348,plain,
spl529_7,
inference(avatar_split_clause,[],[f5287,f5345]) ).
fof(f5350,definition,
( spl529_8
<=> in(sK522,sF527) ),
introduced(definition,[new_symbols(definition,[spl529_8])],[avatar_definition]) ).
fof(f5352,plain,
( in(sK522,sF527)
| ~ spl529_8 ),
inference(avatar_component_clause,[],[f5350]) ).
fof(f5353,plain,
spl529_8,
inference(avatar_split_clause,[],[f5286,f5350]) ).
fof(f5355,definition,
( spl529_9
<=> in(sK521,sF527) ),
introduced(definition,[new_symbols(definition,[spl529_9])],[avatar_definition]) ).
fof(f5357,plain,
( in(sK521,sF527)
| ~ spl529_9 ),
inference(avatar_component_clause,[],[f5355]) ).
fof(f5358,plain,
spl529_9,
inference(avatar_split_clause,[],[f5285,f5355]) ).
fof(f5360,definition,
( spl529_10
<=> related(sK517,sK521,sK522) ),
introduced(definition,[new_symbols(definition,[spl529_10])],[avatar_definition]) ).
fof(f5362,plain,
( related(sK517,sK521,sK522)
| ~ spl529_10 ),
inference(avatar_component_clause,[],[f5360]) ).
fof(f5363,plain,
spl529_10,
inference(avatar_split_clause,[],[f4990,f5360]) ).
fof(f5365,definition,
( spl529_11
<=> related(sK518,sK521,sK522) ),
introduced(definition,[new_symbols(definition,[spl529_11])],[avatar_definition]) ).
fof(f5367,plain,
( ~ related(sK518,sK521,sK522)
| spl529_11 ),
inference(avatar_component_clause,[],[f5365]) ).
fof(f5368,plain,
~ spl529_11,
inference(avatar_split_clause,[],[f4244,f5365]) ).
fof(f6231,definition,
( spl529_178
<=> the_carrier(sK518) = sF527 ),
introduced(definition,[new_symbols(definition,[spl529_178])],[avatar_definition]) ).
fof(f6233,plain,
( the_carrier(sK518) = sF527
| ~ spl529_178 ),
inference(avatar_component_clause,[],[f6231]) ).
fof(f6234,plain,
spl529_178,
inference(avatar_split_clause,[],[f5284,f6231]) ).
fof(f6236,definition,
( spl529_179
<=> the_carrier(sK517) = sF528 ),
introduced(definition,[new_symbols(definition,[spl529_179])],[avatar_definition]) ).
fof(f6238,plain,
( the_carrier(sK517) = sF528
| ~ spl529_179 ),
inference(avatar_component_clause,[],[f6236]) ).
fof(f6239,plain,
spl529_179,
inference(avatar_split_clause,[],[f5290,f6236]) ).
fof(f6279,plain,
( rel_str(sK518)
| ~ spl529_1
| ~ spl529_2 ),
inference(unit_resulting_resolution,[],[f3001,f5317,f5322]) ).
fof(f6282,definition,
( spl529_181
<=> rel_str(sK518) ),
introduced(definition,[new_symbols(definition,[spl529_181])],[avatar_definition]) ).
fof(f6284,plain,
( rel_str(sK518)
| ~ spl529_181 ),
inference(avatar_component_clause,[],[f6282]) ).
fof(f6285,plain,
( spl529_181
| ~ spl529_1
| ~ spl529_2 ),
inference(avatar_split_clause,[],[f6279,f5320,f5315,f6282]) ).
fof(f6294,plain,
( the_InternalRel(sK518) = relation_restriction_as_relation_of(the_InternalRel(sK517),the_carrier(sK518))
| ~ spl529_1
| ~ spl529_2
| ~ spl529_3 ),
inference(unit_resulting_resolution,[],[f2541,f5317,f5322,f5327]) ).
fof(f6297,plain,
( the_InternalRel(sK518) = relation_restriction_as_relation_of(the_InternalRel(sK517),sF527)
| ~ spl529_1
| ~ spl529_2
| ~ spl529_3
| ~ spl529_178 ),
inference(forward_demodulation,[],[f6294,f6233]) ).
fof(f6300,definition,
( spl529_182
<=> the_InternalRel(sK518) = relation_restriction_as_relation_of(the_InternalRel(sK517),sF527) ),
introduced(definition,[new_symbols(definition,[spl529_182])],[avatar_definition]) ).
fof(f6302,plain,
( the_InternalRel(sK518) = relation_restriction_as_relation_of(the_InternalRel(sK517),sF527)
| ~ spl529_182 ),
inference(avatar_component_clause,[],[f6300]) ).
fof(f6303,plain,
( spl529_182
| ~ spl529_1
| ~ spl529_2
| ~ spl529_3
| ~ spl529_178 ),
inference(avatar_split_clause,[],[f6297,f6231,f5325,f5320,f5315,f6300]) ).
fof(f6415,plain,
! [X2,X0,X1] :
( ~ rel_str(X2)
| ~ related(X2,X1,X0)
| ~ element(X0,the_carrier(X2))
| ~ element(X1,the_carrier(X2))
| in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X1,X1)),the_InternalRel(X2)) ),
inference(superposition,[],[f4494,f2453]) ).
fof(f6416,plain,
! [X2,X0,X1] :
( related(X2,X1,X0)
| ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X1,X1)),the_InternalRel(X2))
| ~ element(X0,the_carrier(X2))
| ~ element(X1,the_carrier(X2))
| ~ rel_str(X2) ),
inference(superposition,[],[f4493,f2453]) ).
fof(f6419,plain,
( ~ in(unordered_pair(unordered_pair(sK522,sK521),unordered_pair(sK521,sK521)),the_InternalRel(sK518))
| ~ element(sK522,the_carrier(sK518))
| ~ element(sK521,the_carrier(sK518))
| ~ rel_str(sK518)
| spl529_11 ),
inference(resolution,[],[f6416,f5367]) ).
fof(f6420,plain,
( ~ in(unordered_pair(unordered_pair(sK522,sK521),unordered_pair(sK521,sK521)),the_InternalRel(sK518))
| ~ element(sK522,the_carrier(sK518))
| ~ element(sK521,the_carrier(sK518))
| spl529_11
| ~ spl529_181 ),
inference(forward_subsumption_resolution,[],[f6419,f6284]) ).
fof(f6421,plain,
( ~ in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK522,sK521)),the_InternalRel(sK518))
| ~ element(sK522,the_carrier(sK518))
| ~ element(sK521,the_carrier(sK518))
| spl529_11
| ~ spl529_181 ),
inference(forward_demodulation,[],[f6420,f2453]) ).
fof(f6422,plain,
( ~ in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),the_InternalRel(sK518))
| ~ element(sK522,the_carrier(sK518))
| ~ element(sK521,the_carrier(sK518))
| spl529_11
| ~ spl529_181 ),
inference(forward_demodulation,[],[f6421,f2453]) ).
fof(f6423,plain,
( ~ element(sK522,sF527)
| ~ in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),the_InternalRel(sK518))
| ~ element(sK521,the_carrier(sK518))
| spl529_11
| ~ spl529_178
| ~ spl529_181 ),
inference(forward_demodulation,[],[f6422,f6233]) ).
fof(f6424,plain,
( ~ in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),the_InternalRel(sK518))
| ~ element(sK521,the_carrier(sK518))
| ~ spl529_7
| spl529_11
| ~ spl529_178
| ~ spl529_181 ),
inference(forward_subsumption_resolution,[],[f6423,f5347]) ).
fof(f6425,plain,
( ~ element(sK521,sF527)
| ~ in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),the_InternalRel(sK518))
| ~ spl529_7
| spl529_11
| ~ spl529_178
| ~ spl529_181 ),
inference(forward_demodulation,[],[f6424,f6233]) ).
fof(f6426,plain,
( ~ in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),the_InternalRel(sK518))
| ~ spl529_6
| ~ spl529_7
| spl529_11
| ~ spl529_178
| ~ spl529_181 ),
inference(forward_subsumption_resolution,[],[f6425,f5342]) ).
fof(f6428,definition,
( spl529_190
<=> in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),the_InternalRel(sK518)) ),
introduced(definition,[new_symbols(definition,[spl529_190])],[avatar_definition]) ).
fof(f6431,plain,
( ~ spl529_190
| ~ spl529_6
| ~ spl529_7
| spl529_11
| ~ spl529_178
| ~ spl529_181 ),
inference(avatar_split_clause,[],[f6426,f6282,f6231,f5365,f5345,f5340,f6428]) ).
fof(f6433,plain,
( ! [X0,X1] :
( ~ related(sK517,X0,X1)
| ~ element(X1,the_carrier(sK517))
| ~ element(X0,the_carrier(sK517))
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X0,X0)),the_InternalRel(sK517)) )
| ~ spl529_1 ),
inference(resolution,[],[f6415,f5317]) ).
fof(f6437,plain,
( ! [X0,X1] :
( ~ element(X1,sF528)
| ~ related(sK517,X0,X1)
| ~ element(X0,the_carrier(sK517))
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X0,X0)),the_InternalRel(sK517)) )
| ~ spl529_1
| ~ spl529_179 ),
inference(forward_demodulation,[],[f6433,f6238]) ).
fof(f6439,plain,
( ! [X0,X1] :
( ~ related(sK517,X0,X1)
| ~ element(X1,sF528)
| ~ element(X0,sF528)
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X0,X0)),the_InternalRel(sK517)) )
| ~ spl529_1
| ~ spl529_179 ),
inference(forward_demodulation,[],[f6437,f6238]) ).
fof(f6440,plain,
( in(unordered_pair(unordered_pair(sK522,sK521),unordered_pair(sK521,sK521)),the_InternalRel(sK517))
| ~ spl529_1
| ~ spl529_4
| ~ spl529_5
| ~ spl529_10
| ~ spl529_179 ),
inference(unit_resulting_resolution,[],[f6439,f5332,f5362,f5337]) ).
fof(f6448,plain,
( in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK522,sK521)),the_InternalRel(sK517))
| ~ spl529_1
| ~ spl529_4
| ~ spl529_5
| ~ spl529_10
| ~ spl529_179 ),
inference(forward_demodulation,[],[f6440,f2453]) ).
fof(f6452,plain,
( in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),the_InternalRel(sK517))
| ~ spl529_1
| ~ spl529_4
| ~ spl529_5
| ~ spl529_10
| ~ spl529_179 ),
inference(forward_demodulation,[],[f6448,f2453]) ).
fof(f6457,definition,
( spl529_191
<=> in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),the_InternalRel(sK517)) ),
introduced(definition,[new_symbols(definition,[spl529_191])],[avatar_definition]) ).
fof(f6459,plain,
( in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),the_InternalRel(sK517))
| ~ spl529_191 ),
inference(avatar_component_clause,[],[f6457]) ).
fof(f6460,plain,
( spl529_191
| ~ spl529_1
| ~ spl529_4
| ~ spl529_5
| ~ spl529_10
| ~ spl529_179 ),
inference(avatar_split_clause,[],[f6452,f6236,f5360,f5335,f5330,f5315,f6457]) ).
fof(f6588,plain,
( relation_of2_as_subset(the_InternalRel(sK517),sF528,sF528)
| ~ rel_str(sK517)
| ~ spl529_179 ),
inference(superposition,[],[f3006,f6238]) ).
fof(f6591,plain,
( relation_of2_as_subset(the_InternalRel(sK517),sF528,sF528)
| ~ spl529_1
| ~ spl529_179 ),
inference(forward_subsumption_resolution,[],[f6588,f5317]) ).
fof(f6600,definition,
( spl529_194
<=> relation_of2_as_subset(the_InternalRel(sK517),sF528,sF528) ),
introduced(definition,[new_symbols(definition,[spl529_194])],[avatar_definition]) ).
fof(f6602,plain,
( relation_of2_as_subset(the_InternalRel(sK517),sF528,sF528)
| ~ spl529_194 ),
inference(avatar_component_clause,[],[f6600]) ).
fof(f6603,plain,
( spl529_194
| ~ spl529_1
| ~ spl529_179 ),
inference(avatar_split_clause,[],[f6591,f6236,f5315,f6600]) ).
fof(f6987,plain,
( element(the_InternalRel(sK517),k1_pcomps_1(cartesian_product2(sF528,sF528)))
| ~ spl529_194 ),
inference(unit_resulting_resolution,[],[f4512,f6602]) ).
fof(f6997,definition,
( spl529_221
<=> element(the_InternalRel(sK517),k1_pcomps_1(cartesian_product2(sF528,sF528))) ),
introduced(definition,[new_symbols(definition,[spl529_221])],[avatar_definition]) ).
fof(f6999,plain,
( element(the_InternalRel(sK517),k1_pcomps_1(cartesian_product2(sF528,sF528)))
| ~ spl529_221 ),
inference(avatar_component_clause,[],[f6997]) ).
fof(f7000,plain,
( spl529_221
| ~ spl529_194 ),
inference(avatar_split_clause,[],[f6987,f6600,f6997]) ).
fof(f8524,plain,
( in(unordered_pair(unordered_pair(sK521,sK522),unordered_pair(sK521,sK521)),cartesian_product2(sF527,sF527))
| ~ spl529_8
| ~ spl529_9 ),
inference(unit_resulting_resolution,[],[f4885,f5352,f5357]) ).
fof(f8640,plain,
( in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),cartesian_product2(sF527,sF527))
| ~ spl529_8
| ~ spl529_9 ),
inference(forward_demodulation,[],[f8524,f2453]) ).
fof(f8745,definition,
( spl529_358
<=> in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),cartesian_product2(sF527,sF527)) ),
introduced(definition,[new_symbols(definition,[spl529_358])],[avatar_definition]) ).
fof(f8747,plain,
( in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),cartesian_product2(sF527,sF527))
| ~ spl529_358 ),
inference(avatar_component_clause,[],[f8745]) ).
fof(f8748,plain,
( spl529_358
| ~ spl529_8
| ~ spl529_9 ),
inference(avatar_split_clause,[],[f8640,f5355,f5350,f8745]) ).
fof(f39827,plain,
( relation(the_InternalRel(sK517))
| ~ spl529_221 ),
inference(unit_resulting_resolution,[],[f4324,f6999]) ).
fof(f39957,definition,
( spl529_2949
<=> relation(the_InternalRel(sK517)) ),
introduced(definition,[new_symbols(definition,[spl529_2949])],[avatar_definition]) ).
fof(f39959,plain,
( relation(the_InternalRel(sK517))
| ~ spl529_2949 ),
inference(avatar_component_clause,[],[f39957]) ).
fof(f39960,plain,
( spl529_2949
| ~ spl529_221 ),
inference(avatar_split_clause,[],[f39827,f6997,f39957]) ).
fof(f39990,plain,
( in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),relation_restriction(the_InternalRel(sK517),sF527))
| ~ spl529_191
| ~ spl529_358
| ~ spl529_2949 ),
inference(unit_resulting_resolution,[],[f3994,f6459,f8747,f39959]) ).
fof(f40036,definition,
( spl529_2957
<=> in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),relation_restriction(the_InternalRel(sK517),sF527)) ),
introduced(definition,[new_symbols(definition,[spl529_2957])],[avatar_definition]) ).
fof(f40039,plain,
( spl529_2957
| ~ spl529_191
| ~ spl529_358
| ~ spl529_2949 ),
inference(avatar_split_clause,[],[f39990,f39957,f8745,f6457,f40036]) ).
fof(f45361,plain,
( the_InternalRel(sK518) = relation_restriction(the_InternalRel(sK517),sF527)
| ~ relation(the_InternalRel(sK517))
| ~ spl529_182 ),
inference(superposition,[],[f6302,f3417]) ).
fof(f45362,plain,
( the_InternalRel(sK518) = relation_restriction(the_InternalRel(sK517),sF527)
| ~ spl529_182
| ~ spl529_2949 ),
inference(forward_subsumption_resolution,[],[f45361,f39959]) ).
fof(f45366,definition,
( spl529_3632
<=> the_InternalRel(sK518) = relation_restriction(the_InternalRel(sK517),sF527) ),
introduced(definition,[new_symbols(definition,[spl529_3632])],[avatar_definition]) ).
fof(f45369,plain,
( spl529_3632
| ~ spl529_182
| ~ spl529_2949 ),
inference(avatar_split_clause,[],[f45362,f39957,f6300,f45366]) ).
fof(f45373,plain,
( the_InternalRel(sK518) != relation_restriction(the_InternalRel(sK517),sF527)
| in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),the_InternalRel(sK518))
| ~ in(unordered_pair(unordered_pair(sK521,sK521),unordered_pair(sK521,sK522)),relation_restriction(the_InternalRel(sK517),sF527)) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s1,plain,
spl529_1,
inference(sat_conversion,[],[f5318]) ).
cnf(s2,plain,
spl529_2,
inference(sat_conversion,[],[f5323]) ).
cnf(s3,plain,
spl529_3,
inference(sat_conversion,[],[f5328]) ).
cnf(s4,plain,
spl529_4,
inference(sat_conversion,[],[f5333]) ).
cnf(s5,plain,
spl529_5,
inference(sat_conversion,[],[f5338]) ).
cnf(s6,plain,
spl529_6,
inference(sat_conversion,[],[f5343]) ).
cnf(s7,plain,
spl529_7,
inference(sat_conversion,[],[f5348]) ).
cnf(s8,plain,
spl529_8,
inference(sat_conversion,[],[f5353]) ).
cnf(s9,plain,
spl529_9,
inference(sat_conversion,[],[f5358]) ).
cnf(s10,plain,
spl529_10,
inference(sat_conversion,[],[f5363]) ).
cnf(s11,plain,
~ spl529_11,
inference(sat_conversion,[],[f5368]) ).
cnf(s177,plain,
spl529_178,
inference(sat_conversion,[],[f6234]) ).
cnf(s178,plain,
spl529_179,
inference(sat_conversion,[],[f6239]) ).
cnf(s187,plain,
( ~ spl529_1
| ~ spl529_2
| spl529_181 ),
inference(sat_conversion,[],[f6285]) ).
cnf(s188,plain,
( ~ spl529_1
| ~ spl529_2
| ~ spl529_3
| ~ spl529_178
| spl529_182 ),
inference(sat_conversion,[],[f6303]) ).
cnf(s201,plain,
( ~ spl529_6
| ~ spl529_7
| spl529_11
| ~ spl529_178
| ~ spl529_181
| ~ spl529_190 ),
inference(sat_conversion,[],[f6431]) ).
cnf(s202,plain,
( ~ spl529_1
| ~ spl529_4
| ~ spl529_5
| ~ spl529_10
| ~ spl529_179
| spl529_191 ),
inference(sat_conversion,[],[f6460]) ).
cnf(s206,plain,
( ~ spl529_1
| ~ spl529_179
| spl529_194 ),
inference(sat_conversion,[],[f6603]) ).
cnf(s249,plain,
( ~ spl529_194
| spl529_221 ),
inference(sat_conversion,[],[f7000]) ).
cnf(s418,plain,
( ~ spl529_8
| ~ spl529_9
| spl529_358 ),
inference(sat_conversion,[],[f8748]) ).
cnf(s3442,plain,
( ~ spl529_221
| spl529_2949 ),
inference(sat_conversion,[],[f39960]) ).
cnf(s3452,plain,
( ~ spl529_191
| ~ spl529_358
| ~ spl529_2949
| spl529_2957 ),
inference(sat_conversion,[],[f40039]) ).
cnf(s4163,plain,
( ~ spl529_182
| ~ spl529_2949
| spl529_3632 ),
inference(sat_conversion,[],[f45369]) ).
cnf(s4168,plain,
( spl529_190
| ~ spl529_2957
| ~ spl529_3632 ),
inference(sat_conversion,[],[f45373]) ).
cnf(s4188,plain,
spl529_358,
inference(rat,[],[s418,s9,s8]) ).
cnf(s4423,plain,
spl529_194,
inference(rat,[],[s206,s178,s1]) ).
cnf(s4424,plain,
spl529_191,
inference(rat,[],[s202,s4,s178,s10,s5,s1]) ).
cnf(s4428,plain,
spl529_182,
inference(rat,[],[s188,s2,s177,s3,s1]) ).
cnf(s4429,plain,
spl529_181,
inference(rat,[],[s187,s2,s1]) ).
cnf(s4431,plain,
spl529_221,
inference(rat,[],[s249,s4423]) ).
cnf(s4480,plain,
~ spl529_190,
inference(rat,[],[s201,s6,s7,s177,s11,s4429]) ).
cnf(s4486,plain,
spl529_2949,
inference(rat,[],[s3442,s4431]) ).
cnf(s4670,plain,
spl529_3632,
inference(rat,[],[s4163,s4428,s4486]) ).
cnf(s4671,plain,
spl529_2957,
inference(rat,[],[s3452,s4424,s4188,s4486]) ).
cnf(s5288,plain,
$false,
inference(rat,[],[s4168,s4480,s4670,s4671]) ).
fof(f45374,plain,
$false,
inference(avatar_sat_refutation,[],[s5288]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU363+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.03/0.32 % Computer : n012.cluster.edu
% 0.03/0.32 % Model : x86_64 x86_64
% 0.03/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.32 % Memory : 8046.5625MB
% 0.03/0.32 % OS : Linux 6.8.0-71-generic
% 0.03/0.33 % CPULimit : 300
% 0.03/0.33 % WCLimit : 300
% 0.03/0.33 % DateTime : Mon Sep 28 04:54:35 UTC 2026
% 0.03/0.33 % CPUTime :
% 0.03/0.33 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.03/0.34 Running first-order theorem proving
% 0.03/0.34 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
% 8.31/1.90 % (3025942)Detected formulas, will run a generic FOF schedule.
% 8.31/1.90 % (3025952)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1903010147:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.31/1.90 % (3025949)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=185765839:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.31/1.90 % (3025948)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=3501045185:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.31/1.90 % (3025947)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=183118570:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.31/1.90 % (3025951)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2599512070:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.31/1.90 % (3025953)dis-21_1_sil=8000:lcm=predicate:random_seed=2516412608: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)
% 8.31/1.90 % (3025950)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2445066227:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.31/1.90 % (3025950)Instruction limit reached!
% 8.31/1.90 % (3025950)------------------------------
% 8.31/1.90 % (3025950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/1.90 % (3025950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/1.90 % (3025950)CaDiCaL version: 2.1.3
% 8.31/1.90 % (3025950)Termination reason: Instruction limit
% 8.31/1.90 % (3025950)Termination phase: Saturation
% 8.31/1.90 % (3025950)Time elapsed: 0.032 s
% 8.31/1.90 % (3025950)Peak memory usage: 91 MB
% 8.31/1.90 % (3025950)Instructions burned: 110 (million)
% 8.31/1.90 % (3025953)Instruction limit reached!
% 8.31/1.90 % (3025953)------------------------------
% 8.31/1.90 % (3025953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/1.90 % (3025953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/1.90 % (3025953)CaDiCaL version: 2.1.3
% 8.31/1.90 % (3025953)Termination reason: Instruction limit
% 8.31/1.90 % (3025953)Termination phase: Saturation
% 8.31/1.90 % (3025953)Time elapsed: 0.036 s
% 8.31/1.90 % (3025953)Peak memory usage: 91 MB
% 8.31/1.90 % (3025953)Instructions burned: 132 (million)
% 8.31/1.90 % (3025951)Instruction limit reached!
% 8.31/1.90 % (3025951)------------------------------
% 8.31/1.90 % (3025951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/1.90 % (3025951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/1.90 % (3025951)CaDiCaL version: 2.1.3
% 8.31/1.90 % (3025951)Termination reason: Instruction limit
% 8.31/1.90 % (3025951)Termination phase: Saturation
% 8.31/1.90 % (3025951)Time elapsed: 0.041 s
% 8.31/1.90 % (3025951)Peak memory usage: 91 MB
% 8.31/1.90 % (3025951)Instructions burned: 121 (million)
% 8.31/1.90 % (3025952)Instruction limit reached!
% 8.31/1.90 % (3025952)------------------------------
% 8.31/1.90 % (3025952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/1.90 % (3025952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/1.90 % (3025952)CaDiCaL version: 2.1.3
% 8.31/1.90 % (3025952)Termination reason: Instruction limit
% 8.31/1.90 % (3025952)Termination phase: Saturation
% 8.31/1.90 % (3025952)Time elapsed: 0.047 s
% 8.31/1.90 % (3025952)Peak memory usage: 92 MB
% 8.31/1.90 % (3025952)Instructions burned: 141 (million)
% 8.31/1.90 % (3025961)lrs+10_1_sil=8000:sp=occurrence:random_seed=1374363216:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 8.31/1.90 % (3025962)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4019362461:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 8.31/1.90 % (3025963)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3002886896:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi)
% 8.31/1.90 % (3025964)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=2235838405:s2a=on:i=248:s2at=1.23:gtg=position_2998 on theBenchmark for (2998ds/248Mi)
% 8.31/1.90 % (3025962)Instruction limit reached!
% 12.79/2.49 % (3025962)------------------------------
% 12.79/2.49 % (3025962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.49 % (3025962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.49 % (3025962)CaDiCaL version: 2.1.3
% 12.79/2.49 % (3025962)Termination reason: Instruction limit
% 12.79/2.49 % (3025962)Termination phase: Saturation
% 12.79/2.49 % (3025962)Time elapsed: 0.046 s
% 12.79/2.49 % (3025962)Peak memory usage: 90 MB
% 12.79/2.49 % (3025962)Instructions burned: 158 (million)
% 12.79/2.49 % (3025964)Instruction limit reached!
% 12.79/2.49 % (3025964)------------------------------
% 12.79/2.49 % (3025964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.49 % (3025964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.49 % (3025964)CaDiCaL version: 2.1.3
% 12.79/2.49 % (3025964)Termination reason: Instruction limit
% 12.79/2.49 % (3025964)Termination phase: Saturation
% 12.79/2.49 % (3025964)Time elapsed: 0.082 s
% 12.79/2.49 % (3025964)Peak memory usage: 94 MB
% 12.79/2.49 % (3025964)Instructions burned: 248 (million)
% 12.79/2.49 % (3025961)Instruction limit reached!
% 12.79/2.50 % (3025961)------------------------------
% 12.79/2.50 % (3025961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.50 % (3025961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.50 % (3025961)CaDiCaL version: 2.1.3
% 12.79/2.50 % (3025961)Termination reason: Instruction limit
% 12.79/2.50 % (3025961)Termination phase: Saturation
% 12.79/2.50 % (3025961)Time elapsed: 0.100 s
% 12.79/2.50 % (3025961)Peak memory usage: 95 MB
% 12.79/2.50 % (3025961)Instructions burned: 287 (million)
% 12.79/2.50 % (3025963)Instruction limit reached!
% 12.79/2.50 % (3025963)------------------------------
% 12.79/2.50 % (3025963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.50 % (3025963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.50 % (3025963)CaDiCaL version: 2.1.3
% 12.79/2.50 % (3025963)Termination reason: Instruction limit
% 12.79/2.50 % (3025963)Termination phase: Saturation
% 12.79/2.50 % (3025963)Time elapsed: 0.119 s
% 12.79/2.50 % (3025963)Peak memory usage: 95 MB
% 12.79/2.50 % (3025963)Instructions burned: 325 (million)
% 12.79/2.50 % (3025969)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2960529216:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 12.79/2.50 % (3025970)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=263395768:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 12.79/2.50 % (3025971)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2504062619:cts=off:i=113:fsr=off:ss=included:sgt=4_2996 on theBenchmark for (2996ds/113Mi)
% 12.79/2.50 % (3025971)Instruction limit reached!
% 12.79/2.50 % (3025971)------------------------------
% 12.79/2.50 % (3025971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.50 % (3025971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.50 % (3025971)CaDiCaL version: 2.1.3
% 12.79/2.50 % (3025971)Termination reason: Instruction limit
% 12.79/2.50 % (3025971)Termination phase: Saturation
% 12.79/2.50 % (3025971)Time elapsed: 0.038 s
% 12.79/2.50 % (3025971)Peak memory usage: 91 MB
% 12.79/2.50 % (3025971)Instructions burned: 115 (million)
% 12.79/2.50 % (3025972)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2301594891:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 12.79/2.50 % (3025969)Instruction limit reached!
% 12.79/2.50 % (3025969)------------------------------
% 12.79/2.50 % (3025969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.50 % (3025969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.50 % (3025969)CaDiCaL version: 2.1.3
% 12.79/2.50 % (3025969)Termination reason: Instruction limit
% 12.79/2.50 % (3025969)Termination phase: Saturation
% 12.79/2.50 % (3025969)Time elapsed: 0.106 s
% 12.79/2.50 % (3025969)Peak memory usage: 93 MB
% 12.79/2.50 % (3025969)Instructions burned: 295 (million)
% 12.79/2.50 % (3025972)Instruction limit reached!
% 12.79/2.50 % (3025972)------------------------------
% 12.79/2.50 % (3025972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.50 % (3025972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.50 % (3025972)CaDiCaL version: 2.1.3
% 12.79/2.50 % (3025972)Termination reason: Instruction limit
% 12.79/2.50 % (3025972)Termination phase: Saturation
% 31.49/5.04 % (3025972)Time elapsed: 0.038 s
% 31.49/5.04 % (3025972)Peak memory usage: 91 MB
% 31.49/5.04 % (3025972)Instructions burned: 129 (million)
% 31.49/5.04 % (3025976)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=765092023:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 31.49/5.04 % (3025978)lrs+10_1_sil=8000:sp=occurrence:random_seed=682850437:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 31.49/5.04 % (3025976)Instruction limit reached!
% 31.49/5.04 % (3025976)------------------------------
% 31.49/5.04 % (3025976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.04 % (3025976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.49/5.04 % (3025976)CaDiCaL version: 2.1.3
% 31.49/5.04 % (3025976)Termination reason: Instruction limit
% 31.49/5.04 % (3025976)Termination phase: Saturation
% 31.49/5.04 % (3025976)Time elapsed: 0.039 s
% 31.49/5.04 % (3025976)Peak memory usage: 90 MB
% 31.49/5.04 % (3025976)Instructions burned: 117 (million)
% 31.49/5.04 % (3025979)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3101916967:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi)
% 31.49/5.04 % (3025982)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1641277094:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 31.49/5.04 % (3025979)Instruction limit reached!
% 31.49/5.04 % (3025979)------------------------------
% 31.49/5.04 % (3025979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.04 % (3025979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.49/5.04 % (3025979)CaDiCaL version: 2.1.3
% 31.49/5.04 % (3025979)Termination reason: Instruction limit
% 31.49/5.04 % (3025979)Termination phase: Saturation
% 31.49/5.04 % (3025979)Time elapsed: 0.149 s
% 31.49/5.04 % (3025979)Peak memory usage: 96 MB
% 31.49/5.04 % (3025979)Instructions burned: 440 (million)
% 31.49/5.04 % (3025985)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1822115901:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi)
% 31.49/5.04 % (3025978)Instruction limit reached!
% 31.49/5.04 % (3025978)------------------------------
% 31.49/5.04 % (3025978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.04 % (3025978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.49/5.04 % (3025978)CaDiCaL version: 2.1.3
% 31.49/5.04 % (3025978)Termination reason: Instruction limit
% 31.49/5.04 % (3025978)Termination phase: Saturation
% 31.49/5.04 % (3025978)Time elapsed: 0.322 s
% 31.49/5.04 % (3025978)Peak memory usage: 105 MB
% 31.49/5.04 % (3025978)Instructions burned: 908 (million)
% 31.49/5.04 % (3025985)Instruction limit reached!
% 31.49/5.04 % (3025985)------------------------------
% 31.49/5.04 % (3025985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.04 % (3025985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.49/5.04 % (3025985)CaDiCaL version: 2.1.3
% 31.49/5.04 % (3025985)Termination reason: Instruction limit
% 31.49/5.04 % (3025985)Termination phase: Saturation
% 31.49/5.04 % (3025985)Time elapsed: 0.038 s
% 31.49/5.04 % (3025985)Peak memory usage: 92 MB
% 31.49/5.04 % (3025985)Instructions burned: 136 (million)
% 31.49/5.04 % (3025987)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=5041638:st=8:i=592:sd=3:ep=RST:ss=axioms_2989 on theBenchmark for (2989ds/592Mi)
% 31.49/5.04 % (3025988)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=901801005:st=3:i=13193:sd=3:ss=axioms_2989 on theBenchmark for (2989ds/13193Mi)
% 31.49/5.04 % (3025970)Instruction limit reached!
% 31.49/5.04 % (3025970)------------------------------
% 31.49/5.04 % (3025970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.04 % (3025970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.49/5.04 % (3025970)CaDiCaL version: 2.1.3
% 31.49/5.04 % (3025970)Termination reason: Instruction limit
% 31.49/5.04 % (3025970)Termination phase: Saturation
% 31.49/5.04 % (3025970)Time elapsed: 0.810 s
% 31.49/5.04 % (3025970)Peak memory usage: 157 MB
% 31.49/5.04 % (3025970)Instructions burned: 2352 (million)
% 31.49/5.04 % (3025987)Instruction limit reached!
% 31.49/5.04 % (3025987)------------------------------
% 31.49/5.04 % (3025987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.04 % (3025987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3025987)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3025987)Termination reason: Instruction limit
% 41.56/6.59 % (3025987)Termination phase: Saturation
% 41.56/6.59 % (3025987)Time elapsed: 0.196 s
% 41.56/6.59 % (3025987)Peak memory usage: 100 MB
% 41.56/6.59 % (3025987)Instructions burned: 593 (million)
% 41.56/6.59 % (3025991)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=898823180:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi)
% 41.56/6.59 % (3025992)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2665817190:i=134:gtgl=5:slsql=off:gtg=exists_sym_2986 on theBenchmark for (2986ds/134Mi)
% 41.56/6.59 % (3025991)Instruction limit reached!
% 41.56/6.59 % (3025991)------------------------------
% 41.56/6.59 % (3025991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3025991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3025991)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3025991)Termination reason: Instruction limit
% 41.56/6.59 % (3025991)Termination phase: Saturation
% 41.56/6.59 % (3025991)Time elapsed: 0.040 s
% 41.56/6.59 % (3025991)Peak memory usage: 93 MB
% 41.56/6.59 % (3025991)Instructions burned: 128 (million)
% 41.56/6.59 % (3025992)Instruction limit reached!
% 41.56/6.59 % (3025992)------------------------------
% 41.56/6.59 % (3025992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3025992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3025992)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3025992)Termination reason: Instruction limit
% 41.56/6.59 % (3025992)Termination phase: Saturation
% 41.56/6.59 % (3025992)Time elapsed: 0.040 s
% 41.56/6.59 % (3025992)Peak memory usage: 92 MB
% 41.56/6.59 % (3025992)Instructions burned: 136 (million)
% 41.56/6.59 % (3025995)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3537782389:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/141Mi)
% 41.56/6.59 % (3025996)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=686640320:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2984 on theBenchmark for (2984ds/431Mi)
% 41.56/6.59 % (3025995)Instruction limit reached!
% 41.56/6.59 % (3025995)------------------------------
% 41.56/6.59 % (3025995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3025995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3025995)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3025995)Termination reason: Instruction limit
% 41.56/6.59 % (3025995)Termination phase: Saturation
% 41.56/6.59 % (3025995)Time elapsed: 0.041 s
% 41.56/6.59 % (3025995)Peak memory usage: 92 MB
% 41.56/6.59 % (3025995)Instructions burned: 143 (million)
% 41.56/6.59 % (3025996)Instruction limit reached!
% 41.56/6.59 % (3025996)------------------------------
% 41.56/6.59 % (3025996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3025996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3025996)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3025996)Termination reason: Instruction limit
% 41.56/6.59 % (3025996)Termination phase: Saturation
% 41.56/6.59 % (3025996)Time elapsed: 0.142 s
% 41.56/6.59 % (3025996)Peak memory usage: 96 MB
% 41.56/6.59 % (3025996)Instructions burned: 433 (million)
% 41.56/6.59 % (3025999)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=736907955:i=6060:aac=none:ins=25_2983 on theBenchmark for (2983ds/6060Mi)
% 41.56/6.59 % (3026000)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=920007454:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2982 on theBenchmark for (2982ds/150Mi)
% 41.56/6.59 % (3026000)Instruction limit reached!
% 41.56/6.59 % (3026000)------------------------------
% 41.56/6.59 % (3026000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3026000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3026000)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3026000)Termination reason: Instruction limit
% 41.56/6.59 % (3026000)Termination phase: Saturation
% 41.56/6.59 % (3026000)Time elapsed: 0.046 s
% 41.56/6.59 % (3026000)Peak memory usage: 93 MB
% 41.56/6.59 % (3026000)Instructions burned: 152 (million)
% 41.56/6.59 % (3025982)Instruction limit reached!
% 41.56/6.59 % (3025982)------------------------------
% 41.56/6.59 % (3025982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3025982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3025982)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3025982)Termination reason: Instruction limit
% 41.56/6.59 % (3025982)Termination phase: Saturation
% 41.56/6.59 % (3025982)Time elapsed: 1.190 s
% 41.56/6.59 % (3025982)Peak memory usage: 151 MB
% 41.56/6.59 % (3025982)Instructions burned: 5205 (million)
% 41.56/6.59 % (3026003)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=377951748:i=14155:bd=all_2980 on theBenchmark for (2980ds/14155Mi)
% 41.56/6.59 % (3026004)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=718786279:i=667:av=off:fsr=off_2979 on theBenchmark for (2979ds/667Mi)
% 41.56/6.59 % (3026004)Instruction limit reached!
% 41.56/6.59 % (3026004)------------------------------
% 41.56/6.59 % (3026004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3026004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3026004)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3026004)Termination reason: Instruction limit
% 41.56/6.59 % (3026004)Termination phase: Saturation
% 41.56/6.59 % (3026004)Time elapsed: 0.174 s
% 41.56/6.59 % (3026004)Peak memory usage: 94 MB
% 41.56/6.59 % (3026004)Instructions burned: 668 (million)
% 41.56/6.59 % (3026007)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3419992740:s2a=on:i=185:s2at=1.8:fdi=4_2976 on theBenchmark for (2976ds/185Mi)
% 41.56/6.59 % (3026007)Instruction limit reached!
% 41.56/6.59 % (3026007)------------------------------
% 41.56/6.59 % (3026007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3026007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3026007)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3026007)Termination reason: Instruction limit
% 41.56/6.59 % (3026007)Termination phase: Saturation
% 41.56/6.59 % (3026007)Time elapsed: 0.054 s
% 41.56/6.59 % (3026007)Peak memory usage: 93 MB
% 41.56/6.59 % (3026007)Instructions burned: 187 (million)
% 41.56/6.59 % (3026009)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2072251475:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2974 on theBenchmark for (2974ds/193Mi)
% 41.56/6.59 % (3026009)Instruction limit reached!
% 41.56/6.59 % (3026009)------------------------------
% 41.56/6.59 % (3026009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3026009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3026009)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3026009)Termination reason: Instruction limit
% 41.56/6.59 % (3026009)Termination phase: Saturation
% 41.56/6.59 % (3026009)Time elapsed: 0.062 s
% 41.56/6.59 % (3026009)Peak memory usage: 95 MB
% 41.56/6.59 % (3026009)Instructions burned: 194 (million)
% 41.56/6.59 % (3026011)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1752873405:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2972 on theBenchmark for (2972ds/4850Mi)
% 41.56/6.59 % (3025999)Instruction limit reached!
% 41.56/6.59 % (3025999)------------------------------
% 41.56/6.59 % (3025999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3025999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3025999)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3025999)Termination reason: Instruction limit
% 41.56/6.59 % (3025999)Termination phase: Saturation
% 41.56/6.59 % (3025999)Time elapsed: 2.077 s
% 41.56/6.59 % (3025999)Peak memory usage: 179 MB
% 41.56/6.59 % (3025999)Instructions burned: 6063 (million)
% 41.56/6.59 % (3026013)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=384784024:i=12111:sd=1:ss=included_2961 on theBenchmark for (2961ds/12111Mi)
% 41.56/6.59 % (3026011)Instruction limit reached!
% 41.56/6.59 % (3026011)------------------------------
% 41.56/6.59 % (3026011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3026011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3026011)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3026011)Termination reason: Instruction limit
% 41.56/6.59 % (3026011)Termination phase: Saturation
% 41.56/6.59 % (3026011)Time elapsed: 1.603 s
% 41.56/6.59 % (3026011)Peak memory usage: 145 MB
% 41.56/6.59 % (3026011)Instructions burned: 4851 (million)
% 41.56/6.59 % (3026015)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3926134991:i=319:kws=precedence:fsr=off_2955 on theBenchmark for (2955ds/319Mi)
% 41.56/6.59 % (3026015)Instruction limit reached!
% 41.56/6.59 % (3026015)------------------------------
% 41.56/6.59 % (3026015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3026015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3026015)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3026015)Termination reason: Instruction limit
% 41.56/6.59 % (3026015)Termination phase: Saturation
% 41.56/6.59 % (3026015)Time elapsed: 0.095 s
% 41.56/6.59 % (3026015)Peak memory usage: 96 MB
% 41.56/6.59 % (3026015)Instructions burned: 320 (million)
% 41.56/6.59 % (3026017)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1055059244:i=2064:ep=RST_2952 on theBenchmark for (2952ds/2064Mi)
% 41.56/6.59 % (3025988)Instruction limit reached!
% 41.56/6.59 % (3025988)------------------------------
% 41.56/6.59 % (3025988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3025988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3025988)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3025988)Termination reason: Instruction limit
% 41.56/6.59 % (3025988)Termination phase: Saturation
% 41.56/6.59 % (3025988)Time elapsed: 4.231 s
% 41.56/6.59 % (3025988)Peak memory usage: 234 MB
% 41.56/6.59 % (3025988)Instructions burned: 13193 (million)
% 41.56/6.59 % (3026017)Instruction limit reached!
% 41.56/6.59 % (3026017)------------------------------
% 41.56/6.59 % (3026017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3026017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3026017)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3026017)Termination reason: Instruction limit
% 41.56/6.59 % (3026017)Termination phase: Saturation
% 41.56/6.59 % (3026017)Time elapsed: 0.670 s
% 41.56/6.59 % (3026017)Peak memory usage: 126 MB
% 41.56/6.59 % (3026017)Instructions burned: 2065 (million)
% 41.56/6.59 % (3026019)dis-1011_128_sil=32000:random_seed=365430225:i=3706:ep=RST:av=off_2945 on theBenchmark for (2945ds/3706Mi)
% 41.56/6.59 % (3026021)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1165645285:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2944 on theBenchmark for (2944ds/757Mi)
% 41.56/6.59 % (3026013)First to succeed.
% 41.56/6.59 % (3026013)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3025942"
% 41.56/6.59 % (3026021)Instruction limit reached!
% 41.56/6.59 % (3026021)------------------------------
% 41.56/6.59 % (3026021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.56/6.59 % (3026021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.56/6.59 % (3026021)CaDiCaL version: 2.1.3
% 41.56/6.59 % (3026021)Termination reason: Instruction limit
% 41.56/6.59 % (3026021)Termination phase: Saturation
% 41.56/6.59 % (3026021)Time elapsed: 0.284 s
% 41.56/6.59 % (3026021)Peak memory usage: 109 MB
% 41.56/6.59 % (3026021)Instructions burned: 759 (million)
% 41.56/6.59 % (3026013)Refutation found. Thanks to Tanya!
% 41.56/6.59 % SZS status Theorem for theBenchmark
% 41.56/6.59 % SZS output start Proof for theBenchmark
% See solution above
% 42.60/6.68 % (3026013)------------------------------
% 42.60/6.68 % (3026013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.60/6.68 % (3026013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.60/6.68 % (3026013)CaDiCaL version: 2.1.3
% 42.60/6.68 % (3026013)Termination reason: Refutation
% 42.60/6.68 % (3026013)Time elapsed: 1.847 s
% 42.60/6.68 % (3026013)Peak memory usage: 183 MB
% 42.60/6.68 % (3026013)Instructions burned: 5594 (million)
% 42.60/6.68 % (3026013)------------------------------
% 42.60/6.68 % (3026013)------------------------------
% 42.60/6.68 % (3025942)Success in time 6.04 s
% 42.60/6.68 % Vampire exiting
%------------------------------------------------------------------------------