%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV687-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n005.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:26:14 PM UTC 2026 % Result : Timeout 295.58s 42.10s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV687-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 % Computer : n005.cluster.edu % 0.09/0.24 % Model : x86_64 x86_64 % 0.09/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.24 % Memory : 8046.5625MB % 0.09/0.24 % OS : Linux 6.8.0-71-generic % 0.09/0.24 % CPULimit : 300 % 0.09/0.24 % WCLimit : 300 % 0.09/0.24 % DateTime : Mon Sep 28 12:15:01 UTC 2026 % 0.09/0.24 % CPUTime : % 0.09/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.26/0.29 Running first-order model finding % 0.26/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 % 19.92/3.21 % (748412)Will run a generic schedule for satisfiability detection. % 19.92/3.21 % (748422)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1992095741:i=131_2999 on theBenchmark for (2999ds/131Mi) % 19.92/3.21 % (748418)% WARNING: option uhcvi not known. % 19.92/3.21 % (748418)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1928847930:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 19.92/3.21 % (748417)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=697838154_2999 on theBenchmark for (2999ds/0Mi) % 19.92/3.21 % (748423)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3611109861:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 19.92/3.21 % (748420)dis+10_1_sil=32000:sp=arity:random_seed=1543296051:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 19.92/3.21 % (748421)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3293996875:i=116_2999 on theBenchmark for (2999ds/116Mi) % 19.92/3.21 % (748419)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1399060763:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 19.92/3.21 % (748422)Instruction limit reached! % 19.92/3.21 % (748422)------------------------------ % 19.92/3.21 % (748422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.92/3.21 % (748422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.21 % (748422)CaDiCaL version: 2.1.3 % 19.92/3.21 % (748422)Termination reason: Instruction limit % 19.92/3.21 % (748422)Termination phase: Saturation % 19.92/3.21 % (748422)Time elapsed: 0.071 s % 19.92/3.21 % (748422)Peak memory usage: 14 MB % 19.92/3.21 % (748422)Instructions burned: 131 (million) % 19.92/3.21 % (748431)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1656012683:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 19.92/3.21 % (748421)Instruction limit reached! % 19.92/3.21 % (748421)------------------------------ % 19.92/3.21 % (748421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.92/3.21 % (748421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.21 % (748421)CaDiCaL version: 2.1.3 % 19.92/3.21 % (748421)Termination reason: Instruction limit % 19.92/3.21 % (748421)Termination phase: Saturation % 19.92/3.21 % (748421)Time elapsed: 0.112 s % 19.92/3.21 % (748421)Peak memory usage: 14 MB % 19.92/3.21 % (748421)Instructions burned: 116 (million) % 19.92/3.21 % (748420)Instruction limit reached! % 19.92/3.21 % (748420)------------------------------ % 19.92/3.21 % (748420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.92/3.21 % (748420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.21 % (748420)CaDiCaL version: 2.1.3 % 19.92/3.21 % (748420)Termination reason: Instruction limit % 19.92/3.21 % (748420)Termination phase: Saturation % 19.92/3.21 % (748420)Time elapsed: 0.113 s % 19.92/3.21 % (748420)Peak memory usage: 13 MB % 19.92/3.21 % (748420)Instructions burned: 103 (million) % 19.92/3.21 % (748434)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=230461461:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 19.92/3.21 % (748433)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2744484219:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 19.92/3.21 % (748423)Instruction limit reached! % 19.92/3.21 % (748423)------------------------------ % 19.92/3.21 % (748423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.92/3.21 % (748423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.21 % (748423)CaDiCaL version: 2.1.3 % 19.92/3.21 % (748423)Termination reason: Instruction limit % 19.92/3.21 % (748423)Termination phase: Saturation % 19.92/3.21 % (748423)Time elapsed: 0.157 s % 19.92/3.21 % (748423)Peak memory usage: 15 MB % 19.92/3.21 % (748423)Instructions burned: 160 (million) % 19.92/3.21 % (748437)ott-21_1_sil=16000:fs=off:random_seed=2924438957:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 19.92/3.21 % (748433)Instruction limit reached! % 19.92/3.21 % (748433)------------------------------ % 19.92/3.21 % (748433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.92/3.21 % (748433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.21 % (748433)CaDiCaL version: 2.1.3 % 19.92/3.21 % (748433)Termination reason: Instruction limit % 59.16/8.78 % (748433)Termination phase: Saturation % 59.16/8.78 % (748433)Time elapsed: 0.131 s % 59.16/8.78 % (748433)Peak memory usage: 14 MB % 59.16/8.78 % (748433)Instructions burned: 131 (million) % 59.16/8.78 % (748439)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2283360094:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi) % 59.16/8.78 % (748437)Instruction limit reached! % 59.16/8.78 % (748437)------------------------------ % 59.16/8.78 % (748437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.16/8.78 % (748437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.16/8.78 % (748437)CaDiCaL version: 2.1.3 % 59.16/8.78 % (748437)Termination reason: Instruction limit % 59.16/8.78 % (748437)Termination phase: Saturation % 59.16/8.78 % (748437)Time elapsed: 0.157 s % 59.16/8.78 % (748437)Peak memory usage: 14 MB % 59.16/8.78 % (748437)Instructions burned: 180 (million) % 59.16/8.78 % (748431)Instruction limit reached! % 59.16/8.78 % (748431)------------------------------ % 59.16/8.78 % (748431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.16/8.78 % (748431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.16/8.78 % (748431)CaDiCaL version: 2.1.3 % 59.16/8.78 % (748431)Termination reason: Instruction limit % 59.16/8.78 % (748431)Termination phase: Finite model building preprocessing % 59.16/8.78 % (748431)Time elapsed: 0.266 s % 59.16/8.78 % (748431)Peak memory usage: 20 MB % 59.16/8.78 % (748431)Instructions burned: 717 (million) % 59.16/8.78 % (748442)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1499979444:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 59.16/8.78 % (748441)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3889125701:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 59.16/8.78 % TRYING [1] % 59.16/8.78 % (748439)Instruction limit reached! % 59.16/8.78 % (748439)------------------------------ % 59.16/8.78 % (748439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.16/8.78 % (748439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.16/8.78 % (748439)CaDiCaL version: 2.1.3 % 59.16/8.78 % (748439)Termination reason: Instruction limit % 59.16/8.78 % (748439)Termination phase: Saturation % 59.16/8.78 % (748439)Time elapsed: 0.521 s % 59.16/8.78 % (748439)Peak memory usage: 15 MB % 59.16/8.78 % (748439)Instructions burned: 477 (million) % 59.16/8.78 % (748434)Instruction limit reached! % 59.16/8.78 % (748434)------------------------------ % 59.16/8.78 % (748434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.16/8.78 % (748434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.16/8.78 % (748434)CaDiCaL version: 2.1.3 % 59.16/8.78 % (748434)Termination reason: Instruction limit % 59.16/8.78 % (748434)Termination phase: Saturation % 59.16/8.78 % (748434)Time elapsed: 0.732 s % 59.16/8.78 % (748434)Peak memory usage: 18 MB % 59.16/8.78 % (748434)Instructions burned: 684 (million) % 59.16/8.78 % (748445)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2179327064:i=889:ins=1_2990 on theBenchmark for (2990ds/889Mi) % 59.16/8.78 % TRYING [2] % 59.16/8.78 % (748442)Instruction limit reached! % 59.16/8.78 % (748442)------------------------------ % 59.16/8.78 % (748442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.16/8.78 % (748442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.16/8.78 % (748442)CaDiCaL version: 2.1.3 % 59.16/8.78 % (748442)Termination reason: Instruction limit % 59.16/8.78 % (748442)Termination phase: Saturation % 59.16/8.78 % (748442)Time elapsed: 0.548 s % 59.16/8.78 % (748442)Peak memory usage: 23 MB % 59.16/8.78 % (748442)Instructions burned: 1180 (million) % 59.16/8.78 % (748446)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=1191291112:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2989 on theBenchmark for (2989ds/692Mi) % 59.16/8.78 % (748448)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=267150807:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi) % 59.16/8.78 % (748441)Instruction limit reached! % 59.16/8.78 % (748441)------------------------------ % 59.16/8.78 % (748441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.16/8.78 % (748441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.16/8.78 % (748441)CaDiCaL version: 2.1.3 % 59.16/8.78 % (748441)Termination reason: Instruction limit % 59.16/8.78 % (748441)Termination phase: Finite model building preprocessing % 134.38/19.38 % (748441)Time elapsed: 0.756 s % 134.38/19.38 % (748441)Peak memory usage: 22 MB % 134.38/19.38 % (748441)Instructions burned: 865 (million) % 134.38/19.38 % (748451)fmb+10_1_sil=64000:random_seed=4260517349:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi) % 134.38/19.38 % (748446)Instruction limit reached! % 134.38/19.38 % (748446)------------------------------ % 134.38/19.38 % (748446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.38/19.38 % (748446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.38/19.38 % (748446)CaDiCaL version: 2.1.3 % 134.38/19.38 % (748446)Termination reason: Instruction limit % 134.38/19.38 % (748446)Termination phase: Saturation % 134.38/19.38 % (748446)Time elapsed: 0.416 s % 134.38/19.38 % (748446)Peak memory usage: 20 MB % 134.38/19.38 % (748446)Instructions burned: 693 (million) % 134.38/19.38 % (748453)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3156648239:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi) % 134.38/19.38 % TRYING [3] % 134.38/19.38 % (748445)Instruction limit reached! % 134.38/19.38 % (748445)------------------------------ % 134.38/19.38 % (748445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.38/19.38 % (748445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.38/19.38 % (748445)CaDiCaL version: 2.1.3 % 134.38/19.38 % (748445)Termination reason: Instruction limit % 134.38/19.38 % (748445)Termination phase: Finite model building preprocessing % 134.38/19.38 % (748445)Time elapsed: 0.814 s % 134.38/19.38 % (748445)Peak memory usage: 26 MB % 134.38/19.38 % (748445)Instructions burned: 890 (million) % 134.38/19.38 % (748455)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2076522272:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi) % 134.38/19.38 % (748448)Instruction limit reached! % 134.38/19.38 % (748448)------------------------------ % 134.38/19.38 % (748448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.38/19.38 % (748448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.38/19.38 % (748448)CaDiCaL version: 2.1.3 % 134.38/19.38 % (748448)Termination reason: Instruction limit % 134.38/19.38 % (748448)Termination phase: Saturation % 134.38/19.38 % (748448)Time elapsed: 0.796 s % 134.38/19.38 % (748448)Peak memory usage: 20 MB % 134.38/19.38 % (748448)Instructions burned: 880 (million) % 134.38/19.38 % (748457)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1736153342:i=5131_2981 on theBenchmark for (2981ds/5131Mi) % 134.38/19.38 % (748453)Cannot represent all propositional literals internally % 134.38/19.38 % (748453)Refutation not found, incomplete strategy % 134.38/19.38 % (748453)------------------------------ % 134.38/19.38 % (748453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.38/19.38 % (748453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.38/19.38 % (748453)CaDiCaL version: 2.1.3 % 134.38/19.38 % (748453)Termination reason: Refutation not found, incomplete strategy % 134.38/19.38 % (748453)Time elapsed: 0.538 s % 134.38/19.38 % (748453)Peak memory usage: 26 MB % 134.38/19.38 % (748453)Instructions burned: 998 (million) % 134.38/19.38 % (748453)------------------------------ % 134.38/19.38 % (748453)------------------------------ % 134.38/19.38 % (748459)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3452926545:i=1472:ins=7:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/1472Mi) % 134.38/19.38 % TRYING [1] % 134.38/19.38 % TRYING [2] % 134.38/19.38 % (748455)Instruction limit reached! % 134.38/19.38 % (748455)------------------------------ % 134.38/19.38 % (748455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.38/19.38 % (748455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.38/19.38 % (748455)CaDiCaL version: 2.1.3 % 134.38/19.38 % (748455)Termination reason: Instruction limit % 134.38/19.38 % (748455)Termination phase: Finite model building preprocessing % 134.38/19.38 % (748455)Time elapsed: 0.848 s % 134.38/19.38 % (748455)Peak memory usage: 26 MB % 134.38/19.38 % (748455)Instructions burned: 920 (million) % 134.38/19.38 % (748461)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1719745025:i=6324_2972 on theBenchmark for (2972ds/6324Mi) % 134.38/19.38 % (748459)Instruction limit reached! % 134.38/19.38 % (748459)------------------------------ % 134.38/19.38 % (748459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.38/19.38 % (748459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.38/19.38 % (748459)CaDiCaL version: 2.1.3 % 134.38/19.38 % (748459)Termination reason: Instruction limit % 209.54/29.97 % (748459)Termination phase: Saturation % 209.54/29.97 % (748459)Time elapsed: 0.805 s % 209.54/29.97 % (748459)Peak memory usage: 32 MB % 209.54/29.97 % (748459)Instructions burned: 1473 (million) % 209.54/29.97 % (748465)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2716075897:fmbsr=2.30978:i=2174_2970 on theBenchmark for (2970ds/2174Mi) % 209.54/29.97 % (748461)Cannot represent all propositional literals internally % 209.54/29.97 % (748461)Refutation not found, incomplete strategy % 209.54/29.97 % (748461)------------------------------ % 209.54/29.97 % (748461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.54/29.97 % (748461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.54/29.97 % (748461)CaDiCaL version: 2.1.3 % 209.54/29.97 % (748461)Termination reason: Refutation not found, incomplete strategy % 209.54/29.97 % (748461)Time elapsed: 0.876 s % 209.54/29.97 % (748461)Peak memory usage: 27 MB % 209.54/29.97 % (748461)Instructions burned: 1022 (million) % 209.54/29.97 % (748461)------------------------------ % 209.54/29.97 % (748461)------------------------------ % 209.54/29.97 % (748467)ott-2_1_sil=16000:newcnf=on:random_seed=3168878072:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2963 on theBenchmark for (2963ds/869Mi) % 209.54/29.97 % (748465)Instruction limit reached! % 209.54/29.97 % (748465)------------------------------ % 209.54/29.97 % (748465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.54/29.97 % (748465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.54/29.97 % (748465)CaDiCaL version: 2.1.3 % 209.54/29.97 % (748465)Termination reason: Instruction limit % 209.54/29.97 % (748465)Termination phase: Finite model building preprocessing % 209.54/29.97 % (748465)Time elapsed: 0.929 s % 209.54/29.97 % (748465)Peak memory usage: 29 MB % 209.54/29.97 % (748465)Instructions burned: 2175 (million) % 209.54/29.97 % (748469)ott+10_1_sil=32000:tgt=ground:random_seed=2903103976:i=5114:av=off_2961 on theBenchmark for (2961ds/5114Mi) % 209.54/29.97 % (748467)Instruction limit reached! % 209.54/29.97 % (748467)------------------------------ % 209.54/29.97 % (748467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.54/29.97 % (748467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.54/29.97 % (748467)CaDiCaL version: 2.1.3 % 209.54/29.97 % (748467)Termination reason: Instruction limit % 209.54/29.97 % (748467)Termination phase: Saturation % 209.54/29.97 % (748467)Time elapsed: 0.663 s % 209.54/29.97 % (748467)Peak memory usage: 15 MB % 209.54/29.97 % (748467)Instructions burned: 870 (million) % 209.54/29.97 % (748471)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2848063319:i=54282_2956 on theBenchmark for (2956ds/54282Mi) % 209.54/29.97 % TRYING [4] % 209.54/29.97 % TRYING [1] % 209.54/29.97 % TRYING [2] % 209.54/29.97 % TRYING [3] % 209.54/29.97 % TRYING [3] % 209.54/29.97 % (748469)Instruction limit reached! % 209.54/29.97 % (748469)------------------------------ % 209.54/29.97 % (748469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.54/29.97 % (748469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.54/29.97 % (748469)CaDiCaL version: 2.1.3 % 209.54/29.97 % (748469)Termination reason: Instruction limit % 209.54/29.97 % (748469)Termination phase: Saturation % 209.54/29.97 % (748469)Time elapsed: 2.654 s % 209.54/29.97 % (748469)Peak memory usage: 43 MB % 209.54/29.97 % (748469)Instructions burned: 5116 (million) % 209.54/29.97 % (748473)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1632526181:i=3512:aac=none_2934 on theBenchmark for (2934ds/3512Mi) % 209.54/29.97 % (748457)Instruction limit reached! % 209.54/29.97 % (748457)------------------------------ % 209.54/29.97 % (748457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.54/29.97 % (748457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.54/29.97 % (748457)CaDiCaL version: 2.1.3 % 209.54/29.97 % (748457)Termination reason: Instruction limit % 209.54/29.97 % (748457)Termination phase: Saturation % 209.54/29.97 % (748457)Time elapsed: 4.791 s % 209.54/29.97 % (748457)Peak memory usage: 38 MB % 209.54/29.97 % (748457)Instructions burned: 5131 (million) % 209.54/29.97 % (748475)dis+21_1_sil=32000:sas=cadical:random_seed=478724342:i=3773:amm=off_2932 on theBenchmark for (2932ds/3773Mi) % 209.54/29.97 % (748473)Instruction limit reached! % 209.54/29.97 % (748473)------------------------------ % 209.54/29.97 % (748473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.54/29.97 % (748473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.54/29.97 % (748473)CaDiCaL version: 2.1.3 % 209.54/29.97 % (748473)Termination reason: Instruction limit % 295.58/42.10 % (748473)Termination phase: Saturation % 295.58/42.10 % (748473)Time elapsed: 1.889 s % 295.58/42.10 % (748473)Peak memory usage: 33 MB % 295.58/42.10 % (748473)Instructions burned: 3513 (million) % 295.58/42.10 % (748481)ott+11_1_sil=16000:gs=on:random_seed=1740265981:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2915 on theBenchmark for (2915ds/2251Mi) % 295.58/42.10 % TRYING [4] % 295.58/42.10 % (748481)Instruction limit reached! % 295.58/42.10 % (748481)------------------------------ % 295.58/42.10 % (748481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.58/42.10 % (748481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.58/42.10 % (748481)CaDiCaL version: 2.1.3 % 295.58/42.10 % (748481)Termination reason: Instruction limit % 295.58/42.10 % (748481)Termination phase: Saturation % 295.58/42.10 % (748481)Time elapsed: 1.274 s % 295.58/42.10 % (748481)Peak memory usage: 27 MB % 295.58/42.10 % (748481)Instructions burned: 2252 (million) % 295.58/42.10 % (748483)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=423128926:fmbsr=1.6:i=67534_2902 on theBenchmark for (2902ds/67534Mi) % 295.58/42.10 % (748475)Instruction limit reached! % 295.58/42.10 % (748475)------------------------------ % 295.58/42.10 % (748475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.58/42.10 % (748475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.58/42.10 % (748475)CaDiCaL version: 2.1.3 % 295.58/42.10 % (748475)Termination reason: Instruction limit % 295.58/42.10 % (748475)Termination phase: Saturation % 295.58/42.10 % (748475)Time elapsed: 3.528 s % 295.58/42.10 % (748475)Peak memory usage: 35 MB % 295.58/42.10 % (748475)Instructions burned: 3774 (million) % 295.58/42.10 % (748485)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2342390726:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2896 on theBenchmark for (2896ds/4591Mi) % 295.58/42.10 % (748485)Instruction limit reached! % 295.58/42.10 % (748485)------------------------------ % 295.58/42.10 % (748485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.58/42.10 % (748485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.58/42.10 % (748485)CaDiCaL version: 2.1.3 % 295.58/42.10 % (748485)Termination reason: Instruction limit % 295.58/42.10 % (748485)Termination phase: Saturation % 295.58/42.10 % (748485)Time elapsed: 3.230 s % 295.58/42.10 % (748485)Peak memory usage: 55 MB % 295.58/42.10 % (748485)Instructions burned: 4591 (million) % 295.58/42.10 % (748645)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1400696851:i=29340_2864 on theBenchmark for (2864ds/29340Mi) % 295.58/42.10 % TRYING [4] % 295.58/42.10 % (748451)Instruction limit reached! % 295.58/42.10 % (748451)------------------------------ % 295.58/42.10 % (748451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.58/42.10 % (748451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.58/42.10 % (748451)CaDiCaL version: 2.1.3 % 295.58/42.10 % (748451)Termination reason: Instruction limit % 295.58/42.10 % (748451)Termination phase: Finite model building constraint generation % 295.58/42.10 % (748451)Time elapsed: 14.238 s % 295.58/42.10 % (748451)Peak memory usage: 505 MB % 295.58/42.10 % (748451)Instructions burned: 22061 (million) % 295.58/42.10 % (748647)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3272450576:i=5211_2843 on theBenchmark for (2843ds/5211Mi) % 295.58/42.10 % TRYING [7] % 295.58/42.10 % (748647)Instruction limit reached! % 295.58/42.10 % (748647)------------------------------ % 295.58/42.10 % (748647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.58/42.10 % (748647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.58/42.10 % (748647)CaDiCaL version: 2.1.3 % 295.58/42.10 % (748647)Termination reason: Instruction limit % 295.58/42.10 % (748647)Termination phase: Saturation % 295.58/42.10 % (748647)Time elapsed: 2.878 s % 295.58/42.10 % (748647)Peak memory usage: 51 MB % 295.58/42.10 % (748647)Instructions burned: 5211 (million) % 295.58/42.10 % (748649)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3641245908:i=5497:nm=2_2814 on theBenchmark for (2814ds/5497Mi) % 295.58/42.10 % TRYING [5] % 295.58/42.10 % (748649)Cannot represent all propositional literals internally % 295.58/42.10 % (748649)Refutation not found, incomplete strategy % 295.58/42.10 % (748649)------------------------------ % 295.58/42.10 % (748649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.58/42.10 % (748649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.58/42.10 % (748649)CaDiCaL version: 2.1.3 % 300.58/42.83 % (748649)Termination reason: Refutation not found, incomplete strategy % 300.58/42.83 % (748649)Time elapsed: 0.512 s % 300.58/42.83 % (748649)Peak memory usage: 27 MB % 300.58/42.83 % (748649)Instructions burned: 1022 (million) % 300.58/42.83 % (748649)------------------------------ % 300.58/42.83 % (748649)------------------------------ % 300.58/42.83 % (748651)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3411376734:fmbsr=2:i=46332_2809 on theBenchmark for (2809ds/46332Mi) % 300.58/42.83 % (748651)Cannot represent all propositional literals internally % 300.58/42.83 % (748651)Refutation not found, incomplete strategy % 300.58/42.83 % (748651)------------------------------ % 300.58/42.83 % (748651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.58/42.83 % (748651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/42.83 % (748651)CaDiCaL version: 2.1.3 % 300.58/42.83 % (748651)Termination reason: Refutation not found, incomplete strategy % 300.58/42.83 % (748651)Time elapsed: 0.510 s % 300.58/42.83 % (748651)Peak memory usage: 24 MB % 300.58/42.83 % (748651)Instructions burned: 1046 (million) % 300.58/42.83 % (748651)------------------------------ % 300.58/42.83 % (748651)------------------------------ % 300.58/42.83 % (748653)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=163800942:i=14071_2803 on theBenchmark for (2803ds/14071Mi) % 300.58/42.83 % TRYING [12] % 300.58/42.83 % TRYING [5] % 300.58/42.83 % (748483)Instruction limit reached! % 300.58/42.83 % (748483)------------------------------ % 300.58/42.83 % (748483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.58/42.83 % (748483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/42.83 % (748483)CaDiCaL version: 2.1.3 % 300.58/42.83 % (748483)Termination reason: Instruction limit % 300.58/42.83 % (748483)Termination phase: Finite model building constraint generation % 300.58/42.83 % (748483)Time elapsed: 14.657 s % 300.58/42.83 % (748483)Peak memory usage: 4109 MB % 300.58/42.83 % (748483)Instructions burned: 67540 (million) % 300.58/42.83 % (748653)Instruction limit reached! % 300.58/42.83 % (748653)------------------------------ % 300.58/42.83 % (748653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.58/42.83 % (748653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/42.83 % (748653)CaDiCaL version: 2.1.3 % 300.58/42.83 % (748653)Termination reason: Instruction limit % 300.58/42.83 % (748653)Termination phase: Finite model building constraint generation % 300.58/42.83 % (748653)Time elapsed: 5.020 s % 300.58/42.83 % (748653)Peak memory usage: 849 MB % 300.58/42.83 % (748653)Instructions burned: 14071 (million) % 300.58/42.83 % (748656)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=521514690:i=22565:add=on:rawr=on_2752 on theBenchmark for (2752ds/22565Mi) % 300.58/42.83 % (748658)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4018657922:i=8173:av=off_2750 on theBenchmark for (2750ds/8173Mi) % 300.58/42.83 % (748645)Instruction limit reached! % 300.58/42.83 % (748645)------------------------------ % 300.58/42.83 % (748645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.58/42.83 % (748645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/42.83 % (748645)CaDiCaL version: 2.1.3 % 300.58/42.83 % (748645)Termination reason: Instruction limit % 300.58/42.83 % (748645)Termination phase: Saturation % 300.58/42.83 % (748645)Time elapsed: 13.162 s % 300.58/42.83 % (748645)Peak memory usage: 317 MB % 300.58/42.83 % (748645)Instructions burned: 29340 (million) % 300.58/42.83 % (748660)dis+10_16:1_sil=16000:random_seed=1808746672:i=9155:fsr=off_2731 on theBenchmark for (2731ds/9155Mi) % 300.58/42.83 % (748658)Instruction limit reached! % 300.58/42.83 % (748658)------------------------------ % 300.58/42.83 % (748658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.58/42.83 % (748658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/42.83 % (748658)CaDiCaL version: 2.1.3 % 300.58/42.83 % (748658)Termination reason: Instruction limit % 300.58/42.83 % (748658)Termination phase: Saturation % 300.58/42.83 % (748658)Time elapsed: 2.890 s % 300.58/42.83 % (748658)Peak memory usage: 66 MB % 300.58/42.83 % (748658)Instructions burned: 8174 (million) % 300.58/42.83 % (748662)ott-3_8_sil=64000:random_seed=2265442078:i=20139:bs=on_2721 on theBenchmark for (2721ds/20139Mi) % 300.58/42.83 % (748471)Instruction limit reached! % 300.58/42.83 % (748471)------------------------------ % 300.58/42.83 % (748471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.58/42.83 % (748471)Linked with Z3 4.14.0.0 3c47fd9 % 300.58/42.84 Terminated % 300.58/42.84 % Vampire exiting % 300.58/42.84 Terminated %------------------------------------------------------------------------------