%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR086+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:45:05 AM UTC 2026
% Result : Theorem 173.43s 27.17s
% Output : Refutation 173.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 6
% Syntax : Number of formulae : 32 ( 13 unt; 0 def)
% Number of atoms : 77 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 79 ( 34 ~; 33 |; 6 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-1 aty)
% Number of variables : 45 ( 41 !; 4 ?)
% 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/Axioms/CSR003+2.ax',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/Axioms/CSR003+2.ax',kb_SUMO_26636) ).
fof(f32515,axiom,
s__subclass(s__GraphLoop,s__GraphArc),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_32707) ).
fof(f32518,axiom,
! [X0] :
( s__instance(X0,s__GraphArc)
=> ( s__instance(X0,s__GraphLoop)
<=> ? [X1] :
( s__instance(X1,s__GraphNode)
& s__links(X1,X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_32710) ).
fof(f145102,axiom,
s__instance(s__Arc13_1,s__GraphLoop),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_1) ).
fof(f145103,conjecture,
? [X0] : s__links(X0,X0,s__Arc13_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(f145104,negated_conjecture,
~ ? [X0] : s__links(X0,X0,s__Arc13_1),
inference(negated_conjecture,[status(cth)],[f145103]) ).
fof(f154463,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26456]) ).
fof(f154464,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(f154465,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,[],[f154464]) ).
fof(f162832,plain,
! [X0] :
( ( s__instance(X0,s__GraphLoop)
<=> ? [X1] :
( s__instance(X1,s__GraphNode)
& s__links(X1,X1,X0) ) )
| ~ s__instance(X0,s__GraphArc) ),
inference(ennf_transformation,[],[f32518]) ).
fof(f168504,plain,
! [X0] : ~ s__links(X0,X0,s__Arc13_1),
inference(ennf_transformation,[],[f145104]) ).
fof(f191274,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f154463]) ).
fof(f191275,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f154463]) ).
fof(f191276,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| s__instance(X2,X1) ),
inference(cnf_transformation,[],[f154465]) ).
fof(f197613,plain,
s__subclass(s__GraphLoop,s__GraphArc),
inference(cnf_transformation,[],[f32515]) ).
fof(f197616,plain,
! [X0] :
( ~ s__instance(X0,s__GraphArc)
| s__links(sK1025(X0),sK1025(X0),X0)
| ~ s__instance(X0,s__GraphLoop) ),
inference(cnf_transformation,[],[f162832]) ).
fof(f315067,plain,
s__instance(s__Arc13_1,s__GraphLoop),
inference(cnf_transformation,[],[f145102]) ).
fof(f315068,plain,
! [X0] : ~ s__links(X0,X0,s__Arc13_1),
inference(cnf_transformation,[],[f168504]) ).
fof(f330691,plain,
! [X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(consistent_polarity_flipping,[],[f191275]) ).
fof(f330692,plain,
! [X0,X1] :
( ~ s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(consistent_polarity_flipping,[],[f191274]) ).
fof(f330693,plain,
! [X2,X0,X1] :
( s__instance(X0,s__SetOrClass)
| s__instance(X1,s__SetOrClass)
| s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X1) ),
inference(consistent_polarity_flipping,[],[f191276]) ).
fof(f336415,plain,
! [X0] :
( ~ s__links(sK1025(X0),sK1025(X0),X0)
| s__instance(X0,s__GraphArc)
| s__instance(X0,s__GraphLoop) ),
inference(consistent_polarity_flipping,[],[f197616]) ).
fof(f400142,plain,
~ s__instance(s__Arc13_1,s__GraphLoop),
inference(consistent_polarity_flipping,[],[f315067]) ).
fof(f400143,plain,
! [X0] : s__links(X0,X0,s__Arc13_1),
inference(consistent_polarity_flipping,[],[f315068]) ).
fof(f1199038,plain,
( s__instance(s__Arc13_1,s__GraphArc)
| s__instance(s__Arc13_1,s__GraphLoop) ),
inference(resolution,[],[f336415,f400143]) ).
fof(f1199039,plain,
s__instance(s__Arc13_1,s__GraphArc),
inference(forward_subsumption_resolution,[],[f1199038,f400142]) ).
fof(f1287491,plain,
! [X2,X0,X1] :
( s__instance(X1,s__SetOrClass)
| s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X1) ),
inference(forward_subsumption_resolution,[],[f330693,f330691]) ).
fof(f1287492,plain,
! [X2,X0,X1] :
( ~ s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f1287491,f330692]) ).
fof(f1290593,plain,
! [X0] :
( ~ s__subclass(X0,s__GraphArc)
| s__instance(s__Arc13_1,X0) ),
inference(resolution,[],[f1287492,f1199039]) ).
fof(f1290655,plain,
s__instance(s__Arc13_1,s__GraphLoop),
inference(resolution,[],[f1290593,f197613]) ).
fof(f1290656,plain,
$false,
inference(forward_subsumption_resolution,[],[f1290655,f400142]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR086+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n014.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 22:36:32 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.69/5.56 % (2262826)Will run a generic schedule for satisfiability detection.
% 20.69/5.56 % (2262832)% WARNING: option uhcvi not known.
% 20.69/5.56 % (2262831)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3230398062_2973 on theBenchmark for (2973ds/0Mi)
% 20.69/5.56 % (2262832)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=731518667:i=135531:add=off:rawr=on_2973 on theBenchmark for (2973ds/135531Mi)
% 20.69/5.56 % (2262833)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=859200761:i=88024:add=on:rawr=on_2973 on theBenchmark for (2973ds/88024Mi)
% 20.69/5.56 % (2262834)dis+10_1_sil=32000:sp=arity:random_seed=4017051107:i=103:fgj=on_2973 on theBenchmark for (2973ds/103Mi)
% 20.69/5.56 % (2262838)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2298260322:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2973 on theBenchmark for (2973ds/159Mi)
% 20.69/5.56 % (2262835)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1030726700:i=116_2973 on theBenchmark for (2973ds/116Mi)
% 20.69/5.56 % (2262836)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1205747817:i=131_2973 on theBenchmark for (2973ds/131Mi)
% 20.69/5.56 % (2262838)Instruction limit reached!
% 20.69/5.56 % (2262838)------------------------------
% 20.69/5.56 % (2262838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.69/5.56 % (2262838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.69/5.56 % (2262838)CaDiCaL version: 2.1.3
% 20.69/5.56 % (2262838)Termination reason: Instruction limit
% 20.69/5.56 % (2262838)Termination phase: Preprocessing 1
% 20.69/5.56 % (2262838)Time elapsed: 0.062 s
% 20.69/5.56 % (2262838)Peak memory usage: 155 MB
% 20.69/5.56 % (2262838)Instructions burned: 159 (million)
% 20.69/5.56 % (2262834)Instruction limit reached!
% 20.69/5.56 % (2262834)------------------------------
% 20.69/5.56 % (2262834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.69/5.56 % (2262834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.69/5.56 % (2262834)CaDiCaL version: 2.1.3
% 20.69/5.56 % (2262834)Termination reason: Instruction limit
% 20.69/5.56 % (2262834)Termination phase: Preprocessing 1
% 20.69/5.56 % (2262834)Time elapsed: 0.065 s
% 20.69/5.56 % (2262834)Peak memory usage: 155 MB
% 20.69/5.56 % (2262834)Instructions burned: 103 (million)
% 20.69/5.56 % (2262835)Instruction limit reached!
% 20.69/5.56 % (2262835)------------------------------
% 20.69/5.56 % (2262835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.69/5.56 % (2262835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.69/5.56 % (2262845)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1358213302:i=714:nm=2_2971 on theBenchmark for (2971ds/714Mi)
% 20.69/5.56 % (2262835)CaDiCaL version: 2.1.3
% 20.69/5.56 % (2262835)Termination reason: Instruction limit
% 20.69/5.56 % (2262835)Termination phase: Preprocessing 1
% 20.69/5.56 % (2262835)Time elapsed: 0.084 s
% 20.69/5.56 % (2262835)Peak memory usage: 155 MB
% 20.69/5.56 % (2262835)Instructions burned: 116 (million)
% 20.69/5.56 % (2262836)Instruction limit reached!
% 20.69/5.56 % (2262836)------------------------------
% 20.69/5.56 % (2262836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.69/5.56 % (2262836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.69/5.56 % (2262836)CaDiCaL version: 2.1.3
% 20.69/5.56 % (2262836)Termination reason: Instruction limit
% 20.69/5.56 % (2262836)Termination phase: Preprocessing 1
% 20.69/5.56 % (2262836)Time elapsed: 0.090 s
% 20.69/5.56 % (2262836)Peak memory usage: 155 MB
% 20.69/5.56 % (2262836)Instructions burned: 132 (million)
% 20.69/5.56 % (2262846)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1552638440:i=131:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/131Mi)
% 20.69/5.56 % (2262849)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1536516411:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2971 on theBenchmark for (2971ds/684Mi)
% 20.69/5.56 % (2262850)ott-21_1_sil=16000:fs=off:random_seed=481948006:i=180:av=off:fsr=off_2971 on theBenchmark for (2971ds/180Mi)
% 20.69/5.56 % (2262846)Instruction limit reached!
% 20.69/5.56 % (2262846)------------------------------
% 20.69/5.56 % (2262846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.69/5.56 % (2262846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.49/9.81 % (2262846)CaDiCaL version: 2.1.3
% 51.49/9.81 % (2262846)Termination reason: Instruction limit
% 51.49/9.81 % (2262846)Termination phase: Preprocessing 1
% 51.49/9.81 % (2262846)Time elapsed: 0.086 s
% 51.49/9.81 % (2262846)Peak memory usage: 155 MB
% 51.49/9.81 % (2262846)Instructions burned: 131 (million)
% 51.49/9.81 % (2262853)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2045075258:i=477:bd=all_2970 on theBenchmark for (2970ds/477Mi)
% 51.49/9.81 % (2262850)Instruction limit reached!
% 51.49/9.81 % (2262850)------------------------------
% 51.49/9.81 % (2262850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.49/9.81 % (2262850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.49/9.81 % (2262850)CaDiCaL version: 2.1.3
% 51.49/9.81 % (2262850)Termination reason: Instruction limit
% 51.49/9.81 % (2262850)Termination phase: Preprocessing 1
% 51.49/9.81 % (2262850)Time elapsed: 0.120 s
% 51.49/9.81 % (2262850)Peak memory usage: 155 MB
% 51.49/9.81 % (2262850)Instructions burned: 181 (million)
% 51.49/9.81 % (2262855)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=850170502:fmbsr=1.3:i=865:ins=25_2970 on theBenchmark for (2970ds/865Mi)
% 51.49/9.81 % (2262845)Instruction limit reached!
% 51.49/9.81 % (2262845)------------------------------
% 51.49/9.81 % (2262845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.49/9.81 % (2262845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.49/9.81 % (2262845)CaDiCaL version: 2.1.3
% 51.49/9.81 % (2262845)Termination reason: Instruction limit
% 51.49/9.81 % (2262845)Termination phase: Unused predicate definition removal
% 51.49/9.81 % (2262845)Time elapsed: 0.241 s
% 51.49/9.81 % (2262845)Peak memory usage: 189 MB
% 51.49/9.81 % (2262845)Instructions burned: 715 (million)
% 51.49/9.81 % (2262857)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1295965380:i=1179_2969 on theBenchmark for (2969ds/1179Mi)
% 51.49/9.81 % (2262849)Instruction limit reached!
% 51.49/9.81 % (2262849)------------------------------
% 51.49/9.81 % (2262849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.49/9.81 % (2262849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.49/9.81 % (2262849)CaDiCaL version: 2.1.3
% 51.49/9.81 % (2262849)Termination reason: Instruction limit
% 51.49/9.81 % (2262849)Termination phase: Preprocessing 1
% 51.49/9.81 % (2262849)Time elapsed: 0.380 s
% 51.49/9.81 % (2262849)Peak memory usage: 158 MB
% 51.49/9.81 % (2262849)Instructions burned: 684 (million)
% 51.49/9.81 % (2262859)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1655544355:i=889:ins=1_2967 on theBenchmark for (2967ds/889Mi)
% 51.49/9.81 % (2262853)Instruction limit reached!
% 51.49/9.81 % (2262853)------------------------------
% 51.49/9.81 % (2262853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.49/9.81 % (2262853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.49/9.81 % (2262853)CaDiCaL version: 2.1.3
% 51.49/9.81 % (2262853)Termination reason: Instruction limit
% 51.49/9.81 % (2262853)Termination phase: Naming
% 51.49/9.81 % (2262853)Time elapsed: 0.363 s
% 51.49/9.81 % (2262853)Peak memory usage: 164 MB
% 51.49/9.81 % (2262853)Instructions burned: 478 (million)
% 51.49/9.81 % (2262861)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2998984126:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2966 on theBenchmark for (2966ds/692Mi)
% 51.49/9.81 % (2262857)Instruction limit reached!
% 51.49/9.81 % (2262857)------------------------------
% 51.49/9.81 % (2262857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.49/9.81 % (2262857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.49/9.81 % (2262857)CaDiCaL version: 2.1.3
% 51.49/9.81 % (2262857)Termination reason: Instruction limit
% 51.49/9.81 % (2262857)Termination phase: Property scanning
% 51.49/9.81 % (2262857)Time elapsed: 0.421 s
% 51.49/9.81 % (2262857)Peak memory usage: 185 MB
% 51.49/9.81 % (2262857)Instructions burned: 1179 (million)
% 51.49/9.81 % (2262855)Instruction limit reached!
% 51.49/9.81 % (2262855)------------------------------
% 51.49/9.81 % (2262855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.49/9.81 % (2262855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.49/9.81 % (2262855)CaDiCaL version: 2.1.3
% 51.49/9.81 % (2262855)Termination reason: Instruction limit
% 51.49/9.81 % (2262855)Termination phase: Preprocessing 2
% 82.23/14.15 % (2262855)Time elapsed: 0.518 s
% 82.23/14.15 % (2262855)Peak memory usage: 203 MB
% 82.23/14.15 % (2262855)Instructions burned: 866 (million)
% 82.23/14.15 % (2262863)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=893887713:i=879:kws=inv_precedence:fsr=off_2964 on theBenchmark for (2964ds/879Mi)
% 82.23/14.15 % (2262865)fmb+10_1_sil=64000:random_seed=4188697540:i=22061:nm=2:gsp=on_2964 on theBenchmark for (2964ds/22061Mi)
% 82.23/14.15 % (2262861)Instruction limit reached!
% 82.23/14.15 % (2262861)------------------------------
% 82.23/14.15 % (2262861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.23/14.15 % (2262861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.23/14.15 % (2262861)CaDiCaL version: 2.1.3
% 82.23/14.15 % (2262861)Termination reason: Instruction limit
% 82.23/14.15 % (2262861)Termination phase: Preprocessing 1
% 82.23/14.15 % (2262861)Time elapsed: 0.386 s
% 82.23/14.15 % (2262861)Peak memory usage: 158 MB
% 82.23/14.15 % (2262861)Instructions burned: 692 (million)
% 82.23/14.15 % (2262867)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1992388488:i=9515:nm=5_2962 on theBenchmark for (2962ds/9515Mi)
% 82.23/14.15 % (2262859)Instruction limit reached!
% 82.23/14.15 % (2262859)------------------------------
% 82.23/14.15 % (2262859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.23/14.15 % (2262859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.23/14.15 % (2262859)CaDiCaL version: 2.1.3
% 82.23/14.15 % (2262859)Termination reason: Instruction limit
% 82.23/14.15 % (2262859)Termination phase: Preprocessing 2
% 82.23/14.15 % (2262859)Time elapsed: 0.544 s
% 82.23/14.15 % (2262859)Peak memory usage: 194 MB
% 82.23/14.15 % (2262859)Instructions burned: 890 (million)
% 82.23/14.15 % (2262863)Instruction limit reached!
% 82.23/14.15 % (2262863)------------------------------
% 82.23/14.15 % (2262863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.23/14.15 % (2262863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.23/14.15 % (2262863)CaDiCaL version: 2.1.3
% 82.23/14.15 % (2262863)Termination reason: Instruction limit
% 82.23/14.15 % (2262863)Termination phase: NewCNF
% 82.23/14.15 % (2262863)Time elapsed: 0.309 s
% 82.23/14.15 % (2262863)Peak memory usage: 178 MB
% 82.23/14.15 % (2262863)Instructions burned: 886 (million)
% 82.23/14.15 % (2262869)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=378148007:fmbsr=1.7:i=920_2961 on theBenchmark for (2961ds/920Mi)
% 82.23/14.15 % (2262871)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=448339764:i=5131_2961 on theBenchmark for (2961ds/5131Mi)
% 82.23/14.15 % (2262869)Instruction limit reached!
% 82.23/14.15 % (2262869)------------------------------
% 82.23/14.15 % (2262869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.23/14.15 % (2262869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.23/14.15 % (2262869)CaDiCaL version: 2.1.3
% 82.23/14.15 % (2262869)Termination reason: Instruction limit
% 82.23/14.15 % (2262869)Termination phase: Preprocessing 2
% 82.23/14.15 % (2262869)Time elapsed: 0.567 s
% 82.23/14.15 % (2262869)Peak memory usage: 197 MB
% 82.23/14.15 % (2262869)Instructions burned: 922 (million)
% 82.23/14.15 % (2262873)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2002673969:i=1472:ins=7:fdi=8:gsp=on_2955 on theBenchmark for (2955ds/1472Mi)
% 82.23/14.15 % (2262871)Instruction limit reached!
% 82.23/14.15 % (2262871)------------------------------
% 82.23/14.15 % (2262871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.23/14.15 % (2262871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.23/14.15 % (2262871)CaDiCaL version: 2.1.3
% 82.23/14.15 % (2262871)Termination reason: Instruction limit
% 82.23/14.15 % (2262871)Termination phase: Saturation
% 82.23/14.15 % (2262871)Time elapsed: 1.098 s
% 82.23/14.15 % (2262871)Peak memory usage: 200 MB
% 82.23/14.15 % (2262871)Instructions burned: 5131 (million)
% 82.23/14.15 % (2262875)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1236275890:i=6324_2950 on theBenchmark for (2950ds/6324Mi)
% 82.23/14.15 % (2262873)Instruction limit reached!
% 82.23/14.15 % (2262873)------------------------------
% 82.23/14.15 % (2262873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.23/14.15 % (2262873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.23/14.15 % (2262873)CaDiCaL version: 2.1.3
% 82.23/14.15 % (2262873)Termination reason: Instruction limit
% 82.23/14.15 % (2262873)Termination phase: Property scanning
% 128.15/20.79 % (2262873)Time elapsed: 0.859 s
% 128.15/20.79 % (2262873)Peak memory usage: 185 MB
% 128.15/20.79 % (2262873)Instructions burned: 1473 (million)
% 128.15/20.79 % (2262877)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4151775719:fmbsr=2.30978:i=2174_2946 on theBenchmark for (2946ds/2174Mi)
% 128.15/20.79 % (2262877)Instruction limit reached!
% 128.15/20.79 % (2262877)------------------------------
% 128.15/20.79 % (2262877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.15/20.79 % (2262877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.15/20.79 % (2262877)CaDiCaL version: 2.1.3
% 128.15/20.79 % (2262877)Termination reason: Instruction limit
% 128.15/20.79 % (2262877)Termination phase: Property scanning
% 128.15/20.79 % (2262877)Time elapsed: 1.154 s
% 128.15/20.79 % (2262877)Peak memory usage: 241 MB
% 128.15/20.79 % (2262877)Instructions burned: 2176 (million)
% 128.15/20.79 % (2262879)ott-2_1_sil=16000:newcnf=on:random_seed=3550255472:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2934 on theBenchmark for (2934ds/869Mi)
% 128.15/20.79 % (2262875)Instruction limit reached!
% 128.15/20.79 % (2262875)------------------------------
% 128.15/20.79 % (2262875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.15/20.79 % (2262875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.15/20.79 % (2262875)CaDiCaL version: 2.1.3
% 128.15/20.79 % (2262875)Termination reason: Instruction limit
% 128.15/20.79 % (2262875)Termination phase: Property scanning
% 128.15/20.79 % (2262875)Time elapsed: 1.908 s
% 128.15/20.79 % (2262875)Peak memory usage: 298 MB
% 128.15/20.79 % (2262875)Instructions burned: 6326 (million)
% 128.15/20.79 % (2262881)ott+10_1_sil=32000:tgt=ground:random_seed=2243084290:i=5114:av=off_2930 on theBenchmark for (2930ds/5114Mi)
% 128.15/20.79 % (2262879)Instruction limit reached!
% 128.15/20.79 % (2262879)------------------------------
% 128.15/20.79 % (2262879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.15/20.79 % (2262879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.15/20.79 % (2262879)CaDiCaL version: 2.1.3
% 128.15/20.79 % (2262879)Termination reason: Instruction limit
% 128.15/20.79 % (2262879)Termination phase: NewCNF
% 128.15/20.79 % (2262879)Time elapsed: 0.528 s
% 128.15/20.79 % (2262879)Peak memory usage: 178 MB
% 128.15/20.79 % (2262879)Instructions burned: 869 (million)
% 128.15/20.79 % (2262883)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2634559916:i=54282_2928 on theBenchmark for (2928ds/54282Mi)
% 128.15/20.79 % (2262867)Instruction limit reached!
% 128.15/20.79 % (2262867)------------------------------
% 128.15/20.79 % (2262867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.15/20.79 % (2262867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.15/20.79 % (2262867)CaDiCaL version: 2.1.3
% 128.15/20.79 % (2262867)Termination reason: Instruction limit
% 128.15/20.79 % (2262867)Termination phase: Finite model building preprocessing
% 128.15/20.79 % (2262867)Time elapsed: 4.571 s
% 128.15/20.79 % (2262867)Peak memory usage: 341 MB
% 128.15/20.79 % (2262867)Instructions burned: 9516 (million)
% 128.15/20.79 % (2262885)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2835070497:i=3512:aac=none_2916 on theBenchmark for (2916ds/3512Mi)
% 128.15/20.79 % (2262881)Instruction limit reached!
% 128.15/20.79 % (2262881)------------------------------
% 128.15/20.79 % (2262881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.15/20.79 % (2262881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.15/20.79 % (2262881)CaDiCaL version: 2.1.3
% 128.15/20.79 % (2262881)Termination reason: Instruction limit
% 128.15/20.79 % (2262881)Termination phase: Saturation
% 128.15/20.79 % (2262881)Time elapsed: 1.536 s
% 128.15/20.79 % (2262881)Peak memory usage: 248 MB
% 128.15/20.79 % (2262881)Instructions burned: 5114 (million)
% 128.15/20.79 % (2262887)dis+21_1_sil=32000:sas=cadical:random_seed=2581654188:i=3773:amm=off_2915 on theBenchmark for (2915ds/3773Mi)
% 128.15/20.79 % (2262887)Instruction limit reached!
% 128.15/20.79 % (2262887)------------------------------
% 128.15/20.79 % (2262887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.15/20.79 % (2262887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.15/20.79 % (2262887)CaDiCaL version: 2.1.3
% 128.15/20.79 % (2262887)Termination reason: Instruction limit
% 128.15/20.79 % (2262887)Termination phase: Saturation
% 128.15/20.79 % (2262887)Time elapsed: 1.069 s
% 128.15/20.79 % (2262887)Peak memory usage: 211 MB
% 128.15/20.79 % (2262887)Instructions burned: 3776 (million)
% 165.73/25.97 % (2262889)ott+11_1_sil=16000:gs=on:random_seed=3244074689:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2904 on theBenchmark for (2904ds/2251Mi)
% 165.73/25.97 % Detected minimum model sizes of [617]
% 165.73/25.97 % Detected maximum model sizes of [max]
% 165.73/25.97 % (2262865)Cannot represent all propositional literals internally
% 165.73/25.97 % (2262865)Refutation not found, incomplete strategy
% 165.73/25.97 % (2262865)------------------------------
% 165.73/25.97 % (2262865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.73/25.97 % (2262865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.73/25.97 % (2262865)CaDiCaL version: 2.1.3
% 165.73/25.97 % (2262865)Termination reason: Refutation not found, incomplete strategy
% 165.73/25.97 % (2262865)Time elapsed: 6.417 s
% 165.73/25.97 % (2262865)Peak memory usage: 388 MB
% 165.73/25.97 % (2262865)Instructions burned: 13610 (million)
% 165.73/25.97 % (2262865)------------------------------
% 165.73/25.97 % (2262865)------------------------------
% 165.73/25.97 % (2262885)Instruction limit reached!
% 165.73/25.97 % (2262885)------------------------------
% 165.73/25.97 % (2262885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.73/25.97 % (2262885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.73/25.97 % (2262885)CaDiCaL version: 2.1.3
% 165.73/25.97 % (2262885)Termination reason: Instruction limit
% 165.73/25.97 % (2262885)Termination phase: Saturation
% 165.73/25.97 % (2262885)Time elapsed: 1.858 s
% 165.73/25.97 % (2262885)Peak memory usage: 204 MB
% 165.73/25.97 % (2262885)Instructions burned: 3513 (million)
% 165.73/25.97 % (2262891)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3509786994:fmbsr=1.6:i=67534_2897 on theBenchmark for (2897ds/67534Mi)
% 165.73/25.97 % (2262892)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3336809535:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2896 on theBenchmark for (2896ds/4591Mi)
% 165.73/25.97 % (2262889)Instruction limit reached!
% 165.73/25.97 % (2262889)------------------------------
% 165.73/25.97 % (2262889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.73/25.97 % (2262889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.73/25.97 % (2262889)CaDiCaL version: 2.1.3
% 165.73/25.97 % (2262889)Termination reason: Instruction limit
% 165.73/25.97 % (2262889)Termination phase: Property scanning
% 165.73/25.97 % (2262889)Time elapsed: 0.735 s
% 165.73/25.97 % (2262889)Peak memory usage: 188 MB
% 165.73/25.97 % (2262889)Instructions burned: 2256 (million)
% 165.73/25.97 % (2262895)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1199709262:i=29340_2896 on theBenchmark for (2896ds/29340Mi)
% 165.73/25.97 % Detected minimum model sizes of [617]
% 165.73/25.97 % Detected maximum model sizes of [max]
% 165.73/25.97 % (2262831)Cannot represent all propositional literals internally
% 165.73/25.97 % (2262831)Refutation not found, incomplete strategy
% 165.73/25.97 % (2262831)------------------------------
% 165.73/25.97 % (2262831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.73/25.97 % (2262831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.73/25.97 % (2262831)CaDiCaL version: 2.1.3
% 165.73/25.97 % (2262831)Termination reason: Refutation not found, incomplete strategy
% 165.73/25.97 % (2262831)Time elapsed: 8.357 s
% 165.73/25.97 % (2262831)Peak memory usage: 464 MB
% 165.73/25.97 % (2262831)Instructions burned: 17167 (million)
% 165.73/25.97 % (2262831)------------------------------
% 165.73/25.97 % (2262831)------------------------------
% 165.73/25.97 % (2262897)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=155489333:i=5211_2886 on theBenchmark for (2886ds/5211Mi)
% 165.73/25.97 % (2262892)Instruction limit reached!
% 165.73/25.97 % (2262892)------------------------------
% 165.73/25.97 % (2262892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.73/25.97 % (2262892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.73/25.97 % (2262892)CaDiCaL version: 2.1.3
% 165.73/25.97 % (2262892)Termination reason: Instruction limit
% 165.73/25.97 % (2262892)Termination phase: Saturation
% 165.73/25.97 % (2262892)Time elapsed: 2.505 s
% 165.73/25.97 % (2262892)Peak memory usage: 238 MB
% 165.73/25.97 % (2262892)Instructions burned: 4592 (million)
% 165.73/25.97 % (2262899)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1507613065:i=5497:nm=2_2871 on theBenchmark for (2871ds/5497Mi)
% 165.73/25.97 % (2262897)Instruction limit reached!
% 165.73/25.97 % (2262897)------------------------------
% 165.73/25.97 % (2262897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.60/26.98 % (2262897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.60/26.98 % (2262897)CaDiCaL version: 2.1.3
% 148.60/26.98 % (2262897)Termination reason: Instruction limit
% 148.60/26.98 % (2262897)Termination phase: Saturation
% 148.60/26.98 % (2262897)Time elapsed: 2.516 s
% 148.60/26.98 % (2262897)Peak memory usage: 238 MB
% 148.60/26.98 % (2262897)Instructions burned: 5211 (million)
% 148.60/26.98 % (2262901)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1831096596:fmbsr=2:i=46332_2860 on theBenchmark for (2860ds/46332Mi)
% 148.60/26.98 % Detected minimum model sizes of [617]
% 148.60/26.98 % Detected maximum model sizes of [max]
% 148.60/26.98 % (2262883)Cannot represent all propositional literals internally
% 148.60/26.98 % (2262883)Refutation not found, incomplete strategy
% 148.60/26.98 % (2262883)------------------------------
% 148.60/26.98 % (2262883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.60/26.98 % (2262883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.60/26.98 % (2262883)CaDiCaL version: 2.1.3
% 148.60/26.98 % (2262883)Termination reason: Refutation not found, incomplete strategy
% 148.60/26.98 % (2262883)Time elapsed: 8.353 s
% 148.60/26.98 % (2262883)Peak memory usage: 464 MB
% 148.60/26.98 % (2262883)Instructions burned: 17157 (million)
% 148.60/26.98 % (2262883)------------------------------
% 148.60/26.98 % (2262883)------------------------------
% 148.60/26.98 % (2262903)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1266624548:i=14071_2842 on theBenchmark for (2842ds/14071Mi)
% 148.60/26.98 % (2262899)Instruction limit reached!
% 148.60/26.98 % (2262899)------------------------------
% 148.60/26.98 % (2262899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.60/26.98 % (2262899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.60/26.98 % (2262899)CaDiCaL version: 2.1.3
% 148.60/26.98 % (2262899)Termination reason: Instruction limit
% 148.60/26.98 % (2262899)Termination phase: Property scanning
% 148.60/26.98 % (2262899)Time elapsed: 3.040 s
% 148.60/26.98 % (2262899)Peak memory usage: 301 MB
% 148.60/26.98 % (2262899)Instructions burned: 5498 (million)
% 148.60/26.98 % (2262905)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3328352437:i=22565:add=on:rawr=on_2840 on theBenchmark for (2840ds/22565Mi)
% 148.60/26.98 % Detected minimum model sizes of [617]
% 148.60/26.98 % Detected maximum model sizes of [max]
% 148.60/26.98 % (2262891)Cannot represent all propositional literals internally
% 148.60/26.98 % (2262891)Refutation not found, incomplete strategy
% 148.60/26.98 % (2262891)------------------------------
% 148.60/26.98 % (2262891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.60/26.98 % (2262891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.60/26.98 % (2262891)CaDiCaL version: 2.1.3
% 148.60/26.98 % (2262891)Termination reason: Refutation not found, incomplete strategy
% 148.60/26.98 % (2262891)Time elapsed: 7.246 s
% 148.60/26.98 % (2262891)Peak memory usage: 415 MB
% 148.60/26.98 % (2262891)Instructions burned: 15708 (million)
% 148.60/26.98 % (2262891)------------------------------
% 148.60/26.98 % (2262891)------------------------------
% 148.60/26.98 % (2262908)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3420022851:i=8173:av=off_2821 on theBenchmark for (2821ds/8173Mi)
% 148.60/26.98 % (2262895)Instruction limit reached!
% 148.60/26.98 % (2262895)------------------------------
% 148.60/26.98 % (2262895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.60/26.98 % (2262895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.60/26.98 % (2262895)CaDiCaL version: 2.1.3
% 148.60/26.98 % (2262895)Termination reason: Instruction limit
% 148.60/26.98 % (2262895)Termination phase: Saturation
% 148.60/26.98 % (2262895)Time elapsed: 9.360 s
% 148.60/26.98 % (2262895)Peak memory usage: 942 MB
% 148.60/26.98 % (2262895)Instructions burned: 29346 (million)
% 148.60/26.98 % (2262910)dis+10_16:1_sil=16000:random_seed=3730914746:i=9155:fsr=off_2802 on theBenchmark for (2802ds/9155Mi)
% 148.60/26.98 % (2262908)Instruction limit reached!
% 148.60/26.98 % (2262908)------------------------------
% 148.60/26.98 % (2262908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.60/26.98 % (2262908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.60/26.98 % (2262908)CaDiCaL version: 2.1.3
% 148.60/26.98 % (2262908)Termination reason: Instruction limit
% 148.60/26.98 % (2262908)Termination phase: Saturation
% 148.60/26.98 % (2262908)Time elapsed: 2.667 s
% 173.43/27.17 % (2262908)Peak memory usage: 197 MB
% 173.43/27.17 % (2262908)Instructions burned: 8175 (million)
% 173.43/27.17 % (2262912)ott-3_8_sil=64000:random_seed=3630316825:i=20139:bs=on_2794 on theBenchmark for (2794ds/20139Mi)
% 173.43/27.17 % Detected minimum model sizes of [617]
% 173.43/27.17 % Detected maximum model sizes of [max]
% 173.43/27.17 % (2262901)Cannot represent all propositional literals internally
% 173.43/27.17 % (2262901)Refutation not found, incomplete strategy
% 173.43/27.17 % (2262901)------------------------------
% 173.43/27.17 % (2262901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 173.43/27.17 % (2262901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.43/27.17 % (2262901)CaDiCaL version: 2.1.3
% 173.43/27.17 % (2262901)Termination reason: Refutation not found, incomplete strategy
% 173.43/27.17 % (2262901)Time elapsed: 7.309 s
% 173.43/27.17 % (2262901)Peak memory usage: 415 MB
% 173.43/27.17 % (2262901)Instructions burned: 15709 (million)
% 173.43/27.17 % (2262901)------------------------------
% 173.43/27.17 % (2262901)------------------------------
% 173.43/27.17 % (2262914)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2253931084:fmbsr=2:i=32576_2784 on theBenchmark for (2784ds/32576Mi)
% 173.43/27.17 % (2262905)Instruction limit reached!
% 173.43/27.17 % (2262905)------------------------------
% 173.43/27.17 % (2262905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 173.43/27.17 % (2262905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.43/27.17 % (2262905)CaDiCaL version: 2.1.3
% 173.43/27.17 % (2262905)Termination reason: Instruction limit
% 173.43/27.17 % (2262905)Termination phase: Saturation
% 173.43/27.17 % (2262905)Time elapsed: 6.258 s
% 173.43/27.17 % (2262905)Peak memory usage: 196 MB
% 173.43/27.17 % (2262905)Instructions burned: 22568 (million)
% 173.43/27.17 % (2262916)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=291723209:i=11404_2777 on theBenchmark for (2777ds/11404Mi)
% 173.43/27.17 % (2262903)Instruction limit reached!
% 173.43/27.17 % (2262903)------------------------------
% 173.43/27.17 % (2262903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 173.43/27.17 % (2262903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.43/27.17 % (2262903)CaDiCaL version: 2.1.3
% 173.43/27.17 % (2262903)Termination reason: Instruction limit
% 173.43/27.17 % (2262903)Termination phase: Finite model building preprocessing
% 173.43/27.17 % (2262903)Time elapsed: 6.509 s
% 173.43/27.17 % (2262903)Peak memory usage: 391 MB
% 173.43/27.17 % (2262903)Instructions burned: 14073 (million)
% 173.43/27.17 % (2262918)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1740052171:i=14134_2776 on theBenchmark for (2776ds/14134Mi)
% 173.43/27.17 % (2262910)Instruction limit reached!
% 173.43/27.17 % (2262910)------------------------------
% 173.43/27.17 % (2262910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 173.43/27.17 % (2262910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.43/27.17 % (2262910)CaDiCaL version: 2.1.3
% 173.43/27.17 % (2262910)Termination reason: Instruction limit
% 173.43/27.17 % (2262910)Termination phase: Saturation
% 173.43/27.17 % (2262910)Time elapsed: 2.672 s
% 173.43/27.17 % (2262910)Peak memory usage: 297 MB
% 173.43/27.17 % (2262910)Instructions burned: 9160 (million)
% 173.43/27.17 % (2262920)dis+33_16_sil=32000:sac=on:random_seed=3501302440:i=15851:nm=0_2774 on theBenchmark for (2774ds/15851Mi)
% 173.43/27.17 % (2262833)Instruction limit reached!
% 173.43/27.17 % (2262833)------------------------------
% 173.43/27.17 % (2262833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 173.43/27.17 % (2262833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.43/27.17 % (2262833)CaDiCaL version: 2.1.3
% 173.43/27.17 % (2262833)Termination reason: Instruction limit
% 173.43/27.17 % (2262833)Termination phase: Saturation
% 173.43/27.17 % (2262833)Time elapsed: 21.986 s
% 173.43/27.17 % (2262833)Peak memory usage: 205 MB
% 173.43/27.17 % (2262833)Instructions burned: 88026 (million)
% 173.43/27.17 % (2262922)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3488941396:avsq=on:i=17627:add=on:amm=off_2752 on theBenchmark for (2752ds/17627Mi)
% 173.43/27.17 % (2262916)Instruction limit reached!
% 173.43/27.17 % (2262916)------------------------------
% 173.43/27.17 % (2262916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 173.43/27.17 % (2262916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.43/27.17 % (2262916)CaDiCaL version: 2.1.3
% 173.43/27.17 % (2262916)Termination reason: Instruction limit
% 173.43/27.17 % (2262916)Termination phase: Saturation
% 173.43/27.17 % (2262916)Time elapsed: 3.445 s
% 173.43/27.17 % (2262916)Peak memory usage: 199 MB
% 173.43/27.17 % (2262916)Instructions burned: 11406 (million)
% 173.43/27.17 % (2262924)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1647532869:s2a=on:i=53295_2742 on theBenchmark for (2742ds/53295Mi)
% 173.43/27.17 % (2262832) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2262826-2262832"...
% 173.43/27.17 % (2262832)...printing done.
% 173.43/27.17 % (2262832)Refutation found. Thanks to Tanya!
% 173.43/27.17 % SZS status Theorem for theBenchmark
% 173.43/27.17 % SZS output start Proof for theBenchmark
% See solution above
% 173.43/27.17 % (2262832)------------------------------
% 173.43/27.17 % (2262832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 173.43/27.17 % (2262832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.43/27.17 % (2262832)CaDiCaL version: 2.1.3
% 173.43/27.17 % (2262832)Termination reason: Refutation
% 173.43/27.17 % (2262832)Time elapsed: 23.654 s
% 173.43/27.17 % (2262832)Peak memory usage: 518 MB
% 173.43/27.17 % (2262832)Instructions burned: 48873 (million)
% 173.43/27.17 % (2262826)Success in time 26.742 s
% 173.43/27.17 % Vampire exiting
%------------------------------------------------------------------------------