%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NLP263+1 : TPTP v9.3.1. Bugfixed v4.0.1. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n020.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 12:08:16 PM UTC 2026 % Result : Satisfiable 0.17s 27.93s % Output : Saturation 0.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NLP263+1 : TPTP v9.3.1. Bugfixed v4.0.1. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.41 % Computer : n020.cluster.edu % 0.11/0.41 % Model : x86_64 x86_64 % 0.11/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.41 % Memory : 8046.5625MB % 0.11/0.41 % OS : Linux 6.8.0-71-generic % 0.11/0.41 % CPULimit : 300 % 0.11/0.41 % WCLimit : 300 % 0.11/0.41 % DateTime : Sun Sep 27 18:38:50 UTC 2026 % 0.11/0.41 % CPUTime : % 0.11/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.45 Running first-order theorem proving % 0.11/0.45 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 33.04/17.48 % (3673603)Detected formulas, will run a generic FOF schedule. % 33.04/17.48 % (3673608)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3495993418:i=141193_2861 on theBenchmark for (2861ds/141193Mi) % 33.04/17.48 % (3673609)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1549547822:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2861 on theBenchmark for (2861ds/134677Mi) % 33.04/17.48 % (3673610)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3645835914:i=141695:sd=1:nm=32:gsp=on:ss=included_2861 on theBenchmark for (2861ds/141695Mi) % 33.04/17.48 % (3673611)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=287238306:i=109:sd=1:ins=1:gsp=on:ss=axioms_2861 on theBenchmark for (2861ds/109Mi) % 33.04/17.48 % (3673612)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3292326577:i=119:av=off:ss=axioms_2861 on theBenchmark for (2861ds/119Mi) % 33.04/17.48 % (3673613)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2768213350:s2a=on:i=139:gtg=position_2861 on theBenchmark for (2861ds/139Mi) % 33.04/17.48 % (3673615)dis-21_1_sil=8000:lcm=predicate:random_seed=2754974673:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2861 on theBenchmark for (2861ds/129Mi) % 33.04/17.48 % (3673611)Instruction limit reached! % 33.04/17.48 % (3673611)------------------------------ % 33.04/17.48 % (3673611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.04/17.48 % (3673611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.04/17.48 % (3673611)CaDiCaL version: 2.1.3 % 33.04/17.48 % (3673611)Termination reason: Instruction limit % 33.04/17.48 % (3673611)Termination phase: SInE selection % 33.04/17.48 % (3673611)Time elapsed: 0.083 s % 33.04/17.48 % (3673611)Peak memory usage: 546 MB % 33.04/17.48 % (3673611)Instructions burned: 110 (million) % 33.04/17.48 % (3673612)Instruction limit reached! % 33.04/17.48 % (3673612)------------------------------ % 33.04/17.48 % (3673612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.04/17.48 % (3673612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.04/17.48 % (3673612)CaDiCaL version: 2.1.3 % 33.04/17.48 % (3673612)Termination reason: Instruction limit % 33.04/17.48 % (3673612)Termination phase: SInE selection % 33.04/17.48 % (3673612)Time elapsed: 0.089 s % 33.04/17.48 % (3673612)Peak memory usage: 546 MB % 33.04/17.48 % (3673612)Instructions burned: 119 (million) % 33.04/17.48 % (3673615)Instruction limit reached! % 33.04/17.48 % (3673615)------------------------------ % 33.04/17.48 % (3673615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.04/17.48 % (3673615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.04/17.48 % (3673615)CaDiCaL version: 2.1.3 % 33.04/17.48 % (3673615)Termination reason: Instruction limit % 33.04/17.48 % (3673615)Termination phase: SInE selection % 33.04/17.48 % (3673615)Time elapsed: 0.099 s % 33.04/17.48 % (3673615)Peak memory usage: 546 MB % 33.04/17.48 % (3673615)Instructions burned: 130 (million) % 33.04/17.48 % (3673613)Instruction limit reached! % 33.04/17.48 % (3673613)------------------------------ % 33.04/17.48 % (3673613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.04/17.48 % (3673613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.04/17.48 % (3673613)CaDiCaL version: 2.1.3 % 33.04/17.48 % (3673613)Termination reason: Instruction limit % 33.04/17.48 % (3673613)Termination phase: Property scanning % 33.04/17.48 % (3673613)Time elapsed: 0.204 s % 33.04/17.48 % (3673613)Peak memory usage: 545 MB % 33.04/17.48 % (3673613)Instructions burned: 140 (million) % 33.04/17.48 % (3673622)lrs+10_1_sil=8000:sp=occurrence:random_seed=2838765683:i=285:sd=3:ss=axioms:sgt=8_2858 on theBenchmark for (2858ds/285Mi) % 33.04/17.48 % (3673623)lrs+10_1_sil=32000:urr=on:br=off:random_seed=946454664:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2858 on theBenchmark for (2858ds/157Mi) % 33.04/17.48 % (3673624)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4149823632:i=325:sd=1:ss=axioms:sgt=32_2857 on theBenchmark for (2857ds/325Mi) % 33.04/17.48 % (3673627)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=299015975:s2a=on:i=248:s2at=1.23:gtg=position_2856 on theBenchmark for (2856ds/248Mi) % 33.04/17.48 % (3673622)Instruction limit reached! % 37.31/18.10 % (3673622)------------------------------ % 37.31/18.10 % (3673622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.31/18.10 % (3673622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/18.10 % (3673622)CaDiCaL version: 2.1.3 % 37.31/18.10 % (3673622)Termination reason: Instruction limit % 37.31/18.10 % (3673622)Termination phase: SInE selection % 37.31/18.10 % (3673622)Time elapsed: 0.224 s % 37.31/18.10 % (3673622)Peak memory usage: 546 MB % 37.31/18.10 % (3673622)Instructions burned: 285 (million) % 37.31/18.10 % (3673623)Instruction limit reached! % 37.31/18.10 % (3673623)------------------------------ % 37.31/18.10 % (3673623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.31/18.10 % (3673623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/18.10 % (3673623)CaDiCaL version: 2.1.3 % 37.31/18.10 % (3673623)Termination reason: Instruction limit % 37.31/18.10 % (3673623)Termination phase: Property scanning % 37.31/18.10 % (3673623)Time elapsed: 0.207 s % 37.31/18.10 % (3673623)Peak memory usage: 545 MB % 37.31/18.10 % (3673623)Instructions burned: 159 (million) % 37.31/18.10 % (3673624)Instruction limit reached! % 37.31/18.10 % (3673624)------------------------------ % 37.31/18.10 % (3673624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.31/18.10 % (3673624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/18.10 % (3673624)CaDiCaL version: 2.1.3 % 37.31/18.10 % (3673624)Termination reason: Instruction limit % 37.31/18.10 % (3673624)Termination phase: SInE selection % 37.31/18.10 % (3673624)Time elapsed: 0.261 s % 37.31/18.10 % (3673624)Peak memory usage: 546 MB % 37.31/18.10 % (3673624)Instructions burned: 326 (million) % 37.31/18.10 % (3673630)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2628180666:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2854 on theBenchmark for (2854ds/294Mi) % 37.31/18.10 % (3673627)Instruction limit reached! % 37.31/18.10 % (3673627)------------------------------ % 37.31/18.10 % (3673627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.31/18.10 % (3673627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/18.10 % (3673627)CaDiCaL version: 2.1.3 % 37.31/18.10 % (3673627)Termination reason: Instruction limit % 37.31/18.10 % (3673627)Termination phase: Property scanning % 37.31/18.10 % (3673627)Time elapsed: 0.246 s % 37.31/18.10 % (3673627)Peak memory usage: 545 MB % 37.31/18.10 % (3673627)Instructions burned: 250 (million) % 37.31/18.10 % (3673631)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2854598426:i=2350_2854 on theBenchmark for (2854ds/2350Mi) % 37.31/18.10 % (3673632)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=197604505:cts=off:i=113:fsr=off:ss=included:sgt=4_2853 on theBenchmark for (2853ds/113Mi) % 37.31/18.10 % (3673635)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1545716168:i=127:av=off:fsr=off:sup=off_2852 on theBenchmark for (2852ds/127Mi) % 37.31/18.10 % (3673632)Instruction limit reached! % 37.31/18.10 % (3673632)------------------------------ % 37.31/18.10 % (3673632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.31/18.10 % (3673632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/18.10 % (3673632)CaDiCaL version: 2.1.3 % 37.31/18.10 % (3673632)Termination reason: Instruction limit % 37.31/18.10 % (3673632)Termination phase: SInE selection % 37.31/18.10 % (3673632)Time elapsed: 0.086 s % 37.31/18.10 % (3673632)Peak memory usage: 546 MB % 37.31/18.10 % (3673632)Instructions burned: 114 (million) % 37.31/18.10 % (3673630)Instruction limit reached! % 37.31/18.10 % (3673630)------------------------------ % 37.31/18.10 % (3673630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.31/18.10 % (3673630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/18.10 % (3673630)CaDiCaL version: 2.1.3 % 37.31/18.10 % (3673630)Termination reason: Instruction limit % 37.31/18.10 % (3673630)Termination phase: SInE selection % 37.31/18.10 % (3673630)Time elapsed: 0.233 s % 37.31/18.10 % (3673630)Peak memory usage: 546 MB % 37.31/18.10 % (3673630)Instructions burned: 294 (million) % 37.31/18.10 % (3673635)Instruction limit reached! % 37.31/18.10 % (3673635)------------------------------ % 37.31/18.10 % (3673635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.31/18.10 % (3673635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/18.10 % (3673635)CaDiCaL version: 2.1.3 % 42.71/18.90 % (3673635)Termination reason: Instruction limit % 42.71/18.90 % (3673635)Termination phase: Preprocessing 1 % 42.71/18.90 % (3673635)Time elapsed: 0.095 s % 42.71/18.90 % (3673635)Peak memory usage: 544 MB % 42.71/18.90 % (3673635)Instructions burned: 127 (million) % 42.71/18.90 % (3673638)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4134802968:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2850 on theBenchmark for (2850ds/114Mi) % 42.71/18.90 % (3673639)lrs+10_1_sil=8000:sp=occurrence:random_seed=1746255185:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2850 on theBenchmark for (2850ds/907Mi) % 42.71/18.90 % (3673640)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3181163131:i=437:sd=1:aac=none:ss=included_2849 on theBenchmark for (2849ds/437Mi) % 42.71/18.90 % (3673638)Instruction limit reached! % 42.71/18.90 % (3673638)------------------------------ % 42.71/18.90 % (3673638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.71/18.90 % (3673638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.71/18.90 % (3673638)CaDiCaL version: 2.1.3 % 42.71/18.90 % (3673638)Termination reason: Instruction limit % 42.71/18.90 % (3673638)Termination phase: Property scanning % 42.71/18.90 % (3673638)Time elapsed: 0.189 s % 42.71/18.90 % (3673638)Peak memory usage: 545 MB % 42.71/18.90 % (3673638)Instructions burned: 116 (million) % 42.71/18.90 % (3673644)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=225036772:i=5202:ss=axioms:sgt=16_2846 on theBenchmark for (2846ds/5202Mi) % 42.71/18.90 % (3673640)Instruction limit reached! % 42.71/18.90 % (3673640)------------------------------ % 42.71/18.90 % (3673640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.71/18.90 % (3673640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.71/18.90 % (3673640)CaDiCaL version: 2.1.3 % 42.71/18.90 % (3673640)Termination reason: Instruction limit % 42.71/18.90 % (3673640)Termination phase: SInE selection % 42.71/18.90 % (3673640)Time elapsed: 0.330 s % 42.71/18.90 % (3673640)Peak memory usage: 546 MB % 42.71/18.90 % (3673640)Instructions burned: 438 (million) % 42.71/18.90 % (3673646)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1934016854:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2844 on theBenchmark for (2844ds/134Mi) % 42.71/18.90 % (3673646)Instruction limit reached! % 42.71/18.90 % (3673646)------------------------------ % 42.71/18.90 % (3673646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.71/18.90 % (3673646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.71/18.90 % (3673646)CaDiCaL version: 2.1.3 % 42.71/18.90 % (3673646)Termination reason: Instruction limit % 42.71/18.90 % (3673646)Termination phase: SInE selection % 42.71/18.90 % (3673646)Time elapsed: 0.101 s % 42.71/18.90 % (3673646)Peak memory usage: 546 MB % 42.71/18.90 % (3673646)Instructions burned: 135 (million) % 42.71/18.90 % (3673639)Instruction limit reached! % 42.71/18.90 % (3673639)------------------------------ % 42.71/18.90 % (3673639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.71/18.90 % (3673639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.71/18.90 % (3673639)CaDiCaL version: 2.1.3 % 42.71/18.90 % (3673639)Termination reason: Instruction limit % 42.71/18.90 % (3673639)Termination phase: SInE selection % 42.71/18.90 % (3673639)Time elapsed: 0.721 s % 42.71/18.90 % (3673639)Peak memory usage: 559 MB % 42.71/18.90 % (3673639)Instructions burned: 907 (million) % 42.71/18.90 % (3673648)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1229878962:st=8:i=592:sd=3:ep=RST:ss=axioms_2841 on theBenchmark for (2841ds/592Mi) % 42.71/18.90 % (3673649)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3913091138:st=3:i=13193:sd=3:ss=axioms_2841 on theBenchmark for (2841ds/13193Mi) % 42.71/18.90 % (3673648)Instruction limit reached! % 42.71/18.90 % (3673648)------------------------------ % 42.71/18.90 % (3673648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.71/18.90 % (3673648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.71/18.90 % (3673648)CaDiCaL version: 2.1.3 % 42.71/18.90 % (3673648)Termination reason: Instruction limit % 42.71/18.90 % (3673648)Termination phase: SInE selection % 42.71/18.90 % (3673648)Time elapsed: 0.492 s % 42.71/18.90 % (3673648)Peak memory usage: 546 MB % 42.71/18.90 % (3673648)Instructions burned: 593 (million) % 42.71/18.90 % (3673631)Instruction limit reached! % 42.71/18.90 % (3673631)------------------------------ % 42.71/18.90 % (3673631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.63/19.04 % (3673631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.63/19.04 % (3673631)CaDiCaL version: 2.1.3 % 44.63/19.04 % (3673631)Termination reason: Instruction limit % 44.63/19.04 % (3673631)Termination phase: Unused predicate definition removal % 44.63/19.04 % (3673631)Time elapsed: 1.847 s % 44.63/19.04 % (3673631)Peak memory usage: 571 MB % 44.63/19.04 % (3673631)Instructions burned: 2350 (million) % 44.63/19.04 % (3673652)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2793826531:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2835 on theBenchmark for (2835ds/125Mi) % 44.63/19.04 % (3673654)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=586684856:i=134:gtgl=5:slsql=off:gtg=exists_sym_2833 on theBenchmark for (2833ds/134Mi) % 44.63/19.04 % (3673652)Instruction limit reached! % 44.63/19.04 % (3673652)------------------------------ % 44.63/19.04 % (3673652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.63/19.04 % (3673652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.63/19.04 % (3673652)CaDiCaL version: 2.1.3 % 44.63/19.04 % (3673652)Termination reason: Instruction limit % 44.63/19.04 % (3673652)Termination phase: Property scanning % 44.63/19.04 % (3673652)Time elapsed: 0.192 s % 44.63/19.04 % (3673652)Peak memory usage: 545 MB % 44.63/19.04 % (3673652)Instructions burned: 126 (million) % 44.63/19.04 % (3673654)Instruction limit reached! % 44.63/19.04 % (3673654)------------------------------ % 44.63/19.04 % (3673654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.63/19.04 % (3673654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.63/19.04 % (3673654)CaDiCaL version: 2.1.3 % 44.63/19.04 % (3673654)Termination reason: Instruction limit % 44.63/19.04 % (3673654)Termination phase: Property scanning % 44.63/19.04 % (3673654)Time elapsed: 0.196 s % 44.63/19.04 % (3673654)Peak memory usage: 545 MB % 44.63/19.04 % (3673654)Instructions burned: 134 (million) % 44.63/19.04 % (3673656)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2232169090:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2831 on theBenchmark for (2831ds/141Mi) % 44.63/19.04 % (3673656)Instruction limit reached! % 44.63/19.04 % (3673656)------------------------------ % 44.63/19.04 % (3673656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.63/19.04 % (3673656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.63/19.04 % (3673656)CaDiCaL version: 2.1.3 % 44.63/19.04 % (3673656)Termination reason: Instruction limit % 44.63/19.04 % (3673656)Termination phase: SInE selection % 44.63/19.04 % (3673656)Time elapsed: 0.108 s % 44.63/19.04 % (3673656)Peak memory usage: 546 MB % 44.63/19.04 % (3673656)Instructions burned: 141 (million) % 44.63/19.04 % (3673658)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=447973517:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2829 on theBenchmark for (2829ds/431Mi) % 44.63/19.04 [W927 18:39:08.539157800 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.63/19.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.63/19.04 [W927 18:39:08.539183207 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.63/19.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.63/19.04 [W927 18:39:08.539213093 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.63/19.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.63/19.04 [W927 18:39:08.539220799 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.63/19.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.63/19.04 [W927 18:39:08.539235529 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.20/20.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.20/20.40 [W927 18:39:08.539242036 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.20/20.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.20/20.40 [W927 18:39:08.539270804 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.20/20.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.20/20.40 [W927 18:39:08.539276562 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.20/20.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.20/20.40 [W927 18:39:08.539337711 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.20/20.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.20/20.40 [W927 18:39:08.539347636 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.20/20.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.20/20.40 [W927 18:39:08.539362531 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.20/20.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.20/20.40 [W927 18:39:08.539368530 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.20/20.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.20/20.40 % (3673659)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=132696295:i=6060:aac=none:ins=25_2828 on theBenchmark for (2828ds/6060Mi) % 54.20/20.40 % (3673658)Instruction limit reached! % 54.20/20.40 % (3673658)------------------------------ % 54.20/20.40 % (3673658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.20/20.40 % (3673658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.20/20.40 % (3673658)CaDiCaL version: 2.1.3 % 54.20/20.40 % (3673658)Termination reason: Instruction limit % 54.20/20.40 % (3673658)Termination phase: SInE selection % 54.20/20.40 % (3673658)Time elapsed: 0.351 s % 54.20/20.40 % (3673658)Peak memory usage: 546 MB % 54.20/20.40 % (3673658)Instructions burned: 432 (million) % 54.20/20.40 % (3673662)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=294904484:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2824 on theBenchmark for (2824ds/150Mi) % 54.20/20.40 % (3673662)Instruction limit reached! % 54.20/20.40 % (3673662)------------------------------ % 54.20/20.40 % (3673662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.20/20.40 % (3673662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.20/20.40 % (3673662)CaDiCaL version: 2.1.3 % 54.20/20.40 % (3673662)Termination reason: Instruction limit % 54.20/20.40 % (3673662)Termination phase: SInE selection % 54.20/20.40 % (3673662)Time elapsed: 0.115 s % 54.20/20.40 % (3673662)Peak memory usage: 546 MB % 54.20/20.40 % (3673662)Instructions burned: 150 (million) % 54.20/20.40 % (3673664)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3073124779:i=14155:bd=all_2821 on theBenchmark for (2821ds/14155Mi) % 61.41/21.45 [W927 18:39:08.430869400 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:08.430905637 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:08.430953754 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:08.430966544 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:08.430992818 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:08.431015431 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:08.431044831 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:08.431057165 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:08.431083038 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:08.431094642 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:08.431120472 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:08.431132175 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.41/21.45 [W927 18:39:09.476883255 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.41/21.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 [W927 18:39:09.476918735 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.23/23.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 [W927 18:39:09.476966272 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.23/23.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 [W927 18:39:09.477051246 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.23/23.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 [W927 18:39:09.477090923 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.23/23.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 [W927 18:39:09.477102813 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.23/23.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 [W927 18:39:09.477130277 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.23/23.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 [W927 18:39:09.477141197 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.23/23.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 [W927 18:39:09.477165861 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.23/23.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 [W927 18:39:09.477177091 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.23/23.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 [W927 18:39:09.477202248 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.23/23.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 [W927 18:39:09.477213114 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.23/23.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.23/23.30 % (3673644)Instruction limit reached! % 74.23/23.30 % (3673644)------------------------------ % 74.23/23.30 % (3673644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.23/23.30 % (3673644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.23/23.30 % (3673644)CaDiCaL version: 2.1.3 % 74.23/23.30 % (3673644)Termination reason: Instruction limit % 74.23/23.30 % (3673644)Termination phase: Saturation % 74.23/23.30 % (3673644)Time elapsed: 3.842 s % 74.23/23.30 % (3673644)Peak memory usage: 626 MB % 74.23/23.30 % (3673644)Instructions burned: 5203 (million) % 74.23/23.30 % (3673666)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3734538275:i=667:av=off:fsr=off_2806 on theBenchmark for (2806ds/667Mi) % 78.69/23.99 % (3673666)Instruction limit reached! % 78.69/23.99 % (3673666)------------------------------ % 78.69/23.99 % (3673666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.69/23.99 % (3673666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.69/23.99 % (3673666)CaDiCaL version: 2.1.3 % 78.69/23.99 % (3673666)Termination reason: Instruction limit % 78.69/23.99 % (3673666)Termination phase: Preprocessing 1 % 78.69/23.99 % (3673666)Time elapsed: 0.545 s % 78.69/23.99 % (3673666)Peak memory usage: 544 MB % 78.69/23.99 % (3673666)Instructions burned: 668 (million) % 78.69/23.99 % (3673668)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2302306815:s2a=on:i=185:s2at=1.8:fdi=4_2799 on theBenchmark for (2799ds/185Mi) % 78.69/23.99 % (3673668)Instruction limit reached! % 78.69/23.99 % (3673668)------------------------------ % 78.69/23.99 % (3673668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.69/23.99 % (3673668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.69/23.99 % (3673668)CaDiCaL version: 2.1.3 % 78.69/23.99 % (3673668)Termination reason: Instruction limit % 78.69/23.99 % (3673668)Termination phase: SInE selection % 78.69/23.99 % (3673668)Time elapsed: 0.147 s % 78.69/23.99 % (3673668)Peak memory usage: 546 MB % 78.69/23.99 % (3673668)Instructions burned: 187 (million) % 78.69/23.99 [W927 18:39:11.892976569 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 78.69/23.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 78.69/23.99 [W927 18:39:11.893030819 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 78.69/23.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 78.69/23.99 [W927 18:39:11.893079610 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 78.69/23.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 78.69/23.99 [W927 18:39:11.893092573 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 78.69/23.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 78.69/23.99 [W927 18:39:11.893120720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 78.69/23.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 78.69/23.99 [W927 18:39:11.893133180 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 78.69/23.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 78.69/23.99 [W927 18:39:11.893162313 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 78.69/23.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 78.69/23.99 [W927 18:39:11.893174104 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 78.69/23.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 78.69/23.99 [W927 18:39:11.893202620 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 78.69/23.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.16/27.28 [W927 18:39:11.893214424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.16/27.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.16/27.28 [W927 18:39:11.893247647 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.16/27.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.16/27.28 [W927 18:39:11.893269594 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.16/27.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.16/27.28 % (3673670)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=543739845:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2795 on theBenchmark for (2795ds/193Mi) % 52.16/27.28 % (3673670)Instruction limit reached! % 52.16/27.28 % (3673670)------------------------------ % 52.16/27.28 % (3673670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.16/27.28 % (3673670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.16/27.28 % (3673670)CaDiCaL version: 2.1.3 % 52.16/27.28 % (3673670)Termination reason: Instruction limit % 52.16/27.28 % (3673670)Termination phase: SInE selection % 52.16/27.28 % (3673670)Time elapsed: 0.152 s % 52.16/27.28 % (3673670)Peak memory usage: 546 MB % 52.16/27.28 % (3673670)Instructions burned: 193 (million) % 52.16/27.28 % (3673672)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2580606566:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2792 on theBenchmark for (2792ds/4850Mi) % 52.16/27.28 [W927 18:39:13.734977190 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.16/27.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.16/27.28 [W927 18:39:13.735031767 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.16/27.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.16/27.28 [W927 18:39:13.735082877 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.16/27.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.16/27.28 [W927 18:39:13.735096834 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.16/27.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.16/27.28 [W927 18:39:13.735122371 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.16/27.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.16/27.28 [W927 18:39:13.735133961 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.16/27.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.16/27.28 [W927 18:39:13.735162528 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.16/27.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.16/27.28 [W927 18:39:13.735174225 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.735200328 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.735210652 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.735236825 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.735246815 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 % (3673659)Instruction limit reached! % 0.17/27.93 % (3673659)------------------------------ % 0.17/27.93 % (3673659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 0.17/27.93 % (3673659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.17/27.93 % (3673659)CaDiCaL version: 2.1.3 % 0.17/27.93 % (3673659)Termination reason: Instruction limit % 0.17/27.93 % (3673659)Termination phase: Saturation % 0.17/27.93 % (3673659)Time elapsed: 5.104 s % 0.17/27.93 % (3673659)Peak memory usage: 858 MB % 0.17/27.93 % (3673659)Instructions burned: 6060 (million) % 0.17/27.93 % (3673674)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=874124746:i=12111:sd=1:ss=included_2775 on theBenchmark for (2775ds/12111Mi) % 0.17/27.93 % (3673672)Refutation not found, incomplete strategy % 0.17/27.93 % (3673672)------------------------------ % 0.17/27.93 % (3673672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 0.17/27.93 % (3673672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.17/27.93 % (3673672)CaDiCaL version: 2.1.3 % 0.17/27.93 % (3673672)Termination reason: Refutation not found, incomplete strategy % 0.17/27.93 % (3673672)Time elapsed: 1.964 s % 0.17/27.93 % (3673672)Peak memory usage: 584 MB % 0.17/27.93 % (3673672)Instructions burned: 2100 (million) % 0.17/27.93 [W927 18:39:13.434448889 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.434486512 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.434534376 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.434547840 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.434578516 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.434590397 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.434625574 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.434692177 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.434728294 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.434739848 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.434768068 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 [W927 18:39:13.434779238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 0.17/27.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 0.17/27.93 % (3673672)------------------------------ % 0.17/27.93 % (3673672)------------------------------ % 0.17/27.93 % (3673676)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2225771071:i=319:kws=precedence:fsr=off_2765 on theBenchmark for (2765ds/319Mi) % 0.17/27.93 % (3673676)Instruction limit reached! % 0.17/27.93 % (3673676)------------------------------ % 0.17/27.93 % (3673676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 0.17/27.93 % (3673676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.17/27.93 % (3673676)CaDiCaL version: 2.1.3 % 0.17/27.93 % (3673676)Termination reason: Instruction limit % 0.17/27.93 % (3673676)Termination phase: Preprocessing 1 % 0.17/27.93 % (3673676)Time elapsed: 0.239 s % 0.17/27.93 % (3673676)Peak memory usage: 544 MB % 0.17/27.93 % (3673676)Instructions burned: 320 (million) % 0.17/27.93 % (3673678)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2353785020:i=2064:ep=RST_2760 on theBenchmark for (2760ds/2064Mi) % 0.17/27.93 % (3673608)First to succeed. % 0.17/27.93 % (3673608)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3673603" % 0.17/27.93 % SZS status Satisfiable for theBenchmark % 0.17/27.93 % SZS output start Saturation. % 0.17/27.93 % SZS output end Saturation. % 0.17/27.93 % SZS output start Definitions and Model Updates. % 0.17/27.93 for all inputs, % 0.17/27.93 define has__gloss(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define derivation(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define lexical__category(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define hypernym(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define lexicalization(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define antonym(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define holonym__part(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define instance(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define means(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define hyponym(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define attribute(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define has__category(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define derived(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define has__region__domain(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define meronym__member(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define holonym__member(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define similar(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define category__of(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define meronym__part(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define holonym__substance(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define closely__related(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define verbgroup(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define meronym__substance(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define has__usage__domain(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define has__instance(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define entailment(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define cause(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define region__domain__of(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define usage__domain__of(X0,X1) := $true % 0.17/27.93 for all inputs, % 0.17/27.93 define derived__participle(X0,X1) := $true % 0.17/27.93 % SZS output end Definitions and Model Updates. % 0.17/27.93 % (3673608)------------------------------ % 0.17/27.93 % (3673608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 0.17/27.93 % (3673608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.17/27.93 % (3673608)CaDiCaL version: 2.1.3 % 0.17/27.93 % (3673608)Termination reason: Satisfiable % 0.17/27.93 % (3673608)Time elapsed: 11.863 s % 0.17/27.93 % (3673608)Peak memory usage: 1142 MB % 0.17/27.93 % (3673608)Instructions burned: 14394 (million) % 0.17/27.93 % (3673608)------------------------------ % 0.17/27.93 % (3673608)------------------------------ % 0.17/27.93 % (3673603)Success in time 26.394 s % 0.17/27.93 % Vampire exiting %------------------------------------------------------------------------------