%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI586_1 : TPTP v9.3.1. Released v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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:34:55 AM UTC 2026
% Result : Theorem 43.12s 9.14s
% Output : Refutation 43.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ARI586_1 : TPTP v9.3.1. Released v5.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n011.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 20:53:01 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.01/0.80 % (3772144)Will run a generic schedule for satisfiability detection.
% 4.01/0.80 % (3772154)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4053600385:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.01/0.80 % (3772150)% WARNING: option uhcvi not known.
% 4.01/0.80 % (3772149)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1997451491_2999 on theBenchmark for (2999ds/0Mi)
% 4.01/0.80 % (3772151)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=395653699:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.01/0.80 % (3772152)dis+10_1_sil=32000:sp=arity:random_seed=1204919147:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.01/0.80 % (3772155)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2834860033:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.01/0.80 % (3772153)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=477645224:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.01/0.80 % (3772149)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.01/0.80 % (3772149)Terminated due to inappropriate strategy.
% 4.01/0.80 % (3772149)------------------------------
% 4.01/0.80 % (3772149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.01/0.80 % (3772149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/0.80 % (3772149)CaDiCaL version: 2.1.3
% 4.01/0.80 % (3772149)Termination reason: Inappropriate
% 4.01/0.80 % (3772149)Time elapsed: 0.0000 s
% 4.01/0.80 % (3772149)Peak memory usage: 10 MB
% 4.01/0.80 % (3772150)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2422251144:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.01/0.80 % (3772149)------------------------------
% 4.01/0.80 % (3772149)------------------------------
% 4.01/0.80 % (3772163)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1424421837:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.01/0.80 % (3772163)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.01/0.80 % (3772163)Terminated due to inappropriate strategy.
% 4.01/0.80 % (3772163)------------------------------
% 4.01/0.80 % (3772163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.01/0.80 % (3772163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/0.80 % (3772163)CaDiCaL version: 2.1.3
% 4.01/0.80 % (3772163)Termination reason: Inappropriate
% 4.01/0.80 % (3772163)Time elapsed: 0.0000 s
% 4.01/0.80 % (3772163)Peak memory usage: 10 MB
% 4.01/0.80 % (3772163)------------------------------
% 4.01/0.80 % (3772163)------------------------------
% 4.01/0.80 % (3772154)Instruction limit reached!
% 4.01/0.80 % (3772154)------------------------------
% 4.01/0.80 % (3772154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.01/0.80 % (3772154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/0.80 % (3772154)CaDiCaL version: 2.1.3
% 4.01/0.80 % (3772154)Termination reason: Instruction limit
% 4.01/0.80 % (3772154)Termination phase: Saturation
% 4.01/0.80 % (3772154)Time elapsed: 0.044 s
% 4.01/0.80 % (3772154)Peak memory usage: 13 MB
% 4.01/0.80 % (3772154)Instructions burned: 131 (million)
% 4.01/0.80 % (3772165)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4098149041:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.01/0.80 % (3772166)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=2291823168:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.01/0.80 % (3772152)Instruction limit reached!
% 4.01/0.80 % (3772152)------------------------------
% 4.01/0.80 % (3772152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.01/0.80 % (3772152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/0.80 % (3772152)CaDiCaL version: 2.1.3
% 4.01/0.80 % (3772152)Termination reason: Instruction limit
% 4.01/0.80 % (3772152)Termination phase: Saturation
% 4.01/0.80 % (3772152)Time elapsed: 0.065 s
% 4.01/0.80 % (3772152)Peak memory usage: 12 MB
% 4.01/0.80 % (3772152)Instructions burned: 104 (million)
% 4.01/0.80 % (3772153)Instruction limit reached!
% 4.01/0.80 % (3772153)------------------------------
% 4.01/0.80 % (3772153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.01/0.80 % (3772153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.37 % (3772153)CaDiCaL version: 2.1.3
% 7.44/1.37 % (3772153)Termination reason: Instruction limit
% 7.44/1.37 % (3772153)Termination phase: Saturation
% 7.44/1.37 % (3772153)Time elapsed: 0.073 s
% 7.44/1.37 % (3772153)Peak memory usage: 12 MB
% 7.44/1.37 % (3772153)Instructions burned: 118 (million)
% 7.44/1.37 % (3772169)ott-21_1_sil=16000:fs=off:random_seed=3586319151:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 7.44/1.37 % (3772170)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2004836022:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.44/1.37 % (3772155)Instruction limit reached!
% 7.44/1.37 % (3772155)------------------------------
% 7.44/1.37 % (3772155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.37 % (3772155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.37 % (3772155)CaDiCaL version: 2.1.3
% 7.44/1.37 % (3772155)Termination reason: Instruction limit
% 7.44/1.37 % (3772155)Termination phase: Saturation
% 7.44/1.37 % (3772155)Time elapsed: 0.111 s
% 7.44/1.37 % (3772155)Peak memory usage: 13 MB
% 7.44/1.37 % (3772155)Instructions burned: 160 (million)
% 7.44/1.37 % (3772173)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3973726042:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.44/1.37 % (3772165)Instruction limit reached!
% 7.44/1.37 % (3772165)------------------------------
% 7.44/1.37 % (3772165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.37 % (3772165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.37 % (3772165)CaDiCaL version: 2.1.3
% 7.44/1.37 % (3772165)Termination reason: Instruction limit
% 7.44/1.37 % (3772165)Termination phase: Saturation
% 7.44/1.37 % (3772165)Time elapsed: 0.088 s
% 7.44/1.37 % (3772165)Peak memory usage: 12 MB
% 7.44/1.37 % (3772165)Instructions burned: 131 (million)
% 7.44/1.37 % (3772173)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.44/1.37 % (3772173)Terminated due to inappropriate strategy.
% 7.44/1.37 % (3772173)------------------------------
% 7.44/1.37 % (3772173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.37 % (3772173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.37 % (3772173)CaDiCaL version: 2.1.3
% 7.44/1.37 % (3772173)Termination reason: Inappropriate
% 7.44/1.37 % (3772173)Time elapsed: 0.0000 s
% 7.44/1.37 % (3772173)Peak memory usage: 10 MB
% 7.44/1.37 % (3772173)------------------------------
% 7.44/1.37 % (3772173)------------------------------
% 7.44/1.37 % (3772175)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=514880965:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.44/1.37 % (3772176)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3478595491:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 7.44/1.37 % (3772176)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.44/1.37 % (3772176)Terminated due to inappropriate strategy.
% 7.44/1.37 % (3772176)------------------------------
% 7.44/1.37 % (3772176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.37 % (3772176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.37 % (3772176)CaDiCaL version: 2.1.3
% 7.44/1.37 % (3772176)Termination reason: Inappropriate
% 7.44/1.37 % (3772176)Time elapsed: 0.0000 s
% 7.44/1.37 % (3772176)Peak memory usage: 10 MB
% 7.44/1.37 % (3772176)------------------------------
% 7.44/1.37 % (3772176)------------------------------
% 7.44/1.37 % (3772169)Instruction limit reached!
% 7.44/1.37 % (3772169)------------------------------
% 7.44/1.37 % (3772169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.37 % (3772169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.37 % (3772169)CaDiCaL version: 2.1.3
% 7.44/1.37 % (3772169)Termination reason: Instruction limit
% 7.44/1.37 % (3772169)Termination phase: Saturation
% 7.44/1.37 % (3772169)Time elapsed: 0.081 s
% 7.44/1.37 % (3772169)Peak memory usage: 12 MB
% 7.44/1.37 % (3772169)Instructions burned: 181 (million)
% 7.44/1.37 % (3772179)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=1748729786:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 7.44/1.37 % (3772180)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1467333014:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 21.90/3.35 % (3772166)Instruction limit reached!
% 21.90/3.35 % (3772166)------------------------------
% 21.90/3.35 % (3772166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.90/3.35 % (3772166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.90/3.35 % (3772166)CaDiCaL version: 2.1.3
% 21.90/3.35 % (3772166)Termination reason: Instruction limit
% 21.90/3.35 % (3772166)Termination phase: Saturation
% 21.90/3.35 % (3772166)Time elapsed: 0.168 s
% 21.90/3.35 % (3772166)Peak memory usage: 15 MB
% 21.90/3.35 % (3772166)Instructions burned: 686 (million)
% 21.90/3.35 % (3772183)fmb+10_1_sil=64000:random_seed=2646057094:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 21.90/3.35 % (3772183)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.90/3.35 % (3772183)Terminated due to inappropriate strategy.
% 21.90/3.35 % (3772183)------------------------------
% 21.90/3.35 % (3772183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.90/3.35 % (3772183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.90/3.35 % (3772183)CaDiCaL version: 2.1.3
% 21.90/3.35 % (3772183)Termination reason: Inappropriate
% 21.90/3.35 % (3772183)Time elapsed: 0.0000 s
% 21.90/3.35 % (3772183)Peak memory usage: 11 MB
% 21.90/3.35 % (3772183)------------------------------
% 21.90/3.35 % (3772183)------------------------------
% 21.90/3.35 % (3772185)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=122897413:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 21.90/3.35 % (3772185)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.90/3.35 % (3772185)Terminated due to inappropriate strategy.
% 21.90/3.35 % (3772185)------------------------------
% 21.90/3.35 % (3772185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.90/3.35 % (3772185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.90/3.35 % (3772185)CaDiCaL version: 2.1.3
% 21.90/3.35 % (3772185)Termination reason: Inappropriate
% 21.90/3.35 % (3772185)Time elapsed: 0.0000 s
% 21.90/3.35 % (3772185)Peak memory usage: 10 MB
% 21.90/3.35 % (3772185)------------------------------
% 21.90/3.35 % (3772185)------------------------------
% 21.90/3.35 % (3772187)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=429873113:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 21.90/3.35 % (3772187)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.90/3.35 % (3772187)Terminated due to inappropriate strategy.
% 21.90/3.35 % (3772187)------------------------------
% 21.90/3.35 % (3772187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.90/3.35 % (3772187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.90/3.35 % (3772187)CaDiCaL version: 2.1.3
% 21.90/3.35 % (3772187)Termination reason: Inappropriate
% 21.90/3.35 % (3772187)Time elapsed: 0.0000 s
% 21.90/3.35 % (3772187)Peak memory usage: 10 MB
% 21.90/3.35 % (3772187)------------------------------
% 21.90/3.35 % (3772187)------------------------------
% 21.90/3.35 % (3772189)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1156549068:i=5131_2997 on theBenchmark for (2997ds/5131Mi)
% 21.90/3.35 % (3772170)Instruction limit reached!
% 21.90/3.35 % (3772170)------------------------------
% 21.90/3.35 % (3772170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.90/3.35 % (3772170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.90/3.35 % (3772170)CaDiCaL version: 2.1.3
% 21.90/3.35 % (3772170)Termination reason: Instruction limit
% 21.90/3.35 % (3772170)Termination phase: Saturation
% 21.90/3.35 % (3772170)Time elapsed: 0.307 s
% 21.90/3.35 % (3772170)Peak memory usage: 13 MB
% 21.90/3.35 % (3772170)Instructions burned: 477 (million)
% 21.90/3.35 % (3772191)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2442963279:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 21.90/3.35 % (3772179)Instruction limit reached!
% 21.90/3.35 % (3772179)------------------------------
% 21.90/3.35 % (3772179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.90/3.35 % (3772179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.90/3.35 % (3772179)CaDiCaL version: 2.1.3
% 21.90/3.35 % (3772179)Termination reason: Instruction limit
% 28.30/4.20 % (3772179)Termination phase: Saturation
% 28.30/4.20 % (3772179)Time elapsed: 0.388 s
% 28.30/4.20 % (3772179)Peak memory usage: 17 MB
% 28.30/4.20 % (3772179)Instructions burned: 695 (million)
% 28.30/4.20 % (3772193)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3487183660:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 28.30/4.20 % (3772193)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.30/4.20 % (3772193)Terminated due to inappropriate strategy.
% 28.30/4.20 % (3772193)------------------------------
% 28.30/4.20 % (3772193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.30/4.20 % (3772193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.30/4.20 % (3772193)CaDiCaL version: 2.1.3
% 28.30/4.20 % (3772193)Termination reason: Inappropriate
% 28.30/4.20 % (3772193)Time elapsed: 0.0000 s
% 28.30/4.20 % (3772193)Peak memory usage: 10 MB
% 28.30/4.20 % (3772193)------------------------------
% 28.30/4.20 % (3772193)------------------------------
% 28.30/4.20 % (3772195)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3960176609:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 28.30/4.20 % (3772195)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.30/4.20 % (3772195)Terminated due to inappropriate strategy.
% 28.30/4.20 % (3772195)------------------------------
% 28.30/4.20 % (3772195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.30/4.20 % (3772195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.30/4.20 % (3772195)CaDiCaL version: 2.1.3
% 28.30/4.20 % (3772195)Termination reason: Inappropriate
% 28.30/4.20 % (3772195)Time elapsed: 0.0000 s
% 28.30/4.20 % (3772195)Peak memory usage: 10 MB
% 28.30/4.20 % (3772195)------------------------------
% 28.30/4.20 % (3772195)------------------------------
% 28.30/4.20 % (3772197)ott-2_1_sil=16000:newcnf=on:random_seed=3601113121:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 28.30/4.20 % (3772180)Instruction limit reached!
% 28.30/4.20 % (3772180)------------------------------
% 28.30/4.20 % (3772180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.30/4.20 % (3772180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.30/4.20 % (3772180)CaDiCaL version: 2.1.3
% 28.30/4.20 % (3772180)Termination reason: Instruction limit
% 28.30/4.20 % (3772180)Termination phase: Saturation
% 28.30/4.20 % (3772180)Time elapsed: 0.498 s
% 28.30/4.20 % (3772180)Peak memory usage: 19 MB
% 28.30/4.20 % (3772180)Instructions burned: 881 (million)
% 28.30/4.20 % (3772199)ott+10_1_sil=32000:tgt=ground:random_seed=32441866:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 28.30/4.20 % (3772175)Instruction limit reached!
% 28.30/4.20 % (3772175)------------------------------
% 28.30/4.20 % (3772175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.30/4.20 % (3772175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.30/4.20 % (3772175)CaDiCaL version: 2.1.3
% 28.30/4.20 % (3772175)Termination reason: Instruction limit
% 28.30/4.20 % (3772175)Termination phase: Saturation
% 28.30/4.20 % (3772175)Time elapsed: 0.613 s
% 28.30/4.20 % (3772175)Peak memory usage: 18 MB
% 28.30/4.20 % (3772175)Instructions burned: 1180 (million)
% 28.30/4.20 % (3772201)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1164186680:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 28.30/4.20 % (3772201)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.30/4.20 % (3772201)Terminated due to inappropriate strategy.
% 28.30/4.20 % (3772201)------------------------------
% 28.30/4.20 % (3772201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.30/4.20 % (3772201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.30/4.20 % (3772201)CaDiCaL version: 2.1.3
% 28.30/4.20 % (3772201)Termination reason: Inappropriate
% 28.30/4.20 % (3772201)Time elapsed: 0.0000 s
% 28.30/4.20 % (3772201)Peak memory usage: 11 MB
% 28.30/4.20 % (3772201)------------------------------
% 28.30/4.20 % (3772201)------------------------------
% 28.30/4.20 % (3772203)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4014449108:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 28.30/4.20 % (3772197)Instruction limit reached!
% 28.30/4.20 % (3772197)------------------------------
% 28.30/4.20 % (3772197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.30/4.20 % (3772197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772197)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772197)Termination reason: Instruction limit
% 43.12/9.14 % (3772197)Termination phase: Saturation
% 43.12/9.14 % (3772197)Time elapsed: 0.511 s
% 43.12/9.14 % (3772197)Peak memory usage: 14 MB
% 43.12/9.14 % (3772197)Instructions burned: 869 (million)
% 43.12/9.14 % (3772205)dis+21_1_sil=32000:sas=cadical:random_seed=3038835677:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 43.12/9.14 % (3772191)Instruction limit reached!
% 43.12/9.14 % (3772191)------------------------------
% 43.12/9.14 % (3772191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772191)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772191)Termination reason: Instruction limit
% 43.12/9.14 % (3772191)Termination phase: Saturation
% 43.12/9.14 % (3772191)Time elapsed: 0.877 s
% 43.12/9.14 % (3772191)Peak memory usage: 26 MB
% 43.12/9.14 % (3772191)Instructions burned: 1473 (million)
% 43.12/9.14 % (3772207)ott+11_1_sil=16000:gs=on:random_seed=1444859442:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi)
% 43.12/9.14 % (3772189)Instruction limit reached!
% 43.12/9.14 % (3772189)------------------------------
% 43.12/9.14 % (3772189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772189)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772189)Termination reason: Instruction limit
% 43.12/9.14 % (3772189)Termination phase: Saturation
% 43.12/9.14 % (3772189)Time elapsed: 1.502 s
% 43.12/9.14 % (3772189)Peak memory usage: 40 MB
% 43.12/9.14 % (3772189)Instructions burned: 5133 (million)
% 43.12/9.14 % (3772209)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1032247892:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi)
% 43.12/9.14 % (3772209)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 43.12/9.14 % (3772209)Terminated due to inappropriate strategy.
% 43.12/9.14 % (3772209)------------------------------
% 43.12/9.14 % (3772209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772209)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772209)Termination reason: Inappropriate
% 43.12/9.14 % (3772209)Time elapsed: 0.0000 s
% 43.12/9.14 % (3772209)Peak memory usage: 10 MB
% 43.12/9.14 % (3772209)------------------------------
% 43.12/9.14 % (3772209)------------------------------
% 43.12/9.14 % (3772211)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1534739686:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi)
% 43.12/9.14 % (3772207)Instruction limit reached!
% 43.12/9.14 % (3772207)------------------------------
% 43.12/9.14 % (3772207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772207)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772207)Termination reason: Instruction limit
% 43.12/9.14 % (3772207)Termination phase: Saturation
% 43.12/9.14 % (3772207)Time elapsed: 1.253 s
% 43.12/9.14 % (3772207)Peak memory usage: 26 MB
% 43.12/9.14 % (3772207)Instructions burned: 2251 (million)
% 43.12/9.14 % (3772213)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3618447558:i=29340_2973 on theBenchmark for (2973ds/29340Mi)
% 43.12/9.14 % (3772203)Instruction limit reached!
% 43.12/9.14 % (3772203)------------------------------
% 43.12/9.14 % (3772203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772203)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772203)Termination reason: Instruction limit
% 43.12/9.14 % (3772203)Termination phase: Saturation
% 43.12/9.14 % (3772203)Time elapsed: 1.938 s
% 43.12/9.14 % (3772203)Peak memory usage: 47 MB
% 43.12/9.14 % (3772203)Instructions burned: 3512 (million)
% 43.12/9.14 % (3772215)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2144707038:i=5211_2972 on theBenchmark for (2972ds/5211Mi)
% 43.12/9.14 % (3772211)Instruction limit reached!
% 43.12/9.14 % (3772211)------------------------------
% 43.12/9.14 % (3772211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772211)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772211)Termination reason: Instruction limit
% 43.12/9.14 % (3772211)Termination phase: Saturation
% 43.12/9.14 % (3772211)Time elapsed: 1.323 s
% 43.12/9.14 % (3772211)Peak memory usage: 44 MB
% 43.12/9.14 % (3772211)Instructions burned: 4596 (million)
% 43.12/9.14 % (3772217)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3163017481:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi)
% 43.12/9.14 % (3772217)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 43.12/9.14 % (3772217)Terminated due to inappropriate strategy.
% 43.12/9.14 % (3772217)------------------------------
% 43.12/9.14 % (3772217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772217)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772217)Termination reason: Inappropriate
% 43.12/9.14 % (3772217)Time elapsed: 0.0000 s
% 43.12/9.14 % (3772217)Peak memory usage: 10 MB
% 43.12/9.14 % (3772217)------------------------------
% 43.12/9.14 % (3772217)------------------------------
% 43.12/9.14 % (3772219)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1953361057:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi)
% 43.12/9.14 % (3772219)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 43.12/9.14 % (3772219)Terminated due to inappropriate strategy.
% 43.12/9.14 % (3772219)------------------------------
% 43.12/9.14 % (3772219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772219)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772219)Termination reason: Inappropriate
% 43.12/9.14 % (3772219)Time elapsed: 0.0000 s
% 43.12/9.14 % (3772219)Peak memory usage: 11 MB
% 43.12/9.14 % (3772219)------------------------------
% 43.12/9.14 % (3772219)------------------------------
% 43.12/9.14 % (3772221)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3108519261:i=14071_2968 on theBenchmark for (2968ds/14071Mi)
% 43.12/9.14 % (3772221)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 43.12/9.14 % (3772221)Terminated due to inappropriate strategy.
% 43.12/9.14 % (3772221)------------------------------
% 43.12/9.14 % (3772221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772221)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772221)Termination reason: Inappropriate
% 43.12/9.14 % (3772221)Time elapsed: 0.0000 s
% 43.12/9.14 % (3772221)Peak memory usage: 10 MB
% 43.12/9.14 % (3772221)------------------------------
% 43.12/9.14 % (3772221)------------------------------
% 43.12/9.14 % (3772223)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2562384785:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi)
% 43.12/9.14 % (3772205)Instruction limit reached!
% 43.12/9.14 % (3772205)------------------------------
% 43.12/9.14 % (3772205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772205)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772205)Termination reason: Instruction limit
% 43.12/9.14 % (3772205)Termination phase: Saturation
% 43.12/9.14 % (3772205)Time elapsed: 2.080 s
% 43.12/9.14 % (3772205)Peak memory usage: 33 MB
% 43.12/9.14 % (3772205)Instructions burned: 3773 (million)
% 43.12/9.14 % (3772225)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3832510323:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi)
% 43.12/9.14 % (3772199)Instruction limit reached!
% 43.12/9.14 % (3772199)------------------------------
% 43.12/9.14 % (3772199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772199)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772199)Termination reason: Instruction limit
% 43.12/9.14 % (3772199)Termination phase: Saturation
% 43.12/9.14 % (3772199)Time elapsed: 3.232 s
% 43.12/9.14 % (3772199)Peak memory usage: 34 MB
% 43.12/9.14 % (3772199)Instructions burned: 5114 (million)
% 43.12/9.14 % (3772227)dis+10_16:1_sil=16000:random_seed=1855936583:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi)
% 43.12/9.14 % (3772215)Instruction limit reached!
% 43.12/9.14 % (3772215)------------------------------
% 43.12/9.14 % (3772215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772215)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772215)Termination reason: Instruction limit
% 43.12/9.14 % (3772215)Termination phase: Saturation
% 43.12/9.14 % (3772215)Time elapsed: 2.789 s
% 43.12/9.14 % (3772215)Peak memory usage: 43 MB
% 43.12/9.14 % (3772215)Instructions burned: 5212 (million)
% 43.12/9.14 % (3772229)ott-3_8_sil=64000:random_seed=200946351:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi)
% 43.12/9.14 % (3772223)Instruction limit reached!
% 43.12/9.14 % (3772223)------------------------------
% 43.12/9.14 % (3772223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772223)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772223)Termination reason: Instruction limit
% 43.12/9.14 % (3772223)Termination phase: Saturation
% 43.12/9.14 % (3772223)Time elapsed: 5.074 s
% 43.12/9.14 % (3772223)Peak memory usage: 76 MB
% 43.12/9.14 % (3772223)Instructions burned: 22566 (million)
% 43.12/9.14 % (3772231)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3915580889:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi)
% 43.12/9.14 % (3772231)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 43.12/9.14 % (3772231)Terminated due to inappropriate strategy.
% 43.12/9.14 % (3772231)------------------------------
% 43.12/9.14 % (3772231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772231)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772231)Termination reason: Inappropriate
% 43.12/9.14 % (3772231)Time elapsed: 0.0000 s
% 43.12/9.14 % (3772231)Peak memory usage: 10 MB
% 43.12/9.14 % (3772231)------------------------------
% 43.12/9.14 % (3772231)------------------------------
% 43.12/9.14 % (3772233)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3068690884:i=11404_2917 on theBenchmark for (2917ds/11404Mi)
% 43.12/9.14 % (3772225)Instruction limit reached!
% 43.12/9.14 % (3772225)------------------------------
% 43.12/9.14 % (3772225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772225)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772225)Termination reason: Instruction limit
% 43.12/9.14 % (3772225)Termination phase: Saturation
% 43.12/9.14 % (3772225)Time elapsed: 5.064 s
% 43.12/9.14 % (3772225)Peak memory usage: 54 MB
% 43.12/9.14 % (3772225)Instructions burned: 8173 (million)
% 43.12/9.14 % (3772235)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1898656861:i=14134_2916 on theBenchmark for (2916ds/14134Mi)
% 43.12/9.14 % (3772227)Instruction limit reached!
% 43.12/9.14 % (3772227)------------------------------
% 43.12/9.14 % (3772227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772227)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772227)Termination reason: Instruction limit
% 43.12/9.14 % (3772227)Termination phase: Saturation
% 43.12/9.14 % (3772227)Time elapsed: 4.655 s
% 43.12/9.14 % (3772227)Peak memory usage: 52 MB
% 43.12/9.14 % (3772227)Instructions burned: 9155 (million)
% 43.12/9.14 % (3772237)dis+33_16_sil=32000:sac=on:random_seed=161000733:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi)
% 43.12/9.14 % (3772150) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3772144-3772150"...
% 43.12/9.14 % (3772150)...printing done.
% 43.12/9.14 % (3772150)Refutation found. Thanks to Tanya!
% 43.12/9.14 % SZS status Theorem for theBenchmark
% 43.12/9.14 % SZS output start Proof for theBenchmark
% 43.12/9.14 tff(func_def_6, type, sK0: $int).
% 43.12/9.14 tff(f1,conjecture,(
% 43.12/9.14 ! [X0 : $int] : ($less(0,X0) => ? [X1 : $int] : ($less(X0,X1) & $less(X1,$product(X0,3))))),
% 43.12/9.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exists_Y_between_X_and_3X)).
% 43.12/9.14 tff(f2,negated_conjecture,(
% 43.12/9.14 ~ ! [X0 : $int] : ($less(0,X0) => ? [X1 : $int] : ($less(X0,X1) & $less(X1,$product(X0,3))))),
% 43.12/9.14 inference(negated_conjecture,[status(cth)],[f1])).
% 43.12/9.14 tff(f4,definition,(
% 43.12/9.14 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 43.12/9.14 introduced(theory,[tha_associativity])).
% 43.12/9.14 tff(f7,definition,(
% 43.12/9.14 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 43.12/9.14 introduced(theory,[tha_inverse_op_unit])).
% 43.12/9.14 tff(f11,definition,(
% 43.12/9.14 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,X2),$sum(X1,X2))) )),
% 43.12/9.14 introduced(theory,[tha_order_monotonicity])).
% 43.12/9.14 tff(f14,definition,(
% 43.12/9.14 ( ! [X0 : $int,X1 : $int] : ($product(X0,X1) = $product(X1,X0)) )),
% 43.12/9.14 introduced(theory,[tha_commutativity])).
% 43.12/9.14 tff(f16,definition,(
% 43.12/9.14 ( ! [X0 : $int] : ($product(X0,1) = X0) )),
% 43.12/9.14 introduced(theory,[tha_right_identity])).
% 43.12/9.14 tff(f18,definition,(
% 43.12/9.14 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2))) )),
% 43.12/9.14 introduced(theory,[tha_distributivity])).
% 43.12/9.14 tff(f21,plain,(
% 43.12/9.14 ? [X0 : $int] : (! [X1 : $int] : (~$less(X0,X1) | ~$less(X1,$product(X0,3))) & $less(0,X0))),
% 43.12/9.14 inference(ennf_transformation,[],[f2])).
% 43.12/9.14 tff(f22,plain,(
% 43.12/9.14 ( ! [X1 : $int] : (~$less(X1,$product(sK0,3)) | ~$less(sK0,X1)) )),
% 43.12/9.14 inference(cnf_transformation,[],[f21])).
% 43.12/9.14 tff(f23,plain,(
% 43.12/9.14 $less(0,sK0)),
% 43.12/9.14 inference(cnf_transformation,[],[f21])).
% 43.12/9.14 tff(f73,plain,(
% 43.12/9.14 ( ! [X0 : $int] : ($less($sum(0,X0),$sum(sK0,X0))) )),
% 43.12/9.14 inference(resolution,[],[f11,f23])).
% 43.12/9.14 tff(f78,plain,(
% 43.12/9.14 ( ! [X0 : $int] : ($less(X0,$sum(sK0,X0))) )),
% 43.12/9.14 inference(evaluation,[],[f73])).
% 43.12/9.14 tff(f80,plain,(
% 43.12/9.14 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 43.12/9.14 inference(superposition,[],[f4,f7])).
% 43.12/9.14 tff(f95,plain,(
% 43.12/9.14 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 43.12/9.14 inference(evaluation,[],[f80])).
% 43.12/9.14 tff(f113,plain,(
% 43.12/9.14 ( ! [X0 : $int,X1 : $int] : ($product(X0,$sum(1,X1)) = $sum(X0,$product(X0,X1))) )),
% 43.12/9.14 inference(superposition,[],[f18,f16])).
% 43.12/9.14 tff(f760,plain,(
% 43.12/9.14 ( ! [X0 : $int] : ($less($product(sK0,X0),$product(sK0,$sum(1,X0)))) )),
% 43.12/9.14 inference(superposition,[],[f78,f113])).
% 43.12/9.14 tff(f1942,plain,(
% 43.12/9.14 $less(sK0,$product(sK0,$sum(1,1)))),
% 43.12/9.14 inference(superposition,[],[f760,f16])).
% 43.12/9.14 tff(f1947,plain,(
% 43.12/9.14 ( ! [X0 : $int] : ($less($product(sK0,$sum($uminus(1),X0)),$product(sK0,X0))) )),
% 43.12/9.14 inference(superposition,[],[f760,f95])).
% 43.12/9.14 tff(f1954,plain,(
% 43.12/9.14 ( ! [X0 : $int] : ($less($product(sK0,$sum(-1,X0)),$product(sK0,X0))) )),
% 43.12/9.14 inference(evaluation,[],[f1947])).
% 43.12/9.14 tff(f1957,plain,(
% 43.12/9.14 $less(sK0,$product(sK0,2))),
% 43.12/9.14 inference(evaluation,[],[f1942])).
% 43.12/9.14 tff(f1959,plain,(
% 43.12/9.14 $less(sK0,$product(2,sK0))),
% 43.12/9.14 inference(forward_demodulation,[],[f1957,f14])).
% 43.12/9.14 tff(f247426,plain,(
% 43.12/9.14 ~$less(sK0,$product(sK0,$sum(-1,3)))),
% 43.12/9.14 inference(resolution,[],[f1954,f22])).
% 43.12/9.14 tff(f247542,plain,(
% 43.12/9.14 ~$less(sK0,$product(sK0,2))),
% 43.12/9.14 inference(evaluation,[],[f247426])).
% 43.12/9.14 tff(f247554,plain,(
% 43.12/9.14 ~$less(sK0,$product(2,sK0))),
% 43.12/9.14 inference(forward_demodulation,[],[f247542,f14])).
% 43.12/9.14 tff(f247560,plain,(
% 43.12/9.14 $false),
% 43.12/9.14 inference(forward_subsumption_resolution,[],[f247554,f1959])).
% 43.12/9.14 % SZS output end Proof for theBenchmark
% 43.12/9.14 % (3772150)------------------------------
% 43.12/9.14 % (3772150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.12/9.14 % (3772150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.12/9.14 % (3772150)CaDiCaL version: 2.1.3
% 43.12/9.14 % (3772150)Termination reason: Refutation
% 43.12/9.14 % (3772150)Time elapsed: 8.869 s
% 43.12/9.14 % (3772150)Peak memory usage: 115 MB
% 43.12/9.14 % (3772150)Instructions burned: 17037 (million)
% 43.12/9.14 % (3772144)Success in time 8.926 s
% 43.12/9.14 % Vampire exiting
%------------------------------------------------------------------------------