%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV830-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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 01:19:36 PM UTC 2026
% Result : Unsatisfiable 184.07s 27.13s
% Output : Refutation 184.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 7
% Syntax : Number of formulae : 20 ( 8 unt; 0 def)
% Number of atoms : 35 ( 4 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 29 ( 14 ~; 15 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 8 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 1 con; 0-5 aty)
% Number of variables : 110 ( 110 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f304,axiom,
! [X0,X1] : hBOOL(hAPP(hAPP(c_lessequals(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__subsetI_0) ).
fof(f630,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2))
| hBOOL(hAPP(hAPP(c_in(X0),X1),X3))
| hBOOL(hAPP(hAPP(c_in(X0),X1),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X0,tc_bool)),X2),X3))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DiffI_0) ).
fof(f641,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(c_COMBS(X0,X1,X2,X3,X4),X5) = hAPP(hAPP(X0,X5),hAPP(X1,X5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_COMBS__def_0) ).
fof(f643,axiom,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X0))
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_0) ).
fof(f644,axiom,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_in(X0),X1),X2))
| ~ hBOOL(hAPP(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f656,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X0,tc_bool)),X3),X2)))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f746,axiom,
! [X0,X1] : hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Un__empty__left_0) ).
fof(f876,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(hAPP(c_in(X0),X1),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X0,tc_bool)),X3),X2)))
| hBOOL(hAPP(hAPP(c_in(X0),X1),X2))
| ~ hBOOL(hAPP(X3,X1)) ),
inference(resolution,[],[f630,f644]) ).
fof(f907,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),X5),X5))
| ~ hBOOL(hAPP(c_COMBS(c_in(X0),hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X0,tc_bool)),X1),X2,X3,X4),X5)) ),
inference(superposition,[],[f656,f641]) ).
fof(f908,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(hAPP(c_COMBS(c_in(X0),hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X0,tc_bool)),X1),X2,X3,X4),X5))
| ~ hBOOL(hAPP(X5,X5)) ),
inference(resolution,[],[f907,f644]) ).
fof(f1016,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(hAPP(X1,X5))
| hBOOL(hAPP(hAPP(c_in(X0),X5),X5))
| hBOOL(hAPP(c_COMBS(c_in(X0),hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X0,tc_bool)),X1),X2,X3,X4),X5)) ),
inference(superposition,[],[f876,f641]) ).
fof(f1028,plain,
! [X2,X3,X0,X1,X4,X5] : hAPP(X0,hAPP(X2,X0)) = hAPP(c_COMBS(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),X2,X3,X4,X5),X0),
inference(superposition,[],[f641,f746]) ).
fof(f2236,plain,
! [X2,X3,X0,X1,X4,X5] : hAPP(X0,X0) = hAPP(c_COMBS(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X2,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))),hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),X3,X4,X5),X0),
inference(superposition,[],[f1028,f746]) ).
fof(f11807,plain,
! [X2,X3,X0,X1,X4,X5] :
( hBOOL(hAPP(hAPP(c_in(X0),X1),X1))
| hBOOL(hAPP(c_COMBS(c_in(X0),hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X0,tc_bool)),hAPP(c_lessequals(tc_fun(X2,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)))),X3,X4,X5),X1)) ),
inference(resolution,[],[f1016,f304]) ).
fof(f13516,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ hBOOL(hAPP(c_COMBS(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),X2,X3,X4),c_COMBS(c_in(X5),hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X5,tc_bool)),X6),X7,X8,X9)))
| ~ hBOOL(hAPP(c_COMBS(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),X2,X3,X4),c_COMBS(c_in(X5),hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X5,tc_bool)),X6),X7,X8,X9))) ),
inference(superposition,[],[f908,f2236]) ).
fof(f13567,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : ~ hBOOL(hAPP(c_COMBS(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),X2,X3,X4),c_COMBS(c_in(X5),hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X5,tc_bool)),X6),X7,X8,X9))),
inference(duplicate_literal_removal,[],[f13516]) ).
fof(f22308,plain,
! [X2,X3,X0,X1,X4,X5] :
( hBOOL(hAPP(c_COMBS(c_in(X0),hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X0,tc_bool)),hAPP(c_lessequals(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),X2,X3,X4),X5))
| hBOOL(hAPP(X5,X5)) ),
inference(resolution,[],[f11807,f643]) ).
fof(f22478,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( hBOOL(hAPP(c_COMBS(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),X2,X3,X4),c_COMBS(c_in(X5),hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X5,tc_bool)),hAPP(c_lessequals(tc_fun(X6,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X6,tc_bool)))),X7,X8,X9)))
| hBOOL(hAPP(c_COMBS(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),X2,X3,X4),c_COMBS(c_in(X5),hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X5,tc_bool)),hAPP(c_lessequals(tc_fun(X6,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X6,tc_bool)))),X7,X8,X9))) ),
inference(superposition,[],[f22308,f2236]) ).
fof(f22506,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : hBOOL(hAPP(c_COMBS(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),X2,X3,X4),c_COMBS(c_in(X5),hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X5,tc_bool)),hAPP(c_lessequals(tc_fun(X6,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X6,tc_bool)))),X7,X8,X9))),
inference(duplicate_literal_removal,[],[f22478]) ).
fof(f22518,plain,
$false,
inference(forward_subsumption_resolution,[],[f22506,f13567]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV830-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 % Computer : n015.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Mon Sep 28 12:43:02 UTC 2026
% 0.08/0.22 % CPUTime :
% 0.08/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.27 Running first-order theorem proving
% 0.08/0.27 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
% 17.73/3.44 % (2604882)Input is clausal, will run a generic CNF schedule.
% 17.73/3.44 % (2604889)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2232786195:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 17.73/3.44 % (2604891)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=131135099:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 17.73/3.44 % (2604891)Instruction limit reached!
% 17.73/3.44 % (2604891)------------------------------
% 17.73/3.44 % (2604891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.44 % (2604891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.44 % (2604891)CaDiCaL version: 2.1.3
% 17.73/3.44 % (2604891)Termination reason: Instruction limit
% 17.73/3.44 % (2604891)Termination phase: Saturation
% 17.73/3.44 % (2604891)Time elapsed: 0.070 s
% 17.73/3.44 % (2604891)Peak memory usage: 89 MB
% 17.73/3.44 % (2604891)Instructions burned: 114 (million)
% 17.73/3.44 % (2604893)dis-21_1_sil=8000:lcm=predicate:random_seed=3276134014: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)
% 17.73/3.44 % (2604892)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3300993673:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 17.73/3.44 % (2604887)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=1482180707:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 17.73/3.44 % (2604890)lrs+10_1_sil=8000:sp=occurrence:random_seed=291532664:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 17.73/3.44 % (2604888)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3853735837:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 17.73/3.44 % (2604893)Instruction limit reached!
% 17.73/3.44 % (2604893)------------------------------
% 17.73/3.44 % (2604893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.44 % (2604893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.44 % (2604893)CaDiCaL version: 2.1.3
% 17.73/3.44 % (2604893)Termination reason: Instruction limit
% 17.73/3.44 % (2604893)Termination phase: Saturation
% 17.73/3.44 % (2604893)Time elapsed: 0.053 s
% 17.73/3.44 % (2604893)Peak memory usage: 88 MB
% 17.73/3.44 % (2604893)Instructions burned: 117 (million)
% 17.73/3.44 % (2604890)Instruction limit reached!
% 17.73/3.44 % (2604890)------------------------------
% 17.73/3.44 % (2604890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.44 % (2604890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.44 % (2604890)CaDiCaL version: 2.1.3
% 17.73/3.44 % (2604890)Termination reason: Instruction limit
% 17.73/3.44 % (2604890)Termination phase: Saturation
% 17.73/3.44 % (2604890)Time elapsed: 0.108 s
% 17.73/3.44 % (2604890)Peak memory usage: 89 MB
% 17.73/3.44 % (2604890)Instructions burned: 107 (million)
% 17.73/3.44 % (2604892)Instruction limit reached!
% 17.73/3.44 % (2604892)------------------------------
% 17.73/3.44 % (2604892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.44 % (2604892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.44 % (2604892)CaDiCaL version: 2.1.3
% 17.73/3.44 % (2604892)Termination reason: Instruction limit
% 17.73/3.44 % (2604892)Termination phase: Saturation
% 17.73/3.44 % (2604892)Time elapsed: 0.174 s
% 17.73/3.44 % (2604892)Peak memory usage: 89 MB
% 17.73/3.44 % (2604892)Instructions burned: 180 (million)
% 17.73/3.44 % (2604904)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=893541184: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)
% 17.73/3.44 % (2604896)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=587149064:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 17.73/3.44 % (2604896)Instruction limit reached!
% 17.73/3.44 % (2604896)------------------------------
% 17.73/3.44 % (2604896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.44 % (2604896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.44 % (2604896)CaDiCaL version: 2.1.3
% 31.23/5.39 % (2604896)Termination reason: Instruction limit
% 31.23/5.39 % (2604896)Termination phase: Saturation
% 31.23/5.39 % (2604896)Time elapsed: 0.138 s
% 31.23/5.39 % (2604896)Peak memory usage: 89 MB
% 31.23/5.39 % (2604896)Instructions burned: 143 (million)
% 31.23/5.39 % (2604905)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=432297193:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 31.23/5.39 % (2604904)Instruction limit reached!
% 31.23/5.39 % (2604904)------------------------------
% 31.23/5.39 % (2604904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.39 % (2604904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.23/5.39 % (2604904)CaDiCaL version: 2.1.3
% 31.23/5.39 % (2604904)Termination reason: Instruction limit
% 31.23/5.39 % (2604904)Termination phase: Saturation
% 31.23/5.39 % (2604904)Time elapsed: 0.179 s
% 31.23/5.39 % (2604904)Peak memory usage: 91 MB
% 31.23/5.39 % (2604904)Instructions burned: 190 (million)
% 31.23/5.39 % (2604906)lrs+10_64_to=lpo:sil=8000:random_seed=1672202589:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 31.23/5.39 % (2604905)Instruction limit reached!
% 31.23/5.39 % (2604905)------------------------------
% 31.23/5.39 % (2604905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.39 % (2604905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.23/5.39 % (2604905)CaDiCaL version: 2.1.3
% 31.23/5.39 % (2604905)Termination reason: Instruction limit
% 31.23/5.39 % (2604905)Termination phase: Saturation
% 31.23/5.39 % (2604905)Time elapsed: 0.179 s
% 31.23/5.39 % (2604905)Peak memory usage: 90 MB
% 31.23/5.39 % (2604905)Instructions burned: 219 (million)
% 31.23/5.39 % (2604909)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1693480839:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 31.23/5.39 % (2604906)Instruction limit reached!
% 31.23/5.39 % (2604906)------------------------------
% 31.23/5.39 % (2604906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.39 % (2604906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.23/5.39 % (2604906)CaDiCaL version: 2.1.3
% 31.23/5.39 % (2604906)Termination reason: Instruction limit
% 31.23/5.39 % (2604906)Termination phase: Saturation
% 31.23/5.39 % (2604906)Time elapsed: 0.133 s
% 31.23/5.39 % (2604906)Peak memory usage: 90 MB
% 31.23/5.39 % (2604906)Instructions burned: 126 (million)
% 31.23/5.39 % (2604911)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1192989322:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 31.23/5.39 % (2604909)Instruction limit reached!
% 31.23/5.39 % (2604909)------------------------------
% 31.23/5.39 % (2604909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.39 % (2604909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.23/5.39 % (2604909)CaDiCaL version: 2.1.3
% 31.23/5.39 % (2604909)Termination reason: Instruction limit
% 31.23/5.39 % (2604909)Termination phase: Saturation
% 31.23/5.39 % (2604909)Time elapsed: 0.096 s
% 31.23/5.39 % (2604909)Peak memory usage: 90 MB
% 31.23/5.39 % (2604909)Instructions burned: 196 (million)
% 31.23/5.39 % (2604913)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1096692148:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 31.23/5.39 % (2604911)Instruction limit reached!
% 31.23/5.39 % (2604911)------------------------------
% 31.23/5.39 % (2604911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.39 % (2604911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.23/5.39 % (2604911)CaDiCaL version: 2.1.3
% 31.23/5.39 % (2604911)Termination reason: Instruction limit
% 31.23/5.39 % (2604911)Termination phase: Saturation
% 31.23/5.39 % (2604911)Time elapsed: 0.162 s
% 31.23/5.39 % (2604911)Peak memory usage: 90 MB
% 31.23/5.39 % (2604911)Instructions burned: 157 (million)
% 31.23/5.39 % (2604915)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=611166337:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 31.23/5.39 % (2604917)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3770294053:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 31.23/5.39 % (2604917)Instruction limit reached!
% 31.23/5.39 % (2604917)------------------------------
% 31.23/5.39 % (2604917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/8.27 % (2604917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/8.27 % (2604917)CaDiCaL version: 2.1.3
% 52.05/8.27 % (2604917)Termination reason: Instruction limit
% 52.05/8.27 % (2604917)Termination phase: Saturation
% 52.05/8.27 % (2604917)Time elapsed: 0.053 s
% 52.05/8.27 % (2604917)Peak memory usage: 89 MB
% 52.05/8.27 % (2604917)Instructions burned: 109 (million)
% 52.05/8.27 % (2604915)Instruction limit reached!
% 52.05/8.27 % (2604915)------------------------------
% 52.05/8.27 % (2604915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/8.27 % (2604915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/8.27 % (2604915)CaDiCaL version: 2.1.3
% 52.05/8.27 % (2604915)Termination reason: Instruction limit
% 52.05/8.27 % (2604915)Termination phase: Saturation
% 52.05/8.27 % (2604915)Time elapsed: 0.097 s
% 52.05/8.27 % (2604915)Peak memory usage: 89 MB
% 52.05/8.27 % (2604915)Instructions burned: 106 (million)
% 52.05/8.27 % (2604919)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1576503990:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi)
% 52.05/8.27 % (2604922)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=876013303:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 52.05/8.27 % (2604923)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3833055937:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi)
% 52.05/8.27 % (2604923)Instruction limit reached!
% 52.05/8.27 % (2604923)------------------------------
% 52.05/8.27 % (2604923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/8.27 % (2604923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/8.27 % (2604923)CaDiCaL version: 2.1.3
% 52.05/8.27 % (2604923)Termination reason: Instruction limit
% 52.05/8.27 % (2604923)Termination phase: Saturation
% 52.05/8.27 % (2604923)Time elapsed: 0.053 s
% 52.05/8.27 % (2604923)Peak memory usage: 89 MB
% 52.05/8.27 % (2604923)Instructions burned: 136 (million)
% 52.05/8.27 % (2604919)Instruction limit reached!
% 52.05/8.27 % (2604919)------------------------------
% 52.05/8.27 % (2604919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/8.27 % (2604919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/8.27 % (2604919)CaDiCaL version: 2.1.3
% 52.05/8.27 % (2604919)Termination reason: Instruction limit
% 52.05/8.27 % (2604919)Termination phase: Saturation
% 52.05/8.27 % (2604919)Time elapsed: 0.235 s
% 52.05/8.27 % (2604919)Peak memory usage: 90 MB
% 52.05/8.27 % (2604919)Instructions burned: 242 (million)
% 52.05/8.27 % (2604927)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=282726832:i=499:bd=all_2984 on theBenchmark for (2984ds/499Mi)
% 52.05/8.27 % (2604928)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3502383498:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 52.05/8.27 % (2604928)Instruction limit reached!
% 52.05/8.27 % (2604928)------------------------------
% 52.05/8.27 % (2604928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/8.27 % (2604928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/8.27 % (2604928)CaDiCaL version: 2.1.3
% 52.05/8.27 % (2604928)Termination reason: Instruction limit
% 52.05/8.27 % (2604928)Termination phase: Saturation
% 52.05/8.27 % (2604928)Time elapsed: 0.174 s
% 52.05/8.27 % (2604928)Peak memory usage: 90 MB
% 52.05/8.27 % (2604928)Instructions burned: 191 (million)
% 52.05/8.27 % (2604931)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3463273730:i=264:kws=precedence:fsr=off_2979 on theBenchmark for (2979ds/264Mi)
% 52.05/8.27 % (2604927)Instruction limit reached!
% 52.05/8.27 % (2604927)------------------------------
% 52.05/8.27 % (2604927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/8.27 % (2604927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/8.27 % (2604927)CaDiCaL version: 2.1.3
% 52.05/8.27 % (2604927)Termination reason: Instruction limit
% 52.05/8.27 % (2604927)Termination phase: Saturation
% 52.05/8.27 % (2604927)Time elapsed: 0.500 s
% 52.05/8.27 % (2604927)Peak memory usage: 94 MB
% 52.05/8.27 % (2604927)Instructions burned: 499 (million)
% 52.05/8.27 % (2604931)Instruction limit reached!
% 52.05/8.27 % (2604931)------------------------------
% 87.97/13.37 % (2604931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.97/13.37 % (2604931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.97/13.37 % (2604931)CaDiCaL version: 2.1.3
% 87.97/13.37 % (2604931)Termination reason: Instruction limit
% 87.97/13.37 % (2604931)Termination phase: Saturation
% 87.97/13.37 % (2604931)Time elapsed: 0.187 s
% 87.97/13.37 % (2604931)Peak memory usage: 89 MB
% 87.97/13.37 % (2604931)Instructions burned: 264 (million)
% 87.97/13.37 % (2604933)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1965117642:cond=on:i=156:bs=on:gtg=exists_all:er=known_2976 on theBenchmark for (2976ds/156Mi)
% 87.97/13.37 % (2604934)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=4000908623:i=3256:kws=precedence:bd=preordered:av=off_2974 on theBenchmark for (2974ds/3256Mi)
% 87.97/13.37 % (2604933)Instruction limit reached!
% 87.97/13.37 % (2604933)------------------------------
% 87.97/13.37 % (2604933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.97/13.37 % (2604933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.97/13.37 % (2604933)CaDiCaL version: 2.1.3
% 87.97/13.37 % (2604933)Termination reason: Instruction limit
% 87.97/13.37 % (2604933)Termination phase: Saturation
% 87.97/13.37 % (2604933)Time elapsed: 0.160 s
% 87.97/13.37 % (2604933)Peak memory usage: 89 MB
% 87.97/13.37 % (2604933)Instructions burned: 156 (million)
% 87.97/13.37 % (2604937)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4113725426:i=537:av=off:ss=included_2972 on theBenchmark for (2972ds/537Mi)
% 87.97/13.37 % (2604937)Instruction limit reached!
% 87.97/13.37 % (2604937)------------------------------
% 87.97/13.37 % (2604937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.97/13.37 % (2604937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.97/13.37 % (2604937)CaDiCaL version: 2.1.3
% 87.97/13.37 % (2604937)Termination reason: Instruction limit
% 87.97/13.37 % (2604937)Termination phase: Saturation
% 87.97/13.37 % (2604937)Time elapsed: 0.398 s
% 87.97/13.37 % (2604937)Peak memory usage: 90 MB
% 87.97/13.37 % (2604937)Instructions burned: 537 (million)
% 87.97/13.37 % (2604941)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=912198993:i=180:bd=preordered:av=off_2965 on theBenchmark for (2965ds/180Mi)
% 87.97/13.37 % (2604941)Instruction limit reached!
% 87.97/13.37 % (2604941)------------------------------
% 87.97/13.37 % (2604941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.97/13.37 % (2604941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.97/13.37 % (2604941)CaDiCaL version: 2.1.3
% 87.97/13.37 % (2604941)Termination reason: Instruction limit
% 87.97/13.37 % (2604941)Termination phase: Saturation
% 87.97/13.37 % (2604941)Time elapsed: 0.150 s
% 87.97/13.37 % (2604941)Peak memory usage: 91 MB
% 87.97/13.37 % (2604941)Instructions burned: 181 (million)
% 87.97/13.37 % (2604943)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=3088169452:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2961 on theBenchmark for (2961ds/10307Mi)
% 87.97/13.37 % (2604922)Instruction limit reached!
% 87.97/13.37 % (2604922)------------------------------
% 87.97/13.37 % (2604922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.97/13.37 % (2604922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.97/13.37 % (2604922)CaDiCaL version: 2.1.3
% 87.97/13.37 % (2604922)Termination reason: Instruction limit
% 87.97/13.37 % (2604922)Termination phase: Saturation
% 87.97/13.37 % (2604922)Time elapsed: 2.656 s
% 87.97/13.37 % (2604922)Peak memory usage: 171 MB
% 87.97/13.37 % (2604922)Instructions burned: 5210 (million)
% 87.97/13.37 % (2604945)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=283610445:i=412:gtgl=4:gtg=exists_all_2958 on theBenchmark for (2958ds/412Mi)
% 87.97/13.37 % (2604945)Instruction limit reached!
% 87.97/13.37 % (2604945)------------------------------
% 87.97/13.37 % (2604945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.97/13.37 % (2604945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.97/13.37 % (2604945)CaDiCaL version: 2.1.3
% 87.97/13.37 % (2604945)Termination reason: Instruction limit
% 87.97/13.37 % (2604945)Termination phase: Saturation
% 116.17/17.34 % (2604945)Time elapsed: 0.161 s
% 116.17/17.34 % (2604945)Peak memory usage: 92 MB
% 116.17/17.34 % (2604945)Instructions burned: 412 (million)
% 116.17/17.34 % (2604913)Instruction limit reached!
% 116.17/17.34 % (2604913)------------------------------
% 116.17/17.34 % (2604913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.17/17.34 % (2604913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.17/17.34 % (2604913)CaDiCaL version: 2.1.3
% 116.17/17.34 % (2604913)Termination reason: Instruction limit
% 116.17/17.34 % (2604913)Termination phase: Saturation
% 116.17/17.34 % (2604913)Time elapsed: 3.314 s
% 116.17/17.34 % (2604913)Peak memory usage: 153 MB
% 116.17/17.34 % (2604913)Instructions burned: 3394 (million)
% 116.17/17.34 % (2604948)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=1457687105:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2955 on theBenchmark for (2955ds/303Mi)
% 116.17/17.34 % (2604947)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=2835694100:s2pl=no:i=8478:s2at=4:nm=6_2955 on theBenchmark for (2955ds/8478Mi)
% 116.17/17.34 % (2604948)Instruction limit reached!
% 116.17/17.34 % (2604948)------------------------------
% 116.17/17.34 % (2604948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.17/17.34 % (2604948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.17/17.34 % (2604948)CaDiCaL version: 2.1.3
% 116.17/17.34 % (2604948)Termination reason: Instruction limit
% 116.17/17.34 % (2604948)Termination phase: Saturation
% 116.17/17.34 % (2604948)Time elapsed: 0.137 s
% 116.17/17.34 % (2604948)Peak memory usage: 91 MB
% 116.17/17.34 % (2604948)Instructions burned: 305 (million)
% 116.17/17.34 % (2604951)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1871705609:st=4:i=720:sd=3:fsr=off:ss=axioms_2951 on theBenchmark for (2951ds/720Mi)
% 116.17/17.34 % (2604951)Instruction limit reached!
% 116.17/17.34 % (2604951)------------------------------
% 116.17/17.34 % (2604951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.17/17.34 % (2604951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.17/17.34 % (2604951)CaDiCaL version: 2.1.3
% 116.17/17.34 % (2604951)Termination reason: Instruction limit
% 116.17/17.34 % (2604951)Termination phase: Saturation
% 116.17/17.34 % (2604951)Time elapsed: 0.319 s
% 116.17/17.34 % (2604951)Peak memory usage: 93 MB
% 116.17/17.34 % (2604951)Instructions burned: 722 (million)
% 116.17/17.34 % (2604953)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=956982811:i=598:bs=on:bd=preordered:av=off:ss=axioms_2946 on theBenchmark for (2946ds/598Mi)
% 116.17/17.34 % (2604934)Instruction limit reached!
% 116.17/17.34 % (2604934)------------------------------
% 116.17/17.34 % (2604934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.17/17.34 % (2604934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.17/17.34 % (2604934)CaDiCaL version: 2.1.3
% 116.17/17.34 % (2604934)Termination reason: Instruction limit
% 116.17/17.34 % (2604934)Termination phase: Saturation
% 116.17/17.34 % (2604934)Time elapsed: 3.159 s
% 116.17/17.34 % (2604934)Peak memory usage: 153 MB
% 116.17/17.34 % (2604934)Instructions burned: 3257 (million)
% 116.17/17.34 % (2604953)Instruction limit reached!
% 116.17/17.34 % (2604953)------------------------------
% 116.17/17.34 % (2604953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.17/17.34 % (2604953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.17/17.34 % (2604953)CaDiCaL version: 2.1.3
% 116.17/17.34 % (2604953)Termination reason: Instruction limit
% 116.17/17.34 % (2604953)Termination phase: Saturation
% 116.17/17.34 % (2604953)Time elapsed: 0.319 s
% 116.17/17.34 % (2604953)Peak memory usage: 94 MB
% 116.17/17.34 % (2604953)Instructions burned: 599 (million)
% 116.17/17.34 % (2604956)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=3712097242:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2940 on theBenchmark for (2940ds/1997Mi)
% 116.17/17.34 % (2604955)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=759554202:i=2989:sd=3:ss=axioms:sgt=60_2940 on theBenchmark for (2940ds/2989Mi)
% 116.17/17.34 % (2604956)Instruction limit reached!
% 116.17/17.34 % (2604956)------------------------------
% 175.94/25.72 % (2604956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.94/25.72 % (2604956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.94/25.72 % (2604956)CaDiCaL version: 2.1.3
% 175.94/25.72 % (2604956)Termination reason: Instruction limit
% 175.94/25.72 % (2604956)Termination phase: Saturation
% 175.94/25.72 % (2604956)Time elapsed: 1.229 s
% 175.94/25.72 % (2604956)Peak memory usage: 140 MB
% 175.94/25.72 % (2604956)Instructions burned: 1998 (million)
% 175.94/25.72 % (2604961)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=1280465952:i=2088:bd=preordered:av=off_2926 on theBenchmark for (2926ds/2088Mi)
% 175.94/25.72 % (2604955)Instruction limit reached!
% 175.94/25.72 % (2604955)------------------------------
% 175.94/25.72 % (2604955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.94/25.72 % (2604955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.94/25.72 % (2604955)CaDiCaL version: 2.1.3
% 175.94/25.72 % (2604955)Termination reason: Instruction limit
% 175.94/25.72 % (2604955)Termination phase: Saturation
% 175.94/25.72 % (2604955)Time elapsed: 2.078 s
% 175.94/25.72 % (2604955)Peak memory usage: 148 MB
% 175.94/25.72 % (2604955)Instructions burned: 2990 (million)
% 175.94/25.72 % (2604963)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3555994615:i=1098:nicw=on_2917 on theBenchmark for (2917ds/1098Mi)
% 175.94/25.72 % (2604963)Instruction limit reached!
% 175.94/25.72 % (2604963)------------------------------
% 175.94/25.72 % (2604963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.94/25.72 % (2604963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.94/25.72 % (2604963)CaDiCaL version: 2.1.3
% 175.94/25.72 % (2604963)Termination reason: Instruction limit
% 175.94/25.72 % (2604963)Termination phase: Saturation
% 175.94/25.72 % (2604963)Time elapsed: 0.567 s
% 175.94/25.72 % (2604963)Peak memory usage: 99 MB
% 175.94/25.72 % (2604963)Instructions burned: 1099 (million)
% 175.94/25.72 % (2604965)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2758366074:i=433:bd=preordered_2909 on theBenchmark for (2909ds/433Mi)
% 175.94/25.72 % (2604965)Instruction limit reached!
% 175.94/25.72 % (2604965)------------------------------
% 175.94/25.72 % (2604965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.94/25.72 % (2604965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.94/25.72 % (2604965)CaDiCaL version: 2.1.3
% 175.94/25.72 % (2604965)Termination reason: Instruction limit
% 175.94/25.72 % (2604965)Termination phase: Saturation
% 175.94/25.72 % (2604965)Time elapsed: 0.158 s
% 175.94/25.72 % (2604965)Peak memory usage: 90 MB
% 175.94/25.72 % (2604965)Instructions burned: 433 (million)
% 175.94/25.72 % (2604967)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3294646095:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2905 on theBenchmark for (2905ds/2942Mi)
% 175.94/25.72 % (2604961)Instruction limit reached!
% 175.94/25.72 % (2604961)------------------------------
% 175.94/25.72 % (2604961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.94/25.72 % (2604961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.94/25.72 % (2604961)CaDiCaL version: 2.1.3
% 175.94/25.72 % (2604961)Termination reason: Instruction limit
% 175.94/25.72 % (2604961)Termination phase: Saturation
% 175.94/25.72 % (2604961)Time elapsed: 2.054 s
% 175.94/25.72 % (2604961)Peak memory usage: 142 MB
% 175.94/25.72 % (2604961)Instructions burned: 2089 (million)
% 175.94/25.72 % (2604969)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1472468549:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2902 on theBenchmark for (2902ds/6922Mi)
% 175.94/25.72 % (2604967)Instruction limit reached!
% 175.94/25.72 % (2604967)------------------------------
% 175.94/25.72 % (2604967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.94/25.72 % (2604967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.94/25.72 % (2604967)CaDiCaL version: 2.1.3
% 175.94/25.72 % (2604967)Termination reason: Instruction limit
% 175.94/25.72 % (2604967)Termination phase: Saturation
% 175.94/25.72 % (2604967)Time elapsed: 2.798 s
% 175.94/25.72 % (2604967)Peak memory usage: 150 MB
% 175.94/25.72 % (2604967)Instructions burned: 2942 (million)
% 99.31/26.85 % (2604971)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3198387633:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2875 on theBenchmark for (2875ds/596Mi)
% 99.31/26.85 % (2604971)Instruction limit reached!
% 99.31/26.85 % (2604971)------------------------------
% 99.31/26.85 % (2604971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.31/26.85 % (2604971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.31/26.85 % (2604971)CaDiCaL version: 2.1.3
% 99.31/26.85 % (2604971)Termination reason: Instruction limit
% 99.31/26.85 % (2604971)Termination phase: Saturation
% 99.31/26.85 % (2604971)Time elapsed: 0.280 s
% 99.31/26.85 % (2604971)Peak memory usage: 94 MB
% 99.31/26.85 % (2604971)Instructions burned: 598 (million)
% 99.31/26.85 % (2604973)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=286901113:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2870 on theBenchmark for (2870ds/4123Mi)
% 99.31/26.85 % (2604947)Instruction limit reached!
% 99.31/26.85 % (2604947)------------------------------
% 99.31/26.85 % (2604947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.31/26.85 % (2604947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.31/26.85 % (2604947)CaDiCaL version: 2.1.3
% 99.31/26.85 % (2604947)Termination reason: Instruction limit
% 99.31/26.85 % (2604947)Termination phase: Saturation
% 99.31/26.85 % (2604947)Time elapsed: 8.569 s
% 99.31/26.85 % (2604947)Peak memory usage: 200 MB
% 99.31/26.85 % (2604947)Instructions burned: 8478 (million)
% 99.31/26.85 % (2604975)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2878698622:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2867 on theBenchmark for (2867ds/16411Mi)
% 99.31/26.85 % (2604943)Instruction limit reached!
% 99.31/26.85 % (2604943)------------------------------
% 99.31/26.85 % (2604943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.31/26.85 % (2604943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.31/26.85 % (2604943)CaDiCaL version: 2.1.3
% 99.31/26.85 % (2604943)Termination reason: Instruction limit
% 99.31/26.85 % (2604943)Termination phase: Saturation
% 99.31/26.85 % (2604943)Time elapsed: 10.411 s
% 99.31/26.85 % (2604943)Peak memory usage: 195 MB
% 99.31/26.85 % (2604943)Instructions burned: 10308 (million)
% 99.31/26.85 % (2604969)Instruction limit reached!
% 99.31/26.85 % (2604969)------------------------------
% 99.31/26.85 % (2604969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.31/26.85 % (2604969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.31/26.85 % (2604969)CaDiCaL version: 2.1.3
% 99.31/26.85 % (2604969)Termination reason: Instruction limit
% 99.31/26.85 % (2604969)Termination phase: Saturation
% 99.31/26.85 % (2604969)Time elapsed: 4.552 s
% 99.31/26.85 % (2604969)Peak memory usage: 187 MB
% 99.31/26.85 % (2604969)Instructions burned: 6922 (million)
% 99.31/26.85 % (2604979)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3538625690:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2855 on theBenchmark for (2855ds/1670Mi)
% 99.31/26.85 % (2604980)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=2768874202:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2854 on theBenchmark for (2854ds/1722Mi)
% 99.31/26.85 % (2604973)Instruction limit reached!
% 99.31/26.85 % (2604973)------------------------------
% 99.31/26.85 % (2604973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.31/26.85 % (2604973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.31/26.85 % (2604973)CaDiCaL version: 2.1.3
% 99.31/26.85 % (2604973)Termination reason: Instruction limit
% 99.31/26.85 % (2604973)Termination phase: Saturation
% 99.31/26.85 % (2604973)Time elapsed: 2.216 s
% 99.31/26.85 % (2604973)Peak memory usage: 160 MB
% 99.31/26.85 % (2604973)Instructions burned: 4125 (million)
% 99.31/26.85 % (2604983)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=322327581:cts=off:cond=on:i=9530:bs=on:fsd=on_2845 on theBenchmark for (2845ds/9530Mi)
% 99.31/26.85 % (2604979)Instruction limit reached!
% 99.31/26.85 % (2604979)------------------------------
% 99.31/26.85 % (2604979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.31/26.85 % (2604979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.31/26.85 % (2604979)CaDiCaL version: 2.1.3
% 99.31/26.85 % (2604979)Termination reason: Instruction limit
% 99.31/26.85 % (2604979)Termination phase: Saturation
% 99.31/26.85 % (2604979)Time elapsed: 1.692 s
% 99.31/26.85 % (2604979)Peak memory usage: 140 MB
% 99.31/26.85 % (2604979)Instructions burned: 1670 (million)
% 99.31/26.85 % (2604980)Instruction limit reached!
% 99.31/26.85 % (2604980)------------------------------
% 99.31/26.85 % (2604980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.31/26.85 % (2604980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.31/26.85 % (2604980)CaDiCaL version: 2.1.3
% 99.31/26.85 % (2604980)Termination reason: Instruction limit
% 99.31/26.85 % (2604980)Termination phase: Saturation
% 99.31/26.85 % (2604980)Time elapsed: 1.709 s
% 99.31/26.85 % (2604980)Peak memory usage: 136 MB
% 99.31/26.85 % (2604980)Instructions burned: 1723 (million)
% 99.31/26.85 % (2604985)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=580926176:st=2:i=4495:sd=10:ss=included_2835 on theBenchmark for (2835ds/4495Mi)
% 99.31/26.86 % (2604986)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=4213028214:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2835 on theBenchmark for (2835ds/4920Mi)
% 99.31/26.86 % (2604985)Instruction limit reached!
% 99.31/26.86 % (2604985)------------------------------
% 99.31/26.86 % (2604985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.31/26.86 % (2604985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.31/26.86 % (2604985)CaDiCaL version: 2.1.3
% 99.31/26.86 % (2604985)Termination reason: Instruction limit
% 99.31/26.86 % (2604985)Termination phase: Saturation
% 99.31/26.86 % (2604985)Time elapsed: 4.418 s
% 99.31/26.86 % (2604985)Peak memory usage: 163 MB
% 99.31/26.86 % (2604985)Instructions burned: 4495 (million)
% 99.31/26.86 % (2604991)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=3983529422:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2788 on theBenchmark for (2788ds/2083Mi)
% 99.31/26.86 % (2604986)Instruction limit reached!
% 99.31/26.86 % (2604986)------------------------------
% 99.31/26.86 % (2604986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.31/26.86 % (2604986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.31/26.86 % (2604986)CaDiCaL version: 2.1.3
% 99.31/26.86 % (2604986)Termination reason: Instruction limit
% 99.31/26.86 % (2604986)Termination phase: Saturation
% 99.31/26.86 % (2604986)Time elapsed: 5.026 s
% 99.31/26.86 % (2604986)Peak memory usage: 163 MB
% 99.31/26.86 % (2604986)Instructions burned: 4920 (million)
% 99.31/26.86 % (2604993)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=4258382184:i=4629:av=off:gsp=on_2781 on theBenchmark for (2781ds/4629Mi)
% 99.31/26.86 % (2604991)Instruction limit reached!
% 99.31/26.86 % (2604991)------------------------------
% 99.31/26.86 % (2604991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.31/26.86 % (2604991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.31/26.86 % (2604991)CaDiCaL version: 2.1.3
% 99.31/26.86 % (2604991)Termination reason: Instruction limit
% 99.31/26.86 % (2604991)Termination phase: Saturation
% 99.31/26.86 % (2604991)Time elapsed: 2.120 s
% 99.31/26.86 % (2604991)Peak memory usage: 141 MB
% 99.31/26.86 % (2604991)Instructions burned: 2084 (million)
% 99.31/26.86 % (2604997)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=4085372000:i=1258:av=off_2764 on theBenchmark for (2764ds/1258Mi)
% 99.31/26.86 % (2604983)Instruction limit reached!
% 99.31/26.86 % (2604983)------------------------------
% 99.31/26.86 % (2604983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.31/26.86 % (2604983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.31/26.86 % (2604983)CaDiCaL version: 2.1.3
% 99.31/26.86 % (2604983)Termination reason: Instruction limit
% 99.31/26.86 % (2604983)Termination phase: Saturation
% 99.31/26.86 % (2604983)Time elapsed: 9.150 s
% 99.31/26.86 % (2604983)Peak memory usage: 200 MB
% 184.07/27.13 % (2604983)Instructions burned: 9530 (million)
% 184.07/27.13 % (2604997)Instruction limit reached!
% 184.07/27.13 % (2604997)------------------------------
% 184.07/27.13 % (2604997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 184.07/27.13 % (2604997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.07/27.13 % (2604997)CaDiCaL version: 2.1.3
% 184.07/27.13 % (2604997)Termination reason: Instruction limit
% 184.07/27.13 % (2604997)Termination phase: Saturation
% 184.07/27.13 % (2604997)Time elapsed: 1.221 s
% 184.07/27.13 % (2604997)Peak memory usage: 103 MB
% 184.07/27.13 % (2604997)Instructions burned: 1258 (million)
% 184.07/27.13 % (2604999)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2116007259:i=7343:av=off:ss=included_2751 on theBenchmark for (2751ds/7343Mi)
% 184.07/27.13 % (2605000)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3143939767:i=1325:sd=2:ss=axioms:sgt=16_2749 on theBenchmark for (2749ds/1325Mi)
% 184.07/27.13 % (2604975)First to succeed.
% 184.07/27.13 % (2604975)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2604882"
% 184.07/27.13 % (2604975)Refutation found. Thanks to Tanya!
% 184.07/27.13 % SZS status Unsatisfiable for theBenchmark
% 184.07/27.13 % SZS output start Proof for theBenchmark
% See solution above
% 184.07/27.13 % (2604975)------------------------------
% 184.07/27.13 % (2604975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 184.07/27.13 % (2604975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.07/27.13 % (2604975)CaDiCaL version: 2.1.3
% 184.07/27.13 % (2604975)Termination reason: Refutation
% 184.07/27.13 % (2604975)Time elapsed: 11.909 s
% 184.07/27.13 % (2604975)Peak memory usage: 224 MB
% 184.07/27.13 % (2604975)Instructions burned: 11974 (million)
% 184.07/27.13 % (2604975)------------------------------
% 184.07/27.13 % (2604975)------------------------------
% 184.07/27.13 % (2604882)Success in time 25.939 s
% 184.07/27.13 % Vampire exiting
%------------------------------------------------------------------------------