%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW640_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n020.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 01:40:34 PM UTC 2026 % Result : Timeout 300.08s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW640_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n020.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 14:24:35 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.70/0.87 % (199528)Will run a generic schedule for satisfiability detection. % 3.70/0.87 % (199537)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2734894089:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.70/0.87 % (199534)% WARNING: option uhcvi not known. % 3.70/0.87 % (199536)dis+10_1_sil=32000:sp=arity:random_seed=2588574014:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.70/0.87 % (199533)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4008390836_2999 on theBenchmark for (2999ds/0Mi) % 3.70/0.87 % (199534)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3339690508:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.70/0.87 % (199535)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=419708450:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.70/0.87 % (199538)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=294688230:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.70/0.87 % (199539)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2627033791:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.70/0.87 % (199533)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.70/0.87 % (199533)Terminated due to inappropriate strategy. % 3.70/0.87 % (199533)------------------------------ % 3.70/0.87 % (199533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.70/0.87 % (199533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.70/0.87 % (199533)CaDiCaL version: 2.1.3 % 3.70/0.87 % (199533)Termination reason: Inappropriate % 3.70/0.87 % (199533)Time elapsed: 0.005 s % 3.70/0.87 % (199533)Peak memory usage: 11 MB % 3.70/0.87 % (199533)Instructions burned: 9 (million) % 3.70/0.87 % (199533)------------------------------ % 3.70/0.87 % (199533)------------------------------ % 3.70/0.87 % (199547)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2829928915:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.70/0.87 % (199547)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.70/0.87 % (199547)Terminated due to inappropriate strategy. % 3.70/0.87 % (199547)------------------------------ % 3.70/0.87 % (199547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.70/0.87 % (199547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.70/0.87 % (199547)CaDiCaL version: 2.1.3 % 3.70/0.87 % (199547)Termination reason: Inappropriate % 3.70/0.87 % (199547)Time elapsed: 0.005 s % 3.70/0.87 % (199547)Peak memory usage: 10 MB % 3.70/0.87 % (199547)Instructions burned: 8 (million) % 3.70/0.87 % (199547)------------------------------ % 3.70/0.87 % (199547)------------------------------ % 3.70/0.87 % (199537)Instruction limit reached! % 3.70/0.87 % (199537)------------------------------ % 3.70/0.87 % (199537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.70/0.87 % (199537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.70/0.87 % (199537)CaDiCaL version: 2.1.3 % 3.70/0.87 % (199537)Termination reason: Instruction limit % 3.70/0.87 % (199537)Termination phase: Saturation % 3.70/0.87 % (199537)Time elapsed: 0.041 s % 3.70/0.87 % (199537)Peak memory usage: 13 MB % 3.70/0.87 % (199537)Instructions burned: 117 (million) % 3.70/0.87 % (199550)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=1470781351:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.70/0.87 % (199549)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3664818365:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.70/0.87 % (199536)Instruction limit reached! % 3.70/0.87 % (199536)------------------------------ % 3.70/0.87 % (199536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.70/0.87 % (199536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.70/0.87 % (199536)CaDiCaL version: 2.1.3 % 3.70/0.87 % (199536)Termination reason: Instruction limit % 3.70/0.87 % (199536)Termination phase: Saturation % 3.70/0.87 % (199536)Time elapsed: 0.063 s % 3.70/0.87 % (199536)Peak memory usage: 13 MB % 3.70/0.87 % (199536)Instructions burned: 104 (million) % 3.70/0.87 % (199538)Instruction limit reached! % 3.70/0.87 % (199538)------------------------------ % 3.70/0.87 % (199538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.08/1.44 % (199538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.08/1.44 % (199538)CaDiCaL version: 2.1.3 % 8.08/1.44 % (199538)Termination reason: Instruction limit % 8.08/1.44 % (199538)Termination phase: Saturation % 8.08/1.44 % (199538)Time elapsed: 0.079 s % 8.08/1.44 % (199538)Peak memory usage: 13 MB % 8.08/1.44 % (199538)Instructions burned: 133 (million) % 8.08/1.44 % (199553)ott-21_1_sil=16000:fs=off:random_seed=78625391:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 8.08/1.44 % (199539)Instruction limit reached! % 8.08/1.44 % (199539)------------------------------ % 8.08/1.44 % (199539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.08/1.44 % (199539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.08/1.44 % (199539)CaDiCaL version: 2.1.3 % 8.08/1.44 % (199539)Termination reason: Instruction limit % 8.08/1.44 % (199539)Termination phase: Saturation % 8.08/1.44 % (199539)Time elapsed: 0.085 s % 8.08/1.44 % (199539)Peak memory usage: 13 MB % 8.08/1.44 % (199539)Instructions burned: 159 (million) % 8.08/1.44 % (199554)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1126079334:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.08/1.44 % (199556)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=895040218:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.08/1.44 % (199556)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.08/1.44 % (199556)Terminated due to inappropriate strategy. % 8.08/1.44 % (199556)------------------------------ % 8.08/1.44 % (199556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.08/1.44 % (199556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.08/1.44 % (199556)CaDiCaL version: 2.1.3 % 8.08/1.44 % (199556)Termination reason: Inappropriate % 8.08/1.44 % (199556)Time elapsed: 0.004 s % 8.08/1.44 % (199556)Peak memory usage: 11 MB % 8.08/1.44 % (199556)Instructions burned: 8 (million) % 8.08/1.44 % (199556)------------------------------ % 8.08/1.44 % (199556)------------------------------ % 8.08/1.44 % (199559)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3248078245:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 8.08/1.44 % (199549)Instruction limit reached! % 8.08/1.44 % (199549)------------------------------ % 8.08/1.44 % (199549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.08/1.44 % (199549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.08/1.44 % (199549)CaDiCaL version: 2.1.3 % 8.08/1.44 % (199549)Termination reason: Instruction limit % 8.08/1.44 % (199549)Termination phase: Saturation % 8.08/1.44 % (199549)Time elapsed: 0.082 s % 8.08/1.44 % (199549)Peak memory usage: 13 MB % 8.08/1.44 % (199549)Instructions burned: 132 (million) % 8.08/1.44 % (199561)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=854270239:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 8.08/1.44 % (199561)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.08/1.44 % (199561)Terminated due to inappropriate strategy. % 8.08/1.44 % (199561)------------------------------ % 8.08/1.44 % (199561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.08/1.44 % (199561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.08/1.44 % (199561)CaDiCaL version: 2.1.3 % 8.08/1.44 % (199561)Termination reason: Inappropriate % 8.08/1.44 % (199561)Time elapsed: 0.004 s % 8.08/1.44 % (199561)Peak memory usage: 10 MB % 8.08/1.44 % (199561)Instructions burned: 8 (million) % 8.08/1.44 % (199561)------------------------------ % 8.08/1.44 % (199561)------------------------------ % 8.08/1.44 % (199563)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=2295058110: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) % 8.08/1.44 % (199553)Instruction limit reached! % 8.08/1.44 % (199553)------------------------------ % 8.08/1.44 % (199553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.08/1.44 % (199553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.08/1.44 % (199553)CaDiCaL version: 2.1.3 % 8.08/1.44 % (199553)Termination reason: Instruction limit % 8.08/1.44 % (199553)Termination phase: Saturation % 8.08/1.44 % (199553)Time elapsed: 0.104 s % 8.08/1.44 % (199553)Peak memory usage: 13 MB % 8.08/1.44 % (199553)Instructions burned: 182 (million) % 20.65/3.20 % (199565)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3345585582:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.65/3.20 % (199550)Instruction limit reached! % 20.65/3.20 % (199550)------------------------------ % 20.65/3.20 % (199550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.20 % (199550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.20 % (199550)CaDiCaL version: 2.1.3 % 20.65/3.20 % (199550)Termination reason: Instruction limit % 20.65/3.20 % (199550)Termination phase: Saturation % 20.65/3.20 % (199550)Time elapsed: 0.197 s % 20.65/3.20 % (199550)Peak memory usage: 16 MB % 20.65/3.20 % (199550)Instructions burned: 686 (million) % 20.65/3.20 % (199567)fmb+10_1_sil=64000:random_seed=3243358977:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 20.65/3.20 % (199567)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.65/3.20 % (199567)Terminated due to inappropriate strategy. % 20.65/3.20 % (199567)------------------------------ % 20.65/3.20 % (199567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.20 % (199567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.20 % (199567)CaDiCaL version: 2.1.3 % 20.65/3.20 % (199567)Termination reason: Inappropriate % 20.65/3.20 % (199567)Time elapsed: 0.002 s % 20.65/3.20 % (199567)Peak memory usage: 10 MB % 20.65/3.20 % (199567)Instructions burned: 9 (million) % 20.65/3.20 % (199567)------------------------------ % 20.65/3.20 % (199567)------------------------------ % 20.65/3.20 % (199569)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2790028915:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 20.65/3.20 % (199569)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.65/3.20 % (199569)Terminated due to inappropriate strategy. % 20.65/3.20 % (199569)------------------------------ % 20.65/3.20 % (199569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.20 % (199569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.20 % (199569)CaDiCaL version: 2.1.3 % 20.65/3.20 % (199569)Termination reason: Inappropriate % 20.65/3.20 % (199569)Time elapsed: 0.002 s % 20.65/3.20 % (199569)Peak memory usage: 10 MB % 20.65/3.20 % (199569)Instructions burned: 9 (million) % 20.65/3.20 % (199569)------------------------------ % 20.65/3.20 % (199569)------------------------------ % 20.65/3.20 % (199571)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=297201568:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.65/3.20 % (199571)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.65/3.20 % (199571)Terminated due to inappropriate strategy. % 20.65/3.20 % (199571)------------------------------ % 20.65/3.20 % (199571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.20 % (199571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.20 % (199571)CaDiCaL version: 2.1.3 % 20.65/3.20 % (199571)Termination reason: Inappropriate % 20.65/3.20 % (199571)Time elapsed: 0.002 s % 20.65/3.20 % (199571)Peak memory usage: 10 MB % 20.65/3.20 % (199571)Instructions burned: 9 (million) % 20.65/3.20 % (199571)------------------------------ % 20.65/3.20 % (199571)------------------------------ % 20.65/3.20 % (199573)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=720280141:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.65/3.20 % (199554)Instruction limit reached! % 20.65/3.20 % (199554)------------------------------ % 20.65/3.20 % (199554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.20 % (199554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.20 % (199554)CaDiCaL version: 2.1.3 % 20.65/3.20 % (199554)Termination reason: Instruction limit % 20.65/3.20 % (199554)Termination phase: Saturation % 20.65/3.20 % (199554)Time elapsed: 0.310 s % 20.65/3.20 % (199554)Peak memory usage: 14 MB % 20.65/3.20 % (199554)Instructions burned: 478 (million) % 20.65/3.20 % (199575)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1560368322:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 20.65/3.20 % (199563)Instruction limit reached! % 20.65/3.20 % (199563)------------------------------ % 20.65/3.20 % (199563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.20 % (199563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.01/4.08 % (199563)CaDiCaL version: 2.1.3 % 27.01/4.08 % (199563)Termination reason: Instruction limit % 27.01/4.08 % (199563)Termination phase: Saturation % 27.01/4.08 % (199563)Time elapsed: 0.434 s % 27.01/4.08 % (199563)Peak memory usage: 19 MB % 27.01/4.08 % (199563)Instructions burned: 694 (million) % 27.01/4.08 % (199577)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3216921910:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 27.01/4.08 % (199577)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.01/4.08 % (199577)Terminated due to inappropriate strategy. % 27.01/4.08 % (199577)------------------------------ % 27.01/4.08 % (199577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.01/4.08 % (199577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.01/4.08 % (199577)CaDiCaL version: 2.1.3 % 27.01/4.08 % (199577)Termination reason: Inappropriate % 27.01/4.08 % (199577)Time elapsed: 0.005 s % 27.01/4.08 % (199577)Peak memory usage: 11 MB % 27.01/4.08 % (199577)Instructions burned: 9 (million) % 27.01/4.08 % (199577)------------------------------ % 27.01/4.08 % (199577)------------------------------ % 27.01/4.08 % (199579)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1440471888:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 27.01/4.08 % (199579)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.01/4.08 % (199579)Terminated due to inappropriate strategy. % 27.01/4.08 % (199579)------------------------------ % 27.01/4.08 % (199579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.01/4.08 % (199579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.01/4.08 % (199579)CaDiCaL version: 2.1.3 % 27.01/4.08 % (199579)Termination reason: Inappropriate % 27.01/4.08 % (199579)Time elapsed: 0.005 s % 27.01/4.08 % (199579)Peak memory usage: 11 MB % 27.01/4.08 % (199579)Instructions burned: 9 (million) % 27.01/4.08 % (199579)------------------------------ % 27.01/4.08 % (199579)------------------------------ % 27.01/4.08 % (199581)ott-2_1_sil=16000:newcnf=on:random_seed=325940558:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 27.01/4.08 % (199565)Instruction limit reached! % 27.01/4.08 % (199565)------------------------------ % 27.01/4.08 % (199565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.01/4.08 % (199565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.01/4.08 % (199565)CaDiCaL version: 2.1.3 % 27.01/4.08 % (199565)Termination reason: Instruction limit % 27.01/4.08 % (199565)Termination phase: Saturation % 27.01/4.08 % (199565)Time elapsed: 0.490 s % 27.01/4.08 % (199565)Peak memory usage: 19 MB % 27.01/4.08 % (199565)Instructions burned: 879 (million) % 27.01/4.08 % (199583)ott+10_1_sil=32000:tgt=ground:random_seed=89885947:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 27.01/4.08 % (199559)Instruction limit reached! % 27.01/4.08 % (199559)------------------------------ % 27.01/4.08 % (199559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.01/4.08 % (199559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.01/4.08 % (199559)CaDiCaL version: 2.1.3 % 27.01/4.08 % (199559)Termination reason: Instruction limit % 27.01/4.08 % (199559)Termination phase: Saturation % 27.01/4.08 % (199559)Time elapsed: 0.710 s % 27.01/4.08 % (199559)Peak memory usage: 22 MB % 27.01/4.08 % (199559)Instructions burned: 1180 (million) % 27.01/4.08 % (199585)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2209718447:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 27.01/4.08 % (199585)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.01/4.08 % (199585)Terminated due to inappropriate strategy. % 27.01/4.08 % (199585)------------------------------ % 27.01/4.08 % (199585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.01/4.08 % (199585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.01/4.08 % (199585)CaDiCaL version: 2.1.3 % 27.01/4.08 % (199585)Termination reason: Inappropriate % 27.01/4.08 % (199585)Time elapsed: 0.005 s % 27.01/4.08 % (199585)Peak memory usage: 11 MB % 27.01/4.08 % (199585)Instructions burned: 9 (million) % 27.01/4.08 % (199585)------------------------------ % 27.01/4.08 % (199585)------------------------------ % 27.01/4.08 % (199587)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1593389622:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 27.01/4.08 % (199581)Instruction limit reached! % 97.07/13.92 % (199581)------------------------------ % 97.07/13.92 % (199581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.07/13.92 % (199581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.07/13.92 % (199581)CaDiCaL version: 2.1.3 % 97.07/13.92 % (199581)Termination reason: Instruction limit % 97.07/13.92 % (199581)Termination phase: Saturation % 97.07/13.92 % (199581)Time elapsed: 0.501 s % 97.07/13.92 % (199581)Peak memory usage: 16 MB % 97.07/13.92 % (199581)Instructions burned: 870 (million) % 97.07/13.92 % (199589)dis+21_1_sil=32000:sas=cadical:random_seed=3960015261:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 97.07/13.92 % (199575)Instruction limit reached! % 97.07/13.92 % (199575)------------------------------ % 97.07/13.92 % (199575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.07/13.92 % (199575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.07/13.92 % (199575)CaDiCaL version: 2.1.3 % 97.07/13.92 % (199575)Termination reason: Instruction limit % 97.07/13.92 % (199575)Termination phase: Saturation % 97.07/13.92 % (199575)Time elapsed: 0.788 s % 97.07/13.92 % (199575)Peak memory usage: 27 MB % 97.07/13.92 % (199575)Instructions burned: 1472 (million) % 97.07/13.92 % (199591)ott+11_1_sil=16000:gs=on:random_seed=2794670992:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 97.07/13.92 % (199573)Instruction limit reached! % 97.07/13.92 % (199573)------------------------------ % 97.07/13.92 % (199573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.07/13.92 % (199573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.07/13.92 % (199573)CaDiCaL version: 2.1.3 % 97.07/13.92 % (199573)Termination reason: Instruction limit % 97.07/13.92 % (199573)Termination phase: Saturation % 97.07/13.92 % (199573)Time elapsed: 1.491 s % 97.07/13.92 % (199573)Peak memory usage: 38 MB % 97.07/13.92 % (199573)Instructions burned: 5133 (million) % 97.07/13.92 % (199593)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=545351354:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 97.07/13.92 % (199593)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 97.07/13.92 % (199593)Terminated due to inappropriate strategy. % 97.07/13.92 % (199593)------------------------------ % 97.07/13.92 % (199593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.07/13.92 % (199593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.07/13.92 % (199593)CaDiCaL version: 2.1.3 % 97.07/13.92 % (199593)Termination reason: Inappropriate % 97.07/13.92 % (199593)Time elapsed: 0.003 s % 97.07/13.92 % (199593)Peak memory usage: 11 MB % 97.07/13.92 % (199593)Instructions burned: 9 (million) % 97.07/13.92 % (199593)------------------------------ % 97.07/13.92 % (199593)------------------------------ % 97.07/13.92 % (199595)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1242079491:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 97.07/13.92 % (199591)Instruction limit reached! % 97.07/13.92 % (199591)------------------------------ % 97.07/13.92 % (199591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.07/13.92 % (199591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.07/13.92 % (199591)CaDiCaL version: 2.1.3 % 97.07/13.92 % (199591)Termination reason: Instruction limit % 97.07/13.92 % (199591)Termination phase: Saturation % 97.07/13.92 % (199591)Time elapsed: 1.253 s % 97.07/13.92 % (199591)Peak memory usage: 24 MB % 97.07/13.92 % (199591)Instructions burned: 2251 (million) % 97.07/13.92 % (199597)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=235382919:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 97.07/13.92 % (199587)Instruction limit reached! % 97.07/13.92 % (199587)------------------------------ % 97.07/13.92 % (199587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.07/13.92 % (199587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.07/13.92 % (199587)CaDiCaL version: 2.1.3 % 97.07/13.92 % (199587)Termination reason: Instruction limit % 97.07/13.92 % (199587)Termination phase: Saturation % 97.07/13.92 % (199587)Time elapsed: 1.954 s % 97.07/13.92 % (199587)Peak memory usage: 32 MB % 97.07/13.92 % (199587)Instructions burned: 3513 (million) % 97.07/13.92 % (199599)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2740391240:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 97.07/13.92 % (199595)Instruction limit reached! % 117.33/18.09 % (199595)------------------------------ % 117.33/18.09 % (199595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.33/18.09 % (199595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/18.09 % (199595)CaDiCaL version: 2.1.3 % 117.33/18.09 % (199595)Termination reason: Instruction limit % 117.33/18.09 % (199595)Termination phase: Saturation % 117.33/18.09 % (199595)Time elapsed: 1.128 s % 117.33/18.09 % (199595)Peak memory usage: 33 MB % 117.33/18.09 % (199595)Instructions burned: 4594 (million) % 117.33/18.09 % (199601)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1957567676:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi) % 117.33/18.09 % (199601)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.33/18.09 % (199601)Terminated due to inappropriate strategy. % 117.33/18.09 % (199601)------------------------------ % 117.33/18.09 % (199601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.33/18.09 % (199601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/18.09 % (199601)CaDiCaL version: 2.1.3 % 117.33/18.09 % (199601)Termination reason: Inappropriate % 117.33/18.09 % (199601)Time elapsed: 0.003 s % 117.33/18.09 % (199601)Peak memory usage: 11 MB % 117.33/18.09 % (199601)Instructions burned: 9 (million) % 117.33/18.09 % (199601)------------------------------ % 117.33/18.09 % (199601)------------------------------ % 117.33/18.09 % (199603)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2075590717:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi) % 117.33/18.09 % (199603)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.33/18.09 % (199603)Terminated due to inappropriate strategy. % 117.33/18.09 % (199603)------------------------------ % 117.33/18.09 % (199603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.33/18.09 % (199603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/18.09 % (199603)CaDiCaL version: 2.1.3 % 117.33/18.09 % (199603)Termination reason: Inappropriate % 117.33/18.09 % (199603)Time elapsed: 0.002 s % 117.33/18.09 % (199603)Peak memory usage: 11 MB % 117.33/18.09 % (199603)Instructions burned: 9 (million) % 117.33/18.09 % (199603)------------------------------ % 117.33/18.09 % (199603)------------------------------ % 117.33/18.09 % (199605)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3980731162:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 117.33/18.09 % (199605)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.33/18.09 % (199605)Terminated due to inappropriate strategy. % 117.33/18.09 % (199605)------------------------------ % 117.33/18.09 % (199605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.33/18.09 % (199605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/18.09 % (199605)CaDiCaL version: 2.1.3 % 117.33/18.09 % (199605)Termination reason: Inappropriate % 117.33/18.09 % (199605)Time elapsed: 0.002 s % 117.33/18.09 % (199605)Peak memory usage: 11 MB % 117.33/18.09 % (199605)Instructions burned: 9 (million) % 117.33/18.09 % (199605)------------------------------ % 117.33/18.09 % (199605)------------------------------ % 117.33/18.09 % (199607)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3115189828:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 117.33/18.09 % (199589)Instruction limit reached! % 117.33/18.09 % (199589)------------------------------ % 117.33/18.09 % (199589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.33/18.09 % (199589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/18.09 % (199589)CaDiCaL version: 2.1.3 % 117.33/18.09 % (199589)Termination reason: Instruction limit % 117.33/18.09 % (199589)Termination phase: Saturation % 117.33/18.09 % (199589)Time elapsed: 2.105 s % 117.33/18.09 % (199589)Peak memory usage: 29 MB % 117.33/18.09 % (199589)Instructions burned: 3774 (million) % 117.33/18.09 % (199609)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2501781199:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 117.33/18.09 % (199583)Instruction limit reached! % 117.33/18.09 % (199583)------------------------------ % 117.33/18.09 % (199583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.33/18.09 % (199583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/18.09 % (199583)CaDiCaL version: 2.1.3 % 117.33/18.09 % (199583)Termination reason: Instruction limit % 117.33/18.09 % (199583)Termination phase: Saturation % 117.33/18.09 % (199583)Time elapsed: 3.104 s % 128.23/18.37 % (199583)Peak memory usage: 38 MB % 128.23/18.37 % (199583)Instructions burned: 5115 (million) % 128.23/18.37 % (199611)dis+10_16:1_sil=16000:random_seed=181531089:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 128.23/18.37 % (199599)Instruction limit reached! % 128.23/18.37 % (199599)------------------------------ % 128.23/18.37 % (199599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.37 % (199599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.37 % (199599)CaDiCaL version: 2.1.3 % 128.23/18.37 % (199599)Termination reason: Instruction limit % 128.23/18.37 % (199599)Termination phase: Saturation % 128.23/18.37 % (199599)Time elapsed: 2.841 s % 128.23/18.37 % (199599)Peak memory usage: 55 MB % 128.23/18.37 % (199599)Instructions burned: 5212 (million) % 128.23/18.37 % (199613)ott-3_8_sil=64000:random_seed=473113614:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi) % 128.23/18.37 % (199609)Instruction limit reached! % 128.23/18.37 % (199609)------------------------------ % 128.23/18.37 % (199609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.37 % (199609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.37 % (199609)CaDiCaL version: 2.1.3 % 128.23/18.37 % (199609)Termination reason: Instruction limit % 128.23/18.37 % (199609)Termination phase: Saturation % 128.23/18.37 % (199609)Time elapsed: 5.056 s % 128.23/18.37 % (199609)Peak memory usage: 64 MB % 128.23/18.37 % (199609)Instructions burned: 8174 (million) % 128.23/18.37 % (199615)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=781576015:fmbsr=2:i=32576_2915 on theBenchmark for (2915ds/32576Mi) % 128.23/18.37 % (199615)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.23/18.37 % (199615)Terminated due to inappropriate strategy. % 128.23/18.37 % (199615)------------------------------ % 128.23/18.37 % (199615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.37 % (199615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.37 % (199615)CaDiCaL version: 2.1.3 % 128.23/18.37 % (199615)Termination reason: Inappropriate % 128.23/18.37 % (199615)Time elapsed: 0.005 s % 128.23/18.37 % (199615)Peak memory usage: 11 MB % 128.23/18.37 % (199615)Instructions burned: 10 (million) % 128.23/18.37 % (199615)------------------------------ % 128.23/18.37 % (199615)------------------------------ % 128.23/18.37 % (199617)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3449820444:i=11404_2915 on theBenchmark for (2915ds/11404Mi) % 128.23/18.37 % (199607)Instruction limit reached! % 128.23/18.37 % (199607)------------------------------ % 128.23/18.37 % (199607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.37 % (199607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.37 % (199607)CaDiCaL version: 2.1.3 % 128.23/18.37 % (199607)Termination reason: Instruction limit % 128.23/18.37 % (199607)Termination phase: Saturation % 128.23/18.37 % (199607)Time elapsed: 5.734 s % 128.23/18.37 % (199607)Peak memory usage: 153 MB % 128.23/18.37 % (199607)Instructions burned: 22567 (million) % 128.23/18.37 % (199619)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2187931160:i=14134_2912 on theBenchmark for (2912ds/14134Mi) % 128.23/18.37 % (199611)Instruction limit reached! % 128.23/18.37 % (199611)------------------------------ % 128.23/18.37 % (199611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.37 % (199611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.37 % (199611)CaDiCaL version: 2.1.3 % 128.23/18.37 % (199611)Termination reason: Instruction limit % 128.23/18.37 % (199611)Termination phase: Saturation % 128.23/18.37 % (199611)Time elapsed: 4.931 s % 128.23/18.37 % (199611)Peak memory usage: 52 MB % 128.23/18.37 % (199611)Instructions burned: 9156 (million) % 128.23/18.37 % (199621)dis+33_16_sil=32000:sac=on:random_seed=3280191885:i=15851:nm=0_2911 on theBenchmark for (2911ds/15851Mi) % 128.23/18.37 % (199619)Instruction limit reached! % 128.23/18.37 % (199619)------------------------------ % 128.23/18.37 % (199619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.37 % (199619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.37 % (199619)CaDiCaL version: 2.1.3 % 128.23/18.37 % (199619)Termination reason: Instruction limit % 128.23/18.37 % (199619)Termination phase: Saturation % 128.23/18.37 % (199619)Time elapsed: 4.894 s % 128.23/18.37 % (199619)Peak memory usage: 96 MB % 128.23/18.37 % (199619)Instructions burned: 14137 (million) % 128.23/18.37 % (199739)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2577618275:avsq=on:i=17627:add=on:amm=off_2863 on theBenchmark for (2863ds/17627Mi) % 136.04/19.46 % (199617)Instruction limit reached! % 136.04/19.46 % (199617)------------------------------ % 136.04/19.46 % (199617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.04/19.46 % (199617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.04/19.46 % (199617)CaDiCaL version: 2.1.3 % 136.04/19.46 % (199617)Termination reason: Instruction limit % 136.04/19.46 % (199617)Termination phase: Saturation % 136.04/19.46 % (199617)Time elapsed: 7.731 s % 136.04/19.46 % (199617)Peak memory usage: 58 MB % 136.04/19.46 % (199617)Instructions burned: 11404 (million) % 136.04/19.46 % (200040)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1424093386:s2a=on:i=53295_2837 on theBenchmark for (2837ds/53295Mi) % 136.04/19.46 % (199597)Instruction limit reached! % 136.04/19.46 % (199597)------------------------------ % 136.04/19.46 % (199597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.04/19.46 % (199597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.04/19.46 % (199597)CaDiCaL version: 2.1.3 % 136.04/19.46 % (199597)Termination reason: Instruction limit % 136.04/19.46 % (199597)Termination phase: Saturation % 136.04/19.46 % (199597)Time elapsed: 14.729 s % 136.04/19.46 % (199597)Peak memory usage: 192 MB % 136.04/19.46 % (199597)Instructions burned: 29342 (million) % 136.04/19.46 % (200046)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=993019328:i=26857:ins=20_2826 on theBenchmark for (2826ds/26857Mi) % 136.04/19.46 % (200046)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.04/19.46 % (200046)Terminated due to inappropriate strategy. % 136.04/19.46 % (200046)------------------------------ % 136.04/19.46 % (200046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.04/19.46 % (200046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.04/19.46 % (200046)CaDiCaL version: 2.1.3 % 136.04/19.46 % (200046)Termination reason: Inappropriate % 136.04/19.46 % (200046)Time elapsed: 0.005 s % 136.04/19.46 % (200046)Peak memory usage: 10 MB % 136.04/19.46 % (200046)Instructions burned: 9 (million) % 136.04/19.46 % (200046)------------------------------ % 136.04/19.46 % (200046)------------------------------ % 136.04/19.46 % (200048)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3247621346:i=28120:bs=on:fsr=off_2826 on theBenchmark for (2826ds/28120Mi) % 136.04/19.46 % (199621)Instruction limit reached! % 136.04/19.46 % (199621)------------------------------ % 136.04/19.46 % (199621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.04/19.46 % (199621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.04/19.46 % (199621)CaDiCaL version: 2.1.3 % 136.04/19.46 % (199621)Termination reason: Instruction limit % 136.04/19.46 % (199621)Termination phase: Saturation % 136.04/19.46 % (199621)Time elapsed: 8.963 s % 136.04/19.46 % (199621)Peak memory usage: 105 MB % 136.04/19.46 % (199621)Instructions burned: 15852 (million) % 136.04/19.46 % (200050)fmb+10_1_sil=256000:fmbss=7:random_seed=2077527682:fmbsr=1.6:i=182295_2821 on theBenchmark for (2821ds/182295Mi) % 136.04/19.46 % (200050)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.04/19.46 % (200050)Terminated due to inappropriate strategy. % 136.04/19.46 % (200050)------------------------------ % 136.04/19.46 % (200050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.04/19.46 % (200050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.04/19.46 % (200050)CaDiCaL version: 2.1.3 % 136.04/19.46 % (200050)Termination reason: Inappropriate % 136.04/19.46 % (200050)Time elapsed: 0.005 s % 136.04/19.46 % (200050)Peak memory usage: 10 MB % 136.04/19.46 % (200050)Instructions burned: 9 (million) % 136.04/19.46 % (200050)------------------------------ % 136.04/19.46 % (200050)------------------------------ % 136.04/19.46 % (200052)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=705180563:i=44625:gsp=on_2821 on theBenchmark for (2821ds/44625Mi) % 136.04/19.46 % (200052)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.04/19.46 % (200052)Terminated due to inappropriate strategy. % 136.04/19.46 % (200052)------------------------------ % 136.04/19.46 % (200052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.04/19.46 % (200052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.04/19.46 % (200052)CaDiCaL version: 2.1.3 % 136.04/19.46 % (200052)Termination reason: Inappropriate % 136.04/19.46 % (200052)Time elapsed: 0.005 s % 149.60/21.34 % (200052)Peak memory usage: 11 MB % 149.60/21.34 % (200052)Instructions burned: 9 (million) % 149.60/21.34 % (200052)------------------------------ % 149.60/21.34 % (200052)------------------------------ % 149.60/21.34 % (200054)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3257138554:i=160505_2821 on theBenchmark for (2821ds/160505Mi) % 149.60/21.34 % (200054)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.60/21.34 % (200054)Terminated due to inappropriate strategy. % 149.60/21.34 % (200054)------------------------------ % 149.60/21.34 % (200054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.60/21.34 % (200054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.60/21.34 % (200054)CaDiCaL version: 2.1.3 % 149.60/21.34 % (200054)Termination reason: Inappropriate % 149.60/21.34 % (200054)Time elapsed: 0.005 s % 149.60/21.34 % (200054)Peak memory usage: 10 MB % 149.60/21.34 % (200054)Instructions burned: 9 (million) % 149.60/21.34 % (200054)------------------------------ % 149.60/21.34 % (200054)------------------------------ % 149.60/21.34 % (200056)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3316914464:fmbsr=1.3:i=225729_2821 on theBenchmark for (2821ds/225729Mi) % 149.60/21.34 % (200056)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.60/21.34 % (200056)Terminated due to inappropriate strategy. % 149.60/21.34 % (200056)------------------------------ % 149.60/21.34 % (200056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.60/21.34 % (200056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.60/21.34 % (200056)CaDiCaL version: 2.1.3 % 149.60/21.34 % (200056)Termination reason: Inappropriate % 149.60/21.34 % (200056)Time elapsed: 0.005 s % 149.60/21.34 % (200056)Peak memory usage: 11 MB % 149.60/21.34 % (200056)Instructions burned: 9 (million) % 149.60/21.34 % (200056)------------------------------ % 149.60/21.34 % (200056)------------------------------ % 149.60/21.34 % (200058)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2622191763:fmbsr=2:i=185024:ins=7_2820 on theBenchmark for (2820ds/185024Mi) % 149.60/21.34 % (200058)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.60/21.34 % (200058)Terminated due to inappropriate strategy. % 149.60/21.34 % (200058)------------------------------ % 149.60/21.34 % (200058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.60/21.34 % (200058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.60/21.34 % (200058)CaDiCaL version: 2.1.3 % 149.60/21.34 % (200058)Termination reason: Inappropriate % 149.60/21.34 % (200058)Time elapsed: 0.005 s % 149.60/21.34 % (200058)Peak memory usage: 11 MB % 149.60/21.34 % (200058)Instructions burned: 9 (million) % 149.60/21.34 % (200058)------------------------------ % 149.60/21.34 % (200058)------------------------------ % 149.60/21.34 % (200060)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1824934435:rtra=on_2820 on theBenchmark for (2820ds/0Mi) % 149.60/21.34 % (200060)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.60/21.34 % (200060)Terminated due to inappropriate strategy. % 149.60/21.34 % (200060)------------------------------ % 149.60/21.34 % (200060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.60/21.34 % (200060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.60/21.34 % (200060)CaDiCaL version: 2.1.3 % 149.60/21.34 % (200060)Termination reason: Inappropriate % 149.60/21.34 % (200060)Time elapsed: 0.006 s % 149.60/21.34 % (200060)Peak memory usage: 11 MB % 149.60/21.34 % (200060)Instructions burned: 10 (million) % 149.60/21.34 % (200060)------------------------------ % 149.60/21.34 % (200060)------------------------------ % 149.60/21.34 % (200062)% WARNING: option uhcvi not known. % 149.60/21.34 % (200062)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1857640032:i=271062:add=off:rtra=on:rawr=on_2820 on theBenchmark for (2820ds/271062Mi) % 149.60/21.34 % (199613)Instruction limit reached! % 149.60/21.34 % (199613)------------------------------ % 149.60/21.34 % (199613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.60/21.34 % (199613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.60/21.34 % (199613)CaDiCaL version: 2.1.3 % 149.60/21.34 % (199613)Termination reason: Instruction limit % 149.60/21.34 % (199613)Termination phase: Saturation % 149.60/21.34 % (199613)Time elapsed: 12.340 s % 149.60/21.34 % (199613)Peak memory usage: 127 MB % 149.60/21.34 % (199613)Instructions burned: 20139 (million) % 149.60/21.34 % (200064)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1978557039:i=176048:add=on:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/176048Mi) % 157.44/22.41 % (199739)Instruction limit reached! % 157.44/22.41 % (199739)------------------------------ % 157.44/22.41 % (199739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.44/22.41 % (199739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/22.41 % (199739)CaDiCaL version: 2.1.3 % 157.44/22.41 % (199739)Termination reason: Instruction limit % 157.44/22.41 % (199739)Termination phase: Saturation % 157.44/22.41 % (199739)Time elapsed: 5.119 s % 157.44/22.41 % (199739)Peak memory usage: 200 MB % 157.44/22.41 % (199739)Instructions burned: 17628 (million) % 157.44/22.41 % (200066)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3547481382:i=206:fgj=on:rtra=on_2811 on theBenchmark for (2811ds/206Mi) % 157.44/22.41 % (200066)Instruction limit reached! % 157.44/22.41 % (200066)------------------------------ % 157.44/22.41 % (200066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.44/22.41 % (200066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/22.41 % (200066)CaDiCaL version: 2.1.3 % 157.44/22.41 % (200066)Termination reason: Instruction limit % 157.44/22.41 % (200066)Termination phase: Saturation % 157.44/22.41 % (200066)Time elapsed: 0.068 s % 157.44/22.41 % (200066)Peak memory usage: 13 MB % 157.44/22.41 % (200066)Instructions burned: 207 (million) % 157.44/22.41 % (200068)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1950146588:i=232:rtra=on_2810 on theBenchmark for (2810ds/232Mi) % 157.44/22.41 % (200068)Instruction limit reached! % 157.44/22.41 % (200068)------------------------------ % 157.44/22.41 % (200068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.44/22.41 % (200068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/22.41 % (200068)CaDiCaL version: 2.1.3 % 157.44/22.41 % (200068)Termination reason: Instruction limit % 157.44/22.41 % (200068)Termination phase: Saturation % 157.44/22.41 % (200068)Time elapsed: 0.082 s % 157.44/22.41 % (200068)Peak memory usage: 14 MB % 157.44/22.41 % (200068)Instructions burned: 234 (million) % 157.44/22.41 % (200070)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=785932981:i=262:rtra=on_2809 on theBenchmark for (2809ds/262Mi) % 157.44/22.41 % (200070)Instruction limit reached! % 157.44/22.41 % (200070)------------------------------ % 157.44/22.41 % (200070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.44/22.41 % (200070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/22.41 % (200070)CaDiCaL version: 2.1.3 % 157.44/22.41 % (200070)Termination reason: Instruction limit % 157.44/22.41 % (200070)Termination phase: Saturation % 157.44/22.41 % (200070)Time elapsed: 0.084 s % 157.44/22.41 % (200070)Peak memory usage: 14 MB % 157.44/22.41 % (200070)Instructions burned: 264 (million) % 157.44/22.41 % (200072)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2244490915:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2808 on theBenchmark for (2808ds/318Mi) % 157.44/22.41 % (200072)Instruction limit reached! % 157.44/22.41 % (200072)------------------------------ % 157.44/22.41 % (200072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.44/22.41 % (200072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/22.41 % (200072)CaDiCaL version: 2.1.3 % 157.44/22.41 % (200072)Termination reason: Instruction limit % 157.44/22.41 % (200072)Termination phase: Saturation % 157.44/22.41 % (200072)Time elapsed: 0.110 s % 157.44/22.41 % (200072)Peak memory usage: 15 MB % 157.44/22.41 % (200072)Instructions burned: 321 (million) % 157.44/22.41 % (200074)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2516416664:i=1428:nm=2:rtra=on_2807 on theBenchmark for (2807ds/1428Mi) % 157.44/22.41 % (200074)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.44/22.41 % (200074)Terminated due to inappropriate strategy. % 157.44/22.41 % (200074)------------------------------ % 157.44/22.41 % (200074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.44/22.41 % (200074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/22.41 % (200074)CaDiCaL version: 2.1.3 % 157.44/22.41 % (200074)Termination reason: Inappropriate % 157.44/22.41 % (200074)Time elapsed: 0.003 s % 157.44/22.41 % (200074)Peak memory usage: 10 MB % 157.44/22.41 % (200074)Instructions burned: 9 (million) % 157.44/22.41 % (200074)------------------------------ % 157.44/22.41 % (200074)------------------------------ % 191.46/27.24 % (200076)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1853654149:i=262:bd=preordered:rtra=on:fsd=on_2807 on theBenchmark for (2807ds/262Mi) % 191.46/27.24 % (200076)Instruction limit reached! % 191.46/27.24 % (200076)------------------------------ % 191.46/27.24 % (200076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.46/27.24 % (200076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.46/27.24 % (200076)CaDiCaL version: 2.1.3 % 191.46/27.24 % (200076)Termination reason: Instruction limit % 191.46/27.24 % (200076)Termination phase: Saturation % 191.46/27.24 % (200076)Time elapsed: 0.097 s % 191.46/27.24 % (200076)Peak memory usage: 14 MB % 191.46/27.24 % (200076)Instructions burned: 262 (million) % 191.46/27.24 % (200078)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=2254776273:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2806 on theBenchmark for (2806ds/1368Mi) % 191.46/27.24 % (200078)Instruction limit reached! % 191.46/27.24 % (200078)------------------------------ % 191.46/27.24 % (200078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.46/27.24 % (200078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.46/27.24 % (200078)CaDiCaL version: 2.1.3 % 191.46/27.24 % (200078)Termination reason: Instruction limit % 191.46/27.24 % (200078)Termination phase: Saturation % 191.46/27.24 % (200078)Time elapsed: 0.403 s % 191.46/27.24 % (200078)Peak memory usage: 20 MB % 191.46/27.24 % (200078)Instructions burned: 1371 (million) % 191.46/27.24 % (200080)ott-21_1_sil=16000:si=on:fs=off:random_seed=3057060586:i=360:av=off:fsr=off:rtra=on_2802 on theBenchmark for (2802ds/360Mi) % 191.46/27.24 % (200080)Instruction limit reached! % 191.46/27.24 % (200080)------------------------------ % 191.46/27.24 % (200080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.46/27.24 % (200080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.46/27.24 % (200080)CaDiCaL version: 2.1.3 % 191.46/27.24 % (200080)Termination reason: Instruction limit % 191.46/27.24 % (200080)Termination phase: Saturation % 191.46/27.24 % (200080)Time elapsed: 0.101 s % 191.46/27.24 % (200080)Peak memory usage: 14 MB % 191.46/27.24 % (200080)Instructions burned: 365 (million) % 191.46/27.24 % (200082)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3087035272:i=954:bd=all:rtra=on_2801 on theBenchmark for (2801ds/954Mi) % 191.46/27.24 % (200082)Instruction limit reached! % 191.46/27.24 % (200082)------------------------------ % 191.46/27.24 % (200082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.46/27.24 % (200082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.46/27.24 % (200082)CaDiCaL version: 2.1.3 % 191.46/27.24 % (200082)Termination reason: Instruction limit % 191.46/27.24 % (200082)Termination phase: Saturation % 191.46/27.24 % (200082)Time elapsed: 0.337 s % 191.46/27.24 % (200082)Peak memory usage: 16 MB % 191.46/27.24 % (200082)Instructions burned: 955 (million) % 191.46/27.24 % (200084)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3851281896:fmbsr=1.3:i=1730:ins=25:rtra=on_2797 on theBenchmark for (2797ds/1730Mi) % 191.46/27.24 % (200084)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.46/27.24 % (200084)Terminated due to inappropriate strategy. % 191.46/27.24 % (200084)------------------------------ % 191.46/27.24 % (200084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.46/27.24 % (200084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.46/27.24 % (200084)CaDiCaL version: 2.1.3 % 191.46/27.24 % (200084)Termination reason: Inappropriate % 191.46/27.24 % (200084)Time elapsed: 0.005 s % 191.46/27.24 % (200084)Peak memory usage: 10 MB % 191.46/27.24 % (200084)Instructions burned: 10 (million) % 191.46/27.24 % (200084)------------------------------ % 191.46/27.24 % (200084)------------------------------ % 191.46/27.24 % (200086)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4182202467:i=2358:rtra=on_2797 on theBenchmark for (2797ds/2358Mi) % 191.46/27.24 % (200086)Instruction limit reached! % 191.46/27.24 % (200086)------------------------------ % 191.46/27.24 % (200086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.46/27.24 % (200086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.46/27.24 % (200086)CaDiCaL version: 2.1.3 % 191.46/27.24 % (200086)Termination reason: Instruction limit % 191.46/27.24 % (200086)Termination phase: Saturation % 241.15/34.29 % (200086)Time elapsed: 0.835 s % 241.15/34.29 % (200086)Peak memory usage: 28 MB % 241.15/34.29 % (200086)Instructions burned: 2361 (million) % 241.15/34.29 % (200088)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1821959754:i=1778:ins=1:rtra=on_2788 on theBenchmark for (2788ds/1778Mi) % 241.15/34.29 % (200088)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 241.15/34.29 % (200088)Terminated due to inappropriate strategy. % 241.15/34.29 % (200088)------------------------------ % 241.15/34.29 % (200088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.15/34.29 % (200088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.15/34.29 % (200088)CaDiCaL version: 2.1.3 % 241.15/34.29 % (200088)Termination reason: Inappropriate % 241.15/34.29 % (200088)Time elapsed: 0.003 s % 241.15/34.29 % (200088)Peak memory usage: 10 MB % 241.15/34.29 % (200088)Instructions burned: 10 (million) % 241.15/34.29 % (200088)------------------------------ % 241.15/34.29 % (200088)------------------------------ % 241.15/34.29 % (200090)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=3270918925:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2788 on theBenchmark for (2788ds/1384Mi) % 241.15/34.29 % (200090)Instruction limit reached! % 241.15/34.29 % (200090)------------------------------ % 241.15/34.29 % (200090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.15/34.29 % (200090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.15/34.29 % (200090)CaDiCaL version: 2.1.3 % 241.15/34.29 % (200090)Termination reason: Instruction limit % 241.15/34.29 % (200090)Termination phase: Saturation % 241.15/34.29 % (200090)Time elapsed: 0.464 s % 241.15/34.29 % (200090)Peak memory usage: 23 MB % 241.15/34.29 % (200090)Instructions burned: 1386 (million) % 241.15/34.29 % (200092)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=349173930:i=1758:kws=inv_precedence:fsr=off:rtra=on_2783 on theBenchmark for (2783ds/1758Mi) % 241.15/34.29 % (200092)Instruction limit reached! % 241.15/34.29 % (200092)------------------------------ % 241.15/34.29 % (200092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.15/34.29 % (200092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.15/34.29 % (200092)CaDiCaL version: 2.1.3 % 241.15/34.29 % (200092)Termination reason: Instruction limit % 241.15/34.29 % (200092)Termination phase: Saturation % 241.15/34.29 % (200092)Time elapsed: 0.529 s % 241.15/34.29 % (200092)Peak memory usage: 25 MB % 241.15/34.29 % (200092)Instructions burned: 1759 (million) % 241.15/34.29 % (200094)fmb+10_1_sil=64000:si=on:random_seed=1490575103:i=44122:nm=2:rtra=on:gsp=on_2778 on theBenchmark for (2778ds/44122Mi) % 241.15/34.29 % (200094)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 241.15/34.29 % (200094)Terminated due to inappropriate strategy. % 241.15/34.29 % (200094)------------------------------ % 241.15/34.29 % (200094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.15/34.29 % (200094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.15/34.29 % (200094)CaDiCaL version: 2.1.3 % 241.15/34.29 % (200094)Termination reason: Inappropriate % 241.15/34.29 % (200094)Time elapsed: 0.003 s % 241.15/34.29 % (200094)Peak memory usage: 10 MB % 241.15/34.29 % (200094)Instructions burned: 10 (million) % 241.15/34.29 % (200094)------------------------------ % 241.15/34.29 % (200094)------------------------------ % 241.15/34.29 % (200096)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3414197840:i=19030:nm=5:rtra=on_2778 on theBenchmark for (2778ds/19030Mi) % 241.15/34.29 % (200096)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 241.15/34.29 % (200096)Terminated due to inappropriate strategy. % 241.15/34.29 % (200096)------------------------------ % 241.15/34.29 % (200096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.15/34.29 % (200096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.15/34.29 % (200096)CaDiCaL version: 2.1.3 % 241.15/34.29 % (200096)Termination reason: Inappropriate % 241.15/34.29 % (200096)Time elapsed: 0.003 s % 241.15/34.29 % (200096)Peak memory usage: 10 MB % 241.15/34.29 % (200096)Instructions burned: 10 (million) % 241.15/34.29 % (200096)------------------------------ % 241.15/34.29 % (200096)------------------------------ % 241.15/34.29 % (200098)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=636031130:fmbsr=1.7:i=1840:rtra=on_2778 on theBenchmark for (2778ds/1840Mi) % 252.62/39.10 % (200098)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.62/39.10 % (200098)Terminated due to inappropriate strategy. % 252.62/39.10 % (200098)------------------------------ % 252.62/39.10 % (200098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.62/39.10 % (200098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.62/39.10 % (200098)CaDiCaL version: 2.1.3 % 252.62/39.10 % (200098)Termination reason: Inappropriate % 252.62/39.10 % (200098)Time elapsed: 0.003 s % 252.62/39.10 % (200098)Peak memory usage: 10 MB % 252.62/39.10 % (200098)Instructions burned: 10 (million) % 252.62/39.10 % (200098)------------------------------ % 252.62/39.10 % (200098)------------------------------ % 252.62/39.10 % (200100)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1485653698:i=10262:rtra=on_2778 on theBenchmark for (2778ds/10262Mi) % 252.62/39.10 % (200100)Instruction limit reached! % 252.62/39.10 % (200100)------------------------------ % 252.62/39.10 % (200100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.62/39.10 % (200100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.62/39.10 % (200100)CaDiCaL version: 2.1.3 % 252.62/39.10 % (200100)Termination reason: Instruction limit % 252.62/39.10 % (200100)Termination phase: Saturation % 252.62/39.10 % (200100)Time elapsed: 3.232 s % 252.62/39.10 % (200100)Peak memory usage: 57 MB % 252.62/39.10 % (200100)Instructions burned: 10265 (million) % 252.62/39.10 % (200102)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1492127415:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2745 on theBenchmark for (2745ds/2944Mi) % 252.62/39.10 % (200102)Instruction limit reached! % 252.62/39.10 % (200102)------------------------------ % 252.62/39.10 % (200102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.62/39.10 % (200102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.62/39.10 % (200102)CaDiCaL version: 2.1.3 % 252.62/39.10 % (200102)Termination reason: Instruction limit % 252.62/39.10 % (200102)Termination phase: Saturation % 252.62/39.10 % (200102)Time elapsed: 0.925 s % 252.62/39.10 % (200102)Peak memory usage: 42 MB % 252.62/39.10 % (200102)Instructions burned: 2944 (million) % 252.62/39.10 % (200104)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2887709652:i=12648:rtra=on_2736 on theBenchmark for (2736ds/12648Mi) % 252.62/39.10 % (200104)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.62/39.10 % (200104)Terminated due to inappropriate strategy. % 252.62/39.10 % (200104)------------------------------ % 252.62/39.10 % (200104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.62/39.10 % (200104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.62/39.10 % (200104)CaDiCaL version: 2.1.3 % 252.62/39.10 % (200104)Termination reason: Inappropriate % 252.62/39.10 % (200104)Time elapsed: 0.003 s % 252.62/39.10 % (200104)Peak memory usage: 11 MB % 252.62/39.10 % (200104)Instructions burned: 10 (million) % 252.62/39.10 % (200104)------------------------------ % 252.62/39.10 % (200104)------------------------------ % 252.62/39.10 % (200106)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3910755665:fmbsr=2.30978:i=4348:rtra=on_2736 on theBenchmark for (2736ds/4348Mi) % 252.62/39.10 % (200106)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.62/39.10 % (200106)Terminated due to inappropriate strategy. % 252.62/39.10 % (200106)------------------------------ % 252.62/39.10 % (200106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.62/39.10 % (200106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.62/39.10 % (200106)CaDiCaL version: 2.1.3 % 252.62/39.10 % (200106)Termination reason: Inappropriate % 252.62/39.10 % (200106)Time elapsed: 0.003 s % 252.62/39.10 % (200106)Peak memory usage: 10 MB % 252.62/39.10 % (200106)Instructions burned: 10 (million) % 252.62/39.10 % (200106)------------------------------ % 252.62/39.10 % (200106)------------------------------ % 252.62/39.10 % (200108)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2498392607:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2735 on theBenchmark for (2735ds/1738Mi) % 252.62/39.10 % (200108)Instruction limit reached! % 252.62/39.10 % (200108)------------------------------ % 252.62/39.10 % (200108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.62/39.10 % (200108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819dTerminated % 300.08/42.54 % Vampire exiting %------------------------------------------------------------------------------