%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL100-1 : TPTP v9.3.1. Released v1.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 11:51:11 AM UTC 2026
% Result : Unsatisfiable 72.55s 11.76s
% Output : Refutation 72.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 4
% Syntax : Number of formulae : 39 ( 38 unt; 0 def)
% Number of atoms : 41 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 12 ( 10 ~; 2 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 134 ( 134 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X3,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X0,X1),equivalent(X0,X2)),equivalent(X1,X2)),X3),X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lg_2) ).
fof(f3,axiom,
! [X2,X3,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X2),equivalent(equivalent(X3,X1),equivalent(equivalent(X0,X3),X2)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p_1) ).
fof(f4,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,c)),e),equivalent(equivalent(b,c),e)),falsehood),falsehood)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_lg_3) ).
fof(f9,plain,
! [X2,X3,X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(equivalent(equivalent(X1,X3),X0),equivalent(X3,X2)))),
inference(unit_resulting_resolution,[],[f1,f3,f2]) ).
fof(f11,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(equivalent(equivalent(X2,X3),equivalent(X2,X4)),equivalent(X3,X4)),X0),X1))),
inference(unit_resulting_resolution,[],[f1,f3,f2]) ).
fof(f12,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X1),X2),equivalent(equivalent(X3,X1),X4)),equivalent(X2,equivalent(equivalent(X3,X0),X4)))),
inference(unit_resulting_resolution,[],[f1,f3,f9]) ).
fof(f14,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X0,X1),X2),X3),equivalent(X2,equivalent(X0,X4))),equivalent(X3,equivalent(X1,X4)))),
inference(unit_resulting_resolution,[],[f1,f9,f9]) ).
fof(f19,plain,
! [X2,X3,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X0),X3)),equivalent(equivalent(X2,X1),X3))),
inference(unit_resulting_resolution,[],[f1,f2,f14]) ).
fof(f21,plain,
! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X0,X2)),equivalent(X1,X2))),
inference(unit_resulting_resolution,[],[f1,f2,f14]) ).
fof(f25,plain,
! [X0,X1] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X1),X0))),
inference(unit_resulting_resolution,[],[f1,f3,f21]) ).
fof(f41,plain,
! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X0),X1),X2),equivalent(X1,X2))),
inference(unit_resulting_resolution,[],[f1,f9,f25]) ).
fof(f44,plain,
! [X2,X0,X1] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X1),X0)))),
inference(unit_resulting_resolution,[],[f1,f3,f41]) ).
fof(f45,plain,
! [X0,X1] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X0,X1))),
inference(unit_resulting_resolution,[],[f1,f21,f41]) ).
fof(f68,plain,
! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X0),equivalent(X2,X1)))),
inference(unit_resulting_resolution,[],[f1,f3,f45]) ).
fof(f142,plain,
! [X2,X3,X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(X1,X3))),equivalent(X0,equivalent(X2,X3)))),
inference(unit_resulting_resolution,[],[f1,f21,f68]) ).
fof(f205,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(X1,X3))),equivalent(equivalent(X4,X0),equivalent(X4,equivalent(X2,X3))))),
inference(unit_resulting_resolution,[],[f1,f3,f142]) ).
fof(f329,plain,
! [X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(X0,X0),X1),X1)),
inference(unit_resulting_resolution,[],[f1,f21,f19]) ).
fof(f330,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,X2),X3)),equivalent(equivalent(equivalent(X2,X4),X0),equivalent(equivalent(X1,X4),X3)))),
inference(unit_resulting_resolution,[],[f1,f3,f19]) ).
fof(f364,plain,
! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(X2,X2),X0),X1))),
inference(unit_resulting_resolution,[],[f1,f3,f329]) ).
fof(f374,plain,
! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,X1),X2)),equivalent(X0,X2))),
inference(unit_resulting_resolution,[],[f1,f68,f329]) ).
fof(f469,plain,
! [X2,X3,X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,X1),X2)),equivalent(equivalent(X3,X0),equivalent(X3,X2)))),
inference(unit_resulting_resolution,[],[f1,f3,f374]) ).
fof(f486,plain,
! [X2,X3,X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X1),X3))),equivalent(X0,X3))),
inference(unit_resulting_resolution,[],[f1,f19,f469]) ).
fof(f675,plain,
! [X2,X3,X0,X1,X4,X5] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,X2),X3)),equivalent(equivalent(equivalent(equivalent(X4,X2),X5),X0),equivalent(X5,equivalent(equivalent(X1,X4),X3))))),
inference(unit_resulting_resolution,[],[f1,f3,f12]) ).
fof(f1020,plain,
! [X2,X3,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X1),X2),X3),equivalent(X2,equivalent(equivalent(X1,X0),X3)))),
inference(unit_resulting_resolution,[],[f1,f9,f44]) ).
fof(f1026,plain,
! [X2,X3,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(X0,X0),X1),equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X2),X1)))),
inference(unit_resulting_resolution,[],[f1,f364,f44]) ).
fof(f1692,plain,
! [X2,X3,X0,X1,X4,X5] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X0,X1),X2),X3),equivalent(X2,equivalent(equivalent(X4,X0),X5))),equivalent(X3,equivalent(equivalent(X4,X1),X5)))),
inference(unit_resulting_resolution,[],[f1,f9,f330]) ).
fof(f4372,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X1),X2),equivalent(equivalent(X3,X3),X4)),equivalent(X2,equivalent(equivalent(X1,X0),X4)))),
inference(unit_resulting_resolution,[],[f1,f9,f1026]) ).
fof(f5298,plain,
! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,c)),e),equivalent(equivalent(b,c),e)),falsehood),equivalent(equivalent(X0,X1),equivalent(equivalent(X1,X0),falsehood)))),
inference(unit_resulting_resolution,[],[f1,f4,f486]) ).
fof(f5963,plain,
! [X2,X3,X0,X1,X4,X5] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X1),X2),equivalent(X1,equivalent(X3,X4))),equivalent(X2,equivalent(equivalent(equivalent(X3,X5),X0),equivalent(X5,X4))))),
inference(unit_resulting_resolution,[],[f1,f9,f675]) ).
fof(f14934,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X1),X3)),X4)),equivalent(X0,equivalent(X3,X4)))),
inference(unit_resulting_resolution,[],[f1,f1020,f205]) ).
fof(f15349,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(equivalent(X1,X2),X3)),X4),equivalent(X3,equivalent(equivalent(X0,equivalent(X2,X1)),X4)))),
inference(unit_resulting_resolution,[],[f1,f3,f14934]) ).
fof(f35800,plain,
~ is_a_theorem(equivalent(falsehood,equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,c)),e),equivalent(equivalent(e,equivalent(b,c)),falsehood)))),
inference(unit_resulting_resolution,[],[f1,f9,f5298]) ).
fof(f36083,plain,
! [X0] : ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X0),falsehood),equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,c)),e),equivalent(equivalent(e,equivalent(b,c)),falsehood)))),
inference(unit_resulting_resolution,[],[f1,f41,f35800]) ).
fof(f40318,plain,
! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(e,equivalent(equivalent(a,b),equivalent(a,c))),equivalent(equivalent(X0,X0),falsehood)),equivalent(equivalent(X1,X1),equivalent(equivalent(e,equivalent(b,c)),falsehood)))),
inference(unit_resulting_resolution,[],[f1,f4372,f36083]) ).
fof(f40626,plain,
! [X2,X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,equivalent(e,equivalent(b,c))),X1),equivalent(equivalent(e,equivalent(equivalent(a,b),equivalent(a,c))),equivalent(equivalent(X2,X2),falsehood))),equivalent(X1,equivalent(X0,falsehood)))),
inference(unit_resulting_resolution,[],[f1,f5963,f40318]) ).
fof(f41039,plain,
! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(e,equivalent(equivalent(a,b),equivalent(a,c))),equivalent(equivalent(X0,X0),falsehood)),equivalent(equivalent(X1,equivalent(b,c)),equivalent(equivalent(e,X1),falsehood)))),
inference(unit_resulting_resolution,[],[f1,f11,f40626]) ).
fof(f41288,plain,
! [X2,X3,X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,equivalent(b,c)),X1),equivalent(equivalent(e,equivalent(equivalent(a,b),equivalent(a,c))),equivalent(equivalent(X2,X2),falsehood))),equivalent(X1,equivalent(equivalent(X3,X0),equivalent(equivalent(e,X3),falsehood))))),
inference(unit_resulting_resolution,[],[f1,f1692,f41039]) ).
fof(f41711,plain,
$false,
inference(unit_resulting_resolution,[],[f1,f15349,f11,f41288]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL100-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.22/0.48 % Computer : n016.cluster.edu
% 0.22/0.48 % Model : x86_64 x86_64
% 0.22/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.48 % Memory : 8046.5625MB
% 0.22/0.48 % OS : Linux 6.8.0-71-generic
% 0.22/0.48 % CPULimit : 300
% 0.22/0.48 % WCLimit : 300
% 0.22/0.48 % DateTime : Sun Sep 27 15:26:17 UTC 2026
% 0.22/0.48 % CPUTime :
% 0.22/0.48 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.27/0.54 Running first-order theorem proving
% 0.27/0.54 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
% 18.94/3.97 % (2776373)Input is clausal, will run a generic CNF schedule.
% 18.94/3.97 % (2776379)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2848826189:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.94/3.97 % (2776378)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=2777395550:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.94/3.97 % (2776381)lrs+10_1_sil=8000:sp=occurrence:random_seed=3020423334:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.94/3.97 % (2776380)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=791224205:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.94/3.97 % (2776382)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4278929974:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.94/3.97 % (2776384)dis-21_1_sil=8000:lcm=predicate:random_seed=2228446450:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 18.94/3.97 % (2776383)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3625452651:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.94/3.97 % (2776381)Instruction limit reached!
% 18.94/3.97 % (2776381)------------------------------
% 18.94/3.97 % (2776381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.94/3.97 % (2776381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.94/3.97 % (2776381)CaDiCaL version: 2.1.3
% 18.94/3.97 % (2776381)Termination reason: Instruction limit
% 18.94/3.97 % (2776381)Termination phase: Saturation
% 18.94/3.97 % (2776381)Time elapsed: 0.106 s
% 18.94/3.97 % (2776381)Peak memory usage: 89 MB
% 18.94/3.97 % (2776381)Instructions burned: 107 (million)
% 18.94/3.97 % (2776382)Instruction limit reached!
% 18.94/3.97 % (2776382)------------------------------
% 18.94/3.97 % (2776382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.94/3.97 % (2776382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.94/3.97 % (2776382)CaDiCaL version: 2.1.3
% 18.94/3.97 % (2776382)Termination reason: Instruction limit
% 18.94/3.97 % (2776382)Termination phase: Saturation
% 18.94/3.97 % (2776382)Time elapsed: 0.108 s
% 18.94/3.97 % (2776382)Peak memory usage: 88 MB
% 18.94/3.97 % (2776382)Instructions burned: 116 (million)
% 18.94/3.97 % (2776384)Instruction limit reached!
% 18.94/3.97 % (2776384)------------------------------
% 18.94/3.97 % (2776384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.94/3.97 % (2776384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.94/3.97 % (2776384)CaDiCaL version: 2.1.3
% 18.94/3.97 % (2776384)Termination reason: Instruction limit
% 18.94/3.97 % (2776384)Termination phase: Saturation
% 18.94/3.97 % (2776384)Time elapsed: 0.107 s
% 18.94/3.97 % (2776384)Peak memory usage: 88 MB
% 18.94/3.97 % (2776384)Instructions burned: 119 (million)
% 18.94/3.97 % (2776383)Instruction limit reached!
% 18.94/3.97 % (2776383)------------------------------
% 18.94/3.97 % (2776383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.94/3.97 % (2776383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.94/3.97 % (2776383)CaDiCaL version: 2.1.3
% 18.94/3.97 % (2776383)Termination reason: Instruction limit
% 18.94/3.97 % (2776383)Termination phase: Saturation
% 18.94/3.97 % (2776383)Time elapsed: 0.185 s
% 18.94/3.97 % (2776383)Peak memory usage: 89 MB
% 18.94/3.97 % (2776383)Instructions burned: 180 (million)
% 18.94/3.97 % (2776393)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=503378605:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 18.94/3.97 % (2776392)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2682405140:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 18.94/3.97 % (2776392)Refutation not found, incomplete strategy
% 18.94/3.97 % (2776392)------------------------------
% 18.94/3.97 % (2776392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.94/3.97 % (2776392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.94/3.97 % (2776392)CaDiCaL version: 2.1.3
% 36.88/6.40 % (2776392)Termination reason: Refutation not found, incomplete strategy
% 36.88/6.40 % (2776392)Time elapsed: 0.001 s
% 36.88/6.40 % (2776392)Peak memory usage: 87 MB
% 36.88/6.40 % (2776394)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=376254881:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 36.88/6.40 % (2776394)Refutation not found, incomplete strategy
% 36.88/6.40 % (2776394)------------------------------
% 36.88/6.40 % (2776394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.88/6.40 % (2776394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.88/6.40 % (2776394)CaDiCaL version: 2.1.3
% 36.88/6.40 % (2776394)Termination reason: Refutation not found, incomplete strategy
% 36.88/6.40 % (2776394)Time elapsed: 0.001 s
% 36.88/6.40 % (2776394)Peak memory usage: 87 MB
% 36.88/6.40 % (2776395)lrs+10_64_to=lpo:sil=8000:random_seed=3662470698:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 36.88/6.40 % (2776393)Instruction limit reached!
% 36.88/6.40 % (2776393)------------------------------
% 36.88/6.40 % (2776393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.88/6.40 % (2776393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.88/6.40 % (2776393)CaDiCaL version: 2.1.3
% 36.88/6.40 % (2776393)Termination reason: Instruction limit
% 36.88/6.40 % (2776393)Termination phase: Saturation
% 36.88/6.40 % (2776393)Time elapsed: 0.169 s
% 36.88/6.40 % (2776393)Peak memory usage: 89 MB
% 36.88/6.40 % (2776393)Instructions burned: 189 (million)
% 36.88/6.40 % (2776395)Instruction limit reached!
% 36.88/6.40 % (2776395)------------------------------
% 36.88/6.40 % (2776395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.88/6.40 % (2776395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.88/6.40 % (2776395)CaDiCaL version: 2.1.3
% 36.88/6.40 % (2776395)Termination reason: Instruction limit
% 36.88/6.40 % (2776395)Termination phase: Saturation
% 36.88/6.40 % (2776395)Time elapsed: 0.126 s
% 36.88/6.40 % (2776395)Peak memory usage: 88 MB
% 36.88/6.40 % (2776395)Instructions burned: 126 (million)
% 36.88/6.40 % (2776392)------------------------------
% 36.88/6.40 % (2776392)------------------------------
% 36.88/6.40 % (2776400)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=306638668:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 36.88/6.40 % (2776394)------------------------------
% 36.88/6.40 % (2776394)------------------------------
% 36.88/6.40 % (2776401)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2236453050:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 36.88/6.40 % (2776400)Instruction limit reached!
% 36.88/6.40 % (2776400)------------------------------
% 36.88/6.40 % (2776400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.88/6.40 % (2776400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.88/6.40 % (2776400)CaDiCaL version: 2.1.3
% 36.88/6.40 % (2776400)Termination reason: Instruction limit
% 36.88/6.40 % (2776400)Termination phase: Saturation
% 36.88/6.40 % (2776400)Time elapsed: 0.202 s
% 36.88/6.40 % (2776400)Peak memory usage: 89 MB
% 36.88/6.40 % (2776400)Instructions burned: 194 (million)
% 36.88/6.40 % (2776401)Instruction limit reached!
% 36.88/6.40 % (2776401)------------------------------
% 36.88/6.40 % (2776401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.88/6.40 % (2776401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.88/6.40 % (2776401)CaDiCaL version: 2.1.3
% 36.88/6.40 % (2776401)Termination reason: Instruction limit
% 36.88/6.40 % (2776401)Termination phase: Saturation
% 36.88/6.40 % (2776401)Time elapsed: 0.166 s
% 36.88/6.40 % (2776401)Peak memory usage: 91 MB
% 36.88/6.40 % (2776401)Instructions burned: 157 (million)
% 36.88/6.40 % (2776403)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3276157442:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 36.88/6.40 % (2776404)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=584098462:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 36.88/6.40 % (2776404)Instruction limit reached!
% 36.88/6.40 % (2776404)------------------------------
% 36.88/6.40 % (2776404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.88/6.40 % (2776404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.46/8.79 % (2776404)CaDiCaL version: 2.1.3
% 52.46/8.79 % (2776404)Termination reason: Instruction limit
% 52.46/8.79 % (2776404)Termination phase: Saturation
% 52.46/8.79 % (2776404)Time elapsed: 0.088 s
% 52.46/8.79 % (2776404)Peak memory usage: 88 MB
% 52.46/8.79 % (2776404)Instructions burned: 107 (million)
% 52.46/8.79 % (2776406)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1661517712:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 52.46/8.79 % (2776406)Refutation not found, incomplete strategy
% 52.46/8.79 % (2776406)------------------------------
% 52.46/8.79 % (2776406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.46/8.79 % (2776406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.46/8.79 % (2776406)CaDiCaL version: 2.1.3
% 52.46/8.79 % (2776406)Termination reason: Refutation not found, incomplete strategy
% 52.46/8.79 % (2776406)Time elapsed: 0.001 s
% 52.46/8.79 % (2776406)Peak memory usage: 86 MB
% 52.46/8.79 % (2776407)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4099890960:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi)
% 52.46/8.79 % (2776410)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=412319858:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 52.46/8.79 % (2776407)Instruction limit reached!
% 52.46/8.79 % (2776407)------------------------------
% 52.46/8.79 % (2776407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.46/8.79 % (2776407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.46/8.79 % (2776407)CaDiCaL version: 2.1.3
% 52.46/8.79 % (2776407)Termination reason: Instruction limit
% 52.46/8.79 % (2776407)Termination phase: Saturation
% 52.46/8.79 % (2776407)Time elapsed: 0.239 s
% 52.46/8.79 % (2776407)Peak memory usage: 90 MB
% 52.46/8.79 % (2776407)Instructions burned: 242 (million)
% 52.46/8.79 % (2776406)------------------------------
% 52.46/8.79 % (2776406)------------------------------
% 52.46/8.79 % (2776414)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1685389480:i=134:sd=2:doe=on:ss=axioms:sgt=14_2983 on theBenchmark for (2983ds/134Mi)
% 52.46/8.79 % (2776415)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2996074262:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi)
% 52.46/8.79 % (2776414)Instruction limit reached!
% 52.46/8.79 % (2776414)------------------------------
% 52.46/8.79 % (2776414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.46/8.79 % (2776414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.46/8.79 % (2776414)CaDiCaL version: 2.1.3
% 52.46/8.79 % (2776414)Termination reason: Instruction limit
% 52.46/8.79 % (2776414)Termination phase: Saturation
% 52.46/8.79 % (2776414)Time elapsed: 0.149 s
% 52.46/8.79 % (2776414)Peak memory usage: 89 MB
% 52.46/8.79 % (2776414)Instructions burned: 134 (million)
% 52.46/8.79 % (2776418)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3026654215:i=191:fgj=on:bd=all_2979 on theBenchmark for (2979ds/191Mi)
% 52.46/8.79 % (2776415)Instruction limit reached!
% 52.46/8.79 % (2776415)------------------------------
% 52.46/8.79 % (2776415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.46/8.79 % (2776415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.46/8.79 % (2776415)CaDiCaL version: 2.1.3
% 52.46/8.79 % (2776415)Termination reason: Instruction limit
% 52.46/8.79 % (2776415)Termination phase: Saturation
% 52.46/8.79 % (2776415)Time elapsed: 0.443 s
% 52.46/8.79 % (2776415)Peak memory usage: 91 MB
% 52.46/8.79 % (2776415)Instructions burned: 499 (million)
% 52.46/8.79 % (2776418)Instruction limit reached!
% 52.46/8.79 % (2776418)------------------------------
% 52.46/8.79 % (2776418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.46/8.79 % (2776418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.46/8.79 % (2776418)CaDiCaL version: 2.1.3
% 52.46/8.79 % (2776418)Termination reason: Instruction limit
% 52.46/8.79 % (2776418)Termination phase: Saturation
% 52.46/8.79 % (2776418)Time elapsed: 0.203 s
% 52.46/8.79 % (2776418)Peak memory usage: 90 MB
% 52.46/8.79 % (2776418)Instructions burned: 192 (million)
% 52.46/8.79 % (2776420)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1350211047:i=264:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/264Mi)
% 61.65/11.38 % (2776421)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=277056281:cond=on:i=156:bs=on:gtg=exists_all:er=known_2975 on theBenchmark for (2975ds/156Mi)
% 61.65/11.38 % (2776421)Instruction limit reached!
% 61.65/11.38 % (2776421)------------------------------
% 61.65/11.38 % (2776421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.65/11.38 % (2776421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.65/11.38 % (2776421)CaDiCaL version: 2.1.3
% 61.65/11.38 % (2776421)Termination reason: Instruction limit
% 61.65/11.38 % (2776421)Termination phase: Saturation
% 61.65/11.38 % (2776421)Time elapsed: 0.137 s
% 61.65/11.38 % (2776421)Peak memory usage: 88 MB
% 61.65/11.38 % (2776421)Instructions burned: 156 (million)
% 61.65/11.38 % (2776420)Instruction limit reached!
% 61.65/11.38 % (2776420)------------------------------
% 61.65/11.38 % (2776420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.65/11.38 % (2776420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.65/11.38 % (2776420)CaDiCaL version: 2.1.3
% 61.65/11.38 % (2776420)Termination reason: Instruction limit
% 61.65/11.38 % (2776420)Termination phase: Saturation
% 61.65/11.38 % (2776420)Time elapsed: 0.241 s
% 61.65/11.38 % (2776420)Peak memory usage: 90 MB
% 61.65/11.38 % (2776420)Instructions burned: 264 (million)
% 61.65/11.38 % (2776424)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3647638431:i=3256:kws=precedence:bd=preordered:av=off_2971 on theBenchmark for (2971ds/3256Mi)
% 61.65/11.38 % (2776425)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1009481316:i=537:av=off:ss=included_2970 on theBenchmark for (2970ds/537Mi)
% 61.65/11.38 % (2776425)Instruction limit reached!
% 61.65/11.38 % (2776425)------------------------------
% 61.65/11.38 % (2776425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.65/11.38 % (2776425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.65/11.38 % (2776425)CaDiCaL version: 2.1.3
% 61.65/11.38 % (2776425)Termination reason: Instruction limit
% 61.65/11.38 % (2776425)Termination phase: Saturation
% 61.65/11.38 % (2776425)Time elapsed: 0.491 s
% 61.65/11.38 % (2776425)Peak memory usage: 92 MB
% 61.65/11.38 % (2776425)Instructions burned: 537 (million)
% 61.65/11.38 % (2776428)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4191703004:i=180:bd=preordered:av=off_2963 on theBenchmark for (2963ds/180Mi)
% 61.65/11.38 % (2776428)Instruction limit reached!
% 61.65/11.38 % (2776428)------------------------------
% 61.65/11.38 % (2776428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.65/11.38 % (2776428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.65/11.38 % (2776428)CaDiCaL version: 2.1.3
% 61.65/11.38 % (2776428)Termination reason: Instruction limit
% 61.65/11.38 % (2776428)Termination phase: Saturation
% 61.65/11.38 % (2776428)Time elapsed: 0.160 s
% 61.65/11.38 % (2776428)Peak memory usage: 88 MB
% 61.65/11.38 % (2776428)Instructions burned: 181 (million)
% 61.65/11.38 % (2776430)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1076852980:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2959 on theBenchmark for (2959ds/10307Mi)
% 61.65/11.38 % (2776403)Instruction limit reached!
% 61.65/11.38 % (2776403)------------------------------
% 61.65/11.38 % (2776403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.65/11.38 % (2776403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.65/11.38 % (2776403)CaDiCaL version: 2.1.3
% 61.65/11.38 % (2776403)Termination reason: Instruction limit
% 61.65/11.38 % (2776403)Termination phase: Saturation
% 61.65/11.38 % (2776403)Time elapsed: 3.459 s
% 61.65/11.38 % (2776403)Peak memory usage: 150 MB
% 61.65/11.38 % (2776403)Instructions burned: 3394 (million)
% 61.65/11.38 % (2776432)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=4090295187:i=412:gtgl=4:gtg=exists_all_2953 on theBenchmark for (2953ds/412Mi)
% 61.65/11.38 % (2776424)Instruction limit reached!
% 61.65/11.38 % (2776424)------------------------------
% 61.65/11.38 % (2776424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.65/11.38 % (2776424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.65/11.38 % (2776424)CaDiCaL version: 2.1.3
% 61.65/11.38 % (2776424)Termination reason: Instruction limit
% 61.65/11.38 % (2776424)Termination phase: Saturation
% 61.65/11.38 % (2776424)Time elapsed: 2.030 s
% 61.65/11.38 % (2776424)Peak memory usage: 151 MB
% 61.65/11.38 % (2776424)Instructions burned: 3257 (million)
% 61.65/11.38 % (2776434)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=22926963:s2pl=no:i=8478:s2at=4:nm=6_2948 on theBenchmark for (2948ds/8478Mi)
% 61.65/11.38 % (2776432)Instruction limit reached!
% 61.65/11.38 % (2776432)------------------------------
% 61.65/11.38 % (2776432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.65/11.38 % (2776432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.65/11.38 % (2776432)CaDiCaL version: 2.1.3
% 61.65/11.38 % (2776432)Termination reason: Instruction limit
% 61.65/11.38 % (2776432)Termination phase: Saturation
% 61.65/11.38 % (2776432)Time elapsed: 0.415 s
% 61.65/11.38 % (2776432)Peak memory usage: 94 MB
% 61.65/11.38 % (2776432)Instructions burned: 413 (million)
% 61.65/11.38 % (2776436)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=4260425882:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2946 on theBenchmark for (2946ds/303Mi)
% 61.65/11.38 % (2776436)Instruction limit reached!
% 61.65/11.38 % (2776436)------------------------------
% 61.65/11.38 % (2776436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.65/11.38 % (2776436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.65/11.38 % (2776436)CaDiCaL version: 2.1.3
% 61.65/11.38 % (2776436)Termination reason: Instruction limit
% 61.65/11.38 % (2776436)Termination phase: Saturation
% 61.65/11.38 % (2776436)Time elapsed: 0.259 s
% 61.65/11.38 % (2776436)Peak memory usage: 90 MB
% 61.65/11.38 % (2776436)Instructions burned: 303 (million)
% 61.65/11.38 % (2776438)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2758505414:st=4:i=720:sd=3:fsr=off:ss=axioms_2941 on theBenchmark for (2941ds/720Mi)
% 61.65/11.38 % (2776410)Instruction limit reached!
% 61.65/11.38 % (2776410)------------------------------
% 61.65/11.38 % (2776410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.65/11.38 % (2776410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.65/11.38 % (2776410)CaDiCaL version: 2.1.3
% 61.65/11.38 % (2776410)Termination reason: Instruction limit
% 61.65/11.38 % (2776410)Termination phase: Saturation
% 61.65/11.38 % (2776410)Time elapsed: 5.009 s
% 61.65/11.38 % (2776410)Peak memory usage: 166 MB
% 61.65/11.38 % (2776410)Instructions burned: 5208 (million)
% 61.65/11.38 % (2776438)Instruction limit reached!
% 61.65/11.38 % (2776438)------------------------------
% 61.65/11.38 % (2776438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.65/11.38 % (2776438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.65/11.38 % (2776438)CaDiCaL version: 2.1.3
% 61.65/11.38 % (2776438)Termination reason: Instruction limit
% 61.65/11.38 % (2776438)Termination phase: Saturation
% 61.65/11.38 % (2776438)Time elapsed: 0.673 s
% 61.65/11.38 % (2776438)Peak memory usage: 94 MB
% 61.65/11.38 % (2776438)Instructions burned: 720 (million)
% 61.65/11.38 % (2776440)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=382840134:i=598:bs=on:bd=preordered:av=off:ss=axioms_2934 on theBenchmark for (2934ds/598Mi)
% 61.65/11.38 % (2776441)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1430985483:i=2989:sd=3:ss=axioms:sgt=60_2932 on theBenchmark for (2932ds/2989Mi)
% 61.65/11.38 % (2776440)Instruction limit reached!
% 61.65/11.38 % (2776440)------------------------------
% 61.65/11.38 % (2776440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.65/11.38 % (2776440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.65/11.38 % (2776440)CaDiCaL version: 2.1.3
% 61.65/11.38 % (2776440)Termination reason: Instruction limit
% 61.65/11.38 % (2776440)Termination phase: Saturation
% 61.65/11.38 % (2776440)Time elapsed: 0.530 s
% 61.65/11.38 % (2776440)Peak memory usage: 94 MB
% 61.65/11.38 % (2776440)Instructions burned: 598 (million)
% 61.65/11.38 % (2776444)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3753959618:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2927 on theBenchmark for (2927ds/1997Mi)
% 72.55/11.76 % (2776444)Instruction limit reached!
% 72.55/11.76 % (2776444)------------------------------
% 72.55/11.76 % (2776444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.55/11.76 % (2776444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.55/11.76 % (2776444)CaDiCaL version: 2.1.3
% 72.55/11.76 % (2776444)Termination reason: Instruction limit
% 72.55/11.76 % (2776444)Termination phase: Saturation
% 72.55/11.76 % (2776444)Time elapsed: 1.975 s
% 72.55/11.76 % (2776444)Peak memory usage: 137 MB
% 72.55/11.76 % (2776444)Instructions burned: 1998 (million)
% 72.55/11.76 % (2776379)First to succeed.
% 72.55/11.76 % (2776379)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2776373"
% 72.55/11.76 % (2776434)Instruction limit reached!
% 72.55/11.76 % (2776434)------------------------------
% 72.55/11.76 % (2776434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.55/11.76 % (2776434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.55/11.76 % (2776434)CaDiCaL version: 2.1.3
% 72.55/11.76 % (2776434)Termination reason: Instruction limit
% 72.55/11.76 % (2776434)Termination phase: Saturation
% 72.55/11.76 % (2776434)Time elapsed: 4.376 s
% 72.55/11.76 % (2776434)Peak memory usage: 201 MB
% 72.55/11.76 % (2776434)Instructions burned: 8481 (million)
% 72.55/11.76 % (2776446)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=3858691720:i=2088:bd=preordered:av=off_2905 on theBenchmark for (2905ds/2088Mi)
% 72.55/11.76 % (2776447)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4013767854:i=1098:nicw=on_2903 on theBenchmark for (2903ds/1098Mi)
% 72.55/11.76 % (2776441)Instruction limit reached!
% 72.55/11.76 % (2776441)------------------------------
% 72.55/11.76 % (2776441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.55/11.76 % (2776441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.55/11.76 % (2776441)CaDiCaL version: 2.1.3
% 72.55/11.76 % (2776441)Termination reason: Instruction limit
% 72.55/11.76 % (2776441)Termination phase: Saturation
% 72.55/11.76 % (2776441)Time elapsed: 3.046 s
% 72.55/11.76 % (2776441)Peak memory usage: 146 MB
% 72.55/11.76 % (2776441)Instructions burned: 2990 (million)
% 72.55/11.76 % (2776379)Refutation found. Thanks to Tanya!
% 72.55/11.76 % SZS status Unsatisfiable for theBenchmark
% 72.55/11.76 % SZS output start Proof for theBenchmark
% See solution above
% 72.55/11.76 % (2776379)------------------------------
% 72.55/11.76 % (2776379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.55/11.76 % (2776379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.55/11.76 % (2776379)CaDiCaL version: 2.1.3
% 72.55/11.76 % (2776379)Termination reason: Refutation
% 72.55/11.76 % (2776379)Time elapsed: 9.450 s
% 72.55/11.76 % (2776379)Peak memory usage: 226 MB
% 72.55/11.76 % (2776379)Instructions burned: 13280 (million)
% 72.55/11.76 % (2776379)------------------------------
% 72.55/11.76 % (2776379)------------------------------
% 72.55/11.76 % (2776373)Success in time 10.085 s
% 72.55/11.76 % Vampire exiting
%------------------------------------------------------------------------------