%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV321^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:38:16 AM UTC 2026
% Result : Theorem 14.42s 2.30s
% Output : Refutation 14.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV321^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 % Computer : n026.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Tue Sep 29 15:39:28 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.24 Running higher-order theorem proving
% 0.07/0.25 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
% 1.00/0.45 % (741125)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.00/0.45 % (741135)lrs+10_16_si=on:nwc=1.5:random_seed=2879679500:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 1.00/0.45 % (741141)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.00/0.45 % (741141)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.00/0.45 % (741135)Instruction limit reached!
% 1.00/0.45 % (741135)------------------------------
% 1.00/0.45 % (741135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.45 % (741135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.45 % (741135)CaDiCaL version: 2.1.3
% 1.00/0.45 % (741135)Termination reason: Instruction limit
% 1.00/0.45 % (741135)Termination phase: Saturation
% 1.00/0.45 % (741135)Time elapsed: 0.010 s
% 1.00/0.45 % (741135)Peak memory usage: 12 MB
% 1.00/0.45 % (741135)Instructions burned: 19 (million)
% 1.00/0.45 % (741137)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1703518143:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 1.00/0.45 % (741134)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4100997108:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 1.00/0.45 % (741138)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=3307473340:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 1.00/0.45 % (741139)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3958419379:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 1.00/0.45 % (741141)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=1569809188:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 1.00/0.45 % (741140)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=923579705:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 1.00/0.45 % (741137)Instruction limit reached!
% 1.00/0.45 % (741137)------------------------------
% 1.00/0.45 % (741137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.45 % (741137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.45 % (741137)CaDiCaL version: 2.1.3
% 1.00/0.45 % (741137)Termination reason: Instruction limit
% 1.00/0.45 % (741137)Termination phase: Saturation
% 1.00/0.45 % (741137)Time elapsed: 0.010 s
% 1.00/0.45 % (741137)Peak memory usage: 12 MB
% 1.00/0.45 % (741137)Instructions burned: 4 (million)
% 1.00/0.45 % (741139)Instruction limit reached!
% 1.00/0.45 % (741139)------------------------------
% 1.00/0.45 % (741139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.45 % (741139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.45 % (741139)CaDiCaL version: 2.1.3
% 1.00/0.45 % (741139)Termination reason: Instruction limit
% 1.00/0.45 % (741139)Termination phase: Saturation
% 1.00/0.45 % (741139)Time elapsed: 0.018 s
% 1.00/0.45 % (741139)Peak memory usage: 12 MB
% 1.00/0.45 % (741139)Instructions burned: 26 (million)
% 1.00/0.45 % (741152)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1161548262:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.00/0.45 % (741172)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.00/0.45 % (741152)Instruction limit reached!
% 1.00/0.45 % (741152)------------------------------
% 1.00/0.45 % (741152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.45 % (741152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.45 % (741152)CaDiCaL version: 2.1.3
% 1.00/0.45 % (741152)Termination reason: Instruction limit
% 1.00/0.45 % (741152)Termination phase: Saturation
% 1.00/0.45 % (741152)Time elapsed: 0.003 s
% 1.00/0.45 % (741152)Peak memory usage: 12 MB
% 1.00/0.45 % (741152)Instructions burned: 2 (million)
% 1.00/0.45 % (741172)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3675581509:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.00/0.51 % (741167)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=4080402547:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.00/0.51 % (741172)Instruction limit reached!
% 1.00/0.51 % (741172)------------------------------
% 1.00/0.51 % (741172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.51 % (741172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.51 % (741172)CaDiCaL version: 2.1.3
% 1.00/0.51 % (741172)Termination reason: Instruction limit
% 1.00/0.51 % (741172)Termination phase: Saturation
% 1.00/0.51 % (741172)Time elapsed: 0.004 s
% 1.00/0.51 % (741172)Peak memory usage: 12 MB
% 1.00/0.51 % (741172)Instructions burned: 8 (million)
% 1.00/0.51 % (741167)Instruction limit reached!
% 1.00/0.51 % (741167)------------------------------
% 1.00/0.51 % (741167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.51 % (741167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.51 % (741167)CaDiCaL version: 2.1.3
% 1.00/0.51 % (741167)Termination reason: Instruction limit
% 1.00/0.51 % (741167)Termination phase: Saturation
% 1.00/0.51 % (741167)Time elapsed: 0.009 s
% 1.00/0.51 % (741167)Peak memory usage: 12 MB
% 1.00/0.51 % (741167)Instructions burned: 9 (million)
% 1.00/0.51 % (741186)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.00/0.51 % (741186)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.00/0.51 % (741181)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2115820945:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.00/0.51 % (741134)Instruction limit reached!
% 1.00/0.51 % (741134)------------------------------
% 1.00/0.51 % (741134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.51 % (741134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.51 % (741134)CaDiCaL version: 2.1.3
% 1.00/0.51 % (741134)Termination reason: Instruction limit
% 1.00/0.51 % (741134)Termination phase: Saturation
% 1.00/0.51 % (741134)Time elapsed: 0.071 s
% 1.00/0.51 % (741134)Peak memory usage: 12 MB
% 1.00/0.51 % (741134)Instructions burned: 88 (million)
% 1.00/0.51 % (741140)Instruction limit reached!
% 1.00/0.51 % (741140)------------------------------
% 1.00/0.51 % (741140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.51 % (741140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.51 % (741140)CaDiCaL version: 2.1.3
% 1.00/0.51 % (741140)Termination reason: Instruction limit
% 1.00/0.51 % (741140)Termination phase: Saturation
% 1.00/0.51 % (741140)Time elapsed: 0.066 s
% 1.00/0.51 % (741140)Peak memory usage: 12 MB
% 1.00/0.51 % (741140)Instructions burned: 75 (million)
% 1.00/0.51 % (741186)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=988325001:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.00/0.51 % (741181)Instruction limit reached!
% 1.00/0.51 % (741181)------------------------------
% 1.00/0.51 % (741181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.51 % (741181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.51 % (741181)CaDiCaL version: 2.1.3
% 1.00/0.51 % (741181)Termination reason: Instruction limit
% 1.00/0.51 % (741181)Termination phase: Saturation
% 1.00/0.51 % (741181)Time elapsed: 0.012 s
% 1.00/0.51 % (741181)Peak memory usage: 12 MB
% 1.00/0.51 % (741181)Instructions burned: 12 (million)
% 1.00/0.51 % (741192)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=1856412006:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.00/0.51 % (741186)Instruction limit reached!
% 1.00/0.51 % (741186)------------------------------
% 1.00/0.51 % (741186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.51 % (741186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.56 % (741186)CaDiCaL version: 2.1.3
% 1.83/0.56 % (741186)Termination reason: Instruction limit
% 1.83/0.56 % (741186)Termination phase: Saturation
% 1.83/0.56 % (741186)Time elapsed: 0.024 s
% 1.83/0.56 % (741186)Peak memory usage: 12 MB
% 1.83/0.56 % (741186)Instructions burned: 28 (million)
% 1.83/0.56 % (741202)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.83/0.56 % (741201)lrs+10_1_si=on:cs=on:random_seed=3412218108:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.83/0.56 % (741202)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=2857842400:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.83/0.56 % (741202)Instruction limit reached!
% 1.83/0.56 % (741202)------------------------------
% 1.83/0.56 % (741202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.56 % (741202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.56 % (741202)CaDiCaL version: 2.1.3
% 1.83/0.56 % (741202)Termination reason: Instruction limit
% 1.83/0.56 % (741202)Termination phase: Saturation
% 1.83/0.56 % (741202)Time elapsed: 0.003 s
% 1.83/0.56 % (741202)Peak memory usage: 11 MB
% 1.83/0.56 % (741202)Instructions burned: 2 (million)
% 1.83/0.56 % (741201)Instruction limit reached!
% 1.83/0.56 % (741201)------------------------------
% 1.83/0.56 % (741201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.56 % (741201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.56 % (741201)CaDiCaL version: 2.1.3
% 1.83/0.56 % (741201)Termination reason: Instruction limit
% 1.83/0.56 % (741201)Termination phase: Saturation
% 1.83/0.56 % (741201)Time elapsed: 0.009 s
% 1.83/0.56 % (741201)Peak memory usage: 12 MB
% 1.83/0.56 % (741201)Instructions burned: 8 (million)
% 1.83/0.56 % (741204)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2679108394:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.83/0.56 % (741213)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2868574794:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.83/0.56 % (741141)Instruction limit reached!
% 1.83/0.56 % (741141)------------------------------
% 1.83/0.56 % (741141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.56 % (741141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.56 % (741141)CaDiCaL version: 2.1.3
% 1.83/0.56 % (741141)Termination reason: Instruction limit
% 1.83/0.56 % (741141)Termination phase: Saturation
% 1.83/0.56 % (741141)Time elapsed: 0.139 s
% 1.83/0.56 % (741141)Peak memory usage: 12 MB
% 1.83/0.56 % (741141)Instructions burned: 157 (million)
% 1.83/0.56 % (741220)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1140290555:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.83/0.56 % (741221)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=428319636:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.83/0.56 % (741192)Instruction limit reached!
% 1.83/0.56 % (741192)------------------------------
% 1.83/0.56 % (741192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.56 % (741192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.56 % (741192)CaDiCaL version: 2.1.3
% 1.83/0.56 % (741192)Termination reason: Instruction limit
% 1.83/0.56 % (741192)Termination phase: Saturation
% 1.83/0.56 % (741192)Time elapsed: 0.060 s
% 1.83/0.56 % (741192)Peak memory usage: 12 MB
% 1.83/0.56 % (741192)Instructions burned: 87 (million)
% 1.83/0.56 % (741204)Instruction limit reached!
% 1.83/0.56 % (741204)------------------------------
% 1.83/0.56 % (741204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.56 % (741204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.56 % (741204)CaDiCaL version: 2.1.3
% 1.83/0.56 % (741204)Termination reason: Instruction limit
% 1.83/0.56 % (741204)Termination phase: Saturation
% 1.83/0.56 % (741204)Time elapsed: 0.034 s
% 1.83/0.56 % (741204)Peak memory usage: 12 MB
% 1.83/0.56 % (741204)Instructions burned: 38 (million)
% 1.83/0.56 % (741221)Instruction limit reached!
% 1.83/0.56 % (741221)------------------------------
% 2.31/0.63 % (741221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.63 % (741221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.63 % (741221)CaDiCaL version: 2.1.3
% 2.31/0.63 % (741221)Termination reason: Instruction limit
% 2.31/0.63 % (741221)Termination phase: Saturation
% 2.31/0.63 % (741221)Time elapsed: 0.014 s
% 2.31/0.63 % (741221)Peak memory usage: 12 MB
% 2.31/0.63 % (741221)Instructions burned: 14 (million)
% 2.31/0.63 % (741220)Instruction limit reached!
% 2.31/0.63 % (741220)------------------------------
% 2.31/0.63 % (741220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.63 % (741220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.63 % (741220)CaDiCaL version: 2.1.3
% 2.31/0.63 % (741220)Termination reason: Instruction limit
% 2.31/0.63 % (741220)Termination phase: Saturation
% 2.31/0.63 % (741220)Time elapsed: 0.021 s
% 2.31/0.63 % (741220)Peak memory usage: 12 MB
% 2.31/0.63 % (741220)Instructions burned: 25 (million)
% 2.31/0.63 % (741235)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1576025147:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.31/0.63 % (741240)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3132723083:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.31/0.63 % (741138)Instruction limit reached!
% 2.31/0.63 % (741138)------------------------------
% 2.31/0.63 % (741138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.63 % (741138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.63 % (741138)CaDiCaL version: 2.1.3
% 2.31/0.63 % (741138)Termination reason: Instruction limit
% 2.31/0.63 % (741138)Termination phase: Saturation
% 2.31/0.63 % (741138)Time elapsed: 0.183 s
% 2.31/0.63 % (741138)Peak memory usage: 12 MB
% 2.31/0.63 % (741138)Instructions burned: 636 (million)
% 2.31/0.63 % (741244)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3631115974:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.31/0.63 % (741242)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3115469744:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.31/0.63 % (741249)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2552187827:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.31/0.63 % (741242)Instruction limit reached!
% 2.31/0.63 % (741242)------------------------------
% 2.31/0.63 % (741242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.63 % (741242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.63 % (741242)CaDiCaL version: 2.1.3
% 2.31/0.63 % (741242)Termination reason: Instruction limit
% 2.31/0.63 % (741242)Termination phase: Saturation
% 2.31/0.63 % (741242)Time elapsed: 0.002 s
% 2.31/0.63 % (741242)Peak memory usage: 12 MB
% 2.31/0.63 % (741242)Instructions burned: 3 (million)
% 2.31/0.63 % (741240)Instruction limit reached!
% 2.31/0.63 % (741240)------------------------------
% 2.31/0.63 % (741240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.63 % (741240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.63 % (741240)CaDiCaL version: 2.1.3
% 2.31/0.63 % (741240)Termination reason: Instruction limit
% 2.31/0.63 % (741240)Termination phase: Saturation
% 2.31/0.63 % (741240)Time elapsed: 0.015 s
% 2.31/0.63 % (741240)Peak memory usage: 12 MB
% 2.31/0.63 % (741240)Instructions burned: 14 (million)
% 2.31/0.63 % (741244)Instruction limit reached!
% 2.31/0.63 % (741244)------------------------------
% 2.31/0.63 % (741244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.63 % (741244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.63 % (741244)CaDiCaL version: 2.1.3
% 2.31/0.63 % (741244)Termination reason: Instruction limit
% 2.31/0.63 % (741244)Termination phase: Saturation
% 2.31/0.63 % (741244)Time elapsed: 0.025 s
% 2.31/0.63 % (741244)Peak memory usage: 12 MB
% 2.31/0.63 % (741244)Instructions burned: 26 (million)
% 2.31/0.63 % (741258)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1827673597:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.31/0.63 % (741249)Instruction limit reached!
% 2.31/0.63 % (741249)------------------------------
% 2.61/0.74 % (741249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.74 % (741249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.74 % (741249)CaDiCaL version: 2.1.3
% 2.61/0.74 % (741249)Termination reason: Instruction limit
% 2.61/0.74 % (741249)Termination phase: Saturation
% 2.61/0.74 % (741249)Time elapsed: 0.022 s
% 2.61/0.74 % (741249)Peak memory usage: 11 MB
% 2.61/0.74 % (741249)Instructions burned: 23 (million)
% 2.61/0.74 % (741266)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.61/0.74 % (741266)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.61/0.74 % (741272)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=1557878658:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.61/0.74 % (741266)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=954050391:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.61/0.74 % (741268)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.61/0.74 % (741272)Instruction limit reached!
% 2.61/0.74 % (741272)------------------------------
% 2.61/0.74 % (741272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.74 % (741272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.74 % (741272)CaDiCaL version: 2.1.3
% 2.61/0.74 % (741272)Termination reason: Instruction limit
% 2.61/0.74 % (741272)Termination phase: Saturation
% 2.61/0.74 % (741272)Time elapsed: 0.016 s
% 2.61/0.74 % (741272)Peak memory usage: 12 MB
% 2.61/0.74 % (741272)Instructions burned: 33 (million)
% 2.61/0.74 % (741268)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=3308713774:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.61/0.74 % (741266)Instruction limit reached!
% 2.61/0.74 % (741266)------------------------------
% 2.61/0.74 % (741266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.74 % (741266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.74 % (741266)CaDiCaL version: 2.1.3
% 2.61/0.74 % (741266)Termination reason: Instruction limit
% 2.61/0.74 % (741266)Termination phase: Saturation
% 2.61/0.74 % (741266)Time elapsed: 0.015 s
% 2.61/0.74 % (741266)Peak memory usage: 12 MB
% 2.61/0.74 % (741266)Instructions burned: 14 (million)
% 2.61/0.74 % (741276)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1144489409:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.61/0.74 % (741268)Instruction limit reached!
% 2.61/0.74 % (741268)------------------------------
% 2.61/0.74 % (741268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.74 % (741268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.74 % (741268)CaDiCaL version: 2.1.3
% 2.61/0.74 % (741268)Termination reason: Instruction limit
% 2.61/0.74 % (741268)Termination phase: Saturation
% 2.61/0.74 % (741268)Time elapsed: 0.009 s
% 2.61/0.74 % (741268)Peak memory usage: 12 MB
% 2.61/0.74 % (741268)Instructions burned: 13 (million)
% 2.61/0.74 % (741276)Instruction limit reached!
% 2.61/0.74 % (741276)------------------------------
% 2.61/0.74 % (741276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.74 % (741276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.74 % (741276)CaDiCaL version: 2.1.3
% 2.61/0.74 % (741276)Termination reason: Instruction limit
% 2.61/0.74 % (741276)Termination phase: Saturation
% 2.61/0.74 % (741276)Time elapsed: 0.007 s
% 2.61/0.74 % (741276)Peak memory usage: 12 MB
% 2.61/0.74 % (741276)Instructions burned: 7 (million)
% 2.61/0.74 % (741258)Instruction limit reached!
% 2.61/0.74 % (741258)------------------------------
% 2.61/0.74 % (741258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.74 % (741258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.44/0.82 % (741258)CaDiCaL version: 2.1.3
% 3.44/0.82 % (741258)Termination reason: Instruction limit
% 3.44/0.82 % (741258)Termination phase: Saturation
% 3.44/0.82 % (741258)Time elapsed: 0.049 s
% 3.44/0.82 % (741258)Peak memory usage: 12 MB
% 3.44/0.82 % (741258)Instructions burned: 64 (million)
% 3.44/0.82 % (741289)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1428939404:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 3.44/0.82 % (741289)Instruction limit reached!
% 3.44/0.82 % (741289)------------------------------
% 3.44/0.82 % (741289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.44/0.82 % (741289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.44/0.82 % (741289)CaDiCaL version: 2.1.3
% 3.44/0.82 % (741289)Termination reason: Instruction limit
% 3.44/0.82 % (741289)Termination phase: Saturation
% 3.44/0.82 % (741289)Time elapsed: 0.009 s
% 3.44/0.82 % (741289)Peak memory usage: 11 MB
% 3.44/0.82 % (741289)Instructions burned: 24 (million)
% 3.44/0.82 % (741291)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3331082649:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 3.44/0.82 % (741294)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=524535705:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 3.44/0.82 % (741296)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1133934959:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 3.44/0.82 % (741306)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2842109442:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.44/0.82 % (741299)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=249318206:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.44/0.82 % (741291)Instruction limit reached!
% 3.44/0.82 % (741291)------------------------------
% 3.44/0.82 % (741291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.44/0.82 % (741291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.44/0.82 % (741291)CaDiCaL version: 2.1.3
% 3.44/0.82 % (741291)Termination reason: Instruction limit
% 3.44/0.82 % (741291)Termination phase: Saturation
% 3.44/0.82 % (741291)Time elapsed: 0.021 s
% 3.44/0.82 % (741291)Peak memory usage: 12 MB
% 3.44/0.82 % (741291)Instructions burned: 21 (million)
% 3.44/0.82 % (741306)Instruction limit reached!
% 3.44/0.82 % (741306)------------------------------
% 3.44/0.82 % (741306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.44/0.82 % (741306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.44/0.82 % (741306)CaDiCaL version: 2.1.3
% 3.44/0.82 % (741306)Termination reason: Instruction limit
% 3.44/0.82 % (741306)Termination phase: Saturation
% 3.44/0.82 % (741306)Time elapsed: 0.022 s
% 3.44/0.82 % (741306)Peak memory usage: 12 MB
% 3.44/0.82 % (741306)Instructions burned: 44 (million)
% 3.44/0.82 % (741319)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.44/0.82 % (741319)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=713966137:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.44/0.82 % (741213)Instruction limit reached!
% 3.44/0.82 % (741213)------------------------------
% 3.44/0.82 % (741213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.44/0.82 % (741213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.44/0.82 % (741213)CaDiCaL version: 2.1.3
% 3.44/0.82 % (741213)Termination reason: Instruction limit
% 3.44/0.82 % (741213)Termination phase: Saturation
% 3.44/0.82 % (741213)Time elapsed: 0.203 s
% 3.44/0.82 % (741213)Peak memory usage: 12 MB
% 3.44/0.82 % (741213)Instructions burned: 249 (million)
% 3.44/0.82 % (741319)Instruction limit reached!
% 3.44/0.82 % (741319)------------------------------
% 3.44/0.82 % (741319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.44/0.82 % (741319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.44/0.82 % (741319)CaDiCaL version: 2.1.3
% 3.44/0.82 % (741319)Termination reason: Instruction limit
% 3.44/0.82 % (741319)Termination phase: Saturation
% 3.44/0.82 % (741319)Time elapsed: 0.005 s
% 3.44/0.82 % (741319)Peak memory usage: 12 MB
% 3.65/0.98 % (741319)Instructions burned: 8 (million)
% 3.65/0.98 % (741323)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1990805612:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.65/0.98 % (741331)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.65/0.98 % (741331)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2781030940:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 3.65/0.98 % (741331)Instruction limit reached!
% 3.65/0.98 % (741331)------------------------------
% 3.65/0.98 % (741331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.98 % (741331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.98 % (741331)CaDiCaL version: 2.1.3
% 3.65/0.98 % (741331)Termination reason: Instruction limit
% 3.65/0.98 % (741331)Termination phase: Saturation
% 3.65/0.98 % (741331)Time elapsed: 0.003 s
% 3.65/0.98 % (741331)Peak memory usage: 12 MB
% 3.65/0.98 % (741331)Instructions burned: 6 (million)
% 3.65/0.98 % (741330)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=2358801481:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 3.65/0.98 % (741346)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=974771884:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 3.65/0.98 % (741346)Instruction limit reached!
% 3.65/0.98 % (741346)------------------------------
% 3.65/0.98 % (741346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.98 % (741346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.98 % (741346)CaDiCaL version: 2.1.3
% 3.65/0.98 % (741346)Termination reason: Instruction limit
% 3.65/0.98 % (741346)Termination phase: Saturation
% 3.65/0.98 % (741346)Time elapsed: 0.010 s
% 3.65/0.98 % (741346)Peak memory usage: 12 MB
% 3.65/0.98 % (741346)Instructions burned: 23 (million)
% 3.65/0.98 % (741358)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1463592268:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 3.65/0.98 % (741358)Instruction limit reached!
% 3.65/0.98 % (741358)------------------------------
% 3.65/0.98 % (741358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.98 % (741358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.98 % (741358)CaDiCaL version: 2.1.3
% 3.65/0.98 % (741358)Termination reason: Instruction limit
% 3.65/0.98 % (741358)Termination phase: Saturation
% 3.65/0.98 % (741358)Time elapsed: 0.010 s
% 3.65/0.98 % (741358)Peak memory usage: 12 MB
% 3.65/0.98 % (741358)Instructions burned: 20 (million)
% 3.65/0.98 % (741296)Instruction limit reached!
% 3.65/0.98 % (741296)------------------------------
% 3.65/0.98 % (741296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.98 % (741296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.98 % (741296)CaDiCaL version: 2.1.3
% 3.65/0.98 % (741296)Termination reason: Instruction limit
% 3.65/0.98 % (741296)Termination phase: Saturation
% 3.65/0.98 % (741296)Time elapsed: 0.125 s
% 3.65/0.98 % (741296)Peak memory usage: 13 MB
% 3.65/0.98 % (741296)Instructions burned: 143 (million)
% 3.65/0.98 % (741235)Instruction limit reached!
% 3.65/0.98 % (741235)------------------------------
% 3.65/0.98 % (741235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.98 % (741235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.98 % (741235)CaDiCaL version: 2.1.3
% 3.65/0.98 % (741235)Termination reason: Instruction limit
% 3.65/0.98 % (741235)Termination phase: Saturation
% 3.65/0.98 % (741235)Time elapsed: 0.257 s
% 3.65/0.98 % (741235)Peak memory usage: 13 MB
% 3.65/0.98 % (741235)Instructions burned: 330 (million)
% 3.65/0.98 % (741373)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=2863766323:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 3.65/0.98 % (741377)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=918015899:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 6.17/1.15 % (741384)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=3292016041:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2995 on theBenchmark for (2995ds/45Mi)
% 6.17/1.15 % (741299)Instruction limit reached!
% 6.17/1.15 % (741299)------------------------------
% 6.17/1.15 % (741299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.15 % (741299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.17/1.15 % (741299)CaDiCaL version: 2.1.3
% 6.17/1.15 % (741299)Termination reason: Instruction limit
% 6.17/1.15 % (741299)Termination phase: Saturation
% 6.17/1.15 % (741299)Time elapsed: 0.151 s
% 6.17/1.15 % (741299)Peak memory usage: 13 MB
% 6.17/1.15 % (741299)Instructions burned: 193 (million)
% 6.17/1.15 % (741384)Instruction limit reached!
% 6.17/1.15 % (741384)------------------------------
% 6.17/1.15 % (741384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.15 % (741384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.17/1.15 % (741384)CaDiCaL version: 2.1.3
% 6.17/1.15 % (741384)Termination reason: Instruction limit
% 6.17/1.15 % (741384)Termination phase: Saturation
% 6.17/1.15 % (741384)Time elapsed: 0.021 s
% 6.17/1.15 % (741384)Peak memory usage: 12 MB
% 6.17/1.15 % (741384)Instructions burned: 45 (million)
% 6.17/1.15 % (741393)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2684869408:i=480:rtra=on_2995 on theBenchmark for (2995ds/480Mi)
% 6.17/1.15 % (741330)Instruction limit reached!
% 6.17/1.15 % (741330)------------------------------
% 6.17/1.15 % (741330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.15 % (741330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.17/1.15 % (741330)CaDiCaL version: 2.1.3
% 6.17/1.15 % (741330)Termination reason: Instruction limit
% 6.17/1.15 % (741330)Termination phase: Saturation
% 6.17/1.15 % (741330)Time elapsed: 0.121 s
% 6.17/1.15 % (741330)Peak memory usage: 12 MB
% 6.17/1.15 % (741330)Instructions burned: 169 (million)
% 6.17/1.15 % (741404)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3343681177:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 6.17/1.15 % (741404)Instruction limit reached!
% 6.17/1.15 % (741404)------------------------------
% 6.17/1.15 % (741404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.15 % (741404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.17/1.15 % (741404)CaDiCaL version: 2.1.3
% 6.17/1.15 % (741404)Termination reason: Instruction limit
% 6.17/1.15 % (741404)Termination phase: Saturation
% 6.17/1.15 % (741404)Time elapsed: 0.011 s
% 6.17/1.15 % (741404)Peak memory usage: 12 MB
% 6.17/1.15 % (741404)Instructions burned: 22 (million)
% 6.17/1.15 % (741410)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 6.17/1.15 % (741323)Instruction limit reached!
% 6.17/1.15 % (741323)------------------------------
% 6.17/1.15 % (741323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.15 % (741323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.17/1.15 % (741323)CaDiCaL version: 2.1.3
% 6.17/1.15 % (741323)Termination reason: Instruction limit
% 6.17/1.15 % (741323)Termination phase: Saturation
% 6.17/1.15 % (741323)Time elapsed: 0.157 s
% 6.17/1.15 % (741323)Peak memory usage: 13 MB
% 6.17/1.15 % (741323)Instructions burned: 181 (million)
% 6.17/1.15 % (741410)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3856095875:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 6.17/1.15 % (741421)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2083942077:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 6.17/1.15 % (741421)Instruction limit reached!
% 6.17/1.15 % (741421)------------------------------
% 6.17/1.15 % (741421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.15 % (741421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/1.38 % (741421)CaDiCaL version: 2.1.3
% 6.71/1.38 % (741421)Termination reason: Instruction limit
% 6.71/1.38 % (741421)Termination phase: Saturation
% 6.71/1.38 % (741421)Time elapsed: 0.007 s
% 6.71/1.38 % (741421)Peak memory usage: 12 MB
% 6.71/1.38 % (741421)Instructions burned: 13 (million)
% 6.71/1.38 % (741423)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=2270882182:i=66:s2at=3:nm=2:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/66Mi)
% 6.71/1.38 % (741435)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2855130588:i=51:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/51Mi)
% 6.71/1.38 % (741435)Instruction limit reached!
% 6.71/1.38 % (741435)------------------------------
% 6.71/1.38 % (741435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.71/1.38 % (741435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/1.38 % (741435)CaDiCaL version: 2.1.3
% 6.71/1.38 % (741435)Termination reason: Instruction limit
% 6.71/1.38 % (741435)Termination phase: Saturation
% 6.71/1.38 % (741435)Time elapsed: 0.024 s
% 6.71/1.38 % (741435)Peak memory usage: 12 MB
% 6.71/1.38 % (741435)Instructions burned: 51 (million)
% 6.71/1.38 % (741453)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1744540923:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 6.71/1.38 % (741423)Instruction limit reached!
% 6.71/1.38 % (741423)------------------------------
% 6.71/1.38 % (741423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.71/1.38 % (741423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/1.38 % (741423)CaDiCaL version: 2.1.3
% 6.71/1.38 % (741423)Termination reason: Instruction limit
% 6.71/1.38 % (741423)Termination phase: Saturation
% 6.71/1.38 % (741423)Time elapsed: 0.059 s
% 6.71/1.38 % (741423)Peak memory usage: 13 MB
% 6.71/1.38 % (741423)Instructions burned: 67 (million)
% 6.71/1.38 % (741453)Instruction limit reached!
% 6.71/1.38 % (741453)------------------------------
% 6.71/1.38 % (741453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.71/1.38 % (741453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/1.38 % (741453)CaDiCaL version: 2.1.3
% 6.71/1.38 % (741453)Termination reason: Instruction limit
% 6.71/1.38 % (741453)Termination phase: Saturation
% 6.71/1.38 % (741453)Time elapsed: 0.015 s
% 6.71/1.38 % (741453)Peak memory usage: 12 MB
% 6.71/1.38 % (741453)Instructions burned: 33 (million)
% 6.71/1.38 % (741464)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=881683551:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 6.71/1.38 % (741460)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3425755699:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 6.71/1.38 % (741464)Instruction limit reached!
% 6.71/1.38 % (741464)------------------------------
% 6.71/1.38 % (741464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.71/1.38 % (741464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/1.38 % (741464)CaDiCaL version: 2.1.3
% 6.71/1.38 % (741464)Termination reason: Instruction limit
% 6.71/1.38 % (741464)Termination phase: Saturation
% 6.71/1.38 % (741464)Time elapsed: 0.017 s
% 6.71/1.38 % (741464)Peak memory usage: 12 MB
% 6.71/1.38 % (741464)Instructions burned: 36 (million)
% 6.71/1.38 % (741474)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3481935727:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2993 on theBenchmark for (2993ds/67Mi)
% 6.71/1.38 % (741410)Instruction limit reached!
% 6.71/1.38 % (741410)------------------------------
% 6.71/1.38 % (741410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.71/1.38 % (741410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.71/1.38 % (741410)CaDiCaL version: 2.1.3
% 6.71/1.38 % (741410)Termination reason: Instruction limit
% 6.71/1.38 % (741410)Termination phase: Saturation
% 6.71/1.38 % (741410)Time elapsed: 0.168 s
% 6.71/1.38 % (741410)Peak memory usage: 12 MB
% 6.71/1.38 % (741410)Instructions burned: 201 (million)
% 6.71/1.38 % (741474)Instruction limit reached!
% 6.71/1.38 % (741474)------------------------------
% 6.71/1.38 % (741474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.67 % (741474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.67 % (741474)CaDiCaL version: 2.1.3
% 7.96/1.67 % (741474)Termination reason: Instruction limit
% 7.96/1.67 % (741474)Termination phase: Saturation
% 7.96/1.67 % (741474)Time elapsed: 0.033 s
% 7.96/1.67 % (741474)Peak memory usage: 12 MB
% 7.96/1.67 % (741474)Instructions burned: 70 (million)
% 7.96/1.67 % (741484)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 7.96/1.67 % (741373)Instruction limit reached!
% 7.96/1.67 % (741373)------------------------------
% 7.96/1.67 % (741373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.67 % (741373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.67 % (741373)CaDiCaL version: 2.1.3
% 7.96/1.67 % (741373)Termination reason: Instruction limit
% 7.96/1.67 % (741373)Termination phase: Saturation
% 7.96/1.67 % (741373)Time elapsed: 0.248 s
% 7.96/1.67 % (741373)Peak memory usage: 14 MB
% 7.96/1.67 % (741373)Instructions burned: 318 (million)
% 7.96/1.67 % (741484)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3665045959:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2992 on theBenchmark for (2992ds/180Mi)
% 7.96/1.67 % (741491)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1221799121:st=2:i=246:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/246Mi)
% 7.96/1.67 % (741493)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=2966108763:cond=on:i=96:bd=all:rtra=on_2992 on theBenchmark for (2992ds/96Mi)
% 7.96/1.67 % (741460)Instruction limit reached!
% 7.96/1.67 % (741460)------------------------------
% 7.96/1.67 % (741460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.67 % (741460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.67 % (741460)CaDiCaL version: 2.1.3
% 7.96/1.67 % (741460)Termination reason: Instruction limit
% 7.96/1.67 % (741460)Termination phase: Saturation
% 7.96/1.67 % (741460)Time elapsed: 0.106 s
% 7.96/1.67 % (741460)Peak memory usage: 12 MB
% 7.96/1.67 % (741460)Instructions burned: 137 (million)
% 7.96/1.67 % (741505)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3869914628:i=427:sd=1:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/427Mi)
% 7.96/1.67 % (741493)Instruction limit reached!
% 7.96/1.67 % (741493)------------------------------
% 7.96/1.67 % (741493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.67 % (741493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.67 % (741493)CaDiCaL version: 2.1.3
% 7.96/1.67 % (741493)Termination reason: Instruction limit
% 7.96/1.67 % (741493)Termination phase: Saturation
% 7.96/1.67 % (741493)Time elapsed: 0.079 s
% 7.96/1.67 % (741493)Peak memory usage: 12 MB
% 7.96/1.67 % (741493)Instructions burned: 96 (million)
% 7.96/1.67 % (741491)Instruction limit reached!
% 7.96/1.67 % (741491)------------------------------
% 7.96/1.67 % (741491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.67 % (741491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.67 % (741491)CaDiCaL version: 2.1.3
% 7.96/1.67 % (741491)Termination reason: Instruction limit
% 7.96/1.67 % (741491)Termination phase: Saturation
% 7.96/1.67 % (741491)Time elapsed: 0.111 s
% 7.96/1.67 % (741491)Peak memory usage: 13 MB
% 7.96/1.67 % (741491)Instructions burned: 246 (million)
% 7.96/1.67 % (741525)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3878493854:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/515Mi)
% 7.96/1.67 % (741522)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2963756588:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/874Mi)
% 7.96/1.67 % (741484)Instruction limit reached!
% 7.96/1.67 % (741484)------------------------------
% 7.96/1.67 % (741484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.67 % (741484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.67 % (741484)CaDiCaL version: 2.1.3
% 7.96/1.67 % (741484)Termination reason: Instruction limit
% 7.96/1.67 % (741484)Termination phase: Saturation
% 7.96/1.67 % (741484)Time elapsed: 0.151 s
% 7.96/1.67 % (741484)Peak memory usage: 14 MB
% 7.96/1.67 % (741484)Instructions burned: 181 (million)
% 7.96/1.67 % (741393)Instruction limit reached!
% 7.96/1.67 % (741393)------------------------------
% 8.44/1.77 % (741393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.77 % (741393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.77 % (741393)CaDiCaL version: 2.1.3
% 8.44/1.77 % (741393)Termination reason: Instruction limit
% 8.44/1.77 % (741393)Termination phase: Saturation
% 8.44/1.77 % (741393)Time elapsed: 0.376 s
% 8.44/1.77 % (741393)Peak memory usage: 13 MB
% 8.44/1.77 % (741393)Instructions burned: 480 (million)
% 8.44/1.77 % (741538)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=648073392:i=44:ep=R:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/44Mi)
% 8.44/1.77 % (741537)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3345132633:st=1.5:i=130:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/130Mi)
% 8.44/1.77 % (741538)Instruction limit reached!
% 8.44/1.77 % (741538)------------------------------
% 8.44/1.77 % (741538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.77 % (741538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.77 % (741538)CaDiCaL version: 2.1.3
% 8.44/1.77 % (741538)Termination reason: Instruction limit
% 8.44/1.77 % (741538)Termination phase: Saturation
% 8.44/1.77 % (741538)Time elapsed: 0.040 s
% 8.44/1.77 % (741538)Peak memory usage: 12 MB
% 8.44/1.77 % (741538)Instructions burned: 44 (million)
% 8.44/1.77 % (741558)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=1313520854:s2a=on:i=571:nm=16:rtra=on_2990 on theBenchmark for (2990ds/571Mi)
% 8.44/1.77 % (741537)Instruction limit reached!
% 8.44/1.77 % (741537)------------------------------
% 8.44/1.77 % (741537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.77 % (741537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.77 % (741537)CaDiCaL version: 2.1.3
% 8.44/1.77 % (741537)Termination reason: Instruction limit
% 8.44/1.77 % (741537)Termination phase: Saturation
% 8.44/1.77 % (741537)Time elapsed: 0.092 s
% 8.44/1.77 % (741537)Peak memory usage: 12 MB
% 8.44/1.77 % (741537)Instructions burned: 131 (million)
% 8.44/1.77 % (741569)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=4239407185:i=450:rtra=on:ixr=off:ntd=on_2989 on theBenchmark for (2989ds/450Mi)
% 8.44/1.77 % (741525)Instruction limit reached!
% 8.44/1.77 % (741525)------------------------------
% 8.44/1.77 % (741525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.77 % (741525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.77 % (741525)CaDiCaL version: 2.1.3
% 8.44/1.77 % (741525)Termination reason: Instruction limit
% 8.44/1.77 % (741525)Termination phase: Saturation
% 8.44/1.77 % (741525)Time elapsed: 0.227 s
% 8.44/1.77 % (741525)Peak memory usage: 15 MB
% 8.44/1.77 % (741525)Instructions burned: 515 (million)
% 8.44/1.77 % (741505)Instruction limit reached!
% 8.44/1.77 % (741505)------------------------------
% 8.44/1.77 % (741505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.77 % (741505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.77 % (741505)CaDiCaL version: 2.1.3
% 8.44/1.77 % (741505)Termination reason: Instruction limit
% 8.44/1.77 % (741505)Termination phase: Saturation
% 8.44/1.77 % (741505)Time elapsed: 0.299 s
% 8.44/1.77 % (741505)Peak memory usage: 14 MB
% 8.44/1.77 % (741505)Instructions burned: 427 (million)
% 8.44/1.77 % (741377)Instruction limit reached!
% 8.44/1.77 % (741377)------------------------------
% 8.44/1.77 % (741377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.77 % (741377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.77 % (741377)CaDiCaL version: 2.1.3
% 8.44/1.77 % (741377)Termination reason: Instruction limit
% 8.44/1.77 % (741377)Termination phase: Saturation
% 8.44/1.77 % (741377)Time elapsed: 0.619 s
% 8.44/1.77 % (741377)Peak memory usage: 15 MB
% 8.44/1.77 % (741377)Instructions burned: 854 (million)
% 8.44/1.77 % (741587)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1086443421:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/95Mi)
% 8.44/1.77 % (741589)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=1200354817: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_2988 on theBenchmark for (2988ds/105Mi)
% 10.80/1.93 % (741588)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=1061858612:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2988 on theBenchmark for (2988ds/65Mi)
% 10.80/1.93 % (741589)Instruction limit reached!
% 10.80/1.93 % (741589)------------------------------
% 10.80/1.93 % (741589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.80/1.93 % (741589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/1.93 % (741589)CaDiCaL version: 2.1.3
% 10.80/1.93 % (741589)Termination reason: Instruction limit
% 10.80/1.93 % (741589)Termination phase: Saturation
% 10.80/1.93 % (741589)Time elapsed: 0.050 s
% 10.80/1.93 % (741589)Peak memory usage: 13 MB
% 10.80/1.93 % (741589)Instructions burned: 107 (million)
% 10.80/1.93 % (741588)Instruction limit reached!
% 10.80/1.93 % (741588)------------------------------
% 10.80/1.93 % (741588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.80/1.93 % (741588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/1.93 % (741588)CaDiCaL version: 2.1.3
% 10.80/1.93 % (741588)Termination reason: Instruction limit
% 10.80/1.93 % (741588)Termination phase: Saturation
% 10.80/1.93 % (741588)Time elapsed: 0.060 s
% 10.80/1.93 % (741588)Peak memory usage: 12 MB
% 10.80/1.93 % (741588)Instructions burned: 65 (million)
% 10.80/1.93 % (741601)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=1022812021:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2988 on theBenchmark for (2988ds/5755Mi)
% 10.80/1.93 % (741587)Instruction limit reached!
% 10.80/1.93 % (741587)------------------------------
% 10.80/1.93 % (741587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.80/1.93 % (741587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/1.93 % (741587)CaDiCaL version: 2.1.3
% 10.80/1.93 % (741587)Termination reason: Instruction limit
% 10.80/1.93 % (741587)Termination phase: Saturation
% 10.80/1.93 % (741587)Time elapsed: 0.087 s
% 10.80/1.93 % (741587)Peak memory usage: 12 MB
% 10.80/1.93 % (741587)Instructions burned: 95 (million)
% 10.80/1.93 % (741604)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=3080879642:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/375Mi)
% 10.80/1.93 % (741607)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2672975636:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2987 on theBenchmark for (2987ds/495Mi)
% 10.80/1.93 % (741294)Instruction limit reached!
% 10.80/1.93 % (741294)------------------------------
% 10.80/1.93 % (741294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.80/1.93 % (741294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/1.93 % (741294)CaDiCaL version: 2.1.3
% 10.80/1.93 % (741294)Termination reason: Instruction limit
% 10.80/1.93 % (741294)Termination phase: Saturation
% 10.80/1.93 % (741294)Time elapsed: 0.958 s
% 10.80/1.93 % (741294)Peak memory usage: 14 MB
% 10.80/1.93 % (741294)Instructions burned: 1241 (million)
% 10.80/1.93 % (741619)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=1802610483:cond=on:i=34:hud=10:nm=10:rtra=on_2987 on theBenchmark for (2987ds/34Mi)
% 10.80/1.93 % (741619)Instruction limit reached!
% 10.80/1.93 % (741619)------------------------------
% 10.80/1.93 % (741619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.80/1.93 % (741619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/1.93 % (741619)CaDiCaL version: 2.1.3
% 10.80/1.93 % (741619)Termination reason: Instruction limit
% 10.80/1.93 % (741619)Termination phase: Saturation
% 10.80/1.93 % (741619)Time elapsed: 0.031 s
% 10.80/1.93 % (741619)Peak memory usage: 12 MB
% 10.80/1.93 % (741619)Instructions burned: 35 (million)
% 10.80/1.93 % (741627)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=387829312:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2986 on theBenchmark for (2986ds/91Mi)
% 10.80/1.93 % (741627)Instruction limit reached!
% 10.80/1.93 % (741627)------------------------------
% 10.80/1.93 % (741627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.80/1.93 % (741627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.17/2.17 % (741627)CaDiCaL version: 2.1.3
% 13.17/2.17 % (741627)Termination reason: Instruction limit
% 13.17/2.17 % (741627)Termination phase: Saturation
% 13.17/2.17 % (741627)Time elapsed: 0.053 s
% 13.17/2.17 % (741627)Peak memory usage: 12 MB
% 13.17/2.17 % (741627)Instructions burned: 91 (million)
% 13.17/2.17 % (741569)Instruction limit reached!
% 13.17/2.17 % (741569)------------------------------
% 13.17/2.17 % (741569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.17/2.17 % (741569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.17/2.17 % (741569)CaDiCaL version: 2.1.3
% 13.17/2.17 % (741569)Termination reason: Instruction limit
% 13.17/2.17 % (741569)Termination phase: Saturation
% 13.17/2.17 % (741569)Time elapsed: 0.368 s
% 13.17/2.17 % (741569)Peak memory usage: 13 MB
% 13.17/2.17 % (741569)Instructions burned: 450 (million)
% 13.17/2.17 % (741641)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=1244854702:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2985 on theBenchmark for (2985ds/66Mi)
% 13.17/2.17 % (741642)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=4013150961:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2985 on theBenchmark for (2985ds/22Mi)
% 13.17/2.17 % (741607)Instruction limit reached!
% 13.17/2.17 % (741607)------------------------------
% 13.17/2.17 % (741607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.17/2.17 % (741607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.17/2.17 % (741607)CaDiCaL version: 2.1.3
% 13.17/2.17 % (741607)Termination reason: Instruction limit
% 13.17/2.17 % (741607)Termination phase: Saturation
% 13.17/2.17 % (741607)Time elapsed: 0.221 s
% 13.17/2.17 % (741607)Peak memory usage: 14 MB
% 13.17/2.17 % (741607)Instructions burned: 496 (million)
% 13.17/2.17 % (741558)Instruction limit reached!
% 13.17/2.17 % (741558)------------------------------
% 13.17/2.17 % (741558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.17/2.17 % (741558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.17/2.17 % (741558)CaDiCaL version: 2.1.3
% 13.17/2.17 % (741558)Termination reason: Instruction limit
% 13.17/2.17 % (741558)Termination phase: Saturation
% 13.17/2.17 % (741558)Time elapsed: 0.462 s
% 13.17/2.17 % (741558)Peak memory usage: 14 MB
% 13.17/2.17 % (741558)Instructions burned: 571 (million)
% 13.17/2.17 % (741642)Instruction limit reached!
% 13.17/2.17 % (741642)------------------------------
% 13.17/2.17 % (741642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.17/2.17 % (741642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.17/2.17 % (741642)CaDiCaL version: 2.1.3
% 13.17/2.17 % (741642)Termination reason: Instruction limit
% 13.17/2.17 % (741642)Termination phase: Saturation
% 13.17/2.17 % (741642)Time elapsed: 0.021 s
% 13.17/2.17 % (741642)Peak memory usage: 12 MB
% 13.17/2.17 % (741642)Instructions burned: 22 (million)
% 13.17/2.17 % (741651)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=3729031647:i=338:bd=all:ins=4:rtra=on_2985 on theBenchmark for (2985ds/338Mi)
% 13.17/2.17 % (741641)Instruction limit reached!
% 13.17/2.17 % (741641)------------------------------
% 13.17/2.17 % (741641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.17/2.17 % (741641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.17/2.17 % (741641)CaDiCaL version: 2.1.3
% 13.17/2.17 % (741641)Termination reason: Instruction limit
% 13.17/2.17 % (741641)Termination phase: Saturation
% 13.17/2.17 % (741641)Time elapsed: 0.048 s
% 13.17/2.17 % (741641)Peak memory usage: 12 MB
% 13.17/2.17 % (741641)Instructions burned: 67 (million)
% 13.17/2.17 % (741653)lrs+10_1_sil=128000:si=on:urr=on:random_seed=318951256:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/28Mi)
% 13.17/2.17 % (741655)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 13.17/2.17 % (741653)Instruction limit reached!
% 13.17/2.17 % (741653)------------------------------
% 13.17/2.17 % (741653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.17/2.17 % (741653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.17/2.17 % (741653)CaDiCaL version: 2.1.3
% 13.17/2.17 % (741653)Termination reason: Instruction limit
% 13.42/2.30 % (741653)Termination phase: Saturation
% 13.42/2.30 % (741653)Time elapsed: 0.019 s
% 13.42/2.30 % (741653)Peak memory usage: 12 MB
% 13.42/2.30 % (741653)Instructions burned: 29 (million)
% 13.42/2.30 % (741655)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=4178001569:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2985 on theBenchmark for (2985ds/137Mi)
% 13.42/2.30 % (741657)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=266306222:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2985 on theBenchmark for (2985ds/340Mi)
% 13.42/2.30 % (741664)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2034330148:i=227:sd=1:bd=all:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/227Mi)
% 13.42/2.30 % (741604)Instruction limit reached!
% 13.42/2.30 % (741604)------------------------------
% 13.42/2.30 % (741604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.42/2.30 % (741604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.42/2.30 % (741604)CaDiCaL version: 2.1.3
% 13.42/2.30 % (741604)Termination reason: Instruction limit
% 13.42/2.30 % (741604)Termination phase: Saturation
% 13.42/2.30 % (741604)Time elapsed: 0.315 s
% 13.42/2.30 % (741604)Peak memory usage: 13 MB
% 13.42/2.30 % (741604)Instructions burned: 375 (million)
% 13.42/2.30 % (741670)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 13.42/2.30 % (741670)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=109588360:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/373Mi)
% 13.42/2.30 % (741522)Instruction limit reached!
% 13.42/2.30 % (741522)------------------------------
% 13.42/2.30 % (741522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.42/2.30 % (741522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.42/2.30 % (741522)CaDiCaL version: 2.1.3
% 13.42/2.30 % (741522)Termination reason: Instruction limit
% 13.42/2.30 % (741522)Termination phase: Saturation
% 13.42/2.30 % (741522)Time elapsed: 0.728 s
% 13.42/2.30 % (741522)Peak memory usage: 14 MB
% 13.42/2.30 % (741522)Instructions burned: 875 (million)
% 13.42/2.30 % (741655)Instruction limit reached!
% 13.42/2.30 % (741655)------------------------------
% 13.42/2.30 % (741655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.42/2.30 % (741655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.42/2.30 % (741655)CaDiCaL version: 2.1.3
% 13.42/2.30 % (741655)Termination reason: Instruction limit
% 13.42/2.30 % (741655)Termination phase: Saturation
% 13.42/2.30 % (741655)Time elapsed: 0.123 s
% 13.42/2.30 % (741655)Peak memory usage: 12 MB
% 13.42/2.30 % (741655)Instructions burned: 137 (million)
% 13.42/2.30 % (741651)Instruction limit reached!
% 13.42/2.30 % (741651)------------------------------
% 13.42/2.30 % (741651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.42/2.30 % (741651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.42/2.30 % (741651)CaDiCaL version: 2.1.3
% 13.42/2.30 % (741651)Termination reason: Instruction limit
% 13.42/2.30 % (741651)Termination phase: Saturation
% 13.42/2.30 % (741651)Time elapsed: 0.157 s
% 13.42/2.30 % (741651)Peak memory usage: 14 MB
% 13.42/2.30 % (741651)Instructions burned: 340 (million)
% 13.42/2.30 % (741678)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=1133833049:i=116:ep=RSTC:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/116Mi)
% 13.42/2.30 % (741679)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=2410615929:i=575:rtra=on_2983 on theBenchmark for (2983ds/575Mi)
% 13.42/2.30 % (741681)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=927274882:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2983 on theBenchmark for (2983ds/270Mi)
% 13.42/2.30 % (741664)Instruction limit reached!
% 13.42/2.30 % (741664)------------------------------
% 13.42/2.30 % (741664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.42/2.30 % (741664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.42/2.30 % (741664)CaDiCaL version: 2.1.3
% 13.42/2.30 % (741664)Termination reason: Instruction limit
% 14.42/2.30 % (741664)Termination phase: Saturation
% 14.42/2.30 % (741664)Time elapsed: 0.143 s
% 14.42/2.30 % (741664)Peak memory usage: 12 MB
% 14.42/2.30 % (741664)Instructions burned: 227 (million)
% 14.42/2.30 % (741686)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=2804490910: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_2983 on theBenchmark for (2983ds/9840Mi)
% 14.42/2.30 % (741678)Instruction limit reached!
% 14.42/2.30 % (741678)------------------------------
% 14.42/2.30 % (741678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.42/2.30 % (741678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.42/2.30 % (741678)CaDiCaL version: 2.1.3
% 14.42/2.30 % (741678)Termination reason: Instruction limit
% 14.42/2.30 % (741678)Termination phase: Saturation
% 14.42/2.30 % (741678)Time elapsed: 0.079 s
% 14.42/2.30 % (741678)Peak memory usage: 12 MB
% 14.42/2.30 % (741678)Instructions burned: 118 (million)
% 14.42/2.30 % (741692)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=3833340321:i=421:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/421Mi)
% 14.42/2.30 % (741681)Instruction limit reached!
% 14.42/2.30 % (741681)------------------------------
% 14.42/2.30 % (741681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.42/2.30 % (741681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.42/2.30 % (741681)CaDiCaL version: 2.1.3
% 14.42/2.30 % (741681)Termination reason: Instruction limit
% 14.42/2.30 % (741681)Termination phase: Saturation
% 14.42/2.30 % (741681)Time elapsed: 0.119 s
% 14.42/2.30 % (741681)Peak memory usage: 13 MB
% 14.42/2.30 % (741681)Instructions burned: 271 (million)
% 14.42/2.30 % (741657)Instruction limit reached!
% 14.42/2.30 % (741657)------------------------------
% 14.42/2.30 % (741657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.42/2.30 % (741657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.42/2.30 % (741657)CaDiCaL version: 2.1.3
% 14.42/2.30 % (741657)Termination reason: Instruction limit
% 14.42/2.30 % (741657)Termination phase: Saturation
% 14.42/2.30 % (741657)Time elapsed: 0.271 s
% 14.42/2.30 % (741657)Peak memory usage: 13 MB
% 14.42/2.30 % (741657)Instructions burned: 341 (million)
% 14.42/2.30 % (741696)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
% 14.42/2.30 % (741696)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=1731288703:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/270Mi)
% 14.42/2.30 % (741699)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2210787119:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/31Mi)
% 14.42/2.30 % (741699)Instruction limit reached!
% 14.42/2.30 % (741699)------------------------------
% 14.42/2.30 % (741699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.42/2.30 % (741699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.42/2.30 % (741699)CaDiCaL version: 2.1.3
% 14.42/2.30 % (741699)Termination reason: Instruction limit
% 14.42/2.30 % (741699)Termination phase: Saturation
% 14.42/2.30 % (741699)Time elapsed: 0.015 s
% 14.42/2.30 % (741699)Peak memory usage: 12 MB
% 14.42/2.30 % (741699)Instructions burned: 32 (million)
% 14.42/2.30 % (741704)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 14.42/2.30 % (741704)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
% 14.42/2.30 % (741704)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=1261525259:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2981 on theBenchmark for (2981ds/1440Mi)
% 14.42/2.30 % (741670)Instruction limit reached!
% 14.42/2.30 % (741670)------------------------------
% 14.42/2.30 % (741670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.42/2.30 % (741670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.42/2.30 % (741670)CaDiCaL version: 2.1.3
% 14.42/2.30 % (741670)Termination reason: Instruction limit
% 14.42/2.30 % (741670)Termination phase: Saturation
% 14.42/2.30 % (741670)Time elapsed: 0.323 s
% 14.42/2.30 % (741670)Peak memory usage: 14 MB
% 14.42/2.30 % (741670)Instructions burned: 373 (million)
% 14.42/2.30 % (741710)dis+10_2_sil=128000:si=on:random_seed=236053623:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2980 on theBenchmark for (2980ds/339Mi)
% 14.42/2.30 % (741696) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-741125-741696"...
% 14.42/2.30 % (741696)...printing done.
% 14.42/2.30 % (741696)Refutation found. Thanks to Tanya!
% 14.42/2.30 % SZS status Theorem for theBenchmark
% 14.42/2.30 % SZS output start Proof for theBenchmark
% 14.42/2.30 thf(type_def_5, type, a: $tType).
% 14.42/2.30 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 14.42/2.30 thf(func_def_3, type, sK0: ((a > $o) > a)).
% 14.42/2.30 thf(func_def_4, type, sK1: (a > a > $o)).
% 14.42/2.30 thf(func_def_5, type, sK2: (a > a)).
% 14.42/2.30 thf(func_def_6, type, sK3: (a > (a > $o) > a)).
% 14.42/2.30 thf(func_def_7, type, sF4: (a > a > $o)).
% 14.42/2.30 thf(func_def_8, type, sF5: (a > a)).
% 14.42/2.30 thf(func_def_9, type, sF6: (a > a > $o)).
% 14.42/2.30 thf(func_def_10, type, sF7: (a > $o)).
% 14.42/2.30 thf(func_def_11, type, sF8: (a > $o)).
% 14.42/2.30 thf(func_def_12, type, sF9: (a > (a > $o) > $o)).
% 14.42/2.30 thf(func_def_13, type, sF10: ((a > $o) > a)).
% 14.42/2.30 thf(func_def_14, type, sF11: ((a > $o) > a > $o)).
% 14.42/2.30 thf(func_def_15, type, sF12: (a > (a > $o) > $o)).
% 14.42/2.30 thf(func_def_16, type, sF13: ((a > $o) > a > a)).
% 14.42/2.30 thf(func_def_17, type, sF14: (a > (a > $o) > $o)).
% 14.42/2.30 thf(func_def_18, type, sF15: (a > (a > $o) > $o)).
% 14.42/2.30 thf(func_def_19, type, vNOT: ($o > $o)).
% 14.42/2.30 thf(func_def_20, type, db0: !>[X0: $tType]:(X0)).
% 14.42/2.30 thf(func_def_21, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 14.42/2.30 thf(f1,conjecture,(
% 14.42/2.30 ! [X1 : ((a > $o) > a),X0 : (a > a > $o)] : ((! [X2 : a,X4 : a,X3 : a] : (((X0 @ X2 @ X3) & (X0 @ X3 @ X4)) => (X0 @ X2 @ X4)) & ! [X5 : (a > $o)] : (! [X4 : a] : ((X5 @ X4) => (X0 @ X4 @ (X1 @ X5))) & ! [X6 : a] : (! [X7 : a] : (((X5 @ X7) & (X5 @ X7)) => (X0 @ X7 @ X6)) => ((X0 @ (X1 @ X5) @ X6) & (X0 @ (X1 @ X5) @ X6))))) => ! [X8 : (a > a)] : (! [X3 : a,X2 : a] : ((X0 @ X2 @ X3) => (X0 @ (X8 @ X2) @ (X8 @ X3))) => ? [X9 : a] : ((X0 @ (X8 @ X9) @ X9) & (X0 @ X9 @ (X8 @ X9)))))),
% 14.42/2.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM145_C_pme)).
% 14.42/2.30 thf(f2,negated_conjecture,(
% 14.42/2.30 ~ ! [X1 : ((a > $o) > a),X0 : (a > a > $o)] : ((! [X2 : a,X4 : a,X3 : a] : (((X0 @ X2 @ X3) & (X0 @ X3 @ X4)) => (X0 @ X2 @ X4)) & ! [X5 : (a > $o)] : (! [X4 : a] : ((X5 @ X4) => (X0 @ X4 @ (X1 @ X5))) & ! [X6 : a] : (! [X7 : a] : (((X5 @ X7) & (X5 @ X7)) => (X0 @ X7 @ X6)) => ((X0 @ (X1 @ X5) @ X6) & (X0 @ (X1 @ X5) @ X6))))) => ! [X8 : (a > a)] : (! [X3 : a,X2 : a] : ((X0 @ X2 @ X3) => (X0 @ (X8 @ X2) @ (X8 @ X3))) => ? [X9 : a] : ((X0 @ (X8 @ X9) @ X9) & (X0 @ X9 @ (X8 @ X9)))))),
% 14.42/2.30 inference(negated_conjecture,[status(cth)],[f1])).
% 14.42/2.30 thf(f3,plain,(
% 14.42/2.30 ~ ! [X0 : ((a > $o) > a),X1 : (a > a > $o)] : ((! [X2 : a,X3 : a,X4 : a] : (((X1 @ X2 @ X4) & (X1 @ X4 @ X3)) => (X1 @ X2 @ X3)) & ! [X5 : (a > $o)] : (! [X6 : a] : ((X5 @ X6) => (X1 @ X6 @ (X0 @ X5))) & ! [X7 : a] : (! [X8 : a] : (((X5 @ X8) & (X5 @ X8)) => (X1 @ X8 @ X7)) => ((X1 @ (X0 @ X5) @ X7) & (X1 @ (X0 @ X5) @ X7))))) => ! [X9 : (a > a)] : (! [X10 : a,X11 : a] : ((X1 @ X11 @ X10) => (X1 @ (X9 @ X11) @ (X9 @ X10))) => ? [X12 : a] : ((X1 @ (X9 @ X12) @ X12) & (X1 @ X12 @ (X9 @ X12)))))),
% 14.42/2.30 inference(rectify,[],[f2])).
% 14.42/2.30 thf(f4,plain,(
% 14.42/2.30 ~ ! [X1 : (a > a > $o),X0 : ((a > $o) > a)] : ((! [X5 : (a > $o)] : (! [X7 : a] : (! [X8 : a] : (((((X5 @ X8)) = $true) & (((X5 @ X8)) = $true)) => (((X1 @ X8 @ X7)) = $true)) => ((((X1 @ (X0 @ X5) @ X7)) = $true) & (((X1 @ (X0 @ X5) @ X7)) = $true))) & ! [X6 : a] : ((((X5 @ X6)) = $true) => (((X1 @ X6 @ (X0 @ X5))) = $true))) & ! [X4 : a,X2 : a,X3 : a] : ((($true = ((X1 @ X2 @ X4))) & (((X1 @ X4 @ X3)) = $true)) => (((X1 @ X2 @ X3)) = $true))) => ! [X9 : (a > a)] : (! [X11 : a,X10 : a] : ((((X1 @ X11 @ X10)) = $true) => (((X1 @ (X9 @ X11) @ (X9 @ X10))) = $true)) => ? [X12 : a] : ((((X1 @ (X9 @ X12) @ X12)) = $true) & (((X1 @ X12 @ (X9 @ X12))) = $true))))),
% 14.42/2.30 inference(fool_elimination,[],[f3])).
% 14.42/2.30 thf(f5,plain,(
% 14.42/2.30 ? [X1 : (a > a > $o),X0 : ((a > $o) > a)] : (? [X9 : (a > a)] : (! [X10 : a,X11 : a] : ((((X1 @ X11 @ X10)) != $true) | (((X1 @ (X9 @ X11) @ (X9 @ X10))) = $true)) & ! [X12 : a] : ((((X1 @ (X9 @ X12) @ X12)) != $true) | (((X1 @ X12 @ (X9 @ X12))) != $true))) & (! [X5 : (a > $o)] : (! [X7 : a] : (((((X1 @ (X0 @ X5) @ X7)) = $true) & (((X1 @ (X0 @ X5) @ X7)) = $true)) | ? [X8 : a] : ((((X1 @ X8 @ X7)) != $true) & ((((X5 @ X8)) = $true) & (((X5 @ X8)) = $true)))) & ! [X6 : a] : ((((X5 @ X6)) != $true) | (((X1 @ X6 @ (X0 @ X5))) = $true))) & ! [X4 : a,X2 : a,X3 : a] : ((((X1 @ X2 @ X3)) = $true) | (($true != ((X1 @ X2 @ X4))) | (((X1 @ X4 @ X3)) != $true)))))),
% 14.42/2.30 inference(ennf_transformation,[],[f4])).
% 14.42/2.30 thf(f6,plain,(
% 14.42/2.30 ? [X0 : ((a > $o) > a),X1 : (a > a > $o)] : (? [X9 : (a > a)] : (! [X10 : a,X11 : a] : ((((X1 @ X11 @ X10)) != $true) | (((X1 @ (X9 @ X11) @ (X9 @ X10))) = $true)) & ! [X12 : a] : ((((X1 @ (X9 @ X12) @ X12)) != $true) | (((X1 @ X12 @ (X9 @ X12))) != $true))) & ! [X2 : a,X3 : a,X4 : a] : ((((X1 @ X2 @ X3)) = $true) | ($true != ((X1 @ X2 @ X4))) | (((X1 @ X4 @ X3)) != $true)) & ! [X5 : (a > $o)] : (! [X6 : a] : ((((X5 @ X6)) != $true) | (((X1 @ X6 @ (X0 @ X5))) = $true)) & ! [X7 : a] : (((((X1 @ (X0 @ X5) @ X7)) = $true) & (((X1 @ (X0 @ X5) @ X7)) = $true)) | ? [X8 : a] : ((((X5 @ X8)) = $true) & (((X5 @ X8)) = $true) & (((X1 @ X8 @ X7)) != $true)))))),
% 14.42/2.30 inference(flattening,[],[f5])).
% 14.42/2.30 thf(f7,plain,(
% 14.42/2.30 ? [X0 : ((a > $o) > a),X1 : (a > a > $o)] : (? [X2 : (a > a)] : (! [X3 : a,X4 : a] : ((((X1 @ X4 @ X3)) != $true) | (((X1 @ (X2 @ X4) @ (X2 @ X3))) = $true)) & ! [X5 : a] : ((((X1 @ (X2 @ X5) @ X5)) != $true) | (((X1 @ X5 @ (X2 @ X5))) != $true))) & ! [X6 : a,X7 : a,X8 : a] : ((((X1 @ X6 @ X7)) = $true) | (((X1 @ X6 @ X8)) != $true) | (((X1 @ X8 @ X7)) != $true)) & ! [X9 : (a > $o)] : (! [X10 : a] : ((((X9 @ X10)) != $true) | (((X1 @ X10 @ (X0 @ X9))) = $true)) & ! [X11 : a] : (((((X1 @ (X0 @ X9) @ X11)) = $true) & (((X1 @ (X0 @ X9) @ X11)) = $true)) | ? [X12 : a] : ((((X9 @ X12)) = $true) & (((X9 @ X12)) = $true) & (((X1 @ X12 @ X11)) != $true)))))),
% 14.42/2.30 inference(rectify,[],[f6])).
% 14.42/2.30 thf(f8,plain,(
% 14.42/2.30 (! [X3 : a,X4 : a] : ((((sK1 @ X4 @ X3)) != $true) | (((sK1 @ (sK2 @ X4) @ (sK2 @ X3))) = $true)) & ! [X5 : a] : ((((sK1 @ (sK2 @ X5) @ X5)) != $true) | (((sK1 @ X5 @ (sK2 @ X5))) != $true))) & ! [X6 : a,X7 : a,X8 : a] : (($true = ((sK1 @ X6 @ X7))) | (((sK1 @ X6 @ X8)) != $true) | (((sK1 @ X8 @ X7)) != $true)) & ! [X9 : (a > $o)] : (! [X10 : a] : ((((X9 @ X10)) != $true) | (((sK1 @ X10 @ (sK0 @ X9))) = $true)) & ! [X11 : a] : (((((sK1 @ (sK0 @ X9) @ X11)) = $true) & (((sK1 @ (sK0 @ X9) @ X11)) = $true)) | ((((X9 @ (sK3 @ X11 @ X9))) = $true) & (((X9 @ (sK3 @ X11 @ X9))) = $true) & ($true != ((sK1 @ (sK3 @ X11 @ X9) @ X11))))))),
% 14.42/2.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,vAPP]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X12,sK3 @ X11 @ X9)],[f7])).
% 14.42/2.30 thf(f9,plain,(
% 14.42/2.30 ( ! [X11 : a,X9 : (a > $o)] : ((((sK1 @ (sK0 @ X9) @ X11)) = $true) | ($true != ((sK1 @ (sK3 @ X11 @ X9) @ X11)))) )),
% 14.42/2.30 inference(cnf_transformation,[],[f8])).
% 14.42/2.30 thf(f10,plain,(
% 14.42/2.30 ( ! [X11 : a,X9 : (a > $o)] : ((((sK1 @ (sK0 @ X9) @ X11)) = $true) | (((X9 @ (sK3 @ X11 @ X9))) = $true)) )),
% 14.42/2.30 inference(cnf_transformation,[],[f8])).
% 14.42/2.30 thf(f15,plain,(
% 14.42/2.30 ( ! [X10 : a,X9 : (a > $o)] : ((((X9 @ X10)) != $true) | (((sK1 @ X10 @ (sK0 @ X9))) = $true)) )),
% 14.42/2.30 inference(cnf_transformation,[],[f8])).
% 14.42/2.30 thf(f16,plain,(
% 14.42/2.30 ( ! [X8 : a,X6 : a,X7 : a] : (($true = ((sK1 @ X6 @ X7))) | (((sK1 @ X6 @ X8)) != $true) | (((sK1 @ X8 @ X7)) != $true)) )),
% 14.42/2.30 inference(cnf_transformation,[],[f8])).
% 14.42/2.30 thf(f17,plain,(
% 14.42/2.30 ( ! [X5 : a] : ((((sK1 @ (sK2 @ X5) @ X5)) != $true) | (((sK1 @ X5 @ (sK2 @ X5))) != $true)) )),
% 14.42/2.30 inference(cnf_transformation,[],[f8])).
% 14.42/2.30 thf(f18,plain,(
% 14.42/2.30 ( ! [X3 : a,X4 : a] : ((((sK1 @ X4 @ X3)) != $true) | (((sK1 @ (sK2 @ X4) @ (sK2 @ X3))) = $true)) )),
% 14.42/2.30 inference(cnf_transformation,[],[f8])).
% 14.42/2.30 thf(f21,definition,(
% 14.42/2.30 ( ! [X3 : a,X4 : a] : ((((sF4 @ X3 @ X4)) = ((sK1 @ X4 @ X3)))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 14.42/2.30 thf(f22,definition,(
% 14.42/2.30 ( ! [X4 : a] : ((((sF5 @ X4)) = ((sK2 @ X4)))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 14.42/2.30 thf(f23,definition,(
% 14.42/2.30 ( ! [X3 : a,X4 : a] : ((((sF6 @ X3 @ X4)) = ((sK1 @ (sF5 @ X4) @ (sF5 @ X3))))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 14.42/2.30 thf(f24,plain,(
% 14.42/2.30 ( ! [X3 : a,X4 : a] : ((((sF4 @ X3 @ X4)) != $true) | (((sF6 @ X3 @ X4)) = $true)) )),
% 14.42/2.30 inference(definition_folding,[],[f18,f23,f22,f22,f21])).
% 14.42/2.30 thf(f25,definition,(
% 14.42/2.30 ( ! [X5 : a] : ((((sF7 @ X5)) = ((sK1 @ (sF5 @ X5) @ X5)))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 14.42/2.30 thf(f26,plain,(
% 14.42/2.30 ( ! [X5 : a] : ((((sK1 @ (sF5 @ X5) @ X5)) = ((sF7 @ X5)))) )),
% 14.42/2.30 inference(reorient_equations,[],[f25])).
% 14.42/2.30 thf(f27,definition,(
% 14.42/2.30 ( ! [X5 : a] : ((((sF8 @ X5)) = ((sK1 @ X5 @ (sF5 @ X5))))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 14.42/2.30 thf(f28,plain,(
% 14.42/2.30 ( ! [X5 : a] : ((((sF8 @ X5)) != $true) | (((sF7 @ X5)) != $true)) )),
% 14.42/2.30 inference(definition_folding,[],[f17,f27,f22,f26,f22])).
% 14.42/2.30 thf(f29,plain,(
% 14.42/2.30 ( ! [X8 : a,X6 : a,X7 : a] : ((((sF4 @ X8 @ X6)) != $true) | (((sF4 @ X7 @ X6)) = $true) | (((sF4 @ X7 @ X8)) != $true)) )),
% 14.42/2.30 inference(definition_folding,[],[f16,f21,f21,f21])).
% 14.42/2.30 thf(f30,definition,(
% 14.42/2.30 ( ! [X10 : a,X9 : (a > $o)] : ((((sF9 @ X10 @ X9)) = ((X9 @ X10)))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 14.42/2.30 thf(f31,definition,(
% 14.42/2.30 ( ! [X9 : (a > $o)] : ((((sF10 @ X9)) = ((sK0 @ X9)))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 14.42/2.30 thf(f32,definition,(
% 14.42/2.30 ( ! [X10 : a,X9 : (a > $o)] : ((((sF11 @ X9 @ X10)) = ((sK1 @ X10 @ (sF10 @ X9))))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 14.42/2.30 thf(f33,plain,(
% 14.42/2.30 ( ! [X10 : a,X9 : (a > $o)] : ((((sF9 @ X10 @ X9)) != $true) | (((sF11 @ X9 @ X10)) = $true)) )),
% 14.42/2.30 inference(definition_folding,[],[f15,f32,f31,f30])).
% 14.42/2.30 thf(f34,definition,(
% 14.42/2.30 ( ! [X11 : a,X9 : (a > $o)] : ((((sF12 @ X11 @ X9)) = ((sK1 @ (sF10 @ X9) @ X11)))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 14.42/2.30 thf(f35,plain,(
% 14.42/2.30 ( ! [X11 : a,X9 : (a > $o)] : ((((sK1 @ (sF10 @ X9) @ X11)) = ((sF12 @ X11 @ X9)))) )),
% 14.42/2.30 inference(reorient_equations,[],[f34])).
% 14.42/2.30 thf(f36,definition,(
% 14.42/2.30 ( ! [X11 : a,X9 : (a > $o)] : ((((sF13 @ X9 @ X11)) = ((sK3 @ X11 @ X9)))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 14.42/2.30 thf(f37,definition,(
% 14.42/2.30 ( ! [X11 : a,X9 : (a > $o)] : ((((sF14 @ X11 @ X9)) = ((X9 @ (sF13 @ X9 @ X11))))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 14.42/2.30 thf(f40,definition,(
% 14.42/2.30 ( ! [X11 : a,X9 : (a > $o)] : ((((sF15 @ X11 @ X9)) = ((sK1 @ (sF13 @ X9 @ X11) @ X11)))) )),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 14.42/2.30 thf(f43,plain,(
% 14.42/2.30 ( ! [X11 : a,X9 : (a > $o)] : ((((sF12 @ X11 @ X9)) = $true) | (((sF14 @ X11 @ X9)) = $true)) )),
% 14.42/2.30 inference(definition_folding,[],[f10,f37,f36,f35,f31])).
% 14.42/2.30 thf(f44,plain,(
% 14.42/2.30 ( ! [X11 : a,X9 : (a > $o)] : ((((sF15 @ X11 @ X9)) != $true) | (((sF12 @ X11 @ X9)) = $true)) )),
% 14.42/2.30 inference(definition_folding,[],[f9,f40,f36,f35,f31])).
% 14.42/2.30 thf(f60,plain,(
% 14.42/2.30 ( ! [X0 : a,X1 : a] : ((((sK1 @ X0 @ X1)) != $true) | (((sF6 @ X1 @ X0)) = $true)) )),
% 14.42/2.30 inference(superposition,[],[f24,f21])).
% 14.42/2.30 thf(f62,plain,(
% 14.42/2.30 ( ! [X0 : a] : ((((sF8 @ X0)) != $true) | (((sF6 @ (sF5 @ X0) @ X0)) = $true)) )),
% 14.42/2.30 inference(superposition,[],[f60,f27])).
% 14.42/2.30 thf(f64,plain,(
% 14.42/2.30 ( ! [X0 : a] : ((((sF6 @ (sF5 @ X0) @ X0)) = ((sF8 @ (sF5 @ X0))))) )),
% 14.42/2.30 inference(superposition,[],[f23,f27])).
% 14.42/2.30 thf(f70,plain,(
% 14.42/2.30 ( ! [X0 : a,X1 : a] : ((((sF4 @ (sF5 @ X0) @ (sF5 @ X1))) = ((sF6 @ X0 @ X1)))) )),
% 14.42/2.30 inference(superposition,[],[f21,f23])).
% 14.42/2.30 thf(f73,plain,(
% 14.42/2.30 ( ! [X0 : (a > $o)] : ((((sF11 @ X0 @ (sF5 @ (sF10 @ X0)))) = ((sF7 @ (sF10 @ X0))))) )),
% 14.42/2.30 inference(superposition,[],[f26,f32])).
% 14.42/2.30 thf(f74,plain,(
% 14.42/2.30 ( ! [X0 : (a > $o),X1 : a] : ((((sF11 @ X0 @ X1)) != $true) | (((sF6 @ (sF10 @ X0) @ X1)) = $true)) )),
% 14.42/2.30 inference(superposition,[],[f60,f32])).
% 14.42/2.30 thf(f86,plain,(
% 14.42/2.30 ( ! [X0 : (a > $o),X1 : a] : ((((X0 @ X1)) != $true) | (((sF11 @ X0 @ X1)) = $true)) )),
% 14.42/2.30 inference(superposition,[],[f33,f30])).
% 14.42/2.30 thf(f118,plain,(
% 14.42/2.30 ( ! [X0 : (a > $o)] : ((((sF8 @ (sF10 @ X0))) = ((sF12 @ (sF5 @ (sF10 @ X0)) @ X0)))) )),
% 14.42/2.30 inference(superposition,[],[f27,f35])).
% 14.42/2.30 thf(f128,plain,(
% 14.42/2.30 ( ! [X0 : a] : ((((sF14 @ X0 @ sF8)) != $true) | (((sF6 @ (sF5 @ (sF13 @ sF8 @ X0)) @ (sF13 @ sF8 @ X0))) = $true)) )),
% 14.42/2.30 inference(superposition,[],[f62,f37])).
% 14.42/2.30 thf(f143,plain,(
% 14.42/2.30 ( ! [X0 : a] : ((((sF14 @ X0 @ sF8)) != $true) | (((sF8 @ (sF5 @ (sF13 @ sF8 @ X0)))) = $true)) )),
% 14.42/2.30 inference(forward_demodulation,[],[f128,f64])).
% 14.42/2.30 thf(f201,plain,(
% 14.42/2.30 ( ! [X2 : a,X0 : a,X1 : a] : ((((sF4 @ X2 @ X1)) != $true) | (((sF4 @ X2 @ X0)) = $true) | (((sK1 @ X0 @ X1)) != $true)) )),
% 14.42/2.30 inference(superposition,[],[f29,f21])).
% 14.42/2.30 thf(f375,plain,(
% 14.42/2.30 ( ! [X0 : (a > $o)] : ((((sF14 @ (sF5 @ (sF10 @ X0)) @ X0)) = $true) | (((sF8 @ (sF10 @ X0))) = $true)) )),
% 14.42/2.30 inference(superposition,[],[f43,f118])).
% 14.42/2.30 thf(f497,plain,(
% 14.42/2.30 ( ! [X0 : a,X1 : (a > $o)] : ((((sF4 @ X0 @ (sF13 @ X1 @ X0))) = ((sF15 @ X0 @ X1)))) )),
% 14.42/2.30 inference(superposition,[],[f21,f40])).
% 14.42/2.30 thf(f607,plain,(
% 14.42/2.30 ( ! [X2 : a,X0 : a,X1 : a] : ((((sK1 @ X2 @ X0)) != $true) | (((sK1 @ X0 @ X1)) != $true) | (((sF4 @ X1 @ X2)) = $true)) )),
% 14.42/2.30 inference(superposition,[],[f201,f21])).
% 14.42/2.30 thf(f695,plain,(
% 14.42/2.30 ( ! [X0 : a,X1 : a] : ((((sK1 @ (sF5 @ X0) @ X1)) != $true) | (((sF8 @ X0)) != $true) | (((sF4 @ X1 @ X0)) = $true)) )),
% 14.42/2.30 inference(superposition,[],[f607,f27])).
% 14.42/2.30 thf(f704,plain,(
% 14.42/2.30 ( ! [X0 : a,X1 : a] : ((((sF6 @ X0 @ X1)) != $true) | (((sF8 @ X1)) != $true) | (((sF4 @ (sF5 @ X0) @ X1)) = $true)) )),
% 14.42/2.30 inference(superposition,[],[f695,f23])).
% 14.42/2.30 thf(f1154,plain,(
% 14.42/2.30 ($true != $true) | (((sF8 @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) = $true) | (((sF8 @ (sF10 @ sF8))) = $true)),
% 14.42/2.30 inference(superposition,[],[f143,f375])).
% 14.42/2.30 thf(f1155,plain,(
% 14.42/2.30 (((sF8 @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) = $true) | (((sF8 @ (sF10 @ sF8))) = $true)),
% 14.42/2.30 inference(trivial_inequality_removal,[],[f1154])).
% 14.42/2.30 thf(f1157,definition,(
% 14.42/2.30 spl16_8 <=> (((sF8 @ (sF10 @ sF8))) = $true)),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[spl16_8])],[avatar_definition])).
% 14.42/2.30 thf(f1158,plain,(
% 14.42/2.30 (((sF8 @ (sF10 @ sF8))) != $true) | spl16_8),
% 14.42/2.30 inference(avatar_component_clause,[],[f1157])).
% 14.42/2.30 thf(f1159,plain,(
% 14.42/2.30 (((sF8 @ (sF10 @ sF8))) = $true) | ~spl16_8),
% 14.42/2.30 inference(avatar_component_clause,[],[f1157])).
% 14.42/2.30 thf(f1161,definition,(
% 14.42/2.30 spl16_9 <=> (((sF8 @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) = $true)),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[spl16_9])],[avatar_definition])).
% 14.42/2.30 thf(f1163,plain,(
% 14.42/2.30 (((sF8 @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) = $true) | ~spl16_9),
% 14.42/2.30 inference(avatar_component_clause,[],[f1161])).
% 14.42/2.30 thf(f1164,plain,(
% 14.42/2.30 spl16_8 | spl16_9),
% 14.42/2.30 inference(avatar_split_clause,[],[f1155,f1161,f1157])).
% 14.42/2.30 thf(f1168,plain,(
% 14.42/2.30 ($true != $true) | (((sF6 @ (sF5 @ (sF10 @ sF8)) @ (sF10 @ sF8))) = $true) | ~spl16_8),
% 14.42/2.30 inference(superposition,[],[f62,f1159])).
% 14.42/2.30 thf(f1169,plain,(
% 14.42/2.30 ($true != $true) | (((sF7 @ (sF10 @ sF8))) != $true) | ~spl16_8),
% 14.42/2.30 inference(superposition,[],[f28,f1159])).
% 14.42/2.30 thf(f1173,plain,(
% 14.42/2.30 (((sF7 @ (sF10 @ sF8))) != $true) | ~spl16_8),
% 14.42/2.30 inference(trivial_inequality_removal,[],[f1169])).
% 14.42/2.30 thf(f1177,plain,(
% 14.42/2.30 (((sF6 @ (sF5 @ (sF10 @ sF8)) @ (sF10 @ sF8))) = $true) | ~spl16_8),
% 14.42/2.30 inference(trivial_inequality_removal,[],[f1168])).
% 14.42/2.30 thf(f1180,plain,(
% 14.42/2.30 (((sF8 @ (sF5 @ (sF10 @ sF8)))) = $true) | ~spl16_8),
% 14.42/2.30 inference(forward_demodulation,[],[f1177,f64])).
% 14.42/2.30 thf(f1201,plain,(
% 14.42/2.30 (((sF11 @ sF8 @ (sF5 @ (sF10 @ sF8)))) = $true) | ($true != $true) | ~spl16_8),
% 14.42/2.30 inference(superposition,[],[f86,f1180])).
% 14.42/2.30 thf(f1211,plain,(
% 14.42/2.30 (((sF11 @ sF8 @ (sF5 @ (sF10 @ sF8)))) = $true) | ~spl16_8),
% 14.42/2.30 inference(trivial_inequality_removal,[],[f1201])).
% 14.42/2.30 thf(f1215,plain,(
% 14.42/2.30 (((sF7 @ (sF10 @ sF8))) = $true) | ~spl16_8),
% 14.42/2.30 inference(forward_demodulation,[],[f1211,f73])).
% 14.42/2.30 thf(f1217,plain,(
% 14.42/2.30 $false | ~spl16_8),
% 14.42/2.30 inference(forward_subsumption_resolution,[],[f1215,f1173])).
% 14.42/2.30 thf(f1218,plain,(
% 14.42/2.30 ~spl16_8),
% 14.42/2.30 inference(avatar_contradiction_clause,[],[f1217])).
% 14.42/2.30 thf(f1228,plain,(
% 14.42/2.30 ($true != $true) | (((sF11 @ sF8 @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) = $true) | ~spl16_9),
% 14.42/2.30 inference(superposition,[],[f86,f1163])).
% 14.42/2.30 thf(f1238,plain,(
% 14.42/2.30 (((sF11 @ sF8 @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) = $true) | ~spl16_9),
% 14.42/2.30 inference(trivial_inequality_removal,[],[f1228])).
% 14.42/2.30 thf(f1247,definition,(
% 14.42/2.30 spl16_13 <=> (((sF14 @ (sF5 @ (sF10 @ sF8)) @ sF8)) = $true)),
% 14.42/2.30 introduced(definition,[new_symbols(definition,[spl16_13])],[avatar_definition])).
% 14.42/2.30 thf(f1248,plain,(
% 14.42/2.30 (((sF14 @ (sF5 @ (sF10 @ sF8)) @ sF8)) = $true) | ~spl16_13),
% 14.42/2.30 inference(avatar_component_clause,[],[f1247])).
% 14.42/2.30 thf(f1249,plain,(
% 14.42/2.30 (((sF14 @ (sF5 @ (sF10 @ sF8)) @ sF8)) != $true) | spl16_13),
% 14.42/2.30 inference(avatar_component_clause,[],[f1247])).
% 14.42/2.30 thf(f1251,plain,(
% 14.42/2.30 ($true != $true) | (((sF8 @ (sF10 @ sF8))) = $true) | spl16_13),
% 14.42/2.30 inference(superposition,[],[f1249,f375])).
% 14.42/2.30 thf(f1252,plain,(
% 14.42/2.30 (((sF8 @ (sF10 @ sF8))) = $true) | spl16_13),
% 14.42/2.30 inference(trivial_inequality_removal,[],[f1251])).
% 14.42/2.30 thf(f1253,plain,(
% 14.42/2.30 $false | (spl16_8 | spl16_13)),
% 14.42/2.30 inference(forward_subsumption_resolution,[],[f1252,f1158])).
% 14.42/2.30 thf(f1254,plain,(
% 14.42/2.30 spl16_8 | spl16_13),
% 14.42/2.30 inference(avatar_contradiction_clause,[],[f1253])).
% 14.42/2.30 thf(f1882,plain,(
% 14.42/2.30 ($true != $true) | (((sF6 @ (sF10 @ sF8) @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) = $true) | ~spl16_9),
% 14.42/2.30 inference(superposition,[],[f74,f1238])).
% 14.42/2.30 thf(f1885,plain,(
% 14.42/2.30 (((sF6 @ (sF10 @ sF8) @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) = $true) | ~spl16_9),
% 14.42/2.30 inference(trivial_inequality_removal,[],[f1882])).
% 14.42/2.30 thf(f2446,plain,(
% 14.42/2.30 (((sF8 @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) != $true) | (((sF4 @ (sF5 @ (sF10 @ sF8)) @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) = $true) | ($true != $true) | ~spl16_9),
% 14.42/2.30 inference(superposition,[],[f704,f1885])).
% 14.42/2.30 thf(f2454,plain,(
% 14.42/2.30 (((sF4 @ (sF5 @ (sF10 @ sF8)) @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) = $true) | (((sF8 @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) != $true) | ~spl16_9),
% 14.42/2.30 inference(trivial_inequality_removal,[],[f2446])).
% 14.42/2.30 thf(f2456,plain,(
% 14.42/2.30 (((sF4 @ (sF5 @ (sF10 @ sF8)) @ (sF5 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8)))))) = $true) | ~spl16_9),
% 14.42/2.30 inference(forward_subsumption_resolution,[],[f2454,f1163])).
% 14.42/2.30 thf(f2458,plain,(
% 14.42/2.30 (((sF6 @ (sF10 @ sF8) @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8))))) = $true) | ~spl16_9),
% 14.42/2.30 inference(forward_demodulation,[],[f2456,f70])).
% 14.42/2.30 thf(f2459,plain,(
% 14.42/2.30 ($true != $true) | (((sF4 @ (sF5 @ (sF10 @ sF8)) @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8))))) = $true) | (((sF8 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8))))) != $true) | ~spl16_9),
% 14.42/2.30 inference(superposition,[],[f704,f2458])).
% 14.42/2.30 thf(f2464,plain,(
% 14.42/2.30 (((sF8 @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8))))) != $true) | (((sF4 @ (sF5 @ (sF10 @ sF8)) @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8))))) = $true) | ~spl16_9),
% 14.42/2.30 inference(trivial_inequality_removal,[],[f2459])).
% 14.42/2.30 thf(f2469,plain,(
% 14.42/2.30 (((sF4 @ (sF5 @ (sF10 @ sF8)) @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8))))) = $true) | (((sF14 @ (sF5 @ (sF10 @ sF8)) @ sF8)) != $true) | ~spl16_9),
% 14.42/2.30 inference(forward_demodulation,[],[f2464,f37])).
% 14.42/2.30 thf(f2471,plain,(
% 14.42/2.30 (((sF4 @ (sF5 @ (sF10 @ sF8)) @ (sF13 @ sF8 @ (sF5 @ (sF10 @ sF8))))) = $true) | (~spl16_9 | ~spl16_13)),
% 14.42/2.30 inference(forward_subsumption_resolution,[],[f2469,f1248])).
% 14.42/2.30 thf(f2472,plain,(
% 14.42/2.30 (((sF15 @ (sF5 @ (sF10 @ sF8)) @ sF8)) = $true) | (~spl16_9 | ~spl16_13)),
% 14.42/2.30 inference(forward_demodulation,[],[f2471,f497])).
% 14.42/2.30 thf(f2473,plain,(
% 14.42/2.30 ($true != $true) | (((sF12 @ (sF5 @ (sF10 @ sF8)) @ sF8)) = $true) | (~spl16_9 | ~spl16_13)),
% 14.42/2.30 inference(superposition,[],[f44,f2472])).
% 14.42/2.30 thf(f2474,plain,(
% 14.42/2.30 (((sF12 @ (sF5 @ (sF10 @ sF8)) @ sF8)) = $true) | (~spl16_9 | ~spl16_13)),
% 14.42/2.30 inference(trivial_inequality_removal,[],[f2473])).
% 14.42/2.30 thf(f2475,plain,(
% 14.42/2.30 (((sF8 @ (sF10 @ sF8))) = $true) | (~spl16_9 | ~spl16_13)),
% 14.42/2.30 inference(forward_demodulation,[],[f2474,f118])).
% 14.42/2.30 thf(f2476,plain,(
% 14.42/2.30 $false | (spl16_8 | ~spl16_9 | ~spl16_13)),
% 14.42/2.30 inference(forward_subsumption_resolution,[],[f2475,f1158])).
% 14.42/2.30 thf(f2477,plain,(
% 14.42/2.30 spl16_8 | ~spl16_9 | ~spl16_13),
% 14.42/2.30 inference(avatar_contradiction_clause,[],[f2476])).
% 14.42/2.30 cnf(s5, plain, spl16_8 | spl16_9, inference(sat_conversion,[],[f1164])).
% 14.42/2.30 cnf(s7, plain, ~spl16_8, inference(sat_conversion,[],[f1218])).
% 14.42/2.30 cnf(s9, plain, spl16_8 | spl16_13, inference(sat_conversion,[],[f1254])).
% 14.42/2.30 cnf(s15, plain, spl16_8 | ~spl16_9 | ~spl16_13, inference(sat_conversion,[],[f2477])).
% 14.42/2.30 cnf(s16, plain, spl16_13, inference(rat,[],[s9,s7])).
% 14.42/2.30 cnf(s17, plain, ~spl16_9, inference(rat,[],[s15,s7,s16])).
% 14.42/2.30 cnf(s18, plain, $false, inference(rat,[],[s5,s17,s7])).
% 14.42/2.30 thf(f2478,plain,(
% 14.42/2.30 $false),
% 14.42/2.30 inference(avatar_sat_refutation,[],[s18])).
% 14.42/2.30 % SZS output end Proof for theBenchmark
% 14.42/2.30 % (741696)------------------------------
% 14.42/2.30 % (741696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.42/2.30 % (741696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.42/2.30 % (741696)CaDiCaL version: 2.1.3
% 14.42/2.30 % (741696)Termination reason: Refutation
% 14.42/2.30 % (741696)Time elapsed: 0.215 s
% 14.42/2.30 % (741696)Peak memory usage: 14 MB
% 14.42/2.30 % (741696)Instructions burned: 246 (million)
% 14.42/2.30 % (741125)Success in time 2.039 s
% 14.42/2.30 % Vampire exiting
%------------------------------------------------------------------------------