%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW001_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:38:10 PM UTC 2026 % Result : Timeout 300.27s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW001_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.12/0.24 % Computer : n018.cluster.edu % 0.12/0.24 % Model : x86_64 x86_64 % 0.12/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.24 % Memory : 8046.5625MB % 0.12/0.24 % OS : Linux 6.8.0-71-generic % 0.12/0.24 % CPULimit : 300 % 0.12/0.24 % WCLimit : 300 % 0.12/0.24 % DateTime : Mon Sep 28 13:10:10 UTC 2026 % 0.12/0.25 % CPUTime : % 0.12/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.12/0.29 Running first-order model finding % 0.12/0.29 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 % 6.10/1.20 % (3370301)Will run a generic schedule for satisfiability detection. % 6.10/1.20 % (3370308)% WARNING: option uhcvi not known. % 6.10/1.20 % (3370308)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3497477654:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.10/1.20 % (3370310)dis+10_1_sil=32000:sp=arity:random_seed=1779633657:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.10/1.20 % (3370312)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=613207476:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.10/1.20 % (3370309)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=542390249:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.10/1.20 % (3370311)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2095829616:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.10/1.20 % (3370307)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2491001609_2999 on theBenchmark for (2999ds/0Mi) % 6.10/1.20 % (3370313)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1475354783:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.10/1.20 % (3370307)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.10/1.20 % (3370307)Terminated due to inappropriate strategy. % 6.10/1.20 % (3370307)------------------------------ % 6.10/1.20 % (3370307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.10/1.20 % (3370307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.20 % (3370307)CaDiCaL version: 2.1.3 % 6.10/1.20 % (3370307)Termination reason: Inappropriate % 6.10/1.20 % (3370307)Time elapsed: 0.009 s % 6.10/1.20 % (3370307)Peak memory usage: 10 MB % 6.10/1.20 % (3370307)Instructions burned: 10 (million) % 6.10/1.20 % (3370307)------------------------------ % 6.10/1.20 % (3370307)------------------------------ % 6.10/1.20 % (3370322)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1275381028:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.10/1.20 % (3370322)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.10/1.20 % (3370322)Terminated due to inappropriate strategy. % 6.10/1.20 % (3370322)------------------------------ % 6.10/1.20 % (3370322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.10/1.20 % (3370322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.20 % (3370322)CaDiCaL version: 2.1.3 % 6.10/1.20 % (3370322)Termination reason: Inappropriate % 6.10/1.20 % (3370322)Time elapsed: 0.005 s % 6.10/1.20 % (3370322)Peak memory usage: 10 MB % 6.10/1.20 % (3370322)Instructions burned: 10 (million) % 6.10/1.20 % (3370322)------------------------------ % 6.10/1.20 % (3370322)------------------------------ % 6.10/1.20 % (3370310)Instruction limit reached! % 6.10/1.20 % (3370310)------------------------------ % 6.10/1.20 % (3370310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.10/1.20 % (3370310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.20 % (3370310)CaDiCaL version: 2.1.3 % 6.10/1.20 % (3370310)Termination reason: Instruction limit % 6.10/1.20 % (3370310)Termination phase: Saturation % 6.10/1.20 % (3370310)Time elapsed: 0.083 s % 6.10/1.20 % (3370310)Peak memory usage: 13 MB % 6.10/1.20 % (3370310)Instructions burned: 103 (million) % 6.10/1.20 % (3370312)Instruction limit reached! % 6.10/1.20 % (3370312)------------------------------ % 6.10/1.20 % (3370312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.10/1.20 % (3370312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.20 % (3370312)CaDiCaL version: 2.1.3 % 6.10/1.20 % (3370312)Termination reason: Instruction limit % 6.10/1.20 % (3370312)Termination phase: Saturation % 6.10/1.20 % (3370312)Time elapsed: 0.093 s % 6.10/1.20 % (3370312)Peak memory usage: 12 MB % 6.10/1.20 % (3370312)Instructions burned: 132 (million) % 6.10/1.20 % (3370311)Instruction limit reached! % 6.10/1.20 % (3370311)------------------------------ % 6.10/1.20 % (3370311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.10/1.20 % (3370311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.20 % (3370311)CaDiCaL version: 2.1.3 % 6.10/1.20 % (3370311)Termination reason: Instruction limit % 6.10/1.20 % (3370311)Termination phase: Saturation % 6.10/1.20 % (3370311)Time elapsed: 0.097 s % 6.10/1.20 % (3370311)Peak memory usage: 13 MB % 6.10/1.20 % (3370311)Instructions burned: 117 (million) % 7.64/1.64 % (3370326)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2839631672:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 7.64/1.64 % (3370327)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=403091085:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.64/1.64 % (3370329)ott-21_1_sil=16000:fs=off:random_seed=3960940055:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.64/1.64 % (3370332)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1840731323:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.64/1.64 % (3370313)Instruction limit reached! % 7.64/1.64 % (3370313)------------------------------ % 7.64/1.64 % (3370313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.64/1.64 % (3370313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.64/1.64 % (3370313)CaDiCaL version: 2.1.3 % 7.64/1.64 % (3370313)Termination reason: Instruction limit % 7.64/1.64 % (3370313)Termination phase: Saturation % 7.64/1.64 % (3370313)Time elapsed: 0.162 s % 7.64/1.64 % (3370313)Peak memory usage: 13 MB % 7.64/1.64 % (3370313)Instructions burned: 159 (million) % 7.64/1.64 % (3370326)Instruction limit reached! % 7.64/1.64 % (3370326)------------------------------ % 7.64/1.64 % (3370326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.64/1.64 % (3370326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.64/1.64 % (3370326)CaDiCaL version: 2.1.3 % 7.64/1.64 % (3370326)Termination reason: Instruction limit % 7.64/1.64 % (3370326)Termination phase: Saturation % 7.64/1.64 % (3370326)Time elapsed: 0.103 s % 7.64/1.64 % (3370326)Peak memory usage: 12 MB % 7.64/1.64 % (3370326)Instructions burned: 132 (million) % 7.64/1.64 % (3370339)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1660778900:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 7.64/1.64 % (3370339)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.64/1.64 % (3370339)Terminated due to inappropriate strategy. % 7.64/1.64 % (3370339)------------------------------ % 7.64/1.64 % (3370339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.64/1.64 % (3370339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.64/1.64 % (3370339)CaDiCaL version: 2.1.3 % 7.64/1.64 % (3370339)Termination reason: Inappropriate % 7.64/1.64 % (3370339)Time elapsed: 0.009 s % 7.64/1.64 % (3370339)Peak memory usage: 11 MB % 7.64/1.64 % (3370339)Instructions burned: 10 (million) % 7.64/1.64 % (3370339)------------------------------ % 7.64/1.64 % (3370339)------------------------------ % 7.64/1.64 % (3370340)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2693770073:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.64/1.64 % (3370329)Instruction limit reached! % 7.64/1.64 % (3370329)------------------------------ % 7.64/1.64 % (3370329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.64/1.64 % (3370329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.64/1.64 % (3370329)CaDiCaL version: 2.1.3 % 7.64/1.64 % (3370329)Termination reason: Instruction limit % 7.64/1.64 % (3370329)Termination phase: Saturation % 7.64/1.64 % (3370329)Time elapsed: 0.125 s % 7.64/1.64 % (3370329)Peak memory usage: 12 MB % 7.64/1.64 % (3370329)Instructions burned: 180 (million) % 7.64/1.64 % (3370343)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3312430643:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.64/1.64 % (3370343)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.64/1.64 % (3370343)Terminated due to inappropriate strategy. % 7.64/1.64 % (3370343)------------------------------ % 7.64/1.64 % (3370343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.64/1.64 % (3370343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.64/1.64 % (3370343)CaDiCaL version: 2.1.3 % 7.64/1.64 % (3370343)Termination reason: Inappropriate % 7.64/1.64 % (3370343)Time elapsed: 0.013 s % 7.64/1.64 % (3370343)Peak memory usage: 11 MB % 7.64/1.64 % (3370343)Instructions burned: 15 (million) % 7.64/1.64 % (3370343)------------------------------ % 7.64/1.64 % (3370343)------------------------------ % 7.64/1.64 % (3370346)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=1315636972:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 31.03/4.73 % (3370350)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4190557110:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 31.03/4.73 % (3370332)Instruction limit reached! % 31.03/4.73 % (3370332)------------------------------ % 31.03/4.73 % (3370332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.03/4.73 % (3370332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.03/4.73 % (3370332)CaDiCaL version: 2.1.3 % 31.03/4.73 % (3370332)Termination reason: Instruction limit % 31.03/4.73 % (3370332)Termination phase: Saturation % 31.03/4.73 % (3370332)Time elapsed: 0.426 s % 31.03/4.73 % (3370332)Peak memory usage: 14 MB % 31.03/4.73 % (3370332)Instructions burned: 477 (million) % 31.03/4.73 % (3370366)fmb+10_1_sil=64000:random_seed=4283556176:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 31.03/4.73 % (3370366)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.03/4.73 % (3370366)Terminated due to inappropriate strategy. % 31.03/4.73 % (3370366)------------------------------ % 31.03/4.73 % (3370366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.03/4.73 % (3370366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.03/4.73 % (3370366)CaDiCaL version: 2.1.3 % 31.03/4.73 % (3370366)Termination reason: Inappropriate % 31.03/4.73 % (3370366)Time elapsed: 0.009 s % 31.03/4.73 % (3370366)Peak memory usage: 10 MB % 31.03/4.73 % (3370366)Instructions burned: 11 (million) % 31.03/4.73 % (3370366)------------------------------ % 31.03/4.73 % (3370366)------------------------------ % 31.03/4.73 % (3370371)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=127435205:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 31.03/4.73 % (3370371)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.03/4.73 % (3370371)Terminated due to inappropriate strategy. % 31.03/4.73 % (3370371)------------------------------ % 31.03/4.73 % (3370371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.03/4.73 % (3370371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.03/4.73 % (3370371)CaDiCaL version: 2.1.3 % 31.03/4.73 % (3370371)Termination reason: Inappropriate % 31.03/4.73 % (3370371)Time elapsed: 0.009 s % 31.03/4.73 % (3370371)Peak memory usage: 11 MB % 31.03/4.73 % (3370371)Instructions burned: 10 (million) % 31.03/4.73 % (3370371)------------------------------ % 31.03/4.73 % (3370371)------------------------------ % 31.03/4.73 % (3370327)Instruction limit reached! % 31.03/4.73 % (3370327)------------------------------ % 31.03/4.73 % (3370327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.03/4.73 % (3370327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.03/4.73 % (3370327)CaDiCaL version: 2.1.3 % 31.03/4.73 % (3370327)Termination reason: Instruction limit % 31.03/4.73 % (3370327)Termination phase: Saturation % 31.03/4.73 % (3370327)Time elapsed: 0.571 s % 31.03/4.73 % (3370327)Peak memory usage: 18 MB % 31.03/4.73 % (3370327)Instructions burned: 685 (million) % 31.03/4.73 % (3370374)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2818160254:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 31.03/4.73 % (3370374)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.03/4.73 % (3370374)Terminated due to inappropriate strategy. % 31.03/4.73 % (3370374)------------------------------ % 31.03/4.73 % (3370374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.03/4.73 % (3370374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.03/4.73 % (3370374)CaDiCaL version: 2.1.3 % 31.03/4.73 % (3370374)Termination reason: Inappropriate % 31.03/4.73 % (3370374)Time elapsed: 0.009 s % 31.03/4.73 % (3370374)Peak memory usage: 10 MB % 31.03/4.73 % (3370374)Instructions burned: 10 (million) % 31.03/4.73 % (3370374)------------------------------ % 31.03/4.73 % (3370374)------------------------------ % 31.03/4.73 % (3370379)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=498370411:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 31.03/4.73 % (3370380)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3127857940:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 31.03/4.73 % (3370346)Instruction limit reached! % 31.03/4.73 % (3370346)------------------------------ % 56.20/8.21 % (3370346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.21 % (3370346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.21 % (3370346)CaDiCaL version: 2.1.3 % 56.20/8.21 % (3370346)Termination reason: Instruction limit % 56.20/8.21 % (3370346)Termination phase: Saturation % 56.20/8.21 % (3370346)Time elapsed: 0.585 s % 56.20/8.21 % (3370346)Peak memory usage: 18 MB % 56.20/8.21 % (3370346)Instructions burned: 692 (million) % 56.20/8.21 % (3370389)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2852801873:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 56.20/8.21 % (3370389)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 56.20/8.21 % (3370389)Terminated due to inappropriate strategy. % 56.20/8.21 % (3370389)------------------------------ % 56.20/8.21 % (3370389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.21 % (3370389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.21 % (3370389)CaDiCaL version: 2.1.3 % 56.20/8.21 % (3370389)Termination reason: Inappropriate % 56.20/8.21 % (3370389)Time elapsed: 0.006 s % 56.20/8.21 % (3370389)Peak memory usage: 11 MB % 56.20/8.21 % (3370389)Instructions burned: 10 (million) % 56.20/8.21 % (3370389)------------------------------ % 56.20/8.21 % (3370389)------------------------------ % 56.20/8.21 % (3370391)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1395619579:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 56.20/8.21 % (3370391)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 56.20/8.21 % (3370391)Terminated due to inappropriate strategy. % 56.20/8.21 % (3370391)------------------------------ % 56.20/8.21 % (3370391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.21 % (3370391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.21 % (3370391)CaDiCaL version: 2.1.3 % 56.20/8.21 % (3370391)Termination reason: Inappropriate % 56.20/8.21 % (3370391)Time elapsed: 0.006 s % 56.20/8.21 % (3370391)Peak memory usage: 11 MB % 56.20/8.21 % (3370391)Instructions burned: 10 (million) % 56.20/8.21 % (3370391)------------------------------ % 56.20/8.21 % (3370391)------------------------------ % 56.20/8.21 % (3370395)ott-2_1_sil=16000:newcnf=on:random_seed=811731516:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 56.20/8.21 % (3370350)Instruction limit reached! % 56.20/8.21 % (3370350)------------------------------ % 56.20/8.21 % (3370350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.21 % (3370350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.21 % (3370350)CaDiCaL version: 2.1.3 % 56.20/8.21 % (3370350)Termination reason: Instruction limit % 56.20/8.21 % (3370350)Termination phase: Saturation % 56.20/8.21 % (3370350)Time elapsed: 0.773 s % 56.20/8.21 % (3370350)Peak memory usage: 19 MB % 56.20/8.21 % (3370350)Instructions burned: 879 (million) % 56.20/8.21 % (3370401)ott+10_1_sil=32000:tgt=ground:random_seed=2897450877:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi) % 56.20/8.21 % (3370340)Instruction limit reached! % 56.20/8.21 % (3370340)------------------------------ % 56.20/8.21 % (3370340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.21 % (3370340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.21 % (3370340)CaDiCaL version: 2.1.3 % 56.20/8.21 % (3370340)Termination reason: Instruction limit % 56.20/8.21 % (3370340)Termination phase: Saturation % 56.20/8.21 % (3370340)Time elapsed: 1.021 s % 56.20/8.21 % (3370340)Peak memory usage: 18 MB % 56.20/8.21 % (3370340)Instructions burned: 1180 (million) % 56.20/8.21 % (3370407)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=119112879:i=54282_2986 on theBenchmark for (2986ds/54282Mi) % 56.20/8.21 % (3370407)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 56.20/8.21 % (3370407)Terminated due to inappropriate strategy. % 56.20/8.21 % (3370407)------------------------------ % 56.20/8.21 % (3370407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.21 % (3370407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.21 % (3370407)CaDiCaL version: 2.1.3 % 56.20/8.21 % (3370407)Termination reason: Inappropriate % 56.20/8.21 % (3370407)Time elapsed: 0.006 s % 56.20/8.21 % (3370407)Peak memory usage: 11 MB % 56.20/8.21 % (3370407)Instructions burned: 10 (million) % 186.49/26.50 % (3370407)------------------------------ % 186.49/26.50 % (3370407)------------------------------ % 186.49/26.50 % (3370412)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=454977229:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 186.49/26.50 % (3370395)Instruction limit reached! % 186.49/26.50 % (3370395)------------------------------ % 186.49/26.50 % (3370395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.49/26.50 % (3370395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.49/26.50 % (3370395)CaDiCaL version: 2.1.3 % 186.49/26.50 % (3370395)Termination reason: Instruction limit % 186.49/26.50 % (3370395)Termination phase: Saturation % 186.49/26.50 % (3370395)Time elapsed: 0.853 s % 186.49/26.50 % (3370395)Peak memory usage: 17 MB % 186.49/26.50 % (3370395)Instructions burned: 869 (million) % 186.49/26.50 % (3370425)dis+21_1_sil=32000:sas=cadical:random_seed=2015504536:i=3773:amm=off_2981 on theBenchmark for (2981ds/3773Mi) % 186.49/26.50 % (3370380)Instruction limit reached! % 186.49/26.50 % (3370380)------------------------------ % 186.49/26.50 % (3370380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.49/26.50 % (3370380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.49/26.50 % (3370380)CaDiCaL version: 2.1.3 % 186.49/26.50 % (3370380)Termination reason: Instruction limit % 186.49/26.50 % (3370380)Termination phase: Saturation % 186.49/26.50 % (3370380)Time elapsed: 1.361 s % 186.49/26.50 % (3370380)Peak memory usage: 26 MB % 186.49/26.50 % (3370380)Instructions burned: 1472 (million) % 186.49/26.50 % (3370435)ott+11_1_sil=16000:gs=on:random_seed=1063993994:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 186.49/26.50 % (3370435)Instruction limit reached! % 186.49/26.50 % (3370435)------------------------------ % 186.49/26.50 % (3370435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.49/26.50 % (3370435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.49/26.50 % (3370435)CaDiCaL version: 2.1.3 % 186.49/26.50 % (3370435)Termination reason: Instruction limit % 186.49/26.50 % (3370435)Termination phase: Saturation % 186.49/26.50 % (3370435)Time elapsed: 1.949 s % 186.49/26.50 % (3370435)Peak memory usage: 22 MB % 186.49/26.50 % (3370435)Instructions burned: 2252 (million) % 186.49/26.50 % (3370482)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1784256647:fmbsr=1.6:i=67534_2958 on theBenchmark for (2958ds/67534Mi) % 186.49/26.50 % (3370482)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.49/26.50 % (3370482)Terminated due to inappropriate strategy. % 186.49/26.50 % (3370482)------------------------------ % 186.49/26.50 % (3370482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.49/26.50 % (3370482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.49/26.50 % (3370482)CaDiCaL version: 2.1.3 % 186.49/26.50 % (3370482)Termination reason: Inappropriate % 186.49/26.50 % (3370482)Time elapsed: 0.012 s % 186.49/26.50 % (3370482)Peak memory usage: 11 MB % 186.49/26.50 % (3370482)Instructions burned: 15 (million) % 186.49/26.50 % (3370482)------------------------------ % 186.49/26.50 % (3370482)------------------------------ % 186.49/26.50 % (3370484)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3846565848:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2958 on theBenchmark for (2958ds/4591Mi) % 186.49/26.50 % (3370425)Instruction limit reached! % 186.49/26.50 % (3370425)------------------------------ % 186.49/26.50 % (3370425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.49/26.50 % (3370425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.49/26.50 % (3370425)CaDiCaL version: 2.1.3 % 186.49/26.50 % (3370425)Termination reason: Instruction limit % 186.49/26.50 % (3370425)Termination phase: Saturation % 186.49/26.50 % (3370425)Time elapsed: 2.416 s % 186.49/26.50 % (3370425)Peak memory usage: 19 MB % 186.49/26.50 % (3370425)Instructions burned: 3773 (million) % 186.49/26.50 % (3370491)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4207301660:i=29340_2956 on theBenchmark for (2956ds/29340Mi) % 186.49/26.50 % (3370412)Instruction limit reached! % 186.49/26.50 % (3370412)------------------------------ % 186.49/26.50 % (3370412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.49/26.50 % (3370412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.49/26.50 % (3370412)CaDiCaL version: 2.1.3 % 186.49/26.50 % (3370412)Termination reason: Instruction limit % 222.05/31.54 % (3370412)Termination phase: Saturation % 222.05/31.54 % (3370412)Time elapsed: 3.065 s % 222.05/31.54 % (3370412)Peak memory usage: 28 MB % 222.05/31.54 % (3370412)Instructions burned: 3513 (million) % 222.05/31.54 % (3370493)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1760918067:i=5211_2955 on theBenchmark for (2955ds/5211Mi) % 222.05/31.54 % (3370379)Instruction limit reached! % 222.05/31.54 % (3370379)------------------------------ % 222.05/31.54 % (3370379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.05/31.54 % (3370379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.05/31.54 % (3370379)CaDiCaL version: 2.1.3 % 222.05/31.54 % (3370379)Termination reason: Instruction limit % 222.05/31.54 % (3370379)Termination phase: Saturation % 222.05/31.54 % (3370379)Time elapsed: 4.341 s % 222.05/31.54 % (3370379)Peak memory usage: 40 MB % 222.05/31.54 % (3370379)Instructions burned: 5131 (million) % 222.05/31.54 % (3370507)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1883887074:i=5497:nm=2_2949 on theBenchmark for (2949ds/5497Mi) % 222.05/31.54 % (3370507)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.05/31.54 % (3370507)Terminated due to inappropriate strategy. % 222.05/31.54 % (3370507)------------------------------ % 222.05/31.54 % (3370507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.05/31.54 % (3370507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.05/31.54 % (3370507)CaDiCaL version: 2.1.3 % 222.05/31.54 % (3370507)Termination reason: Inappropriate % 222.05/31.54 % (3370507)Time elapsed: 0.008 s % 222.05/31.54 % (3370507)Peak memory usage: 10 MB % 222.05/31.54 % (3370507)Instructions burned: 10 (million) % 222.05/31.54 % (3370507)------------------------------ % 222.05/31.54 % (3370507)------------------------------ % 222.05/31.54 % (3370509)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2215269518:fmbsr=2:i=46332_2948 on theBenchmark for (2948ds/46332Mi) % 222.05/31.54 % (3370509)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.05/31.54 % (3370509)Terminated due to inappropriate strategy. % 222.05/31.54 % (3370509)------------------------------ % 222.05/31.54 % (3370509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.05/31.54 % (3370509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.05/31.54 % (3370509)CaDiCaL version: 2.1.3 % 222.05/31.54 % (3370509)Termination reason: Inappropriate % 222.05/31.54 % (3370509)Time elapsed: 0.011 s % 222.05/31.54 % (3370509)Peak memory usage: 11 MB % 222.05/31.54 % (3370509)Instructions burned: 15 (million) % 222.05/31.54 % (3370509)------------------------------ % 222.05/31.54 % (3370509)------------------------------ % 222.05/31.54 % (3370511)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=700052149:i=14071_2948 on theBenchmark for (2948ds/14071Mi) % 222.05/31.54 % (3370511)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.05/31.54 % (3370511)Terminated due to inappropriate strategy. % 222.05/31.54 % (3370511)------------------------------ % 222.05/31.54 % (3370511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.05/31.54 % (3370511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.05/31.54 % (3370511)CaDiCaL version: 2.1.3 % 222.05/31.54 % (3370511)Termination reason: Inappropriate % 222.05/31.54 % (3370511)Time elapsed: 0.011 s % 222.05/31.54 % (3370511)Peak memory usage: 11 MB % 222.05/31.54 % (3370511)Instructions burned: 15 (million) % 222.05/31.54 % (3370511)------------------------------ % 222.05/31.54 % (3370511)------------------------------ % 222.05/31.54 % (3370513)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=833450726:i=22565:add=on:rawr=on_2947 on theBenchmark for (2947ds/22565Mi) % 222.05/31.54 % (3370401)Instruction limit reached! % 222.05/31.54 % (3370401)------------------------------ % 222.05/31.54 % (3370401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.05/31.54 % (3370401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.05/31.54 % (3370401)CaDiCaL version: 2.1.3 % 222.05/31.54 % (3370401)Termination reason: Instruction limit % 222.05/31.54 % (3370401)Termination phase: Saturation % 222.05/31.54 % (3370401)Time elapsed: 4.956 s % 222.05/31.54 % (3370401)Peak memory usage: 29 MB % 222.05/31.54 % (3370401)Instructions burned: 5114 (million) % 222.05/31.54 % (3370532)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2441207617:i=8173:av=off_2938 on theBenchmark for (2938ds/8173Mi) % 223.46/31.76 % (3370484)Instruction limit reached! % 223.46/31.76 % (3370484)------------------------------ % 223.46/31.76 % (3370484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.46/31.76 % (3370484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.46/31.76 % (3370484)CaDiCaL version: 2.1.3 % 223.46/31.76 % (3370484)Termination reason: Instruction limit % 223.46/31.76 % (3370484)Termination phase: Saturation % 223.46/31.76 % (3370484)Time elapsed: 3.726 s % 223.46/31.76 % (3370484)Peak memory usage: 47 MB % 223.46/31.76 % (3370484)Instructions burned: 4592 (million) % 223.46/31.76 % (3370559)dis+10_16:1_sil=16000:random_seed=2787465703:i=9155:fsr=off_2920 on theBenchmark for (2920ds/9155Mi) % 223.46/31.76 % (3370493)Instruction limit reached! % 223.46/31.76 % (3370493)------------------------------ % 223.46/31.76 % (3370493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.46/31.76 % (3370493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.46/31.76 % (3370493)CaDiCaL version: 2.1.3 % 223.46/31.76 % (3370493)Termination reason: Instruction limit % 223.46/31.76 % (3370493)Termination phase: Saturation % 223.46/31.76 % (3370493)Time elapsed: 4.575 s % 223.46/31.76 % (3370493)Peak memory usage: 46 MB % 223.46/31.76 % (3370493)Instructions burned: 5212 (million) % 223.46/31.76 % (3370571)ott-3_8_sil=64000:random_seed=1011848564:i=20139:bs=on_2909 on theBenchmark for (2909ds/20139Mi) % 223.46/31.76 % (3370532)Instruction limit reached! % 223.46/31.76 % (3370532)------------------------------ % 223.46/31.76 % (3370532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.46/31.76 % (3370532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.46/31.76 % (3370532)CaDiCaL version: 2.1.3 % 223.46/31.76 % (3370532)Termination reason: Instruction limit % 223.46/31.76 % (3370532)Termination phase: Saturation % 223.46/31.76 % (3370532)Time elapsed: 8.176 s % 223.46/31.76 % (3370532)Peak memory usage: 45 MB % 223.46/31.76 % (3370532)Instructions burned: 8173 (million) % 223.46/31.76 % (3370596)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1304960851:fmbsr=2:i=32576_2856 on theBenchmark for (2856ds/32576Mi) % 223.46/31.76 % (3370596)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.46/31.76 % (3370596)Terminated due to inappropriate strategy. % 223.46/31.76 % (3370596)------------------------------ % 223.46/31.76 % (3370596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.46/31.76 % (3370596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.46/31.76 % (3370596)CaDiCaL version: 2.1.3 % 223.46/31.76 % (3370596)Termination reason: Inappropriate % 223.46/31.76 % (3370596)Time elapsed: 0.008 s % 223.46/31.76 % (3370596)Peak memory usage: 11 MB % 223.46/31.76 % (3370596)Instructions burned: 15 (million) % 223.46/31.76 % (3370596)------------------------------ % 223.46/31.76 % (3370596)------------------------------ % 223.46/31.76 % (3370598)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3078708244:i=11404_2856 on theBenchmark for (2856ds/11404Mi) % 223.46/31.76 % (3370559)Instruction limit reached! % 223.46/31.76 % (3370559)------------------------------ % 223.46/31.76 % (3370559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.46/31.76 % (3370559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.46/31.76 % (3370559)CaDiCaL version: 2.1.3 % 223.46/31.76 % (3370559)Termination reason: Instruction limit % 223.46/31.76 % (3370559)Termination phase: Saturation % 223.46/31.76 % (3370559)Time elapsed: 8.189 s % 223.46/31.76 % (3370559)Peak memory usage: 50 MB % 223.46/31.76 % (3370559)Instructions burned: 9156 (million) % 223.46/31.76 % (3370604)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=739185066:i=14134_2838 on theBenchmark for (2838ds/14134Mi) % 223.46/31.76 % (3370513)Instruction limit reached! % 223.46/31.76 % (3370513)------------------------------ % 223.46/31.76 % (3370513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.46/31.76 % (3370513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.46/31.76 % (3370513)CaDiCaL version: 2.1.3 % 223.46/31.76 % (3370513)Termination reason: Instruction limit % 223.46/31.76 % (3370513)Termination phase: Saturation % 223.46/31.76 % (3370513)Time elapsed: 15.506 s % 223.46/31.76 % (3370513)Peak memory usage: 22 MB % 223.46/31.76 % (3370513)Instructions burned: 22566 (million) % 223.46/31.76 % (3370613)dis+33_16_sil=32000:sac=on:random_seed=1904809859:i=15851:nm=0_2792 on theBenchmark for (2792ds/15851Mi) % 223.46/31.76 % (3370598)Instruction limit reached! % 223.46/31.76 % (3370598)------------------------------ % 223.46/31.76 % (3370598)Version: VamTerminated % 300.27/42.54 % Vampire exiting % 300.27/42.54 Terminated %------------------------------------------------------------------------------