%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX143_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n003.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:46:33 PM UTC 2026 % Result : Timeout 286.06s 40.89s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX143_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.19 % Computer : n003.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 15:06:28 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/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 % 4.89/1.24 % (1684715)Will run a generic schedule for satisfiability detection. % 4.89/1.24 % (1684722)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3104031809:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi) % 4.89/1.24 % (1684721)% WARNING: option uhcvi not known. % 4.89/1.24 % (1684720)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1268275695_2996 on theBenchmark for (2996ds/0Mi) % 4.89/1.24 % (1684724)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1741477956:i=116_2996 on theBenchmark for (2996ds/116Mi) % 4.89/1.24 % (1684721)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1688927740:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi) % 4.89/1.24 % (1684723)dis+10_1_sil=32000:sp=arity:random_seed=1926654689:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi) % 4.89/1.24 % (1684726)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1951930687:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi) % 4.89/1.24 % (1684725)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1490114485:i=131_2996 on theBenchmark for (2996ds/131Mi) % 4.89/1.24 % (1684723)Instruction limit reached! % 4.89/1.24 % (1684723)------------------------------ % 4.89/1.24 % (1684723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.89/1.24 % (1684723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.89/1.24 % (1684723)CaDiCaL version: 2.1.3 % 4.89/1.24 % (1684723)Termination reason: Instruction limit % 4.89/1.24 % (1684723)Termination phase: Property scanning % 4.89/1.24 % (1684723)Time elapsed: 0.041 s % 4.89/1.24 % (1684723)Peak memory usage: 10 MB % 4.89/1.24 % (1684723)Instructions burned: 103 (million) % 4.89/1.24 % (1684724)Instruction limit reached! % 4.89/1.24 % (1684724)------------------------------ % 4.89/1.24 % (1684724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.89/1.24 % (1684724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.89/1.24 % (1684724)CaDiCaL version: 2.1.3 % 4.89/1.24 % (1684724)Termination reason: Instruction limit % 4.89/1.24 % (1684724)Termination phase: Property scanning % 4.89/1.24 % (1684724)Time elapsed: 0.047 s % 4.89/1.24 % (1684724)Peak memory usage: 10 MB % 4.89/1.24 % (1684724)Instructions burned: 117 (million) % 4.89/1.24 % (1684725)Instruction limit reached! % 4.89/1.24 % (1684725)------------------------------ % 4.89/1.24 % (1684725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.89/1.24 % (1684725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.89/1.24 % (1684725)CaDiCaL version: 2.1.3 % 4.89/1.24 % (1684725)Termination reason: Instruction limit % 4.89/1.24 % (1684725)Termination phase: Property scanning % 4.89/1.24 % (1684725)Time elapsed: 0.053 s % 4.89/1.24 % (1684725)Peak memory usage: 10 MB % 4.89/1.24 % (1684725)Instructions burned: 132 (million) % 4.89/1.24 % (1684734)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1637684268:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi) % 4.89/1.24 % (1684726)Instruction limit reached! % 4.89/1.24 % (1684726)------------------------------ % 4.89/1.24 % (1684726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.89/1.24 % (1684726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.89/1.24 % (1684726)CaDiCaL version: 2.1.3 % 4.89/1.24 % (1684726)Termination reason: Instruction limit % 4.89/1.24 % (1684726)Termination phase: Property scanning % 4.89/1.24 % (1684726)Time elapsed: 0.063 s % 4.89/1.24 % (1684726)Peak memory usage: 10 MB % 4.89/1.24 % (1684726)Instructions burned: 160 (million) % 4.89/1.24 % (1684735)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2678927626:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi) % 4.89/1.24 % (1684736)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=3678927414:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi) % 4.89/1.24 % (1684738)ott-21_1_sil=16000:fs=off:random_seed=99910074:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi) % 4.89/1.24 % (1684735)Instruction limit reached! % 4.89/1.24 % (1684735)------------------------------ % 4.89/1.24 % (1684735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.89/1.24 % (1684735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.64 % (1684735)CaDiCaL version: 2.1.3 % 6.43/1.64 % (1684735)Termination reason: Instruction limit % 6.43/1.64 % (1684735)Termination phase: Property scanning % 6.43/1.64 % (1684735)Time elapsed: 0.052 s % 6.43/1.64 % (1684735)Peak memory usage: 10 MB % 6.43/1.64 % (1684735)Instructions burned: 132 (million) % 6.43/1.64 % (1684742)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1358402127:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi) % 6.43/1.64 % (1684738)Instruction limit reached! % 6.43/1.64 % (1684738)------------------------------ % 6.43/1.64 % (1684738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.43/1.64 % (1684738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.64 % (1684738)CaDiCaL version: 2.1.3 % 6.43/1.64 % (1684738)Termination reason: Instruction limit % 6.43/1.64 % (1684738)Termination phase: Property scanning % 6.43/1.64 % (1684738)Time elapsed: 0.070 s % 6.43/1.64 % (1684738)Peak memory usage: 10 MB % 6.43/1.64 % (1684738)Instructions burned: 180 (million) % 6.43/1.64 % (1684744)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3985293778:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 6.43/1.64 % (1684720)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.43/1.64 % (1684720)Terminated due to inappropriate strategy. % 6.43/1.64 % (1684720)------------------------------ % 6.43/1.64 % (1684720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.43/1.64 % (1684720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.64 % (1684720)CaDiCaL version: 2.1.3 % 6.43/1.64 % (1684720)Termination reason: Inappropriate % 6.43/1.64 % (1684720)Time elapsed: 0.177 s % 6.43/1.64 % (1684720)Peak memory usage: 11 MB % 6.43/1.64 % (1684720)Instructions burned: 467 (million) % 6.43/1.64 % (1684720)------------------------------ % 6.43/1.64 % (1684720)------------------------------ % 6.43/1.64 % (1684746)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1513107560:i=1179_2994 on theBenchmark for (2994ds/1179Mi) % 6.43/1.64 % (1684734)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.43/1.64 % (1684734)Terminated due to inappropriate strategy. % 6.43/1.64 % (1684734)------------------------------ % 6.43/1.64 % (1684734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.43/1.64 % (1684734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.64 % (1684734)CaDiCaL version: 2.1.3 % 6.43/1.64 % (1684734)Termination reason: Inappropriate % 6.43/1.64 % (1684734)Time elapsed: 0.177 s % 6.43/1.64 % (1684734)Peak memory usage: 11 MB % 6.43/1.64 % (1684734)Instructions burned: 467 (million) % 6.43/1.64 % (1684734)------------------------------ % 6.43/1.64 % (1684734)------------------------------ % 6.43/1.64 % (1684748)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3861211308:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 6.43/1.64 % (1684744)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.43/1.64 % (1684744)Terminated due to inappropriate strategy. % 6.43/1.64 % (1684744)------------------------------ % 6.43/1.64 % (1684744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.43/1.64 % (1684744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.64 % (1684744)CaDiCaL version: 2.1.3 % 6.43/1.64 % (1684744)Termination reason: Inappropriate % 6.43/1.64 % (1684744)Time elapsed: 0.135 s % 6.43/1.64 % (1684744)Peak memory usage: 11 MB % 6.43/1.64 % (1684744)Instructions burned: 354 (million) % 6.43/1.64 % (1684744)------------------------------ % 6.43/1.64 % (1684744)------------------------------ % 6.43/1.64 % (1684742)Instruction limit reached! % 6.43/1.64 % (1684742)------------------------------ % 6.43/1.64 % (1684742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.43/1.64 % (1684742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.64 % (1684742)CaDiCaL version: 2.1.3 % 6.43/1.64 % (1684742)Termination reason: Instruction limit % 6.43/1.64 % (1684742)Termination phase: Saturation % 6.43/1.64 % (1684742)Time elapsed: 0.182 s % 6.43/1.64 % (1684742)Peak memory usage: 12 MB % 6.43/1.64 % (1684742)Instructions burned: 479 (million) % 6.43/1.64 % (1684750)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=4293549051:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi) % 19.81/3.33 % (1684736)Instruction limit reached! % 19.81/3.33 % (1684736)------------------------------ % 19.81/3.33 % (1684736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.81/3.33 % (1684736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.81/3.33 % (1684736)CaDiCaL version: 2.1.3 % 19.81/3.33 % (1684736)Termination reason: Instruction limit % 19.81/3.33 % (1684736)Termination phase: Saturation % 19.81/3.33 % (1684736)Time elapsed: 0.264 s % 19.81/3.33 % (1684736)Peak memory usage: 12 MB % 19.81/3.33 % (1684736)Instructions burned: 684 (million) % 19.81/3.33 % (1684751)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1669473769:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 19.81/3.33 % (1684753)fmb+10_1_sil=64000:random_seed=3871653232:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 19.81/3.33 % (1684748)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.81/3.33 % (1684748)Terminated due to inappropriate strategy. % 19.81/3.33 % (1684748)------------------------------ % 19.81/3.33 % (1684748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.81/3.33 % (1684748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.81/3.33 % (1684748)CaDiCaL version: 2.1.3 % 19.81/3.33 % (1684748)Termination reason: Inappropriate % 19.81/3.33 % (1684748)Time elapsed: 0.135 s % 19.81/3.33 % (1684748)Peak memory usage: 11 MB % 19.81/3.33 % (1684748)Instructions burned: 354 (million) % 19.81/3.33 % (1684748)------------------------------ % 19.81/3.33 % (1684748)------------------------------ % 19.81/3.33 % (1684756)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3465023784:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 19.81/3.33 % (1684753)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.81/3.33 % (1684753)Terminated due to inappropriate strategy. % 19.81/3.33 % (1684753)------------------------------ % 19.81/3.33 % (1684753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.81/3.33 % (1684753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.81/3.33 % (1684753)CaDiCaL version: 2.1.3 % 19.81/3.33 % (1684753)Termination reason: Inappropriate % 19.81/3.33 % (1684753)Time elapsed: 0.177 s % 19.81/3.33 % (1684753)Peak memory usage: 11 MB % 19.81/3.33 % (1684753)Instructions burned: 467 (million) % 19.81/3.33 % (1684753)------------------------------ % 19.81/3.33 % (1684753)------------------------------ % 19.81/3.33 % (1684758)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1699798895:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 19.81/3.33 % (1684756)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.81/3.33 % (1684756)Terminated due to inappropriate strategy. % 19.81/3.33 % (1684756)------------------------------ % 19.81/3.33 % (1684756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.81/3.33 % (1684756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.81/3.33 % (1684756)CaDiCaL version: 2.1.3 % 19.81/3.33 % (1684756)Termination reason: Inappropriate % 19.81/3.33 % (1684756)Time elapsed: 0.176 s % 19.81/3.33 % (1684756)Peak memory usage: 11 MB % 19.81/3.33 % (1684756)Instructions burned: 467 (million) % 19.81/3.33 % (1684756)------------------------------ % 19.81/3.33 % (1684756)------------------------------ % 19.81/3.33 % (1684750)Instruction limit reached! % 19.81/3.33 % (1684750)------------------------------ % 19.81/3.33 % (1684750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.81/3.33 % (1684750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.81/3.33 % (1684750)CaDiCaL version: 2.1.3 % 19.81/3.33 % (1684750)Termination reason: Instruction limit % 19.81/3.33 % (1684750)Termination phase: Saturation % 19.81/3.33 % (1684750)Time elapsed: 0.266 s % 19.81/3.33 % (1684750)Peak memory usage: 12 MB % 19.81/3.33 % (1684750)Instructions burned: 692 (million) % 19.81/3.33 % (1684760)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=419914545:i=5131_2990 on theBenchmark for (2990ds/5131Mi) % 19.81/3.33 % (1684761)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1249838918:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi) % 19.81/3.33 % (1684746)Instruction limit reached! % 19.81/3.33 % (1684746)------------------------------ % 19.81/3.33 % (1684746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.85 % (1684746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.09/3.85 % (1684746)CaDiCaL version: 2.1.3 % 22.09/3.85 % (1684746)Termination reason: Instruction limit % 22.09/3.85 % (1684746)Termination phase: Saturation % 22.09/3.85 % (1684746)Time elapsed: 0.478 s % 22.09/3.85 % (1684746)Peak memory usage: 18 MB % 22.09/3.85 % (1684746)Instructions burned: 1179 (million) % 22.09/3.85 % (1684751)Instruction limit reached! % 22.09/3.85 % (1684751)------------------------------ % 22.09/3.85 % (1684751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.85 % (1684751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.09/3.85 % (1684751)CaDiCaL version: 2.1.3 % 22.09/3.85 % (1684751)Termination reason: Instruction limit % 22.09/3.85 % (1684751)Termination phase: Saturation % 22.09/3.85 % (1684751)Time elapsed: 0.348 s % 22.09/3.85 % (1684751)Peak memory usage: 15 MB % 22.09/3.85 % (1684751)Instructions burned: 881 (million) % 22.09/3.85 % (1684764)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1875173634:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 22.09/3.85 % (1684765)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1002452884:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 22.09/3.85 % (1684758)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.09/3.85 % (1684758)Terminated due to inappropriate strategy. % 22.09/3.85 % (1684758)------------------------------ % 22.09/3.85 % (1684758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.85 % (1684758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.09/3.85 % (1684758)CaDiCaL version: 2.1.3 % 22.09/3.85 % (1684758)Termination reason: Inappropriate % 22.09/3.85 % (1684758)Time elapsed: 0.177 s % 22.09/3.85 % (1684758)Peak memory usage: 11 MB % 22.09/3.85 % (1684758)Instructions burned: 467 (million) % 22.09/3.85 % (1684758)------------------------------ % 22.09/3.85 % (1684758)------------------------------ % 22.09/3.85 % (1684768)ott-2_1_sil=16000:newcnf=on:random_seed=2125741232:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 22.09/3.85 % (1684764)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.09/3.85 % (1684764)Terminated due to inappropriate strategy. % 22.09/3.85 % (1684764)------------------------------ % 22.09/3.85 % (1684764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.85 % (1684764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.09/3.85 % (1684764)CaDiCaL version: 2.1.3 % 22.09/3.85 % (1684764)Termination reason: Inappropriate % 22.09/3.85 % (1684764)Time elapsed: 0.176 s % 22.09/3.85 % (1684764)Peak memory usage: 11 MB % 22.09/3.85 % (1684764)Instructions burned: 467 (million) % 22.09/3.85 % (1684764)------------------------------ % 22.09/3.85 % (1684764)------------------------------ % 22.09/3.85 % (1684765)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.09/3.85 % (1684765)Terminated due to inappropriate strategy. % 22.09/3.85 % (1684765)------------------------------ % 22.09/3.85 % (1684765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.85 % (1684765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.09/3.85 % (1684765)CaDiCaL version: 2.1.3 % 22.09/3.85 % (1684765)Termination reason: Inappropriate % 22.09/3.85 % (1684765)Time elapsed: 0.176 s % 22.09/3.85 % (1684765)Peak memory usage: 11 MB % 22.09/3.85 % (1684765)Instructions burned: 467 (million) % 22.09/3.85 % (1684765)------------------------------ % 22.09/3.85 % (1684765)------------------------------ % 22.09/3.85 % (1684770)ott+10_1_sil=32000:tgt=ground:random_seed=3103241938:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi) % 22.09/3.85 % (1684771)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=85822201:i=54282_2987 on theBenchmark for (2987ds/54282Mi) % 22.09/3.85 % (1684771)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.09/3.85 % (1684771)Terminated due to inappropriate strategy. % 22.09/3.85 % (1684771)------------------------------ % 22.09/3.85 % (1684771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.85 % (1684771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.09/3.85 % (1684771)CaDiCaL version: 2.1.3 % 22.09/3.85 % (1684771)Termination reason: Inappropriate % 22.09/3.85 % (1684771)Time elapsed: 0.176 s % 22.09/3.85 % (1684771)Peak memory usage: 11 MB % 87.38/12.88 % (1684771)Instructions burned: 467 (million) % 87.38/12.88 % (1684771)------------------------------ % 87.38/12.88 % (1684771)------------------------------ % 87.38/12.88 % (1684774)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3246695787:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 87.38/12.88 % (1684768)Instruction limit reached! % 87.38/12.88 % (1684768)------------------------------ % 87.38/12.88 % (1684768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.38/12.88 % (1684768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.38/12.88 % (1684768)CaDiCaL version: 2.1.3 % 87.38/12.88 % (1684768)Termination reason: Instruction limit % 87.38/12.88 % (1684768)Termination phase: Saturation % 87.38/12.88 % (1684768)Time elapsed: 0.369 s % 87.38/12.88 % (1684768)Peak memory usage: 18 MB % 87.38/12.88 % (1684768)Instructions burned: 870 (million) % 87.38/12.88 % (1684776)dis+21_1_sil=32000:sas=cadical:random_seed=3681253177:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi) % 87.38/12.88 % (1684761)Instruction limit reached! % 87.38/12.88 % (1684761)------------------------------ % 87.38/12.88 % (1684761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.38/12.88 % (1684761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.38/12.88 % (1684761)CaDiCaL version: 2.1.3 % 87.38/12.88 % (1684761)Termination reason: Instruction limit % 87.38/12.88 % (1684761)Termination phase: Saturation % 87.38/12.88 % (1684761)Time elapsed: 0.597 s % 87.38/12.88 % (1684761)Peak memory usage: 18 MB % 87.38/12.88 % (1684761)Instructions burned: 1472 (million) % 87.38/12.88 % (1684778)ott+11_1_sil=16000:gs=on:random_seed=3195402615:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2984 on theBenchmark for (2984ds/2251Mi) % 87.38/12.88 % (1684778)Instruction limit reached! % 87.38/12.88 % (1684778)------------------------------ % 87.38/12.88 % (1684778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.38/12.88 % (1684778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.38/12.88 % (1684778)CaDiCaL version: 2.1.3 % 87.38/12.88 % (1684778)Termination reason: Instruction limit % 87.38/12.88 % (1684778)Termination phase: Saturation % 87.38/12.88 % (1684778)Time elapsed: 0.895 s % 87.38/12.88 % (1684778)Peak memory usage: 19 MB % 87.38/12.88 % (1684778)Instructions burned: 2251 (million) % 87.38/12.88 % (1684780)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2122374064:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi) % 87.38/12.88 % (1684780)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 87.38/12.88 % (1684780)Terminated due to inappropriate strategy. % 87.38/12.88 % (1684780)------------------------------ % 87.38/12.88 % (1684780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.38/12.88 % (1684780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.38/12.88 % (1684780)CaDiCaL version: 2.1.3 % 87.38/12.88 % (1684780)Termination reason: Inappropriate % 87.38/12.88 % (1684780)Time elapsed: 0.177 s % 87.38/12.88 % (1684780)Peak memory usage: 11 MB % 87.38/12.88 % (1684780)Instructions burned: 467 (million) % 87.38/12.88 % (1684780)------------------------------ % 87.38/12.88 % (1684780)------------------------------ % 87.38/12.88 % (1684782)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3672317328:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2973 on theBenchmark for (2973ds/4591Mi) % 87.38/12.88 % (1684774)Instruction limit reached! % 87.38/12.88 % (1684774)------------------------------ % 87.38/12.88 % (1684774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.38/12.88 % (1684774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.38/12.88 % (1684774)CaDiCaL version: 2.1.3 % 87.38/12.88 % (1684774)Termination reason: Instruction limit % 87.38/12.88 % (1684774)Termination phase: Saturation % 87.38/12.88 % (1684774)Time elapsed: 1.479 s % 87.38/12.88 % (1684774)Peak memory usage: 20 MB % 87.38/12.88 % (1684774)Instructions burned: 3513 (million) % 87.38/12.88 % (1684784)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3893861716:i=29340_2970 on theBenchmark for (2970ds/29340Mi) % 87.38/12.88 % (1684776)Instruction limit reached! % 87.38/12.88 % (1684776)------------------------------ % 87.38/12.88 % (1684776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.38/12.88 % (1684776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.39/15.58 % (1684776)CaDiCaL version: 2.1.3 % 106.39/15.58 % (1684776)Termination reason: Instruction limit % 106.39/15.58 % (1684776)Termination phase: Saturation % 106.39/15.58 % (1684776)Time elapsed: 1.628 s % 106.39/15.58 % (1684776)Peak memory usage: 19 MB % 106.39/15.58 % (1684776)Instructions burned: 3773 (million) % 106.39/15.58 % (1684786)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4166358142:i=5211_2968 on theBenchmark for (2968ds/5211Mi) % 106.39/15.58 % (1684760)Instruction limit reached! % 106.39/15.58 % (1684760)------------------------------ % 106.39/15.58 % (1684760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.39/15.58 % (1684760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.39/15.58 % (1684760)CaDiCaL version: 2.1.3 % 106.39/15.58 % (1684760)Termination reason: Instruction limit % 106.39/15.58 % (1684760)Termination phase: Saturation % 106.39/15.58 % (1684760)Time elapsed: 2.254 s % 106.39/15.58 % (1684760)Peak memory usage: 21 MB % 106.39/15.58 % (1684760)Instructions burned: 5131 (million) % 106.39/15.58 % (1684788)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3278649030:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 106.39/15.58 % (1684770)Instruction limit reached! % 106.39/15.58 % (1684770)------------------------------ % 106.39/15.58 % (1684770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.39/15.58 % (1684770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.39/15.58 % (1684770)CaDiCaL version: 2.1.3 % 106.39/15.58 % (1684770)Termination reason: Instruction limit % 106.39/15.58 % (1684770)Termination phase: Saturation % 106.39/15.58 % (1684770)Time elapsed: 1.994 s % 106.39/15.58 % (1684770)Peak memory usage: 29 MB % 106.39/15.58 % (1684770)Instructions burned: 5115 (million) % 106.39/15.58 % (1684790)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2774158342:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 106.39/15.58 % (1684788)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.39/15.58 % (1684788)Terminated due to inappropriate strategy. % 106.39/15.58 % (1684788)------------------------------ % 106.39/15.58 % (1684788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.39/15.58 % (1684788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.39/15.58 % (1684788)CaDiCaL version: 2.1.3 % 106.39/15.58 % (1684788)Termination reason: Inappropriate % 106.39/15.58 % (1684788)Time elapsed: 0.177 s % 106.39/15.58 % (1684788)Peak memory usage: 11 MB % 106.39/15.58 % (1684788)Instructions burned: 467 (million) % 106.39/15.58 % (1684788)------------------------------ % 106.39/15.58 % (1684788)------------------------------ % 106.39/15.58 % (1684792)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2492424558:i=14071_2965 on theBenchmark for (2965ds/14071Mi) % 106.39/15.58 % (1684790)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.39/15.58 % (1684790)Terminated due to inappropriate strategy. % 106.39/15.58 % (1684790)------------------------------ % 106.39/15.58 % (1684790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.39/15.58 % (1684790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.39/15.58 % (1684790)CaDiCaL version: 2.1.3 % 106.39/15.58 % (1684790)Termination reason: Inappropriate % 106.39/15.58 % (1684790)Time elapsed: 0.177 s % 106.39/15.58 % (1684790)Peak memory usage: 11 MB % 106.39/15.58 % (1684790)Instructions burned: 467 (million) % 106.39/15.58 % (1684790)------------------------------ % 106.39/15.58 % (1684790)------------------------------ % 106.39/15.58 % (1684794)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=533256348:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi) % 106.39/15.58 % (1684792)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.39/15.58 % (1684792)Terminated due to inappropriate strategy. % 106.39/15.58 % (1684792)------------------------------ % 106.39/15.58 % (1684792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.39/15.58 % (1684792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.39/15.58 % (1684792)CaDiCaL version: 2.1.3 % 106.39/15.58 % (1684792)Termination reason: Inappropriate % 106.39/15.58 % (1684792)Time elapsed: 0.179 s % 106.39/15.58 % (1684792)Peak memory usage: 11 MB % 106.39/15.58 % (1684792)Instructions burned: 467 (million) % 106.39/15.58 % (1684792)------------------------------ % 106.39/15.58 % (1684792)------------------------------ % 106.39/15.58 % (1684796)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2824640504:i=8173:av=off_2963 on theBenchmark for (2963ds/8173Mi) % 118.44/17.24 % (1684782)Instruction limit reached! % 118.44/17.24 % (1684782)------------------------------ % 118.44/17.24 % (1684782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.44/17.24 % (1684782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.44/17.24 % (1684782)CaDiCaL version: 2.1.3 % 118.44/17.24 % (1684782)Termination reason: Instruction limit % 118.44/17.24 % (1684782)Termination phase: Saturation % 118.44/17.24 % (1684782)Time elapsed: 1.949 s % 118.44/17.24 % (1684782)Peak memory usage: 18 MB % 118.44/17.24 % (1684782)Instructions burned: 4592 (million) % 118.44/17.24 % (1684798)dis+10_16:1_sil=16000:random_seed=548706246:i=9155:fsr=off_2953 on theBenchmark for (2953ds/9155Mi) % 118.44/17.24 % (1684786)Instruction limit reached! % 118.44/17.24 % (1684786)------------------------------ % 118.44/17.24 % (1684786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.44/17.24 % (1684786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.44/17.24 % (1684786)CaDiCaL version: 2.1.3 % 118.44/17.24 % (1684786)Termination reason: Instruction limit % 118.44/17.24 % (1684786)Termination phase: Saturation % 118.44/17.24 % (1684786)Time elapsed: 2.242 s % 118.44/17.24 % (1684786)Peak memory usage: 21 MB % 118.44/17.24 % (1684786)Instructions burned: 5213 (million) % 118.44/17.24 % (1684800)ott-3_8_sil=64000:random_seed=743144685:i=20139:bs=on_2946 on theBenchmark for (2946ds/20139Mi) % 118.44/17.24 % (1684796)Instruction limit reached! % 118.44/17.24 % (1684796)------------------------------ % 118.44/17.24 % (1684796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.44/17.24 % (1684796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.44/17.24 % (1684796)CaDiCaL version: 2.1.3 % 118.44/17.24 % (1684796)Termination reason: Instruction limit % 118.44/17.24 % (1684796)Termination phase: Saturation % 118.44/17.24 % (1684796)Time elapsed: 3.159 s % 118.44/17.24 % (1684796)Peak memory usage: 29 MB % 118.44/17.24 % (1684796)Instructions burned: 8176 (million) % 118.44/17.24 % (1684802)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1031587067:fmbsr=2:i=32576_2932 on theBenchmark for (2932ds/32576Mi) % 118.44/17.24 % (1684802)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.44/17.25 % (1684802)Terminated due to inappropriate strategy. % 118.44/17.25 % (1684802)------------------------------ % 118.44/17.25 % (1684802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.44/17.25 % (1684802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.44/17.25 % (1684802)CaDiCaL version: 2.1.3 % 118.44/17.25 % (1684802)Termination reason: Inappropriate % 118.44/17.25 % (1684802)Time elapsed: 0.177 s % 118.44/17.25 % (1684802)Peak memory usage: 11 MB % 118.44/17.25 % (1684802)Instructions burned: 467 (million) % 118.44/17.25 % (1684802)------------------------------ % 118.44/17.25 % (1684802)------------------------------ % 118.44/17.25 % (1684804)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2024958981:i=11404_2930 on theBenchmark for (2930ds/11404Mi) % 118.44/17.25 % (1684798)Instruction limit reached! % 118.44/17.25 % (1684798)------------------------------ % 118.44/17.25 % (1684798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.44/17.25 % (1684798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.44/17.25 % (1684798)CaDiCaL version: 2.1.3 % 118.44/17.25 % (1684798)Termination reason: Instruction limit % 118.44/17.25 % (1684798)Termination phase: Saturation % 118.44/17.25 % (1684798)Time elapsed: 3.589 s % 118.44/17.25 % (1684798)Peak memory usage: 22 MB % 118.44/17.25 % (1684798)Instructions burned: 9158 (million) % 118.44/17.25 % (1684806)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=402609234:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 118.44/17.25 % (1684804)Instruction limit reached! % 118.44/17.25 % (1684804)------------------------------ % 118.44/17.25 % (1684804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.44/17.25 % (1684804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.44/17.25 % (1684804)CaDiCaL version: 2.1.3 % 118.44/17.25 % (1684804)Termination reason: Instruction limit % 118.44/17.25 % (1684804)Termination phase: Saturation % 118.44/17.25 % (1684804)Time elapsed: 4.389 s % 118.44/17.25 % (1684804)Peak memory usage: 29 MB % 118.44/17.25 % (1684804)Instructions burned: 11404 (million) % 118.44/17.25 % (1684808)dis+33_16_sil=32000:sac=on:random_seed=2047814271:i=15851:nm=0_2886 on theBenchmark for (2886ds/15851Mi) % 118.44/17.25 % (1684794)Instruction limit reached! % 118.44/17.25 % (1684794)------------------------------ % 148.37/21.44 % (1684794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.37/21.44 % (1684794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.37/21.44 % (1684794)CaDiCaL version: 2.1.3 % 148.37/21.44 % (1684794)Termination reason: Instruction limit % 148.37/21.44 % (1684794)Termination phase: Saturation % 148.37/21.44 % (1684794)Time elapsed: 9.216 s % 148.37/21.44 % (1684794)Peak memory usage: 18 MB % 148.37/21.44 % (1684794)Instructions burned: 22567 (million) % 148.37/21.44 % (1684810)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=113423716:avsq=on:i=17627:add=on:amm=off_2873 on theBenchmark for (2873ds/17627Mi) % 148.37/21.44 % (1684800)Instruction limit reached! % 148.37/21.44 % (1684800)------------------------------ % 148.37/21.44 % (1684800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.37/21.44 % (1684800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.37/21.44 % (1684800)CaDiCaL version: 2.1.3 % 148.37/21.44 % (1684800)Termination reason: Instruction limit % 148.37/21.44 % (1684800)Termination phase: Saturation % 148.37/21.44 % (1684800)Time elapsed: 7.515 s % 148.37/21.44 % (1684800)Peak memory usage: 31 MB % 148.37/21.44 % (1684800)Instructions burned: 20141 (million) % 148.37/21.44 % (1684814)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=790698683:s2a=on:i=53295_2870 on theBenchmark for (2870ds/53295Mi) % 148.37/21.44 % (1684806)Instruction limit reached! % 148.37/21.44 % (1684806)------------------------------ % 148.37/21.44 % (1684806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.37/21.44 % (1684806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.37/21.44 % (1684806)CaDiCaL version: 2.1.3 % 148.37/21.44 % (1684806)Termination reason: Instruction limit % 148.37/21.44 % (1684806)Termination phase: Saturation % 148.37/21.44 % (1684806)Time elapsed: 5.409 s % 148.37/21.44 % (1684806)Peak memory usage: 29 MB % 148.37/21.44 % (1684806)Instructions burned: 14134 (million) % 148.37/21.44 % (1684946)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1868530668:i=26857:ins=20_2863 on theBenchmark for (2863ds/26857Mi) % 148.37/21.44 % (1684946)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.37/21.44 % (1684946)Terminated due to inappropriate strategy. % 148.37/21.44 % (1684946)------------------------------ % 148.37/21.44 % (1684946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.37/21.44 % (1684946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.37/21.44 % (1684946)CaDiCaL version: 2.1.3 % 148.37/21.44 % (1684946)Termination reason: Inappropriate % 148.37/21.44 % (1684946)Time elapsed: 0.178 s % 148.37/21.44 % (1684946)Peak memory usage: 11 MB % 148.37/21.44 % (1684946)Instructions burned: 467 (million) % 148.37/21.44 % (1684946)------------------------------ % 148.37/21.44 % (1684946)------------------------------ % 148.37/21.44 % (1685007)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3278132637:i=28120:bs=on:fsr=off_2861 on theBenchmark for (2861ds/28120Mi) % 148.37/21.44 % (1684784)Instruction limit reached! % 148.37/21.44 % (1684784)------------------------------ % 148.37/21.44 % (1684784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.37/21.44 % (1684784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.37/21.44 % (1684784)CaDiCaL version: 2.1.3 % 148.37/21.44 % (1684784)Termination reason: Instruction limit % 148.37/21.44 % (1684784)Termination phase: Saturation % 148.37/21.44 % (1684784)Time elapsed: 12.156 s % 148.37/21.44 % (1684784)Peak memory usage: 17 MB % 148.37/21.44 % (1684784)Instructions burned: 29340 (million) % 148.37/21.44 % (1685124)fmb+10_1_sil=256000:fmbss=7:random_seed=421675543:fmbsr=1.6:i=182295_2849 on theBenchmark for (2849ds/182295Mi) % 148.37/21.44 % (1685124)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.37/21.44 % (1685124)Terminated due to inappropriate strategy. % 148.37/21.44 % (1685124)------------------------------ % 148.37/21.44 % (1685124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.37/21.44 % (1685124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.37/21.44 % (1685124)CaDiCaL version: 2.1.3 % 148.37/21.44 % (1685124)Termination reason: Inappropriate % 148.37/21.44 % (1685124)Time elapsed: 0.237 s % 148.37/21.44 % (1685124)Peak memory usage: 11 MB % 148.37/21.44 % (1685124)Instructions burned: 467 (million) % 148.37/21.44 % (1685124)------------------------------ % 148.37/21.44 % (1685124)------------------------------ % 151.57/22.00 % (1685134)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3119735397:i=44625:gsp=on_2846 on theBenchmark for (2846ds/44625Mi) % 151.57/22.00 % (1685134)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.57/22.00 % (1685134)Terminated due to inappropriate strategy. % 151.57/22.00 % (1685134)------------------------------ % 151.57/22.00 % (1685134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.57/22.00 % (1685134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.57/22.00 % (1685134)CaDiCaL version: 2.1.3 % 151.57/22.00 % (1685134)Termination reason: Inappropriate % 151.57/22.00 % (1685134)Time elapsed: 0.372 s % 151.57/22.00 % (1685134)Peak memory usage: 11 MB % 151.57/22.00 % (1685134)Instructions burned: 467 (million) % 151.57/22.00 % (1685134)------------------------------ % 151.57/22.00 % (1685134)------------------------------ % 151.57/22.00 % (1685142)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4052631275:i=160505_2842 on theBenchmark for (2842ds/160505Mi) % 151.57/22.00 % (1685142)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.57/22.00 % (1685142)Terminated due to inappropriate strategy. % 151.57/22.00 % (1685142)------------------------------ % 151.57/22.00 % (1685142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.57/22.00 % (1685142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.57/22.00 % (1685142)CaDiCaL version: 2.1.3 % 151.57/22.00 % (1685142)Termination reason: Inappropriate % 151.57/22.00 % (1685142)Time elapsed: 0.382 s % 151.57/22.00 % (1685142)Peak memory usage: 11 MB % 151.57/22.00 % (1685142)Instructions burned: 467 (million) % 151.57/22.00 % (1685142)------------------------------ % 151.57/22.00 % (1685142)------------------------------ % 151.57/22.00 % (1685146)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2321901018:fmbsr=1.3:i=225729_2837 on theBenchmark for (2837ds/225729Mi) % 151.57/22.00 % (1685146)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.57/22.00 % (1685146)Terminated due to inappropriate strategy. % 151.57/22.00 % (1685146)------------------------------ % 151.57/22.00 % (1685146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.57/22.00 % (1685146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.57/22.00 % (1685146)CaDiCaL version: 2.1.3 % 151.57/22.00 % (1685146)Termination reason: Inappropriate % 151.57/22.00 % (1685146)Time elapsed: 0.352 s % 151.57/22.00 % (1685146)Peak memory usage: 11 MB % 151.57/22.00 % (1685146)Instructions burned: 467 (million) % 151.57/22.00 % (1685146)------------------------------ % 151.57/22.00 % (1685146)------------------------------ % 151.57/22.00 % (1685149)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2009461786:fmbsr=2:i=185024:ins=7_2833 on theBenchmark for (2833ds/185024Mi) % 151.57/22.00 % (1685149)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.57/22.00 % (1685149)Terminated due to inappropriate strategy. % 151.57/22.00 % (1685149)------------------------------ % 151.57/22.00 % (1685149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.57/22.00 % (1685149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.57/22.00 % (1685149)CaDiCaL version: 2.1.3 % 151.57/22.00 % (1685149)Termination reason: Inappropriate % 151.57/22.00 % (1685149)Time elapsed: 0.177 s % 151.57/22.00 % (1685149)Peak memory usage: 11 MB % 151.57/22.00 % (1685149)Instructions burned: 467 (million) % 151.57/22.00 % (1685149)------------------------------ % 151.57/22.00 % (1685149)------------------------------ % 151.57/22.00 % (1685160)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3491333669:rtra=on_2831 on theBenchmark for (2831ds/0Mi) % 151.57/22.00 % (1685160)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.57/22.00 % (1685160)Terminated due to inappropriate strategy. % 151.57/22.00 % (1685160)------------------------------ % 151.57/22.00 % (1685160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.57/22.00 % (1685160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.57/22.00 % (1685160)CaDiCaL version: 2.1.3 % 151.57/22.00 % (1685160)Termination reason: Inappropriate % 151.57/22.00 % (1685160)Time elapsed: 0.179 s % 151.57/22.00 % (1685160)Peak memory usage: 11 MB % 151.57/22.00 % (1685160)Instructions burned: 469 (million) % 151.57/22.00 % (1685160)------------------------------ % 151.57/22.00 % (1685160)------------------------------ % 151.57/22.00 % (1685232)% WARNING: option uhcvi not known. % 151.57/22.00 % (1685232)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1071885846:i=271062:add=off:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/271062Mi) % 158.14/23.01 % (1684808)Instruction limit reached! % 158.14/23.01 % (1684808)------------------------------ % 158.14/23.01 % (1684808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.14/23.01 % (1684808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.14/23.01 % (1684808)CaDiCaL version: 2.1.3 % 158.14/23.01 % (1684808)Termination reason: Instruction limit % 158.14/23.01 % (1684808)Termination phase: Saturation % 158.14/23.01 % (1684808)Time elapsed: 7.819 s % 158.14/23.01 % (1684808)Peak memory usage: 27 MB % 158.14/23.01 % (1684808)Instructions burned: 15852 (million) % 158.14/23.01 % (1685307)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2037529040:i=176048:add=on:rtra=on:rawr=on_2807 on theBenchmark for (2807ds/176048Mi) % 158.14/23.01 % (1684722)Instruction limit reached! % 158.14/23.01 % (1684722)------------------------------ % 158.14/23.01 % (1684722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.14/23.01 % (1684722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.14/23.01 % (1684722)CaDiCaL version: 2.1.3 % 158.14/23.01 % (1684722)Termination reason: Instruction limit % 158.14/23.01 % (1684722)Termination phase: Saturation % 158.14/23.01 % (1684722)Time elapsed: 20.578 s % 158.14/23.01 % (1684722)Peak memory usage: 91 MB % 158.14/23.01 % (1684722)Instructions burned: 88028 (million) % 158.14/23.01 % (1685309)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2431939403:i=206:fgj=on:rtra=on_2790 on theBenchmark for (2790ds/206Mi) % 158.14/23.01 % (1685309)Instruction limit reached! % 158.14/23.01 % (1685309)------------------------------ % 158.14/23.01 % (1685309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.14/23.01 % (1685309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.14/23.01 % (1685309)CaDiCaL version: 2.1.3 % 158.14/23.01 % (1685309)Termination reason: Instruction limit % 158.14/23.01 % (1685309)Termination phase: Property scanning % 158.14/23.01 % (1685309)Time elapsed: 0.064 s % 158.14/23.01 % (1685309)Peak memory usage: 10 MB % 158.14/23.01 % (1685309)Instructions burned: 208 (million) % 158.14/23.01 % (1685311)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=34013478:i=232:rtra=on_2789 on theBenchmark for (2789ds/232Mi) % 158.14/23.01 % (1685311)Instruction limit reached! % 158.14/23.01 % (1685311)------------------------------ % 158.14/23.01 % (1685311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.14/23.01 % (1685311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.14/23.01 % (1685311)CaDiCaL version: 2.1.3 % 158.14/23.01 % (1685311)Termination reason: Instruction limit % 158.14/23.01 % (1685311)Termination phase: Property scanning % 158.14/23.01 % (1685311)Time elapsed: 0.048 s % 158.14/23.01 % (1685311)Peak memory usage: 10 MB % 158.14/23.01 % (1685311)Instructions burned: 234 (million) % 158.14/23.01 % (1685313)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2295102116:i=262:rtra=on_2789 on theBenchmark for (2789ds/262Mi) % 158.14/23.01 % (1685313)Instruction limit reached! % 158.14/23.01 % (1685313)------------------------------ % 158.14/23.01 % (1685313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.14/23.01 % (1685313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.14/23.01 % (1685313)CaDiCaL version: 2.1.3 % 158.14/23.01 % (1685313)Termination reason: Instruction limit % 158.14/23.01 % (1685313)Termination phase: Property scanning % 158.14/23.01 % (1685313)Time elapsed: 0.055 s % 158.14/23.01 % (1685313)Peak memory usage: 11 MB % 158.14/23.01 % (1685313)Instructions burned: 267 (million) % 158.14/23.01 % (1685315)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=458048249:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2788 on theBenchmark for (2788ds/318Mi) % 158.14/23.01 % (1685315)Instruction limit reached! % 158.14/23.01 % (1685315)------------------------------ % 158.14/23.01 % (1685315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.14/23.01 % (1685315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.14/23.01 % (1685315)CaDiCaL version: 2.1.3 % 158.14/23.01 % (1685315)Termination reason: Instruction limit % 158.14/23.01 % (1685315)Termination phase: Property scanning % 158.14/23.01 % (1685315)Time elapsed: 0.064 s % 158.14/23.01 % (1685315)Peak memory usage: 11 MB % 158.14/23.01 % (1685315)Instructions burned: 319 (million) % 158.14/23.01 % (1685317)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=665048343:i=1428:nm=2:rtra=on_2787 on theBenchmark for (2787ds/1428Mi) % 171.71/24.79 % (1685317)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 171.71/24.79 % (1685317)Terminated due to inappropriate strategy. % 171.71/24.79 % (1685317)------------------------------ % 171.71/24.79 % (1685317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.71/24.79 % (1685317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.71/24.79 % (1685317)CaDiCaL version: 2.1.3 % 171.71/24.79 % (1685317)Termination reason: Inappropriate % 171.71/24.79 % (1685317)Time elapsed: 0.093 s % 171.71/24.79 % (1685317)Peak memory usage: 11 MB % 171.71/24.79 % (1685317)Instructions burned: 468 (million) % 171.71/24.79 % (1685317)------------------------------ % 171.71/24.79 % (1685317)------------------------------ % 171.71/24.79 % (1685319)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1998330326:i=262:bd=preordered:rtra=on:fsd=on_2786 on theBenchmark for (2786ds/262Mi) % 171.71/24.79 % (1685319)Instruction limit reached! % 171.71/24.79 % (1685319)------------------------------ % 171.71/24.79 % (1685319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.71/24.79 % (1685319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.71/24.79 % (1685319)CaDiCaL version: 2.1.3 % 171.71/24.79 % (1685319)Termination reason: Instruction limit % 171.71/24.79 % (1685319)Termination phase: Property scanning % 171.71/24.79 % (1685319)Time elapsed: 0.054 s % 171.71/24.79 % (1685319)Peak memory usage: 11 MB % 171.71/24.79 % (1685319)Instructions burned: 266 (million) % 171.71/24.79 % (1685321)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=3364640721:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2786 on theBenchmark for (2786ds/1368Mi) % 171.71/24.79 % (1684810)Instruction limit reached! % 171.71/24.79 % (1684810)------------------------------ % 171.71/24.79 % (1684810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.71/24.79 % (1684810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.71/24.79 % (1684810)CaDiCaL version: 2.1.3 % 171.71/24.79 % (1684810)Termination reason: Instruction limit % 171.71/24.79 % (1684810)Termination phase: Saturation % 171.71/24.79 % (1684810)Time elapsed: 8.734 s % 171.71/24.79 % (1684810)Peak memory usage: 93 MB % 171.71/24.79 % (1684810)Instructions burned: 17628 (million) % 171.71/24.79 % (1685323)ott-21_1_sil=16000:si=on:fs=off:random_seed=3304197060:i=360:av=off:fsr=off:rtra=on_2785 on theBenchmark for (2785ds/360Mi) % 171.71/24.79 % (1685323)Instruction limit reached! % 171.71/24.79 % (1685323)------------------------------ % 171.71/24.79 % (1685323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.71/24.79 % (1685323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.71/24.79 % (1685323)CaDiCaL version: 2.1.3 % 171.71/24.79 % (1685323)Termination reason: Instruction limit % 171.71/24.79 % (1685323)Termination phase: Property scanning % 171.71/24.79 % (1685323)Time elapsed: 0.138 s % 171.71/24.79 % (1685323)Peak memory usage: 11 MB % 171.71/24.79 % (1685323)Instructions burned: 362 (million) % 171.71/24.79 % (1685325)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1334093607:i=954:bd=all:rtra=on_2784 on theBenchmark for (2784ds/954Mi) % 171.71/24.79 % (1685321)Instruction limit reached! % 171.71/24.79 % (1685321)------------------------------ % 171.71/24.79 % (1685321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.71/24.79 % (1685321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.71/24.79 % (1685321)CaDiCaL version: 2.1.3 % 171.71/24.79 % (1685321)Termination reason: Instruction limit % 171.71/24.79 % (1685321)Termination phase: Saturation % 171.71/24.79 % (1685321)Time elapsed: 0.311 s % 171.71/24.79 % (1685321)Peak memory usage: 18 MB % 171.71/24.79 % (1685321)Instructions burned: 1369 (million) % 171.71/24.79 % (1685327)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1427839249:fmbsr=1.3:i=1730:ins=25:rtra=on_2783 on theBenchmark for (2783ds/1730Mi) % 171.71/24.79 % (1685327)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 171.71/24.79 % (1685327)Terminated due to inappropriate strategy. % 171.71/24.79 % (1685327)------------------------------ % 171.71/24.79 % (1685327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.71/24.79 % (1685327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.40/27.65 % (1685327)CaDiCaL version: 2.1.3 % 192.40/27.65 % (1685327)Termination reason: Inappropriate % 192.40/27.65 % (1685327)Time elapsed: 0.072 s % 192.40/27.65 % (1685327)Peak memory usage: 11 MB % 192.40/27.65 % (1685327)Instructions burned: 355 (million) % 192.40/27.65 % (1685327)------------------------------ % 192.40/27.65 % (1685327)------------------------------ % 192.40/27.65 % (1685329)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4237921600:i=2358:rtra=on_2782 on theBenchmark for (2782ds/2358Mi) % 192.40/27.65 % (1685325)Instruction limit reached! % 192.40/27.65 % (1685325)------------------------------ % 192.40/27.65 % (1685325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.40/27.65 % (1685325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.40/27.65 % (1685325)CaDiCaL version: 2.1.3 % 192.40/27.65 % (1685325)Termination reason: Instruction limit % 192.40/27.65 % (1685325)Termination phase: Saturation % 192.40/27.65 % (1685325)Time elapsed: 0.384 s % 192.40/27.65 % (1685325)Peak memory usage: 15 MB % 192.40/27.65 % (1685325)Instructions burned: 957 (million) % 192.40/27.65 % (1685331)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3327746862:i=1778:ins=1:rtra=on_2780 on theBenchmark for (2780ds/1778Mi) % 192.40/27.65 % (1685331)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.40/27.65 % (1685331)Terminated due to inappropriate strategy. % 192.40/27.65 % (1685331)------------------------------ % 192.40/27.65 % (1685331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.40/27.65 % (1685331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.40/27.65 % (1685331)CaDiCaL version: 2.1.3 % 192.40/27.65 % (1685331)Termination reason: Inappropriate % 192.40/27.65 % (1685331)Time elapsed: 0.136 s % 192.40/27.65 % (1685331)Peak memory usage: 11 MB % 192.40/27.65 % (1685331)Instructions burned: 356 (million) % 192.40/27.65 % (1685331)------------------------------ % 192.40/27.65 % (1685331)------------------------------ % 192.40/27.65 % (1685333)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=3096591596:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2778 on theBenchmark for (2778ds/1384Mi) % 192.40/27.65 % (1685329)Instruction limit reached! % 192.40/27.65 % (1685329)------------------------------ % 192.40/27.65 % (1685329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.40/27.65 % (1685329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.40/27.65 % (1685329)CaDiCaL version: 2.1.3 % 192.40/27.65 % (1685329)Termination reason: Instruction limit % 192.40/27.65 % (1685329)Termination phase: Saturation % 192.40/27.65 % (1685329)Time elapsed: 0.507 s % 192.40/27.65 % (1685329)Peak memory usage: 16 MB % 192.40/27.65 % (1685329)Instructions burned: 2360 (million) % 192.40/27.65 % (1685335)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=192468579:i=1758:kws=inv_precedence:fsr=off:rtra=on_2777 on theBenchmark for (2777ds/1758Mi) % 192.40/27.65 % (1685335)Instruction limit reached! % 192.40/27.65 % (1685335)------------------------------ % 192.40/27.65 % (1685335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.40/27.65 % (1685335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.40/27.65 % (1685335)CaDiCaL version: 2.1.3 % 192.40/27.65 % (1685335)Termination reason: Instruction limit % 192.40/27.65 % (1685335)Termination phase: Saturation % 192.40/27.65 % (1685335)Time elapsed: 0.371 s % 192.40/27.65 % (1685335)Peak memory usage: 15 MB % 192.40/27.65 % (1685335)Instructions burned: 1759 (million) % 192.40/27.65 % (1685337)fmb+10_1_sil=64000:si=on:random_seed=774623274:i=44122:nm=2:rtra=on:gsp=on_2773 on theBenchmark for (2773ds/44122Mi) % 192.40/27.65 % (1685333)Instruction limit reached! % 192.40/27.65 % (1685333)------------------------------ % 192.40/27.65 % (1685333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.40/27.65 % (1685333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.40/27.65 % (1685333)CaDiCaL version: 2.1.3 % 192.40/27.65 % (1685333)Termination reason: Instruction limit % 192.40/27.65 % (1685333)Termination phase: Saturation % 192.40/27.65 % (1685333)Time elapsed: 0.576 s % 192.40/27.65 % (1685333)Peak memory usage: 17 MB % 192.40/27.65 % (1685333)Instructions burned: 1384 (million) % 192.40/27.65 % (1685339)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1672531877:i=19030:nm=5:rtra=on_2772 on theBenchmark for (2772ds/19030Mi) % 229.86/32.96 % (1685337)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.86/32.96 % (1685337)Terminated due to inappropriate strategy. % 229.86/32.96 % (1685337)------------------------------ % 229.86/32.96 % (1685337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.86/32.96 % (1685337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.86/32.96 % (1685337)CaDiCaL version: 2.1.3 % 229.86/32.96 % (1685337)Termination reason: Inappropriate % 229.86/32.96 % (1685337)Time elapsed: 0.094 s % 229.86/32.96 % (1685337)Peak memory usage: 11 MB % 229.86/32.96 % (1685337)Instructions burned: 468 (million) % 229.86/32.96 % (1685337)------------------------------ % 229.86/32.96 % (1685337)------------------------------ % 229.86/32.96 % (1685341)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=115191396:fmbsr=1.7:i=1840:rtra=on_2772 on theBenchmark for (2772ds/1840Mi) % 229.86/32.96 % (1685341)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.86/32.96 % (1685341)Terminated due to inappropriate strategy. % 229.86/32.96 % (1685341)------------------------------ % 229.86/32.96 % (1685341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.86/32.96 % (1685341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.86/32.96 % (1685341)CaDiCaL version: 2.1.3 % 229.86/32.96 % (1685341)Termination reason: Inappropriate % 229.86/32.96 % (1685341)Time elapsed: 0.093 s % 229.86/32.96 % (1685341)Peak memory usage: 11 MB % 229.86/32.96 % (1685341)Instructions burned: 468 (million) % 229.86/32.96 % (1685341)------------------------------ % 229.86/32.96 % (1685341)------------------------------ % 229.86/32.96 % (1685343)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=642351057:i=10262:rtra=on_2771 on theBenchmark for (2771ds/10262Mi) % 229.86/32.96 % (1685339)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.86/32.96 % (1685339)Terminated due to inappropriate strategy. % 229.86/32.96 % (1685339)------------------------------ % 229.86/32.96 % (1685339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.86/32.96 % (1685339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.86/32.96 % (1685339)CaDiCaL version: 2.1.3 % 229.86/32.96 % (1685339)Termination reason: Inappropriate % 229.86/32.96 % (1685339)Time elapsed: 0.178 s % 229.86/32.96 % (1685339)Peak memory usage: 11 MB % 229.86/32.96 % (1685339)Instructions burned: 468 (million) % 229.86/32.96 % (1685339)------------------------------ % 229.86/32.96 % (1685339)------------------------------ % 229.86/32.96 % (1685345)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1642582646:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2770 on theBenchmark for (2770ds/2944Mi) % 229.86/32.96 % (1685345)Instruction limit reached! % 229.86/32.96 % (1685345)------------------------------ % 229.86/32.96 % (1685345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.86/32.96 % (1685345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.86/32.96 % (1685345)CaDiCaL version: 2.1.3 % 229.86/32.96 % (1685345)Termination reason: Instruction limit % 229.86/32.96 % (1685345)Termination phase: Saturation % 229.86/32.96 % (1685345)Time elapsed: 1.208 s % 229.86/32.96 % (1685345)Peak memory usage: 19 MB % 229.86/32.96 % (1685345)Instructions burned: 2946 (million) % 229.86/32.96 % (1685347)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3354426251:i=12648:rtra=on_2758 on theBenchmark for (2758ds/12648Mi) % 229.86/32.96 % (1685347)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.86/32.96 % (1685347)Terminated due to inappropriate strategy. % 229.86/32.96 % (1685347)------------------------------ % 229.86/32.96 % (1685347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.86/32.96 % (1685347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.86/32.96 % (1685347)CaDiCaL version: 2.1.3 % 229.86/32.96 % (1685347)Termination reason: Inappropriate % 229.86/32.96 % (1685347)Time elapsed: 0.177 s % 229.86/32.96 % (1685347)Peak memory usage: 11 MB % 229.86/32.96 % (1685347)Instructions burned: 468 (million) % 229.86/32.96 % (1685347)------------------------------ % 229.86/32.96 % (1685347)------------------------------ % 229.86/32.96 % (1685349)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3986687381:fmbsr=2.30978:i=4348:rtra=on_2756 on theBenchmark for (2756ds/4348Mi) % 229.86/32.96 % (1685349)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.06/40.89 % (1685349)Terminated due to inappropriate strategy. % 286.06/40.89 % (1685349)------------------------------ % 286.06/40.89 % (1685349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/40.89 % (1685349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/40.89 % (1685349)CaDiCaL version: 2.1.3 % 286.06/40.89 % (1685349)Termination reason: Inappropriate % 286.06/40.89 % (1685349)Time elapsed: 0.177 s % 286.06/40.89 % (1685349)Peak memory usage: 11 MB % 286.06/40.89 % (1685349)Instructions burned: 469 (million) % 286.06/40.89 % (1685349)------------------------------ % 286.06/40.89 % (1685349)------------------------------ % 286.06/40.89 % (1685351)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2308871872:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2754 on theBenchmark for (2754ds/1738Mi) % 286.06/40.89 % (1685343)Instruction limit reached! % 286.06/40.89 % (1685343)------------------------------ % 286.06/40.89 % (1685343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/40.89 % (1685343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/40.89 % (1685343)CaDiCaL version: 2.1.3 % 286.06/40.89 % (1685343)Termination reason: Instruction limit % 286.06/40.89 % (1685343)Termination phase: Saturation % 286.06/40.89 % (1685343)Time elapsed: 2.398 s % 286.06/40.89 % (1685343)Peak memory usage: 25 MB % 286.06/40.89 % (1685343)Instructions burned: 10263 (million) % 286.06/40.89 % (1685353)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2582289898:i=10228:av=off:rtra=on_2746 on theBenchmark for (2746ds/10228Mi) % 286.06/40.89 % (1685351)Instruction limit reached! % 286.06/40.89 % (1685351)------------------------------ % 286.06/40.89 % (1685351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/40.89 % (1685351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/40.89 % (1685351)CaDiCaL version: 2.1.3 % 286.06/40.89 % (1685351)Termination reason: Instruction limit % 286.06/40.89 % (1685351)Termination phase: Saturation % 286.06/40.89 % (1685351)Time elapsed: 0.731 s % 286.06/40.89 % (1685351)Peak memory usage: 15 MB % 286.06/40.89 % (1685351)Instructions burned: 1738 (million) % 286.06/40.89 % (1685355)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=216854272:i=108564:rtra=on_2746 on theBenchmark for (2746ds/108564Mi) % 286.06/40.89 % (1685355)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.06/40.89 % (1685355)Terminated due to inappropriate strategy. % 286.06/40.89 % (1685355)------------------------------ % 286.06/40.89 % (1685355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/40.89 % (1685355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/40.89 % (1685355)CaDiCaL version: 2.1.3 % 286.06/40.89 % (1685355)Termination reason: Inappropriate % 286.06/40.89 % (1685355)Time elapsed: 0.177 s % 286.06/40.89 % (1685355)Peak memory usage: 11 MB % 286.06/40.89 % (1685355)Instructions burned: 468 (million) % 286.06/40.89 % (1685355)------------------------------ % 286.06/40.89 % (1685355)------------------------------ % 286.06/40.89 % (1685007)Instruction limit reached! % 286.06/40.89 % (1685007)------------------------------ % 286.06/40.89 % (1685007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/40.89 % (1685007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/40.89 % (1685007)CaDiCaL version: 2.1.3 % 286.06/40.89 % (1685007)Termination reason: Instruction limit % 286.06/40.89 % (1685007)Termination phase: Saturation % 286.06/40.89 % (1685007)Time elapsed: 11.633 s % 286.06/40.89 % (1685007)Peak memory usage: 29 MB % 286.06/40.89 % (1685007)Instructions burned: 28122 (million) % 286.06/40.89 % (1685357)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2863773033:i=7024:aac=none:rtra=on_2744 on theBenchmark for (2744ds/7024Mi) % 286.06/40.89 % (1685358)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=693972905:i=7546:rtra=on:amm=off_2744 on theBenchmark for (2744ds/7546Mi) % 286.06/40.89 % (1685353)Instruction limit reached! % 286.06/40.89 % (1685353)------------------------------ % 286.06/40.89 % (1685353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/40.89 % (1685353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/40.89 % (1685353)CaDiCaL version: 2.1.3 % 286.06/40.89 % (1685353)Termination reason: Instruction limit % 286.06/40.89 % (1685353)Termination phase: Saturation % 286.06/40.89 % (1685353)Time elapsed: 2.100 s % 286.06/40.89 % (1685353)Peak memory usage: 29 MB % 286.06/40.89 % (1685353)Instructions burned: 10232 (million) % 286.06/40.89 % (1685361)ott+11_1_Terminated % 300.27/42.84 % Vampire exiting %------------------------------------------------------------------------------