%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR069+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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 09:44:54 AM UTC 2026
% Result : Theorem 0.28s 28.37s
% Output : Refutation 0.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 2
% Syntax : Number of formulae : 9 ( 3 unt; 0 def)
% Number of atoms : 15 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 11 ( 5 ~; 2 |; 1 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 3 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 0 ( 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f278601,axiom,
( mtvisible(c_tptpgeo_member1_mt)
=> borderson(c_georegion_l4_x38_y24,c_georegion_l4_x39_y24) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+4.ax',ax4_278640) ).
fof(f540250,conjecture,
( mtvisible(c_tptpgeo_member1_mt)
=> borderson(c_georegion_l4_x38_y24,c_georegion_l4_x39_y24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query269) ).
fof(f540251,negated_conjecture,
~ ( mtvisible(c_tptpgeo_member1_mt)
=> borderson(c_georegion_l4_x38_y24,c_georegion_l4_x39_y24) ),
inference(negated_conjecture,[status(cth)],[f540250]) ).
fof(f727273,plain,
( borderson(c_georegion_l4_x38_y24,c_georegion_l4_x39_y24)
| ~ mtvisible(c_tptpgeo_member1_mt) ),
inference(ennf_transformation,[],[f278601]) ).
fof(f936432,plain,
( ~ borderson(c_georegion_l4_x38_y24,c_georegion_l4_x39_y24)
& mtvisible(c_tptpgeo_member1_mt) ),
inference(ennf_transformation,[],[f540251]) ).
fof(f1193495,plain,
( borderson(c_georegion_l4_x38_y24,c_georegion_l4_x39_y24)
| ~ mtvisible(c_tptpgeo_member1_mt) ),
inference(cnf_transformation,[],[f727273]) ).
fof(f1426741,plain,
mtvisible(c_tptpgeo_member1_mt),
inference(cnf_transformation,[],[f936432]) ).
fof(f1426742,plain,
~ borderson(c_georegion_l4_x38_y24,c_georegion_l4_x39_y24),
inference(cnf_transformation,[],[f936432]) ).
fof(f1426973,plain,
$false,
inference(global_subsumption,[],[f1193495,f1426742,f1426741]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR069+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.26 % Computer : n013.cluster.edu
% 0.10/0.26 % Model : x86_64 x86_64
% 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.26 % Memory : 8046.5625MB
% 0.10/0.26 % OS : Linux 6.8.0-71-generic
% 0.10/0.26 % CPULimit : 300
% 0.10/0.26 % WCLimit : 300
% 0.10/0.26 % DateTime : Mon Sep 28 22:24:06 UTC 2026
% 0.10/0.26 % CPUTime :
% 0.10/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.24/0.31 Running first-order model finding
% 0.24/0.31 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
% 76.16/22.05 % (1658122)Will run a generic schedule for satisfiability detection.
% 76.16/22.05 % (1658303)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2623196585_2872 on theBenchmark for (2872ds/0Mi)
% 76.16/22.05 % (1658305)% WARNING: option uhcvi not known.
% 76.16/22.05 % (1658305)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=947930094:i=135531:add=off:rawr=on_2872 on theBenchmark for (2872ds/135531Mi)
% 76.16/22.05 % (1658307)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2629843820:i=88024:add=on:rawr=on_2872 on theBenchmark for (2872ds/88024Mi)
% 76.16/22.05 % (1658309)dis+10_1_sil=32000:sp=arity:random_seed=743165278:i=103:fgj=on_2872 on theBenchmark for (2872ds/103Mi)
% 76.16/22.05 % (1658311)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3404373313:i=116_2872 on theBenchmark for (2872ds/116Mi)
% 76.16/22.05 % (1658313)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4062749957:i=131_2872 on theBenchmark for (2872ds/131Mi)
% 76.16/22.05 % (1658314)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3546404719:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2872 on theBenchmark for (2872ds/159Mi)
% 76.16/22.05 % (1658309)Instruction limit reached!
% 76.16/22.05 % (1658309)------------------------------
% 76.16/22.05 % (1658309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.16/22.05 % (1658309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.16/22.05 % (1658309)CaDiCaL version: 2.1.3
% 76.16/22.05 % (1658309)Termination reason: Instruction limit
% 76.16/22.05 % (1658309)Termination phase: Preprocessing 1
% 76.16/22.05 % (1658309)Time elapsed: 0.088 s
% 76.16/22.05 % (1658309)Peak memory usage: 640 MB
% 76.16/22.05 % (1658309)Instructions burned: 103 (million)
% 76.16/22.05 % (1658311)Instruction limit reached!
% 76.16/22.05 % (1658311)------------------------------
% 76.16/22.05 % (1658311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.16/22.05 % (1658311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.16/22.05 % (1658311)CaDiCaL version: 2.1.3
% 76.16/22.05 % (1658311)Termination reason: Instruction limit
% 76.16/22.05 % (1658311)Termination phase: Preprocessing 1
% 76.16/22.05 % (1658311)Time elapsed: 0.109 s
% 76.16/22.05 % (1658311)Peak memory usage: 639 MB
% 76.16/22.05 % (1658311)Instructions burned: 117 (million)
% 76.16/22.05 % (1658313)Instruction limit reached!
% 76.16/22.05 % (1658313)------------------------------
% 76.16/22.05 % (1658313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.16/22.05 % (1658313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.16/22.05 % (1658313)CaDiCaL version: 2.1.3
% 76.16/22.05 % (1658313)Termination reason: Instruction limit
% 76.16/22.05 % (1658313)Termination phase: Preprocessing 1
% 76.16/22.05 % (1658313)Time elapsed: 0.108 s
% 76.16/22.05 % (1658313)Peak memory usage: 640 MB
% 76.16/22.05 % (1658313)Instructions burned: 131 (million)
% 76.16/22.05 % (1658317)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1943603586:i=714:nm=2_2869 on theBenchmark for (2869ds/714Mi)
% 76.16/22.05 % (1658314)Instruction limit reached!
% 76.16/22.05 % (1658314)------------------------------
% 76.16/22.05 % (1658314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.16/22.05 % (1658314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.16/22.05 % (1658314)CaDiCaL version: 2.1.3
% 76.16/22.05 % (1658314)Termination reason: Instruction limit
% 76.16/22.05 % (1658314)Termination phase: Preprocessing 1
% 76.16/22.05 % (1658314)Time elapsed: 0.131 s
% 76.16/22.05 % (1658314)Peak memory usage: 639 MB
% 76.16/22.05 % (1658314)Instructions burned: 159 (million)
% 76.16/22.05 % (1658319)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1660351865:i=131:bd=preordered:fsd=on_2869 on theBenchmark for (2869ds/131Mi)
% 76.16/22.05 % (1658321)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=3057354250:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2869 on theBenchmark for (2869ds/684Mi)
% 76.16/22.05 % (1658323)ott-21_1_sil=16000:fs=off:random_seed=94243832:i=180:av=off:fsr=off_2868 on theBenchmark for (2868ds/180Mi)
% 76.16/22.05 % (1658319)Instruction limit reached!
% 76.16/22.05 % (1658319)------------------------------
% 76.16/22.05 % (1658319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.16/22.05 % (1658319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.53/27.21 % (1658319)CaDiCaL version: 2.1.3
% 78.53/27.21 % (1658319)Termination reason: Instruction limit
% 78.53/27.21 % (1658319)Termination phase: Preprocessing 1
% 78.53/27.21 % (1658319)Time elapsed: 0.108 s
% 78.53/27.21 % (1658319)Peak memory usage: 640 MB
% 78.53/27.21 % (1658319)Instructions burned: 132 (million)
% 78.53/27.21 % (1658325)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2671174427:i=477:bd=all_2867 on theBenchmark for (2867ds/477Mi)
% 78.53/27.21 % (1658323)Instruction limit reached!
% 78.53/27.21 % (1658323)------------------------------
% 78.53/27.21 % (1658323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.53/27.21 % (1658323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.53/27.21 % (1658323)CaDiCaL version: 2.1.3
% 78.53/27.21 % (1658323)Termination reason: Instruction limit
% 78.53/27.21 % (1658323)Termination phase: Preprocessing 1
% 78.53/27.21 % (1658323)Time elapsed: 0.146 s
% 78.53/27.21 % (1658323)Peak memory usage: 640 MB
% 78.53/27.21 % (1658323)Instructions burned: 180 (million)
% 78.53/27.21 % (1658327)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3541819140:fmbsr=1.3:i=865:ins=25_2866 on theBenchmark for (2866ds/865Mi)
% 78.53/27.21 % (1658317)Instruction limit reached!
% 78.53/27.21 % (1658317)------------------------------
% 78.53/27.21 % (1658317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.53/27.21 % (1658317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.53/27.21 % (1658317)CaDiCaL version: 2.1.3
% 78.53/27.21 % (1658317)Termination reason: Instruction limit
% 78.53/27.21 % (1658317)Termination phase: Preprocessing 1
% 78.53/27.21 % (1658317)Time elapsed: 0.529 s
% 78.53/27.21 % (1658317)Peak memory usage: 639 MB
% 78.53/27.21 % (1658317)Instructions burned: 715 (million)
% 78.53/27.21 % (1658321)Instruction limit reached!
% 78.53/27.21 % (1658321)------------------------------
% 78.53/27.21 % (1658321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.53/27.21 % (1658321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.53/27.21 % (1658321)CaDiCaL version: 2.1.3
% 78.53/27.21 % (1658321)Termination reason: Instruction limit
% 78.53/27.21 % (1658321)Termination phase: SInE selection
% 78.53/27.21 % (1658321)Time elapsed: 0.468 s
% 78.53/27.21 % (1658321)Peak memory usage: 642 MB
% 78.53/27.21 % (1658321)Instructions burned: 684 (million)
% 78.53/27.21 % (1658325)Instruction limit reached!
% 78.53/27.21 % (1658325)------------------------------
% 78.53/27.21 % (1658325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.53/27.21 % (1658325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.53/27.21 % (1658325)CaDiCaL version: 2.1.3
% 78.53/27.21 % (1658325)Termination reason: Instruction limit
% 78.53/27.21 % (1658325)Termination phase: Preprocessing 1
% 78.53/27.21 % (1658325)Time elapsed: 0.375 s
% 78.53/27.21 % (1658325)Peak memory usage: 639 MB
% 78.53/27.21 % (1658325)Instructions burned: 477 (million)
% 78.53/27.21 % (1658329)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1385242905:i=1179_2863 on theBenchmark for (2863ds/1179Mi)
% 78.53/27.21 % (1658331)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1276693295:i=889:ins=1_2863 on theBenchmark for (2863ds/889Mi)
% 78.53/27.21 % (1658335)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=647487558:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2863 on theBenchmark for (2863ds/692Mi)
% 78.53/27.21 % (1658327)Instruction limit reached!
% 78.53/27.21 % (1658327)------------------------------
% 78.53/27.21 % (1658327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.53/27.21 % (1658327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.53/27.21 % (1658327)CaDiCaL version: 2.1.3
% 78.53/27.21 % (1658327)Termination reason: Instruction limit
% 78.53/27.21 % (1658327)Termination phase: Preprocessing 1
% 78.53/27.21 % (1658327)Time elapsed: 0.624 s
% 78.53/27.21 % (1658327)Peak memory usage: 639 MB
% 78.53/27.21 % (1658327)Instructions burned: 866 (million)
% 78.53/27.21 % (1658457)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2057339400:i=879:kws=inv_precedence:fsr=off_2859 on theBenchmark for (2859ds/879Mi)
% 78.53/27.21 % (1658335)Instruction limit reached!
% 78.53/27.21 % (1658335)------------------------------
% 78.53/27.21 % (1658335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.53/27.21 % (1658335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.36 % (1658335)CaDiCaL version: 2.1.3
% 0.28/28.36 % (1658335)Termination reason: Instruction limit
% 0.28/28.36 % (1658335)Termination phase: SInE selection
% 0.28/28.36 % (1658335)Time elapsed: 0.481 s
% 0.28/28.36 % (1658335)Peak memory usage: 642 MB
% 0.28/28.36 % (1658335)Instructions burned: 693 (million)
% 0.28/28.36 % (1658459)fmb+10_1_sil=64000:random_seed=2996393869:i=22061:nm=2:gsp=on_2857 on theBenchmark for (2857ds/22061Mi)
% 0.28/28.36 % (1658331)Instruction limit reached!
% 0.28/28.36 % (1658331)------------------------------
% 0.28/28.36 % (1658331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/28.36 % (1658331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.36 % (1658331)CaDiCaL version: 2.1.3
% 0.28/28.36 % (1658331)Termination reason: Instruction limit
% 0.28/28.36 % (1658331)Termination phase: Preprocessing 1
% 0.28/28.36 % (1658331)Time elapsed: 0.640 s
% 0.28/28.36 % (1658331)Peak memory usage: 639 MB
% 0.28/28.36 % (1658331)Instructions burned: 889 (million)
% 0.28/28.36 % (1658461)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2877768135:i=9515:nm=5_2856 on theBenchmark for (2856ds/9515Mi)
% 0.28/28.36 % (1658329)Instruction limit reached!
% 0.28/28.36 % (1658329)------------------------------
% 0.28/28.36 % (1658329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/28.36 % (1658329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.36 % (1658329)CaDiCaL version: 2.1.3
% 0.28/28.36 % (1658329)Termination reason: Instruction limit
% 0.28/28.36 % (1658329)Termination phase: Unused predicate definition removal
% 0.28/28.36 % (1658329)Time elapsed: 1.051 s
% 0.28/28.36 % (1658329)Peak memory usage: 717 MB
% 0.28/28.36 % (1658329)Instructions burned: 1179 (million)
% 0.28/28.36 % (1658575)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2712766303:fmbsr=1.7:i=920_2852 on theBenchmark for (2852ds/920Mi)
% 0.28/28.36 % (1658457)Instruction limit reached!
% 0.28/28.36 % (1658457)------------------------------
% 0.28/28.36 % (1658457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/28.36 % (1658457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.36 % (1658457)CaDiCaL version: 2.1.3
% 0.28/28.36 % (1658457)Termination reason: Instruction limit
% 0.28/28.36 % (1658457)Termination phase: Unused predicate definition removal
% 0.28/28.36 % (1658457)Time elapsed: 0.815 s
% 0.28/28.36 % (1658457)Peak memory usage: 704 MB
% 0.28/28.36 % (1658457)Instructions burned: 879 (million)
% 0.28/28.36 % (1658595)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=882879624:i=5131_2850 on theBenchmark for (2850ds/5131Mi)
% 0.28/28.36 % (1658575)Instruction limit reached!
% 0.28/28.36 % (1658575)------------------------------
% 0.28/28.36 % (1658575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/28.36 % (1658575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.36 % (1658575)CaDiCaL version: 2.1.3
% 0.28/28.36 % (1658575)Termination reason: Instruction limit
% 0.28/28.36 % (1658575)Termination phase: Preprocessing 1
% 0.28/28.36 % (1658575)Time elapsed: 0.687 s
% 0.28/28.36 % (1658575)Peak memory usage: 640 MB
% 0.28/28.36 % (1658575)Instructions burned: 920 (million)
% 0.28/28.36 % (1658597)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2844011587:i=1472:ins=7:fdi=8:gsp=on_2844 on theBenchmark for (2844ds/1472Mi)
% 0.28/28.37 % (1658597)Instruction limit reached!
% 0.28/28.37 % (1658597)------------------------------
% 0.28/28.37 % (1658597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/28.37 % (1658597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.37 % (1658597)CaDiCaL version: 2.1.3
% 0.28/28.37 % (1658597)Termination reason: Instruction limit
% 0.28/28.37 % (1658597)Termination phase: Preprocessing 2
% 0.28/28.37 % (1658597)Time elapsed: 2.138 s
% 0.28/28.37 % (1658597)Peak memory usage: 724 MB
% 0.28/28.37 % (1658597)Instructions burned: 1472 (million)
% 0.28/28.37 % (1658637)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2085978210:i=6324_2821 on theBenchmark for (2821ds/6324Mi)
% 0.28/28.37 % (1658595)Instruction limit reached!
% 0.28/28.37 % (1658595)------------------------------
% 0.28/28.37 % (1658595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/28.37 % (1658595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.37 % (1658595)CaDiCaL version: 2.1.3
% 0.28/28.37 % (1658595)Termination reason: Instruction limit
% 0.28/28.37 % (1658595)Termination phase: Property scanning
% 0.28/28.37 % (1658595)Time elapsed: 6.734 s
% 0.28/28.37 % (1658595)Peak memory usage: 880 MB
% 0.28/28.37 % (1658595)Instructions burned: 5131 (million)
% 0.28/28.37 % (1658648)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3302217965:fmbsr=2.30978:i=2174_2781 on theBenchmark for (2781ds/2174Mi)
% 0.28/28.37 % (1658648)Instruction limit reached!
% 0.28/28.37 % (1658648)------------------------------
% 0.28/28.37 % (1658648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/28.37 % (1658648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.37 % (1658648)CaDiCaL version: 2.1.3
% 0.28/28.37 % (1658648)Termination reason: Instruction limit
% 0.28/28.37 % (1658648)Termination phase: Naming
% 0.28/28.37 % (1658648)Time elapsed: 1.836 s
% 0.28/28.37 % (1658648)Peak memory usage: 745 MB
% 0.28/28.37 % (1658648)Instructions burned: 2176 (million)
% 0.28/28.37 % (1658461)Instruction limit reached!
% 0.28/28.37 % (1658461)------------------------------
% 0.28/28.37 % (1658461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/28.37 % (1658461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.37 % (1658461)CaDiCaL version: 2.1.3
% 0.28/28.37 % (1658461)Termination reason: Instruction limit
% 0.28/28.37 % (1658461)Termination phase: Finite model building preprocessing
% 0.28/28.37 % (1658461)Time elapsed: 9.477 s
% 0.28/28.37 % (1658461)Peak memory usage: 864 MB
% 0.28/28.37 % (1658461)Instructions burned: 9516 (million)
% 0.28/28.37 % (1658803)ott-2_1_sil=16000:newcnf=on:random_seed=240138927:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2761 on theBenchmark for (2761ds/869Mi)
% 0.28/28.37 % (1658805)ott+10_1_sil=32000:tgt=ground:random_seed=1810233065:i=5114:av=off_2760 on theBenchmark for (2760ds/5114Mi)
% 0.28/28.37 % (1658637)Instruction limit reached!
% 0.28/28.37 % (1658637)------------------------------
% 0.28/28.37 % (1658637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/28.37 % (1658637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.37 % (1658637)CaDiCaL version: 2.1.3
% 0.28/28.37 % (1658637)Termination reason: Instruction limit
% 0.28/28.37 % (1658637)Termination phase: Property scanning
% 0.28/28.37 % (1658637)Time elapsed: 6.273 s
% 0.28/28.37 % (1658637)Peak memory usage: 795 MB
% 0.28/28.37 % (1658637)Instructions burned: 6324 (million)
% 0.28/28.37 % (1658807)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1167833824:i=54282_2757 on theBenchmark for (2757ds/54282Mi)
% 0.28/28.37 % (1658803)Instruction limit reached!
% 0.28/28.37 % (1658803)------------------------------
% 0.28/28.37 % (1658803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/28.37 % (1658803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.37 % (1658803)CaDiCaL version: 2.1.3
% 0.28/28.37 % (1658803)Termination reason: Instruction limit
% 0.28/28.37 % (1658803)Termination phase: Unused predicate definition removal
% 0.28/28.37 % (1658803)Time elapsed: 0.793 s
% 0.28/28.37 % (1658803)Peak memory usage: 701 MB
% 0.28/28.37 % (1658803)Instructions burned: 869 (million)
% 0.28/28.37 % (1658809)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3607633980:i=3512:aac=none_2752 on theBenchmark for (2752ds/3512Mi)
% 0.28/28.37 % (1658307) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1658122-1658307"...
% 0.28/28.37 % (1658307)...printing done.
% 0.28/28.37 % (1658307)Refutation found. Thanks to Tanya!
% 0.28/28.37 % SZS status Theorem for theBenchmark
% 0.28/28.37 % SZS output start Proof for theBenchmark
% See solution above
% 0.28/28.37 % (1658307)------------------------------
% 0.28/28.37 % (1658307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/28.37 % (1658307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/28.37 % (1658307)CaDiCaL version: 2.1.3
% 0.28/28.37 % (1658307)Termination reason: Refutation
% 0.28/28.37 % (1658307)Time elapsed: 13.003 s
% 0.28/28.37 % (1658307)Peak memory usage: 1379 MB
% 0.28/28.37 % (1658307)Instructions burned: 30301 (million)
% 0.28/28.37 % (1658122)Success in time 26.887 s
% 0.28/28.37 % Vampire exiting
%------------------------------------------------------------------------------