%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU319+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 : n008.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 0.14s 6.30s
% Output : Refutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 8
% Syntax : Number of formulae : 57 ( 9 unt; 4 def)
% Number of atoms : 154 ( 6 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 163 ( 66 ~; 67 |; 12 &)
% ( 8 <=>; 9 =>; 0 <=; 1 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 5 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-3 aty)
% Number of variables : 29 ( 0 sgn 23 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f102,axiom,
! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ( closed_subset(X1,X0)
<=> open_subset(subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_pre_topc) ).
fof(f167,axiom,
! [X0] :
( top_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_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,conjecture,
! [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(f419,negated_conjecture,
~ ! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ( closed_subset(X1,X0)
<=> open_subset(subset_complement(the_carrier(X0),X1),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f418]) ).
fof(f673,plain,
! [X0] :
( ! [X1] :
( ( closed_subset(X1,X0)
<=> open_subset(subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1),X0) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f102]) ).
fof(f722,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f167]) ).
fof(f940,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(f992,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,[],[f419]) ).
fof(f1337,plain,
! [X0] :
( ! [X1] :
( ( ( closed_subset(X1,X0)
| ~ open_subset(subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1),X0) )
& ( open_subset(subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1),X0)
| ~ closed_subset(X1,X0) ) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(nnf_transformation,[],[f673]) ).
fof(f1643,plain,
? [X0] :
( ? [X1] :
( ( ~ open_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ closed_subset(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,[],[f992]) ).
fof(f1644,plain,
? [X0] :
( ? [X1] :
( ( ~ open_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ closed_subset(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(flattening,[],[f1643]) ).
fof(f1645,plain,
( ( ~ open_subset(subset_complement(the_carrier(sK373),sK374),sK373)
| ~ closed_subset(sK374,sK373) )
& ( open_subset(subset_complement(the_carrier(sK373),sK374),sK373)
| closed_subset(sK374,sK373) )
& element(sK374,powerset(the_carrier(sK373)))
& top_str(sK373) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK373,sK374]),skolemize(X0,sK373),skolemize(X1,sK374)],[f1644]) ).
fof(f2048,plain,
! [X0,X1] :
( open_subset(subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1),X0)
| ~ closed_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f1337]) ).
fof(f2049,plain,
! [X0,X1] :
( closed_subset(X1,X0)
| ~ open_subset(subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1),X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f1337]) ).
fof(f2134,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f722]) ).
fof(f2849,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,[],[f940]) ).
fof(f2905,plain,
top_str(sK373),
inference(cnf_transformation,[],[f1645]) ).
fof(f2906,plain,
element(sK374,powerset(the_carrier(sK373))),
inference(cnf_transformation,[],[f1645]) ).
fof(f2907,plain,
( open_subset(subset_complement(the_carrier(sK373),sK374),sK373)
| closed_subset(sK374,sK373) ),
inference(cnf_transformation,[],[f1645]) ).
fof(f2908,plain,
( ~ open_subset(subset_complement(the_carrier(sK373),sK374),sK373)
| ~ closed_subset(sK374,sK373) ),
inference(cnf_transformation,[],[f1645]) ).
fof(f3659,definition,
( spl394_1
<=> closed_subset(sK374,sK373) ),
introduced(definition,[new_symbols(definition,[spl394_1])],[avatar_definition]) ).
fof(f3662,definition,
( spl394_2
<=> open_subset(subset_complement(the_carrier(sK373),sK374),sK373) ),
introduced(definition,[new_symbols(definition,[spl394_2])],[avatar_definition]) ).
fof(f3663,plain,
( open_subset(subset_complement(the_carrier(sK373),sK374),sK373)
| ~ spl394_2 ),
inference(avatar_component_clause,[],[f3662]) ).
fof(f3664,plain,
( spl394_1
| spl394_2 ),
inference(avatar_split_clause,[],[f2907,f3662,f3659]) ).
fof(f3665,plain,
( ~ closed_subset(sK374,sK373)
| spl394_1 ),
inference(avatar_component_clause,[],[f3659]) ).
fof(f3667,plain,
( ~ spl394_1
| ~ spl394_2 ),
inference(avatar_split_clause,[],[f2908,f3662,f3659]) ).
fof(f15577,definition,
( spl394_361
<=> one_sorted_str(sK373) ),
introduced(definition,[new_symbols(definition,[spl394_361])],[avatar_definition]) ).
fof(f15578,plain,
( ~ one_sorted_str(sK373)
| spl394_361 ),
inference(avatar_component_clause,[],[f15577]) ).
fof(f15590,plain,
( ~ top_str(sK373)
| spl394_361 ),
inference(resolution,[],[f15578,f2134]) ).
fof(f15592,plain,
( $false
| spl394_361 ),
inference(forward_subsumption_resolution,[],[f15590,f2905]) ).
fof(f15593,plain,
spl394_361,
inference(avatar_contradiction_clause,[],[f15592]) ).
fof(f20734,plain,
( subset_complement(the_carrier(sK373),sK374) = subset_difference(the_carrier(sK373),cast_as_carrier_subset(sK373),sK374)
| ~ one_sorted_str(sK373) ),
inference(resolution,[],[f2849,f2906]) ).
fof(f20742,definition,
( spl394_474
<=> subset_complement(the_carrier(sK373),sK374) = subset_difference(the_carrier(sK373),cast_as_carrier_subset(sK373),sK374) ),
introduced(definition,[new_symbols(definition,[spl394_474])],[avatar_definition]) ).
fof(f20743,plain,
( subset_complement(the_carrier(sK373),sK374) = subset_difference(the_carrier(sK373),cast_as_carrier_subset(sK373),sK374)
| ~ spl394_474 ),
inference(avatar_component_clause,[],[f20742]) ).
fof(f20744,plain,
( ~ spl394_361
| spl394_474 ),
inference(avatar_split_clause,[],[f20734,f20742,f15577]) ).
fof(f21699,plain,
( ~ open_subset(subset_difference(the_carrier(sK373),cast_as_carrier_subset(sK373),sK374),sK373)
| ~ element(sK374,powerset(the_carrier(sK373)))
| ~ top_str(sK373)
| spl394_1 ),
inference(resolution,[],[f2049,f3665]) ).
fof(f21700,plain,
( ~ open_subset(subset_difference(the_carrier(sK373),cast_as_carrier_subset(sK373),sK374),sK373)
| ~ top_str(sK373)
| spl394_1 ),
inference(forward_subsumption_resolution,[],[f21699,f2906]) ).
fof(f21701,plain,
( ~ open_subset(subset_difference(the_carrier(sK373),cast_as_carrier_subset(sK373),sK374),sK373)
| spl394_1 ),
inference(forward_subsumption_resolution,[],[f21700,f2905]) ).
fof(f42248,plain,
( ~ open_subset(subset_complement(the_carrier(sK373),sK374),sK373)
| spl394_1
| ~ spl394_474 ),
inference(superposition,[],[f21701,f20743]) ).
fof(f42249,plain,
( open_subset(subset_complement(the_carrier(sK373),sK374),sK373)
| ~ closed_subset(sK374,sK373)
| ~ element(sK374,powerset(the_carrier(sK373)))
| ~ top_str(sK373)
| ~ spl394_474 ),
inference(superposition,[],[f2048,f20743]) ).
fof(f42251,plain,
( $false
| spl394_1
| ~ spl394_2
| ~ spl394_474 ),
inference(forward_subsumption_resolution,[],[f42248,f3663]) ).
fof(f42252,plain,
( spl394_1
| ~ spl394_2
| ~ spl394_474 ),
inference(avatar_contradiction_clause,[],[f42251]) ).
fof(f42253,plain,
( open_subset(subset_complement(the_carrier(sK373),sK374),sK373)
| ~ closed_subset(sK374,sK373)
| ~ top_str(sK373)
| ~ spl394_474 ),
inference(forward_subsumption_resolution,[],[f42249,f2906]) ).
fof(f42255,plain,
( open_subset(subset_complement(the_carrier(sK373),sK374),sK373)
| ~ closed_subset(sK374,sK373)
| ~ spl394_474 ),
inference(forward_subsumption_resolution,[],[f42253,f2905]) ).
fof(f42260,plain,
( ~ spl394_1
| spl394_2
| ~ spl394_474 ),
inference(avatar_split_clause,[],[f42255,f20742,f3662,f3659]) ).
cnf(s1,plain,
( spl394_1
| spl394_2 ),
inference(sat_conversion,[],[f3664]) ).
cnf(s2,plain,
( ~ spl394_1
| ~ spl394_2 ),
inference(sat_conversion,[],[f3667]) ).
cnf(s279,plain,
spl394_361,
inference(sat_conversion,[],[f15593]) ).
cnf(s358,plain,
( ~ spl394_361
| spl394_474 ),
inference(sat_conversion,[],[f20744]) ).
cnf(s856,plain,
( spl394_1
| ~ spl394_2
| ~ spl394_474 ),
inference(sat_conversion,[],[f42252]) ).
cnf(s858,plain,
( ~ spl394_1
| spl394_2
| ~ spl394_474 ),
inference(sat_conversion,[],[f42260]) ).
cnf(s862,plain,
spl394_474,
inference(rat,[],[s358,s279]) ).
cnf(s930,plain,
spl394_1,
inference(rat,[],[s1,s856,s862]) ).
cnf(s931,plain,
spl394_2,
inference(rat,[],[s858,s862,s930]) ).
cnf(s933,plain,
$false,
inference(rat,[],[s2,s931,s930]) ).
fof(f42261,plain,
$false,
inference(avatar_sat_refutation,[],[s933]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU319+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.09/0.37 % Computer : n008.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 28 04:41:40 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.40 Running first-order model finding
% 0.09/0.40 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.91/1.96 % (1880287)Will run a generic schedule for satisfiability detection.
% 8.91/1.96 % (1880292)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2094660965_2999 on theBenchmark for (2999ds/0Mi)
% 8.91/1.96 % (1880293)% WARNING: option uhcvi not known.
% 8.91/1.96 % (1880294)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2013857972:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.91/1.96 % (1880293)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=506187343:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.91/1.96 % (1880295)dis+10_1_sil=32000:sp=arity:random_seed=3592742843:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.91/1.96 % (1880296)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=71583666:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.91/1.96 % (1880298)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3502631707:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.91/1.96 % (1880297)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2421677033:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.91/1.96 % (1880296)Instruction limit reached!
% 8.91/1.96 % (1880296)------------------------------
% 8.91/1.96 % (1880296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.96 % (1880296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.96 % (1880296)CaDiCaL version: 2.1.3
% 8.91/1.96 % (1880296)Termination reason: Instruction limit
% 8.91/1.96 % (1880296)Termination phase: Blocked clause elimination
% 8.91/1.96 % (1880296)Time elapsed: 0.058 s
% 8.91/1.96 % (1880296)Peak memory usage: 13 MB
% 8.91/1.96 % (1880296)Instructions burned: 117 (million)
% 8.91/1.96 % (1880295)Instruction limit reached!
% 8.91/1.96 % (1880295)------------------------------
% 8.91/1.96 % (1880295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.96 % (1880295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.96 % (1880295)CaDiCaL version: 2.1.3
% 8.91/1.96 % (1880295)Termination reason: Instruction limit
% 8.91/1.96 % (1880295)Termination phase: Saturation
% 8.91/1.96 % (1880295)Time elapsed: 0.059 s
% 8.91/1.96 % (1880295)Peak memory usage: 14 MB
% 8.91/1.96 % (1880295)Instructions burned: 103 (million)
% 8.91/1.96 % (1880297)Instruction limit reached!
% 8.91/1.96 % (1880297)------------------------------
% 8.91/1.96 % (1880297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.96 % (1880297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.96 % (1880297)CaDiCaL version: 2.1.3
% 8.91/1.96 % (1880297)Termination reason: Instruction limit
% 8.91/1.96 % (1880297)Termination phase: Saturation
% 8.91/1.96 % (1880297)Time elapsed: 0.074 s
% 8.91/1.96 % (1880297)Peak memory usage: 15 MB
% 8.91/1.96 % (1880297)Instructions burned: 131 (million)
% 8.91/1.96 % TRYING [1]
% 8.91/1.96 % (1880306)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2695493409:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 8.91/1.96 % (1880307)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3123689309:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.91/1.96 % TRYING [2]
% 8.91/1.96 % (1880298)Instruction limit reached!
% 8.91/1.96 % (1880298)------------------------------
% 8.91/1.96 % (1880298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.96 % (1880298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.96 % (1880298)CaDiCaL version: 2.1.3
% 8.91/1.96 % (1880298)Termination reason: Instruction limit
% 8.91/1.96 % (1880298)Termination phase: Saturation
% 8.91/1.96 % (1880298)Time elapsed: 0.093 s
% 8.91/1.96 % (1880298)Peak memory usage: 16 MB
% 8.91/1.96 % (1880298)Instructions burned: 159 (million)
% 8.91/1.96 % (1880308)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=3176366501:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.91/1.96 % (1880311)ott-21_1_sil=16000:fs=off:random_seed=1733529842:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.91/1.96 % TRYING [3]
% 8.91/1.96 % (1880307)Instruction limit reached!
% 8.91/1.96 % (1880307)------------------------------
% 8.91/1.96 % (1880307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.96 % (1880307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.08 % (1880307)CaDiCaL version: 2.1.3
% 39.68/6.08 % (1880307)Termination reason: Instruction limit
% 39.68/6.08 % (1880307)Termination phase: Saturation
% 39.68/6.08 % (1880307)Time elapsed: 0.072 s
% 39.68/6.08 % (1880307)Peak memory usage: 15 MB
% 39.68/6.08 % (1880307)Instructions burned: 131 (million)
% 39.68/6.08 % (1880314)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1970416147:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 39.68/6.08 % TRYING [1]
% 39.68/6.08 % (1880311)Instruction limit reached!
% 39.68/6.08 % (1880311)------------------------------
% 39.68/6.08 % (1880311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.68/6.08 % (1880311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.08 % (1880311)CaDiCaL version: 2.1.3
% 39.68/6.08 % (1880311)Termination reason: Instruction limit
% 39.68/6.08 % (1880311)Termination phase: Saturation
% 39.68/6.08 % (1880311)Time elapsed: 0.097 s
% 39.68/6.08 % (1880311)Peak memory usage: 15 MB
% 39.68/6.08 % (1880311)Instructions burned: 181 (million)
% 39.68/6.08 % TRYING [2]
% 39.68/6.08 % (1880316)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2480724572:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 39.68/6.08 % TRYING [3]
% 39.68/6.08 % TRYING [1]
% 39.68/6.08 % TRYING [4]
% 39.68/6.08 % (1880306)Instruction limit reached!
% 39.68/6.08 % (1880306)------------------------------
% 39.68/6.08 % (1880306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.68/6.08 % (1880306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.08 % (1880306)CaDiCaL version: 2.1.3
% 39.68/6.08 % (1880306)Termination reason: Instruction limit
% 39.68/6.08 % (1880306)Termination phase: Finite model building constraint generation
% 39.68/6.08 % (1880306)Time elapsed: 0.296 s
% 39.68/6.08 % (1880306)Peak memory usage: 32 MB
% 39.68/6.08 % (1880306)Instructions burned: 715 (million)
% 39.68/6.08 % TRYING [2]
% 39.68/6.08 % (1880318)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2304606856:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 39.68/6.08 % (1880308)Instruction limit reached!
% 39.68/6.08 % (1880308)------------------------------
% 39.68/6.08 % (1880308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.68/6.08 % (1880308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.08 % (1880308)CaDiCaL version: 2.1.3
% 39.68/6.08 % (1880308)Termination reason: Instruction limit
% 39.68/6.08 % (1880308)Termination phase: Saturation
% 39.68/6.08 % (1880308)Time elapsed: 0.372 s
% 39.68/6.08 % (1880308)Peak memory usage: 23 MB
% 39.68/6.08 % (1880308)Instructions burned: 686 (million)
% 39.68/6.08 % (1880320)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3680641685:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 39.68/6.08 % (1880314)Instruction limit reached!
% 39.68/6.08 % (1880314)------------------------------
% 39.68/6.08 % (1880314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.68/6.08 % (1880314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.08 % (1880314)CaDiCaL version: 2.1.3
% 39.68/6.08 % (1880314)Termination reason: Instruction limit
% 39.68/6.08 % (1880314)Termination phase: Saturation
% 39.68/6.08 % (1880314)Time elapsed: 0.321 s
% 39.68/6.08 % (1880314)Peak memory usage: 16 MB
% 39.68/6.08 % (1880314)Instructions burned: 477 (million)
% 39.68/6.08 % (1880322)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=717649618: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)
% 39.68/6.08 % TRYING [3]
% 39.68/6.08 % (1880316)Instruction limit reached!
% 39.68/6.08 % (1880316)------------------------------
% 39.68/6.08 % (1880316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.68/6.08 % (1880316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.08 % (1880316)CaDiCaL version: 2.1.3
% 39.68/6.08 % (1880316)Termination reason: Instruction limit
% 39.68/6.08 % (1880316)Termination phase: Finite model building constraint generation
% 39.68/6.08 % (1880316)Time elapsed: 0.418 s
% 39.68/6.08 % (1880316)Peak memory usage: 35 MB
% 39.68/6.08 % (1880316)Instructions burned: 867 (million)
% 39.68/6.08 % (1880324)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2284745582:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 39.68/6.08 % (1880322)Instruction limit reached!
% 39.68/6.08 % (1880322)------------------------------
% 39.68/6.08 % (1880322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880322)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880322)Termination reason: Instruction limit
% 25.89/6.30 % (1880322)Termination phase: Saturation
% 25.89/6.30 % (1880322)Time elapsed: 0.387 s
% 25.89/6.30 % (1880322)Peak memory usage: 24 MB
% 25.89/6.30 % (1880322)Instructions burned: 694 (million)
% 25.89/6.30 % (1880320)Instruction limit reached!
% 25.89/6.30 % (1880320)------------------------------
% 25.89/6.30 % (1880320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880320)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880320)Termination reason: Instruction limit
% 25.89/6.30 % (1880320)Termination phase: Finite model building constraint generation
% 25.89/6.30 % (1880320)Time elapsed: 0.426 s
% 25.89/6.30 % (1880320)Peak memory usage: 89 MB
% 25.89/6.30 % (1880320)Instructions burned: 889 (million)
% 25.89/6.30 % (1880326)fmb+10_1_sil=64000:random_seed=3666683061:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 25.89/6.30 % (1880328)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3262223007:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 25.89/6.30 % TRYING [1]
% 25.89/6.30 % TRYING [2]
% 25.89/6.30 % (1880328)Cannot represent all propositional literals internally
% 25.89/6.30 % (1880328)Refutation not found, incomplete strategy
% 25.89/6.30 % (1880328)------------------------------
% 25.89/6.30 % (1880328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880328)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880328)Termination reason: Refutation not found, incomplete strategy
% 25.89/6.30 % (1880328)Time elapsed: 0.142 s
% 25.89/6.30 % (1880328)Peak memory usage: 17 MB
% 25.89/6.30 % (1880328)Instructions burned: 282 (million)
% 25.89/6.30 % (1880328)------------------------------
% 25.89/6.30 % (1880328)------------------------------
% 25.89/6.30 % (1880324)Instruction limit reached!
% 25.89/6.30 % (1880324)------------------------------
% 25.89/6.30 % (1880324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880324)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880324)Termination reason: Instruction limit
% 25.89/6.30 % (1880324)Termination phase: Saturation
% 25.89/6.30 % (1880324)Time elapsed: 0.433 s
% 25.89/6.30 % (1880324)Peak memory usage: 23 MB
% 25.89/6.30 % (1880324)Instructions burned: 879 (million)
% 25.89/6.30 % (1880330)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2444546317:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 25.89/6.30 % (1880331)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2133155593:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 25.89/6.30 % (1880318)Instruction limit reached!
% 25.89/6.30 % (1880318)------------------------------
% 25.89/6.30 % (1880318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880318)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880318)Termination reason: Instruction limit
% 25.89/6.30 % (1880318)Termination phase: Saturation
% 25.89/6.30 % (1880318)Time elapsed: 0.730 s
% 25.89/6.30 % (1880318)Peak memory usage: 30 MB
% 25.89/6.30 % (1880318)Instructions burned: 1179 (million)
% 25.89/6.30 % (1880334)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1204635108:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 25.89/6.30 % TRYING [3]
% 25.89/6.30 % TRYING [8]
% 25.89/6.30 % TRYING [5]
% 25.89/6.30 % (1880330)Instruction limit reached!
% 25.89/6.30 % (1880330)------------------------------
% 25.89/6.30 % (1880330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880330)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880330)Termination reason: Instruction limit
% 25.89/6.30 % (1880330)Termination phase: Finite model building constraint generation
% 25.89/6.30 % (1880330)Time elapsed: 0.358 s
% 25.89/6.30 % (1880330)Peak memory usage: 56 MB
% 25.89/6.30 % (1880330)Instructions burned: 922 (million)
% 25.89/6.30 % (1880336)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3270561859:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 25.89/6.30 % (1880336)Cannot represent all propositional literals internally
% 25.89/6.30 % (1880336)Refutation not found, incomplete strategy
% 25.89/6.30 % (1880336)------------------------------
% 25.89/6.30 % (1880336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880336)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880336)Termination reason: Refutation not found, incomplete strategy
% 25.89/6.30 % (1880336)Time elapsed: 0.159 s
% 25.89/6.30 % (1880336)Peak memory usage: 17 MB
% 25.89/6.30 % (1880336)Instructions burned: 320 (million)
% 25.89/6.30 % (1880336)------------------------------
% 25.89/6.30 % (1880336)------------------------------
% 25.89/6.30 % (1880338)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3753883273:fmbsr=2.30978:i=2174_2982 on theBenchmark for (2982ds/2174Mi)
% 25.89/6.30 % (1880334)Instruction limit reached!
% 25.89/6.30 % (1880334)------------------------------
% 25.89/6.30 % (1880334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880334)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880334)Termination reason: Instruction limit
% 25.89/6.30 % (1880334)Termination phase: Saturation
% 25.89/6.30 % (1880334)Time elapsed: 0.779 s
% 25.89/6.30 % (1880334)Peak memory usage: 29 MB
% 25.89/6.30 % (1880334)Instructions burned: 1473 (million)
% 25.89/6.30 % (1880340)ott-2_1_sil=16000:newcnf=on:random_seed=2584040222:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2980 on theBenchmark for (2980ds/869Mi)
% 25.89/6.30 % (1880340)Instruction limit reached!
% 25.89/6.30 % (1880340)------------------------------
% 25.89/6.30 % (1880340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880340)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880340)Termination reason: Instruction limit
% 25.89/6.30 % (1880340)Termination phase: Saturation
% 25.89/6.30 % (1880340)Time elapsed: 0.402 s
% 25.89/6.30 % (1880340)Peak memory usage: 17 MB
% 25.89/6.30 % (1880340)Instructions burned: 870 (million)
% 25.89/6.30 % (1880342)ott+10_1_sil=32000:tgt=ground:random_seed=3645840539:i=5114:av=off_2975 on theBenchmark for (2975ds/5114Mi)
% 25.89/6.30 % TRYING [4]
% 25.89/6.30 % (1880338)Cannot represent all propositional literals internally
% 25.89/6.30 % (1880338)Refutation not found, incomplete strategy
% 25.89/6.30 % (1880338)------------------------------
% 25.89/6.30 % (1880338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880338)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880338)Termination reason: Refutation not found, incomplete strategy
% 25.89/6.30 % (1880338)Time elapsed: 0.793 s
% 25.89/6.30 % (1880338)Peak memory usage: 32 MB
% 25.89/6.30 % (1880338)Instructions burned: 1634 (million)
% 25.89/6.30 % (1880338)------------------------------
% 25.89/6.30 % (1880338)------------------------------
% 25.89/6.30 % (1880344)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2796154258:i=54282_2974 on theBenchmark for (2974ds/54282Mi)
% 25.89/6.30 % TRYING [1]
% 25.89/6.30 % TRYING [2]
% 25.89/6.30 % TRYING [3]
% 25.89/6.30 % TRYING [4]
% 25.89/6.30 % (1880331)Instruction limit reached!
% 25.89/6.30 % (1880331)------------------------------
% 25.89/6.30 % (1880331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880331)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880331)Termination reason: Instruction limit
% 25.89/6.30 % (1880331)Termination phase: Saturation
% 25.89/6.30 % (1880331)Time elapsed: 3.036 s
% 25.89/6.30 % (1880331)Peak memory usage: 49 MB
% 25.89/6.30 % (1880331)Instructions burned: 5132 (million)
% 25.89/6.30 % (1880346)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3294240805:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 25.89/6.30 % TRYING [5]
% 25.89/6.30 % TRYING [6]
% 25.89/6.30 % (1880342)Instruction limit reached!
% 25.89/6.30 % (1880342)------------------------------
% 25.89/6.30 % (1880342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.89/6.30 % (1880342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.30 % (1880342)CaDiCaL version: 2.1.3
% 25.89/6.30 % (1880342)Termination reason: Instruction limit
% 25.89/6.30 % (1880342)Termination phase: Saturation
% 0.14/6.30 % (1880342)Time elapsed: 3.234 s
% 0.14/6.30 % (1880342)Peak memory usage: 69 MB
% 0.14/6.30 % (1880342)Instructions burned: 5115 (million)
% 0.14/6.30 % (1880348)dis+21_1_sil=32000:sas=cadical:random_seed=3662759178:i=3773:amm=off_2943 on theBenchmark for (2943ds/3773Mi)
% 0.14/6.30 % (1880346) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1880287-1880346"...
% 0.14/6.30 % (1880346)...printing done.
% 0.14/6.30 % (1880346)Refutation found. Thanks to Tanya!
% 0.14/6.30 % SZS status Theorem for theBenchmark
% 0.14/6.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.14/6.30 % (1880346)------------------------------
% 0.14/6.30 % (1880346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.14/6.30 % (1880346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.14/6.30 % (1880346)CaDiCaL version: 2.1.3
% 0.14/6.30 % (1880346)Termination reason: Refutation
% 0.14/6.30 % (1880346)Time elapsed: 1.497 s
% 0.14/6.30 % (1880346)Peak memory usage: 33 MB
% 0.14/6.30 % (1880346)Instructions burned: 2491 (million)
% 0.14/6.30 % (1880287)Success in time 5.884 s
% 0.14/6.30 % Vampire exiting
%------------------------------------------------------------------------------