%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO049-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:51:21 AM UTC 2026
% Result : Unsatisfiable 17.97s 3.14s
% Output : Refutation 17.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 17
% Syntax : Number of formulae : 31 ( 22 unt; 1 def)
% Number of atoms : 49 ( 12 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 42 ( 24 ~; 18 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-4 aty)
% Number of variables : 61 ( 61 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X2,X3,X0,X1] : between(X0,X1,extension(X0,X1,X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',segment_construction1) ).
fof(f5,axiom,
! [X2,X3,X0,X1] : equidistant(X0,extension(X1,X0,X2,X3),X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',segment_construction2) ).
fof(f22,axiom,
! [X2,X3,X0,X1] :
( equidistant(X2,X3,X0,X1)
| ~ equidistant(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2) ).
fof(f29,axiom,
! [X2,X3,X0,X1,X4,X5] :
( equidistant(X0,X1,X4,X5)
| ~ equidistant(X2,X3,X4,X5)
| ~ equidistant(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5) ).
fof(f32,axiom,
! [X2,X3,X0,X1,X4] :
( X0 != extension(X1,X2,X3,X4)
| between(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b0) ).
fof(f33,plain,
! [X2,X3,X0,X1,X4] :
( extension(X1,X2,X3,X4) != X0
| between(X1,X2,X0) ),
inference(reorient_equations,[],[f32]) ).
fof(f43,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ between(X0,X1,X4)
| ~ equidistant(X1,X4,X3,X5)
| ~ equidistant(X0,X1,X2,X3)
| ~ between(X2,X3,X5)
| equidistant(X0,X4,X2,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8) ).
fof(f47,axiom,
! [X2,X3,X0,X1,X4,X5] :
( extension(X4,X5,X0,X1) = extension(X4,X5,X2,X3)
| ~ equidistant(X0,X1,X2,X3)
| X4 = X5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_2) ).
fof(f53,axiom,
! [X2,X3,X0,X1] :
( X0 != X2
| ~ between(X0,X1,X2)
| between(X3,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b1) ).
fof(f54,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| between(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1) ).
fof(f55,axiom,
! [X0,X1] : between(X0,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2) ).
fof(f74,axiom,
! [X2,X3,X0,X1] :
( X2 = X3
| ~ equidistant(X0,X2,X0,X3)
| ~ equidistant(X1,X2,X1,X3)
| X0 = X1
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11) ).
fof(f85,axiom,
equidistant(u,v,u1,v1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_v_equals_u1_to_v1) ).
fof(f86,axiom,
equidistant(v,w,v1,w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v_to_w_equals_v1_to_w1) ).
fof(f87,axiom,
equidistant(u,w,u1,w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_w_equals_u1_to_w1) ).
fof(f88,axiom,
between(u,v,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v_between_u_and_w) ).
fof(f89,negated_conjecture,
~ between(u1,v1,w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_v1_between_u1_and_w1) ).
fof(f129,plain,
~ between(w1,v1,u1),
inference(unit_resulting_resolution,[],[f54,f89]) ).
fof(f144,plain,
equidistant(u1,v1,u,v),
inference(unit_resulting_resolution,[],[f22,f85]) ).
fof(f297,plain,
! [X0,X1] : w1 != extension(u1,v1,X0,X1),
inference(unit_resulting_resolution,[],[f33,f89]) ).
fof(f321,plain,
u1 != v1,
inference(unit_resulting_resolution,[],[f53,f129,f55]) ).
fof(f2245,plain,
extension(u1,v1,v1,w1) = extension(u1,v1,v,w),
inference(unit_resulting_resolution,[],[f47,f321,f86]) ).
fof(f2824,definition,
! [X2,X0,X1] : sF2(X2,X0,X1) = extension(X0,v1,X1,X2),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f2825,plain,
! [X2,X0,X1] : extension(X0,v1,X1,X2) = sF2(X2,X0,X1),
inference(reorient_equations,[],[f2824]) ).
fof(f3271,plain,
~ equidistant(u1,extension(u1,v1,v1,w1),u1,w1),
inference(unit_resulting_resolution,[],[f74,f321,f4,f297,f5]) ).
fof(f3426,plain,
~ equidistant(u1,extension(u1,v1,v,w),u1,w1),
inference(forward_demodulation,[],[f3271,f2245]) ).
fof(f3428,plain,
~ equidistant(u1,sF2(w,u1,v),u1,w1),
inference(forward_demodulation,[],[f3426,f2825]) ).
fof(f3448,plain,
~ equidistant(u1,sF2(w,u1,v),u,w),
inference(unit_resulting_resolution,[],[f29,f87,f3428]) ).
fof(f3982,plain,
equidistant(u1,extension(u1,v1,v,w),u,w),
inference(unit_resulting_resolution,[],[f43,f144,f88,f5,f4]) ).
fof(f4078,plain,
equidistant(u1,sF2(w,u1,v),u,w),
inference(forward_demodulation,[],[f3982,f2825]) ).
fof(f4121,plain,
$false,
inference(forward_subsumption_resolution,[],[f4078,f3448]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GEO049-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Sun Sep 27 06:43:20 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.32 Running first-order theorem proving
% 0.07/0.32 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
% 5.73/1.49 % (2017054)Input is clausal, will run a generic CNF schedule.
% 5.73/1.49 % (2017062)lrs+10_1_sil=8000:sp=occurrence:random_seed=2549864896:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.73/1.49 % (2017059)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=3197634347:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.73/1.49 % (2017060)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2862824442:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.73/1.49 % (2017061)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=422403165:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.73/1.49 % (2017064)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1059225216:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.73/1.49 % (2017063)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3079251649:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.73/1.49 % (2017065)dis-21_1_sil=8000:lcm=predicate:random_seed=3397753831: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)
% 5.73/1.49 % (2017062)Refutation not found, incomplete strategy
% 5.73/1.49 % (2017062)------------------------------
% 5.73/1.49 % (2017062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.49 % (2017062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.49 % (2017062)CaDiCaL version: 2.1.3
% 5.73/1.49 % (2017062)Termination reason: Refutation not found, incomplete strategy
% 5.73/1.49 % (2017062)Time elapsed: 0.020 s
% 5.73/1.49 % (2017062)Peak memory usage: 88 MB
% 5.73/1.49 % (2017062)Instructions burned: 67 (million)
% 5.73/1.49 % (2017063)Instruction limit reached!
% 5.73/1.49 % (2017063)------------------------------
% 5.73/1.49 % (2017063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.49 % (2017063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.49 % (2017063)CaDiCaL version: 2.1.3
% 5.73/1.49 % (2017063)Termination reason: Instruction limit
% 5.73/1.49 % (2017063)Termination phase: Saturation
% 5.73/1.49 % (2017063)Time elapsed: 0.034 s
% 5.73/1.49 % (2017063)Peak memory usage: 88 MB
% 5.73/1.49 % (2017063)Instructions burned: 116 (million)
% 5.73/1.49 % (2017065)Instruction limit reached!
% 5.73/1.49 % (2017065)------------------------------
% 5.73/1.49 % (2017065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.49 % (2017065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.49 % (2017065)CaDiCaL version: 2.1.3
% 5.73/1.49 % (2017065)Termination reason: Instruction limit
% 5.73/1.49 % (2017065)Termination phase: Saturation
% 5.73/1.49 % (2017065)Time elapsed: 0.035 s
% 5.73/1.49 % (2017065)Peak memory usage: 88 MB
% 5.73/1.49 % (2017065)Instructions burned: 120 (million)
% 5.73/1.49 % (2017064)Instruction limit reached!
% 5.73/1.49 % (2017064)------------------------------
% 5.73/1.49 % (2017064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.49 % (2017064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.49 % (2017064)CaDiCaL version: 2.1.3
% 5.73/1.49 % (2017064)Termination reason: Instruction limit
% 5.73/1.49 % (2017064)Termination phase: Saturation
% 5.73/1.49 % (2017064)Time elapsed: 0.073 s
% 5.73/1.49 % (2017064)Peak memory usage: 89 MB
% 5.73/1.49 % (2017064)Instructions burned: 180 (million)
% 5.73/1.49 % (2017073)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=1465058811:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 5.73/1.49 % (2017074)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3332410396:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 5.73/1.49 % (2017073)Refutation not found, incomplete strategy
% 5.73/1.49 % (2017073)------------------------------
% 5.73/1.49 % (2017073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.49 % (2017073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.49 % (2017073)CaDiCaL version: 2.1.3
% 12.23/2.39 % (2017073)Termination reason: Refutation not found, incomplete strategy
% 12.23/2.39 % (2017073)Time elapsed: 0.020 s
% 12.23/2.39 % (2017073)Peak memory usage: 88 MB
% 12.23/2.39 % (2017073)Instructions burned: 64 (million)
% 12.23/2.39 % (2017075)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3328775683:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 12.23/2.39 % (2017062)------------------------------
% 12.23/2.39 % (2017062)------------------------------
% 12.23/2.39 % (2017074)Instruction limit reached!
% 12.23/2.39 % (2017074)------------------------------
% 12.23/2.39 % (2017074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.39 % (2017074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.39 % (2017074)CaDiCaL version: 2.1.3
% 12.23/2.39 % (2017074)Termination reason: Instruction limit
% 12.23/2.39 % (2017074)Termination phase: Saturation
% 12.23/2.39 % (2017074)Time elapsed: 0.052 s
% 12.23/2.39 % (2017074)Peak memory usage: 89 MB
% 12.23/2.39 % (2017074)Instructions burned: 190 (million)
% 12.23/2.39 % (2017075)Instruction limit reached!
% 12.23/2.39 % (2017075)------------------------------
% 12.23/2.39 % (2017075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.39 % (2017075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.39 % (2017075)CaDiCaL version: 2.1.3
% 12.23/2.39 % (2017075)Termination reason: Instruction limit
% 12.23/2.39 % (2017075)Termination phase: Saturation
% 12.23/2.39 % (2017075)Time elapsed: 0.075 s
% 12.23/2.39 % (2017075)Peak memory usage: 90 MB
% 12.23/2.39 % (2017075)Instructions burned: 221 (million)
% 12.23/2.39 % (2017079)lrs+10_64_to=lpo:sil=8000:random_seed=3895857971:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 12.23/2.39 % (2017080)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4214939588:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 12.23/2.39 % (2017073)------------------------------
% 12.23/2.39 % (2017073)------------------------------
% 12.23/2.39 % (2017079)Instruction limit reached!
% 12.23/2.39 % (2017079)------------------------------
% 12.23/2.39 % (2017079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.39 % (2017079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.39 % (2017079)CaDiCaL version: 2.1.3
% 12.23/2.39 % (2017079)Termination reason: Instruction limit
% 12.23/2.39 % (2017079)Termination phase: Saturation
% 12.23/2.39 % (2017079)Time elapsed: 0.043 s
% 12.23/2.39 % (2017079)Peak memory usage: 89 MB
% 12.23/2.39 % (2017079)Instructions burned: 127 (million)
% 12.23/2.39 % (2017081)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=499293134:i=157:gtg=all_2996 on theBenchmark for (2996ds/157Mi)
% 12.23/2.39 % (2017080)Instruction limit reached!
% 12.23/2.39 % (2017080)------------------------------
% 12.23/2.39 % (2017080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.39 % (2017080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.39 % (2017080)CaDiCaL version: 2.1.3
% 12.23/2.39 % (2017080)Termination reason: Instruction limit
% 12.23/2.39 % (2017080)Termination phase: Saturation
% 12.23/2.39 % (2017080)Time elapsed: 0.060 s
% 12.23/2.39 % (2017080)Peak memory usage: 89 MB
% 12.23/2.39 % (2017080)Instructions burned: 194 (million)
% 12.23/2.39 % (2017081)Instruction limit reached!
% 12.23/2.39 % (2017081)------------------------------
% 12.23/2.39 % (2017081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.39 % (2017081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.39 % (2017081)CaDiCaL version: 2.1.3
% 12.23/2.39 % (2017081)Termination reason: Instruction limit
% 12.23/2.39 % (2017081)Termination phase: Saturation
% 12.23/2.39 % (2017081)Time elapsed: 0.057 s
% 12.23/2.39 % (2017081)Peak memory usage: 90 MB
% 12.23/2.39 % (2017081)Instructions burned: 157 (million)
% 12.23/2.39 % (2017084)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=637755392:i=3394:sd=4:ss=included:sgt=64_2996 on theBenchmark for (2996ds/3394Mi)
% 12.23/2.39 % (2017085)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=3616619997:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2996 on theBenchmark for (2996ds/106Mi)
% 12.23/2.39 % (2017085)Refutation not found, incomplete strategy
% 12.23/2.39 % (2017085)------------------------------
% 12.23/2.39 % (2017085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.64/3.05 % (2017085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.64/3.05 % (2017085)CaDiCaL version: 2.1.3
% 17.64/3.05 % (2017085)Termination reason: Refutation not found, incomplete strategy
% 17.64/3.05 % (2017085)Time elapsed: 0.018 s
% 17.64/3.05 % (2017085)Peak memory usage: 88 MB
% 17.64/3.05 % (2017085)Instructions burned: 68 (million)
% 17.64/3.05 % (2017087)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=179387909:i=107_2995 on theBenchmark for (2995ds/107Mi)
% 17.64/3.05 % (2017087)Instruction limit reached!
% 17.64/3.05 % (2017087)------------------------------
% 17.64/3.05 % (2017087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.64/3.05 % (2017087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.64/3.05 % (2017087)CaDiCaL version: 2.1.3
% 17.64/3.05 % (2017087)Termination reason: Instruction limit
% 17.64/3.05 % (2017087)Termination phase: Saturation
% 17.64/3.05 % (2017087)Time elapsed: 0.040 s
% 17.64/3.05 % (2017087)Peak memory usage: 89 MB
% 17.64/3.05 % (2017087)Instructions burned: 108 (million)
% 17.64/3.05 % (2017088)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1572198187:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2995 on theBenchmark for (2995ds/242Mi)
% 17.64/3.05 % (2017085)------------------------------
% 17.64/3.05 % (2017085)------------------------------
% 17.64/3.05 % (2017088)Instruction limit reached!
% 17.64/3.05 % (2017088)------------------------------
% 17.64/3.05 % (2017088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.64/3.05 % (2017088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.64/3.05 % (2017088)CaDiCaL version: 2.1.3
% 17.64/3.05 % (2017088)Termination reason: Instruction limit
% 17.64/3.05 % (2017088)Termination phase: Saturation
% 17.64/3.05 % (2017088)Time elapsed: 0.086 s
% 17.64/3.05 % (2017088)Peak memory usage: 90 MB
% 17.64/3.05 % (2017088)Instructions burned: 243 (million)
% 17.64/3.05 % (2017093)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=292873296:cond=fast:i=5208:av=off_2994 on theBenchmark for (2994ds/5208Mi)
% 17.64/3.05 % (2017094)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1022700281:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi)
% 17.64/3.05 % (2017095)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2263643138:i=499:bd=all_2993 on theBenchmark for (2993ds/499Mi)
% 17.64/3.05 % (2017094)Instruction limit reached!
% 17.64/3.05 % (2017094)------------------------------
% 17.64/3.05 % (2017094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.64/3.05 % (2017094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.64/3.05 % (2017094)CaDiCaL version: 2.1.3
% 17.64/3.05 % (2017094)Termination reason: Instruction limit
% 17.64/3.05 % (2017094)Termination phase: Saturation
% 17.64/3.05 % (2017094)Time elapsed: 0.043 s
% 17.64/3.05 % (2017094)Peak memory usage: 88 MB
% 17.64/3.05 % (2017094)Instructions burned: 136 (million)
% 17.64/3.05 % (2017099)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4170398496:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi)
% 17.64/3.05 % (2017095)Instruction limit reached!
% 17.64/3.05 % (2017095)------------------------------
% 17.64/3.05 % (2017095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.64/3.05 % (2017095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.64/3.05 % (2017095)CaDiCaL version: 2.1.3
% 17.64/3.05 % (2017095)Termination reason: Instruction limit
% 17.64/3.05 % (2017095)Termination phase: Saturation
% 17.64/3.05 % (2017095)Time elapsed: 0.145 s
% 17.64/3.05 % (2017095)Peak memory usage: 91 MB
% 17.64/3.05 % (2017095)Instructions burned: 502 (million)
% 17.64/3.05 % (2017099)Instruction limit reached!
% 17.64/3.05 % (2017099)------------------------------
% 17.64/3.05 % (2017099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.64/3.05 % (2017099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.64/3.05 % (2017099)CaDiCaL version: 2.1.3
% 17.64/3.05 % (2017099)Termination reason: Instruction limit
% 17.64/3.05 % (2017099)Termination phase: Saturation
% 17.64/3.05 % (2017099)Time elapsed: 0.068 s
% 17.64/3.05 % (2017099)Peak memory usage: 91 MB
% 17.64/3.05 % (2017099)Instructions burned: 191 (million)
% 17.97/3.14 % (2017101)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1497083670:i=264:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/264Mi)
% 17.97/3.14 % (2017102)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=301311950:cond=on:i=156:bs=on:gtg=exists_all:er=known_2990 on theBenchmark for (2990ds/156Mi)
% 17.97/3.14 % (2017101)Instruction limit reached!
% 17.97/3.14 % (2017101)------------------------------
% 17.97/3.14 % (2017101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.97/3.14 % (2017101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.97/3.14 % (2017101)CaDiCaL version: 2.1.3
% 17.97/3.14 % (2017101)Termination reason: Instruction limit
% 17.97/3.14 % (2017101)Termination phase: Saturation
% 17.97/3.14 % (2017101)Time elapsed: 0.085 s
% 17.97/3.14 % (2017101)Peak memory usage: 91 MB
% 17.97/3.14 % (2017101)Instructions burned: 265 (million)
% 17.97/3.14 % (2017102)Instruction limit reached!
% 17.97/3.14 % (2017102)------------------------------
% 17.97/3.14 % (2017102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.97/3.14 % (2017102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.97/3.14 % (2017102)CaDiCaL version: 2.1.3
% 17.97/3.14 % (2017102)Termination reason: Instruction limit
% 17.97/3.14 % (2017102)Termination phase: Saturation
% 17.97/3.14 % (2017102)Time elapsed: 0.046 s
% 17.97/3.14 % (2017102)Peak memory usage: 89 MB
% 17.97/3.14 % (2017102)Instructions burned: 160 (million)
% 17.97/3.14 % (2017105)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=649218709:i=3256:kws=precedence:bd=preordered:av=off_2989 on theBenchmark for (2989ds/3256Mi)
% 17.97/3.14 % (2017106)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2901681400:i=537:av=off:ss=included_2988 on theBenchmark for (2988ds/537Mi)
% 17.97/3.14 % (2017106)Instruction limit reached!
% 17.97/3.14 % (2017106)------------------------------
% 17.97/3.14 % (2017106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.97/3.14 % (2017106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.97/3.14 % (2017106)CaDiCaL version: 2.1.3
% 17.97/3.14 % (2017106)Termination reason: Instruction limit
% 17.97/3.14 % (2017106)Termination phase: Saturation
% 17.97/3.14 % (2017106)Time elapsed: 0.159 s
% 17.97/3.14 % (2017106)Peak memory usage: 89 MB
% 17.97/3.14 % (2017106)Instructions burned: 537 (million)
% 17.97/3.14 % (2017109)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=444171440:i=180:bd=preordered:av=off_2986 on theBenchmark for (2986ds/180Mi)
% 17.97/3.14 % (2017109)Instruction limit reached!
% 17.97/3.14 % (2017109)------------------------------
% 17.97/3.14 % (2017109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.97/3.14 % (2017109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.97/3.14 % (2017109)CaDiCaL version: 2.1.3
% 17.97/3.14 % (2017109)Termination reason: Instruction limit
% 17.97/3.14 % (2017109)Termination phase: Saturation
% 17.97/3.14 % (2017109)Time elapsed: 0.052 s
% 17.97/3.14 % (2017109)Peak memory usage: 89 MB
% 17.97/3.14 % (2017109)Instructions burned: 183 (million)
% 17.97/3.14 % (2017111)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=3275407116:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2984 on theBenchmark for (2984ds/10307Mi)
% 17.97/3.14 % (2017084)Instruction limit reached!
% 17.97/3.14 % (2017084)------------------------------
% 17.97/3.14 % (2017084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.97/3.14 % (2017084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.97/3.14 % (2017084)CaDiCaL version: 2.1.3
% 17.97/3.14 % (2017084)Termination reason: Instruction limit
% 17.97/3.14 % (2017084)Termination phase: Saturation
% 17.97/3.14 % (2017084)Time elapsed: 1.182 s
% 17.97/3.14 % (2017084)Peak memory usage: 148 MB
% 17.97/3.14 % (2017084)Instructions burned: 3395 (million)
% 17.97/3.14 % (2017113)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=3233209818:i=412:gtgl=4:gtg=exists_all_2983 on theBenchmark for (2983ds/412Mi)
% 17.97/3.14 % (2017113)Instruction limit reached!
% 17.97/3.14 % (2017113)------------------------------
% 17.97/3.14 % (2017113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.97/3.14 % (2017113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.97/3.14 % (2017113)CaDiCaL version: 2.1.3
% 17.97/3.14 % (2017113)Termination reason: Instruction limit
% 17.97/3.14 % (2017113)Termination phase: Saturation
% 17.97/3.14 % (2017113)Time elapsed: 0.097 s
% 17.97/3.14 % (2017113)Peak memory usage: 89 MB
% 17.97/3.14 % (2017113)Instructions burned: 416 (million)
% 17.97/3.14 % (2017115)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=1432953789:s2pl=no:i=8478:s2at=4:nm=6_2981 on theBenchmark for (2981ds/8478Mi)
% 17.97/3.14 % (2017105)Instruction limit reached!
% 17.97/3.14 % (2017105)------------------------------
% 17.97/3.14 % (2017105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.97/3.14 % (2017105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.97/3.14 % (2017105)CaDiCaL version: 2.1.3
% 17.97/3.14 % (2017105)Termination reason: Instruction limit
% 17.97/3.14 % (2017105)Termination phase: Saturation
% 17.97/3.14 % (2017105)Time elapsed: 1.021 s
% 17.97/3.14 % (2017105)Peak memory usage: 142 MB
% 17.97/3.14 % (2017105)Instructions burned: 3259 (million)
% 17.97/3.14 % (2017117)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=3660663759:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2977 on theBenchmark for (2977ds/303Mi)
% 17.97/3.14 % (2017117)First to succeed.
% 17.97/3.14 % (2017117)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2017054"
% 17.97/3.14 % (2017093)Instruction limit reached!
% 17.97/3.14 % (2017093)------------------------------
% 17.97/3.14 % (2017093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.97/3.14 % (2017093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.97/3.14 % (2017093)CaDiCaL version: 2.1.3
% 17.97/3.14 % (2017093)Termination reason: Instruction limit
% 17.97/3.14 % (2017093)Termination phase: Saturation
% 17.97/3.14 % (2017093)Time elapsed: 1.717 s
% 17.97/3.14 % (2017093)Peak memory usage: 158 MB
% 17.97/3.14 % (2017093)Instructions burned: 5209 (million)
% 17.97/3.14 % (2017119)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=917476460:st=4:i=720:sd=3:fsr=off:ss=axioms_2975 on theBenchmark for (2975ds/720Mi)
% 17.97/3.14 % (2017117)Refutation found. Thanks to Tanya!
% 17.97/3.14 % SZS status Unsatisfiable for theBenchmark
% 17.97/3.14 % SZS output start Proof for theBenchmark
% See solution above
% 17.97/3.14 % (2017117)------------------------------
% 17.97/3.14 % (2017117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.97/3.14 % (2017117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.97/3.14 % (2017117)CaDiCaL version: 2.1.3
% 17.97/3.14 % (2017117)Termination reason: Refutation
% 17.97/3.14 % (2017117)Time elapsed: 0.049 s
% 17.97/3.14 % (2017117)Peak memory usage: 90 MB
% 17.97/3.14 % (2017117)Instructions burned: 168 (million)
% 17.97/3.14 % (2017117)------------------------------
% 17.97/3.14 % (2017117)------------------------------
% 17.97/3.14 % (2017054)Success in time 2.528 s
% 17.97/3.14 % Vampire exiting
%------------------------------------------------------------------------------