%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV631+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:59:35 PM UTC 2026
% Result : Theorem 179.77s 35.52s
% Output : Refutation 179.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 5
% Syntax : Number of formulae : 31 ( 12 unt; 2 def)
% Number of atoms : 84 ( 45 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 72 ( 19 ~; 14 |; 22 &)
% ( 2 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-4 aty)
% Number of variables : 88 ( 0 sgn 76 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f431,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( cHList_2ehlist_2eHcons___24a4(X0,X2,X4,X6) = cHList_2ehlist_2eHcons___24a4(X1,X3,X5,X7)
=> ( X6 = X7
& X4 = X5
& X2 = X3
& X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_inj_HList.hlist.Hcons') ).
fof(f2492,axiom,
! [X0,X1,X2,X3] : happ(happ(happ(happ(cHList_2ehlist_2eHcons,X0),X1),X2),X3) = cHList_2ehlist_2eHcons___24a4(X0,X1,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$adef_HList.hlist.Hcons_$a4') ).
fof(f3118,conjecture,
! [X0] :
( ciT___24t(X0)
=> ! [X1] :
( cCoq_2eInit_2eDatatypes_2elist___24t(ciT,X1)
=> ! [X2] :
( cF___24t(X0,X2)
=> ! [X3] :
( cHList_2ehlist_2ehlist___24t(X1,X3)
=> ! [X4] :
( cF___24t(X0,X4)
=> ! [X5] :
( cHList_2ehlist_2ehlist___24t(X1,X5)
=> ( cHList_2ehlist_2eHcons___24a4(X0,X1,X2,X3) = cHList_2ehlist_2eHcons___24a4(X0,X1,X4,X5)
=> ( X2 = X4
& X3 = X5 ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','_HAMMER_GOAL') ).
fof(f3119,negated_conjecture,
~ ! [X0] :
( ciT___24t(X0)
=> ! [X1] :
( cCoq_2eInit_2eDatatypes_2elist___24t(ciT,X1)
=> ! [X2] :
( cF___24t(X0,X2)
=> ! [X3] :
( cHList_2ehlist_2ehlist___24t(X1,X3)
=> ! [X4] :
( cF___24t(X0,X4)
=> ! [X5] :
( cHList_2ehlist_2ehlist___24t(X1,X5)
=> ( cHList_2ehlist_2eHcons___24a4(X0,X1,X2,X3) = cHList_2ehlist_2eHcons___24a4(X0,X1,X4,X5)
=> ( X2 = X4
& X3 = X5 ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3118]) ).
fof(f3676,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( X6 = X7
& X4 = X5
& X2 = X3
& X0 = X1 )
| cHList_2ehlist_2eHcons___24a4(X0,X2,X4,X6) != cHList_2ehlist_2eHcons___24a4(X1,X3,X5,X7) ),
inference(ennf_transformation,[],[f431]) ).
fof(f5328,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ( X2 != X4
| X3 != X5 )
& cHList_2ehlist_2eHcons___24a4(X0,X1,X2,X3) = cHList_2ehlist_2eHcons___24a4(X0,X1,X4,X5)
& cHList_2ehlist_2ehlist___24t(X1,X5) )
& cF___24t(X0,X4) )
& cHList_2ehlist_2ehlist___24t(X1,X3) )
& cF___24t(X0,X2) )
& cCoq_2eInit_2eDatatypes_2elist___24t(ciT,X1) )
& ciT___24t(X0) ),
inference(ennf_transformation,[],[f3119]) ).
fof(f5329,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ( X2 != X4
| X3 != X5 )
& cHList_2ehlist_2eHcons___24a4(X0,X1,X2,X3) = cHList_2ehlist_2eHcons___24a4(X0,X1,X4,X5)
& cHList_2ehlist_2ehlist___24t(X1,X5) )
& cF___24t(X0,X4) )
& cHList_2ehlist_2ehlist___24t(X1,X3) )
& cF___24t(X0,X2) )
& cCoq_2eInit_2eDatatypes_2elist___24t(ciT,X1) )
& ciT___24t(X0) ),
inference(flattening,[],[f5328]) ).
fof(f9392,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( cHList_2ehlist_2eHcons___24a4(X0,X2,X4,X6) != cHList_2ehlist_2eHcons___24a4(X1,X3,X5,X7)
| X4 = X5 ),
inference(cnf_transformation,[],[f3676]) ).
fof(f9393,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( cHList_2ehlist_2eHcons___24a4(X0,X2,X4,X6) != cHList_2ehlist_2eHcons___24a4(X1,X3,X5,X7)
| X6 = X7 ),
inference(cnf_transformation,[],[f3676]) ).
fof(f14640,plain,
! [X2,X3,X0,X1] : cHList_2ehlist_2eHcons___24a4(X0,X1,X2,X3) = happ(happ(happ(happ(cHList_2ehlist_2eHcons,X0),X1),X2),X3),
inference(cnf_transformation,[],[f2492]) ).
fof(f15772,plain,
( sK2444 != sK2446
| sK2443 != sK2445 ),
inference(cnf_transformation,[],[f5329]) ).
fof(f15774,plain,
cHList_2ehlist_2eHcons___24a4(sK2441,sK2442,sK2443,sK2444) = cHList_2ehlist_2eHcons___24a4(sK2441,sK2442,sK2445,sK2446),
inference(cnf_transformation,[],[f5329]) ).
fof(f19189,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( happ(happ(happ(happ(cHList_2ehlist_2eHcons,X0),X2),X4),X6) != happ(happ(happ(happ(cHList_2ehlist_2eHcons,X1),X3),X5),X7)
| X6 = X7 ),
inference(definition_unfolding,[],[f9393,f14640,f14640]) ).
fof(f19190,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( happ(happ(happ(happ(cHList_2ehlist_2eHcons,X0),X2),X4),X6) != happ(happ(happ(happ(cHList_2ehlist_2eHcons,X1),X3),X5),X7)
| X4 = X5 ),
inference(definition_unfolding,[],[f9392,f14640,f14640]) ).
fof(f20932,plain,
happ(happ(happ(happ(cHList_2ehlist_2eHcons,sK2441),sK2442),sK2443),sK2444) = happ(happ(happ(happ(cHList_2ehlist_2eHcons,sK2441),sK2442),sK2445),sK2446),
inference(definition_unfolding,[],[f15774,f14640,f14640]) ).
fof(f28245,definition,
( spl2447_1
<=> sK2443 = sK2445 ),
introduced(definition,[new_symbols(definition,[spl2447_1])],[avatar_definition]) ).
fof(f28247,plain,
( sK2443 != sK2445
| spl2447_1 ),
inference(avatar_component_clause,[],[f28245]) ).
fof(f28249,definition,
( spl2447_2
<=> sK2444 = sK2446 ),
introduced(definition,[new_symbols(definition,[spl2447_2])],[avatar_definition]) ).
fof(f28252,plain,
( ~ spl2447_1
| ~ spl2447_2 ),
inference(avatar_split_clause,[],[f15772,f28249,f28245]) ).
fof(f207370,plain,
! [X2,X3,X0,X1] :
( happ(happ(happ(happ(cHList_2ehlist_2eHcons,X0),X1),X2),X3) != happ(happ(happ(happ(cHList_2ehlist_2eHcons,sK2441),sK2442),sK2443),sK2444)
| sK2446 = X3 ),
inference(superposition,[],[f19189,f20932]) ).
fof(f207373,plain,
! [X2,X3,X0,X1] :
( happ(happ(happ(happ(cHList_2ehlist_2eHcons,X0),X1),X2),X3) != happ(happ(happ(happ(cHList_2ehlist_2eHcons,sK2441),sK2442),sK2443),sK2444)
| sK2445 = X2 ),
inference(superposition,[],[f19190,f20932]) ).
fof(f640051,plain,
sK2444 = sK2446,
inference(equality_resolution,[],[f207370]) ).
fof(f640073,plain,
spl2447_2,
inference(avatar_split_clause,[],[f640051,f28249]) ).
fof(f640654,plain,
sK2443 = sK2445,
inference(equality_resolution,[],[f207373]) ).
fof(f640655,plain,
( $false
| spl2447_1 ),
inference(forward_subsumption_resolution,[],[f640654,f28247]) ).
fof(f640656,plain,
spl2447_1,
inference(avatar_contradiction_clause,[],[f640655]) ).
cnf(s1,plain,
( ~ spl2447_1
| ~ spl2447_2 ),
inference(sat_conversion,[],[f28252]) ).
cnf(s35678,plain,
spl2447_2,
inference(sat_conversion,[],[f640073]) ).
cnf(s35713,plain,
spl2447_1,
inference(sat_conversion,[],[f640656]) ).
cnf(s35889,plain,
$false,
inference(rat,[],[s1,s35678,s35713]) ).
fof(f640665,plain,
$false,
inference(avatar_sat_refutation,[],[s35889]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV631+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n002.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 06:47:22 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.60/3.28 % (165100)Will run a generic schedule for satisfiability detection.
% 18.60/3.28 % (165109)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1930652176:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 18.60/3.28 % (165106)% WARNING: option uhcvi not known.
% 18.60/3.28 % (165105)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1870044945_2998 on theBenchmark for (2998ds/0Mi)
% 18.60/3.28 % (165106)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1442744065:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 18.60/3.28 % (165107)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3709110977:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 18.60/3.28 % (165108)dis+10_1_sil=32000:sp=arity:random_seed=2205198120:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 18.60/3.28 % (165110)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=808109734:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 18.60/3.28 % (165111)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4106724349:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 18.60/3.28 % (165109)Instruction limit reached!
% 18.60/3.28 % (165109)------------------------------
% 18.60/3.28 % (165109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.60/3.28 % (165109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.28 % (165109)CaDiCaL version: 2.1.3
% 18.60/3.28 % (165109)Termination reason: Instruction limit
% 18.60/3.28 % (165109)Termination phase: NewCNF
% 18.60/3.28 % (165109)Time elapsed: 0.042 s
% 18.60/3.28 % (165109)Peak memory usage: 21 MB
% 18.60/3.28 % (165109)Instructions burned: 119 (million)
% 18.60/3.28 % (165119)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1073298279:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 18.60/3.28 % (165108)Instruction limit reached!
% 18.60/3.28 % (165108)------------------------------
% 18.60/3.28 % (165108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.60/3.28 % (165108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.28 % (165108)CaDiCaL version: 2.1.3
% 18.60/3.28 % (165108)Termination reason: Instruction limit
% 18.60/3.28 % (165108)Termination phase: Preprocessing 3
% 18.60/3.28 % (165108)Time elapsed: 0.066 s
% 18.60/3.28 % (165108)Peak memory usage: 20 MB
% 18.60/3.28 % (165108)Instructions burned: 104 (million)
% 18.60/3.28 % (165110)Instruction limit reached!
% 18.60/3.28 % (165110)------------------------------
% 18.60/3.28 % (165110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.60/3.28 % (165110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.28 % (165110)CaDiCaL version: 2.1.3
% 18.60/3.28 % (165110)Termination reason: Instruction limit
% 18.60/3.28 % (165110)Termination phase: Preprocessing 3
% 18.60/3.28 % (165110)Time elapsed: 0.082 s
% 18.60/3.28 % (165110)Peak memory usage: 22 MB
% 18.60/3.28 % (165110)Instructions burned: 131 (million)
% 18.60/3.28 % (165121)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2373561485:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 18.60/3.28 % (165111)Instruction limit reached!
% 18.60/3.28 % (165111)------------------------------
% 18.60/3.28 % (165111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.60/3.28 % (165111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.28 % (165111)CaDiCaL version: 2.1.3
% 18.60/3.28 % (165111)Termination reason: Instruction limit
% 18.60/3.28 % (165111)Termination phase: Preprocessing 3
% 18.60/3.28 % (165111)Time elapsed: 0.098 s
% 18.60/3.28 % (165111)Peak memory usage: 23 MB
% 18.60/3.28 % (165111)Instructions burned: 160 (million)
% 18.60/3.28 % (165122)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=3701482771:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 18.60/3.28 % (165124)ott-21_1_sil=16000:fs=off:random_seed=291965589:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 18.60/3.28 % (165121)Instruction limit reached!
% 18.60/3.28 % (165121)------------------------------
% 18.60/3.28 % (165121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.60/3.28 % (165121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.28 % (165121)CaDiCaL version: 2.1.3
% 18.60/3.28 % (165121)Termination reason: Instruction limit
% 26.98/4.45 % (165121)Termination phase: Preprocessing 3
% 26.98/4.45 % (165121)Time elapsed: 0.082 s
% 26.98/4.45 % (165121)Peak memory usage: 22 MB
% 26.98/4.45 % (165121)Instructions burned: 131 (million)
% 26.98/4.45 % (165127)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=286462314:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 26.98/4.45 % (165124)Instruction limit reached!
% 26.98/4.45 % (165124)------------------------------
% 26.98/4.45 % (165124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.98/4.45 % (165124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.98/4.45 % (165124)CaDiCaL version: 2.1.3
% 26.98/4.45 % (165124)Termination reason: Instruction limit
% 26.98/4.45 % (165124)Termination phase: Clausification
% 26.98/4.45 % (165124)Time elapsed: 0.107 s
% 26.98/4.45 % (165124)Peak memory usage: 24 MB
% 26.98/4.45 % (165124)Instructions burned: 180 (million)
% 26.98/4.45 % (165119)Instruction limit reached!
% 26.98/4.45 % (165119)------------------------------
% 26.98/4.45 % (165119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.98/4.45 % (165119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.98/4.45 % (165119)CaDiCaL version: 2.1.3
% 26.98/4.45 % (165119)Termination reason: Instruction limit
% 26.98/4.45 % (165119)Termination phase: Finite model building preprocessing
% 26.98/4.45 % (165119)Time elapsed: 0.187 s
% 26.98/4.45 % (165119)Peak memory usage: 32 MB
% 26.98/4.45 % (165119)Instructions burned: 719 (million)
% 26.98/4.45 % (165130)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=587029782:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 26.98/4.45 % (165129)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4028986385:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 26.98/4.45 % (165122)Instruction limit reached!
% 26.98/4.45 % (165122)------------------------------
% 26.98/4.45 % (165122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.98/4.45 % (165122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.98/4.45 % (165122)CaDiCaL version: 2.1.3
% 26.98/4.45 % (165122)Termination reason: Instruction limit
% 26.98/4.45 % (165122)Termination phase: Property scanning
% 26.98/4.45 % (165122)Time elapsed: 0.300 s
% 26.98/4.45 % (165122)Peak memory usage: 26 MB
% 26.98/4.45 % (165122)Instructions burned: 687 (million)
% 26.98/4.45 % (165127)Instruction limit reached!
% 26.98/4.45 % (165127)------------------------------
% 26.98/4.45 % (165127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.98/4.45 % (165127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.98/4.45 % (165127)CaDiCaL version: 2.1.3
% 26.98/4.45 % (165127)Termination reason: Instruction limit
% 26.98/4.45 % (165127)Termination phase: Property scanning
% 26.98/4.45 % (165127)Time elapsed: 0.231 s
% 26.98/4.45 % (165127)Peak memory usage: 26 MB
% 26.98/4.45 % (165127)Instructions burned: 480 (million)
% 26.98/4.45 % (165133)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3988780345:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 26.98/4.45 % (165135)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=482797667:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 26.98/4.45 % (165130)Instruction limit reached!
% 26.98/4.45 % (165130)------------------------------
% 26.98/4.45 % (165130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.98/4.45 % (165130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.98/4.45 % (165130)CaDiCaL version: 2.1.3
% 26.98/4.45 % (165130)Termination reason: Instruction limit
% 26.98/4.45 % (165130)Termination phase: Saturation
% 26.98/4.45 % (165130)Time elapsed: 0.329 s
% 26.98/4.45 % (165130)Peak memory usage: 37 MB
% 26.98/4.45 % (165130)Instructions burned: 1179 (million)
% 26.98/4.45 % (165137)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4172732756:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 26.98/4.45 % (165129)Instruction limit reached!
% 26.98/4.45 % (165129)------------------------------
% 26.98/4.45 % (165129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.98/4.45 % (165129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.98/4.45 % (165129)CaDiCaL version: 2.1.3
% 26.98/4.45 % (165129)Termination reason: Instruction limit
% 26.98/4.45 % (165129)Termination phase: Finite model building preprocessing
% 41.11/6.42 % (165129)Time elapsed: 0.426 s
% 41.11/6.42 % (165129)Peak memory usage: 32 MB
% 41.11/6.42 % (165129)Instructions burned: 866 (million)
% 41.11/6.42 % (165139)fmb+10_1_sil=64000:random_seed=2642958106:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 41.11/6.42 % (165135)Instruction limit reached!
% 41.11/6.42 % (165135)------------------------------
% 41.11/6.42 % (165135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.11/6.42 % (165135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.11/6.42 % (165135)CaDiCaL version: 2.1.3
% 41.11/6.42 % (165135)Termination reason: Instruction limit
% 41.11/6.42 % (165135)Termination phase: Saturation
% 41.11/6.42 % (165135)Time elapsed: 0.308 s
% 41.11/6.42 % (165135)Peak memory usage: 29 MB
% 41.11/6.42 % (165135)Instructions burned: 692 (million)
% 41.11/6.42 % (165141)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1507495388:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 41.11/6.42 % (165137)Instruction limit reached!
% 41.11/6.42 % (165137)------------------------------
% 41.11/6.42 % (165137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.11/6.42 % (165137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.11/6.42 % (165137)CaDiCaL version: 2.1.3
% 41.11/6.42 % (165137)Termination reason: Instruction limit
% 41.11/6.42 % (165137)Termination phase: Saturation
% 41.11/6.42 % (165137)Time elapsed: 0.207 s
% 41.11/6.42 % (165137)Peak memory usage: 31 MB
% 41.11/6.42 % (165137)Instructions burned: 881 (million)
% 41.11/6.42 % (165143)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2618945052:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 41.11/6.42 % (165133)Instruction limit reached!
% 41.11/6.42 % (165133)------------------------------
% 41.11/6.42 % (165133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.11/6.42 % (165133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.11/6.42 % (165133)CaDiCaL version: 2.1.3
% 41.11/6.42 % (165133)Termination reason: Instruction limit
% 41.11/6.42 % (165133)Termination phase: Finite model building preprocessing
% 41.11/6.42 % (165133)Time elapsed: 0.433 s
% 41.11/6.42 % (165133)Peak memory usage: 32 MB
% 41.11/6.42 % (165133)Instructions burned: 890 (million)
% 41.11/6.42 % (165145)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2462067625:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 41.11/6.42 % (165143)Instruction limit reached!
% 41.11/6.42 % (165143)------------------------------
% 41.11/6.42 % (165143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.11/6.42 % (165143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.11/6.42 % (165143)CaDiCaL version: 2.1.3
% 41.11/6.42 % (165143)Termination reason: Instruction limit
% 41.11/6.42 % (165143)Termination phase: Finite model building preprocessing
% 41.11/6.42 % (165143)Time elapsed: 0.246 s
% 41.11/6.42 % (165143)Peak memory usage: 32 MB
% 41.11/6.42 % (165143)Instructions burned: 922 (million)
% 41.11/6.42 % (165147)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=80761680:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 41.11/6.42 % (165147)Instruction limit reached!
% 41.11/6.42 % (165147)------------------------------
% 41.11/6.42 % (165147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.11/6.42 % (165147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.11/6.42 % (165147)CaDiCaL version: 2.1.3
% 41.11/6.42 % (165147)Termination reason: Instruction limit
% 41.11/6.42 % (165147)Termination phase: Saturation
% 41.11/6.42 % (165147)Time elapsed: 0.329 s
% 41.11/6.42 % (165147)Peak memory usage: 31 MB
% 41.11/6.42 % (165147)Instructions burned: 1476 (million)
% 41.11/6.42 % (165149)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=604737693:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 41.11/6.42 % TRYING [1]
% 41.11/6.42 % (165139)Cannot represent all propositional literals internally
% 41.11/6.42 % (165139)Refutation not found, incomplete strategy
% 41.11/6.42 % (165139)------------------------------
% 41.11/6.42 % (165139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.11/6.42 % (165139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.11/6.42 % (165139)CaDiCaL version: 2.1.3
% 41.11/6.42 % (165139)Termination reason: Refutation not found, incomplete strategy
% 41.11/6.42 % (165139)Time elapsed: 1.950 s
% 41.11/6.42 % (165139)Peak memory usage: 74 MB
% 65.45/9.83 % (165139)Instructions burned: 3931 (million)
% 65.45/9.83 % (165139)------------------------------
% 65.45/9.83 % (165139)------------------------------
% 65.45/9.83 % TRYING [1]
% 65.45/9.83 % (165151)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2567268733:fmbsr=2.30978:i=2174_2971 on theBenchmark for (2971ds/2174Mi)
% 65.45/9.83 % (165105)Cannot represent all propositional literals internally
% 65.45/9.83 % (165105)Refutation not found, incomplete strategy
% 65.45/9.83 % (165105)------------------------------
% 65.45/9.83 % (165105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.45/9.83 % (165105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.45/9.83 % (165105)CaDiCaL version: 2.1.3
% 65.45/9.83 % (165105)Termination reason: Refutation not found, incomplete strategy
% 65.45/9.83 % (165105)Time elapsed: 2.795 s
% 65.45/9.83 % (165105)Peak memory usage: 100 MB
% 65.45/9.83 % (165105)Instructions burned: 5546 (million)
% 65.45/9.83 % (165105)------------------------------
% 65.45/9.83 % (165105)------------------------------
% 65.45/9.83 % (165141)Cannot represent all propositional literals internally
% 65.45/9.83 % (165141)Refutation not found, incomplete strategy
% 65.45/9.83 % (165141)------------------------------
% 65.45/9.83 % (165141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.45/9.83 % (165141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.45/9.83 % (165141)CaDiCaL version: 2.1.3
% 65.45/9.83 % (165141)Termination reason: Refutation not found, incomplete strategy
% 65.45/9.83 % (165141)Time elapsed: 2.035 s
% 65.45/9.83 % (165141)Peak memory usage: 73 MB
% 65.45/9.83 % (165141)Instructions burned: 4124 (million)
% 65.45/9.83 % (165141)------------------------------
% 65.45/9.83 % (165141)------------------------------
% 65.45/9.83 % (165149)Cannot represent all propositional literals internally
% 65.45/9.83 % (165149)Refutation not found, incomplete strategy
% 65.45/9.83 % (165149)------------------------------
% 65.45/9.83 % (165149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.45/9.83 % (165149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.45/9.83 % (165149)CaDiCaL version: 2.1.3
% 65.45/9.83 % (165149)Termination reason: Refutation not found, incomplete strategy
% 65.45/9.83 % (165149)Time elapsed: 1.426 s
% 65.45/9.83 % (165149)Peak memory usage: 89 MB
% 65.45/9.83 % (165149)Instructions burned: 5329 (million)
% 65.45/9.83 % (165153)ott-2_1_sil=16000:newcnf=on:random_seed=1618408373:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 65.45/9.83 % (165149)------------------------------
% 65.45/9.83 % (165149)------------------------------
% 65.45/9.83 % (165156)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4223522503:i=54282_2969 on theBenchmark for (2969ds/54282Mi)
% 65.45/9.83 % (165155)ott+10_1_sil=32000:tgt=ground:random_seed=530744719:i=5114:av=off_2969 on theBenchmark for (2969ds/5114Mi)
% 65.45/9.83 % (165153)Instruction limit reached!
% 65.45/9.83 % (165153)------------------------------
% 65.45/9.83 % (165153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.45/9.83 % (165153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.45/9.83 % (165153)CaDiCaL version: 2.1.3
% 65.45/9.83 % (165153)Termination reason: Instruction limit
% 65.45/9.83 % (165153)Termination phase: Saturation
% 65.45/9.83 % (165153)Time elapsed: 0.380 s
% 65.45/9.83 % (165153)Peak memory usage: 29 MB
% 65.45/9.83 % (165153)Instructions burned: 870 (million)
% 65.45/9.83 % (165159)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2066850486:i=3512:aac=none_2965 on theBenchmark for (2965ds/3512Mi)
% 65.45/9.83 % (165145)Instruction limit reached!
% 65.45/9.83 % (165145)------------------------------
% 65.45/9.83 % (165145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.45/9.83 % (165145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.45/9.83 % (165145)CaDiCaL version: 2.1.3
% 65.45/9.83 % (165145)Termination reason: Instruction limit
% 65.45/9.83 % (165145)Termination phase: Saturation
% 65.45/9.83 % (165145)Time elapsed: 2.720 s
% 65.45/9.83 % (165145)Peak memory usage: 113 MB
% 65.45/9.83 % (165145)Instructions burned: 5132 (million)
% 65.45/9.83 % (165161)dis+21_1_sil=32000:sas=cadical:random_seed=2022767381:i=3773:amm=off_2961 on theBenchmark for (2961ds/3773Mi)
% 65.45/9.83 % (165151)Instruction limit reached!
% 65.45/9.83 % (165151)------------------------------
% 65.45/9.83 % (165151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.84/20.00 % (165151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.84/20.00 % (165151)CaDiCaL version: 2.1.3
% 136.84/20.00 % (165151)Termination reason: Instruction limit
% 136.84/20.00 % (165151)Termination phase: Finite model building preprocessing
% 136.84/20.00 % (165151)Time elapsed: 1.129 s
% 136.84/20.00 % (165151)Peak memory usage: 51 MB
% 136.84/20.00 % (165151)Instructions burned: 2174 (million)
% 136.84/20.00 % (165163)ott+11_1_sil=16000:gs=on:random_seed=1056654681:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2959 on theBenchmark for (2959ds/2251Mi)
% 136.84/20.00 % TRYING [1]
% 136.84/20.00 % (165156)Cannot represent all propositional literals internally
% 136.84/20.00 % (165156)Refutation not found, incomplete strategy
% 136.84/20.00 % (165156)------------------------------
% 136.84/20.00 % (165156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.84/20.00 % (165156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.84/20.00 % (165156)CaDiCaL version: 2.1.3
% 136.84/20.00 % (165156)Termination reason: Refutation not found, incomplete strategy
% 136.84/20.00 % (165156)Time elapsed: 1.500 s
% 136.84/20.00 % (165156)Peak memory usage: 100 MB
% 136.84/20.00 % (165156)Instructions burned: 5545 (million)
% 136.84/20.00 % (165156)------------------------------
% 136.84/20.00 % (165156)------------------------------
% 136.84/20.00 % (165165)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2249890550:fmbsr=1.6:i=67534_2954 on theBenchmark for (2954ds/67534Mi)
% 136.84/20.00 % (165159)Instruction limit reached!
% 136.84/20.00 % (165159)------------------------------
% 136.84/20.00 % (165159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.84/20.00 % (165159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.84/20.00 % (165159)CaDiCaL version: 2.1.3
% 136.84/20.00 % (165159)Termination reason: Instruction limit
% 136.84/20.00 % (165159)Termination phase: Saturation
% 136.84/20.00 % (165159)Time elapsed: 1.825 s
% 136.84/20.00 % (165159)Peak memory usage: 63 MB
% 136.84/20.00 % (165159)Instructions burned: 3513 (million)
% 136.84/20.00 % (165167)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1910438916:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2947 on theBenchmark for (2947ds/4591Mi)
% 136.84/20.00 % (165163)Instruction limit reached!
% 136.84/20.00 % (165163)------------------------------
% 136.84/20.00 % (165163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.84/20.00 % (165163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.84/20.00 % (165163)CaDiCaL version: 2.1.3
% 136.84/20.00 % (165163)Termination reason: Instruction limit
% 136.84/20.00 % (165163)Termination phase: Saturation
% 136.84/20.00 % (165163)Time elapsed: 1.336 s
% 136.84/20.00 % (165163)Peak memory usage: 66 MB
% 136.84/20.00 % (165163)Instructions burned: 2252 (million)
% 136.84/20.00 % (165169)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2886709316:i=29340_2946 on theBenchmark for (2946ds/29340Mi)
% 136.84/20.00 % (165161)Instruction limit reached!
% 136.84/20.00 % (165161)------------------------------
% 136.84/20.00 % (165161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.84/20.00 % (165161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.84/20.00 % (165161)CaDiCaL version: 2.1.3
% 136.84/20.00 % (165161)Termination reason: Instruction limit
% 136.84/20.00 % (165161)Termination phase: Saturation
% 136.84/20.00 % (165161)Time elapsed: 1.976 s
% 136.84/20.00 % (165161)Peak memory usage: 92 MB
% 136.84/20.00 % (165161)Instructions burned: 3774 (million)
% 136.84/20.00 % (165171)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4156951737:i=5211_2941 on theBenchmark for (2941ds/5211Mi)
% 136.84/20.00 % (165155)Instruction limit reached!
% 136.84/20.00 % (165155)------------------------------
% 136.84/20.00 % (165155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.84/20.00 % (165155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.84/20.00 % (165155)CaDiCaL version: 2.1.3
% 136.84/20.00 % (165155)Termination reason: Instruction limit
% 136.84/20.00 % (165155)Termination phase: Saturation
% 136.84/20.00 % (165155)Time elapsed: 2.814 s
% 136.84/20.00 % (165155)Peak memory usage: 161 MB
% 136.84/20.00 % (165155)Instructions burned: 5115 (million)
% 136.84/20.00 % (165173)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1405443794:i=5497:nm=2_2940 on theBenchmark for (2940ds/5497Mi)
% 136.84/20.00 % (165165)Cannot represent all propositional literals internally
% 136.84/20.00 % (165165)Refutation not found, incomplete strategy
% 207.40/29.86 % (165165)------------------------------
% 207.40/29.86 % (165165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.40/29.86 % (165165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.40/29.86 % (165165)CaDiCaL version: 2.1.3
% 207.40/29.86 % (165165)Termination reason: Refutation not found, incomplete strategy
% 207.40/29.86 % (165165)Time elapsed: 1.395 s
% 207.40/29.86 % (165165)Peak memory usage: 74 MB
% 207.40/29.86 % (165165)Instructions burned: 5478 (million)
% 207.40/29.86 % (165165)------------------------------
% 207.40/29.86 % (165165)------------------------------
% 207.40/29.86 % (165175)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=561577646:fmbsr=2:i=46332_2939 on theBenchmark for (2939ds/46332Mi)
% 207.40/29.86 % (165167)Instruction limit reached!
% 207.40/29.86 % (165167)------------------------------
% 207.40/29.86 % (165167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.40/29.86 % (165167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.40/29.86 % (165167)CaDiCaL version: 2.1.3
% 207.40/29.86 % (165167)Termination reason: Instruction limit
% 207.40/29.86 % (165167)Termination phase: Saturation
% 207.40/29.86 % (165167)Time elapsed: 1.610 s
% 207.40/29.86 % (165167)Peak memory usage: 32 MB
% 207.40/29.86 % (165167)Instructions burned: 4594 (million)
% 207.40/29.86 % (165177)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=676032214:i=14071_2930 on theBenchmark for (2930ds/14071Mi)
% 207.40/29.86 % (165175)Cannot represent all propositional literals internally
% 207.40/29.86 % (165175)Refutation not found, incomplete strategy
% 207.40/29.86 % (165175)------------------------------
% 207.40/29.86 % (165175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.40/29.86 % (165175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.40/29.86 % (165175)CaDiCaL version: 2.1.3
% 207.40/29.86 % (165175)Termination reason: Refutation not found, incomplete strategy
% 207.40/29.86 % (165175)Time elapsed: 1.391 s
% 207.40/29.86 % (165175)Peak memory usage: 74 MB
% 207.40/29.86 % (165175)Instructions burned: 5477 (million)
% 207.40/29.86 % (165175)------------------------------
% 207.40/29.86 % (165175)------------------------------
% 207.40/29.86 % (165179)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3043048257:i=22565:add=on:rawr=on_2925 on theBenchmark for (2925ds/22565Mi)
% 207.40/29.86 % (165171)Instruction limit reached!
% 207.40/29.86 % (165171)------------------------------
% 207.40/29.86 % (165171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.40/29.86 % (165171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.40/29.86 % (165171)CaDiCaL version: 2.1.3
% 207.40/29.86 % (165171)Termination reason: Instruction limit
% 207.40/29.86 % (165171)Termination phase: Saturation
% 207.40/29.86 % (165171)Time elapsed: 1.722 s
% 207.40/29.86 % (165171)Peak memory usage: 48 MB
% 207.40/29.86 % (165171)Instructions burned: 5224 (million)
% 207.40/29.86 % (165181)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2019458649:i=8173:av=off_2924 on theBenchmark for (2924ds/8173Mi)
% 207.40/29.86 % (165173)Cannot represent all propositional literals internally
% 207.40/29.86 % (165173)Refutation not found, incomplete strategy
% 207.40/29.86 % (165173)------------------------------
% 207.40/29.86 % (165173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.40/29.86 % (165173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.40/29.86 % (165173)CaDiCaL version: 2.1.3
% 207.40/29.86 % (165173)Termination reason: Refutation not found, incomplete strategy
% 207.40/29.86 % (165173)Time elapsed: 1.929 s
% 207.40/29.86 % (165173)Peak memory usage: 72 MB
% 207.40/29.86 % (165173)Instructions burned: 3870 (million)
% 207.40/29.86 % (165173)------------------------------
% 207.40/29.86 % (165173)------------------------------
% 207.40/29.86 % (165183)dis+10_16:1_sil=16000:random_seed=18196417:i=9155:fsr=off_2921 on theBenchmark for (2921ds/9155Mi)
% 207.40/29.86 % (165177)Cannot represent all propositional literals internally
% 207.40/29.86 % (165177)Refutation not found, incomplete strategy
% 207.40/29.86 % (165177)------------------------------
% 207.40/29.86 % (165177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.40/29.86 % (165177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.40/29.86 % (165177)CaDiCaL version: 2.1.3
% 207.40/29.86 % (165177)Termination reason: Refutation not found, incomplete strategy
% 207.40/29.86 % (165177)Time elapsed: 2.460 s
% 207.40/29.86 % (165177)Peak memory usage: 80 MB
% 244.53/35.08 % (165177)Instructions burned: 4978 (million)
% 244.53/35.08 % (165177)------------------------------
% 244.53/35.08 % (165177)------------------------------
% 244.53/35.08 % (165185)ott-3_8_sil=64000:random_seed=2188092923:i=20139:bs=on_2905 on theBenchmark for (2905ds/20139Mi)
% 244.53/35.08 % (165181)Instruction limit reached!
% 244.53/35.08 % (165181)------------------------------
% 244.53/35.08 % (165181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.53/35.08 % (165181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.53/35.08 % (165181)CaDiCaL version: 2.1.3
% 244.53/35.08 % (165181)Termination reason: Instruction limit
% 244.53/35.08 % (165181)Termination phase: Saturation
% 244.53/35.08 % (165181)Time elapsed: 4.775 s
% 244.53/35.08 % (165181)Peak memory usage: 225 MB
% 244.53/35.08 % (165181)Instructions burned: 8174 (million)
% 244.53/35.08 % (165187)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=930963711:fmbsr=2:i=32576_2875 on theBenchmark for (2875ds/32576Mi)
% 244.53/35.08 % (165183)Instruction limit reached!
% 244.53/35.08 % (165183)------------------------------
% 244.53/35.08 % (165183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.53/35.08 % (165183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.53/35.08 % (165183)CaDiCaL version: 2.1.3
% 244.53/35.08 % (165183)Termination reason: Instruction limit
% 244.53/35.08 % (165183)Termination phase: Saturation
% 244.53/35.08 % (165183)Time elapsed: 4.763 s
% 244.53/35.08 % (165183)Peak memory usage: 172 MB
% 244.53/35.08 % (165183)Instructions burned: 9155 (million)
% 244.53/35.08 % (165189)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2301668973:i=11404_2873 on theBenchmark for (2873ds/11404Mi)
% 244.53/35.08 % (165187)Cannot represent all propositional literals internally
% 244.53/35.08 % (165187)Refutation not found, incomplete strategy
% 244.53/35.08 % (165187)------------------------------
% 244.53/35.08 % (165187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.53/35.08 % (165187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.53/35.08 % (165187)CaDiCaL version: 2.1.3
% 244.53/35.08 % (165187)Termination reason: Refutation not found, incomplete strategy
% 244.53/35.08 % (165187)Time elapsed: 2.671 s
% 244.53/35.08 % (165187)Peak memory usage: 89 MB
% 244.53/35.08 % (165187)Instructions burned: 5330 (million)
% 244.53/35.08 % (165187)------------------------------
% 244.53/35.08 % (165187)------------------------------
% 244.53/35.08 % (165191)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=590255724:i=14134_2848 on theBenchmark for (2848ds/14134Mi)
% 244.53/35.08 % (165179)Instruction limit reached!
% 244.53/35.08 % (165179)------------------------------
% 244.53/35.08 % (165179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.53/35.08 % (165179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.53/35.08 % (165179)CaDiCaL version: 2.1.3
% 244.53/35.08 % (165179)Termination reason: Instruction limit
% 244.53/35.08 % (165179)Termination phase: Saturation
% 244.53/35.08 % (165179)Time elapsed: 8.168 s
% 244.53/35.08 % (165179)Peak memory usage: 499 MB
% 244.53/35.08 % (165179)Instructions burned: 22567 (million)
% 244.53/35.08 % (165193)dis+33_16_sil=32000:sac=on:random_seed=1512729783:i=15851:nm=0_2843 on theBenchmark for (2843ds/15851Mi)
% 244.53/35.08 % (165169)Instruction limit reached!
% 244.53/35.08 % (165169)------------------------------
% 244.53/35.08 % (165169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.53/35.08 % (165169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.53/35.08 % (165169)CaDiCaL version: 2.1.3
% 244.53/35.08 % (165169)Termination reason: Instruction limit
% 244.53/35.08 % (165169)Termination phase: Saturation
% 244.53/35.08 % (165169)Time elapsed: 13.717 s
% 244.53/35.08 % (165169)Peak memory usage: 448 MB
% 244.53/35.08 % (165169)Instructions burned: 29342 (million)
% 244.53/35.08 % (165195)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2649859945:avsq=on:i=17627:add=on:amm=off_2808 on theBenchmark for (2808ds/17627Mi)
% 244.53/35.08 % (165189)Instruction limit reached!
% 244.53/35.08 % (165189)------------------------------
% 244.53/35.08 % (165189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.53/35.08 % (165189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.53/35.08 % (165189)CaDiCaL version: 2.1.3
% 244.53/35.08 % (165189)Termination reason: Instruction limit
% 244.53/35.08 % (165189)Termination phase: Saturation
% 244.53/35.08 % (165189)Time elapsed: 6.876 s
% 244.53/35.08 % (165189)Peak memory usage: 320 MB
% 244.53/35.08 % (165189)Instructions burned: 11406 (million)
% 179.77/35.51 % (165197)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2435952344:s2a=on:i=53295_2803 on theBenchmark for (2803ds/53295Mi)
% 179.77/35.51 % (165185)Instruction limit reached!
% 179.77/35.51 % (165185)------------------------------
% 179.77/35.51 % (165185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.51 % (165185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.51 % (165185)CaDiCaL version: 2.1.3
% 179.77/35.51 % (165185)Termination reason: Instruction limit
% 179.77/35.51 % (165185)Termination phase: Saturation
% 179.77/35.51 % (165185)Time elapsed: 12.412 s
% 179.77/35.51 % (165185)Peak memory usage: 246 MB
% 179.77/35.51 % (165185)Instructions burned: 20139 (million)
% 179.77/35.51 % (165199)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=377544476:i=26857:ins=20_2781 on theBenchmark for (2781ds/26857Mi)
% 179.77/35.51 % (165191)Instruction limit reached!
% 179.77/35.51 % (165191)------------------------------
% 179.77/35.51 % (165191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.51 % (165191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.51 % (165191)CaDiCaL version: 2.1.3
% 179.77/35.51 % (165191)Termination reason: Instruction limit
% 179.77/35.51 % (165191)Termination phase: Saturation
% 179.77/35.51 % (165191)Time elapsed: 8.249 s
% 179.77/35.51 % (165191)Peak memory usage: 174 MB
% 179.77/35.51 % (165191)Instructions burned: 14135 (million)
% 179.77/35.51 % (165201)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3920090784:i=28120:bs=on:fsr=off_2765 on theBenchmark for (2765ds/28120Mi)
% 179.77/35.51 % (165199)Cannot represent all propositional literals internally
% 179.77/35.51 % (165199)Refutation not found, incomplete strategy
% 179.77/35.51 % (165199)------------------------------
% 179.77/35.51 % (165199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.51 % (165199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.51 % (165199)CaDiCaL version: 2.1.3
% 179.77/35.51 % (165199)Termination reason: Refutation not found, incomplete strategy
% 179.77/35.51 % (165199)Time elapsed: 2.475 s
% 179.77/35.51 % (165199)Peak memory usage: 80 MB
% 179.77/35.51 % (165199)Instructions burned: 4979 (million)
% 179.77/35.51 % (165199)------------------------------
% 179.77/35.51 % (165199)------------------------------
% 179.77/35.51 % (165203)fmb+10_1_sil=256000:fmbss=7:random_seed=2343697973:fmbsr=1.6:i=182295_2755 on theBenchmark for (2755ds/182295Mi)
% 179.77/35.51 % (165203)Cannot represent all propositional literals internally
% 179.77/35.51 % (165203)Refutation not found, incomplete strategy
% 179.77/35.51 % (165203)------------------------------
% 179.77/35.51 % (165203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.51 % (165203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.51 % (165203)CaDiCaL version: 2.1.3
% 179.77/35.51 % (165203)Termination reason: Refutation not found, incomplete strategy
% 179.77/35.51 % (165203)Time elapsed: 2.482 s
% 179.77/35.51 % (165203)Peak memory usage: 80 MB
% 179.77/35.51 % (165203)Instructions burned: 4978 (million)
% 179.77/35.51 % (165203)------------------------------
% 179.77/35.51 % (165203)------------------------------
% 179.77/35.51 % (165205)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1050564953:i=44625:gsp=on_2730 on theBenchmark for (2730ds/44625Mi)
% 179.77/35.51 % (165193)Instruction limit reached!
% 179.77/35.51 % (165193)------------------------------
% 179.77/35.51 % (165193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.51 % (165193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.51 % (165193)CaDiCaL version: 2.1.3
% 179.77/35.51 % (165193)Termination reason: Instruction limit
% 179.77/35.51 % (165193)Termination phase: Clausification
% 179.77/35.51 % (165193)Time elapsed: 11.635 s
% 179.77/35.51 % (165193)Peak memory usage: 11340 MB
% 179.77/35.51 % (165193)Instructions burned: 15852 (million)
% 179.77/35.51 % (165207)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3976511310:i=160505_2719 on theBenchmark for (2719ds/160505Mi)
% 179.77/35.51 % (165207)Cannot represent all propositional literals internally
% 179.77/35.51 % (165207)Refutation not found, incomplete strategy
% 179.77/35.51 % (165207)------------------------------
% 179.77/35.51 % (165207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.51 % (165207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.51 % (165207)CaDiCaL version: 2.1.3
% 179.77/35.51 % (165207)Termination reason: Refutation not found, incomplete strategy
% 179.77/35.52 % (165207)Time elapsed: 1.335 s
% 179.77/35.52 % (165207)Peak memory usage: 80 MB
% 179.77/35.52 % (165207)Instructions burned: 4978 (million)
% 179.77/35.52 % (165207)------------------------------
% 179.77/35.52 % (165207)------------------------------
% 179.77/35.52 % (165209)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2873756619:fmbsr=1.3:i=225729_2705 on theBenchmark for (2705ds/225729Mi)
% 179.77/35.52 % (165209)Cannot represent all propositional literals internally
% 179.77/35.52 % (165209)Refutation not found, incomplete strategy
% 179.77/35.52 % (165209)------------------------------
% 179.77/35.52 % (165209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.52 % (165209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.52 % (165209)CaDiCaL version: 2.1.3
% 179.77/35.52 % (165209)Termination reason: Refutation not found, incomplete strategy
% 179.77/35.52 % (165209)Time elapsed: 1.336 s
% 179.77/35.52 % (165209)Peak memory usage: 80 MB
% 179.77/35.52 % (165209)Instructions burned: 4979 (million)
% 179.77/35.52 % (165209)------------------------------
% 179.77/35.52 % (165209)------------------------------
% 179.77/35.52 % (165211)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3539899776:fmbsr=2:i=185024:ins=7_2691 on theBenchmark for (2691ds/185024Mi)
% 179.77/35.52 % (165195)Instruction limit reached!
% 179.77/35.52 % (165195)------------------------------
% 179.77/35.52 % (165195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.52 % (165195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.52 % (165195)CaDiCaL version: 2.1.3
% 179.77/35.52 % (165195)Termination reason: Instruction limit
% 179.77/35.52 % (165195)Termination phase: Saturation
% 179.77/35.52 % (165195)Time elapsed: 12.421 s
% 179.77/35.52 % (165195)Peak memory usage: 372 MB
% 179.77/35.52 % (165195)Instructions burned: 17627 (million)
% 179.77/35.52 % (165213)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=695538750:rtra=on_2683 on theBenchmark for (2683ds/0Mi)
% 179.77/35.52 % (165211)Cannot represent all propositional literals internally
% 179.77/35.52 % (165211)Refutation not found, incomplete strategy
% 179.77/35.52 % (165211)------------------------------
% 179.77/35.52 % (165211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.52 % (165211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.52 % (165211)CaDiCaL version: 2.1.3
% 179.77/35.52 % (165211)Termination reason: Refutation not found, incomplete strategy
% 179.77/35.52 % (165211)Time elapsed: 1.338 s
% 179.77/35.52 % (165211)Peak memory usage: 80 MB
% 179.77/35.52 % (165211)Instructions burned: 4979 (million)
% 179.77/35.52 % (165211)------------------------------
% 179.77/35.52 % (165211)------------------------------
% 179.77/35.52 % (165215)% WARNING: option uhcvi not known.
% 179.77/35.52 % (165215)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3028605921:i=271062:add=off:rtra=on:rawr=on_2678 on theBenchmark for (2678ds/271062Mi)
% 179.77/35.52 % (165205)Cannot represent all propositional literals internally
% 179.77/35.52 % (165205)Refutation not found, incomplete strategy
% 179.77/35.52 % (165205)------------------------------
% 179.77/35.52 % (165205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.52 % (165205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.52 % (165205)CaDiCaL version: 2.1.3
% 179.77/35.52 % (165205)Termination reason: Refutation not found, incomplete strategy
% 179.77/35.52 % (165205)Time elapsed: 5.957 s
% 179.77/35.52 % (165205)Peak memory usage: 138 MB
% 179.77/35.52 % (165205)Instructions burned: 12234 (million)
% 179.77/35.52 % (165205)------------------------------
% 179.77/35.52 % (165205)------------------------------
% 179.77/35.52 % (165217)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2034840333:i=176048:add=on:rtra=on:rawr=on_2670 on theBenchmark for (2670ds/176048Mi)
% 179.77/35.52 % TRYING [1]
% 179.77/35.52 % (165213)Cannot represent all propositional literals internally
% 179.77/35.52 % (165213)Refutation not found, incomplete strategy
% 179.77/35.52 % (165213)------------------------------
% 179.77/35.52 % (165213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.52 % (165213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.52 % (165213)CaDiCaL version: 2.1.3
% 179.77/35.52 % (165213)Termination reason: Refutation not found, incomplete strategy
% 179.77/35.52 % (165213)Time elapsed: 2.956 s
% 179.77/35.52 % (165213)Peak memory usage: 102 MB
% 179.77/35.52 % (165213)Instructions burned: 5596 (million)
% 179.77/35.52 % (165213)------------------------------
% 179.77/35.52 % (165213)------------------------------
% 179.77/35.52 % (165219)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1503199182:i=206:fgj=on:rtra=on_2653 on theBenchmark for (2653ds/206Mi)
% 179.77/35.52 % (165219)Instruction limit reached!
% 179.77/35.52 % (165219)------------------------------
% 179.77/35.52 % (165219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.52 % (165219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.52 % (165219)CaDiCaL version: 2.1.3
% 179.77/35.52 % (165219)Termination reason: Instruction limit
% 179.77/35.52 % (165219)Termination phase: Clausification
% 179.77/35.52 % (165219)Time elapsed: 0.141 s
% 179.77/35.52 % (165219)Peak memory usage: 27 MB
% 179.77/35.52 % (165219)Instructions burned: 207 (million)
% 179.77/35.52 % (165221)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=413562330:i=232:rtra=on_2651 on theBenchmark for (2651ds/232Mi)
% 179.77/35.52 % (165106) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-165100-165106"...
% 179.77/35.52 % (165106)...printing done.
% 179.77/35.52 % (165106)Refutation found. Thanks to Tanya!
% 179.77/35.52 % SZS status Theorem for theBenchmark
% 179.77/35.52 % SZS output start Proof for theBenchmark
% See solution above
% 179.77/35.52 % (165106)------------------------------
% 179.77/35.52 % (165106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.77/35.52 % (165106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.77/35.52 % (165106)CaDiCaL version: 2.1.3
% 179.77/35.52 % (165106)Termination reason: Refutation
% 179.77/35.52 % (165106)Time elapsed: 34.701 s
% 179.77/35.52 % (165106)Peak memory usage: 401 MB
% 179.77/35.52 % (165106)Instructions burned: 62000 (million)
% 179.77/35.52 % (165100)Success in time 35.086 s
% 179.77/35.52 % Vampire exiting
%------------------------------------------------------------------------------