%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COM159^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 07:46:22 AM UTC 2026
% Result : Theorem 29.98s 4.74s
% Output : Refutation 29.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM159^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 % Computer : n003.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Tue Sep 29 17:48:29 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running higher-order theorem proving
% 0.20/0.30 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/0.46 % (2833790)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.32/0.46 % (2833798)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=2079317793:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.32/0.46 % (2833796)lrs+10_16_si=on:nwc=1.5:random_seed=3564660169:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.32/0.46 % (2833795)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3168706390:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.32/0.46 % (2833797)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=776492935:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.32/0.46 % (2833799)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3027002919:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.32/0.46 % (2833797)Instruction limit reached!
% 0.32/0.46 % (2833797)------------------------------
% 0.32/0.46 % (2833797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.32/0.46 % (2833797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.32/0.46 % (2833797)CaDiCaL version: 2.1.3
% 0.32/0.46 % (2833797)Termination reason: Instruction limit
% 0.32/0.46 % (2833797)Termination phase: shuffling
% 0.32/0.46 % (2833797)Time elapsed: 0.003 s
% 0.32/0.46 % (2833797)Peak memory usage: 10 MB
% 0.32/0.46 % (2833797)Instructions burned: 5 (million)
% 0.32/0.46 % (2833801)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.32/0.46 % (2833801)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.32/0.46 % (2833796)Instruction limit reached!
% 0.32/0.46 % (2833796)------------------------------
% 0.32/0.46 % (2833796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.32/0.46 % (2833796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.32/0.46 % (2833796)CaDiCaL version: 2.1.3
% 0.32/0.46 % (2833796)Termination reason: Instruction limit
% 0.32/0.46 % (2833796)Termination phase: shuffling
% 0.32/0.46 % (2833796)Time elapsed: 0.009 s
% 0.32/0.46 % (2833796)Peak memory usage: 10 MB
% 0.32/0.46 % (2833796)Instructions burned: 19 (million)
% 0.32/0.46 % (2833800)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=805267619:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.32/0.46 % (2833799)Instruction limit reached!
% 0.32/0.46 % (2833799)------------------------------
% 0.32/0.46 % (2833799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.32/0.46 % (2833801)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=1121662665:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.32/0.46 % (2833799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.32/0.46 % (2833799)CaDiCaL version: 2.1.3
% 0.32/0.46 % (2833799)Termination reason: Instruction limit
% 0.32/0.46 % (2833799)Termination phase: shuffling
% 0.32/0.46 % (2833799)Time elapsed: 0.012 s
% 0.32/0.46 % (2833799)Peak memory usage: 10 MB
% 0.32/0.46 % (2833799)Instructions burned: 24 (million)
% 0.32/0.46 % (2833807)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2351688747:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.32/0.46 % (2833807)Instruction limit reached!
% 0.32/0.46 % (2833807)------------------------------
% 0.32/0.46 % (2833807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.32/0.46 % (2833807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.32/0.46 % (2833807)CaDiCaL version: 2.1.3
% 0.32/0.46 % (2833807)Termination reason: Instruction limit
% 0.32/0.46 % (2833807)Termination phase: shuffling
% 0.32/0.46 % (2833807)Time elapsed: 0.002 s
% 0.32/0.46 % (2833807)Peak memory usage: 10 MB
% 0.32/0.46 % (2833807)Instructions burned: 3 (million)
% 0.32/0.46 % (2833808)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=444960232:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.12/0.49 % (2833811)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.12/0.49 % (2833808)Instruction limit reached!
% 1.12/0.49 % (2833808)------------------------------
% 1.12/0.49 % (2833808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.49 % (2833808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.49 % (2833808)CaDiCaL version: 2.1.3
% 1.12/0.49 % (2833808)Termination reason: Instruction limit
% 1.12/0.49 % (2833808)Termination phase: shuffling
% 1.12/0.49 % (2833808)Time elapsed: 0.003 s
% 1.12/0.49 % (2833808)Peak memory usage: 10 MB
% 1.12/0.49 % (2833808)Instructions burned: 6 (million)
% 1.12/0.49 % (2833811)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1724192469:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.12/0.49 % (2833811)Instruction limit reached!
% 1.12/0.49 % (2833811)------------------------------
% 1.12/0.49 % (2833811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.49 % (2833811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.49 % (2833811)CaDiCaL version: 2.1.3
% 1.12/0.49 % (2833811)Termination reason: Instruction limit
% 1.12/0.49 % (2833811)Termination phase: shuffling
% 1.12/0.49 % (2833811)Time elapsed: 0.004 s
% 1.12/0.49 % (2833811)Peak memory usage: 10 MB
% 1.12/0.49 % (2833811)Instructions burned: 8 (million)
% 1.12/0.49 % (2833795)Instruction limit reached!
% 1.12/0.49 % (2833795)------------------------------
% 1.12/0.49 % (2833795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.49 % (2833795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.49 % (2833795)CaDiCaL version: 2.1.3
% 1.12/0.49 % (2833795)Termination reason: Instruction limit
% 1.12/0.49 % (2833795)Termination phase: Property scanning
% 1.12/0.49 % (2833795)Time elapsed: 0.043 s
% 1.12/0.49 % (2833795)Peak memory usage: 12 MB
% 1.12/0.49 % (2833795)Instructions burned: 87 (million)
% 1.12/0.49 % (2833813)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3509663854:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.12/0.49 % (2833816)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.12/0.49 % (2833816)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.12/0.49 % (2833816)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=202555421:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.12/0.49 % (2833800)Instruction limit reached!
% 1.12/0.49 % (2833800)------------------------------
% 1.12/0.49 % (2833800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.49 % (2833800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.49 % (2833800)CaDiCaL version: 2.1.3
% 1.12/0.49 % (2833800)Termination reason: Instruction limit
% 1.12/0.49 % (2833800)Termination phase: Property scanning
% 1.12/0.50 % (2833800)Time elapsed: 0.039 s
% 1.12/0.50 % (2833800)Peak memory usage: 12 MB
% 1.12/0.50 % (2833800)Instructions burned: 77 (million)
% 1.12/0.50 % (2833813)Instruction limit reached!
% 1.12/0.50 % (2833813)------------------------------
% 1.12/0.50 % (2833813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.50 % (2833813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.50 % (2833813)CaDiCaL version: 2.1.3
% 1.12/0.50 % (2833813)Termination reason: Instruction limit
% 1.12/0.50 % (2833813)Termination phase: shuffling
% 1.12/0.50 % (2833813)Time elapsed: 0.007 s
% 1.12/0.50 % (2833813)Peak memory usage: 10 MB
% 1.12/0.50 % (2833813)Instructions burned: 13 (million)
% 1.12/0.50 % (2833817)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=2614679979:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.12/0.50 % (2833818)lrs+10_1_si=on:cs=on:random_seed=1867656661:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.12/0.50 % (2833816)Instruction limit reached!
% 1.12/0.53 % (2833816)------------------------------
% 1.12/0.53 % (2833816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.53 % (2833816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.53 % (2833816)CaDiCaL version: 2.1.3
% 1.12/0.53 % (2833816)Termination reason: Instruction limit
% 1.12/0.53 % (2833816)Termination phase: shuffling
% 1.12/0.53 % (2833816)Time elapsed: 0.014 s
% 1.12/0.53 % (2833816)Peak memory usage: 10 MB
% 1.12/0.53 % (2833816)Instructions burned: 29 (million)
% 1.12/0.53 % (2833821)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.12/0.53 % (2833818)Instruction limit reached!
% 1.12/0.53 % (2833818)------------------------------
% 1.12/0.53 % (2833818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.53 % (2833818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.53 % (2833818)CaDiCaL version: 2.1.3
% 1.12/0.53 % (2833818)Termination reason: Instruction limit
% 1.12/0.53 % (2833818)Termination phase: shuffling
% 1.12/0.53 % (2833818)Time elapsed: 0.004 s
% 1.12/0.53 % (2833818)Peak memory usage: 10 MB
% 1.12/0.53 % (2833818)Instructions burned: 8 (million)
% 1.12/0.53 % (2833821)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=4124941712:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.12/0.53 % (2833822)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1312558582:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.12/0.53 % (2833821)Instruction limit reached!
% 1.12/0.53 % (2833821)------------------------------
% 1.12/0.53 % (2833821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.53 % (2833821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.53 % (2833821)CaDiCaL version: 2.1.3
% 1.12/0.53 % (2833821)Termination reason: Instruction limit
% 1.12/0.53 % (2833821)Termination phase: shuffling
% 1.12/0.53 % (2833821)Time elapsed: 0.001 s
% 1.12/0.53 % (2833821)Peak memory usage: 10 MB
% 1.12/0.53 % (2833821)Instructions burned: 2 (million)
% 1.12/0.53 % (2833825)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2916684026:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.12/0.53 % (2833826)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2681637485:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.12/0.53 % (2833822)Instruction limit reached!
% 1.12/0.53 % (2833822)------------------------------
% 1.12/0.53 % (2833822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.53 % (2833822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.53 % (2833822)CaDiCaL version: 2.1.3
% 1.12/0.53 % (2833822)Termination reason: Instruction limit
% 1.12/0.53 % (2833822)Termination phase: Property scanning
% 1.12/0.53 % (2833822)Time elapsed: 0.018 s
% 1.12/0.53 % (2833822)Peak memory usage: 10 MB
% 1.12/0.53 % (2833822)Instructions burned: 39 (million)
% 1.12/0.53 % (2833829)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2623430613:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.12/0.53 % (2833817)Instruction limit reached!
% 1.12/0.53 % (2833817)------------------------------
% 1.12/0.53 % (2833817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.53 % (2833817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.53 % (2833817)CaDiCaL version: 2.1.3
% 1.12/0.53 % (2833817)Termination reason: Instruction limit
% 1.12/0.53 % (2833817)Termination phase: Preprocessing 1
% 1.12/0.53 % (2833817)Time elapsed: 0.039 s
% 1.12/0.53 % (2833817)Peak memory usage: 11 MB
% 1.12/0.53 % (2833817)Instructions burned: 87 (million)
% 1.12/0.53 % (2833826)Instruction limit reached!
% 1.12/0.53 % (2833826)------------------------------
% 1.12/0.53 % (2833826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.53 % (2833826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.53 % (2833826)CaDiCaL version: 2.1.3
% 1.12/0.53 % (2833826)Termination reason: Instruction limit
% 1.12/0.53 % (2833826)Termination phase: shuffling
% 1.12/0.56 % (2833826)Time elapsed: 0.012 s
% 1.12/0.56 % (2833826)Peak memory usage: 10 MB
% 1.12/0.56 % (2833826)Instructions burned: 25 (million)
% 1.12/0.56 % (2833829)Instruction limit reached!
% 1.12/0.56 % (2833829)------------------------------
% 1.12/0.56 % (2833829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.56 % (2833829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.56 % (2833829)CaDiCaL version: 2.1.3
% 1.12/0.56 % (2833829)Termination reason: Instruction limit
% 1.12/0.56 % (2833829)Termination phase: shuffling
% 1.12/0.56 % (2833829)Time elapsed: 0.007 s
% 1.12/0.56 % (2833829)Peak memory usage: 10 MB
% 1.12/0.56 % (2833829)Instructions burned: 15 (million)
% 1.12/0.56 % (2833801)Instruction limit reached!
% 1.12/0.56 % (2833801)------------------------------
% 1.12/0.56 % (2833801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.56 % (2833801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.56 % (2833801)CaDiCaL version: 2.1.3
% 1.12/0.56 % (2833801)Termination reason: Instruction limit
% 1.12/0.56 % (2833801)Termination phase: Saturation
% 1.12/0.56 % (2833801)Time elapsed: 0.090 s
% 1.12/0.56 % (2833801)Peak memory usage: 14 MB
% 1.12/0.56 % (2833801)Instructions burned: 157 (million)
% 1.12/0.56 % (2833833)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3463639772:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.12/0.56 % (2833825)Refutation not found, incomplete strategy
% 1.12/0.56 % (2833825)------------------------------
% 1.12/0.56 % (2833825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.56 % (2833825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.56 % (2833825)CaDiCaL version: 2.1.3
% 1.12/0.56 % (2833825)Termination reason: Refutation not found, incomplete strategy
% 1.12/0.56 % (2833825)Time elapsed: 0.029 s
% 1.12/0.56 % (2833825)Peak memory usage: 13 MB
% 1.12/0.56 % (2833825)Instructions burned: 57 (million)
% 1.12/0.56 % (2833834)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2647562409:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.12/0.56 % (2833825)------------------------------
% 1.12/0.56 % (2833825)------------------------------
% 1.12/0.56 % (2833836)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3903257451:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.12/0.56 % (2833834)Instruction limit reached!
% 1.12/0.56 % (2833834)------------------------------
% 1.12/0.56 % (2833834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.56 % (2833834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.56 % (2833834)CaDiCaL version: 2.1.3
% 1.12/0.56 % (2833834)Termination reason: Instruction limit
% 1.12/0.56 % (2833834)Termination phase: shuffling
% 1.12/0.56 % (2833834)Time elapsed: 0.008 s
% 1.12/0.56 % (2833834)Peak memory usage: 10 MB
% 1.12/0.56 % (2833834)Instructions burned: 16 (million)
% 1.12/0.56 % (2833836)Instruction limit reached!
% 1.12/0.56 % (2833836)------------------------------
% 1.12/0.56 % (2833836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.56 % (2833836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.56 % (2833836)CaDiCaL version: 2.1.3
% 1.12/0.56 % (2833836)Termination reason: Instruction limit
% 1.12/0.56 % (2833836)Termination phase: shuffling
% 1.12/0.56 % (2833836)Time elapsed: 0.013 s
% 1.12/0.56 % (2833836)Peak memory usage: 10 MB
% 1.12/0.56 % (2833836)Instructions burned: 27 (million)
% 1.12/0.56 % (2833835)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3941305171:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.12/0.56 % (2833840)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3634440837:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.12/0.56 % (2833835)Instruction limit reached!
% 1.12/0.56 % (2833835)------------------------------
% 1.12/0.56 % (2833835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.56 % (2833835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.56 % (2833835)CaDiCaL version: 2.1.3
% 1.12/0.56 % (2833835)Termination reason: Instruction limit
% 1.12/0.56 % (2833835)Termination phase: shuffling
% 1.12/0.56 % (2833835)Time elapsed: 0.002 s
% 2.00/0.63 % (2833835)Peak memory usage: 10 MB
% 2.00/0.63 % (2833835)Instructions burned: 3 (million)
% 2.00/0.63 % (2833837)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3722315786:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.00/0.63 % (2833842)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.00/0.63 % (2833842)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.00/0.63 % (2833842)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=2104216273:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.00/0.63 % (2833843)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.00/0.63 % (2833837)Instruction limit reached!
% 2.00/0.63 % (2833837)------------------------------
% 2.00/0.63 % (2833837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.00/0.63 % (2833837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.00/0.63 % (2833837)CaDiCaL version: 2.1.3
% 2.00/0.63 % (2833837)Termination reason: Instruction limit
% 2.00/0.63 % (2833837)Termination phase: shuffling
% 2.00/0.63 % (2833837)Time elapsed: 0.012 s
% 2.00/0.63 % (2833837)Peak memory usage: 10 MB
% 2.00/0.63 % (2833837)Instructions burned: 24 (million)
% 2.00/0.63 % (2833842)Instruction limit reached!
% 2.00/0.63 % (2833842)------------------------------
% 2.00/0.63 % (2833842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.00/0.63 % (2833842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.00/0.63 % (2833842)CaDiCaL version: 2.1.3
% 2.00/0.63 % (2833842)Termination reason: Instruction limit
% 2.00/0.63 % (2833842)Termination phase: shuffling
% 2.00/0.63 % (2833842)Time elapsed: 0.007 s
% 2.00/0.63 % (2833842)Peak memory usage: 10 MB
% 2.00/0.63 % (2833842)Instructions burned: 14 (million)
% 2.00/0.63 % (2833843)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=1694695471:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.00/0.63 % (2833846)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=3194263399:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.00/0.63 % (2833843)Instruction limit reached!
% 2.00/0.63 % (2833843)------------------------------
% 2.00/0.63 % (2833843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.00/0.63 % (2833843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.00/0.63 % (2833843)CaDiCaL version: 2.1.3
% 2.00/0.63 % (2833843)Termination reason: Instruction limit
% 2.00/0.63 % (2833843)Termination phase: shuffling
% 2.00/0.63 % (2833843)Time elapsed: 0.005 s
% 2.00/0.63 % (2833843)Peak memory usage: 10 MB
% 2.00/0.63 % (2833843)Instructions burned: 10 (million)
% 2.00/0.63 % (2833840)Instruction limit reached!
% 2.00/0.63 % (2833840)------------------------------
% 2.00/0.63 % (2833840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.00/0.63 % (2833840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.00/0.63 % (2833840)CaDiCaL version: 2.1.3
% 2.00/0.63 % (2833840)Termination reason: Instruction limit
% 2.00/0.63 % (2833840)Termination phase: Preprocessing 3
% 2.00/0.63 % (2833840)Time elapsed: 0.029 s
% 2.00/0.63 % (2833840)Peak memory usage: 11 MB
% 2.00/0.63 % (2833840)Instructions burned: 60 (million)
% 2.00/0.63 % (2833798)Instruction limit reached!
% 2.00/0.63 % (2833798)------------------------------
% 2.00/0.63 % (2833798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.00/0.63 % (2833798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.00/0.63 % (2833798)CaDiCaL version: 2.1.3
% 2.00/0.63 % (2833798)Termination reason: Instruction limit
% 2.00/0.63 % (2833798)Termination phase: Saturation
% 2.00/0.63 % (2833798)Time elapsed: 0.177 s
% 2.00/0.63 % (2833798)Peak memory usage: 16 MB
% 2.00/0.63 % (2833798)Instructions burned: 635 (million)
% 2.00/0.63 % (2833850)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2445602143:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.19/0.69 % (2833851)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3062650747:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.19/0.69 % (2833846)Instruction limit reached!
% 2.19/0.69 % (2833846)------------------------------
% 2.19/0.69 % (2833846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.69 % (2833846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.69 % (2833846)CaDiCaL version: 2.1.3
% 2.19/0.69 % (2833846)Termination reason: Instruction limit
% 2.19/0.69 % (2833846)Termination phase: shuffling
% 2.19/0.69 % (2833846)Time elapsed: 0.015 s
% 2.19/0.69 % (2833846)Peak memory usage: 10 MB
% 2.19/0.69 % (2833846)Instructions burned: 33 (million)
% 2.19/0.69 % (2833850)Instruction limit reached!
% 2.19/0.69 % (2833850)------------------------------
% 2.19/0.69 % (2833850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.69 % (2833850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.69 % (2833850)CaDiCaL version: 2.1.3
% 2.19/0.69 % (2833850)Termination reason: Instruction limit
% 2.19/0.69 % (2833850)Termination phase: shuffling
% 2.19/0.69 % (2833850)Time elapsed: 0.004 s
% 2.19/0.69 % (2833850)Peak memory usage: 10 MB
% 2.19/0.69 % (2833850)Instructions burned: 7 (million)
% 2.19/0.69 % (2833853)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4110768907:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.19/0.69 % (2833858)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2940097397:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.19/0.69 % (2833851)Instruction limit reached!
% 2.19/0.69 % (2833851)------------------------------
% 2.19/0.69 % (2833851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.69 % (2833851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.69 % (2833851)CaDiCaL version: 2.1.3
% 2.19/0.69 % (2833851)Termination reason: Instruction limit
% 2.19/0.69 % (2833851)Termination phase: shuffling
% 2.19/0.69 % (2833851)Time elapsed: 0.012 s
% 2.19/0.69 % (2833851)Peak memory usage: 10 MB
% 2.19/0.69 % (2833851)Instructions burned: 25 (million)
% 2.19/0.69 % (2833854)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2688748025:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.19/0.69 % (2833853)Instruction limit reached!
% 2.19/0.69 % (2833853)------------------------------
% 2.19/0.69 % (2833853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.69 % (2833853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.69 % (2833853)CaDiCaL version: 2.1.3
% 2.19/0.69 % (2833853)Termination reason: Instruction limit
% 2.19/0.69 % (2833853)Termination phase: shuffling
% 2.19/0.69 % (2833853)Time elapsed: 0.010 s
% 2.19/0.69 % (2833853)Peak memory usage: 10 MB
% 2.19/0.69 % (2833853)Instructions burned: 21 (million)
% 2.19/0.69 % (2833857)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3226818822:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.19/0.69 % (2833859)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3861658192:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.19/0.69 % (2833862)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.19/0.69 % (2833862)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2340254832:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.19/0.69 % (2833862)Instruction limit reached!
% 2.19/0.69 % (2833862)------------------------------
% 2.19/0.69 % (2833862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.69 % (2833862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.69 % (2833862)CaDiCaL version: 2.1.3
% 2.19/0.69 % (2833862)Termination reason: Instruction limit
% 2.19/0.69 % (2833862)Termination phase: shuffling
% 2.19/0.69 % (2833862)Time elapsed: 0.004 s
% 2.19/0.69 % (2833862)Peak memory usage: 10 MB
% 2.19/0.69 % (2833862)Instructions burned: 8 (million)
% 2.19/0.69 % (2833864)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3736230218:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.86/0.81 % (2833869)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=3423815272:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.86/0.81 % (2833858)Instruction limit reached!
% 2.86/0.81 % (2833858)------------------------------
% 2.86/0.81 % (2833858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.81 % (2833858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.81 % (2833858)CaDiCaL version: 2.1.3
% 2.86/0.81 % (2833858)Termination reason: Instruction limit
% 2.86/0.81 % (2833858)Termination phase: Saturation
% 2.86/0.81 % (2833858)Time elapsed: 0.053 s
% 2.86/0.81 % (2833858)Peak memory usage: 14 MB
% 2.86/0.81 % (2833858)Instructions burned: 194 (million)
% 2.86/0.81 % (2833859)Instruction limit reached!
% 2.86/0.81 % (2833859)------------------------------
% 2.86/0.81 % (2833859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.81 % (2833859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.81 % (2833859)CaDiCaL version: 2.1.3
% 2.86/0.81 % (2833859)Termination reason: Instruction limit
% 2.86/0.81 % (2833859)Termination phase: Preprocessing 1
% 2.86/0.81 % (2833859)Time elapsed: 0.042 s
% 2.86/0.81 % (2833859)Peak memory usage: 10 MB
% 2.86/0.81 % (2833859)Instructions burned: 42 (million)
% 2.86/0.81 % (2833871)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.86/0.81 % (2833871)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3144274998:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.86/0.81 % (2833871)Instruction limit reached!
% 2.86/0.81 % (2833871)------------------------------
% 2.86/0.81 % (2833871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.81 % (2833871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.81 % (2833871)CaDiCaL version: 2.1.3
% 2.86/0.81 % (2833871)Termination reason: Instruction limit
% 2.86/0.81 % (2833871)Termination phase: shuffling
% 2.86/0.81 % (2833871)Time elapsed: 0.003 s
% 2.86/0.81 % (2833871)Peak memory usage: 10 MB
% 2.86/0.81 % (2833871)Instructions burned: 10 (million)
% 2.86/0.81 % (2833857)Instruction limit reached!
% 2.86/0.81 % (2833857)------------------------------
% 2.86/0.81 % (2833857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.81 % (2833857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.81 % (2833857)CaDiCaL version: 2.1.3
% 2.86/0.81 % (2833857)Termination reason: Instruction limit
% 2.86/0.81 % (2833857)Termination phase: Saturation
% 2.86/0.81 % (2833857)Time elapsed: 0.067 s
% 2.86/0.81 % (2833857)Peak memory usage: 13 MB
% 2.86/0.81 % (2833857)Instructions burned: 143 (million)
% 2.86/0.81 % (2833874)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=4261495121:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.86/0.81 % (2833833)Instruction limit reached!
% 2.86/0.81 % (2833833)------------------------------
% 2.86/0.81 % (2833833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.81 % (2833833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.81 % (2833833)CaDiCaL version: 2.1.3
% 2.86/0.81 % (2833833)Termination reason: Instruction limit
% 2.86/0.81 % (2833833)Termination phase: Saturation
% 2.86/0.81 % (2833833)Time elapsed: 0.160 s
% 2.86/0.81 % (2833833)Peak memory usage: 15 MB
% 2.86/0.81 % (2833833)Instructions burned: 328 (million)
% 2.86/0.81 % (2833875)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=2900318894:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 2.86/0.81 % (2833872)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1364799363:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.86/0.81 % (2833874)Instruction limit reached!
% 2.86/0.81 % (2833874)------------------------------
% 2.86/0.81 % (2833874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.34/0.92 % (2833874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/0.92 % (2833874)CaDiCaL version: 2.1.3
% 3.34/0.92 % (2833874)Termination reason: Instruction limit
% 3.34/0.92 % (2833874)Termination phase: shuffling
% 3.34/0.92 % (2833874)Time elapsed: 0.009 s
% 3.34/0.92 % (2833874)Peak memory usage: 10 MB
% 3.34/0.92 % (2833874)Instructions burned: 19 (million)
% 3.34/0.92 % (2833877)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=1210922601:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.34/0.92 % (2833872)Instruction limit reached!
% 3.34/0.92 % (2833872)------------------------------
% 3.34/0.92 % (2833872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.34/0.92 % (2833872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/0.92 % (2833872)CaDiCaL version: 2.1.3
% 3.34/0.92 % (2833872)Termination reason: Instruction limit
% 3.34/0.92 % (2833872)Termination phase: shuffling
% 3.34/0.92 % (2833872)Time elapsed: 0.019 s
% 3.34/0.92 % (2833872)Peak memory usage: 11 MB
% 3.34/0.92 % (2833872)Instructions burned: 22 (million)
% 3.34/0.92 % (2833880)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=2485518222:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.34/0.92 % (2833864)Instruction limit reached!
% 3.34/0.92 % (2833864)------------------------------
% 3.34/0.92 % (2833864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.34/0.92 % (2833864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/0.92 % (2833864)CaDiCaL version: 2.1.3
% 3.34/0.92 % (2833864)Termination reason: Instruction limit
% 3.34/0.92 % (2833864)Termination phase: Saturation
% 3.34/0.92 % (2833864)Time elapsed: 0.097 s
% 3.34/0.92 % (2833864)Peak memory usage: 14 MB
% 3.34/0.92 % (2833864)Instructions burned: 181 (million)
% 3.34/0.92 % (2833869)Instruction limit reached!
% 3.34/0.92 % (2833869)------------------------------
% 3.34/0.92 % (2833869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.34/0.92 % (2833869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/0.92 % (2833869)CaDiCaL version: 2.1.3
% 3.34/0.92 % (2833869)Termination reason: Instruction limit
% 3.34/0.92 % (2833869)Termination phase: Saturation
% 3.34/0.92 % (2833869)Time elapsed: 0.087 s
% 3.34/0.92 % (2833869)Peak memory usage: 15 MB
% 3.34/0.92 % (2833869)Instructions burned: 170 (million)
% 3.34/0.92 % (2833880)Instruction limit reached!
% 3.34/0.92 % (2833880)------------------------------
% 3.34/0.92 % (2833880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.34/0.92 % (2833880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/0.92 % (2833880)CaDiCaL version: 2.1.3
% 3.34/0.92 % (2833880)Termination reason: Instruction limit
% 3.34/0.92 % (2833880)Termination phase: Property scanning
% 3.34/0.92 % (2833880)Time elapsed: 0.021 s
% 3.34/0.92 % (2833880)Peak memory usage: 10 MB
% 3.34/0.92 % (2833880)Instructions burned: 46 (million)
% 3.34/0.92 % (2833886)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=121175476:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 3.34/0.92 % (2833887)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.34/0.92 % (2833887)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1793776101:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.34/0.92 % (2833883)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1247764396:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.34/0.92 % (2833886)Instruction limit reached!
% 3.34/0.92 % (2833886)------------------------------
% 3.34/0.92 % (2833886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.34/0.92 % (2833886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/0.92 % (2833886)CaDiCaL version: 2.1.3
% 3.34/0.92 % (2833886)Termination reason: Instruction limit
% 5.01/1.05 % (2833886)Termination phase: shuffling
% 5.01/1.05 % (2833886)Time elapsed: 0.011 s
% 5.01/1.05 % (2833886)Peak memory usage: 10 MB
% 5.01/1.05 % (2833886)Instructions burned: 22 (million)
% 5.01/1.05 % (2833888)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2982273476:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 5.01/1.05 % (2833888)Instruction limit reached!
% 5.01/1.05 % (2833888)------------------------------
% 5.01/1.05 % (2833888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.05 % (2833888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.05 % (2833888)CaDiCaL version: 2.1.3
% 5.01/1.05 % (2833888)Termination reason: Instruction limit
% 5.01/1.05 % (2833888)Termination phase: shuffling
% 5.01/1.05 % (2833888)Time elapsed: 0.008 s
% 5.01/1.05 % (2833888)Peak memory usage: 10 MB
% 5.01/1.05 % (2833888)Instructions burned: 14 (million)
% 5.01/1.05 % (2833892)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=1381928592:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 5.01/1.05 % (2833894)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1668044837:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 5.01/1.05 % (2833894)Instruction limit reached!
% 5.01/1.05 % (2833894)------------------------------
% 5.01/1.05 % (2833894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.05 % (2833894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.05 % (2833894)CaDiCaL version: 2.1.3
% 5.01/1.05 % (2833894)Termination reason: Instruction limit
% 5.01/1.05 % (2833894)Termination phase: Preprocessing 3
% 5.01/1.05 % (2833894)Time elapsed: 0.025 s
% 5.01/1.05 % (2833894)Peak memory usage: 11 MB
% 5.01/1.05 % (2833894)Instructions burned: 53 (million)
% 5.01/1.05 % (2833892)Instruction limit reached!
% 5.01/1.05 % (2833892)------------------------------
% 5.01/1.05 % (2833892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.05 % (2833892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.05 % (2833892)CaDiCaL version: 2.1.3
% 5.01/1.05 % (2833892)Termination reason: Instruction limit
% 5.01/1.05 % (2833892)Termination phase: Property scanning
% 5.01/1.05 % (2833892)Time elapsed: 0.059 s
% 5.01/1.05 % (2833892)Peak memory usage: 10 MB
% 5.01/1.05 % (2833892)Instructions burned: 67 (million)
% 5.01/1.05 % (2833897)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2217248533:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 5.01/1.05 % (2833887)Instruction limit reached!
% 5.01/1.05 % (2833887)------------------------------
% 5.01/1.05 % (2833887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.05 % (2833887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.05 % (2833887)CaDiCaL version: 2.1.3
% 5.01/1.05 % (2833887)Termination reason: Instruction limit
% 5.01/1.05 % (2833887)Termination phase: Saturation
% 5.01/1.05 % (2833887)Time elapsed: 0.094 s
% 5.01/1.05 % (2833887)Peak memory usage: 14 MB
% 5.01/1.05 % (2833887)Instructions burned: 201 (million)
% 5.01/1.05 % (2833897)Instruction limit reached!
% 5.01/1.05 % (2833897)------------------------------
% 5.01/1.05 % (2833897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.05 % (2833897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.05 % (2833897)CaDiCaL version: 2.1.3
% 5.01/1.05 % (2833897)Termination reason: Instruction limit
% 5.01/1.05 % (2833897)Termination phase: shuffling
% 5.01/1.05 % (2833897)Time elapsed: 0.015 s
% 5.01/1.05 % (2833897)Peak memory usage: 10 MB
% 5.01/1.05 % (2833897)Instructions burned: 31 (million)
% 5.01/1.05 % (2833898)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3379464358:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 5.01/1.05 % (2833900)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=1472785809:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 5.01/1.05 % (2833901)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3146217260:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 5.82/1.23 % (2833900)Instruction limit reached!
% 5.82/1.23 % (2833900)------------------------------
% 5.82/1.23 % (2833900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.23 % (2833900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.23 % (2833900)CaDiCaL version: 2.1.3
% 5.82/1.23 % (2833900)Termination reason: Instruction limit
% 5.82/1.23 % (2833900)Termination phase: shuffling
% 5.82/1.23 % (2833900)Time elapsed: 0.016 s
% 5.82/1.23 % (2833900)Peak memory usage: 10 MB
% 5.82/1.23 % (2833900)Instructions burned: 34 (million)
% 5.82/1.23 % (2833875)Instruction limit reached!
% 5.82/1.23 % (2833875)------------------------------
% 5.82/1.23 % (2833875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.23 % (2833875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.23 % (2833875)CaDiCaL version: 2.1.3
% 5.82/1.23 % (2833875)Termination reason: Instruction limit
% 5.82/1.23 % (2833875)Termination phase: Saturation
% 5.82/1.23 % (2833875)Time elapsed: 0.188 s
% 5.82/1.23 % (2833875)Peak memory usage: 16 MB
% 5.82/1.23 % (2833875)Instructions burned: 317 (million)
% 5.82/1.23 % (2833905)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.82/1.23 % (2833905)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2132051360:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 5.82/1.23 % (2833906)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2086008287:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 5.82/1.23 % (2833901)Instruction limit reached!
% 5.82/1.23 % (2833901)------------------------------
% 5.82/1.23 % (2833901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.23 % (2833901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.23 % (2833901)CaDiCaL version: 2.1.3
% 5.82/1.23 % (2833901)Termination reason: Instruction limit
% 5.82/1.23 % (2833901)Termination phase: Property scanning
% 5.82/1.23 % (2833901)Time elapsed: 0.033 s
% 5.82/1.23 % (2833901)Peak memory usage: 12 MB
% 5.82/1.23 % (2833901)Instructions burned: 67 (million)
% 5.82/1.23 % (2833898)Instruction limit reached!
% 5.82/1.23 % (2833898)------------------------------
% 5.82/1.23 % (2833898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.23 % (2833898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.23 % (2833898)CaDiCaL version: 2.1.3
% 5.82/1.23 % (2833898)Termination reason: Instruction limit
% 5.82/1.23 % (2833898)Termination phase: Saturation
% 5.82/1.23 % (2833898)Time elapsed: 0.067 s
% 5.82/1.23 % (2833898)Peak memory usage: 14 MB
% 5.82/1.23 % (2833898)Instructions burned: 138 (million)
% 5.82/1.23 % (2833909)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1418370916:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 5.82/1.23 % (2833910)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1421457559:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 5.82/1.23 % (2833910)Refutation not found, incomplete strategy
% 5.82/1.23 % (2833910)------------------------------
% 5.82/1.23 % (2833910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.23 % (2833910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.23 % (2833910)CaDiCaL version: 2.1.3
% 5.82/1.23 % (2833910)Termination reason: Refutation not found, incomplete strategy
% 5.82/1.23 % (2833910)Time elapsed: 0.024 s
% 5.82/1.23 % (2833910)Peak memory usage: 13 MB
% 5.82/1.23 % (2833910)Instructions burned: 47 (million)
% 5.82/1.23 % (2833910)------------------------------
% 5.82/1.23 % (2833910)------------------------------
% 5.82/1.23 % (2833909)Instruction limit reached!
% 5.82/1.23 % (2833909)------------------------------
% 5.82/1.23 % (2833909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.23 % (2833909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.23 % (2833909)CaDiCaL version: 2.1.3
% 5.82/1.23 % (2833909)Termination reason: Instruction limit
% 5.82/1.23 % (2833909)Termination phase: Property scanning
% 5.82/1.23 % (2833909)Time elapsed: 0.047 s
% 5.82/1.23 % (2833909)Peak memory usage: 12 MB
% 5.82/1.23 % (2833909)Instructions burned: 97 (million)
% 5.82/1.23 % (2833905)Instruction limit reached!
% 5.82/1.23 % (2833905)------------------------------
% 5.82/1.23 % (2833905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.35 % (2833905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.35 % (2833905)CaDiCaL version: 2.1.3
% 6.36/1.35 % (2833905)Termination reason: Instruction limit
% 6.36/1.35 % (2833905)Termination phase: Saturation
% 6.36/1.35 % (2833905)Time elapsed: 0.080 s
% 6.36/1.35 % (2833905)Peak memory usage: 13 MB
% 6.36/1.35 % (2833905)Instructions burned: 181 (million)
% 6.36/1.35 % (2833913)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3757751632:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/874Mi)
% 6.36/1.35 % (2833914)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2631835088:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/515Mi)
% 6.36/1.35 % (2833883)Instruction limit reached!
% 6.36/1.35 % (2833883)------------------------------
% 6.36/1.35 % (2833883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.35 % (2833883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.35 % (2833883)CaDiCaL version: 2.1.3
% 6.36/1.35 % (2833883)Termination reason: Instruction limit
% 6.36/1.35 % (2833883)Termination phase: Saturation
% 6.36/1.35 % (2833883)Time elapsed: 0.262 s
% 6.36/1.35 % (2833883)Peak memory usage: 16 MB
% 6.36/1.35 % (2833883)Instructions burned: 481 (million)
% 6.36/1.35 % (2833915)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2798330758:st=1.5:i=130:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/130Mi)
% 6.36/1.35 % (2833906)Instruction limit reached!
% 6.36/1.35 % (2833906)------------------------------
% 6.36/1.35 % (2833906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.35 % (2833906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.35 % (2833906)CaDiCaL version: 2.1.3
% 6.36/1.35 % (2833906)Termination reason: Instruction limit
% 6.36/1.35 % (2833906)Termination phase: Saturation
% 6.36/1.35 % (2833906)Time elapsed: 0.147 s
% 6.36/1.35 % (2833906)Peak memory usage: 15 MB
% 6.36/1.35 % (2833906)Instructions burned: 247 (million)
% 6.36/1.35 % (2833919)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=257119891:i=44:ep=R:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/44Mi)
% 6.36/1.35 % (2833921)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2484557717:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 6.36/1.35 % (2833915)Instruction limit reached!
% 6.36/1.35 % (2833915)------------------------------
% 6.36/1.35 % (2833915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.35 % (2833915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.35 % (2833915)CaDiCaL version: 2.1.3
% 6.36/1.35 % (2833915)Termination reason: Instruction limit
% 6.36/1.35 % (2833915)Termination phase: Property scanning
% 6.36/1.35 % (2833915)Time elapsed: 0.064 s
% 6.36/1.35 % (2833915)Peak memory usage: 12 MB
% 6.36/1.35 % (2833915)Instructions burned: 130 (million)
% 6.36/1.35 % (2833919)Instruction limit reached!
% 6.36/1.35 % (2833919)------------------------------
% 6.36/1.35 % (2833919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.35 % (2833919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.35 % (2833919)CaDiCaL version: 2.1.3
% 6.36/1.35 % (2833919)Termination reason: Instruction limit
% 6.36/1.35 % (2833919)Termination phase: Property scanning
% 6.36/1.35 % (2833919)Time elapsed: 0.039 s
% 6.36/1.35 % (2833919)Peak memory usage: 11 MB
% 6.36/1.35 % (2833919)Instructions burned: 45 (million)
% 6.36/1.35 % (2833923)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=2060602946:i=450:rtra=on:ixr=off:ntd=on_2992 on theBenchmark for (2992ds/450Mi)
% 6.36/1.35 % (2833924)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=2675044657:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/95Mi)
% 6.36/1.35 % (2833877)Instruction limit reached!
% 6.36/1.35 % (2833877)------------------------------
% 6.36/1.35 % (2833877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.36/1.35 % (2833877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.36/1.35 % (2833877)CaDiCaL version: 2.1.3
% 6.36/1.35 % (2833877)Termination reason: Instruction limit
% 6.79/1.44 % (2833877)Termination phase: Saturation
% 6.79/1.44 % (2833877)Time elapsed: 0.402 s
% 6.79/1.44 % (2833877)Peak memory usage: 18 MB
% 6.79/1.44 % (2833877)Instructions burned: 854 (million)
% 6.79/1.44 % (2833927)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=2164303478:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2992 on theBenchmark for (2992ds/65Mi)
% 6.79/1.44 % (2833924)Instruction limit reached!
% 6.79/1.44 % (2833924)------------------------------
% 6.79/1.44 % (2833924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.79/1.44 % (2833924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.79/1.44 % (2833924)CaDiCaL version: 2.1.3
% 6.79/1.44 % (2833924)Termination reason: Instruction limit
% 6.79/1.44 % (2833924)Termination phase: Property scanning
% 6.79/1.44 % (2833924)Time elapsed: 0.047 s
% 6.79/1.44 % (2833924)Peak memory usage: 12 MB
% 6.79/1.44 % (2833924)Instructions burned: 96 (million)
% 6.79/1.44 % (2833927)Instruction limit reached!
% 6.79/1.44 % (2833927)------------------------------
% 6.79/1.44 % (2833927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.79/1.44 % (2833927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.79/1.44 % (2833927)CaDiCaL version: 2.1.3
% 6.79/1.44 % (2833927)Termination reason: Instruction limit
% 6.79/1.44 % (2833927)Termination phase: Property scanning
% 6.79/1.44 % (2833927)Time elapsed: 0.030 s
% 6.79/1.44 % (2833927)Peak memory usage: 11 MB
% 6.79/1.44 % (2833927)Instructions burned: 65 (million)
% 6.79/1.44 % (2833929)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=402295858: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_2992 on theBenchmark for (2992ds/105Mi)
% 6.79/1.44 % (2833930)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=3206878959:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2992 on theBenchmark for (2992ds/5755Mi)
% 6.79/1.44 % (2833929)Instruction limit reached!
% 6.79/1.44 % (2833929)------------------------------
% 6.79/1.44 % (2833929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.79/1.44 % (2833929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.79/1.44 % (2833929)CaDiCaL version: 2.1.3
% 6.79/1.44 % (2833929)Termination reason: Instruction limit
% 6.79/1.44 % (2833929)Termination phase: Preprocessing 3
% 6.79/1.44 % (2833929)Time elapsed: 0.050 s
% 6.79/1.44 % (2833929)Peak memory usage: 11 MB
% 6.79/1.44 % (2833929)Instructions burned: 106 (million)
% 6.79/1.44 % (2833854)Instruction limit reached!
% 6.79/1.44 % (2833854)------------------------------
% 6.79/1.44 % (2833854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.79/1.44 % (2833854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.79/1.44 % (2833854)CaDiCaL version: 2.1.3
% 6.79/1.44 % (2833854)Termination reason: Instruction limit
% 6.79/1.44 % (2833854)Termination phase: Saturation
% 6.79/1.44 % (2833854)Time elapsed: 0.627 s
% 6.79/1.44 % (2833854)Peak memory usage: 17 MB
% 6.79/1.44 % (2833854)Instructions burned: 1243 (million)
% 6.79/1.44 % (2833933)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1530459318:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/375Mi)
% 6.79/1.44 % (2833934)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2872395909:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/495Mi)
% 6.79/1.44 % (2833914)Instruction limit reached!
% 6.79/1.44 % (2833914)------------------------------
% 6.79/1.44 % (2833914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.79/1.44 % (2833914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.79/1.44 % (2833914)CaDiCaL version: 2.1.3
% 6.79/1.44 % (2833914)Termination reason: Instruction limit
% 6.79/1.44 % (2833914)Termination phase: Saturation
% 6.79/1.44 % (2833914)Time elapsed: 0.282 s
% 6.79/1.44 % (2833914)Peak memory usage: 17 MB
% 6.79/1.44 % (2833914)Instructions burned: 516 (million)
% 6.79/1.44 % (2833923)Instruction limit reached!
% 6.79/1.44 % (2833923)------------------------------
% 6.79/1.44 % (2833923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.59 % (2833923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.59 % (2833923)CaDiCaL version: 2.1.3
% 7.51/1.59 % (2833923)Termination reason: Instruction limit
% 7.51/1.59 % (2833923)Termination phase: Saturation
% 7.51/1.59 % (2833923)Time elapsed: 0.189 s
% 7.51/1.59 % (2833923)Peak memory usage: 16 MB
% 7.51/1.59 % (2833923)Instructions burned: 450 (million)
% 7.51/1.59 % (2833938)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1104508887:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2990 on theBenchmark for (2990ds/91Mi)
% 7.51/1.59 % (2833937)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=884123989:cond=on:i=34:hud=10:nm=10:rtra=on_2990 on theBenchmark for (2990ds/34Mi)
% 7.51/1.59 % (2833937)Instruction limit reached!
% 7.51/1.59 % (2833937)------------------------------
% 7.51/1.59 % (2833937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.59 % (2833937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.59 % (2833937)CaDiCaL version: 2.1.3
% 7.51/1.59 % (2833937)Termination reason: Instruction limit
% 7.51/1.59 % (2833937)Termination phase: shuffling
% 7.51/1.59 % (2833937)Time elapsed: 0.017 s
% 7.51/1.59 % (2833937)Peak memory usage: 11 MB
% 7.51/1.59 % (2833937)Instructions burned: 36 (million)
% 7.51/1.59 % (2833938)Instruction limit reached!
% 7.51/1.59 % (2833938)------------------------------
% 7.51/1.59 % (2833938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.59 % (2833938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.59 % (2833938)CaDiCaL version: 2.1.3
% 7.51/1.59 % (2833938)Termination reason: Instruction limit
% 7.51/1.59 % (2833938)Termination phase: Function definition elimination
% 7.51/1.59 % (2833938)Time elapsed: 0.024 s
% 7.51/1.59 % (2833938)Peak memory usage: 12 MB
% 7.51/1.59 % (2833938)Instructions burned: 95 (million)
% 7.51/1.59 % (2833942)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2237287332:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2990 on theBenchmark for (2990ds/22Mi)
% 7.51/1.59 % (2833941)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=527478846:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2990 on theBenchmark for (2990ds/66Mi)
% 7.51/1.59 % (2833942)Instruction limit reached!
% 7.51/1.59 % (2833942)------------------------------
% 7.51/1.59 % (2833942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.59 % (2833942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.59 % (2833942)CaDiCaL version: 2.1.3
% 7.51/1.59 % (2833942)Termination reason: Instruction limit
% 7.51/1.59 % (2833942)Termination phase: shuffling
% 7.51/1.59 % (2833942)Time elapsed: 0.006 s
% 7.51/1.59 % (2833942)Peak memory usage: 10 MB
% 7.51/1.59 % (2833942)Instructions burned: 24 (million)
% 7.51/1.59 % (2833945)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=3996441547:i=338:bd=all:ins=4:rtra=on_2990 on theBenchmark for (2990ds/338Mi)
% 7.51/1.59 % (2833941)Instruction limit reached!
% 7.51/1.59 % (2833941)------------------------------
% 7.51/1.59 % (2833941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.59 % (2833941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.59 % (2833941)CaDiCaL version: 2.1.3
% 7.51/1.59 % (2833941)Termination reason: Instruction limit
% 7.51/1.59 % (2833941)Termination phase: Property scanning
% 7.51/1.59 % (2833941)Time elapsed: 0.033 s
% 7.51/1.59 % (2833941)Peak memory usage: 12 MB
% 7.51/1.59 % (2833941)Instructions burned: 66 (million)
% 7.51/1.59 % (2833947)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2342410133:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/28Mi)
% 7.51/1.59 % (2833947)Instruction limit reached!
% 7.51/1.59 % (2833947)------------------------------
% 7.51/1.59 % (2833947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.59 % (2833947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.59 % (2833947)CaDiCaL version: 2.1.3
% 7.51/1.59 % (2833947)Termination reason: Instruction limit
% 7.51/1.59 % (2833947)Termination phase: Property scanning
% 7.51/1.59 % (2833947)Time elapsed: 0.014 s
% 7.51/1.59 % (2833947)Peak memory usage: 10 MB
% 8.27/1.74 % (2833947)Instructions burned: 29 (million)
% 8.27/1.74 % (2833949)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 8.27/1.74 % (2833949)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=2556127503:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2989 on theBenchmark for (2989ds/137Mi)
% 8.27/1.74 % (2833913)Instruction limit reached!
% 8.27/1.74 % (2833913)------------------------------
% 8.27/1.74 % (2833913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.27/1.74 % (2833913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.27/1.74 % (2833913)CaDiCaL version: 2.1.3
% 8.27/1.74 % (2833913)Termination reason: Instruction limit
% 8.27/1.74 % (2833913)Termination phase: Saturation
% 8.27/1.74 % (2833913)Time elapsed: 0.450 s
% 8.27/1.74 % (2833913)Peak memory usage: 17 MB
% 8.27/1.74 % (2833913)Instructions burned: 875 (million)
% 8.27/1.74 % (2833945)Instruction limit reached!
% 8.27/1.74 % (2833945)------------------------------
% 8.27/1.74 % (2833945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.27/1.74 % (2833945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.27/1.74 % (2833945)CaDiCaL version: 2.1.3
% 8.27/1.74 % (2833945)Termination reason: Instruction limit
% 8.27/1.74 % (2833945)Termination phase: Saturation
% 8.27/1.74 % (2833945)Time elapsed: 0.095 s
% 8.27/1.74 % (2833945)Peak memory usage: 17 MB
% 8.27/1.74 % (2833945)Instructions burned: 340 (million)
% 8.27/1.74 % (2833952)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2303473650:i=227:sd=1:bd=all:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/227Mi)
% 8.27/1.74 % (2833933)Instruction limit reached!
% 8.27/1.74 % (2833933)------------------------------
% 8.27/1.74 % (2833933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.27/1.74 % (2833951)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=2655807282:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2989 on theBenchmark for (2989ds/340Mi)
% 8.27/1.74 % (2833933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.27/1.74 % (2833933)CaDiCaL version: 2.1.3
% 8.27/1.74 % (2833933)Termination reason: Instruction limit
% 8.27/1.74 % (2833933)Termination phase: Saturation
% 8.27/1.74 % (2833933)Time elapsed: 0.217 s
% 8.27/1.74 % (2833933)Peak memory usage: 15 MB
% 8.27/1.74 % (2833933)Instructions burned: 376 (million)
% 8.27/1.74 % (2833952)Refutation not found, incomplete strategy
% 8.27/1.74 % (2833952)------------------------------
% 8.27/1.74 % (2833952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.27/1.74 % (2833952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.27/1.74 % (2833952)CaDiCaL version: 2.1.3
% 8.27/1.74 % (2833952)Termination reason: Refutation not found, incomplete strategy
% 8.27/1.74 % (2833952)Time elapsed: 0.013 s
% 8.27/1.74 % (2833952)Peak memory usage: 13 MB
% 8.27/1.74 % (2833952)Instructions burned: 47 (million)
% 8.27/1.74 % (2833952)------------------------------
% 8.27/1.74 % (2833952)------------------------------
% 8.27/1.74 % (2833955)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 8.27/1.74 % (2833955)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=809339670:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/373Mi)
% 8.27/1.74 % (2833956)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2923312191:i=116:ep=RSTC:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/116Mi)
% 8.27/1.74 % (2833949)Instruction limit reached!
% 8.27/1.74 % (2833949)------------------------------
% 8.27/1.74 % (2833949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.27/1.74 % (2833949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.27/1.74 % (2833949)CaDiCaL version: 2.1.3
% 8.27/1.74 % (2833949)Termination reason: Instruction limit
% 8.27/1.74 % (2833949)Termination phase: Saturation
% 8.27/1.74 % (2833949)Time elapsed: 0.061 s
% 8.27/1.74 % (2833949)Peak memory usage: 13 MB
% 8.27/1.74 % (2833949)Instructions burned: 139 (million)
% 8.27/1.74 % (2833921)Instruction limit reached!
% 8.27/1.74 % (2833921)------------------------------
% 8.99/1.87 % (2833921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.87 % (2833921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.87 % (2833921)CaDiCaL version: 2.1.3
% 8.99/1.87 % (2833921)Termination reason: Instruction limit
% 8.99/1.87 % (2833921)Termination phase: Saturation
% 8.99/1.87 % (2833921)Time elapsed: 0.436 s
% 8.99/1.87 % (2833921)Peak memory usage: 16 MB
% 8.99/1.87 % (2833921)Instructions burned: 572 (million)
% 8.99/1.87 % (2833934)Instruction limit reached!
% 8.99/1.87 % (2833934)------------------------------
% 8.99/1.87 % (2833934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.87 % (2833934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.87 % (2833934)CaDiCaL version: 2.1.3
% 8.99/1.87 % (2833934)Termination reason: Instruction limit
% 8.99/1.87 % (2833934)Termination phase: Saturation
% 8.99/1.87 % (2833934)Time elapsed: 0.257 s
% 8.99/1.87 % (2833934)Peak memory usage: 18 MB
% 8.99/1.87 % (2833934)Instructions burned: 496 (million)
% 8.99/1.87 % (2833959)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=4103076581:i=575:rtra=on_2988 on theBenchmark for (2988ds/575Mi)
% 8.99/1.88 % (2833956)Instruction limit reached!
% 8.99/1.88 % (2833956)------------------------------
% 8.99/1.88 % (2833956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.88 % (2833956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.88 % (2833956)CaDiCaL version: 2.1.3
% 8.99/1.88 % (2833956)Termination reason: Instruction limit
% 8.99/1.88 % (2833956)Termination phase: Property scanning
% 8.99/1.88 % (2833956)Time elapsed: 0.029 s
% 8.99/1.88 % (2833956)Peak memory usage: 12 MB
% 8.99/1.88 % (2833956)Instructions burned: 118 (million)
% 8.99/1.88 % (2833960)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2508879305:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2988 on theBenchmark for (2988ds/270Mi)
% 8.99/1.88 % (2833961)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=3699798134:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2988 on theBenchmark for (2988ds/9840Mi)
% 8.99/1.88 % (2833963)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=739204367:i=421:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/421Mi)
% 8.99/1.88 % (2833951)Instruction limit reached!
% 8.99/1.88 % (2833951)------------------------------
% 8.99/1.88 % (2833951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.88 % (2833951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.88 % (2833951)CaDiCaL version: 2.1.3
% 8.99/1.88 % (2833951)Termination reason: Instruction limit
% 8.99/1.88 % (2833951)Termination phase: Saturation
% 8.99/1.88 % (2833951)Time elapsed: 0.170 s
% 8.99/1.88 % (2833951)Peak memory usage: 15 MB
% 8.99/1.88 % (2833951)Instructions burned: 340 (million)
% 8.99/1.88 % (2833963)Instruction limit reached!
% 8.99/1.88 % (2833963)------------------------------
% 8.99/1.88 % (2833963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.88 % (2833963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.88 % (2833963)CaDiCaL version: 2.1.3
% 8.99/1.88 % (2833963)Termination reason: Instruction limit
% 8.99/1.88 % (2833963)Termination phase: Saturation
% 8.99/1.88 % (2833963)Time elapsed: 0.112 s
% 8.99/1.88 % (2833963)Peak memory usage: 16 MB
% 8.99/1.88 % (2833963)Instructions burned: 424 (million)
% 8.99/1.88 % (2833968)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=368894188:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/31Mi)
% 8.99/1.88 % (2833967)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 8.99/1.88 % (2833967)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=1629990130:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/270Mi)
% 8.99/1.88 % (2833960)Instruction limit reached!
% 9.38/2.06 % (2833960)------------------------------
% 9.38/2.06 % (2833960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.38/2.06 % (2833960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.06 % (2833960)CaDiCaL version: 2.1.3
% 9.38/2.06 % (2833960)Termination reason: Instruction limit
% 9.38/2.06 % (2833960)Termination phase: Saturation
% 9.38/2.06 % (2833960)Time elapsed: 0.130 s
% 9.38/2.06 % (2833960)Peak memory usage: 14 MB
% 9.38/2.06 % (2833960)Instructions burned: 271 (million)
% 9.38/2.06 % (2833968)Instruction limit reached!
% 9.38/2.06 % (2833968)------------------------------
% 9.38/2.06 % (2833968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.38/2.06 % (2833968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.06 % (2833968)CaDiCaL version: 2.1.3
% 9.38/2.06 % (2833968)Termination reason: Instruction limit
% 9.38/2.06 % (2833968)Termination phase: shuffling
% 9.38/2.06 % (2833968)Time elapsed: 0.008 s
% 9.38/2.06 % (2833968)Peak memory usage: 10 MB
% 9.38/2.06 % (2833968)Instructions burned: 32 (million)
% 9.38/2.06 % (2833955)Instruction limit reached!
% 9.38/2.06 % (2833955)------------------------------
% 9.38/2.06 % (2833955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.38/2.06 % (2833955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.06 % (2833955)CaDiCaL version: 2.1.3
% 9.38/2.06 % (2833955)Termination reason: Instruction limit
% 9.38/2.06 % (2833955)Termination phase: Saturation
% 9.38/2.06 % (2833955)Time elapsed: 0.183 s
% 9.38/2.06 % (2833955)Peak memory usage: 14 MB
% 9.38/2.06 % (2833955)Instructions burned: 375 (million)
% 9.38/2.06 % (2833972)dis+10_2_sil=128000:si=on:random_seed=172303693:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2987 on theBenchmark for (2987ds/339Mi)
% 9.38/2.06 % (2833971)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 9.38/2.06 % (2833971)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 9.38/2.06 % (2833971)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=4247367576:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2987 on theBenchmark for (2987ds/1440Mi)
% 9.38/2.06 % (2833973)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=1226162143:i=111:add=on:fgj=on:rtra=on:fdi=1024_2986 on theBenchmark for (2986ds/111Mi)
% 9.38/2.06 % (2833973)Instruction limit reached!
% 9.38/2.06 % (2833973)------------------------------
% 9.38/2.06 % (2833973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.38/2.06 % (2833973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.06 % (2833973)CaDiCaL version: 2.1.3
% 9.38/2.06 % (2833973)Termination reason: Instruction limit
% 9.38/2.06 % (2833973)Termination phase: Property scanning
% 9.38/2.06 % (2833973)Time elapsed: 0.052 s
% 9.38/2.06 % (2833973)Peak memory usage: 12 MB
% 9.38/2.06 % (2833973)Instructions burned: 111 (million)
% 9.38/2.06 % (2833977)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=1158621164:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2986 on theBenchmark for (2986ds/122Mi)
% 9.38/2.06 % (2833972)Instruction limit reached!
% 9.38/2.06 % (2833972)------------------------------
% 9.38/2.06 % (2833972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.38/2.06 % (2833972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.06 % (2833972)CaDiCaL version: 2.1.3
% 9.38/2.06 % (2833972)Termination reason: Instruction limit
% 9.38/2.06 % (2833972)Termination phase: Saturation
% 9.38/2.06 % (2833972)Time elapsed: 0.094 s
% 9.38/2.06 % (2833972)Peak memory usage: 16 MB
% 9.38/2.06 % (2833972)Instructions burned: 342 (million)
% 9.38/2.06 % (2833979)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=1899305262:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/136Mi)
% 9.38/2.06 % (2833967)Instruction limit reached!
% 9.38/2.06 % (2833967)------------------------------
% 9.38/2.06 % (2833967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.76/2.31 % (2833967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.31 % (2833967)CaDiCaL version: 2.1.3
% 13.76/2.31 % (2833967)Termination reason: Instruction limit
% 13.76/2.31 % (2833967)Termination phase: Saturation
% 13.76/2.31 % (2833967)Time elapsed: 0.142 s
% 13.76/2.31 % (2833967)Peak memory usage: 15 MB
% 13.76/2.31 % (2833967)Instructions burned: 272 (million)
% 13.76/2.31 % (2833979)Instruction limit reached!
% 13.76/2.31 % (2833979)------------------------------
% 13.76/2.31 % (2833979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.76/2.31 % (2833979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.31 % (2833979)CaDiCaL version: 2.1.3
% 13.76/2.31 % (2833979)Termination reason: Instruction limit
% 13.76/2.31 % (2833979)Termination phase: Property scanning
% 13.76/2.31 % (2833979)Time elapsed: 0.033 s
% 13.76/2.31 % (2833979)Peak memory usage: 12 MB
% 13.76/2.31 % (2833979)Instructions burned: 138 (million)
% 13.76/2.31 % (2833959)Instruction limit reached!
% 13.76/2.31 % (2833959)------------------------------
% 13.76/2.31 % (2833959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.76/2.31 % (2833959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.31 % (2833959)CaDiCaL version: 2.1.3
% 13.76/2.31 % (2833959)Termination reason: Instruction limit
% 13.76/2.31 % (2833959)Termination phase: Saturation
% 13.76/2.31 % (2833959)Time elapsed: 0.298 s
% 13.76/2.31 % (2833959)Peak memory usage: 17 MB
% 13.76/2.31 % (2833959)Instructions burned: 575 (million)
% 13.76/2.31 % (2833981)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=977081888:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2985 on theBenchmark for (2985ds/232Mi)
% 13.76/2.31 % (2833982)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=3499520137:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2985 on theBenchmark for (2985ds/1254Mi)
% 13.76/2.31 % (2833977)Instruction limit reached!
% 13.76/2.31 % (2833977)------------------------------
% 13.76/2.31 % (2833977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.76/2.31 % (2833977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.31 % (2833977)CaDiCaL version: 2.1.3
% 13.76/2.31 % (2833977)Termination reason: Instruction limit
% 13.76/2.31 % (2833977)Termination phase: Saturation
% 13.76/2.31 % (2833977)Time elapsed: 0.060 s
% 13.76/2.31 % (2833977)Peak memory usage: 14 MB
% 13.76/2.31 % (2833977)Instructions burned: 122 (million)
% 13.76/2.31 % (2833983)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 13.76/2.31 % (2833983)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=3007087758:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2985 on theBenchmark for (2985ds/281Mi)
% 13.76/2.31 % (2833986)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=624064026:i=619:add=on:rtra=on_2985 on theBenchmark for (2985ds/619Mi)
% 13.76/2.31 % (2833982)Refutation not found, incomplete strategy
% 13.76/2.31 % (2833982)------------------------------
% 13.76/2.31 % (2833982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.76/2.31 % (2833982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.31 % (2833982)CaDiCaL version: 2.1.3
% 13.76/2.31 % (2833982)Termination reason: Refutation not found, incomplete strategy
% 13.76/2.31 % (2833982)Time elapsed: 0.095 s
% 13.76/2.31 % (2833982)Peak memory usage: 16 MB
% 13.76/2.31 % (2833982)Instructions burned: 272 (million)
% 13.76/2.31 % (2833982)------------------------------
% 13.76/2.31 % (2833982)------------------------------
% 13.76/2.31 % (2833986)Refutation not found, incomplete strategy
% 13.76/2.31 % (2833986)------------------------------
% 13.76/2.31 % (2833986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.76/2.31 % (2833986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.31 % (2833986)CaDiCaL version: 2.1.3
% 13.76/2.31 % (2833986)Termination reason: Refutation not found, incomplete strategy
% 13.76/2.31 % (2833986)Time elapsed: 0.095 s
% 13.76/2.31 % (2833986)Peak memory usage: 16 MB
% 13.76/2.31 % (2833986)Instructions burned: 195 (million)
% 13.76/2.31 % (2833986)------------------------------
% 13.76/2.31 % (2833986)------------------------------
% 15.88/2.70 % (2833991)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=1003378482:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/865Mi)
% 15.88/2.70 % (2833981)Instruction limit reached!
% 15.88/2.70 % (2833981)------------------------------
% 15.88/2.70 % (2833981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.88/2.70 % (2833981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.88/2.70 % (2833981)CaDiCaL version: 2.1.3
% 15.88/2.70 % (2833981)Termination reason: Instruction limit
% 15.88/2.70 % (2833981)Termination phase: Saturation
% 15.88/2.70 % (2833981)Time elapsed: 0.125 s
% 15.88/2.70 % (2833981)Peak memory usage: 14 MB
% 15.88/2.70 % (2833981)Instructions burned: 238 (million)
% 15.88/2.70 % (2833992)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1983120329:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2984 on theBenchmark for (2984ds/212Mi)
% 15.88/2.70 % (2833983)Instruction limit reached!
% 15.88/2.70 % (2833983)------------------------------
% 15.88/2.70 % (2833983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.88/2.70 % (2833983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.88/2.70 % (2833983)CaDiCaL version: 2.1.3
% 15.88/2.70 % (2833983)Termination reason: Instruction limit
% 15.88/2.70 % (2833983)Termination phase: Saturation
% 15.88/2.70 % (2833983)Time elapsed: 0.131 s
% 15.88/2.70 % (2833983)Peak memory usage: 14 MB
% 15.88/2.70 % (2833983)Instructions burned: 281 (million)
% 15.88/2.70 % (2833994)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=3449474546:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/130Mi)
% 15.88/2.70 % (2833997)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3816794034:st=1.5:i=346:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/346Mi)
% 15.88/2.70 % (2833994)Instruction limit reached!
% 15.88/2.70 % (2833994)------------------------------
% 15.88/2.70 % (2833994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.88/2.70 % (2833994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.88/2.70 % (2833994)CaDiCaL version: 2.1.3
% 15.88/2.70 % (2833994)Termination reason: Instruction limit
% 15.88/2.70 % (2833994)Termination phase: Saturation
% 15.88/2.70 % (2833994)Time elapsed: 0.070 s
% 15.88/2.70 % (2833994)Peak memory usage: 13 MB
% 15.88/2.70 % (2833994)Instructions burned: 131 (million)
% 15.88/2.70 % (2833999)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=2864256370:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/152Mi)
% 15.88/2.70 % (2833992)Instruction limit reached!
% 15.88/2.70 % (2833992)------------------------------
% 15.88/2.70 % (2833992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.88/2.70 % (2833992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.88/2.70 % (2833992)CaDiCaL version: 2.1.3
% 15.88/2.70 % (2833992)Termination reason: Instruction limit
% 15.88/2.70 % (2833992)Termination phase: Saturation
% 15.88/2.70 % (2833992)Time elapsed: 0.108 s
% 15.88/2.70 % (2833992)Peak memory usage: 15 MB
% 15.88/2.70 % (2833992)Instructions burned: 212 (million)
% 15.88/2.70 % (2834001)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=355104857:i=75:ep=R:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/75Mi)
% 15.88/2.71 % (2834001)Instruction limit reached!
% 15.88/2.71 % (2834001)------------------------------
% 15.88/2.71 % (2834001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.88/2.71 % (2834001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.88/2.71 % (2834001)CaDiCaL version: 2.1.3
% 15.88/2.71 % (2834001)Termination reason: Instruction limit
% 15.88/2.71 % (2834001)Termination phase: Preprocessing 1
% 15.88/2.71 % (2834001)Time elapsed: 0.034 s
% 15.88/2.71 % (2834001)Peak memory usage: 11 MB
% 15.88/2.71 % (2834001)Instructions burned: 76 (million)
% 15.88/2.71 % (2833999)Instruction limit reached!
% 15.88/2.71 % (2833999)------------------------------
% 15.88/2.71 % (2833999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.88/2.71 % (2833999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.88/2.71 % (2833999)CaDiCaL version: 2.1.3
% 15.88/2.71 % (2833999)Termination reason: Instruction limit
% 15.88/2.71 % (2833999)Termination phase: Saturation
% 15.88/2.71 % (2833999)Time elapsed: 0.071 s
% 17.47/2.97 % (2833999)Peak memory usage: 13 MB
% 17.47/2.97 % (2833999)Instructions burned: 153 (million)
% 17.47/2.97 % (2834003)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=3036260782:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/387Mi)
% 17.47/2.97 % (2834004)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=1950313907:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2982 on theBenchmark for (2982ds/148Mi)
% 17.47/2.97 % (2833997)Instruction limit reached!
% 17.47/2.97 % (2833997)------------------------------
% 17.47/2.97 % (2833997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.47/2.97 % (2833997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/2.97 % (2833997)CaDiCaL version: 2.1.3
% 17.47/2.97 % (2833997)Termination reason: Instruction limit
% 17.47/2.97 % (2833997)Termination phase: Saturation
% 17.47/2.97 % (2833997)Time elapsed: 0.187 s
% 17.47/2.97 % (2833997)Peak memory usage: 15 MB
% 17.47/2.97 % (2833997)Instructions burned: 347 (million)
% 17.47/2.97 % (2834007)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=952547912:i=161:piset=and:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/161Mi)
% 17.47/2.97 % (2834004)Instruction limit reached!
% 17.47/2.97 % (2834004)------------------------------
% 17.47/2.97 % (2834004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.47/2.97 % (2834004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/2.97 % (2834004)CaDiCaL version: 2.1.3
% 17.47/2.97 % (2834004)Termination reason: Instruction limit
% 17.47/2.97 % (2834004)Termination phase: Saturation
% 17.47/2.97 % (2834004)Time elapsed: 0.065 s
% 17.47/2.97 % (2834004)Peak memory usage: 13 MB
% 17.47/2.97 % (2834004)Instructions burned: 148 (million)
% 17.47/2.97 % (2834009)lrs+10_1_sil=128000:si=on:random_seed=436024088:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/888Mi)
% 17.47/2.97 % (2834007)Instruction limit reached!
% 17.47/2.97 % (2834007)------------------------------
% 17.47/2.97 % (2834007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.47/2.97 % (2834007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/2.97 % (2834007)CaDiCaL version: 2.1.3
% 17.47/2.97 % (2834007)Termination reason: Instruction limit
% 17.47/2.97 % (2834007)Termination phase: Saturation
% 17.47/2.97 % (2834007)Time elapsed: 0.076 s
% 17.47/2.97 % (2834007)Peak memory usage: 14 MB
% 17.47/2.97 % (2834007)Instructions burned: 162 (million)
% 17.47/2.97 % (2834011)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=270548928:i=136:add=on:ins=4:rtra=on:sup=off_2981 on theBenchmark for (2981ds/136Mi)
% 17.47/2.97 % (2834011)Instruction limit reached!
% 17.47/2.97 % (2834011)------------------------------
% 17.47/2.97 % (2834011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.47/2.97 % (2834011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/2.97 % (2834011)CaDiCaL version: 2.1.3
% 17.47/2.97 % (2834011)Termination reason: Instruction limit
% 17.47/2.97 % (2834011)Termination phase: Saturation
% 17.47/2.97 % (2834011)Time elapsed: 0.065 s
% 17.47/2.97 % (2834011)Peak memory usage: 13 MB
% 17.47/2.97 % (2834011)Instructions burned: 138 (million)
% 17.47/2.97 % (2834003)Instruction limit reached!
% 17.47/2.97 % (2834003)------------------------------
% 17.47/2.97 % (2834003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.47/2.97 % (2834003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/2.97 % (2834003)CaDiCaL version: 2.1.3
% 17.47/2.97 % (2834003)Termination reason: Instruction limit
% 17.47/2.97 % (2834003)Termination phase: Saturation
% 17.47/2.97 % (2834003)Time elapsed: 0.215 s
% 17.47/2.97 % (2834003)Peak memory usage: 16 MB
% 17.47/2.97 % (2834003)Instructions burned: 387 (million)
% 17.47/2.97 % (2834013)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=1268873622:i=88:s2at=3:nm=2:rtra=on:rawr=on_2980 on theBenchmark for (2980ds/88Mi)
% 17.47/2.97 % (2834014)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=3185580154:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2980 on theBenchmark for (2980ds/93Mi)
% 20.05/3.25 % (2834013)Instruction limit reached!
% 20.05/3.25 % (2834013)------------------------------
% 20.05/3.25 % (2834013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.05/3.25 % (2834013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.05/3.25 % (2834013)CaDiCaL version: 2.1.3
% 20.05/3.25 % (2834013)Termination reason: Instruction limit
% 20.05/3.25 % (2834013)Termination phase: Preprocessing 1
% 20.05/3.25 % (2834013)Time elapsed: 0.042 s
% 20.05/3.25 % (2834013)Peak memory usage: 11 MB
% 20.05/3.25 % (2834013)Instructions burned: 90 (million)
% 20.05/3.25 % (2834014)Instruction limit reached!
% 20.05/3.25 % (2834014)------------------------------
% 20.05/3.25 % (2834014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.05/3.25 % (2834014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.05/3.25 % (2834014)CaDiCaL version: 2.1.3
% 20.05/3.25 % (2834014)Termination reason: Instruction limit
% 20.05/3.25 % (2834014)Termination phase: Preprocessing 1
% 20.05/3.25 % (2834014)Time elapsed: 0.043 s
% 20.05/3.25 % (2834014)Peak memory usage: 11 MB
% 20.05/3.25 % (2834014)Instructions burned: 94 (million)
% 20.05/3.25 % (2834017)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=4084135385:i=2186:rtra=on:ixr=off_2979 on theBenchmark for (2979ds/2186Mi)
% 20.05/3.25 % (2834018)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1587287600:s2a=on:i=240:rtra=on:ntd=on_2979 on theBenchmark for (2979ds/240Mi)
% 20.05/3.25 % (2833991)Instruction limit reached!
% 20.05/3.25 % (2833991)------------------------------
% 20.05/3.25 % (2833991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.05/3.25 % (2833991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.05/3.25 % (2833991)CaDiCaL version: 2.1.3
% 20.05/3.25 % (2833991)Termination reason: Instruction limit
% 20.05/3.25 % (2833991)Termination phase: Saturation
% 20.05/3.25 % (2833991)Time elapsed: 0.527 s
% 20.05/3.25 % (2833991)Peak memory usage: 22 MB
% 20.05/3.25 % (2833991)Instructions burned: 866 (million)
% 20.05/3.25 % (2834021)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=2071563903:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2978 on theBenchmark for (2978ds/805Mi)
% 20.05/3.25 % (2834018)Instruction limit reached!
% 20.05/3.25 % (2834018)------------------------------
% 20.05/3.25 % (2834018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.05/3.25 % (2834018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.05/3.25 % (2834018)CaDiCaL version: 2.1.3
% 20.05/3.25 % (2834018)Termination reason: Instruction limit
% 20.05/3.25 % (2834018)Termination phase: Saturation
% 20.05/3.25 % (2834018)Time elapsed: 0.114 s
% 20.05/3.25 % (2834018)Peak memory usage: 15 MB
% 20.05/3.25 % (2834018)Instructions burned: 240 (million)
% 20.05/3.25 % (2834023)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 20.05/3.25 % (2834023)dis+1002_1_to=lpo:sil=128000:cnfonf=conj_eager:si=on:sp=unary_first:spb=intro:urr=on:cbe=off:uwa=one_side_interpreted:rp=on:avsqc=1:random_seed=2683295132:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2978 on theBenchmark for (2978ds/391Mi)
% 20.05/3.25 % (2834009)Instruction limit reached!
% 20.05/3.25 % (2834009)------------------------------
% 20.05/3.25 % (2834009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.05/3.25 % (2834009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.05/3.25 % (2834009)CaDiCaL version: 2.1.3
% 20.05/3.25 % (2834009)Termination reason: Instruction limit
% 20.05/3.25 % (2834009)Termination phase: Saturation
% 20.05/3.25 % (2834009)Time elapsed: 0.467 s
% 20.05/3.25 % (2834009)Peak memory usage: 21 MB
% 20.05/3.25 % (2834009)Instructions burned: 890 (million)
% 20.05/3.25 % (2834025)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=125534840:i=355:av=off:fsr=off:rtra=on:ixr=off_2976 on theBenchmark for (2976ds/355Mi)
% 20.05/3.25 % (2834023)Instruction limit reached!
% 20.05/3.25 % (2834023)------------------------------
% 20.05/3.25 % (2834023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.05/3.25 % (2834023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.05/3.25 % (2834023)CaDiCaL version: 2.1.3
% 20.05/3.25 % (2834023)Termination reason: Instruction limit
% 20.05/3.25 % (2834023)Termination phase: Saturation
% 21.65/3.41 % (2834023)Time elapsed: 0.192 s
% 21.65/3.41 % (2834023)Peak memory usage: 15 MB
% 21.65/3.41 % (2834023)Instructions burned: 391 (million)
% 21.65/3.41 % (2834027)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=2016029887:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/314Mi)
% 21.65/3.41 % (2833971)Instruction limit reached!
% 21.65/3.41 % (2833971)------------------------------
% 21.65/3.41 % (2833971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.65/3.41 % (2833971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.65/3.41 % (2833971)CaDiCaL version: 2.1.3
% 21.65/3.41 % (2833971)Termination reason: Instruction limit
% 21.65/3.41 % (2833971)Termination phase: Saturation
% 21.65/3.41 % (2833971)Time elapsed: 1.201 s
% 21.65/3.41 % (2833971)Peak memory usage: 20 MB
% 21.65/3.41 % (2833971)Instructions burned: 1440 (million)
% 21.65/3.41 % (2834025)Instruction limit reached!
% 21.65/3.41 % (2834025)------------------------------
% 21.65/3.41 % (2834025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.65/3.41 % (2834025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.65/3.41 % (2834025)CaDiCaL version: 2.1.3
% 21.65/3.41 % (2834025)Termination reason: Instruction limit
% 21.65/3.41 % (2834025)Termination phase: Saturation
% 21.65/3.41 % (2834025)Time elapsed: 0.184 s
% 21.65/3.41 % (2834025)Peak memory usage: 15 MB
% 21.65/3.41 % (2834025)Instructions burned: 356 (million)
% 21.65/3.41 % (2834030)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=322766641:s2a=on:i=251:fsr=off:rtra=on_2974 on theBenchmark for (2974ds/251Mi)
% 21.65/3.41 % (2834031)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=4238229985:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=2470:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2974 on theBenchmark for (2974ds/2470Mi)
% 21.65/3.41 % (2834021)Instruction limit reached!
% 21.65/3.41 % (2834021)------------------------------
% 21.65/3.41 % (2834021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.65/3.41 % (2834021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.65/3.41 % (2834021)CaDiCaL version: 2.1.3
% 21.65/3.41 % (2834021)Termination reason: Instruction limit
% 21.65/3.41 % (2834021)Termination phase: Saturation
% 21.65/3.41 % (2834021)Time elapsed: 0.444 s
% 21.65/3.41 % (2834021)Peak memory usage: 18 MB
% 21.65/3.41 % (2834021)Instructions burned: 806 (million)
% 21.65/3.41 % (2834027)Instruction limit reached!
% 21.65/3.41 % (2834027)------------------------------
% 21.65/3.41 % (2834027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.65/3.41 % (2834027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.65/3.41 % (2834027)CaDiCaL version: 2.1.3
% 21.65/3.41 % (2834027)Termination reason: Instruction limit
% 21.65/3.41 % (2834027)Termination phase: Saturation
% 21.65/3.41 % (2834027)Time elapsed: 0.151 s
% 21.65/3.41 % (2834027)Peak memory usage: 15 MB
% 21.65/3.41 % (2834027)Instructions burned: 315 (million)
% 21.65/3.41 % (2834034)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=1238266707:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2974 on theBenchmark for (2974ds/673Mi)
% 21.65/3.41 % (2834035)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=1004527822:i=116:ep=RSTC:rtra=on:ntd=on_2974 on theBenchmark for (2974ds/116Mi)
% 21.65/3.41 % (2834035)Instruction limit reached!
% 21.65/3.41 % (2834035)------------------------------
% 21.65/3.41 % (2834035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.65/3.41 % (2834035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.65/3.41 % (2834035)CaDiCaL version: 2.1.3
% 21.65/3.41 % (2834035)Termination reason: Instruction limit
% 21.65/3.41 % (2834035)Termination phase: Property scanning
% 21.65/3.41 % (2834035)Time elapsed: 0.055 s
% 21.65/3.41 % (2834035)Peak memory usage: 12 MB
% 21.65/3.41 % (2834035)Instructions burned: 118 (million)
% 21.65/3.41 % (2834030)Instruction limit reached!
% 21.65/3.41 % (2834030)------------------------------
% 21.65/3.41 % (2834030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.65/3.41 % (2834030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.65/3.41 % (2834030)CaDiCaL version: 2.1.3
% 23.38/3.81 % (2834030)Termination reason: Instruction limit
% 23.38/3.81 % (2834030)Termination phase: Saturation
% 23.38/3.81 % (2834030)Time elapsed: 0.112 s
% 23.38/3.81 % (2834030)Peak memory usage: 13 MB
% 23.38/3.81 % (2834030)Instructions burned: 253 (million)
% 23.38/3.81 % (2834038)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2776596800:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2973 on theBenchmark for (2973ds/270Mi)
% 23.38/3.81 % (2834039)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=2482476679:hsq=on:hsqr=16,1:s2a=on:i=30:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2973 on theBenchmark for (2973ds/30Mi)
% 23.38/3.81 % (2834039)Instruction limit reached!
% 23.38/3.81 % (2834039)------------------------------
% 23.38/3.81 % (2834039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.38/3.81 % (2834039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.38/3.81 % (2834039)CaDiCaL version: 2.1.3
% 23.38/3.81 % (2834039)Termination reason: Instruction limit
% 23.38/3.81 % (2834039)Termination phase: shuffling
% 23.38/3.81 % (2834039)Time elapsed: 0.015 s
% 23.38/3.81 % (2834039)Peak memory usage: 10 MB
% 23.38/3.81 % (2834039)Instructions burned: 31 (million)
% 23.38/3.81 % (2834042)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 23.38/3.81 % (2834042)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=2226179952:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2973 on theBenchmark for (2973ds/39Mi)
% 23.38/3.81 % (2834042)Instruction limit reached!
% 23.38/3.81 % (2834042)------------------------------
% 23.38/3.81 % (2834042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.38/3.81 % (2834042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.38/3.81 % (2834042)CaDiCaL version: 2.1.3
% 23.38/3.81 % (2834042)Termination reason: Instruction limit
% 23.38/3.81 % (2834042)Termination phase: Property scanning
% 23.38/3.81 % (2834042)Time elapsed: 0.019 s
% 23.38/3.81 % (2834042)Peak memory usage: 11 MB
% 23.38/3.81 % (2834042)Instructions burned: 40 (million)
% 23.38/3.81 % (2834044)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3756267049:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2972 on theBenchmark for (2972ds/365Mi)
% 23.38/3.81 % (2834038)Instruction limit reached!
% 23.38/3.81 % (2834038)------------------------------
% 23.38/3.81 % (2834038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.38/3.81 % (2834038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.38/3.81 % (2834038)CaDiCaL version: 2.1.3
% 23.38/3.81 % (2834038)Termination reason: Instruction limit
% 23.38/3.81 % (2834038)Termination phase: Saturation
% 23.38/3.81 % (2834038)Time elapsed: 0.130 s
% 23.38/3.81 % (2834038)Peak memory usage: 14 MB
% 23.38/3.81 % (2834038)Instructions burned: 271 (million)
% 23.38/3.81 % (2834046)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1368001880:i=158:av=off:rtra=on_2972 on theBenchmark for (2972ds/158Mi)
% 23.38/3.81 % (2834046)Instruction limit reached!
% 23.38/3.81 % (2834046)------------------------------
% 23.38/3.81 % (2834046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.38/3.81 % (2834046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.38/3.81 % (2834046)CaDiCaL version: 2.1.3
% 23.38/3.81 % (2834046)Termination reason: Instruction limit
% 23.38/3.81 % (2834046)Termination phase: Saturation
% 23.38/3.81 % (2834046)Time elapsed: 0.080 s
% 23.38/3.81 % (2834046)Peak memory usage: 14 MB
% 23.38/3.81 % (2834046)Instructions burned: 159 (million)
% 23.38/3.81 % (2834048)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 23.38/3.81 % (2834048)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=1131946480:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2971 on theBenchmark for (2971ds/252Mi)
% 23.38/3.81 % (2834044)Instruction limit reached!
% 23.38/3.81 % (2834044)------------------------------
% 23.38/3.81 % (2834044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/3.95 % (2834044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/3.95 % (2834044)CaDiCaL version: 2.1.3
% 24.63/3.95 % (2834044)Termination reason: Instruction limit
% 24.63/3.95 % (2834044)Termination phase: Saturation
% 24.63/3.95 % (2834044)Time elapsed: 0.183 s
% 24.63/3.95 % (2834044)Peak memory usage: 17 MB
% 24.63/3.95 % (2834044)Instructions burned: 366 (million)
% 24.63/3.95 % (2834052)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=3231483911:i=213:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/213Mi)
% 24.63/3.95 % (2833930)Instruction limit reached!
% 24.63/3.95 % (2833930)------------------------------
% 24.63/3.95 % (2833930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/3.95 % (2833930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/3.95 % (2833930)CaDiCaL version: 2.1.3
% 24.63/3.95 % (2833930)Termination reason: Instruction limit
% 24.63/3.95 % (2833930)Termination phase: Saturation
% 24.63/3.95 % (2833930)Time elapsed: 2.156 s
% 24.63/3.95 % (2833930)Peak memory usage: 37 MB
% 24.63/3.95 % (2833930)Instructions burned: 5756 (million)
% 24.63/3.95 % (2834054)dis+1010_28_sil=128000:tgt=full:plsq=on:plsqc=1:cnfonf=off:si=on:plsqr=128,1:uwa=off:slsqc=2:sac=on:slsq=on:random_seed=1852774036:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2970 on theBenchmark for (2970ds/160Mi)
% 24.63/3.95 % (2834048)Instruction limit reached!
% 24.63/3.95 % (2834048)------------------------------
% 24.63/3.95 % (2834048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/3.95 % (2834048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/3.95 % (2834048)CaDiCaL version: 2.1.3
% 24.63/3.95 % (2834048)Termination reason: Instruction limit
% 24.63/3.95 % (2834048)Termination phase: Saturation
% 24.63/3.95 % (2834048)Time elapsed: 0.135 s
% 24.63/3.95 % (2834048)Peak memory usage: 15 MB
% 24.63/3.95 % (2834048)Instructions burned: 254 (million)
% 24.63/3.95 % (2834054)Instruction limit reached!
% 24.63/3.95 % (2834054)------------------------------
% 24.63/3.95 % (2834054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/3.95 % (2834054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/3.95 % (2834054)CaDiCaL version: 2.1.3
% 24.63/3.95 % (2834054)Termination reason: Instruction limit
% 24.63/3.95 % (2834054)Termination phase: Saturation
% 24.63/3.95 % (2834054)Time elapsed: 0.070 s
% 24.63/3.95 % (2834054)Peak memory usage: 13 MB
% 24.63/3.95 % (2834054)Instructions burned: 160 (million)
% 24.63/3.95 % (2834052)Instruction limit reached!
% 24.63/3.95 % (2834052)------------------------------
% 24.63/3.95 % (2834052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/3.95 % (2834052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/3.95 % (2834052)CaDiCaL version: 2.1.3
% 24.63/3.95 % (2834052)Termination reason: Instruction limit
% 24.63/3.95 % (2834052)Termination phase: Saturation
% 24.63/3.95 % (2834052)Time elapsed: 0.113 s
% 24.63/3.95 % (2834052)Peak memory usage: 15 MB
% 24.63/3.95 % (2834052)Instructions burned: 214 (million)
% 24.63/3.95 % (2834056)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=19970040:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2969 on theBenchmark for (2969ds/763Mi)
% 24.63/3.95 % (2834034)Instruction limit reached!
% 24.63/3.95 % (2834034)------------------------------
% 24.63/3.95 % (2834034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/3.95 % (2834034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/3.95 % (2834034)CaDiCaL version: 2.1.3
% 24.63/3.95 % (2834034)Termination reason: Instruction limit
% 24.63/3.95 % (2834034)Termination phase: Saturation
% 24.63/3.95 % (2834034)Time elapsed: 0.500 s
% 24.63/3.95 % (2834034)Peak memory usage: 17 MB
% 24.63/3.95 % (2834034)Instructions burned: 674 (million)
% 24.63/3.95 % (2834057)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 24.63/3.95 % (2834057)ott+1010_40_sil=128000:tgt=full:plsq=on:plsqc=5:si=on:sos=all:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=2154587020:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2969 on theBenchmark for (2969ds/237Mi)
% 24.63/3.95 % (2834058)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=3615681087:s2a=on:i=386:rtra=on:ntd=on_2969 on theBenchmark for (2969ds/386Mi)
% 26.19/4.09 % (2834060)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=898507959:i=300:piset=and:nm=32:rtra=on_2969 on theBenchmark for (2969ds/300Mi)
% 26.19/4.09 % (2834057)Instruction limit reached!
% 26.19/4.09 % (2834057)------------------------------
% 26.19/4.09 % (2834057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.19/4.09 % (2834057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/4.09 % (2834057)CaDiCaL version: 2.1.3
% 26.19/4.09 % (2834057)Termination reason: Instruction limit
% 26.19/4.09 % (2834057)Termination phase: Saturation
% 26.19/4.09 % (2834057)Time elapsed: 0.120 s
% 26.19/4.09 % (2834057)Peak memory usage: 15 MB
% 26.19/4.09 % (2834057)Instructions burned: 237 (million)
% 26.19/4.09 % (2834017)Instruction limit reached!
% 26.19/4.09 % (2834017)------------------------------
% 26.19/4.09 % (2834017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.19/4.09 % (2834017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/4.09 % (2834017)CaDiCaL version: 2.1.3
% 26.19/4.09 % (2834017)Termination reason: Instruction limit
% 26.19/4.09 % (2834017)Termination phase: Saturation
% 26.19/4.09 % (2834017)Time elapsed: 1.149 s
% 26.19/4.09 % (2834017)Peak memory usage: 21 MB
% 26.19/4.09 % (2834017)Instructions burned: 2187 (million)
% 26.19/4.09 % (2834064)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=3062640462:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2967 on theBenchmark for (2967ds/567Mi)
% 26.19/4.09 % (2834065)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=5959:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2967 on theBenchmark for (2967ds/379Mi)
% 26.19/4.09 % (2834058)Instruction limit reached!
% 26.19/4.09 % (2834058)------------------------------
% 26.19/4.09 % (2834058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.19/4.09 % (2834058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/4.09 % (2834058)CaDiCaL version: 2.1.3
% 26.19/4.09 % (2834058)Termination reason: Instruction limit
% 26.19/4.09 % (2834058)Termination phase: Saturation
% 26.19/4.09 % (2834058)Time elapsed: 0.172 s
% 26.19/4.09 % (2834058)Peak memory usage: 15 MB
% 26.19/4.09 % (2834058)Instructions burned: 387 (million)
% 26.19/4.09 % (2834060)Instruction limit reached!
% 26.19/4.09 % (2834060)------------------------------
% 26.19/4.09 % (2834060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.19/4.09 % (2834060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/4.09 % (2834060)CaDiCaL version: 2.1.3
% 26.19/4.09 % (2834060)Termination reason: Instruction limit
% 26.19/4.09 % (2834060)Termination phase: Saturation
% 26.19/4.09 % (2834060)Time elapsed: 0.184 s
% 26.19/4.09 % (2834060)Peak memory usage: 15 MB
% 26.19/4.09 % (2834060)Instructions burned: 300 (million)
% 26.19/4.09 % (2834068)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=4247350496:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2967 on theBenchmark for (2967ds/429Mi)
% 26.19/4.09 % (2834069)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=1528664768:i=478:bd=all:rtra=on_2967 on theBenchmark for (2967ds/478Mi)
% 26.19/4.09 % (2834065)Instruction limit reached!
% 26.19/4.09 % (2834065)------------------------------
% 26.19/4.09 % (2834065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.19/4.09 % (2834065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/4.09 % (2834065)CaDiCaL version: 2.1.3
% 26.19/4.09 % (2834065)Termination reason: Instruction limit
% 26.19/4.09 % (2834065)Termination phase: Saturation
% 26.19/4.09 % (2834065)Time elapsed: 0.234 s
% 26.19/4.09 % (2834065)Peak memory usage: 16 MB
% 26.19/4.09 % (2834065)Instructions burned: 379 (million)
% 26.19/4.09 % (2834072)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1809679677:i=445:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2965 on theBenchmark for (2965ds/445Mi)
% 26.19/4.09 % (2834064)Instruction limit reached!
% 26.19/4.09 % (2834064)------------------------------
% 26.19/4.09 % (2834064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.19/4.09 % (2834064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/4.09 % (2834064)CaDiCaL version: 2.1.3
% 26.19/4.09 % (2834064)Termination reason: Instruction limit
% 26.19/4.09 % (2834064)Termination phase: Saturation
% 26.19/4.09 % (2834064)Time elapsed: 0.267 s
% 26.99/4.39 % (2834064)Peak memory usage: 15 MB
% 26.99/4.39 % (2834064)Instructions burned: 567 (million)
% 26.99/4.39 % (2834056)Instruction limit reached!
% 26.99/4.39 % (2834056)------------------------------
% 26.99/4.39 % (2834056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.99/4.39 % (2834056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.99/4.39 % (2834056)CaDiCaL version: 2.1.3
% 26.99/4.39 % (2834056)Termination reason: Instruction limit
% 26.99/4.39 % (2834056)Termination phase: Saturation
% 26.99/4.39 % (2834056)Time elapsed: 0.428 s
% 26.99/4.39 % (2834056)Peak memory usage: 18 MB
% 26.99/4.39 % (2834056)Instructions burned: 764 (million)
% 26.99/4.39 % (2834074)ott+1003_1_to=kbo:cnfonf=lazy_pi_sigma_gen:si=on:sp=weighted_frequency:spb=units:urr=on:cbe=off:random_seed=3735608455:uwa_fpi=on:i=71:hud=10:rtra=on:ixr=off_2964 on theBenchmark for (2964ds/71Mi)
% 26.99/4.39 % (2834068)Instruction limit reached!
% 26.99/4.39 % (2834068)------------------------------
% 26.99/4.39 % (2834068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.99/4.39 % (2834068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.99/4.39 % (2834068)CaDiCaL version: 2.1.3
% 26.99/4.39 % (2834068)Termination reason: Instruction limit
% 26.99/4.39 % (2834068)Termination phase: Saturation
% 26.99/4.39 % (2834068)Time elapsed: 0.229 s
% 26.99/4.39 % (2834068)Peak memory usage: 16 MB
% 26.99/4.39 % (2834068)Instructions burned: 429 (million)
% 26.99/4.39 % (2834075)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3552386699:i=302:sd=2:bd=preordered:rtra=on:ss=axioms_2964 on theBenchmark for (2964ds/302Mi)
% 26.99/4.39 % (2834077)lrs+10_1_sil=128000:fde=none:cnfonf=off:si=on:uwa=off:random_seed=1190447570:s2a=on:i=4980:sd=2:bd=all:rtra=on:ss=axioms:ntd=on_2964 on theBenchmark for (2964ds/4980Mi)
% 26.99/4.39 % (2834074)Instruction limit reached!
% 26.99/4.39 % (2834074)------------------------------
% 26.99/4.39 % (2834074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.99/4.39 % (2834074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.99/4.39 % (2834074)CaDiCaL version: 2.1.3
% 26.99/4.39 % (2834074)Termination reason: Instruction limit
% 26.99/4.39 % (2834074)Termination phase: Preprocessing 1
% 26.99/4.39 % (2834074)Time elapsed: 0.033 s
% 26.99/4.39 % (2834074)Peak memory usage: 11 MB
% 26.99/4.39 % (2834074)Instructions burned: 73 (million)
% 26.99/4.39 % (2834080)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
% 26.99/4.39 % (2834080)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 26.99/4.39 % (2834080)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2235772332:i=100:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2964 on theBenchmark for (2964ds/100Mi)
% 26.99/4.39 % (2834080)Instruction limit reached!
% 26.99/4.39 % (2834080)------------------------------
% 26.99/4.39 % (2834080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.99/4.39 % (2834080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.99/4.39 % (2834080)CaDiCaL version: 2.1.3
% 26.99/4.39 % (2834080)Termination reason: Instruction limit
% 26.99/4.39 % (2834080)Termination phase: Preprocessing 3
% 26.99/4.39 % (2834080)Time elapsed: 0.044 s
% 26.99/4.39 % (2834080)Peak memory usage: 11 MB
% 26.99/4.39 % (2834080)Instructions burned: 100 (million)
% 26.99/4.39 % (2834069)Instruction limit reached!
% 26.99/4.39 % (2834069)------------------------------
% 26.99/4.39 % (2834069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.99/4.39 % (2834069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.99/4.39 % (2834069)CaDiCaL version: 2.1.3
% 26.99/4.39 % (2834069)Termination reason: Instruction limit
% 26.99/4.39 % (2834069)Termination phase: Saturation
% 26.99/4.39 % (2834069)Time elapsed: 0.290 s
% 26.99/4.39 % (2834069)Peak memory usage: 17 MB
% 26.99/4.39 % (2834069)Instructions burned: 480 (million)
% 26.99/4.39 % (2834084)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=2464578806:i=76:piset=equals:rtra=on:ntd=on_2963 on theBenchmark for (2963ds/76Mi)
% 26.99/4.39 % (2834085)lrs+10_1_to=lpo:sil=128000:cnfonf=off:si=on:sp=unary_first:sos=all:spb=goal:uwa=off:random_seed=3193398375:i=289:rtra=on_2963 on theBenchmark for (2963ds/289Mi)
% 29.78/4.61 % (2834084)Instruction limit reached!
% 29.78/4.61 % (2834084)------------------------------
% 29.78/4.61 % (2834084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.78/4.61 % (2834084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/4.61 % (2834084)CaDiCaL version: 2.1.3
% 29.78/4.61 % (2834084)Termination reason: Instruction limit
% 29.78/4.61 % (2834084)Termination phase: Preprocessing 1
% 29.78/4.61 % (2834084)Time elapsed: 0.019 s
% 29.78/4.61 % (2834084)Peak memory usage: 11 MB
% 29.78/4.61 % (2834084)Instructions burned: 81 (million)
% 29.78/4.61 % (2834031)Instruction limit reached!
% 29.78/4.61 % (2834031)------------------------------
% 29.78/4.61 % (2834031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.78/4.61 % (2834031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/4.61 % (2834031)CaDiCaL version: 2.1.3
% 29.78/4.61 % (2834031)Termination reason: Instruction limit
% 29.78/4.61 % (2834031)Termination phase: Saturation
% 29.78/4.61 % (2834031)Time elapsed: 1.099 s
% 29.78/4.61 % (2834031)Peak memory usage: 18 MB
% 29.78/4.61 % (2834031)Instructions burned: 2473 (million)
% 29.78/4.61 % (2834088)lrs+2_64_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_first:bsr=unit_only:cbe=off:uwa=interpreted_only:nwc=0.5:slsqc=5:sac=on:slsq=on:random_seed=770015709:i=493:s2at=5:kws=frequency:doe=on:rtra=on:er=known_2963 on theBenchmark for (2963ds/493Mi)
% 29.78/4.61 % (2834089)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=572460641:cond=on:i=34:hud=10:nm=10:rtra=on_2963 on theBenchmark for (2963ds/34Mi)
% 29.78/4.61 % (2834075)Instruction limit reached!
% 29.78/4.61 % (2834075)------------------------------
% 29.78/4.61 % (2834075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.78/4.61 % (2834075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/4.61 % (2834075)CaDiCaL version: 2.1.3
% 29.78/4.61 % (2834075)Termination reason: Instruction limit
% 29.78/4.61 % (2834075)Termination phase: Saturation
% 29.78/4.61 % (2834075)Time elapsed: 0.168 s
% 29.78/4.61 % (2834075)Peak memory usage: 15 MB
% 29.78/4.61 % (2834075)Instructions burned: 308 (million)
% 29.78/4.61 % (2834089)Instruction limit reached!
% 29.78/4.61 % (2834089)------------------------------
% 29.78/4.61 % (2834089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.78/4.61 % (2834089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/4.61 % (2834089)CaDiCaL version: 2.1.3
% 29.78/4.61 % (2834089)Termination reason: Instruction limit
% 29.78/4.61 % (2834089)Termination phase: Property scanning
% 29.78/4.61 % (2834089)Time elapsed: 0.019 s
% 29.78/4.61 % (2834089)Peak memory usage: 11 MB
% 29.78/4.61 % (2834089)Instructions burned: 41 (million)
% 29.78/4.61 % (2834092)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 29.78/4.61 % (2834092)dis+1010_1_to=lpo:irw=on:plsq=on:drc=ordering:plsqc=4:cnfonf=lazy_simp:si=on:sp=reverse_frequency:sos=on:plsqr=32,1:cbe=off:uwa=off:rp=on:lwlo=on:random_seed=2353110547:i=372:add=off:piset=or:nm=10:fsr=off:rtra=on:c=on_2963 on theBenchmark for (2963ds/372Mi)
% 29.78/4.61 % (2834093)lrs+1002_1024_sil=128000:tgt=ground:e2e=on:si=on:uwa=interpreted_only:fd=off:nwc=1:random_seed=3660995743:cts=off:avsq=on:i=670:avsqr=1,16:nm=16:rtra=on_2962 on theBenchmark for (2962ds/670Mi)
% 29.78/4.61 % (2834072)Instruction limit reached!
% 29.78/4.61 % (2834072)------------------------------
% 29.78/4.61 % (2834072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.78/4.61 % (2834072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/4.61 % (2834072)CaDiCaL version: 2.1.3
% 29.78/4.61 % (2834072)Termination reason: Instruction limit
% 29.78/4.61 % (2834072)Termination phase: Saturation
% 29.78/4.61 % (2834072)Time elapsed: 0.233 s
% 29.78/4.61 % (2834072)Peak memory usage: 17 MB
% 29.78/4.61 % (2834072)Instructions burned: 446 (million)
% 29.78/4.61 % (2834096)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2023962004:hsq=on:st=2:i=647:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2962 on theBenchmark for (2962ds/647Mi)
% 29.78/4.61 % (2834085)Instruction limit reached!
% 29.78/4.61 % (2834085)------------------------------
% 29.98/4.74 % (2834085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.74 % (2834085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.74 % (2834085)CaDiCaL version: 2.1.3
% 29.98/4.74 % (2834085)Termination reason: Instruction limit
% 29.98/4.74 % (2834085)Termination phase: Saturation
% 29.98/4.74 % (2834085)Time elapsed: 0.144 s
% 29.98/4.74 % (2834085)Peak memory usage: 16 MB
% 29.98/4.74 % (2834085)Instructions burned: 290 (million)
% 29.98/4.74 % (2834098)dis+10_128_sil=128000:tgt=full:plsq=on:plsqc=3:cnfonf=off:si=on:sp=arity:spb=goal_then_units:uwa=one_side_interpreted:nwc=1.5:random_seed=1243394846:i=857:add=off:kws=frequency:rtra=on:ntd=on_2962 on theBenchmark for (2962ds/857Mi)
% 29.98/4.74 % (2834092)Refutation not found, incomplete strategy
% 29.98/4.74 % (2834092)------------------------------
% 29.98/4.74 % (2834092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.74 % (2834092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.74 % (2834092)CaDiCaL version: 2.1.3
% 29.98/4.74 % (2834092)Termination reason: Refutation not found, incomplete strategy
% 29.98/4.74 % (2834092)Time elapsed: 0.094 s
% 29.98/4.74 % (2834092)Peak memory usage: 16 MB
% 29.98/4.74 % (2834092)Instructions burned: 195 (million)
% 29.98/4.74 % (2834092)------------------------------
% 29.98/4.74 % (2834092)------------------------------
% 29.98/4.74 % (2834100)dis+1010_4_anc=all_dependent:to=lpo:sil=128000:fde=unused:cnfonf=conj_eager:si=on:sp=reverse_frequency:lma=off:spb=intro:cbe=off:uwa=off:random_seed=4138947463:i=693:add=off:fsr=off:rtra=on:fe=abstraction:ntd=on_2961 on theBenchmark for (2961ds/693Mi)
% 29.98/4.74 % (2834088)Instruction limit reached!
% 29.98/4.74 % (2834088)------------------------------
% 29.98/4.74 % (2834088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.74 % (2834088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.74 % (2834088)CaDiCaL version: 2.1.3
% 29.98/4.74 % (2834088)Termination reason: Instruction limit
% 29.98/4.74 % (2834088)Termination phase: Saturation
% 29.98/4.74 % (2834088)Time elapsed: 0.214 s
% 29.98/4.74 % (2834088)Peak memory usage: 17 MB
% 29.98/4.74 % (2834088)Instructions burned: 494 (million)
% 29.98/4.74 % (2834102)dis+10_7_sil=128000:cnfonf=lazy_gen:si=on:sos=on:random_seed=2924070927:i=285:hud=10:bd=all:rtra=on:ss=axioms_2961 on theBenchmark for (2961ds/285Mi)
% 29.98/4.74 % (2834102)Refutation not found, incomplete strategy
% 29.98/4.74 % (2834102)------------------------------
% 29.98/4.74 % (2834102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.74 % (2834102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.74 % (2834102)CaDiCaL version: 2.1.3
% 29.98/4.74 % (2834102)Termination reason: Refutation not found, incomplete strategy
% 29.98/4.74 % (2834102)Time elapsed: 0.097 s
% 29.98/4.74 % (2834102)Peak memory usage: 15 MB
% 29.98/4.74 % (2834102)Instructions burned: 176 (million)
% 29.98/4.74 % (2834102)------------------------------
% 29.98/4.74 % (2834102)------------------------------
% 29.98/4.74 % (2834104)WARNING Broken Constraint: if ho_split_queue_ratios(23,10) has been set then ho_split_queue(off) is equal to on
% 29.98/4.74 % (2834104)dis+1002_50_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=1:si=on:sp=occurrence:plsqr=64,1:nwc=3:flr=on:chr=on:random_seed=1443575724:hsqr=23,10:uwa_fpi=on:i=52:kws=frequency:hud=15:fsr=off:rtra=on:amm=off:ntd=on:rawr=on_2959 on theBenchmark for (2959ds/52Mi)
% 29.98/4.74 % (2834104)Instruction limit reached!
% 29.98/4.74 % (2834104)------------------------------
% 29.98/4.74 % (2834104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.74 % (2834104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.74 % (2834104)CaDiCaL version: 2.1.3
% 29.98/4.74 % (2834104)Termination reason: Instruction limit
% 29.98/4.74 % (2834104)Termination phase: Preprocessing 3
% 29.98/4.74 % (2834104)Time elapsed: 0.025 s
% 29.98/4.74 % (2834104)Peak memory usage: 11 MB
% 29.98/4.74 % (2834104)Instructions burned: 52 (million)
% 29.98/4.74 % (2834106)dis+10_1_si=on:random_seed=720384007:i=407:sd=4:rtra=on:ss=axioms:sgt=20_2959 on theBenchmark for (2959ds/407Mi)
% 29.98/4.74 % (2834093)Instruction limit reached!
% 29.98/4.74 % (2834093)------------------------------
% 29.98/4.74 % (2834093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.74 % (2834093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.74 % (2834093)CaDiCaL version: 2.1.3
% 29.98/4.74 % (2834093)Termination reason: Instruction limit
% 29.98/4.74 % (2834093)Termination phase: Saturation
% 29.98/4.74 % (2834093)Time elapsed: 0.367 s
% 29.98/4.74 % (2834093)Peak memory usage: 16 MB
% 29.98/4.74 % (2834093)Instructions burned: 670 (million)
% 29.98/4.74 % (2834096)Instruction limit reached!
% 29.98/4.74 % (2834096)------------------------------
% 29.98/4.74 % (2834096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.74 % (2834096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.74 % (2834096)CaDiCaL version: 2.1.3
% 29.98/4.74 % (2834096)Termination reason: Instruction limit
% 29.98/4.74 % (2834096)Termination phase: Saturation
% 29.98/4.74 % (2834096)Time elapsed: 0.351 s
% 29.98/4.74 % (2834096)Peak memory usage: 16 MB
% 29.98/4.74 % (2834096)Instructions burned: 648 (million)
% 29.98/4.74 % (2834108)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=1630906215:i=2240:bs=unit_only:ins=25:rtra=on:ntd=on_2959 on theBenchmark for (2959ds/2240Mi)
% 29.98/4.74 % (2834109)lrs+10_1_sil=128000:e2e=on:si=on:uwa=interpreted_only:random_seed=3347096712:st=2:i=336:sd=1:rtra=on:ss=axioms:ntd=on_2959 on theBenchmark for (2959ds/336Mi)
% 29.98/4.74 % (2834100)Instruction limit reached!
% 29.98/4.74 % (2834100)------------------------------
% 29.98/4.74 % (2834100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.74 % (2834100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.74 % (2834100)CaDiCaL version: 2.1.3
% 29.98/4.74 % (2834100)Termination reason: Instruction limit
% 29.98/4.74 % (2834100)Termination phase: Saturation
% 29.98/4.74 % (2834100)Time elapsed: 0.364 s
% 29.98/4.74 % (2834100)Peak memory usage: 17 MB
% 29.98/4.74 % (2834100)Instructions burned: 694 (million)
% 29.98/4.74 % (2834112)lrs+10_1_to=lpo:sil=128000:fde=none:cnfonf=off:si=on:sp=unary_first:urr=on:uwa=one_side_constant:random_seed=86569750:s2a=on:i=1142:s2at=3:bd=all:rtra=on_2958 on theBenchmark for (2958ds/1142Mi)
% 29.98/4.74 % (2834098)Instruction limit reached!
% 29.98/4.74 % (2834098)------------------------------
% 29.98/4.74 % (2834098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.74 % (2834098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.74 % (2834098)CaDiCaL version: 2.1.3
% 29.98/4.74 % (2834098)Termination reason: Instruction limit
% 29.98/4.74 % (2834098)Termination phase: Saturation
% 29.98/4.74 % (2834098)Time elapsed: 0.425 s
% 29.98/4.74 % (2834098)Peak memory usage: 15 MB
% 29.98/4.74 % (2834098)Instructions burned: 858 (million)
% 29.98/4.74 % (2834116)dis+1002_1_sil=128000:si=on:uwa=off:random_seed=2879982641:st=3:i=376:sd=4:rtra=on:ss=axioms:ntd=on_2957 on theBenchmark for (2957ds/376Mi)
% 29.98/4.74 % (2834106)Instruction limit reached!
% 29.98/4.74 % (2834106)------------------------------
% 29.98/4.74 % (2834106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.74 % (2834106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.74 % (2834106)CaDiCaL version: 2.1.3
% 29.98/4.74 % (2834106)Termination reason: Instruction limit
% 29.98/4.74 % (2834106)Termination phase: Saturation
% 29.98/4.74 % (2834106)Time elapsed: 0.205 s
% 29.98/4.74 % (2834106)Peak memory usage: 16 MB
% 29.98/4.74 % (2834106)Instructions burned: 408 (million)
% 29.98/4.74 % (2834109)Instruction limit reached!
% 29.98/4.74 % (2834109)------------------------------
% 29.98/4.74 % (2834109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.74 % (2834109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.74 % (2834109)CaDiCaL version: 2.1.3
% 29.98/4.74 % (2834109)Termination reason: Instruction limit
% 29.98/4.74 % (2834109)Termination phase: Saturation
% 29.98/4.74 % (2834109)Time elapsed: 0.165 s
% 29.98/4.74 % (2834109)Peak memory usage: 15 MB
% 29.98/4.74 % (2834109)Instructions burned: 336 (million)
% 29.98/4.74 % (2834118)dis+1002_4:1_anc=none:sil=128000:sas=cadical:si=on:sp=weighted_frequency:sos=on:uwa=one_side_interpreted:random_seed=281446973:i=766:bd=all:rtra=on_2957 on theBenchmark for (2957ds/766Mi)
% 29.98/4.74 % (2834119)WARNING Broken Constraint: if avatar_split_queue_cutoffs(4) has been set then avatar_split_queue(off) is equal to on
% 29.98/4.74 % (2834119)lrs+10_1_to=kbo:si=on:sp=const_frequency:sos=on:spb=non_intro:uwa=hol:avsqc=4:random_seed=210515954:st=3:uwa_fpi=on:i=959:fgj=on:piset=pi_sigma:hud=5:nm=16:rtra=on:fe=abstraction:ss=axioms:ixr=off:ntd=on_2957 on theBenchmark for (2957ds/959Mi)
% 29.98/4.74 % (2834112) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2833790-2834112"...
% 29.98/4.74 % (2834112)...printing done.
% 29.98/4.74 % (2834112)Refutation found. Thanks to Tanya!
% 29.98/4.74 % SZS status Theorem for theBenchmark
% 29.98/4.74 % SZS output start Proof for theBenchmark
% 29.98/4.74 thf(type_def_5, type, abstra2103299360e_tree: $tType > $tType).
% 29.98/4.74 thf(type_def_6, type, product_prod: ($tType * $tType) > $tType).
% 29.98/4.74 thf(type_def_7, type, stream: $tType > $tType).
% 29.98/4.74 thf(type_def_8, type, fset: $tType > $tType).
% 29.98/4.74 thf(type_def_9, type, set: $tType > $tType).
% 29.98/4.74 thf(type_def_10, type, nat: $tType).
% 29.98/4.74 thf(type_def_11, type, state: $tType).
% 29.98/4.74 thf(type_def_12, type, itself: $tType > $tType).
% 29.98/4.74 thf(type_def_13, type, rule: $tType).
% 29.98/4.74 thf(type_def_14, type, sTfun: ($tType * $tType) > $tType).
% 29.98/4.74 thf(func_def_0, type, type: !>[X0: $tType]:((itself @ X0 > $o))).
% 29.98/4.74 thf(func_def_1, type, bot: !>[X0: $tType]:((itself @ X0 > $o))).
% 29.98/4.74 thf(func_def_2, type, ord: !>[X0: $tType]:((itself @ X0 > $o))).
% 29.98/4.74 thf(func_def_3, type, order: !>[X0: $tType]:((itself @ X0 > $o))).
% 29.98/4.74 thf(func_def_4, type, linorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 29.98/4.74 thf(func_def_5, type, preorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 29.98/4.74 thf(func_def_6, type, order_bot: !>[X0: $tType]:((itself @ X0 > $o))).
% 29.98/4.74 thf(func_def_7, type, wellorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 29.98/4.74 thf(func_def_8, type, abstra1326562878System: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > stream @ X0 > set @ X1 > $o))).
% 29.98/4.74 thf(func_def_9, type, abstra1332369113inWait: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > stream @ X0 > X1 > nat))).
% 29.98/4.74 thf(func_def_10, type, abstra2097340358le_pos: !>[X0: $tType]:((stream @ X0 > X0 > nat))).
% 29.98/4.74 thf(func_def_11, type, abstra1209608345urated: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > stream @ X0 > stream @ product_prod @ X1 @ X0 > $o))).
% 29.98/4.74 thf(func_def_12, type, abstra1874422341nabled: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > X0 > X1 > $o))).
% 29.98/4.74 thf(func_def_13, type, abstra523868654_epath: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > stream @ X0 > stream @ product_prod @ X1 @ X0 > $o))).
% 29.98/4.74 thf(func_def_14, type, abstra928354080m_fair: !>[X0: $tType]:((stream @ X0 > stream @ X0 > $o))).
% 29.98/4.74 thf(func_def_15, type, abstra1774373515_fenum: !>[X0: $tType]:((stream @ X0 > stream @ X0))).
% 29.98/4.74 thf(func_def_16, type, abstra1225283448mkTree: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > stream @ X0 > X1 > abstra2103299360e_tree @ product_prod @ X1 @ X0))).
% 29.98/4.74 thf(func_def_17, type, abstra1276541928ickEff: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > X0 > X1 > fset @ X1))).
% 29.98/4.74 thf(func_def_18, type, abstra726722745urated: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > X0 > stream @ product_prod @ X1 @ X0 > $o))).
% 29.98/4.74 thf(func_def_19, type, abstra1259602206m_trim: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > stream @ X0 > X1 > stream @ X0))).
% 29.98/4.74 thf(func_def_20, type, abstra1874736267tem_wf: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > stream @ X0 > abstra2103299360e_tree @ product_prod @ X1 @ X0 > $o))).
% 29.98/4.74 thf(func_def_21, type, abstra313004635_ipath: !>[X0: $tType]:((abstra2103299360e_tree @ X0 > stream @ X0 > $o))).
% 29.98/4.74 thf(func_def_22, type, abstra1749095923e_cont: !>[X0: $tType]:((abstra2103299360e_tree @ X0 > fset @ abstra2103299360e_tree @ X0))).
% 29.98/4.74 thf(func_def_23, type, abstra573067619e_root: !>[X0: $tType]:((abstra2103299360e_tree @ X0 > X0))).
% 29.98/4.74 thf(func_def_24, type, fimage: !>[X0: $tType, X1: $tType]:(((X0 > X1) > fset @ X0 > fset @ X1))).
% 29.98/4.74 thf(func_def_25, type, fmember: !>[X0: $tType]:((X0 > fset @ X0 > $o))).
% 29.98/4.74 thf(func_def_26, type, if: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 29.98/4.74 thf(func_def_27, type, linear1386806755on_alw: !>[X0: $tType]:(((stream @ X0 > $o) > stream @ X0 > $o))).
% 29.98/4.74 thf(func_def_28, type, linear1707521579_holds: !>[X0: $tType]:(((X0 > $o) > stream @ X0 > $o))).
% 29.98/4.74 thf(func_def_29, type, bot_bot: !>[X0: $tType]:(X0)).
% 29.98/4.74 thf(func_def_30, type, ord_Least: !>[X0: $tType]:(((X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_31, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 29.98/4.74 thf(func_def_32, type, product_Pair: !>[X0: $tType, X1: $tType]:((X0 > X1 > product_prod @ X0 @ X1))).
% 29.98/4.74 thf(func_def_33, type, product_fst: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X0))).
% 29.98/4.74 thf(func_def_34, type, product_snd: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X1))).
% 29.98/4.74 thf(func_def_35, type, type2: !>[X0: $tType]:(itself @ X0)).
% 29.98/4.74 thf(func_def_36, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 29.98/4.74 thf(func_def_37, type, sdrop: !>[X0: $tType]:((nat > stream @ X0 > stream @ X0))).
% 29.98/4.74 thf(func_def_38, type, sdrop_while: !>[X0: $tType]:(((X0 > $o) > stream @ X0 > stream @ X0))).
% 29.98/4.74 thf(func_def_39, type, shd: !>[X0: $tType]:((stream @ X0 > X0))).
% 29.98/4.74 thf(func_def_40, type, sset: !>[X0: $tType]:((stream @ X0 > set @ X0))).
% 29.98/4.74 thf(func_def_41, type, stl: !>[X0: $tType]:((stream @ X0 > stream @ X0))).
% 29.98/4.74 thf(func_def_42, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 29.98/4.74 thf(func_def_43, type, s: set @ state).
% 29.98/4.74 thf(func_def_44, type, eff: (rule > state > fset @ state > $o)).
% 29.98/4.74 thf(func_def_45, type, r: rule).
% 29.98/4.74 thf(func_def_46, type, rs: stream @ rule).
% 29.98/4.74 thf(func_def_47, type, rsa: stream @ rule).
% 29.98/4.74 thf(func_def_48, type, rules: stream @ rule).
% 29.98/4.74 thf(func_def_49, type, s2: state).
% 29.98/4.74 thf(func_def_50, type, s3: state).
% 29.98/4.74 thf(func_def_51, type, sa: state).
% 29.98/4.74 thf(func_def_52, type, steps: stream @ product_prod @ state @ rule).
% 29.98/4.74 thf(func_def_53, type, stepsa: stream @ product_prod @ state @ rule).
% 29.98/4.74 thf(func_def_55, type, db1: !>[X0: $tType]:(X0)).
% 29.98/4.74 thf(func_def_56, type, db0: !>[X0: $tType]:(X0)).
% 29.98/4.74 thf(func_def_57, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 29.98/4.74 thf(func_def_58, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 29.98/4.74 thf(func_def_59, type, vAND: ($o > $o > $o)).
% 29.98/4.74 thf(func_def_62, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 29.98/4.74 thf(func_def_63, type, db2: !>[X0: $tType]:(X0)).
% 29.98/4.74 thf(func_def_64, type, vIMP: ($o > $o > $o)).
% 29.98/4.74 thf(func_def_65, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 29.98/4.74 thf(func_def_66, type, vNOT: ($o > $o)).
% 29.98/4.74 thf(func_def_67, type, db4: !>[X0: $tType]:(X0)).
% 29.98/4.74 thf(func_def_68, type, db3: !>[X0: $tType]:(X0)).
% 29.98/4.74 thf(func_def_69, type, db5: !>[X0: $tType]:(X0)).
% 29.98/4.74 thf(func_def_70, type, sP0: !>[X0: $tType, X1: $tType]:(((X1 > X0 > fset @ X0 > $o) > stream @ X1 > set @ X0 > $o))).
% 29.98/4.74 thf(func_def_71, type, sP1: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 29.98/4.74 thf(func_def_72, type, sP2: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 29.98/4.74 thf(func_def_73, type, sP3: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 29.98/4.74 thf(func_def_74, type, sK4: !>[X0: $tType]:(((X0 > $o) > X0 > X0))).
% 29.98/4.74 thf(func_def_75, type, sK5: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_76, type, sK6: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_77, type, sK7: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_78, type, sK8: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_79, type, sK9: !>[X0: $tType, X1: $tType]:((X1 > fset @ X0 > (X0 > X1) > X0))).
% 29.98/4.74 thf(func_def_80, type, sK10: !>[X0: $tType, X1: $tType]:(((stream @ product_prod @ X0 @ X1 > $o) > (X1 > X0 > fset @ X0 > $o) > stream @ X1 > stream @ product_prod @ X0 @ X1))).
% 29.98/4.74 thf(func_def_81, type, sK11: !>[X0: $tType]:((fset @ X0 > fset @ X0 > X0))).
% 29.98/4.74 thf(func_def_82, type, sK12: !>[X0: $tType]:(((X0 > $o) > X0 > X0))).
% 29.98/4.74 thf(func_def_83, type, sK13: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_84, type, sK14: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 29.98/4.74 thf(func_def_85, type, sK15: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 29.98/4.74 thf(func_def_86, type, sK16: (state > abstra2103299360e_tree @ product_prod @ state @ rule > stream @ rule > state)).
% 29.98/4.74 thf(func_def_87, type, sK17: (state > abstra2103299360e_tree @ product_prod @ state @ rule > stream @ rule > fset @ state)).
% 29.98/4.74 thf(func_def_88, type, sK18: !>[X0: $tType]:(((stream @ X0 > stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_89, type, sK19: !>[X0: $tType]:(((stream @ X0 > stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_90, type, sK20: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 29.98/4.74 thf(func_def_91, type, sK21: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 29.98/4.74 thf(func_def_92, type, sK22: !>[X0: $tType, X1: $tType]:((stream @ product_prod @ X0 @ X1 > (X1 > X0 > fset @ X0 > $o) > stream @ X1 > fset @ X0))).
% 29.98/4.74 thf(func_def_93, type, sK23: (state > stream @ rule > nat)).
% 29.98/4.74 thf(func_def_94, type, sK24: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_95, type, sK25: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X1 @ product_prod @ X2 @ product_prod @ X0 @ X3 > X2))).
% 29.98/4.74 thf(func_def_96, type, sK26: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X1 @ product_prod @ X2 @ product_prod @ X0 @ X3 > X0))).
% 29.98/4.74 thf(func_def_97, type, sK27: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X1 @ product_prod @ X2 @ product_prod @ X0 @ X3 > X3))).
% 29.98/4.74 thf(func_def_98, type, sK28: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X1 @ product_prod @ X2 @ product_prod @ X0 @ X3 > X1))).
% 29.98/4.74 thf(func_def_99, type, sK29: ((stream @ product_prod @ state @ rule > $o) > stream @ product_prod @ state @ rule)).
% 29.98/4.74 thf(func_def_100, type, sK30: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_101, type, sK31: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_102, type, sK32: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_103, type, sK33: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X4 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X5 > X2))).
% 29.98/4.74 thf(func_def_104, type, sK34: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X4 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X5 > X0))).
% 29.98/4.74 thf(func_def_105, type, sK35: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X4 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X5 > X5))).
% 29.98/4.74 thf(func_def_106, type, sK36: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X4 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X5 > X1))).
% 29.98/4.74 thf(func_def_107, type, sK37: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X4 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X5 > X4))).
% 29.98/4.74 thf(func_def_108, type, sK38: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X4 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X5 > X3))).
% 29.98/4.74 thf(func_def_109, type, sK39: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_110, type, sK40: !>[X0: $tType]:((set @ X0 > X0))).
% 29.98/4.74 thf(func_def_111, type, sK41: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_112, type, sK42: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X5 @ product_prod @ X2 @ product_prod @ X6 @ X1 > X6))).
% 29.98/4.74 thf(func_def_113, type, sK43: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X5 @ product_prod @ X2 @ product_prod @ X6 @ X1 > X0))).
% 29.98/4.74 thf(func_def_114, type, sK44: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X5 @ product_prod @ X2 @ product_prod @ X6 @ X1 > X3))).
% 29.98/4.74 thf(func_def_115, type, sK45: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X5 @ product_prod @ X2 @ product_prod @ X6 @ X1 > X1))).
% 29.98/4.74 thf(func_def_116, type, sK46: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X5 @ product_prod @ X2 @ product_prod @ X6 @ X1 > X5))).
% 29.98/4.74 thf(func_def_117, type, sK47: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X5 @ product_prod @ X2 @ product_prod @ X6 @ X1 > X4))).
% 29.98/4.74 thf(func_def_118, type, sK48: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X5 @ product_prod @ X2 @ product_prod @ X6 @ X1 > X2))).
% 29.98/4.74 thf(func_def_119, type, sK49: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X3 @ product_prod @ X1 @ product_prod @ X2 @ X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_120, type, sK50: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X3 @ product_prod @ X1 @ product_prod @ X2 @ X0 > $o) > X2))).
% 29.98/4.74 thf(func_def_121, type, sK51: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X3 @ product_prod @ X1 @ product_prod @ X2 @ X0 > $o) > X1))).
% 29.98/4.74 thf(func_def_122, type, sK52: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X3 @ product_prod @ X1 @ product_prod @ X2 @ X0 > $o) > X3))).
% 29.98/4.74 thf(func_def_123, type, sK53: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_124, type, sK54: (nat > stream @ product_prod @ state @ rule > stream @ rule > nat)).
% 29.98/4.74 thf(func_def_125, type, sK55: (nat > stream @ product_prod @ state @ rule > stream @ rule > state)).
% 29.98/4.74 thf(func_def_126, type, sK56: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > fset @ X0 > X0))).
% 29.98/4.74 thf(func_def_127, type, sK57: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 29.98/4.74 thf(func_def_128, type, sK58: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_129, type, sK59: !>[X0: $tType, X1: $tType]:(((X1 > X0 > $o) > fset @ X1 > X1 > X0))).
% 29.98/4.74 thf(func_def_130, type, sK60: !>[X0: $tType, X1: $tType]:(((X1 > X0 > $o) > fset @ X1 > X1))).
% 29.98/4.74 thf(func_def_131, type, sK61: !>[X0: $tType]:(((abstra2103299360e_tree @ X0 > stream @ X0 > $o) > abstra2103299360e_tree @ X0))).
% 29.98/4.74 thf(func_def_132, type, sK62: !>[X0: $tType]:(((abstra2103299360e_tree @ X0 > stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_133, type, sK63: !>[X0: $tType, X1: $tType]:(((X1 > X0 > fset @ X0 > $o) > stream @ X1 > set @ X0 > X0))).
% 29.98/4.74 thf(func_def_134, type, sK64: !>[X0: $tType, X1: $tType]:(((X1 > X0 > fset @ X0 > $o) > stream @ X1 > set @ X0 > X1))).
% 29.98/4.74 thf(func_def_135, type, sK65: !>[X0: $tType, X1: $tType]:(((X1 > X0 > fset @ X0 > $o) > stream @ X1 > set @ X0 > fset @ X0))).
% 29.98/4.74 thf(func_def_136, type, sK66: !>[X0: $tType, X1: $tType]:(((X1 > X0 > fset @ X0 > $o) > stream @ X1 > set @ X0 > X0))).
% 29.98/4.74 thf(func_def_137, type, sK67: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > set @ X1 > stream @ X0 > X1))).
% 29.98/4.74 thf(func_def_138, type, sK68: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X0))).
% 29.98/4.74 thf(func_def_139, type, sK69: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X1))).
% 29.98/4.74 thf(func_def_140, type, sK70: !>[X0: $tType]:((abstra2103299360e_tree @ X0 > stream @ X0 > abstra2103299360e_tree @ X0))).
% 29.98/4.74 thf(func_def_141, type, sK71: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_142, type, sK72: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X4 @ product_prod @ X3 @ product_prod @ X0 @ product_prod @ X2 @ X1 > X2))).
% 29.98/4.74 thf(func_def_143, type, sK73: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X4 @ product_prod @ X3 @ product_prod @ X0 @ product_prod @ X2 @ X1 > X1))).
% 29.98/4.74 thf(func_def_144, type, sK74: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X4 @ product_prod @ X3 @ product_prod @ X0 @ product_prod @ X2 @ X1 > X3))).
% 29.98/4.74 thf(func_def_145, type, sK75: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X4 @ product_prod @ X3 @ product_prod @ X0 @ product_prod @ X2 @ X1 > X4))).
% 29.98/4.74 thf(func_def_146, type, sK76: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X4 @ product_prod @ X3 @ product_prod @ X0 @ product_prod @ X2 @ X1 > X0))).
% 29.98/4.74 thf(func_def_147, type, sK77: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > stream @ X0 > X1 > X0))).
% 29.98/4.74 thf(func_def_148, type, sK78: !>[X0: $tType, X1: $tType]:(((X0 > X1 > fset @ X1 > $o) > stream @ X0 > X1 > fset @ X1))).
% 29.98/4.74 thf(func_def_149, type, sK79: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X1 @ product_prod @ X6 @ product_prod @ X0 @ product_prod @ X2 @ product_prod @ X4 @ product_prod @ X3 @ X5 > $o) > X0))).
% 29.98/4.74 thf(func_def_150, type, sK80: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X1 @ product_prod @ X6 @ product_prod @ X0 @ product_prod @ X2 @ product_prod @ X4 @ product_prod @ X3 @ X5 > $o) > X4))).
% 29.98/4.74 thf(func_def_151, type, sK81: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X1 @ product_prod @ X6 @ product_prod @ X0 @ product_prod @ X2 @ product_prod @ X4 @ product_prod @ X3 @ X5 > $o) > X1))).
% 29.98/4.74 thf(func_def_152, type, sK82: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X1 @ product_prod @ X6 @ product_prod @ X0 @ product_prod @ X2 @ product_prod @ X4 @ product_prod @ X3 @ X5 > $o) > X6))).
% 29.98/4.74 thf(func_def_153, type, sK83: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X1 @ product_prod @ X6 @ product_prod @ X0 @ product_prod @ X2 @ product_prod @ X4 @ product_prod @ X3 @ X5 > $o) > X5))).
% 29.98/4.74 thf(func_def_154, type, sK84: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X1 @ product_prod @ X6 @ product_prod @ X0 @ product_prod @ X2 @ product_prod @ X4 @ product_prod @ X3 @ X5 > $o) > X3))).
% 29.98/4.74 thf(func_def_155, type, sK85: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X1 @ product_prod @ X6 @ product_prod @ X0 @ product_prod @ X2 @ product_prod @ X4 @ product_prod @ X3 @ X5 > $o) > X2))).
% 29.98/4.74 thf(func_def_156, type, sK86: !>[X0: $tType]:(((X0 > stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_157, type, sK87: !>[X0: $tType]:(((X0 > stream @ X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_158, type, sK88: !>[X0: $tType]:(((X0 > stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_159, type, sK89: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 29.98/4.74 thf(func_def_160, type, sK90: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 29.98/4.74 thf(func_def_161, type, sK91: (state > rule)).
% 29.98/4.74 thf(func_def_162, type, sK92: (state > fset @ state)).
% 29.98/4.74 thf(func_def_163, type, sK93: state).
% 29.98/4.74 thf(func_def_164, type, sK94: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_165, type, sK95: !>[X0: $tType, X1: $tType]:((product_prod @ X1 @ X0 > X1))).
% 29.98/4.74 thf(func_def_166, type, sK96: !>[X0: $tType, X1: $tType]:((product_prod @ X1 @ X0 > X0))).
% 29.98/4.74 thf(func_def_167, type, sK97: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > X0))).
% 29.98/4.74 thf(func_def_168, type, sK98: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_169, type, sK99: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X3 @ product_prod @ X1 @ product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ X2 > $o) > X2))).
% 29.98/4.74 thf(func_def_170, type, sK100: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X3 @ product_prod @ X1 @ product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ X2 > $o) > X3))).
% 29.98/4.74 thf(func_def_171, type, sK101: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X3 @ product_prod @ X1 @ product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ X2 > $o) > X5))).
% 29.98/4.74 thf(func_def_172, type, sK102: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X3 @ product_prod @ X1 @ product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ X2 > $o) > X4))).
% 29.98/4.74 thf(func_def_173, type, sK103: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X3 @ product_prod @ X1 @ product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ X2 > $o) > X0))).
% 29.98/4.74 thf(func_def_174, type, sK104: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X3 @ product_prod @ X1 @ product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ X2 > $o) > X1))).
% 29.98/4.74 thf(func_def_175, type, sK105: !>[X0: $tType, X1: $tType]:(((product_prod @ X1 @ X0 > $o) > X1))).
% 29.98/4.74 thf(func_def_176, type, sK106: !>[X0: $tType, X1: $tType]:(((product_prod @ X1 @ X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_177, type, sK107: !>[X0: $tType, X1: $tType, X2: $tType]:(((product_prod @ X1 @ product_prod @ X0 @ X2 > $o) > X0))).
% 29.98/4.74 thf(func_def_178, type, sK108: !>[X0: $tType, X1: $tType, X2: $tType]:(((product_prod @ X1 @ product_prod @ X0 @ X2 > $o) > X2))).
% 29.98/4.74 thf(func_def_179, type, sK109: !>[X0: $tType, X1: $tType, X2: $tType]:(((product_prod @ X1 @ product_prod @ X0 @ X2 > $o) > X1))).
% 29.98/4.74 thf(func_def_180, type, sK110: !>[X0: $tType, X1: $tType]:((stream @ product_prod @ X1 @ X0 > stream @ X0 > set @ X1 > nat > (X0 > X1 > fset @ X1 > $o) > X1))).
% 29.98/4.74 thf(func_def_181, type, sK111: !>[X0: $tType, X1: $tType]:((stream @ product_prod @ X1 @ X0 > stream @ X0 > set @ X1 > nat > (X0 > X1 > fset @ X1 > $o) > nat))).
% 29.98/4.74 thf(func_def_182, type, sK112: !>[X0: $tType, X1: $tType]:((stream @ X1 > (X1 > X0 > fset @ X0 > $o) > X0 > nat))).
% 29.98/4.74 thf(func_def_183, type, sK113: !>[X0: $tType, X1: $tType]:(((product_prod @ X1 @ X0 > $o) > X1))).
% 29.98/4.74 thf(func_def_184, type, sK114: !>[X0: $tType, X1: $tType]:(((product_prod @ X1 @ X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_185, type, sK115: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X2 @ product_prod @ X3 @ X1 > $o) > X3))).
% 29.98/4.74 thf(func_def_186, type, sK116: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X2 @ product_prod @ X3 @ X1 > $o) > X4))).
% 29.98/4.74 thf(func_def_187, type, sK117: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X2 @ product_prod @ X3 @ X1 > $o) > X0))).
% 29.98/4.74 thf(func_def_188, type, sK118: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X2 @ product_prod @ X3 @ X1 > $o) > X1))).
% 29.98/4.74 thf(func_def_189, type, sK119: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X2 @ product_prod @ X3 @ X1 > $o) > X2))).
% 29.98/4.74 thf(func_def_190, type, sK120: !>[X0: $tType]:(((stream @ X0 > stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_191, type, sK121: !>[X0: $tType]:(((stream @ X0 > stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_192, type, sK122: !>[X0: $tType, X1: $tType, X2: $tType]:((product_prod @ X0 @ product_prod @ X1 @ X2 > X0))).
% 29.98/4.74 thf(func_def_193, type, sK123: !>[X0: $tType, X1: $tType, X2: $tType]:((product_prod @ X0 @ product_prod @ X1 @ X2 > X1))).
% 29.98/4.74 thf(func_def_194, type, sK124: !>[X0: $tType, X1: $tType, X2: $tType]:((product_prod @ X0 @ product_prod @ X1 @ X2 > X2))).
% 29.98/4.74 thf(func_def_195, type, sK125: !>[X0: $tType]:((fset @ X0 > X0))).
% 29.98/4.74 thf(func_def_196, type, sK126: !>[X0: $tType, X1: $tType]:((fset @ X1 > fset @ X0 > (X0 > X1) > X0))).
% 29.98/4.74 thf(func_def_197, type, sK127: !>[X0: $tType]:((set @ X0 > set @ X0 > X0))).
% 29.98/4.74 thf(func_def_198, type, sK128: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 29.98/4.74 thf(func_def_199, type, sK129: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 29.98/4.74 thf(func_def_200, type, sK130: (stream @ product_prod @ state @ rule > fset @ state)).
% 29.98/4.74 thf(func_def_201, type, sK131: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 29.98/4.74 thf(func_def_202, type, sK132: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_203, type, sK133: !>[X0: $tType]:((fset @ X0 > fset @ X0 > X0))).
% 29.98/4.74 thf(func_def_204, type, sK134: !>[X0: $tType]:(((stream @ X0 > $o) > stream @ X0))).
% 29.98/4.74 thf(func_def_205, type, sK135: !>[X0: $tType, X1: $tType]:(((stream @ X1 > stream @ X0) > stream @ X1))).
% 29.98/4.74 thf(func_def_206, type, sK136: !>[X0: $tType, X1: $tType]:((stream @ X1 > set @ X0 > X0 > (X1 > X0 > fset @ X0 > $o) > abstra2103299360e_tree @ product_prod @ X0 @ X1 > X0))).
% 29.98/4.74 thf(func_def_207, type, sK137: !>[X0: $tType, X1: $tType]:((stream @ X1 > set @ X0 > X0 > (X1 > X0 > fset @ X0 > $o) > abstra2103299360e_tree @ product_prod @ X0 @ X1 > fset @ X0))).
% 29.98/4.74 thf(f8,axiom,(
% 29.98/4.74 (linear1386806755on_alw @ product_prod @ state @ rule @ (linear1707521579_holds @ product_prod @ state @ rule @ (^[X0 : product_prod @ state @ rule] : ((abstra1874422341nabled @ rule @ state @ eff @ r @ (product_fst @ state @ rule @ X0))))) @ stepsa)),
% 29.98/4.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_less_Oprems_I4_J)).
% 29.98/4.74 thf(f24,axiom,(
% 29.98/4.74 ~((((abstra573067619e_root @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ rsa @ sa))) = ((shd @ product_prod @ state @ rule @ stepsa))) => ! [X0 : state] : ((abstra313004635_ipath @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ (stl @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ rsa @ sa)) @ X0) @ (stl @ product_prod @ state @ rule @ stepsa)) => ~(member @ state @ X0 @ s)))),
% 29.98/4.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_23__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062t_H_As_H_O_A_092_060lbrakk_062tree_Oroot_A_ImkTree_Ars_As_J_A_061_Ashd_Asteps_059_Aipath_A_ImkTree_A_Istl_A_Itrim_Ars_As_J_J_As_H_J_A_Istl_Asteps_J_059_As_H_A_092_060in_062_AS_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062)).
% 29.98/4.74 thf(f64,axiom,(
% 29.98/4.74 ! [X1 : state,X0 : stream @ rule] : (((abstra573067619e_root @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ X0 @ X1))) = ((product_Pair @ state @ rule @ X1 @ (shd @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ X0 @ X1)))))),
% 29.98/4.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_63_mkTree_Osimps_I1_J)).
% 29.98/4.74 thf(f131,axiom,(
% 29.98/4.74 ! [X0 : $tType,X2 : stream @ X0,X1 : (stream @ X0 > $o)] : ((linear1386806755on_alw @ X0 @ X1 @ X2) => ~((X1 @ X2) => ~(linear1386806755on_alw @ X0 @ X1 @ (stl @ X0 @ X2))))),
% 29.98/4.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_alw_Ocases)).
% 29.98/4.74 thf(f141,axiom,(
% 29.98/4.74 ! [X0 : $tType,X1 : (X0 > $o),X3 : $o,X2 : stream @ X0] : ((((linear1707521579_holds @ X0 @ X1 @ X2)) = X3) => (X3 = ((X1 @ (shd @ X0 @ X2)))))),
% 29.98/4.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_140_holds_Oelims_I1_J)).
% 29.98/4.74 thf(f220,axiom,(
% 29.98/4.74 ! [X0 : $tType,X1 : $tType,X2 : product_prod @ X1 @ X0] : (((product_Pair @ X1 @ X0 @ (product_fst @ X1 @ X0 @ X2) @ (product_snd @ X1 @ X0 @ X2))) = X2)),
% 29.98/4.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_219_prod_Ocollapse)).
% 29.98/4.74 thf(f253,axiom,(
% 29.98/4.74 ! [X0 : $tType,X1 : $tType,X2 : X0,X3 : X1,X5 : X1,X4 : X0] : ((((product_Pair @ X0 @ X1 @ X2 @ X3)) = ((product_Pair @ X0 @ X1 @ X4 @ X5))) => ~((X2 = X4) => (X3 != X5)))),
% 29.98/4.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_252_Pair__inject)).
% 29.98/4.74 thf(f288,conjecture,(
% 29.98/4.74 (abstra1874422341nabled @ rule @ state @ eff @ r @ sa)),
% 29.98/4.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 29.98/4.74 thf(f289,negated_conjecture,(
% 29.98/4.74 ~(abstra1874422341nabled @ rule @ state @ eff @ r @ sa)),
% 29.98/4.74 inference(negated_conjecture,[status(cth)],[f288])).
% 29.98/4.74 thf(f396,plain,(
% 29.98/4.74 ~((((abstra573067619e_root @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ rsa @ sa))) = ((shd @ product_prod @ state @ rule @ stepsa))) => ! [X0 : state] : ((abstra313004635_ipath @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ (stl @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ rsa @ sa)) @ X0) @ (stl @ product_prod @ state @ rule @ stepsa)) => ~(member @ state @ X0 @ s)))),
% 29.98/4.74 inference(rectify,[],[f24])).
% 29.98/4.74 thf(f397,plain,(
% 29.98/4.74 ~((((abstra573067619e_root @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ rsa @ sa))) = ((shd @ product_prod @ state @ rule @ stepsa))) => ! [X0 : state] : ((((abstra313004635_ipath @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ (stl @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ rsa @ sa)) @ X0) @ (stl @ product_prod @ state @ rule @ stepsa))) = $true) => ~ (((member @ state @ X0 @ s)) = $true)))),
% 29.98/4.74 inference(fool_elimination,[],[f396])).
% 29.98/4.74 thf(f406,plain,(
% 29.98/4.74 (linear1386806755on_alw @ product_prod @ state @ rule @ (linear1707521579_holds @ product_prod @ state @ rule @ (^[X0 : product_prod @ state @ rule] : ((abstra1874422341nabled @ rule @ state @ eff @ r @ (product_fst @ state @ rule @ X0))))) @ stepsa)),
% 29.98/4.74 inference(rectify,[],[f8])).
% 29.98/4.74 thf(f407,plain,(
% 29.98/4.74 ($true = ((linear1386806755on_alw @ product_prod @ state @ rule @ (linear1707521579_holds @ product_prod @ state @ rule @ (^[Y0 : product_prod @ state @ rule]: (abstra1874422341nabled @ rule @ state @ eff @ r @ (product_fst @ state @ rule @ Y0)))) @ stepsa)))),
% 29.98/4.74 inference(fool_elimination,[],[f406])).
% 29.98/4.74 thf(f545,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : (X0 > $o),X2 : $o,X3 : stream @ X0] : ((((linear1707521579_holds @ X0 @ X1 @ X3)) = X2) => (((X1 @ (shd @ X0 @ X3))) = X2))),
% 29.98/4.74 inference(rectify,[],[f141])).
% 29.98/4.74 thf(f546,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : (X0 > $o),X2 : $o,X3 : stream @ X0] : ((((linear1707521579_holds @ X0 @ X1 @ X3)) = X2) => (((X1 @ (shd @ X0 @ X3))) = X2))),
% 29.98/4.74 inference(fool_elimination,[],[f545])).
% 29.98/4.74 thf(f615,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : stream @ X0,X2 : (stream @ X0 > $o)] : ((linear1386806755on_alw @ X0 @ X2 @ X1) => ~((X2 @ X1) => ~(linear1386806755on_alw @ X0 @ X2 @ (stl @ X0 @ X1))))),
% 29.98/4.74 inference(rectify,[],[f131])).
% 29.98/4.74 thf(f616,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : stream @ X0,X2 : (stream @ X0 > $o)] : (($true = ((linear1386806755on_alw @ X0 @ X2 @ X1))) => ~(($true = ((X2 @ X1))) => ~ ($true = ((linear1386806755on_alw @ X0 @ X2 @ (stl @ X0 @ X1))))))),
% 29.98/4.74 inference(fool_elimination,[],[f615])).
% 29.98/4.74 thf(f725,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : $tType,X2 : X0,X3 : X1,X4 : X1,X5 : X0] : ((((product_Pair @ X0 @ X1 @ X2 @ X3)) = ((product_Pair @ X0 @ X1 @ X5 @ X4))) => ~((X2 = X5) => (X3 != X4)))),
% 29.98/4.74 inference(rectify,[],[f253])).
% 29.98/4.74 thf(f726,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : $tType,X3 : X1,X2 : X0,X4 : X1,X5 : X0] : ((((product_Pair @ X0 @ X1 @ X2 @ X3)) = ((product_Pair @ X0 @ X1 @ X5 @ X4))) => ~((X2 = X5) => (X3 != X4)))),
% 29.98/4.74 inference(fool_elimination,[],[f725])).
% 29.98/4.74 thf(f740,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : $tType,X2 : product_prod @ X1 @ X0] : (((product_Pair @ X1 @ X0 @ (product_fst @ X1 @ X0 @ X2) @ (product_snd @ X1 @ X0 @ X2))) = X2)),
% 29.98/4.74 inference(fool_elimination,[],[f220])).
% 29.98/4.74 thf(f815,plain,(
% 29.98/4.74 ! [X0 : state,X1 : stream @ rule] : (((product_Pair @ state @ rule @ X0 @ (shd @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ X1 @ X0)))) = ((abstra573067619e_root @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ X1 @ X0))))),
% 29.98/4.74 inference(rectify,[],[f64])).
% 29.98/4.74 thf(f816,plain,(
% 29.98/4.74 ! [X0 : state,X1 : stream @ rule] : (((product_Pair @ state @ rule @ X0 @ (shd @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ X1 @ X0)))) = ((abstra573067619e_root @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ X1 @ X0))))),
% 29.98/4.74 inference(fool_elimination,[],[f815])).
% 29.98/4.74 thf(f820,plain,(
% 29.98/4.74 ~(abstra1874422341nabled @ rule @ state @ eff @ r @ sa)),
% 29.98/4.74 inference(rectify,[],[f289])).
% 29.98/4.74 thf(f821,plain,(
% 29.98/4.74 ~ (((abstra1874422341nabled @ rule @ state @ eff @ r @ sa)) = $true)),
% 29.98/4.74 inference(fool_elimination,[],[f820])).
% 29.98/4.74 thf(f850,plain,(
% 29.98/4.74 ~((((abstra573067619e_root @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ rsa @ sa))) = ((shd @ product_prod @ state @ rule @ stepsa))) => ! [X0 : state] : ((((abstra313004635_ipath @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ (stl @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ rsa @ sa)) @ X0) @ (stl @ product_prod @ state @ rule @ stepsa))) = $true) => (((member @ state @ X0 @ s)) != $true)))),
% 29.98/4.74 inference(flattening,[],[f397])).
% 29.98/4.74 thf(f862,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : stream @ X0,X2 : (stream @ X0 > $o)] : (($true = ((linear1386806755on_alw @ X0 @ X2 @ X1))) => ~(($true = ((X2 @ X1))) => ($true != ((linear1386806755on_alw @ X0 @ X2 @ (stl @ X0 @ X1))))))),
% 29.98/4.74 inference(flattening,[],[f616])).
% 29.98/4.74 thf(f868,plain,(
% 29.98/4.74 (((abstra1874422341nabled @ rule @ state @ eff @ r @ sa)) != $true)),
% 29.98/4.74 inference(flattening,[],[f821])).
% 29.98/4.74 thf(f1022,plain,(
% 29.98/4.74 ! [X0 : $tType,X3 : stream @ X0,X2 : $o,X1 : (X0 > $o)] : ((((X1 @ (shd @ X0 @ X3))) = X2) | (((linear1707521579_holds @ X0 @ X1 @ X3)) != X2))),
% 29.98/4.74 inference(ennf_transformation,[],[f546])).
% 29.98/4.74 thf(f1040,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : $tType,X2 : X0,X4 : X1,X3 : X1,X5 : X0] : ((((product_Pair @ X0 @ X1 @ X2 @ X3)) != ((product_Pair @ X0 @ X1 @ X5 @ X4))) | ((X3 = X4) & (X2 = X5)))),
% 29.98/4.74 inference(ennf_transformation,[],[f726])).
% 29.98/4.74 thf(f1050,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : stream @ X0,X2 : (stream @ X0 > $o)] : (($true != ((linear1386806755on_alw @ X0 @ X2 @ X1))) | (($true = ((linear1386806755on_alw @ X0 @ X2 @ (stl @ X0 @ X1)))) & ($true = ((X2 @ X1)))))),
% 29.98/4.74 inference(ennf_transformation,[],[f862])).
% 29.98/4.74 thf(f1110,plain,(
% 29.98/4.74 ? [X0 : state] : ((((abstra313004635_ipath @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ (stl @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ rsa @ sa)) @ X0) @ (stl @ product_prod @ state @ rule @ stepsa))) = $true) & (((member @ state @ X0 @ s)) = $true)) & (((abstra573067619e_root @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ rsa @ sa))) = ((shd @ product_prod @ state @ rule @ stepsa)))),
% 29.98/4.74 inference(ennf_transformation,[],[f850])).
% 29.98/4.74 thf(f1176,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : $tType,X2 : X0,X3 : X1,X4 : X1,X5 : X0] : ((((product_Pair @ X0 @ X1 @ X5 @ X3)) != ((product_Pair @ X0 @ X1 @ X2 @ X4))) | ((X3 = X4) & (X2 = X5)))),
% 29.98/4.74 inference(rectify,[],[f1040])).
% 29.98/4.74 thf(f1284,plain,(
% 29.98/4.74 (($true = ((abstra313004635_ipath @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ (stl @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ rsa @ sa)) @ sK93) @ (stl @ product_prod @ state @ rule @ stepsa)))) & ($true = ((member @ state @ sK93 @ s)))) & (((abstra573067619e_root @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ rsa @ sa))) = ((shd @ product_prod @ state @ rule @ stepsa)))),
% 29.98/4.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK93]),skolemize(X0,sK93)],[f1110])).
% 29.98/4.74 thf(f1325,plain,(
% 29.98/4.74 ! [X0 : $tType,X1 : stream @ X0,X2 : $o,X3 : (X0 > $o)] : ((((X3 @ (shd @ X0 @ X1))) = X2) | (((linear1707521579_holds @ X0 @ X3 @ X1)) != X2))),
% 29.98/4.74 inference(rectify,[],[f1022])).
% 29.98/4.74 thf(f1426,plain,(
% 29.98/4.74 ( ! [X1 : $tType,X0 : $tType,X2 : X0,X3 : X1,X4 : X1,X5 : X0] : ((((product_Pair @ X0 @ X1 @ X5 @ X3)) != ((product_Pair @ X0 @ X1 @ X2 @ X4))) | (X2 = X5)) )),
% 29.98/4.74 inference(cnf_transformation,[],[f1176])).
% 29.98/4.74 thf(f1431,plain,(
% 29.98/4.74 ( ! [X1 : $tType,X0 : $tType,X2 : product_prod @ X1 @ X0] : ((((product_Pair @ X1 @ X0 @ (product_fst @ X1 @ X0 @ X2) @ (product_snd @ X1 @ X0 @ X2))) = X2)) )),
% 29.98/4.74 inference(cnf_transformation,[],[f740])).
% 29.98/4.74 thf(f1486,plain,(
% 29.98/4.74 (((abstra1874422341nabled @ rule @ state @ eff @ r @ sa)) != $true)),
% 29.98/4.74 inference(cnf_transformation,[],[f868])).
% 29.98/4.74 thf(f1506,plain,(
% 29.98/4.74 ( ! [X0 : $tType,X2 : (stream @ X0 > $o),X1 : stream @ X0] : (($true != ((linear1386806755on_alw @ X0 @ X2 @ X1))) | ($true = ((X2 @ X1)))) )),
% 29.98/4.74 inference(cnf_transformation,[],[f1050])).
% 29.98/4.74 thf(f1530,plain,(
% 29.98/4.74 ($true = ((linear1386806755on_alw @ product_prod @ state @ rule @ (linear1707521579_holds @ product_prod @ state @ rule @ (^[Y0 : product_prod @ state @ rule]: (abstra1874422341nabled @ rule @ state @ eff @ r @ (product_fst @ state @ rule @ Y0)))) @ stepsa)))),
% 29.98/4.74 inference(cnf_transformation,[],[f407])).
% 29.98/4.74 thf(f1624,plain,(
% 29.98/4.74 (((abstra573067619e_root @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ rsa @ sa))) = ((shd @ product_prod @ state @ rule @ stepsa)))),
% 29.98/4.74 inference(cnf_transformation,[],[f1284])).
% 29.98/4.74 thf(f1688,plain,(
% 29.98/4.74 ( ! [X0 : state,X1 : stream @ rule] : ((((product_Pair @ state @ rule @ X0 @ (shd @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ X1 @ X0)))) = ((abstra573067619e_root @ product_prod @ state @ rule @ (abstra1225283448mkTree @ rule @ state @ eff @ X1 @ X0))))) )),
% 29.98/4.74 inference(cnf_transformation,[],[f816])).
% 29.98/4.74 thf(f1690,plain,(
% 29.98/4.74 ( ! [X0 : $tType,X2 : $o,X3 : (X0 > $o),X1 : stream @ X0] : ((((X3 @ (shd @ X0 @ X1))) = X2) | (((linear1707521579_holds @ X0 @ X3 @ X1)) != X2)) )),
% 29.98/4.74 inference(cnf_transformation,[],[f1325])).
% 29.98/4.74 thf(f1739,definition,(
% 29.98/4.74 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 29.98/4.74 introduced(theory,[fool_exhaustiveness_axiom])).
% 29.98/4.74 thf(f1771,plain,(
% 29.98/4.74 ( ! [X0 : $tType,X3 : (X0 > $o),X1 : stream @ X0] : ((((X3 @ (shd @ X0 @ X1))) = ((linear1707521579_holds @ X0 @ X3 @ X1)))) )),
% 29.98/4.74 inference(equality_resolution,[],[f1690])).
% 29.98/4.74 thf(f1789,plain,(
% 29.98/4.74 (((shd @ product_prod @ state @ rule @ stepsa)) = ((product_Pair @ state @ rule @ sa @ (shd @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ rsa @ sa)))))),
% 29.98/4.74 inference(forward_demodulation,[],[f1624,f1688])).
% 29.98/4.74 thf(f1803,plain,(
% 29.98/4.74 ($true != $true) | (((abstra1874422341nabled @ rule @ state @ eff @ r @ sa)) = $false)),
% 29.98/4.74 inference(constrained_superposition,[],[f1486,f1739])).
% 29.98/4.74 thf(f1805,plain,(
% 29.98/4.74 (((abstra1874422341nabled @ rule @ state @ eff @ r @ sa)) = $false)),
% 29.98/4.75 inference(trivial_inequality_removal,[],[f1803])).
% 29.98/4.75 thf(f2113,plain,(
% 29.98/4.75 ($true = ((linear1707521579_holds @ product_prod @ state @ rule @ (^[Y0 : product_prod @ state @ rule]: (abstra1874422341nabled @ rule @ state @ eff @ r @ (product_fst @ state @ rule @ Y0))) @ stepsa)))),
% 29.98/4.75 inference(unit_resulting_resolution,[],[f1506,f1530])).
% 29.98/4.75 thf(f2119,plain,(
% 29.98/4.75 ($true = (((^[Y0 : product_prod @ state @ rule]: (abstra1874422341nabled @ rule @ state @ eff @ r @ (product_fst @ state @ rule @ Y0))) @ (shd @ product_prod @ state @ rule @ stepsa))))),
% 29.98/4.75 inference(forward_demodulation,[],[f2113,f1771])).
% 29.98/4.75 thf(f2120,plain,(
% 29.98/4.75 ($true = ((abstra1874422341nabled @ rule @ state @ eff @ r @ (product_fst @ state @ rule @ (shd @ product_prod @ state @ rule @ stepsa)))))),
% 29.98/4.75 inference(beta-eta_normalization,[],[f2119])).
% 29.98/4.75 thf(f2121,plain,(
% 29.98/4.75 ($true = ((abstra1874422341nabled @ rule @ state @ eff @ r @ (product_fst @ state @ rule @ (product_Pair @ state @ rule @ sa @ (shd @ rule @ (abstra1259602206m_trim @ rule @ state @ eff @ rsa @ sa)))))))),
% 29.98/4.75 inference(forward_demodulation,[],[f2120,f1789])).
% 29.98/4.75 thf(f2501,plain,(
% 29.98/4.75 ( ! [X1 : $tType,X0 : $tType,X2 : X0,X3 : X1] : ((((product_fst @ X0 @ X1 @ (product_Pair @ X0 @ X1 @ X2 @ X3))) = X2)) )),
% 29.98/4.75 inference(unit_resulting_resolution,[],[f1426,f1431])).
% 29.98/4.75 thf(f2508,plain,(
% 29.98/4.75 (((abstra1874422341nabled @ rule @ state @ eff @ r @ sa)) = $true)),
% 29.98/4.75 inference(backward_demodulation,[],[f2121,f2501])).
% 29.98/4.75 thf(f2509,plain,(
% 29.98/4.75 ($true = $false)),
% 29.98/4.75 inference(forward_demodulation,[],[f2508,f1805])).
% 29.98/4.75 thf(f2510,plain,(
% 29.98/4.75 $false),
% 29.98/4.75 inference(trivial_inequality_removal,[],[f2509])).
% 29.98/4.75 % SZS output end Proof for theBenchmark
% 29.98/4.75 % (2834112)------------------------------
% 29.98/4.75 % (2834112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.98/4.75 % (2834112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/4.75 % (2834112)CaDiCaL version: 2.1.3
% 29.98/4.75 % (2834112)Termination reason: Refutation
% 29.98/4.75 % (2834112)Time elapsed: 0.209 s
% 29.98/4.75 % (2834112)Peak memory usage: 16 MB
% 29.98/4.75 % (2834112)Instructions burned: 347 (million)
% 29.98/4.75 % (2833790)Success in time 4.437 s
% 29.98/4.75 % Vampire exiting
%------------------------------------------------------------------------------