%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI182_1 : TPTP v9.3.1. Released v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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:08 AM UTC 2026
% Result : Theorem 184.62s 30.74s
% Output : Refutation 184.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ARI182_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n018.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 20:46:40 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 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
% 2.85/0.69 % (3748375)Will run a generic schedule for satisfiability detection.
% 2.85/0.69 % (3748380)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2991793446_2999 on theBenchmark for (2999ds/0Mi)
% 2.85/0.69 % (3748380)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.85/0.69 % (3748380)Terminated due to inappropriate strategy.
% 2.85/0.69 % (3748380)------------------------------
% 2.85/0.69 % (3748380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.85/0.69 % (3748380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.85/0.69 % (3748380)CaDiCaL version: 2.1.3
% 2.85/0.69 % (3748380)Termination reason: Inappropriate
% 2.85/0.69 % (3748380)Time elapsed: 0.0000 s
% 2.85/0.69 % (3748380)Peak memory usage: 10 MB
% 2.85/0.69 % (3748380)------------------------------
% 2.85/0.69 % (3748380)------------------------------
% 2.85/0.69 % (3748381)% WARNING: option uhcvi not known.
% 2.85/0.69 % (3748381)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=530680315:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.85/0.69 % (3748382)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2968595166:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.85/0.69 % (3748383)dis+10_1_sil=32000:sp=arity:random_seed=1231731989:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.85/0.69 % (3748384)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1527311873:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.85/0.69 % (3748388)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3660943944:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.85/0.69 % (3748388)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.85/0.69 % (3748388)Terminated due to inappropriate strategy.
% 2.85/0.69 % (3748388)------------------------------
% 2.85/0.69 % (3748388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.85/0.69 % (3748388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.85/0.69 % (3748388)CaDiCaL version: 2.1.3
% 2.85/0.69 % (3748388)Termination reason: Inappropriate
% 2.85/0.69 % (3748388)Time elapsed: 0.0000 s
% 2.85/0.69 % (3748388)Peak memory usage: 10 MB
% 2.85/0.69 % (3748388)------------------------------
% 2.85/0.69 % (3748388)------------------------------
% 2.85/0.69 % (3748386)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2315128855:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.85/0.69 % (3748394)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1552384119:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.85/0.69 % (3748385)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1017930557:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.85/0.69 % (3748383)Instruction limit reached!
% 2.85/0.69 % (3748383)------------------------------
% 2.85/0.69 % (3748383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.85/0.69 % (3748383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.85/0.69 % (3748383)CaDiCaL version: 2.1.3
% 2.85/0.69 % (3748383)Termination reason: Instruction limit
% 2.85/0.69 % (3748383)Termination phase: Saturation
% 2.85/0.69 % (3748383)Time elapsed: 0.065 s
% 2.85/0.69 % (3748383)Peak memory usage: 12 MB
% 2.85/0.69 % (3748383)Instructions burned: 103 (million)
% 2.85/0.69 % (3748394)Instruction limit reached!
% 2.85/0.69 % (3748394)------------------------------
% 2.85/0.69 % (3748394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.85/0.69 % (3748394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.85/0.69 % (3748394)CaDiCaL version: 2.1.3
% 2.85/0.69 % (3748394)Termination reason: Instruction limit
% 2.85/0.69 % (3748394)Termination phase: Saturation
% 2.85/0.69 % (3748394)Time elapsed: 0.049 s
% 2.85/0.69 % (3748394)Peak memory usage: 13 MB
% 2.85/0.69 % (3748394)Instructions burned: 132 (million)
% 2.85/0.69 % (3748399)ott-21_1_sil=16000:fs=off:random_seed=4175945557:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 2.85/0.69 % (3748384)Instruction limit reached!
% 2.85/0.69 % (3748384)------------------------------
% 2.85/0.69 % (3748384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.85/0.69 % (3748384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.85/0.69 % (3748384)CaDiCaL version: 2.1.3
% 7.35/1.32 % (3748384)Termination reason: Instruction limit
% 7.35/1.32 % (3748384)Termination phase: Saturation
% 7.35/1.32 % (3748384)Time elapsed: 0.074 s
% 7.35/1.32 % (3748384)Peak memory usage: 12 MB
% 7.35/1.32 % (3748384)Instructions burned: 117 (million)
% 7.35/1.32 % (3748398)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=3329276433:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 7.35/1.32 % (3748401)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1389838124:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.35/1.32 % (3748385)Instruction limit reached!
% 7.35/1.32 % (3748385)------------------------------
% 7.35/1.32 % (3748385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.35/1.32 % (3748385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.35/1.32 % (3748385)CaDiCaL version: 2.1.3
% 7.35/1.32 % (3748385)Termination reason: Instruction limit
% 7.35/1.32 % (3748385)Termination phase: Saturation
% 7.35/1.32 % (3748385)Time elapsed: 0.091 s
% 7.35/1.32 % (3748385)Peak memory usage: 12 MB
% 7.35/1.32 % (3748385)Instructions burned: 131 (million)
% 7.35/1.32 % (3748386)Instruction limit reached!
% 7.35/1.32 % (3748386)------------------------------
% 7.35/1.32 % (3748386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.35/1.32 % (3748386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.35/1.32 % (3748386)CaDiCaL version: 2.1.3
% 7.35/1.32 % (3748386)Termination reason: Instruction limit
% 7.35/1.32 % (3748386)Termination phase: Saturation
% 7.35/1.32 % (3748386)Time elapsed: 0.107 s
% 7.35/1.32 % (3748386)Peak memory usage: 13 MB
% 7.35/1.32 % (3748386)Instructions burned: 160 (million)
% 7.35/1.32 % (3748399)Instruction limit reached!
% 7.35/1.32 % (3748399)------------------------------
% 7.35/1.32 % (3748399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.35/1.32 % (3748399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.35/1.32 % (3748399)CaDiCaL version: 2.1.3
% 7.35/1.32 % (3748399)Termination reason: Instruction limit
% 7.35/1.32 % (3748399)Termination phase: Saturation
% 7.35/1.32 % (3748399)Time elapsed: 0.043 s
% 7.35/1.32 % (3748399)Peak memory usage: 12 MB
% 7.35/1.32 % (3748399)Instructions burned: 183 (million)
% 7.35/1.32 % (3748406)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=751172160:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 7.35/1.32 % (3748406)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.35/1.32 % (3748406)Terminated due to inappropriate strategy.
% 7.35/1.32 % (3748406)------------------------------
% 7.35/1.32 % (3748406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.35/1.32 % (3748406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.35/1.32 % (3748406)CaDiCaL version: 2.1.3
% 7.35/1.32 % (3748406)Termination reason: Inappropriate
% 7.35/1.32 % (3748406)Time elapsed: 0.0000 s
% 7.35/1.32 % (3748406)Peak memory usage: 10 MB
% 7.35/1.32 % (3748406)------------------------------
% 7.35/1.32 % (3748406)------------------------------
% 7.35/1.32 % (3748404)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3779707576:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.35/1.32 % (3748404)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.35/1.32 % (3748404)Terminated due to inappropriate strategy.
% 7.35/1.32 % (3748404)------------------------------
% 7.35/1.32 % (3748404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.35/1.32 % (3748404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.35/1.32 % (3748404)CaDiCaL version: 2.1.3
% 7.35/1.32 % (3748404)Termination reason: Inappropriate
% 7.35/1.32 % (3748404)Time elapsed: 0.0000 s
% 7.35/1.32 % (3748404)Peak memory usage: 10 MB
% 7.35/1.32 % (3748405)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=958003259:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.35/1.32 % (3748404)------------------------------
% 7.35/1.32 % (3748404)------------------------------
% 7.35/1.32 % (3748409)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=3713066162: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.35/1.32 % (3748411)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=95416487:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 22.93/3.65 % (3748409)Instruction limit reached!
% 22.93/3.65 % (3748409)------------------------------
% 22.93/3.65 % (3748409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.65 % (3748409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.65 % (3748409)CaDiCaL version: 2.1.3
% 22.93/3.65 % (3748409)Termination reason: Instruction limit
% 22.93/3.65 % (3748409)Termination phase: Saturation
% 22.93/3.65 % (3748409)Time elapsed: 0.217 s
% 22.93/3.65 % (3748409)Peak memory usage: 17 MB
% 22.93/3.65 % (3748409)Instructions burned: 695 (million)
% 22.93/3.65 % (3748484)fmb+10_1_sil=64000:random_seed=3455778043:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 22.93/3.65 % (3748484)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 22.93/3.65 % (3748484)Terminated due to inappropriate strategy.
% 22.93/3.65 % (3748484)------------------------------
% 22.93/3.65 % (3748484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.65 % (3748484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.65 % (3748484)CaDiCaL version: 2.1.3
% 22.93/3.65 % (3748484)Termination reason: Inappropriate
% 22.93/3.65 % (3748484)Time elapsed: 0.0000 s
% 22.93/3.65 % (3748484)Peak memory usage: 10 MB
% 22.93/3.65 % (3748484)------------------------------
% 22.93/3.65 % (3748484)------------------------------
% 22.93/3.65 % (3748490)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1529745761:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 22.93/3.65 % (3748490)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 22.93/3.65 % (3748490)Terminated due to inappropriate strategy.
% 22.93/3.65 % (3748490)------------------------------
% 22.93/3.65 % (3748490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.65 % (3748490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.65 % (3748490)CaDiCaL version: 2.1.3
% 22.93/3.65 % (3748490)Termination reason: Inappropriate
% 22.93/3.65 % (3748490)Time elapsed: 0.0000 s
% 22.93/3.65 % (3748490)Peak memory usage: 10 MB
% 22.93/3.65 % (3748490)------------------------------
% 22.93/3.65 % (3748490)------------------------------
% 22.93/3.65 % (3748401)Instruction limit reached!
% 22.93/3.65 % (3748401)------------------------------
% 22.93/3.65 % (3748401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.65 % (3748401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.65 % (3748401)CaDiCaL version: 2.1.3
% 22.93/3.65 % (3748401)Termination reason: Instruction limit
% 22.93/3.65 % (3748401)Termination phase: Saturation
% 22.93/3.65 % (3748401)Time elapsed: 0.292 s
% 22.93/3.65 % (3748401)Peak memory usage: 14 MB
% 22.93/3.65 % (3748401)Instructions burned: 478 (million)
% 22.93/3.65 % (3748497)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1505401341:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 22.93/3.65 % (3748497)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 22.93/3.65 % (3748497)Terminated due to inappropriate strategy.
% 22.93/3.65 % (3748497)------------------------------
% 22.93/3.65 % (3748497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.65 % (3748497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.65 % (3748497)CaDiCaL version: 2.1.3
% 22.93/3.65 % (3748497)Termination reason: Inappropriate
% 22.93/3.65 % (3748497)Time elapsed: 0.0000 s
% 22.93/3.65 % (3748497)Peak memory usage: 10 MB
% 22.93/3.65 % (3748497)------------------------------
% 22.93/3.65 % (3748497)------------------------------
% 22.93/3.65 % (3748499)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1243519486:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 22.93/3.65 % (3748504)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=81660156:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 22.93/3.65 % (3748398)Instruction limit reached!
% 22.93/3.65 % (3748398)------------------------------
% 22.93/3.65 % (3748398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.93/3.65 % (3748398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.65 % (3748398)CaDiCaL version: 2.1.3
% 22.93/3.65 % (3748398)Termination reason: Instruction limit
% 32.58/4.90 % (3748398)Termination phase: Saturation
% 32.58/4.90 % (3748398)Time elapsed: 0.344 s
% 32.58/4.90 % (3748398)Peak memory usage: 16 MB
% 32.58/4.90 % (3748398)Instructions burned: 684 (million)
% 32.58/4.90 % (3748519)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=444002904:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 32.58/4.90 % (3748519)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 32.58/4.90 % (3748519)Terminated due to inappropriate strategy.
% 32.58/4.90 % (3748519)------------------------------
% 32.58/4.90 % (3748519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.58/4.90 % (3748519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.58/4.90 % (3748519)CaDiCaL version: 2.1.3
% 32.58/4.90 % (3748519)Termination reason: Inappropriate
% 32.58/4.90 % (3748519)Time elapsed: 0.0000 s
% 32.58/4.90 % (3748519)Peak memory usage: 10 MB
% 32.58/4.90 % (3748519)------------------------------
% 32.58/4.90 % (3748519)------------------------------
% 32.58/4.90 % (3748529)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=636172335:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 32.58/4.90 % (3748529)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 32.58/4.90 % (3748529)Terminated due to inappropriate strategy.
% 32.58/4.90 % (3748529)------------------------------
% 32.58/4.90 % (3748529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.58/4.90 % (3748529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.58/4.90 % (3748529)CaDiCaL version: 2.1.3
% 32.58/4.90 % (3748529)Termination reason: Inappropriate
% 32.58/4.90 % (3748529)Time elapsed: 0.0000 s
% 32.58/4.90 % (3748529)Peak memory usage: 10 MB
% 32.58/4.90 % (3748529)------------------------------
% 32.58/4.90 % (3748529)------------------------------
% 32.58/4.90 % (3748531)ott-2_1_sil=16000:newcnf=on:random_seed=582141981:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi)
% 32.58/4.90 % (3748411)Instruction limit reached!
% 32.58/4.90 % (3748411)------------------------------
% 32.58/4.90 % (3748411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.58/4.90 % (3748411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.58/4.90 % (3748411)CaDiCaL version: 2.1.3
% 32.58/4.90 % (3748411)Termination reason: Instruction limit
% 32.58/4.90 % (3748411)Termination phase: Saturation
% 32.58/4.90 % (3748411)Time elapsed: 0.506 s
% 32.58/4.90 % (3748411)Peak memory usage: 18 MB
% 32.58/4.90 % (3748411)Instructions burned: 880 (million)
% 32.58/4.90 % (3748560)ott+10_1_sil=32000:tgt=ground:random_seed=467392746:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 32.58/4.90 % (3748405)Instruction limit reached!
% 32.58/4.90 % (3748405)------------------------------
% 32.58/4.90 % (3748405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.58/4.90 % (3748405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.58/4.90 % (3748405)CaDiCaL version: 2.1.3
% 32.58/4.90 % (3748405)Termination reason: Instruction limit
% 32.58/4.90 % (3748405)Termination phase: Saturation
% 32.58/4.90 % (3748405)Time elapsed: 0.655 s
% 32.58/4.90 % (3748405)Peak memory usage: 19 MB
% 32.58/4.90 % (3748405)Instructions burned: 1180 (million)
% 32.58/4.90 % (3748562)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1394494661:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 32.58/4.90 % (3748562)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 32.58/4.90 % (3748562)Terminated due to inappropriate strategy.
% 32.58/4.90 % (3748562)------------------------------
% 32.58/4.90 % (3748562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.58/4.90 % (3748562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.58/4.90 % (3748562)CaDiCaL version: 2.1.3
% 32.58/4.90 % (3748562)Termination reason: Inappropriate
% 32.58/4.90 % (3748562)Time elapsed: 0.0000 s
% 32.58/4.90 % (3748562)Peak memory usage: 10 MB
% 32.58/4.90 % (3748562)------------------------------
% 32.58/4.90 % (3748562)------------------------------
% 32.58/4.90 % (3748564)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1603366616:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 32.58/4.90 % (3748531)Instruction limit reached!
% 32.58/4.90 % (3748531)------------------------------
% 32.58/4.90 % (3748531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.58/4.90 % (3748531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.92/18.43 % (3748531)CaDiCaL version: 2.1.3
% 128.92/18.43 % (3748531)Termination reason: Instruction limit
% 128.92/18.43 % (3748531)Termination phase: Saturation
% 128.92/18.43 % (3748531)Time elapsed: 0.580 s
% 128.92/18.43 % (3748531)Peak memory usage: 16 MB
% 128.92/18.43 % (3748531)Instructions burned: 869 (million)
% 128.92/18.43 % (3748575)dis+21_1_sil=32000:sas=cadical:random_seed=1414365109:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 128.92/18.43 % (3748504)Instruction limit reached!
% 128.92/18.43 % (3748504)------------------------------
% 128.92/18.43 % (3748504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.92/18.43 % (3748504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.92/18.43 % (3748504)CaDiCaL version: 2.1.3
% 128.92/18.43 % (3748504)Termination reason: Instruction limit
% 128.92/18.43 % (3748504)Termination phase: Saturation
% 128.92/18.43 % (3748504)Time elapsed: 0.997 s
% 128.92/18.43 % (3748504)Peak memory usage: 23 MB
% 128.92/18.43 % (3748504)Instructions burned: 1472 (million)
% 128.92/18.43 % (3748590)ott+11_1_sil=16000:gs=on:random_seed=2107258697:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi)
% 128.92/18.43 % (3748590)Instruction limit reached!
% 128.92/18.43 % (3748590)------------------------------
% 128.92/18.43 % (3748590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.92/18.43 % (3748590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.92/18.43 % (3748590)CaDiCaL version: 2.1.3
% 128.92/18.43 % (3748590)Termination reason: Instruction limit
% 128.92/18.43 % (3748590)Termination phase: Saturation
% 128.92/18.43 % (3748590)Time elapsed: 1.302 s
% 128.92/18.43 % (3748590)Peak memory usage: 25 MB
% 128.92/18.43 % (3748590)Instructions burned: 2253 (million)
% 128.92/18.43 % (3748749)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2415423438:fmbsr=1.6:i=67534_2971 on theBenchmark for (2971ds/67534Mi)
% 128.92/18.43 % (3748749)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 128.92/18.43 % (3748749)Terminated due to inappropriate strategy.
% 128.92/18.43 % (3748749)------------------------------
% 128.92/18.43 % (3748749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.92/18.43 % (3748749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.92/18.43 % (3748749)CaDiCaL version: 2.1.3
% 128.92/18.43 % (3748749)Termination reason: Inappropriate
% 128.92/18.43 % (3748749)Time elapsed: 0.0000 s
% 128.92/18.43 % (3748749)Peak memory usage: 10 MB
% 128.92/18.43 % (3748749)------------------------------
% 128.92/18.43 % (3748749)------------------------------
% 128.92/18.43 % (3748751)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=996032690:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi)
% 128.92/18.43 % (3748564)Instruction limit reached!
% 128.92/18.43 % (3748564)------------------------------
% 128.92/18.43 % (3748564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.92/18.43 % (3748564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.92/18.43 % (3748564)CaDiCaL version: 2.1.3
% 128.92/18.43 % (3748564)Termination reason: Instruction limit
% 128.92/18.43 % (3748564)Termination phase: Saturation
% 128.92/18.43 % (3748564)Time elapsed: 2.128 s
% 128.92/18.43 % (3748564)Peak memory usage: 29 MB
% 128.92/18.43 % (3748564)Instructions burned: 3513 (million)
% 128.92/18.43 % (3748753)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4123865823:i=29340_2970 on theBenchmark for (2970ds/29340Mi)
% 128.92/18.43 % (3748575)Instruction limit reached!
% 128.92/18.43 % (3748575)------------------------------
% 128.92/18.43 % (3748575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.92/18.43 % (3748575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.92/18.43 % (3748575)CaDiCaL version: 2.1.3
% 128.92/18.43 % (3748575)Termination reason: Instruction limit
% 128.92/18.43 % (3748575)Termination phase: Saturation
% 128.92/18.43 % (3748575)Time elapsed: 2.211 s
% 128.92/18.43 % (3748575)Peak memory usage: 30 MB
% 128.92/18.43 % (3748575)Instructions burned: 3773 (million)
% 128.92/18.43 % (3748755)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3365603877:i=5211_2966 on theBenchmark for (2966ds/5211Mi)
% 128.92/18.43 % (3748499)Instruction limit reached!
% 128.92/18.43 % (3748499)------------------------------
% 128.92/18.43 % (3748499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.39/19.84 % (3748499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.39/19.84 % (3748499)CaDiCaL version: 2.1.3
% 138.39/19.84 % (3748499)Termination reason: Instruction limit
% 138.39/19.84 % (3748499)Termination phase: Saturation
% 138.39/19.84 % (3748499)Time elapsed: 2.987 s
% 138.39/19.84 % (3748499)Peak memory usage: 40 MB
% 138.39/19.84 % (3748499)Instructions burned: 5131 (million)
% 138.39/19.84 % (3748757)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1411957398:i=5497:nm=2_2965 on theBenchmark for (2965ds/5497Mi)
% 138.39/19.84 % (3748757)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 138.39/19.84 % (3748757)Terminated due to inappropriate strategy.
% 138.39/19.84 % (3748757)------------------------------
% 138.39/19.84 % (3748757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.39/19.84 % (3748757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.39/19.84 % (3748757)CaDiCaL version: 2.1.3
% 138.39/19.84 % (3748757)Termination reason: Inappropriate
% 138.39/19.84 % (3748757)Time elapsed: 0.0000 s
% 138.39/19.84 % (3748757)Peak memory usage: 10 MB
% 138.39/19.84 % (3748757)------------------------------
% 138.39/19.84 % (3748757)------------------------------
% 138.39/19.84 % (3748759)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2430596065:fmbsr=2:i=46332_2965 on theBenchmark for (2965ds/46332Mi)
% 138.39/19.84 % (3748759)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 138.39/19.84 % (3748759)Terminated due to inappropriate strategy.
% 138.39/19.84 % (3748759)------------------------------
% 138.39/19.84 % (3748759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.39/19.84 % (3748759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.39/19.84 % (3748759)CaDiCaL version: 2.1.3
% 138.39/19.84 % (3748759)Termination reason: Inappropriate
% 138.39/19.84 % (3748759)Time elapsed: 0.0000 s
% 138.39/19.84 % (3748759)Peak memory usage: 10 MB
% 138.39/19.84 % (3748759)------------------------------
% 138.39/19.84 % (3748759)------------------------------
% 138.39/19.84 % (3748761)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=312871045:i=14071_2965 on theBenchmark for (2965ds/14071Mi)
% 138.39/19.84 % (3748761)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 138.39/19.84 % (3748761)Terminated due to inappropriate strategy.
% 138.39/19.84 % (3748761)------------------------------
% 138.39/19.84 % (3748761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.39/19.84 % (3748761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.39/19.84 % (3748761)CaDiCaL version: 2.1.3
% 138.39/19.84 % (3748761)Termination reason: Inappropriate
% 138.39/19.84 % (3748761)Time elapsed: 0.0000 s
% 138.39/19.84 % (3748761)Peak memory usage: 11 MB
% 138.39/19.84 % (3748761)------------------------------
% 138.39/19.84 % (3748761)------------------------------
% 138.39/19.84 % (3748763)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3469258571:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi)
% 138.39/19.84 % (3748560)Instruction limit reached!
% 138.39/19.84 % (3748560)------------------------------
% 138.39/19.84 % (3748560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.39/19.84 % (3748560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.39/19.84 % (3748560)CaDiCaL version: 2.1.3
% 138.39/19.84 % (3748560)Termination reason: Instruction limit
% 138.39/19.84 % (3748560)Termination phase: Saturation
% 138.39/19.84 % (3748560)Time elapsed: 3.469 s
% 138.39/19.84 % (3748560)Peak memory usage: 33 MB
% 138.39/19.84 % (3748560)Instructions burned: 5115 (million)
% 138.39/19.84 % (3748765)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3694895476:i=8173:av=off_2958 on theBenchmark for (2958ds/8173Mi)
% 138.39/19.84 % (3748751)Instruction limit reached!
% 138.39/19.84 % (3748751)------------------------------
% 138.39/19.84 % (3748751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.39/19.84 % (3748751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.39/19.84 % (3748751)CaDiCaL version: 2.1.3
% 138.39/19.84 % (3748751)Termination reason: Instruction limit
% 138.39/19.84 % (3748751)Termination phase: Saturation
% 138.39/19.84 % (3748751)Time elapsed: 1.801 s
% 138.39/19.84 % (3748751)Peak memory usage: 24 MB
% 138.39/19.84 % (3748751)Instructions burned: 4592 (million)
% 138.39/19.84 % (3748767)dis+10_16:1_sil=16000:random_seed=3578269474:i=9155:fsr=off_2953 on theBenchmark for (2953ds/9155Mi)
% 197.99/28.14 % (3748755)Instruction limit reached!
% 197.99/28.14 % (3748755)------------------------------
% 197.99/28.14 % (3748755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.99/28.14 % (3748755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.99/28.14 % (3748755)CaDiCaL version: 2.1.3
% 197.99/28.14 % (3748755)Termination reason: Instruction limit
% 197.99/28.14 % (3748755)Termination phase: Saturation
% 197.99/28.14 % (3748755)Time elapsed: 2.821 s
% 197.99/28.14 % (3748755)Peak memory usage: 48 MB
% 197.99/28.14 % (3748755)Instructions burned: 5211 (million)
% 197.99/28.14 % (3748769)ott-3_8_sil=64000:random_seed=409978378:i=20139:bs=on_2937 on theBenchmark for (2937ds/20139Mi)
% 197.99/28.14 % (3748767)Instruction limit reached!
% 197.99/28.14 % (3748767)------------------------------
% 197.99/28.14 % (3748767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.99/28.14 % (3748767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.99/28.14 % (3748767)CaDiCaL version: 2.1.3
% 197.99/28.14 % (3748767)Termination reason: Instruction limit
% 197.99/28.14 % (3748767)Termination phase: Saturation
% 197.99/28.14 % (3748767)Time elapsed: 4.733 s
% 197.99/28.14 % (3748767)Peak memory usage: 50 MB
% 197.99/28.14 % (3748767)Instructions burned: 9155 (million)
% 197.99/28.14 % (3748771)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1523217772:fmbsr=2:i=32576_2905 on theBenchmark for (2905ds/32576Mi)
% 197.99/28.14 % (3748771)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 197.99/28.14 % (3748771)Terminated due to inappropriate strategy.
% 197.99/28.14 % (3748771)------------------------------
% 197.99/28.14 % (3748771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.99/28.14 % (3748771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.99/28.14 % (3748771)CaDiCaL version: 2.1.3
% 197.99/28.14 % (3748771)Termination reason: Inappropriate
% 197.99/28.14 % (3748771)Time elapsed: 0.001 s
% 197.99/28.14 % (3748771)Peak memory usage: 10 MB
% 197.99/28.14 % (3748771)------------------------------
% 197.99/28.14 % (3748771)------------------------------
% 197.99/28.14 % (3748773)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4291268317:i=11404_2905 on theBenchmark for (2905ds/11404Mi)
% 197.99/28.14 % (3748765)Instruction limit reached!
% 197.99/28.14 % (3748765)------------------------------
% 197.99/28.14 % (3748765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.99/28.14 % (3748765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.99/28.14 % (3748765)CaDiCaL version: 2.1.3
% 197.99/28.14 % (3748765)Termination reason: Instruction limit
% 197.99/28.14 % (3748765)Termination phase: Saturation
% 197.99/28.14 % (3748765)Time elapsed: 5.289 s
% 197.99/28.14 % (3748765)Peak memory usage: 43 MB
% 197.99/28.14 % (3748765)Instructions burned: 8173 (million)
% 197.99/28.14 % (3748775)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3261624900:i=14134_2905 on theBenchmark for (2905ds/14134Mi)
% 197.99/28.14 % (3748763)Instruction limit reached!
% 197.99/28.14 % (3748763)------------------------------
% 197.99/28.14 % (3748763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.99/28.14 % (3748763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.99/28.14 % (3748763)CaDiCaL version: 2.1.3
% 197.99/28.14 % (3748763)Termination reason: Instruction limit
% 197.99/28.14 % (3748763)Termination phase: Saturation
% 197.99/28.14 % (3748763)Time elapsed: 9.247 s
% 197.99/28.14 % (3748763)Peak memory usage: 23 MB
% 197.99/28.14 % (3748763)Instructions burned: 22567 (million)
% 197.99/28.14 % (3748777)dis+33_16_sil=32000:sac=on:random_seed=1356019221:i=15851:nm=0_2872 on theBenchmark for (2872ds/15851Mi)
% 197.99/28.14 % (3748773)Instruction limit reached!
% 197.99/28.14 % (3748773)------------------------------
% 197.99/28.14 % (3748773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.99/28.14 % (3748773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.99/28.14 % (3748773)CaDiCaL version: 2.1.3
% 197.99/28.14 % (3748773)Termination reason: Instruction limit
% 197.99/28.14 % (3748773)Termination phase: Saturation
% 197.99/28.14 % (3748773)Time elapsed: 7.987 s
% 197.99/28.14 % (3748773)Peak memory usage: 43 MB
% 197.99/28.14 % (3748773)Instructions burned: 11404 (million)
% 197.99/28.14 % (3749210)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2661335456:avsq=on:i=17627:add=on:amm=off_2825 on theBenchmark for (2825ds/17627Mi)
% 197.99/28.14 % (3748753)Instruction limit reached!
% 197.99/28.14 % (3748753)------------------------------
% 197.99/28.14 % (3748753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.38/29.12 % (3748753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.38/29.12 % (3748753)CaDiCaL version: 2.1.3
% 204.38/29.12 % (3748753)Termination reason: Instruction limit
% 204.38/29.12 % (3748753)Termination phase: Saturation
% 204.38/29.12 % (3748753)Time elapsed: 15.195 s
% 204.38/29.12 % (3748753)Peak memory usage: 181 MB
% 204.38/29.12 % (3748753)Instructions burned: 29340 (million)
% 204.38/29.12 % (3749212)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1138174712:s2a=on:i=53295_2817 on theBenchmark for (2817ds/53295Mi)
% 204.38/29.12 % (3748775)Instruction limit reached!
% 204.38/29.12 % (3748775)------------------------------
% 204.38/29.12 % (3748775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.38/29.12 % (3748775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.38/29.12 % (3748775)CaDiCaL version: 2.1.3
% 204.38/29.12 % (3748775)Termination reason: Instruction limit
% 204.38/29.12 % (3748775)Termination phase: Saturation
% 204.38/29.12 % (3748775)Time elapsed: 9.608 s
% 204.38/29.12 % (3748775)Peak memory usage: 49 MB
% 204.38/29.12 % (3748775)Instructions burned: 14135 (million)
% 204.38/29.12 % (3749214)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=425717746:i=26857:ins=20_2808 on theBenchmark for (2808ds/26857Mi)
% 204.38/29.12 % (3749214)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 204.38/29.12 % (3749214)Terminated due to inappropriate strategy.
% 204.38/29.12 % (3749214)------------------------------
% 204.38/29.12 % (3749214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.38/29.12 % (3749214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.38/29.12 % (3749214)CaDiCaL version: 2.1.3
% 204.38/29.12 % (3749214)Termination reason: Inappropriate
% 204.38/29.12 % (3749214)Time elapsed: 0.0000 s
% 204.38/29.12 % (3749214)Peak memory usage: 10 MB
% 204.38/29.12 % (3749214)------------------------------
% 204.38/29.12 % (3749214)------------------------------
% 204.38/29.12 % (3749216)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=86816504:i=28120:bs=on:fsr=off_2808 on theBenchmark for (2808ds/28120Mi)
% 204.38/29.12 % (3748769)Instruction limit reached!
% 204.38/29.12 % (3748769)------------------------------
% 204.38/29.12 % (3748769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.38/29.12 % (3748769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.38/29.12 % (3748769)CaDiCaL version: 2.1.3
% 204.38/29.12 % (3748769)Termination reason: Instruction limit
% 204.38/29.12 % (3748769)Termination phase: Saturation
% 204.38/29.12 % (3748769)Time elapsed: 13.327 s
% 204.38/29.12 % (3748769)Peak memory usage: 65 MB
% 204.38/29.12 % (3748769)Instructions burned: 20139 (million)
% 204.38/29.12 % (3749218)fmb+10_1_sil=256000:fmbss=7:random_seed=554948543:fmbsr=1.6:i=182295_2804 on theBenchmark for (2804ds/182295Mi)
% 204.38/29.12 % (3749218)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 204.38/29.12 % (3749218)Terminated due to inappropriate strategy.
% 204.38/29.12 % (3749218)------------------------------
% 204.38/29.12 % (3749218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.38/29.12 % (3749218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.38/29.12 % (3749218)CaDiCaL version: 2.1.3
% 204.38/29.12 % (3749218)Termination reason: Inappropriate
% 204.38/29.12 % (3749218)Time elapsed: 0.0000 s
% 204.38/29.12 % (3749218)Peak memory usage: 10 MB
% 204.38/29.12 % (3749218)------------------------------
% 204.38/29.12 % (3749218)------------------------------
% 204.38/29.12 % (3749220)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3219221686:i=44625:gsp=on_2804 on theBenchmark for (2804ds/44625Mi)
% 204.38/29.12 % (3749220)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 204.38/29.12 % (3749220)Terminated due to inappropriate strategy.
% 204.38/29.12 % (3749220)------------------------------
% 204.38/29.12 % (3749220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.38/29.12 % (3749220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.38/29.12 % (3749220)CaDiCaL version: 2.1.3
% 204.38/29.12 % (3749220)Termination reason: Inappropriate
% 204.38/29.12 % (3749220)Time elapsed: 0.0000 s
% 204.38/29.12 % (3749220)Peak memory usage: 10 MB
% 204.38/29.12 % (3749220)------------------------------
% 204.38/29.12 % (3749220)------------------------------
% 204.38/29.12 % (3749222)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3650957836:i=160505_2803 on theBenchmark for (2803ds/160505Mi)
% 214.33/30.58 % (3749222)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 214.33/30.58 % (3749222)Terminated due to inappropriate strategy.
% 214.33/30.58 % (3749222)------------------------------
% 214.33/30.58 % (3749222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.33/30.58 % (3749222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.33/30.58 % (3749222)CaDiCaL version: 2.1.3
% 214.33/30.58 % (3749222)Termination reason: Inappropriate
% 214.33/30.58 % (3749222)Time elapsed: 0.0000 s
% 214.33/30.58 % (3749222)Peak memory usage: 10 MB
% 214.33/30.58 % (3749222)------------------------------
% 214.33/30.58 % (3749222)------------------------------
% 214.33/30.58 % (3749224)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1485675771:fmbsr=1.3:i=225729_2803 on theBenchmark for (2803ds/225729Mi)
% 214.33/30.58 % (3749224)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 214.33/30.58 % (3749224)Terminated due to inappropriate strategy.
% 214.33/30.58 % (3749224)------------------------------
% 214.33/30.58 % (3749224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.33/30.58 % (3749224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.33/30.58 % (3749224)CaDiCaL version: 2.1.3
% 214.33/30.58 % (3749224)Termination reason: Inappropriate
% 214.33/30.58 % (3749224)Time elapsed: 0.0000 s
% 214.33/30.58 % (3749224)Peak memory usage: 10 MB
% 214.33/30.58 % (3749224)------------------------------
% 214.33/30.58 % (3749224)------------------------------
% 214.33/30.58 % (3749226)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2572225011:fmbsr=2:i=185024:ins=7_2803 on theBenchmark for (2803ds/185024Mi)
% 214.33/30.58 % (3749226)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 214.33/30.58 % (3749226)Terminated due to inappropriate strategy.
% 214.33/30.58 % (3749226)------------------------------
% 214.33/30.58 % (3749226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.33/30.58 % (3749226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.33/30.58 % (3749226)CaDiCaL version: 2.1.3
% 214.33/30.58 % (3749226)Termination reason: Inappropriate
% 214.33/30.58 % (3749226)Time elapsed: 0.001 s
% 214.33/30.58 % (3749226)Peak memory usage: 10 MB
% 214.33/30.58 % (3749226)------------------------------
% 214.33/30.58 % (3749226)------------------------------
% 214.33/30.58 % (3749228)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3823711986:rtra=on_2803 on theBenchmark for (2803ds/0Mi)
% 214.33/30.58 % (3749228)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 214.33/30.58 % (3749228)Terminated due to inappropriate strategy.
% 214.33/30.58 % (3749228)------------------------------
% 214.33/30.58 % (3749228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.33/30.58 % (3749228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.33/30.58 % (3749228)CaDiCaL version: 2.1.3
% 214.33/30.58 % (3749228)Termination reason: Inappropriate
% 214.33/30.58 % (3749228)Time elapsed: 0.0000 s
% 214.33/30.58 % (3749228)Peak memory usage: 10 MB
% 214.33/30.58 % (3749228)------------------------------
% 214.33/30.58 % (3749228)------------------------------
% 214.33/30.58 % (3749230)% WARNING: option uhcvi not known.
% 214.33/30.58 % (3749230)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2938826862:i=271062:add=off:rtra=on:rawr=on_2803 on theBenchmark for (2803ds/271062Mi)
% 214.33/30.58 % (3748777)Instruction limit reached!
% 214.33/30.58 % (3748777)------------------------------
% 214.33/30.58 % (3748777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.33/30.58 % (3748777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.33/30.58 % (3748777)CaDiCaL version: 2.1.3
% 214.33/30.58 % (3748777)Termination reason: Instruction limit
% 214.33/30.58 % (3748777)Termination phase: Saturation
% 214.33/30.58 % (3748777)Time elapsed: 9.057 s
% 214.33/30.58 % (3748777)Peak memory usage: 133 MB
% 214.33/30.58 % (3748777)Instructions burned: 15852 (million)
% 214.33/30.58 % (3749232)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1748527510:i=176048:add=on:rtra=on:rawr=on_2781 on theBenchmark for (2781ds/176048Mi)
% 214.33/30.58 % (3749210)Instruction limit reached!
% 214.33/30.58 % (3749210)------------------------------
% 214.33/30.58 % (3749210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749210)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749210)Termination reason: Instruction limit
% 184.62/30.74 % (3749210)Termination phase: Saturation
% 184.62/30.74 % (3749210)Time elapsed: 10.450 s
% 184.62/30.74 % (3749210)Peak memory usage: 192 MB
% 184.62/30.74 % (3749210)Instructions burned: 17627 (million)
% 184.62/30.74 % (3749234)dis+10_1_sil=32000:si=on:sp=arity:random_seed=845185169:i=206:fgj=on:rtra=on_2720 on theBenchmark for (2720ds/206Mi)
% 184.62/30.74 % (3749234)Instruction limit reached!
% 184.62/30.74 % (3749234)------------------------------
% 184.62/30.74 % (3749234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749234)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749234)Termination reason: Instruction limit
% 184.62/30.74 % (3749234)Termination phase: Saturation
% 184.62/30.74 % (3749234)Time elapsed: 0.132 s
% 184.62/30.74 % (3749234)Peak memory usage: 13 MB
% 184.62/30.74 % (3749234)Instructions burned: 207 (million)
% 184.62/30.74 % (3749236)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3312821471:i=232:rtra=on_2719 on theBenchmark for (2719ds/232Mi)
% 184.62/30.74 % (3749236)Instruction limit reached!
% 184.62/30.74 % (3749236)------------------------------
% 184.62/30.74 % (3749236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749236)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749236)Termination reason: Instruction limit
% 184.62/30.74 % (3749236)Termination phase: Saturation
% 184.62/30.74 % (3749236)Time elapsed: 0.145 s
% 184.62/30.74 % (3749236)Peak memory usage: 13 MB
% 184.62/30.74 % (3749236)Instructions burned: 232 (million)
% 184.62/30.74 % (3749238)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2324236059:i=262:rtra=on_2717 on theBenchmark for (2717ds/262Mi)
% 184.62/30.74 % (3749238)Instruction limit reached!
% 184.62/30.74 % (3749238)------------------------------
% 184.62/30.74 % (3749238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749238)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749238)Termination reason: Instruction limit
% 184.62/30.74 % (3749238)Termination phase: Saturation
% 184.62/30.74 % (3749238)Time elapsed: 0.172 s
% 184.62/30.74 % (3749238)Peak memory usage: 13 MB
% 184.62/30.74 % (3749238)Instructions burned: 264 (million)
% 184.62/30.74 % (3749240)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=905955971:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2715 on theBenchmark for (2715ds/318Mi)
% 184.62/30.74 % (3749240)Instruction limit reached!
% 184.62/30.74 % (3749240)------------------------------
% 184.62/30.74 % (3749240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749240)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749240)Termination reason: Instruction limit
% 184.62/30.74 % (3749240)Termination phase: Saturation
% 184.62/30.74 % (3749240)Time elapsed: 0.200 s
% 184.62/30.74 % (3749240)Peak memory usage: 15 MB
% 184.62/30.74 % (3749240)Instructions burned: 319 (million)
% 184.62/30.74 % (3749242)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2387786821:i=1428:nm=2:rtra=on_2713 on theBenchmark for (2713ds/1428Mi)
% 184.62/30.74 % (3749242)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 184.62/30.74 % (3749242)Terminated due to inappropriate strategy.
% 184.62/30.74 % (3749242)------------------------------
% 184.62/30.74 % (3749242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749242)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749242)Termination reason: Inappropriate
% 184.62/30.74 % (3749242)Time elapsed: 0.0000 s
% 184.62/30.74 % (3749242)Peak memory usage: 10 MB
% 184.62/30.74 % (3749242)------------------------------
% 184.62/30.74 % (3749242)------------------------------
% 184.62/30.74 % (3749244)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1524733578:i=262:bd=preordered:rtra=on:fsd=on_2713 on theBenchmark for (2713ds/262Mi)
% 184.62/30.74 % (3749244)Instruction limit reached!
% 184.62/30.74 % (3749244)------------------------------
% 184.62/30.74 % (3749244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749244)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749244)Termination reason: Instruction limit
% 184.62/30.74 % (3749244)Termination phase: Saturation
% 184.62/30.74 % (3749244)Time elapsed: 0.178 s
% 184.62/30.74 % (3749244)Peak memory usage: 14 MB
% 184.62/30.74 % (3749244)Instructions burned: 262 (million)
% 184.62/30.74 % (3749276)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2767741641:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2711 on theBenchmark for (2711ds/1368Mi)
% 184.62/30.74 % (3749276)Instruction limit reached!
% 184.62/30.74 % (3749276)------------------------------
% 184.62/30.74 % (3749276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749276)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749276)Termination reason: Instruction limit
% 184.62/30.74 % (3749276)Termination phase: Saturation
% 184.62/30.74 % (3749276)Time elapsed: 0.676 s
% 184.62/30.74 % (3749276)Peak memory usage: 19 MB
% 184.62/30.74 % (3749276)Instructions burned: 1369 (million)
% 184.62/30.74 % (3749416)ott-21_1_sil=16000:si=on:fs=off:random_seed=466883093:i=360:av=off:fsr=off:rtra=on_2704 on theBenchmark for (2704ds/360Mi)
% 184.62/30.74 % (3749216)Instruction limit reached!
% 184.62/30.74 % (3749216)------------------------------
% 184.62/30.74 % (3749216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749216)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749216)Termination reason: Instruction limit
% 184.62/30.74 % (3749216)Termination phase: Saturation
% 184.62/30.74 % (3749216)Time elapsed: 10.558 s
% 184.62/30.74 % (3749216)Peak memory usage: 23 MB
% 184.62/30.74 % (3749216)Instructions burned: 28121 (million)
% 184.62/30.74 % (3749465)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=657991816:i=954:bd=all:rtra=on_2702 on theBenchmark for (2702ds/954Mi)
% 184.62/30.74 % (3749416)Instruction limit reached!
% 184.62/30.74 % (3749416)------------------------------
% 184.62/30.74 % (3749416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749416)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749416)Termination reason: Instruction limit
% 184.62/30.74 % (3749416)Termination phase: Saturation
% 184.62/30.74 % (3749416)Time elapsed: 0.167 s
% 184.62/30.74 % (3749416)Peak memory usage: 12 MB
% 184.62/30.74 % (3749416)Instructions burned: 360 (million)
% 184.62/30.74 % (3749483)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=329890084:fmbsr=1.3:i=1730:ins=25:rtra=on_2702 on theBenchmark for (2702ds/1730Mi)
% 184.62/30.74 % (3749483)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 184.62/30.74 % (3749483)Terminated due to inappropriate strategy.
% 184.62/30.74 % (3749483)------------------------------
% 184.62/30.74 % (3749483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749483)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749483)Termination reason: Inappropriate
% 184.62/30.74 % (3749483)Time elapsed: 0.0000 s
% 184.62/30.74 % (3749483)Peak memory usage: 10 MB
% 184.62/30.74 % (3749483)------------------------------
% 184.62/30.74 % (3749483)------------------------------
% 184.62/30.74 % (3749485)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1161535976:i=2358:rtra=on_2701 on theBenchmark for (2701ds/2358Mi)
% 184.62/30.74 % (3749465)Instruction limit reached!
% 184.62/30.74 % (3749465)------------------------------
% 184.62/30.74 % (3749465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749465)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749465)Termination reason: Instruction limit
% 184.62/30.74 % (3749465)Termination phase: Saturation
% 184.62/30.74 % (3749465)Time elapsed: 0.583 s
% 184.62/30.74 % (3749465)Peak memory usage: 16 MB
% 184.62/30.74 % (3749465)Instructions burned: 956 (million)
% 184.62/30.74 % (3749519)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4005172052:i=1778:ins=1:rtra=on_2696 on theBenchmark for (2696ds/1778Mi)
% 184.62/30.74 % (3749519)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 184.62/30.74 % (3749519)Terminated due to inappropriate strategy.
% 184.62/30.74 % (3749519)------------------------------
% 184.62/30.74 % (3749519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3749519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3749519)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3749519)Termination reason: Inappropriate
% 184.62/30.74 % (3749519)Time elapsed: 0.0000 s
% 184.62/30.74 % (3749519)Peak memory usage: 10 MB
% 184.62/30.74 % (3749519)------------------------------
% 184.62/30.74 % (3749519)------------------------------
% 184.62/30.74 % (3749521)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1243360250:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2696 on theBenchmark for (2696ds/1384Mi)
% 184.62/30.74 % (3748381) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3748375-3748381"...
% 184.62/30.74 % (3748381)...printing done.
% 184.62/30.74 % (3748381)Refutation found. Thanks to Tanya!
% 184.62/30.74 % SZS status Theorem for theBenchmark
% 184.62/30.74 % SZS output start Proof for theBenchmark
% 184.62/30.74 tff(func_def_0, type, f: $int > $int).
% 184.62/30.74 tff(func_def_6, type, sK0: $int).
% 184.62/30.74 tff(func_def_7, type, sK1: $int).
% 184.62/30.74 tff(f1,conjecture,(
% 184.62/30.74 ! [X0 : $int] : $greater(f(X0),X0) => ! [X1 : $int,X2 : $int] : $greatereq(f($sum(f(X1),X2)),$sum($sum(X1,X2),2))),
% 184.62/30.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1)).
% 184.62/30.74 tff(f2,negated_conjecture,(
% 184.62/30.74 ~(! [X0 : $int] : $greater(f(X0),X0) => ! [X1 : $int,X2 : $int] : $greatereq(f($sum(f(X1),X2)),$sum($sum(X1,X2),2)))),
% 184.62/30.74 inference(negated_conjecture,[status(cth)],[f1])).
% 184.62/30.74 tff(f3,plain,(
% 184.62/30.74 ~(! [X0 : $int] : $less(X0,f(X0)) => ! [X1 : $int,X2 : $int] : ~$less(f($sum(f(X1),X2)),$sum($sum(X1,X2),2)))),
% 184.62/30.74 inference(theory_normalization,[],[f2])).
% 184.62/30.74 tff(f4,definition,(
% 184.62/30.74 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 184.62/30.74 introduced(theory,[tha_commutativity])).
% 184.62/30.74 tff(f5,definition,(
% 184.62/30.74 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 184.62/30.74 introduced(theory,[tha_associativity])).
% 184.62/30.74 tff(f8,definition,(
% 184.62/30.74 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 184.62/30.74 introduced(theory,[tha_inverse_op_unit])).
% 184.62/30.74 tff(f10,definition,(
% 184.62/30.74 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 184.62/30.74 introduced(theory,[tha_transitivity])).
% 184.62/30.74 tff(f11,definition,(
% 184.62/30.74 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 184.62/30.74 introduced(theory,[tha_order_totality])).
% 184.62/30.74 tff(f12,definition,(
% 184.62/30.74 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,X2),$sum(X1,X2))) )),
% 184.62/30.74 introduced(theory,[tha_order_monotonicity])).
% 184.62/30.74 tff(f15,definition,(
% 184.62/30.74 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 184.62/30.74 introduced(theory,[tha_extra_integer_ordering])).
% 184.62/30.74 tff(f16,plain,(
% 184.62/30.74 ? [X1 : $int,X2 : $int] : $less(f($sum(f(X1),X2)),$sum($sum(X1,X2),2)) & ! [X0 : $int] : $less(X0,f(X0))),
% 184.62/30.74 inference(ennf_transformation,[],[f3])).
% 184.62/30.74 tff(f17,plain,(
% 184.62/30.74 ( ! [X0 : $int] : ($less(X0,f(X0))) )),
% 184.62/30.74 inference(cnf_transformation,[],[f16])).
% 184.62/30.74 tff(f18,plain,(
% 184.62/30.74 $less(f($sum(f(sK0),sK1)),$sum($sum(sK0,sK1),2))),
% 184.62/30.74 inference(cnf_transformation,[],[f16])).
% 184.62/30.74 tff(f91,plain,(
% 184.62/30.74 ( ! [X0 : $int,X1 : $int] : ($less($sum(X0,X1),$sum(f(X0),X1))) )),
% 184.62/30.74 inference(resolution,[],[f12,f17])).
% 184.62/30.74 tff(f97,plain,(
% 184.62/30.74 ( ! [X0 : $int] : ($less($sum(f($sum(f(sK0),sK1)),X0),$sum($sum($sum(sK0,sK1),2),X0))) )),
% 184.62/30.74 inference(resolution,[],[f12,f18])).
% 184.62/30.74 tff(f99,plain,(
% 184.62/30.74 ( ! [X0 : $int] : ($less($sum(f($sum(f(sK0),sK1)),X0),$sum($sum(2,$sum(sK0,sK1)),X0))) )),
% 184.62/30.74 inference(forward_demodulation,[],[f97,f4])).
% 184.62/30.74 tff(f100,plain,(
% 184.62/30.74 ( ! [X0 : $int] : ($less($sum(f($sum(sK1,f(sK0))),X0),$sum($sum(2,$sum(sK0,sK1)),X0))) )),
% 184.62/30.74 inference(forward_demodulation,[],[f99,f4])).
% 184.62/30.74 tff(f102,plain,(
% 184.62/30.74 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 184.62/30.74 inference(superposition,[],[f5,f8])).
% 184.62/30.74 tff(f103,plain,(
% 184.62/30.74 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum($sum(X0,X1),X2) = $sum(X1,$sum(X0,X2))) )),
% 184.62/30.74 inference(superposition,[],[f5,f4])).
% 184.62/30.74 tff(f110,plain,(
% 184.62/30.74 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum(X1,$sum(X2,X0))) )),
% 184.62/30.74 inference(superposition,[],[f5,f4])).
% 184.62/30.74 tff(f117,plain,(
% 184.62/30.74 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X2,$sum(X0,$sum(X1,1))) | ~$less($sum(X0,X1),X2)) )),
% 184.62/30.74 inference(superposition,[],[f15,f5])).
% 184.62/30.74 tff(f121,plain,(
% 184.62/30.74 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 184.62/30.74 inference(evaluation,[],[f102])).
% 184.62/30.74 tff(f128,plain,(
% 184.62/30.74 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less(X0,$sum(f(X1),X2)) | ~$less(X0,$sum(X1,X2))) )),
% 184.62/30.74 inference(resolution,[],[f91,f10])).
% 184.62/30.74 tff(f131,plain,(
% 184.62/30.74 ( ! [X0 : $int,X1 : $int] : ($less($sum(X0,X1),$sum(f(X1),X0))) )),
% 184.62/30.74 inference(superposition,[],[f91,f4])).
% 184.62/30.74 tff(f153,plain,(
% 184.62/30.74 ( ! [X0 : $int] : ($less($sum(f($sum(sK1,f(sK0))),X0),$sum(2,$sum($sum(sK0,sK1),X0)))) )),
% 184.62/30.74 inference(forward_demodulation,[],[f100,f5])).
% 184.62/30.74 tff(f154,plain,(
% 184.62/30.74 ( ! [X0 : $int] : ($less($sum(f($sum(sK1,f(sK0))),X0),$sum(2,$sum(sK0,$sum(sK1,X0))))) )),
% 184.62/30.74 inference(forward_demodulation,[],[f153,f5])).
% 184.62/30.74 tff(f215,plain,(
% 184.62/30.74 ( ! [X0 : $int,X1 : $int] : ($sum(X1,$sum(X0,$uminus(X1))) = X0) )),
% 184.62/30.74 inference(superposition,[],[f121,f4])).
% 184.62/30.74 tff(f224,plain,(
% 184.62/30.74 ( ! [X0 : $int] : ($less($sum(f($sum(sK1,f(sK0))),$sum($uminus(sK1),X0)),$sum(2,$sum(sK0,X0)))) )),
% 184.62/30.74 inference(superposition,[],[f154,f121])).
% 184.62/30.74 tff(f517,plain,(
% 184.62/30.74 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,$sum(X2,X3))) = $sum(X2,$sum(X3,$sum(X1,X0)))) )),
% 184.62/30.74 inference(superposition,[],[f110,f103])).
% 184.62/30.74 tff(f530,plain,(
% 184.62/30.74 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : ($sum(X3,$sum(X0,$sum(X1,X2))) = $sum(X2,$sum(X3,$sum(X1,X0)))) )),
% 184.62/30.74 inference(superposition,[],[f110,f103])).
% 184.62/30.74 tff(f707,plain,(
% 184.62/30.74 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,$sum(X1,1)),X2) | ~$less($sum(X0,X1),X2) | $sum(X0,$sum(X1,1)) = X2) )),
% 184.62/30.74 inference(resolution,[],[f117,f11])).
% 184.62/30.74 tff(f709,plain,(
% 184.62/30.74 ( ! [X0 : $int,X1 : $int] : (~$less($sum(f(X0),X1),$sum(X0,$sum(X1,1)))) )),
% 184.62/30.74 inference(resolution,[],[f117,f91])).
% 184.62/30.74 tff(f714,plain,(
% 184.62/30.74 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : (~$less(X2,$sum(X3,$sum(X0,$sum(X1,1)))) | ~$less($sum(X3,$sum(X0,X1)),X2)) )),
% 184.62/30.74 inference(superposition,[],[f117,f5])).
% 184.62/30.74 tff(f1024,plain,(
% 184.62/30.74 ( ! [X0 : $int,X1 : $int] : ($less($sum(X0,X1),$sum(X0,f(X1)))) )),
% 184.62/30.74 inference(superposition,[],[f131,f4])).
% 184.62/30.74 tff(f1029,plain,(
% 184.62/30.74 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum($sum(X0,X1),X2),$sum(X0,$sum(X1,f(X2))))) )),
% 184.62/30.74 inference(superposition,[],[f131,f110])).
% 184.62/30.74 tff(f1034,plain,(
% 184.62/30.74 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,$sum(X1,X2)),$sum(X0,$sum(X1,f(X2))))) )),
% 184.62/30.74 inference(forward_demodulation,[],[f1029,f5])).
% 184.62/30.74 tff(f2699,plain,(
% 184.62/30.74 ( ! [X0 : $int] : ($less($sum($uminus(sK1),$sum(X0,f($sum(sK1,f(sK0))))),$sum(2,$sum(sK0,X0)))) )),
% 184.62/30.74 inference(forward_demodulation,[],[f224,f110])).
% 184.62/30.74 tff(f38998,plain,(
% 184.62/30.74 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int,X4 : $int] : ($less(X4,$sum(X0,$sum(X1,$sum(X2,f(X3))))) | ~$less(X4,$sum(X3,$sum(X2,$sum(X0,X1))))) )),
% 184.62/30.74 inference(superposition,[],[f128,f517])).
% 184.62/30.74 tff(f39003,plain,(
% 184.62/30.74 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : (~$less($sum(X0,$sum(X1,$sum(X2,f(X3)))),$sum(X3,$sum($sum(X2,$sum(X0,X1)),1)))) )),
% 184.62/30.74 inference(superposition,[],[f709,f517])).
% 184.62/30.74 tff(f39499,plain,(
% 184.62/30.74 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : (~$less($sum(X0,$sum(X1,$sum(X2,f(X3)))),$sum(X3,$sum(1,$sum(X2,$sum(X0,X1)))))) )),
% 184.62/30.74 inference(forward_demodulation,[],[f39003,f4])).
% 184.62/30.74 tff(f56305,plain,(
% 184.62/30.74 ( ! [X0 : $int] : (~$less($sum(2,$sum(sK0,X0)),$sum($uminus(sK1),$sum($sum(X0,1),f($sum(sK1,f(sK0))))))) )),
% 184.62/30.74 inference(resolution,[],[f714,f2699])).
% 184.62/30.74 tff(f56488,plain,(
% 184.62/30.74 ( ! [X0 : $int] : (~$less($sum(2,$sum(sK0,X0)),$sum($uminus(sK1),$sum(X0,$sum(1,f($sum(sK1,f(sK0)))))))) )),
% 184.62/30.74 inference(forward_demodulation,[],[f56305,f5])).
% 184.62/30.74 tff(f56543,plain,(
% 184.62/30.74 ( ! [X0 : $int] : (~$less($sum(2,$sum(sK0,X0)),$sum(1,$sum(f($sum(sK1,f(sK0))),$sum(X0,$uminus(sK1)))))) )),
% 184.62/30.74 inference(forward_demodulation,[],[f56488,f517])).
% 184.62/30.74 tff(f56557,plain,(
% 184.62/30.74 ( ! [X0 : $int] : (~$less($sum(2,$sum(sK0,X0)),$sum(1,$sum($uminus(sK1),$sum(f($sum(sK1,f(sK0))),X0))))) )),
% 184.62/30.74 inference(forward_demodulation,[],[f56543,f110])).
% 184.62/30.74 tff(f87636,definition,(
% 184.62/30.74 spl2_200 <=> $sum(1,$sum(2,sK0)) = $sum(1,$sum(1,$sum($uminus(sK1),f($sum(sK1,f(sK0))))))),
% 184.62/30.74 introduced(definition,[new_symbols(definition,[spl2_200])],[avatar_definition])).
% 184.62/30.74 tff(f87638,plain,(
% 184.62/30.74 $sum(1,$sum(2,sK0)) = $sum(1,$sum(1,$sum($uminus(sK1),f($sum(sK1,f(sK0)))))) | ~spl2_200),
% 184.62/30.74 inference(avatar_component_clause,[],[f87636])).
% 184.62/30.74 tff(f87640,definition,(
% 184.62/30.74 spl2_201 <=> $less($sum(2,sK0),$sum(1,$sum(1,$sum($uminus(sK1),f($sum(sK1,f(sK0)))))))),
% 184.62/30.74 introduced(definition,[new_symbols(definition,[spl2_201])],[avatar_definition])).
% 184.62/30.74 tff(f87642,plain,(
% 184.62/30.74 ~$less($sum(2,sK0),$sum(1,$sum(1,$sum($uminus(sK1),f($sum(sK1,f(sK0))))))) | spl2_201),
% 184.62/30.74 inference(avatar_component_clause,[],[f87640])).
% 184.62/30.74 tff(f1314390,plain,(
% 184.62/30.74 ~$less($sum(2,sK0),$sum(1,$sum($uminus(sK1),$sum(f($sum(sK1,f(sK0))),1)))) | $sum(2,$sum(sK0,1)) = $sum(1,$sum($uminus(sK1),$sum(f($sum(sK1,f(sK0))),1)))),
% 184.62/30.74 inference(resolution,[],[f56557,f707])).
% 184.62/30.74 tff(f1314726,plain,(
% 184.62/30.74 ~$less($sum(2,sK0),$sum(1,$sum(1,$sum(f($sum(sK1,f(sK0))),$uminus(sK1))))) | $sum(2,$sum(sK0,1)) = $sum(1,$sum($uminus(sK1),$sum(f($sum(sK1,f(sK0))),1)))),
% 184.62/30.74 inference(forward_demodulation,[],[f1314390,f530])).
% 184.62/30.74 tff(f1314790,plain,(
% 184.62/30.74 ~$less($sum(2,sK0),$sum(1,$sum(1,$sum($uminus(sK1),f($sum(sK1,f(sK0))))))) | $sum(2,$sum(sK0,1)) = $sum(1,$sum($uminus(sK1),$sum(f($sum(sK1,f(sK0))),1)))),
% 184.62/30.74 inference(forward_demodulation,[],[f1314726,f4])).
% 184.62/30.74 tff(f1317300,plain,(
% 184.62/30.74 $sum(2,$sum(sK0,1)) = $sum(1,$sum(1,$sum(f($sum(sK1,f(sK0))),$uminus(sK1)))) | ~$less($sum(2,sK0),$sum(1,$sum(1,$sum($uminus(sK1),f($sum(sK1,f(sK0)))))))),
% 184.62/30.74 inference(forward_demodulation,[],[f1314790,f530])).
% 184.62/30.74 tff(f1317304,plain,(
% 184.62/30.74 $sum(2,$sum(sK0,1)) = $sum(1,$sum(1,$sum($uminus(sK1),f($sum(sK1,f(sK0)))))) | ~$less($sum(2,sK0),$sum(1,$sum(1,$sum($uminus(sK1),f($sum(sK1,f(sK0)))))))),
% 184.62/30.74 inference(forward_demodulation,[],[f1317300,f4])).
% 184.62/30.74 tff(f1317305,plain,(
% 184.62/30.74 $sum(1,$sum(2,sK0)) = $sum(1,$sum(1,$sum($uminus(sK1),f($sum(sK1,f(sK0)))))) | ~$less($sum(2,sK0),$sum(1,$sum(1,$sum($uminus(sK1),f($sum(sK1,f(sK0)))))))),
% 184.62/30.74 inference(forward_demodulation,[],[f1317304,f110])).
% 184.62/30.74 tff(f1317306,plain,(
% 184.62/30.74 ~spl2_201 | spl2_200),
% 184.62/30.74 inference(avatar_split_clause,[],[f1317305,f87636,f87640])).
% 184.62/30.74 tff(f1317426,plain,(
% 184.62/30.74 ~$less($sum(1,$sum(2,sK0)),$sum($sum(sK1,f(sK0)),$sum(1,$sum($uminus(sK1),$sum(1,1))))) | ~spl2_200),
% 184.62/30.74 inference(superposition,[],[f39499,f87638])).
% 184.62/30.74 tff(f1319760,plain,(
% 184.62/30.74 ~$less($sum(1,$sum(2,sK0)),$sum($sum(sK1,f(sK0)),$sum(1,$sum($uminus(sK1),2)))) | ~spl2_200),
% 184.62/30.74 inference(evaluation,[],[f1317426])).
% 184.62/30.74 tff(f1321555,plain,(
% 184.62/30.74 ~$less($sum(1,$sum(2,sK0)),$sum(1,$sum($sum($uminus(sK1),2),$sum(sK1,f(sK0))))) | ~spl2_200),
% 184.62/30.74 inference(forward_demodulation,[],[f1319760,f110])).
% 184.62/30.74 tff(f1323073,plain,(
% 184.62/30.74 ~$less($sum(1,$sum(2,sK0)),$sum(1,$sum($sum(sK1,f(sK0)),$sum($uminus(sK1),2)))) | ~spl2_200),
% 184.62/30.74 inference(forward_demodulation,[],[f1321555,f4])).
% 184.62/30.74 tff(f1324061,plain,(
% 184.62/30.74 ~$less($sum(1,$sum(2,sK0)),$sum(1,$sum($uminus(sK1),$sum(2,$sum(sK1,f(sK0)))))) | ~spl2_200),
% 184.62/30.74 inference(forward_demodulation,[],[f1323073,f110])).
% 184.62/30.74 tff(f1324724,plain,(
% 184.62/30.74 ~$less($sum(1,$sum(2,sK0)),$sum(1,$sum(2,$sum($sum(sK1,f(sK0)),$uminus(sK1))))) | ~spl2_200),
% 184.62/30.74 inference(forward_demodulation,[],[f1324061,f110])).
% 184.62/30.74 tff(f1325185,plain,(
% 184.62/30.74 ~$less($sum(1,$sum(2,sK0)),$sum(1,$sum(2,$sum($uminus(sK1),$sum(sK1,f(sK0)))))) | ~spl2_200),
% 184.62/30.74 inference(forward_demodulation,[],[f1324724,f4])).
% 184.62/30.74 tff(f1325481,plain,(
% 184.62/30.74 ~$less($sum(1,$sum(2,sK0)),$sum(1,$sum(2,$sum(sK1,$sum(f(sK0),$uminus(sK1)))))) | ~spl2_200),
% 184.62/30.74 inference(forward_demodulation,[],[f1325185,f110])).
% 184.62/30.74 tff(f1325696,plain,(
% 184.62/30.74 ~$less($sum(1,$sum(2,sK0)),$sum(1,$sum(2,f(sK0)))) | ~spl2_200),
% 184.62/30.74 inference(forward_demodulation,[],[f1325481,f215])).
% 184.62/30.74 tff(f1325853,plain,(
% 184.62/30.74 $false | ~spl2_200),
% 184.62/30.74 inference(forward_subsumption_resolution,[],[f1325696,f1034])).
% 184.62/30.74 tff(f1325854,plain,(
% 184.62/30.74 ~spl2_200),
% 184.62/30.74 inference(avatar_contradiction_clause,[],[f1325853])).
% 184.62/30.74 tff(f1664052,plain,(
% 184.62/30.74 ~$less($sum(2,sK0),$sum($sum(sK1,f(sK0)),$sum($uminus(sK1),$sum(1,1)))) | spl2_201),
% 184.62/30.74 inference(resolution,[],[f38998,f87642])).
% 184.62/30.74 tff(f1664252,plain,(
% 184.62/30.74 ~$less($sum(2,sK0),$sum($sum(sK1,f(sK0)),$sum($uminus(sK1),2))) | spl2_201),
% 184.62/30.74 inference(evaluation,[],[f1664052])).
% 184.62/30.74 tff(f1664331,plain,(
% 184.62/30.74 ~$less($sum(2,sK0),$sum($uminus(sK1),$sum(2,$sum(sK1,f(sK0))))) | spl2_201),
% 184.62/30.74 inference(forward_demodulation,[],[f1664252,f110])).
% 184.62/30.74 tff(f1664390,plain,(
% 184.62/30.74 ~$less($sum(2,sK0),$sum(2,$sum($sum(sK1,f(sK0)),$uminus(sK1)))) | spl2_201),
% 184.62/30.74 inference(forward_demodulation,[],[f1664331,f110])).
% 184.62/30.74 tff(f1664409,plain,(
% 184.62/30.74 ~$less($sum(2,sK0),$sum(2,$sum($uminus(sK1),$sum(sK1,f(sK0))))) | spl2_201),
% 184.62/30.74 inference(forward_demodulation,[],[f1664390,f4])).
% 184.62/30.74 tff(f1664419,plain,(
% 184.62/30.74 ~$less($sum(2,sK0),$sum(2,$sum(sK1,$sum(f(sK0),$uminus(sK1))))) | spl2_201),
% 184.62/30.74 inference(forward_demodulation,[],[f1664409,f110])).
% 184.62/30.74 tff(f1664423,plain,(
% 184.62/30.74 ~$less($sum(2,sK0),$sum(2,f(sK0))) | spl2_201),
% 184.62/30.74 inference(forward_demodulation,[],[f1664419,f215])).
% 184.62/30.74 tff(f1664424,plain,(
% 184.62/30.74 $false | spl2_201),
% 184.62/30.74 inference(forward_subsumption_resolution,[],[f1664423,f1024])).
% 184.62/30.74 tff(f1664425,plain,(
% 184.62/30.74 spl2_201),
% 184.62/30.74 inference(avatar_contradiction_clause,[],[f1664424])).
% 184.62/30.74 cnf(s9674, plain, spl2_200 | ~spl2_201, inference(sat_conversion,[],[f1317306])).
% 184.62/30.74 cnf(s9711, plain, ~spl2_200, inference(sat_conversion,[],[f1325854])).
% 184.62/30.74 cnf(s11765, plain, spl2_201, inference(sat_conversion,[],[f1664425])).
% 184.62/30.74 cnf(s11787, plain, $false, inference(rat,[],[s9674,s11765,s9711])).
% 184.62/30.74 tff(f1664426,plain,(
% 184.62/30.74 $false),
% 184.62/30.74 inference(avatar_sat_refutation,[],[s11787])).
% 184.62/30.74 % SZS output end Proof for theBenchmark
% 184.62/30.74 % (3748381)------------------------------
% 184.62/30.74 % (3748381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.62/30.74 % (3748381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.62/30.74 % (3748381)CaDiCaL version: 2.1.3
% 184.62/30.74 % (3748381)Termination reason: Refutation
% 184.62/30.74 % (3748381)Time elapsed: 30.414 s
% 184.62/30.74 % (3748381)Peak memory usage: 503 MB
% 184.62/30.74 % (3748381)Instructions burned: 99598 (million)
% 184.62/30.74 % (3748375)Success in time 30.513 s
% 184.62/30.74 % Vampire exiting
%------------------------------------------------------------------------------