%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW478_20 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:16 PM UTC 2026 % Result : Timeout 298.27s 42.32s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW478_20 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.18 % Computer : n001.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 14:19:48 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 27.77/4.28 % (369216)Will run a generic schedule for satisfiability detection. % 27.77/4.28 % (369223)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3592486630:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 27.77/4.28 % (369222)% WARNING: option uhcvi not known. % 27.77/4.28 % (369221)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3188129386_2999 on theBenchmark for (2999ds/0Mi) % 27.77/4.28 % (369222)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4267500006:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 27.77/4.28 % (369224)dis+10_1_sil=32000:sp=arity:random_seed=333544494:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 27.77/4.28 % (369225)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2724000939:i=116_2999 on theBenchmark for (2999ds/116Mi) % 27.77/4.28 % (369226)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1142453918:i=131_2999 on theBenchmark for (2999ds/131Mi) % 27.77/4.28 % (369227)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2315616377:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 27.77/4.28 % (369224)Instruction limit reached! % 27.77/4.28 % (369224)------------------------------ % 27.77/4.28 % (369224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.77/4.28 % (369224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.77/4.28 % (369224)CaDiCaL version: 2.1.3 % 27.77/4.28 % (369224)Termination reason: Instruction limit % 27.77/4.28 % (369224)Termination phase: Saturation % 27.77/4.28 % (369224)Time elapsed: 0.052 s % 27.77/4.28 % (369224)Peak memory usage: 14 MB % 27.77/4.28 % (369224)Instructions burned: 104 (million) % 27.77/4.28 % (369225)Instruction limit reached! % 27.77/4.28 % (369225)------------------------------ % 27.77/4.28 % (369225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.77/4.28 % (369225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.77/4.28 % (369225)CaDiCaL version: 2.1.3 % 27.77/4.28 % (369225)Termination reason: Instruction limit % 27.77/4.28 % (369225)Termination phase: Saturation % 27.77/4.28 % (369225)Time elapsed: 0.061 s % 27.77/4.28 % (369225)Peak memory usage: 14 MB % 27.77/4.28 % (369225)Instructions burned: 116 (million) % 27.77/4.28 % (369226)Instruction limit reached! % 27.77/4.28 % (369226)------------------------------ % 27.77/4.28 % (369226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.77/4.28 % (369226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.77/4.28 % (369226)CaDiCaL version: 2.1.3 % 27.77/4.28 % (369226)Termination reason: Instruction limit % 27.77/4.28 % (369226)Termination phase: Saturation % 27.77/4.28 % (369226)Time elapsed: 0.067 s % 27.77/4.28 % (369226)Peak memory usage: 15 MB % 27.77/4.28 % (369226)Instructions burned: 132 (million) % 27.77/4.28 % (369235)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3001790781:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 27.77/4.28 % (369236)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=360417219:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 27.77/4.28 % (369227)Instruction limit reached! % 27.77/4.28 % (369227)------------------------------ % 27.77/4.28 % (369227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.77/4.28 % (369227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.77/4.28 % (369227)CaDiCaL version: 2.1.3 % 27.77/4.28 % (369227)Termination reason: Instruction limit % 27.77/4.28 % (369227)Termination phase: Saturation % 27.77/4.28 % (369227)Time elapsed: 0.085 s % 27.77/4.28 % (369227)Peak memory usage: 15 MB % 27.77/4.28 % (369227)Instructions burned: 159 (million) % 27.77/4.28 % (369237)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=4185862981:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 27.77/4.28 % (369241)ott-21_1_sil=16000:fs=off:random_seed=2480843985:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 27.77/4.28 % (369236)Instruction limit reached! % 27.77/4.28 % (369236)------------------------------ % 27.77/4.28 % (369236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.77/4.28 % (369236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.77/4.28 % (369236)CaDiCaL version: 2.1.3 % 27.77/4.28 % (369236)Termination reason: Instruction limit % 65.39/9.54 % (369236)Termination phase: Saturation % 65.39/9.54 % (369236)Time elapsed: 0.070 s % 65.39/9.54 % (369236)Peak memory usage: 15 MB % 65.39/9.54 % (369236)Instructions burned: 131 (million) % 65.39/9.54 % (369243)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1739420759:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 65.39/9.54 % (369241)Instruction limit reached! % 65.39/9.54 % (369241)------------------------------ % 65.39/9.54 % (369241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.39/9.54 % (369241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.39/9.54 % (369241)CaDiCaL version: 2.1.3 % 65.39/9.54 % (369241)Termination reason: Instruction limit % 65.39/9.54 % (369241)Termination phase: Saturation % 65.39/9.54 % (369241)Time elapsed: 0.093 s % 65.39/9.54 % (369241)Peak memory usage: 14 MB % 65.39/9.54 % (369241)Instructions burned: 181 (million) % 65.39/9.54 % (369245)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=989469337:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 65.39/9.54 % (369235)Instruction limit reached! % 65.39/9.54 % (369235)------------------------------ % 65.39/9.54 % (369235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.39/9.54 % (369235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.39/9.54 % (369235)CaDiCaL version: 2.1.3 % 65.39/9.54 % (369235)Termination reason: Instruction limit % 65.39/9.54 % (369235)Termination phase: Finite model building preprocessing % 65.39/9.54 % (369235)Time elapsed: 0.300 s % 65.39/9.54 % (369235)Peak memory usage: 16 MB % 65.39/9.54 % (369235)Instructions burned: 715 (million) % 65.39/9.54 % (369247)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3205976243:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 65.39/9.54 % (369237)Instruction limit reached! % 65.39/9.54 % (369237)------------------------------ % 65.39/9.54 % (369237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.39/9.54 % (369237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.39/9.54 % (369237)CaDiCaL version: 2.1.3 % 65.39/9.54 % (369237)Termination reason: Instruction limit % 65.39/9.54 % (369237)Termination phase: Saturation % 65.39/9.54 % (369237)Time elapsed: 0.353 s % 65.39/9.54 % (369237)Peak memory usage: 18 MB % 65.39/9.54 % (369237)Instructions burned: 685 (million) % 65.39/9.54 % (369243)Instruction limit reached! % 65.39/9.54 % (369243)------------------------------ % 65.39/9.54 % (369243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.39/9.54 % (369243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.39/9.54 % (369243)CaDiCaL version: 2.1.3 % 65.39/9.54 % (369243)Termination reason: Instruction limit % 65.39/9.54 % (369243)Termination phase: Saturation % 65.39/9.54 % (369243)Time elapsed: 0.268 s % 65.39/9.54 % (369243)Peak memory usage: 16 MB % 65.39/9.54 % (369243)Instructions burned: 479 (million) % 65.39/9.54 % (369250)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=3444790287:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 65.39/9.54 % (369249)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3198876323:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 65.39/9.54 % (369245)Instruction limit reached! % 65.39/9.54 % (369245)------------------------------ % 65.39/9.54 % (369245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.39/9.54 % (369245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.39/9.54 % (369245)CaDiCaL version: 2.1.3 % 65.39/9.54 % (369245)Termination reason: Instruction limit % 65.39/9.54 % (369245)Termination phase: Finite model building preprocessing % 65.39/9.54 % (369245)Time elapsed: 0.433 s % 65.39/9.54 % (369245)Peak memory usage: 27 MB % 65.39/9.54 % (369245)Instructions burned: 866 (million) % 65.39/9.54 % (369253)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3834502158:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 65.39/9.54 % (369250)Instruction limit reached! % 65.39/9.54 % (369250)------------------------------ % 65.39/9.54 % (369250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.39/9.54 % (369250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.39/9.54 % (369250)CaDiCaL version: 2.1.3 % 65.39/9.54 % (369250)Termination reason: Instruction limit % 65.39/9.54 % (369250)Termination phase: Saturation % 92.32/13.36 % (369250)Time elapsed: 0.399 s % 92.32/13.36 % (369250)Peak memory usage: 18 MB % 92.32/13.36 % (369250)Instructions burned: 692 (million) % 92.32/13.36 % (369255)fmb+10_1_sil=64000:random_seed=3456598542:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 92.32/13.36 % (369249)Instruction limit reached! % 92.32/13.36 % (369249)------------------------------ % 92.32/13.36 % (369249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.32/13.36 % (369249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.32/13.36 % (369249)CaDiCaL version: 2.1.3 % 92.32/13.36 % (369249)Termination reason: Instruction limit % 92.32/13.36 % (369249)Termination phase: Finite model building preprocessing % 92.32/13.36 % (369249)Time elapsed: 0.444 s % 92.32/13.36 % (369249)Peak memory usage: 27 MB % 92.32/13.36 % (369249)Instructions burned: 889 (million) % 92.32/13.36 % (369257)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3773745052:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 92.32/13.36 % (369247)Instruction limit reached! % 92.32/13.36 % (369247)------------------------------ % 92.32/13.36 % (369247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.32/13.36 % (369247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.32/13.36 % (369247)CaDiCaL version: 2.1.3 % 92.32/13.36 % (369247)Termination reason: Instruction limit % 92.32/13.36 % (369247)Termination phase: Saturation % 92.32/13.36 % (369247)Time elapsed: 0.647 s % 92.32/13.36 % (369247)Peak memory usage: 21 MB % 92.32/13.36 % (369247)Instructions burned: 1180 (million) % 92.32/13.36 % (369259)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2623458233:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 92.32/13.36 % (369253)Instruction limit reached! % 92.32/13.36 % (369253)------------------------------ % 92.32/13.36 % (369253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.32/13.36 % (369253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.32/13.36 % (369253)CaDiCaL version: 2.1.3 % 92.32/13.36 % (369253)Termination reason: Instruction limit % 92.32/13.36 % (369253)Termination phase: Saturation % 92.32/13.36 % (369253)Time elapsed: 0.445 s % 92.32/13.36 % (369253)Peak memory usage: 19 MB % 92.32/13.36 % (369253)Instructions burned: 879 (million) % 92.32/13.36 % (369261)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4184000388:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 92.32/13.36 % (369259)Instruction limit reached! % 92.32/13.36 % (369259)------------------------------ % 92.32/13.36 % (369259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.32/13.36 % (369259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.32/13.36 % (369259)CaDiCaL version: 2.1.3 % 92.32/13.36 % (369259)Termination reason: Instruction limit % 92.32/13.36 % (369259)Termination phase: Finite model building preprocessing % 92.32/13.36 % (369259)Time elapsed: 0.461 s % 92.32/13.36 % (369259)Peak memory usage: 27 MB % 92.32/13.36 % (369259)Instructions burned: 921 (million) % 92.32/13.36 % (369263)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1613760359:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi) % 92.32/13.36 % (369263)Instruction limit reached! % 92.32/13.36 % (369263)------------------------------ % 92.32/13.36 % (369263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.32/13.36 % (369263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.32/13.36 % (369263)CaDiCaL version: 2.1.3 % 92.32/13.36 % (369263)Termination reason: Instruction limit % 92.32/13.36 % (369263)Termination phase: Saturation % 92.32/13.36 % (369263)Time elapsed: 0.774 s % 92.32/13.36 % (369263)Peak memory usage: 23 MB % 92.32/13.36 % (369263)Instructions burned: 1473 (million) % 92.32/13.36 % (369265)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1504063401:i=6324_2975 on theBenchmark for (2975ds/6324Mi) % 92.32/13.36 % (369261)Instruction limit reached! % 92.32/13.36 % (369261)------------------------------ % 92.32/13.36 % (369261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.32/13.36 % (369261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.32/13.36 % (369261)CaDiCaL version: 2.1.3 % 92.32/13.36 % (369261)Termination reason: Instruction limit % 92.32/13.36 % (369261)Termination phase: Saturation % 92.32/13.36 % (369261)Time elapsed: 2.784 s % 92.32/13.36 % (369261)Peak memory usage: 39 MB % 92.32/13.36 % (369261)Instructions burned: 5133 (million) % 92.32/13.36 % (369267)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=478348656:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi) % 112.44/16.14 % (369267)Instruction limit reached! % 112.44/16.14 % (369267)------------------------------ % 112.44/16.14 % (369267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.44/16.14 % (369267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.14 % (369267)CaDiCaL version: 2.1.3 % 112.44/16.14 % (369267)Termination reason: Instruction limit % 112.44/16.14 % (369267)Termination phase: Finite model building preprocessing % 112.44/16.14 % (369267)Time elapsed: 1.068 s % 112.44/16.14 % (369267)Peak memory usage: 32 MB % 112.44/16.14 % (369267)Instructions burned: 2175 (million) % 112.44/16.14 % (369269)ott-2_1_sil=16000:newcnf=on:random_seed=292154999:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2948 on theBenchmark for (2948ds/869Mi) % 112.44/16.14 % (369257)Instruction limit reached! % 112.44/16.14 % (369257)------------------------------ % 112.44/16.14 % (369257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.44/16.14 % (369257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.14 % (369257)CaDiCaL version: 2.1.3 % 112.44/16.14 % (369257)Termination reason: Instruction limit % 112.44/16.14 % (369257)Termination phase: Finite model building preprocessing % 112.44/16.14 % (369257)Time elapsed: 4.207 s % 112.44/16.14 % (369257)Peak memory usage: 70 MB % 112.44/16.14 % (369257)Instructions burned: 9516 (million) % 112.44/16.14 % (369265)Instruction limit reached! % 112.44/16.14 % (369265)------------------------------ % 112.44/16.14 % (369265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.44/16.14 % (369265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.14 % (369265)CaDiCaL version: 2.1.3 % 112.44/16.14 % (369265)Termination reason: Instruction limit % 112.44/16.14 % (369265)Termination phase: Finite model building preprocessing % 112.44/16.14 % (369265)Time elapsed: 2.810 s % 112.44/16.14 % (369265)Peak memory usage: 55 MB % 112.44/16.14 % (369265)Instructions burned: 6326 (million) % 112.44/16.14 % (369271)ott+10_1_sil=32000:tgt=ground:random_seed=2391671205:i=5114:av=off_2947 on theBenchmark for (2947ds/5114Mi) % 112.44/16.14 % (369273)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=916581791:i=54282_2947 on theBenchmark for (2947ds/54282Mi) % 112.44/16.14 % (369269)Instruction limit reached! % 112.44/16.14 % (369269)------------------------------ % 112.44/16.14 % (369269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.44/16.14 % (369269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.14 % (369269)CaDiCaL version: 2.1.3 % 112.44/16.14 % (369269)Termination reason: Instruction limit % 112.44/16.14 % (369269)Termination phase: Saturation % 112.44/16.14 % (369269)Time elapsed: 0.378 s % 112.44/16.14 % (369269)Peak memory usage: 20 MB % 112.44/16.14 % (369269)Instructions burned: 870 (million) % 112.44/16.14 % (369275)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3550731816:i=3512:aac=none_2944 on theBenchmark for (2944ds/3512Mi) % 112.44/16.14 % (369275)Instruction limit reached! % 112.44/16.14 % (369275)------------------------------ % 112.44/16.14 % (369275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.44/16.14 % (369275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.14 % (369275)CaDiCaL version: 2.1.3 % 112.44/16.14 % (369275)Termination reason: Instruction limit % 112.44/16.14 % (369275)Termination phase: Saturation % 112.44/16.14 % (369275)Time elapsed: 1.968 s % 112.44/16.14 % (369275)Peak memory usage: 33 MB % 112.44/16.14 % (369275)Instructions burned: 3512 (million) % 112.44/16.14 % (369277)dis+21_1_sil=32000:sas=cadical:random_seed=455220516:i=3773:amm=off_2924 on theBenchmark for (2924ds/3773Mi) % 112.44/16.14 % (369271)Instruction limit reached! % 112.44/16.14 % (369271)------------------------------ % 112.44/16.14 % (369271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.44/16.14 % (369271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.14 % (369271)CaDiCaL version: 2.1.3 % 112.44/16.14 % (369271)Termination reason: Instruction limit % 112.44/16.14 % (369271)Termination phase: Saturation % 112.44/16.14 % (369271)Time elapsed: 2.742 s % 112.44/16.14 % (369271)Peak memory usage: 30 MB % 112.44/16.14 % (369271)Instructions burned: 5115 (million) % 112.44/16.14 % (369279)ott+11_1_sil=16000:gs=on:random_seed=817648980:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2919 on theBenchmark for (2919ds/2251Mi) % 112.44/16.14 % (369279)Instruction limit reached! % 112.44/16.14 % (369279)------------------------------ % 129.94/18.69 % (369279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.94/18.69 % (369279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.94/18.69 % (369279)CaDiCaL version: 2.1.3 % 129.94/18.69 % (369279)Termination reason: Instruction limit % 129.94/18.69 % (369279)Termination phase: Saturation % 129.94/18.69 % (369279)Time elapsed: 1.281 s % 129.94/18.69 % (369279)Peak memory usage: 32 MB % 129.94/18.69 % (369279)Instructions burned: 2253 (million) % 129.94/18.69 % (369281)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2699766784:fmbsr=1.6:i=67534_2906 on theBenchmark for (2906ds/67534Mi) % 129.94/18.69 % (369277)Instruction limit reached! % 129.94/18.69 % (369277)------------------------------ % 129.94/18.69 % (369277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.94/18.69 % (369277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.94/18.69 % (369277)CaDiCaL version: 2.1.3 % 129.94/18.69 % (369277)Termination reason: Instruction limit % 129.94/18.69 % (369277)Termination phase: Saturation % 129.94/18.69 % (369277)Time elapsed: 2.116 s % 129.94/18.69 % (369277)Peak memory usage: 34 MB % 129.94/18.69 % (369277)Instructions burned: 3773 (million) % 129.94/18.69 % (369283)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2629060309:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2903 on theBenchmark for (2903ds/4591Mi) % 129.94/18.69 % (369255)Instruction limit reached! % 129.94/18.69 % (369255)------------------------------ % 129.94/18.69 % (369255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.94/18.69 % (369255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.94/18.69 % (369255)CaDiCaL version: 2.1.3 % 129.94/18.69 % (369255)Termination reason: Instruction limit % 129.94/18.69 % (369255)Termination phase: Finite model building preprocessing % 129.94/18.69 % (369255)Time elapsed: 9.509 s % 129.94/18.69 % (369255)Peak memory usage: 129 MB % 129.94/18.69 % (369255)Instructions burned: 22063 (million) % 129.94/18.69 % (369285)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1653261012:i=29340_2894 on theBenchmark for (2894ds/29340Mi) % 129.94/18.69 % (369283)Instruction limit reached! % 129.94/18.69 % (369283)------------------------------ % 129.94/18.69 % (369283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.94/18.69 % (369283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.94/18.69 % (369283)CaDiCaL version: 2.1.3 % 129.94/18.69 % (369283)Termination reason: Instruction limit % 129.94/18.69 % (369283)Termination phase: Saturation % 129.94/18.69 % (369283)Time elapsed: 1.861 s % 129.94/18.69 % (369283)Peak memory usage: 34 MB % 129.94/18.69 % (369283)Instructions burned: 4591 (million) % 129.94/18.69 % (369287)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2889493117:i=5211_2884 on theBenchmark for (2884ds/5211Mi) % 129.94/18.69 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 129.94/18.69 % Detected maximum model sizes of [max,max,max,max,2,max,max,max,max,max,max,max,max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max] % 129.94/18.69 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 129.94/18.69 % TRYING [1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 129.94/18.69 % TRYING [1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 129.94/18.69 % TRYING [1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 129.94/18.69 % TRYING [1,1,1,1,1,1,1,1,3,1,1,1,1,1,1,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 129.94/18.69 % TRYING [1,1,1,1,1,1,1,2,3,1,1,1,1,1,1,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 129.94/18.69 % TRYING [1,1,1,1,1,1,1,2,3,1,1,1,1,1,1,2,2,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 129.94/18.69 % TRYING [1,1,1,1,1,1,1,2,3,1,1,1,1,1,1,2,2,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 156.88/22.44 % TRYING [1,1,1,1,1,1,1,2,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 156.88/22.44 % TRYING [1,1,1,1,1,1,1,3,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 156.88/22.44 % TRYING [1,1,1,1,1,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 156.88/22.44 % TRYING [1,1,1,1,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 156.88/22.44 % TRYING [1,1,1,1,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,1,2,1,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,2,2,1,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,3,2,1,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,2,2,2,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [2,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,2,3,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % (369287)Instruction limit reached! % 156.88/22.44 % (369287)------------------------------ % 156.88/22.44 % (369287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.88/22.44 % (369287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.88/22.44 % (369287)CaDiCaL version: 2.1.3 % 156.88/22.44 % (369287)Termination reason: Instruction limit % 156.88/22.44 % (369287)Termination phase: Saturation % 156.88/22.44 % (369287)Time elapsed: 2.759 s % 156.88/22.44 % (369287)Peak memory usage: 51 MB % 156.88/22.44 % (369287)Instructions burned: 5212 (million) % 156.88/22.44 % TRYING [1,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % (369506)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=599244585:i=5497:nm=2_2856 on theBenchmark for (2856ds/5497Mi) % 156.88/22.44 % TRYING [1,2,3,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,2,2,2,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,2,2,1,2,2,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,2,3,1,2,2,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [2,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [2,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [2,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,2,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [2,2,2,2,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,2,4,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 156.88/22.44 % TRYING [1,2,4,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 197.55/28.18 % TRYING [1,2,4,1,2,2,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1] % 197.55/28.18 % TRYING [1,2,5,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 197.55/28.18 % (369506)Instruction limit reached! % 197.55/28.18 % (369506)------------------------------ % 197.55/28.18 % (369506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.55/28.18 % (369506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.55/28.18 % (369506)CaDiCaL version: 2.1.3 % 197.55/28.18 % (369506)Termination reason: Instruction limit % 197.55/28.18 % (369506)Termination phase: Finite model building preprocessing % 197.55/28.18 % (369506)Time elapsed: 2.442 s % 197.55/28.18 % (369506)Peak memory usage: 51 MB % 197.55/28.18 % (369506)Instructions burned: 5498 (million) % 197.55/28.18 % (369650)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=432621410:fmbsr=2:i=46332_2831 on theBenchmark for (2831ds/46332Mi) % 197.55/28.18 % TRYING [1,2,5,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 197.55/28.18 % TRYING [1,2,5,1,2,2,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1] % 197.55/28.18 % (369650)Cannot represent all propositional literals internally % 197.55/28.18 % (369650)Refutation not found, incomplete strategy % 197.55/28.18 % (369650)------------------------------ % 197.55/28.18 % (369650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.55/28.18 % (369650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.55/28.18 % (369650)CaDiCaL version: 2.1.3 % 197.55/28.18 % (369650)Termination reason: Refutation not found, incomplete strategy % 197.55/28.18 % (369650)Time elapsed: 0.574 s % 197.55/28.18 % (369650)Peak memory usage: 25 MB % 197.55/28.18 % (369650)Instructions burned: 1239 (million) % 197.55/28.18 % (369650)------------------------------ % 197.55/28.18 % (369650)------------------------------ % 197.55/28.18 % (369652)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=731761828:i=14071_2825 on theBenchmark for (2825ds/14071Mi) % 197.55/28.18 % TRYING [1,2,6,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 197.55/28.18 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 197.55/28.18 % Detected maximum model sizes of [max,max,max,max,2,max,max,max,max,max,max,max,max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max] % 197.55/28.18 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 197.55/28.18 % TRYING [1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 197.55/28.18 % TRYING [1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 197.55/28.18 % TRYING [1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 197.55/28.18 % TRYING [1,1,1,1,1,1,1,1,3,1,1,1,1,1,1,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 197.55/28.18 % TRYING [1,1,1,1,1,1,1,2,3,1,1,1,1,1,1,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 197.55/28.18 % TRYING [1,1,1,1,1,1,1,2,3,1,1,1,1,1,1,2,2,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 197.55/28.18 % TRYING [1,1,1,1,1,1,1,2,3,1,1,1,1,1,1,2,2,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 197.55/28.18 % TRYING [1,1,1,1,1,1,1,2,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 197.55/28.18 % TRYING [1,1,1,1,1,1,1,3,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 298.27/42.32 % TRYING [1,1,1,1,1,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 298.27/42.32 % TRYING [1,2,6,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,1,1,1,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 298.27/42.32 % TRYING [1,1,1,1,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,1,2,1,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,2,1,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,3,2,1,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,2,2,2,1,1,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [2,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,6,1,2,2,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,3,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,3,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,2,2,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,2,1,2,2,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,7,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,3,1,2,2,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [2,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [2,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [2,2,2,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,2,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [2,2,2,2,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,4,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,4,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,7,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,4,1,2,2,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,5,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1] % 298.27/42.32 % TRYING [1,2,5,1,2,1,2,4,3,1,1,1,1,1,1,2,2,2,2,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,Terminated % 300.15/42.63 % Vampire exiting % 300.15/42.64 Terminated %------------------------------------------------------------------------------