%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU320+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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:52:51 PM UTC 2026
% Result : Theorem 38.10s 8.05s
% Output : Refutation 38.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 15
% Syntax : Number of formulae : 89 ( 18 unt; 5 def)
% Number of atoms : 210 ( 22 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 207 ( 86 ~; 85 |; 13 &)
% ( 9 <=>; 13 =>; 0 <=; 1 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 6 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 2 con; 0-3 aty)
% Number of variables : 61 ( 0 sgn 55 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f89,axiom,
! [X0] : cast_to_subset(X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_subset_1) ).
fof(f98,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,X1) = set_difference(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_subset_1) ).
fof(f138,axiom,
! [X0] : element(cast_to_subset(X0),powerset(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_subset_1) ).
fof(f161,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X0))
& element(X2,powerset(X0)) )
=> element(subset_difference(X0,X1,X2),powerset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_subset_1) ).
fof(f167,axiom,
! [X0] :
( top_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f247,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,subset_complement(X0,X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k3_subset_1) ).
fof(f356,axiom,
! [X0] :
( one_sorted_str(X0)
=> cast_as_carrier_subset(X0) = the_carrier(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f380,axiom,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t17_pre_topc) ).
fof(f418,axiom,
! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ( closed_subset(X1,X0)
<=> open_subset(subset_complement(the_carrier(X0),X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t29_tops_1) ).
fof(f425,conjecture,
! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ( open_subset(X1,X0)
<=> closed_subset(subset_complement(the_carrier(X0),X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_tops_1) ).
fof(f426,negated_conjecture,
~ ! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ( open_subset(X1,X0)
<=> closed_subset(subset_complement(the_carrier(X0),X1),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f425]) ).
fof(f672,plain,
! [X0,X1] :
( subset_complement(X0,X1) = set_difference(X0,X1)
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f98]) ).
fof(f717,plain,
! [X0,X1,X2] :
( element(subset_difference(X0,X1,X2),powerset(X0))
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(ennf_transformation,[],[f161]) ).
fof(f718,plain,
! [X0,X1,X2] :
( element(subset_difference(X0,X1,X2),powerset(X0))
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(flattening,[],[f717]) ).
fof(f723,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f167]) ).
fof(f794,plain,
! [X0,X1] :
( subset_complement(X0,subset_complement(X0,X1)) = X1
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f247]) ).
fof(f907,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f356]) ).
fof(f941,plain,
! [X0] :
( ! [X1] :
( subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1)
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f380]) ).
fof(f993,plain,
! [X0] :
( ! [X1] :
( ( closed_subset(X1,X0)
<=> open_subset(subset_complement(the_carrier(X0),X1),X0) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f418]) ).
fof(f999,plain,
? [X0] :
( ? [X1] :
( ( open_subset(X1,X0)
<~> closed_subset(subset_complement(the_carrier(X0),X1),X0) )
& element(X1,powerset(the_carrier(X0))) )
& top_str(X0) ),
inference(ennf_transformation,[],[f426]) ).
fof(f1645,plain,
! [X0] :
( ! [X1] :
( ( ( closed_subset(X1,X0)
| ~ open_subset(subset_complement(the_carrier(X0),X1),X0) )
& ( open_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ closed_subset(X1,X0) ) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(nnf_transformation,[],[f993]) ).
fof(f1648,plain,
? [X0] :
( ? [X1] :
( ( ~ closed_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ open_subset(X1,X0) )
& ( closed_subset(subset_complement(the_carrier(X0),X1),X0)
| open_subset(X1,X0) )
& element(X1,powerset(the_carrier(X0))) )
& top_str(X0) ),
inference(nnf_transformation,[],[f999]) ).
fof(f1649,plain,
? [X0] :
( ? [X1] :
( ( ~ closed_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ open_subset(X1,X0) )
& ( closed_subset(subset_complement(the_carrier(X0),X1),X0)
| open_subset(X1,X0) )
& element(X1,powerset(the_carrier(X0))) )
& top_str(X0) ),
inference(flattening,[],[f1648]) ).
fof(f1650,plain,
( ( ~ closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| ~ open_subset(sK375,sK374) )
& ( closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| open_subset(sK375,sK374) )
& element(sK375,powerset(the_carrier(sK374)))
& top_str(sK374) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK374,sK375]),skolemize(X0,sK374),skolemize(X1,sK375)],[f1649]) ).
fof(f1996,plain,
! [X0] : cast_to_subset(X0) = X0,
inference(cnf_transformation,[],[f89]) ).
fof(f2041,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| set_difference(X0,X1) = subset_complement(X0,X1) ),
inference(cnf_transformation,[],[f672]) ).
fof(f2120,plain,
! [X0] : element(cast_to_subset(X0),powerset(X0)),
inference(cnf_transformation,[],[f138]) ).
fof(f2132,plain,
! [X2,X0,X1] :
( element(subset_difference(X0,X1,X2),powerset(X0))
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[],[f718]) ).
fof(f2137,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f723]) ).
fof(f2295,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| subset_complement(X0,subset_complement(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f794]) ).
fof(f2816,plain,
! [X0] :
( ~ one_sorted_str(X0)
| the_carrier(X0) = cast_as_carrier_subset(X0) ),
inference(cnf_transformation,[],[f907]) ).
fof(f2852,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1) = subset_complement(the_carrier(X0),X1)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f941]) ).
fof(f2908,plain,
! [X0,X1] :
( open_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ closed_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f1645]) ).
fof(f2909,plain,
! [X0,X1] :
( ~ open_subset(subset_complement(the_carrier(X0),X1),X0)
| closed_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f1645]) ).
fof(f2918,plain,
top_str(sK374),
inference(cnf_transformation,[],[f1650]) ).
fof(f2919,plain,
element(sK375,powerset(the_carrier(sK374))),
inference(cnf_transformation,[],[f1650]) ).
fof(f2920,plain,
( closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| open_subset(sK375,sK374) ),
inference(cnf_transformation,[],[f1650]) ).
fof(f2921,plain,
( ~ closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| ~ open_subset(sK375,sK374) ),
inference(cnf_transformation,[],[f1650]) ).
fof(f3664,definition,
( spl394_1
<=> open_subset(sK375,sK374) ),
introduced(definition,[new_symbols(definition,[spl394_1])],[avatar_definition]) ).
fof(f3668,definition,
( spl394_2
<=> closed_subset(subset_complement(the_carrier(sK374),sK375),sK374) ),
introduced(definition,[new_symbols(definition,[spl394_2])],[avatar_definition]) ).
fof(f3669,plain,
( ~ closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| spl394_2 ),
inference(avatar_component_clause,[],[f3668]) ).
fof(f3670,plain,
( closed_subset(subset_complement(the_carrier(sK374),sK375),sK374)
| ~ spl394_2 ),
inference(avatar_component_clause,[],[f3668]) ).
fof(f3671,plain,
( spl394_1
| spl394_2 ),
inference(avatar_split_clause,[],[f2920,f3668,f3664]) ).
fof(f3672,plain,
( ~ spl394_1
| ~ spl394_2 ),
inference(avatar_split_clause,[],[f2921,f3668,f3664]) ).
fof(f3985,plain,
! [X0] : element(X0,powerset(X0)),
inference(forward_demodulation,[],[f2120,f1996]) ).
fof(f11895,plain,
subset_complement(the_carrier(sK374),sK375) = set_difference(the_carrier(sK374),sK375),
inference(resolution,[],[f2041,f2919]) ).
fof(f12240,plain,
sK375 = subset_complement(the_carrier(sK374),subset_complement(the_carrier(sK374),sK375)),
inference(resolution,[],[f2295,f2919]) ).
fof(f18512,definition,
( spl394_514
<=> one_sorted_str(sK374) ),
introduced(definition,[new_symbols(definition,[spl394_514])],[avatar_definition]) ).
fof(f18513,plain,
( one_sorted_str(sK374)
| ~ spl394_514 ),
inference(avatar_component_clause,[],[f18512]) ).
fof(f18514,plain,
( ~ one_sorted_str(sK374)
| spl394_514 ),
inference(avatar_component_clause,[],[f18512]) ).
fof(f18524,plain,
( ~ top_str(sK374)
| spl394_514 ),
inference(resolution,[],[f18514,f2137]) ).
fof(f18525,plain,
( $false
| spl394_514 ),
inference(forward_subsumption_resolution,[],[f18524,f2918]) ).
fof(f18526,plain,
spl394_514,
inference(avatar_contradiction_clause,[],[f18525]) ).
fof(f18586,plain,
( the_carrier(sK374) = cast_as_carrier_subset(sK374)
| ~ spl394_514 ),
inference(resolution,[],[f18513,f2816]) ).
fof(f25248,plain,
( subset_complement(the_carrier(sK374),sK375) = subset_difference(the_carrier(sK374),cast_as_carrier_subset(sK374),sK375)
| ~ one_sorted_str(sK374) ),
inference(resolution,[],[f2852,f2919]) ).
fof(f25252,plain,
( subset_complement(the_carrier(sK374),sK375) = subset_difference(the_carrier(sK374),cast_as_carrier_subset(sK374),sK375)
| ~ spl394_514 ),
inference(forward_subsumption_resolution,[],[f25248,f18513]) ).
fof(f25257,plain,
( subset_complement(the_carrier(sK374),sK375) = subset_difference(the_carrier(sK374),the_carrier(sK374),sK375)
| ~ spl394_514 ),
inference(forward_demodulation,[],[f25252,f18586]) ).
fof(f49637,plain,
( closed_subset(set_difference(the_carrier(sK374),sK375),sK374)
| ~ spl394_2 ),
inference(superposition,[],[f3670,f11895]) ).
fof(f49653,plain,
sK375 = subset_complement(the_carrier(sK374),set_difference(the_carrier(sK374),sK375)),
inference(forward_demodulation,[],[f12240,f11895]) ).
fof(f49715,plain,
( ~ open_subset(sK375,sK374)
| closed_subset(set_difference(the_carrier(sK374),sK375),sK374)
| ~ element(set_difference(the_carrier(sK374),sK375),powerset(the_carrier(sK374)))
| ~ top_str(sK374) ),
inference(superposition,[],[f2909,f49653]) ).
fof(f49716,plain,
( open_subset(sK375,sK374)
| ~ closed_subset(set_difference(the_carrier(sK374),sK375),sK374)
| ~ element(set_difference(the_carrier(sK374),sK375),powerset(the_carrier(sK374)))
| ~ top_str(sK374) ),
inference(superposition,[],[f2908,f49653]) ).
fof(f49723,definition,
( spl394_1332
<=> element(set_difference(the_carrier(sK374),sK375),powerset(the_carrier(sK374))) ),
introduced(definition,[new_symbols(definition,[spl394_1332])],[avatar_definition]) ).
fof(f49742,definition,
( spl394_1336
<=> closed_subset(set_difference(the_carrier(sK374),sK375),sK374) ),
introduced(definition,[new_symbols(definition,[spl394_1336])],[avatar_definition]) ).
fof(f49748,plain,
( set_difference(the_carrier(sK374),sK375) = subset_difference(the_carrier(sK374),the_carrier(sK374),sK375)
| ~ spl394_514 ),
inference(forward_demodulation,[],[f25257,f11895]) ).
fof(f49759,plain,
( element(set_difference(the_carrier(sK374),sK375),powerset(the_carrier(sK374)))
| ~ element(the_carrier(sK374),powerset(the_carrier(sK374)))
| ~ element(sK375,powerset(the_carrier(sK374)))
| ~ spl394_514 ),
inference(superposition,[],[f2132,f49748]) ).
fof(f49760,plain,
( element(set_difference(the_carrier(sK374),sK375),powerset(the_carrier(sK374)))
| ~ element(sK375,powerset(the_carrier(sK374)))
| ~ spl394_514 ),
inference(forward_subsumption_resolution,[],[f49759,f3985]) ).
fof(f49761,plain,
( element(set_difference(the_carrier(sK374),sK375),powerset(the_carrier(sK374)))
| ~ spl394_514 ),
inference(forward_subsumption_resolution,[],[f49760,f2919]) ).
fof(f49762,plain,
( spl394_1332
| ~ spl394_514 ),
inference(avatar_split_clause,[],[f49761,f18512,f49723]) ).
fof(f50582,plain,
( spl394_1336
| ~ spl394_2 ),
inference(avatar_split_clause,[],[f49637,f3668,f49742]) ).
fof(f50583,plain,
( ~ closed_subset(set_difference(the_carrier(sK374),sK375),sK374)
| spl394_2 ),
inference(forward_demodulation,[],[f3669,f11895]) ).
fof(f51555,plain,
( open_subset(sK375,sK374)
| ~ closed_subset(set_difference(the_carrier(sK374),sK375),sK374)
| ~ element(set_difference(the_carrier(sK374),sK375),powerset(the_carrier(sK374))) ),
inference(forward_subsumption_resolution,[],[f49716,f2918]) ).
fof(f51556,plain,
( ~ open_subset(sK375,sK374)
| closed_subset(set_difference(the_carrier(sK374),sK375),sK374)
| ~ element(set_difference(the_carrier(sK374),sK375),powerset(the_carrier(sK374))) ),
inference(forward_subsumption_resolution,[],[f49715,f2918]) ).
fof(f51557,plain,
( ~ spl394_1336
| spl394_2 ),
inference(avatar_split_clause,[],[f50583,f3668,f49742]) ).
fof(f51612,plain,
( ~ spl394_1332
| ~ spl394_1336
| spl394_1 ),
inference(avatar_split_clause,[],[f51555,f3664,f49742,f49723]) ).
fof(f51613,plain,
( ~ spl394_1332
| spl394_1336
| ~ spl394_1 ),
inference(avatar_split_clause,[],[f51556,f3664,f49742,f49723]) ).
cnf(s1,plain,
( spl394_1
| spl394_2 ),
inference(sat_conversion,[],[f3671]) ).
cnf(s2,plain,
( ~ spl394_1
| ~ spl394_2 ),
inference(sat_conversion,[],[f3672]) ).
cnf(s450,plain,
spl394_514,
inference(sat_conversion,[],[f18526]) ).
cnf(s1175,plain,
( ~ spl394_514
| spl394_1332 ),
inference(sat_conversion,[],[f49762]) ).
cnf(s1236,plain,
( ~ spl394_2
| spl394_1336 ),
inference(sat_conversion,[],[f50582]) ).
cnf(s1539,plain,
( spl394_2
| ~ spl394_1336 ),
inference(sat_conversion,[],[f51557]) ).
cnf(s1554,plain,
( spl394_1
| ~ spl394_1332
| ~ spl394_1336 ),
inference(sat_conversion,[],[f51612]) ).
cnf(s1555,plain,
( ~ spl394_1
| ~ spl394_1332
| spl394_1336 ),
inference(sat_conversion,[],[f51613]) ).
cnf(s1556,plain,
spl394_1332,
inference(rat,[],[s1175,s450]) ).
cnf(s1573,plain,
spl394_1,
inference(rat,[],[s1236,s1,s1554,s1556]) ).
cnf(s1574,plain,
spl394_1336,
inference(rat,[],[s1555,s1556,s1573]) ).
cnf(s1577,plain,
~ spl394_2,
inference(rat,[],[s2,s1573]) ).
cnf(s1578,plain,
$false,
inference(rat,[],[s1539,s1574,s1577]) ).
fof(f51614,plain,
$false,
inference(avatar_sat_refutation,[],[s1578]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU320+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 % Computer : n011.cluster.edu
% 0.12/0.41 % Model : x86_64 x86_64
% 0.12/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.41 % Memory : 8046.5625MB
% 0.12/0.41 % OS : Linux 6.8.0-71-generic
% 0.12/0.41 % CPULimit : 300
% 0.12/0.41 % WCLimit : 300
% 0.12/0.41 % DateTime : Mon Sep 28 04:40:46 UTC 2026
% 0.12/0.41 % CPUTime :
% 0.12/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.44 Running first-order model finding
% 0.12/0.44 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.85/1.99 % (3020839)Will run a generic schedule for satisfiability detection.
% 8.85/1.99 % (3020846)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=75057078:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.85/1.99 % (3020845)% WARNING: option uhcvi not known.
% 8.85/1.99 % (3020844)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2681069162_2999 on theBenchmark for (2999ds/0Mi)
% 8.85/1.99 % (3020845)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2107488348:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.85/1.99 % (3020847)dis+10_1_sil=32000:sp=arity:random_seed=297559138:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.85/1.99 % (3020848)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=740825188:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.85/1.99 % (3020849)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=720359963:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.85/1.99 % (3020850)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1041868308:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.85/1.99 % (3020848)Instruction limit reached!
% 8.85/1.99 % (3020848)------------------------------
% 8.85/1.99 % (3020848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.85/1.99 % (3020848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.85/1.99 % (3020848)CaDiCaL version: 2.1.3
% 8.85/1.99 % (3020848)Termination reason: Instruction limit
% 8.85/1.99 % (3020848)Termination phase: Blocked clause elimination
% 8.85/1.99 % (3020848)Time elapsed: 0.059 s
% 8.85/1.99 % (3020848)Peak memory usage: 13 MB
% 8.85/1.99 % (3020848)Instructions burned: 117 (million)
% 8.85/1.99 % (3020847)Instruction limit reached!
% 8.85/1.99 % (3020847)------------------------------
% 8.85/1.99 % (3020847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.85/1.99 % (3020847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.85/1.99 % (3020847)CaDiCaL version: 2.1.3
% 8.85/1.99 % (3020847)Termination reason: Instruction limit
% 8.85/1.99 % (3020847)Termination phase: Saturation
% 8.85/1.99 % (3020847)Time elapsed: 0.061 s
% 8.85/1.99 % (3020847)Peak memory usage: 14 MB
% 8.85/1.99 % (3020847)Instructions burned: 104 (million)
% 8.85/1.99 % (3020849)Instruction limit reached!
% 8.85/1.99 % (3020849)------------------------------
% 8.85/1.99 % (3020849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.85/1.99 % (3020849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.85/1.99 % (3020849)CaDiCaL version: 2.1.3
% 8.85/1.99 % (3020849)Termination reason: Instruction limit
% 8.85/1.99 % (3020849)Termination phase: Saturation
% 8.85/1.99 % (3020849)Time elapsed: 0.076 s
% 8.85/1.99 % (3020849)Peak memory usage: 15 MB
% 8.85/1.99 % (3020849)Instructions burned: 133 (million)
% 8.85/1.99 % (3020858)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=680035757:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 8.85/1.99 % (3020859)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2816484764:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.85/1.99 % (3020850)Instruction limit reached!
% 8.85/1.99 % (3020850)------------------------------
% 8.85/1.99 % (3020850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.85/1.99 % (3020850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.85/1.99 % (3020850)CaDiCaL version: 2.1.3
% 8.85/1.99 % (3020850)Termination reason: Instruction limit
% 8.85/1.99 % (3020850)Termination phase: Saturation
% 8.85/1.99 % (3020850)Time elapsed: 0.094 s
% 8.85/1.99 % (3020850)Peak memory usage: 16 MB
% 8.85/1.99 % (3020850)Instructions burned: 159 (million)
% 8.85/1.99 % (3020860)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=246167621:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.85/1.99 % (3020863)ott-21_1_sil=16000:fs=off:random_seed=2907426421:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.85/1.99 % (3020859)Instruction limit reached!
% 8.85/1.99 % (3020859)------------------------------
% 8.85/1.99 % (3020859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.85/1.99 % (3020859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/6.16 % (3020859)CaDiCaL version: 2.1.3
% 40.22/6.16 % (3020859)Termination reason: Instruction limit
% 40.22/6.16 % (3020859)Termination phase: Saturation
% 40.22/6.16 % (3020859)Time elapsed: 0.073 s
% 40.22/6.16 % (3020859)Peak memory usage: 15 MB
% 40.22/6.16 % (3020859)Instructions burned: 131 (million)
% 40.22/6.16 % TRYING [1]
% 40.22/6.16 % TRYING [2]
% 40.22/6.16 % (3020866)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2669717918:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 40.22/6.16 % TRYING [1]
% 40.22/6.16 % (3020863)Instruction limit reached!
% 40.22/6.16 % (3020863)------------------------------
% 40.22/6.16 % (3020863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/6.16 % (3020863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/6.16 % (3020863)CaDiCaL version: 2.1.3
% 40.22/6.16 % (3020863)Termination reason: Instruction limit
% 40.22/6.16 % (3020863)Termination phase: Saturation
% 40.22/6.16 % (3020863)Time elapsed: 0.098 s
% 40.22/6.16 % (3020863)Peak memory usage: 15 MB
% 40.22/6.16 % (3020863)Instructions burned: 181 (million)
% 40.22/6.16 % TRYING [2]
% 40.22/6.16 % (3020868)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1392319859:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 40.22/6.16 % TRYING [3]
% 40.22/6.16 % TRYING [3]
% 40.22/6.16 % (3020858)Instruction limit reached!
% 40.22/6.16 % (3020858)------------------------------
% 40.22/6.16 % (3020858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/6.16 % (3020858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/6.16 % (3020858)CaDiCaL version: 2.1.3
% 40.22/6.16 % (3020858)Termination reason: Instruction limit
% 40.22/6.16 % (3020858)Termination phase: Finite model building constraint generation
% 40.22/6.16 % (3020858)Time elapsed: 0.293 s
% 40.22/6.16 % (3020858)Peak memory usage: 32 MB
% 40.22/6.16 % (3020858)Instructions burned: 717 (million)
% 40.22/6.16 % TRYING [1]
% 40.22/6.16 % (3020870)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=61716209:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 40.22/6.16 % TRYING [2]
% 40.22/6.16 % (3020860)Instruction limit reached!
% 40.22/6.16 % (3020860)------------------------------
% 40.22/6.16 % (3020860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/6.16 % (3020860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/6.16 % (3020860)CaDiCaL version: 2.1.3
% 40.22/6.16 % (3020860)Termination reason: Instruction limit
% 40.22/6.16 % (3020860)Termination phase: Saturation
% 40.22/6.16 % (3020860)Time elapsed: 0.352 s
% 40.22/6.16 % (3020860)Peak memory usage: 21 MB
% 40.22/6.16 % (3020860)Instructions burned: 686 (million)
% 40.22/6.16 % (3020872)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1180300990:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 40.22/6.16 % (3020866)Instruction limit reached!
% 40.22/6.16 % (3020866)------------------------------
% 40.22/6.16 % (3020866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/6.16 % (3020866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/6.16 % (3020866)CaDiCaL version: 2.1.3
% 40.22/6.16 % (3020866)Termination reason: Instruction limit
% 40.22/6.16 % (3020866)Termination phase: Saturation
% 40.22/6.16 % (3020866)Time elapsed: 0.325 s
% 40.22/6.16 % (3020866)Peak memory usage: 16 MB
% 40.22/6.16 % (3020866)Instructions burned: 478 (million)
% 40.22/6.16 % (3020874)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2205597556:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 40.22/6.16 % TRYING [3]
% 40.22/6.16 % (3020868)Instruction limit reached!
% 40.22/6.16 % (3020868)------------------------------
% 40.22/6.16 % (3020868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.22/6.16 % (3020868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.22/6.16 % (3020868)CaDiCaL version: 2.1.3
% 40.22/6.16 % (3020868)Termination reason: Instruction limit
% 40.22/6.16 % (3020868)Termination phase: Finite model building constraint generation
% 40.22/6.16 % (3020868)Time elapsed: 0.415 s
% 40.22/6.16 % (3020868)Peak memory usage: 35 MB
% 40.22/6.16 % (3020868)Instructions burned: 867 (million)
% 40.22/6.16 % (3020876)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2075671746:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 40.22/6.16 % TRYING [4]
% 40.22/6.16 % (3020872)Instruction limit reached!
% 40.22/6.16 % (3020872)------------------------------
% 40.22/6.16 % (3020872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.04 % (3020872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.04 % (3020872)CaDiCaL version: 2.1.3
% 38.10/8.04 % (3020872)Termination reason: Instruction limit
% 38.10/8.04 % (3020872)Termination phase: Finite model building constraint generation
% 38.10/8.04 % (3020872)Time elapsed: 0.423 s
% 38.10/8.04 % (3020872)Peak memory usage: 85 MB
% 38.10/8.04 % (3020872)Instructions burned: 891 (million)
% 38.10/8.04 % (3020878)fmb+10_1_sil=64000:random_seed=3227907763:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 38.10/8.04 % (3020874)Instruction limit reached!
% 38.10/8.04 % (3020874)------------------------------
% 38.10/8.04 % (3020874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.04 % (3020874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.04 % (3020874)CaDiCaL version: 2.1.3
% 38.10/8.04 % (3020874)Termination reason: Instruction limit
% 38.10/8.04 % (3020874)Termination phase: Saturation
% 38.10/8.04 % (3020874)Time elapsed: 0.409 s
% 38.10/8.04 % (3020874)Peak memory usage: 24 MB
% 38.10/8.04 % (3020874)Instructions burned: 693 (million)
% 38.10/8.04 % (3020880)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1425987589:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 38.10/8.04 % TRYING [1]
% 38.10/8.04 % TRYING [2]
% 38.10/8.04 % (3020880)Cannot represent all propositional literals internally
% 38.10/8.04 % (3020880)Refutation not found, incomplete strategy
% 38.10/8.04 % (3020880)------------------------------
% 38.10/8.04 % (3020880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.04 % (3020880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.04 % (3020880)CaDiCaL version: 2.1.3
% 38.10/8.04 % (3020880)Termination reason: Refutation not found, incomplete strategy
% 38.10/8.04 % (3020880)Time elapsed: 0.140 s
% 38.10/8.04 % (3020880)Peak memory usage: 17 MB
% 38.10/8.04 % (3020880)Instructions burned: 283 (million)
% 38.10/8.04 % (3020880)------------------------------
% 38.10/8.04 % (3020880)------------------------------
% 38.10/8.04 % (3020876)Instruction limit reached!
% 38.10/8.04 % (3020876)------------------------------
% 38.10/8.04 % (3020876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.05 % (3020876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.05 % (3020876)CaDiCaL version: 2.1.3
% 38.10/8.05 % (3020876)Termination reason: Instruction limit
% 38.10/8.05 % (3020876)Termination phase: Saturation
% 38.10/8.05 % (3020876)Time elapsed: 0.428 s
% 38.10/8.05 % (3020876)Peak memory usage: 23 MB
% 38.10/8.05 % (3020876)Instructions burned: 880 (million)
% 38.10/8.05 % (3020882)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2471250967:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 38.10/8.05 % (3020883)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4074215654:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 38.10/8.05 % (3020870)Instruction limit reached!
% 38.10/8.05 % (3020870)------------------------------
% 38.10/8.05 % (3020870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.05 % (3020870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.05 % (3020870)CaDiCaL version: 2.1.3
% 38.10/8.05 % (3020870)Termination reason: Instruction limit
% 38.10/8.05 % (3020870)Termination phase: Saturation
% 38.10/8.05 % (3020870)Time elapsed: 0.737 s
% 38.10/8.05 % (3020870)Peak memory usage: 30 MB
% 38.10/8.05 % (3020870)Instructions burned: 1179 (million)
% 38.10/8.05 % (3020886)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1768737854:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 38.10/8.05 % TRYING [3]
% 38.10/8.05 % TRYING [8]
% 38.10/8.05 % (3020882)Instruction limit reached!
% 38.10/8.05 % (3020882)------------------------------
% 38.10/8.05 % (3020882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.05 % (3020882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.05 % (3020882)CaDiCaL version: 2.1.3
% 38.10/8.05 % (3020882)Termination reason: Instruction limit
% 38.10/8.05 % (3020882)Termination phase: Finite model building constraint generation
% 38.10/8.05 % (3020882)Time elapsed: 0.359 s
% 38.10/8.05 % (3020882)Peak memory usage: 56 MB
% 38.10/8.05 % (3020882)Instructions burned: 921 (million)
% 38.10/8.05 % (3020888)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1687910623:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 38.10/8.05 % (3020888)Cannot represent all propositional literals internally
% 38.10/8.05 % (3020888)Refutation not found, incomplete strategy
% 38.10/8.05 % (3020888)------------------------------
% 38.10/8.05 % (3020888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.05 % (3020888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.05 % (3020888)CaDiCaL version: 2.1.3
% 38.10/8.05 % (3020888)Termination reason: Refutation not found, incomplete strategy
% 38.10/8.05 % (3020888)Time elapsed: 0.160 s
% 38.10/8.05 % (3020888)Peak memory usage: 17 MB
% 38.10/8.05 % (3020888)Instructions burned: 321 (million)
% 38.10/8.05 % (3020888)------------------------------
% 38.10/8.05 % (3020888)------------------------------
% 38.10/8.05 % (3020890)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=16195696:fmbsr=2.30978:i=2174_2982 on theBenchmark for (2982ds/2174Mi)
% 38.10/8.05 % (3020886)Instruction limit reached!
% 38.10/8.05 % (3020886)------------------------------
% 38.10/8.05 % (3020886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.05 % (3020886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.05 % (3020886)CaDiCaL version: 2.1.3
% 38.10/8.05 % (3020886)Termination reason: Instruction limit
% 38.10/8.05 % (3020886)Termination phase: Saturation
% 38.10/8.05 % (3020886)Time elapsed: 0.792 s
% 38.10/8.05 % (3020886)Peak memory usage: 29 MB
% 38.10/8.05 % (3020886)Instructions burned: 1472 (million)
% 38.10/8.05 % (3020892)ott-2_1_sil=16000:newcnf=on:random_seed=1701219258:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2979 on theBenchmark for (2979ds/869Mi)
% 38.10/8.05 % (3020892)Instruction limit reached!
% 38.10/8.05 % (3020892)------------------------------
% 38.10/8.05 % (3020892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.05 % (3020892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.05 % (3020892)CaDiCaL version: 2.1.3
% 38.10/8.05 % (3020892)Termination reason: Instruction limit
% 38.10/8.05 % (3020892)Termination phase: Saturation
% 38.10/8.05 % (3020892)Time elapsed: 0.410 s
% 38.10/8.05 % (3020892)Peak memory usage: 17 MB
% 38.10/8.05 % (3020892)Instructions burned: 869 (million)
% 38.10/8.05 % (3020895)ott+10_1_sil=32000:tgt=ground:random_seed=357613747:i=5114:av=off_2975 on theBenchmark for (2975ds/5114Mi)
% 38.10/8.05 % TRYING [4]
% 38.10/8.05 % (3020890)Cannot represent all propositional literals internally
% 38.10/8.05 % (3020890)Refutation not found, incomplete strategy
% 38.10/8.05 % (3020890)------------------------------
% 38.10/8.05 % (3020890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.05 % (3020890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.05 % (3020890)CaDiCaL version: 2.1.3
% 38.10/8.05 % (3020890)Termination reason: Refutation not found, incomplete strategy
% 38.10/8.05 % (3020890)Time elapsed: 0.803 s
% 38.10/8.05 % (3020890)Peak memory usage: 32 MB
% 38.10/8.05 % (3020890)Instructions burned: 1637 (million)
% 38.10/8.05 % (3020890)------------------------------
% 38.10/8.05 % (3020890)------------------------------
% 38.10/8.05 % (3020897)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=698079356:i=54282_2974 on theBenchmark for (2974ds/54282Mi)
% 38.10/8.05 % TRYING [1]
% 38.10/8.05 % TRYING [2]
% 38.10/8.05 % TRYING [3]
% 38.10/8.05 % TRYING [5]
% 38.10/8.05 % TRYING [4]
% 38.10/8.05 % (3020883)Instruction limit reached!
% 38.10/8.05 % (3020883)------------------------------
% 38.10/8.05 % (3020883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.05 % (3020883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.05 % (3020883)CaDiCaL version: 2.1.3
% 38.10/8.05 % (3020883)Termination reason: Instruction limit
% 38.10/8.05 % (3020883)Termination phase: Saturation
% 38.10/8.05 % (3020883)Time elapsed: 3.050 s
% 38.10/8.05 % (3020883)Peak memory usage: 49 MB
% 38.10/8.05 % (3020883)Instructions burned: 5131 (million)
% 38.10/8.05 % (3020899)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=623429267:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 38.10/8.05 % TRYING [5]
% 38.10/8.05 % (3020895)Instruction limit reached!
% 38.10/8.05 % (3020895)------------------------------
% 38.10/8.05 % (3020895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.05 % (3020895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.05 % (3020895)CaDiCaL version: 2.1.3
% 38.10/8.05 % (3020895)Termination reason: Instruction limit
% 38.10/8.05 % (3020895)Termination phase: Saturation
% 38.10/8.05 % (3020895)Time elapsed: 3.261 s
% 38.10/8.05 % (3020895)Peak memory usage: 69 MB
% 38.10/8.05 % (3020895)Instructions burned: 5115 (million)
% 38.10/8.05 % (3020901)dis+21_1_sil=32000:sas=cadical:random_seed=2572051119:i=3773:amm=off_2942 on theBenchmark for (2942ds/3773Mi)
% 38.10/8.05 % (3020899)Instruction limit reached!
% 38.10/8.05 % (3020899)------------------------------
% 38.10/8.05 % (3020899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.05 % (3020899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.05 % (3020899)CaDiCaL version: 2.1.3
% 38.10/8.05 % (3020899)Termination reason: Instruction limit
% 38.10/8.05 % (3020899)Termination phase: Saturation
% 38.10/8.05 % (3020899)Time elapsed: 2.175 s
% 38.10/8.05 % (3020899)Peak memory usage: 41 MB
% 38.10/8.05 % (3020899)Instructions burned: 3512 (million)
% 38.10/8.05 % (3020903)ott+11_1_sil=16000:gs=on:random_seed=850616371:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi)
% 38.10/8.05 % (3020901) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3020839-3020901"...
% 38.10/8.05 % (3020901)...printing done.
% 38.10/8.05 % (3020901)Refutation found. Thanks to Tanya!
% 38.10/8.05 % SZS status Theorem for theBenchmark
% 38.10/8.05 % SZS output start Proof for theBenchmark
% See solution above
% 38.10/8.05 % (3020901)------------------------------
% 38.10/8.05 % (3020901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.10/8.05 % (3020901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.10/8.05 % (3020901)CaDiCaL version: 2.1.3
% 38.10/8.05 % (3020901)Termination reason: Refutation
% 38.10/8.05 % (3020901)Time elapsed: 1.727 s
% 38.10/8.05 % (3020901)Peak memory usage: 39 MB
% 38.10/8.05 % (3020901)Instructions burned: 2875 (million)
% 38.10/8.05 % (3020839)Success in time 7.6 s
% 38.10/8.05 % Vampire exiting
%------------------------------------------------------------------------------