%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW353+1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n013.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:39:52 PM UTC 2026 % Result : Timeout 300.22s 43.07s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW353+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.26 % Computer : n013.cluster.edu % 0.09/0.26 % Model : x86_64 x86_64 % 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.26 % Memory : 8046.5625MB % 0.09/0.26 % OS : Linux 6.8.0-71-generic % 0.09/0.26 % CPULimit : 300 % 0.09/0.26 % WCLimit : 300 % 0.09/0.26 % DateTime : Mon Sep 28 13:39:51 UTC 2026 % 0.09/0.26 % CPUTime : % 0.09/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.27/0.32 Running first-order model finding % 0.27/0.32 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 % 43.49/7.01 % (1183697)Will run a generic schedule for satisfiability detection. % 43.49/7.01 % (1183704)% WARNING: option uhcvi not known. % 43.49/7.01 % (1183704)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2558866092:i=135531:add=off:rawr=on_2994 on theBenchmark for (2994ds/135531Mi) % 43.49/7.01 % (1183708)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2379659561:i=131_2994 on theBenchmark for (2994ds/131Mi) % 43.49/7.01 % (1183703)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1169315641_2994 on theBenchmark for (2994ds/0Mi) % 43.49/7.01 % (1183706)dis+10_1_sil=32000:sp=arity:random_seed=1516998319:i=103:fgj=on_2994 on theBenchmark for (2994ds/103Mi) % 43.49/7.01 % (1183709)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=863244978:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2994 on theBenchmark for (2994ds/159Mi) % 43.49/7.01 % (1183707)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2660870935:i=116_2994 on theBenchmark for (2994ds/116Mi) % 43.49/7.01 % (1183705)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=521432902:i=88024:add=on:rawr=on_2994 on theBenchmark for (2994ds/88024Mi) % 43.49/7.01 % (1183706)Instruction limit reached! % 43.49/7.01 % (1183706)------------------------------ % 43.49/7.01 % (1183706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.49/7.01 % (1183706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.49/7.01 % (1183706)CaDiCaL version: 2.1.3 % 43.49/7.01 % (1183706)Termination reason: Instruction limit % 43.49/7.01 % (1183706)Termination phase: Preprocessing 3 % 43.49/7.01 % (1183706)Time elapsed: 0.103 s % 43.49/7.01 % (1183706)Peak memory usage: 19 MB % 43.49/7.01 % (1183706)Instructions burned: 103 (million) % 43.49/7.01 % (1183708)Instruction limit reached! % 43.49/7.01 % (1183708)------------------------------ % 43.49/7.01 % (1183708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.49/7.01 % (1183708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.49/7.01 % (1183708)CaDiCaL version: 2.1.3 % 43.49/7.01 % (1183708)Termination reason: Instruction limit % 43.49/7.01 % (1183708)Termination phase: Preprocessing 3 % 43.49/7.01 % (1183708)Time elapsed: 0.128 s % 43.49/7.01 % (1183708)Peak memory usage: 20 MB % 43.49/7.01 % (1183707)Instruction limit reached! % 43.49/7.01 % (1183707)------------------------------ % 43.49/7.01 % (1183707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.49/7.01 % (1183707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.49/7.01 % (1183707)CaDiCaL version: 2.1.3 % 43.49/7.01 % (1183708)Instructions burned: 131 (million) % 43.49/7.01 % (1183707)Termination reason: Instruction limit % 43.49/7.01 % (1183707)Termination phase: NewCNF % 43.49/7.01 % (1183707)Time elapsed: 0.119 s % 43.49/7.01 % (1183707)Peak memory usage: 21 MB % 43.49/7.01 % (1183707)Instructions burned: 118 (million) % 43.49/7.01 % (1183718)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1547864933:i=714:nm=2_2992 on theBenchmark for (2992ds/714Mi) % 43.49/7.01 % (1183720)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=2945301487:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2992 on theBenchmark for (2992ds/684Mi) % 43.49/7.01 % (1183709)Instruction limit reached! % 43.49/7.01 % (1183709)------------------------------ % 43.49/7.01 % (1183709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.49/7.01 % (1183709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.49/7.01 % (1183709)CaDiCaL version: 2.1.3 % 43.49/7.01 % (1183709)Termination reason: Instruction limit % 43.49/7.01 % (1183709)Termination phase: Clausification % 43.49/7.01 % (1183709)Time elapsed: 0.150 s % 43.49/7.01 % (1183709)Peak memory usage: 21 MB % 43.49/7.01 % (1183709)Instructions burned: 159 (million) % 43.49/7.01 % (1183719)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3503081394:i=131:bd=preordered:fsd=on_2992 on theBenchmark for (2992ds/131Mi) % 43.49/7.01 % (1183724)ott-21_1_sil=16000:fs=off:random_seed=2311958495:i=180:av=off:fsr=off_2992 on theBenchmark for (2992ds/180Mi) % 43.49/7.01 % (1183719)Instruction limit reached! % 43.49/7.01 % (1183719)------------------------------ % 43.49/7.01 % (1183719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.49/7.01 % (1183719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.25/14.60 % (1183719)CaDiCaL version: 2.1.3 % 97.25/14.60 % (1183719)Termination reason: Instruction limit % 97.25/14.60 % (1183719)Termination phase: Preprocessing 3 % 97.25/14.60 % (1183719)Time elapsed: 0.127 s % 97.25/14.60 % (1183719)Peak memory usage: 20 MB % 97.25/14.60 % (1183719)Instructions burned: 131 (million) % 97.25/14.60 % (1183726)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3354772827:i=477:bd=all_2991 on theBenchmark for (2991ds/477Mi) % 97.25/14.60 % (1183724)Instruction limit reached! % 97.25/14.60 % (1183724)------------------------------ % 97.25/14.60 % (1183724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.25/14.60 % (1183724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.25/14.60 % (1183724)CaDiCaL version: 2.1.3 % 97.25/14.60 % (1183724)Termination reason: Instruction limit % 97.25/14.60 % (1183724)Termination phase: Property scanning % 97.25/14.60 % (1183724)Time elapsed: 0.171 s % 97.25/14.60 % (1183724)Peak memory usage: 21 MB % 97.25/14.60 % (1183724)Instructions burned: 180 (million) % 97.25/14.60 % (1183728)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=388224516:fmbsr=1.3:i=865:ins=25_2990 on theBenchmark for (2990ds/865Mi) % 97.25/14.60 % (1183720)Instruction limit reached! % 97.25/14.60 % (1183720)------------------------------ % 97.25/14.60 % (1183720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.25/14.60 % (1183720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.25/14.60 % (1183720)CaDiCaL version: 2.1.3 % 97.25/14.60 % (1183720)Termination reason: Instruction limit % 97.25/14.60 % (1183720)Termination phase: Saturation % 97.25/14.60 % (1183720)Time elapsed: 0.560 s % 97.25/14.60 % (1183720)Peak memory usage: 24 MB % 97.25/14.60 % (1183720)Instructions burned: 685 (million) % 97.25/14.60 % (1183730)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3925784565:i=1179_2986 on theBenchmark for (2986ds/1179Mi) % 97.25/14.60 % (1183726)Instruction limit reached! % 97.25/14.60 % (1183726)------------------------------ % 97.25/14.60 % (1183726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.25/14.60 % (1183726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.25/14.60 % (1183726)CaDiCaL version: 2.1.3 % 97.25/14.60 % (1183726)Termination reason: Instruction limit % 97.25/14.60 % (1183726)Termination phase: Property scanning % 97.25/14.60 % (1183726)Time elapsed: 0.421 s % 97.25/14.60 % (1183726)Peak memory usage: 22 MB % 97.25/14.60 % (1183726)Instructions burned: 477 (million) % 97.25/14.60 % (1183718)Instruction limit reached! % 97.25/14.60 % (1183718)------------------------------ % 97.25/14.60 % (1183718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.25/14.60 % (1183718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.25/14.60 % (1183718)CaDiCaL version: 2.1.3 % 97.25/14.60 % (1183718)Termination reason: Instruction limit % 97.25/14.60 % (1183718)Termination phase: Finite model building preprocessing % 97.25/14.60 % (1183718)Time elapsed: 0.612 s % 97.25/14.60 % (1183718)Peak memory usage: 25 MB % 97.25/14.60 % (1183718)Instructions burned: 715 (million) % 97.25/14.60 % (1183732)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4078247799:i=889:ins=1_2986 on theBenchmark for (2986ds/889Mi) % 97.25/14.60 % (1183734)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=232442351:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2986 on theBenchmark for (2986ds/692Mi) % 97.25/14.60 % (1183728)Instruction limit reached! % 97.25/14.60 % (1183728)------------------------------ % 97.25/14.60 % (1183728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.25/14.60 % (1183728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.25/14.60 % (1183728)CaDiCaL version: 2.1.3 % 97.25/14.60 % (1183728)Termination reason: Instruction limit % 97.25/14.60 % (1183728)Termination phase: Finite model building preprocessing % 97.25/14.60 % (1183728)Time elapsed: 0.731 s % 97.25/14.60 % (1183728)Peak memory usage: 30 MB % 97.25/14.60 % (1183728)Instructions burned: 866 (million) % 97.25/14.60 % (1183738)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3567129785:i=879:kws=inv_precedence:fsr=off_2982 on theBenchmark for (2982ds/879Mi) % 97.25/14.60 % (1183734)Instruction limit reached! % 97.25/14.60 % (1183734)------------------------------ % 97.25/14.60 % (1183734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.25/14.60 % (1183734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.01/30.10 % (1183734)CaDiCaL version: 2.1.3 % 208.01/30.10 % (1183734)Termination reason: Instruction limit % 208.01/30.10 % (1183734)Termination phase: Saturation % 208.01/30.10 % (1183734)Time elapsed: 0.628 s % 208.01/30.10 % (1183734)Peak memory usage: 27 MB % 208.01/30.10 % (1183734)Instructions burned: 693 (million) % 208.01/30.10 % (1183740)fmb+10_1_sil=64000:random_seed=32959976:i=22061:nm=2:gsp=on_2979 on theBenchmark for (2979ds/22061Mi) % 208.01/30.10 % (1183732)Instruction limit reached! % 208.01/30.10 % (1183732)------------------------------ % 208.01/30.10 % (1183732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.01/30.10 % (1183732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.01/30.10 % (1183732)CaDiCaL version: 2.1.3 % 208.01/30.10 % (1183732)Termination reason: Instruction limit % 208.01/30.10 % (1183732)Termination phase: Finite model building preprocessing % 208.01/30.10 % (1183732)Time elapsed: 0.773 s % 208.01/30.10 % (1183732)Peak memory usage: 31 MB % 208.01/30.10 % (1183732)Instructions burned: 889 (million) % 208.01/30.10 % (1183742)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3315659885:i=9515:nm=5_2978 on theBenchmark for (2978ds/9515Mi) % 208.01/30.10 % (1183730)Instruction limit reached! % 208.01/30.10 % (1183730)------------------------------ % 208.01/30.10 % (1183730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.01/30.10 % (1183730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.01/30.10 % (1183730)CaDiCaL version: 2.1.3 % 208.01/30.10 % (1183730)Termination reason: Instruction limit % 208.01/30.10 % (1183730)Termination phase: Saturation % 208.01/30.10 % (1183730)Time elapsed: 1.104 s % 208.01/30.10 % (1183730)Peak memory usage: 30 MB % 208.01/30.10 % (1183730)Instructions burned: 1180 (million) % 208.01/30.10 % (1183738)Instruction limit reached! % 208.01/30.10 % (1183738)------------------------------ % 208.01/30.10 % (1183738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.01/30.10 % (1183738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.01/30.10 % (1183738)CaDiCaL version: 2.1.3 % 208.01/30.10 % (1183738)Termination reason: Instruction limit % 208.01/30.10 % (1183738)Termination phase: Saturation % 208.01/30.10 % (1183738)Time elapsed: 0.726 s % 208.01/30.10 % (1183738)Peak memory usage: 30 MB % 208.01/30.10 % (1183738)Instructions burned: 879 (million) % 208.01/30.10 % (1183744)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2697557538:fmbsr=1.7:i=920_2975 on theBenchmark for (2975ds/920Mi) % 208.01/30.10 % (1183746)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3706525174:i=5131_2975 on theBenchmark for (2975ds/5131Mi) % 208.01/30.10 % (1183744)Instruction limit reached! % 208.01/30.10 % (1183744)------------------------------ % 208.01/30.10 % (1183744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.01/30.10 % (1183744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.01/30.10 % (1183744)CaDiCaL version: 2.1.3 % 208.01/30.10 % (1183744)Termination reason: Instruction limit % 208.01/30.10 % (1183744)Termination phase: Finite model building preprocessing % 208.01/30.10 % (1183744)Time elapsed: 0.806 s % 208.01/30.10 % (1183744)Peak memory usage: 32 MB % 208.01/30.10 % (1183744)Instructions burned: 921 (million) % 208.01/30.10 % (1183748)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=478507910:i=1472:ins=7:fdi=8:gsp=on_2967 on theBenchmark for (2967ds/1472Mi) % 208.01/30.10 % (1183748)Instruction limit reached! % 208.01/30.10 % (1183748)------------------------------ % 208.01/30.10 % (1183748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.01/30.10 % (1183748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.01/30.10 % (1183748)CaDiCaL version: 2.1.3 % 208.01/30.10 % (1183748)Termination reason: Instruction limit % 208.01/30.10 % (1183748)Termination phase: Saturation % 208.01/30.10 % (1183748)Time elapsed: 1.207 s % 208.01/30.10 % (1183748)Peak memory usage: 28 MB % 208.01/30.10 % (1183748)Instructions burned: 1473 (million) % 208.01/30.10 % (1183750)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4026975149:i=6324_2954 on theBenchmark for (2954ds/6324Mi) % 208.01/30.10 % (1183746)Instruction limit reached! % 208.01/30.10 % (1183746)------------------------------ % 208.01/30.10 % (1183746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.01/30.10 % (1183746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.01/30.10 % (1183746)CaDiCaL version: 2.1.3 % 208.01/30.10 % (1183746)Termination reason: Instruction limit % 300.22/43.07 % (1183746)Termination phase: Saturation % 300.22/43.07 % (1183746)Time elapsed: 4.177 s % 300.22/43.07 % (1183746)Peak memory usage: 50 MB % 300.22/43.07 % (1183746)Instructions burned: 5131 (million) % 300.22/43.07 % (1183752)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2776917526:fmbsr=2.30978:i=2174_2933 on theBenchmark for (2933ds/2174Mi) % 300.22/43.07 % (1183752)Instruction limit reached! % 300.22/43.07 % (1183752)------------------------------ % 300.22/43.07 % (1183752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183752)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183752)Termination reason: Instruction limit % 300.22/43.07 % (1183752)Termination phase: Finite model building preprocessing % 300.22/43.07 % (1183752)Time elapsed: 1.742 s % 300.22/43.07 % (1183752)Peak memory usage: 48 MB % 300.22/43.07 % (1183752)Instructions burned: 2174 (million) % 300.22/43.07 % (1183754)ott-2_1_sil=16000:newcnf=on:random_seed=2171564148:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2915 on theBenchmark for (2915ds/869Mi) % 300.22/43.07 % (1183754)Instruction limit reached! % 300.22/43.07 % (1183754)------------------------------ % 300.22/43.07 % (1183754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183754)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183754)Termination reason: Instruction limit % 300.22/43.07 % (1183754)Termination phase: Saturation % 300.22/43.07 % (1183754)Time elapsed: 0.757 s % 300.22/43.07 % (1183754)Peak memory usage: 28 MB % 300.22/43.07 % (1183754)Instructions burned: 869 (million) % 300.22/43.07 % (1183756)ott+10_1_sil=32000:tgt=ground:random_seed=661986493:i=5114:av=off_2907 on theBenchmark for (2907ds/5114Mi) % 300.22/43.07 % (1183750)Instruction limit reached! % 300.22/43.07 % (1183750)------------------------------ % 300.22/43.07 % (1183750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183750)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183750)Termination reason: Instruction limit % 300.22/43.07 % (1183750)Termination phase: Finite model building preprocessing % 300.22/43.07 % (1183750)Time elapsed: 5.774 s % 300.22/43.07 % (1183750)Peak memory usage: 65 MB % 300.22/43.07 % (1183750)Instructions burned: 6325 (million) % 300.22/43.07 % (1183758)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2717524692:i=54282_2896 on theBenchmark for (2896ds/54282Mi) % 300.22/43.07 % (1183742)Instruction limit reached! % 300.22/43.07 % (1183742)------------------------------ % 300.22/43.07 % (1183742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183742)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183742)Termination reason: Instruction limit % 300.22/43.07 % (1183742)Termination phase: Finite model building preprocessing % 300.22/43.07 % (1183742)Time elapsed: 8.564 s % 300.22/43.07 % (1183742)Peak memory usage: 78 MB % 300.22/43.07 % (1183742)Instructions burned: 9515 (million) % 300.22/43.07 % (1183760)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1659597577:i=3512:aac=none_2892 on theBenchmark for (2892ds/3512Mi) % 300.22/43.07 % (1183760)Instruction limit reached! % 300.22/43.07 % (1183760)------------------------------ % 300.22/43.07 % (1183760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183760)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183760)Termination reason: Instruction limit % 300.22/43.07 % (1183760)Termination phase: Saturation % 300.22/43.07 % (1183760)Time elapsed: 3.056 s % 300.22/43.07 % (1183760)Peak memory usage: 44 MB % 300.22/43.07 % (1183760)Instructions burned: 3512 (million) % 300.22/43.07 % (1183764)dis+21_1_sil=32000:sas=cadical:random_seed=1704117511:i=3773:amm=off_2861 on theBenchmark for (2861ds/3773Mi) % 300.22/43.07 % (1183756)Instruction limit reached! % 300.22/43.07 % (1183756)------------------------------ % 300.22/43.07 % (1183756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183756)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183756)Termination reason: Instruction limit % 300.22/43.07 % (1183756)Termination phase: Saturation % 300.22/43.07 % (1183756)Time elapsed: 4.960 s % 300.22/43.07 % (1183756)Peak memory usage: 68 MB % 300.22/43.07 % (1183756)Instructions burned: 5114 (million) % 300.22/43.07 % (1183768)ott+11_1_sil=16000:gs=on:random_seed=3289534881:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2857 on theBenchmark for (2857ds/2251Mi) % 300.22/43.07 % (1183768)Instruction limit reached! % 300.22/43.07 % (1183768)------------------------------ % 300.22/43.07 % (1183768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183768)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183768)Termination reason: Instruction limit % 300.22/43.07 % (1183768)Termination phase: Saturation % 300.22/43.07 % (1183768)Time elapsed: 1.953 s % 300.22/43.07 % (1183768)Peak memory usage: 34 MB % 300.22/43.07 % (1183768)Instructions burned: 2251 (million) % 300.22/43.07 % (1183772)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4057020519:fmbsr=1.6:i=67534_2837 on theBenchmark for (2837ds/67534Mi) % 300.22/43.07 % (1183764)Instruction limit reached! % 300.22/43.07 % (1183764)------------------------------ % 300.22/43.07 % (1183764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183764)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183764)Termination reason: Instruction limit % 300.22/43.07 % (1183764)Termination phase: Saturation % 300.22/43.07 % (1183764)Time elapsed: 3.748 s % 300.22/43.07 % (1183764)Peak memory usage: 53 MB % 300.22/43.07 % (1183764)Instructions burned: 3773 (million) % 300.22/43.07 % (1183774)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=70205854:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2823 on theBenchmark for (2823ds/4591Mi) % 300.22/43.07 % (1183774)Instruction limit reached! % 300.22/43.07 % (1183774)------------------------------ % 300.22/43.07 % (1183774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183774)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183774)Termination reason: Instruction limit % 300.22/43.07 % (1183774)Termination phase: Saturation % 300.22/43.07 % (1183774)Time elapsed: 3.489 s % 300.22/43.07 % (1183774)Peak memory usage: 32 MB % 300.22/43.07 % (1183774)Instructions burned: 4592 (million) % 300.22/43.07 % (1183776)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2539435302:i=29340_2788 on theBenchmark for (2788ds/29340Mi) % 300.22/43.07 % (1183740)Instruction limit reached! % 300.22/43.07 % (1183740)------------------------------ % 300.22/43.07 % (1183740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183740)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183740)Termination reason: Instruction limit % 300.22/43.07 % (1183740)Termination phase: Finite model building preprocessing % 300.22/43.07 % (1183740)Time elapsed: 20.077 s % 300.22/43.07 % (1183740)Peak memory usage: 158 MB % 300.22/43.07 % (1183740)Instructions burned: 22061 (million) % 300.22/43.07 % (1183778)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1079786691:i=5211_2778 on theBenchmark for (2778ds/5211Mi) % 300.22/43.07 % TRYING [1] % 300.22/43.07 % TRYING [2] % 300.22/43.07 % (1183778)Instruction limit reached! % 300.22/43.07 % (1183778)------------------------------ % 300.22/43.07 % (1183778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183778)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183778)Termination reason: Instruction limit % 300.22/43.07 % (1183778)Termination phase: Saturation % 300.22/43.07 % (1183778)Time elapsed: 3.771 s % 300.22/43.07 % (1183778)Peak memory usage: 45 MB % 300.22/43.07 % (1183778)Instructions burned: 5213 (million) % 300.22/43.07 % (1183786)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=148228043:i=5497:nm=2_2740 on theBenchmark for (2740ds/5497Mi) % 300.22/43.07 % (1183786)Instruction limit reached! % 300.22/43.07 % (1183786)------------------------------ % 300.22/43.07 % (1183786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.22/43.07 % (1183786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.07 % (1183786)CaDiCaL version: 2.1.3 % 300.22/43.07 % (1183786)Termination reason: Instruction limit % 300.22/43.07 % (1183786)Termination phase: Finite model building preprocessing % 300.22/43.07 % (1183786)Time % 300.22/43.08 Terminated % 300.22/43.08 % Vampire exiting % 300.22/43.08 Terminated %------------------------------------------------------------------------------