%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET271-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:40:39 PM UTC 2026
% Result : Unsatisfiable 143.39s 21.35s
% Output : Refutation 145.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 37
% Syntax : Number of formulae : 131 ( 23 unt; 14 def)
% Number of atoms : 276 ( 40 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 266 ( 121 ~; 131 |; 0 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 18 ( 16 usr; 15 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-3 aty)
% Number of variables : 117 ( 0 sgn 117 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f6,axiom,
! [X0,X1] :
( X0 != X1
| subclass(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equal_implies_subclass2) ).
fof(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_implies_equal) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f10,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair3) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( ~ member(X0,X1)
| ~ member(X2,X3)
| member(ordered_pair(X0,X2),cross_product(X1,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product3) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection3) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',restriction1) ).
fof(f30,axiom,
! [X0,X1] :
( restrict(X0,singleton(X1),universal_class) != null_class
| ~ member(X1,domain_of(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain1) ).
fof(f31,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| restrict(X1,singleton(X0),universal_class) = null_class
| member(X0,domain_of(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain2) ).
fof(f32,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| null_class = restrict(X1,singleton(X0),universal_class)
| member(X0,domain_of(X1)) ),
inference(reorient_equations,[],[f31]) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f122,negated_conjecture,
domain_of(cross_product(x,x)) != x,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_to_domain_property2_1) ).
fof(f123,plain,
x != domain_of(cross_product(x,x)),
inference(reorient_equations,[],[f122]) ).
fof(f128,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),
inference(definition_unfolding,[],[f13,f12,f12]) ).
fof(f137,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X0,X2) ),
inference(definition_unfolding,[],[f14,f128]) ).
fof(f139,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(definition_unfolding,[],[f16,f128]) ).
fof(f140,plain,
! [X2,X0,X1] :
( unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0
| ~ member(X0,cross_product(X1,X2)) ),
inference(definition_unfolding,[],[f17,f128]) ).
fof(f144,plain,
! [X0,X1] :
( null_class != intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,domain_of(X0)) ),
inference(definition_unfolding,[],[f30,f28,f12]) ).
fof(f145,plain,
! [X0,X1] :
( null_class = intersection(X1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,universal_class)
| member(X0,domain_of(X1)) ),
inference(definition_unfolding,[],[f32,f28,f12]) ).
fof(f187,plain,
! [X1] : subclass(X1,X1),
inference(equality_resolution,[],[f6]) ).
fof(f191,definition,
( spl0_1
<=> x = domain_of(cross_product(x,x)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f193,plain,
( x != domain_of(cross_product(x,x))
| spl0_1 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f194,plain,
~ spl0_1,
inference(avatar_split_clause,[],[f123,f191]) ).
fof(f198,plain,
( ~ subclass(x,domain_of(cross_product(x,x)))
| ~ subclass(domain_of(cross_product(x,x)),x)
| spl0_1 ),
inference(extensionality_resolution,[],[f7,f193]) ).
fof(f200,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,X1),X2)
| ~ subclass(X2,X1)
| subclass(X0,X1) ),
inference(resolution,[],[f1,f3]) ).
fof(f207,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,cross_product(X3,X4))
| member(first(X0),X1)
| ~ member(X0,cross_product(X1,X2)) ),
inference(superposition,[],[f137,f140]) ).
fof(f225,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| member(first(X0),X1) ),
inference(factoring,[],[f207]) ).
fof(f226,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f21,f2]) ).
fof(f228,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f226,f3]) ).
fof(f233,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f228]) ).
fof(f286,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(unordered_pair(X2,X2),universal_class))
| member(X0,null_class)
| ~ member(X0,X1)
| ~ member(X2,universal_class)
| member(X2,domain_of(X1)) ),
inference(superposition,[],[f23,f145]) ).
fof(f315,definition,
( spl0_3
<=> subclass(domain_of(cross_product(x,x)),x) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f317,plain,
( ~ subclass(domain_of(cross_product(x,x)),x)
| spl0_3 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f319,definition,
( spl0_4
<=> subclass(x,domain_of(cross_product(x,x))) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f321,plain,
( ~ subclass(x,domain_of(cross_product(x,x)))
| spl0_4 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f322,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_1 ),
inference(avatar_split_clause,[],[f198,f191,f319,f315]) ).
fof(f327,plain,
( member(not_subclass_element(domain_of(cross_product(x,x)),x),domain_of(cross_product(x,x)))
| spl0_3 ),
inference(unit_resulting_resolution,[],[f2,f317]) ).
fof(f329,definition,
( spl0_5
<=> member(not_subclass_element(domain_of(cross_product(x,x)),x),domain_of(cross_product(x,x))) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f331,plain,
( member(not_subclass_element(domain_of(cross_product(x,x)),x),domain_of(cross_product(x,x)))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f332,plain,
( spl0_5
| spl0_3 ),
inference(avatar_split_clause,[],[f327,f315,f329]) ).
fof(f336,plain,
( ~ member(not_subclass_element(x,domain_of(cross_product(x,x))),domain_of(cross_product(x,x)))
| spl0_4 ),
inference(unit_resulting_resolution,[],[f200,f187,f321]) ).
fof(f340,plain,
( member(not_subclass_element(x,domain_of(cross_product(x,x))),x)
| spl0_4 ),
inference(unit_resulting_resolution,[],[f2,f321]) ).
fof(f342,definition,
( spl0_6
<=> member(not_subclass_element(x,domain_of(cross_product(x,x))),x) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f344,plain,
( member(not_subclass_element(x,domain_of(cross_product(x,x))),x)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f345,plain,
( spl0_6
| spl0_4 ),
inference(avatar_split_clause,[],[f340,f319,f342]) ).
fof(f351,plain,
( member(not_subclass_element(x,domain_of(cross_product(x,x))),universal_class)
| ~ spl0_6 ),
inference(unit_resulting_resolution,[],[f1,f4,f344]) ).
fof(f355,definition,
( spl0_7
<=> member(not_subclass_element(x,domain_of(cross_product(x,x))),universal_class) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f357,plain,
( member(not_subclass_element(x,domain_of(cross_product(x,x))),universal_class)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f358,plain,
( spl0_7
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f351,f342,f355]) ).
fof(f446,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X2)
| ~ member(X3,universal_class)
| member(X3,domain_of(X2))
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(X3,X3)) ),
inference(resolution,[],[f286,f139]) ).
fof(f455,plain,
( ! [X0] : member(not_subclass_element(x,domain_of(cross_product(x,x))),unordered_pair(X0,not_subclass_element(x,domain_of(cross_product(x,x)))))
| ~ spl0_7 ),
inference(unit_resulting_resolution,[],[f10,f357]) ).
fof(f509,plain,
! [X0] :
( subclass(null_class,X0)
| null_class = X0 ),
inference(superposition,[],[f233,f70]) ).
fof(f511,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class)
| null_class = X0 ),
inference(resolution,[],[f509,f7]) ).
fof(f512,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f511]) ).
fof(f518,plain,
! [X0] : null_class = intersection(null_class,X0),
inference(resolution,[],[f512,f233]) ).
fof(f530,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(null_class)) ),
inference(superposition,[],[f144,f518]) ).
fof(f531,plain,
! [X0] : ~ member(X0,domain_of(null_class)),
inference(trivial_inequality_removal,[],[f530]) ).
fof(f534,plain,
! [X0,X1] : ~ member(X0,intersection(domain_of(null_class),X1)),
inference(unit_resulting_resolution,[],[f21,f531]) ).
fof(f555,plain,
null_class = domain_of(null_class),
inference(resolution,[],[f531,f68]) ).
fof(f561,plain,
! [X0,X1] : ~ member(X0,intersection(null_class,X1)),
inference(forward_demodulation,[],[f534,f555]) ).
fof(f578,plain,
! [X0] : ~ member(X0,null_class),
inference(forward_demodulation,[],[f561,f518]) ).
fof(f592,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X2)
| ~ member(X3,universal_class)
| member(X3,domain_of(X2))
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(X3,X3)) ),
inference(backward_subsumption_resolution,[],[f446,f578]) ).
fof(f596,plain,
! [X2,X3,X0,X1,X4] :
( member(X0,domain_of(cross_product(X1,X2)))
| ~ member(X0,universal_class)
| ~ member(X3,universal_class)
| ~ member(X4,unordered_pair(X0,X0))
| ~ member(X3,X2)
| ~ member(X4,X1) ),
inference(resolution,[],[f592,f139]) ).
fof(f609,plain,
( member(not_subclass_element(x,domain_of(cross_product(x,x))),domain_of(cross_product(x,x)))
| ~ spl0_6
| ~ spl0_7 ),
inference(unit_resulting_resolution,[],[f596,f344,f357,f344,f357,f455]) ).
fof(f623,plain,
( $false
| spl0_4
| ~ spl0_6
| ~ spl0_7 ),
inference(backward_subsumption_resolution,[],[f336,f609]) ).
fof(f624,plain,
( spl0_4
| ~ spl0_6
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f623]) ).
fof(f630,plain,
( null_class != intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f144,f331]) ).
fof(f685,plain,
( ~ member(not_subclass_element(domain_of(cross_product(x,x)),x),x)
| spl0_3 ),
inference(unit_resulting_resolution,[],[f200,f187,f317]) ).
fof(f693,definition,
( spl0_12
<=> null_class = intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f695,plain,
( null_class != intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))
| spl0_12 ),
inference(avatar_component_clause,[],[f693]) ).
fof(f696,plain,
( ~ spl0_12
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f630,f329,f693]) ).
fof(f703,plain,
( member(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))),intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class)))
| spl0_12 ),
inference(unit_resulting_resolution,[],[f68,f695]) ).
fof(f1043,definition,
( spl0_19
<=> member(not_subclass_element(domain_of(cross_product(x,x)),x),x) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f1046,plain,
( ~ spl0_19
| spl0_3 ),
inference(avatar_split_clause,[],[f685,f315,f1043]) ).
fof(f1158,definition,
( spl0_21
<=> member(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))),intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f1160,plain,
( member(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))),intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class)))
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f1158]) ).
fof(f1161,plain,
( spl0_21
| spl0_12 ),
inference(avatar_split_clause,[],[f703,f693,f1158]) ).
fof(f1193,plain,
( member(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))),cross_product(x,x))
| ~ spl0_21 ),
inference(resolution,[],[f1160,f21]) ).
fof(f1194,plain,
( member(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))
| ~ spl0_21 ),
inference(resolution,[],[f1160,f22]) ).
fof(f1198,definition,
( spl0_22
<=> member(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))),cross_product(x,x)) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f1200,plain,
( member(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))),cross_product(x,x))
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f1198]) ).
fof(f1201,plain,
( spl0_22
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f1193,f1158,f1198]) ).
fof(f1246,plain,
( member(first(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class)))),x)
| ~ spl0_22 ),
inference(resolution,[],[f1200,f225]) ).
fof(f1255,definition,
( spl0_23
<=> member(first(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class)))),x) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f1258,plain,
( spl0_23
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1246,f1198,f1255]) ).
fof(f2906,definition,
( spl0_42
<=> member(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f2908,plain,
( member(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f2906]) ).
fof(f2909,plain,
( spl0_42
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f1194,f1158,f2906]) ).
fof(f3001,plain,
( member(first(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class)))),unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)))
| ~ spl0_42 ),
inference(resolution,[],[f2908,f225]) ).
fof(f3052,definition,
( spl0_45
<=> member(first(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class)))),unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x))) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f3054,plain,
( member(first(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class)))),unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)))
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f3052]) ).
fof(f3055,plain,
( spl0_45
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f3001,f2906,f3052]) ).
fof(f3195,plain,
( not_subclass_element(domain_of(cross_product(x,x)),x) = first(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))))
| not_subclass_element(domain_of(cross_product(x,x)),x) = first(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))))
| ~ spl0_45 ),
inference(resolution,[],[f3054,f8]) ).
fof(f3197,plain,
( not_subclass_element(domain_of(cross_product(x,x)),x) = first(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))))
| ~ spl0_45 ),
inference(duplicate_literal_removal,[],[f3195]) ).
fof(f3264,definition,
( spl0_46
<=> not_subclass_element(domain_of(cross_product(x,x)),x) = first(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f3267,plain,
( spl0_46
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f3197,f3052,f3264]) ).
fof(f3268,plain,
( not_subclass_element(domain_of(cross_product(x,x)),x) != first(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class))))
| member(not_subclass_element(domain_of(cross_product(x,x)),x),x)
| ~ member(first(regular(intersection(cross_product(x,x),cross_product(unordered_pair(not_subclass_element(domain_of(cross_product(x,x)),x),not_subclass_element(domain_of(cross_product(x,x)),x)),universal_class)))),x) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s1,plain,
~ spl0_1,
inference(sat_conversion,[],[f194]) ).
cnf(s3,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_4 ),
inference(sat_conversion,[],[f322]) ).
cnf(s4,plain,
( spl0_3
| spl0_5 ),
inference(sat_conversion,[],[f332]) ).
cnf(s5,plain,
( spl0_4
| spl0_6 ),
inference(sat_conversion,[],[f345]) ).
cnf(s6,plain,
( ~ spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f358]) ).
cnf(s10,plain,
( spl0_4
| ~ spl0_6
| ~ spl0_7 ),
inference(sat_conversion,[],[f624]) ).
cnf(s12,plain,
( ~ spl0_5
| ~ spl0_12 ),
inference(sat_conversion,[],[f696]) ).
cnf(s19,plain,
( spl0_3
| ~ spl0_19 ),
inference(sat_conversion,[],[f1046]) ).
cnf(s21,plain,
( spl0_12
| spl0_21 ),
inference(sat_conversion,[],[f1161]) ).
cnf(s22,plain,
( ~ spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f1201]) ).
cnf(s23,plain,
( ~ spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f1258]) ).
cnf(s42,plain,
( ~ spl0_21
| spl0_42 ),
inference(sat_conversion,[],[f2909]) ).
cnf(s45,plain,
( ~ spl0_42
| spl0_45 ),
inference(sat_conversion,[],[f3055]) ).
cnf(s46,plain,
( ~ spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f3267]) ).
cnf(s47,plain,
( spl0_19
| ~ spl0_23
| ~ spl0_46 ),
inference(sat_conversion,[],[f3268]) ).
cnf(s50,plain,
spl0_3,
inference(rat,[],[s47,s46,s23,s45,s22,s42,s21,s12,s4,s19]) ).
cnf(s51,plain,
~ spl0_4,
inference(rat,[],[s3,s1,s50]) ).
cnf(s52,plain,
spl0_6,
inference(rat,[],[s5,s51]) ).
cnf(s53,plain,
~ spl0_7,
inference(rat,[],[s10,s51,s52]) ).
cnf(s55,plain,
$false,
inference(rat,[],[s6,s53,s52]) ).
fof(f3269,plain,
$false,
inference(avatar_sat_refutation,[],[s55]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET271-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n020.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 01:17:35 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
% 12.49/2.78 % (3943519)Input is clausal, will run a generic CNF schedule.
% 12.49/2.78 % (3943525)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=578294739:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.49/2.78 % (3943530)dis-21_1_sil=8000:lcm=predicate:random_seed=754470013:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 12.49/2.78 % (3943529)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2243817381:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.49/2.78 % (3943526)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2140834764:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.49/2.78 % (3943528)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=926012841:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.49/2.78 % (3943524)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=1962535931:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.49/2.78 % (3943527)lrs+10_1_sil=8000:sp=occurrence:random_seed=220410922:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.49/2.78 % (3943527)Refutation not found, incomplete strategy
% 12.49/2.78 % (3943527)------------------------------
% 12.49/2.78 % (3943527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.78 % (3943527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.78 % (3943527)CaDiCaL version: 2.1.3
% 12.49/2.78 % (3943527)Termination reason: Refutation not found, incomplete strategy
% 12.49/2.78 % (3943527)Time elapsed: 0.001 s
% 12.49/2.78 % (3943527)Peak memory usage: 87 MB
% 12.49/2.78 % (3943528)Refutation not found, incomplete strategy
% 12.49/2.78 % (3943528)------------------------------
% 12.49/2.78 % (3943528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.78 % (3943528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.78 % (3943528)CaDiCaL version: 2.1.3
% 12.49/2.78 % (3943528)Termination reason: Refutation not found, incomplete strategy
% 12.49/2.78 % (3943528)Time elapsed: 0.001 s
% 12.49/2.78 % (3943528)Peak memory usage: 87 MB
% 12.49/2.78 % (3943530)Instruction limit reached!
% 12.49/2.78 % (3943530)------------------------------
% 12.49/2.78 % (3943530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.78 % (3943530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.78 % (3943530)CaDiCaL version: 2.1.3
% 12.49/2.78 % (3943530)Termination reason: Instruction limit
% 12.49/2.78 % (3943530)Termination phase: Saturation
% 12.49/2.78 % (3943530)Time elapsed: 0.069 s
% 12.49/2.78 % (3943530)Peak memory usage: 89 MB
% 12.49/2.78 % (3943530)Instructions burned: 117 (million)
% 12.49/2.78 % (3943529)Instruction limit reached!
% 12.49/2.78 % (3943529)------------------------------
% 12.49/2.78 % (3943529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.78 % (3943529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.78 % (3943529)CaDiCaL version: 2.1.3
% 12.49/2.78 % (3943529)Termination reason: Instruction limit
% 12.49/2.78 % (3943529)Termination phase: Saturation
% 12.49/2.78 % (3943529)Time elapsed: 0.134 s
% 12.49/2.78 % (3943529)Peak memory usage: 91 MB
% 12.49/2.78 % (3943529)Instructions burned: 181 (million)
% 12.49/2.78 % (3943538)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1419293605:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.49/2.78 % (3943538)Refutation not found, incomplete strategy
% 12.49/2.78 % (3943538)------------------------------
% 12.49/2.78 % (3943538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.78 % (3943538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.78 % (3943538)CaDiCaL version: 2.1.3
% 12.49/2.78 % (3943538)Termination reason: Refutation not found, incomplete strategy
% 12.49/2.78 % (3943538)Time elapsed: 0.001 s
% 12.49/2.78 % (3943538)Peak memory usage: 87 MB
% 12.49/2.78 % (3943528)------------------------------
% 12.49/2.78 % (3943528)------------------------------
% 12.49/2.78 % (3943527)------------------------------
% 12.49/2.78 % (3943527)------------------------------
% 21.67/4.01 % (3943539)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3072834472:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 21.67/4.01 % (3943542)lrs+10_64_to=lpo:sil=8000:random_seed=1243046982:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 21.67/4.01 % (3943541)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3249324296:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 21.67/4.01 % (3943539)Instruction limit reached!
% 21.67/4.01 % (3943539)------------------------------
% 21.67/4.01 % (3943539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.67/4.01 % (3943539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.67/4.01 % (3943539)CaDiCaL version: 2.1.3
% 21.67/4.01 % (3943539)Termination reason: Instruction limit
% 21.67/4.01 % (3943539)Termination phase: Saturation
% 21.67/4.01 % (3943539)Time elapsed: 0.107 s
% 21.67/4.01 % (3943539)Peak memory usage: 91 MB
% 21.67/4.01 % (3943539)Instructions burned: 189 (million)
% 21.67/4.01 % (3943541)Refutation not found, incomplete strategy
% 21.67/4.01 % (3943541)------------------------------
% 21.67/4.01 % (3943541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.67/4.01 % (3943541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.67/4.01 % (3943541)CaDiCaL version: 2.1.3
% 21.67/4.01 % (3943541)Termination reason: Refutation not found, incomplete strategy
% 21.67/4.01 % (3943541)Time elapsed: 0.003 s
% 21.67/4.01 % (3943541)Peak memory usage: 87 MB
% 21.67/4.01 % (3943541)Instructions burned: 4 (million)
% 21.67/4.01 % (3943538)------------------------------
% 21.67/4.01 % (3943538)------------------------------
% 21.67/4.01 % (3943542)Instruction limit reached!
% 21.67/4.01 % (3943542)------------------------------
% 21.67/4.01 % (3943542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.67/4.01 % (3943542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.67/4.01 % (3943542)CaDiCaL version: 2.1.3
% 21.67/4.01 % (3943542)Termination reason: Instruction limit
% 21.67/4.01 % (3943542)Termination phase: Saturation
% 21.67/4.01 % (3943542)Time elapsed: 0.081 s
% 21.67/4.01 % (3943542)Peak memory usage: 89 MB
% 21.67/4.01 % (3943542)Instructions burned: 127 (million)
% 21.67/4.01 % (3943546)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3423013622:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 21.67/4.01 % (3943547)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4014395520:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 21.67/4.01 % (3943548)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3686925533:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 21.67/4.01 % (3943541)------------------------------
% 21.67/4.01 % (3943541)------------------------------
% 21.67/4.01 % (3943546)Instruction limit reached!
% 21.67/4.01 % (3943546)------------------------------
% 21.67/4.01 % (3943546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.67/4.01 % (3943546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.67/4.01 % (3943546)CaDiCaL version: 2.1.3
% 21.67/4.01 % (3943546)Termination reason: Instruction limit
% 21.67/4.01 % (3943546)Termination phase: Saturation
% 21.67/4.01 % (3943546)Time elapsed: 0.118 s
% 21.67/4.01 % (3943546)Peak memory usage: 89 MB
% 21.67/4.01 % (3943546)Instructions burned: 194 (million)
% 21.67/4.01 % (3943547)Instruction limit reached!
% 21.67/4.01 % (3943547)------------------------------
% 21.67/4.01 % (3943547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.67/4.01 % (3943547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.67/4.01 % (3943547)CaDiCaL version: 2.1.3
% 21.67/4.01 % (3943547)Termination reason: Instruction limit
% 21.67/4.01 % (3943547)Termination phase: Saturation
% 21.67/4.01 % (3943547)Time elapsed: 0.105 s
% 21.67/4.01 % (3943547)Peak memory usage: 91 MB
% 21.67/4.01 % (3943547)Instructions burned: 157 (million)
% 21.67/4.01 % (3943552)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=665554674:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 21.67/4.01 % (3943552)Refutation not found, incomplete strategy
% 21.67/4.01 % (3943552)------------------------------
% 21.67/4.01 % (3943552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.50/5.97 % (3943552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.50/5.97 % (3943552)CaDiCaL version: 2.1.3
% 35.50/5.97 % (3943552)Termination reason: Refutation not found, incomplete strategy
% 35.50/5.97 % (3943552)Time elapsed: 0.002 s
% 35.50/5.97 % (3943552)Peak memory usage: 88 MB
% 35.50/5.97 % (3943552)Instructions burned: 1 (million)
% 35.50/5.97 % (3943553)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1598979783:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 35.50/5.97 % (3943553)Refutation not found, incomplete strategy
% 35.50/5.97 % (3943553)------------------------------
% 35.50/5.97 % (3943553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.50/5.97 % (3943553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.50/5.97 % (3943553)CaDiCaL version: 2.1.3
% 35.50/5.97 % (3943553)Termination reason: Refutation not found, incomplete strategy
% 35.50/5.97 % (3943553)Time elapsed: 0.005 s
% 35.50/5.97 % (3943553)Peak memory usage: 88 MB
% 35.50/5.97 % (3943553)Instructions burned: 8 (million)
% 35.50/5.97 % (3943554)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=800666257:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 35.50/5.97 % (3943552)------------------------------
% 35.50/5.97 % (3943552)------------------------------
% 35.50/5.97 % (3943553)------------------------------
% 35.50/5.97 % (3943553)------------------------------
% 35.50/5.97 % (3943554)Instruction limit reached!
% 35.50/5.97 % (3943554)------------------------------
% 35.50/5.97 % (3943554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.50/5.97 % (3943554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.50/5.97 % (3943554)CaDiCaL version: 2.1.3
% 35.50/5.97 % (3943554)Termination reason: Instruction limit
% 35.50/5.97 % (3943554)Termination phase: Saturation
% 35.50/5.97 % (3943554)Time elapsed: 0.163 s
% 35.50/5.97 % (3943554)Peak memory usage: 90 MB
% 35.50/5.97 % (3943554)Instructions burned: 243 (million)
% 35.50/5.97 % (3943558)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3631636208:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 35.50/5.97 % (3943560)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2075309629:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 35.50/5.97 % (3943559)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=87975527:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 35.50/5.97 % (3943559)Refutation not found, incomplete strategy
% 35.50/5.97 % (3943559)------------------------------
% 35.50/5.97 % (3943559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.50/5.97 % (3943559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.50/5.97 % (3943559)CaDiCaL version: 2.1.3
% 35.50/5.97 % (3943559)Termination reason: Refutation not found, incomplete strategy
% 35.50/5.97 % (3943559)Time elapsed: 0.001 s
% 35.50/5.97 % (3943559)Peak memory usage: 87 MB
% 35.50/5.97 % (3943559)------------------------------
% 35.50/5.97 % (3943559)------------------------------
% 35.50/5.97 % (3943560)Instruction limit reached!
% 35.50/5.97 % (3943560)------------------------------
% 35.50/5.97 % (3943560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.50/5.97 % (3943560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.50/5.97 % (3943560)CaDiCaL version: 2.1.3
% 35.50/5.97 % (3943560)Termination reason: Instruction limit
% 35.50/5.97 % (3943560)Termination phase: Saturation
% 35.50/5.97 % (3943560)Time elapsed: 0.294 s
% 35.50/5.97 % (3943560)Peak memory usage: 93 MB
% 35.50/5.97 % (3943560)Instructions burned: 501 (million)
% 35.50/5.97 % (3943564)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3285374237:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 35.50/5.97 % (3943565)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1236974766:i=264:kws=precedence:fsr=off_2982 on theBenchmark for (2982ds/264Mi)
% 35.50/5.97 % (3943564)Instruction limit reached!
% 35.50/5.97 % (3943564)------------------------------
% 35.50/5.97 % (3943564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.50/5.97 % (3943564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.28/9.21 % (3943564)CaDiCaL version: 2.1.3
% 59.28/9.21 % (3943564)Termination reason: Instruction limit
% 59.28/9.21 % (3943564)Termination phase: Saturation
% 59.28/9.21 % (3943564)Time elapsed: 0.114 s
% 59.28/9.21 % (3943564)Peak memory usage: 89 MB
% 59.28/9.21 % (3943564)Instructions burned: 192 (million)
% 59.28/9.21 % (3943565)Instruction limit reached!
% 59.28/9.21 % (3943565)------------------------------
% 59.28/9.21 % (3943565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.28/9.21 % (3943565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.28/9.21 % (3943565)CaDiCaL version: 2.1.3
% 59.28/9.21 % (3943565)Termination reason: Instruction limit
% 59.28/9.21 % (3943565)Termination phase: Saturation
% 59.28/9.21 % (3943565)Time elapsed: 0.177 s
% 59.28/9.21 % (3943565)Peak memory usage: 92 MB
% 59.28/9.21 % (3943565)Instructions burned: 265 (million)
% 59.28/9.21 % (3943568)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3088000116:cond=on:i=156:bs=on:gtg=exists_all:er=known_2980 on theBenchmark for (2980ds/156Mi)
% 59.28/9.21 % (3943568)Instruction limit reached!
% 59.28/9.21 % (3943568)------------------------------
% 59.28/9.21 % (3943568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.28/9.21 % (3943568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.28/9.21 % (3943568)CaDiCaL version: 2.1.3
% 59.28/9.21 % (3943568)Termination reason: Instruction limit
% 59.28/9.21 % (3943568)Termination phase: Saturation
% 59.28/9.21 % (3943568)Time elapsed: 0.108 s
% 59.28/9.21 % (3943568)Peak memory usage: 90 MB
% 59.28/9.21 % (3943568)Instructions burned: 157 (million)
% 59.28/9.21 % (3943569)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2804365000:i=3256:kws=precedence:bd=preordered:av=off_2979 on theBenchmark for (2979ds/3256Mi)
% 59.28/9.21 % (3943571)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2605683709:i=537:av=off:ss=included_2978 on theBenchmark for (2978ds/537Mi)
% 59.28/9.21 % (3943571)Refutation not found, incomplete strategy
% 59.28/9.21 % (3943571)------------------------------
% 59.28/9.21 % (3943571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.28/9.21 % (3943571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.28/9.21 % (3943571)CaDiCaL version: 2.1.3
% 59.28/9.21 % (3943571)Termination reason: Refutation not found, incomplete strategy
% 59.28/9.21 % (3943571)Time elapsed: 0.001 s
% 59.28/9.21 % (3943571)Peak memory usage: 87 MB
% 59.28/9.21 % (3943571)------------------------------
% 59.28/9.21 % (3943571)------------------------------
% 59.28/9.21 % (3943574)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3189877904:i=180:bd=preordered:av=off_2974 on theBenchmark for (2974ds/180Mi)
% 59.28/9.21 % (3943574)Instruction limit reached!
% 59.28/9.21 % (3943574)------------------------------
% 59.28/9.21 % (3943574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.28/9.21 % (3943574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.28/9.21 % (3943574)CaDiCaL version: 2.1.3
% 59.28/9.21 % (3943574)Termination reason: Instruction limit
% 59.28/9.21 % (3943574)Termination phase: Saturation
% 59.28/9.21 % (3943574)Time elapsed: 0.107 s
% 59.28/9.21 % (3943574)Peak memory usage: 90 MB
% 59.28/9.21 % (3943574)Instructions burned: 180 (million)
% 59.28/9.21 % (3943548)Instruction limit reached!
% 59.28/9.21 % (3943548)------------------------------
% 59.28/9.21 % (3943548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.28/9.21 % (3943548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.28/9.21 % (3943548)CaDiCaL version: 2.1.3
% 59.28/9.21 % (3943548)Termination reason: Instruction limit
% 59.28/9.21 % (3943548)Termination phase: Saturation
% 59.28/9.21 % (3943548)Time elapsed: 2.146 s
% 59.28/9.21 % (3943548)Peak memory usage: 148 MB
% 59.28/9.21 % (3943548)Instructions burned: 3394 (million)
% 59.28/9.21 % (3943576)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2455841728:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/10307Mi)
% 59.28/9.21 % (3943577)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=387343245:i=412:gtgl=4:gtg=exists_all_2970 on theBenchmark for (2970ds/412Mi)
% 82.12/12.49 % (3943577)Instruction limit reached!
% 82.12/12.49 % (3943577)------------------------------
% 82.12/12.49 % (3943577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.12/12.49 % (3943577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.12/12.49 % (3943577)CaDiCaL version: 2.1.3
% 82.12/12.49 % (3943577)Termination reason: Instruction limit
% 82.12/12.49 % (3943577)Termination phase: Saturation
% 82.12/12.49 % (3943577)Time elapsed: 0.186 s
% 82.12/12.49 % (3943577)Peak memory usage: 90 MB
% 82.12/12.49 % (3943577)Instructions burned: 414 (million)
% 82.12/12.49 % (3943580)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2775612559:s2pl=no:i=8478:s2at=4:nm=6_2966 on theBenchmark for (2966ds/8478Mi)
% 82.12/12.49 % (3943569)Instruction limit reached!
% 82.12/12.49 % (3943569)------------------------------
% 82.12/12.49 % (3943569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.12/12.49 % (3943569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.12/12.49 % (3943569)CaDiCaL version: 2.1.3
% 82.12/12.49 % (3943569)Termination reason: Instruction limit
% 82.12/12.49 % (3943569)Termination phase: Saturation
% 82.12/12.49 % (3943569)Time elapsed: 1.895 s
% 82.12/12.49 % (3943569)Peak memory usage: 149 MB
% 82.12/12.49 % (3943569)Instructions burned: 3256 (million)
% 82.12/12.49 % (3943584)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3562717357:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2958 on theBenchmark for (2958ds/303Mi)
% 82.12/12.49 % (3943584)Refutation not found, incomplete strategy
% 82.12/12.49 % (3943584)------------------------------
% 82.12/12.49 % (3943584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.12/12.49 % (3943584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.12/12.49 % (3943584)CaDiCaL version: 2.1.3
% 82.12/12.49 % (3943584)Termination reason: Refutation not found, incomplete strategy
% 82.12/12.49 % (3943584)Time elapsed: 0.001 s
% 82.12/12.49 % (3943584)Peak memory usage: 88 MB
% 82.12/12.49 % (3943584)Instructions burned: 1 (million)
% 82.12/12.49 % (3943584)------------------------------
% 82.12/12.49 % (3943584)------------------------------
% 82.12/12.49 % (3943558)Instruction limit reached!
% 82.12/12.49 % (3943558)------------------------------
% 82.12/12.49 % (3943558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.12/12.49 % (3943558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.12/12.49 % (3943558)CaDiCaL version: 2.1.3
% 82.12/12.49 % (3943558)Termination reason: Instruction limit
% 82.12/12.49 % (3943558)Termination phase: Saturation
% 82.12/12.49 % (3943558)Time elapsed: 3.205 s
% 82.12/12.49 % (3943558)Peak memory usage: 157 MB
% 82.12/12.49 % (3943558)Instructions burned: 5210 (million)
% 82.12/12.49 % (3943586)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=970781134:st=4:i=720:sd=3:fsr=off:ss=axioms_2954 on theBenchmark for (2954ds/720Mi)
% 82.12/12.49 % (3943587)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2699881404:i=598:bs=on:bd=preordered:av=off:ss=axioms_2954 on theBenchmark for (2954ds/598Mi)
% 82.12/12.49 % (3943587)Refutation not found, incomplete strategy
% 82.12/12.49 % (3943587)------------------------------
% 82.12/12.49 % (3943587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.12/12.49 % (3943587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.12/12.49 % (3943587)CaDiCaL version: 2.1.3
% 82.12/12.49 % (3943587)Termination reason: Refutation not found, incomplete strategy
% 82.12/12.49 % (3943587)Time elapsed: 0.001 s
% 82.12/12.49 % (3943587)Peak memory usage: 87 MB
% 82.12/12.49 % (3943587)------------------------------
% 82.12/12.49 % (3943587)------------------------------
% 82.12/12.49 % (3943586)Instruction limit reached!
% 82.12/12.49 % (3943586)------------------------------
% 82.12/12.49 % (3943586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.12/12.49 % (3943586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.12/12.49 % (3943586)CaDiCaL version: 2.1.3
% 82.12/12.49 % (3943586)Termination reason: Instruction limit
% 82.12/12.49 % (3943586)Termination phase: Saturation
% 82.12/12.49 % (3943586)Time elapsed: 0.443 s
% 82.12/12.49 % (3943586)Peak memory usage: 96 MB
% 82.12/12.49 % (3943586)Instructions burned: 721 (million)
% 112.69/16.88 % (3943590)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3754838866:i=2989:sd=3:ss=axioms:sgt=60_2950 on theBenchmark for (2950ds/2989Mi)
% 112.69/16.88 % (3943591)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3076724119:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2948 on theBenchmark for (2948ds/1997Mi)
% 112.69/16.88 % (3943591)Instruction limit reached!
% 112.69/16.88 % (3943591)------------------------------
% 112.69/16.88 % (3943591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.69/16.88 % (3943591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.69/16.88 % (3943591)CaDiCaL version: 2.1.3
% 112.69/16.88 % (3943591)Termination reason: Instruction limit
% 112.69/16.88 % (3943591)Termination phase: Saturation
% 112.69/16.88 % (3943591)Time elapsed: 1.255 s
% 112.69/16.88 % (3943591)Peak memory usage: 137 MB
% 112.69/16.88 % (3943591)Instructions burned: 1999 (million)
% 112.69/16.88 % (3943594)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2950045885:i=2088:bd=preordered:av=off_2934 on theBenchmark for (2934ds/2088Mi)
% 112.69/16.88 % (3943590)Instruction limit reached!
% 112.69/16.88 % (3943590)------------------------------
% 112.69/16.88 % (3943590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.69/16.88 % (3943590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.69/16.88 % (3943590)CaDiCaL version: 2.1.3
% 112.69/16.88 % (3943590)Termination reason: Instruction limit
% 112.69/16.88 % (3943590)Termination phase: Saturation
% 112.69/16.88 % (3943590)Time elapsed: 1.789 s
% 112.69/16.88 % (3943590)Peak memory usage: 143 MB
% 112.69/16.88 % (3943590)Instructions burned: 2989 (million)
% 112.69/16.88 % (3943596)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3195831699:i=1098:nicw=on_2930 on theBenchmark for (2930ds/1098Mi)
% 112.69/16.88 % (3943596)Instruction limit reached!
% 112.69/16.88 % (3943596)------------------------------
% 112.69/16.88 % (3943596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.69/16.88 % (3943596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.69/16.88 % (3943596)CaDiCaL version: 2.1.3
% 112.69/16.88 % (3943596)Termination reason: Instruction limit
% 112.69/16.88 % (3943596)Termination phase: Saturation
% 112.69/16.88 % (3943596)Time elapsed: 0.641 s
% 112.69/16.88 % (3943596)Peak memory usage: 102 MB
% 112.69/16.88 % (3943596)Instructions burned: 1099 (million)
% 112.69/16.88 % (3943598)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=68498018:i=433:bd=preordered_2922 on theBenchmark for (2922ds/433Mi)
% 112.69/16.88 % (3943598)Refutation not found, incomplete strategy
% 112.69/16.88 % (3943598)------------------------------
% 112.69/16.88 % (3943598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.69/16.88 % (3943598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.69/16.88 % (3943598)CaDiCaL version: 2.1.3
% 112.69/16.88 % (3943598)Termination reason: Refutation not found, incomplete strategy
% 112.69/16.88 % (3943598)Time elapsed: 0.010 s
% 112.69/16.88 % (3943598)Peak memory usage: 88 MB
% 112.69/16.88 % (3943598)Instructions burned: 16 (million)
% 112.69/16.88 % (3943594)Instruction limit reached!
% 112.69/16.88 % (3943594)------------------------------
% 112.69/16.88 % (3943594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.69/16.88 % (3943594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.69/16.88 % (3943594)CaDiCaL version: 2.1.3
% 112.69/16.88 % (3943594)Termination reason: Instruction limit
% 112.69/16.88 % (3943594)Termination phase: Saturation
% 112.69/16.88 % (3943594)Time elapsed: 1.318 s
% 112.69/16.88 % (3943594)Peak memory usage: 138 MB
% 112.69/16.88 % (3943594)Instructions burned: 2088 (million)
% 112.69/16.88 % (3943598)------------------------------
% 112.69/16.88 % (3943598)------------------------------
% 112.69/16.88 % (3943600)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=463706814:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2919 on theBenchmark for (2919ds/2942Mi)
% 112.69/16.88 % (3943601)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3997378729:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2918 on theBenchmark for (2918ds/6922Mi)
% 122.77/18.16 % (3943580)Instruction limit reached!
% 122.77/18.16 % (3943580)------------------------------
% 122.77/18.16 % (3943580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.77/18.16 % (3943580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.77/18.16 % (3943580)CaDiCaL version: 2.1.3
% 122.77/18.16 % (3943580)Termination reason: Instruction limit
% 122.77/18.16 % (3943580)Termination phase: Saturation
% 122.77/18.16 % (3943580)Time elapsed: 4.888 s
% 122.77/18.16 % (3943580)Peak memory usage: 153 MB
% 122.77/18.16 % (3943580)Instructions burned: 8479 (million)
% 122.77/18.16 % (3943604)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3746613789:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2916 on theBenchmark for (2916ds/596Mi)
% 122.77/18.16 % (3943604)Instruction limit reached!
% 122.77/18.16 % (3943604)------------------------------
% 122.77/18.16 % (3943604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.77/18.16 % (3943604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.77/18.16 % (3943604)CaDiCaL version: 2.1.3
% 122.77/18.16 % (3943604)Termination reason: Instruction limit
% 122.77/18.16 % (3943604)Termination phase: Saturation
% 122.77/18.16 % (3943604)Time elapsed: 0.320 s
% 122.77/18.16 % (3943604)Peak memory usage: 99 MB
% 122.77/18.16 % (3943604)Instructions burned: 596 (million)
% 122.77/18.16 % (3943606)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2110997503:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2911 on theBenchmark for (2911ds/4123Mi)
% 122.77/18.16 % (3943576)Instruction limit reached!
% 122.77/18.16 % (3943576)------------------------------
% 122.77/18.16 % (3943576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.77/18.16 % (3943576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.77/18.16 % (3943576)CaDiCaL version: 2.1.3
% 122.77/18.16 % (3943576)Termination reason: Instruction limit
% 122.77/18.16 % (3943576)Termination phase: Saturation
% 122.77/18.16 % (3943576)Time elapsed: 6.559 s
% 122.77/18.16 % (3943576)Peak memory usage: 182 MB
% 122.77/18.16 % (3943576)Instructions burned: 10308 (million)
% 122.77/18.16 % (3943608)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=804944434:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2904 on theBenchmark for (2904ds/16411Mi)
% 122.77/18.16 % (3943600)Instruction limit reached!
% 122.77/18.16 % (3943600)------------------------------
% 122.77/18.16 % (3943600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.77/18.16 % (3943600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.77/18.16 % (3943600)CaDiCaL version: 2.1.3
% 122.77/18.16 % (3943600)Termination reason: Instruction limit
% 122.77/18.16 % (3943600)Termination phase: Saturation
% 122.77/18.16 % (3943600)Time elapsed: 1.689 s
% 122.77/18.16 % (3943600)Peak memory usage: 138 MB
% 122.77/18.16 % (3943600)Instructions burned: 2944 (million)
% 122.77/18.16 % (3943610)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3305960139:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2901 on theBenchmark for (2901ds/1670Mi)
% 122.77/18.16 % (3943610)Instruction limit reached!
% 122.77/18.16 % (3943610)------------------------------
% 122.77/18.16 % (3943610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.77/18.16 % (3943610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.77/18.16 % (3943610)CaDiCaL version: 2.1.3
% 122.77/18.16 % (3943610)Termination reason: Instruction limit
% 122.77/18.16 % (3943610)Termination phase: Saturation
% 122.77/18.16 % (3943610)Time elapsed: 1.052 s
% 122.77/18.16 % (3943610)Peak memory usage: 136 MB
% 122.77/18.16 % (3943610)Instructions burned: 1670 (million)
% 122.77/18.16 % (3943612)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=1685604914:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2888 on theBenchmark for (2888ds/1722Mi)
% 122.77/18.16 % (3943606)Instruction limit reached!
% 122.77/18.16 % (3943606)------------------------------
% 122.77/18.16 % (3943606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.77/18.16 % (3943606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.75/20.02 % (3943606)CaDiCaL version: 2.1.3
% 134.75/20.02 % (3943606)Termination reason: Instruction limit
% 134.75/20.02 % (3943606)Termination phase: Saturation
% 134.75/20.02 % (3943606)Time elapsed: 2.597 s
% 134.75/20.02 % (3943606)Peak memory usage: 155 MB
% 134.75/20.02 % (3943606)Instructions burned: 4123 (million)
% 134.75/20.02 % (3943614)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3835456842:cts=off:cond=on:i=9530:bs=on:fsd=on_2883 on theBenchmark for (2883ds/9530Mi)
% 134.75/20.02 % (3943612)Refutation not found, incomplete strategy
% 134.75/20.02 % (3943612)------------------------------
% 134.75/20.02 % (3943612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.75/20.02 % (3943612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.75/20.02 % (3943612)CaDiCaL version: 2.1.3
% 134.75/20.02 % (3943612)Termination reason: Refutation not found, incomplete strategy
% 134.75/20.02 % (3943612)Time elapsed: 0.596 s
% 134.75/20.02 % (3943612)Peak memory usage: 128 MB
% 134.75/20.03 % (3943612)Instructions burned: 912 (million)
% 134.75/20.03 % (3943601)Instruction limit reached!
% 134.75/20.03 % (3943601)------------------------------
% 134.75/20.03 % (3943601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.75/20.03 % (3943601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.75/20.03 % (3943601)CaDiCaL version: 2.1.3
% 134.75/20.03 % (3943601)Termination reason: Instruction limit
% 134.75/20.03 % (3943601)Termination phase: Saturation
% 134.75/20.03 % (3943601)Time elapsed: 3.634 s
% 134.75/20.03 % (3943601)Peak memory usage: 187 MB
% 134.75/20.03 % (3943601)Instructions burned: 6922 (million)
% 134.75/20.03 % (3943612)------------------------------
% 134.75/20.03 % (3943612)------------------------------
% 134.75/20.03 % (3943616)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2355636491:st=2:i=4495:sd=10:ss=included_2880 on theBenchmark for (2880ds/4495Mi)
% 134.75/20.03 % (3943617)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=2311981508:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2878 on theBenchmark for (2878ds/4920Mi)
% 134.75/20.03 % (3943616)Instruction limit reached!
% 134.75/20.03 % (3943616)------------------------------
% 134.75/20.03 % (3943616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.75/20.03 % (3943616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.75/20.03 % (3943616)CaDiCaL version: 2.1.3
% 134.75/20.03 % (3943616)Termination reason: Instruction limit
% 134.75/20.03 % (3943616)Termination phase: Saturation
% 134.75/20.03 % (3943616)Time elapsed: 2.735 s
% 134.75/20.03 % (3943616)Peak memory usage: 156 MB
% 134.75/20.03 % (3943616)Instructions burned: 4495 (million)
% 134.75/20.03 % (3943620)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=3338222466:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2850 on theBenchmark for (2850ds/2083Mi)
% 134.75/20.03 % (3943617)Instruction limit reached!
% 134.75/20.03 % (3943617)------------------------------
% 134.75/20.03 % (3943617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.75/20.03 % (3943617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.75/20.03 % (3943617)CaDiCaL version: 2.1.3
% 134.75/20.03 % (3943617)Termination reason: Instruction limit
% 134.75/20.03 % (3943617)Termination phase: Saturation
% 134.75/20.03 % (3943617)Time elapsed: 2.987 s
% 134.75/20.03 % (3943617)Peak memory usage: 150 MB
% 134.75/20.03 % (3943617)Instructions burned: 4921 (million)
% 134.75/20.03 % (3943622)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=1175331119:i=4629:av=off:gsp=on_2847 on theBenchmark for (2847ds/4629Mi)
% 134.75/20.03 % (3943622)Refutation not found, incomplete strategy
% 134.75/20.03 % (3943622)------------------------------
% 134.75/20.03 % (3943622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.75/20.03 % (3943622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.75/20.03 % (3943622)CaDiCaL version: 2.1.3
% 134.75/20.03 % (3943622)Termination reason: Refutation not found, incomplete strategy
% 134.75/20.03 % (3943622)Time elapsed: 0.577 s
% 134.75/20.03 % (3943622)Peak memory usage: 129 MB
% 134.75/20.03 % (3943622)Instructions burned: 880 (million)
% 143.39/21.35 % (3943622)------------------------------
% 143.39/21.35 % (3943622)------------------------------
% 143.39/21.35 % (3943620)Instruction limit reached!
% 143.39/21.35 % (3943620)------------------------------
% 143.39/21.35 % (3943620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.39/21.35 % (3943620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.39/21.35 % (3943620)CaDiCaL version: 2.1.3
% 143.39/21.35 % (3943620)Termination reason: Instruction limit
% 143.39/21.35 % (3943620)Termination phase: Saturation
% 143.39/21.35 % (3943620)Time elapsed: 1.249 s
% 143.39/21.35 % (3943620)Peak memory usage: 135 MB
% 143.39/21.35 % (3943620)Instructions burned: 2083 (million)
% 143.39/21.35 % (3943624)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3766050197:i=1258:av=off_2837 on theBenchmark for (2837ds/1258Mi)
% 143.39/21.35 % (3943625)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3382889596:i=7343:av=off:ss=included_2836 on theBenchmark for (2836ds/7343Mi)
% 143.39/21.35 [W928 01:17:52.878655572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 [W928 01:17:52.878689778 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 [W928 01:17:52.878725729 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 [W928 01:17:52.878737145 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 [W928 01:17:52.878769306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 [W928 01:17:52.878781276 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 % (3943625)Refutation not found, incomplete strategy
% 143.39/21.35 % (3943625)------------------------------
% 143.39/21.35 % (3943625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.39/21.35 % (3943625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.39/21.35 % (3943625)CaDiCaL version: 2.1.3
% 143.39/21.35 % (3943625)Termination reason: Refutation not found, incomplete strategy
% 143.39/21.35 % (3943625)Time elapsed: 0.564 s
% 143.39/21.35 % (3943625)Peak memory usage: 127 MB
% 143.39/21.35 % (3943625)Instructions burned: 856 (million)
% 143.39/21.35 % (3943624)Instruction limit reached!
% 143.39/21.35 % (3943624)------------------------------
% 143.39/21.35 % (3943624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.39/21.35 % (3943624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.39/21.35 % (3943624)CaDiCaL version: 2.1.3
% 143.39/21.35 % (3943624)Termination reason: Instruction limit
% 143.39/21.35 % (3943624)Termination phase: Saturation
% 143.39/21.35 % (3943624)Time elapsed: 0.682 s
% 143.39/21.35 % (3943624)Peak memory usage: 94 MB
% 143.39/21.35 % (3943624)Instructions burned: 1259 (million)
% 143.39/21.35 % (3943628)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3461624468:i=1325:sd=2:ss=axioms:sgt=16_2828 on theBenchmark for (2828ds/1325Mi)
% 143.39/21.35 % (3943628)Refutation not found, incomplete strategy
% 143.39/21.35 % (3943628)------------------------------
% 143.39/21.35 % (3943628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.39/21.35 % (3943628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.39/21.35 % (3943628)CaDiCaL version: 2.1.3
% 143.39/21.35 % (3943628)Termination reason: Refutation not found, incomplete strategy
% 143.39/21.35 % (3943628)Time elapsed: 0.001 s
% 143.39/21.35 % (3943628)Peak memory usage: 87 MB
% 143.39/21.35 % (3943625)------------------------------
% 143.39/21.35 % (3943625)------------------------------
% 143.39/21.35 % (3943630)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=184833089:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2826 on theBenchmark for (2826ds/2646Mi)
% 143.39/21.35 % (3943628)------------------------------
% 143.39/21.35 % (3943628)------------------------------
% 143.39/21.35 % (3943632)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3497881686:i=1489:sd=2:ep=R:ss=axioms_2824 on theBenchmark for (2824ds/1489Mi)
% 143.39/21.35 % (3943614)Instruction limit reached!
% 143.39/21.35 % (3943614)------------------------------
% 143.39/21.35 % (3943614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.39/21.35 % (3943614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.39/21.35 % (3943614)CaDiCaL version: 2.1.3
% 143.39/21.35 % (3943614)Termination reason: Instruction limit
% 143.39/21.35 % (3943614)Termination phase: Saturation
% 143.39/21.35 % (3943614)Time elapsed: 5.960 s
% 143.39/21.35 % (3943614)Peak memory usage: 168 MB
% 143.39/21.35 % (3943614)Instructions burned: 9532 (million)
% 143.39/21.35 % (3943634)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=833770315:i=1503_2822 on theBenchmark for (2822ds/1503Mi)
% 143.39/21.35 % (3943632)Refutation not found, incomplete strategy
% 143.39/21.35 % (3943632)------------------------------
% 143.39/21.35 % (3943632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.39/21.35 % (3943632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.39/21.35 % (3943632)CaDiCaL version: 2.1.3
% 143.39/21.35 % (3943632)Termination reason: Refutation not found, incomplete strategy
% 143.39/21.35 % (3943632)Time elapsed: 0.571 s
% 143.39/21.35 % (3943632)Peak memory usage: 127 MB
% 143.39/21.35 % (3943632)Instructions burned: 856 (million)
% 143.39/21.35 % (3943632)------------------------------
% 143.39/21.35 % (3943632)------------------------------
% 143.39/21.35 % (3943636)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=856127225:i=13942:kws=frequency_2814 on theBenchmark for (2814ds/13942Mi)
% 143.39/21.35 % (3943634)Instruction limit reached!
% 143.39/21.35 % (3943634)------------------------------
% 143.39/21.35 % (3943634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.39/21.35 % (3943634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.39/21.35 % (3943634)CaDiCaL version: 2.1.3
% 143.39/21.35 % (3943634)Termination reason: Instruction limit
% 143.39/21.35 % (3943634)Termination phase: Saturation
% 143.39/21.35 % (3943634)Time elapsed: 1.008 s
% 143.39/21.35 % (3943634)Peak memory usage: 133 MB
% 143.39/21.35 % (3943634)Instructions burned: 1504 (million)
% 143.39/21.35 % (3943608)Instruction limit reached!
% 143.39/21.35 % (3943608)------------------------------
% 143.39/21.35 % (3943608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.39/21.35 % (3943608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.39/21.35 % (3943608)CaDiCaL version: 2.1.3
% 143.39/21.35 % (3943608)Termination reason: Instruction limit
% 143.39/21.35 % (3943608)Termination phase: Saturation
% 143.39/21.35 % (3943608)Time elapsed: 9.291 s
% 143.39/21.35 % (3943608)Peak memory usage: 203 MB
% 143.39/21.35 % (3943608)Instructions burned: 16412 (million)
% 143.39/21.35 % (3943638)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=2357643090:i=3604:fsr=off:er=filter_2810 on theBenchmark for (2810ds/3604Mi)
% 143.39/21.35 % (3943630)Instruction limit reached!
% 143.39/21.35 % (3943630)------------------------------
% 143.39/21.35 % (3943630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.39/21.35 % (3943630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.39/21.35 % (3943630)CaDiCaL version: 2.1.3
% 143.39/21.35 % (3943630)Termination reason: Instruction limit
% 143.39/21.35 % (3943630)Termination phase: Saturation
% 143.39/21.35 % (3943630)Time elapsed: 1.683 s
% 143.39/21.35 % (3943630)Peak memory usage: 144 MB
% 143.39/21.35 % (3943630)Instructions burned: 2647 (million)
% 143.39/21.35 % (3943639)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1778138722:i=1876:sd=1:ss=included:sgt=32_2809 on theBenchmark for (2809ds/1876Mi)
% 143.39/21.35 % (3943641)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=737674657:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2808 on theBenchmark for (2808ds/1932Mi)
% 143.39/21.35 [W928 01:17:55.714283513 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 [W928 01:17:55.714320927 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 [W928 01:17:55.714356777 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 [W928 01:17:55.714368677 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 [W928 01:17:55.714393394 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 [W928 01:17:55.714405628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.39/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.39/21.35 % (3943641)Refutation not found, incomplete strategy
% 143.39/21.35 % (3943641)------------------------------
% 143.39/21.35 % (3943641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.39/21.35 % (3943641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.39/21.35 % (3943641)CaDiCaL version: 2.1.3
% 143.39/21.35 % (3943641)Termination reason: Refutation not found, incomplete strategy
% 143.39/21.35 % (3943641)Time elapsed: 0.562 s
% 143.39/21.35 % (3943641)Peak memory usage: 127 MB
% 143.39/21.35 % (3943641)Instructions burned: 856 (million)
% 143.39/21.35 % (3943641)------------------------------
% 143.39/21.35 % (3943641)------------------------------
% 143.39/21.35 % (3943638)First to succeed.
% 143.39/21.35 % (3943638)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3943519"
% 143.39/21.35 % (3943644)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=3447081315:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2798 on theBenchmark for (2798ds/1980Mi)
% 143.39/21.35 % (3943639)Instruction limit reached!
% 143.39/21.35 % (3943639)------------------------------
% 143.39/21.35 % (3943639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.39/21.35 % (3943639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.39/21.35 % (3943639)CaDiCaL version: 2.1.3
% 143.39/21.35 % (3943639)Termination reason: Instruction limit
% 143.39/21.35 % (3943639)Termination phase: Saturation
% 143.39/21.35 % (3943639)Time elapsed: 1.155 s
% 143.39/21.35 % (3943639)Peak memory usage: 135 MB
% 143.39/21.35 % (3943639)Instructions burned: 1876 (million)
% 143.39/21.35 % (3943638)Refutation found. Thanks to Tanya!
% 143.39/21.35 % SZS status Unsatisfiable for theBenchmark
% 143.39/21.35 % SZS output start Proof for theBenchmark
% See solution above
% 145.60/21.56 % (3943638)------------------------------
% 145.60/21.56 % (3943638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.60/21.56 % (3943638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.60/21.56 % (3943638)CaDiCaL version: 2.1.3
% 145.60/21.56 % (3943638)Termination reason: Refutation
% 145.60/21.56 % (3943638)Time elapsed: 1.060 s
% 145.60/21.56 % (3943638)Peak memory usage: 138 MB
% 145.60/21.56 % (3943638)Instructions burned: 1723 (million)
% 145.60/21.56 % (3943638)------------------------------
% 145.60/21.56 % (3943638)------------------------------
% 145.60/21.56 % (3943519)Success in time 20.485 s
% 145.60/21.56 % Vampire exiting
%------------------------------------------------------------------------------