%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR025+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:42:00 AM UTC 2026
% Result : Theorem 0.33s 33.97s
% Output : Refutation 0.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 2
% Syntax : Number of formulae : 7 ( 4 unt; 0 def)
% Number of atoms : 10 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 6 ( 3 ~; 0 |; 1 &)
% ( 0 <=>; 2 =>; 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(f135567,axiom,
genls(c_tptpcol_16_130933,c_tptpcol_15_130931),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_135591) ).
fof(f540250,conjecture,
( mtvisible(c_patterndetectormt)
=> genls(c_tptpcol_16_130933,c_tptpcol_15_130931) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query225) ).
fof(f540251,negated_conjecture,
~ ( mtvisible(c_patterndetectormt)
=> genls(c_tptpcol_16_130933,c_tptpcol_15_130931) ),
inference(negated_conjecture,[status(cth)],[f540250]) ).
fof(f540938,plain,
( ~ genls(c_tptpcol_16_130933,c_tptpcol_15_130931)
& mtvisible(c_patterndetectormt) ),
inference(ennf_transformation,[],[f540251]) ).
fof(f541429,plain,
~ genls(c_tptpcol_16_130933,c_tptpcol_15_130931),
inference(cnf_transformation,[],[f540938]) ).
fof(f541444,plain,
genls(c_tptpcol_16_130933,c_tptpcol_15_130931),
inference(cnf_transformation,[],[f135567]) ).
fof(f542722,plain,
$false,
inference(forward_subsumption_resolution,[],[f541429,f541444]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR025+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.29 % Computer : n026.cluster.edu
% 0.12/0.29 % Model : x86_64 x86_64
% 0.12/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.29 % Memory : 8046.5625MB
% 0.12/0.29 % OS : Linux 6.8.0-71-generic
% 0.12/0.29 % CPULimit : 300
% 0.12/0.29 % WCLimit : 300
% 0.12/0.29 % DateTime : Mon Sep 28 22:09:12 UTC 2026
% 0.12/0.29 % CPUTime :
% 0.12/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.30/0.34 Running first-order theorem proving
% 0.30/0.34 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 44.04/24.50 % (142070)Detected formulas, will run a generic FOF schedule.
% 44.04/24.50 % (142076)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2730833630:i=141193_2800 on theBenchmark for (2800ds/141193Mi)
% 44.04/24.50 % (142077)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=546641177:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2800 on theBenchmark for (2800ds/134677Mi)
% 44.04/24.50 % (142081)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1209210207:s2a=on:i=139:gtg=position_2800 on theBenchmark for (2800ds/139Mi)
% 44.04/24.50 % (142079)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2742381249:i=109:sd=1:ins=1:gsp=on:ss=axioms_2800 on theBenchmark for (2800ds/109Mi)
% 44.04/24.50 % (142078)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=175236568:i=141695:sd=1:nm=32:gsp=on:ss=included_2800 on theBenchmark for (2800ds/141695Mi)
% 44.04/24.50 % (142080)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2597180702:i=119:av=off:ss=axioms_2800 on theBenchmark for (2800ds/119Mi)
% 44.04/24.50 % (142082)dis-21_1_sil=8000:lcm=predicate:random_seed=3872615545:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2800 on theBenchmark for (2800ds/129Mi)
% 44.04/24.50 % (142079)Instruction limit reached!
% 44.04/24.50 % (142079)------------------------------
% 44.04/24.50 % (142079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.04/24.50 % (142079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/24.50 % (142079)CaDiCaL version: 2.1.3
% 44.04/24.50 % (142079)Termination reason: Instruction limit
% 44.04/24.50 % (142079)Termination phase: SInE selection
% 44.04/24.50 % (142079)Time elapsed: 0.128 s
% 44.04/24.50 % (142079)Peak memory usage: 462 MB
% 44.04/24.50 % (142079)Instructions burned: 109 (million)
% 44.04/24.50 % (142081)Instruction limit reached!
% 44.04/24.50 % (142081)------------------------------
% 44.04/24.50 % (142081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.04/24.50 % (142081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/24.50 % (142081)CaDiCaL version: 2.1.3
% 44.04/24.50 % (142081)Termination reason: Instruction limit
% 44.04/24.50 % (142081)Termination phase: Property scanning
% 44.04/24.50 % (142081)Time elapsed: 0.174 s
% 44.04/24.50 % (142081)Peak memory usage: 463 MB
% 44.04/24.50 % (142081)Instructions burned: 140 (million)
% 44.04/24.50 % (142080)Instruction limit reached!
% 44.04/24.50 % (142080)------------------------------
% 44.04/24.50 % (142080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.04/24.50 % (142080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/24.50 % (142080)CaDiCaL version: 2.1.3
% 44.04/24.50 % (142080)Termination reason: Instruction limit
% 44.04/24.50 % (142080)Termination phase: SInE selection
% 44.04/24.50 % (142080)Time elapsed: 0.146 s
% 44.04/24.50 % (142080)Peak memory usage: 462 MB
% 44.04/24.50 % (142080)Instructions burned: 119 (million)
% 44.04/24.50 % (142082)Instruction limit reached!
% 44.04/24.50 % (142082)------------------------------
% 44.04/24.50 % (142082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.04/24.50 % (142082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/24.50 % (142082)CaDiCaL version: 2.1.3
% 44.04/24.50 % (142082)Termination reason: Instruction limit
% 44.04/24.50 % (142082)Termination phase: SInE selection
% 44.04/24.50 % (142082)Time elapsed: 0.159 s
% 44.04/24.50 % (142082)Peak memory usage: 462 MB
% 44.04/24.50 % (142082)Instructions burned: 129 (million)
% 44.04/24.50 % (142091)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1899873029:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2795 on theBenchmark for (2795ds/157Mi)
% 44.04/24.50 % (142090)lrs+10_1_sil=8000:sp=occurrence:random_seed=1365393566:i=285:sd=3:ss=axioms:sgt=8_2796 on theBenchmark for (2796ds/285Mi)
% 44.04/24.50 % (142092)lrs+1011_1_sil=32000:sp=occurrence:random_seed=134986583:i=325:sd=1:ss=axioms:sgt=32_2795 on theBenchmark for (2795ds/325Mi)
% 44.04/24.50 % (142093)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2163195889:s2a=on:i=248:s2at=1.23:gtg=position_2794 on theBenchmark for (2794ds/248Mi)
% 44.04/24.50 % (142091)Instruction limit reached!
% 44.04/24.50 % (142091)------------------------------
% 59.24/26.58 % (142091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.24/26.58 % (142091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.24/26.58 % (142091)CaDiCaL version: 2.1.3
% 59.24/26.58 % (142091)Termination reason: Instruction limit
% 59.24/26.58 % (142091)Termination phase: Property scanning
% 59.24/26.58 % (142091)Time elapsed: 0.181 s
% 59.24/26.58 % (142091)Peak memory usage: 463 MB
% 59.24/26.58 % (142091)Instructions burned: 158 (million)
% 59.24/26.58 % (142090)Instruction limit reached!
% 59.24/26.58 % (142090)------------------------------
% 59.24/26.58 % (142090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.24/26.58 % (142090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.24/26.58 % (142090)CaDiCaL version: 2.1.3
% 59.24/26.58 % (142090)Termination reason: Instruction limit
% 59.24/26.58 % (142090)Termination phase: SInE selection
% 59.24/26.58 % (142090)Time elapsed: 0.298 s
% 59.24/26.58 % (142090)Peak memory usage: 463 MB
% 59.24/26.58 % (142090)Instructions burned: 285 (million)
% 59.24/26.58 % (142098)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4096536476:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2792 on theBenchmark for (2792ds/294Mi)
% 59.24/26.58 % (142099)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=532988154:i=2350_2790 on theBenchmark for (2790ds/2350Mi)
% 59.24/26.58 % (142092)Instruction limit reached!
% 59.24/26.58 % (142092)------------------------------
% 59.24/26.58 % (142092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.24/26.58 % (142092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.24/26.58 % (142092)CaDiCaL version: 2.1.3
% 59.24/26.58 % (142092)Termination reason: Instruction limit
% 59.24/26.58 % (142092)Termination phase: SInE selection
% 59.24/26.58 % (142092)Time elapsed: 0.420 s
% 59.24/26.58 % (142092)Peak memory usage: 462 MB
% 59.24/26.58 % (142092)Instructions burned: 325 (million)
% 59.24/26.58 % (142093)Instruction limit reached!
% 59.24/26.58 % (142093)------------------------------
% 59.24/26.58 % (142093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.24/26.58 % (142093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.24/26.58 % (142093)CaDiCaL version: 2.1.3
% 59.24/26.58 % (142093)Termination reason: Instruction limit
% 59.24/26.58 % (142093)Termination phase: Property scanning
% 59.24/26.58 % (142093)Time elapsed: 0.392 s
% 59.24/26.58 % (142093)Peak memory usage: 463 MB
% 59.24/26.58 % (142093)Instructions burned: 248 (million)
% 59.24/26.58 % (142102)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2786322952:cts=off:i=113:fsr=off:ss=included:sgt=4_2788 on theBenchmark for (2788ds/113Mi)
% 59.24/26.58 % (142098)Instruction limit reached!
% 59.24/26.58 % (142098)------------------------------
% 59.24/26.58 % (142098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.24/26.58 % (142098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.24/26.58 % (142098)CaDiCaL version: 2.1.3
% 59.24/26.58 % (142098)Termination reason: Instruction limit
% 59.24/26.58 % (142098)Termination phase: SInE selection
% 59.24/26.58 % (142098)Time elapsed: 0.369 s
% 59.24/26.58 % (142098)Peak memory usage: 462 MB
% 59.24/26.58 % (142098)Instructions burned: 294 (million)
% 59.24/26.58 % (142103)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1794530961:i=127:av=off:fsr=off:sup=off_2788 on theBenchmark for (2788ds/127Mi)
% 59.24/26.58 % (142102)Instruction limit reached!
% 59.24/26.58 % (142102)------------------------------
% 59.24/26.58 % (142102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.24/26.58 % (142102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.24/26.58 % (142102)CaDiCaL version: 2.1.3
% 59.24/26.58 % (142102)Termination reason: Instruction limit
% 59.24/26.58 % (142102)Termination phase: SInE selection
% 59.24/26.58 % (142102)Time elapsed: 0.144 s
% 59.24/26.58 % (142102)Peak memory usage: 463 MB
% 59.24/26.58 % (142102)Instructions burned: 113 (million)
% 59.24/26.58 % (142103)Instruction limit reached!
% 59.24/26.58 % (142103)------------------------------
% 59.24/26.58 % (142103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.24/26.58 % (142103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.24/26.58 % (142103)CaDiCaL version: 2.1.3
% 59.24/26.58 % (142103)Termination reason: Instruction limit
% 59.24/26.58 % (142103)Termination phase: Preprocessing 1
% 59.24/26.58 % (142103)Time elapsed: 0.166 s
% 51.39/33.08 % (142103)Peak memory usage: 463 MB
% 51.39/33.08 % (142103)Instructions burned: 127 (million)
% 51.39/33.08 % (142106)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=906704535:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2785 on theBenchmark for (2785ds/114Mi)
% 51.39/33.08 % (142107)lrs+10_1_sil=8000:sp=occurrence:random_seed=4071936356:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2784 on theBenchmark for (2784ds/907Mi)
% 51.39/33.08 % (142108)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=676510959:i=437:sd=1:aac=none:ss=included_2783 on theBenchmark for (2783ds/437Mi)
% 51.39/33.08 % (142106)Instruction limit reached!
% 51.39/33.08 % (142106)------------------------------
% 51.39/33.08 % (142106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.39/33.08 % (142106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.39/33.08 % (142106)CaDiCaL version: 2.1.3
% 51.39/33.08 % (142106)Termination reason: Instruction limit
% 51.39/33.08 % (142106)Termination phase: Property scanning
% 51.39/33.08 % (142106)Time elapsed: 0.282 s
% 51.39/33.08 % (142106)Peak memory usage: 463 MB
% 51.39/33.08 % (142106)Instructions burned: 114 (million)
% 51.39/33.08 % (142112)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=273468437:i=5202:ss=axioms:sgt=16_2779 on theBenchmark for (2779ds/5202Mi)
% 51.39/33.08 % (142108)Instruction limit reached!
% 51.39/33.08 % (142108)------------------------------
% 51.39/33.08 % (142108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.39/33.08 % (142108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.39/33.08 % (142108)CaDiCaL version: 2.1.3
% 51.39/33.08 % (142108)Termination reason: Instruction limit
% 51.39/33.08 % (142108)Termination phase: SInE selection
% 51.39/33.08 % (142108)Time elapsed: 0.543 s
% 51.39/33.08 % (142108)Peak memory usage: 462 MB
% 51.39/33.08 % (142108)Instructions burned: 437 (million)
% 51.39/33.08 % (142114)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1183797199:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2775 on theBenchmark for (2775ds/134Mi)
% 51.39/33.08 % (142114)Instruction limit reached!
% 51.39/33.08 % (142114)------------------------------
% 51.39/33.08 % (142114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.39/33.08 % (142114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.39/33.08 % (142114)CaDiCaL version: 2.1.3
% 51.39/33.08 % (142114)Termination reason: Instruction limit
% 51.39/33.08 % (142114)Termination phase: SInE selection
% 51.39/33.08 % (142114)Time elapsed: 0.202 s
% 51.39/33.08 % (142114)Peak memory usage: 463 MB
% 51.39/33.08 % (142114)Instructions burned: 134 (million)
% 51.39/33.08 % (142107)Instruction limit reached!
% 51.39/33.08 % (142107)------------------------------
% 51.39/33.08 % (142107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.39/33.08 % (142107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.39/33.08 % (142107)CaDiCaL version: 2.1.3
% 51.39/33.08 % (142107)Termination reason: Instruction limit
% 51.39/33.08 % (142107)Termination phase: SInE selection
% 51.39/33.08 % (142107)Time elapsed: 1.142 s
% 51.39/33.08 % (142107)Peak memory usage: 474 MB
% 51.39/33.08 % (142107)Instructions burned: 907 (million)
% 51.39/33.08 % (142099)Instruction limit reached!
% 51.39/33.08 % (142099)------------------------------
% 51.39/33.08 % (142099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.39/33.08 % (142099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.39/33.08 % (142099)CaDiCaL version: 2.1.3
% 51.39/33.08 % (142099)Termination reason: Instruction limit
% 51.39/33.08 % (142099)Termination phase: Unused predicate definition removal
% 51.39/33.08 % (142099)Time elapsed: 1.907 s
% 51.39/33.08 % (142099)Peak memory usage: 555 MB
% 51.39/33.08 % (142099)Instructions burned: 2350 (million)
% 51.39/33.08 % (142116)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=725619083:st=8:i=592:sd=3:ep=RST:ss=axioms_2770 on theBenchmark for (2770ds/592Mi)
% 51.39/33.08 % (142117)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1807541831:st=3:i=13193:sd=3:ss=axioms_2770 on theBenchmark for (2770ds/13193Mi)
% 51.39/33.08 % (142118)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=182639151:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2769 on theBenchmark for (2769ds/125Mi)
% 51.39/33.08 % (142118)Instruction limit reached!
% 51.39/33.08 % (142118)------------------------------
% 0.33/33.97 % (142118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142118)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142118)Termination reason: Instruction limit
% 0.33/33.97 % (142118)Termination phase: Property scanning
% 0.33/33.97 % (142118)Time elapsed: 0.162 s
% 0.33/33.97 % (142118)Peak memory usage: 463 MB
% 0.33/33.97 % (142118)Instructions burned: 125 (million)
% 0.33/33.97 % (142122)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1540497178:i=134:gtgl=5:slsql=off:gtg=exists_sym_2765 on theBenchmark for (2765ds/134Mi)
% 0.33/33.97 % (142122)Instruction limit reached!
% 0.33/33.97 % (142122)------------------------------
% 0.33/33.97 % (142122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142122)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142122)Termination reason: Instruction limit
% 0.33/33.97 % (142122)Termination phase: Property scanning
% 0.33/33.97 % (142122)Time elapsed: 0.170 s
% 0.33/33.97 % (142122)Peak memory usage: 463 MB
% 0.33/33.97 % (142122)Instructions burned: 135 (million)
% 0.33/33.97 % (142116)Instruction limit reached!
% 0.33/33.97 % (142116)------------------------------
% 0.33/33.97 % (142116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142116)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142116)Termination reason: Instruction limit
% 0.33/33.97 % (142116)Termination phase: SInE selection
% 0.33/33.97 % (142116)Time elapsed: 0.737 s
% 0.33/33.97 % (142116)Peak memory usage: 469 MB
% 0.33/33.97 % (142116)Instructions burned: 592 (million)
% 0.33/33.97 % (142124)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1086385224:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2761 on theBenchmark for (2761ds/141Mi)
% 0.33/33.97 % (142124)Instruction limit reached!
% 0.33/33.97 % (142124)------------------------------
% 0.33/33.97 % (142124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142124)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142124)Termination reason: Instruction limit
% 0.33/33.97 % (142124)Termination phase: SInE selection
% 0.33/33.97 % (142124)Time elapsed: 0.112 s
% 0.33/33.97 % (142124)Peak memory usage: 462 MB
% 0.33/33.97 % (142124)Instructions burned: 142 (million)
% 0.33/33.97 % (142125)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2995861591:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2760 on theBenchmark for (2760ds/431Mi)
% 0.33/33.97 % (142127)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3111425700:i=6060:aac=none:ins=25_2758 on theBenchmark for (2758ds/6060Mi)
% 0.33/33.97 % (142125)Instruction limit reached!
% 0.33/33.97 % (142125)------------------------------
% 0.33/33.97 % (142125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142125)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142125)Termination reason: Instruction limit
% 0.33/33.97 % (142125)Termination phase: SInE selection
% 0.33/33.97 % (142125)Time elapsed: 0.539 s
% 0.33/33.97 % (142125)Peak memory usage: 462 MB
% 0.33/33.97 % (142125)Instructions burned: 431 (million)
% 0.33/33.97 % (142130)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=480221850:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2752 on theBenchmark for (2752ds/150Mi)
% 0.33/33.97 % (142130)Instruction limit reached!
% 0.33/33.97 % (142130)------------------------------
% 0.33/33.97 % (142130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142130)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142130)Termination reason: Instruction limit
% 0.33/33.97 % (142130)Termination phase: SInE selection
% 0.33/33.97 % (142130)Time elapsed: 0.188 s
% 0.33/33.97 % (142130)Peak memory usage: 462 MB
% 0.33/33.97 % (142130)Instructions burned: 150 (million)
% 0.33/33.97 % (142132)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4117284330:i=14155:bd=all_2747 on theBenchmark for (2747ds/14155Mi)
% 0.33/33.97 % (142112)Instruction limit reached!
% 0.33/33.97 % (142112)------------------------------
% 0.33/33.97 % (142112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142112)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142112)Termination reason: Instruction limit
% 0.33/33.97 % (142112)Termination phase: Saturation
% 0.33/33.97 % (142112)Time elapsed: 5.755 s
% 0.33/33.97 % (142112)Peak memory usage: 708 MB
% 0.33/33.97 % (142112)Instructions burned: 5202 (million)
% 0.33/33.97 % (142134)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3047805791:i=667:av=off:fsr=off_2718 on theBenchmark for (2718ds/667Mi)
% 0.33/33.97 % (142127)Instruction limit reached!
% 0.33/33.97 % (142127)------------------------------
% 0.33/33.97 % (142127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142127)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142127)Termination reason: Instruction limit
% 0.33/33.97 % (142127)Termination phase: Property scanning
% 0.33/33.97 % (142127)Time elapsed: 4.834 s
% 0.33/33.97 % (142127)Peak memory usage: 701 MB
% 0.33/33.97 % (142127)Instructions burned: 6060 (million)
% 0.33/33.97 % (142134)Instruction limit reached!
% 0.33/33.97 % (142134)------------------------------
% 0.33/33.97 % (142134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142134)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142134)Termination reason: Instruction limit
% 0.33/33.97 % (142134)Termination phase: Preprocessing 1
% 0.33/33.97 % (142134)Time elapsed: 0.881 s
% 0.33/33.97 % (142134)Peak memory usage: 463 MB
% 0.33/33.97 % (142134)Instructions burned: 667 (million)
% 0.33/33.97 % (142136)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3114211546:s2a=on:i=185:s2at=1.8:fdi=4_2707 on theBenchmark for (2707ds/185Mi)
% 0.33/33.97 % (142136)Instruction limit reached!
% 0.33/33.97 % (142136)------------------------------
% 0.33/33.97 % (142136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142136)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142136)Termination reason: Instruction limit
% 0.33/33.97 % (142136)Termination phase: SInE selection
% 0.33/33.97 % (142136)Time elapsed: 0.155 s
% 0.33/33.97 % (142136)Peak memory usage: 462 MB
% 0.33/33.97 % (142136)Instructions burned: 186 (million)
% 0.33/33.97 % (142137)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4123629306:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2706 on theBenchmark for (2706ds/193Mi)
% 0.33/33.97 % (142139)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=991300495:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2704 on theBenchmark for (2704ds/4850Mi)
% 0.33/33.97 % (142137)Instruction limit reached!
% 0.33/33.97 % (142137)------------------------------
% 0.33/33.97 % (142137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142137)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142137)Termination reason: Instruction limit
% 0.33/33.97 % (142137)Termination phase: SInE selection
% 0.33/33.97 % (142137)Time elapsed: 0.246 s
% 0.33/33.97 % (142137)Peak memory usage: 462 MB
% 0.33/33.97 % (142137)Instructions burned: 193 (million)
% 0.33/33.97 % (142142)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1963948030:i=12111:sd=1:ss=included_2701 on theBenchmark for (2701ds/12111Mi)
% 0.33/33.97 % (142139)First to succeed.
% 0.33/33.97 % (142139)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-142070"
% 0.33/33.97 % (142139)Refutation found. Thanks to Tanya!
% 0.33/33.97 % SZS status Theorem for theBenchmark
% 0.33/33.97 % SZS output start Proof for theBenchmark
% See solution above
% 0.33/33.97 % (142139)------------------------------
% 0.33/33.97 % (142139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.33/33.97 % (142139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/33.97 % (142139)CaDiCaL version: 2.1.3
% 0.33/33.97 % (142139)Termination reason: Refutation
% 0.33/33.97 % (142139)Time elapsed: 1.392 s
% 0.33/33.97 % (142139)Peak memory usage: 536 MB
% 0.33/33.97 % (142139)Instructions burned: 1623 (million)
% 0.33/33.97 % (142139)------------------------------
% 0.33/33.97 % (142139)------------------------------
% 0.33/33.97 % (142070)Success in time 31.987 s
% 0.33/33.97 % Vampire exiting
%------------------------------------------------------------------------------