%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR079+6 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 09:42:43 AM UTC 2026
% Result : Theorem 21.38s 11.00s
% Output : Refutation 66.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 18
% Syntax : Number of formulae : 72 ( 49 unt; 0 def)
% Number of atoms : 124 ( 26 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 120 ( 68 ~; 45 |; 4 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 17 con; 0-0 aty)
% Number of variables : 35 ( 35 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26456,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_26635) ).
fof(f26457,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_26636) ).
fof(f34863,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_35116) ).
fof(f34892,axiom,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_35145) ).
fof(f34966,axiom,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_35219) ).
fof(f55588,axiom,
s__instance(s__Organism5_1,s__Lizard5_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(f55609,axiom,
s__Class5_1 = s__Class5_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_23) ).
fof(f55610,axiom,
s__Class5_2 = s__Class5_3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_24) ).
fof(f55611,axiom,
s__Class5_3 = s__Class5_4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_25) ).
fof(f55612,axiom,
s__Class5_4 = s__Class5_5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_26) ).
fof(f55613,axiom,
s__Class5_5 = s__Class5_6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_27) ).
fof(f55614,axiom,
s__Class5_6 = s__Class5_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_28) ).
fof(f55615,axiom,
s__Class5_7 = s__Class5_8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_29) ).
fof(f55616,axiom,
s__Class5_8 = s__Class5_9,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_30) ).
fof(f55617,axiom,
s__Class5_9 = s__Class5_10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_31) ).
fof(f55618,axiom,
s__subclass(s__Lizard5_1,s__Class5_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_32) ).
fof(f55619,axiom,
s__subclass(s__Class5_10,s__Reptile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_33) ).
fof(f55620,conjecture,
s__instance(s__Organism5_1,s__Animal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(f55621,negated_conjecture,
~ s__instance(s__Organism5_1,s__Animal),
inference(negated_conjecture,[status(cth)],[f55620]) ).
fof(f55622,plain,
~ s__instance(s__Organism5_1,s__Animal),
inference(flattening,[],[f55621]) ).
fof(f57912,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f26457]) ).
fof(f57913,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f57912]) ).
fof(f57914,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26456]) ).
fof(f61991,plain,
s__instance(s__Organism5_1,s__Lizard5_1),
inference(cnf_transformation,[],[f55588]) ).
fof(f62012,plain,
s__Class5_1 = s__Class5_2,
inference(cnf_transformation,[],[f55609]) ).
fof(f62013,plain,
s__Class5_2 = s__Class5_3,
inference(cnf_transformation,[],[f55610]) ).
fof(f62014,plain,
s__Class5_3 = s__Class5_4,
inference(cnf_transformation,[],[f55611]) ).
fof(f62015,plain,
s__Class5_4 = s__Class5_5,
inference(cnf_transformation,[],[f55612]) ).
fof(f62016,plain,
s__Class5_5 = s__Class5_6,
inference(cnf_transformation,[],[f55613]) ).
fof(f62017,plain,
s__Class5_6 = s__Class5_7,
inference(cnf_transformation,[],[f55614]) ).
fof(f62018,plain,
s__Class5_7 = s__Class5_8,
inference(cnf_transformation,[],[f55615]) ).
fof(f62019,plain,
s__Class5_8 = s__Class5_9,
inference(cnf_transformation,[],[f55616]) ).
fof(f62020,plain,
s__Class5_9 = s__Class5_10,
inference(cnf_transformation,[],[f55617]) ).
fof(f62021,plain,
s__subclass(s__Lizard5_1,s__Class5_1),
inference(cnf_transformation,[],[f55618]) ).
fof(f62022,plain,
s__subclass(s__Class5_10,s__Reptile),
inference(cnf_transformation,[],[f55619]) ).
fof(f62023,plain,
~ s__instance(s__Organism5_1,s__Animal),
inference(cnf_transformation,[],[f55622]) ).
fof(f62032,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f57913]) ).
fof(f62033,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f57914]) ).
fof(f62034,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f57914]) ).
fof(f62068,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
inference(cnf_transformation,[],[f34966]) ).
fof(f62200,plain,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
inference(cnf_transformation,[],[f34892]) ).
fof(f63410,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(cnf_transformation,[],[f34863]) ).
fof(f69202,plain,
s__Class5_8 = s__Class5_10,
inference(definition_unfolding,[],[f62019,f62020]) ).
fof(f69203,plain,
s__Class5_7 = s__Class5_10,
inference(definition_unfolding,[],[f62018,f69202]) ).
fof(f69204,plain,
s__Class5_6 = s__Class5_10,
inference(definition_unfolding,[],[f62017,f69203]) ).
fof(f69205,plain,
s__Class5_5 = s__Class5_10,
inference(definition_unfolding,[],[f62016,f69204]) ).
fof(f69206,plain,
s__Class5_4 = s__Class5_10,
inference(definition_unfolding,[],[f62015,f69205]) ).
fof(f69207,plain,
s__Class5_3 = s__Class5_10,
inference(definition_unfolding,[],[f62014,f69206]) ).
fof(f69208,plain,
s__Class5_2 = s__Class5_10,
inference(definition_unfolding,[],[f62013,f69207]) ).
fof(f69209,plain,
s__Class5_1 = s__Class5_10,
inference(definition_unfolding,[],[f62012,f69208]) ).
fof(f69228,plain,
s__subclass(s__Lizard5_1,s__Class5_10),
inference(definition_unfolding,[],[f62021,f69209]) ).
fof(f69469,plain,
! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[],[f62023,f62032]) ).
fof(f69483,plain,
! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f69469,f62034]) ).
fof(f69485,plain,
! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Organism5_1,X0) ),
inference(forward_subsumption_resolution,[],[f69483,f62033]) ).
fof(f69519,plain,
~ s__instance(s__Organism5_1,s__Vertebrate),
inference(resolution,[],[f69485,f63410]) ).
fof(f69549,plain,
! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[],[f69519,f62032]) ).
fof(f69563,plain,
! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f69549,f62034]) ).
fof(f69564,plain,
! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Organism5_1,X0) ),
inference(forward_subsumption_resolution,[],[f69563,f62033]) ).
fof(f69696,plain,
~ s__instance(s__Organism5_1,s__ColdBloodedVertebrate),
inference(resolution,[],[f69564,f62200]) ).
fof(f69705,plain,
! [X0] :
( ~ s__subclass(X0,s__ColdBloodedVertebrate)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[],[f69696,f62032]) ).
fof(f69719,plain,
! [X0] :
( ~ s__subclass(X0,s__ColdBloodedVertebrate)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f69705,f62034]) ).
fof(f69720,plain,
! [X0] :
( ~ s__subclass(X0,s__ColdBloodedVertebrate)
| ~ s__instance(s__Organism5_1,X0) ),
inference(forward_subsumption_resolution,[],[f69719,f62033]) ).
fof(f70028,plain,
~ s__instance(s__Organism5_1,s__Reptile),
inference(resolution,[],[f69720,f62068]) ).
fof(f70039,plain,
! [X0] :
( ~ s__subclass(X0,s__Reptile)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__instance(s__Reptile,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[],[f70028,f62032]) ).
fof(f70053,plain,
! [X0] :
( ~ s__subclass(X0,s__Reptile)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__instance(s__Reptile,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f70039,f62034]) ).
fof(f70054,plain,
! [X0] :
( ~ s__subclass(X0,s__Reptile)
| ~ s__instance(s__Organism5_1,X0) ),
inference(forward_subsumption_resolution,[],[f70053,f62033]) ).
fof(f70519,plain,
~ s__instance(s__Organism5_1,s__Class5_10),
inference(resolution,[],[f70054,f62022]) ).
fof(f70582,plain,
! [X0] :
( ~ s__subclass(X0,s__Class5_10)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__instance(s__Class5_10,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[],[f70519,f62032]) ).
fof(f70596,plain,
! [X0] :
( ~ s__subclass(X0,s__Class5_10)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__instance(s__Class5_10,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f70582,f62034]) ).
fof(f70597,plain,
! [X0] :
( ~ s__subclass(X0,s__Class5_10)
| ~ s__instance(s__Organism5_1,X0) ),
inference(forward_subsumption_resolution,[],[f70596,f62033]) ).
fof(f71280,plain,
~ s__instance(s__Organism5_1,s__Lizard5_1),
inference(resolution,[],[f70597,f69228]) ).
fof(f71281,plain,
$false,
inference(forward_subsumption_resolution,[],[f71280,f61991]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR079+6 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 % Computer : n002.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Mon Sep 28 22:31:38 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.25 Running first-order theorem proving
% 0.08/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.65/4.91 % (855617)Detected formulas, will run a generic FOF schedule.
% 23.65/4.91 % (855647)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2881950732:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 23.65/4.91 % (855642)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=3588884577:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 23.65/4.91 % (855644)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=3884821956:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 23.65/4.91 % (855647)Instruction limit reached!
% 23.65/4.91 % (855647)------------------------------
% 23.65/4.91 % (855647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.65/4.91 % (855647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.65/4.91 % (855647)CaDiCaL version: 2.1.3
% 23.65/4.91 % (855647)Termination reason: Instruction limit
% 23.65/4.91 % (855647)Termination phase: Property scanning
% 23.65/4.91 % (855647)Time elapsed: 0.076 s
% 23.65/4.91 % (855647)Peak memory usage: 138 MB
% 23.65/4.91 % (855647)Instructions burned: 141 (million)
% 23.65/4.91 % (855645)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2095387992:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 23.65/4.91 % (855643)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=849845083:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 23.65/4.91 % (855648)dis-21_1_sil=8000:lcm=predicate:random_seed=2043638367:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 23.65/4.91 % (855646)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1076814771:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 23.65/4.91 % (855645)Instruction limit reached!
% 23.65/4.91 % (855645)------------------------------
% 23.65/4.91 % (855645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.65/4.91 % (855645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.65/4.91 % (855645)CaDiCaL version: 2.1.3
% 23.65/4.91 % (855645)Termination reason: Instruction limit
% 23.65/4.91 % (855645)Termination phase: SInE selection
% 23.65/4.91 % (855645)Time elapsed: 0.103 s
% 23.65/4.91 % (855645)Peak memory usage: 138 MB
% 23.65/4.91 % (855645)Instructions burned: 110 (million)
% 23.65/4.91 % (855646)Instruction limit reached!
% 23.65/4.91 % (855646)------------------------------
% 23.65/4.91 % (855646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.65/4.91 % (855646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.65/4.91 % (855646)CaDiCaL version: 2.1.3
% 23.65/4.91 % (855646)Termination reason: Instruction limit
% 23.65/4.91 % (855646)Termination phase: SInE selection
% 23.65/4.91 % (855646)Time elapsed: 0.109 s
% 23.65/4.91 % (855646)Peak memory usage: 139 MB
% 23.65/4.91 % (855646)Instructions burned: 119 (million)
% 23.65/4.91 % (855648)Instruction limit reached!
% 23.65/4.91 % (855648)------------------------------
% 23.65/4.91 % (855648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.65/4.91 % (855648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.65/4.91 % (855648)CaDiCaL version: 2.1.3
% 23.65/4.91 % (855648)Termination reason: Instruction limit
% 23.65/4.91 % (855648)Termination phase: SInE selection
% 23.65/4.91 % (855648)Time elapsed: 0.113 s
% 23.65/4.91 % (855648)Peak memory usage: 139 MB
% 23.65/4.91 % (855648)Instructions burned: 129 (million)
% 23.65/4.91 % (855655)lrs+10_1_sil=8000:sp=occurrence:random_seed=1912320992:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 23.65/4.91 % (855655)Refutation not found, incomplete strategy
% 23.65/4.91 % (855655)------------------------------
% 23.65/4.91 % (855655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.65/4.91 % (855655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.65/4.91 % (855655)CaDiCaL version: 2.1.3
% 23.65/4.91 % (855655)Termination reason: Refutation not found, incomplete strategy
% 23.65/4.91 % (855655)Time elapsed: 0.140 s
% 23.65/4.91 % (855655)Peak memory usage: 143 MB
% 23.65/4.91 % (855655)Instructions burned: 204 (million)
% 23.65/4.91 % (855659)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1542102945:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/157Mi)
% 31.93/6.12 % (855661)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=763842766:s2a=on:i=248:s2at=1.23:gtg=position_2985 on theBenchmark for (2985ds/248Mi)
% 31.93/6.12 % (855660)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2102865129:i=325:sd=1:ss=axioms:sgt=32_2985 on theBenchmark for (2985ds/325Mi)
% 31.93/6.12 % (855659)Instruction limit reached!
% 31.93/6.12 % (855659)------------------------------
% 31.93/6.12 % (855659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/6.12 % (855659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/6.12 % (855659)CaDiCaL version: 2.1.3
% 31.93/6.12 % (855659)Termination reason: Instruction limit
% 31.93/6.12 % (855659)Termination phase: Property scanning
% 31.93/6.12 % (855659)Time elapsed: 0.153 s
% 31.93/6.12 % (855659)Peak memory usage: 138 MB
% 31.93/6.12 % (855659)Instructions burned: 157 (million)
% 31.93/6.12 % (855655)------------------------------
% 31.93/6.12 % (855655)------------------------------
% 31.93/6.12 % (855661)Instruction limit reached!
% 31.93/6.12 % (855661)------------------------------
% 31.93/6.12 % (855661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/6.12 % (855661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/6.12 % (855661)CaDiCaL version: 2.1.3
% 31.93/6.12 % (855661)Termination reason: Instruction limit
% 31.93/6.12 % (855661)Termination phase: Property scanning
% 31.93/6.12 % (855661)Time elapsed: 0.217 s
% 31.93/6.12 % (855661)Peak memory usage: 138 MB
% 31.93/6.12 % (855661)Instructions burned: 249 (million)
% 31.93/6.12 % (855660)Refutation not found, incomplete strategy
% 31.93/6.12 % (855660)------------------------------
% 31.93/6.12 % (855660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/6.12 % (855660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/6.12 % (855660)CaDiCaL version: 2.1.3
% 31.93/6.12 % (855660)Termination reason: Refutation not found, incomplete strategy
% 31.93/6.12 % (855660)Time elapsed: 0.229 s
% 31.93/6.12 % (855660)Peak memory usage: 144 MB
% 31.93/6.12 % (855660)Instructions burned: 201 (million)
% 31.93/6.12 % (855666)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3191822017:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2981 on theBenchmark for (2981ds/294Mi)
% 31.93/6.12 % (855668)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=585668519:cts=off:i=113:fsr=off:ss=included:sgt=4_2980 on theBenchmark for (2980ds/113Mi)
% 31.93/6.12 % (855667)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3632985813:i=2350_2981 on theBenchmark for (2981ds/2350Mi)
% 31.93/6.12 % (855668)Instruction limit reached!
% 31.93/6.12 % (855668)------------------------------
% 31.93/6.12 % (855668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/6.12 % (855668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/6.12 % (855668)CaDiCaL version: 2.1.3
% 31.93/6.12 % (855668)Termination reason: Instruction limit
% 31.93/6.12 % (855668)Termination phase: SInE selection
% 31.93/6.12 % (855668)Time elapsed: 0.067 s
% 31.93/6.12 % (855668)Peak memory usage: 139 MB
% 31.93/6.12 % (855668)Instructions burned: 113 (million)
% 31.93/6.12 % (855666)Instruction limit reached!
% 31.93/6.12 % (855666)------------------------------
% 31.93/6.12 % (855666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/6.12 % (855666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/6.12 % (855666)CaDiCaL version: 2.1.3
% 31.93/6.12 % (855666)Termination reason: Instruction limit
% 31.93/6.12 % (855666)Termination phase: Saturation
% 31.93/6.12 % (855666)Time elapsed: 0.263 s
% 31.93/6.12 % (855666)Peak memory usage: 142 MB
% 31.93/6.12 % (855666)Instructions burned: 296 (million)
% 31.93/6.12 % (855672)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3773450014:i=127:av=off:fsr=off:sup=off_2978 on theBenchmark for (2978ds/127Mi)
% 31.93/6.12 % (855660)------------------------------
% 31.93/6.12 % (855660)------------------------------
% 31.93/6.12 % (855672)Instruction limit reached!
% 31.93/6.12 % (855672)------------------------------
% 31.93/6.12 % (855672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/6.12 % (855672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855672)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855672)Termination reason: Instruction limit
% 21.38/11.00 % (855672)Termination phase: Preprocessing 1
% 21.38/11.00 % (855672)Time elapsed: 0.080 s
% 21.38/11.00 % (855672)Peak memory usage: 138 MB
% 21.38/11.00 % (855672)Instructions burned: 127 (million)
% 21.38/11.00 % (855673)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1508864467:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2977 on theBenchmark for (2977ds/114Mi)
% 21.38/11.00 % (855673)Instruction limit reached!
% 21.38/11.00 % (855673)------------------------------
% 21.38/11.00 % (855673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855673)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855673)Termination reason: Instruction limit
% 21.38/11.00 % (855673)Termination phase: Property scanning
% 21.38/11.00 % (855673)Time elapsed: 0.065 s
% 21.38/11.00 % (855673)Peak memory usage: 138 MB
% 21.38/11.00 % (855673)Instructions burned: 114 (million)
% 21.38/11.00 % (855675)lrs+10_1_sil=8000:sp=occurrence:random_seed=1674709712:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2976 on theBenchmark for (2976ds/907Mi)
% 21.38/11.00 % (855676)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3566362708:i=437:sd=1:aac=none:ss=included_2976 on theBenchmark for (2976ds/437Mi)
% 21.38/11.00 % (855678)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1924578472:i=5202:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/5202Mi)
% 21.38/11.00 % (855675)Refutation not found, incomplete strategy
% 21.38/11.00 % (855675)------------------------------
% 21.38/11.00 % (855675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855675)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855675)Termination reason: Refutation not found, incomplete strategy
% 21.38/11.00 % (855675)Time elapsed: 0.274 s
% 21.38/11.00 % (855675)Peak memory usage: 144 MB
% 21.38/11.00 % (855675)Instructions burned: 255 (million)
% 21.38/11.00 % (855676)Instruction limit reached!
% 21.38/11.00 % (855676)------------------------------
% 21.38/11.00 % (855676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855676)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855676)Termination reason: Instruction limit
% 21.38/11.00 % (855676)Termination phase: Saturation
% 21.38/11.00 % (855676)Time elapsed: 0.392 s
% 21.38/11.00 % (855676)Peak memory usage: 143 MB
% 21.38/11.00 % (855676)Instructions burned: 438 (million)
% 21.38/11.00 % (855686)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2810742311:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2969 on theBenchmark for (2969ds/134Mi)
% 21.38/11.00 % (855675)------------------------------
% 21.38/11.00 % (855675)------------------------------
% 21.38/11.00 % (855686)Instruction limit reached!
% 21.38/11.00 % (855686)------------------------------
% 21.38/11.00 % (855686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855686)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855686)Termination reason: Instruction limit
% 21.38/11.00 % (855686)Termination phase: SInE selection
% 21.38/11.00 % (855686)Time elapsed: 0.132 s
% 21.38/11.00 % (855686)Peak memory usage: 139 MB
% 21.38/11.00 % (855686)Instructions burned: 134 (million)
% 21.38/11.00 % (855688)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1037959362:st=8:i=592:sd=3:ep=RST:ss=axioms_2967 on theBenchmark for (2967ds/592Mi)
% 21.38/11.00 % (855690)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4072375524:st=3:i=13193:sd=3:ss=axioms_2966 on theBenchmark for (2966ds/13193Mi)
% 21.38/11.00 % (855688)Instruction limit reached!
% 21.38/11.00 % (855688)------------------------------
% 21.38/11.00 % (855688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855688)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855688)Termination reason: Instruction limit
% 21.38/11.00 % (855688)Termination phase: Saturation
% 21.38/11.00 % (855688)Time elapsed: 0.579 s
% 21.38/11.00 % (855688)Peak memory usage: 148 MB
% 21.38/11.00 % (855688)Instructions burned: 592 (million)
% 21.38/11.00 % (855694)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=3589210749:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2959 on theBenchmark for (2959ds/125Mi)
% 21.38/11.00 % (855694)Instruction limit reached!
% 21.38/11.00 % (855694)------------------------------
% 21.38/11.00 % (855694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855694)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855694)Termination reason: Instruction limit
% 21.38/11.00 % (855694)Termination phase: Property scanning
% 21.38/11.00 % (855694)Time elapsed: 0.126 s
% 21.38/11.00 % (855694)Peak memory usage: 138 MB
% 21.38/11.00 % (855694)Instructions burned: 126 (million)
% 21.38/11.00 % (855702)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3935116027:i=134:gtgl=5:slsql=off:gtg=exists_sym_2955 on theBenchmark for (2955ds/134Mi)
% 21.38/11.00 % (855667)Instruction limit reached!
% 21.38/11.00 % (855667)------------------------------
% 21.38/11.00 % (855667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855667)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855667)Termination reason: Instruction limit
% 21.38/11.00 % (855667)Termination phase: Saturation
% 21.38/11.00 % (855667)Time elapsed: 2.484 s
% 21.38/11.00 % (855667)Peak memory usage: 246 MB
% 21.38/11.00 % (855667)Instructions burned: 2353 (million)
% 21.38/11.00 % (855702)Instruction limit reached!
% 21.38/11.00 % (855702)------------------------------
% 21.38/11.00 % (855702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855702)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855702)Termination reason: Instruction limit
% 21.38/11.00 % (855702)Termination phase: Property scanning
% 21.38/11.00 % (855702)Time elapsed: 0.076 s
% 21.38/11.00 % (855702)Peak memory usage: 138 MB
% 21.38/11.00 % (855702)Instructions burned: 134 (million)
% 21.38/11.00 % (855704)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1870545338:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2953 on theBenchmark for (2953ds/141Mi)
% 21.38/11.00 % (855705)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1461089948:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2953 on theBenchmark for (2953ds/431Mi)
% 21.38/11.00 % (855704)Instruction limit reached!
% 21.38/11.00 % (855704)------------------------------
% 21.38/11.00 % (855704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855704)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855704)Termination reason: Instruction limit
% 21.38/11.00 % (855704)Termination phase: SInE selection
% 21.38/11.00 % (855704)Time elapsed: 0.135 s
% 21.38/11.00 % (855704)Peak memory usage: 139 MB
% 21.38/11.00 % (855704)Instructions burned: 141 (million)
% 21.38/11.00 % (855705)Refutation not found, incomplete strategy
% 21.38/11.00 % (855705)------------------------------
% 21.38/11.00 % (855705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855705)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855705)Termination reason: Refutation not found, incomplete strategy
% 21.38/11.00 % (855705)Time elapsed: 0.142 s
% 21.38/11.00 % (855705)Peak memory usage: 143 MB
% 21.38/11.00 % (855705)Instructions burned: 201 (million)
% 21.38/11.00 % (855705)------------------------------
% 21.38/11.00 % (855705)------------------------------
% 21.38/11.00 % (855708)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=2664832658:i=6060:aac=none:ins=25_2950 on theBenchmark for (2950ds/6060Mi)
% 21.38/11.00 % (855712)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=817730103:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2947 on theBenchmark for (2947ds/150Mi)
% 21.38/11.00 % (855712)Instruction limit reached!
% 21.38/11.00 % (855712)------------------------------
% 21.38/11.00 % (855712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855712)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855712)Termination reason: Instruction limit
% 21.38/11.00 % (855712)Termination phase: SInE selection
% 21.38/11.00 % (855712)Time elapsed: 0.099 s
% 21.38/11.00 % (855712)Peak memory usage: 139 MB
% 21.38/11.00 % (855712)Instructions burned: 150 (million)
% 21.38/11.00 % (855714)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1098134359:i=14155:bd=all_2944 on theBenchmark for (2944ds/14155Mi)
% 21.38/11.00 % (855678)Instruction limit reached!
% 21.38/11.00 % (855678)------------------------------
% 21.38/11.00 % (855678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855678)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855678)Termination reason: Instruction limit
% 21.38/11.00 % (855678)Termination phase: Saturation
% 21.38/11.00 % (855678)Time elapsed: 4.216 s
% 21.38/11.00 % (855678)Peak memory usage: 394 MB
% 21.38/11.00 % (855678)Instructions burned: 5203 (million)
% 21.38/11.00 % (855718)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3926187857:i=667:av=off:fsr=off_2930 on theBenchmark for (2930ds/667Mi)
% 21.38/11.00 % (855718)Instruction limit reached!
% 21.38/11.00 % (855718)------------------------------
% 21.38/11.00 % (855718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855718)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855718)Termination reason: Instruction limit
% 21.38/11.00 % (855718)Termination phase: NewCNF
% 21.38/11.00 % (855718)Time elapsed: 0.776 s
% 21.38/11.00 % (855718)Peak memory usage: 162 MB
% 21.38/11.00 % (855718)Instructions burned: 667 (million)
% 21.38/11.00 % (855722)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=1415090097:s2a=on:i=185:s2at=1.8:fdi=4_2920 on theBenchmark for (2920ds/185Mi)
% 21.38/11.00 % (855722)Instruction limit reached!
% 21.38/11.00 % (855722)------------------------------
% 21.38/11.00 % (855722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855722)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855722)Termination reason: Instruction limit
% 21.38/11.00 % (855722)Termination phase: SInE selection
% 21.38/11.00 % (855722)Time elapsed: 0.171 s
% 21.38/11.00 % (855722)Peak memory usage: 139 MB
% 21.38/11.00 % (855722)Instructions burned: 185 (million)
% 21.38/11.00 % (855728)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=480786691:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2916 on theBenchmark for (2916ds/193Mi)
% 21.38/11.00 % (855728)Instruction limit reached!
% 21.38/11.00 % (855728)------------------------------
% 21.38/11.00 % (855728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/11.00 % (855728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/11.00 % (855728)CaDiCaL version: 2.1.3
% 21.38/11.00 % (855728)Termination reason: Instruction limit
% 21.38/11.00 % (855728)Termination phase: SInE selection
% 21.38/11.00 % (855728)Time elapsed: 0.191 s
% 21.38/11.00 % (855728)Peak memory usage: 139 MB
% 21.38/11.00 % (855728)Instructions burned: 194 (million)
% 21.38/11.00 % (855730)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=743758123:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2912 on theBenchmark for (2912ds/4850Mi)
% 21.38/11.00 % (855730)First to succeed.
% 21.38/11.00 % (855730)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-855617"
% 21.38/11.00 % (855730)Refutation found. Thanks to Tanya!
% 21.38/11.00 % SZS status Theorem for theBenchmark
% 21.38/11.00 % SZS output start Proof for theBenchmark
% See solution above
% 66.74/11.28 % (855730)------------------------------
% 66.74/11.28 % (855730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.74/11.28 % (855730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.74/11.28 % (855730)CaDiCaL version: 2.1.3
% 66.74/11.28 % (855730)Termination reason: Refutation
% 66.74/11.28 % (855730)Time elapsed: 0.832 s
% 66.74/11.28 % (855730)Peak memory usage: 152 MB
% 66.74/11.28 % (855730)Instructions burned: 771 (million)
% 66.74/11.28 % (855730)------------------------------
% 66.74/11.28 % (855730)------------------------------
% 66.74/11.28 % (855617)Success in time 10.391 s
% 66.74/11.28 % Vampire exiting
%------------------------------------------------------------------------------