%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI179_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 : n016.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 162.73s 30.17s
% Output : Refutation 162.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ARI179_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n016.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 20:49:04 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 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
% 3.62/0.85 % (3973543)Will run a generic schedule for satisfiability detection.
% 3.62/0.85 % (3973551)dis+10_1_sil=32000:sp=arity:random_seed=583779976:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.62/0.85 % (3973549)% WARNING: option uhcvi not known.
% 3.62/0.85 % (3973548)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3897448272_2999 on theBenchmark for (2999ds/0Mi)
% 3.62/0.85 % (3973549)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=330685261:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.62/0.85 % (3973550)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4168202721:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.62/0.85 % (3973554)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1457017049:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.62/0.85 % (3973552)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2670815250:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.62/0.85 % (3973548)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.62/0.85 % (3973553)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1075680857:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.62/0.85 % (3973548)Terminated due to inappropriate strategy.
% 3.62/0.85 % (3973548)------------------------------
% 3.62/0.85 % (3973548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.85 % (3973548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.85 % (3973548)CaDiCaL version: 2.1.3
% 3.62/0.85 % (3973548)Termination reason: Inappropriate
% 3.62/0.85 % (3973548)Time elapsed: 0.0000 s
% 3.62/0.85 % (3973548)Peak memory usage: 10 MB
% 3.62/0.85 % (3973548)------------------------------
% 3.62/0.85 % (3973548)------------------------------
% 3.62/0.85 % (3973562)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3369527624:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.62/0.85 % (3973562)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.62/0.85 % (3973562)Terminated due to inappropriate strategy.
% 3.62/0.85 % (3973562)------------------------------
% 3.62/0.85 % (3973562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.85 % (3973562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.85 % (3973562)CaDiCaL version: 2.1.3
% 3.62/0.85 % (3973562)Termination reason: Inappropriate
% 3.62/0.85 % (3973562)Time elapsed: 0.0000 s
% 3.62/0.85 % (3973562)Peak memory usage: 10 MB
% 3.62/0.85 % (3973562)------------------------------
% 3.62/0.85 % (3973562)------------------------------
% 3.62/0.85 % (3973551)Instruction limit reached!
% 3.62/0.85 % (3973551)------------------------------
% 3.62/0.85 % (3973551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.85 % (3973551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.85 % (3973551)CaDiCaL version: 2.1.3
% 3.62/0.85 % (3973551)Termination reason: Instruction limit
% 3.62/0.85 % (3973551)Termination phase: Saturation
% 3.62/0.85 % (3973551)Time elapsed: 0.035 s
% 3.62/0.85 % (3973551)Peak memory usage: 12 MB
% 3.62/0.85 % (3973551)Instructions burned: 103 (million)
% 3.62/0.85 % (3973565)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=2423434685:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.62/0.85 % (3973564)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3870210978:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.62/0.85 % (3973552)Instruction limit reached!
% 3.62/0.85 % (3973552)------------------------------
% 3.62/0.85 % (3973552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.85 % (3973552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.85 % (3973552)CaDiCaL version: 2.1.3
% 3.62/0.85 % (3973552)Termination reason: Instruction limit
% 3.62/0.85 % (3973552)Termination phase: Saturation
% 3.62/0.85 % (3973552)Time elapsed: 0.070 s
% 3.62/0.85 % (3973552)Peak memory usage: 12 MB
% 3.62/0.85 % (3973552)Instructions burned: 117 (million)
% 3.62/0.85 % (3973553)Instruction limit reached!
% 3.62/0.85 % (3973553)------------------------------
% 3.62/0.85 % (3973553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.85 % (3973553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.42 % (3973553)CaDiCaL version: 2.1.3
% 7.93/1.42 % (3973553)Termination reason: Instruction limit
% 7.93/1.42 % (3973553)Termination phase: Saturation
% 7.93/1.42 % (3973553)Time elapsed: 0.083 s
% 7.93/1.42 % (3973553)Peak memory usage: 13 MB
% 7.93/1.42 % (3973553)Instructions burned: 132 (million)
% 7.93/1.42 % (3973568)ott-21_1_sil=16000:fs=off:random_seed=3372662514:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.93/1.42 % (3973569)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1751902000:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.93/1.42 % (3973554)Instruction limit reached!
% 7.93/1.42 % (3973554)------------------------------
% 7.93/1.42 % (3973554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.93/1.42 % (3973554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.42 % (3973554)CaDiCaL version: 2.1.3
% 7.93/1.42 % (3973554)Termination reason: Instruction limit
% 7.93/1.42 % (3973554)Termination phase: Saturation
% 7.93/1.42 % (3973554)Time elapsed: 0.112 s
% 7.93/1.42 % (3973554)Peak memory usage: 13 MB
% 7.93/1.42 % (3973554)Instructions burned: 160 (million)
% 7.93/1.42 % (3973572)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4051884586:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.93/1.42 % (3973572)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.93/1.42 % (3973572)Terminated due to inappropriate strategy.
% 7.93/1.42 % (3973572)------------------------------
% 7.93/1.42 % (3973572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.93/1.42 % (3973572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.42 % (3973572)CaDiCaL version: 2.1.3
% 7.93/1.42 % (3973572)Termination reason: Inappropriate
% 7.93/1.42 % (3973572)Time elapsed: 0.0000 s
% 7.93/1.42 % (3973572)Peak memory usage: 10 MB
% 7.93/1.42 % (3973572)------------------------------
% 7.93/1.42 % (3973572)------------------------------
% 7.93/1.42 % (3973564)Instruction limit reached!
% 7.93/1.42 % (3973564)------------------------------
% 7.93/1.42 % (3973564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.93/1.42 % (3973564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.42 % (3973564)CaDiCaL version: 2.1.3
% 7.93/1.42 % (3973564)Termination reason: Instruction limit
% 7.93/1.42 % (3973564)Termination phase: Saturation
% 7.93/1.42 % (3973564)Time elapsed: 0.097 s
% 7.93/1.42 % (3973564)Peak memory usage: 13 MB
% 7.93/1.42 % (3973564)Instructions burned: 131 (million)
% 7.93/1.42 % (3973574)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=167161078:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.93/1.42 % (3973575)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=143656501:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 7.93/1.42 % (3973575)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.93/1.42 % (3973575)Terminated due to inappropriate strategy.
% 7.93/1.42 % (3973575)------------------------------
% 7.93/1.42 % (3973575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.93/1.42 % (3973575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.42 % (3973575)CaDiCaL version: 2.1.3
% 7.93/1.42 % (3973575)Termination reason: Inappropriate
% 7.93/1.42 % (3973575)Time elapsed: 0.0000 s
% 7.93/1.42 % (3973575)Peak memory usage: 10 MB
% 7.93/1.42 % (3973575)------------------------------
% 7.93/1.42 % (3973575)------------------------------
% 7.93/1.42 % (3973568)Instruction limit reached!
% 7.93/1.42 % (3973568)------------------------------
% 7.93/1.42 % (3973568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.93/1.42 % (3973568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.42 % (3973568)CaDiCaL version: 2.1.3
% 7.93/1.42 % (3973568)Termination reason: Instruction limit
% 7.93/1.42 % (3973568)Termination phase: Saturation
% 7.93/1.42 % (3973568)Time elapsed: 0.078 s
% 7.93/1.42 % (3973568)Peak memory usage: 12 MB
% 7.93/1.42 % (3973568)Instructions burned: 180 (million)
% 7.93/1.42 % (3973578)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=665435722: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.93/1.42 % (3973579)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4017958687:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 21.01/3.25 % (3973565)Instruction limit reached!
% 21.01/3.25 % (3973565)------------------------------
% 21.01/3.25 % (3973565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.01/3.25 % (3973565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/3.25 % (3973565)CaDiCaL version: 2.1.3
% 21.01/3.25 % (3973565)Termination reason: Instruction limit
% 21.01/3.25 % (3973565)Termination phase: Saturation
% 21.01/3.25 % (3973565)Time elapsed: 0.177 s
% 21.01/3.25 % (3973565)Peak memory usage: 17 MB
% 21.01/3.25 % (3973565)Instructions burned: 685 (million)
% 21.01/3.25 % (3973582)fmb+10_1_sil=64000:random_seed=455639548:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 21.01/3.25 % (3973582)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.01/3.25 % (3973582)Terminated due to inappropriate strategy.
% 21.01/3.25 % (3973582)------------------------------
% 21.01/3.25 % (3973582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.01/3.25 % (3973582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/3.25 % (3973582)CaDiCaL version: 2.1.3
% 21.01/3.25 % (3973582)Termination reason: Inappropriate
% 21.01/3.25 % (3973582)Time elapsed: 0.0000 s
% 21.01/3.25 % (3973582)Peak memory usage: 10 MB
% 21.01/3.25 % (3973582)------------------------------
% 21.01/3.25 % (3973582)------------------------------
% 21.01/3.25 % (3973584)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2999885426:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 21.01/3.25 % (3973584)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.01/3.25 % (3973584)Terminated due to inappropriate strategy.
% 21.01/3.25 % (3973584)------------------------------
% 21.01/3.25 % (3973584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.01/3.25 % (3973584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/3.25 % (3973584)CaDiCaL version: 2.1.3
% 21.01/3.25 % (3973584)Termination reason: Inappropriate
% 21.01/3.25 % (3973584)Time elapsed: 0.0000 s
% 21.01/3.25 % (3973584)Peak memory usage: 10 MB
% 21.01/3.25 % (3973584)------------------------------
% 21.01/3.25 % (3973584)------------------------------
% 21.01/3.25 % (3973586)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1059142243:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 21.01/3.25 % (3973586)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.01/3.25 % (3973586)Terminated due to inappropriate strategy.
% 21.01/3.25 % (3973586)------------------------------
% 21.01/3.25 % (3973586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.01/3.25 % (3973586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/3.25 % (3973586)CaDiCaL version: 2.1.3
% 21.01/3.25 % (3973586)Termination reason: Inappropriate
% 21.01/3.25 % (3973586)Time elapsed: 0.0000 s
% 21.01/3.25 % (3973586)Peak memory usage: 11 MB
% 21.01/3.25 % (3973586)------------------------------
% 21.01/3.25 % (3973586)------------------------------
% 21.01/3.25 % (3973588)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2703599519:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 21.01/3.25 % (3973569)Instruction limit reached!
% 21.01/3.25 % (3973569)------------------------------
% 21.01/3.25 % (3973569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.01/3.25 % (3973569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/3.25 % (3973569)CaDiCaL version: 2.1.3
% 21.01/3.25 % (3973569)Termination reason: Instruction limit
% 21.01/3.25 % (3973569)Termination phase: Saturation
% 21.01/3.25 % (3973569)Time elapsed: 0.308 s
% 21.01/3.25 % (3973569)Peak memory usage: 14 MB
% 21.01/3.25 % (3973569)Instructions burned: 477 (million)
% 21.01/3.25 % (3973590)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2524159310:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 21.01/3.25 % (3973578)Instruction limit reached!
% 21.01/3.25 % (3973578)------------------------------
% 21.01/3.25 % (3973578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.01/3.25 % (3973578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/3.25 % (3973578)CaDiCaL version: 2.1.3
% 21.01/3.25 % (3973578)Termination reason: Instruction limit
% 28.10/4.21 % (3973578)Termination phase: Saturation
% 28.10/4.21 % (3973578)Time elapsed: 0.400 s
% 28.10/4.21 % (3973578)Peak memory usage: 18 MB
% 28.10/4.21 % (3973578)Instructions burned: 692 (million)
% 28.10/4.21 % (3973592)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1244073763:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 28.10/4.21 % (3973592)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.10/4.21 % (3973592)Terminated due to inappropriate strategy.
% 28.10/4.21 % (3973592)------------------------------
% 28.10/4.21 % (3973592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.10/4.21 % (3973592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.10/4.21 % (3973592)CaDiCaL version: 2.1.3
% 28.10/4.21 % (3973592)Termination reason: Inappropriate
% 28.10/4.21 % (3973592)Time elapsed: 0.0000 s
% 28.10/4.21 % (3973592)Peak memory usage: 10 MB
% 28.10/4.21 % (3973592)------------------------------
% 28.10/4.21 % (3973592)------------------------------
% 28.10/4.21 % (3973594)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2251100417:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 28.10/4.21 % (3973594)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.10/4.21 % (3973594)Terminated due to inappropriate strategy.
% 28.10/4.21 % (3973594)------------------------------
% 28.10/4.21 % (3973594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.10/4.21 % (3973594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.10/4.21 % (3973594)CaDiCaL version: 2.1.3
% 28.10/4.21 % (3973594)Termination reason: Inappropriate
% 28.10/4.21 % (3973594)Time elapsed: 0.0000 s
% 28.10/4.21 % (3973594)Peak memory usage: 10 MB
% 28.10/4.21 % (3973594)------------------------------
% 28.10/4.21 % (3973594)------------------------------
% 28.10/4.21 % (3973596)ott-2_1_sil=16000:newcnf=on:random_seed=467428964:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 28.10/4.21 % (3973579)Instruction limit reached!
% 28.10/4.21 % (3973579)------------------------------
% 28.10/4.21 % (3973579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.10/4.21 % (3973579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.10/4.21 % (3973579)CaDiCaL version: 2.1.3
% 28.10/4.21 % (3973579)Termination reason: Instruction limit
% 28.10/4.21 % (3973579)Termination phase: Saturation
% 28.10/4.21 % (3973579)Time elapsed: 0.496 s
% 28.10/4.21 % (3973579)Peak memory usage: 19 MB
% 28.10/4.21 % (3973579)Instructions burned: 880 (million)
% 28.10/4.21 % (3973598)ott+10_1_sil=32000:tgt=ground:random_seed=2579080303:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 28.10/4.21 % (3973574)Instruction limit reached!
% 28.10/4.21 % (3973574)------------------------------
% 28.10/4.21 % (3973574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.10/4.21 % (3973574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.10/4.21 % (3973574)CaDiCaL version: 2.1.3
% 28.10/4.21 % (3973574)Termination reason: Instruction limit
% 28.10/4.21 % (3973574)Termination phase: Saturation
% 28.10/4.21 % (3973574)Time elapsed: 0.635 s
% 28.10/4.21 % (3973574)Peak memory usage: 18 MB
% 28.10/4.21 % (3973574)Instructions burned: 1180 (million)
% 28.10/4.21 % (3973600)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2755974494:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 28.10/4.21 % (3973600)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.10/4.21 % (3973600)Terminated due to inappropriate strategy.
% 28.10/4.21 % (3973600)------------------------------
% 28.10/4.21 % (3973600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.10/4.21 % (3973600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.10/4.21 % (3973600)CaDiCaL version: 2.1.3
% 28.10/4.21 % (3973600)Termination reason: Inappropriate
% 28.10/4.21 % (3973600)Time elapsed: 0.0000 s
% 28.10/4.21 % (3973600)Peak memory usage: 10 MB
% 28.10/4.21 % (3973600)------------------------------
% 28.10/4.21 % (3973600)------------------------------
% 28.10/4.21 % (3973602)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3241596779:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 28.10/4.21 % (3973596)Instruction limit reached!
% 28.10/4.21 % (3973596)------------------------------
% 28.10/4.21 % (3973596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.10/4.21 % (3973596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.19/17.09 % (3973596)CaDiCaL version: 2.1.3
% 119.19/17.09 % (3973596)Termination reason: Instruction limit
% 119.19/17.09 % (3973596)Termination phase: Saturation
% 119.19/17.09 % (3973596)Time elapsed: 0.506 s
% 119.19/17.09 % (3973596)Peak memory usage: 14 MB
% 119.19/17.09 % (3973596)Instructions burned: 870 (million)
% 119.19/17.09 % (3973604)dis+21_1_sil=32000:sas=cadical:random_seed=2003889421:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 119.19/17.09 % (3973590)Instruction limit reached!
% 119.19/17.09 % (3973590)------------------------------
% 119.19/17.09 % (3973590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.19/17.09 % (3973590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.19/17.09 % (3973590)CaDiCaL version: 2.1.3
% 119.19/17.09 % (3973590)Termination reason: Instruction limit
% 119.19/17.09 % (3973590)Termination phase: Saturation
% 119.19/17.09 % (3973590)Time elapsed: 0.740 s
% 119.19/17.09 % (3973590)Peak memory usage: 25 MB
% 119.19/17.09 % (3973590)Instructions burned: 1472 (million)
% 119.19/17.09 % (3973606)ott+11_1_sil=16000:gs=on:random_seed=2840313822:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 119.19/17.09 % (3973588)Instruction limit reached!
% 119.19/17.09 % (3973588)------------------------------
% 119.19/17.09 % (3973588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.19/17.09 % (3973588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.19/17.09 % (3973588)CaDiCaL version: 2.1.3
% 119.19/17.09 % (3973588)Termination reason: Instruction limit
% 119.19/17.09 % (3973588)Termination phase: Saturation
% 119.19/17.09 % (3973588)Time elapsed: 1.445 s
% 119.19/17.09 % (3973588)Peak memory usage: 41 MB
% 119.19/17.09 % (3973588)Instructions burned: 5135 (million)
% 119.19/17.09 % (3973608)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3507322536:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi)
% 119.19/17.09 % (3973608)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 119.19/17.09 % (3973608)Terminated due to inappropriate strategy.
% 119.19/17.09 % (3973608)------------------------------
% 119.19/17.09 % (3973608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.19/17.09 % (3973608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.19/17.09 % (3973608)CaDiCaL version: 2.1.3
% 119.19/17.09 % (3973608)Termination reason: Inappropriate
% 119.19/17.09 % (3973608)Time elapsed: 0.0000 s
% 119.19/17.09 % (3973608)Peak memory usage: 11 MB
% 119.19/17.09 % (3973608)------------------------------
% 119.19/17.09 % (3973608)------------------------------
% 119.19/17.09 % (3973610)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2454647188:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi)
% 119.19/17.09 % (3973606)Instruction limit reached!
% 119.19/17.09 % (3973606)------------------------------
% 119.19/17.09 % (3973606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.19/17.09 % (3973606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.19/17.09 % (3973606)CaDiCaL version: 2.1.3
% 119.19/17.09 % (3973606)Termination reason: Instruction limit
% 119.19/17.09 % (3973606)Termination phase: Saturation
% 119.19/17.09 % (3973606)Time elapsed: 1.289 s
% 119.19/17.09 % (3973606)Peak memory usage: 24 MB
% 119.19/17.09 % (3973606)Instructions burned: 2252 (million)
% 119.19/17.09 % (3973612)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2859254279:i=29340_2974 on theBenchmark for (2974ds/29340Mi)
% 119.19/17.09 % (3973602)Instruction limit reached!
% 119.19/17.09 % (3973602)------------------------------
% 119.19/17.09 % (3973602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.19/17.09 % (3973602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.19/17.09 % (3973602)CaDiCaL version: 2.1.3
% 119.19/17.09 % (3973602)Termination reason: Instruction limit
% 119.19/17.09 % (3973602)Termination phase: Saturation
% 119.19/17.09 % (3973602)Time elapsed: 1.834 s
% 119.19/17.09 % (3973602)Peak memory usage: 40 MB
% 119.19/17.09 % (3973602)Instructions burned: 3512 (million)
% 119.19/17.09 % (3973614)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=860277957:i=5211_2972 on theBenchmark for (2972ds/5211Mi)
% 119.19/17.09 % (3973610)Instruction limit reached!
% 119.19/17.09 % (3973610)------------------------------
% 119.19/17.09 % (3973610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.00/17.51 % (3973610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.00/17.51 % (3973610)CaDiCaL version: 2.1.3
% 122.00/17.51 % (3973610)Termination reason: Instruction limit
% 122.00/17.51 % (3973610)Termination phase: Saturation
% 122.00/17.51 % (3973610)Time elapsed: 1.230 s
% 122.00/17.51 % (3973610)Peak memory usage: 32 MB
% 122.00/17.51 % (3973610)Instructions burned: 4591 (million)
% 122.00/17.51 % (3973616)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=386814875:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi)
% 122.00/17.51 % (3973616)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 122.00/17.51 % (3973616)Terminated due to inappropriate strategy.
% 122.00/17.51 % (3973616)------------------------------
% 122.00/17.51 % (3973616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.00/17.51 % (3973616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.00/17.51 % (3973616)CaDiCaL version: 2.1.3
% 122.00/17.51 % (3973616)Termination reason: Inappropriate
% 122.00/17.51 % (3973616)Time elapsed: 0.0000 s
% 122.00/17.51 % (3973616)Peak memory usage: 10 MB
% 122.00/17.51 % (3973616)------------------------------
% 122.00/17.51 % (3973616)------------------------------
% 122.00/17.51 % (3973618)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4196518753:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi)
% 122.00/17.51 % (3973618)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 122.00/17.51 % (3973618)Terminated due to inappropriate strategy.
% 122.00/17.51 % (3973618)------------------------------
% 122.00/17.51 % (3973618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.00/17.51 % (3973618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.00/17.51 % (3973618)CaDiCaL version: 2.1.3
% 122.00/17.51 % (3973618)Termination reason: Inappropriate
% 122.00/17.51 % (3973618)Time elapsed: 0.0000 s
% 122.00/17.51 % (3973618)Peak memory usage: 10 MB
% 122.00/17.51 % (3973618)------------------------------
% 122.00/17.51 % (3973618)------------------------------
% 122.00/17.51 % (3973620)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1621870650:i=14071_2969 on theBenchmark for (2969ds/14071Mi)
% 122.00/17.51 % (3973620)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 122.00/17.51 % (3973620)Terminated due to inappropriate strategy.
% 122.00/17.51 % (3973620)------------------------------
% 122.00/17.51 % (3973620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.00/17.51 % (3973620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.00/17.51 % (3973620)CaDiCaL version: 2.1.3
% 122.00/17.51 % (3973620)Termination reason: Inappropriate
% 122.00/17.51 % (3973620)Time elapsed: 0.0000 s
% 122.00/17.51 % (3973620)Peak memory usage: 10 MB
% 122.00/17.51 % (3973620)------------------------------
% 122.00/17.51 % (3973620)------------------------------
% 122.00/17.51 % (3973622)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2634860600:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi)
% 122.00/17.51 % (3973604)Instruction limit reached!
% 122.00/17.51 % (3973604)------------------------------
% 122.00/17.51 % (3973604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.00/17.51 % (3973604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.00/17.51 % (3973604)CaDiCaL version: 2.1.3
% 122.00/17.51 % (3973604)Termination reason: Instruction limit
% 122.00/17.51 % (3973604)Termination phase: Saturation
% 122.00/17.51 % (3973604)Time elapsed: 2.047 s
% 122.00/17.51 % (3973604)Peak memory usage: 32 MB
% 122.00/17.51 % (3973604)Instructions burned: 3775 (million)
% 122.00/17.51 % (3973624)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3765277581:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi)
% 122.00/17.51 % (3973598)Instruction limit reached!
% 122.00/17.51 % (3973598)------------------------------
% 122.00/17.51 % (3973598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.00/17.51 % (3973598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.00/17.51 % (3973598)CaDiCaL version: 2.1.3
% 122.00/17.51 % (3973598)Termination reason: Instruction limit
% 122.00/17.51 % (3973598)Termination phase: Saturation
% 122.00/17.51 % (3973598)Time elapsed: 3.209 s
% 122.00/17.51 % (3973598)Peak memory usage: 38 MB
% 122.00/17.51 % (3973598)Instructions burned: 5116 (million)
% 122.00/17.51 % (3973626)dis+10_16:1_sil=16000:random_seed=3955542358:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi)
% 132.45/18.91 % (3973614)Instruction limit reached!
% 132.45/18.91 % (3973614)------------------------------
% 132.45/18.91 % (3973614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 132.45/18.91 % (3973614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.45/18.91 % (3973614)CaDiCaL version: 2.1.3
% 132.45/18.91 % (3973614)Termination reason: Instruction limit
% 132.45/18.91 % (3973614)Termination phase: Saturation
% 132.45/18.91 % (3973614)Time elapsed: 2.749 s
% 132.45/18.91 % (3973614)Peak memory usage: 48 MB
% 132.45/18.91 % (3973614)Instructions burned: 5211 (million)
% 132.45/18.91 % (3973628)ott-3_8_sil=64000:random_seed=2095523411:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi)
% 132.45/18.91 % (3973622)Instruction limit reached!
% 132.45/18.91 % (3973622)------------------------------
% 132.45/18.91 % (3973622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 132.45/18.91 % (3973622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.45/18.91 % (3973622)CaDiCaL version: 2.1.3
% 132.45/18.91 % (3973622)Termination reason: Instruction limit
% 132.45/18.91 % (3973622)Termination phase: Saturation
% 132.45/18.91 % (3973622)Time elapsed: 4.898 s
% 132.45/18.91 % (3973622)Peak memory usage: 206 MB
% 132.45/18.91 % (3973622)Instructions burned: 22567 (million)
% 132.45/18.91 % (3973630)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2523946462:fmbsr=2:i=32576_2919 on theBenchmark for (2919ds/32576Mi)
% 132.45/18.91 % (3973630)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 132.45/18.91 % (3973630)Terminated due to inappropriate strategy.
% 132.45/18.91 % (3973630)------------------------------
% 132.45/18.91 % (3973630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 132.45/18.91 % (3973630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.45/18.91 % (3973630)CaDiCaL version: 2.1.3
% 132.45/18.91 % (3973630)Termination reason: Inappropriate
% 132.45/18.91 % (3973630)Time elapsed: 0.0000 s
% 132.45/18.91 % (3973630)Peak memory usage: 10 MB
% 132.45/18.91 % (3973630)------------------------------
% 132.45/18.91 % (3973630)------------------------------
% 132.45/18.91 % (3973632)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=548002131:i=11404_2919 on theBenchmark for (2919ds/11404Mi)
% 132.45/18.91 % (3973624)Instruction limit reached!
% 132.45/18.91 % (3973624)------------------------------
% 132.45/18.91 % (3973624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 132.45/18.91 % (3973624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.45/18.91 % (3973624)CaDiCaL version: 2.1.3
% 132.45/18.91 % (3973624)Termination reason: Instruction limit
% 132.45/18.91 % (3973624)Termination phase: Saturation
% 132.45/18.91 % (3973624)Time elapsed: 5.024 s
% 132.45/18.91 % (3973624)Peak memory usage: 51 MB
% 132.45/18.91 % (3973624)Instructions burned: 8174 (million)
% 132.45/18.91 % (3973634)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=67708913:i=14134_2916 on theBenchmark for (2916ds/14134Mi)
% 132.45/18.91 % (3973626)Instruction limit reached!
% 132.45/18.91 % (3973626)------------------------------
% 132.45/18.91 % (3973626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 132.45/18.91 % (3973626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.45/18.91 % (3973626)CaDiCaL version: 2.1.3
% 132.45/18.91 % (3973626)Termination reason: Instruction limit
% 132.45/18.91 % (3973626)Termination phase: Saturation
% 132.45/18.91 % (3973626)Time elapsed: 4.642 s
% 132.45/18.91 % (3973626)Peak memory usage: 52 MB
% 132.45/18.91 % (3973626)Instructions burned: 9155 (million)
% 132.45/18.91 % (3973636)dis+33_16_sil=32000:sac=on:random_seed=2212221401:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi)
% 132.45/18.91 % (3973632)Instruction limit reached!
% 132.45/18.91 % (3973632)------------------------------
% 132.45/18.91 % (3973632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 132.45/18.91 % (3973632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.45/18.91 % (3973632)CaDiCaL version: 2.1.3
% 132.45/18.91 % (3973632)Termination reason: Instruction limit
% 132.45/18.91 % (3973632)Termination phase: Saturation
% 132.45/18.91 % (3973632)Time elapsed: 3.879 s
% 132.45/18.91 % (3973632)Peak memory usage: 60 MB
% 132.45/18.91 % (3973632)Instructions burned: 11405 (million)
% 132.45/18.91 % (3973638)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3089226154:avsq=on:i=17627:add=on:amm=off_2880 on theBenchmark for (2880ds/17627Mi)
% 132.45/18.91 % (3973638)Instruction limit reached!
% 132.45/18.91 % (3973638)------------------------------
% 139.36/19.91 % (3973638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.36/19.91 % (3973638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.36/19.91 % (3973638)CaDiCaL version: 2.1.3
% 139.36/19.91 % (3973638)Termination reason: Instruction limit
% 139.36/19.91 % (3973638)Termination phase: Saturation
% 139.36/19.91 % (3973638)Time elapsed: 4.934 s
% 139.36/19.91 % (3973638)Peak memory usage: 68 MB
% 139.36/19.91 % (3973638)Instructions burned: 17628 (million)
% 139.36/19.91 % (3973999)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3290432082:s2a=on:i=53295_2831 on theBenchmark for (2831ds/53295Mi)
% 139.36/19.91 % (3973636)Instruction limit reached!
% 139.36/19.91 % (3973636)------------------------------
% 139.36/19.91 % (3973636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.36/19.91 % (3973636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.36/19.91 % (3973636)CaDiCaL version: 2.1.3
% 139.36/19.91 % (3973636)Termination reason: Instruction limit
% 139.36/19.91 % (3973636)Termination phase: Saturation
% 139.36/19.91 % (3973636)Time elapsed: 8.465 s
% 139.36/19.91 % (3973636)Peak memory usage: 121 MB
% 139.36/19.91 % (3973636)Instructions burned: 15851 (million)
% 139.36/19.91 % (3974001)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3746813:i=26857:ins=20_2828 on theBenchmark for (2828ds/26857Mi)
% 139.36/19.91 % (3974001)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 139.36/19.91 % (3974001)Terminated due to inappropriate strategy.
% 139.36/19.91 % (3974001)------------------------------
% 139.36/19.91 % (3974001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.36/19.91 % (3974001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.36/19.91 % (3974001)CaDiCaL version: 2.1.3
% 139.36/19.91 % (3974001)Termination reason: Inappropriate
% 139.36/19.91 % (3974001)Time elapsed: 0.0000 s
% 139.36/19.91 % (3974001)Peak memory usage: 11 MB
% 139.36/19.91 % (3974001)------------------------------
% 139.36/19.91 % (3974001)------------------------------
% 139.36/19.91 % (3974003)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2262947887:i=28120:bs=on:fsr=off_2828 on theBenchmark for (2828ds/28120Mi)
% 139.36/19.91 % (3973634)Instruction limit reached!
% 139.36/19.91 % (3973634)------------------------------
% 139.36/19.91 % (3973634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.36/19.91 % (3973634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.36/19.91 % (3973634)CaDiCaL version: 2.1.3
% 139.36/19.91 % (3973634)Termination reason: Instruction limit
% 139.36/19.91 % (3973634)Termination phase: Saturation
% 139.36/19.91 % (3973634)Time elapsed: 8.886 s
% 139.36/19.91 % (3973634)Peak memory usage: 69 MB
% 139.36/19.91 % (3973634)Instructions burned: 14134 (million)
% 139.36/19.91 % (3974005)fmb+10_1_sil=256000:fmbss=7:random_seed=3104899683:fmbsr=1.6:i=182295_2827 on theBenchmark for (2827ds/182295Mi)
% 139.36/19.91 % (3974005)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 139.36/19.91 % (3974005)Terminated due to inappropriate strategy.
% 139.36/19.91 % (3974005)------------------------------
% 139.36/19.91 % (3974005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.36/19.91 % (3974005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.36/19.91 % (3974005)CaDiCaL version: 2.1.3
% 139.36/19.91 % (3974005)Termination reason: Inappropriate
% 139.36/19.91 % (3974005)Time elapsed: 0.0000 s
% 139.36/19.91 % (3974005)Peak memory usage: 10 MB
% 139.36/19.91 % (3974005)------------------------------
% 139.36/19.91 % (3974005)------------------------------
% 139.36/19.91 % (3974007)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2735233778:i=44625:gsp=on_2827 on theBenchmark for (2827ds/44625Mi)
% 139.36/19.91 % (3974007)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 139.36/19.91 % (3974007)Terminated due to inappropriate strategy.
% 139.36/19.91 % (3974007)------------------------------
% 139.36/19.91 % (3974007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.36/19.91 % (3974007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.36/19.91 % (3974007)CaDiCaL version: 2.1.3
% 139.36/19.91 % (3974007)Termination reason: Inappropriate
% 139.36/19.91 % (3974007)Time elapsed: 0.0000 s
% 139.36/19.91 % (3974007)Peak memory usage: 10 MB
% 139.36/19.91 % (3974007)------------------------------
% 139.36/19.91 % (3974007)------------------------------
% 139.36/19.91 % (3974009)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2780556247:i=160505_2827 on theBenchmark for (2827ds/160505Mi)
% 158.71/22.64 % (3974009)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 158.71/22.64 % (3974009)Terminated due to inappropriate strategy.
% 158.71/22.64 % (3974009)------------------------------
% 158.71/22.64 % (3974009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 158.71/22.64 % (3974009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.71/22.64 % (3974009)CaDiCaL version: 2.1.3
% 158.71/22.64 % (3974009)Termination reason: Inappropriate
% 158.71/22.64 % (3974009)Time elapsed: 0.0000 s
% 158.71/22.64 % (3974009)Peak memory usage: 10 MB
% 158.71/22.64 % (3974009)------------------------------
% 158.71/22.64 % (3974009)------------------------------
% 158.71/22.64 % (3974011)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2403431020:fmbsr=1.3:i=225729_2827 on theBenchmark for (2827ds/225729Mi)
% 158.71/22.64 % (3974011)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 158.71/22.64 % (3974011)Terminated due to inappropriate strategy.
% 158.71/22.64 % (3974011)------------------------------
% 158.71/22.64 % (3974011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 158.71/22.64 % (3974011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.71/22.64 % (3974011)CaDiCaL version: 2.1.3
% 158.71/22.64 % (3974011)Termination reason: Inappropriate
% 158.71/22.64 % (3974011)Time elapsed: 0.0000 s
% 158.71/22.64 % (3974011)Peak memory usage: 10 MB
% 158.71/22.64 % (3974011)------------------------------
% 158.71/22.64 % (3974011)------------------------------
% 158.71/22.64 % (3974013)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3511725222:fmbsr=2:i=185024:ins=7_2826 on theBenchmark for (2826ds/185024Mi)
% 158.71/22.64 % (3974013)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 158.71/22.64 % (3974013)Terminated due to inappropriate strategy.
% 158.71/22.64 % (3974013)------------------------------
% 158.71/22.64 % (3974013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 158.71/22.64 % (3974013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.71/22.64 % (3974013)CaDiCaL version: 2.1.3
% 158.71/22.64 % (3974013)Termination reason: Inappropriate
% 158.71/22.64 % (3974013)Time elapsed: 0.0000 s
% 158.71/22.64 % (3974013)Peak memory usage: 11 MB
% 158.71/22.64 % (3974013)------------------------------
% 158.71/22.64 % (3974013)------------------------------
% 158.71/22.64 % (3974015)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3009097269:rtra=on_2826 on theBenchmark for (2826ds/0Mi)
% 158.71/22.64 % (3974015)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 158.71/22.64 % (3974015)Terminated due to inappropriate strategy.
% 158.71/22.64 % (3974015)------------------------------
% 158.71/22.64 % (3974015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 158.71/22.64 % (3974015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.71/22.64 % (3974015)CaDiCaL version: 2.1.3
% 158.71/22.64 % (3974015)Termination reason: Inappropriate
% 158.71/22.64 % (3974015)Time elapsed: 0.0000 s
% 158.71/22.64 % (3974015)Peak memory usage: 10 MB
% 158.71/22.64 % (3974015)------------------------------
% 158.71/22.64 % (3974015)------------------------------
% 158.71/22.64 % (3973612)Instruction limit reached!
% 158.71/22.64 % (3973612)------------------------------
% 158.71/22.64 % (3973612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 158.71/22.64 % (3973612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.71/22.64 % (3973612)CaDiCaL version: 2.1.3
% 158.71/22.64 % (3973612)Termination reason: Instruction limit
% 158.71/22.64 % (3973612)Termination phase: Saturation
% 158.71/22.64 % (3973612)Time elapsed: 14.810 s
% 158.71/22.64 % (3973612)Peak memory usage: 188 MB
% 158.71/22.64 % (3973612)Instructions burned: 29341 (million)
% 158.71/22.64 % (3974017)% WARNING: option uhcvi not known.
% 158.71/22.64 % (3974017)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=410304575:i=271062:add=off:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/271062Mi)
% 158.71/22.64 % (3974019)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=607016161:i=176048:add=on:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/176048Mi)
% 158.71/22.64 % (3973628)Instruction limit reached!
% 158.71/22.64 % (3973628)------------------------------
% 158.71/22.64 % (3973628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.21/24.56 % (3973628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.21/24.56 % (3973628)CaDiCaL version: 2.1.3
% 172.21/24.56 % (3973628)Termination reason: Instruction limit
% 172.21/24.56 % (3973628)Termination phase: Saturation
% 172.21/24.56 % (3973628)Time elapsed: 13.180 s
% 172.21/24.56 % (3973628)Peak memory usage: 67 MB
% 172.21/24.56 % (3973628)Instructions burned: 20139 (million)
% 172.21/24.56 % (3974021)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2399583104:i=206:fgj=on:rtra=on_2813 on theBenchmark for (2813ds/206Mi)
% 172.21/24.56 % (3974021)Instruction limit reached!
% 172.21/24.56 % (3974021)------------------------------
% 172.21/24.56 % (3974021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.21/24.56 % (3974021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.21/24.56 % (3974021)CaDiCaL version: 2.1.3
% 172.21/24.56 % (3974021)Termination reason: Instruction limit
% 172.21/24.56 % (3974021)Termination phase: Saturation
% 172.21/24.56 % (3974021)Time elapsed: 0.133 s
% 172.21/24.56 % (3974021)Peak memory usage: 13 MB
% 172.21/24.56 % (3974021)Instructions burned: 207 (million)
% 172.21/24.56 % (3974023)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2714285041:i=232:rtra=on_2811 on theBenchmark for (2811ds/232Mi)
% 172.21/24.56 % (3974023)Instruction limit reached!
% 172.21/24.56 % (3974023)------------------------------
% 172.21/24.56 % (3974023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.21/24.56 % (3974023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.21/24.56 % (3974023)CaDiCaL version: 2.1.3
% 172.21/24.56 % (3974023)Termination reason: Instruction limit
% 172.21/24.56 % (3974023)Termination phase: Saturation
% 172.21/24.56 % (3974023)Time elapsed: 0.148 s
% 172.21/24.56 % (3974023)Peak memory usage: 13 MB
% 172.21/24.56 % (3974023)Instructions burned: 232 (million)
% 172.21/24.56 % (3974025)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=84904705:i=262:rtra=on_2809 on theBenchmark for (2809ds/262Mi)
% 172.21/24.56 % (3974025)Instruction limit reached!
% 172.21/24.56 % (3974025)------------------------------
% 172.21/24.56 % (3974025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.21/24.56 % (3974025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.21/24.56 % (3974025)CaDiCaL version: 2.1.3
% 172.21/24.56 % (3974025)Termination reason: Instruction limit
% 172.21/24.56 % (3974025)Termination phase: Saturation
% 172.21/24.56 % (3974025)Time elapsed: 0.171 s
% 172.21/24.56 % (3974025)Peak memory usage: 14 MB
% 172.21/24.56 % (3974025)Instructions burned: 262 (million)
% 172.21/24.56 % (3974027)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=11904531:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2807 on theBenchmark for (2807ds/318Mi)
% 172.21/24.56 % (3974027)Instruction limit reached!
% 172.21/24.56 % (3974027)------------------------------
% 172.21/24.56 % (3974027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.21/24.56 % (3974027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.21/24.56 % (3974027)CaDiCaL version: 2.1.3
% 172.21/24.56 % (3974027)Termination reason: Instruction limit
% 172.21/24.56 % (3974027)Termination phase: Saturation
% 172.21/24.56 % (3974027)Time elapsed: 0.224 s
% 172.21/24.56 % (3974027)Peak memory usage: 14 MB
% 172.21/24.56 % (3974027)Instructions burned: 318 (million)
% 172.21/24.56 % (3974029)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1212798063:i=1428:nm=2:rtra=on_2805 on theBenchmark for (2805ds/1428Mi)
% 172.21/24.56 % (3974029)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 172.21/24.56 % (3974029)Terminated due to inappropriate strategy.
% 172.21/24.56 % (3974029)------------------------------
% 172.21/24.56 % (3974029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.21/24.56 % (3974029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.21/24.56 % (3974029)CaDiCaL version: 2.1.3
% 172.21/24.56 % (3974029)Termination reason: Inappropriate
% 172.21/24.56 % (3974029)Time elapsed: 0.0000 s
% 172.21/24.56 % (3974029)Peak memory usage: 10 MB
% 172.21/24.56 % (3974029)------------------------------
% 172.21/24.56 % (3974029)------------------------------
% 172.21/24.56 % (3974031)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=902782134:i=262:bd=preordered:rtra=on:fsd=on_2805 on theBenchmark for (2805ds/262Mi)
% 172.21/24.56 % (3974031)Instruction limit reached!
% 172.21/24.56 % (3974031)------------------------------
% 172.21/24.56 % (3974031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974031)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974031)Termination reason: Instruction limit
% 162.73/30.17 % (3974031)Termination phase: Saturation
% 162.73/30.17 % (3974031)Time elapsed: 0.186 s
% 162.73/30.17 % (3974031)Peak memory usage: 14 MB
% 162.73/30.17 % (3974031)Instructions burned: 262 (million)
% 162.73/30.17 % (3974033)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=2212968367:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2803 on theBenchmark for (2803ds/1368Mi)
% 162.73/30.17 % (3974033)Instruction limit reached!
% 162.73/30.17 % (3974033)------------------------------
% 162.73/30.17 % (3974033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974033)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974033)Termination reason: Instruction limit
% 162.73/30.17 % (3974033)Termination phase: Saturation
% 162.73/30.17 % (3974033)Time elapsed: 0.722 s
% 162.73/30.17 % (3974033)Peak memory usage: 25 MB
% 162.73/30.17 % (3974033)Instructions burned: 1369 (million)
% 162.73/30.17 % (3974035)ott-21_1_sil=16000:si=on:fs=off:random_seed=485431215:i=360:av=off:fsr=off:rtra=on_2795 on theBenchmark for (2795ds/360Mi)
% 162.73/30.17 % (3974035)Instruction limit reached!
% 162.73/30.17 % (3974035)------------------------------
% 162.73/30.17 % (3974035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974035)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974035)Termination reason: Instruction limit
% 162.73/30.17 % (3974035)Termination phase: Saturation
% 162.73/30.17 % (3974035)Time elapsed: 0.159 s
% 162.73/30.17 % (3974035)Peak memory usage: 13 MB
% 162.73/30.17 % (3974035)Instructions burned: 360 (million)
% 162.73/30.17 % (3974037)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=311409673:i=954:bd=all:rtra=on_2793 on theBenchmark for (2793ds/954Mi)
% 162.73/30.17 % (3974037)Instruction limit reached!
% 162.73/30.17 % (3974037)------------------------------
% 162.73/30.17 % (3974037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974037)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974037)Termination reason: Instruction limit
% 162.73/30.17 % (3974037)Termination phase: Saturation
% 162.73/30.17 % (3974037)Time elapsed: 0.621 s
% 162.73/30.17 % (3974037)Peak memory usage: 16 MB
% 162.73/30.17 % (3974037)Instructions burned: 955 (million)
% 162.73/30.17 % (3974039)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=51889843:fmbsr=1.3:i=1730:ins=25:rtra=on_2787 on theBenchmark for (2787ds/1730Mi)
% 162.73/30.17 % (3974039)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.73/30.17 % (3974039)Terminated due to inappropriate strategy.
% 162.73/30.17 % (3974039)------------------------------
% 162.73/30.17 % (3974039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974039)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974039)Termination reason: Inappropriate
% 162.73/30.17 % (3974039)Time elapsed: 0.0000 s
% 162.73/30.17 % (3974039)Peak memory usage: 10 MB
% 162.73/30.17 % (3974039)------------------------------
% 162.73/30.17 % (3974039)------------------------------
% 162.73/30.17 % (3974041)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1632512927:i=2358:rtra=on_2787 on theBenchmark for (2787ds/2358Mi)
% 162.73/30.17 % (3974041)Instruction limit reached!
% 162.73/30.17 % (3974041)------------------------------
% 162.73/30.17 % (3974041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974041)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974041)Termination reason: Instruction limit
% 162.73/30.17 % (3974041)Termination phase: Saturation
% 162.73/30.17 % (3974041)Time elapsed: 1.091 s
% 162.73/30.17 % (3974041)Peak memory usage: 24 MB
% 162.73/30.17 % (3974041)Instructions burned: 2360 (million)
% 162.73/30.17 % (3974043)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3438066884:i=1778:ins=1:rtra=on_2776 on theBenchmark for (2776ds/1778Mi)
% 162.73/30.17 % (3974043)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.73/30.17 % (3974043)Terminated due to inappropriate strategy.
% 162.73/30.17 % (3974043)------------------------------
% 162.73/30.17 % (3974043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974043)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974043)Termination reason: Inappropriate
% 162.73/30.17 % (3974043)Time elapsed: 0.0000 s
% 162.73/30.17 % (3974043)Peak memory usage: 10 MB
% 162.73/30.17 % (3974043)------------------------------
% 162.73/30.17 % (3974043)------------------------------
% 162.73/30.17 % (3974045)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=2000705615:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2775 on theBenchmark for (2775ds/1384Mi)
% 162.73/30.17 % (3974045)Instruction limit reached!
% 162.73/30.17 % (3974045)------------------------------
% 162.73/30.17 % (3974045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974045)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974045)Termination reason: Instruction limit
% 162.73/30.17 % (3974045)Termination phase: Saturation
% 162.73/30.17 % (3974045)Time elapsed: 0.802 s
% 162.73/30.17 % (3974045)Peak memory usage: 22 MB
% 162.73/30.17 % (3974045)Instructions burned: 1384 (million)
% 162.73/30.17 % (3974047)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3259992056:i=1758:kws=inv_precedence:fsr=off:rtra=on_2767 on theBenchmark for (2767ds/1758Mi)
% 162.73/30.17 % (3974047)Instruction limit reached!
% 162.73/30.17 % (3974047)------------------------------
% 162.73/30.17 % (3974047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974047)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974047)Termination reason: Instruction limit
% 162.73/30.17 % (3974047)Termination phase: Saturation
% 162.73/30.17 % (3974047)Time elapsed: 1.004 s
% 162.73/30.17 % (3974047)Peak memory usage: 24 MB
% 162.73/30.17 % (3974047)Instructions burned: 1759 (million)
% 162.73/30.17 % (3974049)fmb+10_1_sil=64000:si=on:random_seed=2969196701:i=44122:nm=2:rtra=on:gsp=on_2757 on theBenchmark for (2757ds/44122Mi)
% 162.73/30.17 % (3974049)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.73/30.17 % (3974049)Terminated due to inappropriate strategy.
% 162.73/30.17 % (3974049)------------------------------
% 162.73/30.17 % (3974049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974049)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974049)Termination reason: Inappropriate
% 162.73/30.17 % (3974049)Time elapsed: 0.001 s
% 162.73/30.17 % (3974049)Peak memory usage: 10 MB
% 162.73/30.17 % (3974049)------------------------------
% 162.73/30.17 % (3974049)------------------------------
% 162.73/30.17 % (3974051)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4189505378:i=19030:nm=5:rtra=on_2757 on theBenchmark for (2757ds/19030Mi)
% 162.73/30.17 % (3974051)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.73/30.17 % (3974051)Terminated due to inappropriate strategy.
% 162.73/30.17 % (3974051)------------------------------
% 162.73/30.17 % (3974051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974051)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974051)Termination reason: Inappropriate
% 162.73/30.17 % (3974051)Time elapsed: 0.001 s
% 162.73/30.17 % (3974051)Peak memory usage: 11 MB
% 162.73/30.17 % (3974051)------------------------------
% 162.73/30.17 % (3974051)------------------------------
% 162.73/30.17 % (3974053)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1233293457:fmbsr=1.7:i=1840:rtra=on_2756 on theBenchmark for (2756ds/1840Mi)
% 162.73/30.17 % (3974053)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.73/30.17 % (3974053)Terminated due to inappropriate strategy.
% 162.73/30.17 % (3974053)------------------------------
% 162.73/30.17 % (3974053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974053)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974053)Termination reason: Inappropriate
% 162.73/30.17 % (3974053)Time elapsed: 0.0000 s
% 162.73/30.17 % (3974053)Peak memory usage: 10 MB
% 162.73/30.17 % (3974053)------------------------------
% 162.73/30.17 % (3974053)------------------------------
% 162.73/30.17 % (3974055)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3397931701:i=10262:rtra=on_2756 on theBenchmark for (2756ds/10262Mi)
% 162.73/30.17 % (3974003)Instruction limit reached!
% 162.73/30.17 % (3974003)------------------------------
% 162.73/30.17 % (3974003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3974003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3974003)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3974003)Termination reason: Instruction limit
% 162.73/30.17 % (3974003)Termination phase: Saturation
% 162.73/30.17 % (3974003)Time elapsed: 12.052 s
% 162.73/30.17 % (3974003)Peak memory usage: 25 MB
% 162.73/30.17 % (3974003)Instructions burned: 28120 (million)
% 162.73/30.17 % (3974311)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=577791612:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2707 on theBenchmark for (2707ds/2944Mi)
% 162.73/30.17 % (3973549) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3973543-3973549"...
% 162.73/30.17 % (3973549)...printing done.
% 162.73/30.17 % (3973549)Refutation found. Thanks to Tanya!
% 162.73/30.17 % SZS status Theorem for theBenchmark
% 162.73/30.17 % SZS output start Proof for theBenchmark
% 162.73/30.17 tff(func_def_9, type, sK0: $int).
% 162.73/30.17 tff(func_def_10, type, sK1: $int).
% 162.73/30.17 tff(f1,conjecture,(
% 162.73/30.17 ! [X0 : $int,X1 : $int,X2 : $int] : (($less(X0,5) & $less(X1,3) & $greater($sum(X0,$product(2,X1)),7)) => X1 = 2)),
% 162.73/30.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1)).
% 162.73/30.17 tff(f2,negated_conjecture,(
% 162.73/30.17 ~ ! [X0 : $int,X1 : $int,X2 : $int] : (($less(X0,5) & $less(X1,3) & $greater($sum(X0,$product(2,X1)),7)) => X1 = 2)),
% 162.73/30.17 inference(negated_conjecture,[status(cth)],[f1])).
% 162.73/30.17 tff(f3,plain,(
% 162.73/30.17 ~ ! [X0 : $int,X1 : $int,X2 : $int] : (($less(X0,5) & $less(X1,3) & $less(7,$sum(X0,$product(2,X1)))) => X1 = 2)),
% 162.73/30.17 inference(theory_normalization,[],[f2])).
% 162.73/30.17 tff(f4,definition,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 162.73/30.17 introduced(theory,[tha_commutativity])).
% 162.73/30.17 tff(f5,definition,(
% 162.73/30.17 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 162.73/30.17 introduced(theory,[tha_associativity])).
% 162.73/30.17 tff(f6,definition,(
% 162.73/30.17 ( ! [X0 : $int] : ($sum(X0,0) = X0) )),
% 162.73/30.17 introduced(theory,[tha_right_identity])).
% 162.73/30.17 tff(f7,definition,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X0,X1)) = $sum($uminus(X1),$uminus(X0))) )),
% 162.73/30.17 introduced(theory,[tha_inverse_op_op_inverses])).
% 162.73/30.17 tff(f8,definition,(
% 162.73/30.17 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 162.73/30.17 introduced(theory,[tha_inverse_op_unit])).
% 162.73/30.17 tff(f10,definition,(
% 162.73/30.17 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 162.73/30.17 introduced(theory,[tha_transitivity])).
% 162.73/30.17 tff(f11,definition,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 162.73/30.17 introduced(theory,[tha_order_totality])).
% 162.73/30.17 tff(f12,definition,(
% 162.73/30.17 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,X2),$sum(X1,X2))) )),
% 162.73/30.17 introduced(theory,[tha_order_monotonicity])).
% 162.73/30.17 tff(f13,definition,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 162.73/30.17 introduced(theory,[tha_order_plus_one_dichotomy])).
% 162.73/30.17 tff(f14,definition,(
% 162.73/30.17 ( ! [X0 : $int] : ($uminus($uminus(X0)) = X0) )),
% 162.73/30.17 introduced(theory,[tha_minus_minus_x])).
% 162.73/30.17 tff(f15,definition,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($product(X0,X1) = $product(X1,X0)) )),
% 162.73/30.17 introduced(theory,[tha_commutativity])).
% 162.73/30.17 tff(f17,definition,(
% 162.73/30.17 ( ! [X0 : $int] : ($product(X0,1) = X0) )),
% 162.73/30.17 introduced(theory,[tha_right_identity])).
% 162.73/30.17 tff(f19,definition,(
% 162.73/30.17 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2))) )),
% 162.73/30.17 introduced(theory,[tha_distributivity])).
% 162.73/30.17 tff(f21,definition,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 162.73/30.17 introduced(theory,[tha_extra_integer_ordering])).
% 162.73/30.17 tff(f22,plain,(
% 162.73/30.17 ~ ! [X0 : $int,X1 : $int] : (($less(X0,5) & $less(X1,3) & $less(7,$sum(X0,$product(2,X1)))) => X1 = 2)),
% 162.73/30.17 inference(rectify,[],[f3])).
% 162.73/30.17 tff(f23,plain,(
% 162.73/30.17 ? [X0 : $int,X1 : $int] : (2 != X1 & ($less(X0,5) & $less(X1,3) & $less(7,$sum(X0,$product(2,X1)))))),
% 162.73/30.17 inference(ennf_transformation,[],[f22])).
% 162.73/30.17 tff(f24,plain,(
% 162.73/30.17 ? [X0 : $int,X1 : $int] : (2 != X1 & $less(X0,5) & $less(X1,3) & $less(7,$sum(X0,$product(2,X1))))),
% 162.73/30.17 inference(flattening,[],[f23])).
% 162.73/30.17 tff(f25,plain,(
% 162.73/30.17 $less(7,$sum(sK0,$product(2,sK1)))),
% 162.73/30.17 inference(cnf_transformation,[],[f24])).
% 162.73/30.17 tff(f26,plain,(
% 162.73/30.17 $less(sK1,3)),
% 162.73/30.17 inference(cnf_transformation,[],[f24])).
% 162.73/30.17 tff(f27,plain,(
% 162.73/30.17 $less(sK0,5)),
% 162.73/30.17 inference(cnf_transformation,[],[f24])).
% 162.73/30.17 tff(f28,plain,(
% 162.73/30.17 2 != sK1),
% 162.73/30.17 inference(cnf_transformation,[],[f24])).
% 162.73/30.17 tff(f30,plain,(
% 162.73/30.17 ( ! [X0 : $int] : (0 = $sum($uminus(X0),X0)) )),
% 162.73/30.17 inference(superposition,[],[f8,f14])).
% 162.73/30.17 tff(f44,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(X0,X1)) )),
% 162.73/30.17 inference(superposition,[],[f13,f4])).
% 162.73/30.17 tff(f50,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(1,X0)) | ~$less(X0,X1)) )),
% 162.73/30.17 inference(superposition,[],[f21,f4])).
% 162.73/30.17 tff(f55,plain,(
% 162.73/30.17 ( ! [X0 : $int] : (~$less(X0,sK0) | $less(X0,5)) )),
% 162.73/30.17 inference(resolution,[],[f10,f27])).
% 162.73/30.17 tff(f58,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($less($sum(X1,1),X0) | $sum(X1,1) = X0 | ~$less(X1,X0)) )),
% 162.73/30.17 inference(resolution,[],[f11,f21])).
% 162.73/30.17 tff(f59,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less(sK0,X0) | $less(X0,5) | sK0 = X0) )),
% 162.73/30.17 inference(resolution,[],[f11,f55])).
% 162.73/30.17 tff(f80,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less($sum(7,X0),$sum($sum(sK0,$product(2,sK1)),X0))) )),
% 162.73/30.17 inference(resolution,[],[f12,f25])).
% 162.73/30.17 tff(f81,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less($sum(sK0,X0),$sum(5,X0))) )),
% 162.73/30.17 inference(resolution,[],[f12,f27])).
% 162.73/30.17 tff(f82,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less($sum(sK1,X0),$sum(3,X0))) )),
% 162.73/30.17 inference(resolution,[],[f12,f26])).
% 162.73/30.17 tff(f86,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 162.73/30.17 inference(superposition,[],[f5,f8])).
% 162.73/30.17 tff(f92,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : (0 = $sum(X0,$sum(X1,$uminus($sum(X0,X1))))) )),
% 162.73/30.17 inference(superposition,[],[f5,f8])).
% 162.73/30.17 tff(f93,plain,(
% 162.73/30.17 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum(X1,$sum(X2,X0))) )),
% 162.73/30.17 inference(superposition,[],[f5,f4])).
% 162.73/30.17 tff(f98,plain,(
% 162.73/30.17 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X2,$sum(X0,$sum(X1,1))) | ~$less($sum(X0,X1),X2)) )),
% 162.73/30.17 inference(superposition,[],[f21,f5])).
% 162.73/30.17 tff(f102,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 162.73/30.17 inference(evaluation,[],[f86])).
% 162.73/30.17 tff(f120,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($product(X0,$sum(1,X1)) = $sum(X0,$product(X0,X1))) )),
% 162.73/30.17 inference(superposition,[],[f19,f17])).
% 162.73/30.17 tff(f152,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : (~$less(X0,$sum(sK0,X1)) | $less(X0,$sum(5,X1))) )),
% 162.73/30.17 inference(resolution,[],[f81,f10])).
% 162.73/30.17 tff(f192,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less($sum(7,X0),$sum(sK0,$sum($product(2,sK1),X0)))) )),
% 162.73/30.17 inference(forward_demodulation,[],[f80,f5])).
% 162.73/30.17 tff(f194,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($less(X0,$sum(sK0,$sum($product(2,sK1),X1))) | ~$less(X0,$sum(7,X1))) )),
% 162.73/30.17 inference(resolution,[],[f192,f10])).
% 162.73/30.17 tff(f201,plain,(
% 162.73/30.17 $less($sum(7,$uminus($product(2,sK1))),$sum(sK0,0))),
% 162.73/30.17 inference(superposition,[],[f192,f8])).
% 162.73/30.17 tff(f204,plain,(
% 162.73/30.17 $less($sum(7,$uminus($product(2,sK1))),sK0)),
% 162.73/30.17 inference(evaluation,[],[f201])).
% 162.73/30.17 tff(f218,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum($uminus(X0),$sum(X0,X1))) )),
% 162.73/30.17 inference(superposition,[],[f5,f30])).
% 162.73/30.17 tff(f227,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($sum($uminus(X0),$sum(X0,X1)) = X1) )),
% 162.73/30.17 inference(evaluation,[],[f218])).
% 162.73/30.17 tff(f235,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less(X0,1) | $less(0,X0)) )),
% 162.73/30.17 inference(superposition,[],[f44,f6])).
% 162.73/30.17 tff(f246,plain,(
% 162.73/30.17 ( ! [X0 : $int] : (~$less(X0,1) | ~$less(0,X0)) )),
% 162.73/30.17 inference(superposition,[],[f50,f6])).
% 162.73/30.17 tff(f261,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($uminus(X0) = $sum(X1,$uminus($sum(X0,X1)))) )),
% 162.73/30.17 inference(superposition,[],[f102,f7])).
% 162.73/30.17 tff(f263,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($sum(X1,$sum(X0,$uminus(X1))) = X0) )),
% 162.73/30.17 inference(superposition,[],[f102,f4])).
% 162.73/30.17 tff(f412,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less($sum(sK0,$sum(X0,$uminus($sum(5,X0)))),0)) )),
% 162.73/30.17 inference(superposition,[],[f81,f92])).
% 162.73/30.17 tff(f826,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($product(X0,$sum(1,1)) = $sum(X0,X0)) )),
% 162.73/30.17 inference(superposition,[],[f120,f17])).
% 162.73/30.17 tff(f854,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($sum(X0,X0) = $product(X0,2)) )),
% 162.73/30.17 inference(evaluation,[],[f826])).
% 162.73/30.17 tff(f1018,plain,(
% 162.73/30.17 ( ! [X0 : $int] : (~$less($sum(3,X0),$sum(sK1,$sum(X0,1)))) )),
% 162.73/30.17 inference(resolution,[],[f98,f82])).
% 162.73/30.17 tff(f1053,plain,(
% 162.73/30.17 ( ! [X0 : $int] : (~$less($sum(3,X0),$sum(1,$sum(sK1,X0)))) )),
% 162.73/30.17 inference(forward_demodulation,[],[f1018,f93])).
% 162.73/30.17 tff(f1165,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,$sum(1,X1)) | $sum(X0,1) = $sum(1,X1)) )),
% 162.73/30.17 inference(resolution,[],[f58,f50])).
% 162.73/30.17 tff(f1766,plain,(
% 162.73/30.17 $less($sum(7,$uminus($product(2,sK1))),5)),
% 162.73/30.17 inference(resolution,[],[f204,f55])).
% 162.73/30.17 tff(f1889,plain,(
% 162.73/30.17 ( ! [X0 : $int,X1 : $int] : ($less($sum(sK0,X1),$sum(X0,X1)) | sK0 = X0 | $less(X0,5)) )),
% 162.73/30.17 inference(resolution,[],[f59,f12])).
% 162.73/30.17 tff(f1918,definition,(
% 162.73/30.17 spl2_11 <=> 7 = sK0),
% 162.73/30.17 introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition])).
% 162.73/30.17 tff(f1920,plain,(
% 162.73/30.17 7 = sK0 | ~spl2_11),
% 162.73/30.17 inference(avatar_component_clause,[],[f1918])).
% 162.73/30.17 tff(f2160,plain,(
% 162.73/30.17 $less(7,$sum(5,$product(2,sK1)))),
% 162.73/30.17 inference(resolution,[],[f152,f25])).
% 162.73/30.17 tff(f5917,plain,(
% 162.73/30.17 ~$less($sum(3,$uminus(1)),sK1)),
% 162.73/30.17 inference(superposition,[],[f1053,f263])).
% 162.73/30.17 tff(f5939,plain,(
% 162.73/30.17 ( ! [X0 : $int] : (~$less(X0,$sum(7,$uminus(sK0))) | $less(X0,$product(2,sK1))) )),
% 162.73/30.17 inference(superposition,[],[f194,f263])).
% 162.73/30.17 tff(f5993,plain,(
% 162.73/30.17 ~$less(2,sK1)),
% 162.73/30.17 inference(evaluation,[],[f5917])).
% 162.73/30.17 tff(f118429,definition,(
% 162.73/30.17 spl2_81 <=> 0 = sK1),
% 162.73/30.17 introduced(definition,[new_symbols(definition,[spl2_81])],[avatar_definition])).
% 162.73/30.17 tff(f118430,plain,(
% 162.73/30.17 0 != sK1 | spl2_81),
% 162.73/30.17 inference(avatar_component_clause,[],[f118429])).
% 162.73/30.17 tff(f118431,plain,(
% 162.73/30.17 0 = sK1 | ~spl2_81),
% 162.73/30.17 inference(avatar_component_clause,[],[f118429])).
% 162.73/30.17 tff(f133609,definition,(
% 162.73/30.17 spl2_182 <=> 1 = sK1),
% 162.73/30.17 introduced(definition,[new_symbols(definition,[spl2_182])],[avatar_definition])).
% 162.73/30.17 tff(f133610,plain,(
% 162.73/30.17 1 != sK1 | spl2_182),
% 162.73/30.17 inference(avatar_component_clause,[],[f133609])).
% 162.73/30.17 tff(f133611,plain,(
% 162.73/30.17 1 = sK1 | ~spl2_182),
% 162.73/30.17 inference(avatar_component_clause,[],[f133609])).
% 162.73/30.17 tff(f170984,plain,(
% 162.73/30.17 $less(7,$sum(5,$product(2,1))) | ~spl2_182),
% 162.73/30.17 inference(superposition,[],[f2160,f133611])).
% 162.73/30.17 tff(f171061,plain,(
% 162.73/30.17 $false | ~spl2_182),
% 162.73/30.17 inference(evaluation,[],[f170984])).
% 162.73/30.17 tff(f171062,plain,(
% 162.73/30.17 ~spl2_182),
% 162.73/30.17 inference(avatar_contradiction_clause,[],[f171061])).
% 162.73/30.17 tff(f197772,definition,(
% 162.73/30.17 spl2_301 <=> $less(0,$product(2,sK1))),
% 162.73/30.17 introduced(definition,[new_symbols(definition,[spl2_301])],[avatar_definition])).
% 162.73/30.17 tff(f197774,plain,(
% 162.73/30.17 $less(0,$product(2,sK1)) | ~spl2_301),
% 162.73/30.17 inference(avatar_component_clause,[],[f197772])).
% 162.73/30.17 tff(f201667,definition,(
% 162.73/30.17 spl2_329 <=> $less($product(2,sK1),1)),
% 162.73/30.17 introduced(definition,[new_symbols(definition,[spl2_329])],[avatar_definition])).
% 162.73/30.17 tff(f201668,plain,(
% 162.73/30.17 $less($product(2,sK1),1) | ~spl2_329),
% 162.73/30.17 inference(avatar_component_clause,[],[f201667])).
% 162.73/30.17 tff(f264242,definition,(
% 162.73/30.17 spl2_389 <=> $less(sK1,0)),
% 162.73/30.17 introduced(definition,[new_symbols(definition,[spl2_389])],[avatar_definition])).
% 162.73/30.17 tff(f264243,plain,(
% 162.73/30.17 ~$less(sK1,0) | spl2_389),
% 162.73/30.17 inference(avatar_component_clause,[],[f264242])).
% 162.73/30.17 tff(f264244,plain,(
% 162.73/30.17 $less(sK1,0) | ~spl2_389),
% 162.73/30.17 inference(avatar_component_clause,[],[f264242])).
% 162.73/30.17 tff(f264274,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less($sum(sK1,X0),$sum(0,X0))) ) | ~spl2_389),
% 162.73/30.17 inference(resolution,[],[f264244,f12])).
% 162.73/30.17 tff(f264283,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less($sum(sK1,X0),X0)) ) | ~spl2_389),
% 162.73/30.17 inference(evaluation,[],[f264274])).
% 162.73/30.17 tff(f264311,plain,(
% 162.73/30.17 $less(0,sK1) | 0 = sK1 | spl2_389),
% 162.73/30.17 inference(resolution,[],[f264243,f11])).
% 162.73/30.17 tff(f264325,definition,(
% 162.73/30.17 spl2_399 <=> $less(0,sK1)),
% 162.73/30.17 introduced(definition,[new_symbols(definition,[spl2_399])],[avatar_definition])).
% 162.73/30.17 tff(f264326,plain,(
% 162.73/30.17 ~$less(0,sK1) | spl2_399),
% 162.73/30.17 inference(avatar_component_clause,[],[f264325])).
% 162.73/30.17 tff(f264327,plain,(
% 162.73/30.17 $less(0,sK1) | ~spl2_399),
% 162.73/30.17 inference(avatar_component_clause,[],[f264325])).
% 162.73/30.17 tff(f264430,plain,(
% 162.73/30.17 $less($sum(7,$uminus($product(2,0))),5) | ~spl2_81),
% 162.73/30.17 inference(superposition,[],[f1766,f118431])).
% 162.73/30.17 tff(f264583,plain,(
% 162.73/30.17 $false | ~spl2_81),
% 162.73/30.17 inference(evaluation,[],[f264430])).
% 162.73/30.17 tff(f264584,plain,(
% 162.73/30.17 ~spl2_81),
% 162.73/30.17 inference(avatar_contradiction_clause,[],[f264583])).
% 162.73/30.17 tff(f264817,plain,(
% 162.73/30.17 $less($product(sK1,2),sK1) | ~spl2_389),
% 162.73/30.17 inference(superposition,[],[f264283,f854])).
% 162.73/30.17 tff(f264875,plain,(
% 162.73/30.17 $less($product(2,sK1),sK1) | ~spl2_389),
% 162.73/30.17 inference(forward_demodulation,[],[f264817,f15])).
% 162.73/30.17 tff(f264934,plain,(
% 162.73/30.17 $less(0,sK1) | (spl2_81 | spl2_389)),
% 162.73/30.17 inference(forward_subsumption_resolution,[],[f264311,f118430])).
% 162.73/30.17 tff(f264938,plain,(
% 162.73/30.17 spl2_399 | spl2_81 | spl2_389),
% 162.73/30.17 inference(avatar_split_clause,[],[f264934,f264242,f118429,f264325])).
% 162.73/30.17 tff(f265029,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less($sum(0,X0),$sum(sK1,X0))) ) | ~spl2_399),
% 162.73/30.17 inference(resolution,[],[f264327,f12])).
% 162.73/30.17 tff(f265040,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less(X0,$sum(sK1,X0))) ) | ~spl2_399),
% 162.73/30.17 inference(evaluation,[],[f265029])).
% 162.73/30.17 tff(f265650,plain,(
% 162.73/30.17 ~$less(sK1,$sum(1,1)) | $sum(sK1,1) = $sum(1,1) | ~spl2_399),
% 162.73/30.17 inference(resolution,[],[f265040,f1165])).
% 162.73/30.17 tff(f265724,plain,(
% 162.73/30.17 ~$less(sK1,2) | 2 = $sum(sK1,1) | ~spl2_399),
% 162.73/30.17 inference(evaluation,[],[f265650])).
% 162.73/30.17 tff(f265740,plain,(
% 162.73/30.17 2 = $sum(1,sK1) | ~$less(sK1,2) | ~spl2_399),
% 162.73/30.17 inference(forward_demodulation,[],[f265724,f4])).
% 162.73/30.17 tff(f265745,definition,(
% 162.73/30.17 spl2_415 <=> $less(sK1,2)),
% 162.73/30.17 introduced(definition,[new_symbols(definition,[spl2_415])],[avatar_definition])).
% 162.73/30.17 tff(f265747,plain,(
% 162.73/30.17 ~$less(sK1,2) | spl2_415),
% 162.73/30.17 inference(avatar_component_clause,[],[f265745])).
% 162.73/30.17 tff(f265749,definition,(
% 162.73/30.17 spl2_416 <=> 2 = $sum(1,sK1)),
% 162.73/30.17 introduced(definition,[new_symbols(definition,[spl2_416])],[avatar_definition])).
% 162.73/30.17 tff(f265751,plain,(
% 162.73/30.17 2 = $sum(1,sK1) | ~spl2_416),
% 162.73/30.17 inference(avatar_component_clause,[],[f265749])).
% 162.73/30.17 tff(f265753,plain,(
% 162.73/30.17 ~spl2_415 | spl2_416 | ~spl2_399),
% 162.73/30.17 inference(avatar_split_clause,[],[f265740,f264325,f265749,f265745])).
% 162.73/30.17 tff(f265816,plain,(
% 162.73/30.17 $less(2,sK1) | 2 = sK1 | spl2_415),
% 162.73/30.17 inference(resolution,[],[f265747,f11])).
% 162.73/30.17 tff(f265824,plain,(
% 162.73/30.17 2 = sK1 | spl2_415),
% 162.73/30.17 inference(forward_subsumption_resolution,[],[f265816,f5993])).
% 162.73/30.17 tff(f265827,plain,(
% 162.73/30.17 $false | spl2_415),
% 162.73/30.17 inference(forward_subsumption_resolution,[],[f265824,f28])).
% 162.73/30.17 tff(f265828,plain,(
% 162.73/30.17 spl2_415),
% 162.73/30.17 inference(avatar_contradiction_clause,[],[f265827])).
% 162.73/30.17 tff(f267046,plain,(
% 162.73/30.17 sK1 = $sum($uminus(1),2) | ~spl2_416),
% 162.73/30.17 inference(superposition,[],[f227,f265751])).
% 162.73/30.17 tff(f267287,plain,(
% 162.73/30.17 1 = sK1 | ~spl2_416),
% 162.73/30.17 inference(evaluation,[],[f267046])).
% 162.73/30.17 tff(f267346,plain,(
% 162.73/30.17 $false | (spl2_182 | ~spl2_416)),
% 162.73/30.17 inference(forward_subsumption_resolution,[],[f267287,f133610])).
% 162.73/30.17 tff(f267347,plain,(
% 162.73/30.17 spl2_182 | ~spl2_416),
% 162.73/30.17 inference(avatar_contradiction_clause,[],[f267346])).
% 162.73/30.17 tff(f288470,definition,(
% 162.73/30.17 spl2_783 <=> $less(sK1,1)),
% 162.73/30.17 introduced(definition,[new_symbols(definition,[spl2_783])],[avatar_definition])).
% 162.73/30.17 tff(f288471,plain,(
% 162.73/30.17 ~$less(sK1,1) | spl2_783),
% 162.73/30.17 inference(avatar_component_clause,[],[f288470])).
% 162.73/30.17 tff(f288472,plain,(
% 162.73/30.17 $less(sK1,1) | ~spl2_783),
% 162.73/30.17 inference(avatar_component_clause,[],[f288470])).
% 162.73/30.17 tff(f403342,plain,(
% 162.73/30.17 ( ! [X0 : $int] : (~$less(X0,sK1) | $less(X0,1)) ) | ~spl2_783),
% 162.73/30.17 inference(resolution,[],[f288472,f10])).
% 162.73/30.17 tff(f506646,plain,(
% 162.73/30.17 7 = sK0 | $less(7,5) | $less($sum(sK0,$uminus(sK0)),$product(2,sK1))),
% 162.73/30.17 inference(resolution,[],[f1889,f5939])).
% 162.73/30.17 tff(f506942,plain,(
% 162.73/30.17 7 = sK0 | $less($sum(sK0,$uminus(sK0)),$product(2,sK1))),
% 162.73/30.17 inference(evaluation,[],[f506646])).
% 162.73/30.17 tff(f506962,plain,(
% 162.73/30.17 $less(0,$product(2,sK1)) | 7 = sK0),
% 162.73/30.17 inference(forward_demodulation,[],[f506942,f8])).
% 162.73/30.17 tff(f538416,plain,(
% 162.73/30.17 spl2_11 | spl2_301),
% 162.73/30.17 inference(avatar_split_clause,[],[f506962,f197772,f1918])).
% 162.73/30.17 tff(f656046,plain,(
% 162.73/30.17 ( ! [X0 : $int] : ($less($sum(7,$sum(X0,$uminus($sum(5,X0)))),0)) ) | ~spl2_11),
% 162.73/30.17 inference(superposition,[],[f412,f1920])).
% 162.73/30.17 tff(f656968,plain,(
% 162.73/30.17 $less($sum(7,$uminus(5)),0) | ~spl2_11),
% 162.73/30.17 inference(forward_demodulation,[],[f656046,f261])).
% 162.73/30.17 tff(f656969,plain,(
% 162.73/30.17 $false | ~spl2_11),
% 162.73/30.17 inference(evaluation,[],[f656968])).
% 162.73/30.17 tff(f656970,plain,(
% 162.73/30.17 ~spl2_11),
% 162.73/30.17 inference(avatar_contradiction_clause,[],[f656969])).
% 162.73/30.17 tff(f928576,plain,(
% 162.73/30.17 $less($product(2,sK1),1) | (~spl2_389 | ~spl2_783)),
% 162.73/30.17 inference(resolution,[],[f403342,f264875])).
% 162.73/30.17 tff(f928685,plain,(
% 162.73/30.17 spl2_329 | ~spl2_389 | ~spl2_783),
% 162.73/30.17 inference(avatar_split_clause,[],[f928576,f288470,f264242,f201667])).
% 162.73/30.17 tff(f928703,plain,(
% 162.73/30.17 ~$less(0,$product(2,sK1)) | ~spl2_329),
% 162.73/30.17 inference(resolution,[],[f201668,f246])).
% 162.73/30.17 tff(f928724,plain,(
% 162.73/30.17 $false | (~spl2_301 | ~spl2_329)),
% 162.73/30.17 inference(forward_subsumption_resolution,[],[f928703,f197774])).
% 162.73/30.17 tff(f928725,plain,(
% 162.73/30.17 ~spl2_301 | ~spl2_329),
% 162.73/30.17 inference(avatar_contradiction_clause,[],[f928724])).
% 162.73/30.17 tff(f931400,plain,(
% 162.73/30.17 $less(0,sK1) | spl2_783),
% 162.73/30.17 inference(resolution,[],[f288471,f235])).
% 162.73/30.17 tff(f931411,plain,(
% 162.73/30.17 $false | (spl2_399 | spl2_783)),
% 162.73/30.17 inference(forward_subsumption_resolution,[],[f931400,f264326])).
% 162.73/30.17 tff(f931412,plain,(
% 162.73/30.17 spl2_399 | spl2_783),
% 162.73/30.17 inference(avatar_contradiction_clause,[],[f931411])).
% 162.73/30.17 cnf(s350, plain, ~spl2_182, inference(sat_conversion,[],[f171062])).
% 162.73/30.17 cnf(s614, plain, ~spl2_81, inference(sat_conversion,[],[f264584])).
% 162.73/30.17 cnf(s641, plain, spl2_81 | spl2_389 | spl2_399, inference(sat_conversion,[],[f264938])).
% 162.73/30.17 cnf(s668, plain, ~spl2_399 | ~spl2_415 | spl2_416, inference(sat_conversion,[],[f265753])).
% 162.73/30.17 cnf(s671, plain, spl2_415, inference(sat_conversion,[],[f265828])).
% 162.73/30.17 cnf(s692, plain, spl2_182 | ~spl2_416, inference(sat_conversion,[],[f267347])).
% 162.73/30.17 cnf(s6427, plain, spl2_11 | spl2_301, inference(sat_conversion,[],[f538416])).
% 162.73/30.17 cnf(s8420, plain, ~spl2_11, inference(sat_conversion,[],[f656970])).
% 162.73/30.17 cnf(s10673, plain, spl2_329 | ~spl2_389 | ~spl2_783, inference(sat_conversion,[],[f928685])).
% 162.73/30.17 cnf(s10678, plain, ~spl2_301 | ~spl2_329, inference(sat_conversion,[],[f928725])).
% 162.73/30.17 cnf(s10709, plain, spl2_399 | spl2_783, inference(sat_conversion,[],[f931412])).
% 162.73/30.17 cnf(s10782, plain, spl2_301, inference(rat,[],[s6427,s8420])).
% 162.73/30.17 cnf(s10783, plain, ~spl2_329, inference(rat,[],[s10678,s10782])).
% 162.73/30.17 cnf(s11034, plain, ~spl2_399 | spl2_416, inference(rat,[],[s668,s671])).
% 162.73/30.17 cnf(s11077, plain, ~spl2_416, inference(rat,[],[s692,s350])).
% 162.73/30.17 cnf(s11084, plain, ~spl2_399, inference(rat,[],[s11034,s11077])).
% 162.73/30.17 cnf(s11089, plain, spl2_783, inference(rat,[],[s10709,s11084])).
% 162.73/30.17 cnf(s11091, plain, spl2_389, inference(rat,[],[s641,s614,s11084])).
% 162.73/30.17 cnf(s11092, plain, $false, inference(rat,[],[s10673,s10783,s11089,s11091])).
% 162.73/30.17 tff(f931420,plain,(
% 162.73/30.17 $false),
% 162.73/30.17 inference(avatar_sat_refutation,[],[s11092])).
% 162.73/30.17 % SZS output end Proof for theBenchmark
% 162.73/30.17 % (3973549)------------------------------
% 162.73/30.17 % (3973549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.73/30.17 % (3973549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.73/30.17 % (3973549)CaDiCaL version: 2.1.3
% 162.73/30.17 % (3973549)Termination reason: Refutation
% 162.73/30.17 % (3973549)Time elapsed: 29.686 s
% 162.73/30.17 % (3973549)Peak memory usage: 275 MB
% 162.73/30.17 % (3973549)Instructions burned: 54936 (million)
% 162.73/30.17 % (3973543)Success in time 29.938 s
% 162.73/30.17 % Vampire exiting
%------------------------------------------------------------------------------