%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP096^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:08:19 AM UTC 2026
% Result : ContradictoryAxioms 9.51s 1.92s
% Output : Refutation 9.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP096^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n002.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 19:55:37 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.22/0.27 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.41 % (1765275)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.64/0.41 % (1765284)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1933270036:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.64/0.41 % (1765286)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.64/0.41 % (1765286)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.64/0.41 % (1765284)Instruction limit reached!
% 0.64/0.41 % (1765284)------------------------------
% 0.64/0.41 % (1765284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.41 % (1765284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.41 % (1765284)CaDiCaL version: 2.1.3
% 0.64/0.41 % (1765284)Termination reason: Instruction limit
% 0.64/0.41 % (1765284)Termination phase: Preprocessing 3
% 0.64/0.41 % (1765284)Time elapsed: 0.006 s
% 0.64/0.41 % (1765284)Peak memory usage: 11 MB
% 0.64/0.41 % (1765284)Instructions burned: 27 (million)
% 0.64/0.41 % (1765280)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=662365669:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.64/0.41 % (1765281)lrs+10_16_si=on:nwc=1.5:random_seed=3282729412:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.64/0.41 % (1765282)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=506748740:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.64/0.41 % (1765283)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=1641489979:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.64/0.41 % (1765285)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3897618528:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.64/0.41 % (1765286)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=713624674:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.64/0.41 % (1765282)Instruction limit reached!
% 0.64/0.41 % (1765282)------------------------------
% 0.64/0.41 % (1765282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.41 % (1765282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.41 % (1765282)CaDiCaL version: 2.1.3
% 0.64/0.41 % (1765282)Termination reason: Instruction limit
% 0.64/0.41 % (1765282)Termination phase: shuffling
% 0.64/0.41 % (1765282)Time elapsed: 0.003 s
% 0.64/0.41 % (1765282)Peak memory usage: 10 MB
% 0.64/0.41 % (1765282)Instructions burned: 6 (million)
% 0.64/0.41 % (1765288)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2527355049:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.64/0.41 % (1765281)Instruction limit reached!
% 0.64/0.41 % (1765281)------------------------------
% 0.64/0.41 % (1765281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.41 % (1765281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.41 % (1765281)CaDiCaL version: 2.1.3
% 0.64/0.41 % (1765281)Termination reason: Instruction limit
% 0.64/0.41 % (1765281)Termination phase: Property scanning
% 0.64/0.41 % (1765281)Time elapsed: 0.013 s
% 0.64/0.41 % (1765281)Peak memory usage: 10 MB
% 0.64/0.41 % (1765281)Instructions burned: 20 (million)
% 0.64/0.41 % (1765288)Instruction limit reached!
% 0.64/0.41 % (1765288)------------------------------
% 0.64/0.41 % (1765288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.41 % (1765288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.41 % (1765288)CaDiCaL version: 2.1.3
% 0.64/0.41 % (1765288)Termination reason: Instruction limit
% 0.64/0.41 % (1765288)Termination phase: shuffling
% 0.64/0.41 % (1765288)Time elapsed: 0.003 s
% 0.64/0.41 % (1765288)Peak memory usage: 10 MB
% 0.64/0.41 % (1765288)Instructions burned: 13 (million)
% 0.64/0.41 % (1765297)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.64/0.42 % (1765295)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3839939224:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.64/0.42 % (1765297)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=855265581:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.64/0.42 % (1765295)Instruction limit reached!
% 0.64/0.42 % (1765295)------------------------------
% 0.64/0.42 % (1765295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.42 % (1765295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.42 % (1765295)CaDiCaL version: 2.1.3
% 0.64/0.42 % (1765295)Termination reason: Instruction limit
% 0.64/0.42 % (1765295)Termination phase: shuffling
% 0.64/0.42 % (1765295)Time elapsed: 0.003 s
% 0.64/0.42 % (1765295)Peak memory usage: 10 MB
% 0.64/0.42 % (1765295)Instructions burned: 7 (million)
% 0.64/0.42 % (1765297)Instruction limit reached!
% 0.64/0.42 % (1765297)------------------------------
% 0.64/0.42 % (1765297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.42 % (1765297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.42 % (1765297)CaDiCaL version: 2.1.3
% 0.64/0.42 % (1765297)Termination reason: Instruction limit
% 0.64/0.42 % (1765297)Termination phase: shuffling
% 0.64/0.42 % (1765297)Time elapsed: 0.002 s
% 0.64/0.42 % (1765297)Peak memory usage: 10 MB
% 0.64/0.42 % (1765297)Instructions burned: 11 (million)
% 0.64/0.42 % (1765285)Instruction limit reached!
% 0.64/0.42 % (1765285)------------------------------
% 0.64/0.42 % (1765285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.42 % (1765285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.42 % (1765285)CaDiCaL version: 2.1.3
% 0.64/0.42 % (1765285)Termination reason: Instruction limit
% 0.64/0.42 % (1765285)Termination phase: Saturation
% 0.64/0.42 % (1765285)Time elapsed: 0.033 s
% 0.64/0.42 % (1765285)Peak memory usage: 12 MB
% 0.64/0.42 % (1765285)Instructions burned: 75 (million)
% 0.64/0.42 % (1765280)Instruction limit reached!
% 0.64/0.42 % (1765280)------------------------------
% 0.64/0.42 % (1765280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.42 % (1765280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.42 % (1765280)CaDiCaL version: 2.1.3
% 0.64/0.42 % (1765280)Termination reason: Instruction limit
% 0.64/0.42 % (1765280)Termination phase: Saturation
% 0.64/0.42 % (1765280)Time elapsed: 0.039 s
% 0.64/0.42 % (1765280)Peak memory usage: 13 MB
% 0.64/0.42 % (1765280)Instructions burned: 87 (million)
% 0.64/0.42 % (1765302)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=862730981:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.64/0.42 % (1765301)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.64/0.42 % (1765301)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.64/0.42 % (1765298)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2245428392:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.64/0.42 % (1765301)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=551818587:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.64/0.42 % (1765298)Instruction limit reached!
% 0.64/0.42 % (1765298)------------------------------
% 0.64/0.42 % (1765298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.42 % (1765298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.42 % (1765298)CaDiCaL version: 2.1.3
% 0.64/0.42 % (1765298)Termination reason: Instruction limit
% 0.64/0.42 % (1765298)Termination phase: shuffling
% 0.64/0.42 % (1765298)Time elapsed: 0.006 s
% 0.64/0.42 % (1765298)Peak memory usage: 10 MB
% 0.64/0.42 % (1765298)Instructions burned: 12 (million)
% 0.64/0.42 % (1765303)lrs+10_1_si=on:cs=on:random_seed=2462032102:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.64/0.42 % (1765304)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.64/0.45 % (1765301)Instruction limit reached!
% 0.64/0.45 % (1765301)------------------------------
% 0.64/0.45 % (1765301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.45 % (1765301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.45 % (1765301)CaDiCaL version: 2.1.3
% 0.64/0.45 % (1765301)Termination reason: Instruction limit
% 0.64/0.45 % (1765301)Termination phase: Property scanning
% 0.64/0.45 % (1765301)Time elapsed: 0.013 s
% 0.64/0.45 % (1765301)Peak memory usage: 10 MB
% 0.64/0.45 % (1765301)Instructions burned: 29 (million)
% 0.64/0.45 % (1765304)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=4012592068:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.64/0.45 % (1765303)Instruction limit reached!
% 0.64/0.45 % (1765303)------------------------------
% 0.64/0.45 % (1765303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.45 % (1765303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.45 % (1765303)CaDiCaL version: 2.1.3
% 0.64/0.45 % (1765303)Termination reason: Instruction limit
% 0.64/0.45 % (1765303)Termination phase: shuffling
% 0.64/0.45 % (1765303)Time elapsed: 0.007 s
% 0.64/0.45 % (1765303)Peak memory usage: 10 MB
% 0.64/0.45 % (1765303)Instructions burned: 8 (million)
% 0.64/0.45 % (1765304)Instruction limit reached!
% 0.64/0.45 % (1765304)------------------------------
% 0.64/0.45 % (1765304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.45 % (1765304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.45 % (1765304)CaDiCaL version: 2.1.3
% 0.64/0.45 % (1765304)Termination reason: Instruction limit
% 0.64/0.45 % (1765304)Termination phase: shuffling
% 0.64/0.45 % (1765304)Time elapsed: 0.002 s
% 0.64/0.45 % (1765304)Peak memory usage: 10 MB
% 0.64/0.45 % (1765304)Instructions burned: 4 (million)
% 0.64/0.45 % (1765308)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2156607158:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.64/0.45 % (1765302)Instruction limit reached!
% 0.64/0.45 % (1765302)------------------------------
% 0.64/0.45 % (1765302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.45 % (1765302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.45 % (1765302)CaDiCaL version: 2.1.3
% 0.64/0.45 % (1765302)Termination reason: Instruction limit
% 0.64/0.45 % (1765302)Termination phase: Property scanning
% 0.64/0.45 % (1765302)Time elapsed: 0.027 s
% 0.64/0.45 % (1765302)Peak memory usage: 11 MB
% 0.64/0.45 % (1765302)Instructions burned: 91 (million)
% 0.64/0.45 % (1765286)Instruction limit reached!
% 0.64/0.45 % (1765286)------------------------------
% 0.64/0.45 % (1765286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.45 % (1765286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.45 % (1765286)CaDiCaL version: 2.1.3
% 0.64/0.45 % (1765286)Termination reason: Instruction limit
% 0.64/0.45 % (1765286)Termination phase: Saturation
% 0.64/0.45 % (1765286)Time elapsed: 0.075 s
% 0.64/0.45 % (1765286)Peak memory usage: 13 MB
% 0.64/0.45 % (1765286)Instructions burned: 159 (million)
% 0.64/0.45 % (1765311)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1689634308:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.64/0.45 % (1765315)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3548897831:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.64/0.45 % (1765312)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=620867184:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.64/0.45 % (1765313)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=190923945:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.64/0.45 % (1765308)Refutation not found, incomplete strategy
% 0.64/0.45 % (1765308)------------------------------
% 0.64/0.45 % (1765308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.45 % (1765308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.49 % (1765308)CaDiCaL version: 2.1.3
% 0.64/0.49 % (1765308)Termination reason: Refutation not found, incomplete strategy
% 0.64/0.49 % (1765308)Time elapsed: 0.012 s
% 0.64/0.49 % (1765308)Peak memory usage: 12 MB
% 0.64/0.49 % (1765308)Instructions burned: 26 (million)
% 0.64/0.49 % (1765308)------------------------------
% 0.64/0.49 % (1765308)------------------------------
% 0.64/0.49 % (1765315)Refutation not found, incomplete strategy
% 0.64/0.49 % (1765315)------------------------------
% 0.64/0.49 % (1765315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.49 % (1765315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.49 % (1765315)CaDiCaL version: 2.1.3
% 0.64/0.49 % (1765315)Termination reason: Refutation not found, incomplete strategy
% 0.64/0.49 % (1765315)Time elapsed: 0.008 s
% 0.64/0.49 % (1765315)Peak memory usage: 12 MB
% 0.64/0.49 % (1765315)Instructions burned: 35 (million)
% 0.64/0.49 % (1765313)Instruction limit reached!
% 0.64/0.49 % (1765313)------------------------------
% 0.64/0.49 % (1765313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.49 % (1765313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.49 % (1765313)CaDiCaL version: 2.1.3
% 0.64/0.49 % (1765313)Termination reason: Instruction limit
% 0.64/0.49 % (1765313)Termination phase: Property scanning
% 0.64/0.49 % (1765313)Time elapsed: 0.007 s
% 0.64/0.49 % (1765313)Peak memory usage: 10 MB
% 0.64/0.49 % (1765313)Instructions burned: 15 (million)
% 0.64/0.49 % (1765315)------------------------------
% 0.64/0.49 % (1765315)------------------------------
% 0.64/0.49 % (1765311)Refutation not found, incomplete strategy
% 0.64/0.49 % (1765311)------------------------------
% 0.64/0.49 % (1765311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.49 % (1765311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.49 % (1765311)CaDiCaL version: 2.1.3
% 0.64/0.49 % (1765311)Termination reason: Refutation not found, incomplete strategy
% 0.64/0.49 % (1765311)Time elapsed: 0.014 s
% 0.64/0.49 % (1765311)Peak memory usage: 12 MB
% 0.64/0.49 % (1765311)Instructions burned: 31 (million)
% 0.64/0.49 % (1765312)Instruction limit reached!
% 0.64/0.49 % (1765312)------------------------------
% 0.64/0.49 % (1765312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.49 % (1765312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.49 % (1765312)CaDiCaL version: 2.1.3
% 0.64/0.49 % (1765312)Termination reason: Instruction limit
% 0.64/0.49 % (1765312)Termination phase: SInE selection
% 0.64/0.49 % (1765312)Time elapsed: 0.012 s
% 0.64/0.49 % (1765312)Peak memory usage: 10 MB
% 0.64/0.49 % (1765312)Instructions burned: 26 (million)
% 0.64/0.49 % (1765311)------------------------------
% 0.64/0.49 % (1765311)------------------------------
% 0.64/0.49 % (1765317)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3376827082:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.64/0.49 % (1765323)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=4210705042:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.64/0.49 % (1765321)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3086127275: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)
% 0.64/0.49 % (1765321)Instruction limit reached!
% 0.64/0.49 % (1765321)------------------------------
% 0.64/0.49 % (1765321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.49 % (1765321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.49 % (1765321)CaDiCaL version: 2.1.3
% 0.64/0.49 % (1765321)Termination reason: Instruction limit
% 0.64/0.49 % (1765321)Termination phase: shuffling
% 0.64/0.49 % (1765321)Time elapsed: 0.001 s
% 0.64/0.49 % (1765321)Peak memory usage: 10 MB
% 0.64/0.49 % (1765321)Instructions burned: 2 (million)
% 0.64/0.49 % (1765317)Instruction limit reached!
% 0.64/0.49 % (1765317)------------------------------
% 0.64/0.49 % (1765317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.49 % (1765317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.49 % (1765317)CaDiCaL version: 2.1.3
% 0.64/0.49 % (1765317)Termination reason: Instruction limit
% 0.64/0.49 % (1765317)Termination phase: Property scanning
% 0.64/0.49 % (1765317)Time elapsed: 0.007 s
% 1.47/0.54 % (1765317)Peak memory usage: 10 MB
% 1.47/0.54 % (1765317)Instructions burned: 15 (million)
% 1.47/0.54 % (1765323)Instruction limit reached!
% 1.47/0.54 % (1765323)------------------------------
% 1.47/0.54 % (1765323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.54 % (1765323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.54 % (1765323)CaDiCaL version: 2.1.3
% 1.47/0.54 % (1765323)Termination reason: Instruction limit
% 1.47/0.54 % (1765323)Termination phase: Property scanning
% 1.47/0.54 % (1765323)Time elapsed: 0.006 s
% 1.47/0.54 % (1765323)Peak memory usage: 10 MB
% 1.47/0.54 % (1765323)Instructions burned: 25 (million)
% 1.47/0.54 % (1765322)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=88754404:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.47/0.54 % (1765325)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.47/0.54 % (1765325)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.47/0.54 % (1765324)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1264196989:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.47/0.54 % (1765325)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=1302360520:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.47/0.54 % (1765330)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=749696804:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.47/0.54 % (1765322)Instruction limit reached!
% 1.47/0.54 % (1765322)------------------------------
% 1.47/0.54 % (1765322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.54 % (1765322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.54 % (1765322)CaDiCaL version: 2.1.3
% 1.47/0.54 % (1765322)Termination reason: Instruction limit
% 1.47/0.54 % (1765322)Termination phase: shuffling
% 1.47/0.54 % (1765322)Time elapsed: 0.012 s
% 1.47/0.54 % (1765322)Peak memory usage: 10 MB
% 1.47/0.54 % (1765322)Instructions burned: 26 (million)
% 1.47/0.54 % (1765325)Instruction limit reached!
% 1.47/0.54 % (1765325)------------------------------
% 1.47/0.54 % (1765325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.54 % (1765325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.54 % (1765325)CaDiCaL version: 2.1.3
% 1.47/0.54 % (1765325)Termination reason: Instruction limit
% 1.47/0.54 % (1765325)Termination phase: shuffling
% 1.47/0.54 % (1765325)Time elapsed: 0.006 s
% 1.47/0.54 % (1765325)Peak memory usage: 10 MB
% 1.47/0.54 % (1765325)Instructions burned: 14 (million)
% 1.47/0.54 % (1765329)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.47/0.54 % (1765330)Instruction limit reached!
% 1.47/0.54 % (1765330)------------------------------
% 1.47/0.54 % (1765330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.54 % (1765330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.47/0.54 % (1765330)CaDiCaL version: 2.1.3
% 1.47/0.54 % (1765330)Termination reason: Instruction limit
% 1.47/0.54 % (1765330)Termination phase: Property scanning
% 1.47/0.54 % (1765330)Time elapsed: 0.008 s
% 1.47/0.54 % (1765330)Peak memory usage: 10 MB
% 1.47/0.54 % (1765330)Instructions burned: 34 (million)
% 1.47/0.54 % (1765332)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=4087546308:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.47/0.54 % (1765329)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=3369501403:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.47/0.54 % (1765332)Instruction limit reached!
% 1.47/0.54 % (1765332)------------------------------
% 1.47/0.54 % (1765332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.47/0.54 % (1765332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.60 % (1765332)CaDiCaL version: 2.1.3
% 2.15/0.60 % (1765332)Termination reason: Instruction limit
% 2.15/0.60 % (1765332)Termination phase: shuffling
% 2.15/0.60 % (1765332)Time elapsed: 0.004 s
% 2.15/0.60 % (1765332)Peak memory usage: 10 MB
% 2.15/0.60 % (1765332)Instructions burned: 9 (million)
% 2.15/0.60 % (1765329)Instruction limit reached!
% 2.15/0.60 % (1765329)------------------------------
% 2.15/0.60 % (1765329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.60 % (1765329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.60 % (1765329)CaDiCaL version: 2.1.3
% 2.15/0.60 % (1765329)Termination reason: Instruction limit
% 2.15/0.60 % (1765329)Termination phase: shuffling
% 2.15/0.60 % (1765329)Time elapsed: 0.004 s
% 2.15/0.60 % (1765329)Peak memory usage: 10 MB
% 2.15/0.60 % (1765329)Instructions burned: 8 (million)
% 2.15/0.60 % (1765339)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3087399422:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.15/0.60 % (1765337)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2448164599:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.15/0.60 % (1765324)Instruction limit reached!
% 2.15/0.60 % (1765324)------------------------------
% 2.15/0.60 % (1765324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.60 % (1765324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.60 % (1765324)CaDiCaL version: 2.1.3
% 2.15/0.60 % (1765324)Termination reason: Instruction limit
% 2.15/0.60 % (1765324)Termination phase: Property scanning
% 2.15/0.60 % (1765324)Time elapsed: 0.027 s
% 2.15/0.60 % (1765324)Peak memory usage: 11 MB
% 2.15/0.60 % (1765324)Instructions burned: 61 (million)
% 2.15/0.60 % (1765341)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1033900879:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.15/0.60 % (1765337)Instruction limit reached!
% 2.15/0.60 % (1765337)------------------------------
% 2.15/0.60 % (1765337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.60 % (1765337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.60 % (1765337)CaDiCaL version: 2.1.3
% 2.15/0.60 % (1765337)Termination reason: Instruction limit
% 2.15/0.60 % (1765337)Termination phase: Property scanning
% 2.15/0.60 % (1765337)Time elapsed: 0.010 s
% 2.15/0.60 % (1765337)Peak memory usage: 10 MB
% 2.15/0.60 % (1765337)Instructions burned: 22 (million)
% 2.15/0.60 % (1765342)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1226524578:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.15/0.60 % (1765336)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=477763930:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.15/0.60 % (1765345)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4138094048:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 2.15/0.60 % (1765348)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.15/0.60 % (1765342)Refutation not found, incomplete strategy
% 2.15/0.60 % (1765342)------------------------------
% 2.15/0.60 % (1765342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.60 % (1765342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.60 % (1765342)CaDiCaL version: 2.1.3
% 2.15/0.60 % (1765342)Termination reason: Refutation not found, incomplete strategy
% 2.15/0.60 % (1765342)Time elapsed: 0.016 s
% 2.15/0.60 % (1765342)Peak memory usage: 12 MB
% 2.15/0.60 % (1765342)Instructions burned: 35 (million)
% 2.15/0.60 % (1765342)------------------------------
% 2.15/0.60 % (1765342)------------------------------
% 2.15/0.60 % (1765348)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=714082405:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 2.15/0.60 % (1765348)Instruction limit reached!
% 2.15/0.60 % (1765348)------------------------------
% 2.15/0.60 % (1765348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.60 % (1765348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.69 % (1765348)CaDiCaL version: 2.1.3
% 2.41/0.69 % (1765348)Termination reason: Instruction limit
% 2.41/0.69 % (1765348)Termination phase: shuffling
% 2.41/0.69 % (1765348)Time elapsed: 0.003 s
% 2.41/0.69 % (1765348)Peak memory usage: 10 MB
% 2.41/0.69 % (1765348)Instructions burned: 7 (million)
% 2.41/0.69 % (1765336)Instruction limit reached!
% 2.41/0.69 % (1765336)------------------------------
% 2.41/0.69 % (1765336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.41/0.69 % (1765336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.69 % (1765336)CaDiCaL version: 2.1.3
% 2.41/0.69 % (1765336)Termination reason: Instruction limit
% 2.41/0.69 % (1765336)Termination phase: shuffling
% 2.41/0.69 % (1765336)Time elapsed: 0.018 s
% 2.41/0.69 % (1765336)Peak memory usage: 10 MB
% 2.41/0.69 % (1765336)Instructions burned: 23 (million)
% 2.41/0.69 % (1765345)Instruction limit reached!
% 2.41/0.69 % (1765345)------------------------------
% 2.41/0.69 % (1765345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.41/0.69 % (1765345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.69 % (1765345)CaDiCaL version: 2.1.3
% 2.41/0.69 % (1765345)Termination reason: Instruction limit
% 2.41/0.69 % (1765345)Termination phase: Property scanning
% 2.41/0.69 % (1765345)Time elapsed: 0.019 s
% 2.41/0.69 % (1765345)Peak memory usage: 11 MB
% 2.41/0.69 % (1765345)Instructions burned: 45 (million)
% 2.41/0.69 % (1765352)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1819328097:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.41/0.69 % (1765354)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.41/0.69 % (1765354)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3719523078:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.41/0.69 % (1765353)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=1672033690:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.41/0.69 % (1765352)Refutation not found, incomplete strategy
% 2.41/0.69 % (1765352)------------------------------
% 2.41/0.69 % (1765352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.41/0.69 % (1765352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.69 % (1765352)CaDiCaL version: 2.1.3
% 2.41/0.69 % (1765352)Termination reason: Refutation not found, incomplete strategy
% 2.41/0.69 % (1765352)Time elapsed: 0.014 s
% 2.41/0.69 % (1765352)Peak memory usage: 12 MB
% 2.41/0.69 % (1765352)Instructions burned: 30 (million)
% 2.41/0.69 % (1765354)Instruction limit reached!
% 2.41/0.69 % (1765354)------------------------------
% 2.41/0.69 % (1765354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.41/0.69 % (1765354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.69 % (1765354)CaDiCaL version: 2.1.3
% 2.41/0.69 % (1765354)Termination reason: Instruction limit
% 2.41/0.69 % (1765354)Termination phase: shuffling
% 2.41/0.69 % (1765354)Time elapsed: 0.003 s
% 2.41/0.69 % (1765354)Peak memory usage: 10 MB
% 2.41/0.69 % (1765354)Instructions burned: 6 (million)
% 2.41/0.69 % (1765352)------------------------------
% 2.41/0.69 % (1765352)------------------------------
% 2.41/0.69 % (1765355)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2645341834:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.41/0.69 % (1765353)Refutation not found, incomplete strategy
% 2.41/0.69 % (1765353)------------------------------
% 2.41/0.69 % (1765353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.41/0.69 % (1765353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.69 % (1765353)CaDiCaL version: 2.1.3
% 2.41/0.69 % (1765353)Termination reason: Refutation not found, incomplete strategy
% 2.41/0.69 % (1765353)Time elapsed: 0.014 s
% 2.41/0.69 % (1765353)Peak memory usage: 12 MB
% 2.41/0.69 % (1765353)Instructions burned: 31 (million)
% 2.41/0.69 % (1765353)------------------------------
% 2.41/0.69 % (1765353)------------------------------
% 2.41/0.69 % (1765355)Instruction limit reached!
% 2.41/0.69 % (1765355)------------------------------
% 2.41/0.69 % (1765355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.88/0.75 % (1765355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/0.75 % (1765355)CaDiCaL version: 2.1.3
% 2.88/0.75 % (1765355)Termination reason: Instruction limit
% 2.88/0.75 % (1765355)Termination phase: Property scanning
% 2.88/0.75 % (1765355)Time elapsed: 0.010 s
% 2.88/0.75 % (1765355)Peak memory usage: 10 MB
% 2.88/0.75 % (1765355)Instructions burned: 24 (million)
% 2.88/0.75 % (1765359)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1970343460:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.88/0.75 % (1765360)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=3049872211:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.88/0.75 % (1765359)Instruction limit reached!
% 2.88/0.75 % (1765359)------------------------------
% 2.88/0.75 % (1765359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.88/0.75 % (1765359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/0.75 % (1765359)CaDiCaL version: 2.1.3
% 2.88/0.75 % (1765359)Termination reason: Instruction limit
% 2.88/0.75 % (1765359)Termination phase: shuffling
% 2.88/0.75 % (1765359)Time elapsed: 0.009 s
% 2.88/0.75 % (1765359)Peak memory usage: 10 MB
% 2.88/0.75 % (1765359)Instructions burned: 20 (million)
% 2.88/0.75 % (1765341)Instruction limit reached!
% 2.88/0.75 % (1765341)------------------------------
% 2.88/0.75 % (1765341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.88/0.75 % (1765341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/0.75 % (1765341)CaDiCaL version: 2.1.3
% 2.88/0.75 % (1765341)Termination reason: Instruction limit
% 2.88/0.75 % (1765341)Termination phase: Saturation
% 2.88/0.75 % (1765341)Time elapsed: 0.083 s
% 2.88/0.75 % (1765341)Peak memory usage: 14 MB
% 2.88/0.75 % (1765341)Instructions burned: 144 (million)
% 2.88/0.75 % (1765362)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=2778620541:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 2.88/0.75 % (1765363)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=137508716:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 2.88/0.75 % (1765366)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=172449072:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 2.88/0.75 % (1765367)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=482918748:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2997 on theBenchmark for (2997ds/21Mi)
% 2.88/0.75 % (1765363)Instruction limit reached!
% 2.88/0.75 % (1765363)------------------------------
% 2.88/0.75 % (1765363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.88/0.75 % (1765363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/0.75 % (1765363)CaDiCaL version: 2.1.3
% 2.88/0.75 % (1765363)Termination reason: Instruction limit
% 2.88/0.75 % (1765363)Termination phase: SInE selection
% 2.88/0.75 % (1765363)Time elapsed: 0.020 s
% 2.88/0.75 % (1765363)Peak memory usage: 10 MB
% 2.88/0.75 % (1765363)Instructions burned: 45 (million)
% 2.88/0.75 % (1765367)Instruction limit reached!
% 2.88/0.75 % (1765367)------------------------------
% 2.88/0.75 % (1765367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.88/0.75 % (1765367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/0.75 % (1765367)CaDiCaL version: 2.1.3
% 2.88/0.75 % (1765367)Termination reason: Instruction limit
% 2.88/0.75 % (1765367)Termination phase: Property scanning
% 2.88/0.75 % (1765367)Time elapsed: 0.010 s
% 2.88/0.75 % (1765367)Peak memory usage: 10 MB
% 2.88/0.75 % (1765367)Instructions burned: 22 (million)
% 2.88/0.75 % (1765372)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.88/0.75 % (1765372)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3467184669:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/200Mi)
% 2.88/0.80 % (1765373)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=85553665:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 2.88/0.80 % (1765373)Instruction limit reached!
% 2.88/0.80 % (1765373)------------------------------
% 2.88/0.80 % (1765373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.88/0.80 % (1765373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/0.80 % (1765373)CaDiCaL version: 2.1.3
% 2.88/0.80 % (1765373)Termination reason: Instruction limit
% 2.88/0.80 % (1765373)Termination phase: Property scanning
% 2.88/0.80 % (1765373)Time elapsed: 0.007 s
% 2.88/0.80 % (1765373)Peak memory usage: 10 MB
% 2.88/0.80 % (1765373)Instructions burned: 15 (million)
% 2.88/0.80 % (1765376)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=2870992239:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 2.88/0.80 % (1765366)Refutation not found, incomplete strategy
% 2.88/0.80 % (1765366)------------------------------
% 2.88/0.80 % (1765366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.88/0.80 % (1765366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/0.80 % (1765366)CaDiCaL version: 2.1.3
% 2.88/0.80 % (1765366)Termination reason: Refutation not found, incomplete strategy
% 2.88/0.80 % (1765366)Time elapsed: 0.080 s
% 2.88/0.80 % (1765366)Peak memory usage: 13 MB
% 2.88/0.80 % (1765366)Instructions burned: 92 (million)
% 2.88/0.80 % (1765366)------------------------------
% 2.88/0.80 % (1765366)------------------------------
% 2.88/0.80 % (1765376)Instruction limit reached!
% 2.88/0.80 % (1765376)------------------------------
% 2.88/0.80 % (1765376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.88/0.80 % (1765376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/0.80 % (1765376)CaDiCaL version: 2.1.3
% 2.88/0.80 % (1765376)Termination reason: Instruction limit
% 2.88/0.80 % (1765376)Termination phase: Property scanning
% 2.88/0.80 % (1765376)Time elapsed: 0.029 s
% 2.88/0.80 % (1765376)Peak memory usage: 11 MB
% 2.88/0.80 % (1765376)Instructions burned: 66 (million)
% 2.88/0.80 % (1765283)Instruction limit reached!
% 2.88/0.80 % (1765283)------------------------------
% 2.88/0.80 % (1765283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.88/0.80 % (1765283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/0.80 % (1765283)CaDiCaL version: 2.1.3
% 2.88/0.80 % (1765283)Termination reason: Instruction limit
% 2.88/0.80 % (1765283)Termination phase: Saturation
% 2.88/0.80 % (1765283)Time elapsed: 0.338 s
% 2.88/0.80 % (1765283)Peak memory usage: 16 MB
% 2.88/0.80 % (1765283)Instructions burned: 635 (million)
% 2.88/0.80 % (1765378)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=769676943:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 2.88/0.80 % (1765379)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1103809453:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 2.88/0.80 % (1765380)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1359285062:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2996 on theBenchmark for (2996ds/137Mi)
% 2.88/0.80 % (1765379)Instruction limit reached!
% 2.88/0.80 % (1765379)------------------------------
% 2.88/0.80 % (1765379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.88/0.80 % (1765379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/0.80 % (1765379)CaDiCaL version: 2.1.3
% 2.88/0.80 % (1765379)Termination reason: Instruction limit
% 2.88/0.80 % (1765379)Termination phase: Property scanning
% 2.88/0.80 % (1765379)Time elapsed: 0.014 s
% 2.88/0.80 % (1765379)Peak memory usage: 11 MB
% 2.88/0.80 % (1765379)Instructions burned: 32 (million)
% 2.88/0.80 % (1765372)Instruction limit reached!
% 2.88/0.80 % (1765372)------------------------------
% 2.88/0.80 % (1765372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.88/0.80 % (1765372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/0.80 % (1765372)CaDiCaL version: 2.1.3
% 2.88/0.80 % (1765372)Termination reason: Instruction limit
% 3.60/0.85 % (1765372)Termination phase: Saturation
% 3.60/0.85 % (1765372)Time elapsed: 0.094 s
% 3.60/0.85 % (1765372)Peak memory usage: 13 MB
% 3.60/0.85 % (1765372)Instructions burned: 202 (million)
% 3.60/0.85 % (1765378)Instruction limit reached!
% 3.60/0.85 % (1765378)------------------------------
% 3.60/0.85 % (1765378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.85 % (1765378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.85 % (1765378)CaDiCaL version: 2.1.3
% 3.60/0.85 % (1765378)Termination reason: Instruction limit
% 3.60/0.85 % (1765378)Termination phase: Property scanning
% 3.60/0.85 % (1765378)Time elapsed: 0.023 s
% 3.60/0.85 % (1765378)Peak memory usage: 11 MB
% 3.60/0.85 % (1765378)Instructions burned: 53 (million)
% 3.60/0.85 % (1765360)Instruction limit reached!
% 3.60/0.85 % (1765360)------------------------------
% 3.60/0.85 % (1765360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.85 % (1765360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.85 % (1765360)CaDiCaL version: 2.1.3
% 3.60/0.85 % (1765360)Termination reason: Instruction limit
% 3.60/0.85 % (1765360)Termination phase: Saturation
% 3.60/0.85 % (1765360)Time elapsed: 0.158 s
% 3.60/0.85 % (1765360)Peak memory usage: 15 MB
% 3.60/0.85 % (1765360)Instructions burned: 316 (million)
% 3.60/0.85 % (1765386)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.60/0.85 % (1765384)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=1584511450:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.60/0.85 % (1765385)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3635328783:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.60/0.85 % (1765386)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2402438842:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 3.60/0.85 % (1765387)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=378131786:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 3.60/0.85 % (1765384)Instruction limit reached!
% 3.60/0.85 % (1765384)------------------------------
% 3.60/0.85 % (1765384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.85 % (1765384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.85 % (1765384)CaDiCaL version: 2.1.3
% 3.60/0.85 % (1765384)Termination reason: Instruction limit
% 3.60/0.85 % (1765384)Termination phase: Property scanning
% 3.60/0.85 % (1765384)Time elapsed: 0.015 s
% 3.60/0.85 % (1765384)Peak memory usage: 10 MB
% 3.60/0.85 % (1765384)Instructions burned: 34 (million)
% 3.60/0.85 % (1765387)Refutation not found, incomplete strategy
% 3.60/0.85 % (1765387)------------------------------
% 3.60/0.85 % (1765387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.85 % (1765387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.85 % (1765387)CaDiCaL version: 2.1.3
% 3.60/0.85 % (1765387)Termination reason: Refutation not found, incomplete strategy
% 3.60/0.85 % (1765387)Time elapsed: 0.014 s
% 3.60/0.85 % (1765387)Peak memory usage: 12 MB
% 3.60/0.85 % (1765387)Instructions burned: 31 (million)
% 3.60/0.85 % (1765387)------------------------------
% 3.60/0.85 % (1765387)------------------------------
% 3.60/0.85 % (1765385)Instruction limit reached!
% 3.60/0.85 % (1765385)------------------------------
% 3.60/0.85 % (1765385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.85 % (1765385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.85 % (1765385)CaDiCaL version: 2.1.3
% 3.60/0.85 % (1765385)Termination reason: Instruction limit
% 3.60/0.85 % (1765385)Termination phase: Saturation
% 3.60/0.85 % (1765385)Time elapsed: 0.030 s
% 3.60/0.85 % (1765385)Peak memory usage: 12 MB
% 3.60/0.85 % (1765385)Instructions burned: 68 (million)
% 3.60/0.85 % (1765392)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3527654361:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 3.60/0.85 % (1765380)Instruction limit reached!
% 3.60/0.85 % (1765380)------------------------------
% 3.60/0.85 % (1765380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.85 % (1765380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/0.90 % (1765380)CaDiCaL version: 2.1.3
% 4.13/0.90 % (1765380)Termination reason: Instruction limit
% 4.13/0.90 % (1765380)Termination phase: Saturation
% 4.13/0.90 % (1765380)Time elapsed: 0.069 s
% 4.13/0.90 % (1765380)Peak memory usage: 13 MB
% 4.13/0.90 % (1765380)Instructions burned: 139 (million)
% 4.13/0.90 % (1765393)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1642850352:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 4.13/0.90 % (1765394)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=4251450207:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 4.13/0.90 % (1765393)Refutation not found, incomplete strategy
% 4.13/0.90 % (1765393)------------------------------
% 4.13/0.90 % (1765393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.13/0.90 % (1765393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/0.90 % (1765393)CaDiCaL version: 2.1.3
% 4.13/0.90 % (1765393)Termination reason: Refutation not found, incomplete strategy
% 4.13/0.90 % (1765393)Time elapsed: 0.013 s
% 4.13/0.90 % (1765393)Peak memory usage: 12 MB
% 4.13/0.90 % (1765393)Instructions burned: 30 (million)
% 4.13/0.90 % (1765396)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=59273950:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/515Mi)
% 4.13/0.90 % (1765393)------------------------------
% 4.13/0.90 % (1765393)------------------------------
% 4.13/0.90 % (1765394)Refutation not found, incomplete strategy
% 4.13/0.90 % (1765394)------------------------------
% 4.13/0.90 % (1765394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.13/0.90 % (1765394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/0.90 % (1765394)CaDiCaL version: 2.1.3
% 4.13/0.90 % (1765394)Termination reason: Refutation not found, incomplete strategy
% 4.13/0.90 % (1765394)Time elapsed: 0.016 s
% 4.13/0.90 % (1765394)Peak memory usage: 12 MB
% 4.13/0.90 % (1765394)Instructions burned: 35 (million)
% 4.13/0.90 % (1765394)------------------------------
% 4.13/0.90 % (1765394)------------------------------
% 4.13/0.90 % (1765396)Refutation not found, incomplete strategy
% 4.13/0.90 % (1765396)------------------------------
% 4.13/0.90 % (1765396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.13/0.90 % (1765396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/0.90 % (1765396)CaDiCaL version: 2.1.3
% 4.13/0.90 % (1765396)Termination reason: Refutation not found, incomplete strategy
% 4.13/0.90 % (1765396)Time elapsed: 0.016 s
% 4.13/0.90 % (1765396)Peak memory usage: 12 MB
% 4.13/0.90 % (1765396)Instructions burned: 35 (million)
% 4.13/0.90 % (1765396)------------------------------
% 4.13/0.90 % (1765396)------------------------------
% 4.13/0.90 % (1765400)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1103929431:st=1.5:i=130:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/130Mi)
% 4.13/0.90 % (1765392)Instruction limit reached!
% 4.13/0.90 % (1765392)------------------------------
% 4.13/0.90 % (1765392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.13/0.90 % (1765392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/0.90 % (1765392)CaDiCaL version: 2.1.3
% 4.13/0.90 % (1765392)Termination reason: Instruction limit
% 4.13/0.90 % (1765392)Termination phase: Saturation
% 4.13/0.90 % (1765392)Time elapsed: 0.044 s
% 4.13/0.90 % (1765392)Peak memory usage: 13 MB
% 4.13/0.90 % (1765392)Instructions burned: 97 (million)
% 4.13/0.90 % (1765386)Instruction limit reached!
% 4.13/0.90 % (1765386)------------------------------
% 4.13/0.90 % (1765386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.13/0.90 % (1765386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/0.90 % (1765386)CaDiCaL version: 2.1.3
% 4.13/0.90 % (1765386)Termination reason: Instruction limit
% 4.13/0.90 % (1765386)Termination phase: Saturation
% 4.13/0.90 % (1765386)Time elapsed: 0.076 s
% 4.13/0.90 % (1765386)Peak memory usage: 13 MB
% 4.13/0.90 % (1765386)Instructions burned: 180 (million)
% 4.13/0.90 % (1765339)Instruction limit reached!
% 4.13/0.90 % (1765339)------------------------------
% 4.13/0.90 % (1765339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.13/0.90 % (1765339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/0.90 % (1765339)CaDiCaL version: 2.1.3
% 4.13/0.90 % (1765339)Termination reason: Instruction limit
% 4.13/0.99 % (1765339)Termination phase: Saturation
% 4.13/0.99 % (1765339)Time elapsed: 0.339 s
% 4.13/0.99 % (1765339)Peak memory usage: 20 MB
% 4.13/0.99 % (1765339)Instructions burned: 1240 (million)
% 4.13/0.99 % (1765401)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2687096470:i=44:ep=R:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/44Mi)
% 4.13/0.99 % (1765402)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=4281296853:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 4.13/0.99 % (1765406)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=340399670:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2994 on theBenchmark for (2994ds/65Mi)
% 4.13/0.99 % (1765404)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=681996474:i=450:rtra=on:ixr=off:ntd=on_2994 on theBenchmark for (2994ds/450Mi)
% 4.13/0.99 % (1765405)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=2657461153:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/95Mi)
% 4.13/0.99 % (1765401)Instruction limit reached!
% 4.13/0.99 % (1765401)------------------------------
% 4.13/0.99 % (1765401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.13/0.99 % (1765401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/0.99 % (1765401)CaDiCaL version: 2.1.3
% 4.13/0.99 % (1765401)Termination reason: Instruction limit
% 4.13/0.99 % (1765401)Termination phase: Property scanning
% 4.13/0.99 % (1765401)Time elapsed: 0.019 s
% 4.13/0.99 % (1765401)Peak memory usage: 10 MB
% 4.13/0.99 % (1765401)Instructions burned: 45 (million)
% 4.13/0.99 % (1765406)Instruction limit reached!
% 4.13/0.99 % (1765406)------------------------------
% 4.13/0.99 % (1765406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.13/0.99 % (1765406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/0.99 % (1765406)CaDiCaL version: 2.1.3
% 4.13/0.99 % (1765406)Termination reason: Instruction limit
% 4.13/0.99 % (1765406)Termination phase: Property scanning
% 4.13/0.99 % (1765406)Time elapsed: 0.015 s
% 4.13/0.99 % (1765406)Peak memory usage: 11 MB
% 4.13/0.99 % (1765406)Instructions burned: 68 (million)
% 4.13/0.99 % (1765413)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=4183090560:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2994 on theBenchmark for (2994ds/5755Mi)
% 4.13/0.99 % (1765412)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=2757183115: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_2994 on theBenchmark for (2994ds/105Mi)
% 4.13/0.99 % (1765413)Refutation not found, incomplete strategy
% 4.13/0.99 % (1765413)------------------------------
% 4.13/0.99 % (1765413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.13/0.99 % (1765413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/0.99 % (1765413)CaDiCaL version: 2.1.3
% 4.13/0.99 % (1765413)Termination reason: Refutation not found, incomplete strategy
% 4.13/0.99 % (1765413)Time elapsed: 0.008 s
% 4.13/0.99 % (1765413)Peak memory usage: 12 MB
% 4.13/0.99 % (1765413)Instructions burned: 35 (million)
% 4.13/0.99 % (1765413)------------------------------
% 4.13/0.99 % (1765413)------------------------------
% 4.13/0.99 % (1765400)Instruction limit reached!
% 4.13/0.99 % (1765400)------------------------------
% 4.13/0.99 % (1765400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.13/0.99 % (1765400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/0.99 % (1765400)CaDiCaL version: 2.1.3
% 4.13/0.99 % (1765400)Termination reason: Instruction limit
% 4.13/0.99 % (1765400)Termination phase: Saturation
% 4.13/0.99 % (1765400)Time elapsed: 0.060 s
% 4.13/0.99 % (1765400)Peak memory usage: 13 MB
% 4.13/0.99 % (1765400)Instructions burned: 130 (million)
% 4.13/0.99 % (1765402)Refutation not found, incomplete strategy
% 4.13/0.99 % (1765402)------------------------------
% 4.13/0.99 % (1765402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.08 % (1765402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.08 % (1765402)CaDiCaL version: 2.1.3
% 5.25/1.08 % (1765402)Termination reason: Refutation not found, incomplete strategy
% 5.25/1.08 % (1765402)Time elapsed: 0.047 s
% 5.25/1.08 % (1765402)Peak memory usage: 13 MB
% 5.25/1.08 % (1765402)Instructions burned: 98 (million)
% 5.25/1.08 % (1765405)Instruction limit reached!
% 5.25/1.08 % (1765405)------------------------------
% 5.25/1.08 % (1765405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.08 % (1765405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.08 % (1765405)CaDiCaL version: 2.1.3
% 5.25/1.08 % (1765405)Termination reason: Instruction limit
% 5.25/1.08 % (1765405)Termination phase: Saturation
% 5.25/1.08 % (1765405)Time elapsed: 0.043 s
% 5.25/1.08 % (1765405)Peak memory usage: 13 MB
% 5.25/1.08 % (1765405)Instructions burned: 96 (million)
% 5.25/1.08 % (1765416)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=2230264252:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/375Mi)
% 5.25/1.08 % (1765402)------------------------------
% 5.25/1.08 % (1765402)------------------------------
% 5.25/1.08 % (1765417)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=581439827:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2994 on theBenchmark for (2994ds/495Mi)
% 5.25/1.08 % (1765419)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=3683122325:cond=on:i=34:hud=10:nm=10:rtra=on_2994 on theBenchmark for (2994ds/34Mi)
% 5.25/1.08 % (1765420)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=671173720:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2994 on theBenchmark for (2994ds/91Mi)
% 5.25/1.08 % (1765416)Refutation not found, incomplete strategy
% 5.25/1.08 % (1765416)------------------------------
% 5.25/1.08 % (1765416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.08 % (1765416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.08 % (1765416)CaDiCaL version: 2.1.3
% 5.25/1.08 % (1765416)Termination reason: Refutation not found, incomplete strategy
% 5.25/1.08 % (1765416)Time elapsed: 0.024 s
% 5.25/1.08 % (1765416)Peak memory usage: 12 MB
% 5.25/1.08 % (1765416)Instructions burned: 31 (million)
% 5.25/1.08 % (1765416)------------------------------
% 5.25/1.08 % (1765416)------------------------------
% 5.25/1.08 % (1765412)Instruction limit reached!
% 5.25/1.08 % (1765412)------------------------------
% 5.25/1.08 % (1765412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.08 % (1765412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.08 % (1765412)CaDiCaL version: 2.1.3
% 5.25/1.08 % (1765412)Termination reason: Instruction limit
% 5.25/1.08 % (1765412)Termination phase: Property scanning
% 5.25/1.08 % (1765412)Time elapsed: 0.044 s
% 5.25/1.08 % (1765412)Peak memory usage: 11 MB
% 5.25/1.08 % (1765412)Instructions burned: 106 (million)
% 5.25/1.08 % (1765419)Instruction limit reached!
% 5.25/1.08 % (1765419)------------------------------
% 5.25/1.08 % (1765419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.08 % (1765419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.08 % (1765419)CaDiCaL version: 2.1.3
% 5.25/1.08 % (1765419)Termination reason: Instruction limit
% 5.25/1.08 % (1765419)Termination phase: Property scanning
% 5.25/1.08 % (1765419)Time elapsed: 0.015 s
% 5.25/1.08 % (1765419)Peak memory usage: 10 MB
% 5.25/1.08 % (1765419)Instructions burned: 34 (million)
% 5.25/1.08 % (1765424)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=1594106215:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2993 on theBenchmark for (2993ds/66Mi)
% 5.25/1.08 % (1765424)Refutation not found, incomplete strategy
% 5.25/1.08 % (1765424)------------------------------
% 5.25/1.08 % (1765424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.08 % (1765424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.08 % (1765424)CaDiCaL version: 2.1.3
% 5.25/1.08 % (1765424)Termination reason: Refutation not found, incomplete strategy
% 5.25/1.08 % (1765424)Time elapsed: 0.006 s
% 5.25/1.08 % (1765424)Peak memory usage: 12 MB
% 5.25/1.08 % (1765424)Instructions burned: 26 (million)
% 5.25/1.08 % (1765424)------------------------------
% 5.71/1.14 % (1765424)------------------------------
% 5.71/1.14 % (1765425)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1660259698:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2993 on theBenchmark for (2993ds/22Mi)
% 5.71/1.14 % (1765426)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=3766611267:i=338:bd=all:ins=4:rtra=on_2993 on theBenchmark for (2993ds/338Mi)
% 5.71/1.14 % (1765428)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2083308606:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2993 on theBenchmark for (2993ds/28Mi)
% 5.71/1.14 % (1765425)Instruction limit reached!
% 5.71/1.14 % (1765425)------------------------------
% 5.71/1.14 % (1765425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.14 % (1765425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.14 % (1765425)CaDiCaL version: 2.1.3
% 5.71/1.14 % (1765425)Termination reason: Instruction limit
% 5.71/1.14 % (1765425)Termination phase: Property scanning
% 5.71/1.14 % (1765425)Time elapsed: 0.010 s
% 5.71/1.14 % (1765425)Peak memory usage: 10 MB
% 5.71/1.14 % (1765425)Instructions burned: 22 (million)
% 5.71/1.14 % (1765420)Instruction limit reached!
% 5.71/1.14 % (1765420)------------------------------
% 5.71/1.14 % (1765420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.14 % (1765420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.14 % (1765420)CaDiCaL version: 2.1.3
% 5.71/1.14 % (1765420)Termination reason: Instruction limit
% 5.71/1.14 % (1765420)Termination phase: Saturation
% 5.71/1.14 % (1765420)Time elapsed: 0.041 s
% 5.71/1.14 % (1765420)Peak memory usage: 13 MB
% 5.71/1.14 % (1765420)Instructions burned: 92 (million)
% 5.71/1.14 % (1765428)Refutation not found, incomplete strategy
% 5.71/1.14 % (1765428)------------------------------
% 5.71/1.14 % (1765428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.14 % (1765428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.14 % (1765428)CaDiCaL version: 2.1.3
% 5.71/1.14 % (1765428)Termination reason: Refutation not found, incomplete strategy
% 5.71/1.14 % (1765428)Time elapsed: 0.007 s
% 5.71/1.14 % (1765428)Peak memory usage: 12 MB
% 5.71/1.14 % (1765428)Instructions burned: 30 (million)
% 5.71/1.14 % (1765428)------------------------------
% 5.71/1.14 % (1765428)------------------------------
% 5.71/1.14 % (1765432)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 5.71/1.14 % (1765434)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=3601818417:i=227:sd=1:bd=all:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/227Mi)
% 5.71/1.14 % (1765432)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3949692779:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2993 on theBenchmark for (2993ds/137Mi)
% 5.71/1.14 % (1765433)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=3389202546:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2993 on theBenchmark for (2993ds/340Mi)
% 5.71/1.14 % (1765434)Refutation not found, incomplete strategy
% 5.71/1.14 % (1765434)------------------------------
% 5.71/1.14 % (1765434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.14 % (1765434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.14 % (1765434)CaDiCaL version: 2.1.3
% 5.71/1.14 % (1765434)Termination reason: Refutation not found, incomplete strategy
% 5.71/1.14 % (1765434)Time elapsed: 0.007 s
% 5.71/1.14 % (1765434)Peak memory usage: 12 MB
% 5.71/1.14 % (1765434)Instructions burned: 30 (million)
% 5.71/1.14 % (1765434)------------------------------
% 5.71/1.14 % (1765434)------------------------------
% 5.71/1.14 % (1765438)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 5.71/1.14 % (1765438)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1744762406:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/373Mi)
% 5.71/1.14 % (1765432)Instruction limit reached!
% 5.71/1.14 % (1765432)------------------------------
% 5.71/1.14 % (1765432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.03/1.20 % (1765432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.20 % (1765432)CaDiCaL version: 2.1.3
% 6.03/1.20 % (1765432)Termination reason: Instruction limit
% 6.03/1.20 % (1765432)Termination phase: Saturation
% 6.03/1.20 % (1765432)Time elapsed: 0.058 s
% 6.03/1.20 % (1765432)Peak memory usage: 13 MB
% 6.03/1.20 % (1765432)Instructions burned: 138 (million)
% 6.03/1.20 % (1765362)Instruction limit reached!
% 6.03/1.20 % (1765362)------------------------------
% 6.03/1.20 % (1765362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.03/1.20 % (1765362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.20 % (1765362)CaDiCaL version: 2.1.3
% 6.03/1.20 % (1765362)Termination reason: Instruction limit
% 6.03/1.20 % (1765362)Termination phase: Saturation
% 6.03/1.20 % (1765362)Time elapsed: 0.437 s
% 6.03/1.20 % (1765362)Peak memory usage: 19 MB
% 6.03/1.20 % (1765362)Instructions burned: 854 (million)
% 6.03/1.20 % (1765440)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=1428896499:i=116:ep=RSTC:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/116Mi)
% 6.03/1.20 % (1765441)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1729997391:i=575:rtra=on_2992 on theBenchmark for (2992ds/575Mi)
% 6.03/1.20 % (1765404)Instruction limit reached!
% 6.03/1.20 % (1765404)------------------------------
% 6.03/1.20 % (1765404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.03/1.20 % (1765404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.20 % (1765404)CaDiCaL version: 2.1.3
% 6.03/1.20 % (1765404)Termination reason: Instruction limit
% 6.03/1.20 % (1765404)Termination phase: Saturation
% 6.03/1.20 % (1765404)Time elapsed: 0.214 s
% 6.03/1.20 % (1765404)Peak memory usage: 14 MB
% 6.03/1.20 % (1765404)Instructions burned: 450 (million)
% 6.03/1.20 % (1765438)Instruction limit reached!
% 6.03/1.20 % (1765438)------------------------------
% 6.03/1.20 % (1765438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.03/1.20 % (1765438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.20 % (1765438)CaDiCaL version: 2.1.3
% 6.03/1.20 % (1765438)Termination reason: Instruction limit
% 6.03/1.20 % (1765438)Termination phase: Saturation
% 6.03/1.20 % (1765438)Time elapsed: 0.093 s
% 6.03/1.20 % (1765438)Peak memory usage: 13 MB
% 6.03/1.20 % (1765438)Instructions burned: 375 (million)
% 6.03/1.20 % (1765444)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=309070011:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2992 on theBenchmark for (2992ds/270Mi)
% 6.03/1.20 % (1765445)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=3547320348: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_2992 on theBenchmark for (2992ds/9840Mi)
% 6.03/1.20 % (1765441)Refutation not found, incomplete strategy
% 6.03/1.20 % (1765441)------------------------------
% 6.03/1.20 % (1765441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.03/1.20 % (1765441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.20 % (1765441)CaDiCaL version: 2.1.3
% 6.03/1.20 % (1765441)Termination reason: Refutation not found, incomplete strategy
% 6.03/1.20 % (1765441)Time elapsed: 0.049 s
% 6.03/1.20 % (1765441)Peak memory usage: 13 MB
% 6.03/1.20 % (1765441)Instructions burned: 101 (million)
% 6.03/1.20 % (1765440)Instruction limit reached!
% 6.03/1.20 % (1765440)------------------------------
% 6.03/1.20 % (1765440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.03/1.20 % (1765440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.20 % (1765440)CaDiCaL version: 2.1.3
% 6.03/1.20 % (1765440)Termination reason: Instruction limit
% 6.03/1.20 % (1765440)Termination phase: Saturation
% 6.03/1.20 % (1765440)Time elapsed: 0.057 s
% 6.03/1.20 % (1765440)Peak memory usage: 13 MB
% 6.03/1.20 % (1765440)Instructions burned: 117 (million)
% 6.03/1.20 % (1765441)------------------------------
% 6.03/1.20 % (1765441)------------------------------
% 6.03/1.20 % (1765449)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
% 6.03/1.29 % (1765433)Instruction limit reached!
% 6.03/1.29 % (1765433)------------------------------
% 6.03/1.29 % (1765433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.03/1.29 % (1765433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.29 % (1765433)CaDiCaL version: 2.1.3
% 6.03/1.29 % (1765433)Termination reason: Instruction limit
% 6.03/1.29 % (1765433)Termination phase: Saturation
% 6.03/1.29 % (1765433)Time elapsed: 0.147 s
% 6.03/1.29 % (1765433)Peak memory usage: 13 MB
% 6.03/1.29 % (1765433)Instructions burned: 340 (million)
% 6.03/1.29 % (1765448)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=372737757:i=421:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/421Mi)
% 6.03/1.29 % (1765449)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=3405013380:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/270Mi)
% 6.03/1.29 % (1765448)Refutation not found, incomplete strategy
% 6.03/1.29 % (1765448)------------------------------
% 6.03/1.29 % (1765448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.03/1.29 % (1765448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.29 % (1765448)CaDiCaL version: 2.1.3
% 6.03/1.29 % (1765448)Termination reason: Refutation not found, incomplete strategy
% 6.03/1.29 % (1765448)Time elapsed: 0.013 s
% 6.03/1.29 % (1765448)Peak memory usage: 12 MB
% 6.03/1.29 % (1765448)Instructions burned: 30 (million)
% 6.03/1.29 % (1765448)------------------------------
% 6.03/1.29 % (1765448)------------------------------
% 6.03/1.29 % (1765450)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3655204631:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/31Mi)
% 6.03/1.29 % (1765417)Instruction limit reached!
% 6.03/1.29 % (1765417)------------------------------
% 6.03/1.29 % (1765417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.03/1.29 % (1765417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.29 % (1765453)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 6.03/1.29 % (1765417)CaDiCaL version: 2.1.3
% 6.03/1.29 % (1765417)Termination reason: Instruction limit
% 6.03/1.29 % (1765417)Termination phase: Saturation
% 6.03/1.29 % (1765417)Time elapsed: 0.246 s
% 6.03/1.29 % (1765417)Peak memory usage: 16 MB
% 6.03/1.29 % (1765417)Instructions burned: 496 (million)
% 6.03/1.29 % (1765453)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
% 6.03/1.29 % (1765450)Instruction limit reached!
% 6.03/1.29 % (1765450)------------------------------
% 6.03/1.29 % (1765450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.03/1.29 % (1765450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.29 % (1765450)CaDiCaL version: 2.1.3
% 6.03/1.29 % (1765450)Termination reason: Instruction limit
% 6.03/1.29 % (1765450)Termination phase: Property scanning
% 6.03/1.29 % (1765450)Time elapsed: 0.014 s
% 6.03/1.29 % (1765450)Peak memory usage: 10 MB
% 6.03/1.29 % (1765450)Instructions burned: 31 (million)
% 6.03/1.29 % (1765453)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=2884162023:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2991 on theBenchmark for (2991ds/1440Mi)
% 6.03/1.29 % (1765426)Instruction limit reached!
% 6.03/1.29 % (1765426)------------------------------
% 6.03/1.29 % (1765426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.03/1.29 % (1765426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.29 % (1765426)CaDiCaL version: 2.1.3
% 6.03/1.29 % (1765426)Termination reason: Instruction limit
% 6.03/1.29 % (1765426)Termination phase: Saturation
% 6.03/1.29 % (1765426)Time elapsed: 0.212 s
% 6.03/1.29 % (1765426)Peak memory usage: 16 MB
% 6.03/1.29 % (1765426)Instructions burned: 339 (million)
% 6.03/1.29 % (1765455)dis+10_2_sil=128000:si=on:random_seed=41797349:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2991 on theBenchmark for (2991ds/339Mi)
% 6.03/1.29 % (1765456)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=93087691:i=111:add=on:fgj=on:rtra=on:fdi=1024_2991 on theBenchmark for (2991ds/111Mi)
% 6.80/1.46 % (1765458)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=3231467173:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2991 on theBenchmark for (2991ds/122Mi)
% 6.80/1.46 % (1765455)Refutation not found, incomplete strategy
% 6.80/1.46 % (1765455)------------------------------
% 6.80/1.46 % (1765455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.46 % (1765455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.46 % (1765455)CaDiCaL version: 2.1.3
% 6.80/1.46 % (1765455)Termination reason: Refutation not found, incomplete strategy
% 6.80/1.46 % (1765455)Time elapsed: 0.015 s
% 6.80/1.46 % (1765455)Peak memory usage: 11 MB
% 6.80/1.46 % (1765455)Instructions burned: 34 (million)
% 6.80/1.46 % (1765455)------------------------------
% 6.80/1.46 % (1765455)------------------------------
% 6.80/1.46 % (1765458)Refutation not found, incomplete strategy
% 6.80/1.46 % (1765458)------------------------------
% 6.80/1.46 % (1765458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.46 % (1765458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.46 % (1765458)CaDiCaL version: 2.1.3
% 6.80/1.46 % (1765458)Termination reason: Refutation not found, incomplete strategy
% 6.80/1.46 % (1765458)Time elapsed: 0.014 s
% 6.80/1.46 % (1765458)Peak memory usage: 12 MB
% 6.80/1.46 % (1765458)Instructions burned: 31 (million)
% 6.80/1.46 % (1765458)------------------------------
% 6.80/1.46 % (1765458)------------------------------
% 6.80/1.46 % (1765462)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=706017510:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/136Mi)
% 6.80/1.46 % (1765444)Instruction limit reached!
% 6.80/1.46 % (1765444)------------------------------
% 6.80/1.46 % (1765444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.46 % (1765444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.46 % (1765444)CaDiCaL version: 2.1.3
% 6.80/1.46 % (1765444)Termination reason: Instruction limit
% 6.80/1.46 % (1765444)Termination phase: Saturation
% 6.80/1.46 % (1765444)Time elapsed: 0.130 s
% 6.80/1.46 % (1765444)Peak memory usage: 14 MB
% 6.80/1.46 % (1765444)Instructions burned: 270 (million)
% 6.80/1.46 % (1765463)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=120393385:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2991 on theBenchmark for (2991ds/232Mi)
% 6.80/1.46 % (1765456)Instruction limit reached!
% 6.80/1.46 % (1765456)------------------------------
% 6.80/1.46 % (1765456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.46 % (1765456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.46 % (1765456)CaDiCaL version: 2.1.3
% 6.80/1.46 % (1765456)Termination reason: Instruction limit
% 6.80/1.46 % (1765456)Termination phase: Saturation
% 6.80/1.46 % (1765456)Time elapsed: 0.050 s
% 6.80/1.46 % (1765456)Peak memory usage: 13 MB
% 6.80/1.46 % (1765456)Instructions burned: 111 (million)
% 6.80/1.46 % (1765463)Refutation not found, incomplete strategy
% 6.80/1.46 % (1765463)------------------------------
% 6.80/1.46 % (1765463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.46 % (1765463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.46 % (1765463)CaDiCaL version: 2.1.3
% 6.80/1.46 % (1765463)Termination reason: Refutation not found, incomplete strategy
% 6.80/1.46 % (1765463)Time elapsed: 0.013 s
% 6.80/1.46 % (1765463)Peak memory usage: 12 MB
% 6.80/1.46 % (1765463)Instructions burned: 28 (million)
% 6.80/1.46 % (1765463)------------------------------
% 6.80/1.46 % (1765463)------------------------------
% 6.80/1.46 % (1765465)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=4001838863:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2991 on theBenchmark for (2991ds/1254Mi)
% 6.80/1.46 % (1765467)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 6.80/1.46 % (1765467)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=2941469299:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2990 on theBenchmark for (2990ds/281Mi)
% 7.22/1.55 % (1765468)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=762375966:i=619:add=on:rtra=on_2990 on theBenchmark for (2990ds/619Mi)
% 7.22/1.55 % (1765462)Refutation not found, incomplete strategy
% 7.22/1.55 % (1765462)------------------------------
% 7.22/1.55 % (1765462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.22/1.55 % (1765462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.55 % (1765462)CaDiCaL version: 2.1.3
% 7.22/1.55 % (1765462)Termination reason: Refutation not found, incomplete strategy
% 7.22/1.55 % (1765462)Time elapsed: 0.041 s
% 7.22/1.55 % (1765462)Peak memory usage: 13 MB
% 7.22/1.55 % (1765462)Instructions burned: 90 (million)
% 7.22/1.55 % (1765462)------------------------------
% 7.22/1.55 % (1765462)------------------------------
% 7.22/1.55 % (1765449)Instruction limit reached!
% 7.22/1.55 % (1765449)------------------------------
% 7.22/1.55 % (1765449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.22/1.55 % (1765449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.55 % (1765449)CaDiCaL version: 2.1.3
% 7.22/1.55 % (1765449)Termination reason: Instruction limit
% 7.22/1.55 % (1765449)Termination phase: Saturation
% 7.22/1.55 % (1765449)Time elapsed: 0.138 s
% 7.22/1.55 % (1765449)Peak memory usage: 14 MB
% 7.22/1.55 % (1765449)Instructions burned: 270 (million)
% 7.22/1.55 % (1765472)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=629375665:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/865Mi)
% 7.22/1.55 % (1765473)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3367931186:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/212Mi)
% 7.22/1.55 % (1765473)Refutation not found, incomplete strategy
% 7.22/1.55 % (1765473)------------------------------
% 7.22/1.55 % (1765473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.22/1.55 % (1765473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.55 % (1765473)CaDiCaL version: 2.1.3
% 7.22/1.55 % (1765473)Termination reason: Refutation not found, incomplete strategy
% 7.22/1.55 % (1765473)Time elapsed: 0.014 s
% 7.22/1.55 % (1765473)Peak memory usage: 12 MB
% 7.22/1.55 % (1765473)Instructions burned: 30 (million)
% 7.22/1.55 % (1765473)------------------------------
% 7.22/1.55 % (1765473)------------------------------
% 7.22/1.55 % (1765465)Refutation not found, incomplete strategy
% 7.22/1.55 % (1765465)------------------------------
% 7.22/1.55 % (1765465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.22/1.55 % (1765465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.55 % (1765465)CaDiCaL version: 2.1.3
% 7.22/1.55 % (1765465)Termination reason: Refutation not found, incomplete strategy
% 7.22/1.55 % (1765465)Time elapsed: 0.077 s
% 7.22/1.55 % (1765465)Peak memory usage: 14 MB
% 7.22/1.55 % (1765465)Instructions burned: 172 (million)
% 7.22/1.55 % (1765465)------------------------------
% 7.22/1.55 % (1765465)------------------------------
% 7.22/1.55 % (1765476)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=2650026689:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/130Mi)
% 7.22/1.55 % (1765468)Refutation not found, incomplete strategy
% 7.22/1.55 % (1765468)------------------------------
% 7.22/1.55 % (1765468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.22/1.55 % (1765468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.55 % (1765468)CaDiCaL version: 2.1.3
% 7.22/1.55 % (1765468)Termination reason: Refutation not found, incomplete strategy
% 7.22/1.55 % (1765468)Time elapsed: 0.068 s
% 7.22/1.55 % (1765468)Peak memory usage: 15 MB
% 7.22/1.55 % (1765468)Instructions burned: 155 (million)
% 7.22/1.55 % (1765468)------------------------------
% 7.22/1.55 % (1765468)------------------------------
% 7.22/1.55 % (1765477)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=651540142:st=1.5:i=346:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/346Mi)
% 7.22/1.55 % (1765476)Refutation not found, incomplete strategy
% 7.22/1.55 % (1765476)------------------------------
% 7.22/1.55 % (1765476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.82 % (1765476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.82 % (1765476)CaDiCaL version: 2.1.3
% 8.42/1.82 % (1765476)Termination reason: Refutation not found, incomplete strategy
% 8.42/1.82 % (1765476)Time elapsed: 0.014 s
% 8.42/1.82 % (1765476)Peak memory usage: 12 MB
% 8.42/1.82 % (1765476)Instructions burned: 32 (million)
% 8.42/1.82 % (1765476)------------------------------
% 8.42/1.82 % (1765476)------------------------------
% 8.42/1.82 % (1765479)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=2649976400:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/152Mi)
% 8.42/1.82 % (1765481)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1804900466:i=75:ep=R:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/75Mi)
% 8.42/1.82 % (1765467)Instruction limit reached!
% 8.42/1.82 % (1765467)------------------------------
% 8.42/1.82 % (1765467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.82 % (1765467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.82 % (1765467)CaDiCaL version: 2.1.3
% 8.42/1.82 % (1765467)Termination reason: Instruction limit
% 8.42/1.82 % (1765467)Termination phase: Saturation
% 8.42/1.82 % (1765467)Time elapsed: 0.126 s
% 8.42/1.82 % (1765467)Peak memory usage: 14 MB
% 8.42/1.82 % (1765467)Instructions burned: 282 (million)
% 8.42/1.82 % (1765481)Instruction limit reached!
% 8.42/1.82 % (1765481)------------------------------
% 8.42/1.82 % (1765481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.82 % (1765481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.82 % (1765481)CaDiCaL version: 2.1.3
% 8.42/1.82 % (1765481)Termination reason: Instruction limit
% 8.42/1.82 % (1765481)Termination phase: Property scanning
% 8.42/1.82 % (1765481)Time elapsed: 0.031 s
% 8.42/1.82 % (1765481)Peak memory usage: 11 MB
% 8.42/1.82 % (1765481)Instructions burned: 75 (million)
% 8.42/1.82 % (1765484)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=2308098817:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/387Mi)
% 8.42/1.82 % (1765485)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=3474871659:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2989 on theBenchmark for (2989ds/148Mi)
% 8.42/1.82 % (1765479)Instruction limit reached!
% 8.42/1.82 % (1765479)------------------------------
% 8.42/1.82 % (1765479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.82 % (1765479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.82 % (1765479)CaDiCaL version: 2.1.3
% 8.42/1.82 % (1765479)Termination reason: Instruction limit
% 8.42/1.82 % (1765479)Termination phase: Saturation
% 8.42/1.82 % (1765479)Time elapsed: 0.071 s
% 8.42/1.82 % (1765479)Peak memory usage: 14 MB
% 8.42/1.82 % (1765479)Instructions burned: 154 (million)
% 8.42/1.82 % (1765488)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1248252607:i=161:piset=and:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/161Mi)
% 8.42/1.82 % (1765485)Instruction limit reached!
% 8.42/1.82 % (1765485)------------------------------
% 8.42/1.82 % (1765485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.82 % (1765485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.82 % (1765485)CaDiCaL version: 2.1.3
% 8.42/1.82 % (1765485)Termination reason: Instruction limit
% 8.42/1.82 % (1765485)Termination phase: Saturation
% 8.42/1.82 % (1765485)Time elapsed: 0.063 s
% 8.42/1.82 % (1765485)Peak memory usage: 13 MB
% 8.42/1.82 % (1765485)Instructions burned: 148 (million)
% 8.42/1.82 % (1765490)lrs+10_1_sil=128000:si=on:random_seed=3432027203:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/888Mi)
% 8.42/1.82 % (1765490)Refutation not found, incomplete strategy
% 8.42/1.82 % (1765490)------------------------------
% 8.42/1.82 % (1765490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.82 % (1765490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.82 % (1765490)CaDiCaL version: 2.1.3
% 8.42/1.82 % (1765490)Termination reason: Refutation not found, incomplete strategy
% 8.42/1.82 % (1765490)Time elapsed: 0.015 s
% 8.42/1.82 % (1765490)Peak memory usage: 12 MB
% 9.51/1.92 % (1765490)Instructions burned: 31 (million)
% 9.51/1.92 % (1765477)Instruction limit reached!
% 9.51/1.92 % (1765477)------------------------------
% 9.51/1.92 % (1765477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765490)------------------------------
% 9.51/1.92 % (1765490)------------------------------
% 9.51/1.92 % (1765477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765477)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765477)Termination reason: Instruction limit
% 9.51/1.92 % (1765477)Termination phase: Saturation
% 9.51/1.92 % (1765477)Time elapsed: 0.172 s
% 9.51/1.92 % (1765477)Peak memory usage: 15 MB
% 9.51/1.92 % (1765477)Instructions burned: 350 (million)
% 9.51/1.92 % (1765488)Instruction limit reached!
% 9.51/1.92 % (1765488)------------------------------
% 9.51/1.92 % (1765488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765488)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765488)Termination reason: Instruction limit
% 9.51/1.92 % (1765488)Termination phase: Saturation
% 9.51/1.92 % (1765488)Time elapsed: 0.080 s
% 9.51/1.92 % (1765488)Peak memory usage: 13 MB
% 9.51/1.92 % (1765488)Instructions burned: 161 (million)
% 9.51/1.92 % (1765492)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=1221507801:i=136:add=on:ins=4:rtra=on:sup=off_2988 on theBenchmark for (2988ds/136Mi)
% 9.51/1.92 % (1765493)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=739736117:i=88:s2at=3:nm=2:rtra=on:rawr=on_2988 on theBenchmark for (2988ds/88Mi)
% 9.51/1.92 % (1765494)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=3068593976:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2988 on theBenchmark for (2988ds/93Mi)
% 9.51/1.92 % (1765493)Instruction limit reached!
% 9.51/1.92 % (1765493)------------------------------
% 9.51/1.92 % (1765493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765493)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765493)Termination reason: Instruction limit
% 9.51/1.92 % (1765493)Termination phase: Property scanning
% 9.51/1.92 % (1765493)Time elapsed: 0.038 s
% 9.51/1.92 % (1765493)Peak memory usage: 11 MB
% 9.51/1.92 % (1765493)Instructions burned: 90 (million)
% 9.51/1.92 % (1765494)Instruction limit reached!
% 9.51/1.92 % (1765494)------------------------------
% 9.51/1.92 % (1765494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765494)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765494)Termination reason: Instruction limit
% 9.51/1.92 % (1765494)Termination phase: Property scanning
% 9.51/1.92 % (1765494)Time elapsed: 0.040 s
% 9.51/1.92 % (1765494)Peak memory usage: 11 MB
% 9.51/1.92 % (1765494)Instructions burned: 94 (million)
% 9.51/1.92 % (1765498)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3778733457:i=2186:rtra=on:ixr=off_2987 on theBenchmark for (2987ds/2186Mi)
% 9.51/1.92 % (1765492)Instruction limit reached!
% 9.51/1.92 % (1765492)------------------------------
% 9.51/1.92 % (1765492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765492)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765492)Termination reason: Instruction limit
% 9.51/1.92 % (1765492)Termination phase: Saturation
% 9.51/1.92 % (1765492)Time elapsed: 0.065 s
% 9.51/1.92 % (1765492)Peak memory usage: 14 MB
% 9.51/1.92 % (1765492)Instructions burned: 138 (million)
% 9.51/1.92 % (1765499)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3484040575:s2a=on:i=240:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/240Mi)
% 9.51/1.92 % (1765484)Instruction limit reached!
% 9.51/1.92 % (1765484)------------------------------
% 9.51/1.92 % (1765484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765484)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765484)Termination reason: Instruction limit
% 9.51/1.92 % (1765484)Termination phase: Saturation
% 9.51/1.92 % (1765484)Time elapsed: 0.197 s
% 9.51/1.92 % (1765484)Peak memory usage: 15 MB
% 9.51/1.92 % (1765484)Instructions burned: 387 (million)
% 9.51/1.92 % (1765503)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 9.51/1.92 % (1765501)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=2176739895:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2987 on theBenchmark for (2987ds/805Mi)
% 9.51/1.92 % (1765503)dis+1002_1_to=lpo:sil=128000:cnfonf=conj_eager:si=on:sp=unary_first:spb=intro:urr=on:cbe=off:uwa=one_side_interpreted:rp=on:avsqc=1:random_seed=3648682946:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2987 on theBenchmark for (2987ds/391Mi)
% 9.51/1.92 % (1765503)Refutation not found, incomplete strategy
% 9.51/1.92 % (1765503)------------------------------
% 9.51/1.92 % (1765503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765503)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765503)Termination reason: Refutation not found, incomplete strategy
% 9.51/1.92 % (1765503)Time elapsed: 0.032 s
% 9.51/1.92 % (1765503)Peak memory usage: 12 MB
% 9.51/1.92 % (1765503)Instructions burned: 72 (million)
% 9.51/1.92 % (1765503)------------------------------
% 9.51/1.92 % (1765503)------------------------------
% 9.51/1.92 % (1765506)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=1962947497:i=355:av=off:fsr=off:rtra=on:ixr=off_2986 on theBenchmark for (2986ds/355Mi)
% 9.51/1.92 % (1765499)Instruction limit reached!
% 9.51/1.92 % (1765499)------------------------------
% 9.51/1.92 % (1765499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765499)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765499)Termination reason: Instruction limit
% 9.51/1.92 % (1765499)Termination phase: Saturation
% 9.51/1.92 % (1765499)Time elapsed: 0.156 s
% 9.51/1.92 % (1765499)Peak memory usage: 14 MB
% 9.51/1.92 % (1765499)Instructions burned: 241 (million)
% 9.51/1.92 % (1765472)Instruction limit reached!
% 9.51/1.92 % (1765472)------------------------------
% 9.51/1.92 % (1765472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765472)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765472)Termination reason: Instruction limit
% 9.51/1.92 % (1765472)Termination phase: Saturation
% 9.51/1.92 % (1765472)Time elapsed: 0.477 s
% 9.51/1.92 % (1765472)Peak memory usage: 20 MB
% 9.51/1.92 % (1765472)Instructions burned: 865 (million)
% 9.51/1.92 % (1765508)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=1386830636:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/314Mi)
% 9.51/1.92 % (1765509)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=2641501603:s2a=on:i=251:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/251Mi)
% 9.51/1.92 % (1765508)Refutation not found, incomplete strategy
% 9.51/1.92 % (1765508)------------------------------
% 9.51/1.92 % (1765508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765508)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765508)Termination reason: Refutation not found, incomplete strategy
% 9.51/1.92 % (1765508)Time elapsed: 0.016 s
% 9.51/1.92 % (1765508)Peak memory usage: 12 MB
% 9.51/1.92 % (1765508)Instructions burned: 33 (million)
% 9.51/1.92 % (1765508)------------------------------
% 9.51/1.92 % (1765508)------------------------------
% 9.51/1.92 % (1765512)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=3677126526:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=2470:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2985 on theBenchmark for (2985ds/2470Mi)
% 9.51/1.92 % (1765453)Instruction limit reached!
% 9.51/1.92 % (1765453)------------------------------
% 9.51/1.92 % (1765453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765453)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765453)Termination reason: Instruction limit
% 9.51/1.92 % (1765453)Termination phase: Saturation
% 9.51/1.92 % (1765453)Time elapsed: 0.703 s
% 9.51/1.92 % (1765453)Peak memory usage: 16 MB
% 9.51/1.92 % (1765453)Instructions burned: 1442 (million)
% 9.51/1.92 % (1765509)Instruction limit reached!
% 9.51/1.92 % (1765509)------------------------------
% 9.51/1.92 % (1765509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765506)Instruction limit reached!
% 9.51/1.92 % (1765506)------------------------------
% 9.51/1.92 % (1765506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765509)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765506)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765506)Termination reason: Instruction limit
% 9.51/1.92 % (1765506)Termination phase: Saturation
% 9.51/1.92 % (1765509)Termination reason: Instruction limit
% 9.51/1.92 % (1765509)Termination phase: Saturation
% 9.51/1.92 % (1765506)Time elapsed: 0.204 s
% 9.51/1.92 % (1765509)Time elapsed: 0.104 s
% 9.51/1.92 % (1765506)Peak memory usage: 14 MB
% 9.51/1.92 % (1765509)Peak memory usage: 13 MB
% 9.51/1.92 % (1765506)Instructions burned: 358 (million)
% 9.51/1.92 % (1765509)Instructions burned: 253 (million)
% 9.51/1.92 % (1765514)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=1028657756:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2984 on theBenchmark for (2984ds/673Mi)
% 9.51/1.92 % (1765515)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=472195740:i=116:ep=RSTC:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/116Mi)
% 9.51/1.92 % (1765516)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1088663178:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2984 on theBenchmark for (2984ds/270Mi)
% 9.51/1.92 % (1765515)Instruction limit reached!
% 9.51/1.92 % (1765515)------------------------------
% 9.51/1.92 % (1765515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.92 % (1765515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.92 % (1765515)CaDiCaL version: 2.1.3
% 9.51/1.92 % (1765515)Termination reason: Instruction limit
% 9.51/1.92 % (1765515)Termination phase: Saturation
% 9.51/1.92 % (1765515)Time elapsed: 0.054 s
% 9.51/1.92 % (1765515)Peak memory usage: 13 MB
% 9.51/1.92 % (1765515)Instructions burned: 116 (million)
% 9.51/1.92 % (1765501) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1765275-1765501"...
% 9.51/1.92 % (1765501)...printing done.
% 9.51/1.92 % (1765501)Refutation found. Thanks to Tanya!
% 9.51/1.92 % SZS status ContradictoryAxioms for theBenchmark
% 9.51/1.92 % SZS output start Proof for theBenchmark
% 9.51/1.92 thf(type_def_5, type, set_real: $tType).
% 9.51/1.92 thf(type_def_6, type, real: $tType).
% 9.51/1.92 thf(type_def_7, type, nat: $tType).
% 9.51/1.92 thf(type_def_8, type, int: $tType).
% 9.51/1.92 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 9.51/1.92 thf(func_def_0, type, abs_abs_int: (int > int)).
% 9.51/1.92 thf(func_def_1, type, abs_abs_real: (real > real)).
% 9.51/1.92 thf(func_def_2, type, minus_minus_int: (int > int > int)).
% 9.51/1.92 thf(func_def_3, type, minus_minus_nat: (nat > nat > nat)).
% 9.51/1.92 thf(func_def_4, type, minus_minus_real: (real > real > real)).
% 9.51/1.92 thf(func_def_5, type, one_one_int: int).
% 9.51/1.92 thf(func_def_6, type, one_one_nat: nat).
% 9.51/1.92 thf(func_def_7, type, one_one_real: real).
% 9.51/1.92 thf(func_def_8, type, times_times_int: (int > int > int)).
% 9.51/1.92 thf(func_def_9, type, times_times_nat: (nat > nat > nat)).
% 9.51/1.92 thf(func_def_10, type, times_times_real: (real > real > real)).
% 9.51/1.92 thf(func_def_11, type, zero_zero_int: int).
% 9.51/1.92 thf(func_def_12, type, zero_zero_nat: nat).
% 9.51/1.92 thf(func_def_13, type, zero_zero_real: real).
% 9.51/1.92 thf(func_def_14, type, ring_1_of_int_int: (int > int)).
% 9.51/1.92 thf(func_def_15, type, ring_1_of_int_real: (int > real)).
% 9.51/1.92 thf(func_def_16, type, liouvi1159869758uville: (real > (nat > int) > (nat > int) > $o)).
% 9.51/1.92 thf(func_def_17, type, ord_less_int: (int > int > $o)).
% 9.51/1.92 thf(func_def_18, type, ord_less_nat: (nat > nat > $o)).
% 9.51/1.92 thf(func_def_19, type, ord_less_real: (real > real > $o)).
% 9.51/1.92 thf(func_def_20, type, algebraic_real: (real > $o)).
% 9.51/1.92 thf(func_def_21, type, power_power_int: (int > nat > int)).
% 9.51/1.92 thf(func_def_22, type, power_power_nat: (nat > nat > nat)).
% 9.51/1.92 thf(func_def_23, type, power_power_real: (real > nat > real)).
% 9.51/1.92 thf(func_def_24, type, field_1537545994s_real: set_real).
% 9.51/1.92 thf(func_def_25, type, divide_divide_int: (int > int > int)).
% 9.51/1.92 thf(func_def_26, type, divide_divide_nat: (nat > nat > nat)).
% 9.51/1.92 thf(func_def_27, type, divide_divide_real: (real > real > real)).
% 9.51/1.92 thf(func_def_28, type, collect_real: ((real > $o) > set_real)).
% 9.51/1.92 thf(func_def_29, type, member_real: (real > set_real > $o)).
% 9.51/1.92 thf(func_def_30, type, c: real).
% 9.51/1.92 thf(func_def_31, type, m: nat).
% 9.51/1.92 thf(func_def_32, type, n: nat).
% 9.51/1.92 thf(func_def_33, type, p: (nat > int)).
% 9.51/1.92 thf(func_def_34, type, q: (nat > int)).
% 9.51/1.92 thf(func_def_35, type, r: nat).
% 9.51/1.92 thf(func_def_36, type, x: real).
% 9.51/1.92 thf(func_def_38, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 9.51/1.92 thf(func_def_41, type, vOR: ($o > $o > $o)).
% 9.51/1.92 thf(func_def_42, type, vNOT: ($o > $o)).
% 9.51/1.92 thf(func_def_43, type, db1: !>[X0: $tType]:(X0)).
% 9.51/1.92 thf(func_def_44, type, db0: !>[X0: $tType]:(X0)).
% 9.51/1.92 thf(func_def_45, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 9.51/1.92 thf(func_def_46, type, vAND: ($o > $o > $o)).
% 9.51/1.92 thf(func_def_47, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 9.51/1.92 thf(func_def_48, type, db3: !>[X0: $tType]:(X0)).
% 9.51/1.92 thf(func_def_49, type, db2: !>[X0: $tType]:(X0)).
% 9.51/1.92 thf(func_def_50, type, vIMP: ($o > $o > $o)).
% 9.51/1.92 thf(func_def_51, type, sK0: (real > real)).
% 9.51/1.92 thf(func_def_52, type, sK1: (real > real > nat)).
% 9.51/1.92 thf(func_def_53, type, sK2: ((nat > $o) > nat)).
% 9.51/1.92 thf(func_def_54, type, sK3: (real > int)).
% 9.51/1.92 thf(func_def_55, type, sK4: (real > int)).
% 9.51/1.92 thf(func_def_56, type, sK5: (real > real > real > real)).
% 9.51/1.92 thf(func_def_57, type, sK6: (real > real > nat)).
% 9.51/1.92 thf(func_def_58, type, sK7: ((int > $o) > int > int)).
% 9.51/1.92 thf(func_def_59, type, sK8: (nat > real > real)).
% 9.51/1.92 thf(func_def_60, type, sK9: (real > real)).
% 9.51/1.92 thf(func_def_61, type, sK10: (real > real > real)).
% 9.51/1.92 thf(func_def_62, type, sK11: (real > real > real)).
% 9.51/1.92 thf(func_def_63, type, sK12: real).
% 9.51/1.92 thf(func_def_64, type, sK13: nat).
% 9.51/1.92 thf(func_def_65, type, sK14: (real > real)).
% 9.51/1.92 thf(func_def_66, type, sK15: ((nat > $o) > nat)).
% 9.51/1.92 thf(func_def_67, type, sK16: (nat > real > real)).
% 9.51/1.92 thf(func_def_68, type, sK17: real).
% 9.51/1.92 thf(func_def_69, type, sK18: nat).
% 9.51/1.92 thf(func_def_70, type, sK19: ((int > $o) > int)).
% 9.51/1.92 thf(func_def_71, type, sK20: ((nat > $o) > nat)).
% 9.51/1.92 thf(func_def_72, type, sK21: (real > real)).
% 9.51/1.92 thf(func_def_73, type, sK22: (real > nat)).
% 9.51/1.92 thf(func_def_74, type, sK23: ((nat > int) > nat)).
% 9.51/1.92 thf(func_def_75, type, sK24: (real > (nat > int) > (nat > int) > nat)).
% 9.51/1.92 thf(func_def_76, type, sK25: (real > (nat > int) > (nat > int) > nat)).
% 9.51/1.92 thf(func_def_77, type, sK26: ((nat > int) > nat)).
% 9.51/1.92 thf(func_def_78, type, sK27: ((nat > int) > real > (nat > int) > nat)).
% 9.51/1.92 thf(func_def_79, type, sK28: ((nat > int) > real > (nat > int) > nat)).
% 9.51/1.92 thf(func_def_80, type, sK29: (real > (nat > int) > (nat > int) > nat)).
% 9.51/1.92 thf(func_def_81, type, sK30: ((nat > int) > nat)).
% 9.51/1.92 thf(func_def_82, type, sK31: (real > (nat > int) > (nat > int) > nat)).
% 9.51/1.92 thf(func_def_83, type, sK32: ((nat > int) > (nat > int) > real > nat)).
% 9.51/1.92 thf(func_def_84, type, sK33: ((nat > int) > nat)).
% 9.51/1.92 thf(func_def_85, type, sK34: ((nat > int) > (nat > int) > real > nat)).
% 9.51/1.92 thf(func_def_86, type, sK35: (real > (nat > int) > (nat > int) > nat)).
% 9.51/1.92 thf(func_def_87, type, sK36: ((nat > int) > nat)).
% 9.51/1.92 thf(func_def_88, type, sK37: (real > (nat > int) > (nat > int) > nat)).
% 9.51/1.92 thf(f3,axiom,(
% 9.51/1.92 ! [X0 : nat] : (ord_less_int @ one_one_int @ (q @ X0))),
% 9.51/1.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_denom__gt__1)).
% 9.51/1.92 thf(f9,axiom,(
% 9.51/1.92 (ord_less_real @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))) @ (divide_divide_real @ c @ (power_power_real @ (ring_1_of_int_real @ (q @ m)) @ n)))),
% 9.51/1.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_8__092_060open_062_092_060bar_062x_A_N_Areal__of__int_A_Ip_Am_J_A_P_Areal__of__int_A_Iq_Am_J_092_060bar_062_A_060_Ac_A_P_Areal__of__int_A_Iq_Am_J_A_094_An_092_060close_062)).
% 9.51/1.92 thf(f10,axiom,(
% 9.51/1.92 (ord_less_int @ zero_zero_int @ (q @ m)) => (ord_less_real @ (divide_divide_real @ c @ (power_power_real @ (ring_1_of_int_real @ (q @ m)) @ n)) @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))))),
% 9.51/1.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9__092_060open_0620_A_060_Aq_Am_A_092_060Longrightarrow_062_Ac_A_P_Areal__of__int_A_Iq_Am_J_A_094_An_A_060_A_092_060bar_062x_A_N_Areal__of__int_A_Ip_Am_J_A_P_Areal__of__int_A_Iq_Am_J_092_060bar_062_092_060close_062)).
% 9.51/1.92 thf(f20,axiom,(
% 9.51/1.92 (ord_less_int @ zero_zero_int @ one_one_int)),
% 9.51/1.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_19_zero__less__one)).
% 9.51/1.92 thf(f32,axiom,(
% 9.51/1.92 ! [X0 : int] : (((minus_minus_int @ X0 @ X0)) = zero_zero_int)),
% 9.51/1.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_31_cancel__comm__monoid__add__class_Odiff__cancel)).
% 9.51/1.92 thf(f40,axiom,(
% 9.51/1.92 ! [X0 : real] : (((minus_minus_real @ X0 @ X0)) = zero_zero_real)),
% 9.51/1.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_39_diff__self)).
% 9.51/1.92 thf(f65,axiom,(
% 9.51/1.92 ! [X1 : nat,X0 : int] : (((ring_1_of_int_real @ (power_power_int @ X0 @ X1))) = ((power_power_real @ (ring_1_of_int_real @ X0) @ X1)))),
% 9.51/1.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_64_of__int__power)).
% 9.51/1.92 thf(f124,axiom,(
% 9.51/1.92 ! [X1 : int,X3 : int,X2 : int,X0 : int] : ((ord_less_int @ X0 @ X1) => ((ord_less_int @ X2 @ X3) => (ord_less_int @ (minus_minus_int @ X0 @ X3) @ (minus_minus_int @ X1 @ X2))))),
% 9.51/1.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_123_diff__strict__mono)).
% 9.51/1.92 thf(f125,axiom,(
% 9.51/1.92 ! [X3 : real,X0 : real,X1 : real,X2 : real] : ((ord_less_real @ X0 @ X1) => ((ord_less_real @ X2 @ X3) => (ord_less_real @ (minus_minus_real @ X0 @ X3) @ (minus_minus_real @ X1 @ X2))))),
% 9.51/1.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_124_diff__strict__mono)).
% 9.51/1.92 thf(f154,axiom,(
% 9.51/1.92 ~(ord_less_real @ zero_zero_real @ zero_zero_real)),
% 9.51/1.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_153_less__numeral__extra_I3_J)).
% 9.51/1.92 thf(f203,axiom,(
% 9.51/1.92 ! [X0 : int] : (((minus_minus_int @ X0 @ zero_zero_int)) = X0)),
% 9.51/1.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_202_minus__int__code_I1_J)).
% 9.51/1.92 thf(f431,plain,(
% 9.51/1.92 ! [X0 : real,X1 : real,X2 : real,X3 : real] : ((ord_less_real @ X1 @ X2) => ((ord_less_real @ X3 @ X0) => (ord_less_real @ (minus_minus_real @ X1 @ X0) @ (minus_minus_real @ X2 @ X3))))),
% 9.51/1.92 inference(rectify,[],[f125])).
% 9.51/1.92 thf(f432,plain,(
% 9.51/1.92 ! [X1 : real,X0 : real,X2 : real,X3 : real] : ((((ord_less_real @ X1 @ X2)) = $true) => ((((ord_less_real @ X3 @ X0)) = $true) => (((ord_less_real @ (minus_minus_real @ X1 @ X0) @ (minus_minus_real @ X2 @ X3))) = $true)))),
% 9.51/1.92 inference(fool_elimination,[],[f431])).
% 9.51/1.92 thf(f492,plain,(
% 9.51/1.92 ! [X0 : nat] : (ord_less_int @ one_one_int @ (q @ X0))),
% 9.51/1.92 inference(rectify,[],[f3])).
% 9.51/1.92 thf(f493,plain,(
% 9.51/1.92 ! [X0 : nat] : (((ord_less_int @ one_one_int @ (q @ X0))) = $true)),
% 9.51/1.92 inference(fool_elimination,[],[f492])).
% 9.51/1.92 thf(f503,plain,(
% 9.51/1.92 (ord_less_int @ zero_zero_int @ one_one_int)),
% 9.51/1.92 inference(rectify,[],[f20])).
% 9.51/1.92 thf(f504,plain,(
% 9.51/1.92 (((ord_less_int @ zero_zero_int @ one_one_int)) = $true)),
% 9.51/1.92 inference(fool_elimination,[],[f503])).
% 9.51/1.92 thf(f533,plain,(
% 9.51/1.92 (ord_less_int @ zero_zero_int @ (q @ m)) => (ord_less_real @ (divide_divide_real @ c @ (power_power_real @ (ring_1_of_int_real @ (q @ m)) @ n)) @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))))),
% 9.51/1.92 inference(rectify,[],[f10])).
% 9.51/1.92 thf(f534,plain,(
% 9.51/1.92 (((ord_less_int @ zero_zero_int @ (q @ m))) = $true) => (((ord_less_real @ (divide_divide_real @ c @ (power_power_real @ (ring_1_of_int_real @ (q @ m)) @ n)) @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))))) = $true)),
% 9.51/1.92 inference(fool_elimination,[],[f533])).
% 9.51/1.92 thf(f572,plain,(
% 9.51/1.92 ~(ord_less_real @ zero_zero_real @ zero_zero_real)),
% 9.51/1.92 inference(rectify,[],[f154])).
% 9.51/1.92 thf(f573,plain,(
% 9.51/1.92 ~ (((ord_less_real @ zero_zero_real @ zero_zero_real)) = $true)),
% 9.51/1.92 inference(fool_elimination,[],[f572])).
% 9.51/1.92 thf(f644,plain,(
% 9.51/1.92 ! [X0 : int,X1 : int,X2 : int,X3 : int] : ((ord_less_int @ X3 @ X0) => ((ord_less_int @ X2 @ X1) => (ord_less_int @ (minus_minus_int @ X3 @ X1) @ (minus_minus_int @ X0 @ X2))))),
% 9.51/1.92 inference(rectify,[],[f124])).
% 9.51/1.92 thf(f645,plain,(
% 9.51/1.92 ! [X2 : int,X1 : int,X0 : int,X3 : int] : (($true = ((ord_less_int @ X3 @ X0))) => ((((ord_less_int @ X2 @ X1)) = $true) => ($true = ((ord_less_int @ (minus_minus_int @ X3 @ X1) @ (minus_minus_int @ X0 @ X2))))))),
% 9.51/1.92 inference(fool_elimination,[],[f644])).
% 9.51/1.92 thf(f664,plain,(
% 9.51/1.92 (ord_less_real @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))) @ (divide_divide_real @ c @ (power_power_real @ (ring_1_of_int_real @ (q @ m)) @ n)))),
% 9.51/1.92 inference(rectify,[],[f9])).
% 9.51/1.92 thf(f665,plain,(
% 9.51/1.92 (((ord_less_real @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))) @ (divide_divide_real @ c @ (power_power_real @ (ring_1_of_int_real @ (q @ m)) @ n)))) = $true)),
% 9.51/1.92 inference(fool_elimination,[],[f664])).
% 9.51/1.92 thf(f766,plain,(
% 9.51/1.92 (((ord_less_real @ zero_zero_real @ zero_zero_real)) != $true)),
% 9.51/1.92 inference(flattening,[],[f573])).
% 9.51/1.92 thf(f768,plain,(
% 9.51/1.92 ! [X0 : nat,X1 : int] : (((power_power_real @ (ring_1_of_int_real @ X1) @ X0)) = ((ring_1_of_int_real @ (power_power_int @ X1 @ X0))))),
% 9.51/1.92 inference(rectify,[],[f65])).
% 9.51/1.92 thf(f803,plain,(
% 9.51/1.92 ! [X1 : real,X0 : real,X2 : real,X3 : real] : (((((ord_less_real @ (minus_minus_real @ X1 @ X0) @ (minus_minus_real @ X2 @ X3))) = $true) | (((ord_less_real @ X3 @ X0)) != $true)) | (((ord_less_real @ X1 @ X2)) != $true))),
% 9.51/1.92 inference(ennf_transformation,[],[f432])).
% 9.51/1.92 thf(f804,plain,(
% 9.51/1.92 ! [X1 : real,X3 : real,X0 : real,X2 : real] : ((((ord_less_real @ (minus_minus_real @ X1 @ X0) @ (minus_minus_real @ X2 @ X3))) = $true) | (((ord_less_real @ X1 @ X2)) != $true) | (((ord_less_real @ X3 @ X0)) != $true))),
% 9.51/1.92 inference(flattening,[],[f803])).
% 9.51/1.92 thf(f870,plain,(
% 9.51/1.92 (((ord_less_real @ (divide_divide_real @ c @ (power_power_real @ (ring_1_of_int_real @ (q @ m)) @ n)) @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))))) = $true) | (((ord_less_int @ zero_zero_int @ (q @ m))) != $true)),
% 9.51/1.92 inference(ennf_transformation,[],[f534])).
% 9.51/1.92 thf(f945,plain,(
% 9.51/1.92 ! [X2 : int,X1 : int,X0 : int,X3 : int] : ((($true = ((ord_less_int @ (minus_minus_int @ X3 @ X1) @ (minus_minus_int @ X0 @ X2)))) | (((ord_less_int @ X2 @ X1)) != $true)) | ($true != ((ord_less_int @ X3 @ X0))))),
% 9.51/1.92 inference(ennf_transformation,[],[f645])).
% 9.51/1.92 thf(f946,plain,(
% 9.51/1.92 ! [X2 : int,X1 : int,X3 : int,X0 : int] : (($true != ((ord_less_int @ X3 @ X0))) | ($true = ((ord_less_int @ (minus_minus_int @ X3 @ X1) @ (minus_minus_int @ X0 @ X2)))) | (((ord_less_int @ X2 @ X1)) != $true))),
% 9.51/1.92 inference(flattening,[],[f945])).
% 9.51/1.92 thf(f997,plain,(
% 9.51/1.92 ! [X0 : real,X1 : real,X2 : real,X3 : real] : (($true = ((ord_less_real @ (minus_minus_real @ X0 @ X2) @ (minus_minus_real @ X3 @ X1)))) | ($true != ((ord_less_real @ X0 @ X3))) | (((ord_less_real @ X1 @ X2)) != $true))),
% 9.51/1.92 inference(rectify,[],[f804])).
% 9.51/1.92 thf(f1012,plain,(
% 9.51/1.92 ! [X0 : int,X1 : int,X2 : int,X3 : int] : ((((ord_less_int @ X2 @ X3)) != $true) | ($true = ((ord_less_int @ (minus_minus_int @ X2 @ X1) @ (minus_minus_int @ X3 @ X0)))) | (((ord_less_int @ X0 @ X1)) != $true))),
% 9.51/1.92 inference(rectify,[],[f946])).
% 9.51/1.92 thf(f1173,plain,(
% 9.51/1.92 (((ord_less_real @ (divide_divide_real @ c @ (power_power_real @ (ring_1_of_int_real @ (q @ m)) @ n)) @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))))) = $true) | (((ord_less_int @ zero_zero_int @ (q @ m))) != $true)),
% 9.51/1.92 inference(cnf_transformation,[],[f870])).
% 9.51/1.92 thf(f1182,plain,(
% 9.51/1.92 (((ord_less_int @ zero_zero_int @ one_one_int)) = $true)),
% 9.51/1.92 inference(cnf_transformation,[],[f504])).
% 9.51/1.92 thf(f1200,plain,(
% 9.51/1.92 ( ! [X2 : real,X3 : real,X0 : real,X1 : real] : (($true != ((ord_less_real @ X0 @ X3))) | ($true = ((ord_less_real @ (minus_minus_real @ X0 @ X2) @ (minus_minus_real @ X3 @ X1)))) | (((ord_less_real @ X1 @ X2)) != $true)) )),
% 9.51/1.92 inference(cnf_transformation,[],[f997])).
% 9.51/1.92 thf(f1223,plain,(
% 9.51/1.92 ( ! [X0 : int] : ((((minus_minus_int @ X0 @ zero_zero_int)) = X0)) )),
% 9.51/1.92 inference(cnf_transformation,[],[f203])).
% 9.51/1.92 thf(f1240,plain,(
% 9.51/1.92 ( ! [X0 : int] : ((zero_zero_int = ((minus_minus_int @ X0 @ X0)))) )),
% 9.51/1.92 inference(cnf_transformation,[],[f32])).
% 9.51/1.92 thf(f1245,plain,(
% 9.51/1.92 ( ! [X0 : nat] : ((((ord_less_int @ one_one_int @ (q @ X0))) = $true)) )),
% 9.51/1.92 inference(cnf_transformation,[],[f493])).
% 9.51/1.92 thf(f1261,plain,(
% 9.51/1.92 ( ! [X2 : int,X3 : int,X0 : int,X1 : int] : ((((ord_less_int @ X2 @ X3)) != $true) | (((ord_less_int @ X0 @ X1)) != $true) | ($true = ((ord_less_int @ (minus_minus_int @ X2 @ X1) @ (minus_minus_int @ X3 @ X0))))) )),
% 9.51/1.92 inference(cnf_transformation,[],[f1012])).
% 9.51/1.92 thf(f1305,plain,(
% 9.51/1.92 ( ! [X0 : real] : ((zero_zero_real = ((minus_minus_real @ X0 @ X0)))) )),
% 9.51/1.92 inference(cnf_transformation,[],[f40])).
% 9.51/1.92 thf(f1331,plain,(
% 9.51/1.92 ( ! [X0 : nat,X1 : int] : ((((power_power_real @ (ring_1_of_int_real @ X1) @ X0)) = ((ring_1_of_int_real @ (power_power_int @ X1 @ X0))))) )),
% 9.51/1.93 inference(cnf_transformation,[],[f768])).
% 9.51/1.93 thf(f1388,plain,(
% 9.51/1.93 (((ord_less_real @ zero_zero_real @ zero_zero_real)) != $true)),
% 9.51/1.93 inference(cnf_transformation,[],[f766])).
% 9.51/1.93 thf(f1439,plain,(
% 9.51/1.93 (((ord_less_real @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))) @ (divide_divide_real @ c @ (power_power_real @ (ring_1_of_int_real @ (q @ m)) @ n)))) = $true)),
% 9.51/1.93 inference(cnf_transformation,[],[f665])).
% 9.51/1.93 thf(f1453,definition,(
% 9.51/1.93 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 9.51/1.93 introduced(theory,[fool_exhaustiveness_axiom])).
% 9.51/1.93 thf(f2267,definition,(
% 9.51/1.93 spl38_1 <=> (((ord_less_real @ (divide_divide_real @ c @ (power_power_real @ (ring_1_of_int_real @ (q @ m)) @ n)) @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))))) = $true)),
% 9.51/1.93 introduced(definition,[new_symbols(definition,[spl38_1])],[avatar_definition])).
% 9.51/1.93 thf(f2268,plain,(
% 9.51/1.93 (((ord_less_real @ (divide_divide_real @ c @ (power_power_real @ (ring_1_of_int_real @ (q @ m)) @ n)) @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))))) = $true) | ~spl38_1),
% 9.51/1.93 inference(avatar_component_clause,[],[f2267])).
% 9.51/1.93 thf(f2270,definition,(
% 9.51/1.93 spl38_2 <=> (((ord_less_int @ zero_zero_int @ (q @ m))) = $true)),
% 9.51/1.93 introduced(definition,[new_symbols(definition,[spl38_2])],[avatar_definition])).
% 9.51/1.93 thf(f2271,plain,(
% 9.51/1.93 (((ord_less_int @ zero_zero_int @ (q @ m))) != $true) | spl38_2),
% 9.51/1.93 inference(avatar_component_clause,[],[f2270])).
% 9.51/1.93 thf(f2272,plain,(
% 9.51/1.93 spl38_1 | ~spl38_2),
% 9.51/1.93 inference(avatar_split_clause,[],[f1173,f2270,f2267])).
% 9.51/1.93 thf(f2457,plain,(
% 9.51/1.93 (((ord_less_real @ zero_zero_real @ zero_zero_real)) = $false)),
% 9.51/1.93 inference(unit_resulting_resolution,[],[f1453,f1388])).
% 9.51/1.93 thf(f2614,plain,(
% 9.51/1.93 (((ord_less_int @ zero_zero_int @ (q @ m))) = $false) | spl38_2),
% 9.51/1.93 inference(unit_resulting_resolution,[],[f1453,f2271])).
% 9.51/1.93 thf(f4670,plain,(
% 9.51/1.93 ( ! [X0 : nat] : (($true = ((ord_less_int @ (minus_minus_int @ one_one_int @ one_one_int) @ (minus_minus_int @ (q @ X0) @ zero_zero_int))))) )),
% 9.51/1.93 inference(unit_resulting_resolution,[],[f1261,f1245,f1182])).
% 9.51/1.93 thf(f4682,plain,(
% 9.51/1.93 ( ! [X0 : nat] : (($true = ((ord_less_int @ zero_zero_int @ (minus_minus_int @ (q @ X0) @ zero_zero_int))))) )),
% 9.51/1.93 inference(forward_demodulation,[],[f4670,f1240])).
% 9.51/1.93 thf(f4687,plain,(
% 9.51/1.93 ( ! [X0 : nat] : (($true = ((ord_less_int @ zero_zero_int @ (q @ X0))))) )),
% 9.51/1.93 inference(forward_demodulation,[],[f4682,f1223])).
% 9.51/1.93 thf(f4688,plain,(
% 9.51/1.93 ($false = $true) | spl38_2),
% 9.51/1.93 inference(backward_demodulation,[],[f2614,f4687])).
% 9.51/1.93 thf(f4704,plain,(
% 9.51/1.93 $false | spl38_2),
% 9.51/1.93 inference(trivial_inequality_removal,[],[f4688])).
% 9.51/1.93 thf(f4705,plain,(
% 9.51/1.93 spl38_2),
% 9.51/1.93 inference(avatar_contradiction_clause,[],[f4704])).
% 9.51/1.93 thf(f4714,plain,(
% 9.51/1.93 ($true = ((ord_less_real @ (divide_divide_real @ c @ (ring_1_of_int_real @ (power_power_int @ (q @ m) @ n))) @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m)))))))) | ~spl38_1),
% 9.51/1.93 inference(forward_demodulation,[],[f2268,f1331])).
% 9.51/1.93 thf(f7171,plain,(
% 9.51/1.93 ($true = ((ord_less_real @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))) @ (divide_divide_real @ c @ (ring_1_of_int_real @ (power_power_int @ (q @ m) @ n))))))),
% 9.51/1.93 inference(forward_demodulation,[],[f1439,f1331])).
% 9.51/1.93 thf(f8004,plain,(
% 9.51/1.93 ($true = ((ord_less_real @ (minus_minus_real @ (divide_divide_real @ c @ (ring_1_of_int_real @ (power_power_int @ (q @ m) @ n))) @ (divide_divide_real @ c @ (ring_1_of_int_real @ (power_power_int @ (q @ m) @ n)))) @ (minus_minus_real @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))) @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))))))) | ~spl38_1),
% 9.51/1.93 inference(unit_resulting_resolution,[],[f1200,f4714,f7171])).
% 9.51/1.93 thf(f8030,plain,(
% 9.51/1.93 (((ord_less_real @ zero_zero_real @ (minus_minus_real @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m))))) @ (abs_abs_real @ (minus_minus_real @ x @ (divide_divide_real @ (ring_1_of_int_real @ (p @ m)) @ (ring_1_of_int_real @ (q @ m)))))))) = $true) | ~spl38_1),
% 9.51/1.93 inference(forward_demodulation,[],[f8004,f1305])).
% 9.51/1.93 thf(f8042,plain,(
% 9.51/1.93 (((ord_less_real @ zero_zero_real @ zero_zero_real)) = $true) | ~spl38_1),
% 9.51/1.93 inference(forward_demodulation,[],[f8030,f1305])).
% 9.51/1.93 thf(f8046,plain,(
% 9.51/1.93 ($false = $true) | ~spl38_1),
% 9.51/1.93 inference(forward_demodulation,[],[f8042,f2457])).
% 9.51/1.93 thf(f8047,plain,(
% 9.51/1.93 $false | ~spl38_1),
% 9.51/1.93 inference(trivial_inequality_removal,[],[f8046])).
% 9.51/1.93 thf(f8048,plain,(
% 9.51/1.93 ~spl38_1),
% 9.51/1.93 inference(avatar_contradiction_clause,[],[f8047])).
% 9.51/1.93 cnf(s1, plain, spl38_1 | ~spl38_2, inference(sat_conversion,[],[f2272])).
% 9.51/1.93 cnf(s2, plain, spl38_2, inference(sat_conversion,[],[f4705])).
% 9.51/1.93 cnf(s4, plain, ~spl38_1, inference(sat_conversion,[],[f8048])).
% 9.51/1.93 cnf(s5, plain, $false, inference(rat,[],[s1,s2,s4])).
% 9.51/1.93 thf(f8049,plain,(
% 9.51/1.93 $false),
% 9.51/1.93 inference(avatar_sat_refutation,[],[s5])).
% 9.51/1.93 % SZS output end Proof for theBenchmark
% 9.51/1.93 % (1765501)------------------------------
% 9.51/1.93 % (1765501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.51/1.93 % (1765501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/1.93 % (1765501)CaDiCaL version: 2.1.3
% 9.51/1.93 % (1765501)Termination reason: Refutation
% 9.51/1.93 % (1765501)Time elapsed: 0.352 s
% 9.51/1.93 % (1765501)Peak memory usage: 17 MB
% 9.51/1.93 % (1765501)Instructions burned: 650 (million)
% 9.51/1.93 % (1765275)Success in time 1.643 s
% 9.51/1.93 % Vampire exiting
%------------------------------------------------------------------------------