%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : TOP045+2 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n010.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 02:34:29 PM UTC 2026 % Result : Timeout 300.25s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : TOP045+2 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n010.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 19:06:10 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.21 Running first-order model finding % 0.07/0.21 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 % 22.24/3.58 % (2222407)Will run a generic schedule for satisfiability detection. % 22.24/3.58 % (2222413)% WARNING: option uhcvi not known. % 22.24/3.58 % (2222412)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2335665792_2998 on theBenchmark for (2998ds/0Mi) % 22.24/3.58 % (2222415)dis+10_1_sil=32000:sp=arity:random_seed=3585596753:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 22.24/3.58 % (2222413)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3219473370:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 22.24/3.58 % (2222414)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3345633564:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 22.24/3.58 % (2222416)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1834482274:i=116_2998 on theBenchmark for (2998ds/116Mi) % 22.24/3.58 % (2222417)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4207186777:i=131_2998 on theBenchmark for (2998ds/131Mi) % 22.24/3.58 % (2222418)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=835059429:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 22.24/3.58 % (2222415)Instruction limit reached! % 22.24/3.58 % (2222415)------------------------------ % 22.24/3.58 % (2222415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.24/3.58 % (2222415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/3.58 % (2222415)CaDiCaL version: 2.1.3 % 22.24/3.58 % (2222415)Termination reason: Instruction limit % 22.24/3.58 % (2222415)Termination phase: Preprocessing 2 % 22.24/3.58 % (2222415)Time elapsed: 0.078 s % 22.24/3.58 % (2222415)Peak memory usage: 29 MB % 22.24/3.58 % (2222415)Instructions burned: 103 (million) % 22.24/3.58 % (2222416)Instruction limit reached! % 22.24/3.58 % (2222416)------------------------------ % 22.24/3.58 % (2222416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.24/3.58 % (2222416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/3.58 % (2222416)CaDiCaL version: 2.1.3 % 22.24/3.58 % (2222416)Termination reason: Instruction limit % 22.24/3.58 % (2222416)Termination phase: NewCNF % 22.24/3.58 % (2222416)Time elapsed: 0.097 s % 22.24/3.58 % (2222416)Peak memory usage: 34 MB % 22.24/3.58 % (2222416)Instructions burned: 117 (million) % 22.24/3.58 % (2222418)Instruction limit reached! % 22.24/3.58 % (2222418)------------------------------ % 22.24/3.58 % (2222418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.24/3.58 % (2222418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/3.58 % (2222418)CaDiCaL version: 2.1.3 % 22.24/3.58 % (2222418)Termination reason: Instruction limit % 22.24/3.58 % (2222418)Termination phase: Naming % 22.24/3.58 % (2222418)Time elapsed: 0.098 s % 22.24/3.58 % (2222418)Peak memory usage: 35 MB % 22.24/3.58 % (2222418)Instructions burned: 159 (million) % 22.24/3.58 % (2222417)Instruction limit reached! % 22.24/3.58 % (2222417)------------------------------ % 22.24/3.58 % (2222417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.24/3.58 % (2222417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/3.58 % (2222417)CaDiCaL version: 2.1.3 % 22.24/3.58 % (2222417)Termination reason: Instruction limit % 22.24/3.58 % (2222417)Termination phase: Naming % 22.24/3.58 % (2222417)Time elapsed: 0.100 s % 22.24/3.58 % (2222417)Peak memory usage: 34 MB % 22.24/3.58 % (2222417)Instructions burned: 131 (million) % 22.24/3.58 % (2222426)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2042552719:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi) % 22.24/3.58 % (2222429)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=2387632853:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 22.24/3.58 % (2222428)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1984943708:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 22.24/3.58 % (2222430)ott-21_1_sil=16000:fs=off:random_seed=2309573464:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 22.24/3.58 % (2222428)Instruction limit reached! % 22.24/3.58 % (2222428)------------------------------ % 22.24/3.58 % (2222428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.24/3.58 % (2222428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/3.58 % (2222428)CaDiCaL version: 2.1.3 % 49.92/7.47 % (2222428)Termination reason: Instruction limit % 49.92/7.47 % (2222428)Termination phase: Naming % 49.92/7.47 % (2222428)Time elapsed: 0.104 s % 49.92/7.47 % (2222428)Peak memory usage: 34 MB % 49.92/7.47 % (2222428)Instructions burned: 134 (million) % 49.92/7.47 % (2222430)Instruction limit reached! % 49.92/7.47 % (2222430)------------------------------ % 49.92/7.47 % (2222430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.92/7.47 % (2222430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.92/7.47 % (2222430)CaDiCaL version: 2.1.3 % 49.92/7.47 % (2222430)Termination reason: Instruction limit % 49.92/7.47 % (2222430)Termination phase: Preprocessing 3 % 49.92/7.47 % (2222430)Time elapsed: 0.126 s % 49.92/7.47 % (2222430)Peak memory usage: 35 MB % 49.92/7.47 % (2222430)Instructions burned: 181 (million) % 49.92/7.47 % (2222434)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3451471443:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi) % 49.92/7.47 % (2222436)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1328466788:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 49.92/7.47 % (2222429)Instruction limit reached! % 49.92/7.47 % (2222429)------------------------------ % 49.92/7.47 % (2222429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.92/7.47 % (2222429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.92/7.47 % (2222429)CaDiCaL version: 2.1.3 % 49.92/7.47 % (2222429)Termination reason: Instruction limit % 49.92/7.47 % (2222429)Termination phase: Property scanning % 49.92/7.47 % (2222429)Time elapsed: 0.218 s % 49.92/7.47 % (2222429)Peak memory usage: 49 MB % 49.92/7.47 % (2222429)Instructions burned: 685 (million) % 49.92/7.47 % (2222438)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2596041217:i=1179_2994 on theBenchmark for (2994ds/1179Mi) % 49.92/7.47 % (2222426)Instruction limit reached! % 49.92/7.47 % (2222426)------------------------------ % 49.92/7.47 % (2222426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.92/7.47 % (2222426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.92/7.47 % (2222426)CaDiCaL version: 2.1.3 % 49.92/7.47 % (2222426)Termination reason: Instruction limit % 49.92/7.47 % (2222426)Termination phase: Function definition elimination % 49.92/7.47 % (2222426)Time elapsed: 0.412 s % 49.92/7.47 % (2222426)Peak memory usage: 54 MB % 49.92/7.47 % (2222426)Instructions burned: 714 (million) % 49.92/7.47 % (2222440)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=86762395:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi) % 49.92/7.47 % (2222434)Instruction limit reached! % 49.92/7.47 % (2222434)------------------------------ % 49.92/7.47 % (2222434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.92/7.47 % (2222434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.92/7.47 % (2222434)CaDiCaL version: 2.1.3 % 49.92/7.47 % (2222434)Termination reason: Instruction limit % 49.92/7.47 % (2222434)Termination phase: Property scanning % 49.92/7.47 % (2222434)Time elapsed: 0.293 s % 49.92/7.47 % (2222434)Peak memory usage: 47 MB % 49.92/7.47 % (2222434)Instructions burned: 478 (million) % 49.92/7.47 % (2222442)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=3051570291:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi) % 49.92/7.47 % (2222438)Instruction limit reached! % 49.92/7.47 % (2222438)------------------------------ % 49.92/7.47 % (2222438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.92/7.47 % (2222438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.92/7.47 % (2222438)CaDiCaL version: 2.1.3 % 49.92/7.47 % (2222438)Termination reason: Instruction limit % 49.92/7.47 % (2222438)Termination phase: Saturation % 49.92/7.47 % (2222438)Time elapsed: 0.342 s % 49.92/7.47 % (2222438)Peak memory usage: 53 MB % 49.92/7.47 % (2222438)Instructions burned: 1183 (million) % 49.92/7.47 % (2222444)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1893728412:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi) % 49.92/7.47 % (2222436)Instruction limit reached! % 49.92/7.47 % (2222436)------------------------------ % 49.92/7.47 % (2222436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.92/7.47 % (2222436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.62/13.79 % (2222436)CaDiCaL version: 2.1.3 % 94.62/13.79 % (2222436)Termination reason: Instruction limit % 94.62/13.79 % (2222436)Termination phase: Property scanning % 94.62/13.79 % (2222436)Time elapsed: 0.448 s % 94.62/13.79 % (2222436)Peak memory usage: 49 MB % 94.62/13.79 % (2222436)Instructions burned: 866 (million) % 94.62/13.79 % (2222446)fmb+10_1_sil=64000:random_seed=1733817023:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 94.62/13.79 % (2222444)Instruction limit reached! % 94.62/13.79 % (2222444)------------------------------ % 94.62/13.79 % (2222444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.62/13.79 % (2222444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.62/13.79 % (2222444)CaDiCaL version: 2.1.3 % 94.62/13.79 % (2222444)Termination reason: Instruction limit % 94.62/13.79 % (2222444)Termination phase: Function definition elimination % 94.62/13.79 % (2222444)Time elapsed: 0.252 s % 94.62/13.79 % (2222444)Peak memory usage: 48 MB % 94.62/13.79 % (2222444)Instructions burned: 879 (million) % 94.62/13.79 % (2222442)Instruction limit reached! % 94.62/13.79 % (2222442)------------------------------ % 94.62/13.79 % (2222442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.62/13.79 % (2222442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.62/13.79 % (2222442)CaDiCaL version: 2.1.3 % 94.62/13.79 % (2222442)Termination reason: Instruction limit % 94.62/13.79 % (2222442)Termination phase: Property scanning % 94.62/13.79 % (2222442)Time elapsed: 0.397 s % 94.62/13.79 % (2222442)Peak memory usage: 48 MB % 94.62/13.79 % (2222442)Instructions burned: 693 (million) % 94.62/13.79 % (2222448)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=90699007:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi) % 94.62/13.79 % (2222450)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3783120160:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 94.62/13.79 % (2222440)Instruction limit reached! % 94.62/13.79 % (2222440)------------------------------ % 94.62/13.79 % (2222440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.62/13.79 % (2222440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.62/13.79 % (2222440)CaDiCaL version: 2.1.3 % 94.62/13.79 % (2222440)Termination reason: Instruction limit % 94.62/13.79 % (2222440)Termination phase: Property scanning % 94.62/13.79 % (2222440)Time elapsed: 0.468 s % 94.62/13.79 % (2222440)Peak memory usage: 50 MB % 94.62/13.79 % (2222440)Instructions burned: 889 (million) % 94.62/13.79 % (2222452)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2844709895:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 94.62/13.79 % (2222450)Instruction limit reached! % 94.62/13.79 % (2222450)------------------------------ % 94.62/13.79 % (2222450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.62/13.79 % (2222450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.62/13.79 % (2222450)CaDiCaL version: 2.1.3 % 94.62/13.79 % (2222450)Termination reason: Instruction limit % 94.62/13.79 % (2222450)Termination phase: Property scanning % 94.62/13.79 % (2222450)Time elapsed: 0.483 s % 94.62/13.79 % (2222450)Peak memory usage: 50 MB % 94.62/13.79 % (2222450)Instructions burned: 920 (million) % 94.62/13.79 % (2222454)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1848878205:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi) % 94.62/13.79 % (2222454)Instruction limit reached! % 94.62/13.79 % (2222454)------------------------------ % 94.62/13.79 % (2222454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.62/13.79 % (2222454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.62/13.79 % (2222454)CaDiCaL version: 2.1.3 % 94.62/13.79 % (2222454)Termination reason: Instruction limit % 94.62/13.79 % (2222454)Termination phase: Saturation % 94.62/13.79 % (2222454)Time elapsed: 0.756 s % 94.62/13.79 % (2222454)Peak memory usage: 55 MB % 94.62/13.79 % (2222454)Instructions burned: 1473 (million) % 94.62/13.79 % (2222456)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=741460520:i=6324_2975 on theBenchmark for (2975ds/6324Mi) % 94.62/13.79 % Detected minimum model sizes of [5] % 94.62/13.79 % Detected maximum model sizes of [max] % 94.62/13.79 % (2222448)Cannot represent all propositional literals internally % 94.62/13.79 % (2222448)Refutation not found, incomplete strategy % 94.62/13.79 % (2222448)------------------------------ % 94.62/13.79 % (2222448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.62/13.79 % (2222448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.40/25.46 % (2222448)CaDiCaL version: 2.1.3 % 177.40/25.46 % (2222448)Termination reason: Refutation not found, incomplete strategy % 177.40/25.46 % (2222448)Time elapsed: 2.194 s % 177.40/25.46 % (2222448)Peak memory usage: 156 MB % 177.40/25.46 % (2222448)Instructions burned: 7986 (million) % 177.40/25.46 % (2222448)------------------------------ % 177.40/25.46 % (2222448)------------------------------ % 177.40/25.46 % (2222458)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=640778522:fmbsr=2.30978:i=2174_2966 on theBenchmark for (2966ds/2174Mi) % 177.40/25.46 % (2222458)Instruction limit reached! % 177.40/25.46 % (2222458)------------------------------ % 177.40/25.46 % (2222458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.40/25.46 % (2222458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.40/25.46 % (2222458)CaDiCaL version: 2.1.3 % 177.40/25.46 % (2222458)Termination reason: Instruction limit % 177.40/25.46 % (2222458)Termination phase: Finite model building preprocessing % 177.40/25.46 % (2222458)Time elapsed: 0.597 s % 177.40/25.46 % (2222458)Peak memory usage: 76 MB % 177.40/25.46 % (2222458)Instructions burned: 2178 (million) % 177.40/25.46 % (2222460)ott-2_1_sil=16000:newcnf=on:random_seed=950648007:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2959 on theBenchmark for (2959ds/869Mi) % 177.40/25.46 % Detected minimum model sizes of [5] % 177.40/25.46 % Detected maximum model sizes of [max] % 177.40/25.46 % (2222452)Instruction limit reached! % 177.40/25.46 % (2222452)------------------------------ % 177.40/25.46 % (2222452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.40/25.46 % (2222452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.40/25.46 % (2222452)CaDiCaL version: 2.1.3 % 177.40/25.46 % (2222452)Termination reason: Instruction limit % 177.40/25.46 % (2222452)Termination phase: Saturation % 177.40/25.46 % (2222452)Time elapsed: 2.967 s % 177.40/25.46 % (2222452)Peak memory usage: 101 MB % 177.40/25.46 % (2222452)Instructions burned: 5131 (million) % 177.40/25.46 % (2222462)ott+10_1_sil=32000:tgt=ground:random_seed=2789103801:i=5114:av=off_2957 on theBenchmark for (2957ds/5114Mi) % 177.40/25.46 % (2222460)Instruction limit reached! % 177.40/25.46 % (2222460)------------------------------ % 177.40/25.46 % (2222460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.40/25.46 % (2222460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.40/25.46 % (2222460)CaDiCaL version: 2.1.3 % 177.40/25.46 % (2222460)Termination reason: Instruction limit % 177.40/25.46 % (2222460)Termination phase: Function definition elimination % 177.40/25.46 % (2222460)Time elapsed: 0.251 s % 177.40/25.46 % (2222460)Peak memory usage: 48 MB % 177.40/25.46 % (2222460)Instructions burned: 871 (million) % 177.40/25.46 % (2222464)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=796792924:i=54282_2957 on theBenchmark for (2957ds/54282Mi) % 177.40/25.46 % Detected minimum model sizes of [5] % 177.40/25.46 % Detected maximum model sizes of [max] % 177.40/25.46 % TRYING [5] % 177.40/25.46 % (2222456)Instruction limit reached! % 177.40/25.46 % (2222456)------------------------------ % 177.40/25.46 % (2222456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.40/25.46 % (2222456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.40/25.46 % (2222456)CaDiCaL version: 2.1.3 % 177.40/25.46 % (2222456)Termination reason: Instruction limit % 177.40/25.46 % (2222456)Termination phase: Finite model building preprocessing % 177.40/25.46 % (2222456)Time elapsed: 3.231 s % 177.40/25.46 % (2222456)Peak memory usage: 117 MB % 177.40/25.46 % (2222456)Instructions burned: 6326 (million) % 177.40/25.46 % (2222466)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3897312379:i=3512:aac=none_2942 on theBenchmark for (2942ds/3512Mi) % 177.40/25.46 % Detected minimum model sizes of [5] % 177.40/25.46 % Detected maximum model sizes of [max] % 177.40/25.46 % TRYING [5] % 177.40/25.46 % (2222462)Instruction limit reached! % 177.40/25.46 % (2222462)------------------------------ % 177.40/25.46 % (2222462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.40/25.46 % (2222462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.40/25.46 % (2222462)CaDiCaL version: 2.1.3 % 177.40/25.46 % (2222462)Termination reason: Instruction limit % 177.40/25.46 % (2222462)Termination phase: Saturation % 177.40/25.46 % (2222462)Time elapsed: 2.984 s % 177.40/25.46 % (2222462)Peak memory usage: 112 MB % 177.40/25.46 % (2222462)Instructions burned: 5115 (million) % 177.40/25.46 % (2222468)dis+21_1_sil=32000:sas=cadical:random_seed=2622512834:i=3773:amm=off_2927 on theBenchmark for (2927ds/3773Mi) % 257.02/36.60 % (2222466)Instruction limit reached! % 257.02/36.60 % (2222466)------------------------------ % 257.02/36.60 % (2222466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.02/36.60 % (2222466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.02/36.60 % (2222466)CaDiCaL version: 2.1.3 % 257.02/36.60 % (2222466)Termination reason: Instruction limit % 257.02/36.60 % (2222466)Termination phase: Saturation % 257.02/36.60 % (2222466)Time elapsed: 1.854 s % 257.02/36.60 % (2222466)Peak memory usage: 75 MB % 257.02/36.60 % (2222466)Instructions burned: 3513 (million) % 257.02/36.60 % (2222470)ott+11_1_sil=16000:gs=on:random_seed=3748152287:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2923 on theBenchmark for (2923ds/2251Mi) % 257.02/36.60 % (2222470)Instruction limit reached! % 257.02/36.60 % (2222470)------------------------------ % 257.02/36.60 % (2222470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.02/36.60 % (2222470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.02/36.60 % (2222470)CaDiCaL version: 2.1.3 % 257.02/36.60 % (2222470)Termination reason: Instruction limit % 257.02/36.60 % (2222470)Termination phase: Saturation % 257.02/36.60 % (2222470)Time elapsed: 1.283 s % 257.02/36.60 % (2222470)Peak memory usage: 74 MB % 257.02/36.60 % (2222470)Instructions burned: 2252 (million) % 257.02/36.60 % (2222472)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3492114040:fmbsr=1.6:i=67534_2910 on theBenchmark for (2910ds/67534Mi) % 257.02/36.60 % (2222468)Instruction limit reached! % 257.02/36.60 % (2222468)------------------------------ % 257.02/36.60 % (2222468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.02/36.60 % (2222468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.02/36.60 % (2222468)CaDiCaL version: 2.1.3 % 257.02/36.60 % (2222468)Termination reason: Instruction limit % 257.02/36.60 % (2222468)Termination phase: Saturation % 257.02/36.60 % (2222468)Time elapsed: 1.981 s % 257.02/36.60 % (2222468)Peak memory usage: 78 MB % 257.02/36.60 % (2222468)Instructions burned: 3774 (million) % 257.02/36.60 % (2222474)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3912648058:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2907 on theBenchmark for (2907ds/4591Mi) % 257.02/36.60 % (2222446)Instruction limit reached! % 257.02/36.60 % (2222446)------------------------------ % 257.02/36.60 % (2222446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.02/36.60 % (2222446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.02/36.60 % (2222446)CaDiCaL version: 2.1.3 % 257.02/36.60 % (2222446)Termination reason: Instruction limit % 257.02/36.60 % (2222446)Termination phase: Finite model building constraint generation % 257.02/36.60 % (2222446)Time elapsed: 9.842 s % 257.02/36.60 % (2222446)Peak memory usage: 1656 MB % 257.02/36.60 % (2222446)Instructions burned: 22066 (million) % 257.02/36.60 % (2222476)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=637875430:i=29340_2889 on theBenchmark for (2889ds/29340Mi) % 257.02/36.60 % (2222474)Instruction limit reached! % 257.02/36.60 % (2222474)------------------------------ % 257.02/36.60 % (2222474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.02/36.60 % (2222474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.02/36.60 % (2222474)CaDiCaL version: 2.1.3 % 257.02/36.60 % (2222474)Termination reason: Instruction limit % 257.02/36.60 % (2222474)Termination phase: Saturation % 257.02/36.60 % (2222474)Time elapsed: 2.312 s % 257.02/36.60 % (2222474)Peak memory usage: 86 MB % 257.02/36.60 % (2222474)Instructions burned: 4593 (million) % 257.02/36.60 % (2222478)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1094937562:i=5211_2884 on theBenchmark for (2884ds/5211Mi) % 257.02/36.60 % Detected minimum model sizes of [5] % 257.02/36.60 % Detected maximum model sizes of [max] % 257.02/36.60 % (2222478)Instruction limit reached! % 257.02/36.60 % (2222478)------------------------------ % 257.02/36.60 % (2222478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.02/36.60 % (2222478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.02/36.60 % (2222478)CaDiCaL version: 2.1.3 % 257.02/36.60 % (2222478)Termination reason: Instruction limit % 257.02/36.60 % (2222478)Termination phase: Saturation % 257.02/36.60 % (2222478)Time elapsed: 1.928 s % 257.02/36.60 % (2222478)Peak memory usage: 82 MB % 257.02/36.60 % (2222478)Instructions burned: 5214 (million) % 257.02/36.60 % (2222480)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=727493362:i=5497:nm=2_2864 on theBenchmark for (2864ds/5497Mi) % 300.25/42.74 % (2222464)Instruction limit reached! % 300.25/42.74 % (2222464)------------------------------ % 300.25/42.74 % (2222464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.74 % (2222464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/42.74 % (2222464)CaDiCaL version: 2.1.3 % 300.25/42.74 % (2222464)Termination reason: Instruction limit % 300.25/42.74 % (2222464)Termination phase: Finite model building constraint generation % 300.25/42.74 % (2222464)Time elapsed: 10.884 s % 300.25/42.74 % (2222464)Peak memory usage: 2182 MB % 300.25/42.74 % (2222464)Instructions burned: 54285 (million) % 300.25/42.74 % (2222482)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1909493444:fmbsr=2:i=46332_2846 on theBenchmark for (2846ds/46332Mi) % 300.25/42.74 % (2222480)Instruction limit reached! % 300.25/42.74 % (2222480)------------------------------ % 300.25/42.74 % (2222480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.74 % (2222480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/42.74 % (2222480)CaDiCaL version: 2.1.3 % 300.25/42.74 % (2222480)Termination reason: Instruction limit % 300.25/42.74 % (2222480)Termination phase: Finite model building preprocessing % 300.25/42.74 % (2222480)Time elapsed: 2.945 s % 300.25/42.74 % (2222480)Peak memory usage: 118 MB % 300.25/42.74 % (2222480)Instructions burned: 5499 (million) % 300.25/42.74 % (2222484)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2261276967:i=14071_2834 on theBenchmark for (2834ds/14071Mi) % 300.25/42.74 % Detected minimum model sizes of [5] % 300.25/42.74 % Detected maximum model sizes of [max] % 300.25/42.74 % (2222482)Cannot represent all propositional literals internally % 300.25/42.74 % (2222482)Refutation not found, incomplete strategy % 300.25/42.74 % (2222482)------------------------------ % 300.25/42.74 % (2222482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.74 % (2222482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/42.74 % (2222482)CaDiCaL version: 2.1.3 % 300.25/42.74 % (2222482)Termination reason: Refutation not found, incomplete strategy % 300.25/42.74 % (2222482)Time elapsed: 2.439 s % 300.25/42.74 % (2222482)Peak memory usage: 150 MB % 300.25/42.74 % (2222482)Instructions burned: 9359 (million) % 300.25/42.74 % (2222482)------------------------------ % 300.25/42.74 % (2222482)------------------------------ % 300.25/42.74 % (2222486)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=928140923:i=22565:add=on:rawr=on_2821 on theBenchmark for (2821ds/22565Mi) % 300.25/42.74 % Detected minimum model sizes of [5] % 300.25/42.74 % Detected maximum model sizes of [max] % 300.25/42.74 % (2222484)Cannot represent all propositional literals internally % 300.25/42.74 % (2222484)Refutation not found, incomplete strategy % 300.25/42.74 % (2222484)------------------------------ % 300.25/42.74 % (2222484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.74 % (2222484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/42.74 % (2222484)CaDiCaL version: 2.1.3 % 300.25/42.74 % (2222484)Termination reason: Refutation not found, incomplete strategy % 300.25/42.74 % (2222484)Time elapsed: 4.415 s % 300.25/42.74 % (2222484)Peak memory usage: 162 MB % 300.25/42.74 % (2222484)Instructions burned: 8944 (million) % 300.25/42.74 % (2222484)------------------------------ % 300.25/42.74 % (2222484)------------------------------ % 300.25/42.74 % (2222488)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3776477960:i=8173:av=off_2789 on theBenchmark for (2789ds/8173Mi) % 300.25/42.74 % (2222476)Instruction limit reached! % 300.25/42.74 % (2222476)------------------------------ % 300.25/42.74 % (2222476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.74 % (2222476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/42.74 % (2222476)CaDiCaL version: 2.1.3 % 300.25/42.74 % (2222476)Termination reason: Instruction limit % 300.25/42.74 % (2222476)Termination phase: Saturation % 300.25/42.74 % (2222476)Time elapsed: 13.901 s % 300.25/42.74 % (2222476)Peak memory usage: 364 MB % 300.25/42.74 % (2222476)Instructions burned: 29342 (million) % 300.25/42.74 % (2222491)dis+10_16:1_sil=16000:random_seed=3631350272:i=9155:fsr=off_2749 on theBenchmark for (2749ds/9155Mi) % 300.25/42.74 % (2222486)Instruction limit reached! % 300.25/42.74 % (2222486)------------------------------ % 300.25/42.74 % (2222486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.74 % (2222486)Linked with Z3 4.14.0.0 3c47fd % 300.25/42.74 Terminated %------------------------------------------------------------------------------