%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM925^4 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:19:02 AM UTC 2026
% Result : Theorem 9.74s 3.19s
% Output : Refutation 9.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925^4 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 % Computer : n009.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Tue Sep 29 13:05:45 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.25 Running higher-order theorem proving
% 1.46/1.59 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.56/2.06 % (3951531)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.56/2.06 % (3951536)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=614877673:s2a=on:i=87:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/87Mi)
% 1.56/2.06 % (3951538)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1499448554:i=3:rtra=on:inj=on:ntd=on_2996 on theBenchmark for (2996ds/3Mi)
% 1.56/2.06 % (3951537)lrs+10_16_si=on:nwc=1.5:random_seed=1905688287:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2996 on theBenchmark for (2996ds/18Mi)
% 1.56/2.06 % (3951539)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=2495992711: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_2996 on theBenchmark for (2996ds/634Mi)
% 1.56/2.06 % (3951538)Instruction limit reached!
% 1.56/2.06 % (3951538)------------------------------
% 1.56/2.06 % (3951538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/2.06 % (3951538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/2.06 % (3951538)CaDiCaL version: 2.1.3
% 1.56/2.06 % (3951538)Termination reason: Instruction limit
% 1.56/2.06 % (3951538)Termination phase: shuffling
% 1.56/2.06 % (3951538)Time elapsed: 0.005 s
% 1.56/2.06 % (3951538)Peak memory usage: 15 MB
% 1.56/2.06 % (3951538)Instructions burned: 3 (million)
% 1.56/2.06 % (3951540)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3397220620:i=24:av=off:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 1.56/2.06 % (3951537)Instruction limit reached!
% 1.56/2.06 % (3951537)------------------------------
% 1.56/2.06 % (3951537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/2.06 % (3951537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/2.06 % (3951537)CaDiCaL version: 2.1.3
% 1.56/2.06 % (3951537)Termination reason: Instruction limit
% 1.56/2.06 % (3951537)Termination phase: shuffling
% 1.56/2.06 % (3951537)Time elapsed: 0.014 s
% 1.56/2.06 % (3951537)Peak memory usage: 16 MB
% 1.56/2.06 % (3951537)Instructions burned: 20 (million)
% 1.56/2.06 % (3951541)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3936750430:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/75Mi)
% 1.56/2.06 % (3951542)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.56/2.06 % (3951542)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.56/2.06 % (3951542)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=3482809829:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2996 on theBenchmark for (2996ds/157Mi)
% 1.56/2.06 % (3951547)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2586756401:i=2:hud=10:rtra=on_2996 on theBenchmark for (2996ds/2Mi)
% 1.56/2.06 % (3951547)Instruction limit reached!
% 1.56/2.06 % (3951547)------------------------------
% 1.56/2.06 % (3951547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/2.06 % (3951547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/2.06 % (3951547)CaDiCaL version: 2.1.3
% 1.56/2.06 % (3951547)Termination reason: Instruction limit
% 1.56/2.06 % (3951547)Termination phase: shuffling
% 1.56/2.06 % (3951547)Time elapsed: 0.003 s
% 1.56/2.06 % (3951547)Peak memory usage: 15 MB
% 1.56/2.06 % (3951547)Instructions burned: 2 (million)
% 1.56/2.06 % (3951550)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1913375067:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/5Mi)
% 1.56/2.06 % (3951540)Instruction limit reached!
% 1.56/2.06 % (3951540)------------------------------
% 1.56/2.06 % (3951540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/2.06 % (3951540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/2.06 % (3951540)CaDiCaL version: 2.1.3
% 1.56/2.06 % (3951540)Termination reason: Instruction limit
% 1.56/2.06 % (3951540)Termination phase: shuffling
% 1.56/2.06 % (3951540)Time elapsed: 0.026 s
% 1.56/2.06 % (3951540)Peak memory usage: 17 MB
% 1.56/2.06 % (3951540)Instructions burned: 24 (million)
% 2.66/2.14 % (3951550)Instruction limit reached!
% 2.66/2.14 % (3951550)------------------------------
% 2.66/2.14 % (3951550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.66/2.14 % (3951550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/2.14 % (3951550)CaDiCaL version: 2.1.3
% 2.66/2.14 % (3951550)Termination reason: Instruction limit
% 2.66/2.14 % (3951550)Termination phase: shuffling
% 2.66/2.14 % (3951550)Time elapsed: 0.008 s
% 2.66/2.14 % (3951550)Peak memory usage: 16 MB
% 2.66/2.14 % (3951550)Instructions burned: 6 (million)
% 2.66/2.14 % (3951553)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.66/2.14 % (3951553)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1718764218:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 2.66/2.14 % (3951541)Instruction limit reached!
% 2.66/2.14 % (3951541)------------------------------
% 2.66/2.14 % (3951541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.66/2.14 % (3951541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/2.14 % (3951541)CaDiCaL version: 2.1.3
% 2.66/2.14 % (3951541)Termination reason: Instruction limit
% 2.66/2.14 % (3951541)Termination phase: shuffling
% 2.66/2.14 % (3951541)Time elapsed: 0.037 s
% 2.66/2.14 % (3951541)Peak memory usage: 17 MB
% 2.66/2.14 % (3951541)Instructions burned: 75 (million)
% 2.66/2.14 % (3951536)Instruction limit reached!
% 2.66/2.14 % (3951536)------------------------------
% 2.66/2.14 % (3951536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.66/2.14 % (3951536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/2.14 % (3951536)CaDiCaL version: 2.1.3
% 2.66/2.14 % (3951536)Termination reason: Instruction limit
% 2.66/2.14 % (3951536)Termination phase: shuffling
% 2.66/2.14 % (3951536)Time elapsed: 0.057 s
% 2.66/2.14 % (3951536)Peak memory usage: 17 MB
% 2.66/2.14 % (3951536)Instructions burned: 88 (million)
% 2.66/2.14 % (3951553)Instruction limit reached!
% 2.66/2.14 % (3951553)------------------------------
% 2.66/2.14 % (3951553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.66/2.14 % (3951553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/2.14 % (3951553)CaDiCaL version: 2.1.3
% 2.66/2.14 % (3951553)Termination reason: Instruction limit
% 2.66/2.14 % (3951553)Termination phase: shuffling
% 2.66/2.14 % (3951553)Time elapsed: 0.009 s
% 2.66/2.14 % (3951553)Peak memory usage: 16 MB
% 2.66/2.14 % (3951553)Instructions burned: 9 (million)
% 2.66/2.14 % (3951556)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
% 2.66/2.14 % (3951556)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.66/2.14 % (3951560)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 2.66/2.14 % (3951556)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3106689794:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2996 on theBenchmark for (2996ds/28Mi)
% 2.66/2.14 % (3951559)lrs+10_1_si=on:cs=on:random_seed=573604630:i=8:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/8Mi)
% 2.66/2.14 % (3951560)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=269795102:i=2:add=on:rtra=on_2996 on theBenchmark for (2996ds/2Mi)
% 2.66/2.14 % (3951555)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1076993314:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/12Mi)
% 2.66/2.14 % (3951560)Instruction limit reached!
% 2.66/2.14 % (3951560)------------------------------
% 2.66/2.14 % (3951560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.66/2.14 % (3951560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/2.14 % (3951560)CaDiCaL version: 2.1.3
% 2.66/2.14 % (3951560)Termination reason: Instruction limit
% 2.66/2.14 % (3951560)Termination phase: shuffling
% 2.66/2.14 % (3951560)Time elapsed: 0.003 s
% 3.04/2.18 % (3951560)Peak memory usage: 15 MB
% 3.04/2.18 % (3951560)Instructions burned: 2 (million)
% 3.04/2.18 % (3951559)Instruction limit reached!
% 3.04/2.18 % (3951559)------------------------------
% 3.04/2.18 % (3951559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/2.18 % (3951559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/2.18 % (3951559)CaDiCaL version: 2.1.3
% 3.04/2.18 % (3951559)Termination reason: Instruction limit
% 3.04/2.18 % (3951559)Termination phase: shuffling
% 3.04/2.18 % (3951559)Time elapsed: 0.008 s
% 3.04/2.18 % (3951559)Peak memory usage: 16 MB
% 3.04/2.18 % (3951559)Instructions burned: 9 (million)
% 3.04/2.18 % (3951558)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=99005475:i=86:piset=equals:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/86Mi)
% 3.04/2.18 % (3951556)Instruction limit reached!
% 3.04/2.18 % (3951556)------------------------------
% 3.04/2.18 % (3951556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/2.18 % (3951556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/2.18 % (3951556)CaDiCaL version: 2.1.3
% 3.04/2.18 % (3951556)Termination reason: Instruction limit
% 3.04/2.18 % (3951556)Termination phase: shuffling
% 3.04/2.18 % (3951556)Time elapsed: 0.022 s
% 3.04/2.18 % (3951556)Peak memory usage: 17 MB
% 3.04/2.18 % (3951556)Instructions burned: 29 (million)
% 3.04/2.18 % (3951555)Instruction limit reached!
% 3.04/2.18 % (3951555)------------------------------
% 3.04/2.18 % (3951555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/2.18 % (3951555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/2.18 % (3951555)CaDiCaL version: 2.1.3
% 3.04/2.18 % (3951555)Termination reason: Instruction limit
% 3.04/2.18 % (3951555)Termination phase: shuffling
% 3.04/2.18 % (3951555)Time elapsed: 0.022 s
% 3.04/2.18 % (3951555)Peak memory usage: 16 MB
% 3.04/2.18 % (3951555)Instructions burned: 13 (million)
% 3.04/2.18 % (3951566)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=997698742:st=2:i=249:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/249Mi)
% 3.04/2.18 % (3951565)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2317771844:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2995 on theBenchmark for (2995ds/38Mi)
% 3.04/2.18 % (3951568)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=852464766:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2995 on theBenchmark for (2995ds/25Mi)
% 3.04/2.18 % (3951569)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=4147214359:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2995 on theBenchmark for (2995ds/14Mi)
% 3.04/2.18 % (3951542)Instruction limit reached!
% 3.04/2.18 % (3951542)------------------------------
% 3.04/2.18 % (3951542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/2.18 % (3951542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/2.18 % (3951542)CaDiCaL version: 2.1.3
% 3.04/2.18 % (3951542)Termination reason: Instruction limit
% 3.04/2.18 % (3951542)Termination phase: shuffling
% 3.04/2.18 % (3951542)Time elapsed: 0.105 s
% 3.04/2.18 % (3951542)Peak memory usage: 19 MB
% 3.04/2.18 % (3951542)Instructions burned: 159 (million)
% 3.04/2.18 % (3951569)Instruction limit reached!
% 3.04/2.18 % (3951569)------------------------------
% 3.04/2.18 % (3951569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/2.18 % (3951569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/2.18 % (3951569)CaDiCaL version: 2.1.3
% 3.04/2.18 % (3951569)Termination reason: Instruction limit
% 3.04/2.18 % (3951569)Termination phase: shuffling
% 3.04/2.18 % (3951569)Time elapsed: 0.011 s
% 3.04/2.18 % (3951569)Peak memory usage: 16 MB
% 3.04/2.18 % (3951569)Instructions burned: 15 (million)
% 3.04/2.18 % (3951568)Instruction limit reached!
% 3.04/2.18 % (3951568)------------------------------
% 3.04/2.18 % (3951568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/2.18 % (3951568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/2.18 % (3951568)CaDiCaL version: 2.1.3
% 3.04/2.18 % (3951568)Termination reason: Instruction limit
% 3.04/2.18 % (3951568)Termination phase: shuffling
% 3.04/2.18 % (3951568)Time elapsed: 0.016 s
% 3.43/2.24 % (3951568)Peak memory usage: 17 MB
% 3.43/2.24 % (3951568)Instructions burned: 26 (million)
% 3.43/2.24 % (3951574)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2270326948:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/327Mi)
% 3.43/2.24 % (3951565)Instruction limit reached!
% 3.43/2.24 % (3951565)------------------------------
% 3.43/2.24 % (3951565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/2.24 % (3951565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/2.24 % (3951565)CaDiCaL version: 2.1.3
% 3.43/2.24 % (3951565)Termination reason: Instruction limit
% 3.43/2.24 % (3951565)Termination phase: shuffling
% 3.43/2.24 % (3951565)Time elapsed: 0.037 s
% 3.43/2.24 % (3951565)Peak memory usage: 16 MB
% 3.43/2.24 % (3951565)Instructions burned: 38 (million)
% 3.43/2.24 % (3951575)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2177273945:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2995 on theBenchmark for (2995ds/14Mi)
% 3.43/2.24 % (3951576)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3981903145:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2995 on theBenchmark for (2995ds/2Mi)
% 3.43/2.24 % (3951576)Instruction limit reached!
% 3.43/2.24 % (3951576)------------------------------
% 3.43/2.24 % (3951576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/2.24 % (3951576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/2.24 % (3951576)CaDiCaL version: 2.1.3
% 3.43/2.24 % (3951576)Termination reason: Instruction limit
% 3.43/2.24 % (3951576)Termination phase: shuffling
% 3.43/2.24 % (3951576)Time elapsed: 0.003 s
% 3.43/2.24 % (3951576)Peak memory usage: 15 MB
% 3.43/2.24 % (3951576)Instructions burned: 2 (million)
% 3.43/2.24 % (3951575)Instruction limit reached!
% 3.43/2.24 % (3951575)------------------------------
% 3.43/2.24 % (3951575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/2.24 % (3951575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/2.24 % (3951575)CaDiCaL version: 2.1.3
% 3.43/2.24 % (3951575)Termination reason: Instruction limit
% 3.43/2.24 % (3951575)Termination phase: shuffling
% 3.43/2.24 % (3951575)Time elapsed: 0.011 s
% 3.43/2.24 % (3951575)Peak memory usage: 16 MB
% 3.43/2.24 % (3951575)Instructions burned: 16 (million)
% 3.43/2.24 % (3951558)Instruction limit reached!
% 3.43/2.24 % (3951558)------------------------------
% 3.43/2.24 % (3951558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/2.24 % (3951558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/2.24 % (3951558)CaDiCaL version: 2.1.3
% 3.43/2.24 % (3951558)Termination reason: Instruction limit
% 3.43/2.24 % (3951558)Termination phase: shuffling
% 3.43/2.24 % (3951558)Time elapsed: 0.078 s
% 3.43/2.24 % (3951558)Peak memory usage: 18 MB
% 3.43/2.24 % (3951558)Instructions burned: 87 (million)
% 3.43/2.24 % (3951578)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3668729890:i=26:ep=R:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/26Mi)
% 3.43/2.24 % (3951583)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
% 3.43/2.24 % (3951583)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 3.43/2.24 % (3951582)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3874381586:cond=on:i=60:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/60Mi)
% 3.43/2.24 % (3951581)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3895627920:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/23Mi)
% 3.43/2.24 % (3951583)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=1753437822:i=14:add=off:nm=40:rtra=on:rawr=on_2995 on theBenchmark for (2995ds/14Mi)
% 3.43/2.24 % (3951578)Instruction limit reached!
% 3.43/2.24 % (3951578)------------------------------
% 3.43/2.24 % (3951578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/2.24 % (3951578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/2.24 % (3951578)CaDiCaL version: 2.1.3
% 3.86/2.30 % (3951578)Termination reason: Instruction limit
% 3.86/2.30 % (3951578)Termination phase: shuffling
% 3.86/2.30 % (3951578)Time elapsed: 0.036 s
% 3.86/2.30 % (3951578)Peak memory usage: 17 MB
% 3.86/2.30 % (3951578)Instructions burned: 28 (million)
% 3.86/2.30 % (3951583)Instruction limit reached!
% 3.86/2.30 % (3951583)------------------------------
% 3.86/2.30 % (3951583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/2.30 % (3951583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/2.30 % (3951583)CaDiCaL version: 2.1.3
% 3.86/2.30 % (3951583)Termination reason: Instruction limit
% 3.86/2.30 % (3951583)Termination phase: shuffling
% 3.86/2.30 % (3951583)Time elapsed: 0.011 s
% 3.86/2.30 % (3951583)Peak memory usage: 16 MB
% 3.86/2.30 % (3951583)Instructions burned: 14 (million)
% 3.86/2.30 % (3951581)Instruction limit reached!
% 3.86/2.30 % (3951581)------------------------------
% 3.86/2.30 % (3951581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/2.30 % (3951581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/2.30 % (3951581)CaDiCaL version: 2.1.3
% 3.86/2.30 % (3951581)Termination reason: Instruction limit
% 3.86/2.30 % (3951581)Termination phase: shuffling
% 3.86/2.30 % (3951581)Time elapsed: 0.016 s
% 3.86/2.30 % (3951581)Peak memory usage: 16 MB
% 3.86/2.30 % (3951581)Instructions burned: 24 (million)
% 3.86/2.30 % (3951588)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 3.86/2.30 % (3951588)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=2706348767:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2994 on theBenchmark for (2994ds/8Mi)
% 3.86/2.30 % (3951589)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=2172318914:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2994 on theBenchmark for (2994ds/31Mi)
% 3.86/2.30 % (3951590)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=912494124:i=7:hud=5:bd=preordered:rtra=on:bet=on_2994 on theBenchmark for (2994ds/7Mi)
% 3.86/2.30 % (3951588)Instruction limit reached!
% 3.86/2.30 % (3951588)------------------------------
% 3.86/2.30 % (3951588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/2.30 % (3951588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/2.30 % (3951588)CaDiCaL version: 2.1.3
% 3.86/2.30 % (3951588)Termination reason: Instruction limit
% 3.86/2.30 % (3951588)Termination phase: shuffling
% 3.86/2.30 % (3951588)Time elapsed: 0.009 s
% 3.86/2.30 % (3951588)Peak memory usage: 16 MB
% 3.86/2.30 % (3951588)Instructions burned: 8 (million)
% 3.86/2.30 % (3951590)Instruction limit reached!
% 3.86/2.30 % (3951590)------------------------------
% 3.86/2.30 % (3951590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/2.30 % (3951590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/2.30 % (3951590)CaDiCaL version: 2.1.3
% 3.86/2.30 % (3951590)Termination reason: Instruction limit
% 3.86/2.30 % (3951590)Termination phase: shuffling
% 3.86/2.30 % (3951590)Time elapsed: 0.008 s
% 3.86/2.30 % (3951590)Peak memory usage: 16 MB
% 3.86/2.30 % (3951590)Instructions burned: 8 (million)
% 3.86/2.30 % (3951566)Instruction limit reached!
% 3.86/2.30 % (3951566)------------------------------
% 3.86/2.30 % (3951566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/2.30 % (3951566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/2.30 % (3951566)CaDiCaL version: 2.1.3
% 3.86/2.30 % (3951566)Termination reason: Instruction limit
% 3.86/2.30 % (3951566)Termination phase: shuffling
% 3.86/2.30 % (3951566)Time elapsed: 0.142 s
% 3.86/2.30 % (3951566)Peak memory usage: 20 MB
% 3.86/2.30 % (3951566)Instructions burned: 249 (million)
% 3.86/2.30 % (3951582)Instruction limit reached!
% 3.86/2.30 % (3951582)------------------------------
% 3.86/2.30 % (3951582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/2.30 % (3951582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/2.30 % (3951582)CaDiCaL version: 2.1.3
% 3.86/2.30 % (3951582)Termination reason: Instruction limit
% 3.86/2.30 % (3951582)Termination phase: shuffling
% 3.86/2.30 % (3951582)Time elapsed: 0.056 s
% 3.86/2.30 % (3951582)Peak memory usage: 17 MB
% 3.86/2.30 % (3951582)Instructions burned: 61 (million)
% 3.86/2.39 % (3951589)Instruction limit reached!
% 3.86/2.39 % (3951589)------------------------------
% 3.86/2.39 % (3951589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/2.39 % (3951589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/2.39 % (3951589)CaDiCaL version: 2.1.3
% 3.86/2.39 % (3951589)Termination reason: Instruction limit
% 3.86/2.39 % (3951589)Termination phase: shuffling
% 3.86/2.39 % (3951589)Time elapsed: 0.019 s
% 3.86/2.39 % (3951589)Peak memory usage: 17 MB
% 3.86/2.39 % (3951589)Instructions burned: 33 (million)
% 3.86/2.39 % (3951595)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4154091026:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/20Mi)
% 3.86/2.39 % (3951594)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3116820545:i=23:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/23Mi)
% 3.86/2.39 % (3951595)Instruction limit reached!
% 3.86/2.39 % (3951595)------------------------------
% 3.86/2.39 % (3951595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/2.39 % (3951595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/2.39 % (3951595)CaDiCaL version: 2.1.3
% 3.86/2.39 % (3951595)Termination reason: Instruction limit
% 3.86/2.39 % (3951595)Termination phase: shuffling
% 3.86/2.39 % (3951595)Time elapsed: 0.014 s
% 3.86/2.39 % (3951595)Peak memory usage: 16 MB
% 3.86/2.39 % (3951595)Instructions burned: 21 (million)
% 3.86/2.39 % (3951574)Instruction limit reached!
% 3.86/2.39 % (3951574)------------------------------
% 3.86/2.39 % (3951574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/2.39 % (3951574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/2.39 % (3951574)CaDiCaL version: 2.1.3
% 3.86/2.39 % (3951574)Termination reason: Instruction limit
% 3.86/2.39 % (3951574)Termination phase: Property scanning
% 3.86/2.39 % (3951574)Time elapsed: 0.143 s
% 3.86/2.39 % (3951574)Peak memory usage: 21 MB
% 3.86/2.39 % (3951574)Instructions burned: 329 (million)
% 3.86/2.39 % (3951597)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3190759142:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2994 on theBenchmark for (2994ds/143Mi)
% 3.86/2.39 % (3951596)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2661183549:i=1240:rtra=on:ixr=off_2994 on theBenchmark for (2994ds/1240Mi)
% 3.86/2.39 % (3951598)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2098216137:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/193Mi)
% 3.86/2.39 % (3951539)Instruction limit reached!
% 3.86/2.39 % (3951539)------------------------------
% 3.86/2.39 % (3951539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/2.39 % (3951539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/2.39 % (3951539)CaDiCaL version: 2.1.3
% 3.86/2.39 % (3951539)Termination reason: Instruction limit
% 3.86/2.39 % (3951539)Termination phase: Property scanning
% 3.86/2.39 % (3951539)Time elapsed: 0.302 s
% 3.86/2.39 % (3951539)Peak memory usage: 21 MB
% 3.86/2.39 % (3951539)Instructions burned: 636 (million)
% 3.86/2.39 % (3951601)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3591376124:i=42:hud=10:rtra=on_2993 on theBenchmark for (2993ds/42Mi)
% 3.86/2.39 % (3951602)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.86/2.39 % (3951602)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=807842562:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2993 on theBenchmark for (2993ds/7Mi)
% 3.86/2.39 % (3951594)Instruction limit reached!
% 3.86/2.39 % (3951594)------------------------------
% 3.86/2.39 % (3951594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/2.39 % (3951594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/2.39 % (3951594)CaDiCaL version: 2.1.3
% 3.86/2.39 % (3951594)Termination reason: Instruction limit
% 3.86/2.39 % (3951594)Termination phase: shuffling
% 3.86/2.39 % (3951594)Time elapsed: 0.032 s
% 3.86/2.39 % (3951594)Peak memory usage: 17 MB
% 3.86/2.39 % (3951594)Instructions burned: 23 (million)
% 3.86/2.39 % (3951602)Instruction limit reached!
% 3.86/2.39 % (3951602)------------------------------
% 3.86/2.39 % (3951602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/2.52 % (3951602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/2.52 % (3951602)CaDiCaL version: 2.1.3
% 4.70/2.52 % (3951602)Termination reason: Instruction limit
% 4.70/2.52 % (3951602)Termination phase: shuffling
% 4.70/2.52 % (3951602)Time elapsed: 0.008 s
% 4.70/2.52 % (3951602)Peak memory usage: 16 MB
% 4.70/2.52 % (3951602)Instructions burned: 8 (million)
% 4.70/2.52 % (3951606)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2317903812:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/181Mi)
% 4.70/2.52 % (3951601)Instruction limit reached!
% 4.70/2.52 % (3951601)------------------------------
% 4.70/2.52 % (3951601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/2.52 % (3951601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/2.52 % (3951601)CaDiCaL version: 2.1.3
% 4.70/2.52 % (3951601)Termination reason: Instruction limit
% 4.70/2.52 % (3951601)Termination phase: shuffling
% 4.70/2.52 % (3951601)Time elapsed: 0.023 s
% 4.70/2.52 % (3951601)Peak memory usage: 17 MB
% 4.70/2.52 % (3951601)Instructions burned: 44 (million)
% 4.70/2.52 % (3951610)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 4.70/2.52 % (3951610)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=1237906633:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2993 on theBenchmark for (2993ds/6Mi)
% 4.70/2.52 % (3951610)Instruction limit reached!
% 4.70/2.52 % (3951610)------------------------------
% 4.70/2.52 % (3951610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/2.52 % (3951610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/2.52 % (3951610)CaDiCaL version: 2.1.3
% 4.70/2.52 % (3951610)Termination reason: Instruction limit
% 4.70/2.52 % (3951610)Termination phase: shuffling
% 4.70/2.52 % (3951610)Time elapsed: 0.007 s
% 4.70/2.52 % (3951610)Peak memory usage: 16 MB
% 4.70/2.52 % (3951610)Instructions burned: 6 (million)
% 4.70/2.52 % (3951612)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1281501153:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2993 on theBenchmark for (2993ds/22Mi)
% 4.70/2.52 % (3951609)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=130104625:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2993 on theBenchmark for (2993ds/169Mi)
% 4.70/2.52 % (3951612)Instruction limit reached!
% 4.70/2.52 % (3951612)------------------------------
% 4.70/2.52 % (3951612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/2.52 % (3951612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/2.52 % (3951612)CaDiCaL version: 2.1.3
% 4.70/2.52 % (3951612)Termination reason: Instruction limit
% 4.70/2.52 % (3951612)Termination phase: shuffling
% 4.70/2.52 % (3951612)Time elapsed: 0.014 s
% 4.70/2.52 % (3951612)Peak memory usage: 16 MB
% 4.70/2.52 % (3951612)Instructions burned: 22 (million)
% 4.70/2.52 % (3951614)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3963218501:i=19:add=on:rtra=on_2993 on theBenchmark for (2993ds/19Mi)
% 4.70/2.52 % (3951614)Instruction limit reached!
% 4.70/2.52 % (3951614)------------------------------
% 4.70/2.52 % (3951614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/2.52 % (3951614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/2.52 % (3951614)CaDiCaL version: 2.1.3
% 4.70/2.52 % (3951614)Termination reason: Instruction limit
% 4.70/2.52 % (3951614)Termination phase: shuffling
% 4.70/2.52 % (3951614)Time elapsed: 0.013 s
% 4.70/2.52 % (3951614)Peak memory usage: 16 MB
% 4.70/2.52 % (3951614)Instructions burned: 19 (million)
% 4.70/2.52 % (3951597)Instruction limit reached!
% 4.70/2.52 % (3951597)------------------------------
% 4.70/2.52 % (3951597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/2.52 % (3951597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/2.52 % (3951597)CaDiCaL version: 2.1.3
% 4.70/2.52 % (3951597)Termination reason: Instruction limit
% 4.70/2.52 % (3951597)Termination phase: shuffling
% 4.70/2.52 % (3951597)Time elapsed: 0.087 s
% 4.70/2.52 % (3951597)Peak memory usage: 18 MB
% 5.36/2.61 % (3951597)Instructions burned: 145 (million)
% 5.36/2.61 % (3951617)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=461768424:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/316Mi)
% 5.36/2.61 % (3951620)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=1942699532:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2992 on theBenchmark for (2992ds/45Mi)
% 5.36/2.61 % (3951606)Instruction limit reached!
% 5.36/2.61 % (3951606)------------------------------
% 5.36/2.61 % (3951606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.36/2.61 % (3951606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/2.61 % (3951606)CaDiCaL version: 2.1.3
% 5.36/2.61 % (3951606)Termination reason: Instruction limit
% 5.36/2.61 % (3951606)Termination phase: shuffling
% 5.36/2.61 % (3951606)Time elapsed: 0.082 s
% 5.36/2.61 % (3951606)Peak memory usage: 19 MB
% 5.36/2.61 % (3951606)Instructions burned: 182 (million)
% 5.36/2.61 % (3951619)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=717334872:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2992 on theBenchmark for (2992ds/853Mi)
% 5.36/2.61 % (3951623)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3225069466:i=480:rtra=on_2992 on theBenchmark for (2992ds/480Mi)
% 5.36/2.61 % (3951620)Instruction limit reached!
% 5.36/2.61 % (3951620)------------------------------
% 5.36/2.61 % (3951620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.36/2.61 % (3951620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/2.61 % (3951620)CaDiCaL version: 2.1.3
% 5.36/2.61 % (3951620)Termination reason: Instruction limit
% 5.36/2.61 % (3951620)Termination phase: Property scanning
% 5.36/2.61 % (3951620)Time elapsed: 0.024 s
% 5.36/2.61 % (3951620)Peak memory usage: 16 MB
% 5.36/2.61 % (3951620)Instructions burned: 47 (million)
% 5.36/2.61 % (3951609)Instruction limit reached!
% 5.36/2.61 % (3951609)------------------------------
% 5.36/2.61 % (3951609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.36/2.61 % (3951609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/2.61 % (3951609)CaDiCaL version: 2.1.3
% 5.36/2.61 % (3951609)Termination reason: Instruction limit
% 5.36/2.61 % (3951609)Termination phase: shuffling
% 5.36/2.61 % (3951609)Time elapsed: 0.093 s
% 5.36/2.61 % (3951609)Peak memory usage: 19 MB
% 5.36/2.61 % (3951609)Instructions burned: 171 (million)
% 5.36/2.61 % (3951626)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1694600716:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2992 on theBenchmark for (2992ds/21Mi)
% 5.36/2.61 % (3951626)Instruction limit reached!
% 5.36/2.61 % (3951626)------------------------------
% 5.36/2.61 % (3951626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.36/2.61 % (3951626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/2.62 % (3951626)CaDiCaL version: 2.1.3
% 5.36/2.62 % (3951626)Termination reason: Instruction limit
% 5.36/2.62 % (3951626)Termination phase: shuffling
% 5.36/2.62 % (3951626)Time elapsed: 0.014 s
% 5.36/2.62 % (3951626)Peak memory usage: 16 MB
% 5.36/2.62 % (3951626)Instructions burned: 23 (million)
% 5.36/2.62 % (3951628)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 5.36/2.62 % (3951598)Instruction limit reached!
% 5.36/2.62 % (3951598)------------------------------
% 5.36/2.62 % (3951598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.36/2.62 % (3951598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/2.62 % (3951598)CaDiCaL version: 2.1.3
% 5.36/2.62 % (3951598)Termination reason: Instruction limit
% 5.36/2.62 % (3951598)Termination phase: shuffling
% 5.36/2.62 % (3951598)Time elapsed: 0.164 s
% 5.36/2.62 % (3951598)Peak memory usage: 19 MB
% 5.36/2.62 % (3951598)Instructions burned: 193 (million)
% 5.36/2.62 % (3951628)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=4267730209:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/200Mi)
% 5.98/2.76 % (3951629)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3218207239:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2992 on theBenchmark for (2992ds/13Mi)
% 5.98/2.76 % (3951630)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=2389205666:i=66:s2at=3:nm=2:rtra=on:rawr=on_2992 on theBenchmark for (2992ds/66Mi)
% 5.98/2.76 % (3951629)Instruction limit reached!
% 5.98/2.76 % (3951629)------------------------------
% 5.98/2.76 % (3951629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/2.76 % (3951629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/2.76 % (3951629)CaDiCaL version: 2.1.3
% 5.98/2.76 % (3951629)Termination reason: Instruction limit
% 5.98/2.76 % (3951629)Termination phase: shuffling
% 5.98/2.76 % (3951629)Time elapsed: 0.012 s
% 5.98/2.76 % (3951629)Peak memory usage: 16 MB
% 5.98/2.76 % (3951629)Instructions burned: 15 (million)
% 5.98/2.76 % (3951634)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3250346884:i=51:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/51Mi)
% 5.98/2.76 % (3951630)Instruction limit reached!
% 5.98/2.76 % (3951630)------------------------------
% 5.98/2.76 % (3951630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/2.76 % (3951630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/2.76 % (3951630)CaDiCaL version: 2.1.3
% 5.98/2.76 % (3951630)Termination reason: Instruction limit
% 5.98/2.76 % (3951630)Termination phase: shuffling
% 5.98/2.76 % (3951630)Time elapsed: 0.035 s
% 5.98/2.76 % (3951630)Peak memory usage: 18 MB
% 5.98/2.76 % (3951630)Instructions burned: 68 (million)
% 5.98/2.76 % (3951636)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=795570605:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/31Mi)
% 5.98/2.76 % (3951634)Instruction limit reached!
% 5.98/2.76 % (3951634)------------------------------
% 5.98/2.76 % (3951634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/2.76 % (3951634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/2.76 % (3951634)CaDiCaL version: 2.1.3
% 5.98/2.76 % (3951634)Termination reason: Instruction limit
% 5.98/2.76 % (3951634)Termination phase: shuffling
% 5.98/2.76 % (3951634)Time elapsed: 0.027 s
% 5.98/2.76 % (3951634)Peak memory usage: 17 MB
% 5.98/2.76 % (3951634)Instructions burned: 52 (million)
% 5.98/2.76 % (3951628)Instruction limit reached!
% 5.98/2.76 % (3951628)------------------------------
% 5.98/2.76 % (3951628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/2.76 % (3951628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/2.76 % (3951628)CaDiCaL version: 2.1.3
% 5.98/2.76 % (3951628)Termination reason: Instruction limit
% 5.98/2.76 % (3951628)Termination phase: shuffling
% 5.98/2.76 % (3951628)Time elapsed: 0.090 s
% 5.98/2.76 % (3951628)Peak memory usage: 19 MB
% 5.98/2.76 % (3951628)Instructions burned: 202 (million)
% 5.98/2.76 % (3951636)Instruction limit reached!
% 5.98/2.76 % (3951636)------------------------------
% 5.98/2.76 % (3951636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/2.76 % (3951636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/2.76 % (3951636)CaDiCaL version: 2.1.3
% 5.98/2.76 % (3951636)Termination reason: Instruction limit
% 5.98/2.76 % (3951636)Termination phase: shuffling
% 5.98/2.76 % (3951636)Time elapsed: 0.019 s
% 5.98/2.76 % (3951636)Peak memory usage: 17 MB
% 5.98/2.76 % (3951636)Instructions burned: 32 (million)
% 5.98/2.76 % (3951638)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3121857133:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2991 on theBenchmark for (2991ds/137Mi)
% 5.98/2.76 % (3951639)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=2401556740:cond=on:i=34:hud=10:nm=10:rtra=on_2991 on theBenchmark for (2991ds/34Mi)
% 5.98/2.76 % (3951640)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3097377870:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2991 on theBenchmark for (2991ds/67Mi)
% 5.98/2.76 % (3951639)Instruction limit reached!
% 5.98/2.76 % (3951639)------------------------------
% 5.98/2.76 % (3951639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.36/2.93 % (3951639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.36/2.93 % (3951639)CaDiCaL version: 2.1.3
% 7.36/2.93 % (3951639)Termination reason: Instruction limit
% 7.36/2.93 % (3951639)Termination phase: shuffling
% 7.36/2.93 % (3951639)Time elapsed: 0.020 s
% 7.36/2.93 % (3951639)Peak memory usage: 17 MB
% 7.36/2.93 % (3951639)Instructions burned: 35 (million)
% 7.36/2.93 % (3951617)Instruction limit reached!
% 7.36/2.93 % (3951617)------------------------------
% 7.36/2.93 % (3951617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.36/2.93 % (3951617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.36/2.93 % (3951617)CaDiCaL version: 2.1.3
% 7.36/2.93 % (3951617)Termination reason: Instruction limit
% 7.36/2.93 % (3951617)Termination phase: shuffling
% 7.36/2.93 % (3951617)Time elapsed: 0.221 s
% 7.36/2.93 % (3951617)Peak memory usage: 22 MB
% 7.36/2.93 % (3951617)Instructions burned: 316 (million)
% 7.36/2.93 % (3951640)Instruction limit reached!
% 7.36/2.93 % (3951640)------------------------------
% 7.36/2.93 % (3951640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.36/2.93 % (3951640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.36/2.93 % (3951640)CaDiCaL version: 2.1.3
% 7.36/2.93 % (3951640)Termination reason: Instruction limit
% 7.36/2.93 % (3951640)Termination phase: shuffling
% 7.36/2.93 % (3951640)Time elapsed: 0.033 s
% 7.36/2.93 % (3951640)Peak memory usage: 17 MB
% 7.36/2.93 % (3951640)Instructions burned: 69 (million)
% 7.36/2.93 % (3951644)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 7.36/2.93 % (3951644)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2871014833:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2990 on theBenchmark for (2990ds/180Mi)
% 7.36/2.93 % (3951623)Instruction limit reached!
% 7.36/2.93 % (3951623)------------------------------
% 7.36/2.93 % (3951623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.36/2.93 % (3951623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.36/2.93 % (3951623)CaDiCaL version: 2.1.3
% 7.36/2.93 % (3951623)Termination reason: Instruction limit
% 7.36/2.93 % (3951623)Termination phase: Property scanning
% 7.36/2.93 % (3951623)Time elapsed: 0.207 s
% 7.36/2.93 % (3951623)Peak memory usage: 21 MB
% 7.36/2.93 % (3951623)Instructions burned: 480 (million)
% 7.36/2.93 % (3951646)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3006913667:cond=on:i=96:bd=all:rtra=on_2990 on theBenchmark for (2990ds/96Mi)
% 7.36/2.93 % (3951638)Instruction limit reached!
% 7.36/2.93 % (3951638)------------------------------
% 7.36/2.93 % (3951638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.36/2.93 % (3951638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.36/2.93 % (3951638)CaDiCaL version: 2.1.3
% 7.36/2.93 % (3951638)Termination reason: Instruction limit
% 7.36/2.93 % (3951638)Termination phase: shuffling
% 7.36/2.93 % (3951638)Time elapsed: 0.070 s
% 7.36/2.93 % (3951638)Peak memory usage: 18 MB
% 7.36/2.93 % (3951638)Instructions burned: 137 (million)
% 7.36/2.93 % (3951645)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=4287528474:st=2:i=246:sd=3:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/246Mi)
% 7.36/2.93 % (3951649)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=666891866:i=427:sd=1:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/427Mi)
% 7.36/2.93 % (3951651)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=973899995:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/874Mi)
% 7.36/2.93 % (3951596)Instruction limit reached!
% 7.36/2.93 % (3951596)------------------------------
% 7.36/2.93 % (3951596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.36/2.93 % (3951596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.36/2.93 % (3951596)CaDiCaL version: 2.1.3
% 7.36/2.93 % (3951596)Termination reason: Instruction limit
% 7.36/2.93 % (3951596)Termination phase: Property scanning
% 7.36/2.93 % (3951596)Time elapsed: 0.386 s
% 7.36/2.93 % (3951596)Peak memory usage: 29 MB
% 7.36/2.93 % (3951596)Instructions burned: 1243 (million)
% 7.36/2.93 % (3951646)Instruction limit reached!
% 7.36/2.93 % (3951646)------------------------------
% 7.36/2.93 % (3951646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.29/3.06 % (3951646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/3.06 % (3951646)CaDiCaL version: 2.1.3
% 9.29/3.06 % (3951646)Termination reason: Instruction limit
% 9.29/3.06 % (3951646)Termination phase: shuffling
% 9.29/3.06 % (3951646)Time elapsed: 0.061 s
% 9.29/3.06 % (3951646)Peak memory usage: 18 MB
% 9.29/3.06 % (3951646)Instructions burned: 97 (million)
% 9.29/3.06 % (3951654)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=273663938:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/515Mi)
% 9.29/3.06 % (3951655)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1114352383:st=1.5:i=130:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/130Mi)
% 9.29/3.06 % (3951644)Instruction limit reached!
% 9.29/3.06 % (3951644)------------------------------
% 9.29/3.06 % (3951644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.29/3.06 % (3951644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/3.06 % (3951644)CaDiCaL version: 2.1.3
% 9.29/3.06 % (3951644)Termination reason: Instruction limit
% 9.29/3.06 % (3951644)Termination phase: shuffling
% 9.29/3.06 % (3951644)Time elapsed: 0.102 s
% 9.29/3.06 % (3951644)Peak memory usage: 20 MB
% 9.29/3.06 % (3951644)Instructions burned: 181 (million)
% 9.29/3.06 % (3951658)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1196077497:i=44:ep=R:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/44Mi)
% 9.29/3.06 % (3951658)Instruction limit reached!
% 9.29/3.06 % (3951658)------------------------------
% 9.29/3.06 % (3951658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.29/3.06 % (3951658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/3.06 % (3951658)CaDiCaL version: 2.1.3
% 9.29/3.06 % (3951658)Termination reason: Instruction limit
% 9.29/3.06 % (3951658)Termination phase: shuffling
% 9.29/3.06 % (3951658)Time elapsed: 0.024 s
% 9.29/3.06 % (3951658)Peak memory usage: 17 MB
% 9.29/3.06 % (3951658)Instructions burned: 45 (million)
% 9.29/3.06 % (3951645)Instruction limit reached!
% 9.29/3.06 % (3951645)------------------------------
% 9.29/3.06 % (3951645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.29/3.06 % (3951645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/3.06 % (3951645)CaDiCaL version: 2.1.3
% 9.29/3.06 % (3951645)Termination reason: Instruction limit
% 9.29/3.06 % (3951645)Termination phase: shuffling
% 9.29/3.06 % (3951645)Time elapsed: 0.143 s
% 9.29/3.06 % (3951645)Peak memory usage: 20 MB
% 9.29/3.06 % (3951645)Instructions burned: 247 (million)
% 9.29/3.06 % (3951660)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=1011769942:s2a=on:i=571:nm=16:rtra=on_2989 on theBenchmark for (2989ds/571Mi)
% 9.29/3.06 % (3951655)Instruction limit reached!
% 9.29/3.06 % (3951655)------------------------------
% 9.29/3.06 % (3951655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.29/3.06 % (3951655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/3.06 % (3951655)CaDiCaL version: 2.1.3
% 9.29/3.06 % (3951655)Termination reason: Instruction limit
% 9.29/3.06 % (3951655)Termination phase: shuffling
% 9.29/3.06 % (3951655)Time elapsed: 0.087 s
% 9.29/3.06 % (3951655)Peak memory usage: 19 MB
% 9.29/3.06 % (3951655)Instructions burned: 130 (million)
% 9.29/3.06 % (3951662)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=219964134:i=450:rtra=on:ixr=off:ntd=on_2988 on theBenchmark for (2988ds/450Mi)
% 9.29/3.06 % (3951654)Instruction limit reached!
% 9.29/3.06 % (3951654)------------------------------
% 9.29/3.06 % (3951654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.29/3.06 % (3951654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/3.06 % (3951654)CaDiCaL version: 2.1.3
% 9.29/3.06 % (3951654)Termination reason: Instruction limit
% 9.29/3.06 % (3951654)Termination phase: Property scanning
% 9.29/3.06 % (3951654)Time elapsed: 0.120 s
% 9.29/3.06 % (3951654)Peak memory usage: 21 MB
% 9.29/3.06 % (3951654)Instructions burned: 518 (million)
% 9.29/3.06 % (3951666)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=3322992334:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2988 on theBenchmark for (2988ds/65Mi)
% 9.29/3.06 % (3951649)Instruction limit reached!
% 9.74/3.19 % (3951649)------------------------------
% 9.74/3.19 % (3951649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951649)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951649)Termination reason: Instruction limit
% 9.74/3.19 % (3951649)Termination phase: Property scanning
% 9.74/3.19 % (3951649)Time elapsed: 0.185 s
% 9.74/3.19 % (3951649)Peak memory usage: 21 MB
% 9.74/3.19 % (3951649)Instructions burned: 429 (million)
% 9.74/3.19 % (3951664)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1916437742:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/95Mi)
% 9.74/3.19 % (3951666)Instruction limit reached!
% 9.74/3.19 % (3951666)------------------------------
% 9.74/3.19 % (3951666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951666)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951666)Termination reason: Instruction limit
% 9.74/3.19 % (3951666)Termination phase: shuffling
% 9.74/3.19 % (3951666)Time elapsed: 0.019 s
% 9.74/3.19 % (3951666)Peak memory usage: 18 MB
% 9.74/3.19 % (3951666)Instructions burned: 69 (million)
% 9.74/3.19 % (3951670)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=3720077670:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2988 on theBenchmark for (2988ds/5755Mi)
% 9.74/3.19 % (3951668)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=1735182460:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2988 on theBenchmark for (2988ds/105Mi)
% 9.74/3.19 % (3951664)Instruction limit reached!
% 9.74/3.19 % (3951664)------------------------------
% 9.74/3.19 % (3951664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951664)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951664)Termination reason: Instruction limit
% 9.74/3.19 % (3951664)Termination phase: shuffling
% 9.74/3.19 % (3951664)Time elapsed: 0.061 s
% 9.74/3.19 % (3951664)Peak memory usage: 18 MB
% 9.74/3.19 % (3951664)Instructions burned: 97 (million)
% 9.74/3.19 % (3951668)Instruction limit reached!
% 9.74/3.19 % (3951668)------------------------------
% 9.74/3.19 % (3951668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951668)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951668)Termination reason: Instruction limit
% 9.74/3.19 % (3951668)Termination phase: shuffling
% 9.74/3.19 % (3951668)Time elapsed: 0.050 s
% 9.74/3.19 % (3951668)Peak memory usage: 18 MB
% 9.74/3.19 % (3951668)Instructions burned: 107 (million)
% 9.74/3.19 % (3951673)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=3148984015:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/375Mi)
% 9.74/3.19 % (3951674)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1671984884:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2987 on theBenchmark for (2987ds/495Mi)
% 9.74/3.19 % (3951619)Instruction limit reached!
% 9.74/3.19 % (3951619)------------------------------
% 9.74/3.19 % (3951619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951619)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951619)Termination reason: Instruction limit
% 9.74/3.19 % (3951619)Termination phase: Preprocessing 1
% 9.74/3.19 % (3951619)Time elapsed: 0.544 s
% 9.74/3.19 % (3951619)Peak memory usage: 21 MB
% 9.74/3.19 % (3951619)Instructions burned: 854 (million)
% 9.74/3.19 % (3951677)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=1015586538:cond=on:i=34:hud=10:nm=10:rtra=on_2987 on theBenchmark for (2987ds/34Mi)
% 9.74/3.19 % (3951677)Instruction limit reached!
% 9.74/3.19 % (3951677)------------------------------
% 9.74/3.19 % (3951677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951677)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951677)Termination reason: Instruction limit
% 9.74/3.19 % (3951677)Termination phase: shuffling
% 9.74/3.19 % (3951677)Time elapsed: 0.021 s
% 9.74/3.19 % (3951677)Peak memory usage: 17 MB
% 9.74/3.19 % (3951677)Instructions burned: 36 (million)
% 9.74/3.19 % (3951679)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2532417796:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2986 on theBenchmark for (2986ds/91Mi)
% 9.74/3.19 % (3951660)Instruction limit reached!
% 9.74/3.19 % (3951660)------------------------------
% 9.74/3.19 % (3951660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951660)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951660)Termination reason: Instruction limit
% 9.74/3.19 % (3951660)Termination phase: SInE selection
% 9.74/3.19 % (3951660)Time elapsed: 0.249 s
% 9.74/3.19 % (3951660)Peak memory usage: 21 MB
% 9.74/3.19 % (3951660)Instructions burned: 571 (million)
% 9.74/3.19 % (3951681)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=3485105584:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2986 on theBenchmark for (2986ds/66Mi)
% 9.74/3.19 % (3951679)Instruction limit reached!
% 9.74/3.19 % (3951679)------------------------------
% 9.74/3.19 % (3951679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951679)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951679)Termination reason: Instruction limit
% 9.74/3.19 % (3951679)Termination phase: shuffling
% 9.74/3.19 % (3951679)Time elapsed: 0.044 s
% 9.74/3.19 % (3951679)Peak memory usage: 17 MB
% 9.74/3.19 % (3951679)Instructions burned: 91 (million)
% 9.74/3.19 % (3951673)Instruction limit reached!
% 9.74/3.19 % (3951673)------------------------------
% 9.74/3.19 % (3951673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951673)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951673)Termination reason: Instruction limit
% 9.74/3.19 % (3951673)Termination phase: Property scanning
% 9.74/3.19 % (3951673)Time elapsed: 0.162 s
% 9.74/3.19 % (3951673)Peak memory usage: 21 MB
% 9.74/3.19 % (3951673)Instructions burned: 377 (million)
% 9.74/3.19 % (3951683)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3263000284:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2986 on theBenchmark for (2986ds/22Mi)
% 9.74/3.19 % (3951681)Instruction limit reached!
% 9.74/3.19 % (3951681)------------------------------
% 9.74/3.19 % (3951681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951681)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951681)Termination reason: Instruction limit
% 9.74/3.19 % (3951681)Termination phase: shuffling
% 9.74/3.19 % (3951681)Time elapsed: 0.033 s
% 9.74/3.19 % (3951681)Peak memory usage: 17 MB
% 9.74/3.19 % (3951681)Instructions burned: 66 (million)
% 9.74/3.19 % (3951683)Instruction limit reached!
% 9.74/3.19 % (3951683)------------------------------
% 9.74/3.19 % (3951683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951683)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951683)Termination reason: Instruction limit
% 9.74/3.19 % (3951683)Termination phase: shuffling
% 9.74/3.19 % (3951683)Time elapsed: 0.015 s
% 9.74/3.19 % (3951683)Peak memory usage: 16 MB
% 9.74/3.19 % (3951683)Instructions burned: 24 (million)
% 9.74/3.19 % (3951685)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=1873475324:i=338:bd=all:ins=4:rtra=on_2985 on theBenchmark for (2985ds/338Mi)
% 9.74/3.19 % (3951686)lrs+10_1_sil=128000:si=on:urr=on:random_seed=595609254:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/28Mi)
% 9.74/3.19 % (3951687)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 9.74/3.19 % (3951674)Instruction limit reached!
% 9.74/3.19 % (3951674)------------------------------
% 9.74/3.19 % (3951674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951674)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951674)Termination reason: Instruction limit
% 9.74/3.19 % (3951674)Termination phase: Property scanning
% 9.74/3.19 % (3951674)Time elapsed: 0.211 s
% 9.74/3.19 % (3951674)Peak memory usage: 21 MB
% 9.74/3.19 % (3951674)Instructions burned: 495 (million)
% 9.74/3.19 % (3951687)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=1315402630:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2985 on theBenchmark for (2985ds/137Mi)
% 9.74/3.19 % (3951686)Instruction limit reached!
% 9.74/3.19 % (3951686)------------------------------
% 9.74/3.19 % (3951686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951686)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951686)Termination reason: Instruction limit
% 9.74/3.19 % (3951686)Termination phase: shuffling
% 9.74/3.19 % (3951686)Time elapsed: 0.018 s
% 9.74/3.19 % (3951686)Peak memory usage: 17 MB
% 9.74/3.19 % (3951686)Instructions burned: 30 (million)
% 9.74/3.19 % (3951691)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=1806141756:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2985 on theBenchmark for (2985ds/340Mi)
% 9.74/3.19 % (3951692)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=1220887240:i=227:sd=1:bd=all:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/227Mi)
% 9.74/3.19 % (3951662)Instruction limit reached!
% 9.74/3.19 % (3951662)------------------------------
% 9.74/3.19 % (3951662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951662)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951662)Termination reason: Instruction limit
% 9.74/3.19 % (3951662)Termination phase: Property scanning
% 9.74/3.19 % (3951662)Time elapsed: 0.370 s
% 9.74/3.19 % (3951662)Peak memory usage: 21 MB
% 9.74/3.19 % (3951662)Instructions burned: 451 (million)
% 9.74/3.19 % (3951695)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 9.74/3.19 % (3951687)Instruction limit reached!
% 9.74/3.19 % (3951687)------------------------------
% 9.74/3.19 % (3951687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.19 % (3951687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.19 % (3951687)CaDiCaL version: 2.1.3
% 9.74/3.19 % (3951687)Termination reason: Instruction limit
% 9.74/3.19 % (3951687)Termination phase: shuffling
% 9.74/3.19 % (3951687)Time elapsed: 0.065 s
% 9.74/3.19 % (3951687)Peak memory usage: 19 MB
% 9.74/3.19 % (3951687)Instructions burned: 137 (million)
% 9.74/3.19 % (3951695)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=3180639913:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/373Mi)
% 9.74/3.19 % (3951697)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=1331659150:i=116:ep=RSTC:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/116Mi)
% 9.74/3.19 % (3951670) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3951531-3951670"...
% 9.74/3.19 % (3951670)...printing done.
% 9.74/3.19 % (3951670)Refutation found. Thanks to Tanya!
% 9.74/3.19 % SZS status Theorem for theBenchmark
% 9.74/3.19 % SZS output start Proof for theBenchmark
% 9.74/3.19 thf(type_def_5, type, code_code_numeral: $tType).
% 9.74/3.19 thf(type_def_6, type, complex: $tType).
% 9.74/3.19 thf(type_def_7, type, int: $tType).
% 9.74/3.19 thf(type_def_8, type, filter_complex: $tType).
% 9.74/3.19 thf(type_def_9, type, filter_nat: $tType).
% 9.74/3.19 thf(type_def_10, type, filter_real: $tType).
% 9.74/3.19 thf(type_def_11, type, list_int: $tType).
% 9.74/3.19 thf(type_def_12, type, nat: $tType).
% 9.74/3.19 thf(type_def_13, type, quickcheck_code_int: $tType).
% 9.74/3.19 thf(type_def_14, type, rat: $tType).
% 9.74/3.19 thf(type_def_15, type, real: $tType).
% 9.74/3.19 thf(type_def_16, type, produc975137661_int_o: $tType).
% 9.74/3.19 thf(type_def_17, type, produc1359518119umeral: $tType).
% 9.74/3.19 thf(type_def_18, type, product_prod_int_int: $tType).
% 9.74/3.19 thf(type_def_19, type, produc393999548nt_int: $tType).
% 9.74/3.19 thf(type_def_20, type, product_prod_nat_nat: $tType).
% 9.74/3.19 thf(type_def_21, type, produc167071911de_int: $tType).
% 9.74/3.19 thf(type_def_22, type, produc914805421l_real: $tType).
% 9.74/3.19 thf(type_def_23, type, produc1137372701nt_int: $tType).
% 9.74/3.19 thf(type_def_24, type, produc1322466333at_nat: $tType).
% 9.74/3.19 thf(type_def_25, type, sTfun: ($tType * $tType) > $tType).
% 9.74/3.19 thf(func_def_0, type, all: ((nat > $o) > $o)).
% 9.74/3.19 thf(func_def_1, type, archim856651990g_real: (real > int)).
% 9.74/3.19 thf(func_def_2, type, archim791455193or_rat: (rat > int)).
% 9.74/3.19 thf(func_def_3, type, archim1246769320r_real: (real > int)).
% 9.74/3.19 thf(func_def_4, type, big_co1971440592_o_nat: (((int > $o) > nat) > ((int > $o) > $o) > nat)).
% 9.74/3.19 thf(func_def_5, type, big_co230513141nt_int: ((int > int) > (int > $o) > int)).
% 9.74/3.19 thf(func_def_6, type, big_co1024481617at_int: ((nat > int) > (nat > $o) > int)).
% 9.74/3.19 thf(func_def_7, type, big_co387207925at_nat: ((nat > nat) > (nat > $o) > nat)).
% 9.74/3.19 thf(func_def_8, type, big_co604158596t_real: ((nat > real) > (nat > $o) > real)).
% 9.74/3.19 thf(func_def_9, type, big_co1548731110nt_int: ((int > int) > (int > $o) > int)).
% 9.74/3.19 thf(func_def_10, type, big_co1705425894at_nat: ((nat > nat) > (nat > $o) > nat)).
% 9.74/3.19 thf(func_def_11, type, bijR_int_int: ((int > int > $o) > produc975137661_int_o > $o)).
% 9.74/3.19 thf(func_def_12, type, code_S1047413653umeral: (code_code_numeral > code_code_numeral)).
% 9.74/3.19 thf(func_def_13, type, code_c271388182l_size: (code_code_numeral > nat)).
% 9.74/3.19 thf(func_def_14, type, code_d418564891umeral: (code_code_numeral > code_code_numeral > produc1359518119umeral)).
% 9.74/3.19 thf(func_def_15, type, code_int_of: (code_code_numeral > int)).
% 9.74/3.19 thf(func_def_16, type, code_nat_of_aux: (code_code_numeral > nat > nat)).
% 9.74/3.19 thf(func_def_17, type, comple1092985777_int_o: (((int > $o) > $o) > int > $o)).
% 9.74/3.19 thf(func_def_18, type, comple124823625p_real: ((real > $o) > real)).
% 9.74/3.19 thf(func_def_19, type, im: (complex > real)).
% 9.74/3.19 thf(func_def_20, type, re: (complex > real)).
% 9.74/3.19 thf(func_def_21, type, arg: (complex > real)).
% 9.74/3.19 thf(func_def_22, type, cis: (real > complex)).
% 9.74/3.19 thf(func_def_23, type, cnj: (complex > complex)).
% 9.74/3.19 thf(func_def_24, type, complex_1: (real > real > complex)).
% 9.74/3.19 thf(func_def_25, type, complex_size: (complex > nat)).
% 9.74/3.19 thf(func_def_26, type, expi: (complex > complex)).
% 9.74/3.19 thf(func_def_27, type, ii: complex).
% 9.74/3.19 thf(func_def_28, type, rcis: (real > real > complex)).
% 9.74/3.19 thf(func_def_29, type, bolzano_bisect: ((produc914805421l_real > $o) > real > real > nat > produc914805421l_real)).
% 9.74/3.19 thf(func_def_30, type, deriv_real: ((real > real) > real > real > $o)).
% 9.74/3.19 thf(func_def_31, type, adjust: (int > product_prod_int_int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_32, type, div_di1218280263umeral: (code_code_numeral > code_code_numeral > code_code_numeral)).
% 9.74/3.19 thf(func_def_33, type, div_div_int: (int > int > int)).
% 9.74/3.19 thf(func_def_34, type, div_div_nat: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_35, type, div_di1430059507de_int: (quickcheck_code_int > quickcheck_code_int > quickcheck_code_int)).
% 9.74/3.19 thf(func_def_36, type, div_mo1740067990umeral: (code_code_numeral > code_code_numeral > code_code_numeral)).
% 9.74/3.19 thf(func_def_37, type, div_mod_int: (int > int > int)).
% 9.74/3.19 thf(func_def_38, type, div_mod_nat: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_39, type, div_mo231679042de_int: (quickcheck_code_int > quickcheck_code_int > quickcheck_code_int)).
% 9.74/3.19 thf(func_def_40, type, divmod_int: (int > int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_41, type, divmod_int_rel: (int > int > product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_42, type, divmod_nat: (nat > nat > product_prod_nat_nat)).
% 9.74/3.19 thf(func_def_43, type, divmod_nat_rel: (nat > nat > product_prod_nat_nat > $o)).
% 9.74/3.19 thf(func_def_44, type, negDivAlg: (int > int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_45, type, negDivAlg_rel: (product_prod_int_int > product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_46, type, negateSnd: (product_prod_int_int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_47, type, pdivmod: (int > int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_48, type, posDivAlg: (int > int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_49, type, posDivAlg_rel: (product_prod_int_int > product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_50, type, bnorRset: (int > int > int > $o)).
% 9.74/3.19 thf(func_def_51, type, rRset2norRR: ((int > $o) > int > int > int)).
% 9.74/3.19 thf(func_def_52, type, rsetR: (int > (int > $o) > $o)).
% 9.74/3.19 thf(func_def_53, type, is_RRset: ((int > $o) > int > $o)).
% 9.74/3.19 thf(func_def_54, type, noXRRset: (int > int > int > $o)).
% 9.74/3.19 thf(func_def_55, type, norRRset: (int > int > $o)).
% 9.74/3.19 thf(func_def_56, type, phi: (int > nat)).
% 9.74/3.19 thf(func_def_57, type, zcongm: (int > int > int > $o)).
% 9.74/3.19 thf(func_def_58, type, multInvPair: (int > int > int > int > $o)).
% 9.74/3.19 thf(func_def_59, type, setS: (int > int > (int > $o) > $o)).
% 9.74/3.19 thf(func_def_60, type, zEven: (int > $o)).
% 9.74/3.19 thf(func_def_61, type, zOdd: (int > $o)).
% 9.74/3.19 thf(func_def_62, type, fact_fact_int: (int > int)).
% 9.74/3.19 thf(func_def_63, type, fact_fact_nat: (nat > nat)).
% 9.74/3.19 thf(func_def_64, type, invers1025623611omplex: (complex > complex > complex)).
% 9.74/3.19 thf(func_def_65, type, inverse_divide_rat: (rat > rat > rat)).
% 9.74/3.19 thf(func_def_66, type, inverse_divide_real: (real > real > real)).
% 9.74/3.19 thf(func_def_67, type, invers1449016382omplex: (complex > complex)).
% 9.74/3.19 thf(func_def_68, type, inverse_inverse_rat: (rat > rat)).
% 9.74/3.19 thf(func_def_69, type, inverse_inverse_real: (real > real)).
% 9.74/3.19 thf(func_def_70, type, finite_card_int_o: (((int > $o) > $o) > nat)).
% 9.74/3.19 thf(func_def_71, type, finite_card_int: ((int > $o) > nat)).
% 9.74/3.19 thf(func_def_72, type, finite_card_nat: ((nat > $o) > nat)).
% 9.74/3.19 thf(func_def_73, type, finite_finite_int_o: (((int > $o) > $o) > $o)).
% 9.74/3.19 thf(func_def_74, type, finite_finite_int: ((int > $o) > $o)).
% 9.74/3.19 thf(func_def_75, type, finite_finite_nat: ((nat > $o) > $o)).
% 9.74/3.19 thf(func_def_76, type, pair_leq: (produc1322466333at_nat > $o)).
% 9.74/3.19 thf(func_def_77, type, pair_less: (produc1322466333at_nat > $o)).
% 9.74/3.19 thf(func_def_78, type, bezw: (nat > nat > product_prod_int_int)).
% 9.74/3.19 thf(func_def_79, type, gcd_gcd_int: (int > int > int)).
% 9.74/3.19 thf(func_def_80, type, gcd_gcd_nat: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_81, type, abs_abs_int: (int > int)).
% 9.74/3.19 thf(func_def_82, type, abs_abs_rat: (rat > rat)).
% 9.74/3.19 thf(func_def_83, type, abs_abs_real: (real > real)).
% 9.74/3.19 thf(func_def_84, type, minus_1690775515umeral: (code_code_numeral > code_code_numeral > code_code_numeral)).
% 9.74/3.19 thf(func_def_85, type, minus_minus_complex: (complex > complex > complex)).
% 9.74/3.19 thf(func_def_86, type, minus_minus_int: (int > int > int)).
% 9.74/3.19 thf(func_def_87, type, minus_minus_nat: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_88, type, minus_534354567de_int: (quickcheck_code_int > quickcheck_code_int > quickcheck_code_int)).
% 9.74/3.19 thf(func_def_89, type, minus_minus_rat: (rat > rat > rat)).
% 9.74/3.19 thf(func_def_90, type, minus_minus_real: (real > real > real)).
% 9.74/3.19 thf(func_def_91, type, one_on1645066479umeral: code_code_numeral).
% 9.74/3.19 thf(func_def_92, type, one_one_complex: complex).
% 9.74/3.19 thf(func_def_93, type, one_one_int: int).
% 9.74/3.19 thf(func_def_94, type, one_one_nat: nat).
% 9.74/3.19 thf(func_def_95, type, one_on1684967323de_int: quickcheck_code_int).
% 9.74/3.19 thf(func_def_96, type, one_one_rat: rat).
% 9.74/3.19 thf(func_def_97, type, one_one_real: real).
% 9.74/3.19 thf(func_def_98, type, plus_p1627245867umeral: (code_code_numeral > code_code_numeral > code_code_numeral)).
% 9.74/3.19 thf(func_def_99, type, plus_plus_complex: (complex > complex > complex)).
% 9.74/3.19 thf(func_def_100, type, plus_plus_int: (int > int > int)).
% 9.74/3.19 thf(func_def_101, type, plus_plus_nat: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_102, type, plus_p1446045655de_int: (quickcheck_code_int > quickcheck_code_int > quickcheck_code_int)).
% 9.74/3.19 thf(func_def_103, type, plus_plus_rat: (rat > rat > rat)).
% 9.74/3.19 thf(func_def_104, type, plus_plus_real: (real > real > real)).
% 9.74/3.19 thf(func_def_105, type, sgn_sgn_complex: (complex > complex)).
% 9.74/3.19 thf(func_def_106, type, sgn_sgn_int: (int > int)).
% 9.74/3.19 thf(func_def_107, type, sgn_sgn_rat: (rat > rat)).
% 9.74/3.19 thf(func_def_108, type, sgn_sgn_real: (real > real)).
% 9.74/3.19 thf(func_def_109, type, times_1655362735umeral: (code_code_numeral > code_code_numeral > code_code_numeral)).
% 9.74/3.19 thf(func_def_110, type, times_times_complex: (complex > complex > complex)).
% 9.74/3.19 thf(func_def_111, type, times_times_int: (int > int > int)).
% 9.74/3.19 thf(func_def_112, type, times_times_nat: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_113, type, times_123202395de_int: (quickcheck_code_int > quickcheck_code_int > quickcheck_code_int)).
% 9.74/3.19 thf(func_def_114, type, times_times_rat: (rat > rat > rat)).
% 9.74/3.19 thf(func_def_115, type, times_times_real: (real > real > real)).
% 9.74/3.19 thf(func_def_116, type, uminus473333897omplex: (complex > complex)).
% 9.74/3.19 thf(func_def_117, type, uminus_uminus_int: (int > int)).
% 9.74/3.19 thf(func_def_118, type, uminus_uminus_rat: (rat > rat)).
% 9.74/3.19 thf(func_def_119, type, uminus_uminus_real: (real > real)).
% 9.74/3.19 thf(func_def_120, type, zero_z126310315umeral: code_code_numeral).
% 9.74/3.19 thf(func_def_121, type, zero_zero_complex: complex).
% 9.74/3.19 thf(func_def_122, type, zero_zero_int: int).
% 9.74/3.19 thf(func_def_123, type, zero_zero_nat: nat).
% 9.74/3.19 thf(func_def_124, type, zero_z891286103de_int: quickcheck_code_int).
% 9.74/3.19 thf(func_def_125, type, zero_zero_rat: rat).
% 9.74/3.19 thf(func_def_126, type, zero_zero_real: real).
% 9.74/3.19 thf(func_def_127, type, the_int: ((int > $o) > int)).
% 9.74/3.19 thf(func_def_128, type, the_real: ((real > $o) > real)).
% 9.74/3.19 thf(func_def_129, type, the_Pr2103884470nt_int: ((product_prod_int_int > $o) > product_prod_int_int)).
% 9.74/3.19 thf(func_def_130, type, the_Pr588456374at_nat: ((product_prod_nat_nat > $o) > product_prod_nat_nat)).
% 9.74/3.19 thf(func_def_131, type, hilbert_Eps_int: ((int > $o) > int)).
% 9.74/3.19 thf(func_def_132, type, hilbert_Eps_real: ((real > $o) > real)).
% 9.74/3.19 thf(func_def_133, type, if_int: ($o > int > int > int)).
% 9.74/3.19 thf(func_def_134, type, if_nat: ($o > nat > nat > nat)).
% 9.74/3.19 thf(func_def_135, type, if_real: ($o > real > real > real)).
% 9.74/3.19 thf(func_def_136, type, if_Pro1731782967nt_int: ($o > product_prod_int_int > product_prod_int_int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_137, type, if_Pro313124157l_real: ($o > produc914805421l_real > produc914805421l_real > produc914805421l_real)).
% 9.74/3.19 thf(func_def_138, type, multInv: (int > int > int)).
% 9.74/3.19 thf(func_def_139, type, d22set: (int > int > $o)).
% 9.74/3.19 thf(func_def_140, type, zfact: (int > int)).
% 9.74/3.19 thf(func_def_141, type, xzgcd: (int > int > produc393999548nt_int)).
% 9.74/3.19 thf(func_def_142, type, xzgcda: (int > int > int > int > int > int > int > int > produc393999548nt_int)).
% 9.74/3.19 thf(func_def_143, type, zcong: (int > int > int > $o)).
% 9.74/3.19 thf(func_def_144, type, zprime: (int > $o)).
% 9.74/3.19 thf(func_def_145, type, bit0: (int > int)).
% 9.74/3.19 thf(func_def_146, type, bit1: (int > int)).
% 9.74/3.19 thf(func_def_147, type, min: int).
% 9.74/3.19 thf(func_def_148, type, pls: int).
% 9.74/3.19 thf(func_def_149, type, int_ge_less_than: (int > product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_150, type, int_ge_less_than2: (int > product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_151, type, iszero_int: (int > $o)).
% 9.74/3.19 thf(func_def_152, type, iszero_rat: (rat > $o)).
% 9.74/3.19 thf(func_def_153, type, nat_1: (int > nat)).
% 9.74/3.19 thf(func_def_154, type, nat_aux: (int > nat > nat)).
% 9.74/3.19 thf(func_def_155, type, number1443263063umeral: (int > code_code_numeral)).
% 9.74/3.19 thf(func_def_156, type, number528085621omplex: (int > complex)).
% 9.74/3.19 thf(func_def_157, type, number_number_of_int: (int > int)).
% 9.74/3.19 thf(func_def_158, type, number_number_of_nat: (int > nat)).
% 9.74/3.19 thf(func_def_159, type, number1226105091de_int: (int > quickcheck_code_int)).
% 9.74/3.19 thf(func_def_160, type, number_number_of_rat: (int > rat)).
% 9.74/3.19 thf(func_def_161, type, number267125858f_real: (int > real)).
% 9.74/3.19 thf(func_def_162, type, pred: (int > int)).
% 9.74/3.19 thf(func_def_163, type, ring_1_Ints_real: (real > $o)).
% 9.74/3.19 thf(func_def_164, type, ring_11397209091omplex: (int > complex)).
% 9.74/3.19 thf(func_def_165, type, ring_1_of_int_int: (int > int)).
% 9.74/3.19 thf(func_def_166, type, ring_1_of_int_rat: (int > rat)).
% 9.74/3.19 thf(func_def_167, type, ring_1_of_int_real: (int > real)).
% 9.74/3.19 thf(func_def_168, type, succ: (int > int)).
% 9.74/3.19 thf(func_def_169, type, lazy_small_lazy_rel: (product_prod_int_int > product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_170, type, legacy_zgcd: (int > int > int)).
% 9.74/3.19 thf(func_def_171, type, isCont156215680omplex: ((complex > complex) > complex > $o)).
% 9.74/3.19 thf(func_def_172, type, isCont_complex_real: ((complex > real) > complex > $o)).
% 9.74/3.19 thf(func_def_173, type, isCont_real_real: ((real > real) > real > $o)).
% 9.74/3.19 thf(func_def_174, type, at_complex: (complex > filter_complex)).
% 9.74/3.19 thf(func_def_175, type, at_real: (real > filter_real)).
% 9.74/3.19 thf(func_def_176, type, sequentially: filter_nat).
% 9.74/3.19 thf(func_def_177, type, tendst1507391555omplex: ((complex > complex) > complex > filter_complex > $o)).
% 9.74/3.19 thf(func_def_178, type, tendsto_complex_real: ((complex > real) > real > filter_complex > $o)).
% 9.74/3.19 thf(func_def_179, type, tendsto_nat_complex: ((nat > complex) > complex > filter_nat > $o)).
% 9.74/3.19 thf(func_def_180, type, tendsto_nat_real: ((nat > real) > real > filter_nat > $o)).
% 9.74/3.19 thf(func_def_181, type, tendsto_real_real: ((real > real) > real > filter_real > $o)).
% 9.74/3.19 thf(func_def_182, type, trivial_limit_nat: (filter_nat > $o)).
% 9.74/3.19 thf(func_def_183, type, upto_rel: (product_prod_int_int > product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_184, type, log: (real > real > real)).
% 9.74/3.19 thf(func_def_185, type, powr: (real > real > real)).
% 9.74/3.19 thf(func_def_186, type, suc: (nat > nat)).
% 9.74/3.19 thf(func_def_187, type, nat_case_o: ($o > (nat > $o) > nat > $o)).
% 9.74/3.19 thf(func_def_188, type, nat_case_nat: (nat > (nat > nat) > nat > nat)).
% 9.74/3.19 thf(func_def_189, type, nat_size: (nat > nat)).
% 9.74/3.19 thf(func_def_190, type, semiri1619134803umeral: (nat > code_code_numeral)).
% 9.74/3.19 thf(func_def_191, type, semiri2020571505omplex: (nat > complex)).
% 9.74/3.19 thf(func_def_192, type, semiri1621563631at_int: (nat > int)).
% 9.74/3.19 thf(func_def_193, type, semiri984289939at_nat: (nat > nat)).
% 9.74/3.19 thf(func_def_194, type, semiri1424489471de_int: (nat > quickcheck_code_int)).
% 9.74/3.19 thf(func_def_195, type, semiri151668891at_rat: (nat > rat)).
% 9.74/3.19 thf(func_def_196, type, semiri132038758t_real: (nat > real)).
% 9.74/3.19 thf(func_def_197, type, size_s945831648umeral: (code_code_numeral > nat)).
% 9.74/3.19 thf(func_def_198, type, size_size_complex: (complex > nat)).
% 9.74/3.19 thf(func_def_199, type, size_size_list_int: (list_int > nat)).
% 9.74/3.19 thf(func_def_200, type, size_size_nat: (nat > nat)).
% 9.74/3.19 thf(func_def_201, type, nat_neg: (int > $o)).
% 9.74/3.19 thf(func_def_202, type, nat_is_nat: (int > $o)).
% 9.74/3.19 thf(func_def_203, type, nat_nat_set: ((int > $o) > $o)).
% 9.74/3.19 thf(func_def_204, type, nat_tr876908586nt_nat: ((int > nat) > (int > $o) > $o)).
% 9.74/3.19 thf(func_def_205, type, nat_tr160667106at_int: ((nat > int) > (nat > $o) > $o)).
% 9.74/3.19 thf(func_def_206, type, nat_tsub: (int > int > int)).
% 9.74/3.19 thf(func_def_207, type, frac: (product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_208, type, int_gcd: (int > int > int)).
% 9.74/3.19 thf(func_def_209, type, int_lcm: (int > int > int)).
% 9.74/3.19 thf(func_def_210, type, nat_gcd: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_211, type, nat_gcd_rel: (product_prod_nat_nat > product_prod_nat_nat > $o)).
% 9.74/3.19 thf(func_def_212, type, nat_lcm: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_213, type, norm_frac: (int > int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_214, type, norm_frac_rel: (product_prod_int_int > product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_215, type, root: (nat > real > real)).
% 9.74/3.19 thf(func_def_216, type, sqrt: (real > real)).
% 9.74/3.19 thf(func_def_217, type, ord_less_int_o: ((int > $o) > (int > $o) > $o)).
% 9.74/3.19 thf(func_def_218, type, ord_less_nat_o: ((nat > $o) > (nat > $o) > $o)).
% 9.74/3.19 thf(func_def_219, type, ord_le1304079648umeral: (code_code_numeral > code_code_numeral > $o)).
% 9.74/3.19 thf(func_def_220, type, ord_less_int: (int > int > $o)).
% 9.74/3.19 thf(func_def_221, type, ord_less_nat: (nat > nat > $o)).
% 9.74/3.19 thf(func_def_222, type, ord_le1860547276de_int: (quickcheck_code_int > quickcheck_code_int > $o)).
% 9.74/3.19 thf(func_def_223, type, ord_less_rat: (rat > rat > $o)).
% 9.74/3.19 thf(func_def_224, type, ord_less_real: (real > real > $o)).
% 9.74/3.19 thf(func_def_225, type, ord_less_eq_int_o: ((int > $o) > (int > $o) > $o)).
% 9.74/3.19 thf(func_def_226, type, ord_less_eq_nat_o: ((nat > $o) > (nat > $o) > $o)).
% 9.74/3.19 thf(func_def_227, type, ord_less_eq_o: ($o > $o > $o)).
% 9.74/3.19 thf(func_def_228, type, ord_le565307924umeral: (code_code_numeral > code_code_numeral > $o)).
% 9.74/3.19 thf(func_def_229, type, ord_less_eq_int: (int > int > $o)).
% 9.74/3.19 thf(func_def_230, type, ord_less_eq_nat: (nat > nat > $o)).
% 9.74/3.19 thf(func_def_231, type, ord_le258702272de_int: (quickcheck_code_int > quickcheck_code_int > $o)).
% 9.74/3.19 thf(func_def_232, type, ord_less_eq_rat: (rat > rat > $o)).
% 9.74/3.19 thf(func_def_233, type, ord_less_eq_real: (real > real > $o)).
% 9.74/3.19 thf(func_def_234, type, ord_max_nat: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_235, type, ord_min_nat: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_236, type, even_odd_even_int: (int > $o)).
% 9.74/3.19 thf(func_def_237, type, even_odd_even_nat: (nat > $o)).
% 9.74/3.19 thf(func_def_238, type, power_2100829034umeral: (code_code_numeral > nat > code_code_numeral)).
% 9.74/3.19 thf(func_def_239, type, power_power_complex: (complex > nat > complex)).
% 9.74/3.19 thf(func_def_240, type, power_power_int: (int > nat > int)).
% 9.74/3.19 thf(func_def_241, type, power_power_nat: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_242, type, power_881366806de_int: (quickcheck_code_int > nat > quickcheck_code_int)).
% 9.74/3.19 thf(func_def_243, type, power_power_rat: (rat > nat > rat)).
% 9.74/3.19 thf(func_def_244, type, power_power_real: (real > nat > real)).
% 9.74/3.19 thf(func_def_245, type, coprime: (nat > nat > $o)).
% 9.74/3.19 thf(func_def_246, type, fact: (nat > nat)).
% 9.74/3.19 thf(func_def_247, type, prime: (nat > $o)).
% 9.74/3.19 thf(func_def_248, type, produc398918003_int_o: ((int > $o) > (int > $o) > produc975137661_int_o)).
% 9.74/3.19 thf(func_def_249, type, produc2136830103umeral: (code_code_numeral > code_code_numeral > produc1359518119umeral)).
% 9.74/3.19 thf(func_def_250, type, product_Pair_int_int: (int > int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_251, type, produc282740534nt_int: (int > product_prod_int_int > produc393999548nt_int)).
% 9.74/3.19 thf(func_def_252, type, product_Pair_nat_nat: (nat > nat > product_prod_nat_nat)).
% 9.74/3.19 thf(func_def_253, type, produc1318306967de_int: (quickcheck_code_int > quickcheck_code_int > produc167071911de_int)).
% 9.74/3.19 thf(func_def_254, type, produc865579683l_real: (real > real > produc914805421l_real)).
% 9.74/3.19 thf(func_def_255, type, produc883642259nt_int: (product_prod_int_int > product_prod_int_int > produc1137372701nt_int)).
% 9.74/3.19 thf(func_def_256, type, produc494345619at_nat: (product_prod_nat_nat > product_prod_nat_nat > produc1322466333at_nat)).
% 9.74/3.19 thf(func_def_257, type, produc713050258nt_int: ((int > int) > product_prod_int_int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_258, type, product_fst_int_int: (product_prod_int_int > int)).
% 9.74/3.19 thf(func_def_259, type, product_fst_nat_nat: (product_prod_nat_nat > nat)).
% 9.74/3.19 thf(func_def_260, type, produc1935615926l_real: (produc914805421l_real > real)).
% 9.74/3.19 thf(func_def_261, type, produc450523309_int_o: ((int > int > $o) > product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_262, type, produc1298267108nt_int: ((int > int > int) > product_prod_int_int > int)).
% 9.74/3.19 thf(func_def_263, type, produc1518849193nt_int: ((int > int > product_prod_int_int) > product_prod_int_int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_264, type, produc1038563245_nat_o: ((nat > nat > $o) > product_prod_nat_nat > $o)).
% 9.74/3.19 thf(func_def_265, type, produc1391996073at_nat: ((nat > nat > product_prod_nat_nat) > product_prod_nat_nat > product_prod_nat_nat)).
% 9.74/3.19 thf(func_def_266, type, produc595218619l_real: ((real > real > produc914805421l_real) > produc914805421l_real > produc914805421l_real)).
% 9.74/3.19 thf(func_def_267, type, produc141074865_int_o: ((product_prod_int_int > product_prod_int_int > $o) > produc1137372701nt_int > $o)).
% 9.74/3.19 thf(func_def_268, type, product_snd_int_int: (product_prod_int_int > int)).
% 9.74/3.19 thf(func_def_269, type, product_snd_nat_nat: (product_prod_nat_nat > nat)).
% 9.74/3.19 thf(func_def_270, type, produc556554744l_real: (produc914805421l_real > real)).
% 9.74/3.19 thf(func_def_271, type, quickc666637781d_zero: (int > list_int)).
% 9.74/3.19 thf(func_def_272, type, quickc1265749348ro_rel: (int > int > $o)).
% 9.74/3.19 thf(func_def_273, type, quickc495462417de_int: (quickcheck_code_int > quickcheck_code_int > produc167071911de_int)).
% 9.74/3.19 thf(func_def_274, type, quickcheck_int_of: (quickcheck_code_int > int)).
% 9.74/3.19 thf(func_def_275, type, quickcheck_nat_of: (quickcheck_code_int > nat)).
% 9.74/3.19 thf(func_def_276, type, quickcheck_of_int: (int > quickcheck_code_int)).
% 9.74/3.19 thf(func_def_277, type, natceiling: (real > nat)).
% 9.74/3.19 thf(func_def_278, type, natfloor: (real > nat)).
% 9.74/3.19 thf(func_def_279, type, fract: (int > int > rat)).
% 9.74/3.19 thf(func_def_280, type, frct: (product_prod_int_int > rat)).
% 9.74/3.19 thf(func_def_281, type, field_1210416355s_real: (real > $o)).
% 9.74/3.19 thf(func_def_282, type, normalize: (product_prod_int_int > product_prod_int_int)).
% 9.74/3.19 thf(func_def_283, type, quotient_of: (rat > product_prod_int_int)).
% 9.74/3.19 thf(func_def_284, type, ratrel: (produc1137372701nt_int > $o)).
% 9.74/3.19 thf(func_def_285, type, ratreal: (rat > real)).
% 9.74/3.19 thf(func_def_286, type, real_int: (int > real)).
% 9.74/3.19 thf(func_def_287, type, real_nat: (nat > real)).
% 9.74/3.19 thf(func_def_288, type, vanishes: ((nat > rat) > $o)).
% 9.74/3.19 thf(func_def_289, type, dist_dist_complex: (complex > complex > real)).
% 9.74/3.19 thf(func_def_290, type, dist_dist_real: (real > real > real)).
% 9.74/3.19 thf(func_def_291, type, norm_norm_complex: (complex > real)).
% 9.74/3.19 thf(func_def_292, type, norm_norm_real: (real > real)).
% 9.74/3.19 thf(func_def_293, type, of_real_complex: (real > complex)).
% 9.74/3.19 thf(func_def_294, type, scaleR1652505878omplex: (real > complex > complex)).
% 9.74/3.19 thf(func_def_295, type, scaleR_scaleR_real: (real > real > real)).
% 9.74/3.19 thf(func_def_296, type, legendre: (int > int > int)).
% 9.74/3.19 thf(func_def_297, type, quadRes: (int > int > $o)).
% 9.74/3.19 thf(func_def_298, type, resSet: (int > (int > $o) > $o)).
% 9.74/3.19 thf(func_def_299, type, sr: (int > int > $o)).
% 9.74/3.19 thf(func_def_300, type, sRStar: (int > int > $o)).
% 9.74/3.19 thf(func_def_301, type, standardRes: (int > int > int)).
% 9.74/3.19 thf(func_def_302, type, dvd_dv174992974umeral: (code_code_numeral > code_code_numeral > $o)).
% 9.74/3.19 thf(func_def_303, type, dvd_dvd_complex: (complex > complex > $o)).
% 9.74/3.19 thf(func_def_304, type, dvd_dvd_int: (int > int > $o)).
% 9.74/3.19 thf(func_def_305, type, dvd_dvd_nat: (nat > nat > $o)).
% 9.74/3.19 thf(func_def_306, type, dvd_dv1760642554de_int: (quickcheck_code_int > quickcheck_code_int > $o)).
% 9.74/3.19 thf(func_def_307, type, dvd_dvd_rat: (rat > rat > $o)).
% 9.74/3.19 thf(func_def_308, type, dvd_dvd_real: (real > real > $o)).
% 9.74/3.19 thf(func_def_309, type, bseq_real: ((nat > real) > $o)).
% 9.74/3.19 thf(func_def_310, type, cauchy_complex: ((nat > complex) > $o)).
% 9.74/3.19 thf(func_def_311, type, cauchy_real: ((nat > real) > $o)).
% 9.74/3.19 thf(func_def_312, type, monoseq_real: ((nat > real) > $o)).
% 9.74/3.19 thf(func_def_313, type, z3div: (int > int > int)).
% 9.74/3.19 thf(func_def_314, type, z3mod: (int > int > int)).
% 9.74/3.19 thf(func_def_315, type, suminf_complex: ((nat > complex) > complex)).
% 9.74/3.19 thf(func_def_316, type, suminf_real: ((nat > real) > real)).
% 9.74/3.19 thf(func_def_317, type, summable_complex: ((nat > complex) > $o)).
% 9.74/3.19 thf(func_def_318, type, summable_real: ((nat > real) > $o)).
% 9.74/3.19 thf(func_def_319, type, sums_complex: ((nat > complex) > complex > $o)).
% 9.74/3.19 thf(func_def_320, type, sums_real: ((nat > real) > real > $o)).
% 9.74/3.19 thf(func_def_321, type, ord_at875362053st_int: (int > int > int > $o)).
% 9.74/3.19 thf(func_def_322, type, ord_at238088361st_nat: (nat > nat > nat > $o)).
% 9.74/3.19 thf(func_def_323, type, ord_at1589558736t_real: (real > real > real > $o)).
% 9.74/3.19 thf(func_def_324, type, ord_at641636577an_int: (int > int > int > $o)).
% 9.74/3.19 thf(func_def_325, type, ord_at4362885an_nat: (nat > nat > nat > $o)).
% 9.74/3.19 thf(func_def_326, type, ord_at1496968948n_real: (real > real > real > $o)).
% 9.74/3.19 thf(func_def_327, type, ord_atMost_nat: (nat > nat > $o)).
% 9.74/3.19 thf(func_def_328, type, ord_atMost_real: (real > real > $o)).
% 9.74/3.19 thf(func_def_329, type, ord_gr1297742076an_int: (int > int > int > $o)).
% 9.74/3.19 thf(func_def_330, type, ord_gr660468384an_nat: (nat > nat > nat > $o)).
% 9.74/3.19 thf(func_def_331, type, ord_gr788844697n_real: (real > real > real > $o)).
% 9.74/3.19 thf(func_def_332, type, ord_lessThan_nat: (nat > nat > $o)).
% 9.74/3.19 thf(func_def_333, type, ord_lessThan_real: (real > real > $o)).
% 9.74/3.19 thf(func_def_334, type, collect_int: ((int > $o) > int > $o)).
% 9.74/3.19 thf(func_def_335, type, collect_nat: ((nat > $o) > nat > $o)).
% 9.74/3.19 thf(func_def_336, type, collect_real: ((real > $o) > real > $o)).
% 9.74/3.19 thf(func_def_337, type, collec1347809874nt_int: ((product_prod_int_int > $o) > product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_338, type, collec1979865426at_nat: ((product_prod_nat_nat > $o) > product_prod_nat_nat > $o)).
% 9.74/3.19 thf(func_def_339, type, collec50511176nt_int: ((produc1137372701nt_int > $o) > produc1137372701nt_int > $o)).
% 9.74/3.19 thf(func_def_340, type, image_int_int_o: ((int > int > $o) > (int > $o) > (int > $o) > $o)).
% 9.74/3.19 thf(func_def_341, type, image_int_int: ((int > int) > (int > $o) > int > $o)).
% 9.74/3.19 thf(func_def_342, type, image_int_nat: ((int > nat) > (int > $o) > nat > $o)).
% 9.74/3.19 thf(func_def_343, type, image_nat_int: ((nat > int) > (nat > $o) > int > $o)).
% 9.74/3.19 thf(func_def_344, type, image_nat_nat: ((nat > nat) > (nat > $o) > nat > $o)).
% 9.74/3.19 thf(func_def_345, type, arccos: (real > real)).
% 9.74/3.19 thf(func_def_346, type, arcsin: (real > real)).
% 9.74/3.19 thf(func_def_347, type, arctan: (real > real)).
% 9.74/3.19 thf(func_def_348, type, cos: (real > real)).
% 9.74/3.19 thf(func_def_349, type, cos_coeff: (nat > real)).
% 9.74/3.19 thf(func_def_350, type, diffs_real: ((nat > real) > nat > real)).
% 9.74/3.19 thf(func_def_351, type, exp_real: (real > real)).
% 9.74/3.19 thf(func_def_352, type, ln: (real > real)).
% 9.74/3.19 thf(func_def_353, type, pi: real).
% 9.74/3.19 thf(func_def_354, type, sin: (real > real)).
% 9.74/3.19 thf(func_def_355, type, sin_coeff: (nat > real)).
% 9.74/3.19 thf(func_def_356, type, tan: (real > real)).
% 9.74/3.19 thf(func_def_357, type, twoSqu1152398899sum2sq: (int > $o)).
% 9.74/3.19 thf(func_def_358, type, twoSqu2072599593sum2sq: (product_prod_int_int > int)).
% 9.74/3.19 thf(func_def_359, type, accp_int: ((int > int > $o) > int > $o)).
% 9.74/3.19 thf(func_def_360, type, accp_P2006205492nt_int: ((product_prod_int_int > product_prod_int_int > $o) > product_prod_int_int > $o)).
% 9.74/3.19 thf(func_def_361, type, accp_P490777396at_nat: ((product_prod_nat_nat > product_prod_nat_nat > $o) > product_prod_nat_nat > $o)).
% 9.74/3.19 thf(func_def_362, type, pred_nat: (product_prod_nat_nat > $o)).
% 9.74/3.19 thf(func_def_363, type, inv: (int > int > int)).
% 9.74/3.19 thf(func_def_364, type, wset: (int > int > int > $o)).
% 9.74/3.19 thf(func_def_365, type, member_int_o: ((int > $o) > ((int > $o) > $o) > $o)).
% 9.74/3.19 thf(func_def_366, type, member_int: (int > (int > $o) > $o)).
% 9.74/3.19 thf(func_def_367, type, member_nat: (nat > (nat > $o) > $o)).
% 9.74/3.19 thf(func_def_368, type, member_real: (real > (real > $o) > $o)).
% 9.74/3.19 thf(func_def_369, type, member1329254762_int_o: (produc975137661_int_o > (produc975137661_int_o > $o) > $o)).
% 9.74/3.19 thf(func_def_370, type, member2143287562nt_int: (produc1137372701nt_int > (produc1137372701nt_int > $o) > $o)).
% 9.74/3.19 thf(func_def_371, type, member180897546at_nat: (produc1322466333at_nat > (produc1322466333at_nat > $o) > $o)).
% 9.74/3.19 thf(func_def_372, type, m: int).
% 9.74/3.19 thf(func_def_373, type, m1: int).
% 9.74/3.19 thf(func_def_374, type, n: nat).
% 9.74/3.19 thf(func_def_375, type, r: int).
% 9.74/3.19 thf(func_def_376, type, s1: int).
% 9.74/3.19 thf(func_def_377, type, s: int).
% 9.74/3.19 thf(func_def_378, type, sa: int).
% 9.74/3.19 thf(func_def_379, type, t: int).
% 9.74/3.19 thf(func_def_380, type, tn: nat).
% 9.74/3.19 thf(func_def_381, type, v: int).
% 9.74/3.19 thf(func_def_382, type, w: int).
% 9.74/3.19 thf(func_def_383, type, x: int).
% 9.74/3.19 thf(func_def_384, type, y: int).
% 9.74/3.19 thf(func_def_386, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 9.74/3.19 thf(func_def_387, type, vAND: ($o > $o > $o)).
% 9.74/3.19 thf(func_def_388, type, vIMP: ($o > $o > $o)).
% 9.74/3.19 thf(func_def_389, type, vNOT: ($o > $o)).
% 9.74/3.19 thf(func_def_390, type, vOR: ($o > $o > $o)).
% 9.74/3.19 thf(func_def_391, type, db0: !>[X0: $tType]:(X0)).
% 9.74/3.19 thf(func_def_392, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 9.74/3.19 thf(func_def_395, type, db1: !>[X0: $tType]:(X0)).
% 9.74/3.19 thf(func_def_396, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 9.74/3.19 thf(func_def_397, type, db2: !>[X0: $tType]:(X0)).
% 9.74/3.19 thf(func_def_398, type, sP0: ((int > $o) > int > int > $o)).
% 9.74/3.19 thf(func_def_399, type, sK1: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_400, type, sK2: ((nat > $o) > int > nat)).
% 9.74/3.19 thf(func_def_401, type, sK3: int).
% 9.74/3.19 thf(func_def_402, type, sK4: ((int > $o) > int > int)).
% 9.74/3.19 thf(func_def_403, type, sK5: (int > nat)).
% 9.74/3.19 thf(func_def_404, type, sK6: ((nat > $o) > nat)).
% 9.74/3.19 thf(func_def_405, type, sK7: ((nat > nat) > nat)).
% 9.74/3.19 thf(func_def_406, type, sK8: ((nat > nat) > nat)).
% 9.74/3.19 thf(func_def_407, type, sK9: (real > nat > real)).
% 9.74/3.19 thf(func_def_408, type, sK10: (nat > nat)).
% 9.74/3.19 thf(func_def_409, type, sK11: (int > (int > $o) > int)).
% 9.74/3.19 thf(func_def_410, type, sK12: (int > nat)).
% 9.74/3.19 thf(func_def_411, type, sK13: ((nat > real) > nat)).
% 9.74/3.19 thf(func_def_412, type, sK14: (nat > nat > (nat > $o) > nat)).
% 9.74/3.19 thf(func_def_413, type, sK15: (int > nat)).
% 9.74/3.19 thf(func_def_414, type, sK16: ((nat > $o) > nat > nat > nat)).
% 9.74/3.19 thf(func_def_415, type, sK17: (int > int > int > int)).
% 9.74/3.19 thf(func_def_416, type, sK18: (int > (int > $o) > int)).
% 9.74/3.19 thf(func_def_417, type, sK19: ((int > $o) > int > int)).
% 9.74/3.19 thf(func_def_418, type, sK20: ((nat > nat) > nat)).
% 9.74/3.19 thf(func_def_419, type, sK21: ((nat > nat) > nat)).
% 9.74/3.19 thf(func_def_420, type, sK22: ((nat > nat) > nat)).
% 9.74/3.19 thf(func_def_421, type, sK23: (nat > real > real)).
% 9.74/3.19 thf(func_def_422, type, sK24: int).
% 9.74/3.19 thf(func_def_423, type, sK25: int).
% 9.74/3.19 thf(func_def_424, type, sK26: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_425, type, sK27: ((int > $o) > nat)).
% 9.74/3.19 thf(func_def_426, type, sK28: ((int > $o) > int)).
% 9.74/3.19 thf(func_def_427, type, sK29: (nat > (nat > $o) > nat)).
% 9.74/3.19 thf(func_def_428, type, sK30: (int > int > int)).
% 9.74/3.19 thf(func_def_429, type, sK31: ((nat > $o) > nat > nat)).
% 9.74/3.19 thf(func_def_430, type, sK32: (nat > nat)).
% 9.74/3.19 thf(func_def_431, type, sK33: (int > int > nat)).
% 9.74/3.19 thf(func_def_432, type, sK34: (nat > (nat > $o) > nat)).
% 9.74/3.19 thf(func_def_433, type, sK35: (nat > (nat > $o) > nat)).
% 9.74/3.19 thf(func_def_434, type, sK36: (nat > nat)).
% 9.74/3.19 thf(func_def_435, type, sK37: ((nat > $o) > nat > nat)).
% 9.74/3.19 thf(func_def_436, type, sK38: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_437, type, sK39: ((int > $o) > int)).
% 9.74/3.19 thf(func_def_438, type, sK40: ((int > $o) > int)).
% 9.74/3.19 thf(func_def_439, type, sK41: ((int > $o) > nat)).
% 9.74/3.19 thf(func_def_440, type, sK42: ((nat > nat) > nat)).
% 9.74/3.19 thf(func_def_441, type, sK43: (int > int)).
% 9.74/3.19 thf(func_def_442, type, sK44: (real > real > real)).
% 9.74/3.19 thf(func_def_443, type, sK45: ((int > $o) > int > int)).
% 9.74/3.19 thf(func_def_444, type, sK46: ((int > $o) > int > int)).
% 9.74/3.19 thf(func_def_445, type, sK47: (int > nat)).
% 9.74/3.19 thf(func_def_446, type, sK48: ((nat > $o) > nat)).
% 9.74/3.19 thf(func_def_447, type, sK49: (int > int)).
% 9.74/3.19 thf(func_def_448, type, sK50: ((nat > $o) > nat)).
% 9.74/3.19 thf(func_def_449, type, sK51: (int > nat)).
% 9.74/3.19 thf(func_def_450, type, sK52: (int > nat)).
% 9.74/3.19 thf(func_def_451, type, sK53: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_452, type, sK54: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_453, type, sK55: ((nat > nat) > nat)).
% 9.74/3.19 thf(func_def_454, type, sK56: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_455, type, sK57: (real > nat > real)).
% 9.74/3.19 thf(func_def_456, type, sK58: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_457, type, sK59: ((int > $o) > int > int > int)).
% 9.74/3.19 thf(func_def_458, type, sK60: ((int > $o) > int > int > int)).
% 9.74/3.19 thf(func_def_459, type, sK61: (int > (int > $o) > int > int)).
% 9.74/3.19 thf(func_def_460, type, sK62: (int > (int > $o) > int > int)).
% 9.74/3.19 thf(func_def_461, type, sK63: (int > (int > $o) > int)).
% 9.74/3.19 thf(func_def_462, type, sK64: (int > (int > $o) > int)).
% 9.74/3.19 thf(func_def_463, type, sK65: (nat > nat)).
% 9.74/3.19 thf(func_def_464, type, sK66: ((nat > nat) > nat)).
% 9.74/3.19 thf(func_def_465, type, sK67: ((nat > nat) > nat)).
% 9.74/3.19 thf(func_def_466, type, sK68: (int > (int > $o) > int)).
% 9.74/3.19 thf(func_def_467, type, sK69: (int > (int > $o) > int)).
% 9.74/3.19 thf(func_def_468, type, sK70: (int > int > nat)).
% 9.74/3.19 thf(func_def_469, type, sK71: (nat > nat)).
% 9.74/3.19 thf(func_def_470, type, sK72: (nat > nat > nat)).
% 9.74/3.19 thf(func_def_471, type, sK73: (nat > nat > nat)).
% 9.74/3.19 thf(f1,axiom,(
% 9.74/3.19 (ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))),
% 9.74/3.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_n1pos)).
% 9.74/3.19 thf(f19,axiom,(
% 9.74/3.19 (((power_power_int @ zero_zero_int @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) = zero_zero_int)),
% 9.74/3.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_zero__power2)).
% 9.74/3.19 thf(f348,axiom,(
% 9.74/3.19 ! [X1 : int,X0 : nat] : ((X1 != zero_zero_int) => (((power_power_int @ X1 @ X0)) != zero_zero_int))),
% 9.74/3.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_347_field__power__not__zero)).
% 9.74/3.19 thf(f1445,axiom,(
% 9.74/3.19 ! [X1 : int,X0 : int] : ((((plus_plus_int @ (times_times_int @ X0 @ X0) @ (times_times_int @ X1 @ X1))) = zero_zero_int) <=> ((X0 = zero_zero_int) & (X1 = zero_zero_int)))),
% 9.74/3.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1444_sum__squares__eq__zero__iff)).
% 9.74/3.19 thf(f1593,axiom,(
% 9.74/3.19 ! [X0 : int,X1 : int] : ((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ X0 @ X0) @ (times_times_int @ X1 @ X1))) <=> ((X1 != zero_zero_int) | (X0 != zero_zero_int)))),
% 9.74/3.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1592_sum__squares__gt__zero__iff)).
% 9.74/3.19 thf(f5212,conjecture,(
% 9.74/3.19 (((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) != zero_zero_int)),
% 9.74/3.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 9.74/3.19 thf(f5213,negated_conjecture,(
% 9.74/3.19 ~ (((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) != zero_zero_int)),
% 9.74/3.19 inference(negated_conjecture,[status(cth)],[f5212])).
% 9.74/3.19 thf(f5245,plain,(
% 9.74/3.19 ~ (zero_zero_int != ((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 9.74/3.19 inference(fool_elimination,[],[f5213])).
% 9.74/3.19 thf(f5455,plain,(
% 9.74/3.19 ! [X0 : int,X1 : int] : ((zero_zero_int = ((plus_plus_int @ (times_times_int @ X1 @ X1) @ (times_times_int @ X0 @ X0)))) <=> ((zero_zero_int = X1) & (zero_zero_int = X0)))),
% 9.74/3.20 inference(rectify,[],[f1445])).
% 9.74/3.20 thf(f5456,plain,(
% 9.74/3.20 ! [X0 : int,X1 : int] : ((zero_zero_int = ((plus_plus_int @ (times_times_int @ X1 @ X1) @ (times_times_int @ X0 @ X0)))) <=> ((zero_zero_int = X1) & (zero_zero_int = X0)))),
% 9.74/3.20 inference(fool_elimination,[],[f5455])).
% 9.74/3.20 thf(f7106,plain,(
% 9.74/3.20 (zero_zero_int = ((power_power_int @ zero_zero_int @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 9.74/3.20 inference(fool_elimination,[],[f19])).
% 9.74/3.20 thf(f10236,plain,(
% 9.74/3.20 (ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))),
% 9.74/3.20 inference(rectify,[],[f1])).
% 9.74/3.20 thf(f10237,plain,(
% 9.74/3.20 (((ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))) = $true)),
% 9.74/3.20 inference(fool_elimination,[],[f10236])).
% 9.74/3.20 thf(f13135,plain,(
% 9.74/3.20 ! [X0 : int,X1 : nat] : ((zero_zero_int != X0) => (zero_zero_int != ((power_power_int @ X0 @ X1))))),
% 9.74/3.20 inference(rectify,[],[f348])).
% 9.74/3.20 thf(f13136,plain,(
% 9.74/3.20 ! [X1 : nat,X0 : int] : ((zero_zero_int != X0) => (zero_zero_int != ((power_power_int @ X0 @ X1))))),
% 9.74/3.20 inference(fool_elimination,[],[f13135])).
% 9.74/3.20 thf(f14103,plain,(
% 9.74/3.20 ! [X0 : int,X1 : int] : ((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ X0 @ X0) @ (times_times_int @ X1 @ X1))) <=> ((X1 != zero_zero_int) | (X0 != zero_zero_int)))),
% 9.74/3.20 inference(rectify,[],[f1593])).
% 9.74/3.20 thf(f14104,plain,(
% 9.74/3.20 ! [X1 : int,X0 : int] : (((zero_zero_int != X1) | (zero_zero_int != X0)) <=> (((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ X0 @ X0) @ (times_times_int @ X1 @ X1)))) = $true))),
% 9.74/3.20 inference(fool_elimination,[],[f14103])).
% 9.74/3.20 thf(f14420,plain,(
% 9.74/3.20 (zero_zero_int = ((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 9.74/3.20 inference(flattening,[],[f5245])).
% 9.74/3.20 thf(f15069,plain,(
% 9.74/3.20 ! [X0 : int,X1 : nat] : ((zero_zero_int = X0) | (zero_zero_int != ((power_power_int @ X0 @ X1))))),
% 9.74/3.20 inference(ennf_transformation,[],[f13136])).
% 9.74/3.20 thf(f16568,plain,(
% 9.74/3.20 ! [X1 : int,X0 : int] : ((((zero_zero_int != X1) | (zero_zero_int != X0)) | (((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ X0 @ X0) @ (times_times_int @ X1 @ X1)))) != $true)) & ((((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ X0 @ X0) @ (times_times_int @ X1 @ X1)))) = $true) | ((zero_zero_int = X1) & (zero_zero_int = X0))))),
% 9.74/3.20 inference(nnf_transformation,[],[f14104])).
% 9.74/3.20 thf(f16569,plain,(
% 9.74/3.20 ! [X1 : int,X0 : int] : (((zero_zero_int != X1) | (zero_zero_int != X0) | (((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ X0 @ X0) @ (times_times_int @ X1 @ X1)))) != $true)) & ((((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ X0 @ X0) @ (times_times_int @ X1 @ X1)))) = $true) | ((zero_zero_int = X1) & (zero_zero_int = X0))))),
% 9.74/3.20 inference(flattening,[],[f16568])).
% 9.74/3.20 thf(f16570,plain,(
% 9.74/3.20 ! [X0 : int,X1 : int] : (((zero_zero_int != X0) | (zero_zero_int != X1) | (((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ X1 @ X1) @ (times_times_int @ X0 @ X0)))) != $true)) & ((((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ X1 @ X1) @ (times_times_int @ X0 @ X0)))) = $true) | ((zero_zero_int = X0) & (zero_zero_int = X1))))),
% 9.74/3.20 inference(rectify,[],[f16569])).
% 9.74/3.20 thf(f16782,plain,(
% 9.74/3.20 ! [X0 : int,X1 : int] : (((zero_zero_int = ((plus_plus_int @ (times_times_int @ X1 @ X1) @ (times_times_int @ X0 @ X0)))) | ((zero_zero_int != X1) | (zero_zero_int != X0))) & (((zero_zero_int = X1) & (zero_zero_int = X0)) | (zero_zero_int != ((plus_plus_int @ (times_times_int @ X1 @ X1) @ (times_times_int @ X0 @ X0))))))),
% 9.74/3.20 inference(nnf_transformation,[],[f5456])).
% 9.74/3.20 thf(f16783,plain,(
% 9.74/3.20 ! [X0 : int,X1 : int] : (((zero_zero_int = ((plus_plus_int @ (times_times_int @ X1 @ X1) @ (times_times_int @ X0 @ X0)))) | (zero_zero_int != X1) | (zero_zero_int != X0)) & (((zero_zero_int = X1) & (zero_zero_int = X0)) | (zero_zero_int != ((plus_plus_int @ (times_times_int @ X1 @ X1) @ (times_times_int @ X0 @ X0))))))),
% 9.74/3.20 inference(flattening,[],[f16782])).
% 9.74/3.20 thf(f17304,plain,(
% 9.74/3.20 ( ! [X0 : int,X1 : nat] : ((zero_zero_int != ((power_power_int @ X0 @ X1))) | (zero_zero_int = X0)) )),
% 9.74/3.20 inference(cnf_transformation,[],[f15069])).
% 9.74/3.20 thf(f17608,plain,(
% 9.74/3.20 (zero_zero_int = ((power_power_int @ zero_zero_int @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 9.74/3.20 inference(cnf_transformation,[],[f7106])).
% 9.74/3.20 thf(f18346,plain,(
% 9.74/3.20 ( ! [X0 : int,X1 : int] : ((zero_zero_int != X0) | (zero_zero_int != X1) | (((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ X1 @ X1) @ (times_times_int @ X0 @ X0)))) != $true)) )),
% 9.74/3.20 inference(cnf_transformation,[],[f16570])).
% 9.74/3.20 thf(f18723,plain,(
% 9.74/3.20 ( ! [X0 : int,X1 : int] : ((zero_zero_int = ((plus_plus_int @ (times_times_int @ X1 @ X1) @ (times_times_int @ X0 @ X0)))) | (zero_zero_int != X1) | (zero_zero_int != X0)) )),
% 9.74/3.20 inference(cnf_transformation,[],[f16783])).
% 9.74/3.20 thf(f18844,plain,(
% 9.74/3.20 (zero_zero_int = ((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 9.74/3.20 inference(cnf_transformation,[],[f14420])).
% 9.74/3.20 thf(f19025,plain,(
% 9.74/3.20 (((ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))) = $true)),
% 9.74/3.20 inference(cnf_transformation,[],[f10237])).
% 9.74/3.20 thf(f19480,plain,(
% 9.74/3.20 ( ! [X1 : int] : ((zero_zero_int != X1) | (((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ X1 @ X1) @ (times_times_int @ zero_zero_int @ zero_zero_int)))) != $true)) )),
% 9.74/3.20 inference(equality_resolution,[],[f18346])).
% 9.74/3.20 thf(f19481,plain,(
% 9.74/3.20 ($true != ((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ zero_zero_int @ zero_zero_int) @ (times_times_int @ zero_zero_int @ zero_zero_int)))))),
% 9.74/3.20 inference(equality_resolution,[],[f19480])).
% 9.74/3.20 thf(f19541,plain,(
% 9.74/3.20 ( ! [X0 : int] : ((zero_zero_int = ((plus_plus_int @ (times_times_int @ zero_zero_int @ zero_zero_int) @ (times_times_int @ X0 @ X0)))) | (zero_zero_int != X0)) )),
% 9.74/3.20 inference(equality_resolution,[],[f18723])).
% 9.74/3.20 thf(f19542,plain,(
% 9.74/3.20 (zero_zero_int = ((plus_plus_int @ (times_times_int @ zero_zero_int @ zero_zero_int) @ (times_times_int @ zero_zero_int @ zero_zero_int))))),
% 9.74/3.20 inference(equality_resolution,[],[f19541])).
% 9.74/3.20 thf(f19800,definition,(
% 9.74/3.20 spl74_31 <=> (zero_zero_int = ((power_power_int @ zero_zero_int @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 9.74/3.20 introduced(definition,[new_symbols(definition,[spl74_31])],[avatar_definition])).
% 9.74/3.20 thf(f19803,plain,(
% 9.74/3.20 spl74_31),
% 9.74/3.20 inference(avatar_split_clause,[],[f17608,f19800])).
% 9.74/3.20 thf(f20013,definition,(
% 9.74/3.20 spl74_74 <=> (((ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))) = $true)),
% 9.74/3.20 introduced(definition,[new_symbols(definition,[spl74_74])],[avatar_definition])).
% 9.74/3.20 thf(f20016,plain,(
% 9.74/3.20 spl74_74),
% 9.74/3.20 inference(avatar_split_clause,[],[f19025,f20013])).
% 9.74/3.20 thf(f20087,definition,(
% 9.74/3.20 spl74_89 <=> (zero_zero_int = ((plus_plus_int @ (times_times_int @ zero_zero_int @ zero_zero_int) @ (times_times_int @ zero_zero_int @ zero_zero_int))))),
% 9.74/3.20 introduced(definition,[new_symbols(definition,[spl74_89])],[avatar_definition])).
% 9.74/3.20 thf(f20090,plain,(
% 9.74/3.20 spl74_89),
% 9.74/3.20 inference(avatar_split_clause,[],[f19542,f20087])).
% 9.74/3.20 thf(f20174,definition,(
% 9.74/3.20 spl74_106 <=> (zero_zero_int = ((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 9.74/3.20 introduced(definition,[new_symbols(definition,[spl74_106])],[avatar_definition])).
% 9.74/3.20 thf(f20176,plain,(
% 9.74/3.20 (zero_zero_int = ((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))) | ~spl74_106),
% 9.74/3.20 inference(avatar_component_clause,[],[f20174])).
% 9.74/3.20 thf(f20177,plain,(
% 9.74/3.20 spl74_106),
% 9.74/3.20 inference(avatar_split_clause,[],[f18844,f20174])).
% 9.74/3.20 thf(f20206,definition,(
% 9.74/3.20 spl74_112 <=> ($true = ((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ zero_zero_int @ zero_zero_int) @ (times_times_int @ zero_zero_int @ zero_zero_int)))))),
% 9.74/3.20 introduced(definition,[new_symbols(definition,[spl74_112])],[avatar_definition])).
% 9.74/3.20 thf(f20209,plain,(
% 9.74/3.20 ~spl74_112),
% 9.74/3.20 inference(avatar_split_clause,[],[f19481,f20206])).
% 9.74/3.20 thf(f20270,plain,(
% 9.74/3.20 (zero_zero_int != zero_zero_int) | (zero_zero_int = ((plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))) | ~spl74_106),
% 9.74/3.20 inference(superposition,[],[f17304,f20176])).
% 9.74/3.20 thf(f20272,plain,(
% 9.74/3.20 (zero_zero_int = ((plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))) | ~spl74_106),
% 9.74/3.20 inference(trivial_inequality_removal,[],[f20270])).
% 9.74/3.20 thf(f20275,definition,(
% 9.74/3.20 spl74_119 <=> (zero_zero_int = ((plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n))))),
% 9.74/3.20 introduced(definition,[new_symbols(definition,[spl74_119])],[avatar_definition])).
% 9.74/3.20 thf(f20278,plain,(
% 9.74/3.20 spl74_119 | ~spl74_106),
% 9.74/3.20 inference(avatar_split_clause,[],[f20272,f20174,f20275])).
% 9.74/3.20 thf(f20284,definition,(
% 9.74/3.20 (zero_zero_int != ((plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))) | (zero_zero_int != ((plus_plus_int @ (times_times_int @ zero_zero_int @ zero_zero_int) @ (times_times_int @ zero_zero_int @ zero_zero_int)))) | (zero_zero_int != ((power_power_int @ zero_zero_int @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))) | (((ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))) != $true) | ($true = ((ord_less_int @ zero_zero_int @ (plus_plus_int @ (times_times_int @ zero_zero_int @ zero_zero_int) @ (times_times_int @ zero_zero_int @ zero_zero_int)))))),
% 9.74/3.20 introduced(theory,[theory_tautology_sat_conflict])).
% 9.74/3.20 cnf(s35, plain, spl74_31, inference(sat_conversion,[],[f19803])).
% 9.74/3.20 cnf(s95, plain, spl74_74, inference(sat_conversion,[],[f20016])).
% 9.74/3.20 cnf(s116, plain, spl74_89, inference(sat_conversion,[],[f20090])).
% 9.74/3.20 cnf(s155, plain, spl74_106, inference(sat_conversion,[],[f20177])).
% 9.74/3.20 cnf(s166, plain, ~spl74_112, inference(sat_conversion,[],[f20209])).
% 9.74/3.20 cnf(s176, plain, ~spl74_106 | spl74_119, inference(sat_conversion,[],[f20278])).
% 9.74/3.20 cnf(s182, plain, ~spl74_31 | ~spl74_74 | ~spl74_89 | spl74_112 | ~spl74_119, inference(sat_conversion,[],[f20284])).
% 9.74/3.20 cnf(s183, plain, spl74_119, inference(rat,[],[s176,s155])).
% 9.74/3.20 cnf(s185, plain, ~spl74_31, inference(rat,[],[s182,s183,s166,s116,s95])).
% 9.74/3.20 cnf(s189, plain, $false, inference(rat,[],[s35,s185])).
% 9.74/3.20 thf(f20285,plain,(
% 9.74/3.20 $false),
% 9.74/3.20 inference(avatar_sat_refutation,[],[s189])).
% 9.74/3.20 % SZS output end Proof for theBenchmark
% 9.74/3.20 % (3951670)------------------------------
% 9.74/3.20 % (3951670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/3.20 % (3951670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/3.20 % (3951670)CaDiCaL version: 2.1.3
% 9.74/3.20 % (3951670)Termination reason: Refutation
% 9.74/3.20 % (3951670)Time elapsed: 0.390 s
% 9.74/3.20 % (3951670)Peak memory usage: 28 MB
% 9.74/3.20 % (3951670)Instructions burned: 1100 (million)
% 9.74/3.20 % (3951531)Success in time 1.592 s
% 9.74/3.20 % Vampire exiting
%------------------------------------------------------------------------------