%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV317^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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 : Wed Sep 30 08:38:15 AM UTC 2026
% Result : Theorem 57.27s 8.66s
% Output : Refutation 57.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV317^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.26 % Computer : n001.cluster.edu
% 0.10/0.26 % Model : x86_64 x86_64
% 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.26 % Memory : 8046.5625MB
% 0.10/0.26 % OS : Linux 6.8.0-71-generic
% 0.10/0.26 % CPULimit : 300
% 0.10/0.26 % WCLimit : 300
% 0.10/0.26 % DateTime : Tue Sep 29 15:40:21 UTC 2026
% 0.10/0.27 % CPUTime :
% 0.10/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.32 Running higher-order theorem proving
% 0.24/0.34 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.07/0.53 % (1390572)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.07/0.53 % (1390581)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1563253390:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 1.07/0.53 % (1390583)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.07/0.53 % (1390583)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.07/0.53 % (1390579)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4112222518:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 1.07/0.53 % (1390578)lrs+10_16_si=on:nwc=1.5:random_seed=997277388:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 1.07/0.53 % (1390580)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=4176554036:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 1.07/0.53 % (1390581)Instruction limit reached!
% 1.07/0.53 % (1390581)------------------------------
% 1.07/0.53 % (1390581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.53 % (1390581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.53 % (1390581)CaDiCaL version: 2.1.3
% 1.07/0.53 % (1390581)Termination reason: Instruction limit
% 1.07/0.53 % (1390581)Termination phase: Saturation
% 1.07/0.53 % (1390581)Time elapsed: 0.013 s
% 1.07/0.53 % (1390581)Peak memory usage: 12 MB
% 1.07/0.53 % (1390581)Instructions burned: 26 (million)
% 1.07/0.53 % (1390582)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3124474316:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 1.07/0.53 % (1390583)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=1364972375:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 1.07/0.53 % (1390577)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1345147294:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 1.07/0.53 % (1390579)Instruction limit reached!
% 1.07/0.53 % (1390579)------------------------------
% 1.07/0.53 % (1390579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.53 % (1390579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.53 % (1390579)CaDiCaL version: 2.1.3
% 1.07/0.53 % (1390579)Termination reason: Instruction limit
% 1.07/0.53 % (1390579)Termination phase: Saturation
% 1.07/0.53 % (1390579)Time elapsed: 0.004 s
% 1.07/0.53 % (1390579)Peak memory usage: 12 MB
% 1.07/0.53 % (1390579)Instructions burned: 3 (million)
% 1.07/0.53 % (1390578)Instruction limit reached!
% 1.07/0.53 % (1390578)------------------------------
% 1.07/0.53 % (1390578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.53 % (1390578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.53 % (1390578)CaDiCaL version: 2.1.3
% 1.07/0.53 % (1390578)Termination reason: Instruction limit
% 1.07/0.53 % (1390578)Termination phase: Saturation
% 1.07/0.53 % (1390578)Time elapsed: 0.018 s
% 1.07/0.53 % (1390578)Peak memory usage: 12 MB
% 1.07/0.53 % (1390578)Instructions burned: 18 (million)
% 1.07/0.53 % (1390590)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=114593616:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.07/0.53 % (1390592)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1532318128:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.07/0.53 % (1390590)Instruction limit reached!
% 1.07/0.53 % (1390590)------------------------------
% 1.07/0.53 % (1390590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.53 % (1390590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.53 % (1390590)CaDiCaL version: 2.1.3
% 1.07/0.53 % (1390590)Termination reason: Instruction limit
% 1.07/0.53 % (1390590)Termination phase: Saturation
% 1.07/0.53 % (1390590)Time elapsed: 0.002 s
% 1.07/0.53 % (1390590)Peak memory usage: 12 MB
% 1.07/0.53 % (1390590)Instructions burned: 2 (million)
% 1.79/0.60 % (1390592)Instruction limit reached!
% 1.79/0.60 % (1390592)------------------------------
% 1.79/0.60 % (1390592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.79/0.60 % (1390592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.79/0.60 % (1390592)CaDiCaL version: 2.1.3
% 1.79/0.60 % (1390592)Termination reason: Instruction limit
% 1.79/0.60 % (1390592)Termination phase: Saturation
% 1.79/0.60 % (1390592)Time elapsed: 0.003 s
% 1.79/0.60 % (1390592)Peak memory usage: 12 MB
% 1.79/0.60 % (1390592)Instructions burned: 6 (million)
% 1.79/0.60 % (1390597)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.79/0.60 % (1390597)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.79/0.60 % (1390597)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3171033558:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.79/0.60 % (1390593)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.79/0.60 % (1390596)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3893793562:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.79/0.60 % (1390593)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2678423229:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.79/0.60 % (1390596)Instruction limit reached!
% 1.79/0.60 % (1390596)------------------------------
% 1.79/0.60 % (1390596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.79/0.60 % (1390596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.79/0.60 % (1390596)CaDiCaL version: 2.1.3
% 1.79/0.60 % (1390596)Termination reason: Instruction limit
% 1.79/0.60 % (1390596)Termination phase: Saturation
% 1.79/0.60 % (1390596)Time elapsed: 0.008 s
% 1.79/0.60 % (1390596)Peak memory usage: 12 MB
% 1.79/0.60 % (1390596)Instructions burned: 12 (million)
% 1.79/0.60 % (1390593)Instruction limit reached!
% 1.79/0.60 % (1390593)------------------------------
% 1.79/0.60 % (1390593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.79/0.60 % (1390593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.79/0.60 % (1390593)CaDiCaL version: 2.1.3
% 1.79/0.60 % (1390593)Termination reason: Instruction limit
% 1.79/0.60 % (1390593)Termination phase: Saturation
% 1.79/0.60 % (1390593)Time elapsed: 0.009 s
% 1.79/0.60 % (1390593)Peak memory usage: 12 MB
% 1.79/0.60 % (1390593)Instructions burned: 10 (million)
% 1.79/0.60 % (1390597)Instruction limit reached!
% 1.79/0.60 % (1390597)------------------------------
% 1.79/0.60 % (1390597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.79/0.60 % (1390597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.79/0.60 % (1390597)CaDiCaL version: 2.1.3
% 1.79/0.60 % (1390597)Termination reason: Instruction limit
% 1.79/0.60 % (1390597)Termination phase: Saturation
% 1.79/0.60 % (1390597)Time elapsed: 0.016 s
% 1.79/0.60 % (1390597)Peak memory usage: 12 MB
% 1.79/0.60 % (1390597)Instructions burned: 35 (million)
% 1.79/0.60 % (1390582)Instruction limit reached!
% 1.79/0.60 % (1390582)------------------------------
% 1.79/0.60 % (1390582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.79/0.60 % (1390582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.79/0.60 % (1390582)CaDiCaL version: 2.1.3
% 1.79/0.60 % (1390582)Termination reason: Instruction limit
% 1.79/0.60 % (1390582)Termination phase: Saturation
% 1.79/0.60 % (1390582)Time elapsed: 0.068 s
% 1.79/0.60 % (1390582)Peak memory usage: 12 MB
% 1.79/0.60 % (1390582)Instructions burned: 75 (million)
% 1.79/0.60 % (1390602)lrs+10_1_si=on:cs=on:random_seed=2214027600:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.79/0.60 % (1390577)Instruction limit reached!
% 1.79/0.60 % (1390577)------------------------------
% 1.79/0.60 % (1390577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.79/0.60 % (1390577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.66 % (1390577)CaDiCaL version: 2.1.3
% 2.11/0.66 % (1390577)Termination reason: Instruction limit
% 2.11/0.66 % (1390577)Termination phase: Saturation
% 2.11/0.66 % (1390577)Time elapsed: 0.079 s
% 2.11/0.66 % (1390577)Peak memory usage: 12 MB
% 2.11/0.66 % (1390577)Instructions burned: 87 (million)
% 2.11/0.66 % (1390602)Instruction limit reached!
% 2.11/0.66 % (1390602)------------------------------
% 2.11/0.66 % (1390602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.66 % (1390602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.66 % (1390602)CaDiCaL version: 2.1.3
% 2.11/0.66 % (1390602)Termination reason: Instruction limit
% 2.11/0.66 % (1390602)Termination phase: Saturation
% 2.11/0.66 % (1390602)Time elapsed: 0.006 s
% 2.11/0.66 % (1390602)Peak memory usage: 12 MB
% 2.11/0.66 % (1390602)Instructions burned: 10 (million)
% 2.11/0.66 % (1390603)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 2.11/0.66 % (1390601)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=3705884339:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 2.11/0.66 % (1390603)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=3360483842:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 2.11/0.66 % (1390603)Instruction limit reached!
% 2.11/0.66 % (1390603)------------------------------
% 2.11/0.66 % (1390603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.66 % (1390603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.66 % (1390603)CaDiCaL version: 2.1.3
% 2.11/0.66 % (1390603)Termination reason: Instruction limit
% 2.11/0.66 % (1390603)Termination phase: Saturation
% 2.11/0.66 % (1390603)Time elapsed: 0.002 s
% 2.11/0.66 % (1390603)Peak memory usage: 11 MB
% 2.11/0.66 % (1390603)Instructions burned: 2 (million)
% 2.11/0.66 % (1390604)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=810620012:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 2.11/0.66 % (1390607)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3384428322:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 2.11/0.66 % (1390606)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1514333336:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 2.11/0.66 % (1390607)Instruction limit reached!
% 2.11/0.66 % (1390607)------------------------------
% 2.11/0.66 % (1390607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.66 % (1390607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.66 % (1390607)CaDiCaL version: 2.1.3
% 2.11/0.66 % (1390607)Termination reason: Instruction limit
% 2.11/0.66 % (1390607)Termination phase: Saturation
% 2.11/0.66 % (1390607)Time elapsed: 0.013 s
% 2.11/0.66 % (1390607)Peak memory usage: 12 MB
% 2.11/0.66 % (1390607)Instructions burned: 27 (million)
% 2.11/0.66 % (1390610)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=989721330:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.11/0.66 % (1390583)Instruction limit reached!
% 2.11/0.66 % (1390583)------------------------------
% 2.11/0.66 % (1390583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.66 % (1390583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.66 % (1390583)CaDiCaL version: 2.1.3
% 2.11/0.66 % (1390583)Termination reason: Instruction limit
% 2.11/0.66 % (1390583)Termination phase: Saturation
% 2.11/0.66 % (1390583)Time elapsed: 0.137 s
% 2.11/0.66 % (1390583)Peak memory usage: 12 MB
% 2.11/0.66 % (1390583)Instructions burned: 157 (million)
% 2.11/0.66 % (1390604)Instruction limit reached!
% 2.11/0.66 % (1390604)------------------------------
% 2.11/0.66 % (1390604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.66 % (1390604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.66 % (1390604)CaDiCaL version: 2.1.3
% 2.11/0.66 % (1390604)Termination reason: Instruction limit
% 2.11/0.66 % (1390604)Termination phase: Saturation
% 2.11/0.66 % (1390604)Time elapsed: 0.035 s
% 2.53/0.75 % (1390604)Peak memory usage: 12 MB
% 2.53/0.75 % (1390604)Instructions burned: 38 (million)
% 2.53/0.75 % (1390614)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1700267534:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.53/0.75 % (1390610)Instruction limit reached!
% 2.53/0.75 % (1390610)------------------------------
% 2.53/0.75 % (1390610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.53/0.75 % (1390610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.53/0.75 % (1390610)CaDiCaL version: 2.1.3
% 2.53/0.75 % (1390610)Termination reason: Instruction limit
% 2.53/0.75 % (1390610)Termination phase: Saturation
% 2.53/0.75 % (1390610)Time elapsed: 0.015 s
% 2.53/0.75 % (1390610)Peak memory usage: 12 MB
% 2.53/0.75 % (1390610)Instructions burned: 15 (million)
% 2.53/0.75 % (1390619)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2280959296:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.53/0.75 % (1390618)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1267534723:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.53/0.75 % (1390616)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2596583396:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.53/0.75 % (1390601)Instruction limit reached!
% 2.53/0.75 % (1390601)------------------------------
% 2.53/0.75 % (1390601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.53/0.75 % (1390601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.53/0.75 % (1390601)CaDiCaL version: 2.1.3
% 2.53/0.75 % (1390601)Termination reason: Instruction limit
% 2.53/0.75 % (1390601)Termination phase: Saturation
% 2.53/0.75 % (1390601)Time elapsed: 0.078 s
% 2.53/0.75 % (1390601)Peak memory usage: 12 MB
% 2.53/0.75 % (1390601)Instructions burned: 86 (million)
% 2.53/0.75 % (1390618)Instruction limit reached!
% 2.53/0.75 % (1390618)------------------------------
% 2.53/0.75 % (1390618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.53/0.75 % (1390618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.53/0.75 % (1390618)CaDiCaL version: 2.1.3
% 2.53/0.75 % (1390618)Termination reason: Instruction limit
% 2.53/0.75 % (1390618)Termination phase: Saturation
% 2.53/0.75 % (1390618)Time elapsed: 0.003 s
% 2.53/0.75 % (1390618)Peak memory usage: 12 MB
% 2.53/0.75 % (1390618)Instructions burned: 2 (million)
% 2.53/0.75 % (1390619)Instruction limit reached!
% 2.53/0.75 % (1390619)------------------------------
% 2.53/0.75 % (1390619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.53/0.75 % (1390619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.53/0.75 % (1390619)CaDiCaL version: 2.1.3
% 2.53/0.75 % (1390619)Termination reason: Instruction limit
% 2.53/0.75 % (1390619)Termination phase: Saturation
% 2.53/0.75 % (1390619)Time elapsed: 0.015 s
% 2.53/0.75 % (1390619)Peak memory usage: 12 MB
% 2.53/0.75 % (1390619)Instructions burned: 32 (million)
% 2.53/0.75 % (1390616)Instruction limit reached!
% 2.53/0.75 % (1390616)------------------------------
% 2.53/0.75 % (1390616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.53/0.75 % (1390616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.53/0.75 % (1390616)CaDiCaL version: 2.1.3
% 2.53/0.75 % (1390616)Termination reason: Instruction limit
% 2.53/0.75 % (1390616)Termination phase: Saturation
% 2.53/0.75 % (1390616)Time elapsed: 0.014 s
% 2.53/0.75 % (1390616)Peak memory usage: 12 MB
% 2.53/0.75 % (1390616)Instructions burned: 14 (million)
% 2.53/0.75 % (1390626)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.53/0.75 % (1390626)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.53/0.75 % (1390626)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=1646656516:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.53/0.75 % (1390625)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3249409231:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.83/0.84 % (1390624)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=211616820:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.83/0.84 % (1390626)Instruction limit reached!
% 2.83/0.84 % (1390626)------------------------------
% 2.83/0.84 % (1390626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.84 % (1390626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.84 % (1390626)CaDiCaL version: 2.1.3
% 2.83/0.84 % (1390626)Termination reason: Instruction limit
% 2.83/0.84 % (1390626)Termination phase: Saturation
% 2.83/0.84 % (1390626)Time elapsed: 0.008 s
% 2.83/0.84 % (1390626)Peak memory usage: 12 MB
% 2.83/0.84 % (1390626)Instructions burned: 16 (million)
% 2.83/0.84 % (1390627)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.83/0.84 % (1390627)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=1569356128:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.83/0.84 % (1390627)Instruction limit reached!
% 2.83/0.84 % (1390627)------------------------------
% 2.83/0.84 % (1390627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.84 % (1390627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.84 % (1390627)CaDiCaL version: 2.1.3
% 2.83/0.84 % (1390627)Termination reason: Instruction limit
% 2.83/0.84 % (1390627)Termination phase: Saturation
% 2.83/0.84 % (1390627)Time elapsed: 0.009 s
% 2.83/0.84 % (1390627)Peak memory usage: 11 MB
% 2.83/0.84 % (1390627)Instructions burned: 8 (million)
% 2.83/0.84 % (1390631)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=4041602354:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.83/0.84 % (1390624)Instruction limit reached!
% 2.83/0.84 % (1390624)------------------------------
% 2.83/0.84 % (1390624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.84 % (1390624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.84 % (1390624)CaDiCaL version: 2.1.3
% 2.83/0.84 % (1390624)Termination reason: Instruction limit
% 2.83/0.84 % (1390624)Termination phase: Saturation
% 2.83/0.84 % (1390624)Time elapsed: 0.023 s
% 2.83/0.84 % (1390624)Peak memory usage: 12 MB
% 2.83/0.84 % (1390624)Instructions burned: 23 (million)
% 2.83/0.84 % (1390631)Instruction limit reached!
% 2.83/0.84 % (1390631)------------------------------
% 2.83/0.84 % (1390631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.84 % (1390631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.84 % (1390631)CaDiCaL version: 2.1.3
% 2.83/0.84 % (1390631)Termination reason: Instruction limit
% 2.83/0.84 % (1390631)Termination phase: Saturation
% 2.83/0.84 % (1390631)Time elapsed: 0.018 s
% 2.83/0.84 % (1390631)Peak memory usage: 12 MB
% 2.83/0.84 % (1390631)Instructions burned: 32 (million)
% 2.83/0.84 % (1390634)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1973947994:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.83/0.84 % (1390625)Instruction limit reached!
% 2.83/0.84 % (1390625)------------------------------
% 2.83/0.84 % (1390625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.84 % (1390625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.84 % (1390625)CaDiCaL version: 2.1.3
% 2.83/0.84 % (1390625)Termination reason: Instruction limit
% 2.83/0.84 % (1390625)Termination phase: Saturation
% 2.83/0.84 % (1390625)Time elapsed: 0.055 s
% 2.83/0.84 % (1390625)Peak memory usage: 12 MB
% 2.83/0.84 % (1390625)Instructions burned: 62 (million)
% 2.83/0.84 % (1390636)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3520644728:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.83/0.84 % (1390634)Instruction limit reached!
% 2.83/0.84 % (1390634)------------------------------
% 2.83/0.84 % (1390634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.84 % (1390634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.84 % (1390634)CaDiCaL version: 2.1.3
% 3.57/0.93 % (1390634)Termination reason: Instruction limit
% 3.57/0.93 % (1390634)Termination phase: Saturation
% 3.57/0.93 % (1390634)Time elapsed: 0.008 s
% 3.57/0.93 % (1390634)Peak memory usage: 12 MB
% 3.57/0.93 % (1390634)Instructions burned: 7 (million)
% 3.57/0.93 % (1390637)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3414953348:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 3.57/0.93 % (1390636)Instruction limit reached!
% 3.57/0.93 % (1390636)------------------------------
% 3.57/0.93 % (1390636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.57/0.93 % (1390636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.57/0.93 % (1390636)CaDiCaL version: 2.1.3
% 3.57/0.93 % (1390636)Termination reason: Instruction limit
% 3.57/0.93 % (1390636)Termination phase: Saturation
% 3.57/0.93 % (1390636)Time elapsed: 0.019 s
% 3.57/0.93 % (1390636)Peak memory usage: 11 MB
% 3.57/0.93 % (1390636)Instructions burned: 24 (million)
% 3.57/0.93 % (1390637)Instruction limit reached!
% 3.57/0.93 % (1390637)------------------------------
% 3.57/0.93 % (1390637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.57/0.93 % (1390637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.57/0.93 % (1390637)CaDiCaL version: 2.1.3
% 3.57/0.93 % (1390637)Termination reason: Instruction limit
% 3.57/0.93 % (1390637)Termination phase: Saturation
% 3.57/0.93 % (1390637)Time elapsed: 0.013 s
% 3.57/0.93 % (1390637)Peak memory usage: 12 MB
% 3.57/0.93 % (1390637)Instructions burned: 20 (million)
% 3.57/0.93 % (1390639)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=968968771:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 3.57/0.93 % (1390641)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3125412691:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 3.57/0.93 % (1390644)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2204013190:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.57/0.93 % (1390643)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1149569505:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.57/0.93 % (1390644)Instruction limit reached!
% 3.57/0.93 % (1390644)------------------------------
% 3.57/0.93 % (1390644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.57/0.93 % (1390644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.57/0.93 % (1390644)CaDiCaL version: 2.1.3
% 3.57/0.93 % (1390644)Termination reason: Instruction limit
% 3.57/0.93 % (1390644)Termination phase: Saturation
% 3.57/0.93 % (1390644)Time elapsed: 0.023 s
% 3.57/0.93 % (1390644)Peak memory usage: 12 MB
% 3.57/0.93 % (1390644)Instructions burned: 42 (million)
% 3.57/0.93 % (1390606)Instruction limit reached!
% 3.57/0.93 % (1390606)------------------------------
% 3.57/0.93 % (1390606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.57/0.93 % (1390606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.57/0.93 % (1390606)CaDiCaL version: 2.1.3
% 3.57/0.93 % (1390606)Termination reason: Instruction limit
% 3.57/0.93 % (1390606)Termination phase: Saturation
% 3.57/0.93 % (1390606)Time elapsed: 0.216 s
% 3.57/0.93 % (1390606)Peak memory usage: 13 MB
% 3.57/0.93 % (1390606)Instructions burned: 249 (million)
% 3.57/0.93 % (1390649)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.57/0.93 % (1390650)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=953190453:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.57/0.93 % (1390649)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=730445516:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.57/0.93 % (1390649)Instruction limit reached!
% 3.57/0.93 % (1390649)------------------------------
% 3.57/0.93 % (1390649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.57/0.93 % (1390649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.57/0.93 % (1390649)CaDiCaL version: 2.1.3
% 3.57/0.93 % (1390649)Termination reason: Instruction limit
% 3.57/0.93 % (1390649)Termination phase: Saturation
% 3.57/0.93 % (1390649)Time elapsed: 0.004 s
% 3.57/0.93 % (1390649)Peak memory usage: 12 MB
% 4.99/1.11 % (1390649)Instructions burned: 7 (million)
% 4.99/1.11 % (1390580)Instruction limit reached!
% 4.99/1.11 % (1390580)------------------------------
% 4.99/1.11 % (1390580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.99/1.11 % (1390580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.99/1.11 % (1390580)CaDiCaL version: 2.1.3
% 4.99/1.11 % (1390580)Termination reason: Instruction limit
% 4.99/1.11 % (1390580)Termination phase: Saturation
% 4.99/1.11 % (1390580)Time elapsed: 0.362 s
% 4.99/1.11 % (1390580)Peak memory usage: 12 MB
% 4.99/1.11 % (1390580)Instructions burned: 635 (million)
% 4.99/1.11 % (1390653)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=1787112521:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 4.99/1.11 % (1390654)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 4.99/1.11 % (1390654)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=854162813:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 4.99/1.11 % (1390654)Instruction limit reached!
% 4.99/1.11 % (1390654)------------------------------
% 4.99/1.11 % (1390654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.99/1.11 % (1390654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.99/1.11 % (1390654)CaDiCaL version: 2.1.3
% 4.99/1.11 % (1390654)Termination reason: Instruction limit
% 4.99/1.11 % (1390654)Termination phase: Saturation
% 4.99/1.11 % (1390654)Time elapsed: 0.007 s
% 4.99/1.11 % (1390654)Peak memory usage: 12 MB
% 4.99/1.11 % (1390654)Instructions burned: 7 (million)
% 4.99/1.11 % (1390614)Instruction limit reached!
% 4.99/1.11 % (1390614)------------------------------
% 4.99/1.11 % (1390614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.99/1.11 % (1390614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.99/1.11 % (1390614)CaDiCaL version: 2.1.3
% 4.99/1.11 % (1390614)Termination reason: Instruction limit
% 4.99/1.11 % (1390614)Termination phase: Saturation
% 4.99/1.11 % (1390614)Time elapsed: 0.270 s
% 4.99/1.11 % (1390614)Peak memory usage: 13 MB
% 4.99/1.11 % (1390614)Instructions burned: 327 (million)
% 4.99/1.11 % (1390641)Instruction limit reached!
% 4.99/1.11 % (1390641)------------------------------
% 4.99/1.11 % (1390641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.99/1.11 % (1390641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.99/1.11 % (1390641)CaDiCaL version: 2.1.3
% 4.99/1.11 % (1390657)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=871757455:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 4.99/1.11 % (1390641)Termination reason: Instruction limit
% 4.99/1.11 % (1390641)Termination phase: Saturation
% 4.99/1.11 % (1390641)Time elapsed: 0.128 s
% 4.99/1.11 % (1390641)Peak memory usage: 13 MB
% 4.99/1.11 % (1390641)Instructions burned: 144 (million)
% 4.99/1.11 % (1390650)Instruction limit reached!
% 4.99/1.11 % (1390650)------------------------------
% 4.99/1.11 % (1390650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.99/1.11 % (1390650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.99/1.11 % (1390650)CaDiCaL version: 2.1.3
% 4.99/1.11 % (1390650)Termination reason: Instruction limit
% 4.99/1.11 % (1390650)Termination phase: Saturation
% 4.99/1.11 % (1390650)Time elapsed: 0.086 s
% 4.99/1.11 % (1390650)Peak memory usage: 13 MB
% 4.99/1.11 % (1390650)Instructions burned: 181 (million)
% 4.99/1.11 % (1390658)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=675490284:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 4.99/1.11 % (1390657)Instruction limit reached!
% 4.99/1.11 % (1390657)------------------------------
% 4.99/1.11 % (1390657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.99/1.11 % (1390657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.99/1.11 % (1390657)CaDiCaL version: 2.1.3
% 4.99/1.11 % (1390657)Termination reason: Instruction limit
% 4.99/1.11 % (1390657)Termination phase: Saturation
% 4.99/1.11 % (1390657)Time elapsed: 0.020 s
% 4.99/1.11 % (1390657)Peak memory usage: 12 MB
% 5.83/1.28 % (1390657)Instructions burned: 22 (million)
% 5.83/1.28 % (1390660)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=113263093:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 5.83/1.28 % (1390658)Instruction limit reached!
% 5.83/1.28 % (1390658)------------------------------
% 5.83/1.28 % (1390658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.28 % (1390658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.28 % (1390658)CaDiCaL version: 2.1.3
% 5.83/1.28 % (1390658)Termination reason: Instruction limit
% 5.83/1.28 % (1390658)Termination phase: Saturation
% 5.83/1.28 % (1390658)Time elapsed: 0.018 s
% 5.83/1.28 % (1390658)Peak memory usage: 12 MB
% 5.83/1.28 % (1390658)Instructions burned: 19 (million)
% 5.83/1.28 % (1390661)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=3934850590:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 5.83/1.28 % (1390665)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3462070766:i=480:rtra=on_2995 on theBenchmark for (2995ds/480Mi)
% 5.83/1.28 % (1390664)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=1517315334:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2995 on theBenchmark for (2995ds/45Mi)
% 5.83/1.28 % (1390643)Instruction limit reached!
% 5.83/1.28 % (1390643)------------------------------
% 5.83/1.28 % (1390643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.28 % (1390643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.28 % (1390643)CaDiCaL version: 2.1.3
% 5.83/1.28 % (1390643)Termination reason: Instruction limit
% 5.83/1.28 % (1390643)Termination phase: Saturation
% 5.83/1.28 % (1390643)Time elapsed: 0.170 s
% 5.83/1.28 % (1390643)Peak memory usage: 13 MB
% 5.83/1.28 % (1390643)Instructions burned: 193 (million)
% 5.83/1.28 % (1390653)Instruction limit reached!
% 5.83/1.28 % (1390653)------------------------------
% 5.83/1.28 % (1390653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.28 % (1390653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.28 % (1390653)CaDiCaL version: 2.1.3
% 5.83/1.28 % (1390653)Termination reason: Instruction limit
% 5.83/1.28 % (1390653)Termination phase: Saturation
% 5.83/1.28 % (1390653)Time elapsed: 0.130 s
% 5.83/1.28 % (1390653)Peak memory usage: 13 MB
% 5.83/1.28 % (1390653)Instructions burned: 169 (million)
% 5.83/1.28 % (1390669)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2748801011:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 5.83/1.28 % (1390664)Instruction limit reached!
% 5.83/1.28 % (1390664)------------------------------
% 5.83/1.28 % (1390664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.28 % (1390664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.28 % (1390664)CaDiCaL version: 2.1.3
% 5.83/1.28 % (1390664)Termination reason: Instruction limit
% 5.83/1.28 % (1390664)Termination phase: Saturation
% 5.83/1.28 % (1390664)Time elapsed: 0.042 s
% 5.83/1.28 % (1390664)Peak memory usage: 12 MB
% 5.83/1.28 % (1390664)Instructions burned: 45 (million)
% 5.83/1.28 % (1390669)Instruction limit reached!
% 5.83/1.28 % (1390669)------------------------------
% 5.83/1.28 % (1390669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.83/1.28 % (1390669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.28 % (1390669)CaDiCaL version: 2.1.3
% 5.83/1.28 % (1390669)Termination reason: Instruction limit
% 5.83/1.28 % (1390669)Termination phase: Saturation
% 5.83/1.28 % (1390669)Time elapsed: 0.021 s
% 5.83/1.28 % (1390669)Peak memory usage: 12 MB
% 5.83/1.28 % (1390669)Instructions burned: 21 (million)
% 5.83/1.28 % (1390671)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 5.83/1.28 % (1390671)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2117929565:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 7.18/1.57 % (1390674)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2016586060:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 7.18/1.57 % (1390674)Instruction limit reached!
% 7.18/1.57 % (1390674)------------------------------
% 7.18/1.57 % (1390674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.18/1.57 % (1390674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.18/1.57 % (1390674)CaDiCaL version: 2.1.3
% 7.18/1.57 % (1390674)Termination reason: Instruction limit
% 7.18/1.57 % (1390674)Termination phase: Saturation
% 7.18/1.57 % (1390674)Time elapsed: 0.009 s
% 7.18/1.57 % (1390674)Peak memory usage: 12 MB
% 7.18/1.57 % (1390674)Instructions burned: 13 (million)
% 7.18/1.57 % (1390675)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=950550570:i=66:s2at=3:nm=2:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/66Mi)
% 7.18/1.57 % (1390678)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=4138907338:i=51:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/51Mi)
% 7.18/1.57 % (1390678)Instruction limit reached!
% 7.18/1.57 % (1390678)------------------------------
% 7.18/1.57 % (1390678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.18/1.57 % (1390678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.18/1.57 % (1390678)CaDiCaL version: 2.1.3
% 7.18/1.57 % (1390678)Termination reason: Instruction limit
% 7.18/1.57 % (1390678)Termination phase: Saturation
% 7.18/1.57 % (1390678)Time elapsed: 0.033 s
% 7.18/1.57 % (1390678)Peak memory usage: 12 MB
% 7.18/1.57 % (1390678)Instructions burned: 51 (million)
% 7.18/1.57 % (1390675)Instruction limit reached!
% 7.18/1.57 % (1390675)------------------------------
% 7.18/1.57 % (1390675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.18/1.57 % (1390675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.18/1.57 % (1390675)CaDiCaL version: 2.1.3
% 7.18/1.57 % (1390675)Termination reason: Instruction limit
% 7.18/1.57 % (1390675)Termination phase: Saturation
% 7.18/1.57 % (1390675)Time elapsed: 0.062 s
% 7.18/1.57 % (1390675)Peak memory usage: 13 MB
% 7.18/1.57 % (1390675)Instructions burned: 66 (million)
% 7.18/1.57 % (1390681)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2257560131:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 7.18/1.57 % (1390682)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=857030162:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 7.18/1.57 % (1390681)Instruction limit reached!
% 7.18/1.57 % (1390681)------------------------------
% 7.18/1.57 % (1390681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.18/1.57 % (1390681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.18/1.57 % (1390681)CaDiCaL version: 2.1.3
% 7.18/1.57 % (1390681)Termination reason: Instruction limit
% 7.18/1.57 % (1390681)Termination phase: Saturation
% 7.18/1.57 % (1390681)Time elapsed: 0.032 s
% 7.18/1.57 % (1390681)Peak memory usage: 12 MB
% 7.18/1.57 % (1390681)Instructions burned: 31 (million)
% 7.18/1.57 % (1390665)Instruction limit reached!
% 7.18/1.57 % (1390665)------------------------------
% 7.18/1.57 % (1390665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.18/1.57 % (1390665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.18/1.57 % (1390665)CaDiCaL version: 2.1.3
% 7.18/1.57 % (1390665)Termination reason: Instruction limit
% 7.18/1.57 % (1390665)Termination phase: Saturation
% 7.18/1.57 % (1390665)Time elapsed: 0.212 s
% 7.18/1.57 % (1390665)Peak memory usage: 13 MB
% 7.18/1.57 % (1390665)Instructions burned: 481 (million)
% 7.18/1.57 % (1390686)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=4181209620:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2992 on theBenchmark for (2992ds/67Mi)
% 7.18/1.57 % (1390671)Instruction limit reached!
% 7.18/1.57 % (1390671)------------------------------
% 7.18/1.57 % (1390671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.18/1.57 % (1390671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.18/1.57 % (1390671)CaDiCaL version: 2.1.3
% 8.63/1.71 % (1390671)Termination reason: Instruction limit
% 8.63/1.71 % (1390671)Termination phase: Saturation
% 8.63/1.71 % (1390671)Time elapsed: 0.174 s
% 8.63/1.71 % (1390671)Peak memory usage: 12 MB
% 8.63/1.71 % (1390671)Instructions burned: 200 (million)
% 8.63/1.71 % (1390685)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=3203767351:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 8.63/1.71 % (1390660)Instruction limit reached!
% 8.63/1.71 % (1390660)------------------------------
% 8.63/1.71 % (1390660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.63/1.71 % (1390660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/1.71 % (1390660)CaDiCaL version: 2.1.3
% 8.63/1.71 % (1390660)Termination reason: Instruction limit
% 8.63/1.71 % (1390660)Termination phase: Saturation
% 8.63/1.71 % (1390660)Time elapsed: 0.273 s
% 8.63/1.71 % (1390660)Peak memory usage: 15 MB
% 8.63/1.71 % (1390660)Instructions burned: 317 (million)
% 8.63/1.71 % (1390686)Instruction limit reached!
% 8.63/1.71 % (1390686)------------------------------
% 8.63/1.71 % (1390686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.63/1.71 % (1390686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/1.71 % (1390686)CaDiCaL version: 2.1.3
% 8.63/1.71 % (1390686)Termination reason: Instruction limit
% 8.63/1.71 % (1390686)Termination phase: Saturation
% 8.63/1.71 % (1390686)Time elapsed: 0.032 s
% 8.63/1.71 % (1390686)Peak memory usage: 12 MB
% 8.63/1.71 % (1390686)Instructions burned: 68 (million)
% 8.63/1.71 % (1390688)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 8.63/1.71 % (1390688)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1740199277:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2992 on theBenchmark for (2992ds/180Mi)
% 8.63/1.71 % (1390685)Instruction limit reached!
% 8.63/1.71 % (1390685)------------------------------
% 8.63/1.71 % (1390685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.63/1.71 % (1390685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/1.72 % (1390685)CaDiCaL version: 2.1.3
% 8.63/1.72 % (1390685)Termination reason: Instruction limit
% 8.63/1.72 % (1390685)Termination phase: Saturation
% 8.63/1.72 % (1390685)Time elapsed: 0.032 s
% 8.63/1.72 % (1390685)Peak memory usage: 12 MB
% 8.63/1.72 % (1390685)Instructions burned: 35 (million)
% 8.63/1.72 % (1390690)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=3641913364:st=2:i=246:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/246Mi)
% 8.63/1.72 % (1390682)Instruction limit reached!
% 8.63/1.72 % (1390682)------------------------------
% 8.63/1.72 % (1390682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.63/1.72 % (1390682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/1.72 % (1390682)CaDiCaL version: 2.1.3
% 8.63/1.72 % (1390682)Termination reason: Instruction limit
% 8.63/1.72 % (1390682)Termination phase: Saturation
% 8.63/1.72 % (1390682)Time elapsed: 0.098 s
% 8.63/1.72 % (1390682)Peak memory usage: 12 MB
% 8.63/1.72 % (1390682)Instructions burned: 140 (million)
% 8.63/1.72 % (1390691)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3570124065:cond=on:i=96:bd=all:rtra=on_2992 on theBenchmark for (2992ds/96Mi)
% 8.63/1.72 % (1390697)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=769147423:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/874Mi)
% 8.63/1.72 % (1390695)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1915829023:i=427:sd=1:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/427Mi)
% 8.63/1.72 % (1390691)Instruction limit reached!
% 8.63/1.72 % (1390691)------------------------------
% 8.63/1.72 % (1390691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.63/1.72 % (1390691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/1.72 % (1390691)CaDiCaL version: 2.1.3
% 8.63/1.72 % (1390691)Termination reason: Instruction limit
% 8.63/1.72 % (1390691)Termination phase: Saturation
% 8.63/1.72 % (1390691)Time elapsed: 0.087 s
% 8.63/1.72 % (1390691)Peak memory usage: 12 MB
% 8.63/1.72 % (1390691)Instructions burned: 97 (million)
% 8.63/1.72 % (1390701)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2306011406:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/515Mi)
% 9.51/1.85 % (1390688)Instruction limit reached!
% 9.51/1.85 % (1390688)------------------------------
% 9.51/1.85 % (1390688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.85 % (1390688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.85 % (1390688)CaDiCaL version: 2.1.3
% 9.51/1.85 % (1390688)Termination reason: Instruction limit
% 9.51/1.85 % (1390688)Termination phase: Saturation
% 9.51/1.85 % (1390688)Time elapsed: 0.149 s
% 9.51/1.85 % (1390688)Peak memory usage: 14 MB
% 9.51/1.85 % (1390688)Instructions burned: 180 (million)
% 9.51/1.85 % (1390705)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1834297801:st=1.5:i=130:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/130Mi)
% 9.51/1.85 % (1390690)Instruction limit reached!
% 9.51/1.85 % (1390690)------------------------------
% 9.51/1.85 % (1390690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.85 % (1390690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.85 % (1390690)CaDiCaL version: 2.1.3
% 9.51/1.85 % (1390690)Termination reason: Instruction limit
% 9.51/1.85 % (1390690)Termination phase: Saturation
% 9.51/1.85 % (1390690)Time elapsed: 0.211 s
% 9.51/1.85 % (1390690)Peak memory usage: 13 MB
% 9.51/1.85 % (1390690)Instructions burned: 246 (million)
% 9.51/1.85 % (1390709)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1685526112:i=44:ep=R:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/44Mi)
% 9.51/1.85 % (1390705)Instruction limit reached!
% 9.51/1.85 % (1390705)------------------------------
% 9.51/1.85 % (1390705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.85 % (1390705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.85 % (1390705)CaDiCaL version: 2.1.3
% 9.51/1.85 % (1390705)Termination reason: Instruction limit
% 9.51/1.85 % (1390705)Termination phase: Saturation
% 9.51/1.85 % (1390705)Time elapsed: 0.096 s
% 9.51/1.85 % (1390705)Peak memory usage: 12 MB
% 9.51/1.85 % (1390705)Instructions burned: 131 (million)
% 9.51/1.85 % (1390709)Instruction limit reached!
% 9.51/1.85 % (1390709)------------------------------
% 9.51/1.85 % (1390709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.85 % (1390709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.85 % (1390709)CaDiCaL version: 2.1.3
% 9.51/1.85 % (1390709)Termination reason: Instruction limit
% 9.51/1.85 % (1390709)Termination phase: Saturation
% 9.51/1.85 % (1390709)Time elapsed: 0.036 s
% 9.51/1.85 % (1390709)Peak memory usage: 12 MB
% 9.51/1.85 % (1390709)Instructions burned: 45 (million)
% 9.51/1.85 % (1390711)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3224920201:s2a=on:i=571:nm=16:rtra=on_2989 on theBenchmark for (2989ds/571Mi)
% 9.51/1.85 % (1390712)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3277102017:i=450:rtra=on:ixr=off:ntd=on_2989 on theBenchmark for (2989ds/450Mi)
% 9.51/1.85 % (1390695)Instruction limit reached!
% 9.51/1.85 % (1390695)------------------------------
% 9.51/1.85 % (1390695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.85 % (1390695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.85 % (1390695)CaDiCaL version: 2.1.3
% 9.51/1.85 % (1390695)Termination reason: Instruction limit
% 9.51/1.85 % (1390695)Termination phase: Saturation
% 9.51/1.85 % (1390695)Time elapsed: 0.369 s
% 9.51/1.85 % (1390695)Peak memory usage: 14 MB
% 9.51/1.85 % (1390695)Instructions burned: 427 (million)
% 9.51/1.85 % (1390661)Instruction limit reached!
% 9.51/1.85 % (1390661)------------------------------
% 9.51/1.85 % (1390661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.85 % (1390661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.85 % (1390661)CaDiCaL version: 2.1.3
% 9.51/1.85 % (1390661)Termination reason: Instruction limit
% 9.51/1.85 % (1390661)Termination phase: Saturation
% 9.51/1.85 % (1390661)Time elapsed: 0.701 s
% 9.51/1.85 % (1390661)Peak memory usage: 16 MB
% 9.51/1.85 % (1390661)Instructions burned: 853 (million)
% 9.51/1.85 % (1390697)Instruction limit reached!
% 9.51/1.85 % (1390697)------------------------------
% 9.51/1.85 % (1390697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.85 % (1390697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.00/2.11 % (1390697)CaDiCaL version: 2.1.3
% 12.00/2.11 % (1390697)Termination reason: Instruction limit
% 12.00/2.11 % (1390697)Termination phase: Saturation
% 12.00/2.11 % (1390697)Time elapsed: 0.385 s
% 12.00/2.11 % (1390697)Peak memory usage: 14 MB
% 12.00/2.11 % (1390697)Instructions burned: 874 (million)
% 12.00/2.11 % (1390718)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=4272313681:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/95Mi)
% 12.00/2.11 % (1390719)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=146598442:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 12.00/2.11 % (1390720)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=932498598:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2987 on theBenchmark for (2987ds/105Mi)
% 12.00/2.11 % (1390719)Instruction limit reached!
% 12.00/2.11 % (1390719)------------------------------
% 12.00/2.11 % (1390719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.00/2.11 % (1390719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.00/2.11 % (1390719)CaDiCaL version: 2.1.3
% 12.00/2.11 % (1390719)Termination reason: Instruction limit
% 12.00/2.11 % (1390719)Termination phase: Saturation
% 12.00/2.11 % (1390719)Time elapsed: 0.060 s
% 12.00/2.11 % (1390719)Peak memory usage: 13 MB
% 12.00/2.11 % (1390719)Instructions burned: 65 (million)
% 12.00/2.11 % (1390718)Instruction limit reached!
% 12.00/2.11 % (1390718)------------------------------
% 12.00/2.11 % (1390718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.00/2.11 % (1390718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.00/2.11 % (1390718)CaDiCaL version: 2.1.3
% 12.00/2.11 % (1390718)Termination reason: Instruction limit
% 12.00/2.11 % (1390718)Termination phase: Saturation
% 12.00/2.11 % (1390718)Time elapsed: 0.093 s
% 12.00/2.11 % (1390718)Peak memory usage: 12 MB
% 12.00/2.11 % (1390718)Instructions burned: 95 (million)
% 12.00/2.11 % (1390639)Instruction limit reached!
% 12.00/2.11 % (1390639)------------------------------
% 12.00/2.11 % (1390639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.00/2.11 % (1390639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.00/2.11 % (1390639)CaDiCaL version: 2.1.3
% 12.00/2.11 % (1390639)Termination reason: Instruction limit
% 12.00/2.11 % (1390639)Termination phase: Saturation
% 12.00/2.11 % (1390639)Time elapsed: 1.001 s
% 12.00/2.11 % (1390639)Peak memory usage: 14 MB
% 12.00/2.11 % (1390639)Instructions burned: 1240 (million)
% 12.00/2.11 % (1390720)Instruction limit reached!
% 12.00/2.11 % (1390720)------------------------------
% 12.00/2.11 % (1390720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.00/2.11 % (1390720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.00/2.11 % (1390720)CaDiCaL version: 2.1.3
% 12.00/2.11 % (1390720)Termination reason: Instruction limit
% 12.00/2.11 % (1390720)Termination phase: Saturation
% 12.00/2.11 % (1390720)Time elapsed: 0.090 s
% 12.00/2.11 % (1390720)Peak memory usage: 13 MB
% 12.00/2.11 % (1390720)Instructions burned: 106 (million)
% 12.00/2.11 % (1390727)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=1120874883:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2986 on theBenchmark for (2986ds/5755Mi)
% 12.00/2.11 % (1390729)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1851742498:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2986 on theBenchmark for (2986ds/495Mi)
% 12.00/2.11 % (1390728)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1593476241:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/375Mi)
% 12.00/2.11 % (1390701)Instruction limit reached!
% 12.00/2.11 % (1390701)------------------------------
% 12.00/2.11 % (1390701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.00/2.11 % (1390701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.00/2.11 % (1390701)CaDiCaL version: 2.1.3
% 12.00/2.11 % (1390701)Termination reason: Instruction limit
% 12.63/2.17 % (1390701)Termination phase: Saturation
% 12.63/2.17 % (1390701)Time elapsed: 0.431 s
% 12.63/2.17 % (1390701)Peak memory usage: 15 MB
% 12.63/2.17 % (1390701)Instructions burned: 516 (million)
% 12.63/2.17 % (1390712)Instruction limit reached!
% 12.63/2.17 % (1390712)------------------------------
% 12.63/2.17 % (1390712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.63/2.17 % (1390712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.17 % (1390712)CaDiCaL version: 2.1.3
% 12.63/2.17 % (1390712)Termination reason: Instruction limit
% 12.63/2.17 % (1390712)Termination phase: Saturation
% 12.63/2.17 % (1390712)Time elapsed: 0.261 s
% 12.63/2.17 % (1390712)Peak memory usage: 13 MB
% 12.63/2.17 % (1390712)Instructions burned: 452 (million)
% 12.63/2.17 % (1390730)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=1075902069:cond=on:i=34:hud=10:nm=10:rtra=on_2986 on theBenchmark for (2986ds/34Mi)
% 12.63/2.17 % (1390734)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1556850811:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2986 on theBenchmark for (2986ds/91Mi)
% 12.63/2.17 % (1390735)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=3195504377:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2986 on theBenchmark for (2986ds/66Mi)
% 12.63/2.17 % (1390730)Instruction limit reached!
% 12.63/2.17 % (1390730)------------------------------
% 12.63/2.17 % (1390730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.63/2.17 % (1390730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.17 % (1390730)CaDiCaL version: 2.1.3
% 12.63/2.17 % (1390730)Termination reason: Instruction limit
% 12.63/2.17 % (1390730)Termination phase: Saturation
% 12.63/2.17 % (1390730)Time elapsed: 0.032 s
% 12.63/2.17 % (1390730)Peak memory usage: 12 MB
% 12.63/2.17 % (1390730)Instructions burned: 34 (million)
% 12.63/2.17 % (1390734)Instruction limit reached!
% 12.63/2.17 % (1390734)------------------------------
% 12.63/2.17 % (1390734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.63/2.17 % (1390734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.17 % (1390734)CaDiCaL version: 2.1.3
% 12.63/2.17 % (1390734)Termination reason: Instruction limit
% 12.63/2.17 % (1390734)Termination phase: Saturation
% 12.63/2.17 % (1390734)Time elapsed: 0.042 s
% 12.63/2.17 % (1390734)Peak memory usage: 12 MB
% 12.63/2.17 % (1390734)Instructions burned: 91 (million)
% 12.63/2.17 % (1390739)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1886001706:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2985 on theBenchmark for (2985ds/22Mi)
% 12.63/2.17 % (1390740)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=1367545400:i=338:bd=all:ins=4:rtra=on_2985 on theBenchmark for (2985ds/338Mi)
% 12.63/2.17 % (1390739)Instruction limit reached!
% 12.63/2.17 % (1390739)------------------------------
% 12.63/2.17 % (1390739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.63/2.17 % (1390739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.17 % (1390739)CaDiCaL version: 2.1.3
% 12.63/2.17 % (1390739)Termination reason: Instruction limit
% 12.63/2.17 % (1390739)Termination phase: Saturation
% 12.63/2.17 % (1390739)Time elapsed: 0.021 s
% 12.63/2.17 % (1390739)Peak memory usage: 12 MB
% 12.63/2.17 % (1390739)Instructions burned: 23 (million)
% 12.63/2.17 % (1390735)Instruction limit reached!
% 12.63/2.17 % (1390735)------------------------------
% 12.63/2.17 % (1390735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.63/2.17 % (1390735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.17 % (1390735)CaDiCaL version: 2.1.3
% 12.63/2.17 % (1390735)Termination reason: Instruction limit
% 12.63/2.17 % (1390735)Termination phase: Saturation
% 12.63/2.17 % (1390735)Time elapsed: 0.063 s
% 12.63/2.17 % (1390735)Peak memory usage: 12 MB
% 12.63/2.17 % (1390735)Instructions burned: 70 (million)
% 12.63/2.17 % (1390744)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 12.63/2.17 % (1390743)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3801750463:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/28Mi)
% 12.63/2.17 % (1390744)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3623234624:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2985 on theBenchmark for (2985ds/137Mi)
% 13.97/2.60 % (1390711)Instruction limit reached!
% 13.97/2.60 % (1390711)------------------------------
% 13.97/2.60 % (1390711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.60 % (1390711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.60 % (1390711)CaDiCaL version: 2.1.3
% 13.97/2.60 % (1390711)Termination reason: Instruction limit
% 13.97/2.60 % (1390711)Termination phase: Saturation
% 13.97/2.60 % (1390711)Time elapsed: 0.435 s
% 13.97/2.60 % (1390711)Peak memory usage: 14 MB
% 13.97/2.60 % (1390711)Instructions burned: 572 (million)
% 13.97/2.60 % (1390743)Instruction limit reached!
% 13.97/2.60 % (1390743)------------------------------
% 13.97/2.60 % (1390743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.60 % (1390743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.60 % (1390743)CaDiCaL version: 2.1.3
% 13.97/2.60 % (1390743)Termination reason: Instruction limit
% 13.97/2.60 % (1390743)Termination phase: Saturation
% 13.97/2.60 % (1390743)Time elapsed: 0.028 s
% 13.97/2.60 % (1390743)Peak memory usage: 12 MB
% 13.97/2.60 % (1390743)Instructions burned: 28 (million)
% 13.97/2.60 % (1390747)dis+10_32_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=32,1:uwa=one_side_interpreted:nwc=1:random_seed=308043660:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2984 on theBenchmark for (2984ds/340Mi)
% 13.97/2.60 % (1390748)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=3362350910:i=227:sd=1:bd=all:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/227Mi)
% 13.97/2.60 % (1390728)Instruction limit reached!
% 13.97/2.60 % (1390728)------------------------------
% 13.97/2.60 % (1390728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.60 % (1390728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.60 % (1390728)CaDiCaL version: 2.1.3
% 13.97/2.60 % (1390728)Termination reason: Instruction limit
% 13.97/2.60 % (1390728)Termination phase: Saturation
% 13.97/2.60 % (1390728)Time elapsed: 0.222 s
% 13.97/2.60 % (1390728)Peak memory usage: 14 MB
% 13.97/2.60 % (1390728)Instructions burned: 376 (million)
% 13.97/2.60 % (1390751)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 13.97/2.60 % (1390751)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=127388789:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/373Mi)
% 13.97/2.60 % (1390744)Instruction limit reached!
% 13.97/2.60 % (1390744)------------------------------
% 13.97/2.60 % (1390744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.60 % (1390744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.60 % (1390744)CaDiCaL version: 2.1.3
% 13.97/2.60 % (1390744)Termination reason: Instruction limit
% 13.97/2.60 % (1390744)Termination phase: Saturation
% 13.97/2.60 % (1390744)Time elapsed: 0.122 s
% 13.97/2.60 % (1390744)Peak memory usage: 12 MB
% 13.97/2.60 % (1390744)Instructions burned: 137 (million)
% 13.97/2.60 % (1390753)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=1051857805:i=116:ep=RSTC:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/116Mi)
% 13.97/2.60 % (1390740)Instruction limit reached!
% 13.97/2.60 % (1390740)------------------------------
% 13.97/2.60 % (1390740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.60 % (1390740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.60 % (1390740)CaDiCaL version: 2.1.3
% 13.97/2.60 % (1390740)Termination reason: Instruction limit
% 13.97/2.60 % (1390740)Termination phase: Saturation
% 13.97/2.60 % (1390740)Time elapsed: 0.271 s
% 13.97/2.60 % (1390740)Peak memory usage: 15 MB
% 13.97/2.60 % (1390740)Instructions burned: 338 (million)
% 13.97/2.60 % (1390755)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1258888863:i=575:rtra=on_2982 on theBenchmark for (2982ds/575Mi)
% 13.97/2.60 % (1390748)Instruction limit reached!
% 13.97/2.60 % (1390748)------------------------------
% 13.97/2.60 % (1390748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.60 % (1390748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.49/2.92 % (1390748)CaDiCaL version: 2.1.3
% 16.49/2.92 % (1390748)Termination reason: Instruction limit
% 16.49/2.92 % (1390748)Termination phase: Saturation
% 16.49/2.92 % (1390748)Time elapsed: 0.199 s
% 16.49/2.92 % (1390748)Peak memory usage: 13 MB
% 16.49/2.92 % (1390748)Instructions burned: 227 (million)
% 16.49/2.92 % (1390729)Instruction limit reached!
% 16.49/2.92 % (1390729)------------------------------
% 16.49/2.92 % (1390729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.49/2.92 % (1390729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.49/2.92 % (1390729)CaDiCaL version: 2.1.3
% 16.49/2.92 % (1390729)Termination reason: Instruction limit
% 16.49/2.92 % (1390729)Termination phase: Saturation
% 16.49/2.92 % (1390729)Time elapsed: 0.401 s
% 16.49/2.92 % (1390729)Peak memory usage: 14 MB
% 16.49/2.92 % (1390729)Instructions burned: 496 (million)
% 16.49/2.92 % (1390753)Instruction limit reached!
% 16.49/2.92 % (1390753)------------------------------
% 16.49/2.92 % (1390753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.49/2.92 % (1390753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.49/2.92 % (1390753)CaDiCaL version: 2.1.3
% 16.49/2.92 % (1390753)Termination reason: Instruction limit
% 16.49/2.92 % (1390753)Termination phase: Saturation
% 16.49/2.92 % (1390753)Time elapsed: 0.104 s
% 16.49/2.92 % (1390753)Peak memory usage: 12 MB
% 16.49/2.92 % (1390753)Instructions burned: 116 (million)
% 16.49/2.92 % (1390751)Instruction limit reached!
% 16.49/2.92 % (1390751)------------------------------
% 16.49/2.92 % (1390751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.49/2.92 % (1390751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.49/2.92 % (1390751)CaDiCaL version: 2.1.3
% 16.49/2.92 % (1390751)Termination reason: Instruction limit
% 16.49/2.92 % (1390751)Termination phase: Saturation
% 16.49/2.92 % (1390751)Time elapsed: 0.166 s
% 16.49/2.92 % (1390751)Peak memory usage: 14 MB
% 16.49/2.92 % (1390751)Instructions burned: 374 (million)
% 16.49/2.92 % (1390747)Instruction limit reached!
% 16.49/2.92 % (1390747)------------------------------
% 16.49/2.92 % (1390747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.49/2.92 % (1390747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.49/2.92 % (1390747)CaDiCaL version: 2.1.3
% 16.49/2.92 % (1390747)Termination reason: Instruction limit
% 16.49/2.92 % (1390747)Termination phase: Saturation
% 16.49/2.92 % (1390747)Time elapsed: 0.233 s
% 16.49/2.92 % (1390747)Peak memory usage: 12 MB
% 16.49/2.92 % (1390747)Instructions burned: 340 (million)
% 16.49/2.92 % (1390759)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=1618660976:i=421:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/421Mi)
% 16.49/2.92 % (1390757)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=508208835:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2982 on theBenchmark for (2982ds/270Mi)
% 16.49/2.92 % (1390758)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=18305954:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2982 on theBenchmark for (2982ds/9840Mi)
% 16.49/2.92 % (1390760)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 16.49/2.92 % (1390761)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=4026361908:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/31Mi)
% 16.49/2.92 % (1390760)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=1856620865:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/270Mi)
% 16.49/2.92 % (1390761)Instruction limit reached!
% 16.49/2.92 % (1390761)------------------------------
% 16.49/2.92 % (1390761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.49/2.92 % (1390761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.49/2.92 % (1390761)CaDiCaL version: 2.1.3
% 16.49/2.92 % (1390761)Termination reason: Instruction limit
% 16.49/2.92 % (1390761)Termination phase: Saturation
% 19.90/3.26 % (1390761)Time elapsed: 0.015 s
% 19.90/3.26 % (1390761)Peak memory usage: 12 MB
% 19.90/3.26 % (1390761)Instructions burned: 31 (million)
% 19.90/3.26 % (1390767)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 19.90/3.26 % (1390767)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 19.90/3.26 % (1390767)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=2326464662:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2981 on theBenchmark for (2981ds/1440Mi)
% 19.90/3.26 % (1390757)Instruction limit reached!
% 19.90/3.26 % (1390757)------------------------------
% 19.90/3.26 % (1390757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.90/3.26 % (1390757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.26 % (1390757)CaDiCaL version: 2.1.3
% 19.90/3.26 % (1390757)Termination reason: Instruction limit
% 19.90/3.26 % (1390757)Termination phase: Saturation
% 19.90/3.26 % (1390757)Time elapsed: 0.233 s
% 19.90/3.26 % (1390757)Peak memory usage: 13 MB
% 19.90/3.26 % (1390757)Instructions burned: 270 (million)
% 19.90/3.26 % (1390760)Instruction limit reached!
% 19.90/3.26 % (1390760)------------------------------
% 19.90/3.26 % (1390760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.90/3.26 % (1390760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.26 % (1390760)CaDiCaL version: 2.1.3
% 19.90/3.26 % (1390760)Termination reason: Instruction limit
% 19.90/3.26 % (1390760)Termination phase: Saturation
% 19.90/3.26 % (1390760)Time elapsed: 0.246 s
% 19.90/3.26 % (1390760)Peak memory usage: 14 MB
% 19.90/3.26 % (1390760)Instructions burned: 270 (million)
% 19.90/3.26 % (1390769)dis+10_2_sil=128000:si=on:random_seed=294354909:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2979 on theBenchmark for (2979ds/339Mi)
% 19.90/3.26 % (1390770)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=826631049:i=111:add=on:fgj=on:rtra=on:fdi=1024_2979 on theBenchmark for (2979ds/111Mi)
% 19.90/3.26 % (1390759)Instruction limit reached!
% 19.90/3.26 % (1390759)------------------------------
% 19.90/3.26 % (1390759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.90/3.26 % (1390759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.26 % (1390759)CaDiCaL version: 2.1.3
% 19.90/3.26 % (1390759)Termination reason: Instruction limit
% 19.90/3.26 % (1390759)Termination phase: Saturation
% 19.90/3.26 % (1390759)Time elapsed: 0.359 s
% 19.90/3.26 % (1390759)Peak memory usage: 13 MB
% 19.90/3.26 % (1390759)Instructions burned: 421 (million)
% 19.90/3.26 % (1390770)Instruction limit reached!
% 19.90/3.26 % (1390770)------------------------------
% 19.90/3.26 % (1390770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.90/3.26 % (1390770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.26 % (1390770)CaDiCaL version: 2.1.3
% 19.90/3.26 % (1390770)Termination reason: Instruction limit
% 19.90/3.26 % (1390770)Termination phase: Saturation
% 19.90/3.26 % (1390770)Time elapsed: 0.079 s
% 19.90/3.26 % (1390770)Peak memory usage: 12 MB
% 19.90/3.26 % (1390770)Instructions burned: 112 (million)
% 19.90/3.26 % (1390774)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=3353341794:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/136Mi)
% 19.90/3.26 % (1390773)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=3093347162:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2978 on theBenchmark for (2978ds/122Mi)
% 19.90/3.26 % (1390755)Instruction limit reached!
% 19.90/3.26 % (1390755)------------------------------
% 19.90/3.26 % (1390755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.90/3.26 % (1390755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.26 % (1390755)CaDiCaL version: 2.1.3
% 19.90/3.26 % (1390755)Termination reason: Instruction limit
% 19.90/3.26 % (1390755)Termination phase: Saturation
% 19.90/3.26 % (1390755)Time elapsed: 0.491 s
% 19.90/3.26 % (1390755)Peak memory usage: 14 MB
% 19.90/3.26 % (1390755)Instructions burned: 576 (million)
% 21.29/3.49 % (1390774)Instruction limit reached!
% 21.29/3.49 % (1390774)------------------------------
% 21.29/3.49 % (1390774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.29/3.49 % (1390774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.29/3.49 % (1390774)CaDiCaL version: 2.1.3
% 21.29/3.49 % (1390774)Termination reason: Instruction limit
% 21.29/3.49 % (1390774)Termination phase: Saturation
% 21.29/3.49 % (1390774)Time elapsed: 0.098 s
% 21.29/3.49 % (1390774)Peak memory usage: 13 MB
% 21.29/3.49 % (1390774)Instructions burned: 137 (million)
% 21.29/3.49 % (1390777)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=4286886458:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2977 on theBenchmark for (2977ds/232Mi)
% 21.29/3.49 % (1390773)Instruction limit reached!
% 21.29/3.49 % (1390773)------------------------------
% 21.29/3.49 % (1390773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.29/3.49 % (1390773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.29/3.49 % (1390773)CaDiCaL version: 2.1.3
% 21.29/3.49 % (1390773)Termination reason: Instruction limit
% 21.29/3.49 % (1390773)Termination phase: Saturation
% 21.29/3.49 % (1390773)Time elapsed: 0.105 s
% 21.29/3.49 % (1390773)Peak memory usage: 12 MB
% 21.29/3.49 % (1390773)Instructions burned: 122 (million)
% 21.29/3.49 % (1390778)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=2797993562:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2977 on theBenchmark for (2977ds/1254Mi)
% 21.29/3.49 % (1390780)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 21.29/3.49 % (1390780)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=3128892869:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2977 on theBenchmark for (2977ds/281Mi)
% 21.29/3.49 % (1390769)Instruction limit reached!
% 21.29/3.49 % (1390769)------------------------------
% 21.29/3.49 % (1390769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.29/3.49 % (1390769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.29/3.49 % (1390769)CaDiCaL version: 2.1.3
% 21.29/3.49 % (1390769)Termination reason: Instruction limit
% 21.29/3.49 % (1390769)Termination phase: Saturation
% 21.29/3.49 % (1390769)Time elapsed: 0.289 s
% 21.29/3.49 % (1390769)Peak memory usage: 13 MB
% 21.29/3.49 % (1390769)Instructions burned: 339 (million)
% 21.29/3.49 % (1390783)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1491270008:i=619:add=on:rtra=on_2976 on theBenchmark for (2976ds/619Mi)
% 21.29/3.49 % (1390767)Instruction limit reached!
% 21.29/3.49 % (1390767)------------------------------
% 21.29/3.49 % (1390767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.29/3.49 % (1390767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.29/3.49 % (1390767)CaDiCaL version: 2.1.3
% 21.29/3.49 % (1390767)Termination reason: Instruction limit
% 21.29/3.49 % (1390767)Termination phase: Saturation
% 21.29/3.49 % (1390767)Time elapsed: 0.634 s
% 21.29/3.49 % (1390767)Peak memory usage: 13 MB
% 21.29/3.49 % (1390767)Instructions burned: 1442 (million)
% 21.29/3.49 % (1390777)Instruction limit reached!
% 21.29/3.49 % (1390777)------------------------------
% 21.29/3.49 % (1390777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.29/3.49 % (1390777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.29/3.49 % (1390777)CaDiCaL version: 2.1.3
% 21.29/3.49 % (1390777)Termination reason: Instruction limit
% 21.29/3.49 % (1390777)Termination phase: Saturation
% 21.29/3.49 % (1390777)Time elapsed: 0.199 s
% 21.29/3.49 % (1390777)Peak memory usage: 12 MB
% 21.29/3.49 % (1390777)Instructions burned: 233 (million)
% 21.29/3.49 % (1390785)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=753541572:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2975 on theBenchmark for (2975ds/865Mi)
% 21.29/3.49 % (1390786)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1000153934:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/212Mi)
% 21.29/3.49 % (1390780)Instruction limit reached!
% 21.29/3.49 % (1390780)------------------------------
% 21.29/3.49 % (1390780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.23/4.07 % (1390780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.23/4.07 % (1390780)CaDiCaL version: 2.1.3
% 26.23/4.07 % (1390780)Termination reason: Instruction limit
% 26.23/4.07 % (1390780)Termination phase: Saturation
% 26.23/4.07 % (1390780)Time elapsed: 0.248 s
% 26.23/4.07 % (1390780)Peak memory usage: 13 MB
% 26.23/4.07 % (1390780)Instructions burned: 282 (million)
% 26.23/4.07 % (1390789)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=552347628:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/130Mi)
% 26.23/4.07 % (1390789)Instruction limit reached!
% 26.23/4.07 % (1390789)------------------------------
% 26.23/4.07 % (1390789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.23/4.07 % (1390789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.23/4.07 % (1390789)CaDiCaL version: 2.1.3
% 26.23/4.07 % (1390789)Termination reason: Instruction limit
% 26.23/4.07 % (1390789)Termination phase: Saturation
% 26.23/4.07 % (1390789)Time elapsed: 0.117 s
% 26.23/4.07 % (1390789)Peak memory usage: 12 MB
% 26.23/4.07 % (1390789)Instructions burned: 130 (million)
% 26.23/4.07 % (1390786)Instruction limit reached!
% 26.23/4.07 % (1390786)------------------------------
% 26.23/4.07 % (1390786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.23/4.07 % (1390786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.23/4.07 % (1390786)CaDiCaL version: 2.1.3
% 26.23/4.07 % (1390786)Termination reason: Instruction limit
% 26.23/4.07 % (1390786)Termination phase: Saturation
% 26.23/4.07 % (1390786)Time elapsed: 0.211 s
% 26.23/4.07 % (1390786)Peak memory usage: 13 MB
% 26.23/4.07 % (1390786)Instructions burned: 213 (million)
% 26.23/4.07 % (1390793)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2524576924:st=1.5:i=346:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/346Mi)
% 26.23/4.07 % (1390794)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=843631302:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2972 on theBenchmark for (2972ds/152Mi)
% 26.23/4.07 % (1390783)Instruction limit reached!
% 26.23/4.07 % (1390783)------------------------------
% 26.23/4.07 % (1390783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.23/4.07 % (1390783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.23/4.07 % (1390783)CaDiCaL version: 2.1.3
% 26.23/4.07 % (1390783)Termination reason: Instruction limit
% 26.23/4.07 % (1390783)Termination phase: Saturation
% 26.23/4.07 % (1390783)Time elapsed: 0.407 s
% 26.23/4.07 % (1390783)Peak memory usage: 13 MB
% 26.23/4.07 % (1390783)Instructions burned: 619 (million)
% 26.23/4.07 % (1390797)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1182192665:i=75:ep=R:rtra=on:ntd=on_2972 on theBenchmark for (2972ds/75Mi)
% 26.23/4.07 % (1390785)Instruction limit reached!
% 26.23/4.07 % (1390785)------------------------------
% 26.23/4.07 % (1390785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.23/4.07 % (1390785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.23/4.07 % (1390785)CaDiCaL version: 2.1.3
% 26.23/4.07 % (1390785)Termination reason: Instruction limit
% 26.23/4.07 % (1390785)Termination phase: Saturation
% 26.23/4.07 % (1390785)Time elapsed: 0.397 s
% 26.23/4.07 % (1390785)Peak memory usage: 17 MB
% 26.23/4.07 % (1390785)Instructions burned: 866 (million)
% 26.23/4.07 % (1390797)Instruction limit reached!
% 26.23/4.07 % (1390797)------------------------------
% 26.23/4.07 % (1390797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.23/4.07 % (1390797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.23/4.07 % (1390797)CaDiCaL version: 2.1.3
% 26.23/4.07 % (1390797)Termination reason: Instruction limit
% 26.23/4.07 % (1390797)Termination phase: Saturation
% 26.23/4.07 % (1390797)Time elapsed: 0.080 s
% 26.23/4.07 % (1390797)Peak memory usage: 12 MB
% 26.23/4.07 % (1390797)Instructions burned: 75 (million)
% 26.23/4.07 % (1390794)Instruction limit reached!
% 26.23/4.07 % (1390794)------------------------------
% 26.23/4.07 % (1390794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.23/4.07 % (1390794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.23/4.07 % (1390794)CaDiCaL version: 2.1.3
% 26.23/4.07 % (1390794)Termination reason: Instruction limit
% 26.23/4.07 % (1390794)Termination phase: Saturation
% 26.23/4.07 % (1390794)Time elapsed: 0.146 s
% 28.07/4.45 % (1390794)Peak memory usage: 13 MB
% 28.07/4.45 % (1390794)Instructions burned: 152 (million)
% 28.07/4.45 % (1390799)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=2021915216:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/387Mi)
% 28.07/4.45 % (1390800)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=735585645:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2971 on theBenchmark for (2971ds/148Mi)
% 28.07/4.45 % (1390801)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1521499724:i=161:piset=and:rtra=on:ntd=on_2970 on theBenchmark for (2970ds/161Mi)
% 28.07/4.45 % (1390800)Instruction limit reached!
% 28.07/4.45 % (1390800)------------------------------
% 28.07/4.45 % (1390800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.07/4.45 % (1390800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.07/4.45 % (1390800)CaDiCaL version: 2.1.3
% 28.07/4.45 % (1390800)Termination reason: Instruction limit
% 28.07/4.45 % (1390800)Termination phase: Saturation
% 28.07/4.45 % (1390800)Time elapsed: 0.070 s
% 28.07/4.45 % (1390800)Peak memory usage: 12 MB
% 28.07/4.45 % (1390800)Instructions burned: 149 (million)
% 28.07/4.45 % (1390805)lrs+10_1_sil=128000:si=on:random_seed=1923676663:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/888Mi)
% 28.07/4.45 % (1390793)Instruction limit reached!
% 28.07/4.45 % (1390793)------------------------------
% 28.07/4.45 % (1390793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.07/4.45 % (1390793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.07/4.45 % (1390793)CaDiCaL version: 2.1.3
% 28.07/4.45 % (1390793)Termination reason: Instruction limit
% 28.07/4.45 % (1390793)Termination phase: Saturation
% 28.07/4.45 % (1390793)Time elapsed: 0.286 s
% 28.07/4.45 % (1390793)Peak memory usage: 13 MB
% 28.07/4.45 % (1390793)Instructions burned: 346 (million)
% 28.07/4.45 % (1390807)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=2033005593:i=136:add=on:ins=4:rtra=on:sup=off_2969 on theBenchmark for (2969ds/136Mi)
% 28.07/4.45 % (1390801)Instruction limit reached!
% 28.07/4.45 % (1390801)------------------------------
% 28.07/4.45 % (1390801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.07/4.45 % (1390801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.07/4.45 % (1390801)CaDiCaL version: 2.1.3
% 28.07/4.45 % (1390801)Termination reason: Instruction limit
% 28.07/4.45 % (1390801)Termination phase: Saturation
% 28.07/4.45 % (1390801)Time elapsed: 0.141 s
% 28.07/4.45 % (1390801)Peak memory usage: 12 MB
% 28.07/4.45 % (1390801)Instructions burned: 161 (million)
% 28.07/4.45 % (1390807)Instruction limit reached!
% 28.07/4.45 % (1390807)------------------------------
% 28.07/4.45 % (1390807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.07/4.45 % (1390807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.07/4.45 % (1390807)CaDiCaL version: 2.1.3
% 28.07/4.45 % (1390807)Termination reason: Instruction limit
% 28.07/4.45 % (1390807)Termination phase: Saturation
% 28.07/4.45 % (1390807)Time elapsed: 0.059 s
% 28.07/4.45 % (1390807)Peak memory usage: 12 MB
% 28.07/4.45 % (1390807)Instructions burned: 138 (million)
% 28.07/4.45 % (1390799)Instruction limit reached!
% 28.07/4.45 % (1390799)------------------------------
% 28.07/4.45 % (1390799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.07/4.45 % (1390799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.07/4.45 % (1390799)CaDiCaL version: 2.1.3
% 28.07/4.45 % (1390799)Termination reason: Instruction limit
% 28.07/4.45 % (1390799)Termination phase: Saturation
% 28.07/4.45 % (1390799)Time elapsed: 0.203 s
% 28.07/4.45 % (1390799)Peak memory usage: 13 MB
% 28.07/4.45 % (1390799)Instructions burned: 389 (million)
% 28.07/4.45 % (1390811)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=2576399214:i=88:s2at=3:nm=2:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/88Mi)
% 28.07/4.45 % (1390816)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3117990685:i=2186:rtra=on:ixr=off_2968 on theBenchmark for (2968ds/2186Mi)
% 28.07/4.45 % (1390815)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=3703926848:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2968 on theBenchmark for (2968ds/93Mi)
% 28.99/4.68 % (1390811)Instruction limit reached!
% 28.99/4.68 % (1390811)------------------------------
% 28.99/4.68 % (1390811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.99/4.68 % (1390811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.99/4.68 % (1390811)CaDiCaL version: 2.1.3
% 28.99/4.68 % (1390811)Termination reason: Instruction limit
% 28.99/4.68 % (1390811)Termination phase: Saturation
% 28.99/4.68 % (1390811)Time elapsed: 0.081 s
% 28.99/4.68 % (1390811)Peak memory usage: 13 MB
% 28.99/4.68 % (1390811)Instructions burned: 88 (million)
% 28.99/4.68 % (1390815)Instruction limit reached!
% 28.99/4.68 % (1390815)------------------------------
% 28.99/4.68 % (1390815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.99/4.68 % (1390815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.99/4.68 % (1390815)CaDiCaL version: 2.1.3
% 28.99/4.68 % (1390815)Termination reason: Instruction limit
% 28.99/4.68 % (1390815)Termination phase: Saturation
% 28.99/4.68 % (1390815)Time elapsed: 0.080 s
% 28.99/4.68 % (1390815)Peak memory usage: 12 MB
% 28.99/4.68 % (1390815)Instructions burned: 94 (million)
% 28.99/4.68 % (1390819)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3624760906:s2a=on:i=240:rtra=on:ntd=on_2967 on theBenchmark for (2967ds/240Mi)
% 28.99/4.68 % (1390820)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=1022481434:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2967 on theBenchmark for (2967ds/805Mi)
% 28.99/4.68 % (1390778)Instruction limit reached!
% 28.99/4.68 % (1390778)------------------------------
% 28.99/4.68 % (1390778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.99/4.68 % (1390778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.99/4.68 % (1390778)CaDiCaL version: 2.1.3
% 28.99/4.68 % (1390778)Termination reason: Instruction limit
% 28.99/4.68 % (1390778)Termination phase: Saturation
% 28.99/4.68 % (1390778)Time elapsed: 1.031 s
% 28.99/4.68 % (1390778)Peak memory usage: 19 MB
% 28.99/4.68 % (1390778)Instructions burned: 1254 (million)
% 28.99/4.68 % (1390823)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 28.99/4.68 % (1390823)dis+1002_1_to=lpo:sil=128000:cnfonf=conj_eager:si=on:sp=unary_first:spb=intro:urr=on:cbe=off:uwa=one_side_interpreted:rp=on:avsqc=1:random_seed=410879797:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2966 on theBenchmark for (2966ds/391Mi)
% 28.99/4.68 % (1390819)Instruction limit reached!
% 28.99/4.68 % (1390819)------------------------------
% 28.99/4.68 % (1390819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.99/4.68 % (1390819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.99/4.68 % (1390819)CaDiCaL version: 2.1.3
% 28.99/4.68 % (1390819)Termination reason: Instruction limit
% 28.99/4.68 % (1390819)Termination phase: Saturation
% 28.99/4.68 % (1390819)Time elapsed: 0.208 s
% 28.99/4.68 % (1390819)Peak memory usage: 13 MB
% 28.99/4.68 % (1390819)Instructions burned: 240 (million)
% 28.99/4.68 % (1390825)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=2236376832:i=355:av=off:fsr=off:rtra=on:ixr=off_2965 on theBenchmark for (2965ds/355Mi)
% 28.99/4.68 % (1390823)Instruction limit reached!
% 28.99/4.68 % (1390823)------------------------------
% 28.99/4.68 % (1390823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.99/4.68 % (1390823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.99/4.68 % (1390823)CaDiCaL version: 2.1.3
% 28.99/4.68 % (1390823)Termination reason: Instruction limit
% 28.99/4.68 % (1390823)Termination phase: Saturation
% 28.99/4.68 % (1390823)Time elapsed: 0.334 s
% 28.99/4.68 % (1390823)Peak memory usage: 13 MB
% 28.99/4.68 % (1390823)Instructions burned: 392 (million)
% 28.99/4.68 % (1390820)Instruction limit reached!
% 28.99/4.68 % (1390820)------------------------------
% 28.99/4.68 % (1390820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.99/4.68 % (1390820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.99/4.68 % (1390820)CaDiCaL version: 2.1.3
% 28.99/4.68 % (1390820)Termination reason: Instruction limit
% 28.99/4.68 % (1390820)Termination phase: Saturation
% 28.99/4.68 % (1390820)Time elapsed: 0.477 s
% 31.15/4.98 % (1390820)Peak memory usage: 14 MB
% 31.15/4.98 % (1390820)Instructions burned: 805 (million)
% 31.15/4.98 % (1390830)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=3371822910:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2963 on theBenchmark for (2963ds/314Mi)
% 31.15/4.98 % (1390833)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=1294654842:s2a=on:i=251:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/251Mi)
% 31.15/4.98 % (1390825)Instruction limit reached!
% 31.15/4.98 % (1390825)------------------------------
% 31.15/4.98 % (1390825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.15/4.98 % (1390825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.15/4.98 % (1390825)CaDiCaL version: 2.1.3
% 31.15/4.98 % (1390825)Termination reason: Instruction limit
% 31.15/4.98 % (1390825)Termination phase: Saturation
% 31.15/4.98 % (1390825)Time elapsed: 0.310 s
% 31.15/4.98 % (1390825)Peak memory usage: 12 MB
% 31.15/4.98 % (1390825)Instructions burned: 355 (million)
% 31.15/4.98 % (1390835)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=214593795:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=2470:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2962 on theBenchmark for (2962ds/2470Mi)
% 31.15/4.98 % (1390805)Instruction limit reached!
% 31.15/4.98 % (1390805)------------------------------
% 31.15/4.98 % (1390805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.15/4.98 % (1390805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.15/4.98 % (1390805)CaDiCaL version: 2.1.3
% 31.15/4.98 % (1390805)Termination reason: Instruction limit
% 31.15/4.98 % (1390805)Termination phase: Saturation
% 31.15/4.98 % (1390805)Time elapsed: 0.779 s
% 31.15/4.98 % (1390805)Peak memory usage: 15 MB
% 31.15/4.98 % (1390805)Instructions burned: 889 (million)
% 31.15/4.98 % (1390837)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=3624803652:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2961 on theBenchmark for (2961ds/673Mi)
% 31.15/4.98 % (1390833)Instruction limit reached!
% 31.15/4.98 % (1390833)------------------------------
% 31.15/4.98 % (1390833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.15/4.98 % (1390833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.15/4.98 % (1390833)CaDiCaL version: 2.1.3
% 31.15/4.98 % (1390833)Termination reason: Instruction limit
% 31.15/4.98 % (1390833)Termination phase: Saturation
% 31.15/4.98 % (1390833)Time elapsed: 0.213 s
% 31.15/4.98 % (1390833)Peak memory usage: 13 MB
% 31.15/4.98 % (1390833)Instructions burned: 251 (million)
% 31.15/4.98 % (1390830)Instruction limit reached!
% 31.15/4.98 % (1390830)------------------------------
% 31.15/4.98 % (1390830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.15/4.98 % (1390830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.15/4.98 % (1390830)CaDiCaL version: 2.1.3
% 31.15/4.98 % (1390830)Termination reason: Instruction limit
% 31.15/4.98 % (1390830)Termination phase: Saturation
% 31.15/4.98 % (1390830)Time elapsed: 0.256 s
% 31.15/4.98 % (1390830)Peak memory usage: 13 MB
% 31.15/4.98 % (1390830)Instructions burned: 314 (million)
% 31.15/4.98 % (1390842)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1108771661:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2960 on theBenchmark for (2960ds/270Mi)
% 31.15/4.98 % (1390841)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=4200622286:i=116:ep=RSTC:rtra=on:ntd=on_2960 on theBenchmark for (2960ds/116Mi)
% 31.15/4.98 % (1390816)Instruction limit reached!
% 31.15/4.98 % (1390816)------------------------------
% 31.15/4.98 % (1390816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.15/4.98 % (1390816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.15/4.98 % (1390816)CaDiCaL version: 2.1.3
% 31.15/4.98 % (1390816)Termination reason: Instruction limit
% 31.15/4.98 % (1390816)Termination phase: Saturation
% 31.15/4.98 % (1390816)Time elapsed: 0.944 s
% 31.15/4.98 % (1390816)Peak memory usage: 16 MB
% 31.15/4.98 % (1390816)Instructions burned: 2187 (million)
% 31.15/4.98 % (1390841)Instruction limit reached!
% 31.15/4.98 % (1390841)------------------------------
% 31.15/4.98 % (1390841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.00/5.50 % (1390841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.00/5.50 % (1390841)CaDiCaL version: 2.1.3
% 36.00/5.50 % (1390841)Termination reason: Instruction limit
% 36.00/5.50 % (1390841)Termination phase: Saturation
% 36.00/5.50 % (1390841)Time elapsed: 0.100 s
% 36.00/5.50 % (1390841)Peak memory usage: 12 MB
% 36.00/5.50 % (1390841)Instructions burned: 117 (million)
% 36.00/5.50 % (1390845)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=1068934613:hsq=on:hsqr=16,1:s2a=on:i=30:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2959 on theBenchmark for (2959ds/30Mi)
% 36.00/5.50 % (1390845)Instruction limit reached!
% 36.00/5.50 % (1390845)------------------------------
% 36.00/5.50 % (1390845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.00/5.50 % (1390845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.00/5.50 % (1390845)CaDiCaL version: 2.1.3
% 36.00/5.50 % (1390845)Termination reason: Instruction limit
% 36.00/5.50 % (1390845)Termination phase: Saturation
% 36.00/5.50 % (1390845)Time elapsed: 0.013 s
% 36.00/5.50 % (1390845)Peak memory usage: 12 MB
% 36.00/5.50 % (1390845)Instructions burned: 32 (million)
% 36.00/5.50 % (1390847)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 36.00/5.50 % (1390848)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3480331849:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2958 on theBenchmark for (2958ds/365Mi)
% 36.00/5.50 % (1390847)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=2596335944:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2958 on theBenchmark for (2958ds/39Mi)
% 36.00/5.50 % (1390847)Instruction limit reached!
% 36.00/5.50 % (1390847)------------------------------
% 36.00/5.50 % (1390847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.00/5.50 % (1390847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.00/5.50 % (1390847)CaDiCaL version: 2.1.3
% 36.00/5.50 % (1390847)Termination reason: Instruction limit
% 36.00/5.50 % (1390847)Termination phase: Saturation
% 36.00/5.50 % (1390847)Time elapsed: 0.035 s
% 36.00/5.50 % (1390847)Peak memory usage: 12 MB
% 36.00/5.50 % (1390847)Instructions burned: 39 (million)
% 36.00/5.50 % (1390851)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1116911882:i=158:av=off:rtra=on_2958 on theBenchmark for (2958ds/158Mi)
% 36.00/5.50 % (1390842)Instruction limit reached!
% 36.00/5.50 % (1390842)------------------------------
% 36.00/5.50 % (1390842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.00/5.50 % (1390842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.00/5.50 % (1390842)CaDiCaL version: 2.1.3
% 36.00/5.50 % (1390842)Termination reason: Instruction limit
% 36.00/5.50 % (1390842)Termination phase: Saturation
% 36.00/5.50 % (1390842)Time elapsed: 0.216 s
% 36.00/5.50 % (1390842)Peak memory usage: 13 MB
% 36.00/5.50 % (1390842)Instructions burned: 271 (million)
% 36.00/5.50 % (1390853)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 36.00/5.50 % (1390853)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=1504490933:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2957 on theBenchmark for (2957ds/252Mi)
% 36.00/5.50 % (1390848)Instruction limit reached!
% 36.00/5.50 % (1390848)------------------------------
% 36.00/5.50 % (1390848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.00/5.50 % (1390848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.00/5.50 % (1390848)CaDiCaL version: 2.1.3
% 36.00/5.50 % (1390848)Termination reason: Instruction limit
% 36.00/5.50 % (1390848)Termination phase: Saturation
% 36.00/5.50 % (1390848)Time elapsed: 0.169 s
% 36.00/5.50 % (1390848)Peak memory usage: 13 MB
% 36.00/5.50 % (1390848)Instructions burned: 366 (million)
% 36.00/5.50 % (1390855)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=3899502577:i=213:rtra=on:ss=axioms_2956 on theBenchmark for (2956ds/213Mi)
% 36.00/5.50 % (1390851)Instruction limit reached!
% 36.00/5.50 % (1390851)------------------------------
% 36.62/5.69 % (1390851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.62/5.69 % (1390851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.62/5.69 % (1390851)CaDiCaL version: 2.1.3
% 36.62/5.69 % (1390851)Termination reason: Instruction limit
% 36.62/5.69 % (1390851)Termination phase: Saturation
% 36.62/5.69 % (1390851)Time elapsed: 0.129 s
% 36.62/5.69 % (1390851)Peak memory usage: 12 MB
% 36.62/5.69 % (1390851)Instructions burned: 158 (million)
% 36.62/5.69 % (1390857)dis+1010_28_sil=128000:tgt=full:plsq=on:plsqc=1:cnfonf=off:si=on:plsqr=128,1:uwa=off:slsqc=2:sac=on:slsq=on:random_seed=3803843823:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2956 on theBenchmark for (2956ds/160Mi)
% 36.62/5.69 % (1390855)Instruction limit reached!
% 36.62/5.69 % (1390855)------------------------------
% 36.62/5.69 % (1390855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.62/5.69 % (1390855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.62/5.69 % (1390855)CaDiCaL version: 2.1.3
% 36.62/5.69 % (1390855)Termination reason: Instruction limit
% 36.62/5.69 % (1390855)Termination phase: Saturation
% 36.62/5.69 % (1390855)Time elapsed: 0.097 s
% 36.62/5.69 % (1390855)Peak memory usage: 13 MB
% 36.62/5.69 % (1390855)Instructions burned: 215 (million)
% 36.62/5.69 % (1390837)Instruction limit reached!
% 36.62/5.69 % (1390837)------------------------------
% 36.62/5.69 % (1390837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.62/5.69 % (1390837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.62/5.69 % (1390837)CaDiCaL version: 2.1.3
% 36.62/5.69 % (1390837)Termination reason: Instruction limit
% 36.62/5.69 % (1390837)Termination phase: Saturation
% 36.62/5.69 % (1390837)Time elapsed: 0.593 s
% 36.62/5.69 % (1390837)Peak memory usage: 14 MB
% 36.62/5.69 % (1390837)Instructions burned: 673 (million)
% 36.62/5.69 % (1390861)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=1876839154:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2955 on theBenchmark for (2955ds/763Mi)
% 36.62/5.69 % (1390862)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 36.62/5.69 % (1390862)ott+1010_40_sil=128000:tgt=full:plsq=on:plsqc=5:si=on:sos=all:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=2230311099:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2955 on theBenchmark for (2955ds/237Mi)
% 36.62/5.69 % (1390853)Instruction limit reached!
% 36.62/5.69 % (1390853)------------------------------
% 36.62/5.69 % (1390853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.62/5.69 % (1390853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.62/5.69 % (1390853)CaDiCaL version: 2.1.3
% 36.62/5.69 % (1390853)Termination reason: Instruction limit
% 36.62/5.69 % (1390853)Termination phase: Saturation
% 36.62/5.69 % (1390853)Time elapsed: 0.233 s
% 36.62/5.69 % (1390853)Peak memory usage: 13 MB
% 36.62/5.69 % (1390853)Instructions burned: 252 (million)
% 36.62/5.69 % (1390857)Instruction limit reached!
% 36.62/5.69 % (1390857)------------------------------
% 36.62/5.69 % (1390857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.62/5.69 % (1390857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.62/5.69 % (1390857)CaDiCaL version: 2.1.3
% 36.62/5.69 % (1390857)Termination reason: Instruction limit
% 36.62/5.69 % (1390857)Termination phase: Saturation
% 36.62/5.69 % (1390857)Time elapsed: 0.139 s
% 36.62/5.69 % (1390857)Peak memory usage: 13 MB
% 36.62/5.69 % (1390857)Instructions burned: 161 (million)
% 36.62/5.69 % (1390865)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=2997451754:s2a=on:i=386:rtra=on:ntd=on_2955 on theBenchmark for (2955ds/386Mi)
% 36.62/5.69 % (1390866)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=1691176395:i=300:piset=and:nm=32:rtra=on_2954 on theBenchmark for (2954ds/300Mi)
% 36.62/5.69 % (1390862)Instruction limit reached!
% 36.62/5.69 % (1390862)------------------------------
% 36.62/5.69 % (1390862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.62/5.69 % (1390862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.62/5.69 % (1390862)CaDiCaL version: 2.1.3
% 36.62/5.69 % (1390862)Termination reason: Instruction limit
% 40.41/6.18 % (1390862)Termination phase: Saturation
% 40.41/6.18 % (1390862)Time elapsed: 0.172 s
% 40.41/6.18 % (1390862)Peak memory usage: 13 MB
% 40.41/6.18 % (1390862)Instructions burned: 237 (million)
% 40.41/6.18 % (1390869)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=3047337352:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2953 on theBenchmark for (2953ds/567Mi)
% 40.41/6.18 % (1390866)Instruction limit reached!
% 40.41/6.18 % (1390866)------------------------------
% 40.41/6.18 % (1390866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.41/6.18 % (1390866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.41/6.18 % (1390866)CaDiCaL version: 2.1.3
% 40.41/6.18 % (1390866)Termination reason: Instruction limit
% 40.41/6.18 % (1390866)Termination phase: Saturation
% 40.41/6.18 % (1390866)Time elapsed: 0.251 s
% 40.41/6.18 % (1390866)Peak memory usage: 12 MB
% 40.41/6.18 % (1390866)Instructions burned: 301 (million)
% 40.41/6.18 % (1390861)Instruction limit reached!
% 40.41/6.18 % (1390861)------------------------------
% 40.41/6.18 % (1390861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.41/6.18 % (1390861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.41/6.18 % (1390861)CaDiCaL version: 2.1.3
% 40.41/6.18 % (1390861)Termination reason: Instruction limit
% 40.41/6.18 % (1390861)Termination phase: Saturation
% 40.41/6.18 % (1390861)Time elapsed: 0.348 s
% 40.41/6.18 % (1390861)Peak memory usage: 16 MB
% 40.41/6.18 % (1390861)Instructions burned: 767 (million)
% 40.41/6.18 % (1390873)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=3494188156:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2952 on theBenchmark for (2952ds/379Mi)
% 40.41/6.18 % (1390874)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=1473833944:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2952 on theBenchmark for (2952ds/429Mi)
% 40.41/6.18 % (1390865)Instruction limit reached!
% 40.41/6.18 % (1390865)------------------------------
% 40.41/6.18 % (1390865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.41/6.18 % (1390865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.41/6.18 % (1390865)CaDiCaL version: 2.1.3
% 40.41/6.18 % (1390865)Termination reason: Instruction limit
% 40.41/6.18 % (1390865)Termination phase: Saturation
% 40.41/6.18 % (1390865)Time elapsed: 0.298 s
% 40.41/6.18 % (1390865)Peak memory usage: 12 MB
% 40.41/6.18 % (1390865)Instructions burned: 387 (million)
% 40.41/6.18 % (1390877)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=2158990321:i=478:bd=all:rtra=on_2951 on theBenchmark for (2951ds/478Mi)
% 40.41/6.18 % (1390874)Instruction limit reached!
% 40.41/6.18 % (1390874)------------------------------
% 40.41/6.18 % (1390874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.41/6.18 % (1390874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.41/6.18 % (1390874)CaDiCaL version: 2.1.3
% 40.41/6.18 % (1390874)Termination reason: Instruction limit
% 40.41/6.18 % (1390874)Termination phase: Saturation
% 40.41/6.18 % (1390874)Time elapsed: 0.191 s
% 40.41/6.18 % (1390874)Peak memory usage: 13 MB
% 40.41/6.18 % (1390874)Instructions burned: 429 (million)
% 40.41/6.18 % (1390879)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3908484009:i=445:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2949 on theBenchmark for (2949ds/445Mi)
% 40.41/6.18 % (1390873)Instruction limit reached!
% 40.41/6.18 % (1390873)------------------------------
% 40.41/6.18 % (1390873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.41/6.18 % (1390873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.41/6.18 % (1390873)CaDiCaL version: 2.1.3
% 40.41/6.18 % (1390873)Termination reason: Instruction limit
% 40.41/6.18 % (1390873)Termination phase: Saturation
% 40.41/6.18 % (1390873)Time elapsed: 0.307 s
% 40.41/6.18 % (1390873)Peak memory usage: 14 MB
% 40.41/6.18 % (1390873)Instructions burned: 379 (million)
% 40.41/6.18 % (1390881)ott+1003_1_to=kbo:cnfonf=lazy_pi_sigma_gen:si=on:sp=weighted_frequency:spb=units:urr=on:cbe=off:random_seed=1344004005:uwa_fpi=on:i=71:hud=10:rtra=on:ixr=off_2948 on theBenchmark for (2948ds/71Mi)
% 40.41/6.18 % (1390869)Instruction limit reached!
% 40.41/6.18 % (1390869)------------------------------
% 40.41/6.18 % (1390869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.41/6.18 % (1390869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.96/6.48 % (1390869)CaDiCaL version: 2.1.3
% 41.96/6.48 % (1390869)Termination reason: Instruction limit
% 41.96/6.48 % (1390869)Termination phase: Saturation
% 41.96/6.48 % (1390869)Time elapsed: 0.495 s
% 41.96/6.48 % (1390869)Peak memory usage: 14 MB
% 41.96/6.48 % (1390869)Instructions burned: 568 (million)
% 41.96/6.48 % (1390883)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1910681093:i=302:sd=2:bd=preordered:rtra=on:ss=axioms_2948 on theBenchmark for (2948ds/302Mi)
% 41.96/6.48 % (1390881)Instruction limit reached!
% 41.96/6.48 % (1390881)------------------------------
% 41.96/6.48 % (1390881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.96/6.48 % (1390881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.96/6.48 % (1390881)CaDiCaL version: 2.1.3
% 41.96/6.48 % (1390881)Termination reason: Instruction limit
% 41.96/6.48 % (1390881)Termination phase: Saturation
% 41.96/6.48 % (1390881)Time elapsed: 0.067 s
% 41.96/6.48 % (1390881)Peak memory usage: 13 MB
% 41.96/6.48 % (1390881)Instructions burned: 71 (million)
% 41.96/6.48 % (1390879)Instruction limit reached!
% 41.96/6.48 % (1390879)------------------------------
% 41.96/6.48 % (1390879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.96/6.48 % (1390879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.96/6.48 % (1390879)CaDiCaL version: 2.1.3
% 41.96/6.48 % (1390879)Termination reason: Instruction limit
% 41.96/6.48 % (1390879)Termination phase: Saturation
% 41.96/6.48 % (1390879)Time elapsed: 0.202 s
% 41.96/6.48 % (1390879)Peak memory usage: 14 MB
% 41.96/6.48 % (1390879)Instructions burned: 446 (million)
% 41.96/6.48 % (1390886)lrs+10_1_sil=128000:fde=none:cnfonf=off:si=on:uwa=off:random_seed=2750819384:s2a=on:i=4980:sd=2:bd=all:rtra=on:ss=axioms:ntd=on_2947 on theBenchmark for (2947ds/4980Mi)
% 41.96/6.48 % (1390888)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 41.96/6.48 % (1390888)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 41.96/6.48 % (1390888)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2476473704:i=100:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2947 on theBenchmark for (2947ds/100Mi)
% 41.96/6.48 % (1390877)Instruction limit reached!
% 41.96/6.48 % (1390877)------------------------------
% 41.96/6.48 % (1390877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.96/6.48 % (1390877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.96/6.48 % (1390877)CaDiCaL version: 2.1.3
% 41.96/6.48 % (1390877)Termination reason: Instruction limit
% 41.96/6.48 % (1390877)Termination phase: Saturation
% 41.96/6.48 % (1390877)Time elapsed: 0.411 s
% 41.96/6.48 % (1390877)Peak memory usage: 13 MB
% 41.96/6.48 % (1390877)Instructions burned: 479 (million)
% 41.96/6.48 % (1390888)Instruction limit reached!
% 41.96/6.48 % (1390888)------------------------------
% 41.96/6.48 % (1390888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.96/6.48 % (1390888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.96/6.48 % (1390888)CaDiCaL version: 2.1.3
% 41.96/6.48 % (1390888)Termination reason: Instruction limit
% 41.96/6.48 % (1390888)Termination phase: Saturation
% 41.96/6.48 % (1390888)Time elapsed: 0.047 s
% 41.96/6.48 % (1390888)Peak memory usage: 12 MB
% 41.96/6.48 % (1390888)Instructions burned: 100 (million)
% 41.96/6.48 % (1390892)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=1895753797:i=76:piset=equals:rtra=on:ntd=on_2947 on theBenchmark for (2947ds/76Mi)
% 41.96/6.48 % (1390894)lrs+10_1_to=lpo:sil=128000:cnfonf=off:si=on:sp=unary_first:sos=all:spb=goal:uwa=off:random_seed=1771743523:i=289:rtra=on_2947 on theBenchmark for (2947ds/289Mi)
% 41.96/6.48 % (1390892)Instruction limit reached!
% 41.96/6.48 % (1390892)------------------------------
% 41.96/6.48 % (1390892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.96/6.48 % (1390892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.96/6.48 % (1390892)CaDiCaL version: 2.1.3
% 41.96/6.48 % (1390892)Termination reason: Instruction limit
% 41.96/6.48 % (1390892)Termination phase: Saturation
% 41.96/6.48 % (1390892)Time elapsed: 0.040 s
% 47.85/7.14 % (1390892)Peak memory usage: 12 MB
% 47.85/7.14 % (1390892)Instructions burned: 76 (million)
% 47.85/7.14 % (1390897)lrs+2_64_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_first:bsr=unit_only:cbe=off:uwa=interpreted_only:nwc=0.5:slsqc=5:sac=on:slsq=on:random_seed=3716603387:i=493:s2at=5:kws=frequency:doe=on:rtra=on:er=known_2946 on theBenchmark for (2946ds/493Mi)
% 47.85/7.14 % (1390894)Instruction limit reached!
% 47.85/7.14 % (1390894)------------------------------
% 47.85/7.14 % (1390894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.85/7.14 % (1390894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.85/7.14 % (1390894)CaDiCaL version: 2.1.3
% 47.85/7.14 % (1390894)Termination reason: Instruction limit
% 47.85/7.14 % (1390894)Termination phase: Saturation
% 47.85/7.14 % (1390894)Time elapsed: 0.131 s
% 47.85/7.14 % (1390894)Peak memory usage: 12 MB
% 47.85/7.14 % (1390894)Instructions burned: 290 (million)
% 47.85/7.14 % (1390883)Instruction limit reached!
% 47.85/7.14 % (1390883)------------------------------
% 47.85/7.14 % (1390883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.85/7.14 % (1390883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.85/7.14 % (1390883)CaDiCaL version: 2.1.3
% 47.85/7.14 % (1390883)Termination reason: Instruction limit
% 47.85/7.14 % (1390883)Termination phase: Saturation
% 47.85/7.14 % (1390883)Time elapsed: 0.275 s
% 47.85/7.14 % (1390883)Peak memory usage: 13 MB
% 47.85/7.14 % (1390883)Instructions burned: 302 (million)
% 47.85/7.14 % (1390899)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=534844471:cond=on:i=34:hud=10:nm=10:rtra=on_2945 on theBenchmark for (2945ds/34Mi)
% 47.85/7.14 % (1390900)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 47.85/7.14 % (1390900)dis+1010_1_to=lpo:irw=on:plsq=on:drc=ordering:plsqc=4:cnfonf=lazy_simp:si=on:sp=reverse_frequency:sos=on:plsqr=32,1:cbe=off:uwa=off:rp=on:lwlo=on:random_seed=3846087509:i=372:add=off:piset=or:nm=10:fsr=off:rtra=on:c=on_2945 on theBenchmark for (2945ds/372Mi)
% 47.85/7.14 % (1390899)Instruction limit reached!
% 47.85/7.14 % (1390899)------------------------------
% 47.85/7.14 % (1390899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.85/7.14 % (1390899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.85/7.14 % (1390899)CaDiCaL version: 2.1.3
% 47.85/7.14 % (1390899)Termination reason: Instruction limit
% 47.85/7.14 % (1390899)Termination phase: Saturation
% 47.85/7.14 % (1390899)Time elapsed: 0.031 s
% 47.85/7.14 % (1390899)Peak memory usage: 12 MB
% 47.85/7.14 % (1390899)Instructions burned: 34 (million)
% 47.85/7.14 % (1390905)lrs+1002_1024_sil=128000:tgt=ground:e2e=on:si=on:uwa=interpreted_only:fd=off:nwc=1:random_seed=3094471294:cts=off:avsq=on:i=670:avsqr=1,16:nm=16:rtra=on_2944 on theBenchmark for (2944ds/670Mi)
% 47.85/7.14 % (1390897)Instruction limit reached!
% 47.85/7.14 % (1390897)------------------------------
% 47.85/7.14 % (1390897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.85/7.14 % (1390897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.85/7.14 % (1390897)CaDiCaL version: 2.1.3
% 47.85/7.14 % (1390897)Termination reason: Instruction limit
% 47.85/7.14 % (1390897)Termination phase: Saturation
% 47.85/7.14 % (1390897)Time elapsed: 0.210 s
% 47.85/7.14 % (1390897)Peak memory usage: 12 MB
% 47.85/7.14 % (1390897)Instructions burned: 497 (million)
% 47.85/7.14 % (1390907)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1726997681:hsq=on:st=2:i=647:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2944 on theBenchmark for (2944ds/647Mi)
% 47.85/7.14 % (1390900)Instruction limit reached!
% 47.85/7.14 % (1390900)------------------------------
% 47.85/7.14 % (1390900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.85/7.14 % (1390900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.85/7.14 % (1390900)CaDiCaL version: 2.1.3
% 47.85/7.14 % (1390900)Termination reason: Instruction limit
% 47.85/7.14 % (1390900)Termination phase: Saturation
% 47.85/7.14 % (1390900)Time elapsed: 0.308 s
% 47.85/7.14 % (1390900)Peak memory usage: 12 MB
% 47.85/7.14 % (1390900)Instructions burned: 373 (million)
% 47.85/7.14 % (1390727)Instruction limit reached!
% 47.85/7.14 % (1390727)------------------------------
% 47.85/7.14 % (1390727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.01/7.56 % (1390727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.01/7.56 % (1390727)CaDiCaL version: 2.1.3
% 50.01/7.56 % (1390727)Termination reason: Instruction limit
% 50.01/7.56 % (1390727)Termination phase: Saturation
% 50.01/7.56 % (1390727)Time elapsed: 4.489 s
% 50.01/7.56 % (1390727)Peak memory usage: 26 MB
% 50.01/7.56 % (1390727)Instructions burned: 5756 (million)
% 50.01/7.56 % (1390835)Instruction limit reached!
% 50.01/7.56 % (1390835)------------------------------
% 50.01/7.56 % (1390835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.01/7.56 % (1390835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.01/7.56 % (1390835)CaDiCaL version: 2.1.3
% 50.01/7.56 % (1390835)Termination reason: Instruction limit
% 50.01/7.56 % (1390835)Termination phase: Saturation
% 50.01/7.56 % (1390835)Time elapsed: 2.052 s
% 50.01/7.56 % (1390835)Peak memory usage: 20 MB
% 50.01/7.56 % (1390835)Instructions burned: 2470 (million)
% 50.01/7.56 % (1390911)dis+10_128_sil=128000:tgt=full:plsq=on:plsqc=3:cnfonf=off:si=on:sp=arity:spb=goal_then_units:uwa=one_side_interpreted:nwc=1.5:random_seed=509199418:i=857:add=off:kws=frequency:rtra=on:ntd=on_2941 on theBenchmark for (2941ds/857Mi)
% 50.01/7.56 % (1390907)Instruction limit reached!
% 50.01/7.56 % (1390907)------------------------------
% 50.01/7.56 % (1390907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.01/7.56 % (1390907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.01/7.56 % (1390907)CaDiCaL version: 2.1.3
% 50.01/7.56 % (1390907)Termination reason: Instruction limit
% 50.01/7.56 % (1390907)Termination phase: Saturation
% 50.01/7.56 % (1390907)Time elapsed: 0.284 s
% 50.01/7.56 % (1390907)Peak memory usage: 13 MB
% 50.01/7.56 % (1390907)Instructions burned: 648 (million)
% 50.01/7.56 % (1390912)dis+1010_4_anc=all_dependent:to=lpo:sil=128000:fde=unused:cnfonf=conj_eager:si=on:sp=reverse_frequency:lma=off:spb=intro:cbe=off:uwa=off:random_seed=1342457717:i=693:add=off:fsr=off:rtra=on:fe=abstraction:ntd=on_2941 on theBenchmark for (2941ds/693Mi)
% 50.01/7.56 % (1390916)WARNING Broken Constraint: if ho_split_queue_ratios(23,10) has been set then ho_split_queue(off) is equal to on
% 50.01/7.56 % (1390916)dis+1002_50_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=1:si=on:sp=occurrence:plsqr=64,1:nwc=3:flr=on:chr=on:random_seed=3848911529:hsqr=23,10:uwa_fpi=on:i=52:kws=frequency:hud=15:fsr=off:rtra=on:amm=off:ntd=on:rawr=on_2941 on theBenchmark for (2941ds/52Mi)
% 50.01/7.56 % (1390914)dis+10_7_sil=128000:cnfonf=lazy_gen:si=on:sos=on:random_seed=644833479:i=285:hud=10:bd=all:rtra=on:ss=axioms_2941 on theBenchmark for (2941ds/285Mi)
% 50.01/7.56 % (1390916)Instruction limit reached!
% 50.01/7.56 % (1390916)------------------------------
% 50.01/7.56 % (1390916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.01/7.56 % (1390916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.01/7.56 % (1390916)CaDiCaL version: 2.1.3
% 50.01/7.56 % (1390916)Termination reason: Instruction limit
% 50.01/7.56 % (1390916)Termination phase: Saturation
% 50.01/7.56 % (1390916)Time elapsed: 0.026 s
% 50.01/7.56 % (1390916)Peak memory usage: 12 MB
% 50.01/7.56 % (1390916)Instructions burned: 54 (million)
% 50.01/7.56 % (1390921)dis+10_1_si=on:random_seed=1491630879:i=407:sd=4:rtra=on:ss=axioms:sgt=20_2940 on theBenchmark for (2940ds/407Mi)
% 50.01/7.56 % (1390921)Instruction limit reached!
% 50.01/7.56 % (1390921)------------------------------
% 50.01/7.56 % (1390921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.01/7.56 % (1390921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.01/7.56 % (1390921)CaDiCaL version: 2.1.3
% 50.01/7.56 % (1390921)Termination reason: Instruction limit
% 50.01/7.56 % (1390921)Termination phase: Saturation
% 50.01/7.56 % (1390921)Time elapsed: 0.184 s
% 50.01/7.56 % (1390921)Peak memory usage: 13 MB
% 50.01/7.56 % (1390921)Instructions burned: 408 (million)
% 50.01/7.56 % (1390914)Instruction limit reached!
% 50.01/7.56 % (1390914)------------------------------
% 50.01/7.56 % (1390914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.01/7.56 % (1390914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.01/7.56 % (1390914)CaDiCaL version: 2.1.3
% 50.01/7.56 % (1390914)Termination reason: Instruction limit
% 50.01/7.56 % (1390914)Termination phase: Saturation
% 50.01/7.56 % (1390914)Time elapsed: 0.235 s
% 50.01/7.56 % (1390914)Peak memory usage: 13 MB
% 51.42/7.95 % (1390914)Instructions burned: 285 (million)
% 51.42/7.95 % (1390923)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=4031127765:i=2240:bs=unit_only:ins=25:rtra=on:ntd=on_2938 on theBenchmark for (2938ds/2240Mi)
% 51.42/7.95 % (1390924)lrs+10_1_sil=128000:e2e=on:si=on:uwa=interpreted_only:random_seed=3262746333:st=2:i=336:sd=1:rtra=on:ss=axioms:ntd=on_2938 on theBenchmark for (2938ds/336Mi)
% 51.42/7.95 % (1390905)Instruction limit reached!
% 51.42/7.95 % (1390905)------------------------------
% 51.42/7.95 % (1390905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.42/7.95 % (1390905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.42/7.95 % (1390905)CaDiCaL version: 2.1.3
% 51.42/7.95 % (1390905)Termination reason: Instruction limit
% 51.42/7.95 % (1390905)Termination phase: Saturation
% 51.42/7.95 % (1390905)Time elapsed: 0.602 s
% 51.42/7.95 % (1390905)Peak memory usage: 13 MB
% 51.42/7.95 % (1390905)Instructions burned: 671 (million)
% 51.42/7.95 % (1390927)lrs+10_1_to=lpo:sil=128000:fde=none:cnfonf=off:si=on:sp=unary_first:urr=on:uwa=one_side_constant:random_seed=4148971935:s2a=on:i=1142:s2at=3:bd=all:rtra=on_2938 on theBenchmark for (2938ds/1142Mi)
% 51.42/7.95 % (1390912)Instruction limit reached!
% 51.42/7.95 % (1390912)------------------------------
% 51.42/7.95 % (1390912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.42/7.95 % (1390912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.42/7.95 % (1390912)CaDiCaL version: 2.1.3
% 51.42/7.95 % (1390912)Termination reason: Instruction limit
% 51.42/7.95 % (1390912)Termination phase: Saturation
% 51.42/7.95 % (1390912)Time elapsed: 0.558 s
% 51.42/7.95 % (1390912)Peak memory usage: 14 MB
% 51.42/7.95 % (1390912)Instructions burned: 693 (million)
% 51.42/7.95 % (1390924)Instruction limit reached!
% 51.42/7.95 % (1390924)------------------------------
% 51.42/7.95 % (1390924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.42/7.95 % (1390924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.42/7.95 % (1390924)CaDiCaL version: 2.1.3
% 51.42/7.95 % (1390924)Termination reason: Instruction limit
% 51.42/7.95 % (1390924)Termination phase: Saturation
% 51.42/7.95 % (1390924)Time elapsed: 0.284 s
% 51.42/7.95 % (1390924)Peak memory usage: 13 MB
% 51.42/7.95 % (1390924)Instructions burned: 336 (million)
% 51.42/7.95 % (1390930)dis+1002_1_sil=128000:si=on:uwa=off:random_seed=2361366540:st=3:i=376:sd=4:rtra=on:ss=axioms:ntd=on_2935 on theBenchmark for (2935ds/376Mi)
% 51.42/7.95 % (1390931)dis+1002_4:1_anc=none:sil=128000:sas=cadical:si=on:sp=weighted_frequency:sos=on:uwa=one_side_interpreted:random_seed=2610705525:i=766:bd=all:rtra=on_2935 on theBenchmark for (2935ds/766Mi)
% 51.42/7.95 % (1390911)Instruction limit reached!
% 51.42/7.95 % (1390911)------------------------------
% 51.42/7.95 % (1390911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.42/7.95 % (1390911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.42/7.95 % (1390911)CaDiCaL version: 2.1.3
% 51.42/7.95 % (1390911)Termination reason: Instruction limit
% 51.42/7.95 % (1390911)Termination phase: Saturation
% 51.42/7.95 % (1390911)Time elapsed: 0.730 s
% 51.42/7.95 % (1390911)Peak memory usage: 16 MB
% 51.42/7.95 % (1390911)Instructions burned: 858 (million)
% 51.42/7.95 % (1390937)WARNING Broken Constraint: if avatar_split_queue_cutoffs(4) has been set then avatar_split_queue(off) is equal to on
% 51.42/7.95 % (1390937)lrs+10_1_to=kbo:si=on:sp=const_frequency:sos=on:spb=non_intro:uwa=hol:avsqc=4:random_seed=1597605892:st=3:uwa_fpi=on:i=959:fgj=on:piset=pi_sigma:hud=5:nm=16:rtra=on:fe=abstraction:ss=axioms:ixr=off:ntd=on_2934 on theBenchmark for (2934ds/959Mi)
% 51.42/7.95 % (1390930)Instruction limit reached!
% 51.42/7.95 % (1390930)------------------------------
% 51.42/7.95 % (1390930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.42/7.95 % (1390930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.42/7.95 % (1390930)CaDiCaL version: 2.1.3
% 51.42/7.95 % (1390930)Termination reason: Instruction limit
% 51.42/7.95 % (1390930)Termination phase: Saturation
% 51.42/7.95 % (1390930)Time elapsed: 0.297 s
% 51.42/7.95 % (1390930)Peak memory usage: 13 MB
% 51.42/7.95 % (1390930)Instructions burned: 377 (million)
% 51.42/7.95 % (1390939)dis+1010_1024_sil=128000:plsq=on:plsqc=1:e2e=on:si=on:lma=off:plsqr=64,1:uwa=interpreted_only:fd=off:random_seed=1360314465:i=6359:add=on:kws=inv_frequency:aac=none:rtra=on:c=on:er=filter:ntd=on_2932 on theBenchmark for (2932ds/6359Mi)
% 54.82/8.23 % (1390758)Instruction limit reached!
% 54.82/8.23 % (1390758)------------------------------
% 54.82/8.23 % (1390758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.82/8.23 % (1390758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.82/8.23 % (1390758)CaDiCaL version: 2.1.3
% 54.82/8.23 % (1390758)Termination reason: Instruction limit
% 54.82/8.23 % (1390758)Termination phase: Saturation
% 54.82/8.23 % (1390758)Time elapsed: 5.321 s
% 54.82/8.23 % (1390758)Peak memory usage: 12 MB
% 54.82/8.23 % (1390758)Instructions burned: 9842 (million)
% 54.82/8.23 % (1390927)Instruction limit reached!
% 54.82/8.23 % (1390927)------------------------------
% 54.82/8.23 % (1390927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.82/8.23 % (1390927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.82/8.23 % (1390927)CaDiCaL version: 2.1.3
% 54.82/8.23 % (1390927)Termination reason: Instruction limit
% 54.82/8.23 % (1390927)Termination phase: Saturation
% 54.82/8.23 % (1390927)Time elapsed: 0.935 s
% 54.82/8.23 % (1390927)Peak memory usage: 17 MB
% 54.82/8.23 % (1390927)Instructions burned: 1143 (million)
% 54.82/8.23 % (1390931)Instruction limit reached!
% 54.82/8.23 % (1390931)------------------------------
% 54.82/8.23 % (1390931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.82/8.23 % (1390931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.82/8.23 % (1390931)CaDiCaL version: 2.1.3
% 54.82/8.23 % (1390931)Termination reason: Instruction limit
% 54.82/8.23 % (1390931)Termination phase: Saturation
% 54.82/8.23 % (1390931)Time elapsed: 0.650 s
% 54.82/8.23 % (1390931)Peak memory usage: 14 MB
% 54.82/8.23 % (1390931)Instructions burned: 767 (million)
% 54.82/8.23 % (1390945)dis+21_1_sil=128000:tgt=full:fde=none:e2e=on:si=on:urr=on:uwa=interpreted_only:s2agt=32:sac=on:random_seed=2763088485:s2a=on:i=876:s2at=6:nm=2:rtra=on_2928 on theBenchmark for (2928ds/876Mi)
% 54.82/8.23 % (1390943)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3155506440:st=4:i=35:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2928 on theBenchmark for (2928ds/35Mi)
% 54.82/8.23 % (1390944)dis+10_1_sfv=off:sil=128000:cnfonf=lazy_gen:si=on:uwa=off:nwc=1:chr=on:random_seed=4180591442:hsq=on:hsqr=1,8:i=53:hsql=off:bd=all:rtra=on:ixr=off_2928 on theBenchmark for (2928ds/53Mi)
% 54.82/8.23 % (1390923)Instruction limit reached!
% 54.82/8.23 % (1390923)------------------------------
% 54.82/8.23 % (1390923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.82/8.23 % (1390923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.82/8.23 % (1390923)CaDiCaL version: 2.1.3
% 54.82/8.23 % (1390923)Termination reason: Instruction limit
% 54.82/8.23 % (1390923)Termination phase: Saturation
% 54.82/8.23 % (1390923)Time elapsed: 1.038 s
% 54.82/8.23 % (1390923)Peak memory usage: 28 MB
% 54.82/8.23 % (1390923)Instructions burned: 2242 (million)
% 54.82/8.23 % (1390943)Instruction limit reached!
% 54.82/8.23 % (1390943)------------------------------
% 54.82/8.23 % (1390943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.82/8.23 % (1390943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.82/8.23 % (1390943)CaDiCaL version: 2.1.3
% 54.82/8.23 % (1390943)Termination reason: Instruction limit
% 54.82/8.23 % (1390943)Termination phase: Saturation
% 54.82/8.23 % (1390943)Time elapsed: 0.033 s
% 54.82/8.23 % (1390943)Peak memory usage: 12 MB
% 54.82/8.23 % (1390943)Instructions burned: 35 (million)
% 54.82/8.23 % (1390951)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 54.82/8.23 % (1390951)dis+1002_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_min:sos=on:fd=preordered:slsqc=2:chr=on:random_seed=322803039:i=306:bd=all:rtra=on_2928 on theBenchmark for (2928ds/306Mi)
% 54.82/8.23 % (1390944)Instruction limit reached!
% 54.82/8.23 % (1390944)------------------------------
% 54.82/8.23 % (1390944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.82/8.23 % (1390944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.82/8.23 % (1390944)CaDiCaL version: 2.1.3
% 54.82/8.23 % (1390944)Termination reason: Instruction limit
% 54.82/8.23 % (1390944)Termination phase: Saturation
% 54.82/8.23 % (1390944)Time elapsed: 0.049 s
% 56.36/8.53 % (1390944)Peak memory usage: 12 MB
% 56.36/8.53 % (1390944)Instructions burned: 53 (million)
% 56.36/8.53 % (1390950)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=4282314678:i=57:ep=R:rtra=on:ntd=on_2928 on theBenchmark for (2928ds/57Mi)
% 56.36/8.53 % (1390954)dis+10_8:1_sil=128000:si=on:uwa=off:random_seed=2141661362:i=262:sd=2:bd=preordered:rtra=on:ss=axioms:sgt=8_2927 on theBenchmark for (2927ds/262Mi)
% 56.36/8.53 % (1390950)Instruction limit reached!
% 56.36/8.53 % (1390950)------------------------------
% 56.36/8.53 % (1390950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.36/8.53 % (1390950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.36/8.53 % (1390950)CaDiCaL version: 2.1.3
% 56.36/8.53 % (1390950)Termination reason: Instruction limit
% 56.36/8.53 % (1390950)Termination phase: Saturation
% 56.36/8.53 % (1390950)Time elapsed: 0.053 s
% 56.36/8.53 % (1390950)Peak memory usage: 12 MB
% 56.36/8.53 % (1390950)Instructions burned: 58 (million)
% 56.36/8.53 % (1390957)WARNING Broken Constraint: if ho_split_queue_ratios(1,3) has been set then ho_split_queue(off) is equal to on
% 56.36/8.53 % (1390957)ott+1002_16_sil=128000:si=on:random_seed=636487876:hsqr=1,3:i=409:add=on:rtra=on:fe=abstraction_2927 on theBenchmark for (2927ds/409Mi)
% 56.36/8.53 % (1390951)Instruction limit reached!
% 56.36/8.53 % (1390951)------------------------------
% 56.36/8.53 % (1390951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.36/8.53 % (1390951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.36/8.53 % (1390951)CaDiCaL version: 2.1.3
% 56.36/8.53 % (1390951)Termination reason: Instruction limit
% 56.36/8.53 % (1390951)Termination phase: Saturation
% 56.36/8.53 % (1390951)Time elapsed: 0.144 s
% 56.36/8.53 % (1390951)Peak memory usage: 13 MB
% 56.36/8.53 % (1390951)Instructions burned: 307 (million)
% 56.36/8.53 % (1390960)dis+10_1_sil=128000:plsq=on:si=on:plsqr=32,1:uwa=off:random_seed=2954865885:s2a=on:i=381:rtra=on_2926 on theBenchmark for (2926ds/381Mi)
% 56.36/8.53 % (1390937)Instruction limit reached!
% 56.36/8.53 % (1390937)------------------------------
% 56.36/8.53 % (1390937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.36/8.53 % (1390937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.36/8.53 % (1390937)CaDiCaL version: 2.1.3
% 56.36/8.53 % (1390937)Termination reason: Instruction limit
% 56.36/8.53 % (1390937)Termination phase: Saturation
% 56.36/8.53 % (1390937)Time elapsed: 0.825 s
% 56.36/8.53 % (1390937)Peak memory usage: 18 MB
% 56.36/8.53 % (1390937)Instructions burned: 959 (million)
% 56.36/8.53 % (1390963)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=909630116:cond=on:i=324:rtra=on:ntd=on_2925 on theBenchmark for (2925ds/324Mi)
% 56.36/8.53 % (1390954)Instruction limit reached!
% 56.36/8.53 % (1390954)------------------------------
% 56.36/8.53 % (1390954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.36/8.53 % (1390954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.36/8.53 % (1390954)CaDiCaL version: 2.1.3
% 56.36/8.53 % (1390954)Termination reason: Instruction limit
% 56.36/8.53 % (1390954)Termination phase: Saturation
% 56.36/8.53 % (1390954)Time elapsed: 0.220 s
% 56.36/8.53 % (1390954)Peak memory usage: 13 MB
% 56.36/8.53 % (1390954)Instructions burned: 262 (million)
% 56.36/8.53 % (1390965)lrs+10_1_sil=128000:fde=none:si=on:sos=on:spb=goal_then_units:urr=on:random_seed=1558832039:i=240:kws=inv_precedence:rtra=on_2925 on theBenchmark for (2925ds/240Mi)
% 56.36/8.53 % (1390960)Instruction limit reached!
% 56.36/8.53 % (1390960)------------------------------
% 56.36/8.53 % (1390960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.36/8.53 % (1390960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.36/8.53 % (1390960)CaDiCaL version: 2.1.3
% 56.36/8.53 % (1390960)Termination reason: Instruction limit
% 56.36/8.53 % (1390960)Termination phase: Saturation
% 56.36/8.53 % (1390960)Time elapsed: 0.210 s
% 56.36/8.53 % (1390960)Peak memory usage: 13 MB
% 56.36/8.53 % (1390960)Instructions burned: 383 (million)
% 56.36/8.53 % (1390967)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 56.36/8.53 % (1390967)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2756147995:cts=off:uwa_fpi=on:i=124:av=off:fsr=off:rtra=on:ntd=on_2924 on theBenchmark for (2924ds/124Mi)
% 57.27/8.66 % (1390957)Instruction limit reached!
% 57.27/8.66 % (1390957)------------------------------
% 57.27/8.66 % (1390957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390957)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390957)Termination reason: Instruction limit
% 57.27/8.66 % (1390957)Termination phase: Saturation
% 57.27/8.66 % (1390957)Time elapsed: 0.351 s
% 57.27/8.66 % (1390957)Peak memory usage: 13 MB
% 57.27/8.66 % (1390957)Instructions burned: 409 (million)
% 57.27/8.66 % (1390970)lrs+1010_2_to=lpo:cnfonf=off:e2e=on:si=on:random_seed=4053568976:uwa_fpi=on:i=223:bd=all:rtra=on:fe=abstraction:ntd=on_2923 on theBenchmark for (2923ds/223Mi)
% 57.27/8.66 % (1390965)Instruction limit reached!
% 57.27/8.66 % (1390965)------------------------------
% 57.27/8.66 % (1390965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390965)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390965)Termination reason: Instruction limit
% 57.27/8.66 % (1390965)Termination phase: Saturation
% 57.27/8.66 % (1390965)Time elapsed: 0.208 s
% 57.27/8.66 % (1390965)Peak memory usage: 13 MB
% 57.27/8.66 % (1390965)Instructions burned: 240 (million)
% 57.27/8.66 % (1390973)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1545259188:s2a=on:i=282:kws=inv_frequency:bd=all:rtra=on_2922 on theBenchmark for (2922ds/282Mi)
% 57.27/8.66 % (1390963)Instruction limit reached!
% 57.27/8.66 % (1390963)------------------------------
% 57.27/8.66 % (1390963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390963)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390963)Termination reason: Instruction limit
% 57.27/8.66 % (1390963)Termination phase: Saturation
% 57.27/8.66 % (1390963)Time elapsed: 0.270 s
% 57.27/8.66 % (1390963)Peak memory usage: 12 MB
% 57.27/8.66 % (1390963)Instructions burned: 325 (million)
% 57.27/8.66 % (1390967)Instruction limit reached!
% 57.27/8.66 % (1390967)------------------------------
% 57.27/8.66 % (1390967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390967)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390967)Termination reason: Instruction limit
% 57.27/8.66 % (1390967)Termination phase: Saturation
% 57.27/8.66 % (1390967)Time elapsed: 0.134 s
% 57.27/8.66 % (1390967)Peak memory usage: 12 MB
% 57.27/8.66 % (1390967)Instructions burned: 125 (million)
% 57.27/8.66 % (1390975)lrs+10_1_sil=128000:tgt=ground:cnfonf=conj_eager:si=on:random_seed=2303965778:s2a=on:i=464:kws=frequency:bd=all:rtra=on:ss=axioms_2922 on theBenchmark for (2922ds/464Mi)
% 57.27/8.66 % (1390976)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=816117174:i=88:s2at=3:nm=2:rtra=on:rawr=on_2922 on theBenchmark for (2922ds/88Mi)
% 57.27/8.66 % (1390976)Instruction limit reached!
% 57.27/8.66 % (1390976)------------------------------
% 57.27/8.66 % (1390976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390976)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390976)Termination reason: Instruction limit
% 57.27/8.66 % (1390976)Termination phase: Saturation
% 57.27/8.66 % (1390976)Time elapsed: 0.081 s
% 57.27/8.66 % (1390976)Peak memory usage: 13 MB
% 57.27/8.66 % (1390976)Instructions burned: 89 (million)
% 57.27/8.66 % (1390970)Instruction limit reached!
% 57.27/8.66 % (1390970)------------------------------
% 57.27/8.66 % (1390970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390970)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390970)Termination reason: Instruction limit
% 57.27/8.66 % (1390970)Termination phase: Saturation
% 57.27/8.66 % (1390970)Time elapsed: 0.189 s
% 57.27/8.66 % (1390970)Peak memory usage: 13 MB
% 57.27/8.66 % (1390970)Instructions burned: 224 (million)
% 57.27/8.66 % (1390945)Instruction limit reached!
% 57.27/8.66 % (1390945)------------------------------
% 57.27/8.66 % (1390945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390945)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390945)Termination reason: Instruction limit
% 57.27/8.66 % (1390945)Termination phase: Saturation
% 57.27/8.66 % (1390945)Time elapsed: 0.730 s
% 57.27/8.66 % (1390945)Peak memory usage: 14 MB
% 57.27/8.66 % (1390945)Instructions burned: 878 (million)
% 57.27/8.66 % (1390979)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=2554150511:s2a=on:cond=on:i=280:add=on:bd=preordered:rtra=on:er=filter_2921 on theBenchmark for (2921ds/280Mi)
% 57.27/8.66 % (1390980)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 57.27/8.66 % (1390980)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2751561549:i=4386:hud=10:nm=16:av=off:rtra=on:ntd=on_2921 on theBenchmark for (2921ds/4386Mi)
% 57.27/8.66 % (1390981)WARNING Broken Constraint: if lookahaed_delay(10) has been set then selection(21) is not lookahead selection
% 57.27/8.66 % (1390981)WARNING Broken Constraint: if mono_ep(off) has been set then equality_proxy(off) is not equal to off
% 57.27/8.66 % (1390981)ott+21_3:13_sil=128000:cnfonf=off:sas=cadical:si=on:sp=arity:lma=off:lsd=10:uwa=one_side_interpreted:mep=off:chr=on:random_seed=447018919:hsq=on:st=2:i=483:sd=1:hsql=off:rtra=on:fe=abstraction:fdi=32:ss=axioms:sgt=20:ntd=on_2921 on theBenchmark for (2921ds/483Mi)
% 57.27/8.66 % (1390973)Instruction limit reached!
% 57.27/8.66 % (1390973)------------------------------
% 57.27/8.66 % (1390973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390973)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390973)Termination reason: Instruction limit
% 57.27/8.66 % (1390973)Termination phase: Saturation
% 57.27/8.66 % (1390973)Time elapsed: 0.190 s
% 57.27/8.66 % (1390973)Peak memory usage: 14 MB
% 57.27/8.66 % (1390973)Instructions burned: 283 (million)
% 57.27/8.66 % (1390985)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=562966305:i=73:rtra=on_2920 on theBenchmark for (2920ds/73Mi)
% 57.27/8.66 % (1390985)Instruction limit reached!
% 57.27/8.66 % (1390985)------------------------------
% 57.27/8.66 % (1390985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390985)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390985)Termination reason: Instruction limit
% 57.27/8.66 % (1390985)Termination phase: Saturation
% 57.27/8.66 % (1390985)Time elapsed: 0.065 s
% 57.27/8.66 % (1390985)Peak memory usage: 12 MB
% 57.27/8.66 % (1390985)Instructions burned: 74 (million)
% 57.27/8.66 % (1390987)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2714121360:cts=off:i=176:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2919 on theBenchmark for (2919ds/176Mi)
% 57.27/8.66 % (1390979)Instruction limit reached!
% 57.27/8.66 % (1390979)------------------------------
% 57.27/8.66 % (1390979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390979)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390979)Termination reason: Instruction limit
% 57.27/8.66 % (1390979)Termination phase: Saturation
% 57.27/8.66 % (1390979)Time elapsed: 0.249 s
% 57.27/8.66 % (1390979)Peak memory usage: 13 MB
% 57.27/8.66 % (1390979)Instructions burned: 280 (million)
% 57.27/8.66 % (1390975)Instruction limit reached!
% 57.27/8.66 % (1390975)------------------------------
% 57.27/8.66 % (1390975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390975)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390975)Termination reason: Instruction limit
% 57.27/8.66 % (1390975)Termination phase: Saturation
% 57.27/8.66 % (1390975)Time elapsed: 0.401 s
% 57.27/8.66 % (1390975)Peak memory usage: 14 MB
% 57.27/8.66 % (1390975)Instructions burned: 464 (million)
% 57.27/8.66 % (1390989)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 57.27/8.66 % (1390989)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=1415229815:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2918 on theBenchmark for (2918ds/39Mi)
% 57.27/8.66 % (1390987)Instruction limit reached!
% 57.27/8.66 % (1390987)------------------------------
% 57.27/8.66 % (1390987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390987)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390987)Termination reason: Instruction limit
% 57.27/8.66 % (1390987)Termination phase: Saturation
% 57.27/8.66 % (1390987)Time elapsed: 0.152 s
% 57.27/8.66 % (1390987)Peak memory usage: 13 MB
% 57.27/8.66 % (1390987)Instructions burned: 177 (million)
% 57.27/8.66 % (1390990)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3636144572:i=708:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2918 on theBenchmark for (2918ds/708Mi)
% 57.27/8.66 % (1390992)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 57.27/8.66 % (1390989)Instruction limit reached!
% 57.27/8.66 % (1390989)------------------------------
% 57.27/8.66 % (1390989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390989)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390989)Termination reason: Instruction limit
% 57.27/8.66 % (1390989)Termination phase: Saturation
% 57.27/8.66 % (1390989)Time elapsed: 0.035 s
% 57.27/8.66 % (1390989)Peak memory usage: 12 MB
% 57.27/8.66 % (1390989)Instructions burned: 40 (million)
% 57.27/8.66 % (1390992)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=1734448622:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2918 on theBenchmark for (2918ds/252Mi)
% 57.27/8.66 % (1390994)dis+10_4_sil=128000:tgt=full:fde=unused:cnfonf=lazy_not_gen:sas=cadical:si=on:uwa=off:sac=on:random_seed=2901530638:i=823:fsr=off:rtra=on_2917 on theBenchmark for (2917ds/823Mi)
% 57.27/8.66 % (1390992) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1390572-1390992"...
% 57.27/8.66 % (1390992)...printing done.
% 57.27/8.66 % (1390992)Refutation found. Thanks to Tanya!
% 57.27/8.66 % SZS status Theorem for theBenchmark
% 57.27/8.66 % SZS output start Proof for theBenchmark
% 57.27/8.66 thf(type_def_5, type, a: $tType).
% 57.27/8.66 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 57.27/8.66 thf(func_def_3, type, sK0: (a > a > $o)).
% 57.27/8.66 thf(func_def_4, type, sK1: ((a > $o) > a)).
% 57.27/8.66 thf(func_def_5, type, sK2: (a > a)).
% 57.27/8.66 thf(func_def_6, type, sK3: (a > (a > $o) > a)).
% 57.27/8.66 thf(func_def_7, type, sF4: (a > a > $o)).
% 57.27/8.66 thf(func_def_8, type, sF5: (a > a)).
% 57.27/8.66 thf(func_def_9, type, sF6: (a > $o)).
% 57.27/8.66 thf(func_def_10, type, sF7: (a > $o)).
% 57.27/8.66 thf(func_def_11, type, sF8: (a > a > $o)).
% 57.27/8.66 thf(func_def_12, type, sF9: ((a > $o) > a)).
% 57.27/8.66 thf(func_def_13, type, sF10: ((a > $o) > a > $o)).
% 57.27/8.66 thf(func_def_14, type, sF11: (a > (a > $o) > $o)).
% 57.27/8.66 thf(func_def_15, type, sF12: ((a > $o) > a > a)).
% 57.27/8.66 thf(func_def_16, type, sF13: (a > (a > $o) > $o)).
% 57.27/8.66 thf(func_def_17, type, sF14: (a > (a > $o) > $o)).
% 57.27/8.66 thf(func_def_18, type, sF15: (a > (a > $o) > $o)).
% 57.27/8.66 thf(func_def_19, type, vNOT: ($o > $o)).
% 57.27/8.66 thf(func_def_20, type, db0: !>[X0: $tType]:(X0)).
% 57.27/8.66 thf(func_def_21, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 57.27/8.66 thf(f1,conjecture,(
% 57.27/8.66 ! [X0 : (a > a > $o),X1 : ((a > $o) > a)] : ((! [X5 : (a > $o)] : (! [X4 : a] : ((X5 @ X4) => (X0 @ X4 @ (X1 @ X5))) & ! [X6 : a] : (! [X7 : a] : (((X5 @ X7) & (X5 @ X7)) => (X0 @ X7 @ X6)) => ((X0 @ (X1 @ X5) @ X6) & (X0 @ (X1 @ X5) @ X6))) & ! [X4 : a] : ((X5 @ X4) => (X0 @ X4 @ (X1 @ X5)))) & ! [X2 : a,X4 : a,X3 : a] : (((X0 @ X3 @ X4) & (X0 @ X2 @ X3)) => (X0 @ X2 @ X4))) => ! [X8 : (a > a)] : ((! [X3 : a,X2 : a] : ((X0 @ X2 @ X3) => (X0 @ (X8 @ X2) @ (X8 @ X3))) & ! [X3 : a,X2 : a] : ((X0 @ X2 @ X3) => (X0 @ (X8 @ X2) @ (X8 @ X3)))) => ? [X9 : a] : ((X0 @ X9 @ (X8 @ X9)) & (X0 @ (X8 @ X9) @ X9))))),
% 57.27/8.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM145_A_pme)).
% 57.27/8.66 thf(f2,negated_conjecture,(
% 57.27/8.66 ~ ! [X0 : (a > a > $o),X1 : ((a > $o) > a)] : ((! [X5 : (a > $o)] : (! [X4 : a] : ((X5 @ X4) => (X0 @ X4 @ (X1 @ X5))) & ! [X6 : a] : (! [X7 : a] : (((X5 @ X7) & (X5 @ X7)) => (X0 @ X7 @ X6)) => ((X0 @ (X1 @ X5) @ X6) & (X0 @ (X1 @ X5) @ X6))) & ! [X4 : a] : ((X5 @ X4) => (X0 @ X4 @ (X1 @ X5)))) & ! [X2 : a,X4 : a,X3 : a] : (((X0 @ X3 @ X4) & (X0 @ X2 @ X3)) => (X0 @ X2 @ X4))) => ! [X8 : (a > a)] : ((! [X3 : a,X2 : a] : ((X0 @ X2 @ X3) => (X0 @ (X8 @ X2) @ (X8 @ X3))) & ! [X3 : a,X2 : a] : ((X0 @ X2 @ X3) => (X0 @ (X8 @ X2) @ (X8 @ X3)))) => ? [X9 : a] : ((X0 @ X9 @ (X8 @ X9)) & (X0 @ (X8 @ X9) @ X9))))),
% 57.27/8.66 inference(negated_conjecture,[status(cth)],[f1])).
% 57.27/8.66 thf(f3,plain,(
% 57.27/8.66 ~ ! [X0 : (a > a > $o),X1 : ((a > $o) > a)] : ((! [X2 : (a > $o)] : (! [X3 : a] : ((X2 @ X3) => (X0 @ X3 @ (X1 @ X2))) & ! [X4 : a] : (! [X5 : a] : (((X2 @ X5) & (X2 @ X5)) => (X0 @ X5 @ X4)) => ((X0 @ (X1 @ X2) @ X4) & (X0 @ (X1 @ X2) @ X4))) & ! [X6 : a] : ((X2 @ X6) => (X0 @ X6 @ (X1 @ X2)))) & ! [X7 : a,X8 : a,X9 : a] : (((X0 @ X9 @ X8) & (X0 @ X7 @ X9)) => (X0 @ X7 @ X8))) => ! [X10 : (a > a)] : ((! [X11 : a,X12 : a] : ((X0 @ X12 @ X11) => (X0 @ (X10 @ X12) @ (X10 @ X11))) & ! [X13 : a,X14 : a] : ((X0 @ X14 @ X13) => (X0 @ (X10 @ X14) @ (X10 @ X13)))) => ? [X15 : a] : ((X0 @ X15 @ (X10 @ X15)) & (X0 @ (X10 @ X15) @ X15))))),
% 57.27/8.66 inference(rectify,[],[f2])).
% 57.27/8.66 thf(f4,plain,(
% 57.27/8.66 ~ ! [X1 : ((a > $o) > a),X0 : (a > a > $o)] : ((! [X2 : (a > $o)] : (! [X3 : a] : ((((X2 @ X3)) = $true) => (((X0 @ X3 @ (X1 @ X2))) = $true)) & ! [X4 : a] : (! [X5 : a] : (((((X2 @ X5)) = $true) & (((X2 @ X5)) = $true)) => (((X0 @ X5 @ X4)) = $true)) => (($true = ((X0 @ (X1 @ X2) @ X4))) & ($true = ((X0 @ (X1 @ X2) @ X4))))) & ! [X6 : a] : (($true = ((X2 @ X6))) => (((X0 @ X6 @ (X1 @ X2))) = $true))) & ! [X9 : a,X7 : a,X8 : a] : (((((X0 @ X7 @ X9)) = $true) & ($true = ((X0 @ X9 @ X8)))) => (((X0 @ X7 @ X8)) = $true))) => ! [X10 : (a > a)] : ((! [X12 : a,X11 : a] : ((((X0 @ X12 @ X11)) = $true) => ($true = ((X0 @ (X10 @ X12) @ (X10 @ X11))))) & ! [X14 : a,X13 : a] : ((((X0 @ X14 @ X13)) = $true) => (((X0 @ (X10 @ X14) @ (X10 @ X13))) = $true))) => ? [X15 : a] : ((((X0 @ X15 @ (X10 @ X15))) = $true) & ($true = ((X0 @ (X10 @ X15) @ X15))))))),
% 57.27/8.66 inference(fool_elimination,[],[f3])).
% 57.27/8.66 thf(f5,plain,(
% 57.27/8.66 ? [X1 : ((a > $o) > a),X0 : (a > a > $o)] : (? [X10 : (a > a)] : (! [X15 : a] : ((((X0 @ X15 @ (X10 @ X15))) != $true) | ($true != ((X0 @ (X10 @ X15) @ X15)))) & (! [X11 : a,X12 : a] : (($true = ((X0 @ (X10 @ X12) @ (X10 @ X11)))) | (((X0 @ X12 @ X11)) != $true)) & ! [X14 : a,X13 : a] : ((((X0 @ X14 @ X13)) != $true) | (((X0 @ (X10 @ X14) @ (X10 @ X13))) = $true)))) & (! [X2 : (a > $o)] : (! [X3 : a] : ((((X2 @ X3)) != $true) | (((X0 @ X3 @ (X1 @ X2))) = $true)) & ! [X4 : a] : ((($true = ((X0 @ (X1 @ X2) @ X4))) & ($true = ((X0 @ (X1 @ X2) @ X4)))) | ? [X5 : a] : ((((X0 @ X5 @ X4)) != $true) & ((((X2 @ X5)) = $true) & (((X2 @ X5)) = $true)))) & ! [X6 : a] : ((((X0 @ X6 @ (X1 @ X2))) = $true) | ($true != ((X2 @ X6))))) & ! [X9 : a,X7 : a,X8 : a] : ((((X0 @ X7 @ X8)) = $true) | ((((X0 @ X7 @ X9)) != $true) | ($true != ((X0 @ X9 @ X8)))))))),
% 57.27/8.66 inference(ennf_transformation,[],[f4])).
% 57.27/8.66 thf(f6,plain,(
% 57.27/8.66 ? [X0 : (a > a > $o),X1 : ((a > $o) > a)] : (! [X9 : a,X8 : a,X7 : a] : (($true != ((X0 @ X9 @ X8))) | (((X0 @ X7 @ X8)) = $true) | (((X0 @ X7 @ X9)) != $true)) & ? [X10 : (a > a)] : (! [X15 : a] : ((((X0 @ X15 @ (X10 @ X15))) != $true) | ($true != ((X0 @ (X10 @ X15) @ X15)))) & ! [X14 : a,X13 : a] : ((((X0 @ X14 @ X13)) != $true) | (((X0 @ (X10 @ X14) @ (X10 @ X13))) = $true)) & ! [X11 : a,X12 : a] : (($true = ((X0 @ (X10 @ X12) @ (X10 @ X11)))) | (((X0 @ X12 @ X11)) != $true))) & ! [X2 : (a > $o)] : (! [X6 : a] : ((((X0 @ X6 @ (X1 @ X2))) = $true) | ($true != ((X2 @ X6)))) & ! [X4 : a] : (? [X5 : a] : ((((X2 @ X5)) = $true) & (((X2 @ X5)) = $true) & (((X0 @ X5 @ X4)) != $true)) | (($true = ((X0 @ (X1 @ X2) @ X4))) & ($true = ((X0 @ (X1 @ X2) @ X4))))) & ! [X3 : a] : ((((X2 @ X3)) != $true) | (((X0 @ X3 @ (X1 @ X2))) = $true))))),
% 57.27/8.66 inference(flattening,[],[f5])).
% 57.27/8.66 thf(f7,plain,(
% 57.27/8.66 ? [X0 : (a > a > $o),X1 : ((a > $o) > a)] : (! [X2 : a,X3 : a,X4 : a] : ((((X0 @ X2 @ X3)) != $true) | (((X0 @ X4 @ X3)) = $true) | ($true != ((X0 @ X4 @ X2)))) & ? [X5 : (a > a)] : (! [X6 : a] : (($true != ((X0 @ X6 @ (X5 @ X6)))) | (((X0 @ (X5 @ X6) @ X6)) != $true)) & ! [X7 : a,X8 : a] : ((((X0 @ X7 @ X8)) != $true) | ($true = ((X0 @ (X5 @ X7) @ (X5 @ X8))))) & ! [X9 : a,X10 : a] : (($true = ((X0 @ (X5 @ X10) @ (X5 @ X9)))) | (((X0 @ X10 @ X9)) != $true))) & ! [X11 : (a > $o)] : (! [X12 : a] : ((((X0 @ X12 @ (X1 @ X11))) = $true) | (((X11 @ X12)) != $true)) & ! [X13 : a] : (? [X14 : a] : (($true = ((X11 @ X14))) & ($true = ((X11 @ X14))) & (((X0 @ X14 @ X13)) != $true)) | (($true = ((X0 @ (X1 @ X11) @ X13))) & ($true = ((X0 @ (X1 @ X11) @ X13))))) & ! [X15 : a] : ((((X11 @ X15)) != $true) | (((X0 @ X15 @ (X1 @ X11))) = $true))))),
% 57.27/8.66 inference(rectify,[],[f6])).
% 57.27/8.66 thf(f8,plain,(
% 57.27/8.66 ! [X2 : a,X3 : a,X4 : a] : ((((sK0 @ X2 @ X3)) != $true) | ($true = ((sK0 @ X4 @ X3))) | ($true != ((sK0 @ X4 @ X2)))) & (! [X6 : a] : (($true != ((sK0 @ X6 @ (sK2 @ X6)))) | (((sK0 @ (sK2 @ X6) @ X6)) != $true)) & ! [X7 : a,X8 : a] : (($true != ((sK0 @ X7 @ X8))) | (((sK0 @ (sK2 @ X7) @ (sK2 @ X8))) = $true)) & ! [X9 : a,X10 : a] : (($true = ((sK0 @ (sK2 @ X10) @ (sK2 @ X9)))) | (((sK0 @ X10 @ X9)) != $true))) & ! [X11 : (a > $o)] : (! [X12 : a] : (($true = ((sK0 @ X12 @ (sK1 @ X11)))) | (((X11 @ X12)) != $true)) & ! [X13 : a] : ((($true = ((X11 @ (sK3 @ X13 @ X11)))) & ($true = ((X11 @ (sK3 @ X13 @ X11)))) & (((sK0 @ (sK3 @ X13 @ X11) @ X13)) != $true)) | ((((sK0 @ (sK1 @ X11) @ X13)) = $true) & (((sK0 @ (sK1 @ X11) @ X13)) = $true))) & ! [X15 : a] : ((((X11 @ X15)) != $true) | ($true = ((sK0 @ X15 @ (sK1 @ X11))))))),
% 57.27/8.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,vAPP]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X5,sK2),skolemize(X14,sK3 @ X13 @ X11)],[f7])).
% 57.27/8.66 thf(f11,plain,(
% 57.27/8.66 ( ! [X11 : (a > $o),X13 : a] : ((((sK0 @ (sK3 @ X13 @ X11) @ X13)) != $true) | (((sK0 @ (sK1 @ X11) @ X13)) = $true)) )),
% 57.27/8.66 inference(cnf_transformation,[],[f8])).
% 57.27/8.66 thf(f15,plain,(
% 57.27/8.66 ( ! [X11 : (a > $o),X13 : a] : (($true = ((X11 @ (sK3 @ X13 @ X11)))) | (((sK0 @ (sK1 @ X11) @ X13)) = $true)) )),
% 57.27/8.66 inference(cnf_transformation,[],[f8])).
% 57.27/8.66 thf(f16,plain,(
% 57.27/8.66 ( ! [X11 : (a > $o),X12 : a] : (($true = ((sK0 @ X12 @ (sK1 @ X11)))) | (((X11 @ X12)) != $true)) )),
% 57.27/8.66 inference(cnf_transformation,[],[f8])).
% 57.27/8.66 thf(f17,plain,(
% 57.27/8.66 ( ! [X10 : a,X9 : a] : (($true = ((sK0 @ (sK2 @ X10) @ (sK2 @ X9)))) | (((sK0 @ X10 @ X9)) != $true)) )),
% 57.27/8.66 inference(cnf_transformation,[],[f8])).
% 57.27/8.66 thf(f19,plain,(
% 57.27/8.66 ( ! [X6 : a] : (($true != ((sK0 @ X6 @ (sK2 @ X6)))) | (((sK0 @ (sK2 @ X6) @ X6)) != $true)) )),
% 57.27/8.66 inference(cnf_transformation,[],[f8])).
% 57.27/8.66 thf(f20,plain,(
% 57.27/8.66 ( ! [X2 : a,X3 : a,X4 : a] : ((((sK0 @ X2 @ X3)) != $true) | ($true = ((sK0 @ X4 @ X3))) | ($true != ((sK0 @ X4 @ X2)))) )),
% 57.27/8.66 inference(cnf_transformation,[],[f8])).
% 57.27/8.66 thf(f23,definition,(
% 57.27/8.66 ( ! [X2 : a,X3 : a] : ((((sF4 @ X3 @ X2)) = ((sK0 @ X2 @ X3)))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 57.27/8.66 thf(f24,plain,(
% 57.27/8.66 ( ! [X2 : a,X3 : a,X4 : a] : (($true != ((sF4 @ X2 @ X4))) | (((sF4 @ X3 @ X2)) != $true) | ($true = ((sF4 @ X3 @ X4)))) )),
% 57.27/8.66 inference(definition_folding,[],[f20,f23,f23,f23])).
% 57.27/8.66 thf(f25,definition,(
% 57.27/8.66 ( ! [X6 : a] : ((((sF5 @ X6)) = ((sK2 @ X6)))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 57.27/8.66 thf(f26,plain,(
% 57.27/8.66 ( ! [X6 : a] : ((((sK2 @ X6)) = ((sF5 @ X6)))) )),
% 57.27/8.66 inference(reorient_equations,[],[f25])).
% 57.27/8.66 thf(f27,definition,(
% 57.27/8.66 ( ! [X6 : a] : ((((sF6 @ X6)) = ((sK0 @ X6 @ (sF5 @ X6))))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 57.27/8.66 thf(f28,definition,(
% 57.27/8.66 ( ! [X6 : a] : ((((sF7 @ X6)) = ((sK0 @ (sF5 @ X6) @ X6)))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 57.27/8.66 thf(f29,plain,(
% 57.27/8.66 ( ! [X6 : a] : ((((sK0 @ (sF5 @ X6) @ X6)) = ((sF7 @ X6)))) )),
% 57.27/8.66 inference(reorient_equations,[],[f28])).
% 57.27/8.66 thf(f30,plain,(
% 57.27/8.66 ( ! [X6 : a] : ((((sF7 @ X6)) != $true) | (((sF6 @ X6)) != $true)) )),
% 57.27/8.66 inference(definition_folding,[],[f19,f29,f26,f27,f26])).
% 57.27/8.66 thf(f31,definition,(
% 57.27/8.66 ( ! [X8 : a,X7 : a] : ((((sF8 @ X8 @ X7)) = ((sK0 @ (sF5 @ X7) @ (sF5 @ X8))))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 57.27/8.66 thf(f33,plain,(
% 57.27/8.66 ( ! [X10 : a,X9 : a] : (($true != ((sF4 @ X9 @ X10))) | (((sF8 @ X9 @ X10)) = $true)) )),
% 57.27/8.66 inference(definition_folding,[],[f17,f23,f31,f26,f26])).
% 57.27/8.66 thf(f34,definition,(
% 57.27/8.66 ( ! [X11 : (a > $o)] : ((((sF9 @ X11)) = ((sK1 @ X11)))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 57.27/8.66 thf(f35,definition,(
% 57.27/8.66 ( ! [X11 : (a > $o),X12 : a] : ((((sF10 @ X11 @ X12)) = ((sK0 @ X12 @ (sF9 @ X11))))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 57.27/8.66 thf(f36,definition,(
% 57.27/8.66 ( ! [X11 : (a > $o),X12 : a] : ((((sF11 @ X12 @ X11)) = ((X11 @ X12)))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 57.27/8.66 thf(f37,plain,(
% 57.27/8.66 ( ! [X11 : (a > $o),X12 : a] : ((((X11 @ X12)) = ((sF11 @ X12 @ X11)))) )),
% 57.27/8.66 inference(reorient_equations,[],[f36])).
% 57.27/8.66 thf(f38,plain,(
% 57.27/8.66 ( ! [X11 : (a > $o),X12 : a] : ((((sF11 @ X12 @ X11)) != $true) | (((sF10 @ X11 @ X12)) = $true)) )),
% 57.27/8.66 inference(definition_folding,[],[f16,f37,f35,f34])).
% 57.27/8.66 thf(f39,definition,(
% 57.27/8.66 ( ! [X11 : (a > $o),X13 : a] : ((((sF12 @ X11 @ X13)) = ((sK3 @ X13 @ X11)))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 57.27/8.66 thf(f40,plain,(
% 57.27/8.66 ( ! [X11 : (a > $o),X13 : a] : ((((sK3 @ X13 @ X11)) = ((sF12 @ X11 @ X13)))) )),
% 57.27/8.66 inference(reorient_equations,[],[f39])).
% 57.27/8.66 thf(f41,definition,(
% 57.27/8.66 ( ! [X11 : (a > $o),X13 : a] : ((((sF13 @ X13 @ X11)) = ((X11 @ (sF12 @ X11 @ X13))))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 57.27/8.66 thf(f42,definition,(
% 57.27/8.66 ( ! [X11 : (a > $o),X13 : a] : ((((sF14 @ X13 @ X11)) = ((sK0 @ (sF9 @ X11) @ X13)))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 57.27/8.66 thf(f43,plain,(
% 57.27/8.66 ( ! [X11 : (a > $o),X13 : a] : ((((sK0 @ (sF9 @ X11) @ X13)) = ((sF14 @ X13 @ X11)))) )),
% 57.27/8.66 inference(reorient_equations,[],[f42])).
% 57.27/8.66 thf(f44,plain,(
% 57.27/8.66 ( ! [X11 : (a > $o),X13 : a] : ((((sF14 @ X13 @ X11)) = $true) | (((sF13 @ X13 @ X11)) = $true)) )),
% 57.27/8.66 inference(definition_folding,[],[f15,f43,f34,f41,f40])).
% 57.27/8.66 thf(f48,definition,(
% 57.27/8.66 ( ! [X11 : (a > $o),X13 : a] : ((((sF15 @ X13 @ X11)) = ((sK0 @ (sF12 @ X11 @ X13) @ X13)))) )),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 57.27/8.66 thf(f49,plain,(
% 57.27/8.66 ( ! [X11 : (a > $o),X13 : a] : ((((sF15 @ X13 @ X11)) != $true) | (((sF14 @ X13 @ X11)) = $true)) )),
% 57.27/8.66 inference(definition_folding,[],[f11,f43,f34,f48,f40])).
% 57.27/8.66 thf(f66,plain,(
% 57.27/8.66 ( ! [X0 : a,X1 : a] : ((((sK0 @ X0 @ X1)) != $true) | (((sF8 @ X1 @ X0)) = $true)) )),
% 57.27/8.66 inference(superposition,[],[f33,f23])).
% 57.27/8.66 thf(f68,plain,(
% 57.27/8.66 ( ! [X0 : a] : ((((sF6 @ X0)) != $true) | ($true = ((sF8 @ (sF5 @ X0) @ X0)))) )),
% 57.27/8.66 inference(superposition,[],[f66,f27])).
% 57.27/8.66 thf(f74,plain,(
% 57.27/8.66 ( ! [X0 : a] : ((((sF8 @ (sF5 @ X0) @ X0)) = ((sF6 @ (sF5 @ X0))))) )),
% 57.27/8.66 inference(superposition,[],[f27,f31])).
% 57.27/8.66 thf(f77,plain,(
% 57.27/8.66 ( ! [X0 : a,X1 : a] : ((((sF4 @ (sF5 @ X0) @ (sF5 @ X1))) = ((sF8 @ X0 @ X1)))) )),
% 57.27/8.66 inference(superposition,[],[f23,f31])).
% 57.27/8.66 thf(f80,plain,(
% 57.27/8.66 ( ! [X0 : (a > $o)] : ((((sF7 @ (sF9 @ X0))) = ((sF10 @ X0 @ (sF5 @ (sF9 @ X0)))))) )),
% 57.27/8.66 inference(superposition,[],[f29,f35])).
% 57.27/8.66 thf(f81,plain,(
% 57.27/8.66 ( ! [X0 : (a > $o),X1 : a] : (($true != ((sF10 @ X0 @ X1))) | (((sF8 @ (sF9 @ X0) @ X1)) = $true)) )),
% 57.27/8.66 inference(superposition,[],[f66,f35])).
% 57.27/8.66 thf(f93,plain,(
% 57.27/8.66 ( ! [X0 : (a > $o),X1 : a] : ((((X0 @ X1)) != $true) | ($true = ((sF10 @ X0 @ X1)))) )),
% 57.27/8.66 inference(superposition,[],[f38,f37])).
% 57.27/8.66 thf(f132,plain,(
% 57.27/8.66 ( ! [X0 : a] : ((((sF8 @ (sF5 @ (sF12 @ sF6 @ X0)) @ (sF12 @ sF6 @ X0))) = $true) | (((sF13 @ X0 @ sF6)) != $true)) )),
% 57.27/8.66 inference(superposition,[],[f68,f41])).
% 57.27/8.66 thf(f140,plain,(
% 57.27/8.66 ( ! [X0 : a] : ((((sF13 @ X0 @ sF6)) != $true) | ($true = ((sF6 @ (sF5 @ (sF12 @ sF6 @ X0)))))) )),
% 57.27/8.66 inference(forward_demodulation,[],[f132,f74])).
% 57.27/8.66 thf(f142,plain,(
% 57.27/8.66 ( ! [X0 : (a > $o)] : ((((sF6 @ (sF9 @ X0))) = ((sF14 @ (sF5 @ (sF9 @ X0)) @ X0)))) )),
% 57.27/8.66 inference(superposition,[],[f43,f27])).
% 57.27/8.66 thf(f206,plain,(
% 57.27/8.66 ( ! [X2 : a,X0 : a,X1 : a] : (($true != ((sF4 @ X2 @ X1))) | (((sK0 @ X0 @ X1)) != $true) | (((sF4 @ X2 @ X0)) = $true)) )),
% 57.27/8.66 inference(superposition,[],[f24,f23])).
% 57.27/8.66 thf(f392,plain,(
% 57.27/8.66 ( ! [X0 : a,X1 : (a > $o)] : ((((sF15 @ X0 @ X1)) = ((sF4 @ X0 @ (sF12 @ X1 @ X0))))) )),
% 57.27/8.66 inference(superposition,[],[f23,f48])).
% 57.27/8.66 thf(f405,plain,(
% 57.27/8.66 ( ! [X0 : (a > $o)] : ((((sF13 @ (sF5 @ (sF9 @ X0)) @ X0)) = $true) | (((sF6 @ (sF9 @ X0))) = $true)) )),
% 57.27/8.66 inference(superposition,[],[f44,f142])).
% 57.27/8.66 thf(f642,plain,(
% 57.27/8.66 ( ! [X2 : a,X0 : a,X1 : a] : (($true != ((sK0 @ X2 @ X0))) | (((sK0 @ X0 @ X1)) != $true) | (((sF4 @ X1 @ X2)) = $true)) )),
% 57.27/8.66 inference(superposition,[],[f206,f23])).
% 57.27/8.66 thf(f726,plain,(
% 57.27/8.66 ( ! [X0 : a,X1 : a] : (($true != ((sK0 @ (sF5 @ X0) @ X1))) | (((sF4 @ X1 @ X0)) = $true) | (((sF6 @ X0)) != $true)) )),
% 57.27/8.66 inference(superposition,[],[f642,f27])).
% 57.27/8.66 thf(f736,plain,(
% 57.27/8.66 ( ! [X0 : a,X1 : a] : (($true != ((sF8 @ X0 @ X1))) | (((sF4 @ (sF5 @ X0) @ X1)) = $true) | ($true != ((sF6 @ X1)))) )),
% 57.27/8.66 inference(superposition,[],[f726,f31])).
% 57.27/8.66 thf(f1141,plain,(
% 57.27/8.66 ($true != $true) | ($true = ((sF6 @ (sF9 @ sF6)))) | (((sF6 @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6)))))) = $true)),
% 57.27/8.66 inference(superposition,[],[f140,f405])).
% 57.27/8.66 thf(f1142,plain,(
% 57.27/8.66 (((sF6 @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6)))))) = $true) | ($true = ((sF6 @ (sF9 @ sF6))))),
% 57.27/8.66 inference(trivial_inequality_removal,[],[f1141])).
% 57.27/8.66 thf(f1144,definition,(
% 57.27/8.66 spl16_1 <=> ($true = ((sF6 @ (sF9 @ sF6))))),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition])).
% 57.27/8.66 thf(f1146,plain,(
% 57.27/8.66 ($true = ((sF6 @ (sF9 @ sF6)))) | ~spl16_1),
% 57.27/8.66 inference(avatar_component_clause,[],[f1144])).
% 57.27/8.66 thf(f1148,definition,(
% 57.27/8.66 spl16_2 <=> (((sF6 @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6)))))) = $true)),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition])).
% 57.27/8.66 thf(f1150,plain,(
% 57.27/8.66 (((sF6 @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6)))))) = $true) | ~spl16_2),
% 57.27/8.66 inference(avatar_component_clause,[],[f1148])).
% 57.27/8.66 thf(f1151,plain,(
% 57.27/8.66 spl16_1 | spl16_2),
% 57.27/8.66 inference(avatar_split_clause,[],[f1142,f1148,f1144])).
% 57.27/8.66 thf(f1160,plain,(
% 57.27/8.66 (((sF10 @ sF6 @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6)))))) = $true) | ($true != $true) | ~spl16_2),
% 57.27/8.66 inference(superposition,[],[f93,f1150])).
% 57.27/8.66 thf(f1169,plain,(
% 57.27/8.66 (((sF10 @ sF6 @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6)))))) = $true) | ~spl16_2),
% 57.27/8.66 inference(trivial_inequality_removal,[],[f1160])).
% 57.27/8.66 thf(f1174,definition,(
% 57.27/8.66 spl16_3 <=> (((sF13 @ (sF5 @ (sF9 @ sF6)) @ sF6)) = $true)),
% 57.27/8.66 introduced(definition,[new_symbols(definition,[spl16_3])],[avatar_definition])).
% 57.27/8.66 thf(f1175,plain,(
% 57.27/8.66 (((sF13 @ (sF5 @ (sF9 @ sF6)) @ sF6)) = $true) | ~spl16_3),
% 57.27/8.66 inference(avatar_component_clause,[],[f1174])).
% 57.27/8.66 thf(f1176,plain,(
% 57.27/8.66 (((sF13 @ (sF5 @ (sF9 @ sF6)) @ sF6)) != $true) | spl16_3),
% 57.27/8.66 inference(avatar_component_clause,[],[f1174])).
% 57.27/8.66 thf(f1182,plain,(
% 57.27/8.66 ($true != $true) | ($true = ((sF6 @ (sF9 @ sF6)))) | spl16_3),
% 57.27/8.66 inference(superposition,[],[f1176,f405])).
% 57.27/8.66 thf(f1183,plain,(
% 57.27/8.66 ($true = ((sF6 @ (sF9 @ sF6)))) | spl16_3),
% 57.27/8.66 inference(trivial_inequality_removal,[],[f1182])).
% 57.27/8.66 thf(f1184,plain,(
% 57.27/8.66 spl16_1 | spl16_3),
% 57.27/8.66 inference(avatar_split_clause,[],[f1183,f1174,f1144])).
% 57.27/8.66 thf(f1209,plain,(
% 57.27/8.66 ($true != $true) | ($true = ((sF8 @ (sF9 @ sF6) @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6))))))) | ~spl16_2),
% 57.27/8.66 inference(superposition,[],[f81,f1169])).
% 57.27/8.66 thf(f1214,plain,(
% 57.27/8.66 ($true = ((sF8 @ (sF9 @ sF6) @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6))))))) | ~spl16_2),
% 57.27/8.66 inference(trivial_inequality_removal,[],[f1209])).
% 57.27/8.66 thf(f1243,plain,(
% 57.27/8.66 (((sF6 @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6)))))) != $true) | ($true != $true) | ($true = ((sF4 @ (sF5 @ (sF9 @ sF6)) @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6))))))) | ~spl16_2),
% 57.27/8.66 inference(superposition,[],[f736,f1214])).
% 57.27/8.66 thf(f1248,plain,(
% 57.27/8.66 (((sF6 @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6)))))) != $true) | ($true = ((sF4 @ (sF5 @ (sF9 @ sF6)) @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6))))))) | ~spl16_2),
% 57.27/8.66 inference(trivial_inequality_removal,[],[f1243])).
% 57.27/8.66 thf(f1253,plain,(
% 57.27/8.66 ($true = ((sF4 @ (sF5 @ (sF9 @ sF6)) @ (sF5 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6))))))) | ~spl16_2),
% 57.27/8.66 inference(forward_subsumption_resolution,[],[f1248,f1150])).
% 57.27/8.66 thf(f1255,plain,(
% 57.27/8.66 ($true = ((sF8 @ (sF9 @ sF6) @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6)))))) | ~spl16_2),
% 57.27/8.66 inference(forward_demodulation,[],[f1253,f77])).
% 57.27/8.66 thf(f1256,plain,(
% 57.27/8.66 (((sF6 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6))))) != $true) | (((sF4 @ (sF5 @ (sF9 @ sF6)) @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6))))) = $true) | ($true != $true) | ~spl16_2),
% 57.27/8.66 inference(superposition,[],[f736,f1255])).
% 57.27/8.66 thf(f1263,plain,(
% 57.27/8.66 (((sF6 @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6))))) != $true) | (((sF4 @ (sF5 @ (sF9 @ sF6)) @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6))))) = $true) | ~spl16_2),
% 57.27/8.66 inference(trivial_inequality_removal,[],[f1256])).
% 57.27/8.66 thf(f1266,plain,(
% 57.27/8.66 (((sF13 @ (sF5 @ (sF9 @ sF6)) @ sF6)) != $true) | (((sF4 @ (sF5 @ (sF9 @ sF6)) @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6))))) = $true) | ~spl16_2),
% 57.27/8.66 inference(forward_demodulation,[],[f1263,f41])).
% 57.27/8.66 thf(f1268,plain,(
% 57.27/8.66 (((sF4 @ (sF5 @ (sF9 @ sF6)) @ (sF12 @ sF6 @ (sF5 @ (sF9 @ sF6))))) = $true) | (~spl16_2 | ~spl16_3)),
% 57.27/8.66 inference(forward_subsumption_resolution,[],[f1266,f1175])).
% 57.27/8.66 thf(f1269,plain,(
% 57.27/8.66 (((sF15 @ (sF5 @ (sF9 @ sF6)) @ sF6)) = $true) | (~spl16_2 | ~spl16_3)),
% 57.27/8.66 inference(forward_demodulation,[],[f1268,f392])).
% 57.27/8.66 thf(f1270,plain,(
% 57.27/8.66 ($true = ((sF14 @ (sF5 @ (sF9 @ sF6)) @ sF6))) | ($true != $true) | (~spl16_2 | ~spl16_3)),
% 57.27/8.66 inference(superposition,[],[f49,f1269])).
% 57.27/8.66 thf(f1271,plain,(
% 57.27/8.66 ($true = ((sF14 @ (sF5 @ (sF9 @ sF6)) @ sF6))) | (~spl16_2 | ~spl16_3)),
% 57.27/8.66 inference(trivial_inequality_removal,[],[f1270])).
% 57.27/8.66 thf(f1272,plain,(
% 57.27/8.66 ($true = ((sF6 @ (sF9 @ sF6)))) | (~spl16_2 | ~spl16_3)),
% 57.27/8.66 inference(forward_demodulation,[],[f1271,f142])).
% 57.27/8.66 thf(f1273,plain,(
% 57.27/8.66 spl16_1 | ~spl16_2 | ~spl16_3),
% 57.27/8.66 inference(avatar_split_clause,[],[f1272,f1174,f1148,f1144])).
% 57.27/8.66 thf(f1277,plain,(
% 57.27/8.66 ($true = ((sF8 @ (sF5 @ (sF9 @ sF6)) @ (sF9 @ sF6)))) | ($true != $true) | ~spl16_1),
% 57.27/8.66 inference(superposition,[],[f68,f1146])).
% 57.27/8.66 thf(f1280,plain,(
% 57.27/8.66 ($true = ((sF8 @ (sF5 @ (sF9 @ sF6)) @ (sF9 @ sF6)))) | ~spl16_1),
% 57.27/8.66 inference(trivial_inequality_removal,[],[f1277])).
% 57.27/8.66 thf(f1286,plain,(
% 57.27/8.66 (((sF6 @ (sF5 @ (sF9 @ sF6)))) = $true) | ~spl16_1),
% 57.27/8.66 inference(forward_demodulation,[],[f1280,f74])).
% 57.27/8.66 thf(f1296,plain,(
% 57.27/8.66 ($true = ((sF10 @ sF6 @ (sF5 @ (sF9 @ sF6))))) | ($true != $true) | ~spl16_1),
% 57.27/8.66 inference(superposition,[],[f93,f1286])).
% 57.27/8.66 thf(f1303,plain,(
% 57.27/8.66 ($true = ((sF10 @ sF6 @ (sF5 @ (sF9 @ sF6))))) | ~spl16_1),
% 57.27/8.66 inference(trivial_inequality_removal,[],[f1296])).
% 57.27/8.66 thf(f1309,plain,(
% 57.27/8.66 ($true = ((sF7 @ (sF9 @ sF6)))) | ~spl16_1),
% 57.27/8.66 inference(forward_demodulation,[],[f1303,f80])).
% 57.27/8.66 thf(f1314,plain,(
% 57.27/8.66 ($true != ((sF6 @ (sF9 @ sF6)))) | ($true != $true) | ~spl16_1),
% 57.27/8.66 inference(superposition,[],[f30,f1309])).
% 57.27/8.66 thf(f1322,plain,(
% 57.27/8.66 ($true != ((sF6 @ (sF9 @ sF6)))) | ~spl16_1),
% 57.27/8.66 inference(trivial_inequality_removal,[],[f1314])).
% 57.27/8.66 thf(f1324,plain,(
% 57.27/8.66 $false | ~spl16_1),
% 57.27/8.66 inference(forward_subsumption_resolution,[],[f1322,f1146])).
% 57.27/8.66 thf(f1325,plain,(
% 57.27/8.66 ~spl16_1),
% 57.27/8.66 inference(avatar_contradiction_clause,[],[f1324])).
% 57.27/8.66 cnf(s1, plain, spl16_1 | spl16_2, inference(sat_conversion,[],[f1151])).
% 57.27/8.66 cnf(s3, plain, spl16_1 | spl16_3, inference(sat_conversion,[],[f1184])).
% 57.27/8.66 cnf(s4, plain, spl16_1 | ~spl16_2 | ~spl16_3, inference(sat_conversion,[],[f1273])).
% 57.27/8.66 cnf(s5, plain, ~spl16_1, inference(sat_conversion,[],[f1325])).
% 57.27/8.66 cnf(s6, plain, ~spl16_2 | ~spl16_3, inference(rat,[],[s4,s5])).
% 57.27/8.66 cnf(s7, plain, spl16_3, inference(rat,[],[s3,s5])).
% 57.27/8.66 cnf(s8, plain, ~spl16_2, inference(rat,[],[s6,s7])).
% 57.27/8.66 cnf(s9, plain, $false, inference(rat,[],[s1,s8,s5])).
% 57.27/8.66 thf(f1326,plain,(
% 57.27/8.66 $false),
% 57.27/8.66 inference(avatar_sat_refutation,[],[s9])).
% 57.27/8.66 % SZS output end Proof for theBenchmark
% 57.27/8.66 % (1390992)------------------------------
% 57.27/8.66 % (1390992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.27/8.66 % (1390992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.27/8.66 % (1390992)CaDiCaL version: 2.1.3
% 57.27/8.66 % (1390992)Termination reason: Refutation
% 57.27/8.66 % (1390992)Time elapsed: 0.081 s
% 57.27/8.66 % (1390992)Peak memory usage: 14 MB
% 57.27/8.66 % (1390992)Instructions burned: 128 (million)
% 57.27/8.66 % (1390572)Success in time 8.303 s
% 57.27/8.66 % Vampire exiting
%------------------------------------------------------------------------------