%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR143_8 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:43:54 AM UTC 2026
% Result : CounterSatisfiable 70.68s 10.83s
% Output : Saturation 70.68s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u15,negated_conjecture,
~ holdsDuring_THFTYPE_IiooI(lYearFn_THFTYPE_IiiI(n2009_THFTYPE_i),$false) ).
cnf(u13,axiom,
( $true = X0
| $false = X0 ) ).
cnf(u16,negated_conjecture,
wife_THFTYPE_IiioI(lCorina_THFTYPE_i,lChris_THFTYPE_i) ).
cnf(u12,axiom,
$true != $false ).
cnf(u14,negated_conjecture,
~ husband_THFTYPE_IiioI(X0,lCorina_THFTYPE_i) ).
cnf(u7,axiom,
holdsDuring_THFTYPE_IiooI(X0,$true) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR143_8 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.22 % Computer : n016.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Mon Sep 28 23:42:34 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.26/0.28 Running first-order theorem proving
% 0.26/0.28 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.16/2.19 % (4149505)Detected formulas, will run a generic FOF schedule.
% 10.16/2.19 % (4149520)dis-21_1_sil=8000:lcm=predicate:random_seed=1990933544:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.16/2.19 % (4149520)Refutation not found, incomplete strategy
% 10.16/2.19 % (4149520)------------------------------
% 10.16/2.19 % (4149520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.19 % (4149520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.19 % (4149520)CaDiCaL version: 2.1.3
% 10.16/2.19 % (4149520)Termination reason: Refutation not found, incomplete strategy
% 10.16/2.19 % (4149520)Time elapsed: 0.002 s
% 10.16/2.19 % (4149520)Peak memory usage: 89 MB
% 10.16/2.19 % (4149516)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=2612685151:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.16/2.19 % (4149519)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3509145688:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.16/2.19 % (4149518)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3578436566:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.16/2.19 % (4149515)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=677942610:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.16/2.19 % (4149517)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2379406076:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.16/2.19 % (4149514)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=2780746489:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.16/2.19 % (4149517)Refutation not found, incomplete strategy
% 10.16/2.19 % (4149517)------------------------------
% 10.16/2.19 % (4149517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.19 % (4149517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.19 % (4149518)Refutation not found, incomplete strategy
% 10.16/2.19 % (4149518)------------------------------
% 10.16/2.19 % (4149518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.19 % (4149517)CaDiCaL version: 2.1.3
% 10.16/2.19 % (4149517)Termination reason: Refutation not found, incomplete strategy
% 10.16/2.19 % (4149517)Time elapsed: 0.001 s
% 10.16/2.19 % (4149517)Peak memory usage: 88 MB
% 10.16/2.19 % (4149518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.19 % (4149518)CaDiCaL version: 2.1.3
% 10.16/2.19 % (4149518)Termination reason: Refutation not found, incomplete strategy
% 10.16/2.19 % (4149518)Time elapsed: 0.002 s
% 10.16/2.19 % (4149518)Peak memory usage: 88 MB
% 10.16/2.19 % (4149519)Instruction limit reached!
% 10.16/2.19 % (4149519)------------------------------
% 10.16/2.19 % (4149519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.19 % (4149519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.19 % (4149519)CaDiCaL version: 2.1.3
% 10.16/2.19 % (4149519)Termination reason: Instruction limit
% 10.16/2.19 % (4149519)Termination phase: Saturation
% 10.16/2.19 % (4149519)Time elapsed: 0.106 s
% 10.16/2.19 % (4149519)Peak memory usage: 88 MB
% 10.16/2.19 % (4149519)Instructions burned: 140 (million)
% 10.16/2.19 % (4149520)------------------------------
% 10.16/2.19 % (4149520)------------------------------
% 10.16/2.19 % (4149528)lrs+10_1_sil=8000:sp=occurrence:random_seed=2220792722:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 10.16/2.19 % (4149518)------------------------------
% 10.16/2.19 % (4149518)------------------------------
% 10.16/2.19 % (4149529)lrs+10_1_sil=32000:urr=on:br=off:random_seed=102934809:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 10.16/2.19 % (4149517)------------------------------
% 10.16/2.19 % (4149517)------------------------------
% 10.16/2.19 % (4149528)Instruction limit reached!
% 10.16/2.19 % (4149528)------------------------------
% 10.16/2.19 % (4149528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.19 % (4149528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.99/2.80 % (4149528)CaDiCaL version: 2.1.3
% 13.99/2.80 % (4149528)Termination reason: Instruction limit
% 13.99/2.80 % (4149528)Termination phase: Saturation
% 13.99/2.80 % (4149528)Time elapsed: 0.068 s
% 13.99/2.80 % (4149528)Peak memory usage: 88 MB
% 13.99/2.80 % (4149528)Instructions burned: 288 (million)
% 13.99/2.80 % (4149529)Instruction limit reached!
% 13.99/2.80 % (4149529)------------------------------
% 13.99/2.80 % (4149529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.99/2.80 % (4149529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.99/2.80 % (4149529)CaDiCaL version: 2.1.3
% 13.99/2.80 % (4149529)Termination reason: Instruction limit
% 13.99/2.80 % (4149529)Termination phase: Saturation
% 13.99/2.80 % (4149529)Time elapsed: 0.069 s
% 13.99/2.80 % (4149529)Peak memory usage: 88 MB
% 13.99/2.80 % (4149529)Instructions burned: 158 (million)
% 13.99/2.80 % (4149541)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3762289721:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 13.99/2.80 % (4149541)Refutation not found, incomplete strategy
% 13.99/2.80 % (4149541)------------------------------
% 13.99/2.80 % (4149541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.99/2.80 % (4149541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.99/2.80 % (4149541)CaDiCaL version: 2.1.3
% 13.99/2.80 % (4149541)Termination reason: Refutation not found, incomplete strategy
% 13.99/2.80 % (4149541)Time elapsed: 0.001 s
% 13.99/2.80 % (4149541)Peak memory usage: 88 MB
% 13.99/2.80 % (4149539)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3947766774:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 13.99/2.80 % (4149540)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=3152293104:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 13.99/2.80 % (4149542)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3883896537:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 13.99/2.80 % (4149540)Instruction limit reached!
% 13.99/2.80 % (4149540)------------------------------
% 13.99/2.80 % (4149540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.99/2.80 % (4149540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.99/2.80 % (4149540)CaDiCaL version: 2.1.3
% 13.99/2.80 % (4149540)Termination reason: Instruction limit
% 13.99/2.80 % (4149540)Termination phase: Saturation
% 13.99/2.80 % (4149540)Time elapsed: 0.109 s
% 13.99/2.80 % (4149540)Peak memory usage: 89 MB
% 13.99/2.80 % (4149540)Instructions burned: 249 (million)
% 13.99/2.80 % (4149539)Instruction limit reached!
% 13.99/2.80 % (4149539)------------------------------
% 13.99/2.80 % (4149539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.99/2.80 % (4149539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.99/2.80 % (4149539)CaDiCaL version: 2.1.3
% 13.99/2.80 % (4149539)Termination reason: Instruction limit
% 13.99/2.80 % (4149539)Termination phase: Saturation
% 13.99/2.80 % (4149539)Time elapsed: 0.123 s
% 13.99/2.80 % (4149539)Peak memory usage: 88 MB
% 13.99/2.80 % (4149539)Instructions burned: 325 (million)
% 13.99/2.80 % (4149541)------------------------------
% 13.99/2.80 % (4149541)------------------------------
% 13.99/2.80 % (4149516)Refutation not found, incomplete strategy
% 13.99/2.80 % (4149516)------------------------------
% 13.99/2.80 % (4149516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.99/2.80 % (4149516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.99/2.80 % (4149516)CaDiCaL version: 2.1.3
% 13.99/2.80 % (4149516)Termination reason: Refutation not found, incomplete strategy
% 13.99/2.80 % (4149516)Time elapsed: 0.746 s
% 13.99/2.80 % (4149516)Peak memory usage: 128 MB
% 13.99/2.80 % (4149516)Instructions burned: 897 (million)
% 13.99/2.80 % (4149514)Refutation not found, incomplete strategy
% 13.99/2.80 % (4149514)------------------------------
% 13.99/2.80 % (4149514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.99/2.80 % (4149514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.99/2.80 % (4149514)CaDiCaL version: 2.1.3
% 13.99/2.80 % (4149514)Termination reason: Refutation not found, incomplete strategy
% 13.99/2.80 % (4149514)Time elapsed: 0.717 s
% 13.99/2.80 % (4149514)Peak memory usage: 128 MB
% 13.99/2.80 % (4149514)Instructions burned: 892 (million)
% 13.99/2.80 % (4149600)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1018085497:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 19.92/3.57 % (4149600)Refutation not found, incomplete strategy
% 19.92/3.57 % (4149600)------------------------------
% 19.92/3.57 % (4149600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.92/3.57 % (4149600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.57 % (4149600)CaDiCaL version: 2.1.3
% 19.92/3.57 % (4149600)Termination reason: Refutation not found, incomplete strategy
% 19.92/3.57 % (4149600)Time elapsed: 0.002 s
% 19.92/3.57 % (4149600)Peak memory usage: 89 MB
% 19.92/3.57 % (4149616)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1801490290:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 19.92/3.57 % (4149616)Refutation not found, incomplete strategy
% 19.92/3.57 % (4149616)------------------------------
% 19.92/3.57 % (4149616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.92/3.57 % (4149616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.57 % (4149616)CaDiCaL version: 2.1.3
% 19.92/3.57 % (4149616)Termination reason: Refutation not found, incomplete strategy
% 19.92/3.57 % (4149616)Time elapsed: 0.001 s
% 19.92/3.57 % (4149616)Peak memory usage: 88 MB
% 19.92/3.57 % (4149607)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2686436561:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 19.92/3.57 % (4149607)Refutation not found, incomplete strategy
% 19.92/3.57 % (4149607)------------------------------
% 19.92/3.57 % (4149607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.92/3.57 % (4149607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.57 % (4149607)CaDiCaL version: 2.1.3
% 19.92/3.57 % (4149607)Termination reason: Refutation not found, incomplete strategy
% 19.92/3.57 % (4149607)Time elapsed: 0.001 s
% 19.92/3.57 % (4149607)Peak memory usage: 88 MB
% 19.92/3.57 % (4149616)------------------------------
% 19.92/3.57 % (4149616)------------------------------
% 19.92/3.57 % (4149516)------------------------------
% 19.92/3.57 % (4149516)------------------------------
% 19.92/3.57 % (4149514)------------------------------
% 19.92/3.57 % (4149514)------------------------------
% 19.92/3.57 % (4149600)------------------------------
% 19.92/3.57 % (4149600)------------------------------
% 19.92/3.57 % (4149607)------------------------------
% 19.92/3.57 % (4149607)------------------------------
% 19.92/3.57 % (4149658)lrs+10_1_sil=8000:sp=occurrence:random_seed=1667750423:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 19.92/3.57 % (4149659)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=178262106:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 19.92/3.57 % (4149659)Refutation not found, incomplete strategy
% 19.92/3.57 % (4149659)------------------------------
% 19.92/3.57 % (4149659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.92/3.57 % (4149659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.57 % (4149659)CaDiCaL version: 2.1.3
% 19.92/3.57 % (4149659)Termination reason: Refutation not found, incomplete strategy
% 19.92/3.57 % (4149659)Time elapsed: 0.001 s
% 19.92/3.57 % (4149659)Peak memory usage: 88 MB
% 19.92/3.57 % (4149660)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3604256962:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 19.92/3.57 % (4149668)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=757874185:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 19.92/3.57 % (4149668)Refutation not found, incomplete strategy
% 19.92/3.57 % (4149668)------------------------------
% 19.92/3.57 % (4149668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.92/3.57 % (4149668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.57 % (4149668)CaDiCaL version: 2.1.3
% 19.92/3.57 % (4149668)Termination reason: Refutation not found, incomplete strategy
% 19.92/3.57 % (4149668)Time elapsed: 0.001 s
% 19.92/3.57 % (4149668)Peak memory usage: 89 MB
% 19.92/3.57 % (4149671)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2056772419:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 19.92/3.57 % (4149671)Refutation not found, incomplete strategy
% 19.92/3.57 % (4149671)------------------------------
% 29.23/5.03 % (4149671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.23/5.03 % (4149671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.23/5.03 % (4149671)CaDiCaL version: 2.1.3
% 29.23/5.03 % (4149671)Termination reason: Refutation not found, incomplete strategy
% 29.23/5.03 % (4149671)Time elapsed: 0.001 s
% 29.23/5.03 % (4149671)Peak memory usage: 88 MB
% 29.23/5.03 % (4149658)Instruction limit reached!
% 29.23/5.03 % (4149658)------------------------------
% 29.23/5.03 % (4149658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.23/5.03 % (4149658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.23/5.03 % (4149658)CaDiCaL version: 2.1.3
% 29.23/5.03 % (4149658)Termination reason: Instruction limit
% 29.23/5.03 % (4149658)Termination phase: Saturation
% 29.23/5.03 % (4149658)Time elapsed: 0.188 s
% 29.23/5.03 % (4149658)Peak memory usage: 89 MB
% 29.23/5.03 % (4149658)Instructions burned: 911 (million)
% 29.23/5.03 % (4149659)------------------------------
% 29.23/5.03 % (4149659)------------------------------
% 29.23/5.03 % (4149715)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3431427117:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 29.23/5.03 % (4149668)------------------------------
% 29.23/5.03 % (4149668)------------------------------
% 29.23/5.03 % (4149671)------------------------------
% 29.23/5.03 % (4149671)------------------------------
% 29.23/5.03 % (4149716)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=133331962:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 29.23/5.03 % (4149716)Refutation not found, incomplete strategy
% 29.23/5.03 % (4149716)------------------------------
% 29.23/5.03 % (4149716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.23/5.03 % (4149716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.23/5.03 % (4149716)CaDiCaL version: 2.1.3
% 29.23/5.03 % (4149716)Termination reason: Refutation not found, incomplete strategy
% 29.23/5.03 % (4149716)Time elapsed: 0.003 s
% 29.23/5.03 % (4149716)Peak memory usage: 89 MB
% 29.23/5.03 % (4149716)Instructions burned: 2 (million)
% 29.23/5.03 % (4149718)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2297928406:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 29.23/5.03 % (4149719)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=656425243:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 29.23/5.03 % (4149719)Refutation not found, incomplete strategy
% 29.23/5.03 % (4149719)------------------------------
% 29.23/5.03 % (4149719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.23/5.03 % (4149719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.23/5.03 % (4149719)CaDiCaL version: 2.1.3
% 29.23/5.03 % (4149719)Termination reason: Refutation not found, incomplete strategy
% 29.23/5.03 % (4149719)Time elapsed: 0.001 s
% 29.23/5.03 % (4149719)Peak memory usage: 88 MB
% 29.23/5.03 % (4149718)Instruction limit reached!
% 29.23/5.03 % (4149718)------------------------------
% 29.23/5.03 % (4149718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.23/5.03 % (4149718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.23/5.03 % (4149718)CaDiCaL version: 2.1.3
% 29.23/5.03 % (4149718)Termination reason: Instruction limit
% 29.23/5.03 % (4149718)Termination phase: Saturation
% 29.23/5.03 % (4149718)Time elapsed: 0.059 s
% 29.23/5.03 % (4149718)Peak memory usage: 88 MB
% 29.23/5.03 % (4149718)Instructions burned: 136 (million)
% 29.23/5.03 % (4149716)------------------------------
% 29.23/5.03 % (4149716)------------------------------
% 29.23/5.03 % (4149542)Instruction limit reached!
% 29.23/5.03 % (4149542)------------------------------
% 29.23/5.03 % (4149542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.23/5.03 % (4149542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.23/5.03 % (4149542)CaDiCaL version: 2.1.3
% 29.23/5.03 % (4149542)Termination reason: Instruction limit
% 29.23/5.03 % (4149542)Termination phase: Saturation
% 29.23/5.03 % (4149542)Time elapsed: 1.191 s
% 29.23/5.03 % (4149542)Peak memory usage: 129 MB
% 29.23/5.03 % (4149542)Instructions burned: 2352 (million)
% 29.23/5.03 % (4149723)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3561498013:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 40.89/6.58 % (4149723)Refutation not found, incomplete strategy
% 40.89/6.58 % (4149723)------------------------------
% 40.89/6.58 % (4149723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.89/6.58 % (4149723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.89/6.58 % (4149723)CaDiCaL version: 2.1.3
% 40.89/6.58 % (4149723)Termination reason: Refutation not found, incomplete strategy
% 40.89/6.58 % (4149723)Time elapsed: 0.001 s
% 40.89/6.58 % (4149723)Peak memory usage: 88 MB
% 40.89/6.58 % (4149719)------------------------------
% 40.89/6.58 % (4149719)------------------------------
% 40.89/6.58 % (4149724)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=2096344454:i=6060:aac=none:ins=25_2979 on theBenchmark for (2979ds/6060Mi)
% 40.89/6.58 % (4149725)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=3108641939:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2979 on theBenchmark for (2979ds/150Mi)
% 40.89/6.58 % (4149727)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=523721461:i=14155:bd=all_2978 on theBenchmark for (2978ds/14155Mi)
% 40.89/6.58 % (4149725)Instruction limit reached!
% 40.89/6.58 % (4149725)------------------------------
% 40.89/6.58 % (4149725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.89/6.58 % (4149725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.89/6.58 % (4149725)CaDiCaL version: 2.1.3
% 40.89/6.58 % (4149725)Termination reason: Instruction limit
% 40.89/6.58 % (4149725)Termination phase: Saturation
% 40.89/6.58 % (4149725)Time elapsed: 0.066 s
% 40.89/6.58 % (4149725)Peak memory usage: 89 MB
% 40.89/6.58 % (4149725)Instructions burned: 151 (million)
% 40.89/6.58 % (4149723)------------------------------
% 40.89/6.58 % (4149723)------------------------------
% 40.89/6.58 % (4149731)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1291806160:i=667:av=off:fsr=off_2977 on theBenchmark for (2977ds/667Mi)
% 40.89/6.58 % (4149731)Refutation not found, incomplete strategy
% 40.89/6.58 % (4149731)------------------------------
% 40.89/6.58 % (4149731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.89/6.58 % (4149731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.89/6.58 % (4149731)CaDiCaL version: 2.1.3
% 40.89/6.58 % (4149731)Termination reason: Refutation not found, incomplete strategy
% 40.89/6.58 % (4149731)Time elapsed: 0.001 s
% 40.89/6.58 % (4149731)Peak memory usage: 88 MB
% 40.89/6.58 % (4149732)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=234087075:s2a=on:i=185:s2at=1.8:fdi=4_2976 on theBenchmark for (2976ds/185Mi)
% 40.89/6.58 % (4149732)Refutation not found, incomplete strategy
% 40.89/6.58 % (4149732)------------------------------
% 40.89/6.58 % (4149732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.89/6.58 % (4149732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.89/6.58 % (4149732)CaDiCaL version: 2.1.3
% 40.89/6.58 % (4149732)Termination reason: Refutation not found, incomplete strategy
% 40.89/6.58 % (4149732)Time elapsed: 0.002 s
% 40.89/6.58 % (4149732)Peak memory usage: 89 MB
% 40.89/6.58 % (4149731)------------------------------
% 40.89/6.58 % (4149731)------------------------------
% 40.89/6.58 % (4149732)------------------------------
% 40.89/6.58 % (4149732)------------------------------
% 40.89/6.58 % (4149735)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2734021660:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2973 on theBenchmark for (2973ds/193Mi)
% 40.89/6.58 % (4149735)Refutation not found, incomplete strategy
% 40.89/6.58 % (4149735)------------------------------
% 40.89/6.58 % (4149735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.89/6.58 % (4149735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.89/6.58 % (4149735)CaDiCaL version: 2.1.3
% 40.89/6.58 % (4149735)Termination reason: Refutation not found, incomplete strategy
% 40.89/6.58 % (4149735)Time elapsed: 0.001 s
% 40.89/6.58 % (4149735)Peak memory usage: 88 MB
% 61.79/9.44 % (4149736)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3017468915:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2972 on theBenchmark for (2972ds/4850Mi)
% 61.79/9.44 % (4149736)Refutation not found, incomplete strategy
% 61.79/9.44 % (4149736)------------------------------
% 61.79/9.44 % (4149736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.79/9.44 % (4149736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.79/9.44 % (4149736)CaDiCaL version: 2.1.3
% 61.79/9.44 % (4149736)Termination reason: Refutation not found, incomplete strategy
% 61.79/9.44 % (4149736)Time elapsed: 0.001 s
% 61.79/9.44 % (4149736)Peak memory usage: 88 MB
% 61.79/9.44 % (4149735)------------------------------
% 61.79/9.44 % (4149735)------------------------------
% 61.79/9.44 % (4149736)------------------------------
% 61.79/9.44 % (4149736)------------------------------
% 61.79/9.44 % (4149739)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3826839626:i=12111:sd=1:ss=included_2969 on theBenchmark for (2969ds/12111Mi)
% 61.79/9.44 % (4149740)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2698484348:i=319:kws=precedence:fsr=off_2968 on theBenchmark for (2968ds/319Mi)
% 61.79/9.44 % (4149740)Instruction limit reached!
% 61.79/9.44 % (4149740)------------------------------
% 61.79/9.44 % (4149740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.79/9.44 % (4149740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.79/9.44 % (4149740)CaDiCaL version: 2.1.3
% 61.79/9.44 % (4149740)Termination reason: Instruction limit
% 61.79/9.44 % (4149740)Termination phase: Saturation
% 61.79/9.44 % (4149740)Time elapsed: 0.126 s
% 61.79/9.44 % (4149740)Peak memory usage: 89 MB
% 61.79/9.44 % (4149740)Instructions burned: 322 (million)
% 61.79/9.44 % (4149743)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4005164173:i=2064:ep=RST_2966 on theBenchmark for (2966ds/2064Mi)
% 61.79/9.44 % (4149743)Refutation not found, incomplete strategy
% 61.79/9.44 % (4149743)------------------------------
% 61.79/9.44 % (4149743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.79/9.44 % (4149743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.79/9.44 % (4149743)CaDiCaL version: 2.1.3
% 61.79/9.44 % (4149743)Termination reason: Refutation not found, incomplete strategy
% 61.79/9.44 % (4149743)Time elapsed: 0.001 s
% 61.79/9.44 % (4149743)Peak memory usage: 88 MB
% 61.79/9.44 % (4149743)------------------------------
% 61.79/9.44 % (4149743)------------------------------
% 61.79/9.44 % (4149660)Instruction limit reached!
% 61.79/9.44 % (4149660)------------------------------
% 61.79/9.44 % (4149660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.79/9.44 % (4149660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.79/9.44 % (4149660)CaDiCaL version: 2.1.3
% 61.79/9.44 % (4149660)Termination reason: Instruction limit
% 61.79/9.44 % (4149660)Termination phase: Saturation
% 61.79/9.44 % (4149660)Time elapsed: 2.463 s
% 61.79/9.44 % (4149660)Peak memory usage: 130 MB
% 61.79/9.44 % (4149660)Instructions burned: 5203 (million)
% 61.79/9.44 % (4149745)dis-1011_128_sil=32000:random_seed=2750939526:i=3706:ep=RST:av=off_2962 on theBenchmark for (2962ds/3706Mi)
% 61.79/9.44 % (4149746)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4110403068:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2961 on theBenchmark for (2961ds/757Mi)
% 61.79/9.44 % (4149746)Refutation not found, incomplete strategy
% 61.79/9.44 % (4149746)------------------------------
% 61.79/9.44 % (4149746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.79/9.44 % (4149746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.79/9.44 % (4149746)CaDiCaL version: 2.1.3
% 61.79/9.44 % (4149746)Termination reason: Refutation not found, incomplete strategy
% 61.79/9.44 % (4149746)Time elapsed: 0.001 s
% 61.79/9.44 % (4149746)Peak memory usage: 88 MB
% 61.79/9.44 % (4149746)------------------------------
% 61.79/9.44 % (4149746)------------------------------
% 61.79/9.44 % (4149715)Instruction limit reached!
% 61.79/9.44 % (4149715)------------------------------
% 61.79/9.44 % (4149715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.79/9.44 % (4149715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.79/9.44 % (4149715)CaDiCaL version: 2.1.3
% 68.20/10.42 % (4149715)Termination reason: Instruction limit
% 68.20/10.42 % (4149715)Termination phase: Saturation
% 68.20/10.42 % (4149715)Time elapsed: 2.667 s
% 68.20/10.42 % (4149715)Peak memory usage: 130 MB
% 68.20/10.42 % (4149715)Instructions burned: 13199 (million)
% 68.20/10.42 % (4149749)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=835185243:i=13913:ss=axioms:sgt=8_2957 on theBenchmark for (2957ds/13913Mi)
% 68.20/10.42 % (4149750)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1770678863:i=9925:aac=none_2957 on theBenchmark for (2957ds/9925Mi)
% 68.20/10.42 % (4149750)Refutation not found, incomplete strategy
% 68.20/10.42 % (4149750)------------------------------
% 68.20/10.42 % (4149750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.20/10.42 % (4149750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.20/10.42 % (4149750)CaDiCaL version: 2.1.3
% 68.20/10.42 % (4149750)Termination reason: Refutation not found, incomplete strategy
% 68.20/10.42 % (4149750)Time elapsed: 0.348 s
% 68.20/10.42 % (4149750)Peak memory usage: 128 MB
% 68.20/10.42 % (4149750)Instructions burned: 898 (million)
% 68.20/10.42 % (4149750)------------------------------
% 68.20/10.42 % (4149750)------------------------------
% 68.20/10.42 % (4149753)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3418725105:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2950 on theBenchmark for (2950ds/2479Mi)
% 68.20/10.42 % (4149753)Refutation not found, incomplete strategy
% 68.20/10.42 % (4149753)------------------------------
% 68.20/10.42 % (4149753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.20/10.42 % (4149753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.20/10.42 % (4149753)CaDiCaL version: 2.1.3
% 68.20/10.42 % (4149753)Termination reason: Refutation not found, incomplete strategy
% 68.20/10.42 % (4149753)Time elapsed: 0.001 s
% 68.20/10.42 % (4149753)Peak memory usage: 88 MB
% 68.20/10.42 % (4149753)------------------------------
% 68.20/10.42 % (4149753)------------------------------
% 68.20/10.42 % (4149724)Instruction limit reached!
% 68.20/10.42 % (4149724)------------------------------
% 68.20/10.42 % (4149724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.20/10.42 % (4149724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.20/10.42 % (4149724)CaDiCaL version: 2.1.3
% 68.20/10.42 % (4149724)Termination reason: Instruction limit
% 68.20/10.42 % (4149724)Termination phase: Saturation
% 68.20/10.42 % (4149724)Time elapsed: 3.059 s
% 68.20/10.42 % (4149724)Peak memory usage: 129 MB
% 68.20/10.42 % (4149724)Instructions burned: 6060 (million)
% 68.20/10.42 % (4149755)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1431102331:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2948 on theBenchmark for (2948ds/440Mi)
% 68.20/10.42 % (4149756)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=398445256:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2947 on theBenchmark for (2947ds/11145Mi)
% 68.20/10.42 % (4149755)Instruction limit reached!
% 68.20/10.42 % (4149755)------------------------------
% 68.20/10.42 % (4149755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.20/10.42 % (4149755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.20/10.42 % (4149755)CaDiCaL version: 2.1.3
% 68.20/10.42 % (4149755)Termination reason: Instruction limit
% 68.20/10.42 % (4149755)Termination phase: Saturation
% 68.20/10.42 % (4149755)Time elapsed: 0.105 s
% 68.20/10.42 % (4149755)Peak memory usage: 88 MB
% 68.20/10.42 % (4149755)Instructions burned: 443 (million)
% 68.20/10.42 % (4149759)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1010512730:cts=off:i=3034:av=off:er=known:fsd=on_2945 on theBenchmark for (2945ds/3034Mi)
% 68.20/10.42 % (4149745)Instruction limit reached!
% 68.20/10.42 % (4149745)------------------------------
% 68.20/10.42 % (4149745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.20/10.42 % (4149745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.20/10.42 % (4149745)CaDiCaL version: 2.1.3
% 68.20/10.42 % (4149745)Termination reason: Instruction limit
% 68.20/10.42 % (4149745)Termination phase: Saturation
% 68.20/10.42 % (4149745)Time elapsed: 1.748 s
% 68.20/10.42 % (4149745)Peak memory usage: 89 MB
% 68.20/10.42 % (4149745)Instructions burned: 3708 (million)
% 68.20/10.42 % (4149761)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1094646653:st=2:s2a=on:i=524:s2at=2:ss=axioms_2943 on theBenchmark for (2943ds/524Mi)
% 70.68/10.83 % (4149761)Refutation not found, incomplete strategy
% 70.68/10.83 % (4149761)------------------------------
% 70.68/10.83 % (4149761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149761)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149761)Termination reason: Refutation not found, incomplete strategy
% 70.68/10.83 % (4149761)Time elapsed: 0.039 s
% 70.68/10.83 % (4149761)Peak memory usage: 89 MB
% 70.68/10.83 % (4149761)Instructions burned: 90 (million)
% 70.68/10.83 % (4149761)------------------------------
% 70.68/10.83 % (4149761)------------------------------
% 70.68/10.83 % (4149763)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=4263622729:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2938 on theBenchmark for (2938ds/1016Mi)
% 70.68/10.83 % (4149763)Refutation not found, incomplete strategy
% 70.68/10.83 % (4149763)------------------------------
% 70.68/10.83 % (4149763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149763)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149763)Termination reason: Refutation not found, incomplete strategy
% 70.68/10.83 % (4149763)Time elapsed: 0.001 s
% 70.68/10.83 % (4149763)Peak memory usage: 89 MB
% 70.68/10.83 % (4149763)------------------------------
% 70.68/10.83 % (4149763)------------------------------
% 70.68/10.83 % (4149759)Instruction limit reached!
% 70.68/10.83 % (4149759)------------------------------
% 70.68/10.83 % (4149759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149759)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149759)Termination reason: Instruction limit
% 70.68/10.83 % (4149759)Termination phase: Saturation
% 70.68/10.83 % (4149759)Time elapsed: 0.943 s
% 70.68/10.83 % (4149759)Peak memory usage: 128 MB
% 70.68/10.83 % (4149759)Instructions burned: 3037 (million)
% 70.68/10.83 % (4149765)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1241088545:i=14123:bd=preordered:ins=4_2934 on theBenchmark for (2934ds/14123Mi)
% 70.68/10.83 % (4149766)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2361339586:i=5781:kws=precedence:bd=all:rawr=on_2934 on theBenchmark for (2934ds/5781Mi)
% 70.68/10.83 % (4149727)Instruction limit reached!
% 70.68/10.83 % (4149727)------------------------------
% 70.68/10.83 % (4149727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149727)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149727)Termination reason: Instruction limit
% 70.68/10.83 % (4149727)Termination phase: Saturation
% 70.68/10.83 % (4149727)Time elapsed: 5.073 s
% 70.68/10.83 % (4149727)Peak memory usage: 130 MB
% 70.68/10.83 % (4149727)Instructions burned: 14156 (million)
% 70.68/10.83 % (4149769)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=3874131610:i=2448:gtgl=5:bd=preordered:gtg=all_2926 on theBenchmark for (2926ds/2448Mi)
% 70.68/10.83 % (4149739)Instruction limit reached!
% 70.68/10.83 % (4149739)------------------------------
% 70.68/10.83 % (4149739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149739)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149739)Termination reason: Instruction limit
% 70.68/10.83 % (4149739)Termination phase: Saturation
% 70.68/10.83 % (4149739)Time elapsed: 4.489 s
% 70.68/10.83 % (4149739)Peak memory usage: 131 MB
% 70.68/10.83 % (4149739)Instructions burned: 12113 (million)
% 70.68/10.83 % (4149771)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=692148984:i=3223:kws=precedence:fgj=on:av=off_2922 on theBenchmark for (2922ds/3223Mi)
% 70.68/10.83 % (4149769)Instruction limit reached!
% 70.68/10.83 % (4149769)------------------------------
% 70.68/10.83 % (4149769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149769)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149769)Termination reason: Instruction limit
% 70.68/10.83 % (4149769)Termination phase: Saturation
% 70.68/10.83 % (4149769)Time elapsed: 1.195 s
% 70.68/10.83 % (4149769)Peak memory usage: 129 MB
% 70.68/10.83 % (4149769)Instructions burned: 2448 (million)
% 70.68/10.83 % (4149773)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1680447693:st=5.6:i=2033:sd=3:ss=axioms_2913 on theBenchmark for (2913ds/2033Mi)
% 70.68/10.83 % (4149766)Instruction limit reached!
% 70.68/10.83 % (4149766)------------------------------
% 70.68/10.83 % (4149766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149766)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149766)Termination reason: Instruction limit
% 70.68/10.83 % (4149766)Termination phase: Saturation
% 70.68/10.83 % (4149766)Time elapsed: 2.389 s
% 70.68/10.83 % (4149766)Peak memory usage: 93 MB
% 70.68/10.83 % (4149766)Instructions burned: 5783 (million)
% 70.68/10.83 % (4149775)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2504749165:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2909 on theBenchmark for (2909ds/2055Mi)
% 70.68/10.83 % (4149765)Instruction limit reached!
% 70.68/10.83 % (4149765)------------------------------
% 70.68/10.83 % (4149765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149765)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149765)Termination reason: Instruction limit
% 70.68/10.83 % (4149765)Termination phase: Saturation
% 70.68/10.83 % (4149765)Time elapsed: 2.703 s
% 70.68/10.83 % (4149765)Peak memory usage: 129 MB
% 70.68/10.83 % (4149765)Instructions burned: 14129 (million)
% 70.68/10.83 % (4149771)Instruction limit reached!
% 70.68/10.83 % (4149771)------------------------------
% 70.68/10.83 % (4149771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149771)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149771)Termination reason: Instruction limit
% 70.68/10.83 % (4149771)Termination phase: Saturation
% 70.68/10.83 % (4149771)Time elapsed: 1.479 s
% 70.68/10.83 % (4149771)Peak memory usage: 129 MB
% 70.68/10.83 % (4149771)Instructions burned: 3225 (million)
% 70.68/10.83 % (4149773)Refutation not found, incomplete strategy
% 70.68/10.83 % (4149773)------------------------------
% 70.68/10.83 % (4149773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149773)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149773)Termination reason: Refutation not found, incomplete strategy
% 70.68/10.83 % (4149773)Time elapsed: 0.554 s
% 70.68/10.83 % (4149773)Peak memory usage: 128 MB
% 70.68/10.83 % (4149773)Instructions burned: 894 (million)
% 70.68/10.83 % (4149777)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=2554007885:i=21611:sd=3:ss=axioms_2906 on theBenchmark for (2906ds/21611Mi)
% 70.68/10.83 % (4149778)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1654936184:i=4835:sd=13:ss=axioms:sgt=23_2906 on theBenchmark for (2906ds/4835Mi)
% 70.68/10.83 % (4149778)Refutation not found, incomplete strategy
% 70.68/10.83 % (4149778)------------------------------
% 70.68/10.83 % (4149778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149778)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149778)Termination reason: Refutation not found, incomplete strategy
% 70.68/10.83 % (4149778)Time elapsed: 0.002 s
% 70.68/10.83 % (4149778)Peak memory usage: 88 MB
% 70.68/10.83 % (4149778)Instructions burned: 1 (million)
% 70.68/10.83 % (4149773)------------------------------
% 70.68/10.83 % (4149773)------------------------------
% 70.68/10.83 % (4149756)Instruction limit reached!
% 70.68/10.83 % (4149756)------------------------------
% 70.68/10.83 % (4149756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149756)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149756)Termination reason: Instruction limit
% 70.68/10.83 % (4149756)Termination phase: Saturation
% 70.68/10.83 % (4149756)Time elapsed: 4.283 s
% 70.68/10.83 % (4149756)Peak memory usage: 133 MB
% 70.68/10.83 % (4149756)Instructions burned: 11146 (million)
% 70.68/10.83 % (4149781)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=3797768477:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2904 on theBenchmark for (2904ds/797Mi)
% 70.68/10.83 % (4149781)First to succeed.
% 70.68/10.83 % (4149781)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4149505"
% 70.68/10.83 % (4149778)------------------------------
% 70.68/10.83 % (4149778)------------------------------
% 70.68/10.83 % (4149775)Refutation not found, incomplete strategy
% 70.68/10.83 % (4149775)------------------------------
% 70.68/10.83 % (4149775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149775)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149775)Termination reason: Refutation not found, incomplete strategy
% 70.68/10.83 % (4149775)Time elapsed: 0.578 s
% 70.68/10.83 % (4149775)Peak memory usage: 128 MB
% 70.68/10.83 % (4149775)Instructions burned: 855 (million)
% 70.68/10.83 % (4149749)Instruction limit reached!
% 70.68/10.83 % (4149749)------------------------------
% 70.68/10.83 % (4149749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149749)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149749)Termination reason: Instruction limit
% 70.68/10.83 % (4149749)Termination phase: Saturation
% 70.68/10.83 % (4149749)Time elapsed: 5.466 s
% 70.68/10.83 % (4149749)Peak memory usage: 130 MB
% 70.68/10.83 % (4149749)Instructions burned: 13916 (million)
% 70.68/10.83 % (4149782)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3852957925:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2903 on theBenchmark for (2903ds/2326Mi)
% 70.68/10.83 % (4149782)Refutation not found, incomplete strategy
% 70.68/10.83 % (4149782)------------------------------
% 70.68/10.83 % (4149782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149782)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149782)Termination reason: Refutation not found, incomplete strategy
% 70.68/10.83 % (4149782)Time elapsed: 0.002 s
% 70.68/10.83 % (4149782)Peak memory usage: 88 MB
% 70.68/10.83 % SZS status CounterSatisfiable for theBenchmark
% 70.68/10.83 % SZS output start Saturation.
% See solution above
% 70.68/10.83 % SZS output start Definitions and Model Updates.
% 70.68/10.83 % SZS output end Definitions and Model Updates.
% 70.68/10.83 % (4149781)------------------------------
% 70.68/10.83 % (4149781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/10.83 % (4149781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/10.83 % (4149781)CaDiCaL version: 2.1.3
% 70.68/10.83 % (4149781)Termination reason: Satisfiable
% 70.68/10.83 % (4149781)Time elapsed: 0.001 s
% 70.68/10.83 % (4149781)Peak memory usage: 88 MB
% 70.68/10.83 % (4149781)------------------------------
% 70.68/10.83 % (4149781)------------------------------
% 70.68/10.83 % (4149505)Success in time 9.879 s
% 70.68/10.83 % Vampire exiting
%------------------------------------------------------------------------------