%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEO030-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:53:20 AM UTC 2026
% Result : Unsatisfiable 40.59s 11.09s
% Output : Refutation 40.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 9
% Syntax : Number of formulae : 12 ( 9 unt; 0 def)
% Number of atoms : 21 ( 4 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 21 ( 12 ~; 9 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 19 ( 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X2,X0,X1] :
( ~ equidistant(X0,X1,X2,X2)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax',identity_for_equidistance) ).
fof(f6,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ equidistant(X1,X6,X3,X7)
| ~ equidistant(X1,X4,X3,X5)
| ~ equidistant(X0,X6,X2,X7)
| ~ equidistant(X0,X1,X2,X3)
| ~ between(X0,X1,X4)
| ~ between(X2,X3,X5)
| X0 = X1
| equidistant(X4,X6,X5,X7) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax',outer_five_segment) ).
fof(f20,axiom,
! [X0,X1] : equidistant(X0,X1,X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1) ).
fof(f21,axiom,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2) ).
fof(f73,axiom,
between(u,v,w),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v_between_u_and_w) ).
fof(f74,axiom,
equidistant(u,w,u,w1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u_to_w_equals_u_to_w1) ).
fof(f75,axiom,
equidistant(v,w,v,w1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v_to_w_equals_v_to_w1) ).
fof(f76,axiom,
u != v,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u_not_v) ).
fof(f77,negated_conjecture,
w != w1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_w_is_w1) ).
fof(f109,plain,
! [X0] : ~ equidistant(w,w1,X0,X0),
inference(unit_resulting_resolution,[],[f3,f77]) ).
fof(f185,plain,
! [X0] : ~ equidistant(X0,X0,w,w1),
inference(unit_resulting_resolution,[],[f21,f109]) ).
fof(f68698,plain,
$false,
inference(unit_resulting_resolution,[],[f6,f76,f73,f73,f74,f20,f185,f20,f75]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO030-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.41 % Computer : n017.cluster.edu
% 0.13/0.41 % Model : x86_64 x86_64
% 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.41 % Memory : 8046.5625MB
% 0.13/0.41 % OS : Linux 6.8.0-71-generic
% 0.13/0.41 % CPULimit : 300
% 0.13/0.41 % WCLimit : 300
% 0.13/0.41 % DateTime : Sun Sep 27 06:32:21 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.44 Running first-order model finding
% 0.13/0.45 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.74/1.79 % (2188124)Will run a generic schedule for satisfiability detection.
% 7.74/1.79 % (2188133)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3495376981:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.74/1.79 % (2188130)% WARNING: option uhcvi not known.
% 7.74/1.79 % (2188129)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1446468807_2999 on theBenchmark for (2999ds/0Mi)
% 7.74/1.79 % (2188134)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3520124487:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.74/1.79 % (2188130)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1713291229:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.74/1.79 % (2188131)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1566558515:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.74/1.79 % (2188132)dis+10_1_sil=32000:sp=arity:random_seed=4185216646:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.74/1.79 % (2188135)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3925720996:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.74/1.79 % Detected minimum model sizes of [3]
% 7.74/1.79 % Detected maximum model sizes of [max]
% 7.74/1.79 % TRYING [3]
% 7.74/1.79 % (2188133)Instruction limit reached!
% 7.74/1.79 % (2188133)------------------------------
% 7.74/1.79 % (2188133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.79 % (2188133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.79 % (2188133)CaDiCaL version: 2.1.3
% 7.74/1.79 % (2188133)Termination reason: Instruction limit
% 7.74/1.79 % (2188133)Termination phase: Saturation
% 7.74/1.79 % (2188133)Time elapsed: 0.035 s
% 7.74/1.79 % (2188133)Peak memory usage: 12 MB
% 7.74/1.79 % (2188133)Instructions burned: 119 (million)
% 7.74/1.79 % (2188143)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1726790337:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.74/1.79 % Detected minimum model sizes of [3]
% 7.74/1.79 % Detected maximum model sizes of [max]
% 7.74/1.79 % TRYING [3]
% 7.74/1.79 % TRYING [4]
% 7.74/1.79 % (2188132)Instruction limit reached!
% 7.74/1.79 % (2188132)------------------------------
% 7.74/1.79 % (2188132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.79 % (2188132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.79 % (2188132)CaDiCaL version: 2.1.3
% 7.74/1.79 % (2188132)Termination reason: Instruction limit
% 7.74/1.79 % (2188132)Termination phase: Saturation
% 7.74/1.79 % (2188132)Time elapsed: 0.063 s
% 7.74/1.79 % (2188132)Peak memory usage: 12 MB
% 7.74/1.79 % (2188132)Instructions burned: 104 (million)
% 7.74/1.79 % TRYING [4]
% 7.74/1.79 % (2188145)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4013630918:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.74/1.79 % (2188134)Instruction limit reached!
% 7.74/1.79 % (2188134)------------------------------
% 7.74/1.79 % (2188134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.79 % (2188134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.79 % (2188134)CaDiCaL version: 2.1.3
% 7.74/1.79 % (2188134)Termination reason: Instruction limit
% 7.74/1.79 % (2188134)Termination phase: Saturation
% 7.74/1.79 % (2188134)Time elapsed: 0.084 s
% 7.74/1.79 % (2188134)Peak memory usage: 12 MB
% 7.74/1.79 % (2188134)Instructions burned: 131 (million)
% 7.74/1.79 % (2188135)Instruction limit reached!
% 7.74/1.79 % (2188135)------------------------------
% 7.74/1.79 % (2188135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.79 % (2188135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.79 % (2188135)CaDiCaL version: 2.1.3
% 7.74/1.79 % (2188135)Termination reason: Instruction limit
% 7.74/1.79 % (2188135)Termination phase: Saturation
% 7.74/1.79 % (2188135)Time elapsed: 0.091 s
% 7.74/1.79 % (2188135)Peak memory usage: 12 MB
% 7.74/1.79 % (2188135)Instructions burned: 160 (million)
% 7.74/1.79 % (2188147)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1875203881:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.74/1.79 % (2188148)ott-21_1_sil=16000:fs=off:random_seed=3413900987:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.74/1.79 % (2188145)Instruction limit reached!
% 7.74/1.79 % (2188145)------------------------------
% 26.57/4.23 % (2188145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.57/4.23 % (2188145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.57/4.23 % (2188145)CaDiCaL version: 2.1.3
% 26.57/4.23 % (2188145)Termination reason: Instruction limit
% 26.57/4.23 % (2188145)Termination phase: Saturation
% 26.57/4.23 % (2188145)Time elapsed: 0.078 s
% 26.57/4.23 % (2188145)Peak memory usage: 12 MB
% 26.57/4.23 % (2188145)Instructions burned: 132 (million)
% 26.57/4.23 % (2188151)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=812141416:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 26.57/4.23 % (2188143)Instruction limit reached!
% 26.57/4.23 % (2188143)------------------------------
% 26.57/4.23 % (2188143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.57/4.23 % (2188143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.57/4.23 % (2188143)CaDiCaL version: 2.1.3
% 26.57/4.23 % (2188143)Termination reason: Instruction limit
% 26.57/4.23 % (2188143)Termination phase: Finite model building constraint generation
% 26.57/4.23 % (2188143)Time elapsed: 0.146 s
% 26.57/4.23 % (2188143)Peak memory usage: 42 MB
% 26.57/4.23 % (2188143)Instructions burned: 715 (million)
% 26.57/4.23 % (2188148)Instruction limit reached!
% 26.57/4.23 % (2188148)------------------------------
% 26.57/4.23 % (2188148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.57/4.23 % (2188148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.57/4.23 % (2188148)CaDiCaL version: 2.1.3
% 26.57/4.23 % (2188148)Termination reason: Instruction limit
% 26.57/4.23 % (2188148)Termination phase: Saturation
% 26.57/4.23 % (2188148)Time elapsed: 0.096 s
% 26.57/4.23 % (2188148)Peak memory usage: 12 MB
% 26.57/4.23 % (2188148)Instructions burned: 181 (million)
% 26.57/4.23 % (2188153)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2868671910:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 26.57/4.23 % Detected minimum model sizes of [3]
% 26.57/4.23 % Detected maximum model sizes of [max]
% 26.57/4.23 % TRYING [3]
% 26.57/4.23 % (2188155)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1178098460:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 26.57/4.23 % TRYING [4]
% 26.57/4.23 % (2188151)Instruction limit reached!
% 26.57/4.23 % (2188151)------------------------------
% 26.57/4.23 % (2188151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.57/4.23 % (2188151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.57/4.23 % (2188151)CaDiCaL version: 2.1.3
% 26.57/4.23 % (2188151)Termination reason: Instruction limit
% 26.57/4.23 % (2188151)Termination phase: Saturation
% 26.57/4.23 % (2188151)Time elapsed: 0.175 s
% 26.57/4.23 % (2188151)Peak memory usage: 13 MB
% 26.57/4.23 % (2188151)Instructions burned: 479 (million)
% 26.57/4.23 % (2188157)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=873571349:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 26.57/4.23 % TRYING [5]
% 26.57/4.23 % (2188147)Instruction limit reached!
% 26.57/4.23 % (2188147)------------------------------
% 26.57/4.23 % (2188147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.57/4.23 % (2188147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.57/4.23 % (2188147)CaDiCaL version: 2.1.3
% 26.57/4.23 % (2188147)Termination reason: Instruction limit
% 26.57/4.23 % (2188147)Termination phase: Saturation
% 26.57/4.23 % (2188147)Time elapsed: 0.390 s
% 26.57/4.23 % (2188147)Peak memory usage: 16 MB
% 26.57/4.23 % (2188147)Instructions burned: 685 (million)
% 26.57/4.23 % (2188159)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3254092426:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 26.57/4.23 % (2188153)Instruction limit reached!
% 26.57/4.23 % (2188153)------------------------------
% 26.57/4.23 % (2188153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.57/4.23 % (2188153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.57/4.23 % (2188153)CaDiCaL version: 2.1.3
% 26.57/4.23 % (2188153)Termination reason: Instruction limit
% 26.57/4.23 % (2188153)Termination phase: Finite model building SAT solving
% 26.57/4.23 % (2188153)Time elapsed: 0.374 s
% 26.57/4.23 % (2188153)Peak memory usage: 47 MB
% 26.57/4.23 % (2188153)Instructions burned: 865 (million)
% 26.57/4.23 % (2188157)Instruction limit reached!
% 26.57/4.23 % (2188157)------------------------------
% 69.87/10.34 % (2188157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.87/10.34 % (2188157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.87/10.34 % (2188157)CaDiCaL version: 2.1.3
% 69.87/10.34 % (2188157)Termination reason: Instruction limit
% 69.87/10.34 % (2188157)Termination phase: Finite model building constraint generation
% 69.87/10.34 % (2188157)Time elapsed: 0.234 s
% 69.87/10.34 % (2188157)Peak memory usage: 106 MB
% 69.87/10.34 % (2188157)Instructions burned: 891 (million)
% 69.87/10.34 % (2188161)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1317067310:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 69.87/10.34 % (2188163)fmb+10_1_sil=64000:random_seed=266336070:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 69.87/10.34 % Detected minimum model sizes of [3]
% 69.87/10.34 % Detected maximum model sizes of [max]
% 69.87/10.34 % TRYING [3]
% 69.87/10.34 % TRYING [4]
% 69.87/10.34 % (2188159)Instruction limit reached!
% 69.87/10.34 % (2188159)------------------------------
% 69.87/10.34 % (2188159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.87/10.34 % (2188159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.87/10.34 % (2188159)CaDiCaL version: 2.1.3
% 69.87/10.34 % (2188159)Termination reason: Instruction limit
% 69.87/10.34 % (2188159)Termination phase: Saturation
% 69.87/10.34 % (2188159)Time elapsed: 0.444 s
% 69.87/10.34 % (2188159)Peak memory usage: 19 MB
% 69.87/10.34 % (2188159)Instructions burned: 694 (million)
% 69.87/10.34 % (2188165)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3286154820:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 69.87/10.34 % Detected minimum model sizes of [3]
% 69.87/10.34 % Detected maximum model sizes of [max]
% 69.87/10.34 % (2188165)Cannot represent all propositional literals internally
% 69.87/10.34 % (2188165)Refutation not found, incomplete strategy
% 69.87/10.34 % (2188165)------------------------------
% 69.87/10.34 % (2188165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.87/10.34 % (2188165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.87/10.34 % (2188165)CaDiCaL version: 2.1.3
% 69.87/10.34 % (2188165)Termination reason: Refutation not found, incomplete strategy
% 69.87/10.34 % (2188165)Time elapsed: 0.003 s
% 69.87/10.34 % (2188165)Peak memory usage: 10 MB
% 69.87/10.34 % (2188165)Instructions burned: 5 (million)
% 69.87/10.34 % (2188165)------------------------------
% 69.87/10.34 % (2188165)------------------------------
% 69.87/10.34 % (2188155)Instruction limit reached!
% 69.87/10.34 % (2188155)------------------------------
% 69.87/10.34 % (2188155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.87/10.34 % (2188155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.87/10.34 % (2188155)CaDiCaL version: 2.1.3
% 69.87/10.34 % (2188155)Termination reason: Instruction limit
% 69.87/10.34 % (2188155)Termination phase: Saturation
% 69.87/10.34 % (2188155)Time elapsed: 0.772 s
% 69.87/10.34 % (2188155)Peak memory usage: 19 MB
% 69.87/10.34 % (2188155)Instructions burned: 1179 (million)
% 69.87/10.34 % (2188167)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4104469088:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 69.87/10.34 % Detected minimum model sizes of [3]
% 69.87/10.34 % Detected maximum model sizes of [max]
% 69.87/10.34 % TRYING [8]
% 69.87/10.34 % (2188168)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=635705228:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 69.87/10.34 % TRYING [5]
% 69.87/10.34 % (2188161)Instruction limit reached!
% 69.87/10.34 % (2188161)------------------------------
% 69.87/10.34 % (2188161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.87/10.34 % (2188161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.87/10.34 % (2188161)CaDiCaL version: 2.1.3
% 69.87/10.34 % (2188161)Termination reason: Instruction limit
% 69.87/10.34 % (2188161)Termination phase: Saturation
% 69.87/10.34 % (2188161)Time elapsed: 0.495 s
% 69.87/10.34 % (2188161)Peak memory usage: 18 MB
% 69.87/10.34 % (2188161)Instructions burned: 880 (million)
% 69.87/10.34 % (2188171)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3380440799:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 69.87/10.34 % (2188167)Instruction limit reached!
% 69.87/10.34 % (2188167)------------------------------
% 69.87/10.34 % (2188167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.87/10.34 % (2188167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188167)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188167)Termination reason: Instruction limit
% 40.59/11.09 % (2188167)Termination phase: Finite model building constraint generation
% 40.59/11.09 % (2188167)Time elapsed: 0.304 s
% 40.59/11.09 % (2188167)Peak memory usage: 53 MB
% 40.59/11.09 % (2188167)Instructions burned: 922 (million)
% 40.59/11.09 % (2188173)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3078282323:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 40.59/11.09 % Detected minimum model sizes of [3]
% 40.59/11.09 % Detected maximum model sizes of [max]
% 40.59/11.09 % (2188173)Cannot represent all propositional literals internally
% 40.59/11.09 % (2188173)Refutation not found, incomplete strategy
% 40.59/11.09 % (2188173)------------------------------
% 40.59/11.09 % (2188173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188173)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188173)Termination reason: Refutation not found, incomplete strategy
% 40.59/11.09 % (2188173)Time elapsed: 0.004 s
% 40.59/11.09 % (2188173)Peak memory usage: 10 MB
% 40.59/11.09 % (2188173)Instructions burned: 6 (million)
% 40.59/11.09 % (2188173)------------------------------
% 40.59/11.09 % (2188173)------------------------------
% 40.59/11.09 % (2188175)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1674242610:fmbsr=2.30978:i=2174_2986 on theBenchmark for (2986ds/2174Mi)
% 40.59/11.09 % Detected minimum model sizes of [3]
% 40.59/11.09 % Detected maximum model sizes of [max]
% 40.59/11.09 % (2188175)Cannot represent all propositional literals internally
% 40.59/11.09 % (2188175)Refutation not found, incomplete strategy
% 40.59/11.09 % (2188175)------------------------------
% 40.59/11.09 % (2188175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188175)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188175)Termination reason: Refutation not found, incomplete strategy
% 40.59/11.09 % (2188175)Time elapsed: 0.028 s
% 40.59/11.09 % (2188175)Peak memory usage: 11 MB
% 40.59/11.09 % (2188175)Instructions burned: 57 (million)
% 40.59/11.09 % (2188175)------------------------------
% 40.59/11.09 % (2188175)------------------------------
% 40.59/11.09 % (2188177)ott-2_1_sil=16000:newcnf=on:random_seed=941639090:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2985 on theBenchmark for (2985ds/869Mi)
% 40.59/11.09 % (2188171)Instruction limit reached!
% 40.59/11.09 % (2188171)------------------------------
% 40.59/11.09 % (2188171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188171)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188171)Termination reason: Instruction limit
% 40.59/11.09 % (2188171)Termination phase: Saturation
% 40.59/11.09 % (2188171)Time elapsed: 0.801 s
% 40.59/11.09 % (2188171)Peak memory usage: 26 MB
% 40.59/11.09 % (2188171)Instructions burned: 1473 (million)
% 40.59/11.09 % (2188177)Instruction limit reached!
% 40.59/11.09 % (2188177)------------------------------
% 40.59/11.09 % (2188177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188177)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188177)Termination reason: Instruction limit
% 40.59/11.09 % (2188177)Termination phase: Saturation
% 40.59/11.09 % (2188177)Time elapsed: 0.529 s
% 40.59/11.09 % (2188177)Peak memory usage: 16 MB
% 40.59/11.09 % (2188177)Instructions burned: 870 (million)
% 40.59/11.09 % (2188179)ott+10_1_sil=32000:tgt=ground:random_seed=2069749873:i=5114:av=off_2980 on theBenchmark for (2980ds/5114Mi)
% 40.59/11.09 % (2188180)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1957075596:i=54282_2980 on theBenchmark for (2980ds/54282Mi)
% 40.59/11.09 % Detected minimum model sizes of [3]
% 40.59/11.09 % Detected maximum model sizes of [max]
% 40.59/11.09 % TRYING [3]
% 40.59/11.09 % TRYING [4]
% 40.59/11.09 % TRYING [6]
% 40.59/11.09 % TRYING [5]
% 40.59/11.09 % (2188168)Instruction limit reached!
% 40.59/11.09 % (2188168)------------------------------
% 40.59/11.09 % (2188168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188168)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188168)Termination reason: Instruction limit
% 40.59/11.09 % (2188168)Termination phase: Saturation
% 40.59/11.09 % (2188168)Time elapsed: 2.728 s
% 40.59/11.09 % (2188168)Peak memory usage: 23 MB
% 40.59/11.09 % (2188168)Instructions burned: 5132 (million)
% 40.59/11.09 % (2188183)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2287905198:i=3512:aac=none_2962 on theBenchmark for (2962ds/3512Mi)
% 40.59/11.09 % TRYING [6]
% 40.59/11.09 % TRYING [6]
% 40.59/11.09 % (2188179)Instruction limit reached!
% 40.59/11.09 % (2188179)------------------------------
% 40.59/11.09 % (2188179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188179)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188179)Termination reason: Instruction limit
% 40.59/11.09 % (2188179)Termination phase: Saturation
% 40.59/11.09 % (2188179)Time elapsed: 3.194 s
% 40.59/11.09 % (2188179)Peak memory usage: 36 MB
% 40.59/11.09 % (2188179)Instructions burned: 5115 (million)
% 40.59/11.09 % (2188185)dis+21_1_sil=32000:sas=cadical:random_seed=3675925519:i=3773:amm=off_2948 on theBenchmark for (2948ds/3773Mi)
% 40.59/11.09 % (2188183)Instruction limit reached!
% 40.59/11.09 % (2188183)------------------------------
% 40.59/11.09 % (2188183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188183)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188183)Termination reason: Instruction limit
% 40.59/11.09 % (2188183)Termination phase: Saturation
% 40.59/11.09 % (2188183)Time elapsed: 1.903 s
% 40.59/11.09 % (2188183)Peak memory usage: 24 MB
% 40.59/11.09 % (2188183)Instructions burned: 3512 (million)
% 40.59/11.09 % (2188187)ott+11_1_sil=16000:gs=on:random_seed=2977046040:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi)
% 40.59/11.09 % (2188163)Instruction limit reached!
% 40.59/11.09 % (2188163)------------------------------
% 40.59/11.09 % (2188163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188163)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188163)Termination reason: Instruction limit
% 40.59/11.09 % (2188163)Termination phase: Finite model building constraint generation
% 40.59/11.09 % (2188163)Time elapsed: 6.262 s
% 40.59/11.09 % (2188163)Peak memory usage: 480 MB
% 40.59/11.09 % (2188163)Instructions burned: 22063 (million)
% 40.59/11.09 % (2188189)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2723360440:fmbsr=1.6:i=67534_2930 on theBenchmark for (2930ds/67534Mi)
% 40.59/11.09 % Detected minimum model sizes of [3]
% 40.59/11.09 % Detected maximum model sizes of [max]
% 40.59/11.09 % (2188187)Instruction limit reached!
% 40.59/11.09 % (2188187)------------------------------
% 40.59/11.09 % (2188187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188187)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188187)Termination reason: Instruction limit
% 40.59/11.09 % (2188187)Termination phase: Saturation
% 40.59/11.09 % (2188187)Time elapsed: 1.312 s
% 40.59/11.09 % (2188187)Peak memory usage: 49 MB
% 40.59/11.09 % (2188187)Instructions burned: 2253 (million)
% 40.59/11.09 % (2188191)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2883734753:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2929 on theBenchmark for (2929ds/4591Mi)
% 40.59/11.09 % TRYING [7]
% 40.59/11.09 % (2188185)Instruction limit reached!
% 40.59/11.09 % (2188185)------------------------------
% 40.59/11.09 % (2188185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188185)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188185)Termination reason: Instruction limit
% 40.59/11.09 % (2188185)Termination phase: Saturation
% 40.59/11.09 % (2188185)Time elapsed: 2.279 s
% 40.59/11.09 % (2188185)Peak memory usage: 29 MB
% 40.59/11.09 % (2188185)Instructions burned: 3773 (million)
% 40.59/11.09 % (2188193)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1217692872:i=29340_2925 on theBenchmark for (2925ds/29340Mi)
% 40.59/11.09 % TRYING [7]
% 40.59/11.09 % (2188191)Instruction limit reached!
% 40.59/11.09 % (2188191)------------------------------
% 40.59/11.09 % (2188191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188191)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188191)Termination reason: Instruction limit
% 40.59/11.09 % (2188191)Termination phase: Saturation
% 40.59/11.09 % (2188191)Time elapsed: 2.824 s
% 40.59/11.09 % (2188191)Peak memory usage: 47 MB
% 40.59/11.09 % (2188191)Instructions burned: 4591 (million)
% 40.59/11.09 % (2188195)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3149619277:i=5211_2901 on theBenchmark for (2901ds/5211Mi)
% 40.59/11.09 % TRYING [7]
% 40.59/11.09 % (2188193) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2188124-2188193"...
% 40.59/11.09 % (2188193)...printing done.
% 40.59/11.09 % (2188193)Refutation found. Thanks to Tanya!
% 40.59/11.09 % SZS status Unsatisfiable for theBenchmark
% 40.59/11.09 % SZS output start Proof for theBenchmark
% See solution above
% 40.59/11.09 % (2188193)------------------------------
% 40.59/11.09 % (2188193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.59/11.09 % (2188193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.59/11.09 % (2188193)CaDiCaL version: 2.1.3
% 40.59/11.09 % (2188193)Termination reason: Refutation
% 40.59/11.09 % (2188193)Time elapsed: 3.010 s
% 40.59/11.09 % (2188193)Peak memory usage: 45 MB
% 40.59/11.09 % (2188193)Instructions burned: 6063 (million)
% 40.59/11.09 % (2188124)Success in time 10.634 s
% 40.59/11.09 % Vampire exiting
%------------------------------------------------------------------------------