%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP262+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 : n011.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:15 PM UTC 2026
% Result : Theorem 81.51s 25.68s
% Output : Refutation 81.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 23 ( 16 unt; 0 def)
% Number of atoms : 34 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 29 ( 18 ~; 9 |; 1 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 15 ( 15 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1050,axiom,
hypernym(n9986904,n10126424),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb1049) ).
fof(f117092,axiom,
hypernym(n10560637,n7846),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb117091) ).
fof(f340305,axiom,
hypernym(n10126424,n9855630),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb340304) ).
fof(f886123,axiom,
hypernym(n9855630,n10560637),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb886122) ).
fof(f1026858,axiom,
! [X0,X1,X2] :
( ( hypernym(X0,X1)
& hypernym(X1,X2) )
=> hypernym(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom1) ).
fof(f1026861,conjecture,
hypernym(n9986904,n7846),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hypernym_transitiviy_1) ).
fof(f1026862,negated_conjecture,
~ hypernym(n9986904,n7846),
inference(negated_conjecture,[status(cth)],[f1026861]) ).
fof(f1026863,plain,
~ hypernym(n9986904,n7846),
inference(flattening,[],[f1026862]) ).
fof(f1027217,plain,
! [X0,X1,X2] :
( hypernym(X0,X2)
| ~ hypernym(X0,X1)
| ~ hypernym(X1,X2) ),
inference(ennf_transformation,[],[f1026858]) ).
fof(f1027218,plain,
! [X0,X1,X2] :
( hypernym(X0,X2)
| ~ hypernym(X0,X1)
| ~ hypernym(X1,X2) ),
inference(flattening,[],[f1027217]) ).
fof(f1027221,plain,
! [X2,X0,X1] :
( hypernym(X0,X2)
| ~ hypernym(X0,X1)
| ~ hypernym(X1,X2) ),
inference(cnf_transformation,[],[f1027218]) ).
fof(f1027224,plain,
~ hypernym(n9986904,n7846),
inference(cnf_transformation,[],[f1026863]) ).
fof(f1027226,plain,
hypernym(n9986904,n10126424),
inference(cnf_transformation,[],[f1050]) ).
fof(f1027228,plain,
hypernym(n10126424,n9855630),
inference(cnf_transformation,[],[f340305]) ).
fof(f1027229,plain,
hypernym(n9855630,n10560637),
inference(cnf_transformation,[],[f886123]) ).
fof(f1027283,plain,
hypernym(n10560637,n7846),
inference(cnf_transformation,[],[f117092]) ).
fof(f1027354,plain,
! [X0] :
( ~ hypernym(n9986904,X0)
| ~ hypernym(X0,n7846) ),
inference(resolution,[],[f1027224,f1027221]) ).
fof(f1027356,plain,
~ hypernym(n10126424,n7846),
inference(resolution,[],[f1027354,f1027226]) ).
fof(f1027360,plain,
! [X0] :
( ~ hypernym(n10126424,X0)
| ~ hypernym(X0,n7846) ),
inference(resolution,[],[f1027356,f1027221]) ).
fof(f1027364,plain,
~ hypernym(n9855630,n7846),
inference(resolution,[],[f1027360,f1027228]) ).
fof(f1027368,plain,
! [X0] :
( ~ hypernym(n9855630,X0)
| ~ hypernym(X0,n7846) ),
inference(resolution,[],[f1027364,f1027221]) ).
fof(f1027375,plain,
~ hypernym(n10560637,n7846),
inference(resolution,[],[f1027368,f1027229]) ).
fof(f1027378,plain,
$false,
inference(forward_subsumption_resolution,[],[f1027375,f1027283]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP262+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.14/0.41 % Computer : n011.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 27 18:38:15 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.45 Running first-order theorem proving
% 0.14/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
% 31.11/18.12 % (2681294)Detected formulas, will run a generic FOF schedule.
% 31.11/18.12 % (2681896)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=3816336041:i=141193_2851 on theBenchmark for (2851ds/141193Mi)
% 31.11/18.12 % (2681932)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2156418882:i=109:sd=1:ins=1:gsp=on:ss=axioms_2851 on theBenchmark for (2851ds/109Mi)
% 31.11/18.12 % (2681907)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=837260084:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2851 on theBenchmark for (2851ds/134677Mi)
% 31.11/18.12 % (2681921)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=2702203062:i=141695:sd=1:nm=32:gsp=on:ss=included_2851 on theBenchmark for (2851ds/141695Mi)
% 31.11/18.12 % (2681932)Instruction limit reached!
% 31.11/18.12 % (2681932)------------------------------
% 31.11/18.12 % (2681932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.11/18.12 % (2681932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.11/18.12 % (2681932)CaDiCaL version: 2.1.3
% 31.11/18.12 % (2681932)Termination reason: Instruction limit
% 31.11/18.12 % (2681932)Termination phase: SInE selection
% 31.11/18.12 % (2681932)Time elapsed: 0.045 s
% 31.11/18.12 % (2681932)Peak memory usage: 546 MB
% 31.11/18.12 % (2681932)Instructions burned: 109 (million)
% 31.11/18.12 % (2681938)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1814542870:i=119:av=off:ss=axioms_2851 on theBenchmark for (2851ds/119Mi)
% 31.11/18.12 % (2681940)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1813952176:s2a=on:i=139:gtg=position_2851 on theBenchmark for (2851ds/139Mi)
% 31.11/18.12 % (2681941)dis-21_1_sil=8000:lcm=predicate:random_seed=1608550565:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2851 on theBenchmark for (2851ds/129Mi)
% 31.11/18.12 % (2681938)Instruction limit reached!
% 31.11/18.12 % (2681938)------------------------------
% 31.11/18.12 % (2681938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.11/18.12 % (2681938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.11/18.12 % (2681938)CaDiCaL version: 2.1.3
% 31.11/18.12 % (2681938)Termination reason: Instruction limit
% 31.11/18.12 % (2681938)Termination phase: SInE selection
% 31.11/18.12 % (2681938)Time elapsed: 0.084 s
% 31.11/18.12 % (2681938)Peak memory usage: 546 MB
% 31.11/18.12 % (2681938)Instructions burned: 120 (million)
% 31.11/18.12 % (2681941)Instruction limit reached!
% 31.11/18.12 % (2681941)------------------------------
% 31.11/18.12 % (2681941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.11/18.12 % (2681941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.11/18.12 % (2681941)CaDiCaL version: 2.1.3
% 31.11/18.12 % (2681941)Termination reason: Instruction limit
% 31.11/18.12 % (2681941)Termination phase: SInE selection
% 31.11/18.12 % (2681941)Time elapsed: 0.091 s
% 31.11/18.12 % (2681941)Peak memory usage: 546 MB
% 31.11/18.12 % (2681941)Instructions burned: 129 (million)
% 31.11/18.12 % (2681950)lrs+10_1_sil=8000:sp=occurrence:random_seed=3181233540:i=285:sd=3:ss=axioms:sgt=8_2849 on theBenchmark for (2849ds/285Mi)
% 31.11/18.12 % (2681940)Instruction limit reached!
% 31.11/18.12 % (2681940)------------------------------
% 31.11/18.12 % (2681940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.11/18.12 % (2681940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.11/18.12 % (2681940)CaDiCaL version: 2.1.3
% 31.11/18.12 % (2681940)Termination reason: Instruction limit
% 31.11/18.12 % (2681940)Termination phase: Property scanning
% 31.11/18.12 % (2681940)Time elapsed: 0.200 s
% 31.11/18.12 % (2681940)Peak memory usage: 545 MB
% 31.11/18.12 % (2681940)Instructions burned: 140 (million)
% 31.11/18.12 % (2681950)Instruction limit reached!
% 31.11/18.12 % (2681950)------------------------------
% 31.11/18.12 % (2681950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.11/18.12 % (2681950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.11/18.12 % (2681950)CaDiCaL version: 2.1.3
% 31.11/18.12 % (2681950)Termination reason: Instruction limit
% 31.11/18.12 % (2681950)Termination phase: SInE selection
% 31.11/18.12 % (2681950)Time elapsed: 0.128 s
% 31.11/18.12 % (2681950)Peak memory usage: 546 MB
% 31.11/18.12 % (2681950)Instructions burned: 286 (million)
% 40.61/19.44 % (2681952)lrs+10_1_sil=32000:urr=on:br=off:random_seed=487464274:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2848 on theBenchmark for (2848ds/157Mi)
% 40.61/19.44 % (2681954)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4015728440:i=325:sd=1:ss=axioms:sgt=32_2847 on theBenchmark for (2847ds/325Mi)
% 40.61/19.44 % (2681955)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=1713147616:s2a=on:i=248:s2at=1.23:gtg=position_2846 on theBenchmark for (2846ds/248Mi)
% 40.61/19.44 % (2681957)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1898719618:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2846 on theBenchmark for (2846ds/294Mi)
% 40.61/19.44 % (2681952)Instruction limit reached!
% 40.61/19.44 % (2681952)------------------------------
% 40.61/19.44 % (2681952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.61/19.44 % (2681952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.61/19.44 % (2681952)CaDiCaL version: 2.1.3
% 40.61/19.44 % (2681952)Termination reason: Instruction limit
% 40.61/19.44 % (2681952)Termination phase: Property scanning
% 40.61/19.44 % (2681952)Time elapsed: 0.206 s
% 40.61/19.44 % (2681952)Peak memory usage: 545 MB
% 40.61/19.44 % (2681952)Instructions burned: 157 (million)
% 40.61/19.44 % (2681954)Instruction limit reached!
% 40.61/19.44 % (2681954)------------------------------
% 40.61/19.44 % (2681954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.61/19.44 % (2681954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.61/19.44 % (2681954)CaDiCaL version: 2.1.3
% 40.61/19.44 % (2681954)Termination reason: Instruction limit
% 40.61/19.44 % (2681954)Termination phase: SInE selection
% 40.61/19.44 % (2681954)Time elapsed: 0.242 s
% 40.61/19.44 % (2681954)Peak memory usage: 546 MB
% 40.61/19.44 % (2681954)Instructions burned: 326 (million)
% 40.61/19.44 % (2681957)Instruction limit reached!
% 40.61/19.44 % (2681957)------------------------------
% 40.61/19.44 % (2681957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.61/19.44 % (2681957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.61/19.44 % (2681957)CaDiCaL version: 2.1.3
% 40.61/19.44 % (2681957)Termination reason: Instruction limit
% 40.61/19.44 % (2681957)Termination phase: SInE selection
% 40.61/19.44 % (2681957)Time elapsed: 0.147 s
% 40.61/19.44 % (2681957)Peak memory usage: 546 MB
% 40.61/19.44 % (2681957)Instructions burned: 295 (million)
% 40.61/19.44 % (2681955)Instruction limit reached!
% 40.61/19.44 % (2681955)------------------------------
% 40.61/19.44 % (2681955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.61/19.44 % (2681955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.61/19.44 % (2681955)CaDiCaL version: 2.1.3
% 40.61/19.44 % (2681955)Termination reason: Instruction limit
% 40.61/19.44 % (2681955)Termination phase: Property scanning
% 40.61/19.44 % (2681955)Time elapsed: 0.246 s
% 40.61/19.44 % (2681955)Peak memory usage: 545 MB
% 40.61/19.44 % (2681955)Instructions burned: 249 (million)
% 40.61/19.44 % (2681961)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2167001785:i=2350_2844 on theBenchmark for (2844ds/2350Mi)
% 40.61/19.44 % (2681963)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3005834898:i=127:av=off:fsr=off:sup=off_2843 on theBenchmark for (2843ds/127Mi)
% 40.61/19.44 % (2681962)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3894483485:cts=off:i=113:fsr=off:ss=included:sgt=4_2843 on theBenchmark for (2843ds/113Mi)
% 40.61/19.44 % (2681963)Instruction limit reached!
% 40.61/19.44 % (2681963)------------------------------
% 40.61/19.44 % (2681963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.61/19.44 % (2681963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.61/19.44 % (2681963)CaDiCaL version: 2.1.3
% 40.61/19.44 % (2681963)Termination reason: Instruction limit
% 40.61/19.44 % (2681963)Termination phase: Preprocessing 1
% 40.61/19.44 % (2681963)Time elapsed: 0.056 s
% 40.61/19.44 % (2681963)Peak memory usage: 544 MB
% 40.61/19.44 % (2681963)Instructions burned: 129 (million)
% 40.61/19.44 % (2681962)Instruction limit reached!
% 40.61/19.44 % (2681962)------------------------------
% 40.61/19.44 % (2681962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.61/19.44 % (2681962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.61/19.44 % (2681962)CaDiCaL version: 2.1.3
% 37.24/25.11 % (2681962)Termination reason: Instruction limit
% 37.24/25.11 % (2681962)Termination phase: SInE selection
% 37.24/25.11 % (2681962)Time elapsed: 0.079 s
% 37.24/25.11 % (2681962)Peak memory usage: 546 MB
% 37.24/25.11 % (2681962)Instructions burned: 114 (million)
% 37.24/25.11 % (2681965)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=826183088:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2842 on theBenchmark for (2842ds/114Mi)
% 37.24/25.11 % (2681968)lrs+10_1_sil=8000:sp=occurrence:random_seed=2441714202:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2841 on theBenchmark for (2841ds/907Mi)
% 37.24/25.11 % (2681969)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1514851267:i=437:sd=1:aac=none:ss=included_2840 on theBenchmark for (2840ds/437Mi)
% 37.24/25.11 % (2681965)Instruction limit reached!
% 37.24/25.11 % (2681965)------------------------------
% 37.24/25.11 % (2681965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.24/25.11 % (2681965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.24/25.11 % (2681965)CaDiCaL version: 2.1.3
% 37.24/25.11 % (2681965)Termination reason: Instruction limit
% 37.24/25.11 % (2681965)Termination phase: Property scanning
% 37.24/25.11 % (2681965)Time elapsed: 0.187 s
% 37.24/25.11 % (2681965)Peak memory usage: 545 MB
% 37.24/25.11 % (2681965)Instructions burned: 114 (million)
% 37.24/25.11 % (2681973)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=48702844:i=5202:ss=axioms:sgt=16_2838 on theBenchmark for (2838ds/5202Mi)
% 37.24/25.11 % (2681969)Instruction limit reached!
% 37.24/25.11 % (2681969)------------------------------
% 37.24/25.11 % (2681969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.24/25.11 % (2681969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.24/25.11 % (2681969)CaDiCaL version: 2.1.3
% 37.24/25.11 % (2681969)Termination reason: Instruction limit
% 37.24/25.11 % (2681969)Termination phase: SInE selection
% 37.24/25.11 % (2681969)Time elapsed: 0.330 s
% 37.24/25.11 % (2681969)Peak memory usage: 546 MB
% 37.24/25.11 % (2681969)Instructions burned: 438 (million)
% 37.24/25.11 % (2681968)Instruction limit reached!
% 37.24/25.11 % (2681968)------------------------------
% 37.24/25.11 % (2681968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.24/25.11 % (2681968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.24/25.11 % (2681968)CaDiCaL version: 2.1.3
% 37.24/25.11 % (2681968)Termination reason: Instruction limit
% 37.24/25.11 % (2681968)Termination phase: SInE selection
% 37.24/25.11 % (2681968)Time elapsed: 0.472 s
% 37.24/25.11 % (2681968)Peak memory usage: 559 MB
% 37.24/25.11 % (2681968)Instructions burned: 908 (million)
% 37.24/25.11 % (2681975)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2481052424:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2835 on theBenchmark for (2835ds/134Mi)
% 37.24/25.11 % (2681976)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1303780638:st=8:i=592:sd=3:ep=RST:ss=axioms_2834 on theBenchmark for (2834ds/592Mi)
% 37.24/25.11 % (2681975)Instruction limit reached!
% 37.24/25.11 % (2681975)------------------------------
% 37.24/25.11 % (2681975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.24/25.11 % (2681975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.24/25.11 % (2681975)CaDiCaL version: 2.1.3
% 37.24/25.11 % (2681975)Termination reason: Instruction limit
% 37.24/25.11 % (2681975)Termination phase: SInE selection
% 37.24/25.11 % (2681975)Time elapsed: 0.095 s
% 37.24/25.11 % (2681975)Peak memory usage: 546 MB
% 37.24/25.11 % (2681975)Instructions burned: 135 (million)
% 37.24/25.11 % (2681979)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3013885651:st=3:i=13193:sd=3:ss=axioms_2832 on theBenchmark for (2832ds/13193Mi)
% 37.24/25.11 % (2681976)Instruction limit reached!
% 37.24/25.11 % (2681976)------------------------------
% 37.24/25.11 % (2681976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.24/25.11 % (2681976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.24/25.11 % (2681976)CaDiCaL version: 2.1.3
% 37.24/25.11 % (2681976)Termination reason: Instruction limit
% 37.24/25.11 % (2681976)Termination phase: SInE selection
% 37.24/25.11 % (2681976)Time elapsed: 0.317 s
% 37.24/25.11 % (2681976)Peak memory usage: 546 MB
% 37.24/25.11 % (2681976)Instructions burned: 593 (million)
% 37.24/25.11 % (2681981)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=126396308:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2829 on theBenchmark for (2829ds/125Mi)
% 81.51/25.68 % (2681981)Instruction limit reached!
% 81.51/25.68 % (2681981)------------------------------
% 81.51/25.68 % (2681981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2681981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2681981)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2681981)Termination reason: Instruction limit
% 81.51/25.68 % (2681981)Termination phase: Property scanning
% 81.51/25.68 % (2681981)Time elapsed: 0.116 s
% 81.51/25.68 % (2681981)Peak memory usage: 545 MB
% 81.51/25.68 % (2681981)Instructions burned: 127 (million)
% 81.51/25.68 % (2681983)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2205875428:i=134:gtgl=5:slsql=off:gtg=exists_sym_2827 on theBenchmark for (2827ds/134Mi)
% 81.51/25.68 % (2681983)Instruction limit reached!
% 81.51/25.68 % (2681983)------------------------------
% 81.51/25.68 % (2681983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2681983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2681983)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2681983)Termination reason: Instruction limit
% 81.51/25.68 % (2681983)Termination phase: Property scanning
% 81.51/25.68 % (2681983)Time elapsed: 0.118 s
% 81.51/25.68 % (2681983)Peak memory usage: 545 MB
% 81.51/25.68 % (2681983)Instructions burned: 136 (million)
% 81.51/25.68 % (2681961)Instruction limit reached!
% 81.51/25.68 % (2681961)------------------------------
% 81.51/25.68 % (2681961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2681961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2681961)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2681961)Termination reason: Instruction limit
% 81.51/25.68 % (2681961)Termination phase: Unused predicate definition removal
% 81.51/25.68 % (2681961)Time elapsed: 1.838 s
% 81.51/25.68 % (2681961)Peak memory usage: 571 MB
% 81.51/25.68 % (2681961)Instructions burned: 2350 (million)
% 81.51/25.68 % (2681985)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3632337679:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2824 on theBenchmark for (2824ds/141Mi)
% 81.51/25.68 % (2681985)Instruction limit reached!
% 81.51/25.68 % (2681985)------------------------------
% 81.51/25.68 % (2681985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2681985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2681985)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2681985)Termination reason: Instruction limit
% 81.51/25.68 % (2681985)Termination phase: SInE selection
% 81.51/25.68 % (2681985)Time elapsed: 0.068 s
% 81.51/25.68 % (2681985)Peak memory usage: 546 MB
% 81.51/25.68 % (2681985)Instructions burned: 143 (million)
% 81.51/25.68 % (2681986)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=853864109:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2823 on theBenchmark for (2823ds/431Mi)
% 81.51/25.68 % (2681989)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=2689893961:i=6060:aac=none:ins=25_2821 on theBenchmark for (2821ds/6060Mi)
% 81.51/25.68 % (2681986)Instruction limit reached!
% 81.51/25.68 % (2681986)------------------------------
% 81.51/25.68 % (2681986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2681986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2681986)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2681986)Termination reason: Instruction limit
% 81.51/25.68 % (2681986)Termination phase: SInE selection
% 81.51/25.68 % (2681986)Time elapsed: 0.328 s
% 81.51/25.68 % (2681986)Peak memory usage: 546 MB
% 81.51/25.68 % (2681986)Instructions burned: 432 (million)
% 81.51/25.68 % (2681991)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=809449561:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2818 on theBenchmark for (2818ds/150Mi)
% 81.51/25.68 % (2681991)Instruction limit reached!
% 81.51/25.68 % (2681991)------------------------------
% 81.51/25.68 % (2681991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2681991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2681991)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2681991)Termination reason: Instruction limit
% 81.51/25.68 % (2681991)Termination phase: SInE selection
% 81.51/25.68 % (2681991)Time elapsed: 0.115 s
% 81.51/25.68 % (2681991)Peak memory usage: 546 MB
% 81.51/25.68 % (2681991)Instructions burned: 150 (million)
% 81.51/25.68 % (2681993)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=95812433:i=14155:bd=all_2815 on theBenchmark for (2815ds/14155Mi)
% 81.51/25.68 % (2681973)Instruction limit reached!
% 81.51/25.68 % (2681973)------------------------------
% 81.51/25.68 % (2681973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2681973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2681973)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2681973)Termination reason: Instruction limit
% 81.51/25.68 % (2681973)Termination phase: Saturation
% 81.51/25.68 % (2681973)Time elapsed: 3.803 s
% 81.51/25.68 % (2681973)Peak memory usage: 628 MB
% 81.51/25.68 % (2681973)Instructions burned: 5202 (million)
% 81.51/25.68 % (2681995)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1930791612:i=667:av=off:fsr=off_2798 on theBenchmark for (2798ds/667Mi)
% 81.51/25.68 % (2681995)Instruction limit reached!
% 81.51/25.68 % (2681995)------------------------------
% 81.51/25.68 % (2681995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2681995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2681995)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2681995)Termination reason: Instruction limit
% 81.51/25.68 % (2681995)Termination phase: Preprocessing 1
% 81.51/25.68 % (2681995)Time elapsed: 0.555 s
% 81.51/25.68 % (2681995)Peak memory usage: 544 MB
% 81.51/25.68 % (2681995)Instructions burned: 668 (million)
% 81.51/25.68 % (2681989)Instruction limit reached!
% 81.51/25.68 % (2681989)------------------------------
% 81.51/25.68 % (2681989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2681989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2681989)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2681989)Termination reason: Instruction limit
% 81.51/25.68 % (2681989)Termination phase: Saturation
% 81.51/25.68 % (2681989)Time elapsed: 3.184 s
% 81.51/25.68 % (2681989)Peak memory usage: 771 MB
% 81.51/25.68 % (2681989)Instructions burned: 6064 (million)
% 81.51/25.68 % (2681997)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=3774422925:s2a=on:i=185:s2at=1.8:fdi=4_2790 on theBenchmark for (2790ds/185Mi)
% 81.51/25.68 % (2681997)Instruction limit reached!
% 81.51/25.68 % (2681997)------------------------------
% 81.51/25.68 % (2681997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2681997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2681997)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2681997)Termination reason: Instruction limit
% 81.51/25.68 % (2681997)Termination phase: SInE selection
% 81.51/25.68 % (2681997)Time elapsed: 0.145 s
% 81.51/25.68 % (2681997)Peak memory usage: 546 MB
% 81.51/25.68 % (2681997)Instructions burned: 185 (million)
% 81.51/25.68 % (2681999)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3553982960:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2788 on theBenchmark for (2788ds/193Mi)
% 81.51/25.68 % (2681999)Instruction limit reached!
% 81.51/25.68 % (2681999)------------------------------
% 81.51/25.68 % (2681999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2681999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2681999)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2681999)Termination reason: Instruction limit
% 81.51/25.68 % (2681999)Termination phase: SInE selection
% 81.51/25.68 % (2681999)Time elapsed: 0.098 s
% 81.51/25.68 % (2681999)Peak memory usage: 546 MB
% 81.51/25.68 % (2681999)Instructions burned: 195 (million)
% 81.51/25.68 % (2682001)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=576210285:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2786 on theBenchmark for (2786ds/4850Mi)
% 81.51/25.68 % (2682002)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4211113857:i=12111:sd=1:ss=included_2785 on theBenchmark for (2785ds/12111Mi)
% 81.51/25.68 % (2682001)First to succeed.
% 81.51/25.68 % (2682001)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2681294"
% 81.51/25.68 % (2682001)Refutation found. Thanks to Tanya!
% 81.51/25.68 % SZS status Theorem for theBenchmark
% 81.51/25.68 % SZS output start Proof for theBenchmark
% See solution above
% 81.51/25.68 % (2682001)------------------------------
% 81.51/25.68 % (2682001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.51/25.68 % (2682001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.51/25.68 % (2682001)CaDiCaL version: 2.1.3
% 81.51/25.68 % (2682001)Termination reason: Refutation
% 81.51/25.68 % (2682001)Time elapsed: 1.913 s
% 81.51/25.68 % (2682001)Peak memory usage: 586 MB
% 81.51/25.68 % (2682001)Instructions burned: 2165 (million)
% 81.51/25.68 % (2682001)------------------------------
% 81.51/25.68 % (2682001)------------------------------
% 81.51/25.68 % (2681294)Success in time 24.145 s
% 81.51/25.68 % Vampire exiting
%------------------------------------------------------------------------------