%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP032^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:08:02 AM UTC 2026
% Result : Theorem 3.85s 1.00s
% Output : Refutation 3.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP032^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n020.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 19:39:57 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/0.24 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.69/0.39 % (1491557)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.69/0.39 % (1491567)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3223970977:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.69/0.39 % (1491568)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.69/0.39 % (1491568)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.69/0.39 % (1491562)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3642308693:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.69/0.39 % (1491563)lrs+10_16_si=on:nwc=1.5:random_seed=2939447595:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.69/0.39 % (1491564)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3680723745:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.69/0.39 % (1491566)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3021100767:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.69/0.39 % (1491565)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=668417167: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.69/0.39 % (1491568)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=469838173:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.69/0.39 % (1491564)Instruction limit reached!
% 0.69/0.39 % (1491564)------------------------------
% 0.69/0.39 % (1491564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.39 % (1491564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.39 % (1491564)CaDiCaL version: 2.1.3
% 0.69/0.39 % (1491564)Termination reason: Instruction limit
% 0.69/0.39 % (1491564)Termination phase: shuffling
% 0.69/0.39 % (1491564)Time elapsed: 0.003 s
% 0.69/0.39 % (1491564)Peak memory usage: 10 MB
% 0.69/0.39 % (1491564)Instructions burned: 6 (million)
% 0.69/0.39 % (1491563)Instruction limit reached!
% 0.69/0.39 % (1491563)------------------------------
% 0.69/0.39 % (1491563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.39 % (1491563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.39 % (1491563)CaDiCaL version: 2.1.3
% 0.69/0.39 % (1491563)Termination reason: Instruction limit
% 0.69/0.39 % (1491563)Termination phase: Property scanning
% 0.69/0.39 % (1491563)Time elapsed: 0.009 s
% 0.69/0.39 % (1491563)Peak memory usage: 10 MB
% 0.69/0.39 % (1491563)Instructions burned: 18 (million)
% 0.69/0.39 % (1491567)Instruction limit reached!
% 0.69/0.39 % (1491567)------------------------------
% 0.69/0.39 % (1491567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.39 % (1491567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.39 % (1491567)CaDiCaL version: 2.1.3
% 0.69/0.40 % (1491567)Termination reason: Instruction limit
% 0.69/0.40 % (1491567)Termination phase: Function definition elimination
% 0.69/0.40 % (1491567)Time elapsed: 0.019 s
% 0.69/0.40 % (1491567)Peak memory usage: 12 MB
% 0.69/0.40 % (1491567)Instructions burned: 76 (million)
% 0.69/0.40 % (1491566)Instruction limit reached!
% 0.69/0.40 % (1491566)------------------------------
% 0.69/0.40 % (1491566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.40 % (1491566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.40 % (1491566)CaDiCaL version: 2.1.3
% 0.69/0.40 % (1491566)Termination reason: Instruction limit
% 0.69/0.40 % (1491566)Termination phase: Property scanning
% 0.69/0.40 % (1491566)Time elapsed: 0.011 s
% 0.69/0.40 % (1491566)Peak memory usage: 10 MB
% 0.69/0.40 % (1491566)Instructions burned: 24 (million)
% 0.69/0.40 % (1491578)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.69/0.40 % (1491578)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4291793570:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.69/0.42 % (1491576)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=324206022:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.69/0.42 % (1491578)Instruction limit reached!
% 0.69/0.42 % (1491578)------------------------------
% 0.69/0.42 % (1491578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.42 % (1491578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.42 % (1491578)CaDiCaL version: 2.1.3
% 0.69/0.42 % (1491578)Termination reason: Instruction limit
% 0.69/0.42 % (1491578)Termination phase: shuffling
% 0.69/0.42 % (1491578)Time elapsed: 0.003 s
% 0.69/0.42 % (1491578)Peak memory usage: 10 MB
% 0.69/0.42 % (1491578)Instructions burned: 11 (million)
% 0.69/0.42 % (1491576)Instruction limit reached!
% 0.69/0.42 % (1491576)------------------------------
% 0.69/0.42 % (1491576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.42 % (1491576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.42 % (1491576)CaDiCaL version: 2.1.3
% 0.69/0.42 % (1491576)Termination reason: Instruction limit
% 0.69/0.42 % (1491576)Termination phase: shuffling
% 0.69/0.42 % (1491576)Time elapsed: 0.003 s
% 0.69/0.42 % (1491576)Peak memory usage: 10 MB
% 0.69/0.42 % (1491576)Instructions burned: 4 (million)
% 0.69/0.42 % (1491577)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=749670683:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.69/0.42 % (1491579)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=269323301:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.69/0.42 % (1491582)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.69/0.42 % (1491582)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.69/0.42 % (1491577)Instruction limit reached!
% 0.69/0.42 % (1491577)------------------------------
% 0.69/0.42 % (1491577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.42 % (1491577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.42 % (1491577)CaDiCaL version: 2.1.3
% 0.69/0.42 % (1491577)Termination reason: Instruction limit
% 0.69/0.42 % (1491577)Termination phase: shuffling
% 0.69/0.42 % (1491577)Time elapsed: 0.007 s
% 0.69/0.42 % (1491577)Peak memory usage: 10 MB
% 0.69/0.42 % (1491577)Instructions burned: 5 (million)
% 0.69/0.42 % (1491582)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3867139885:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.69/0.42 % (1491579)Instruction limit reached!
% 0.69/0.42 % (1491579)------------------------------
% 0.69/0.42 % (1491579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.42 % (1491579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.42 % (1491579)CaDiCaL version: 2.1.3
% 0.69/0.42 % (1491579)Termination reason: Instruction limit
% 0.69/0.42 % (1491579)Termination phase: shuffling
% 0.69/0.42 % (1491579)Time elapsed: 0.006 s
% 0.69/0.42 % (1491579)Peak memory usage: 10 MB
% 0.69/0.42 % (1491579)Instructions burned: 12 (million)
% 0.69/0.42 % (1491562)Instruction limit reached!
% 0.69/0.42 % (1491562)------------------------------
% 0.69/0.42 % (1491562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.42 % (1491562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.42 % (1491562)CaDiCaL version: 2.1.3
% 0.69/0.42 % (1491562)Termination reason: Instruction limit
% 0.69/0.42 % (1491562)Termination phase: Property scanning
% 0.69/0.42 % (1491562)Time elapsed: 0.041 s
% 0.69/0.42 % (1491562)Peak memory usage: 12 MB
% 0.69/0.42 % (1491562)Instructions burned: 88 (million)
% 0.69/0.42 % (1491582)Instruction limit reached!
% 0.69/0.42 % (1491582)------------------------------
% 0.69/0.42 % (1491582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.42 % (1491582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.42 % (1491582)CaDiCaL version: 2.1.3
% 0.69/0.42 % (1491582)Termination reason: Instruction limit
% 0.69/0.45 % (1491582)Termination phase: Property scanning
% 0.69/0.45 % (1491582)Time elapsed: 0.007 s
% 0.69/0.45 % (1491582)Peak memory usage: 10 MB
% 0.69/0.45 % (1491582)Instructions burned: 31 (million)
% 0.69/0.45 % (1491583)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=3109109676:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.69/0.45 % (1491588)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.69/0.45 % (1491589)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=299995209:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.69/0.45 % (1491587)lrs+10_1_si=on:cs=on:random_seed=8824686:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.69/0.45 % (1491588)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=2125359035:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.69/0.45 % (1491587)Instruction limit reached!
% 0.69/0.45 % (1491587)------------------------------
% 0.69/0.45 % (1491587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.45 % (1491587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.45 % (1491587)CaDiCaL version: 2.1.3
% 0.69/0.45 % (1491587)Termination reason: Instruction limit
% 0.69/0.45 % (1491587)Termination phase: shuffling
% 0.69/0.45 % (1491587)Time elapsed: 0.008 s
% 0.69/0.45 % (1491587)Peak memory usage: 10 MB
% 0.69/0.45 % (1491587)Instructions burned: 9 (million)
% 0.69/0.45 % (1491568)Instruction limit reached!
% 0.69/0.45 % (1491568)------------------------------
% 0.69/0.45 % (1491568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.45 % (1491568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.45 % (1491568)CaDiCaL version: 2.1.3
% 0.69/0.45 % (1491568)Termination reason: Instruction limit
% 0.69/0.45 % (1491568)Termination phase: Saturation
% 0.69/0.45 % (1491568)Time elapsed: 0.078 s
% 0.69/0.45 % (1491568)Peak memory usage: 14 MB
% 0.69/0.45 % (1491568)Instructions burned: 158 (million)
% 0.69/0.45 % (1491588)Instruction limit reached!
% 0.69/0.45 % (1491588)------------------------------
% 0.69/0.45 % (1491588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.45 % (1491588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.45 % (1491588)CaDiCaL version: 2.1.3
% 0.69/0.45 % (1491588)Termination reason: Instruction limit
% 0.69/0.45 % (1491588)Termination phase: shuffling
% 0.69/0.45 % (1491588)Time elapsed: 0.003 s
% 0.69/0.45 % (1491588)Peak memory usage: 10 MB
% 0.69/0.45 % (1491588)Instructions burned: 6 (million)
% 0.69/0.45 % (1491590)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=4202947251:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.69/0.45 % (1491589)Instruction limit reached!
% 0.69/0.45 % (1491589)------------------------------
% 0.69/0.45 % (1491589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.45 % (1491589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.45 % (1491589)CaDiCaL version: 2.1.3
% 0.69/0.45 % (1491589)Termination reason: Instruction limit
% 0.69/0.45 % (1491589)Termination phase: Property scanning
% 0.69/0.45 % (1491589)Time elapsed: 0.019 s
% 0.69/0.45 % (1491589)Peak memory usage: 11 MB
% 0.69/0.45 % (1491589)Instructions burned: 40 (million)
% 0.69/0.45 % (1491583)Instruction limit reached!
% 0.69/0.45 % (1491583)------------------------------
% 0.69/0.45 % (1491583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.45 % (1491583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.45 % (1491583)CaDiCaL version: 2.1.3
% 0.69/0.45 % (1491583)Termination reason: Instruction limit
% 0.69/0.45 % (1491583)Termination phase: Property scanning
% 0.69/0.45 % (1491583)Time elapsed: 0.037 s
% 0.69/0.45 % (1491583)Peak memory usage: 11 MB
% 0.69/0.45 % (1491583)Instructions burned: 87 (million)
% 0.69/0.45 % (1491595)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1257144948:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.69/0.45 % (1491595)Instruction limit reached!
% 0.69/0.45 % (1491595)------------------------------
% 1.44/0.52 % (1491595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.44/0.52 % (1491595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.44/0.52 % (1491595)CaDiCaL version: 2.1.3
% 1.44/0.52 % (1491595)Termination reason: Instruction limit
% 1.44/0.52 % (1491595)Termination phase: SInE selection
% 1.44/0.52 % (1491595)Time elapsed: 0.007 s
% 1.44/0.52 % (1491595)Peak memory usage: 11 MB
% 1.44/0.52 % (1491595)Instructions burned: 29 (million)
% 1.44/0.52 % (1491598)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2081201566:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.44/0.52 % (1491597)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1370474585:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.44/0.52 % (1491599)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2073179322:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.44/0.52 % (1491600)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2409098179: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.44/0.52 % (1491600)Instruction limit reached!
% 1.44/0.52 % (1491600)------------------------------
% 1.44/0.52 % (1491600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.44/0.52 % (1491600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.44/0.52 % (1491600)CaDiCaL version: 2.1.3
% 1.44/0.52 % (1491600)Termination reason: Instruction limit
% 1.44/0.52 % (1491600)Termination phase: shuffling
% 1.44/0.52 % (1491600)Time elapsed: 0.002 s
% 1.44/0.52 % (1491600)Peak memory usage: 10 MB
% 1.44/0.52 % (1491600)Instructions burned: 3 (million)
% 1.44/0.52 % (1491597)Instruction limit reached!
% 1.44/0.52 % (1491597)------------------------------
% 1.44/0.52 % (1491597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.44/0.52 % (1491597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.44/0.52 % (1491597)CaDiCaL version: 2.1.3
% 1.44/0.52 % (1491597)Termination reason: Instruction limit
% 1.44/0.52 % (1491597)Termination phase: shuffling
% 1.44/0.52 % (1491597)Time elapsed: 0.007 s
% 1.44/0.52 % (1491597)Peak memory usage: 10 MB
% 1.44/0.52 % (1491597)Instructions burned: 15 (million)
% 1.44/0.52 % (1491599)Instruction limit reached!
% 1.44/0.52 % (1491599)------------------------------
% 1.44/0.52 % (1491599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.44/0.52 % (1491599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.44/0.52 % (1491599)CaDiCaL version: 2.1.3
% 1.44/0.52 % (1491599)Termination reason: Instruction limit
% 1.44/0.52 % (1491599)Termination phase: shuffling
% 1.44/0.52 % (1491599)Time elapsed: 0.007 s
% 1.44/0.52 % (1491599)Peak memory usage: 10 MB
% 1.44/0.52 % (1491599)Instructions burned: 14 (million)
% 1.44/0.52 % (1491590)Refutation not found, incomplete strategy
% 1.44/0.52 % (1491590)------------------------------
% 1.44/0.52 % (1491590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.44/0.52 % (1491590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.44/0.52 % (1491590)CaDiCaL version: 2.1.3
% 1.44/0.52 % (1491590)Termination reason: Refutation not found, incomplete strategy
% 1.44/0.52 % (1491590)Time elapsed: 0.031 s
% 1.44/0.52 % (1491590)Peak memory usage: 12 MB
% 1.44/0.52 % (1491590)Instructions burned: 35 (million)
% 1.44/0.52 % (1491590)------------------------------
% 1.44/0.52 % (1491590)------------------------------
% 1.44/0.52 % (1491602)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2598756314:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.44/0.52 % (1491609)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.44/0.52 % (1491609)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.44/0.52 % (1491610)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.44/0.52 % (1491607)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1600056719:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.22/0.59 % (1491610)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=3416351775:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.22/0.59 % (1491608)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=922747954:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 2.22/0.59 % (1491609)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=3345235567:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.22/0.59 % (1491610)Instruction limit reached!
% 2.22/0.59 % (1491610)------------------------------
% 2.22/0.59 % (1491610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.59 % (1491610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.59 % (1491610)CaDiCaL version: 2.1.3
% 2.22/0.59 % (1491610)Termination reason: Instruction limit
% 2.22/0.59 % (1491610)Termination phase: shuffling
% 2.22/0.59 % (1491610)Time elapsed: 0.002 s
% 2.22/0.59 % (1491610)Peak memory usage: 10 MB
% 2.22/0.59 % (1491610)Instructions burned: 8 (million)
% 2.22/0.59 % (1491602)Instruction limit reached!
% 2.22/0.59 % (1491602)------------------------------
% 2.22/0.59 % (1491602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.59 % (1491602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.59 % (1491602)CaDiCaL version: 2.1.3
% 2.22/0.59 % (1491602)Termination reason: Instruction limit
% 2.22/0.59 % (1491602)Termination phase: shuffling
% 2.22/0.59 % (1491602)Time elapsed: 0.013 s
% 2.22/0.59 % (1491602)Peak memory usage: 10 MB
% 2.22/0.59 % (1491602)Instructions burned: 27 (million)
% 2.22/0.59 % (1491609)Instruction limit reached!
% 2.22/0.59 % (1491609)------------------------------
% 2.22/0.59 % (1491609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.59 % (1491609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.59 % (1491609)CaDiCaL version: 2.1.3
% 2.22/0.59 % (1491609)Termination reason: Instruction limit
% 2.22/0.59 % (1491609)Termination phase: shuffling
% 2.22/0.59 % (1491609)Time elapsed: 0.007 s
% 2.22/0.59 % (1491609)Peak memory usage: 10 MB
% 2.22/0.59 % (1491609)Instructions burned: 15 (million)
% 2.22/0.59 % (1491616)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=1238456823:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.22/0.59 % (1491607)Instruction limit reached!
% 2.22/0.59 % (1491607)------------------------------
% 2.22/0.59 % (1491607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.59 % (1491607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.59 % (1491607)CaDiCaL version: 2.1.3
% 2.22/0.59 % (1491607)Termination reason: Instruction limit
% 2.22/0.59 % (1491607)Termination phase: Property scanning
% 2.22/0.59 % (1491607)Time elapsed: 0.016 s
% 2.22/0.59 % (1491607)Peak memory usage: 10 MB
% 2.22/0.59 % (1491607)Instructions burned: 25 (million)
% 2.22/0.59 % (1491616)Instruction limit reached!
% 2.22/0.59 % (1491616)------------------------------
% 2.22/0.59 % (1491616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.59 % (1491616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.59 % (1491616)CaDiCaL version: 2.1.3
% 2.22/0.59 % (1491616)Termination reason: Instruction limit
% 2.22/0.59 % (1491616)Termination phase: Property scanning
% 2.22/0.59 % (1491616)Time elapsed: 0.008 s
% 2.22/0.59 % (1491616)Peak memory usage: 10 MB
% 2.22/0.59 % (1491616)Instructions burned: 33 (million)
% 2.22/0.59 % (1491617)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1494313004:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.22/0.59 % (1491617)Instruction limit reached!
% 2.22/0.59 % (1491617)------------------------------
% 2.22/0.59 % (1491617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.59 % (1491618)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=112688771:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.48/0.65 % (1491617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.48/0.65 % (1491617)CaDiCaL version: 2.1.3
% 2.48/0.65 % (1491617)Termination reason: Instruction limit
% 2.48/0.65 % (1491617)Termination phase: shuffling
% 2.48/0.65 % (1491617)Time elapsed: 0.004 s
% 2.48/0.65 % (1491617)Peak memory usage: 10 MB
% 2.48/0.65 % (1491617)Instructions burned: 8 (million)
% 2.48/0.65 % (1491608)Instruction limit reached!
% 2.48/0.65 % (1491608)------------------------------
% 2.48/0.65 % (1491608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.48/0.65 % (1491608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.48/0.65 % (1491608)CaDiCaL version: 2.1.3
% 2.48/0.65 % (1491608)Termination reason: Instruction limit
% 2.48/0.65 % (1491608)Termination phase: Property scanning
% 2.48/0.65 % (1491608)Time elapsed: 0.029 s
% 2.48/0.65 % (1491608)Peak memory usage: 11 MB
% 2.48/0.65 % (1491608)Instructions burned: 61 (million)
% 2.48/0.65 % (1491621)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=668745753:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.48/0.65 % (1491618)Instruction limit reached!
% 2.48/0.65 % (1491618)------------------------------
% 2.48/0.65 % (1491618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.48/0.65 % (1491618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.48/0.65 % (1491618)CaDiCaL version: 2.1.3
% 2.48/0.65 % (1491618)Termination reason: Instruction limit
% 2.48/0.65 % (1491618)Termination phase: Property scanning
% 2.48/0.65 % (1491618)Time elapsed: 0.014 s
% 2.48/0.65 % (1491618)Peak memory usage: 10 MB
% 2.48/0.65 % (1491618)Instructions burned: 32 (million)
% 2.48/0.65 % (1491624)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=4030748257:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.48/0.65 % (1491625)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1612518060:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.48/0.65 % (1491620)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1939487826:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.48/0.65 % (1491627)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=90611927:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.48/0.65 % (1491620)Instruction limit reached!
% 2.48/0.65 % (1491620)------------------------------
% 2.48/0.65 % (1491620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.48/0.65 % (1491620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.48/0.65 % (1491620)CaDiCaL version: 2.1.3
% 2.48/0.65 % (1491620)Termination reason: Instruction limit
% 2.48/0.65 % (1491620)Termination phase: Property scanning
% 2.48/0.65 % (1491620)Time elapsed: 0.018 s
% 2.48/0.65 % (1491620)Peak memory usage: 10 MB
% 2.48/0.65 % (1491620)Instructions burned: 20 (million)
% 2.48/0.65 % (1491627)Instruction limit reached!
% 2.48/0.65 % (1491627)------------------------------
% 2.48/0.65 % (1491627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.48/0.65 % (1491627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.48/0.65 % (1491627)CaDiCaL version: 2.1.3
% 2.48/0.65 % (1491627)Termination reason: Instruction limit
% 2.48/0.65 % (1491627)Termination phase: Preprocessing 3
% 2.48/0.65 % (1491627)Time elapsed: 0.021 s
% 2.48/0.65 % (1491627)Peak memory usage: 11 MB
% 2.48/0.65 % (1491627)Instructions burned: 43 (million)
% 2.48/0.65 % (1491632)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.48/0.65 % (1491632)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1044654245:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.48/0.65 % (1491632)Instruction limit reached!
% 2.48/0.65 % (1491632)------------------------------
% 2.48/0.65 % (1491632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.48/0.65 % (1491632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.48/0.65 % (1491632)CaDiCaL version: 2.1.3
% 2.48/0.65 % (1491632)Termination reason: Instruction limit
% 2.48/0.65 % (1491632)Termination phase: shuffling
% 2.48/0.65 % (1491632)Time elapsed: 0.004 s
% 2.48/0.65 % (1491632)Peak memory usage: 10 MB
% 2.60/0.75 % (1491632)Instructions burned: 7 (million)
% 2.60/0.75 % (1491633)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3721010948:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.60/0.75 % (1491635)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=1758960638: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.60/0.75 % (1491624)Instruction limit reached!
% 2.60/0.75 % (1491624)------------------------------
% 2.60/0.75 % (1491624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.75 % (1491624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.75 % (1491624)CaDiCaL version: 2.1.3
% 2.60/0.75 % (1491624)Termination reason: Instruction limit
% 2.60/0.75 % (1491624)Termination phase: Saturation
% 2.60/0.75 % (1491624)Time elapsed: 0.066 s
% 2.60/0.75 % (1491624)Peak memory usage: 13 MB
% 2.60/0.75 % (1491624)Instructions burned: 143 (million)
% 2.60/0.75 % (1491638)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.60/0.75 % (1491638)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=92327051: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.60/0.75 % (1491638)Instruction limit reached!
% 2.60/0.75 % (1491638)------------------------------
% 2.60/0.75 % (1491638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.75 % (1491638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.75 % (1491638)CaDiCaL version: 2.1.3
% 2.60/0.75 % (1491638)Termination reason: Instruction limit
% 2.60/0.75 % (1491638)Termination phase: shuffling
% 2.60/0.75 % (1491638)Time elapsed: 0.003 s
% 2.60/0.75 % (1491638)Peak memory usage: 10 MB
% 2.60/0.75 % (1491638)Instructions burned: 6 (million)
% 2.60/0.75 % (1491598)Instruction limit reached!
% 2.60/0.75 % (1491598)------------------------------
% 2.60/0.75 % (1491598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.75 % (1491598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.75 % (1491598)CaDiCaL version: 2.1.3
% 2.60/0.75 % (1491598)Termination reason: Instruction limit
% 2.60/0.75 % (1491598)Termination phase: Saturation
% 2.60/0.75 % (1491598)Time elapsed: 0.164 s
% 2.60/0.75 % (1491598)Peak memory usage: 14 MB
% 2.60/0.75 % (1491598)Instructions burned: 328 (million)
% 2.60/0.75 % (1491565)Instruction limit reached!
% 2.60/0.75 % (1491565)------------------------------
% 2.60/0.75 % (1491565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.75 % (1491565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.75 % (1491565)CaDiCaL version: 2.1.3
% 2.60/0.75 % (1491565)Termination reason: Instruction limit
% 2.60/0.75 % (1491565)Termination phase: Saturation
% 2.60/0.75 % (1491565)Time elapsed: 0.268 s
% 2.60/0.75 % (1491565)Peak memory usage: 15 MB
% 2.60/0.75 % (1491565)Instructions burned: 636 (million)
% 2.60/0.75 % (1491625)Instruction limit reached!
% 2.60/0.75 % (1491625)------------------------------
% 2.60/0.75 % (1491625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.75 % (1491625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.75 % (1491625)CaDiCaL version: 2.1.3
% 2.60/0.75 % (1491625)Termination reason: Instruction limit
% 2.60/0.75 % (1491625)Termination phase: Saturation
% 2.60/0.75 % (1491625)Time elapsed: 0.098 s
% 2.60/0.75 % (1491625)Peak memory usage: 14 MB
% 2.60/0.75 % (1491625)Instructions burned: 193 (million)
% 2.60/0.75 % (1491640)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1704538389:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 2.60/0.75 % (1491641)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2933652244:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 2.60/0.75 % (1491642)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=4212399925:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 2.60/0.75 % (1491641)Instruction limit reached!
% 2.60/0.75 % (1491641)------------------------------
% 3.31/0.83 % (1491641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.83 % (1491641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.83 % (1491641)CaDiCaL version: 2.1.3
% 3.31/0.83 % (1491641)Termination reason: Instruction limit
% 3.31/0.83 % (1491641)Termination phase: shuffling
% 3.31/0.83 % (1491641)Time elapsed: 0.010 s
% 3.31/0.83 % (1491641)Peak memory usage: 10 MB
% 3.31/0.83 % (1491641)Instructions burned: 21 (million)
% 3.31/0.83 % (1491643)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=1583448951: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.31/0.83 % (1491640)Instruction limit reached!
% 3.31/0.83 % (1491640)------------------------------
% 3.31/0.83 % (1491640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.83 % (1491640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.83 % (1491640)CaDiCaL version: 2.1.3
% 3.31/0.83 % (1491640)Termination reason: Instruction limit
% 3.31/0.83 % (1491640)Termination phase: Property scanning
% 3.31/0.83 % (1491640)Time elapsed: 0.011 s
% 3.31/0.83 % (1491640)Peak memory usage: 10 MB
% 3.31/0.83 % (1491640)Instructions burned: 22 (million)
% 3.31/0.83 % (1491648)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=1220430521: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.31/0.83 % (1491649)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3904339296:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.31/0.83 % (1491633)Instruction limit reached!
% 3.31/0.83 % (1491633)------------------------------
% 3.31/0.83 % (1491633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.83 % (1491633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.83 % (1491633)CaDiCaL version: 2.1.3
% 3.31/0.83 % (1491633)Termination reason: Instruction limit
% 3.31/0.83 % (1491633)Termination phase: Saturation
% 3.31/0.83 % (1491633)Time elapsed: 0.093 s
% 3.31/0.83 % (1491633)Peak memory usage: 14 MB
% 3.31/0.83 % (1491633)Instructions burned: 181 (million)
% 3.31/0.83 % (1491648)Instruction limit reached!
% 3.31/0.83 % (1491648)------------------------------
% 3.31/0.83 % (1491648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.83 % (1491648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.83 % (1491635)Refutation not found, incomplete strategy
% 3.31/0.83 % (1491635)------------------------------
% 3.31/0.83 % (1491635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.83 % (1491635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.83 % (1491648)CaDiCaL version: 2.1.3
% 3.31/0.83 % (1491648)Termination reason: Instruction limit
% 3.31/0.83 % (1491648)Termination phase: Naming
% 3.31/0.83 % (1491635)CaDiCaL version: 2.1.3
% 3.31/0.83 % (1491648)Time elapsed: 0.022 s
% 3.31/0.83 % (1491635)Termination reason: Refutation not found, incomplete strategy
% 3.31/0.83 % (1491635)Time elapsed: 0.095 s
% 3.31/0.83 % (1491648)Peak memory usage: 11 MB
% 3.31/0.83 % (1491635)Peak memory usage: 14 MB
% 3.31/0.83 % (1491648)Instructions burned: 45 (million)
% 3.31/0.83 % (1491635)Instructions burned: 111 (million)
% 3.31/0.83 % (1491635)------------------------------
% 3.31/0.83 % (1491635)------------------------------
% 3.31/0.83 % (1491652)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3262721120: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.31/0.83 % (1491653)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.31/0.83 % (1491652)Instruction limit reached!
% 3.31/0.83 % (1491652)------------------------------
% 3.31/0.83 % (1491652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.83 % (1491652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.83 % (1491652)CaDiCaL version: 2.1.3
% 3.31/0.83 % (1491652)Termination reason: Instruction limit
% 3.31/0.83 % (1491652)Termination phase: Property scanning
% 3.85/0.93 % (1491652)Time elapsed: 0.010 s
% 3.85/0.93 % (1491652)Peak memory usage: 10 MB
% 3.85/0.93 % (1491652)Instructions burned: 21 (million)
% 3.85/0.93 % (1491653)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=4238723458:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.85/0.93 % (1491654)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1296933865:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.85/0.93 % (1491654)Instruction limit reached!
% 3.85/0.93 % (1491654)------------------------------
% 3.85/0.93 % (1491654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/0.93 % (1491654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/0.93 % (1491654)CaDiCaL version: 2.1.3
% 3.85/0.93 % (1491654)Termination reason: Instruction limit
% 3.85/0.93 % (1491654)Termination phase: shuffling
% 3.85/0.93 % (1491654)Time elapsed: 0.007 s
% 3.85/0.93 % (1491654)Peak memory usage: 10 MB
% 3.85/0.93 % (1491654)Instructions burned: 15 (million)
% 3.85/0.93 % (1491656)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=4251048803:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.85/0.93 % (1491659)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1965944168:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 3.85/0.93 % (1491656)Instruction limit reached!
% 3.85/0.93 % (1491656)------------------------------
% 3.85/0.93 % (1491656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/0.93 % (1491656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/0.93 % (1491656)CaDiCaL version: 2.1.3
% 3.85/0.93 % (1491656)Termination reason: Instruction limit
% 3.85/0.93 % (1491656)Termination phase: Preprocessing 1
% 3.85/0.93 % (1491656)Time elapsed: 0.030 s
% 3.85/0.93 % (1491656)Peak memory usage: 11 MB
% 3.85/0.93 % (1491656)Instructions burned: 67 (million)
% 3.85/0.93 % (1491659)Instruction limit reached!
% 3.85/0.93 % (1491659)------------------------------
% 3.85/0.93 % (1491659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/0.93 % (1491659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/0.93 % (1491659)CaDiCaL version: 2.1.3
% 3.85/0.93 % (1491659)Termination reason: Instruction limit
% 3.85/0.93 % (1491659)Termination phase: Property scanning
% 3.85/0.93 % (1491659)Time elapsed: 0.025 s
% 3.85/0.93 % (1491659)Peak memory usage: 11 MB
% 3.85/0.93 % (1491659)Instructions burned: 53 (million)
% 3.85/0.93 % (1491662)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3585850540:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 3.85/0.93 % (1491663)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=279740485:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.85/0.93 % (1491662)Instruction limit reached!
% 3.85/0.93 % (1491662)------------------------------
% 3.85/0.93 % (1491662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/0.93 % (1491662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/0.93 % (1491662)CaDiCaL version: 2.1.3
% 3.85/0.93 % (1491662)Termination reason: Instruction limit
% 3.85/0.93 % (1491662)Termination phase: Property scanning
% 3.85/0.93 % (1491662)Time elapsed: 0.014 s
% 3.85/0.93 % (1491662)Peak memory usage: 11 MB
% 3.85/0.93 % (1491662)Instructions burned: 31 (million)
% 3.85/0.93 % (1491653)Instruction limit reached!
% 3.85/0.93 % (1491653)------------------------------
% 3.85/0.93 % (1491653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/0.93 % (1491653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/0.93 % (1491653)CaDiCaL version: 2.1.3
% 3.85/0.93 % (1491653)Termination reason: Instruction limit
% 3.85/0.93 % (1491653)Termination phase: Saturation
% 3.85/0.93 % (1491653)Time elapsed: 0.088 s
% 3.85/0.93 % (1491653)Peak memory usage: 13 MB
% 3.85/0.93 % (1491653)Instructions burned: 200 (million)
% 3.85/0.93 % (1491666)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=896736437:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.85/1.00 % (1491642)Instruction limit reached!
% 3.85/1.00 % (1491642)------------------------------
% 3.85/1.00 % (1491642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491642)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491642)Termination reason: Instruction limit
% 3.85/1.00 % (1491642)Termination phase: Saturation
% 3.85/1.00 % (1491642)Time elapsed: 0.168 s
% 3.85/1.00 % (1491642)Peak memory usage: 17 MB
% 3.85/1.00 % (1491642)Instructions burned: 317 (million)
% 3.85/1.00 % (1491667)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2567953744:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.85/1.00 % (1491666)Instruction limit reached!
% 3.85/1.00 % (1491666)------------------------------
% 3.85/1.00 % (1491666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491666)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491666)Termination reason: Instruction limit
% 3.85/1.00 % (1491666)Termination phase: Property scanning
% 3.85/1.00 % (1491666)Time elapsed: 0.016 s
% 3.85/1.00 % (1491666)Peak memory usage: 10 MB
% 3.85/1.00 % (1491666)Instructions burned: 34 (million)
% 3.85/1.00 % (1491669)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.85/1.00 % (1491669)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1891647124:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 3.85/1.00 % (1491671)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2189370671:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 3.85/1.00 % (1491663)Instruction limit reached!
% 3.85/1.00 % (1491663)------------------------------
% 3.85/1.00 % (1491663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491663)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491663)Termination reason: Instruction limit
% 3.85/1.00 % (1491663)Termination phase: Saturation
% 3.85/1.00 % (1491663)Time elapsed: 0.067 s
% 3.85/1.00 % (1491663)Peak memory usage: 14 MB
% 3.85/1.00 % (1491663)Instructions burned: 138 (million)
% 3.85/1.00 % (1491667)Instruction limit reached!
% 3.85/1.00 % (1491667)------------------------------
% 3.85/1.00 % (1491667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491667)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491667)Termination reason: Instruction limit
% 3.85/1.00 % (1491667)Termination phase: Property scanning
% 3.85/1.00 % (1491667)Time elapsed: 0.032 s
% 3.85/1.00 % (1491667)Peak memory usage: 12 MB
% 3.85/1.00 % (1491667)Instructions burned: 70 (million)
% 3.85/1.00 % (1491674)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=2589080749:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 3.85/1.00 % (1491675)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1157403196:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 3.85/1.00 % (1491675)Refutation not found, incomplete strategy
% 3.85/1.00 % (1491675)------------------------------
% 3.85/1.00 % (1491675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491675)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491675)Termination reason: Refutation not found, incomplete strategy
% 3.85/1.00 % (1491675)Time elapsed: 0.017 s
% 3.85/1.00 % (1491675)Peak memory usage: 13 MB
% 3.85/1.00 % (1491675)Instructions burned: 33 (million)
% 3.85/1.00 % (1491621)Instruction limit reached!
% 3.85/1.00 % (1491621)------------------------------
% 3.85/1.00 % (1491621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491621)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491621)Termination reason: Instruction limit
% 3.85/1.00 % (1491621)Termination phase: Saturation
% 3.85/1.00 % (1491621)Time elapsed: 0.372 s
% 3.85/1.00 % (1491621)Peak memory usage: 17 MB
% 3.85/1.00 % (1491621)Instructions burned: 1240 (million)
% 3.85/1.00 % (1491675)------------------------------
% 3.85/1.00 % (1491675)------------------------------
% 3.85/1.00 % (1491679)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3459087490:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 3.85/1.00 % (1491678)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2034007432:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 3.85/1.00 % (1491649)Instruction limit reached!
% 3.85/1.00 % (1491649)------------------------------
% 3.85/1.00 % (1491649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491649)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491649)Termination reason: Instruction limit
% 3.85/1.00 % (1491649)Termination phase: Saturation
% 3.85/1.00 % (1491649)Time elapsed: 0.241 s
% 3.85/1.00 % (1491649)Peak memory usage: 15 MB
% 3.85/1.00 % (1491649)Instructions burned: 481 (million)
% 3.85/1.00 % (1491674)Instruction limit reached!
% 3.85/1.00 % (1491674)------------------------------
% 3.85/1.00 % (1491674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491674)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491674)Termination reason: Instruction limit
% 3.85/1.00 % (1491674)Termination phase: Saturation
% 3.85/1.00 % (1491674)Time elapsed: 0.045 s
% 3.85/1.00 % (1491674)Peak memory usage: 13 MB
% 3.85/1.00 % (1491674)Instructions burned: 98 (million)
% 3.85/1.00 % (1491669)Instruction limit reached!
% 3.85/1.00 % (1491669)------------------------------
% 3.85/1.00 % (1491669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491669)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491669)Termination reason: Instruction limit
% 3.85/1.00 % (1491669)Termination phase: Saturation
% 3.85/1.00 % (1491669)Time elapsed: 0.079 s
% 3.85/1.00 % (1491669)Peak memory usage: 13 MB
% 3.85/1.00 % (1491669)Instructions burned: 181 (million)
% 3.85/1.00 % (1491682)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3127110134:st=1.5:i=130:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/130Mi)
% 3.85/1.00 % (1491683)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=638081556:i=44:ep=R:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/44Mi)
% 3.85/1.00 % (1491684)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=444144582:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 3.85/1.00 % (1491683)Instruction limit reached!
% 3.85/1.00 % (1491683)------------------------------
% 3.85/1.00 % (1491683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491683)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491683)Termination reason: Instruction limit
% 3.85/1.00 % (1491683)Termination phase: Property scanning
% 3.85/1.00 % (1491683)Time elapsed: 0.019 s
% 3.85/1.00 % (1491683)Peak memory usage: 10 MB
% 3.85/1.00 % (1491683)Instructions burned: 44 (million)
% 3.85/1.00 % (1491688)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=1852104018:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 3.85/1.00 % (1491671)Instruction limit reached!
% 3.85/1.00 % (1491671)------------------------------
% 3.85/1.00 % (1491671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491671)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491671)Termination reason: Instruction limit
% 3.85/1.00 % (1491671)Termination phase: Saturation
% 3.85/1.00 % (1491671)Time elapsed: 0.127 s
% 3.85/1.00 % (1491671)Peak memory usage: 14 MB
% 3.85/1.00 % (1491671)Instructions burned: 247 (million)
% 3.85/1.00 % (1491682)Instruction limit reached!
% 3.85/1.00 % (1491682)------------------------------
% 3.85/1.00 % (1491682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491682)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491682)Termination reason: Instruction limit
% 3.85/1.00 % (1491682)Termination phase: Saturation
% 3.85/1.00 % (1491682)Time elapsed: 0.057 s
% 3.85/1.00 % (1491682)Peak memory usage: 14 MB
% 3.85/1.00 % (1491682)Instructions burned: 131 (million)
% 3.85/1.00 % (1491690)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=167320470:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 3.85/1.00 % (1491691)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=926946822:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 3.85/1.00 % (1491690)Instruction limit reached!
% 3.85/1.00 % (1491690)------------------------------
% 3.85/1.00 % (1491690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491690)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491690)Termination reason: Instruction limit
% 3.85/1.00 % (1491690)Termination phase: Saturation
% 3.85/1.00 % (1491690)Time elapsed: 0.044 s
% 3.85/1.00 % (1491690)Peak memory usage: 13 MB
% 3.85/1.00 % (1491690)Instructions burned: 95 (million)
% 3.85/1.00 % (1491691)Instruction limit reached!
% 3.85/1.00 % (1491691)------------------------------
% 3.85/1.00 % (1491691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491691)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491691)Termination reason: Instruction limit
% 3.85/1.00 % (1491691)Termination phase: Preprocessing 1
% 3.85/1.00 % (1491691)Time elapsed: 0.030 s
% 3.85/1.00 % (1491691)Peak memory usage: 11 MB
% 3.85/1.00 % (1491691)Instructions burned: 66 (million)
% 3.85/1.00 % (1491684) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1491557-1491684"...
% 3.85/1.00 % (1491684)...printing done.
% 3.85/1.00 % (1491684)Refutation found. Thanks to Tanya!
% 3.85/1.00 % SZS status Theorem for theBenchmark
% 3.85/1.00 % SZS output start Proof for theBenchmark
% 3.85/1.00 thf(type_def_5, type, binary1291135688e_Tree: $tType > $tType).
% 3.85/1.00 thf(type_def_6, type, set: $tType > $tType).
% 3.85/1.00 thf(type_def_7, type, int: $tType).
% 3.85/1.00 thf(type_def_8, type, a: $tType).
% 3.85/1.00 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 3.85/1.00 thf(func_def_0, type, bounded_lattice: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_1, type, type: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_2, type, minus: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_3, type, bot: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_4, type, ord: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_5, type, order: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_6, type, group_add: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_7, type, lattice: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_8, type, no_bot: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_9, type, no_top: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_10, type, linorder: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_11, type, preorder: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_12, type, order_bot: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_13, type, wellorder: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_14, type, dense_order: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_15, type, linordered_idom: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_16, type, linordered_field: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_17, type, semilattice_sup: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_18, type, ordered_ab_group_add: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_19, type, cancel146912293up_add: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_20, type, bounde1808546759up_bot: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_21, type, condit1656338222tinuum: !>[X0: $tType]:($o)).
% 3.85/1.00 thf(func_def_22, type, binary210054475elle_T: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > X0 > binary1291135688e_Tree @ X0 > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_23, type, binary1746293266le_Tip: !>[X0: $tType]:(binary1291135688e_Tree @ X0)).
% 3.85/1.00 thf(func_def_24, type, binary536355927e_Tree: !>[X0: $tType, X1: $tType]:((X0 > (binary1291135688e_Tree @ X1 > X1 > binary1291135688e_Tree @ X1 > X0) > binary1291135688e_Tree @ X1 > X0))).
% 3.85/1.00 thf(func_def_25, type, binary1693644968d_Tree: !>[X0: $tType]:(((X0 > $o) > binary1291135688e_Tree @ X0 > $o))).
% 3.85/1.00 thf(func_def_26, type, binary1929596613c_Tree: !>[X0: $tType, X1: $tType]:((X0 > (binary1291135688e_Tree @ X1 > X1 > binary1291135688e_Tree @ X1 > X0 > X0 > X0) > binary1291135688e_Tree @ X1 > X0))).
% 3.85/1.00 thf(func_def_27, type, binary2130109271t_Tree: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > set @ X0))).
% 3.85/1.00 thf(func_def_28, type, binary1830089824insert: !>[X0: $tType]:(((X0 > int) > X0 > binary1291135688e_Tree @ X0 > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_29, type, binary64540844le_eqs: !>[X0: $tType]:(((X0 > int) > X0 > set @ X0))).
% 3.85/1.00 thf(func_def_30, type, binary827270440e_memb: !>[X0: $tType]:(((X0 > int) > X0 > binary1291135688e_Tree @ X0 > $o))).
% 3.85/1.00 thf(func_def_31, type, binary1653327646_setOf: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > set @ X0))).
% 3.85/1.00 thf(func_def_32, type, binary1610619414edTree: !>[X0: $tType]:(((X0 > int) > binary1291135688e_Tree @ X0 > $o))).
% 3.85/1.00 thf(func_def_33, type, binary231205461t_pred: !>[X0: $tType]:(((X0 > int) > X0 > X0 > binary1291135688e_Tree @ X0 > $o))).
% 3.85/1.00 thf(func_def_34, type, minus_minus: !>[X0: $tType]:((X0 > X0 > X0))).
% 3.85/1.00 thf(func_def_35, type, the: !>[X0: $tType]:(((X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_36, type, sup_sup: !>[X0: $tType]:((X0 > X0 > X0))).
% 3.85/1.00 thf(func_def_37, type, bot_bot: !>[X0: $tType]:(X0)).
% 3.85/1.00 thf(func_def_38, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.85/1.00 thf(func_def_39, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.85/1.00 thf(func_def_40, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 3.85/1.00 thf(func_def_41, type, insert: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 3.85/1.00 thf(func_def_42, type, is_empty: !>[X0: $tType]:((set @ X0 > $o))).
% 3.85/1.00 thf(func_def_43, type, is_singleton: !>[X0: $tType]:((set @ X0 > $o))).
% 3.85/1.00 thf(func_def_44, type, remove: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 3.85/1.00 thf(func_def_45, type, the_elem: !>[X0: $tType]:((set @ X0 > X0))).
% 3.85/1.00 thf(func_def_46, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 3.85/1.00 thf(func_def_47, type, e: a).
% 3.85/1.00 thf(func_def_48, type, h: (a > int)).
% 3.85/1.00 thf(func_def_49, type, t1: binary1291135688e_Tree @ a).
% 3.85/1.00 thf(func_def_50, type, t2: binary1291135688e_Tree @ a).
% 3.85/1.00 thf(func_def_51, type, w: a).
% 3.85/1.00 thf(func_def_52, type, x: a).
% 3.85/1.00 thf(func_def_56, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.85/1.00 thf(func_def_57, type, db0: !>[X0: $tType]:(X0)).
% 3.85/1.00 thf(func_def_58, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.85/1.00 thf(func_def_59, type, db2: !>[X0: $tType]:(X0)).
% 3.85/1.00 thf(func_def_60, type, db1: !>[X0: $tType]:(X0)).
% 3.85/1.00 thf(func_def_61, type, vIMP: ($o > $o > $o)).
% 3.85/1.00 thf(func_def_62, type, vAND: ($o > $o > $o)).
% 3.85/1.00 thf(func_def_63, type, db3: !>[X0: $tType]:(X0)).
% 3.85/1.00 thf(func_def_64, type, vOR: ($o > $o > $o)).
% 3.85/1.00 thf(func_def_65, type, vNOT: ($o > $o)).
% 3.85/1.00 thf(func_def_66, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.85/1.00 thf(func_def_67, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.85/1.00 thf(func_def_68, type, sK0: !>[X0: $tType]:((set @ X0 > X0))).
% 3.85/1.00 thf(func_def_69, type, sK1: !>[X0: $tType, X1: $tType]:((((X0 > X1) > X0 > X1 > $o) > X0 > X1))).
% 3.85/1.00 thf(func_def_70, type, sK2: !>[X0: $tType, X1: $tType]:((((X0 > X1) > X0 > X1 > $o) > X1))).
% 3.85/1.00 thf(func_def_71, type, sK3: !>[X0: $tType, X1: $tType]:((((X0 > X1) > X0 > X1 > $o) > X0))).
% 3.85/1.00 thf(func_def_72, type, sK4: !>[X0: $tType, X1: $tType]:((((X0 > X1) > X0 > X1 > $o) > X0 > X1))).
% 3.85/1.00 thf(func_def_73, type, sK5: !>[X0: $tType, X1: $tType]:((((X0 > X1) > X0 > X1 > $o) > X0))).
% 3.85/1.00 thf(func_def_74, type, sK6: !>[X0: $tType, X1: $tType]:((((X0 > X1) > X0 > X1 > $o) > X0 > X1))).
% 3.85/1.00 thf(func_def_75, type, sK7: !>[X0: $tType, X1: $tType]:((((X0 > X1) > X0 > X1 > $o) > X0 > X1))).
% 3.85/1.00 thf(func_def_76, type, sK8: !>[X0: $tType]:((set @ X0 > X0))).
% 3.85/1.00 thf(func_def_77, type, sK9: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > binary1291135688e_Tree @ X0 > X0))).
% 3.85/1.00 thf(func_def_78, type, sK10: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 3.85/1.00 thf(func_def_79, type, sK11: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 3.85/1.00 thf(func_def_80, type, sK12: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_81, type, sK13: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_82, type, sK14: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_83, type, sK15: !>[X0: $tType]:((X0 > X0 > X0))).
% 3.85/1.00 thf(func_def_84, type, sK16: !>[X0: $tType]:(((X0 > $o) > set @ X0 > set @ X0 > X0))).
% 3.85/1.00 thf(func_def_85, type, sK17: !>[X0: $tType]:(((X0 > $o) > set @ X0 > X0))).
% 3.85/1.00 thf(func_def_86, type, sK18: !>[X0: $tType]:(((X0 > $o) > set @ X0 > X0))).
% 3.85/1.00 thf(func_def_87, type, sK19: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_88, type, sK20: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_89, type, sK21: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_90, type, sK22: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_91, type, sK23: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 3.85/1.00 thf(func_def_92, type, sK24: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 3.85/1.00 thf(func_def_93, type, sK25: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 3.85/1.00 thf(func_def_94, type, sK26: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 3.85/1.00 thf(func_def_95, type, sK27: !>[X0: $tType]:(((X0 > int) > X0 > binary1291135688e_Tree @ X0 > X0))).
% 3.85/1.00 thf(func_def_96, type, sK28: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > (X0 > int) > X0 > X0))).
% 3.85/1.00 thf(func_def_97, type, sK29: !>[X0: $tType]:(((X0 > $o) > set @ X0 > X0))).
% 3.85/1.00 thf(func_def_98, type, sK30: !>[X0: $tType]:(((X0 > $o) > set @ X0 > X0))).
% 3.85/1.00 thf(func_def_99, type, sK31: !>[X0: $tType]:(((X0 > $o) > set @ X0 > set @ X0 > X0))).
% 3.85/1.00 thf(func_def_100, type, sK32: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_101, type, sK33: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_102, type, sK34: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_103, type, sK35: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_104, type, sK36: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_105, type, sK37: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_106, type, sK38: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_107, type, sK39: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_108, type, sK40: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_109, type, sK41: !>[X0: $tType]:((X0 > X0 > set @ X0 > set @ X0 > set @ X0))).
% 3.85/1.00 thf(func_def_110, type, sK42: !>[X0: $tType]:((set @ X0 > X0))).
% 3.85/1.00 thf(func_def_111, type, sK43: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 3.85/1.00 thf(func_def_112, type, sK44: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_113, type, sK45: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_114, type, sK46: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_115, type, sK47: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_116, type, sK48: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_117, type, sK49: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > X0))).
% 3.85/1.00 thf(func_def_118, type, sK50: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_119, type, sK51: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_120, type, sK52: !>[X0: $tType]:(((X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_121, type, sK53: !>[X0: $tType]:((set @ X0 > set @ X0 > X0))).
% 3.85/1.00 thf(func_def_122, type, sK54: !>[X0: $tType, X1: $tType]:((X0 > X1))).
% 3.85/1.00 thf(func_def_123, type, sK55: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > X0 > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_124, type, sK56: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > X0 > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_125, type, sK57: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > X0 > X0))).
% 3.85/1.00 thf(func_def_126, type, sK58: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > X0 > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_127, type, sK59: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > X0 > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_128, type, sK60: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > X0 > X0))).
% 3.85/1.00 thf(func_def_129, type, sK61: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > X0 > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_130, type, sK62: !>[X0: $tType]:((binary1291135688e_Tree @ X0 > X0 > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_131, type, sK63: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_132, type, sK64: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 3.85/1.00 thf(func_def_133, type, sK65: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 3.85/1.00 thf(func_def_134, type, sK66: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_135, type, sK67: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_136, type, sK68: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_137, type, sK69: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_138, type, sK70: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_139, type, sK71: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > $o) > X1))).
% 3.85/1.00 thf(func_def_140, type, sK72: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_141, type, sK73: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_142, type, sK74: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 3.85/1.00 thf(func_def_143, type, sK75: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 3.85/1.00 thf(func_def_144, type, sK76: !>[X0: $tType]:((X0 > X0))).
% 3.85/1.00 thf(func_def_145, type, sK77: !>[X0: $tType, X1: $tType]:((X1 > X0))).
% 3.85/1.00 thf(func_def_146, type, sK78: !>[X0: $tType]:((set @ X0 > X0))).
% 3.85/1.00 thf(func_def_147, type, sK79: !>[X0: $tType]:((set @ X0 > X0))).
% 3.85/1.00 thf(func_def_148, type, sK80: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_149, type, sK81: !>[X0: $tType]:(((X0 > $o) > binary1291135688e_Tree @ X0 > (X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_150, type, sK82: !>[X0: $tType, X1: $tType]:(((X1 > $o) > (X1 > X0) > X1))).
% 3.85/1.00 thf(func_def_151, type, sK83: !>[X0: $tType]:(((X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_152, type, sK84: !>[X0: $tType]:(((X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_153, type, sK85: !>[X0: $tType]:(((binary1291135688e_Tree @ X0 > $o) > X0))).
% 3.85/1.00 thf(func_def_154, type, sK86: !>[X0: $tType]:(((binary1291135688e_Tree @ X0 > $o) > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_155, type, sK87: !>[X0: $tType]:(((binary1291135688e_Tree @ X0 > $o) > binary1291135688e_Tree @ X0))).
% 3.85/1.00 thf(func_def_156, type, sK88: !>[X0: $tType]:((set @ X0 > X0))).
% 3.85/1.00 thf(f1,axiom,(
% 3.85/1.00 (member @ a @ w @ (binary1653327646_setOf @ a @ t1))),
% 3.85/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_whSet)).
% 3.85/1.00 thf(f2,axiom,(
% 3.85/1.00 (binary1610619414edTree @ a @ h @ (binary210054475elle_T @ a @ t1 @ x @ t2))),
% 3.85/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_s)).
% 3.85/1.00 thf(f22,axiom,(
% 3.85/1.00 ! [X0 : $tType,X2 : binary1291135688e_Tree @ X0,X1 : (X0 > int),X4 : binary1291135688e_Tree @ X0,X3 : X0] : (((binary1610619414edTree @ X0 @ X1 @ (binary210054475elle_T @ X0 @ X2 @ X3 @ X4))) = ! [X5 : X0] : ((member @ X0 @ X5 @ (binary1653327646_setOf @ X0 @ X2)) => (ord_less @ int @ (X1 @ X5) @ (X1 @ X3))) & (binary1610619414edTree @ X0 @ X1 @ X2) & ! [X5 : X0] : ((member @ X0 @ X5 @ (binary1653327646_setOf @ X0 @ X4)) => (ord_less @ int @ (X1 @ X3) @ (X1 @ X5))) & (binary1610619414edTree @ X0 @ X1 @ X4))),
% 3.85/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_21_sortedTree_Osimps_I2_J)).
% 3.85/1.00 thf(f301,conjecture,(
% 3.85/1.00 (ord_less @ int @ (h @ w) @ (h @ x))),
% 3.85/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 3.85/1.00 thf(f302,negated_conjecture,(
% 3.85/1.00 ~(ord_less @ int @ (h @ w) @ (h @ x))),
% 3.85/1.00 inference(negated_conjecture,[status(cth)],[f301])).
% 3.85/1.00 thf(f309,plain,(
% 3.85/1.00 (binary1610619414edTree @ a @ h @ (binary210054475elle_T @ a @ t1 @ x @ t2))),
% 3.85/1.00 inference(rectify,[],[f2])).
% 3.85/1.00 thf(f310,plain,(
% 3.85/1.00 (((binary1610619414edTree @ a @ h @ (binary210054475elle_T @ a @ t1 @ x @ t2))) = $true)),
% 3.85/1.00 inference(fool_elimination,[],[f309])).
% 3.85/1.00 thf(f388,plain,(
% 3.85/1.00 ~(ord_less @ int @ (h @ w) @ (h @ x))),
% 3.85/1.00 inference(rectify,[],[f302])).
% 3.85/1.00 thf(f389,plain,(
% 3.85/1.00 ~ (((ord_less @ int @ (h @ w) @ (h @ x))) = $true)),
% 3.85/1.00 inference(fool_elimination,[],[f388])).
% 3.85/1.00 thf(f432,plain,(
% 3.85/1.00 (member @ a @ w @ (binary1653327646_setOf @ a @ t1))),
% 3.85/1.00 inference(rectify,[],[f1])).
% 3.85/1.00 thf(f433,plain,(
% 3.85/1.00 (((member @ a @ w @ (binary1653327646_setOf @ a @ t1))) = $true)),
% 3.85/1.00 inference(fool_elimination,[],[f432])).
% 3.85/1.00 thf(f781,plain,(
% 3.85/1.00 ! [X0 : $tType,X1 : binary1291135688e_Tree @ X0,X2 : (X0 > int),X3 : binary1291135688e_Tree @ X0,X4 : X0] : (((binary1610619414edTree @ X0 @ X2 @ (binary210054475elle_T @ X0 @ X1 @ X4 @ X3))) = ! [X5 : X0] : ((member @ X0 @ X5 @ (binary1653327646_setOf @ X0 @ X1)) => (ord_less @ int @ (X2 @ X5) @ (X2 @ X4))) & (binary1610619414edTree @ X0 @ X2 @ X1) & ! [X6 : X0] : ((member @ X0 @ X6 @ (binary1653327646_setOf @ X0 @ X3)) => (ord_less @ int @ (X2 @ X4) @ (X2 @ X6))) & (binary1610619414edTree @ X0 @ X2 @ X3))),
% 3.85/1.00 inference(rectify,[],[f22])).
% 3.85/1.00 thf(f782,plain,(
% 3.85/1.00 ! [X0 : $tType,X2 : (X0 > int),X3 : binary1291135688e_Tree @ X0,X4 : X0,X1 : binary1291135688e_Tree @ X0] : ((! [X6 : X0] : (($true = ((member @ X0 @ X6 @ (binary1653327646_setOf @ X0 @ X3)))) => (((ord_less @ int @ (X2 @ X4) @ (X2 @ X6))) = $true)) & ($true = ((binary1610619414edTree @ X0 @ X2 @ X3))) & ! [X5 : X0] : (($true = ((member @ X0 @ X5 @ (binary1653327646_setOf @ X0 @ X1)))) => (((ord_less @ int @ (X2 @ X5) @ (X2 @ X4))) = $true)) & (((binary1610619414edTree @ X0 @ X2 @ X1)) = $true)) <=> (((binary1610619414edTree @ X0 @ X2 @ (binary210054475elle_T @ X0 @ X1 @ X4 @ X3))) = $true))),
% 3.85/1.00 inference(fool_elimination,[],[f781])).
% 3.85/1.00 thf(f824,plain,(
% 3.85/1.00 (((ord_less @ int @ (h @ w) @ (h @ x))) != $true)),
% 3.85/1.00 inference(flattening,[],[f389])).
% 3.85/1.00 thf(f1023,plain,(
% 3.85/1.00 ! [X0 : $tType,X3 : binary1291135688e_Tree @ X0,X4 : X0,X2 : (X0 > int),X1 : binary1291135688e_Tree @ X0] : ((! [X6 : X0] : (($true != ((member @ X0 @ X6 @ (binary1653327646_setOf @ X0 @ X3)))) | (((ord_less @ int @ (X2 @ X4) @ (X2 @ X6))) = $true)) & ! [X5 : X0] : (($true != ((member @ X0 @ X5 @ (binary1653327646_setOf @ X0 @ X1)))) | (((ord_less @ int @ (X2 @ X5) @ (X2 @ X4))) = $true)) & (((binary1610619414edTree @ X0 @ X2 @ X1)) = $true) & ($true = ((binary1610619414edTree @ X0 @ X2 @ X3)))) <=> (((binary1610619414edTree @ X0 @ X2 @ (binary210054475elle_T @ X0 @ X1 @ X4 @ X3))) = $true))),
% 3.85/1.00 inference(ennf_transformation,[],[f782])).
% 3.85/1.00 thf(f1152,plain,(
% 3.85/1.00 ! [X0 : $tType,X3 : binary1291135688e_Tree @ X0,X4 : X0,X2 : (X0 > int),X1 : binary1291135688e_Tree @ X0] : (((! [X6 : X0] : (($true != ((member @ X0 @ X6 @ (binary1653327646_setOf @ X0 @ X3)))) | (((ord_less @ int @ (X2 @ X4) @ (X2 @ X6))) = $true)) & ! [X5 : X0] : (($true != ((member @ X0 @ X5 @ (binary1653327646_setOf @ X0 @ X1)))) | (((ord_less @ int @ (X2 @ X5) @ (X2 @ X4))) = $true)) & (((binary1610619414edTree @ X0 @ X2 @ X1)) = $true) & ($true = ((binary1610619414edTree @ X0 @ X2 @ X3)))) | (((binary1610619414edTree @ X0 @ X2 @ (binary210054475elle_T @ X0 @ X1 @ X4 @ X3))) != $true)) & ((((binary1610619414edTree @ X0 @ X2 @ (binary210054475elle_T @ X0 @ X1 @ X4 @ X3))) = $true) | (? [X6 : X0] : (($true = ((member @ X0 @ X6 @ (binary1653327646_setOf @ X0 @ X3)))) & (((ord_less @ int @ (X2 @ X4) @ (X2 @ X6))) != $true)) | ? [X5 : X0] : (($true = ((member @ X0 @ X5 @ (binary1653327646_setOf @ X0 @ X1)))) & (((ord_less @ int @ (X2 @ X5) @ (X2 @ X4))) != $true)) | (((binary1610619414edTree @ X0 @ X2 @ X1)) != $true) | ($true != ((binary1610619414edTree @ X0 @ X2 @ X3))))))),
% 3.85/1.00 inference(nnf_transformation,[],[f1023])).
% 3.85/1.00 thf(f1153,plain,(
% 3.85/1.00 ! [X0 : $tType,X3 : binary1291135688e_Tree @ X0,X4 : X0,X2 : (X0 > int),X1 : binary1291135688e_Tree @ X0] : (((! [X6 : X0] : (($true != ((member @ X0 @ X6 @ (binary1653327646_setOf @ X0 @ X3)))) | (((ord_less @ int @ (X2 @ X4) @ (X2 @ X6))) = $true)) & ! [X5 : X0] : (($true != ((member @ X0 @ X5 @ (binary1653327646_setOf @ X0 @ X1)))) | (((ord_less @ int @ (X2 @ X5) @ (X2 @ X4))) = $true)) & (((binary1610619414edTree @ X0 @ X2 @ X1)) = $true) & ($true = ((binary1610619414edTree @ X0 @ X2 @ X3)))) | (((binary1610619414edTree @ X0 @ X2 @ (binary210054475elle_T @ X0 @ X1 @ X4 @ X3))) != $true)) & ((((binary1610619414edTree @ X0 @ X2 @ (binary210054475elle_T @ X0 @ X1 @ X4 @ X3))) = $true) | ? [X6 : X0] : (($true = ((member @ X0 @ X6 @ (binary1653327646_setOf @ X0 @ X3)))) & (((ord_less @ int @ (X2 @ X4) @ (X2 @ X6))) != $true)) | ? [X5 : X0] : (($true = ((member @ X0 @ X5 @ (binary1653327646_setOf @ X0 @ X1)))) & (((ord_less @ int @ (X2 @ X5) @ (X2 @ X4))) != $true)) | (((binary1610619414edTree @ X0 @ X2 @ X1)) != $true) | ($true != ((binary1610619414edTree @ X0 @ X2 @ X3)))))),
% 3.85/1.00 inference(flattening,[],[f1152])).
% 3.85/1.00 thf(f1154,plain,(
% 3.85/1.00 ! [X0 : $tType,X1 : binary1291135688e_Tree @ X0,X2 : X0,X3 : (X0 > int),X4 : binary1291135688e_Tree @ X0] : (((! [X5 : X0] : (($true != ((member @ X0 @ X5 @ (binary1653327646_setOf @ X0 @ X1)))) | ($true = ((ord_less @ int @ (X3 @ X2) @ (X3 @ X5))))) & ! [X6 : X0] : ((((member @ X0 @ X6 @ (binary1653327646_setOf @ X0 @ X4))) != $true) | (((ord_less @ int @ (X3 @ X6) @ (X3 @ X2))) = $true)) & (((binary1610619414edTree @ X0 @ X3 @ X4)) = $true) & (((binary1610619414edTree @ X0 @ X3 @ X1)) = $true)) | (((binary1610619414edTree @ X0 @ X3 @ (binary210054475elle_T @ X0 @ X4 @ X2 @ X1))) != $true)) & ((((binary1610619414edTree @ X0 @ X3 @ (binary210054475elle_T @ X0 @ X4 @ X2 @ X1))) = $true) | ? [X7 : X0] : (($true = ((member @ X0 @ X7 @ (binary1653327646_setOf @ X0 @ X1)))) & ($true != ((ord_less @ int @ (X3 @ X2) @ (X3 @ X7))))) | ? [X8 : X0] : ((((member @ X0 @ X8 @ (binary1653327646_setOf @ X0 @ X4))) = $true) & (((ord_less @ int @ (X3 @ X8) @ (X3 @ X2))) != $true)) | (((binary1610619414edTree @ X0 @ X3 @ X4)) != $true) | (((binary1610619414edTree @ X0 @ X3 @ X1)) != $true)))),
% 3.85/1.00 inference(rectify,[],[f1153])).
% 3.85/1.00 thf(f1155,plain,(
% 3.85/1.00 ! [X0 : $tType,X1 : binary1291135688e_Tree @ X0,X2 : X0,X3 : (X0 > int),X4 : binary1291135688e_Tree @ X0] : (((! [X5 : X0] : (($true != ((member @ X0 @ X5 @ (binary1653327646_setOf @ X0 @ X1)))) | ($true = ((ord_less @ int @ (X3 @ X2) @ (X3 @ X5))))) & ! [X6 : X0] : ((((member @ X0 @ X6 @ (binary1653327646_setOf @ X0 @ X4))) != $true) | (((ord_less @ int @ (X3 @ X6) @ (X3 @ X2))) = $true)) & (((binary1610619414edTree @ X0 @ X3 @ X4)) = $true) & (((binary1610619414edTree @ X0 @ X3 @ X1)) = $true)) | (((binary1610619414edTree @ X0 @ X3 @ (binary210054475elle_T @ X0 @ X4 @ X2 @ X1))) != $true)) & ((((binary1610619414edTree @ X0 @ X3 @ (binary210054475elle_T @ X0 @ X4 @ X2 @ X1))) = $true) | (($true = ((member @ X0 @ (sK27 @ X0 @ X3 @ X2 @ X1) @ (binary1653327646_setOf @ X0 @ X1)))) & (((ord_less @ int @ (X3 @ X2) @ (X3 @ (sK27 @ X0 @ X3 @ X2 @ X1)))) != $true)) | (($true = ((member @ X0 @ (sK28 @ X0 @ X4 @ X3 @ X2) @ (binary1653327646_setOf @ X0 @ X4)))) & (((ord_less @ int @ (X3 @ (sK28 @ X0 @ X4 @ X3 @ X2)) @ (X3 @ X2))) != $true)) | (((binary1610619414edTree @ X0 @ X3 @ X4)) != $true) | (((binary1610619414edTree @ X0 @ X3 @ X1)) != $true)))),
% 3.85/1.00 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X2,sK0 @ X0 @ X1),skolemize(X2,sK0 @ X0 @ X1)],[f1154])).
% 3.85/1.00 thf(f1405,plain,(
% 3.85/1.00 (((binary1610619414edTree @ a @ h @ (binary210054475elle_T @ a @ t1 @ x @ t2))) = $true)),
% 3.85/1.00 inference(cnf_transformation,[],[f310])).
% 3.85/1.00 thf(f1486,plain,(
% 3.85/1.00 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > int),X1 : binary1291135688e_Tree @ X0,X6 : X0,X4 : binary1291135688e_Tree @ X0] : ((((binary1610619414edTree @ X0 @ X3 @ (binary210054475elle_T @ X0 @ X4 @ X2 @ X1))) != $true) | (((ord_less @ int @ (X3 @ X6) @ (X3 @ X2))) = $true) | (((member @ X0 @ X6 @ (binary1653327646_setOf @ X0 @ X4))) != $true)) )),
% 3.85/1.00 inference(cnf_transformation,[],[f1155])).
% 3.85/1.00 thf(f1700,plain,(
% 3.85/1.00 (((member @ a @ w @ (binary1653327646_setOf @ a @ t1))) = $true)),
% 3.85/1.00 inference(cnf_transformation,[],[f433])).
% 3.85/1.00 thf(f1764,plain,(
% 3.85/1.00 (((ord_less @ int @ (h @ w) @ (h @ x))) != $true)),
% 3.85/1.00 inference(cnf_transformation,[],[f824])).
% 3.85/1.00 thf(f1918,plain,(
% 3.85/1.00 $false),
% 3.85/1.00 inference(unit_resulting_resolution,[],[f1486,f1700,f1405,f1764])).
% 3.85/1.00 % SZS output end Proof for theBenchmark
% 3.85/1.00 % (1491684)------------------------------
% 3.85/1.00 % (1491684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.85/1.00 % (1491684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.00 % (1491684)CaDiCaL version: 2.1.3
% 3.85/1.00 % (1491684)Termination reason: Refutation
% 3.85/1.00 % (1491684)Time elapsed: 0.120 s
% 3.85/1.00 % (1491684)Peak memory usage: 15 MB
% 3.85/1.00 % (1491684)Instructions burned: 241 (million)
% 3.85/1.00 % (1491557)Success in time 0.748 s
% 3.85/1.00 % Vampire exiting
%------------------------------------------------------------------------------