%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET275-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:40 PM UTC 2026
% Result : Unsatisfiable 117.15s 17.96s
% Output : Refutation 121.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 23
% Syntax : Number of formulae : 74 ( 39 unt; 5 def)
% Number of atoms : 117 ( 39 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 87 ( 44 ~; 43 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 10 con; 0-3 aty)
% Number of variables : 75 ( 75 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ member(X2,X0)
| ~ subclass(X0,X1)
| member(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement1) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f122,negated_conjecture,
~ subclass(domain_of(restrict(x,y,z)),intersection(domain_of(x),y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_corollary_1_to_domain_property4_1) ).
fof(f127,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(f136,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,f127]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(definition_unfolding,[],[f17,f127]) ).
fof(f143,plain,
! [X0,X1] :
( ~ member(X1,domain_of(X0))
| null_class != intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)) ),
inference(definition_unfolding,[],[f30,f28,f12]) ).
fof(f144,plain,
! [X0,X1] :
( member(X0,domain_of(X1))
| null_class = intersection(X1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,universal_class) ),
inference(definition_unfolding,[],[f32,f28,f12]) ).
fof(f185,plain,
~ subclass(domain_of(intersection(x,cross_product(y,z))),intersection(domain_of(x),y)),
inference(definition_unfolding,[],[f122,f28]) ).
fof(f190,definition,
sF0 = cross_product(y,z),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f191,plain,
cross_product(y,z) = sF0,
inference(reorient_equations,[],[f190]) ).
fof(f192,definition,
sF1 = intersection(x,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f193,plain,
intersection(x,sF0) = sF1,
inference(reorient_equations,[],[f192]) ).
fof(f194,definition,
sF2 = domain_of(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f195,plain,
domain_of(sF1) = sF2,
inference(reorient_equations,[],[f194]) ).
fof(f196,definition,
sF3 = domain_of(x),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f197,plain,
domain_of(x) = sF3,
inference(reorient_equations,[],[f196]) ).
fof(f198,definition,
sF4 = intersection(sF3,y),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f199,plain,
intersection(sF3,y) = sF4,
inference(reorient_equations,[],[f198]) ).
fof(f200,plain,
~ subclass(sF2,sF4),
inference(definition_folding,[],[f185,f199,f197,f195,f193,f191]) ).
fof(f208,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f209,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f213,plain,
! [X0] :
( ~ member(X0,y)
| member(X0,sF4)
| ~ member(X0,sF3) ),
inference(superposition,[],[f23,f199]) ).
fof(f223,plain,
member(not_subclass_element(sF2,sF4),sF2),
inference(unit_resulting_resolution,[],[f2,f200]) ).
fof(f224,plain,
~ member(not_subclass_element(sF2,sF4),sF4),
inference(unit_resulting_resolution,[],[f3,f200]) ).
fof(f232,plain,
! [X0] :
( ~ member(X0,sF1)
| member(X0,sF0) ),
inference(superposition,[],[f22,f193]) ).
fof(f233,plain,
! [X0] :
( member(X0,x)
| ~ member(X0,sF1) ),
inference(superposition,[],[f21,f193]) ).
fof(f241,plain,
member(not_subclass_element(sF2,sF4),universal_class),
inference(unit_resulting_resolution,[],[f1,f223,f4]) ).
fof(f256,plain,
! [X0] :
( ~ member(X0,sF2)
| null_class != intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)) ),
inference(superposition,[],[f143,f195]) ).
fof(f266,plain,
! [X0] :
( member(X0,sF3)
| null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,universal_class) ),
inference(superposition,[],[f144,f197]) ).
fof(f271,plain,
null_class != intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)),
inference(resolution,[],[f256,f223]) ).
fof(f325,plain,
member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))),cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)),
inference(unit_resulting_resolution,[],[f208,f271]) ).
fof(f329,plain,
! [X0,X1] :
( ~ member(regular(intersection(X0,complement(X1))),X1)
| null_class = intersection(X0,complement(X1)) ),
inference(resolution,[],[f208,f24]) ).
fof(f346,plain,
member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))),sF1),
inference(unit_resulting_resolution,[],[f209,f271]) ).
fof(f360,plain,
member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))),x),
inference(unit_resulting_resolution,[],[f233,f346]) ).
fof(f366,plain,
~ member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))),complement(sF1)),
inference(unit_resulting_resolution,[],[f24,f346]) ).
fof(f372,plain,
member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))),sF0),
inference(resolution,[],[f346,f232]) ).
fof(f400,plain,
member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))),intersection(x,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))),
inference(unit_resulting_resolution,[],[f23,f325,f360]) ).
fof(f699,plain,
! [X0] :
( null_class = intersection(X0,complement(X0))
| null_class = intersection(X0,complement(X0)) ),
inference(resolution,[],[f329,f209]) ).
fof(f711,plain,
! [X0] : null_class = intersection(X0,complement(X0)),
inference(duplicate_literal_removal,[],[f699]) ).
fof(f715,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1) ),
inference(superposition,[],[f21,f711]) ).
fof(f801,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X0,y) ),
inference(superposition,[],[f136,f191]) ).
fof(f1109,plain,
regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))))))),
inference(resolution,[],[f139,f325]) ).
fof(f1115,plain,
! [X0,X1] :
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),X0) ),
inference(superposition,[],[f136,f1109]) ).
fof(f1122,plain,
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))),sF0)
| member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),y) ),
inference(superposition,[],[f801,f1109]) ).
fof(f1126,plain,
member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),y),
inference(forward_subsumption_resolution,[],[f1122,f372]) ).
fof(f1157,plain,
( member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),sF4)
| ~ member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),sF3) ),
inference(resolution,[],[f1126,f213]) ).
fof(f1247,plain,
member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4))),
inference(resolution,[],[f1115,f325]) ).
fof(f1300,plain,
( not_subclass_element(sF2,sF4) = first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))))
| not_subclass_element(sF2,sF4) = first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))) ),
inference(resolution,[],[f1247,f8]) ).
fof(f1303,plain,
not_subclass_element(sF2,sF4) = first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),
inference(duplicate_literal_removal,[],[f1300]) ).
fof(f1332,plain,
( member(not_subclass_element(sF2,sF4),sF4)
| ~ member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),sF3) ),
inference(backward_demodulation,[],[f1157,f1303]) ).
fof(f1416,plain,
~ member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)))),sF3),
inference(forward_subsumption_resolution,[],[f1332,f224]) ).
fof(f1423,plain,
~ member(not_subclass_element(sF2,sF4),sF3),
inference(forward_demodulation,[],[f1416,f1303]) ).
fof(f1425,plain,
null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class)),
inference(unit_resulting_resolution,[],[f266,f241,f1423]) ).
fof(f1452,plain,
member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))),null_class),
inference(backward_demodulation,[],[f400,f1425]) ).
fof(f7653,plain,
~ member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF4),not_subclass_element(sF2,sF4)),universal_class))),null_class),
inference(unit_resulting_resolution,[],[f715,f366]) ).
fof(f7675,plain,
$false,
inference(forward_subsumption_resolution,[],[f7653,f1452]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET275-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 % Computer : n009.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 28 01:17:30 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.47 Running first-order theorem proving
% 0.15/0.47 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.70/3.64 % (2579560)Input is clausal, will run a generic CNF schedule.
% 18.70/3.64 % (2579571)dis-21_1_sil=8000:lcm=predicate:random_seed=4000449331: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)
% 18.70/3.64 % (2579570)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1700362508:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.70/3.64 % (2579569)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1327138994:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.70/3.64 % (2579568)lrs+10_1_sil=8000:sp=occurrence:random_seed=2526149907:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.70/3.64 % (2579565)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=3254672080:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.70/3.64 % (2579566)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3397789855:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.70/3.64 % (2579567)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4137401640:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.70/3.64 % (2579568)Refutation not found, incomplete strategy
% 18.70/3.64 % (2579568)------------------------------
% 18.70/3.64 % (2579568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/3.64 % (2579568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/3.64 % (2579568)CaDiCaL version: 2.1.3
% 18.70/3.64 % (2579568)Termination reason: Refutation not found, incomplete strategy
% 18.70/3.64 % (2579568)Time elapsed: 0.004 s
% 18.70/3.64 % (2579568)Peak memory usage: 88 MB
% 18.70/3.64 % (2579568)Instructions burned: 2 (million)
% 18.70/3.64 % (2579571)Instruction limit reached!
% 18.70/3.64 % (2579571)------------------------------
% 18.70/3.64 % (2579571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/3.64 % (2579571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/3.64 % (2579571)CaDiCaL version: 2.1.3
% 18.70/3.64 % (2579571)Termination reason: Instruction limit
% 18.70/3.64 % (2579571)Termination phase: Saturation
% 18.70/3.64 % (2579571)Time elapsed: 0.060 s
% 18.70/3.64 % (2579571)Peak memory usage: 90 MB
% 18.70/3.64 % (2579571)Instructions burned: 119 (million)
% 18.70/3.64 % (2579569)Instruction limit reached!
% 18.70/3.64 % (2579569)------------------------------
% 18.70/3.64 % (2579569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/3.64 % (2579569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/3.64 % (2579569)CaDiCaL version: 2.1.3
% 18.70/3.64 % (2579569)Termination reason: Instruction limit
% 18.70/3.64 % (2579569)Termination phase: Saturation
% 18.70/3.64 % (2579569)Time elapsed: 0.103 s
% 18.70/3.64 % (2579569)Peak memory usage: 89 MB
% 18.70/3.64 % (2579569)Instructions burned: 114 (million)
% 18.70/3.64 % (2579570)Instruction limit reached!
% 18.70/3.64 % (2579570)------------------------------
% 18.70/3.64 % (2579570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/3.64 % (2579570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/3.64 % (2579570)CaDiCaL version: 2.1.3
% 18.70/3.64 % (2579570)Termination reason: Instruction limit
% 18.70/3.64 % (2579570)Termination phase: Saturation
% 18.70/3.64 % (2579570)Time elapsed: 0.202 s
% 18.70/3.64 % (2579570)Peak memory usage: 90 MB
% 18.70/3.64 % (2579570)Instructions burned: 180 (million)
% 18.70/3.64 % (2579579)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=2914242401:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 18.70/3.64 % (2579579)Refutation not found, incomplete strategy
% 18.70/3.64 % (2579579)------------------------------
% 18.70/3.64 % (2579579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/3.64 % (2579579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/3.64 % (2579579)CaDiCaL version: 2.1.3
% 18.70/3.64 % (2579579)Termination reason: Refutation not found, incomplete strategy
% 18.70/3.64 % (2579579)Time elapsed: 0.003 s
% 18.70/3.64 % (2579579)Peak memory usage: 88 MB
% 18.70/3.64 % (2579579)Instructions burned: 3 (million)
% 18.70/3.64 % (2579580)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=306492620: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)
% 36.24/6.05 % (2579568)------------------------------
% 36.24/6.05 % (2579568)------------------------------
% 36.24/6.05 % (2579581)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3483911494:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 36.24/6.05 % (2579581)Instruction limit reached!
% 36.24/6.05 % (2579581)------------------------------
% 36.24/6.05 % (2579581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/6.05 % (2579581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/6.05 % (2579581)CaDiCaL version: 2.1.3
% 36.24/6.05 % (2579581)Termination reason: Instruction limit
% 36.24/6.05 % (2579581)Termination phase: Saturation
% 36.24/6.05 % (2579581)Time elapsed: 0.110 s
% 36.24/6.05 % (2579581)Peak memory usage: 89 MB
% 36.24/6.05 % (2579581)Instructions burned: 221 (million)
% 36.24/6.05 % (2579580)Instruction limit reached!
% 36.24/6.05 % (2579580)------------------------------
% 36.24/6.05 % (2579580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/6.05 % (2579580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/6.05 % (2579580)CaDiCaL version: 2.1.3
% 36.24/6.05 % (2579580)Termination reason: Instruction limit
% 36.24/6.05 % (2579580)Termination phase: Saturation
% 36.24/6.05 % (2579580)Time elapsed: 0.171 s
% 36.24/6.05 % (2579580)Peak memory usage: 91 MB
% 36.24/6.05 % (2579580)Instructions burned: 189 (million)
% 36.24/6.05 % (2579584)lrs+10_64_to=lpo:sil=8000:random_seed=3176929176:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 36.24/6.05 % (2579579)------------------------------
% 36.24/6.05 % (2579579)------------------------------
% 36.24/6.05 % (2579584)Instruction limit reached!
% 36.24/6.05 % (2579584)------------------------------
% 36.24/6.05 % (2579584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/6.05 % (2579584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/6.05 % (2579584)CaDiCaL version: 2.1.3
% 36.24/6.05 % (2579584)Termination reason: Instruction limit
% 36.24/6.05 % (2579584)Termination phase: Saturation
% 36.24/6.05 % (2579584)Time elapsed: 0.071 s
% 36.24/6.05 % (2579584)Peak memory usage: 89 MB
% 36.24/6.05 % (2579584)Instructions burned: 128 (million)
% 36.24/6.05 % (2579589)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1272585595:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 36.24/6.05 % (2579588)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3385946564:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 36.24/6.05 % (2579589)Instruction limit reached!
% 36.24/6.05 % (2579589)------------------------------
% 36.24/6.05 % (2579589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/6.05 % (2579589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/6.05 % (2579589)CaDiCaL version: 2.1.3
% 36.24/6.05 % (2579589)Termination reason: Instruction limit
% 36.24/6.05 % (2579589)Termination phase: Saturation
% 36.24/6.05 % (2579589)Time elapsed: 0.095 s
% 36.24/6.05 % (2579589)Peak memory usage: 91 MB
% 36.24/6.05 % (2579589)Instructions burned: 158 (million)
% 36.24/6.05 % (2579591)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3659837388:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 36.24/6.05 % (2579592)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=988748205:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 36.24/6.05 % (2579588)Instruction limit reached!
% 36.24/6.05 % (2579588)------------------------------
% 36.24/6.05 % (2579588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.24/6.05 % (2579588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.24/6.05 % (2579588)CaDiCaL version: 2.1.3
% 36.24/6.05 % (2579588)Termination reason: Instruction limit
% 36.24/6.05 % (2579588)Termination phase: Saturation
% 36.24/6.05 % (2579588)Time elapsed: 0.196 s
% 36.24/6.05 % (2579588)Peak memory usage: 90 MB
% 36.24/6.05 % (2579588)Instructions burned: 194 (million)
% 36.24/6.05 % (2579592)Instruction limit reached!
% 36.24/6.05 % (2579592)------------------------------
% 36.24/6.05 % (2579592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.27/8.76 % (2579592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.27/8.76 % (2579592)CaDiCaL version: 2.1.3
% 54.27/8.76 % (2579592)Termination reason: Instruction limit
% 54.27/8.76 % (2579592)Termination phase: Saturation
% 54.27/8.76 % (2579592)Time elapsed: 0.089 s
% 54.27/8.76 % (2579592)Peak memory usage: 89 MB
% 54.27/8.76 % (2579592)Instructions burned: 106 (million)
% 54.27/8.76 % (2579595)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=858529060:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 54.27/8.76 % (2579595)Instruction limit reached!
% 54.27/8.76 % (2579595)------------------------------
% 54.27/8.76 % (2579595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.27/8.76 % (2579595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.27/8.76 % (2579595)CaDiCaL version: 2.1.3
% 54.27/8.76 % (2579595)Termination reason: Instruction limit
% 54.27/8.76 % (2579595)Termination phase: Saturation
% 54.27/8.76 % (2579595)Time elapsed: 0.113 s
% 54.27/8.76 % (2579595)Peak memory usage: 89 MB
% 54.27/8.76 % (2579595)Instructions burned: 107 (million)
% 54.27/8.77 % (2579598)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=650709905:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 54.27/8.77 % (2579599)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1755366337:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 54.27/8.77 % (2579601)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1729360658:i=134:sd=2:doe=on:ss=axioms:sgt=14_2985 on theBenchmark for (2985ds/134Mi)
% 54.27/8.77 % (2579598)Instruction limit reached!
% 54.27/8.77 % (2579598)------------------------------
% 54.27/8.77 % (2579598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.27/8.77 % (2579598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.27/8.77 % (2579598)CaDiCaL version: 2.1.3
% 54.27/8.77 % (2579598)Termination reason: Instruction limit
% 54.27/8.77 % (2579598)Termination phase: Saturation
% 54.27/8.77 % (2579598)Time elapsed: 0.255 s
% 54.27/8.77 % (2579598)Peak memory usage: 90 MB
% 54.27/8.77 % (2579598)Instructions burned: 242 (million)
% 54.27/8.77 % (2579601)Instruction limit reached!
% 54.27/8.77 % (2579601)------------------------------
% 54.27/8.77 % (2579601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.27/8.77 % (2579601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.27/8.77 % (2579601)CaDiCaL version: 2.1.3
% 54.27/8.77 % (2579601)Termination reason: Instruction limit
% 54.27/8.77 % (2579601)Termination phase: Saturation
% 54.27/8.77 % (2579601)Time elapsed: 0.155 s
% 54.27/8.77 % (2579601)Peak memory usage: 90 MB
% 54.27/8.77 % (2579601)Instructions burned: 134 (million)
% 54.27/8.77 % (2579605)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4082335165:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi)
% 54.27/8.77 % (2579606)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1780743980:i=191:fgj=on:bd=all_2980 on theBenchmark for (2980ds/191Mi)
% 54.27/8.77 % (2579606)Instruction limit reached!
% 54.27/8.77 % (2579606)------------------------------
% 54.27/8.77 % (2579606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.27/8.77 % (2579606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.27/8.77 % (2579606)CaDiCaL version: 2.1.3
% 54.27/8.77 % (2579606)Termination reason: Instruction limit
% 54.27/8.77 % (2579606)Termination phase: Saturation
% 54.27/8.77 % (2579606)Time elapsed: 0.200 s
% 54.27/8.77 % (2579606)Peak memory usage: 89 MB
% 54.27/8.77 % (2579606)Instructions burned: 191 (million)
% 54.27/8.77 % (2579605)Instruction limit reached!
% 54.27/8.77 % (2579605)------------------------------
% 54.27/8.77 % (2579605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.27/8.77 % (2579605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.27/8.77 % (2579605)CaDiCaL version: 2.1.3
% 54.27/8.77 % (2579605)Termination reason: Instruction limit
% 54.27/8.77 % (2579605)Termination phase: Saturation
% 54.27/8.77 % (2579605)Time elapsed: 0.478 s
% 54.27/8.77 % (2579605)Peak memory usage: 93 MB
% 54.27/8.77 % (2579605)Instructions burned: 499 (million)
% 54.27/8.77 % (2579609)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3392814935:i=264:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/264Mi)
% 89.93/13.74 % (2579610)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=329146603:cond=on:i=156:bs=on:gtg=exists_all:er=known_2974 on theBenchmark for (2974ds/156Mi)
% 89.93/13.74 % (2579609)Instruction limit reached!
% 89.93/13.74 % (2579609)------------------------------
% 89.93/13.74 % (2579609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.93/13.74 % (2579609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.93/13.74 % (2579609)CaDiCaL version: 2.1.3
% 89.93/13.74 % (2579609)Termination reason: Instruction limit
% 89.93/13.74 % (2579609)Termination phase: Saturation
% 89.93/13.74 % (2579609)Time elapsed: 0.221 s
% 89.93/13.74 % (2579609)Peak memory usage: 90 MB
% 89.93/13.74 % (2579609)Instructions burned: 265 (million)
% 89.93/13.74 % (2579610)Instruction limit reached!
% 89.93/13.74 % (2579610)------------------------------
% 89.93/13.74 % (2579610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.93/13.74 % (2579610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.93/13.74 % (2579610)CaDiCaL version: 2.1.3
% 89.93/13.74 % (2579610)Termination reason: Instruction limit
% 89.93/13.74 % (2579610)Termination phase: Saturation
% 89.93/13.74 % (2579610)Time elapsed: 0.150 s
% 89.93/13.74 % (2579610)Peak memory usage: 89 MB
% 89.93/13.74 % (2579610)Instructions burned: 156 (million)
% 89.93/13.74 % (2579613)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=3315704847:i=3256:kws=precedence:bd=preordered:av=off_2971 on theBenchmark for (2971ds/3256Mi)
% 89.93/13.74 % (2579614)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3245338106:i=537:av=off:ss=included_2970 on theBenchmark for (2970ds/537Mi)
% 89.93/13.74 % (2579614)Refutation not found, incomplete strategy
% 89.93/13.74 % (2579614)------------------------------
% 89.93/13.74 % (2579614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.93/13.74 % (2579614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.93/13.74 % (2579614)CaDiCaL version: 2.1.3
% 89.93/13.74 % (2579614)Termination reason: Refutation not found, incomplete strategy
% 89.93/13.74 % (2579614)Time elapsed: 0.005 s
% 89.93/13.74 % (2579614)Peak memory usage: 88 MB
% 89.93/13.74 % (2579614)Instructions burned: 3 (million)
% 89.93/13.74 % (2579614)------------------------------
% 89.93/13.74 % (2579614)------------------------------
% 89.93/13.74 % (2579617)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1122488217:i=180:bd=preordered:av=off_2963 on theBenchmark for (2963ds/180Mi)
% 89.93/13.74 % (2579617)Instruction limit reached!
% 89.93/13.74 % (2579617)------------------------------
% 89.93/13.74 % (2579617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.93/13.74 % (2579617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.93/13.74 % (2579617)CaDiCaL version: 2.1.3
% 89.93/13.74 % (2579617)Termination reason: Instruction limit
% 89.93/13.74 % (2579617)Termination phase: Saturation
% 89.93/13.74 % (2579617)Time elapsed: 0.163 s
% 89.93/13.74 % (2579617)Peak memory usage: 90 MB
% 89.93/13.74 % (2579617)Instructions burned: 180 (million)
% 89.93/13.74 % (2579619)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=4262311870:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2958 on theBenchmark for (2958ds/10307Mi)
% 89.93/13.74 % (2579591)Instruction limit reached!
% 89.93/13.74 % (2579591)------------------------------
% 89.93/13.74 % (2579591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.93/13.74 % (2579591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.93/13.74 % (2579591)CaDiCaL version: 2.1.3
% 89.93/13.74 % (2579591)Termination reason: Instruction limit
% 89.93/13.74 % (2579591)Termination phase: Saturation
% 89.93/13.74 % (2579591)Time elapsed: 3.276 s
% 89.93/13.74 % (2579591)Peak memory usage: 149 MB
% 89.93/13.74 % (2579591)Instructions burned: 3394 (million)
% 89.93/13.74 % (2579621)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=2743608836:i=412:gtgl=4:gtg=exists_all_2955 on theBenchmark for (2955ds/412Mi)
% 89.93/13.74 % (2579621)Instruction limit reached!
% 89.93/13.74 % (2579621)------------------------------
% 89.93/13.74 % (2579621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579621)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579621)Termination reason: Instruction limit
% 117.15/17.96 % (2579621)Termination phase: Saturation
% 117.15/17.96 % (2579621)Time elapsed: 0.295 s
% 117.15/17.96 % (2579621)Peak memory usage: 90 MB
% 117.15/17.96 % (2579621)Instructions burned: 413 (million)
% 117.15/17.96 % (2579623)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=2137958262:s2pl=no:i=8478:s2at=4:nm=6_2949 on theBenchmark for (2949ds/8478Mi)
% 117.15/17.96 % (2579613)Instruction limit reached!
% 117.15/17.96 % (2579613)------------------------------
% 117.15/17.96 % (2579613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579613)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579613)Termination reason: Instruction limit
% 117.15/17.96 % (2579613)Termination phase: Saturation
% 117.15/17.96 % (2579613)Time elapsed: 3.161 s
% 117.15/17.96 % (2579613)Peak memory usage: 150 MB
% 117.15/17.96 % (2579613)Instructions burned: 3256 (million)
% 117.15/17.96 % (2579625)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=3269155615:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2936 on theBenchmark for (2936ds/303Mi)
% 117.15/17.96 % (2579625)Refutation not found, incomplete strategy
% 117.15/17.96 % (2579625)------------------------------
% 117.15/17.96 % (2579625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579625)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579625)Termination reason: Refutation not found, incomplete strategy
% 117.15/17.96 % (2579625)Time elapsed: 0.005 s
% 117.15/17.96 % (2579625)Peak memory usage: 88 MB
% 117.15/17.96 % (2579625)Instructions burned: 2 (million)
% 117.15/17.96 % (2579599)Instruction limit reached!
% 117.15/17.96 % (2579599)------------------------------
% 117.15/17.96 % (2579599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579599)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579599)Termination reason: Instruction limit
% 117.15/17.96 % (2579599)Termination phase: Saturation
% 117.15/17.96 % (2579599)Time elapsed: 5.220 s
% 117.15/17.96 % (2579599)Peak memory usage: 162 MB
% 117.15/17.96 % (2579599)Instructions burned: 5208 (million)
% 117.15/17.96 % (2579625)------------------------------
% 117.15/17.96 % (2579625)------------------------------
% 117.15/17.96 % (2579627)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1340492183:st=4:i=720:sd=3:fsr=off:ss=axioms_2931 on theBenchmark for (2931ds/720Mi)
% 117.15/17.96 % (2579627)Refutation not found, incomplete strategy
% 117.15/17.96 % (2579627)------------------------------
% 117.15/17.96 % (2579627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579627)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579627)Termination reason: Refutation not found, incomplete strategy
% 117.15/17.96 % (2579627)Time elapsed: 0.006 s
% 117.15/17.96 % (2579627)Peak memory usage: 88 MB
% 117.15/17.96 % (2579627)Instructions burned: 4 (million)
% 117.15/17.96 % (2579628)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1173656005:i=598:bs=on:bd=preordered:av=off:ss=axioms_2929 on theBenchmark for (2929ds/598Mi)
% 117.15/17.96 % (2579628)Refutation not found, incomplete strategy
% 117.15/17.96 % (2579628)------------------------------
% 117.15/17.96 % (2579628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579628)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579628)Termination reason: Refutation not found, incomplete strategy
% 117.15/17.96 % (2579628)Time elapsed: 0.006 s
% 117.15/17.96 % (2579628)Peak memory usage: 88 MB
% 117.15/17.96 % (2579628)Instructions burned: 4 (million)
% 117.15/17.96 % (2579627)------------------------------
% 117.15/17.96 % (2579627)------------------------------
% 117.15/17.96 % (2579628)------------------------------
% 117.15/17.96 % (2579628)------------------------------
% 117.15/17.96 % (2579631)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=839986337:i=2989:sd=3:ss=axioms:sgt=60_2925 on theBenchmark for (2925ds/2989Mi)
% 117.15/17.96 % (2579632)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=2405735714:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2922 on theBenchmark for (2922ds/1997Mi)
% 117.15/17.96 % (2579632)Instruction limit reached!
% 117.15/17.96 % (2579632)------------------------------
% 117.15/17.96 % (2579632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579632)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579632)Termination reason: Instruction limit
% 117.15/17.96 % (2579632)Termination phase: Saturation
% 117.15/17.96 % (2579632)Time elapsed: 2.149 s
% 117.15/17.96 % (2579632)Peak memory usage: 137 MB
% 117.15/17.96 % (2579632)Instructions burned: 1997 (million)
% 117.15/17.96 % (2579635)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=3750975514:i=2088:bd=preordered:av=off_2898 on theBenchmark for (2898ds/2088Mi)
% 117.15/17.96 % (2579631)Instruction limit reached!
% 117.15/17.96 % (2579631)------------------------------
% 117.15/17.96 % (2579631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579631)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579631)Termination reason: Instruction limit
% 117.15/17.96 % (2579631)Termination phase: Saturation
% 117.15/17.96 % (2579631)Time elapsed: 3.040 s
% 117.15/17.96 % (2579631)Peak memory usage: 143 MB
% 117.15/17.96 % (2579631)Instructions burned: 2989 (million)
% 117.15/17.96 % (2579637)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2865469152:i=1098:nicw=on_2891 on theBenchmark for (2891ds/1098Mi)
% 117.15/17.96 % (2579637)Instruction limit reached!
% 117.15/17.96 % (2579637)------------------------------
% 117.15/17.96 % (2579637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579637)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579637)Termination reason: Instruction limit
% 117.15/17.96 % (2579637)Termination phase: Saturation
% 117.15/17.96 % (2579637)Time elapsed: 1.032 s
% 117.15/17.96 % (2579637)Peak memory usage: 102 MB
% 117.15/17.96 % (2579637)Instructions burned: 1098 (million)
% 117.15/17.96 % (2579639)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=592352433:i=433:bd=preordered_2878 on theBenchmark for (2878ds/433Mi)
% 117.15/17.96 % (2579623)Instruction limit reached!
% 117.15/17.96 % (2579623)------------------------------
% 117.15/17.96 % (2579623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579623)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579623)Termination reason: Instruction limit
% 117.15/17.96 % (2579623)Termination phase: Saturation
% 117.15/17.96 % (2579623)Time elapsed: 7.188 s
% 117.15/17.96 % (2579623)Peak memory usage: 175 MB
% 117.15/17.96 % (2579623)Instructions burned: 8479 (million)
% 117.15/17.96 % (2579635)Instruction limit reached!
% 117.15/17.96 % (2579635)------------------------------
% 117.15/17.96 % (2579635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579635)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579635)Termination reason: Instruction limit
% 117.15/17.96 % (2579635)Termination phase: Saturation
% 117.15/17.96 % (2579635)Time elapsed: 2.145 s
% 117.15/17.96 % (2579635)Peak memory usage: 137 MB
% 117.15/17.96 % (2579635)Instructions burned: 2088 (million)
% 117.15/17.96 % (2579639)Instruction limit reached!
% 117.15/17.96 % (2579639)------------------------------
% 117.15/17.96 % (2579639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579639)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579639)Termination reason: Instruction limit
% 117.15/17.96 % (2579639)Termination phase: Saturation
% 117.15/17.96 % (2579639)Time elapsed: 0.389 s
% 117.15/17.96 % (2579639)Peak memory usage: 93 MB
% 117.15/17.96 % (2579639)Instructions burned: 434 (million)
% 117.15/17.96 % (2579641)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3909133865:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2874 on theBenchmark for (2874ds/2942Mi)
% 117.15/17.96 % (2579642)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=322333618:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2873 on theBenchmark for (2873ds/6922Mi)
% 117.15/17.96 % (2579643)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=856027596:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2872 on theBenchmark for (2872ds/596Mi)
% 117.15/17.96 % (2579643)Instruction limit reached!
% 117.15/17.96 % (2579643)------------------------------
% 117.15/17.96 % (2579643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579643)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579643)Termination reason: Instruction limit
% 117.15/17.96 % (2579643)Termination phase: Saturation
% 117.15/17.96 % (2579643)Time elapsed: 0.508 s
% 117.15/17.96 % (2579643)Peak memory usage: 99 MB
% 117.15/17.96 % (2579643)Instructions burned: 596 (million)
% 117.15/17.96 % (2579647)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=1439434408:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2864 on theBenchmark for (2864ds/4123Mi)
% 117.15/17.96 % (2579619)Instruction limit reached!
% 117.15/17.96 % (2579619)------------------------------
% 117.15/17.96 % (2579619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579619)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579619)Termination reason: Instruction limit
% 117.15/17.96 % (2579619)Termination phase: Saturation
% 117.15/17.96 % (2579619)Time elapsed: 10.925 s
% 117.15/17.96 % (2579619)Peak memory usage: 169 MB
% 117.15/17.96 % (2579619)Instructions burned: 10307 (million)
% 117.15/17.96 % (2579651)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=867362552:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2846 on theBenchmark for (2846ds/16411Mi)
% 117.15/17.96 % (2579641)Instruction limit reached!
% 117.15/17.96 % (2579641)------------------------------
% 117.15/17.96 % (2579641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.15/17.96 % (2579641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.15/17.96 % (2579641)CaDiCaL version: 2.1.3
% 117.15/17.96 % (2579641)Termination reason: Instruction limit
% 117.15/17.96 % (2579641)Termination phase: Saturation
% 117.15/17.96 % (2579641)Time elapsed: 2.885 s
% 117.15/17.96 % (2579641)Peak memory usage: 145 MB
% 117.15/17.96 % (2579641)Instructions burned: 2942 (million)
% 117.15/17.96 % (2579653)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3482902920:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2843 on theBenchmark for (2843ds/1670Mi)
% 117.15/17.96 % (2579647)First to succeed.
% 117.15/17.96 % (2579647)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2579560"
% 117.15/17.96 % (2579647)Refutation found. Thanks to Tanya!
% 117.15/17.96 % SZS status Unsatisfiable for theBenchmark
% 117.15/17.96 % SZS output start Proof for theBenchmark
% See solution above
% 121.13/18.34 % (2579647)------------------------------
% 121.13/18.34 % (2579647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.13/18.34 % (2579647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.13/18.34 % (2579647)CaDiCaL version: 2.1.3
% 121.13/18.34 % (2579647)Termination reason: Refutation
% 121.13/18.34 % (2579647)Time elapsed: 2.771 s
% 121.13/18.34 % (2579647)Peak memory usage: 149 MB
% 121.13/18.34 % (2579647)Instructions burned: 2794 (million)
% 121.13/18.34 % (2579647)------------------------------
% 121.13/18.34 % (2579647)------------------------------
% 121.13/18.34 % (2579560)Success in time 17.092 s
% 121.13/18.34 % Vampire exiting
%------------------------------------------------------------------------------