%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV381+2 : TPTP v9.3.1. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:21:07 PM UTC 2026 % Result : Timeout 300.49s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV381+2 : TPTP v9.3.1. Released v3.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n003.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 10:48:27 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.21 Running first-order model finding % 0.07/0.21 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 % 13.97/2.20 % (1506964)Will run a generic schedule for satisfiability detection. % 13.97/2.20 % (1506973)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3347648281:i=116_2999 on theBenchmark for (2999ds/116Mi) % 13.97/2.20 % (1506970)% WARNING: option uhcvi not known. % 13.97/2.20 % (1506970)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2995163527:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 13.97/2.20 % (1506969)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=230789082_2999 on theBenchmark for (2999ds/0Mi) % 13.97/2.20 % (1506971)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2731958511:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 13.97/2.20 % (1506972)dis+10_1_sil=32000:sp=arity:random_seed=220170724:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 13.97/2.20 % (1506974)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2407572120:i=131_2999 on theBenchmark for (2999ds/131Mi) % 13.97/2.20 % (1506975)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4011779173:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 13.97/2.20 % TRYING [1] % 13.97/2.20 % TRYING [2] % 13.97/2.20 % TRYING [3] % 13.97/2.20 % (1506973)Instruction limit reached! % 13.97/2.20 % (1506973)------------------------------ % 13.97/2.20 % (1506973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.97/2.20 % (1506973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.97/2.20 % (1506973)CaDiCaL version: 2.1.3 % 13.97/2.20 % (1506973)Termination reason: Instruction limit % 13.97/2.20 % (1506973)Termination phase: Saturation % 13.97/2.20 % (1506973)Time elapsed: 0.031 s % 13.97/2.20 % (1506973)Peak memory usage: 12 MB % 13.97/2.20 % (1506973)Instructions burned: 116 (million) % 13.97/2.20 % (1506983)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2587542073:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 13.97/2.20 % TRYING [4] % 13.97/2.20 % TRYING [1] % 13.97/2.20 % TRYING [2] % 13.97/2.20 % TRYING [3] % 13.97/2.20 % TRYING [4] % 13.97/2.20 % (1506975)Instruction limit reached! % 13.97/2.20 % (1506975)------------------------------ % 13.97/2.20 % (1506975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.97/2.20 % (1506975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.97/2.20 % (1506975)CaDiCaL version: 2.1.3 % 13.97/2.20 % (1506975)Termination reason: Instruction limit % 13.97/2.20 % (1506975)Termination phase: Saturation % 13.97/2.20 % (1506975)Time elapsed: 0.062 s % 13.97/2.20 % (1506975)Peak memory usage: 11 MB % 13.97/2.20 % (1506975)Instructions burned: 161 (million) % 13.97/2.20 % (1506972)Instruction limit reached! % 13.97/2.20 % (1506972)------------------------------ % 13.97/2.20 % (1506972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.97/2.20 % (1506972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.97/2.20 % (1506972)CaDiCaL version: 2.1.3 % 13.97/2.20 % (1506972)Termination reason: Instruction limit % 13.97/2.20 % (1506972)Termination phase: Saturation % 13.97/2.20 % (1506972)Time elapsed: 0.066 s % 13.97/2.20 % (1506972)Peak memory usage: 12 MB % 13.97/2.20 % (1506972)Instructions burned: 104 (million) % 13.97/2.20 % (1506974)Instruction limit reached! % 13.97/2.20 % (1506974)------------------------------ % 13.97/2.20 % (1506974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.97/2.20 % (1506974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.97/2.20 % (1506974)CaDiCaL version: 2.1.3 % 13.97/2.20 % (1506974)Termination reason: Instruction limit % 13.97/2.20 % (1506974)Termination phase: Saturation % 13.97/2.20 % (1506974)Time elapsed: 0.079 s % 13.97/2.20 % (1506974)Peak memory usage: 13 MB % 13.97/2.20 % (1506974)Instructions burned: 131 (million) % 13.97/2.20 % (1506985)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1832394577:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 13.97/2.20 % (1506986)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=1313737646:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 13.97/2.20 % (1506987)ott-21_1_sil=16000:fs=off:random_seed=2441383521:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 13.97/2.20 % TRYING [5] % 13.97/2.20 % TRYING [5] % 13.97/2.20 % (1506985)Instruction limit reached! % 13.97/2.20 % (1506985)------------------------------ % 13.97/2.20 % (1506985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.52/5.84 % (1506985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.52/5.84 % (1506985)CaDiCaL version: 2.1.3 % 39.52/5.84 % (1506985)Termination reason: Instruction limit % 39.52/5.84 % (1506985)Termination phase: Saturation % 39.52/5.84 % (1506985)Time elapsed: 0.082 s % 39.52/5.84 % (1506985)Peak memory usage: 13 MB % 39.52/5.84 % (1506985)Instructions burned: 131 (million) % 39.52/5.84 % (1506987)Instruction limit reached! % 39.52/5.84 % (1506987)------------------------------ % 39.52/5.84 % (1506987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.52/5.84 % (1506987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.52/5.84 % (1506987)CaDiCaL version: 2.1.3 % 39.52/5.84 % (1506987)Termination reason: Instruction limit % 39.52/5.84 % (1506987)Termination phase: Saturation % 39.52/5.84 % (1506987)Time elapsed: 0.068 s % 39.52/5.84 % (1506987)Peak memory usage: 11 MB % 39.52/5.84 % (1506987)Instructions burned: 180 (million) % 39.52/5.84 % (1506983)Instruction limit reached! % 39.52/5.84 % (1506983)------------------------------ % 39.52/5.84 % (1506983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.52/5.84 % (1506983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.52/5.84 % (1506983)CaDiCaL version: 2.1.3 % 39.52/5.84 % (1506983)Termination reason: Instruction limit % 39.52/5.84 % (1506983)Termination phase: Finite model building constraint generation % 39.52/5.84 % (1506983)Time elapsed: 0.135 s % 39.52/5.84 % (1506983)Peak memory usage: 31 MB % 39.52/5.84 % (1506983)Instructions burned: 720 (million) % 39.52/5.84 % (1506993)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3658250577:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 39.52/5.84 % (1506991)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=661441006:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 39.52/5.84 % (1506992)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=962526186:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 39.52/5.84 % TRYING [1] % 39.52/5.84 % TRYING [2] % 39.52/5.84 % TRYING [3] % 39.52/5.84 % TRYING [4] % 39.52/5.84 % (1506986)Instruction limit reached! % 39.52/5.84 % (1506986)------------------------------ % 39.52/5.84 % (1506986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.52/5.84 % (1506986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.52/5.84 % (1506986)CaDiCaL version: 2.1.3 % 39.52/5.84 % (1506986)Termination reason: Instruction limit % 39.52/5.84 % (1506986)Termination phase: Saturation % 39.52/5.84 % (1506986)Time elapsed: 0.307 s % 39.52/5.84 % (1506986)Peak memory usage: 15 MB % 39.52/5.84 % (1506986)Instructions burned: 686 (million) % 39.52/5.84 % TRYING [6] % 39.52/5.84 % (1506997)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3416454906:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 39.52/5.84 % (1506991)Instruction limit reached! % 39.52/5.84 % (1506991)------------------------------ % 39.52/5.84 % (1506991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.52/5.84 % (1506991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.52/5.84 % (1506991)CaDiCaL version: 2.1.3 % 39.52/5.84 % (1506991)Termination reason: Instruction limit % 39.52/5.84 % (1506991)Termination phase: Saturation % 39.52/5.84 % (1506991)Time elapsed: 0.303 s % 39.52/5.84 % (1506991)Peak memory usage: 14 MB % 39.52/5.84 % (1506991)Instructions burned: 477 (million) % 39.52/5.84 % (1506999)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=198295193: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) % 39.52/5.84 % (1506992)Instruction limit reached! % 39.52/5.84 % (1506992)------------------------------ % 39.52/5.84 % (1506992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.52/5.84 % (1506992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.52/5.84 % (1506992)CaDiCaL version: 2.1.3 % 39.52/5.84 % (1506992)Termination reason: Instruction limit % 39.52/5.84 % (1506992)Termination phase: Finite model building SAT solving % 39.52/5.84 % (1506992)Time elapsed: 0.343 s % 39.52/5.84 % (1506992)Peak memory usage: 24 MB % 39.52/5.84 % (1506992)Instructions burned: 865 (million) % 39.52/5.84 % (1506993)Instruction limit reached! % 39.52/5.84 % (1506993)------------------------------ % 39.52/5.84 % (1506993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.52/5.84 % (1506993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.67/11.02 % (1506993)CaDiCaL version: 2.1.3 % 75.67/11.02 % (1506993)Termination reason: Instruction limit % 75.67/11.02 % (1506993)Termination phase: Saturation % 75.67/11.02 % (1506993)Time elapsed: 0.370 s % 75.67/11.02 % (1506993)Peak memory usage: 19 MB % 75.67/11.02 % (1506993)Instructions burned: 1181 (million) % 75.67/11.02 % (1507001)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1310270046:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 75.67/11.02 % (1507002)fmb+10_1_sil=64000:random_seed=4001767189:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 75.67/11.02 % TRYING [1] % 75.67/11.02 % TRYING [2] % 75.67/11.02 % TRYING [3] % 75.67/11.02 % TRYING [4] % 75.67/11.02 % TRYING [5] % 75.67/11.02 % (1506997)Instruction limit reached! % 75.67/11.02 % (1506997)------------------------------ % 75.67/11.02 % (1506997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.67/11.02 % (1506997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.67/11.02 % (1506997)CaDiCaL version: 2.1.3 % 75.67/11.02 % (1506997)Termination reason: Instruction limit % 75.67/11.02 % (1506997)Termination phase: Finite model building constraint generation % 75.67/11.02 % (1506997)Time elapsed: 0.410 s % 75.67/11.02 % (1506997)Peak memory usage: 113 MB % 75.67/11.02 % (1506997)Instructions burned: 889 (million) % 75.67/11.02 % (1507005)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2244704639:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 75.67/11.02 % TRYING [20] % 75.67/11.02 % (1506999)Instruction limit reached! % 75.67/11.02 % (1506999)------------------------------ % 75.67/11.02 % (1506999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.67/11.02 % (1506999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.67/11.02 % (1506999)CaDiCaL version: 2.1.3 % 75.67/11.02 % (1506999)Termination reason: Instruction limit % 75.67/11.02 % (1506999)Termination phase: Saturation % 75.67/11.02 % (1506999)Time elapsed: 0.370 s % 75.67/11.02 % (1506999)Peak memory usage: 18 MB % 75.67/11.02 % (1506999)Instructions burned: 693 (million) % 75.67/11.02 % (1507007)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1510511544:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 75.67/11.02 % TRYING [8] % 75.67/11.02 % (1507001)Instruction limit reached! % 75.67/11.02 % (1507001)------------------------------ % 75.67/11.02 % (1507001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.67/11.02 % (1507001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.67/11.02 % (1507001)CaDiCaL version: 2.1.3 % 75.67/11.02 % (1507001)Termination reason: Instruction limit % 75.67/11.02 % (1507001)Termination phase: Saturation % 75.67/11.02 % (1507001)Time elapsed: 0.527 s % 75.67/11.02 % (1507001)Peak memory usage: 18 MB % 75.67/11.02 % (1507001)Instructions burned: 880 (million) % 75.67/11.02 % (1507009)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=636457810:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 75.67/11.02 % TRYING [7] % 75.67/11.02 % (1507007)Instruction limit reached! % 75.67/11.02 % (1507007)------------------------------ % 75.67/11.02 % (1507007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.67/11.02 % (1507007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.67/11.02 % (1507007)CaDiCaL version: 2.1.3 % 75.67/11.02 % (1507007)Termination reason: Instruction limit % 75.67/11.02 % (1507007)Termination phase: Finite model building constraint generation % 75.67/11.02 % (1507007)Time elapsed: 0.328 s % 75.67/11.02 % (1507007)Peak memory usage: 75 MB % 75.67/11.02 % (1507007)Instructions burned: 921 (million) % 75.67/11.02 % (1507011)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3684718116:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi) % 75.67/11.02 % TRYING [6] % 75.67/11.02 % (1507011)Instruction limit reached! % 75.67/11.02 % (1507011)------------------------------ % 75.67/11.02 % (1507011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.67/11.02 % (1507011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.67/11.02 % (1507011)CaDiCaL version: 2.1.3 % 75.67/11.02 % (1507011)Termination reason: Instruction limit % 75.67/11.02 % (1507011)Termination phase: Saturation % 75.67/11.02 % (1507011)Time elapsed: 0.651 s % 75.67/11.02 % (1507011)Peak memory usage: 23 MB % 75.67/11.02 % (1507011)Instructions burned: 1474 (million) % 75.67/11.02 % (1507013)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3600064533:i=6324_2980 on theBenchmark for (2980ds/6324Mi) % 75.67/11.02 % (1507013)Cannot represent all propositional literals internally % 174.32/24.96 % (1507013)Refutation not found, incomplete strategy % 174.32/24.96 % (1507013)------------------------------ % 174.32/24.96 % (1507013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.32/24.96 % (1507013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.32/24.96 % (1507013)CaDiCaL version: 2.1.3 % 174.32/24.96 % (1507013)Termination reason: Refutation not found, incomplete strategy % 174.32/24.96 % (1507013)Time elapsed: 0.009 s % 174.32/24.96 % (1507013)Peak memory usage: 11 MB % 174.32/24.96 % (1507013)Instructions burned: 17 (million) % 174.32/24.96 % (1507013)------------------------------ % 174.32/24.96 % (1507013)------------------------------ % 174.32/24.96 % (1507015)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=315375187:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi) % 174.32/24.96 % TRYING [16] % 174.32/24.96 % (1507015)Instruction limit reached! % 174.32/24.96 % (1507015)------------------------------ % 174.32/24.96 % (1507015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.32/24.96 % (1507015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.32/24.96 % (1507015)CaDiCaL version: 2.1.3 % 174.32/24.96 % (1507015)Termination reason: Instruction limit % 174.32/24.96 % (1507015)Termination phase: Finite model building constraint generation % 174.32/24.96 % (1507015)Time elapsed: 0.763 s % 174.32/24.96 % (1507015)Peak memory usage: 142 MB % 174.32/24.96 % (1507015)Instructions burned: 2177 (million) % 174.32/24.96 % (1507017)ott-2_1_sil=16000:newcnf=on:random_seed=178651374:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2972 on theBenchmark for (2972ds/869Mi) % 174.32/24.96 % TRYING [8] % 174.32/24.96 % TRYING [7] % 174.32/24.96 % (1507017)Instruction limit reached! % 174.32/24.96 % (1507017)------------------------------ % 174.32/24.96 % (1507017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.32/24.96 % (1507017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.32/24.96 % (1507017)CaDiCaL version: 2.1.3 % 174.32/24.96 % (1507017)Termination reason: Instruction limit % 174.32/24.96 % (1507017)Termination phase: Saturation % 174.32/24.96 % (1507017)Time elapsed: 0.481 s % 174.32/24.96 % (1507017)Peak memory usage: 15 MB % 174.32/24.96 % (1507017)Instructions burned: 871 (million) % 174.32/24.96 % (1507019)ott+10_1_sil=32000:tgt=ground:random_seed=3102148714:i=5114:av=off_2967 on theBenchmark for (2967ds/5114Mi) % 174.32/24.96 % (1507009)Instruction limit reached! % 174.32/24.96 % (1507009)------------------------------ % 174.32/24.96 % (1507009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.32/24.96 % (1507009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.32/24.96 % (1507009)CaDiCaL version: 2.1.3 % 174.32/24.96 % (1507009)Termination reason: Instruction limit % 174.32/24.96 % (1507009)Termination phase: Saturation % 174.32/24.96 % (1507009)Time elapsed: 2.725 s % 174.32/24.96 % (1507009)Peak memory usage: 28 MB % 174.32/24.96 % (1507009)Instructions burned: 5132 (million) % 174.32/24.96 % (1507021)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=413683202:i=54282_2961 on theBenchmark for (2961ds/54282Mi) % 174.32/24.96 % TRYING [1] % 174.32/24.96 % TRYING [2] % 174.32/24.96 % TRYING [3] % 174.32/24.96 % TRYING [4] % 174.32/24.96 % TRYING [5] % 174.32/24.96 % (1507005)Instruction limit reached! % 174.32/24.96 % (1507005)------------------------------ % 174.32/24.96 % (1507005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.32/24.96 % (1507005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.32/24.96 % (1507005)CaDiCaL version: 2.1.3 % 174.32/24.96 % (1507005)Termination reason: Instruction limit % 174.32/24.96 % (1507005)Termination phase: Finite model building constraint generation % 174.32/24.96 % (1507005)Time elapsed: 3.360 s % 174.32/24.96 % (1507005)Peak memory usage: 587 MB % 174.32/24.96 % (1507005)Instructions burned: 9515 (million) % 174.32/24.96 % TRYING [6] % 174.32/24.96 % (1507023)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2713372114:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi) % 174.32/24.96 % TRYING [7] % 174.32/24.96 % (1507002)Instruction limit reached! % 174.32/24.96 % (1507002)------------------------------ % 174.32/24.96 % (1507002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.32/24.96 % (1507002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.32/24.96 % (1507002)CaDiCaL version: 2.1.3 % 174.32/24.96 % (1507002)Termination reason: Instruction limit % 174.32/24.96 % (1507002)Termination phase: Finite model building SAT solving % 174.32/24.96 % (1507002)Time elapsed: 5.014 s % 174.32/24.96 % (1507002)Peak memory usage: 276 MB % 174.32/24.96 % (1507002)Instructions burned: 22064 (million) % 252.98/36.03 % (1507025)dis+21_1_sil=32000:sas=cadical:random_seed=793010983:i=3773:amm=off_2943 on theBenchmark for (2943ds/3773Mi) % 252.98/36.03 % (1507019)Instruction limit reached! % 252.98/36.03 % (1507019)------------------------------ % 252.98/36.03 % (1507019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.98/36.03 % (1507019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.98/36.03 % (1507019)CaDiCaL version: 2.1.3 % 252.98/36.03 % (1507019)Termination reason: Instruction limit % 252.98/36.03 % (1507019)Termination phase: Saturation % 252.98/36.03 % (1507019)Time elapsed: 2.350 s % 252.98/36.03 % (1507019)Peak memory usage: 21 MB % 252.98/36.03 % (1507019)Instructions burned: 5115 (million) % 252.98/36.03 % (1507027)ott+11_1_sil=16000:gs=on:random_seed=92163521:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2943 on theBenchmark for (2943ds/2251Mi) % 252.98/36.03 % (1507023)Instruction limit reached! % 252.98/36.03 % (1507023)------------------------------ % 252.98/36.03 % (1507023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.98/36.03 % (1507023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.98/36.03 % (1507023)CaDiCaL version: 2.1.3 % 252.98/36.03 % (1507023)Termination reason: Instruction limit % 252.98/36.03 % (1507023)Termination phase: Saturation % 252.98/36.03 % (1507023)Time elapsed: 1.800 s % 252.98/36.03 % (1507023)Peak memory usage: 25 MB % 252.98/36.03 % (1507023)Instructions burned: 3513 (million) % 252.98/36.03 % (1507029)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=278142113:fmbsr=1.6:i=67534_2938 on theBenchmark for (2938ds/67534Mi) % 252.98/36.03 % TRYING [9] % 252.98/36.03 % TRYING [7] % 252.98/36.03 % TRYING [8] % 252.98/36.03 % (1507027)Instruction limit reached! % 252.98/36.03 % (1507027)------------------------------ % 252.98/36.03 % (1507027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.98/36.03 % (1507027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.98/36.03 % (1507027)CaDiCaL version: 2.1.3 % 252.98/36.03 % (1507027)Termination reason: Instruction limit % 252.98/36.03 % (1507027)Termination phase: Saturation % 252.98/36.03 % (1507027)Time elapsed: 0.999 s % 252.98/36.03 % (1507027)Peak memory usage: 15 MB % 252.98/36.03 % (1507027)Instructions burned: 2253 (million) % 252.98/36.03 % (1507025)Instruction limit reached! % 252.98/36.03 % (1507025)------------------------------ % 252.98/36.03 % (1507025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.98/36.03 % (1507025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.98/36.03 % (1507025)CaDiCaL version: 2.1.3 % 252.98/36.03 % (1507025)Termination reason: Instruction limit % 252.98/36.03 % (1507025)Termination phase: Saturation % 252.98/36.03 % (1507025)Time elapsed: 1.033 s % 252.98/36.03 % (1507025)Peak memory usage: 26 MB % 252.98/36.03 % (1507025)Instructions burned: 3774 (million) % 252.98/36.03 % (1507032)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3873368810:i=29340_2933 on theBenchmark for (2933ds/29340Mi) % 252.98/36.03 % (1507031)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2856384629:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2933 on theBenchmark for (2933ds/4591Mi) % 252.98/36.03 % (1507031)Instruction limit reached! % 252.98/36.03 % (1507031)------------------------------ % 252.98/36.03 % (1507031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.98/36.03 % (1507031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.98/36.03 % (1507031)CaDiCaL version: 2.1.3 % 252.98/36.03 % (1507031)Termination reason: Instruction limit % 252.98/36.03 % (1507031)Termination phase: Saturation % 252.98/36.03 % (1507031)Time elapsed: 1.488 s % 252.98/36.03 % (1507031)Peak memory usage: 14 MB % 252.98/36.03 % (1507031)Instructions burned: 4594 (million) % 252.98/36.03 % (1507035)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=431197336:i=5211_2918 on theBenchmark for (2918ds/5211Mi) % 252.98/36.03 % TRYING [9] % 252.98/36.03 % (1507035)Instruction limit reached! % 252.98/36.03 % (1507035)------------------------------ % 252.98/36.03 % (1507035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.98/36.03 % (1507035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.98/36.03 % (1507035)CaDiCaL version: 2.1.3 % 252.98/36.03 % (1507035)Termination reason: Instruction limit % 252.98/36.03 % (1507035)Termination phase: Saturation % 252.98/36.03 % (1507035)Time elapsed: 2.594 s % 252.98/36.03 % (1507035)Peak memory usage: 43 MB % 252.98/36.03 % (1507035)Instructions burnTerminated % 300.49/42.64 % Vampire exiting %------------------------------------------------------------------------------