%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP146^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:08:33 AM UTC 2026
% Result : Theorem 15.68s 2.69s
% Output : Refutation 15.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP146^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 % Computer : n016.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Tue Sep 29 20:05:35 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 Running higher-order theorem proving
% 0.22/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.74/0.41 % (840538)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.74/0.41 % (840548)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2996761041:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.74/0.41 % (840544)lrs+10_16_si=on:nwc=1.5:random_seed=10100413:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.74/0.41 % (840543)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2819412947:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.74/0.41 % (840545)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2051903385:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.74/0.41 % (840547)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=161118794:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.74/0.41 % (840545)Instruction limit reached!
% 0.74/0.41 % (840545)------------------------------
% 0.74/0.41 % (840545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.41 % (840545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.41 % (840545)CaDiCaL version: 2.1.3
% 0.74/0.41 % (840545)Termination reason: Instruction limit
% 0.74/0.41 % (840545)Termination phase: shuffling
% 0.74/0.41 % (840545)Time elapsed: 0.002 s
% 0.74/0.41 % (840545)Peak memory usage: 10 MB
% 0.74/0.41 % (840545)Instructions burned: 5 (million)
% 0.74/0.41 % (840546)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=1556490558: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)
% 0.74/0.41 % (840549)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.74/0.41 % (840549)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
% 0.74/0.41 % (840544)Instruction limit reached!
% 0.74/0.41 % (840544)------------------------------
% 0.74/0.41 % (840544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.41 % (840544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.41 % (840544)CaDiCaL version: 2.1.3
% 0.74/0.41 % (840544)Termination reason: Instruction limit
% 0.74/0.41 % (840544)Termination phase: shuffling
% 0.74/0.41 % (840544)Time elapsed: 0.008 s
% 0.74/0.41 % (840544)Peak memory usage: 10 MB
% 0.74/0.41 % (840544)Instructions burned: 19 (million)
% 0.74/0.41 % (840548)Instruction limit reached!
% 0.74/0.41 % (840548)------------------------------
% 0.74/0.41 % (840548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.41 % (840548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.41 % (840548)CaDiCaL version: 2.1.3
% 0.74/0.41 % (840548)Termination reason: Instruction limit
% 0.74/0.41 % (840548)Termination phase: Property scanning
% 0.74/0.41 % (840548)Time elapsed: 0.018 s
% 0.74/0.41 % (840548)Peak memory usage: 11 MB
% 0.74/0.41 % (840548)Instructions burned: 77 (million)
% 0.74/0.41 % (840547)Instruction limit reached!
% 0.74/0.41 % (840547)------------------------------
% 0.74/0.41 % (840547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.41 % (840547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.41 % (840547)CaDiCaL version: 2.1.3
% 0.74/0.41 % (840547)Termination reason: Instruction limit
% 0.74/0.41 % (840547)Termination phase: Property scanning
% 0.74/0.41 % (840547)Time elapsed: 0.011 s
% 0.74/0.41 % (840547)Peak memory usage: 10 MB
% 0.74/0.41 % (840547)Instructions burned: 26 (million)
% 0.74/0.41 % (840549)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=2020611731:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.74/0.41 % (840558)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.74/0.41 % (840558)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=462784575:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.74/0.47 % (840555)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1352600615:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.74/0.47 % (840555)Instruction limit reached!
% 0.74/0.47 % (840555)------------------------------
% 0.74/0.47 % (840555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.47 % (840555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.47 % (840555)CaDiCaL version: 2.1.3
% 0.74/0.47 % (840555)Termination reason: Instruction limit
% 0.74/0.47 % (840555)Termination phase: shuffling
% 0.74/0.47 % (840555)Time elapsed: 0.002 s
% 0.74/0.47 % (840555)Peak memory usage: 10 MB
% 0.74/0.47 % (840555)Instructions burned: 3 (million)
% 0.74/0.47 % (840558)Instruction limit reached!
% 0.74/0.47 % (840558)------------------------------
% 0.74/0.47 % (840558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.47 % (840558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.47 % (840558)CaDiCaL version: 2.1.3
% 0.74/0.47 % (840558)Termination reason: Instruction limit
% 0.74/0.47 % (840558)Termination phase: shuffling
% 0.74/0.47 % (840558)Time elapsed: 0.003 s
% 0.74/0.47 % (840558)Peak memory usage: 10 MB
% 0.74/0.47 % (840558)Instructions burned: 15 (million)
% 0.74/0.47 % (840557)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=758296094:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.74/0.47 % (840559)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1843302950:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.74/0.47 % (840557)Instruction limit reached!
% 0.74/0.47 % (840557)------------------------------
% 0.74/0.47 % (840557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.47 % (840557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.47 % (840557)CaDiCaL version: 2.1.3
% 0.74/0.47 % (840557)Termination reason: Instruction limit
% 0.74/0.47 % (840557)Termination phase: shuffling
% 0.74/0.47 % (840557)Time elapsed: 0.003 s
% 0.74/0.47 % (840557)Peak memory usage: 10 MB
% 0.74/0.47 % (840557)Instructions burned: 6 (million)
% 0.74/0.47 % (840559)Instruction limit reached!
% 0.74/0.47 % (840559)------------------------------
% 0.74/0.47 % (840559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.47 % (840559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.47 % (840559)CaDiCaL version: 2.1.3
% 0.74/0.47 % (840559)Termination reason: Instruction limit
% 0.74/0.47 % (840559)Termination phase: shuffling
% 0.74/0.47 % (840559)Time elapsed: 0.005 s
% 0.74/0.47 % (840559)Peak memory usage: 10 MB
% 0.74/0.47 % (840559)Instructions burned: 12 (million)
% 0.74/0.47 % (840564)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=366713511:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.74/0.47 % (840543)Instruction limit reached!
% 0.74/0.47 % (840543)------------------------------
% 0.74/0.47 % (840543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.47 % (840543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.47 % (840543)CaDiCaL version: 2.1.3
% 0.74/0.47 % (840543)Termination reason: Instruction limit
% 0.74/0.47 % (840543)Termination phase: Property scanning
% 0.74/0.47 % (840543)Time elapsed: 0.038 s
% 0.74/0.47 % (840543)Peak memory usage: 11 MB
% 0.74/0.47 % (840543)Instructions burned: 89 (million)
% 0.74/0.47 % (840563)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
% 0.74/0.47 % (840563)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.74/0.47 % (840563)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2816787151:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.74/0.47 % (840567)lrs+10_1_si=on:cs=on:random_seed=2764043738:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.74/0.47 % (840569)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.74/0.49 % (840567)Instruction limit reached!
% 0.74/0.49 % (840567)------------------------------
% 0.74/0.49 % (840567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.49 % (840567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.49 % (840567)CaDiCaL version: 2.1.3
% 0.74/0.49 % (840567)Termination reason: Instruction limit
% 0.74/0.49 % (840567)Termination phase: shuffling
% 0.74/0.49 % (840567)Time elapsed: 0.004 s
% 0.74/0.49 % (840567)Peak memory usage: 10 MB
% 0.74/0.49 % (840567)Instructions burned: 9 (million)
% 0.74/0.49 % (840569)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=2847095716:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.74/0.49 % (840564)Instruction limit reached!
% 0.74/0.49 % (840564)------------------------------
% 0.74/0.49 % (840564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.49 % (840564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.49 % (840564)CaDiCaL version: 2.1.3
% 0.74/0.49 % (840564)Termination reason: Instruction limit
% 0.74/0.49 % (840564)Termination phase: Property scanning
% 0.74/0.49 % (840564)Time elapsed: 0.019 s
% 0.74/0.49 % (840564)Peak memory usage: 11 MB
% 0.74/0.49 % (840564)Instructions burned: 89 (million)
% 0.74/0.49 % (840569)Instruction limit reached!
% 0.74/0.49 % (840569)------------------------------
% 0.74/0.49 % (840569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.49 % (840569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.49 % (840569)CaDiCaL version: 2.1.3
% 0.74/0.49 % (840569)Termination reason: Instruction limit
% 0.74/0.49 % (840569)Termination phase: shuffling
% 0.74/0.49 % (840569)Time elapsed: 0.002 s
% 0.74/0.49 % (840569)Peak memory usage: 10 MB
% 0.74/0.49 % (840569)Instructions burned: 4 (million)
% 0.74/0.49 % (840563)Instruction limit reached!
% 0.74/0.49 % (840563)------------------------------
% 0.74/0.49 % (840563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.49 % (840563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.49 % (840563)CaDiCaL version: 2.1.3
% 0.74/0.49 % (840563)Termination reason: Instruction limit
% 0.74/0.49 % (840563)Termination phase: shuffling
% 0.74/0.49 % (840563)Time elapsed: 0.013 s
% 0.74/0.49 % (840563)Peak memory usage: 10 MB
% 0.74/0.49 % (840563)Instructions burned: 29 (million)
% 0.74/0.49 % (840570)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4016282616:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.74/0.49 % (840575)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3784843447:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.74/0.49 % (840575)Instruction limit reached!
% 0.74/0.49 % (840575)------------------------------
% 0.74/0.49 % (840575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.49 % (840575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.49 % (840575)CaDiCaL version: 2.1.3
% 0.74/0.49 % (840575)Termination reason: Instruction limit
% 0.74/0.49 % (840575)Termination phase: Property scanning
% 0.74/0.49 % (840575)Time elapsed: 0.005 s
% 0.74/0.49 % (840575)Peak memory usage: 10 MB
% 0.74/0.49 % (840575)Instructions burned: 26 (million)
% 0.74/0.49 % (840576)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3035635297:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.74/0.49 % (840574)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2459663396:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.74/0.49 % (840577)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=795241049:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.74/0.49 % (840570)Instruction limit reached!
% 0.74/0.49 % (840570)------------------------------
% 0.74/0.49 % (840570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.49 % (840570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.49 % (840570)CaDiCaL version: 2.1.3
% 0.74/0.49 % (840570)Termination reason: Instruction limit
% 0.74/0.49 % (840570)Termination phase: SInE selection
% 0.74/0.49 % (840570)Time elapsed: 0.019 s
% 1.47/0.57 % (840570)Peak memory usage: 10 MB
% 1.47/0.57 % (840570)Instructions burned: 39 (million)
% 1.47/0.57 % (840576)Instruction limit reached!
% 1.47/0.57 % (840576)------------------------------
% 1.47/0.57 % (840576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.57 % (840576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.57 % (840576)CaDiCaL version: 2.1.3
% 1.47/0.57 % (840576)Termination reason: Instruction limit
% 1.47/0.57 % (840576)Termination phase: shuffling
% 1.47/0.57 % (840576)Time elapsed: 0.006 s
% 1.47/0.57 % (840576)Peak memory usage: 10 MB
% 1.47/0.57 % (840576)Instructions burned: 15 (million)
% 1.47/0.57 % (840584)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1976126464: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)
% 1.47/0.57 % (840585)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3946588914:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.47/0.57 % (840584)Instruction limit reached!
% 1.47/0.57 % (840584)------------------------------
% 1.47/0.57 % (840584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.57 % (840584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.57 % (840584)CaDiCaL version: 2.1.3
% 1.47/0.57 % (840584)Termination reason: Instruction limit
% 1.47/0.57 % (840584)Termination phase: shuffling
% 1.47/0.57 % (840584)Time elapsed: 0.002 s
% 1.47/0.57 % (840584)Peak memory usage: 10 MB
% 1.47/0.57 % (840584)Instructions burned: 4 (million)
% 1.47/0.57 % (840580)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3363566463:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.47/0.57 % (840585)Instruction limit reached!
% 1.47/0.57 % (840585)------------------------------
% 1.47/0.57 % (840585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.57 % (840585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.57 % (840585)CaDiCaL version: 2.1.3
% 1.47/0.57 % (840585)Termination reason: Instruction limit
% 1.47/0.57 % (840585)Termination phase: shuffling
% 1.47/0.57 % (840585)Time elapsed: 0.011 s
% 1.47/0.57 % (840585)Peak memory usage: 10 MB
% 1.47/0.57 % (840585)Instructions burned: 27 (million)
% 1.47/0.57 % (840580)Instruction limit reached!
% 1.47/0.57 % (840580)------------------------------
% 1.47/0.57 % (840580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.57 % (840580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.57 % (840580)CaDiCaL version: 2.1.3
% 1.47/0.57 % (840580)Termination reason: Instruction limit
% 1.47/0.57 % (840580)Termination phase: shuffling
% 1.47/0.57 % (840580)Time elapsed: 0.011 s
% 1.47/0.57 % (840580)Peak memory usage: 10 MB
% 1.47/0.57 % (840580)Instructions burned: 14 (million)
% 1.47/0.57 % (840574)Refutation not found, incomplete strategy
% 1.47/0.57 % (840574)------------------------------
% 1.47/0.57 % (840574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.57 % (840574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.57 % (840574)CaDiCaL version: 2.1.3
% 1.47/0.57 % (840574)Termination reason: Refutation not found, incomplete strategy
% 1.47/0.57 % (840574)Time elapsed: 0.039 s
% 1.47/0.57 % (840574)Peak memory usage: 13 MB
% 1.47/0.57 % (840574)Instructions burned: 86 (million)
% 1.47/0.57 % (840574)------------------------------
% 1.47/0.57 % (840574)------------------------------
% 1.47/0.57 % (840589)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3137478505:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.47/0.57 % (840591)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
% 1.47/0.57 % (840591)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.47/0.57 % (840591)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=3979929391:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.47/0.57 % (840591)Instruction limit reached!
% 1.47/0.57 % (840591)------------------------------
% 1.47/0.63 % (840591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.63 % (840591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.63 % (840591)CaDiCaL version: 2.1.3
% 1.47/0.63 % (840591)Termination reason: Instruction limit
% 1.47/0.63 % (840591)Termination phase: shuffling
% 1.47/0.63 % (840591)Time elapsed: 0.004 s
% 1.47/0.63 % (840591)Peak memory usage: 10 MB
% 1.47/0.63 % (840591)Instructions burned: 18 (million)
% 1.47/0.63 % (840590)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2310711218:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.47/0.63 % (840589)Instruction limit reached!
% 1.47/0.63 % (840589)------------------------------
% 1.47/0.63 % (840589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.63 % (840589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.63 % (840589)CaDiCaL version: 2.1.3
% 1.47/0.63 % (840589)Termination reason: Instruction limit
% 1.47/0.63 % (840589)Termination phase: Property scanning
% 1.47/0.63 % (840589)Time elapsed: 0.010 s
% 1.47/0.63 % (840589)Peak memory usage: 10 MB
% 1.47/0.63 % (840589)Instructions burned: 25 (million)
% 1.47/0.63 % (840592)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.47/0.63 % (840592)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=2618173030:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.47/0.63 % (840596)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=822042422:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.47/0.63 % (840549)Instruction limit reached!
% 1.47/0.63 % (840549)------------------------------
% 1.47/0.63 % (840549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.63 % (840549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.63 % (840549)CaDiCaL version: 2.1.3
% 1.47/0.63 % (840549)Termination reason: Instruction limit
% 1.47/0.63 % (840549)Termination phase: Saturation
% 1.47/0.63 % (840549)Time elapsed: 0.131 s
% 1.47/0.63 % (840549)Peak memory usage: 13 MB
% 1.47/0.63 % (840549)Instructions burned: 157 (million)
% 1.47/0.63 % (840592)Instruction limit reached!
% 1.47/0.63 % (840592)------------------------------
% 1.47/0.63 % (840592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.63 % (840592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.63 % (840592)CaDiCaL version: 2.1.3
% 1.47/0.63 % (840592)Termination reason: Instruction limit
% 1.47/0.63 % (840592)Termination phase: shuffling
% 1.47/0.63 % (840592)Time elapsed: 0.004 s
% 1.47/0.63 % (840592)Peak memory usage: 10 MB
% 1.47/0.63 % (840592)Instructions burned: 10 (million)
% 1.47/0.63 % (840596)Instruction limit reached!
% 1.47/0.63 % (840596)------------------------------
% 1.47/0.63 % (840596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.63 % (840596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.63 % (840596)CaDiCaL version: 2.1.3
% 1.47/0.63 % (840596)Termination reason: Instruction limit
% 1.47/0.63 % (840596)Termination phase: shuffling
% 1.47/0.63 % (840596)Time elapsed: 0.007 s
% 1.47/0.63 % (840596)Peak memory usage: 10 MB
% 1.47/0.63 % (840596)Instructions burned: 32 (million)
% 1.47/0.63 % (840590)Instruction limit reached!
% 1.47/0.63 % (840590)------------------------------
% 1.47/0.63 % (840590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.63 % (840590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.63 % (840590)CaDiCaL version: 2.1.3
% 1.47/0.63 % (840590)Termination reason: Instruction limit
% 1.47/0.63 % (840590)Termination phase: Property scanning
% 1.47/0.63 % (840590)Time elapsed: 0.026 s
% 1.47/0.63 % (840590)Peak memory usage: 11 MB
% 1.47/0.63 % (840590)Instructions burned: 62 (million)
% 1.47/0.63 % (840597)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=671709458:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.47/0.63 % (840602)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1851642136:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.58/0.73 % (840600)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1238855283:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.58/0.73 % (840597)Instruction limit reached!
% 2.58/0.73 % (840597)------------------------------
% 2.58/0.73 % (840597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.73 % (840597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.73 % (840597)CaDiCaL version: 2.1.3
% 2.58/0.73 % (840597)Termination reason: Instruction limit
% 2.58/0.73 % (840597)Termination phase: shuffling
% 2.58/0.73 % (840597)Time elapsed: 0.006 s
% 2.58/0.73 % (840597)Peak memory usage: 10 MB
% 2.58/0.73 % (840597)Instructions burned: 7 (million)
% 2.58/0.73 % (840600)Instruction limit reached!
% 2.58/0.73 % (840600)------------------------------
% 2.58/0.73 % (840600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.73 % (840600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.73 % (840600)CaDiCaL version: 2.1.3
% 2.58/0.73 % (840600)Termination reason: Instruction limit
% 2.58/0.73 % (840600)Termination phase: shuffling
% 2.58/0.73 % (840600)Time elapsed: 0.010 s
% 2.58/0.73 % (840600)Peak memory usage: 10 MB
% 2.58/0.73 % (840600)Instructions burned: 23 (million)
% 2.58/0.73 % (840603)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3582227798:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.58/0.73 % (840601)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1973548279:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.58/0.73 % (840608)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2001226005:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.58/0.73 % (840601)Instruction limit reached!
% 2.58/0.73 % (840601)------------------------------
% 2.58/0.73 % (840601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.73 % (840601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.73 % (840601)CaDiCaL version: 2.1.3
% 2.58/0.73 % (840601)Termination reason: Instruction limit
% 2.58/0.73 % (840601)Termination phase: shuffling
% 2.58/0.73 % (840601)Time elapsed: 0.014 s
% 2.58/0.73 % (840601)Peak memory usage: 10 MB
% 2.58/0.73 % (840601)Instructions burned: 21 (million)
% 2.58/0.73 % (840607)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2709122502:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.58/0.73 % (840608)Instruction limit reached!
% 2.58/0.73 % (840608)------------------------------
% 2.58/0.73 % (840608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.73 % (840608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.73 % (840608)CaDiCaL version: 2.1.3
% 2.58/0.73 % (840608)Termination reason: Instruction limit
% 2.58/0.73 % (840608)Termination phase: Preprocessing 3
% 2.58/0.73 % (840608)Time elapsed: 0.018 s
% 2.58/0.73 % (840608)Peak memory usage: 11 MB
% 2.58/0.73 % (840608)Instructions burned: 43 (million)
% 2.58/0.73 % (840612)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.58/0.73 % (840612)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1524006917:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.58/0.73 % (840612)Instruction limit reached!
% 2.58/0.73 % (840612)------------------------------
% 2.58/0.73 % (840612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.73 % (840612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.73 % (840612)CaDiCaL version: 2.1.3
% 2.58/0.73 % (840612)Termination reason: Instruction limit
% 2.58/0.73 % (840612)Termination phase: shuffling
% 2.58/0.73 % (840612)Time elapsed: 0.004 s
% 2.58/0.73 % (840612)Peak memory usage: 10 MB
% 2.58/0.73 % (840612)Instructions burned: 8 (million)
% 2.58/0.73 % (840614)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=196274935:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.58/0.73 % (840577)Instruction limit reached!
% 2.58/0.73 % (840577)------------------------------
% 2.58/0.73 % (840577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.79 % (840577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.79 % (840577)CaDiCaL version: 2.1.3
% 2.58/0.79 % (840577)Termination reason: Instruction limit
% 2.58/0.79 % (840577)Termination phase: Saturation
% 2.58/0.79 % (840577)Time elapsed: 0.153 s
% 2.58/0.79 % (840577)Peak memory usage: 14 MB
% 2.58/0.79 % (840577)Instructions burned: 328 (million)
% 2.58/0.79 % (840603)Instruction limit reached!
% 2.58/0.79 % (840603)------------------------------
% 2.58/0.79 % (840603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.79 % (840603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.79 % (840603)CaDiCaL version: 2.1.3
% 2.58/0.79 % (840603)Termination reason: Instruction limit
% 2.58/0.79 % (840603)Termination phase: Saturation
% 2.58/0.79 % (840603)Time elapsed: 0.068 s
% 2.58/0.79 % (840603)Peak memory usage: 13 MB
% 2.58/0.79 % (840603)Instructions burned: 145 (million)
% 2.58/0.79 % (840618)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.58/0.79 % (840618)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=323167700:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.58/0.79 % (840616)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=2757881219:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.58/0.79 % (840618)Instruction limit reached!
% 2.58/0.79 % (840618)------------------------------
% 2.58/0.79 % (840618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.79 % (840618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.79 % (840618)CaDiCaL version: 2.1.3
% 2.58/0.79 % (840618)Termination reason: Instruction limit
% 2.58/0.79 % (840618)Termination phase: shuffling
% 2.58/0.79 % (840618)Time elapsed: 0.004 s
% 2.58/0.79 % (840618)Peak memory usage: 10 MB
% 2.58/0.79 % (840618)Instructions burned: 8 (million)
% 2.58/0.79 % (840619)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2678905003:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.58/0.79 % (840619)Instruction limit reached!
% 2.58/0.79 % (840619)------------------------------
% 2.58/0.79 % (840619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.79 % (840619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.79 % (840619)CaDiCaL version: 2.1.3
% 2.58/0.79 % (840619)Termination reason: Instruction limit
% 2.58/0.79 % (840619)Termination phase: Property scanning
% 2.58/0.79 % (840619)Time elapsed: 0.010 s
% 2.58/0.79 % (840619)Peak memory usage: 10 MB
% 2.58/0.79 % (840619)Instructions burned: 24 (million)
% 2.58/0.79 % (840622)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=904657611:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 2.58/0.79 % (840622)Instruction limit reached!
% 2.58/0.79 % (840622)------------------------------
% 2.58/0.79 % (840622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.79 % (840622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.79 % (840622)CaDiCaL version: 2.1.3
% 2.58/0.79 % (840622)Termination reason: Instruction limit
% 2.58/0.79 % (840622)Termination phase: shuffling
% 2.58/0.79 % (840622)Time elapsed: 0.009 s
% 2.58/0.79 % (840622)Peak memory usage: 10 MB
% 2.58/0.79 % (840622)Instructions burned: 21 (million)
% 2.58/0.79 % (840607)Instruction limit reached!
% 2.58/0.79 % (840607)------------------------------
% 2.58/0.79 % (840607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.79 % (840607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.79 % (840607)CaDiCaL version: 2.1.3
% 2.58/0.79 % (840607)Termination reason: Instruction limit
% 2.58/0.79 % (840607)Termination phase: Saturation
% 2.58/0.79 % (840607)Time elapsed: 0.091 s
% 2.58/0.79 % (840607)Peak memory usage: 13 MB
% 2.58/0.79 % (840607)Instructions burned: 194 (million)
% 2.58/0.79 % (840624)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=1871020816:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 3.12/0.84 % (840626)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=408774834:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.12/0.84 % (840628)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=1396469615:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.12/0.84 % (840614)Instruction limit reached!
% 3.12/0.84 % (840614)------------------------------
% 3.12/0.84 % (840614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.84 % (840614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.84 % (840614)CaDiCaL version: 2.1.3
% 3.12/0.84 % (840614)Termination reason: Instruction limit
% 3.12/0.84 % (840614)Termination phase: Saturation
% 3.12/0.84 % (840614)Time elapsed: 0.090 s
% 3.12/0.84 % (840614)Peak memory usage: 13 MB
% 3.12/0.84 % (840614)Instructions burned: 183 (million)
% 3.12/0.84 % (840628)Instruction limit reached!
% 3.12/0.84 % (840628)------------------------------
% 3.12/0.84 % (840628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.84 % (840628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.84 % (840628)CaDiCaL version: 2.1.3
% 3.12/0.84 % (840628)Termination reason: Instruction limit
% 3.12/0.84 % (840628)Termination phase: Property scanning
% 3.12/0.84 % (840628)Time elapsed: 0.018 s
% 3.12/0.84 % (840628)Peak memory usage: 10 MB
% 3.12/0.84 % (840628)Instructions burned: 45 (million)
% 3.12/0.84 % (840631)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3469126049:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.12/0.84 % (840616)Refutation not found, incomplete strategy
% 3.12/0.84 % (840616)------------------------------
% 3.12/0.84 % (840616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.84 % (840616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.84 % (840616)CaDiCaL version: 2.1.3
% 3.12/0.84 % (840616)Termination reason: Refutation not found, incomplete strategy
% 3.12/0.84 % (840616)Time elapsed: 0.096 s
% 3.12/0.84 % (840616)Peak memory usage: 13 MB
% 3.12/0.84 % (840616)Instructions burned: 111 (million)
% 3.12/0.84 % (840616)------------------------------
% 3.12/0.84 % (840616)------------------------------
% 3.12/0.84 % (840632)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1221918841:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 3.12/0.84 % (840632)Instruction limit reached!
% 3.12/0.84 % (840632)------------------------------
% 3.12/0.84 % (840632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.84 % (840632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.84 % (840632)CaDiCaL version: 2.1.3
% 3.12/0.84 % (840632)Termination reason: Instruction limit
% 3.12/0.84 % (840632)Termination phase: Property scanning
% 3.12/0.84 % (840632)Time elapsed: 0.009 s
% 3.12/0.84 % (840632)Peak memory usage: 10 MB
% 3.12/0.84 % (840632)Instructions burned: 23 (million)
% 3.12/0.84 % (840635)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.12/0.84 % (840635)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2008809971:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/200Mi)
% 3.12/0.84 % (840636)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1792054211:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2995 on theBenchmark for (2995ds/13Mi)
% 3.12/0.84 % (840636)Instruction limit reached!
% 3.12/0.84 % (840636)------------------------------
% 3.12/0.84 % (840636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.84 % (840636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.84 % (840636)CaDiCaL version: 2.1.3
% 3.12/0.84 % (840636)Termination reason: Instruction limit
% 3.12/0.84 % (840636)Termination phase: shuffling
% 3.12/0.84 % (840636)Time elapsed: 0.006 s
% 3.12/0.84 % (840636)Peak memory usage: 10 MB
% 3.12/0.84 % (840636)Instructions burned: 13 (million)
% 3.12/0.84 % (840631)Refutation not found, incomplete strategy
% 3.63/0.98 % (840631)------------------------------
% 3.63/0.98 % (840631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.98 % (840631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.98 % (840631)CaDiCaL version: 2.1.3
% 3.63/0.98 % (840631)Termination reason: Refutation not found, incomplete strategy
% 3.63/0.98 % (840631)Time elapsed: 0.050 s
% 3.63/0.98 % (840631)Peak memory usage: 13 MB
% 3.63/0.98 % (840631)Instructions burned: 112 (million)
% 3.63/0.98 % (840631)------------------------------
% 3.63/0.98 % (840631)------------------------------
% 3.63/0.98 % (840639)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=3474509769:i=66:s2at=3:nm=2:rtra=on:rawr=on_2995 on theBenchmark for (2995ds/66Mi)
% 3.63/0.98 % (840602)Instruction limit reached!
% 3.63/0.98 % (840602)------------------------------
% 3.63/0.98 % (840602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.98 % (840602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.98 % (840602)CaDiCaL version: 2.1.3
% 3.63/0.98 % (840602)Termination reason: Instruction limit
% 3.63/0.98 % (840602)Termination phase: Saturation
% 3.63/0.98 % (840602)Time elapsed: 0.245 s
% 3.63/0.98 % (840602)Peak memory usage: 15 MB
% 3.63/0.98 % (840602)Instructions burned: 1241 (million)
% 3.63/0.98 % (840640)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3053444441:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 3.63/0.98 % (840642)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3161928908:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 3.63/0.98 % (840642)Instruction limit reached!
% 3.63/0.98 % (840642)------------------------------
% 3.63/0.98 % (840642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.98 % (840642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.98 % (840642)CaDiCaL version: 2.1.3
% 3.63/0.98 % (840642)Termination reason: Instruction limit
% 3.63/0.98 % (840642)Termination phase: shuffling
% 3.63/0.98 % (840642)Time elapsed: 0.007 s
% 3.63/0.98 % (840642)Peak memory usage: 10 MB
% 3.63/0.98 % (840642)Instructions burned: 33 (million)
% 3.63/0.98 % (840640)Instruction limit reached!
% 3.63/0.98 % (840640)------------------------------
% 3.63/0.98 % (840640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.98 % (840640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.98 % (840640)CaDiCaL version: 2.1.3
% 3.63/0.98 % (840640)Termination reason: Instruction limit
% 3.63/0.98 % (840640)Termination phase: Property scanning
% 3.63/0.98 % (840640)Time elapsed: 0.022 s
% 3.63/0.98 % (840640)Peak memory usage: 11 MB
% 3.63/0.98 % (840640)Instructions burned: 52 (million)
% 3.63/0.98 % (840639)Instruction limit reached!
% 3.63/0.98 % (840639)------------------------------
% 3.63/0.98 % (840639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.98 % (840639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.98 % (840639)CaDiCaL version: 2.1.3
% 3.63/0.98 % (840639)Termination reason: Instruction limit
% 3.63/0.98 % (840639)Termination phase: SInE selection
% 3.63/0.98 % (840639)Time elapsed: 0.028 s
% 3.63/0.98 % (840639)Peak memory usage: 11 MB
% 3.63/0.98 % (840639)Instructions burned: 67 (million)
% 3.63/0.98 % (840645)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2945155830:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.63/0.98 % (840647)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=1491935729:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.63/0.98 % (840646)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=3943357217:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.63/0.98 % (840624)Instruction limit reached!
% 3.63/0.98 % (840624)------------------------------
% 3.63/0.98 % (840624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.98 % (840624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.98 % (840624)CaDiCaL version: 2.1.3
% 3.63/0.98 % (840624)Termination reason: Instruction limit
% 4.80/1.08 % (840624)Termination phase: Saturation
% 4.80/1.08 % (840624)Time elapsed: 0.160 s
% 4.80/1.08 % (840624)Peak memory usage: 15 MB
% 4.80/1.08 % (840624)Instructions burned: 316 (million)
% 4.80/1.08 % (840635)Instruction limit reached!
% 4.80/1.08 % (840635)------------------------------
% 4.80/1.08 % (840635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.08 % (840635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.08 % (840635)CaDiCaL version: 2.1.3
% 4.80/1.08 % (840635)Termination reason: Instruction limit
% 4.80/1.08 % (840635)Termination phase: Saturation
% 4.80/1.08 % (840635)Time elapsed: 0.094 s
% 4.80/1.08 % (840635)Peak memory usage: 13 MB
% 4.80/1.08 % (840635)Instructions burned: 202 (million)
% 4.80/1.08 % (840646)Instruction limit reached!
% 4.80/1.08 % (840646)------------------------------
% 4.80/1.08 % (840646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.08 % (840646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.08 % (840646)CaDiCaL version: 2.1.3
% 4.80/1.08 % (840646)Termination reason: Instruction limit
% 4.80/1.08 % (840646)Termination phase: Property scanning
% 4.80/1.08 % (840646)Time elapsed: 0.015 s
% 4.80/1.08 % (840646)Peak memory usage: 10 MB
% 4.80/1.08 % (840646)Instructions burned: 35 (million)
% 4.80/1.08 % (840645)Instruction limit reached!
% 4.80/1.08 % (840645)------------------------------
% 4.80/1.08 % (840645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.08 % (840645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.08 % (840645)CaDiCaL version: 2.1.3
% 4.80/1.08 % (840645)Termination reason: Instruction limit
% 4.80/1.08 % (840645)Termination phase: Saturation
% 4.80/1.08 % (840645)Time elapsed: 0.033 s
% 4.80/1.08 % (840645)Peak memory usage: 13 MB
% 4.80/1.08 % (840645)Instructions burned: 138 (million)
% 4.80/1.08 % (840651)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 4.80/1.08 % (840651)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3253173870:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 4.80/1.08 % (840654)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1748333027:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 4.80/1.08 % (840647)Instruction limit reached!
% 4.80/1.08 % (840647)------------------------------
% 4.80/1.08 % (840647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.08 % (840647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.08 % (840647)CaDiCaL version: 2.1.3
% 4.80/1.08 % (840647)Termination reason: Instruction limit
% 4.80/1.08 % (840647)Termination phase: Property scanning
% 4.80/1.08 % (840647)Time elapsed: 0.029 s
% 4.80/1.08 % (840647)Peak memory usage: 11 MB
% 4.80/1.08 % (840647)Instructions burned: 69 (million)
% 4.80/1.08 % (840652)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=3451918692:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 4.80/1.08 % (840653)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3358124490:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 4.80/1.08 % (840654)Refutation not found, incomplete strategy
% 4.80/1.08 % (840654)------------------------------
% 4.80/1.08 % (840654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.08 % (840654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.08 % (840654)CaDiCaL version: 2.1.3
% 4.80/1.08 % (840654)Termination reason: Refutation not found, incomplete strategy
% 4.80/1.08 % (840654)Time elapsed: 0.012 s
% 4.80/1.08 % (840654)Peak memory usage: 12 MB
% 4.80/1.08 % (840654)Instructions burned: 54 (million)
% 4.80/1.08 % (840654)------------------------------
% 4.80/1.08 % (840654)------------------------------
% 4.80/1.08 % (840657)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=980332403:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 4.80/1.08 % (840660)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=4182244747:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 4.80/1.08 % (840546)Instruction limit reached!
% 4.80/1.08 % (840546)------------------------------
% 4.80/1.08 % (840546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.08 % (840546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.16 % (840546)CaDiCaL version: 2.1.3
% 4.80/1.16 % (840546)Termination reason: Instruction limit
% 4.80/1.16 % (840546)Termination phase: Saturation
% 4.80/1.16 % (840546)Time elapsed: 0.502 s
% 4.80/1.16 % (840546)Peak memory usage: 15 MB
% 4.80/1.16 % (840546)Instructions burned: 635 (million)
% 4.80/1.16 % (840663)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2142272163:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 4.80/1.16 % (840653)Instruction limit reached!
% 4.80/1.16 % (840653)------------------------------
% 4.80/1.16 % (840653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.16 % (840653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.16 % (840653)CaDiCaL version: 2.1.3
% 4.80/1.16 % (840653)Termination reason: Instruction limit
% 4.80/1.16 % (840653)Termination phase: Saturation
% 4.80/1.16 % (840653)Time elapsed: 0.041 s
% 4.80/1.16 % (840653)Peak memory usage: 13 MB
% 4.80/1.16 % (840653)Instructions burned: 96 (million)
% 4.80/1.16 % (840665)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3122006065:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 4.80/1.16 % (840651)Instruction limit reached!
% 4.80/1.16 % (840651)------------------------------
% 4.80/1.16 % (840651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.16 % (840651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.16 % (840651)CaDiCaL version: 2.1.3
% 4.80/1.16 % (840651)Termination reason: Instruction limit
% 4.80/1.16 % (840651)Termination phase: Saturation
% 4.80/1.16 % (840651)Time elapsed: 0.075 s
% 4.80/1.16 % (840651)Peak memory usage: 13 MB
% 4.80/1.16 % (840651)Instructions burned: 180 (million)
% 4.80/1.16 % (840663)Instruction limit reached!
% 4.80/1.16 % (840663)------------------------------
% 4.80/1.16 % (840663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.16 % (840663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.16 % (840663)CaDiCaL version: 2.1.3
% 4.80/1.16 % (840663)Termination reason: Instruction limit
% 4.80/1.16 % (840663)Termination phase: Saturation
% 4.80/1.16 % (840663)Time elapsed: 0.029 s
% 4.80/1.16 % (840663)Peak memory usage: 12 MB
% 4.80/1.16 % (840663)Instructions burned: 133 (million)
% 4.80/1.16 % (840668)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=1904325283:i=450:rtra=on:ixr=off:ntd=on_2994 on theBenchmark for (2994ds/450Mi)
% 4.80/1.16 % (840667)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3685037943:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 4.80/1.16 % (840665)Instruction limit reached!
% 4.80/1.16 % (840665)------------------------------
% 4.80/1.16 % (840665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.16 % (840665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.16 % (840665)CaDiCaL version: 2.1.3
% 4.80/1.16 % (840665)Termination reason: Instruction limit
% 4.80/1.16 % (840665)Termination phase: Property scanning
% 4.80/1.16 % (840665)Time elapsed: 0.020 s
% 4.80/1.16 % (840665)Peak memory usage: 10 MB
% 4.80/1.16 % (840665)Instructions burned: 46 (million)
% 4.80/1.16 % (840671)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=183438194:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 4.80/1.16 % (840671)Instruction limit reached!
% 4.80/1.16 % (840671)------------------------------
% 4.80/1.16 % (840671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.16 % (840671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.16 % (840671)CaDiCaL version: 2.1.3
% 4.80/1.16 % (840671)Termination reason: Instruction limit
% 4.80/1.16 % (840671)Termination phase: Saturation
% 4.80/1.16 % (840671)Time elapsed: 0.041 s
% 4.80/1.16 % (840671)Peak memory usage: 13 MB
% 4.80/1.16 % (840671)Instructions burned: 96 (million)
% 4.80/1.16 % (840652)Instruction limit reached!
% 4.80/1.16 % (840652)------------------------------
% 4.80/1.16 % (840652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.16 % (840652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.16 % (840652)CaDiCaL version: 2.1.3
% 4.80/1.16 % (840652)Termination reason: Instruction limit
% 5.95/1.26 % (840652)Termination phase: Saturation
% 5.95/1.26 % (840652)Time elapsed: 0.157 s
% 5.95/1.26 % (840652)Peak memory usage: 13 MB
% 5.95/1.26 % (840652)Instructions burned: 246 (million)
% 5.95/1.26 % (840668)Instruction limit reached!
% 5.95/1.26 % (840668)------------------------------
% 5.95/1.26 % (840668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.95/1.26 % (840668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.95/1.26 % (840668)CaDiCaL version: 2.1.3
% 5.95/1.26 % (840668)Termination reason: Instruction limit
% 5.95/1.26 % (840668)Termination phase: Saturation
% 5.95/1.26 % (840668)Time elapsed: 0.085 s
% 5.95/1.26 % (840668)Peak memory usage: 13 MB
% 5.95/1.26 % (840668)Instructions burned: 457 (million)
% 5.95/1.26 % (840673)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=537462449:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 5.95/1.26 % (840674)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=842173406: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_2993 on theBenchmark for (2993ds/105Mi)
% 5.95/1.26 % (840675)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=2594930421:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2993 on theBenchmark for (2993ds/5755Mi)
% 5.95/1.26 % (840674)Instruction limit reached!
% 5.95/1.26 % (840674)------------------------------
% 5.95/1.26 % (840674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.95/1.26 % (840674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.95/1.26 % (840674)CaDiCaL version: 2.1.3
% 5.95/1.26 % (840674)Termination reason: Instruction limit
% 5.95/1.26 % (840674)Termination phase: Property scanning
% 5.95/1.26 % (840674)Time elapsed: 0.023 s
% 5.95/1.26 % (840674)Peak memory usage: 11 MB
% 5.95/1.26 % (840674)Instructions burned: 105 (million)
% 5.95/1.26 % (840679)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=3874088599:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 5.95/1.26 % (840673)Instruction limit reached!
% 5.95/1.26 % (840673)------------------------------
% 5.95/1.26 % (840673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.95/1.26 % (840673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.95/1.26 % (840673)CaDiCaL version: 2.1.3
% 5.95/1.26 % (840673)Termination reason: Instruction limit
% 5.95/1.26 % (840673)Termination phase: Property scanning
% 5.95/1.26 % (840673)Time elapsed: 0.040 s
% 5.95/1.26 % (840673)Peak memory usage: 10 MB
% 5.95/1.26 % (840673)Instructions burned: 65 (million)
% 5.95/1.26 % (840626)Instruction limit reached!
% 5.95/1.26 % (840626)------------------------------
% 5.95/1.26 % (840626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.95/1.26 % (840626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.95/1.26 % (840626)CaDiCaL version: 2.1.3
% 5.95/1.26 % (840626)Termination reason: Instruction limit
% 5.95/1.26 % (840626)Termination phase: Saturation
% 5.95/1.26 % (840626)Time elapsed: 0.420 s
% 5.95/1.26 % (840626)Peak memory usage: 17 MB
% 5.95/1.26 % (840626)Instructions burned: 855 (million)
% 5.95/1.26 % (840681)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3107600178:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/495Mi)
% 5.95/1.26 % (840660)Instruction limit reached!
% 5.95/1.26 % (840660)------------------------------
% 5.95/1.26 % (840660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.95/1.26 % (840660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.95/1.26 % (840660)CaDiCaL version: 2.1.3
% 5.95/1.26 % (840660)Termination reason: Instruction limit
% 5.95/1.26 % (840660)Termination phase: Saturation
% 5.95/1.26 % (840660)Time elapsed: 0.236 s
% 5.95/1.26 % (840660)Peak memory usage: 14 MB
% 5.95/1.26 % (840660)Instructions burned: 516 (million)
% 5.95/1.26 % (840682)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=57826281:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 6.36/1.36 % (840684)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2543755679:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/91Mi)
% 6.36/1.36 % (840682)Instruction limit reached!
% 6.36/1.36 % (840682)------------------------------
% 6.36/1.36 % (840682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.36 % (840682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.36 % (840682)CaDiCaL version: 2.1.3
% 6.36/1.36 % (840682)Termination reason: Instruction limit
% 6.36/1.36 % (840682)Termination phase: shuffling
% 6.36/1.36 % (840682)Time elapsed: 0.015 s
% 6.36/1.36 % (840682)Peak memory usage: 10 MB
% 6.36/1.36 % (840682)Instructions burned: 34 (million)
% 6.36/1.36 % (840687)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=4039340794:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2991 on theBenchmark for (2991ds/66Mi)
% 6.36/1.36 % (840679)Instruction limit reached!
% 6.36/1.36 % (840679)------------------------------
% 6.36/1.36 % (840679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.36 % (840679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.36 % (840679)CaDiCaL version: 2.1.3
% 6.36/1.36 % (840679)Termination reason: Instruction limit
% 6.36/1.36 % (840679)Termination phase: Saturation
% 6.36/1.36 % (840679)Time elapsed: 0.098 s
% 6.36/1.36 % (840679)Peak memory usage: 13 MB
% 6.36/1.36 % (840679)Instructions burned: 378 (million)
% 6.36/1.36 % (840684)Instruction limit reached!
% 6.36/1.36 % (840684)------------------------------
% 6.36/1.36 % (840684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.36 % (840684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.36 % (840684)CaDiCaL version: 2.1.3
% 6.36/1.36 % (840684)Termination reason: Instruction limit
% 6.36/1.36 % (840684)Termination phase: Saturation
% 6.36/1.36 % (840684)Time elapsed: 0.038 s
% 6.36/1.36 % (840684)Peak memory usage: 12 MB
% 6.36/1.36 % (840684)Instructions burned: 91 (million)
% 6.36/1.36 % (840689)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2911440806:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 6.36/1.36 % (840689)Instruction limit reached!
% 6.36/1.36 % (840689)------------------------------
% 6.36/1.36 % (840689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.36 % (840689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.36 % (840689)CaDiCaL version: 2.1.3
% 6.36/1.36 % (840689)Termination reason: Instruction limit
% 6.36/1.36 % (840689)Termination phase: Property scanning
% 6.36/1.36 % (840689)Time elapsed: 0.005 s
% 6.36/1.36 % (840689)Peak memory usage: 10 MB
% 6.36/1.36 % (840689)Instructions burned: 26 (million)
% 6.36/1.36 % (840687)Instruction limit reached!
% 6.36/1.36 % (840687)------------------------------
% 6.36/1.36 % (840687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.36 % (840687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.36 % (840687)CaDiCaL version: 2.1.3
% 6.36/1.36 % (840687)Termination reason: Instruction limit
% 6.36/1.36 % (840687)Termination phase: Saturation
% 6.36/1.36 % (840687)Time elapsed: 0.028 s
% 6.36/1.36 % (840687)Peak memory usage: 12 MB
% 6.36/1.36 % (840687)Instructions burned: 67 (million)
% 6.36/1.36 % (840692)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1101067979:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/28Mi)
% 6.36/1.36 % (840690)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=1586121722:i=338:bd=all:ins=4:rtra=on_2991 on theBenchmark for (2991ds/338Mi)
% 6.36/1.36 % (840693)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 6.36/1.36 % (840692)Instruction limit reached!
% 6.36/1.36 % (840692)------------------------------
% 6.36/1.36 % (840692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.36 % (840692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.36 % (840692)CaDiCaL version: 2.1.3
% 6.36/1.36 % (840692)Termination reason: Instruction limit
% 6.36/1.36 % (840692)Termination phase: Property scanning
% 6.36/1.36 % (840692)Time elapsed: 0.006 s
% 6.36/1.36 % (840692)Peak memory usage: 10 MB
% 7.50/1.57 % (840692)Instructions burned: 30 (million)
% 7.50/1.57 % (840693)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=979580686:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2991 on theBenchmark for (2991ds/137Mi)
% 7.50/1.57 % (840696)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=1755162112:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2991 on theBenchmark for (2991ds/340Mi)
% 7.50/1.57 % (840657)Instruction limit reached!
% 7.50/1.57 % (840657)------------------------------
% 7.50/1.57 % (840657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.50/1.57 % (840657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.50/1.57 % (840657)CaDiCaL version: 2.1.3
% 7.50/1.57 % (840657)Termination reason: Instruction limit
% 7.50/1.57 % (840657)Termination phase: Saturation
% 7.50/1.57 % (840657)Time elapsed: 0.339 s
% 7.50/1.57 % (840657)Peak memory usage: 15 MB
% 7.50/1.57 % (840657)Instructions burned: 874 (million)
% 7.50/1.57 % (840699)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=1393207317:i=227:sd=1:bd=all:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/227Mi)
% 7.50/1.57 % (840667)Instruction limit reached!
% 7.50/1.57 % (840667)------------------------------
% 7.50/1.57 % (840667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.50/1.57 % (840667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.50/1.57 % (840667)CaDiCaL version: 2.1.3
% 7.50/1.57 % (840667)Termination reason: Instruction limit
% 7.50/1.57 % (840667)Termination phase: Saturation
% 7.50/1.57 % (840667)Time elapsed: 0.299 s
% 7.50/1.57 % (840667)Peak memory usage: 14 MB
% 7.50/1.57 % (840667)Instructions burned: 572 (million)
% 7.50/1.57 % (840701)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.50/1.57 % (840693)Instruction limit reached!
% 7.50/1.57 % (840693)------------------------------
% 7.50/1.57 % (840693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.50/1.57 % (840693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.50/1.57 % (840693)CaDiCaL version: 2.1.3
% 7.50/1.57 % (840693)Termination reason: Instruction limit
% 7.50/1.57 % (840693)Termination phase: Saturation
% 7.50/1.57 % (840693)Time elapsed: 0.057 s
% 7.50/1.57 % (840693)Peak memory usage: 13 MB
% 7.50/1.57 % (840693)Instructions burned: 137 (million)
% 7.50/1.57 % (840699)Refutation not found, incomplete strategy
% 7.50/1.57 % (840699)------------------------------
% 7.50/1.57 % (840699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.50/1.57 % (840699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.50/1.57 % (840699)CaDiCaL version: 2.1.3
% 7.50/1.57 % (840699)Termination reason: Refutation not found, incomplete strategy
% 7.50/1.57 % (840699)Time elapsed: 0.024 s
% 7.50/1.57 % (840699)Peak memory usage: 12 MB
% 7.50/1.57 % (840699)Instructions burned: 55 (million)
% 7.50/1.57 % (840699)------------------------------
% 7.50/1.57 % (840699)------------------------------
% 7.50/1.57 % (840701)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2338022365:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/373Mi)
% 7.50/1.57 % (840702)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=638620577:i=116:ep=RSTC:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/116Mi)
% 7.50/1.57 % (840704)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=525501540:i=575:rtra=on_2990 on theBenchmark for (2990ds/575Mi)
% 7.50/1.57 % (840696)Instruction limit reached!
% 7.50/1.57 % (840696)------------------------------
% 7.50/1.57 % (840696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.50/1.57 % (840696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.50/1.57 % (840696)CaDiCaL version: 2.1.3
% 7.50/1.57 % (840696)Termination reason: Instruction limit
% 7.50/1.57 % (840696)Termination phase: Saturation
% 7.50/1.57 % (840696)Time elapsed: 0.085 s
% 7.50/1.57 % (840696)Peak memory usage: 14 MB
% 7.50/1.57 % (840696)Instructions burned: 342 (million)
% 7.50/1.57 % (840707)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=3740846513:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2990 on theBenchmark for (2990ds/270Mi)
% 8.80/1.70 % (840702)Instruction limit reached!
% 8.80/1.70 % (840702)------------------------------
% 8.80/1.70 % (840702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.70 % (840702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.70 % (840702)CaDiCaL version: 2.1.3
% 8.80/1.70 % (840702)Termination reason: Instruction limit
% 8.80/1.70 % (840702)Termination phase: Saturation
% 8.80/1.70 % (840702)Time elapsed: 0.052 s
% 8.80/1.70 % (840702)Peak memory usage: 13 MB
% 8.80/1.70 % (840702)Instructions burned: 117 (million)
% 8.80/1.70 % (840709)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=4219242498: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_2989 on theBenchmark for (2989ds/9840Mi)
% 8.80/1.70 % (840690)Instruction limit reached!
% 8.80/1.70 % (840690)------------------------------
% 8.80/1.70 % (840690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.70 % (840690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.70 % (840690)CaDiCaL version: 2.1.3
% 8.80/1.70 % (840690)Termination reason: Instruction limit
% 8.80/1.70 % (840690)Termination phase: Saturation
% 8.80/1.70 % (840690)Time elapsed: 0.168 s
% 8.80/1.70 % (840690)Peak memory usage: 16 MB
% 8.80/1.70 % (840690)Instructions burned: 339 (million)
% 8.80/1.70 % (840681)Instruction limit reached!
% 8.80/1.70 % (840681)------------------------------
% 8.80/1.70 % (840681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.70 % (840681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.70 % (840681)CaDiCaL version: 2.1.3
% 8.80/1.70 % (840681)Termination reason: Instruction limit
% 8.80/1.70 % (840681)Termination phase: Saturation
% 8.80/1.70 % (840681)Time elapsed: 0.258 s
% 8.80/1.70 % (840681)Peak memory usage: 15 MB
% 8.80/1.70 % (840681)Instructions burned: 496 (million)
% 8.80/1.70 % (840707)Instruction limit reached!
% 8.80/1.70 % (840707)------------------------------
% 8.80/1.70 % (840707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.70 % (840707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.70 % (840707)CaDiCaL version: 2.1.3
% 8.80/1.70 % (840707)Termination reason: Instruction limit
% 8.80/1.70 % (840707)Termination phase: Saturation
% 8.80/1.70 % (840707)Time elapsed: 0.069 s
% 8.80/1.70 % (840707)Peak memory usage: 14 MB
% 8.80/1.70 % (840707)Instructions burned: 270 (million)
% 8.80/1.70 % (840711)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=3199063354:i=421:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/421Mi)
% 8.80/1.70 % (840712)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
% 8.80/1.70 % (840713)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=655126207:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/31Mi)
% 8.80/1.70 % (840712)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=1727744908:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/270Mi)
% 8.80/1.70 % (840713)Instruction limit reached!
% 8.80/1.70 % (840713)------------------------------
% 8.80/1.70 % (840713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.70 % (840713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.70 % (840713)CaDiCaL version: 2.1.3
% 8.80/1.70 % (840713)Termination reason: Instruction limit
% 8.80/1.70 % (840713)Termination phase: Property scanning
% 8.80/1.70 % (840713)Time elapsed: 0.008 s
% 8.80/1.70 % (840713)Peak memory usage: 10 MB
% 8.80/1.70 % (840713)Instructions burned: 36 (million)
% 8.80/1.70 % (840717)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 8.80/1.70 % (840717)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
% 9.66/1.83 % (840717)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=472494936:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2989 on theBenchmark for (2989ds/1440Mi)
% 9.66/1.83 % (840701)Instruction limit reached!
% 9.66/1.83 % (840701)------------------------------
% 9.66/1.83 % (840701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.66/1.83 % (840701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.83 % (840701)CaDiCaL version: 2.1.3
% 9.66/1.83 % (840701)Termination reason: Instruction limit
% 9.66/1.83 % (840701)Termination phase: Saturation
% 9.66/1.83 % (840701)Time elapsed: 0.178 s
% 9.66/1.83 % (840701)Peak memory usage: 13 MB
% 9.66/1.83 % (840701)Instructions burned: 374 (million)
% 9.66/1.83 % (840719)dis+10_2_sil=128000:si=on:random_seed=1677072306:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2988 on theBenchmark for (2988ds/339Mi)
% 9.66/1.83 % (840712)Instruction limit reached!
% 9.66/1.83 % (840712)------------------------------
% 9.66/1.83 % (840712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.66/1.83 % (840712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.83 % (840712)CaDiCaL version: 2.1.3
% 9.66/1.83 % (840712)Termination reason: Instruction limit
% 9.66/1.83 % (840712)Termination phase: Saturation
% 9.66/1.83 % (840712)Time elapsed: 0.130 s
% 9.66/1.83 % (840712)Peak memory usage: 14 MB
% 9.66/1.83 % (840712)Instructions burned: 270 (million)
% 9.66/1.83 % (840721)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=134205204:i=111:add=on:fgj=on:rtra=on:fdi=1024_2988 on theBenchmark for (2988ds/111Mi)
% 9.66/1.83 % (840704)Instruction limit reached!
% 9.66/1.83 % (840704)------------------------------
% 9.66/1.83 % (840704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.66/1.83 % (840704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.83 % (840704)CaDiCaL version: 2.1.3
% 9.66/1.83 % (840704)Termination reason: Instruction limit
% 9.66/1.83 % (840704)Termination phase: Saturation
% 9.66/1.83 % (840704)Time elapsed: 0.267 s
% 9.66/1.83 % (840704)Peak memory usage: 15 MB
% 9.66/1.83 % (840704)Instructions burned: 575 (million)
% 9.66/1.83 % (840723)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=3142813951:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2987 on theBenchmark for (2987ds/122Mi)
% 9.66/1.83 % (840711)Instruction limit reached!
% 9.66/1.83 % (840711)------------------------------
% 9.66/1.83 % (840711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.66/1.83 % (840711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.83 % (840711)CaDiCaL version: 2.1.3
% 9.66/1.83 % (840711)Termination reason: Instruction limit
% 9.66/1.83 % (840711)Termination phase: Saturation
% 9.66/1.83 % (840711)Time elapsed: 0.191 s
% 9.66/1.83 % (840711)Peak memory usage: 14 MB
% 9.66/1.83 % (840711)Instructions burned: 422 (million)
% 9.66/1.83 % (840721)Instruction limit reached!
% 9.66/1.83 % (840721)------------------------------
% 9.66/1.83 % (840721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.66/1.83 % (840721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.83 % (840721)CaDiCaL version: 2.1.3
% 9.66/1.83 % (840721)Termination reason: Instruction limit
% 9.66/1.83 % (840721)Termination phase: Saturation
% 9.66/1.83 % (840721)Time elapsed: 0.050 s
% 9.66/1.83 % (840721)Peak memory usage: 13 MB
% 9.66/1.83 % (840721)Instructions burned: 112 (million)
% 9.66/1.83 % (840725)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=3890906030:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/136Mi)
% 9.66/1.83 % (840726)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=637488218:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2987 on theBenchmark for (2987ds/232Mi)
% 9.66/1.83 % (840719)Instruction limit reached!
% 9.66/1.83 % (840719)------------------------------
% 9.66/1.83 % (840719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.66/1.83 % (840719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/1.95 % (840719)CaDiCaL version: 2.1.3
% 10.28/1.95 % (840719)Termination reason: Instruction limit
% 10.28/1.95 % (840719)Termination phase: Saturation
% 10.28/1.95 % (840719)Time elapsed: 0.153 s
% 10.28/1.95 % (840719)Peak memory usage: 13 MB
% 10.28/1.95 % (840719)Instructions burned: 339 (million)
% 10.28/1.95 % (840723)Refutation not found, incomplete strategy
% 10.28/1.95 % (840723)------------------------------
% 10.28/1.95 % (840723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.28/1.95 % (840723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/1.95 % (840723)CaDiCaL version: 2.1.3
% 10.28/1.95 % (840723)Termination reason: Refutation not found, incomplete strategy
% 10.28/1.95 % (840723)Time elapsed: 0.049 s
% 10.28/1.95 % (840723)Peak memory usage: 13 MB
% 10.28/1.95 % (840723)Instructions burned: 108 (million)
% 10.28/1.95 % (840723)------------------------------
% 10.28/1.95 % (840723)------------------------------
% 10.28/1.95 % (840730)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 10.28/1.95 % (840729)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=3459193202:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2987 on theBenchmark for (2987ds/1254Mi)
% 10.28/1.95 % (840730)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=1556487013:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2987 on theBenchmark for (2987ds/281Mi)
% 10.28/1.95 % (840725)Refutation not found, incomplete strategy
% 10.28/1.95 % (840725)------------------------------
% 10.28/1.95 % (840725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.28/1.95 % (840725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/1.95 % (840725)CaDiCaL version: 2.1.3
% 10.28/1.95 % (840725)Termination reason: Refutation not found, incomplete strategy
% 10.28/1.95 % (840725)Time elapsed: 0.048 s
% 10.28/1.95 % (840725)Peak memory usage: 13 MB
% 10.28/1.95 % (840725)Instructions burned: 110 (million)
% 10.28/1.95 % (840725)------------------------------
% 10.28/1.95 % (840725)------------------------------
% 10.28/1.95 % (840733)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2201363226:i=619:add=on:rtra=on_2986 on theBenchmark for (2986ds/619Mi)
% 10.28/1.95 % (840733)Refutation not found, incomplete strategy
% 10.28/1.95 % (840733)------------------------------
% 10.28/1.95 % (840733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.28/1.95 % (840733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/1.95 % (840733)CaDiCaL version: 2.1.3
% 10.28/1.95 % (840733)Termination reason: Refutation not found, incomplete strategy
% 10.28/1.95 % (840733)Time elapsed: 0.065 s
% 10.28/1.95 % (840733)Peak memory usage: 15 MB
% 10.28/1.95 % (840733)Instructions burned: 149 (million)
% 10.28/1.95 % (840733)------------------------------
% 10.28/1.95 % (840733)------------------------------
% 10.28/1.95 % (840729)Refutation not found, incomplete strategy
% 10.28/1.95 % (840729)------------------------------
% 10.28/1.95 % (840729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.28/1.95 % (840729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/1.95 % (840729)CaDiCaL version: 2.1.3
% 10.28/1.95 % (840729)Termination reason: Refutation not found, incomplete strategy
% 10.28/1.95 % (840729)Time elapsed: 0.099 s
% 10.28/1.95 % (840729)Peak memory usage: 15 MB
% 10.28/1.95 % (840729)Instructions burned: 227 (million)
% 10.28/1.95 % (840729)------------------------------
% 10.28/1.95 % (840729)------------------------------
% 10.28/1.95 % (840726)Instruction limit reached!
% 10.28/1.95 % (840726)------------------------------
% 10.28/1.95 % (840726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.28/1.95 % (840726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/1.95 % (840726)CaDiCaL version: 2.1.3
% 10.28/1.95 % (840726)Termination reason: Instruction limit
% 10.28/1.95 % (840726)Termination phase: Saturation
% 10.28/1.95 % (840726)Time elapsed: 0.141 s
% 10.28/1.95 % (840726)Peak memory usage: 13 MB
% 10.28/1.95 % (840726)Instructions burned: 233 (million)
% 10.28/1.95 % (840735)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=1414863833:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/865Mi)
% 13.75/2.35 % (840736)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2642481470:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/212Mi)
% 13.75/2.35 % (840717)Instruction limit reached!
% 13.75/2.35 % (840717)------------------------------
% 13.75/2.35 % (840717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.75/2.35 % (840717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.75/2.35 % (840717)CaDiCaL version: 2.1.3
% 13.75/2.35 % (840717)Termination reason: Instruction limit
% 13.75/2.35 % (840717)Termination phase: Saturation
% 13.75/2.35 % (840717)Time elapsed: 0.354 s
% 13.75/2.35 % (840717)Peak memory usage: 16 MB
% 13.75/2.35 % (840717)Instructions burned: 1444 (million)
% 13.75/2.35 % (840730)Instruction limit reached!
% 13.75/2.35 % (840730)------------------------------
% 13.75/2.35 % (840730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.75/2.35 % (840730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.75/2.35 % (840730)CaDiCaL version: 2.1.3
% 13.75/2.35 % (840730)Termination reason: Instruction limit
% 13.75/2.35 % (840730)Termination phase: Saturation
% 13.75/2.35 % (840730)Time elapsed: 0.124 s
% 13.75/2.35 % (840730)Peak memory usage: 14 MB
% 13.75/2.35 % (840730)Instructions burned: 283 (million)
% 13.75/2.35 % (840738)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=2008062924:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/130Mi)
% 13.75/2.35 % (840740)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2388529752:st=1.5:i=346:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/346Mi)
% 13.75/2.35 % (840741)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=2252058991:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/152Mi)
% 13.75/2.35 % (840738)Instruction limit reached!
% 13.75/2.35 % (840738)------------------------------
% 13.75/2.35 % (840738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.75/2.35 % (840738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.75/2.35 % (840738)CaDiCaL version: 2.1.3
% 13.75/2.35 % (840738)Termination reason: Instruction limit
% 13.75/2.35 % (840738)Termination phase: Saturation
% 13.75/2.35 % (840738)Time elapsed: 0.063 s
% 13.75/2.35 % (840738)Peak memory usage: 13 MB
% 13.75/2.35 % (840738)Instructions burned: 132 (million)
% 13.75/2.35 % (840741)Instruction limit reached!
% 13.75/2.35 % (840741)------------------------------
% 13.75/2.35 % (840741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.75/2.35 % (840741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.75/2.35 % (840741)CaDiCaL version: 2.1.3
% 13.75/2.35 % (840741)Termination reason: Instruction limit
% 13.75/2.35 % (840741)Termination phase: Saturation
% 13.75/2.35 % (840741)Time elapsed: 0.069 s
% 13.75/2.35 % (840741)Peak memory usage: 14 MB
% 13.75/2.35 % (840741)Instructions burned: 153 (million)
% 13.75/2.35 % (840736)Instruction limit reached!
% 13.75/2.35 % (840736)------------------------------
% 13.75/2.35 % (840736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.75/2.35 % (840736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.75/2.35 % (840736)CaDiCaL version: 2.1.3
% 13.75/2.35 % (840736)Termination reason: Instruction limit
% 13.75/2.35 % (840736)Termination phase: Saturation
% 13.75/2.35 % (840736)Time elapsed: 0.097 s
% 13.75/2.35 % (840736)Peak memory usage: 13 MB
% 13.75/2.35 % (840736)Instructions burned: 213 (million)
% 13.75/2.35 % (840745)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=69408449:i=75:ep=R:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/75Mi)
% 13.75/2.35 % (840740)Instruction limit reached!
% 13.75/2.35 % (840740)------------------------------
% 13.75/2.35 % (840740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.75/2.35 % (840740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.75/2.35 % (840740)CaDiCaL version: 2.1.3
% 13.75/2.35 % (840740)Termination reason: Instruction limit
% 13.75/2.35 % (840740)Termination phase: Saturation
% 13.75/2.35 % (840740)Time elapsed: 0.088 s
% 13.75/2.35 % (840740)Peak memory usage: 15 MB
% 13.75/2.35 % (840740)Instructions burned: 346 (million)
% 13.75/2.35 % (840749)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=4246297052:i=161:piset=and:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/161Mi)
% 13.75/2.35 % (840746)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=2382697108:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/387Mi)
% 14.31/2.48 % (840747)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=1690731777:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2984 on theBenchmark for (2984ds/148Mi)
% 14.31/2.48 % (840745)Instruction limit reached!
% 14.31/2.48 % (840745)------------------------------
% 14.31/2.48 % (840745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.31/2.48 % (840745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.31/2.48 % (840745)CaDiCaL version: 2.1.3
% 14.31/2.48 % (840745)Termination reason: Instruction limit
% 14.31/2.48 % (840745)Termination phase: Property scanning
% 14.31/2.48 % (840745)Time elapsed: 0.054 s
% 14.31/2.48 % (840745)Peak memory usage: 11 MB
% 14.31/2.48 % (840745)Instructions burned: 76 (million)
% 14.31/2.48 % (840749)Instruction limit reached!
% 14.31/2.48 % (840749)------------------------------
% 14.31/2.48 % (840749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.31/2.48 % (840749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.31/2.48 % (840749)CaDiCaL version: 2.1.3
% 14.31/2.48 % (840749)Termination reason: Instruction limit
% 14.31/2.48 % (840749)Termination phase: Saturation
% 14.31/2.48 % (840749)Time elapsed: 0.041 s
% 14.31/2.48 % (840749)Peak memory usage: 13 MB
% 14.31/2.48 % (840749)Instructions burned: 162 (million)
% 14.31/2.48 % (840754)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=2132975894:i=136:add=on:ins=4:rtra=on:sup=off_2984 on theBenchmark for (2984ds/136Mi)
% 14.31/2.48 % (840753)lrs+10_1_sil=128000:si=on:random_seed=2186938651:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/888Mi)
% 14.31/2.48 % (840747)Instruction limit reached!
% 14.31/2.48 % (840747)------------------------------
% 14.31/2.48 % (840747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.31/2.48 % (840747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.31/2.48 % (840747)CaDiCaL version: 2.1.3
% 14.31/2.48 % (840747)Termination reason: Instruction limit
% 14.31/2.48 % (840747)Termination phase: Saturation
% 14.31/2.48 % (840747)Time elapsed: 0.061 s
% 14.31/2.48 % (840747)Peak memory usage: 13 MB
% 14.31/2.48 % (840747)Instructions burned: 149 (million)
% 14.31/2.48 % (840754)Instruction limit reached!
% 14.31/2.48 % (840754)------------------------------
% 14.31/2.48 % (840754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.31/2.48 % (840754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.31/2.48 % (840754)CaDiCaL version: 2.1.3
% 14.31/2.48 % (840754)Termination reason: Instruction limit
% 14.31/2.48 % (840754)Termination phase: Saturation
% 14.31/2.48 % (840754)Time elapsed: 0.033 s
% 14.31/2.48 % (840754)Peak memory usage: 13 MB
% 14.31/2.48 % (840754)Instructions burned: 138 (million)
% 14.31/2.48 % (840757)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=3926077816:i=88:s2at=3:nm=2:rtra=on:rawr=on_2983 on theBenchmark for (2983ds/88Mi)
% 14.31/2.48 % (840759)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=551049122:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2983 on theBenchmark for (2983ds/93Mi)
% 14.31/2.48 % (840759)Instruction limit reached!
% 14.31/2.48 % (840759)------------------------------
% 14.31/2.48 % (840759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.31/2.48 % (840759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.31/2.48 % (840759)CaDiCaL version: 2.1.3
% 14.31/2.48 % (840759)Termination reason: Instruction limit
% 14.31/2.48 % (840759)Termination phase: Property scanning
% 14.31/2.48 % (840759)Time elapsed: 0.020 s
% 14.31/2.48 % (840759)Peak memory usage: 11 MB
% 14.31/2.48 % (840759)Instructions burned: 94 (million)
% 14.31/2.48 % (840757)Instruction limit reached!
% 14.31/2.48 % (840757)------------------------------
% 14.31/2.48 % (840757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.31/2.48 % (840757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.31/2.48 % (840757)CaDiCaL version: 2.1.3
% 14.31/2.48 % (840757)Termination reason: Instruction limit
% 15.68/2.63 % (840757)Termination phase: Property scanning
% 15.68/2.63 % (840757)Time elapsed: 0.038 s
% 15.68/2.63 % (840757)Peak memory usage: 11 MB
% 15.68/2.63 % (840757)Instructions burned: 89 (million)
% 15.68/2.63 % (840761)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3043206796:i=2186:rtra=on:ixr=off_2983 on theBenchmark for (2983ds/2186Mi)
% 15.68/2.63 % (840762)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=328510322:s2a=on:i=240:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/240Mi)
% 15.68/2.63 % (840746)Instruction limit reached!
% 15.68/2.63 % (840746)------------------------------
% 15.68/2.63 % (840746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.63 % (840746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.63 % (840746)CaDiCaL version: 2.1.3
% 15.68/2.63 % (840746)Termination reason: Instruction limit
% 15.68/2.63 % (840746)Termination phase: Saturation
% 15.68/2.63 % (840746)Time elapsed: 0.163 s
% 15.68/2.63 % (840746)Peak memory usage: 14 MB
% 15.68/2.63 % (840746)Instructions burned: 387 (million)
% 15.68/2.63 % (840765)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=2904242176:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2982 on theBenchmark for (2982ds/805Mi)
% 15.68/2.63 % (840762)Instruction limit reached!
% 15.68/2.63 % (840762)------------------------------
% 15.68/2.63 % (840762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.63 % (840762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.63 % (840762)CaDiCaL version: 2.1.3
% 15.68/2.63 % (840762)Termination reason: Instruction limit
% 15.68/2.63 % (840762)Termination phase: Saturation
% 15.68/2.63 % (840762)Time elapsed: 0.167 s
% 15.68/2.63 % (840762)Peak memory usage: 14 MB
% 15.68/2.63 % (840762)Instructions burned: 240 (million)
% 15.68/2.63 % (840735)Instruction limit reached!
% 15.68/2.63 % (840735)------------------------------
% 15.68/2.63 % (840735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.63 % (840735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.63 % (840735)CaDiCaL version: 2.1.3
% 15.68/2.63 % (840735)Termination reason: Instruction limit
% 15.68/2.63 % (840735)Termination phase: Saturation
% 15.68/2.63 % (840735)Time elapsed: 0.445 s
% 15.68/2.63 % (840735)Peak memory usage: 18 MB
% 15.68/2.63 % (840735)Instructions burned: 865 (million)
% 15.68/2.63 % (840768)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 15.68/2.63 % (840769)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=163531802:i=355:av=off:fsr=off:rtra=on:ixr=off_2981 on theBenchmark for (2981ds/355Mi)
% 15.68/2.63 % (840768)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=3695662468:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2981 on theBenchmark for (2981ds/391Mi)
% 15.68/2.63 % (840753)Instruction limit reached!
% 15.68/2.63 % (840753)------------------------------
% 15.68/2.63 % (840753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.63 % (840753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.63 % (840753)CaDiCaL version: 2.1.3
% 15.68/2.63 % (840753)Termination reason: Instruction limit
% 15.68/2.63 % (840753)Termination phase: Saturation
% 15.68/2.63 % (840753)Time elapsed: 0.384 s
% 15.68/2.63 % (840753)Peak memory usage: 15 MB
% 15.68/2.63 % (840753)Instructions burned: 891 (million)
% 15.68/2.63 % (840772)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=598557569:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/314Mi)
% 15.68/2.63 % (840761)Instruction limit reached!
% 15.68/2.63 % (840761)------------------------------
% 15.68/2.63 % (840761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.63 % (840761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.63 % (840761)CaDiCaL version: 2.1.3
% 15.68/2.63 % (840761)Termination reason: Instruction limit
% 15.68/2.63 % (840761)Termination phase: Saturation
% 15.68/2.63 % (840761)Time elapsed: 0.392 s
% 15.68/2.63 % (840761)Peak memory usage: 15 MB
% 15.68/2.63 % (840761)Instructions burned: 2189 (million)
% 15.68/2.63 % (840769)Instruction limit reached!
% 15.68/2.63 % (840769)------------------------------
% 15.68/2.63 % (840769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840769)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840769)Termination reason: Instruction limit
% 15.68/2.69 % (840769)Termination phase: Saturation
% 15.68/2.69 % (840769)Time elapsed: 0.181 s
% 15.68/2.69 % (840769)Peak memory usage: 13 MB
% 15.68/2.69 % (840769)Instructions burned: 356 (million)
% 15.68/2.69 % (840774)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=1214158646:s2a=on:i=251:fsr=off:rtra=on_2979 on theBenchmark for (2979ds/251Mi)
% 15.68/2.69 % (840775)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=3424901518: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_2979 on theBenchmark for (2979ds/2470Mi)
% 15.68/2.69 % (840765)Instruction limit reached!
% 15.68/2.69 % (840765)------------------------------
% 15.68/2.69 % (840765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840765)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840765)Termination reason: Instruction limit
% 15.68/2.69 % (840765)Termination phase: Saturation
% 15.68/2.69 % (840765)Time elapsed: 0.378 s
% 15.68/2.69 % (840765)Peak memory usage: 16 MB
% 15.68/2.69 % (840765)Instructions burned: 806 (million)
% 15.68/2.69 % (840778)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=2696450683:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2978 on theBenchmark for (2978ds/673Mi)
% 15.68/2.69 % (840774)Instruction limit reached!
% 15.68/2.69 % (840774)------------------------------
% 15.68/2.69 % (840774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840774)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840774)Termination reason: Instruction limit
% 15.68/2.69 % (840774)Termination phase: Saturation
% 15.68/2.69 % (840774)Time elapsed: 0.063 s
% 15.68/2.69 % (840774)Peak memory usage: 14 MB
% 15.68/2.69 % (840774)Instructions burned: 252 (million)
% 15.68/2.69 % (840780)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=492180178:i=116:ep=RSTC:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/116Mi)
% 15.68/2.69 % (840772)Instruction limit reached!
% 15.68/2.69 % (840772)------------------------------
% 15.68/2.69 % (840772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840772)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840772)Termination reason: Instruction limit
% 15.68/2.69 % (840772)Termination phase: Saturation
% 15.68/2.69 % (840772)Time elapsed: 0.143 s
% 15.68/2.69 % (840772)Peak memory usage: 14 MB
% 15.68/2.69 % (840772)Instructions burned: 316 (million)
% 15.68/2.69 % (840782)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2750160064:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2978 on theBenchmark for (2978ds/270Mi)
% 15.68/2.69 % (840780)Instruction limit reached!
% 15.68/2.69 % (840780)------------------------------
% 15.68/2.69 % (840780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840780)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840780)Termination reason: Instruction limit
% 15.68/2.69 % (840780)Termination phase: Saturation
% 15.68/2.69 % (840780)Time elapsed: 0.028 s
% 15.68/2.69 % (840780)Peak memory usage: 13 MB
% 15.68/2.69 % (840780)Instructions burned: 119 (million)
% 15.68/2.69 % (840784)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=743197889: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_2978 on theBenchmark for (2978ds/30Mi)
% 15.68/2.69 % (840784)Instruction limit reached!
% 15.68/2.69 % (840784)------------------------------
% 15.68/2.69 % (840784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840784)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840784)Termination reason: Instruction limit
% 15.68/2.69 % (840784)Termination phase: shuffling
% 15.68/2.69 % (840784)Time elapsed: 0.007 s
% 15.68/2.69 % (840784)Peak memory usage: 10 MB
% 15.68/2.69 % (840784)Instructions burned: 34 (million)
% 15.68/2.69 % (840786)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 15.68/2.69 % (840786)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=503221776:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2978 on theBenchmark for (2978ds/39Mi)
% 15.68/2.69 % (840768)Instruction limit reached!
% 15.68/2.69 % (840768)------------------------------
% 15.68/2.69 % (840768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840768)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840768)Termination reason: Instruction limit
% 15.68/2.69 % (840768)Termination phase: Saturation
% 15.68/2.69 % (840768)Time elapsed: 0.319 s
% 15.68/2.69 % (840768)Peak memory usage: 15 MB
% 15.68/2.69 % (840768)Instructions burned: 391 (million)
% 15.68/2.69 % (840788)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1628145199:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2977 on theBenchmark for (2977ds/365Mi)
% 15.68/2.69 % (840786)Instruction limit reached!
% 15.68/2.69 % (840786)------------------------------
% 15.68/2.69 % (840786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840786)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840786)Termination reason: Instruction limit
% 15.68/2.69 % (840786)Termination phase: Property scanning
% 15.68/2.69 % (840786)Time elapsed: 0.025 s
% 15.68/2.69 % (840786)Peak memory usage: 10 MB
% 15.68/2.69 % (840786)Instructions burned: 40 (million)
% 15.68/2.69 % (840790)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2120427768:i=158:av=off:rtra=on_2977 on theBenchmark for (2977ds/158Mi)
% 15.68/2.69 % (840782)Instruction limit reached!
% 15.68/2.69 % (840782)------------------------------
% 15.68/2.69 % (840782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840782)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840782)Termination reason: Instruction limit
% 15.68/2.69 % (840782)Termination phase: Saturation
% 15.68/2.69 % (840782)Time elapsed: 0.130 s
% 15.68/2.69 % (840782)Peak memory usage: 14 MB
% 15.68/2.69 % (840782)Instructions burned: 271 (million)
% 15.68/2.69 % (840788)Instruction limit reached!
% 15.68/2.69 % (840788)------------------------------
% 15.68/2.69 % (840788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840788)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840788)Termination reason: Instruction limit
% 15.68/2.69 % (840788)Termination phase: Saturation
% 15.68/2.69 % (840788)Time elapsed: 0.091 s
% 15.68/2.69 % (840788)Peak memory usage: 14 MB
% 15.68/2.69 % (840788)Instructions burned: 367 (million)
% 15.68/2.69 % (840792)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
% 15.68/2.69 % (840792)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=3716337018:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2977 on theBenchmark for (2977ds/252Mi)
% 15.68/2.69 % (840793)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=2950059686:i=213:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/213Mi)
% 15.68/2.69 % (840793)Refutation not found, incomplete strategy
% 15.68/2.69 % (840793)------------------------------
% 15.68/2.69 % (840793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840793)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840793)Termination reason: Refutation not found, incomplete strategy
% 15.68/2.69 % (840793)Time elapsed: 0.023 s
% 15.68/2.69 % (840793)Peak memory usage: 13 MB
% 15.68/2.69 % (840793)Instructions burned: 89 (million)
% 15.68/2.69 % (840793)------------------------------
% 15.68/2.69 % (840793)------------------------------
% 15.68/2.69 % (840778)Instruction limit reached!
% 15.68/2.69 % (840778)------------------------------
% 15.68/2.69 % (840778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840778)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840778)Termination reason: Instruction limit
% 15.68/2.69 % (840778)Termination phase: Saturation
% 15.68/2.69 % (840778)Time elapsed: 0.252 s
% 15.68/2.69 % (840778)Peak memory usage: 14 MB
% 15.68/2.69 % (840778)Instructions burned: 675 (million)
% 15.68/2.69 % (840796)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=2764670977:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2976 on theBenchmark for (2976ds/160Mi)
% 15.68/2.69 % (840797)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=930639496:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2976 on theBenchmark for (2976ds/763Mi)
% 15.68/2.69 % (840790)Instruction limit reached!
% 15.68/2.69 % (840790)------------------------------
% 15.68/2.69 % (840790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.69 % (840790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.69 % (840790)CaDiCaL version: 2.1.3
% 15.68/2.69 % (840790)Termination reason: Instruction limit
% 15.68/2.69 % (840790)Termination phase: Saturation
% 15.68/2.69 % (840790)Time elapsed: 0.131 s
% 15.68/2.69 % (840790)Peak memory usage: 13 MB
% 15.68/2.69 % (840790)Instructions burned: 158 (million)
% 15.68/2.69 % (840675) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-840538-840675"...
% 15.68/2.69 % (840675)...printing done.
% 15.68/2.69 % (840675)Refutation found. Thanks to Tanya!
% 15.68/2.69 % SZS status Theorem for theBenchmark
% 15.68/2.69 % SZS output start Proof for theBenchmark
% 15.68/2.69 thf(type_def_5, type, set_real: $tType).
% 15.68/2.69 thf(type_def_6, type, set_a: $tType).
% 15.68/2.69 thf(type_def_7, type, real: $tType).
% 15.68/2.69 thf(type_def_8, type, a: $tType).
% 15.68/2.69 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 15.68/2.69 thf(func_def_0, type, auto_l612940ivl0_a: ((a > a) > set_a > a > set_real)).
% 15.68/2.69 thf(func_def_1, type, auto_ll_on_flow0_a: ((a > a) > set_a > a > real > a)).
% 15.68/2.69 thf(func_def_2, type, minus_minus_real: (real > real > real)).
% 15.68/2.69 thf(func_def_3, type, minus_minus_a: (a > a > a)).
% 15.68/2.69 thf(func_def_4, type, plus_plus_real: (real > real > real)).
% 15.68/2.69 thf(func_def_5, type, plus_plus_a: (a > a > a)).
% 15.68/2.69 thf(func_def_6, type, uminus_uminus_a_a: ((a > a) > a > a)).
% 15.68/2.69 thf(func_def_7, type, uminus_uminus_real: (real > real)).
% 15.68/2.69 thf(func_def_8, type, uminus_uminus_a: (a > a)).
% 15.68/2.69 thf(func_def_9, type, zero_zero_real: real).
% 15.68/2.69 thf(func_def_10, type, zero_zero_a: a).
% 15.68/2.69 thf(func_def_11, type, initia826609931terval: (set_real > $o)).
% 15.68/2.69 thf(func_def_12, type, bot_bot_set_real: set_real).
% 15.68/2.69 thf(func_def_13, type, ord_less_real: (real > real > $o)).
% 15.68/2.69 thf(func_def_14, type, ord_less_a: (a > a > $o)).
% 15.68/2.69 thf(func_def_15, type, top_top_set_real: set_real).
% 15.68/2.69 thf(func_def_16, type, period720806154rbit_a: ((a > a) > set_a > a > $o)).
% 15.68/2.69 thf(func_def_17, type, period1305449585riod_a: ((a > a) > set_a > a > real)).
% 15.68/2.69 thf(func_def_18, type, period138238489rbit_a: ((a > a) > set_a > a > $o)).
% 15.68/2.69 thf(func_def_19, type, collect_real: ((real > $o) > set_real)).
% 15.68/2.69 thf(func_def_20, type, collect_a: ((a > $o) > set_a)).
% 15.68/2.69 thf(func_def_21, type, member_real: (real > set_real > $o)).
% 15.68/2.69 thf(func_def_22, type, member_a: (a > set_a > $o)).
% 15.68/2.69 thf(func_def_23, type, x: set_a).
% 15.68/2.69 thf(func_def_24, type, d: real).
% 15.68/2.69 thf(func_def_25, type, f: (a > a)).
% 15.68/2.69 thf(func_def_26, type, i1: real).
% 15.68/2.69 thf(func_def_27, type, i2: real).
% 15.68/2.69 thf(func_def_28, type, ss: real).
% 15.68/2.69 thf(func_def_29, type, t: real).
% 15.68/2.69 thf(func_def_30, type, tt: real).
% 15.68/2.69 thf(func_def_31, type, x2: a).
% 15.68/2.69 thf(func_def_32, type, xx: a).
% 15.68/2.69 thf(func_def_36, type, db0: !>[X0: $tType]:(X0)).
% 15.68/2.69 thf(func_def_37, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 15.68/2.69 thf(func_def_38, type, db1: !>[X0: $tType]:(X0)).
% 15.68/2.69 thf(func_def_39, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 15.68/2.69 thf(f3,axiom,(
% 15.68/2.69 (((auto_ll_on_flow0_a @ f @ x @ xx @ tt)) = ((auto_ll_on_flow0_a @ f @ x @ x2 @ ss)))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_eq)).
% 15.68/2.69 thf(f5,axiom,(
% 15.68/2.69 (member_real @ tt @ (auto_l612940ivl0_a @ f @ x @ xx))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_tt__ex)).
% 15.68/2.69 thf(f6,axiom,(
% 15.68/2.69 (member_real @ ss @ (auto_l612940ivl0_a @ f @ x @ x2))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_ss__ex)).
% 15.68/2.69 thf(f12,axiom,(
% 15.68/2.69 ! [X1 : real,X0 : real,X2 : a] : ((member_real @ (minus_minus_real @ X0 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2)) => (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X0 @ X1)) @ (minus_minus_real @ X1 @ X0))) = X2))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_general_Oflows__reverse)).
% 15.68/2.69 thf(f32,axiom,(
% 15.68/2.69 ! [X0 : real] : (((minus_minus_real @ zero_zero_real @ X0)) = ((uminus_uminus_real @ X0)))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_31_verit__minus__simplify_I3_J)).
% 15.68/2.69 thf(f34,axiom,(
% 15.68/2.69 ! [X1 : a,X0 : real] : ((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X1)) => (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ X0) @ (minus_minus_real @ zero_zero_real @ X0))) = X1))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_33_local_Oflows__reverse)).
% 15.68/2.69 thf(f35,axiom,(
% 15.68/2.69 ! [X0 : real,X1 : a] : ((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X1)) => (member_real @ (minus_minus_real @ zero_zero_real @ X0) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ X0))))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_34_local_Oexistence__ivl__reverse)).
% 15.68/2.69 thf(f167,axiom,(
% 15.68/2.69 ! [X1 : real,X2 : a,X0 : real,X3 : real] : ((member_real @ (minus_minus_real @ X0 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2)) => ((member_real @ X3 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X0 @ X1)))) => (((auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ (plus_plus_real @ X0 @ X3) @ X1))) = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X0 @ X1)) @ X3)))))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_166_general_Oflow__trans)).
% 15.68/2.69 thf(f169,axiom,(
% 15.68/2.69 ! [X3 : real,X1 : real,X2 : a,X0 : real] : ((member_real @ (minus_minus_real @ X0 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2)) => ((member_real @ X3 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X0 @ X1)))) => (member_real @ (minus_minus_real @ (plus_plus_real @ X0 @ X3) @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2))))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_168_general_Oexistence__ivl__trans)).
% 15.68/2.69 thf(f205,axiom,(
% 15.68/2.69 ! [X0 : real,X1 : real] : (((minus_minus_real @ (plus_plus_real @ X0 @ X1) @ X0)) = X1)),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_204_add__diff__cancel__left_H)).
% 15.68/2.69 thf(f209,axiom,(
% 15.68/2.69 ! [X1 : real,X0 : real] : (((plus_plus_real @ (minus_minus_real @ X0 @ X1) @ X1)) = X0)),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_208_diff__add__cancel)).
% 15.68/2.69 thf(f240,axiom,(
% 15.68/2.69 ! [X0 : real,X1 : real] : (((plus_plus_real @ (uminus_uminus_real @ X0) @ X1)) = ((minus_minus_real @ X1 @ X0)))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_239_uminus__add__conv__diff)).
% 15.68/2.69 thf(f328,axiom,(
% 15.68/2.69 ! [X0 : real,X1 : real,X2 : real] : (((minus_minus_real @ (minus_minus_real @ X0 @ X1) @ X2)) = ((minus_minus_real @ X0 @ (plus_plus_real @ X1 @ X2))))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_327_diff__diff__add)).
% 15.68/2.69 thf(f334,axiom,(
% 15.68/2.69 ! [X2 : real,X1 : real,X0 : real] : (((minus_minus_real @ X0 @ (minus_minus_real @ X1 @ X2))) = ((minus_minus_real @ (plus_plus_real @ X0 @ X2) @ X1)))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_333_diff__diff__eq2)).
% 15.68/2.69 thf(f343,conjecture,(
% 15.68/2.69 (xx = ((auto_ll_on_flow0_a @ f @ x @ x2 @ (minus_minus_real @ ss @ tt))))),
% 15.68/2.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 15.68/2.69 thf(f344,negated_conjecture,(
% 15.68/2.69 ~ (xx = ((auto_ll_on_flow0_a @ f @ x @ x2 @ (minus_minus_real @ ss @ tt))))),
% 15.68/2.69 inference(negated_conjecture,[status(cth)],[f343])).
% 15.68/2.69 thf(f408,plain,(
% 15.68/2.69 ! [X0 : real] : (((uminus_uminus_real @ X0)) = ((minus_minus_real @ zero_zero_real @ X0)))),
% 15.68/2.69 inference(fool_elimination,[],[f32])).
% 15.68/2.69 thf(f421,plain,(
% 15.68/2.69 ~ (xx = ((auto_ll_on_flow0_a @ f @ x @ x2 @ (minus_minus_real @ ss @ tt))))),
% 15.68/2.69 inference(fool_elimination,[],[f344])).
% 15.68/2.69 thf(f437,plain,(
% 15.68/2.69 ! [X0 : real,X1 : a] : ((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X1)) => (member_real @ (minus_minus_real @ zero_zero_real @ X0) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ X0))))),
% 15.68/2.69 inference(rectify,[],[f35])).
% 15.68/2.69 thf(f438,plain,(
% 15.68/2.69 ! [X1 : a,X0 : real] : ((((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X1))) = $true) => (((member_real @ (minus_minus_real @ zero_zero_real @ X0) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ X0)))) = $true))),
% 15.68/2.69 inference(fool_elimination,[],[f437])).
% 15.68/2.69 thf(f467,plain,(
% 15.68/2.69 (member_real @ tt @ (auto_l612940ivl0_a @ f @ x @ xx))),
% 15.68/2.69 inference(rectify,[],[f5])).
% 15.68/2.69 thf(f468,plain,(
% 15.68/2.69 (((member_real @ tt @ (auto_l612940ivl0_a @ f @ x @ xx))) = $true)),
% 15.68/2.69 inference(fool_elimination,[],[f467])).
% 15.68/2.69 thf(f500,plain,(
% 15.68/2.69 ! [X0 : real,X1 : real] : (((minus_minus_real @ X1 @ X0)) = ((plus_plus_real @ (uminus_uminus_real @ X0) @ X1)))),
% 15.68/2.69 inference(fool_elimination,[],[f240])).
% 15.68/2.69 thf(f549,plain,(
% 15.68/2.69 ! [X0 : real,X1 : real] : (((minus_minus_real @ (plus_plus_real @ X0 @ X1) @ X0)) = X1)),
% 15.68/2.69 inference(fool_elimination,[],[f205])).
% 15.68/2.69 thf(f569,plain,(
% 15.68/2.69 ! [X0 : real,X1 : real,X2 : a,X3 : real] : ((member_real @ (minus_minus_real @ X3 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2)) => ((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X3 @ X1)))) => (member_real @ (minus_minus_real @ (plus_plus_real @ X3 @ X0) @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2))))),
% 15.68/2.69 inference(rectify,[],[f169])).
% 15.68/2.69 thf(f570,plain,(
% 15.68/2.69 ! [X3 : real,X1 : real,X0 : real,X2 : a] : ((((member_real @ (minus_minus_real @ X3 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2))) = $true) => ((((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X3 @ X1))))) = $true) => (((member_real @ (minus_minus_real @ (plus_plus_real @ X3 @ X0) @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2))) = $true)))),
% 15.68/2.69 inference(fool_elimination,[],[f569])).
% 15.68/2.69 thf(f571,plain,(
% 15.68/2.69 (((auto_ll_on_flow0_a @ f @ x @ xx @ tt)) = ((auto_ll_on_flow0_a @ f @ x @ x2 @ ss)))),
% 15.68/2.69 inference(fool_elimination,[],[f3])).
% 15.68/2.69 thf(f573,plain,(
% 15.68/2.69 ! [X0 : real,X1 : real,X2 : real] : (((minus_minus_real @ (plus_plus_real @ X2 @ X0) @ X1)) = ((minus_minus_real @ X2 @ (minus_minus_real @ X1 @ X0))))),
% 15.68/2.69 inference(rectify,[],[f334])).
% 15.68/2.69 thf(f574,plain,(
% 15.68/2.69 ! [X0 : real,X1 : real,X2 : real] : (((minus_minus_real @ (plus_plus_real @ X2 @ X0) @ X1)) = ((minus_minus_real @ X2 @ (minus_minus_real @ X1 @ X0))))),
% 15.68/2.69 inference(fool_elimination,[],[f573])).
% 15.68/2.69 thf(f707,plain,(
% 15.68/2.69 ! [X0 : real,X1 : a,X2 : real,X3 : real] : ((member_real @ (minus_minus_real @ X2 @ X0) @ (auto_l612940ivl0_a @ f @ x @ X1)) => ((member_real @ X3 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ X2 @ X0)))) => (((auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ (plus_plus_real @ X2 @ X3) @ X0))) = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ X2 @ X0)) @ X3)))))),
% 15.68/2.69 inference(rectify,[],[f167])).
% 15.68/2.69 thf(f708,plain,(
% 15.68/2.69 ! [X0 : real,X2 : real,X3 : real,X1 : a] : ((((member_real @ (minus_minus_real @ X2 @ X0) @ (auto_l612940ivl0_a @ f @ x @ X1))) = $true) => ((((member_real @ X3 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ X2 @ X0))))) = $true) => (((auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ (plus_plus_real @ X2 @ X3) @ X0))) = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ X2 @ X0)) @ X3)))))),
% 15.68/2.69 inference(fool_elimination,[],[f707])).
% 15.68/2.69 thf(f777,plain,(
% 15.68/2.69 ! [X0 : real,X1 : real,X2 : a] : ((member_real @ (minus_minus_real @ X1 @ X0) @ (auto_l612940ivl0_a @ f @ x @ X2)) => (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X1 @ X0)) @ (minus_minus_real @ X0 @ X1))) = X2))),
% 15.68/2.69 inference(rectify,[],[f12])).
% 15.68/2.69 thf(f778,plain,(
% 15.68/2.69 ! [X2 : a,X1 : real,X0 : real] : ((((member_real @ (minus_minus_real @ X1 @ X0) @ (auto_l612940ivl0_a @ f @ x @ X2))) = $true) => (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X1 @ X0)) @ (minus_minus_real @ X0 @ X1))) = X2))),
% 15.68/2.69 inference(fool_elimination,[],[f777])).
% 15.68/2.69 thf(f824,plain,(
% 15.68/2.69 (member_real @ ss @ (auto_l612940ivl0_a @ f @ x @ x2))),
% 15.68/2.69 inference(rectify,[],[f6])).
% 15.68/2.69 thf(f825,plain,(
% 15.68/2.69 (((member_real @ ss @ (auto_l612940ivl0_a @ f @ x @ x2))) = $true)),
% 15.68/2.69 inference(fool_elimination,[],[f824])).
% 15.68/2.69 thf(f847,plain,(
% 15.68/2.69 ! [X1 : real,X2 : real,X0 : real] : (((minus_minus_real @ (minus_minus_real @ X0 @ X1) @ X2)) = ((minus_minus_real @ X0 @ (plus_plus_real @ X1 @ X2))))),
% 15.68/2.69 inference(fool_elimination,[],[f328])).
% 15.68/2.69 thf(f888,plain,(
% 15.68/2.69 ! [X0 : real,X1 : real] : (((plus_plus_real @ (minus_minus_real @ X1 @ X0) @ X0)) = X1)),
% 15.68/2.69 inference(rectify,[],[f209])).
% 15.68/2.69 thf(f889,plain,(
% 15.68/2.69 ! [X1 : real,X0 : real] : (((plus_plus_real @ (minus_minus_real @ X1 @ X0) @ X0)) = X1)),
% 15.68/2.69 inference(fool_elimination,[],[f888])).
% 15.68/2.69 thf(f923,plain,(
% 15.68/2.69 ! [X0 : a,X1 : real] : ((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ X0)) => (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ X1) @ (minus_minus_real @ zero_zero_real @ X1))) = X0))),
% 15.68/2.69 inference(rectify,[],[f34])).
% 15.68/2.69 thf(f924,plain,(
% 15.68/2.69 ! [X1 : real,X0 : a] : ((((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ X0))) = $true) => (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ X1) @ (minus_minus_real @ zero_zero_real @ X1))) = X0))),
% 15.68/2.69 inference(fool_elimination,[],[f923])).
% 15.68/2.69 thf(f932,plain,(
% 15.68/2.69 (xx != ((auto_ll_on_flow0_a @ f @ x @ x2 @ (minus_minus_real @ ss @ tt))))),
% 15.68/2.69 inference(flattening,[],[f421])).
% 15.68/2.69 thf(f940,plain,(
% 15.68/2.69 ! [X2 : a,X0 : real,X1 : real] : ((((member_real @ (minus_minus_real @ X1 @ X0) @ (auto_l612940ivl0_a @ f @ x @ X2))) != $true) | (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X1 @ X0)) @ (minus_minus_real @ X0 @ X1))) = X2))),
% 15.68/2.69 inference(ennf_transformation,[],[f778])).
% 15.68/2.69 thf(f970,plain,(
% 15.68/2.69 ! [X1 : a,X0 : real] : ((((member_real @ (minus_minus_real @ zero_zero_real @ X0) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ X0)))) = $true) | (((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X1))) != $true))),
% 15.68/2.69 inference(ennf_transformation,[],[f438])).
% 15.68/2.69 thf(f998,plain,(
% 15.68/2.69 ! [X0 : a,X1 : real] : ((((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true) | (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ X1) @ (minus_minus_real @ zero_zero_real @ X1))) = X0))),
% 15.68/2.69 inference(ennf_transformation,[],[f924])).
% 15.68/2.69 thf(f1009,plain,(
% 15.68/2.69 ! [X3 : real,X1 : real,X0 : real,X2 : a] : (((((member_real @ (minus_minus_real @ (plus_plus_real @ X3 @ X0) @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2))) = $true) | (((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X3 @ X1))))) != $true)) | (((member_real @ (minus_minus_real @ X3 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2))) != $true))),
% 15.68/2.69 inference(ennf_transformation,[],[f570])).
% 15.68/2.69 thf(f1010,plain,(
% 15.68/2.69 ! [X2 : a,X0 : real,X3 : real,X1 : real] : ((((member_real @ (minus_minus_real @ (plus_plus_real @ X3 @ X0) @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2))) = $true) | (((member_real @ (minus_minus_real @ X3 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X2))) != $true) | (((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X3 @ X1))))) != $true))),
% 15.68/2.69 inference(flattening,[],[f1009])).
% 15.68/2.69 thf(f1018,plain,(
% 15.68/2.69 ! [X0 : real,X2 : real,X3 : real,X1 : a] : (((((auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ (plus_plus_real @ X2 @ X3) @ X0))) = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ X2 @ X0)) @ X3))) | (((member_real @ X3 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ X2 @ X0))))) != $true)) | (((member_real @ (minus_minus_real @ X2 @ X0) @ (auto_l612940ivl0_a @ f @ x @ X1))) != $true))),
% 15.68/2.69 inference(ennf_transformation,[],[f708])).
% 15.68/2.69 thf(f1019,plain,(
% 15.68/2.69 ! [X1 : a,X0 : real,X2 : real,X3 : real] : ((((auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ (plus_plus_real @ X2 @ X3) @ X0))) = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ X2 @ X0)) @ X3))) | (((member_real @ (minus_minus_real @ X2 @ X0) @ (auto_l612940ivl0_a @ f @ x @ X1))) != $true) | (((member_real @ X3 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X1 @ (minus_minus_real @ X2 @ X0))))) != $true))),
% 15.68/2.69 inference(flattening,[],[f1018])).
% 15.68/2.69 thf(f1048,plain,(
% 15.68/2.69 ! [X0 : a,X1 : real] : ((((member_real @ (minus_minus_real @ zero_zero_real @ X1) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ X1)))) = $true) | (((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true))),
% 15.68/2.69 inference(rectify,[],[f970])).
% 15.68/2.69 thf(f1059,plain,(
% 15.68/2.69 ! [X0 : a,X1 : real,X2 : real,X3 : real] : ((((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ X1)) @ X3)) = ((auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ (plus_plus_real @ X2 @ X3) @ X1)))) | (((member_real @ (minus_minus_real @ X2 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true) | (((member_real @ X3 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ X1))))) != $true))),
% 15.68/2.69 inference(rectify,[],[f1019])).
% 15.68/2.69 thf(f1060,plain,(
% 15.68/2.69 ! [X0 : real,X1 : real,X2 : real] : (((minus_minus_real @ (minus_minus_real @ X2 @ X0) @ X1)) = ((minus_minus_real @ X2 @ (plus_plus_real @ X0 @ X1))))),
% 15.68/2.69 inference(rectify,[],[f847])).
% 15.68/2.69 thf(f1099,plain,(
% 15.68/2.69 ! [X0 : a,X1 : real,X2 : real,X3 : real] : (($true = ((member_real @ (minus_minus_real @ (plus_plus_real @ X2 @ X1) @ X3) @ (auto_l612940ivl0_a @ f @ x @ X0)))) | (((member_real @ (minus_minus_real @ X2 @ X3) @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true) | (((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ X3))))) != $true))),
% 15.68/2.69 inference(rectify,[],[f1010])).
% 15.68/2.69 thf(f1106,plain,(
% 15.68/2.69 ! [X0 : real,X1 : real] : (((plus_plus_real @ (minus_minus_real @ X0 @ X1) @ X1)) = X0)),
% 15.68/2.69 inference(rectify,[],[f889])).
% 15.68/2.69 thf(f1134,plain,(
% 15.68/2.69 ! [X0 : a,X1 : real,X2 : real] : ((((member_real @ (minus_minus_real @ X2 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true) | (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ X1)) @ (minus_minus_real @ X1 @ X2))) = X0))),
% 15.68/2.69 inference(rectify,[],[f940])).
% 15.68/2.69 thf(f1173,plain,(
% 15.68/2.69 (((member_real @ ss @ (auto_l612940ivl0_a @ f @ x @ x2))) = $true)),
% 15.68/2.69 inference(cnf_transformation,[],[f825])).
% 15.68/2.69 thf(f1175,plain,(
% 15.68/2.69 ( ! [X0 : real,X1 : real] : ((((minus_minus_real @ X1 @ X0)) = ((plus_plus_real @ (uminus_uminus_real @ X0) @ X1)))) )),
% 15.68/2.69 inference(cnf_transformation,[],[f500])).
% 15.68/2.69 thf(f1176,plain,(
% 15.68/2.69 ( ! [X0 : a,X1 : real] : ((((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true) | (((member_real @ (minus_minus_real @ zero_zero_real @ X1) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ X1)))) = $true)) )),
% 15.68/2.69 inference(cnf_transformation,[],[f1048])).
% 15.68/2.69 thf(f1197,plain,(
% 15.68/2.69 ( ! [X2 : real,X3 : real,X0 : a,X1 : real] : ((((member_real @ (minus_minus_real @ X2 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true) | (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ X1)) @ X3)) = ((auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ (plus_plus_real @ X2 @ X3) @ X1)))) | (((member_real @ X3 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ X1))))) != $true)) )),
% 15.68/2.69 inference(cnf_transformation,[],[f1059])).
% 15.68/2.69 thf(f1198,plain,(
% 15.68/2.69 ( ! [X2 : real,X0 : real,X1 : real] : ((((minus_minus_real @ (minus_minus_real @ X2 @ X0) @ X1)) = ((minus_minus_real @ X2 @ (plus_plus_real @ X0 @ X1))))) )),
% 15.68/2.69 inference(cnf_transformation,[],[f1060])).
% 15.68/2.69 thf(f1199,plain,(
% 15.68/2.69 ( ! [X0 : real] : ((((uminus_uminus_real @ X0)) = ((minus_minus_real @ zero_zero_real @ X0)))) )),
% 15.68/2.69 inference(cnf_transformation,[],[f408])).
% 15.68/2.69 thf(f1220,plain,(
% 15.68/2.69 (((auto_ll_on_flow0_a @ f @ x @ xx @ tt)) = ((auto_ll_on_flow0_a @ f @ x @ x2 @ ss)))),
% 15.68/2.69 inference(cnf_transformation,[],[f571])).
% 15.68/2.69 thf(f1242,plain,(
% 15.68/2.69 (xx != ((auto_ll_on_flow0_a @ f @ x @ x2 @ (minus_minus_real @ ss @ tt))))),
% 15.68/2.69 inference(cnf_transformation,[],[f932])).
% 15.68/2.69 thf(f1266,plain,(
% 15.68/2.69 ( ! [X2 : real,X3 : real,X0 : a,X1 : real] : (($true = ((member_real @ (minus_minus_real @ (plus_plus_real @ X2 @ X1) @ X3) @ (auto_l612940ivl0_a @ f @ x @ X0)))) | (((member_real @ (minus_minus_real @ X2 @ X3) @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true) | (((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ X3))))) != $true)) )),
% 15.68/2.69 inference(cnf_transformation,[],[f1099])).
% 15.68/2.69 thf(f1280,plain,(
% 15.68/2.69 ( ! [X0 : a,X1 : real] : ((((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true) | (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ X1) @ (minus_minus_real @ zero_zero_real @ X1))) = X0)) )),
% 15.68/2.69 inference(cnf_transformation,[],[f998])).
% 15.68/2.69 thf(f1283,plain,(
% 15.68/2.69 ( ! [X0 : real,X1 : real] : ((((plus_plus_real @ (minus_minus_real @ X0 @ X1) @ X1)) = X0)) )),
% 15.68/2.69 inference(cnf_transformation,[],[f1106])).
% 15.68/2.69 thf(f1286,plain,(
% 15.68/2.69 ( ! [X0 : real,X1 : real] : ((((minus_minus_real @ (plus_plus_real @ X0 @ X1) @ X0)) = X1)) )),
% 15.68/2.69 inference(cnf_transformation,[],[f549])).
% 15.68/2.69 thf(f1288,plain,(
% 15.68/2.69 ( ! [X2 : real,X0 : real,X1 : real] : ((((minus_minus_real @ (plus_plus_real @ X2 @ X0) @ X1)) = ((minus_minus_real @ X2 @ (minus_minus_real @ X1 @ X0))))) )),
% 15.68/2.69 inference(cnf_transformation,[],[f574])).
% 15.68/2.69 thf(f1325,plain,(
% 15.68/2.69 ( ! [X2 : real,X0 : a,X1 : real] : ((((member_real @ (minus_minus_real @ X2 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true) | (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ X1)) @ (minus_minus_real @ X1 @ X2))) = X0)) )),
% 15.68/2.69 inference(cnf_transformation,[],[f1134])).
% 15.68/2.69 thf(f1348,plain,(
% 15.68/2.69 (((member_real @ tt @ (auto_l612940ivl0_a @ f @ x @ xx))) = $true)),
% 15.68/2.69 inference(cnf_transformation,[],[f468])).
% 15.68/2.69 thf(f1439,definition,(
% 15.68/2.69 spl0_2 <=> (((member_real @ ss @ (auto_l612940ivl0_a @ f @ x @ x2))) = $true)),
% 15.68/2.69 introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition])).
% 15.68/2.69 thf(f1441,plain,(
% 15.68/2.69 (((member_real @ ss @ (auto_l612940ivl0_a @ f @ x @ x2))) = $true) | ~spl0_2),
% 15.68/2.69 inference(avatar_component_clause,[],[f1439])).
% 15.68/2.69 thf(f1442,plain,(
% 15.68/2.69 spl0_2),
% 15.68/2.69 inference(avatar_split_clause,[],[f1173,f1439])).
% 15.68/2.69 thf(f1444,definition,(
% 15.68/2.69 spl0_3 <=> (((auto_ll_on_flow0_a @ f @ x @ xx @ tt)) = ((auto_ll_on_flow0_a @ f @ x @ x2 @ ss)))),
% 15.68/2.69 introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition])).
% 15.68/2.69 thf(f1446,plain,(
% 15.68/2.69 (((auto_ll_on_flow0_a @ f @ x @ xx @ tt)) = ((auto_ll_on_flow0_a @ f @ x @ x2 @ ss))) | ~spl0_3),
% 15.68/2.69 inference(avatar_component_clause,[],[f1444])).
% 15.68/2.69 thf(f1447,plain,(
% 15.68/2.69 spl0_3),
% 15.68/2.69 inference(avatar_split_clause,[],[f1220,f1444])).
% 15.68/2.69 thf(f1469,definition,(
% 15.68/2.69 spl0_8 <=> (xx = ((auto_ll_on_flow0_a @ f @ x @ x2 @ (minus_minus_real @ ss @ tt))))),
% 15.68/2.70 introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition])).
% 15.68/2.70 thf(f1472,plain,(
% 15.68/2.70 ~spl0_8),
% 15.68/2.70 inference(avatar_split_clause,[],[f1242,f1469])).
% 15.68/2.70 thf(f1484,definition,(
% 15.68/2.70 spl0_11 <=> (((member_real @ tt @ (auto_l612940ivl0_a @ f @ x @ xx))) = $true)),
% 15.68/2.70 introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition])).
% 15.68/2.70 thf(f1486,plain,(
% 15.68/2.70 (((member_real @ tt @ (auto_l612940ivl0_a @ f @ x @ xx))) = $true) | ~spl0_11),
% 15.68/2.70 inference(avatar_component_clause,[],[f1484])).
% 15.68/2.70 thf(f1487,plain,(
% 15.68/2.70 spl0_11),
% 15.68/2.70 inference(avatar_split_clause,[],[f1348,f1484])).
% 15.68/2.70 thf(f1507,plain,(
% 15.68/2.70 ( ! [X0 : real,X1 : real] : ((((minus_minus_real @ X0 @ (minus_minus_real @ X0 @ X1))) = X1)) )),
% 15.68/2.70 inference(superposition,[],[f1286,f1283])).
% 15.68/2.70 thf(f1725,plain,(
% 15.68/2.70 (((member_real @ (minus_minus_real @ zero_zero_real @ ss) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ x2 @ ss)))) = $true) | ($true != $true) | ~spl0_2),
% 15.68/2.70 inference(superposition,[],[f1176,f1441])).
% 15.68/2.70 thf(f1728,plain,(
% 15.68/2.70 (((member_real @ (minus_minus_real @ zero_zero_real @ ss) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ x2 @ ss)))) = $true) | ~spl0_2),
% 15.68/2.70 inference(trivial_inequality_removal,[],[f1725])).
% 15.68/2.70 thf(f1731,plain,(
% 15.68/2.70 (((member_real @ (minus_minus_real @ zero_zero_real @ ss) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt)))) = $true) | (~spl0_2 | ~spl0_3)),
% 15.68/2.70 inference(forward_demodulation,[],[f1728,f1446])).
% 15.68/2.70 thf(f1743,definition,(
% 15.68/2.70 spl0_17 <=> (((member_real @ (minus_minus_real @ zero_zero_real @ ss) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt)))) = $true)),
% 15.68/2.70 introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition])).
% 15.68/2.70 thf(f1745,plain,(
% 15.68/2.70 (((member_real @ (minus_minus_real @ zero_zero_real @ ss) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt)))) = $true) | ~spl0_17),
% 15.68/2.70 inference(avatar_component_clause,[],[f1743])).
% 15.68/2.70 thf(f1746,plain,(
% 15.68/2.70 spl0_17 | ~spl0_2 | ~spl0_3),
% 15.68/2.70 inference(avatar_split_clause,[],[f1731,f1444,f1439,f1743])).
% 15.68/2.70 thf(f1747,plain,(
% 15.68/2.70 ($true != $true) | (x2 = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ x2 @ ss) @ (minus_minus_real @ zero_zero_real @ ss)))) | ~spl0_2),
% 15.68/2.70 inference(superposition,[],[f1280,f1441])).
% 15.68/2.70 thf(f1752,plain,(
% 15.68/2.70 (x2 = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ x2 @ ss) @ (minus_minus_real @ zero_zero_real @ ss)))) | ~spl0_2),
% 15.68/2.70 inference(trivial_inequality_removal,[],[f1747])).
% 15.68/2.70 thf(f1763,plain,(
% 15.68/2.70 (x2 = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt) @ (minus_minus_real @ zero_zero_real @ ss)))) | (~spl0_2 | ~spl0_3)),
% 15.68/2.70 inference(forward_demodulation,[],[f1752,f1446])).
% 15.68/2.70 thf(f1765,definition,(
% 15.68/2.70 spl0_20 <=> (x2 = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt) @ (minus_minus_real @ zero_zero_real @ ss))))),
% 15.68/2.70 introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition])).
% 15.68/2.70 thf(f1767,plain,(
% 15.68/2.70 (x2 = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt) @ (minus_minus_real @ zero_zero_real @ ss)))) | ~spl0_20),
% 15.68/2.70 inference(avatar_component_clause,[],[f1765])).
% 15.68/2.70 thf(f1768,plain,(
% 15.68/2.70 spl0_20 | ~spl0_2 | ~spl0_3),
% 15.68/2.70 inference(avatar_split_clause,[],[f1763,f1444,f1439,f1765])).
% 15.68/2.70 thf(f1814,plain,(
% 15.68/2.70 ( ! [X2 : real,X3 : real,X0 : a,X1 : real] : ((((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ X3))))) != $true) | (((member_real @ (minus_minus_real @ X2 @ (minus_minus_real @ X3 @ X1)) @ (auto_l612940ivl0_a @ f @ x @ X0))) = $true) | (((member_real @ (minus_minus_real @ X2 @ X3) @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true)) )),
% 15.68/2.70 inference(forward_demodulation,[],[f1266,f1288])).
% 15.68/2.70 thf(f1820,plain,(
% 15.68/2.70 ( ! [X2 : a,X3 : real,X0 : real,X1 : real] : ((((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0)))) != $true) | (((member_real @ (minus_minus_real @ (plus_plus_real @ X3 @ X0) @ (minus_minus_real @ X3 @ X1)) @ (auto_l612940ivl0_a @ f @ x @ X2))) = $true) | (((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X2))) != $true)) )),
% 15.68/2.70 inference(superposition,[],[f1814,f1286])).
% 15.68/2.70 thf(f1828,plain,(
% 15.68/2.70 ( ! [X2 : a,X3 : real,X0 : real,X1 : real] : ((((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X2))) != $true) | (((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0)))) != $true) | (((member_real @ (minus_minus_real @ X3 @ (minus_minus_real @ (minus_minus_real @ X3 @ X1) @ X0)) @ (auto_l612940ivl0_a @ f @ x @ X2))) = $true)) )),
% 15.68/2.70 inference(forward_demodulation,[],[f1820,f1288])).
% 15.68/2.70 thf(f1834,plain,(
% 15.68/2.70 ( ! [X2 : a,X3 : real,X0 : real,X1 : real] : ((((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0)))) != $true) | (((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X2))) != $true) | (((member_real @ (minus_minus_real @ X3 @ (minus_minus_real @ X3 @ (plus_plus_real @ X1 @ X0))) @ (auto_l612940ivl0_a @ f @ x @ X2))) = $true)) )),
% 15.68/2.70 inference(forward_demodulation,[],[f1828,f1198])).
% 15.68/2.70 thf(f1894,plain,(
% 15.68/2.70 ( ! [X2 : real,X3 : real,X0 : a,X1 : real] : ((((member_real @ X3 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ X1))))) != $true) | (((member_real @ (minus_minus_real @ X2 @ X1) @ (auto_l612940ivl0_a @ f @ x @ X0))) != $true) | (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ X1)) @ X3)) = ((auto_ll_on_flow0_a @ f @ x @ X0 @ (minus_minus_real @ X2 @ (minus_minus_real @ X1 @ X3)))))) )),
% 15.68/2.70 inference(forward_demodulation,[],[f1197,f1288])).
% 15.68/2.70 thf(f1899,plain,(
% 15.68/2.70 ( ! [X2 : a,X3 : real,X0 : real,X1 : real] : ((((auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ (plus_plus_real @ X3 @ X0) @ (minus_minus_real @ X3 @ X1)))) = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0) @ X1))) | (((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0)))) != $true) | (((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X2))) != $true)) )),
% 15.68/2.70 inference(superposition,[],[f1894,f1286])).
% 15.68/2.70 thf(f1903,plain,(
% 15.68/2.70 ( ! [X2 : a,X3 : real,X0 : real,X1 : real] : ((((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0)))) != $true) | (((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X2))) != $true) | (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0) @ X1)) = ((auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X3 @ (minus_minus_real @ (minus_minus_real @ X3 @ X1) @ X0)))))) )),
% 15.68/2.70 inference(forward_demodulation,[],[f1899,f1288])).
% 15.68/2.70 thf(f1909,plain,(
% 15.68/2.70 ( ! [X2 : a,X3 : real,X0 : real,X1 : real] : ((((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X2))) != $true) | (((auto_ll_on_flow0_a @ f @ x @ X2 @ (minus_minus_real @ X3 @ (minus_minus_real @ X3 @ (plus_plus_real @ X1 @ X0))))) = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0) @ X1))) | (((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0)))) != $true)) )),
% 15.68/2.70 inference(forward_demodulation,[],[f1903,f1198])).
% 15.68/2.70 thf(f9581,plain,(
% 15.68/2.70 (((member_real @ (uminus_uminus_real @ ss) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt)))) = $true) | ~spl0_17),
% 15.68/2.70 inference(forward_demodulation,[],[f1745,f1199])).
% 15.68/2.70 thf(f9583,definition,(
% 15.68/2.70 spl0_35 <=> (((member_real @ (uminus_uminus_real @ ss) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt)))) = $true)),
% 15.68/2.70 introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition])).
% 15.68/2.70 thf(f9585,plain,(
% 15.68/2.70 (((member_real @ (uminus_uminus_real @ ss) @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt)))) = $true) | ~spl0_35),
% 15.68/2.70 inference(avatar_component_clause,[],[f9583])).
% 15.68/2.70 thf(f9586,plain,(
% 15.68/2.70 spl0_35 | ~spl0_17),
% 15.68/2.70 inference(avatar_split_clause,[],[f9581,f1743,f9583])).
% 15.68/2.70 thf(f9643,plain,(
% 15.68/2.70 (x2 = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt) @ (uminus_uminus_real @ ss)))) | ~spl0_20),
% 15.68/2.70 inference(forward_demodulation,[],[f1767,f1199])).
% 15.68/2.70 thf(f9645,definition,(
% 15.68/2.70 spl0_41 <=> (x2 = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt) @ (uminus_uminus_real @ ss))))),
% 15.68/2.70 introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition])).
% 15.68/2.70 thf(f9647,plain,(
% 15.68/2.70 (x2 = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt) @ (uminus_uminus_real @ ss)))) | ~spl0_41),
% 15.68/2.70 inference(avatar_component_clause,[],[f9645])).
% 15.68/2.70 thf(f9648,plain,(
% 15.68/2.70 spl0_41 | ~spl0_20),
% 15.68/2.70 inference(avatar_split_clause,[],[f9643,f1765,f9645])).
% 15.68/2.70 thf(f11042,plain,(
% 15.68/2.70 ( ! [X2 : a,X0 : real,X1 : real] : ((((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0)))) != $true) | (((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X2))) != $true) | (((member_real @ (plus_plus_real @ X1 @ X0) @ (auto_l612940ivl0_a @ f @ x @ X2))) = $true)) )),
% 15.68/2.70 inference(forward_demodulation,[],[f1834,f1507])).
% 15.68/2.70 thf(f11048,plain,(
% 15.68/2.70 (((member_real @ tt @ (auto_l612940ivl0_a @ f @ x @ xx))) != $true) | ($true = ((member_real @ (plus_plus_real @ (uminus_uminus_real @ ss) @ tt) @ (auto_l612940ivl0_a @ f @ x @ xx)))) | ($true != $true) | ~spl0_35),
% 15.68/2.70 inference(superposition,[],[f11042,f9585])).
% 15.68/2.70 thf(f11049,plain,(
% 15.68/2.70 ($true = ((member_real @ (plus_plus_real @ (uminus_uminus_real @ ss) @ tt) @ (auto_l612940ivl0_a @ f @ x @ xx)))) | (((member_real @ tt @ (auto_l612940ivl0_a @ f @ x @ xx))) != $true) | ~spl0_35),
% 15.68/2.70 inference(trivial_inequality_removal,[],[f11048])).
% 15.68/2.70 thf(f11052,plain,(
% 15.68/2.70 ($true = ((member_real @ (plus_plus_real @ (uminus_uminus_real @ ss) @ tt) @ (auto_l612940ivl0_a @ f @ x @ xx)))) | (~spl0_11 | ~spl0_35)),
% 15.68/2.70 inference(forward_subsumption_resolution,[],[f11049,f1486])).
% 15.68/2.70 thf(f11057,plain,(
% 15.68/2.70 (((member_real @ (minus_minus_real @ tt @ ss) @ (auto_l612940ivl0_a @ f @ x @ xx))) = $true) | (~spl0_11 | ~spl0_35)),
% 15.68/2.70 inference(forward_demodulation,[],[f11052,f1175])).
% 15.68/2.70 thf(f11060,definition,(
% 15.68/2.70 spl0_53 <=> (((member_real @ (minus_minus_real @ tt @ ss) @ (auto_l612940ivl0_a @ f @ x @ xx))) = $true)),
% 15.68/2.70 introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition])).
% 15.68/2.70 thf(f11062,plain,(
% 15.68/2.70 (((member_real @ (minus_minus_real @ tt @ ss) @ (auto_l612940ivl0_a @ f @ x @ xx))) = $true) | ~spl0_53),
% 15.68/2.70 inference(avatar_component_clause,[],[f11060])).
% 15.68/2.70 thf(f11063,plain,(
% 15.68/2.70 spl0_53 | ~spl0_11 | ~spl0_35),
% 15.68/2.70 inference(avatar_split_clause,[],[f11057,f9583,f1484,f11060])).
% 15.68/2.70 thf(f13059,plain,(
% 15.68/2.70 ( ! [X2 : a,X0 : real,X1 : real] : ((((member_real @ X1 @ (auto_l612940ivl0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0)))) != $true) | (((member_real @ X0 @ (auto_l612940ivl0_a @ f @ x @ X2))) != $true) | (((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ X2 @ X0) @ X1)) = ((auto_ll_on_flow0_a @ f @ x @ X2 @ (plus_plus_real @ X1 @ X0))))) )),
% 15.68/2.70 inference(forward_demodulation,[],[f1909,f1507])).
% 15.68/2.70 thf(f13065,plain,(
% 15.68/2.70 ($true != $true) | (((auto_ll_on_flow0_a @ f @ x @ xx @ (plus_plus_real @ (uminus_uminus_real @ ss) @ tt))) = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt) @ (uminus_uminus_real @ ss)))) | (((member_real @ tt @ (auto_l612940ivl0_a @ f @ x @ xx))) != $true) | ~spl0_35),
% 15.68/2.70 inference(superposition,[],[f13059,f9585])).
% 15.68/2.70 thf(f13067,plain,(
% 15.68/2.70 (((auto_ll_on_flow0_a @ f @ x @ xx @ (plus_plus_real @ (uminus_uminus_real @ ss) @ tt))) = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt) @ (uminus_uminus_real @ ss)))) | (((member_real @ tt @ (auto_l612940ivl0_a @ f @ x @ xx))) != $true) | ~spl0_35),
% 15.68/2.70 inference(trivial_inequality_removal,[],[f13065])).
% 15.68/2.70 thf(f13072,plain,(
% 15.68/2.70 (((auto_ll_on_flow0_a @ f @ x @ xx @ (plus_plus_real @ (uminus_uminus_real @ ss) @ tt))) = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt) @ (uminus_uminus_real @ ss)))) | (~spl0_11 | ~spl0_35)),
% 15.68/2.70 inference(forward_subsumption_resolution,[],[f13067,f1486])).
% 15.68/2.70 thf(f13074,plain,(
% 15.68/2.70 (x2 = ((auto_ll_on_flow0_a @ f @ x @ xx @ (plus_plus_real @ (uminus_uminus_real @ ss) @ tt)))) | (~spl0_11 | ~spl0_35 | ~spl0_41)),
% 15.68/2.70 inference(forward_demodulation,[],[f13072,f9647])).
% 15.68/2.70 thf(f13076,plain,(
% 15.68/2.70 (x2 = ((auto_ll_on_flow0_a @ f @ x @ xx @ (minus_minus_real @ tt @ ss)))) | (~spl0_11 | ~spl0_35 | ~spl0_41)),
% 15.68/2.70 inference(forward_demodulation,[],[f13074,f1175])).
% 15.68/2.70 thf(f13078,definition,(
% 15.68/2.70 spl0_57 <=> (x2 = ((auto_ll_on_flow0_a @ f @ x @ xx @ (minus_minus_real @ tt @ ss))))),
% 15.68/2.70 introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition])).
% 15.68/2.70 thf(f13081,plain,(
% 15.68/2.70 spl0_57 | ~spl0_11 | ~spl0_35 | ~spl0_41),
% 15.68/2.70 inference(avatar_split_clause,[],[f13076,f9645,f9583,f1484,f13078])).
% 15.68/2.70 thf(f24940,plain,(
% 15.68/2.70 ($true != $true) | (xx = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ (minus_minus_real @ tt @ ss)) @ (minus_minus_real @ ss @ tt)))) | ~spl0_53),
% 15.68/2.70 inference(superposition,[],[f1325,f11062])).
% 15.68/2.70 thf(f24950,plain,(
% 15.68/2.70 (xx = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ (minus_minus_real @ tt @ ss)) @ (minus_minus_real @ ss @ tt)))) | ~spl0_53),
% 15.68/2.70 inference(trivial_inequality_removal,[],[f24940])).
% 15.68/2.70 thf(f24964,definition,(
% 15.68/2.70 spl0_64 <=> (xx = ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ (minus_minus_real @ tt @ ss)) @ (minus_minus_real @ ss @ tt))))),
% 15.68/2.70 introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition])).
% 15.68/2.70 thf(f24967,plain,(
% 15.68/2.70 spl0_64 | ~spl0_53),
% 15.68/2.70 inference(avatar_split_clause,[],[f24950,f11060,f24964])).
% 15.68/2.70 thf(f24999,definition,(
% 15.68/2.70 (x2 != ((auto_ll_on_flow0_a @ f @ x @ xx @ (minus_minus_real @ tt @ ss)))) | (x2 != ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ tt) @ (uminus_uminus_real @ ss)))) | (xx != ((auto_ll_on_flow0_a @ f @ x @ (auto_ll_on_flow0_a @ f @ x @ xx @ (minus_minus_real @ tt @ ss)) @ (minus_minus_real @ ss @ tt)))) | (xx = ((auto_ll_on_flow0_a @ f @ x @ x2 @ (minus_minus_real @ ss @ tt))))),
% 15.68/2.70 introduced(theory,[theory_tautology_sat_conflict])).
% 15.68/2.70 cnf(s2, plain, spl0_2, inference(sat_conversion,[],[f1442])).
% 15.68/2.70 cnf(s3, plain, spl0_3, inference(sat_conversion,[],[f1447])).
% 15.68/2.70 cnf(s9, plain, ~spl0_8, inference(sat_conversion,[],[f1472])).
% 15.68/2.70 cnf(s14, plain, spl0_11, inference(sat_conversion,[],[f1487])).
% 15.68/2.70 cnf(s22, plain, ~spl0_2 | ~spl0_3 | spl0_17, inference(sat_conversion,[],[f1746])).
% 15.68/2.70 cnf(s25, plain, ~spl0_2 | ~spl0_3 | spl0_20, inference(sat_conversion,[],[f1768])).
% 15.68/2.70 cnf(s38, plain, ~spl0_17 | spl0_35, inference(sat_conversion,[],[f9586])).
% 15.68/2.70 cnf(s45, plain, ~spl0_20 | spl0_41, inference(sat_conversion,[],[f9648])).
% 15.68/2.70 cnf(s59, plain, ~spl0_11 | ~spl0_35 | spl0_53, inference(sat_conversion,[],[f11063])).
% 15.68/2.70 cnf(s65, plain, ~spl0_11 | ~spl0_35 | ~spl0_41 | spl0_57, inference(sat_conversion,[],[f13081])).
% 15.68/2.70 cnf(s72, plain, ~spl0_53 | spl0_64, inference(sat_conversion,[],[f24967])).
% 15.68/2.70 cnf(s82, plain, spl0_8 | ~spl0_41 | ~spl0_57 | ~spl0_64, inference(sat_conversion,[],[f24999])).
% 15.68/2.70 cnf(s101, plain, spl0_20, inference(rat,[],[s25,s3,s2])).
% 15.68/2.70 cnf(s102, plain, spl0_17, inference(rat,[],[s22,s3,s2])).
% 15.68/2.70 cnf(s105, plain, spl0_41, inference(rat,[],[s45,s101])).
% 15.68/2.70 cnf(s106, plain, spl0_35, inference(rat,[],[s38,s102])).
% 15.68/2.70 cnf(s107, plain, spl0_57, inference(rat,[],[s65,s105,s14,s106])).
% 15.68/2.70 cnf(s109, plain, spl0_53, inference(rat,[],[s59,s14,s106])).
% 15.68/2.70 cnf(s115, plain, ~spl0_64, inference(rat,[],[s82,s105,s9,s107])).
% 15.68/2.70 cnf(s120, plain, $false, inference(rat,[],[s72,s115,s109])).
% 15.68/2.70 thf(f25000,plain,(
% 15.68/2.70 $false),
% 15.68/2.70 inference(avatar_sat_refutation,[],[s120])).
% 15.68/2.70 % SZS output end Proof for theBenchmark
% 15.68/2.70 % (840675)------------------------------
% 15.68/2.70 % (840675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.68/2.70 % (840675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/2.70 % (840675)CaDiCaL version: 2.1.3
% 15.68/2.70 % (840675)Termination reason: Refutation
% 15.68/2.70 % (840675)Time elapsed: 1.676 s
% 15.68/2.70 % (840675)Peak memory usage: 22 MB
% 15.68/2.70 % (840675)Instructions burned: 2643 (million)
% 15.68/2.70 % (840538)Success in time 2.409 s
% 15.68/2.70 % Vampire exiting
%------------------------------------------------------------------------------