%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP137^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:08:30 AM UTC 2026
% Result : Theorem 8.60s 1.67s
% Output : Refutation 8.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP137^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.16 % Computer : n026.cluster.edu
% 0.08/0.16 % Model : x86_64 x86_64
% 0.08/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.16 % Memory : 8046.5625MB
% 0.08/0.16 % OS : Linux 6.8.0-71-generic
% 0.08/0.16 % CPULimit : 300
% 0.08/0.16 % WCLimit : 300
% 0.08/0.16 % DateTime : Tue Sep 29 20:01:42 UTC 2026
% 0.08/0.16 % CPUTime :
% 0.08/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 Running higher-order theorem proving
% 0.22/0.26 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.60/0.40 % (1107049)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.60/0.40 % (1107054)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1884213272:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.60/0.40 % (1107060)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.60/0.40 % (1107060)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.60/0.40 % (1107055)lrs+10_16_si=on:nwc=1.5:random_seed=266998319:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.60/0.40 % (1107056)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1232888804:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.60/0.40 % (1107057)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=1605464139: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.60/0.40 % (1107058)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2984542921:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.60/0.40 % (1107060)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=3600135212:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.60/0.40 % (1107059)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=804860313:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.60/0.40 % (1107056)Instruction limit reached!
% 0.60/0.40 % (1107056)------------------------------
% 0.60/0.40 % (1107056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.40 % (1107056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.40 % (1107056)CaDiCaL version: 2.1.3
% 0.60/0.40 % (1107056)Termination reason: Instruction limit
% 0.60/0.40 % (1107056)Termination phase: shuffling
% 0.60/0.40 % (1107056)Time elapsed: 0.003 s
% 0.60/0.40 % (1107056)Peak memory usage: 10 MB
% 0.60/0.40 % (1107056)Instructions burned: 5 (million)
% 0.60/0.40 % (1107058)Instruction limit reached!
% 0.60/0.40 % (1107058)------------------------------
% 0.60/0.40 % (1107058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.40 % (1107058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.40 % (1107058)CaDiCaL version: 2.1.3
% 0.60/0.40 % (1107058)Termination reason: Instruction limit
% 0.60/0.40 % (1107058)Termination phase: Property scanning
% 0.60/0.40 % (1107058)Time elapsed: 0.011 s
% 0.60/0.40 % (1107058)Peak memory usage: 11 MB
% 0.60/0.40 % (1107058)Instructions burned: 24 (million)
% 0.60/0.40 % (1107055)Instruction limit reached!
% 0.60/0.40 % (1107055)------------------------------
% 0.60/0.40 % (1107055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.40 % (1107055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.40 % (1107055)CaDiCaL version: 2.1.3
% 0.60/0.40 % (1107055)Termination reason: Instruction limit
% 0.60/0.40 % (1107055)Termination phase: Property scanning
% 0.60/0.40 % (1107055)Time elapsed: 0.012 s
% 0.60/0.40 % (1107055)Peak memory usage: 11 MB
% 0.60/0.40 % (1107055)Instructions burned: 26 (million)
% 0.60/0.40 % (1107054)Instruction limit reached!
% 0.60/0.40 % (1107054)------------------------------
% 0.60/0.40 % (1107054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.40 % (1107054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.40 % (1107054)CaDiCaL version: 2.1.3
% 0.60/0.40 % (1107054)Termination reason: Instruction limit
% 0.60/0.40 % (1107054)Termination phase: Property scanning
% 0.60/0.40 % (1107054)Time elapsed: 0.023 s
% 0.60/0.40 % (1107054)Peak memory usage: 12 MB
% 0.60/0.40 % (1107054)Instructions burned: 90 (million)
% 0.60/0.40 % (1107068)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3802088856:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.60/0.40 % (1107071)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3739602243:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.60/0.44 % (1107068)Instruction limit reached!
% 0.60/0.44 % (1107068)------------------------------
% 0.60/0.44 % (1107068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.44 % (1107068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.44 % (1107068)CaDiCaL version: 2.1.3
% 0.60/0.44 % (1107068)Termination reason: Instruction limit
% 0.60/0.44 % (1107068)Termination phase: shuffling
% 0.60/0.44 % (1107068)Time elapsed: 0.002 s
% 0.60/0.44 % (1107068)Peak memory usage: 10 MB
% 0.60/0.44 % (1107068)Instructions burned: 2 (million)
% 0.60/0.44 % (1107070)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.60/0.44 % (1107071)Instruction limit reached!
% 0.60/0.44 % (1107071)------------------------------
% 0.60/0.44 % (1107071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.44 % (1107071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.44 % (1107071)CaDiCaL version: 2.1.3
% 0.60/0.44 % (1107071)Termination reason: Instruction limit
% 0.60/0.44 % (1107071)Termination phase: shuffling
% 0.60/0.44 % (1107071)Time elapsed: 0.003 s
% 0.60/0.44 % (1107071)Peak memory usage: 10 MB
% 0.60/0.44 % (1107071)Instructions burned: 12 (million)
% 0.60/0.44 % (1107069)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3701128541:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.60/0.44 % (1107070)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1156558910:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.60/0.44 % (1107069)Instruction limit reached!
% 0.60/0.44 % (1107069)------------------------------
% 0.60/0.44 % (1107069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.44 % (1107069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.44 % (1107069)CaDiCaL version: 2.1.3
% 0.60/0.44 % (1107069)Termination reason: Instruction limit
% 0.60/0.44 % (1107069)Termination phase: shuffling
% 0.60/0.44 % (1107069)Time elapsed: 0.003 s
% 0.60/0.44 % (1107069)Peak memory usage: 10 MB
% 0.60/0.44 % (1107069)Instructions burned: 5 (million)
% 0.60/0.44 % (1107070)Instruction limit reached!
% 0.60/0.44 % (1107070)------------------------------
% 0.60/0.44 % (1107070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.44 % (1107070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.44 % (1107070)CaDiCaL version: 2.1.3
% 0.60/0.44 % (1107070)Termination reason: Instruction limit
% 0.60/0.44 % (1107070)Termination phase: shuffling
% 0.60/0.44 % (1107070)Time elapsed: 0.004 s
% 0.60/0.44 % (1107070)Peak memory usage: 10 MB
% 0.60/0.44 % (1107070)Instructions burned: 8 (million)
% 0.60/0.44 % (1107059)Instruction limit reached!
% 0.60/0.44 % (1107059)------------------------------
% 0.60/0.44 % (1107059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.44 % (1107059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.44 % (1107059)CaDiCaL version: 2.1.3
% 0.60/0.44 % (1107059)Termination reason: Instruction limit
% 0.60/0.44 % (1107059)Termination phase: Property scanning
% 0.60/0.44 % (1107059)Time elapsed: 0.036 s
% 0.60/0.44 % (1107059)Peak memory usage: 12 MB
% 0.60/0.44 % (1107059)Instructions burned: 75 (million)
% 0.60/0.44 % (1107075)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=3721591806:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.60/0.44 % (1107074)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.60/0.44 % (1107074)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.60/0.44 % (1107074)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=4110127671: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.60/0.44 % (1107079)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.30/0.47 % (1107078)lrs+10_1_si=on:cs=on:random_seed=3717676798:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.30/0.47 % (1107079)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=661414646:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.30/0.47 % (1107080)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1790278766:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 1.30/0.47 % (1107078)Instruction limit reached!
% 1.30/0.47 % (1107078)------------------------------
% 1.30/0.47 % (1107078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.47 % (1107078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.47 % (1107078)CaDiCaL version: 2.1.3
% 1.30/0.47 % (1107078)Termination reason: Instruction limit
% 1.30/0.47 % (1107078)Termination phase: shuffling
% 1.30/0.47 % (1107078)Time elapsed: 0.004 s
% 1.30/0.47 % (1107078)Peak memory usage: 10 MB
% 1.30/0.47 % (1107078)Instructions burned: 8 (million)
% 1.30/0.47 % (1107079)Instruction limit reached!
% 1.30/0.47 % (1107079)------------------------------
% 1.30/0.47 % (1107079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.47 % (1107079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.47 % (1107079)CaDiCaL version: 2.1.3
% 1.30/0.47 % (1107079)Termination reason: Instruction limit
% 1.30/0.47 % (1107079)Termination phase: shuffling
% 1.30/0.47 % (1107079)Time elapsed: 0.002 s
% 1.30/0.47 % (1107079)Peak memory usage: 10 MB
% 1.30/0.47 % (1107079)Instructions burned: 3 (million)
% 1.30/0.47 % (1107074)Instruction limit reached!
% 1.30/0.47 % (1107074)------------------------------
% 1.30/0.47 % (1107074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.47 % (1107074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.47 % (1107074)CaDiCaL version: 2.1.3
% 1.30/0.47 % (1107074)Termination reason: Instruction limit
% 1.30/0.47 % (1107074)Termination phase: shuffling
% 1.30/0.47 % (1107074)Time elapsed: 0.013 s
% 1.30/0.47 % (1107074)Peak memory usage: 11 MB
% 1.30/0.47 % (1107074)Instructions burned: 28 (million)
% 1.30/0.47 % (1107075)Instruction limit reached!
% 1.30/0.47 % (1107075)------------------------------
% 1.30/0.47 % (1107075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.47 % (1107075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.47 % (1107075)CaDiCaL version: 2.1.3
% 1.30/0.47 % (1107075)Termination reason: Instruction limit
% 1.30/0.47 % (1107075)Termination phase: Property scanning
% 1.30/0.47 % (1107075)Time elapsed: 0.020 s
% 1.30/0.47 % (1107075)Peak memory usage: 12 MB
% 1.30/0.47 % (1107075)Instructions burned: 88 (million)
% 1.30/0.47 % (1107089)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1422077867:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.30/0.47 % (1107060)Instruction limit reached!
% 1.30/0.47 % (1107060)------------------------------
% 1.30/0.47 % (1107060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.47 % (1107060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.47 % (1107060)CaDiCaL version: 2.1.3
% 1.30/0.47 % (1107060)Termination reason: Instruction limit
% 1.30/0.47 % (1107060)Termination phase: Saturation
% 1.30/0.47 % (1107060)Time elapsed: 0.073 s
% 1.30/0.47 % (1107060)Peak memory usage: 14 MB
% 1.30/0.47 % (1107060)Instructions burned: 157 (million)
% 1.30/0.47 % (1107080)Instruction limit reached!
% 1.30/0.47 % (1107080)------------------------------
% 1.30/0.47 % (1107080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.47 % (1107080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.47 % (1107080)CaDiCaL version: 2.1.3
% 1.30/0.47 % (1107080)Termination reason: Instruction limit
% 1.30/0.47 % (1107080)Termination phase: Saturation
% 1.30/0.47 % (1107080)Time elapsed: 0.018 s
% 1.30/0.47 % (1107080)Peak memory usage: 12 MB
% 1.30/0.47 % (1107080)Instructions burned: 39 (million)
% 1.30/0.47 % (1107086)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=376716306:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.30/0.47 % (1107087)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3470337307:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.30/0.50 % (1107088)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2441019213:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.30/0.50 % (1107088)Instruction limit reached!
% 1.30/0.50 % (1107088)------------------------------
% 1.30/0.50 % (1107088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.50 % (1107088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.50 % (1107088)CaDiCaL version: 2.1.3
% 1.30/0.50 % (1107088)Termination reason: Instruction limit
% 1.30/0.50 % (1107088)Termination phase: shuffling
% 1.30/0.50 % (1107088)Time elapsed: 0.008 s
% 1.30/0.50 % (1107088)Peak memory usage: 10 MB
% 1.30/0.50 % (1107088)Instructions burned: 16 (million)
% 1.30/0.50 % (1107087)Instruction limit reached!
% 1.30/0.50 % (1107087)------------------------------
% 1.30/0.50 % (1107087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.50 % (1107087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.50 % (1107087)CaDiCaL version: 2.1.3
% 1.30/0.50 % (1107087)Termination reason: Instruction limit
% 1.30/0.50 % (1107087)Termination phase: Property scanning
% 1.30/0.50 % (1107087)Time elapsed: 0.011 s
% 1.30/0.50 % (1107087)Peak memory usage: 11 MB
% 1.30/0.50 % (1107087)Instructions burned: 25 (million)
% 1.30/0.50 % (1107091)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2603059998:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.30/0.50 % (1107092)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3020279730: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.30/0.50 % (1107092)Instruction limit reached!
% 1.30/0.50 % (1107092)------------------------------
% 1.30/0.50 % (1107092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.50 % (1107092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.50 % (1107092)CaDiCaL version: 2.1.3
% 1.30/0.50 % (1107092)Termination reason: Instruction limit
% 1.30/0.50 % (1107092)Termination phase: shuffling
% 1.30/0.50 % (1107092)Time elapsed: 0.002 s
% 1.30/0.50 % (1107092)Peak memory usage: 10 MB
% 1.30/0.50 % (1107092)Instructions burned: 3 (million)
% 1.30/0.50 % (1107091)Instruction limit reached!
% 1.30/0.50 % (1107091)------------------------------
% 1.30/0.50 % (1107091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.50 % (1107091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.50 % (1107091)CaDiCaL version: 2.1.3
% 1.30/0.50 % (1107091)Termination reason: Instruction limit
% 1.30/0.50 % (1107091)Termination phase: shuffling
% 1.30/0.50 % (1107091)Time elapsed: 0.007 s
% 1.30/0.50 % (1107091)Peak memory usage: 10 MB
% 1.30/0.50 % (1107091)Instructions burned: 15 (million)
% 1.30/0.50 % (1107086)Refutation not found, incomplete strategy
% 1.30/0.50 % (1107086)------------------------------
% 1.30/0.50 % (1107086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.50 % (1107086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.50 % (1107086)CaDiCaL version: 2.1.3
% 1.30/0.50 % (1107086)Termination reason: Refutation not found, incomplete strategy
% 1.30/0.50 % (1107086)Time elapsed: 0.024 s
% 1.30/0.50 % (1107086)Peak memory usage: 13 MB
% 1.30/0.50 % (1107086)Instructions burned: 50 (million)
% 1.30/0.50 % (1107086)------------------------------
% 1.30/0.50 % (1107086)------------------------------
% 1.30/0.50 % (1107096)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=838531196:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.30/0.50 % (1107097)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2643083425:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.30/0.50 % (1107101)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.30/0.50 % (1107101)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.30/0.50 % (1107100)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2730719951:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 2.01/0.58 % (1107096)Instruction limit reached!
% 2.01/0.58 % (1107096)------------------------------
% 2.01/0.58 % (1107096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.58 % (1107096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.58 % (1107096)CaDiCaL version: 2.1.3
% 2.01/0.58 % (1107096)Termination reason: Instruction limit
% 2.01/0.58 % (1107096)Termination phase: shuffling
% 2.01/0.58 % (1107096)Time elapsed: 0.012 s
% 2.01/0.58 % (1107096)Peak memory usage: 11 MB
% 2.01/0.58 % (1107096)Instructions burned: 26 (million)
% 2.01/0.58 % (1107102)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.01/0.58 % (1107101)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=1133784507:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.01/0.58 % (1107102)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=3195495116:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.01/0.58 % (1107097)Instruction limit reached!
% 2.01/0.58 % (1107097)------------------------------
% 2.01/0.58 % (1107097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.58 % (1107097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.58 % (1107097)CaDiCaL version: 2.1.3
% 2.01/0.58 % (1107097)Termination reason: Instruction limit
% 2.01/0.58 % (1107097)Termination phase: Property scanning
% 2.01/0.58 % (1107097)Time elapsed: 0.013 s
% 2.01/0.58 % (1107097)Peak memory usage: 11 MB
% 2.01/0.58 % (1107097)Instructions burned: 30 (million)
% 2.01/0.58 % (1107101)Instruction limit reached!
% 2.01/0.58 % (1107101)------------------------------
% 2.01/0.58 % (1107101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.58 % (1107101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.58 % (1107101)CaDiCaL version: 2.1.3
% 2.01/0.58 % (1107101)Termination reason: Instruction limit
% 2.01/0.58 % (1107101)Termination phase: shuffling
% 2.01/0.58 % (1107101)Time elapsed: 0.007 s
% 2.01/0.58 % (1107101)Peak memory usage: 10 MB
% 2.01/0.58 % (1107101)Instructions burned: 14 (million)
% 2.01/0.58 % (1107102)Instruction limit reached!
% 2.01/0.58 % (1107102)------------------------------
% 2.01/0.58 % (1107102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.58 % (1107102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.58 % (1107102)CaDiCaL version: 2.1.3
% 2.01/0.58 % (1107102)Termination reason: Instruction limit
% 2.01/0.58 % (1107102)Termination phase: shuffling
% 2.01/0.58 % (1107102)Time elapsed: 0.004 s
% 2.01/0.58 % (1107102)Peak memory usage: 10 MB
% 2.01/0.58 % (1107102)Instructions burned: 8 (million)
% 2.01/0.58 % (1107106)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=3947951951:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.01/0.58 % (1107089)Instruction limit reached!
% 2.01/0.58 % (1107089)------------------------------
% 2.01/0.58 % (1107089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.58 % (1107089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.58 % (1107089)CaDiCaL version: 2.1.3
% 2.01/0.58 % (1107089)Termination reason: Instruction limit
% 2.01/0.58 % (1107089)Termination phase: Saturation
% 2.01/0.58 % (1107089)Time elapsed: 0.068 s
% 2.01/0.58 % (1107089)Peak memory usage: 14 MB
% 2.01/0.58 % (1107089)Instructions burned: 329 (million)
% 2.01/0.58 % (1107109)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3375138972:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.01/0.58 % (1107110)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=311281298:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.01/0.58 % (1107111)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2117695522:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.01/0.58 % (1107100)Instruction limit reached!
% 2.40/0.64 % (1107100)------------------------------
% 2.40/0.64 % (1107100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.64 % (1107100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (1107100)CaDiCaL version: 2.1.3
% 2.40/0.64 % (1107100)Termination reason: Instruction limit
% 2.40/0.64 % (1107100)Termination phase: Property scanning
% 2.40/0.64 % (1107100)Time elapsed: 0.029 s
% 2.40/0.64 % (1107100)Peak memory usage: 12 MB
% 2.40/0.64 % (1107100)Instructions burned: 61 (million)
% 2.40/0.64 % (1107109)Instruction limit reached!
% 2.40/0.64 % (1107109)------------------------------
% 2.40/0.64 % (1107109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.64 % (1107109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (1107109)CaDiCaL version: 2.1.3
% 2.40/0.64 % (1107109)Termination reason: Instruction limit
% 2.40/0.64 % (1107109)Termination phase: shuffling
% 2.40/0.64 % (1107109)Time elapsed: 0.004 s
% 2.40/0.64 % (1107109)Peak memory usage: 10 MB
% 2.40/0.64 % (1107109)Instructions burned: 8 (million)
% 2.40/0.64 % (1107106)Instruction limit reached!
% 2.40/0.64 % (1107106)------------------------------
% 2.40/0.64 % (1107106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.64 % (1107106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (1107106)CaDiCaL version: 2.1.3
% 2.40/0.64 % (1107106)Termination reason: Instruction limit
% 2.40/0.64 % (1107106)Termination phase: shuffling
% 2.40/0.64 % (1107106)Time elapsed: 0.015 s
% 2.40/0.64 % (1107106)Peak memory usage: 11 MB
% 2.40/0.64 % (1107106)Instructions burned: 32 (million)
% 2.40/0.64 % (1107114)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1956669582:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.40/0.64 % (1107111)Instruction limit reached!
% 2.40/0.64 % (1107111)------------------------------
% 2.40/0.64 % (1107111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.64 % (1107111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (1107111)CaDiCaL version: 2.1.3
% 2.40/0.64 % (1107111)Termination reason: Instruction limit
% 2.40/0.64 % (1107111)Termination phase: shuffling
% 2.40/0.64 % (1107111)Time elapsed: 0.009 s
% 2.40/0.64 % (1107111)Peak memory usage: 11 MB
% 2.40/0.64 % (1107111)Instructions burned: 20 (million)
% 2.40/0.64 % (1107110)Instruction limit reached!
% 2.40/0.64 % (1107110)------------------------------
% 2.40/0.64 % (1107110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.64 % (1107110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (1107110)CaDiCaL version: 2.1.3
% 2.40/0.64 % (1107110)Termination reason: Instruction limit
% 2.40/0.64 % (1107110)Termination phase: shuffling
% 2.40/0.64 % (1107110)Time elapsed: 0.011 s
% 2.40/0.64 % (1107110)Peak memory usage: 10 MB
% 2.40/0.64 % (1107110)Instructions burned: 24 (million)
% 2.40/0.64 % (1107117)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=555554625:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.40/0.64 % (1107118)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1502237871:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.40/0.64 % (1107121)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.40/0.64 % (1107120)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1440265165:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.40/0.64 % (1107121)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3302484308:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.40/0.64 % (1107122)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1557917430:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.40/0.64 % (1107121)Instruction limit reached!
% 2.40/0.64 % (1107121)------------------------------
% 2.40/0.64 % (1107121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.64 % (1107121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (1107121)CaDiCaL version: 2.1.3
% 2.40/0.64 % (1107121)Termination reason: Instruction limit
% 2.57/0.73 % (1107121)Termination phase: shuffling
% 2.57/0.73 % (1107121)Time elapsed: 0.004 s
% 2.57/0.73 % (1107121)Peak memory usage: 10 MB
% 2.57/0.73 % (1107121)Instructions burned: 8 (million)
% 2.57/0.73 % (1107120)Instruction limit reached!
% 2.57/0.73 % (1107120)------------------------------
% 2.57/0.73 % (1107120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.73 % (1107120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.73 % (1107120)CaDiCaL version: 2.1.3
% 2.57/0.73 % (1107120)Termination reason: Instruction limit
% 2.57/0.73 % (1107120)Termination phase: Preprocessing 3
% 2.57/0.73 % (1107120)Time elapsed: 0.019 s
% 2.57/0.73 % (1107120)Peak memory usage: 11 MB
% 2.57/0.73 % (1107120)Instructions burned: 43 (million)
% 2.57/0.73 % (1107128)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=1970070243: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.57/0.73 % (1107129)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.57/0.73 % (1107129)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2560382883: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.57/0.73 % (1107129)Instruction limit reached!
% 2.57/0.73 % (1107129)------------------------------
% 2.57/0.73 % (1107129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.73 % (1107129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.73 % (1107129)CaDiCaL version: 2.1.3
% 2.57/0.73 % (1107129)Termination reason: Instruction limit
% 2.57/0.73 % (1107129)Termination phase: shuffling
% 2.57/0.73 % (1107129)Time elapsed: 0.003 s
% 2.57/0.73 % (1107129)Peak memory usage: 10 MB
% 2.57/0.73 % (1107129)Instructions burned: 6 (million)
% 2.57/0.73 % (1107132)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=4116904851:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.57/0.73 % (1107117)Instruction limit reached!
% 2.57/0.73 % (1107117)------------------------------
% 2.57/0.73 % (1107117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.73 % (1107117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.73 % (1107117)CaDiCaL version: 2.1.3
% 2.57/0.73 % (1107117)Termination reason: Instruction limit
% 2.57/0.73 % (1107117)Termination phase: Saturation
% 2.57/0.73 % (1107117)Time elapsed: 0.067 s
% 2.57/0.73 % (1107117)Peak memory usage: 14 MB
% 2.57/0.73 % (1107117)Instructions burned: 144 (million)
% 2.57/0.73 % (1107132)Instruction limit reached!
% 2.57/0.73 % (1107132)------------------------------
% 2.57/0.73 % (1107132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.73 % (1107132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.73 % (1107132)CaDiCaL version: 2.1.3
% 2.57/0.73 % (1107132)Termination reason: Instruction limit
% 2.57/0.73 % (1107132)Termination phase: Property scanning
% 2.57/0.73 % (1107132)Time elapsed: 0.010 s
% 2.57/0.73 % (1107132)Peak memory usage: 11 MB
% 2.57/0.73 % (1107132)Instructions burned: 22 (million)
% 2.57/0.73 % (1107134)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1084954706:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.57/0.73 % (1107122)Instruction limit reached!
% 2.57/0.73 % (1107122)------------------------------
% 2.57/0.73 % (1107122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.73 % (1107122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.73 % (1107122)CaDiCaL version: 2.1.3
% 2.57/0.73 % (1107122)Termination reason: Instruction limit
% 2.57/0.73 % (1107122)Termination phase: Saturation
% 2.57/0.73 % (1107122)Time elapsed: 0.079 s
% 2.57/0.73 % (1107122)Peak memory usage: 13 MB
% 2.57/0.73 % (1107122)Instructions burned: 181 (million)
% 2.57/0.73 % (1107135)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=2673927277:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.57/0.73 % (1107134)Instruction limit reached!
% 2.57/0.73 % (1107134)------------------------------
% 2.57/0.80 % (1107134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.80 % (1107134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.80 % (1107134)CaDiCaL version: 2.1.3
% 2.57/0.80 % (1107134)Termination reason: Instruction limit
% 2.57/0.80 % (1107134)Termination phase: shuffling
% 2.57/0.80 % (1107134)Time elapsed: 0.009 s
% 2.57/0.80 % (1107134)Peak memory usage: 10 MB
% 2.57/0.80 % (1107134)Instructions burned: 20 (million)
% 2.57/0.80 % (1107118)Instruction limit reached!
% 2.57/0.80 % (1107118)------------------------------
% 2.57/0.80 % (1107118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.80 % (1107118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.80 % (1107118)CaDiCaL version: 2.1.3
% 2.57/0.80 % (1107118)Termination reason: Instruction limit
% 2.57/0.80 % (1107118)Termination phase: Saturation
% 2.57/0.80 % (1107118)Time elapsed: 0.097 s
% 2.57/0.80 % (1107118)Peak memory usage: 14 MB
% 2.57/0.80 % (1107118)Instructions burned: 193 (million)
% 2.57/0.80 % (1107137)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=1747935315: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)
% 2.57/0.80 % (1107128)Instruction limit reached!
% 2.57/0.80 % (1107128)------------------------------
% 2.57/0.80 % (1107128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.80 % (1107128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.80 % (1107128)CaDiCaL version: 2.1.3
% 2.57/0.80 % (1107128)Termination reason: Instruction limit
% 2.57/0.80 % (1107128)Termination phase: Saturation
% 2.57/0.80 % (1107128)Time elapsed: 0.080 s
% 2.57/0.80 % (1107128)Peak memory usage: 14 MB
% 2.57/0.80 % (1107128)Instructions burned: 170 (million)
% 2.57/0.80 % (1107139)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=2906342656: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)
% 2.57/0.80 % (1107140)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3099254061:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 2.57/0.80 % (1107142)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1342896421: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)
% 2.57/0.80 % (1107139)Instruction limit reached!
% 2.57/0.80 % (1107139)------------------------------
% 2.57/0.80 % (1107139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.80 % (1107139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.80 % (1107139)CaDiCaL version: 2.1.3
% 2.57/0.80 % (1107139)Termination reason: Instruction limit
% 2.57/0.80 % (1107139)Termination phase: Property scanning
% 2.57/0.80 % (1107139)Time elapsed: 0.019 s
% 2.57/0.80 % (1107139)Peak memory usage: 11 MB
% 2.57/0.80 % (1107139)Instructions burned: 45 (million)
% 2.57/0.80 % (1107057)Instruction limit reached!
% 2.57/0.80 % (1107057)------------------------------
% 2.57/0.80 % (1107057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.80 % (1107057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.80 % (1107057)CaDiCaL version: 2.1.3
% 2.57/0.80 % (1107057)Termination reason: Instruction limit
% 2.57/0.80 % (1107057)Termination phase: Saturation
% 2.57/0.80 % (1107057)Time elapsed: 0.303 s
% 2.57/0.80 % (1107057)Peak memory usage: 16 MB
% 2.57/0.80 % (1107057)Instructions burned: 635 (million)
% 2.57/0.80 % (1107142)Instruction limit reached!
% 2.57/0.80 % (1107142)------------------------------
% 2.57/0.80 % (1107142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.80 % (1107142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.80 % (1107142)CaDiCaL version: 2.1.3
% 2.57/0.80 % (1107142)Termination reason: Instruction limit
% 2.57/0.80 % (1107142)Termination phase: shuffling
% 2.57/0.80 % (1107142)Time elapsed: 0.010 s
% 2.57/0.80 % (1107142)Peak memory usage: 10 MB
% 2.57/0.80 % (1107142)Instructions burned: 21 (million)
% 2.57/0.80 % (1107146)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.16/0.90 % (1107146)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=791627739:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.16/0.90 % (1107147)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2969019753:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.16/0.90 % (1107148)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=1021596296:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.16/0.90 % (1107147)Instruction limit reached!
% 3.16/0.90 % (1107147)------------------------------
% 3.16/0.90 % (1107147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.90 % (1107147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.90 % (1107147)CaDiCaL version: 2.1.3
% 3.16/0.90 % (1107147)Termination reason: Instruction limit
% 3.16/0.90 % (1107147)Termination phase: shuffling
% 3.16/0.90 % (1107147)Time elapsed: 0.006 s
% 3.16/0.90 % (1107147)Peak memory usage: 10 MB
% 3.16/0.90 % (1107147)Instructions burned: 13 (million)
% 3.16/0.90 % (1107152)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1739110325:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.16/0.90 % (1107148)Instruction limit reached!
% 3.16/0.90 % (1107148)------------------------------
% 3.16/0.90 % (1107148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.90 % (1107148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.90 % (1107148)CaDiCaL version: 2.1.3
% 3.16/0.90 % (1107148)Termination reason: Instruction limit
% 3.16/0.90 % (1107148)Termination phase: Property scanning
% 3.16/0.90 % (1107148)Time elapsed: 0.029 s
% 3.16/0.90 % (1107148)Peak memory usage: 11 MB
% 3.16/0.90 % (1107148)Instructions burned: 67 (million)
% 3.16/0.90 % (1107152)Instruction limit reached!
% 3.16/0.90 % (1107152)------------------------------
% 3.16/0.90 % (1107152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.90 % (1107152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.90 % (1107152)CaDiCaL version: 2.1.3
% 3.16/0.90 % (1107152)Termination reason: Instruction limit
% 3.16/0.90 % (1107152)Termination phase: Preprocessing 3
% 3.16/0.90 % (1107152)Time elapsed: 0.023 s
% 3.16/0.90 % (1107152)Peak memory usage: 11 MB
% 3.16/0.90 % (1107152)Instructions burned: 51 (million)
% 3.16/0.90 % (1107154)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3149165088:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 3.16/0.90 % (1107114)Instruction limit reached!
% 3.16/0.90 % (1107114)------------------------------
% 3.16/0.90 % (1107114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.90 % (1107114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.90 % (1107114)CaDiCaL version: 2.1.3
% 3.16/0.90 % (1107114)Termination reason: Instruction limit
% 3.16/0.90 % (1107114)Termination phase: Saturation
% 3.16/0.90 % (1107114)Time elapsed: 0.236 s
% 3.16/0.90 % (1107114)Peak memory usage: 16 MB
% 3.16/0.90 % (1107114)Instructions burned: 1244 (million)
% 3.16/0.90 % (1107154)Instruction limit reached!
% 3.16/0.90 % (1107154)------------------------------
% 3.16/0.90 % (1107154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.90 % (1107154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.90 % (1107154)CaDiCaL version: 2.1.3
% 3.16/0.90 % (1107154)Termination reason: Instruction limit
% 3.16/0.90 % (1107154)Termination phase: shuffling
% 3.16/0.90 % (1107154)Time elapsed: 0.015 s
% 3.16/0.90 % (1107154)Peak memory usage: 11 MB
% 3.16/0.90 % (1107154)Instructions burned: 33 (million)
% 3.16/0.90 % (1107155)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2722815513:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.16/0.90 % (1107157)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=4142071507:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.16/0.90 % (1107157)Instruction limit reached!
% 3.16/0.90 % (1107157)------------------------------
% 3.16/0.90 % (1107157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/1.00 % (1107157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.00 % (1107157)CaDiCaL version: 2.1.3
% 3.77/1.00 % (1107157)Termination reason: Instruction limit
% 3.77/1.00 % (1107157)Termination phase: shuffling
% 3.77/1.00 % (1107157)Time elapsed: 0.008 s
% 3.77/1.00 % (1107157)Peak memory usage: 11 MB
% 3.77/1.00 % (1107157)Instructions burned: 35 (million)
% 3.77/1.00 % (1107158)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2294697518:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.77/1.00 % (1107162)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.77/1.00 % (1107135)Instruction limit reached!
% 3.77/1.00 % (1107135)------------------------------
% 3.77/1.00 % (1107135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/1.00 % (1107135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.00 % (1107135)CaDiCaL version: 2.1.3
% 3.77/1.00 % (1107135)Termination reason: Instruction limit
% 3.77/1.00 % (1107135)Termination phase: Saturation
% 3.77/1.00 % (1107135)Time elapsed: 0.157 s
% 3.77/1.00 % (1107135)Peak memory usage: 17 MB
% 3.77/1.00 % (1107135)Instructions burned: 317 (million)
% 3.77/1.00 % (1107146)Instruction limit reached!
% 3.77/1.00 % (1107146)------------------------------
% 3.77/1.00 % (1107146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/1.00 % (1107146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.00 % (1107146)CaDiCaL version: 2.1.3
% 3.77/1.00 % (1107146)Termination reason: Instruction limit
% 3.77/1.00 % (1107146)Termination phase: Saturation
% 3.77/1.00 % (1107146)Time elapsed: 0.095 s
% 3.77/1.00 % (1107146)Peak memory usage: 14 MB
% 3.77/1.00 % (1107146)Instructions burned: 202 (million)
% 3.77/1.00 % (1107162)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1729948065:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 3.77/1.00 % (1107164)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=4199243358:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 3.77/1.00 % (1107165)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1896196674:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 3.77/1.00 % (1107158)Instruction limit reached!
% 3.77/1.00 % (1107158)------------------------------
% 3.77/1.00 % (1107158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/1.00 % (1107158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.00 % (1107158)CaDiCaL version: 2.1.3
% 3.77/1.00 % (1107158)Termination reason: Instruction limit
% 3.77/1.00 % (1107158)Termination phase: Property scanning
% 3.77/1.00 % (1107158)Time elapsed: 0.031 s
% 3.77/1.00 % (1107158)Peak memory usage: 12 MB
% 3.77/1.00 % (1107158)Instructions burned: 69 (million)
% 3.77/1.00 % (1107155)Instruction limit reached!
% 3.77/1.00 % (1107155)------------------------------
% 3.77/1.00 % (1107155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/1.00 % (1107155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.00 % (1107155)CaDiCaL version: 2.1.3
% 3.77/1.00 % (1107155)Termination reason: Instruction limit
% 3.77/1.00 % (1107155)Termination phase: Saturation
% 3.77/1.00 % (1107155)Time elapsed: 0.064 s
% 3.77/1.00 % (1107155)Peak memory usage: 14 MB
% 3.77/1.00 % (1107155)Instructions burned: 139 (million)
% 3.77/1.00 % (1107168)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=351722030:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 3.77/1.00 % (1107162)Instruction limit reached!
% 3.77/1.00 % (1107162)------------------------------
% 3.77/1.00 % (1107162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/1.00 % (1107162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.00 % (1107162)CaDiCaL version: 2.1.3
% 3.77/1.00 % (1107162)Termination reason: Instruction limit
% 3.77/1.00 % (1107162)Termination phase: Saturation
% 3.77/1.00 % (1107162)Time elapsed: 0.041 s
% 3.77/1.00 % (1107162)Peak memory usage: 13 MB
% 3.77/1.00 % (1107162)Instructions burned: 181 (million)
% 3.77/1.00 % (1107169)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=650107146:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 5.30/1.08 % (1107168)Refutation not found, incomplete strategy
% 5.30/1.08 % (1107168)------------------------------
% 5.30/1.08 % (1107168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.08 % (1107168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.08 % (1107168)CaDiCaL version: 2.1.3
% 5.30/1.08 % (1107168)Termination reason: Refutation not found, incomplete strategy
% 5.30/1.08 % (1107168)Time elapsed: 0.020 s
% 5.30/1.08 % (1107168)Peak memory usage: 13 MB
% 5.30/1.08 % (1107168)Instructions burned: 42 (million)
% 5.30/1.08 % (1107171)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=1005224527:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 5.30/1.08 % (1107168)------------------------------
% 5.30/1.08 % (1107168)------------------------------
% 5.30/1.08 % (1107165)Instruction limit reached!
% 5.30/1.08 % (1107165)------------------------------
% 5.30/1.08 % (1107165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.08 % (1107165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.08 % (1107165)CaDiCaL version: 2.1.3
% 5.30/1.08 % (1107165)Termination reason: Instruction limit
% 5.30/1.08 % (1107165)Termination phase: Property scanning
% 5.30/1.08 % (1107165)Time elapsed: 0.043 s
% 5.30/1.08 % (1107165)Peak memory usage: 12 MB
% 5.30/1.08 % (1107165)Instructions burned: 96 (million)
% 5.30/1.08 % (1107174)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3189703452:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 5.30/1.08 % (1107175)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2209937492:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 5.30/1.08 % (1107140)Instruction limit reached!
% 5.30/1.08 % (1107140)------------------------------
% 5.30/1.08 % (1107140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.08 % (1107140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.08 % (1107140)CaDiCaL version: 2.1.3
% 5.30/1.08 % (1107140)Termination reason: Instruction limit
% 5.30/1.08 % (1107140)Termination phase: Saturation
% 5.30/1.08 % (1107140)Time elapsed: 0.235 s
% 5.30/1.08 % (1107140)Peak memory usage: 17 MB
% 5.30/1.08 % (1107140)Instructions burned: 481 (million)
% 5.30/1.08 % (1107175)Instruction limit reached!
% 5.30/1.08 % (1107175)------------------------------
% 5.30/1.08 % (1107175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.08 % (1107175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.08 % (1107175)CaDiCaL version: 2.1.3
% 5.30/1.08 % (1107175)Termination reason: Instruction limit
% 5.30/1.08 % (1107175)Termination phase: shuffling
% 5.30/1.08 % (1107175)Time elapsed: 0.022 s
% 5.30/1.08 % (1107175)Peak memory usage: 11 MB
% 5.30/1.08 % (1107175)Instructions burned: 44 (million)
% 5.30/1.08 % (1107178)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=4098354846:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 5.30/1.08 % (1107179)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3909802780:i=450:rtra=on:ixr=off:ntd=on_2994 on theBenchmark for (2994ds/450Mi)
% 5.30/1.08 % (1107164)Instruction limit reached!
% 5.30/1.08 % (1107164)------------------------------
% 5.30/1.08 % (1107164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.08 % (1107164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.08 % (1107164)CaDiCaL version: 2.1.3
% 5.30/1.08 % (1107164)Termination reason: Instruction limit
% 5.30/1.08 % (1107164)Termination phase: Saturation
% 5.30/1.08 % (1107164)Time elapsed: 0.119 s
% 5.30/1.08 % (1107164)Peak memory usage: 14 MB
% 5.30/1.08 % (1107164)Instructions burned: 247 (million)
% 5.30/1.08 % (1107174)Instruction limit reached!
% 5.30/1.08 % (1107174)------------------------------
% 5.30/1.08 % (1107174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.08 % (1107174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.08 % (1107174)CaDiCaL version: 2.1.3
% 5.30/1.08 % (1107174)Termination reason: Instruction limit
% 5.30/1.08 % (1107174)Termination phase: Property scanning
% 5.30/1.08 % (1107174)Time elapsed: 0.057 s
% 5.30/1.08 % (1107174)Peak memory usage: 12 MB
% 5.30/1.08 % (1107174)Instructions burned: 132 (million)
% 5.30/1.08 % (1107182)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=2941137707:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 5.87/1.15 % (1107183)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=1411010618:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 5.87/1.15 % (1107183)Instruction limit reached!
% 5.87/1.15 % (1107183)------------------------------
% 5.87/1.15 % (1107183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.15 % (1107183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.15 % (1107183)CaDiCaL version: 2.1.3
% 5.87/1.15 % (1107183)Termination reason: Instruction limit
% 5.87/1.15 % (1107183)Termination phase: Property scanning
% 5.87/1.15 % (1107183)Time elapsed: 0.028 s
% 5.87/1.15 % (1107183)Peak memory usage: 11 MB
% 5.87/1.15 % (1107183)Instructions burned: 65 (million)
% 5.87/1.15 % (1107178)Refutation not found, incomplete strategy
% 5.87/1.15 % (1107178)------------------------------
% 5.87/1.15 % (1107178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.15 % (1107178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.15 % (1107178)CaDiCaL version: 2.1.3
% 5.87/1.15 % (1107178)Termination reason: Refutation not found, incomplete strategy
% 5.87/1.15 % (1107178)Time elapsed: 0.070 s
% 5.87/1.15 % (1107178)Peak memory usage: 15 MB
% 5.87/1.15 % (1107178)Instructions burned: 142 (million)
% 5.87/1.15 % (1107178)------------------------------
% 5.87/1.15 % (1107178)------------------------------
% 5.87/1.15 % (1107182)Instruction limit reached!
% 5.87/1.15 % (1107182)------------------------------
% 5.87/1.15 % (1107182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.15 % (1107182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.15 % (1107182)CaDiCaL version: 2.1.3
% 5.87/1.15 % (1107182)Termination reason: Instruction limit
% 5.87/1.15 % (1107182)Termination phase: Property scanning
% 5.87/1.15 % (1107182)Time elapsed: 0.043 s
% 5.87/1.15 % (1107182)Peak memory usage: 12 MB
% 5.87/1.15 % (1107182)Instructions burned: 96 (million)
% 5.87/1.15 % (1107171)Instruction limit reached!
% 5.87/1.15 % (1107171)------------------------------
% 5.87/1.15 % (1107171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.15 % (1107171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.15 % (1107171)CaDiCaL version: 2.1.3
% 5.87/1.15 % (1107171)Termination reason: Instruction limit
% 5.87/1.15 % (1107171)Termination phase: Saturation
% 5.87/1.15 % (1107171)Time elapsed: 0.143 s
% 5.87/1.15 % (1107171)Peak memory usage: 14 MB
% 5.87/1.15 % (1107171)Instructions burned: 517 (million)
% 5.87/1.15 % (1107186)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=1311259750: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_2993 on theBenchmark for (2993ds/105Mi)
% 5.87/1.15 % (1107187)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=1026979132:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2993 on theBenchmark for (2993ds/5755Mi)
% 5.87/1.15 % (1107189)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3765999342:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2993 on theBenchmark for (2993ds/495Mi)
% 5.87/1.15 % (1107188)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=3731171548:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/375Mi)
% 5.87/1.15 % (1107186)Instruction limit reached!
% 5.87/1.15 % (1107186)------------------------------
% 5.87/1.15 % (1107186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.15 % (1107186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.15 % (1107186)CaDiCaL version: 2.1.3
% 5.87/1.15 % (1107186)Termination reason: Instruction limit
% 5.87/1.15 % (1107186)Termination phase: Property scanning
% 5.87/1.15 % (1107186)Time elapsed: 0.047 s
% 5.87/1.15 % (1107186)Peak memory usage: 12 MB
% 5.87/1.15 % (1107186)Instructions burned: 105 (million)
% 5.87/1.15 % (1107137)Instruction limit reached!
% 6.11/1.26 % (1107137)------------------------------
% 6.11/1.26 % (1107137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (1107137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (1107137)CaDiCaL version: 2.1.3
% 6.11/1.26 % (1107137)Termination reason: Instruction limit
% 6.11/1.26 % (1107137)Termination phase: Saturation
% 6.11/1.26 % (1107137)Time elapsed: 0.405 s
% 6.11/1.26 % (1107137)Peak memory usage: 16 MB
% 6.11/1.26 % (1107137)Instructions burned: 856 (million)
% 6.11/1.26 % (1107194)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=1700947846:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 6.11/1.26 % (1107195)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=4222569647:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/91Mi)
% 6.11/1.26 % (1107194)Instruction limit reached!
% 6.11/1.26 % (1107194)------------------------------
% 6.11/1.26 % (1107194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (1107194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (1107194)CaDiCaL version: 2.1.3
% 6.11/1.26 % (1107194)Termination reason: Instruction limit
% 6.11/1.26 % (1107194)Termination phase: shuffling
% 6.11/1.26 % (1107194)Time elapsed: 0.016 s
% 6.11/1.26 % (1107194)Peak memory usage: 11 MB
% 6.11/1.26 % (1107194)Instructions burned: 36 (million)
% 6.11/1.26 % (1107179)Instruction limit reached!
% 6.11/1.26 % (1107179)------------------------------
% 6.11/1.26 % (1107179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (1107179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (1107179)CaDiCaL version: 2.1.3
% 6.11/1.26 % (1107179)Termination reason: Instruction limit
% 6.11/1.26 % (1107179)Termination phase: Saturation
% 6.11/1.26 % (1107179)Time elapsed: 0.166 s
% 6.11/1.26 % (1107179)Peak memory usage: 14 MB
% 6.11/1.26 % (1107179)Instructions burned: 452 (million)
% 6.11/1.26 % (1107198)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=1006596163:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2992 on theBenchmark for (2992ds/66Mi)
% 6.11/1.26 % (1107199)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1976057208:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2992 on theBenchmark for (2992ds/22Mi)
% 6.11/1.26 % (1107199)Instruction limit reached!
% 6.11/1.26 % (1107199)------------------------------
% 6.11/1.26 % (1107199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (1107199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (1107199)CaDiCaL version: 2.1.3
% 6.11/1.26 % (1107199)Termination reason: Instruction limit
% 6.11/1.26 % (1107199)Termination phase: Property scanning
% 6.11/1.26 % (1107199)Time elapsed: 0.010 s
% 6.11/1.26 % (1107199)Peak memory usage: 11 MB
% 6.11/1.26 % (1107199)Instructions burned: 23 (million)
% 6.11/1.26 % (1107195)Instruction limit reached!
% 6.11/1.26 % (1107195)------------------------------
% 6.11/1.26 % (1107195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (1107195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (1107195)CaDiCaL version: 2.1.3
% 6.11/1.26 % (1107195)Termination reason: Instruction limit
% 6.11/1.26 % (1107195)Termination phase: Property scanning
% 6.11/1.26 % (1107195)Time elapsed: 0.042 s
% 6.11/1.26 % (1107195)Peak memory usage: 13 MB
% 6.11/1.26 % (1107195)Instructions burned: 92 (million)
% 6.11/1.26 % (1107198)Refutation not found, incomplete strategy
% 6.11/1.26 % (1107198)------------------------------
% 6.11/1.26 % (1107198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.11/1.26 % (1107198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.11/1.26 % (1107198)CaDiCaL version: 2.1.3
% 6.11/1.26 % (1107198)Termination reason: Refutation not found, incomplete strategy
% 6.11/1.26 % (1107198)Time elapsed: 0.019 s
% 6.11/1.26 % (1107198)Peak memory usage: 13 MB
% 6.11/1.26 % (1107198)Instructions burned: 40 (million)
% 6.11/1.26 % (1107198)------------------------------
% 6.11/1.26 % (1107198)------------------------------
% 6.11/1.26 % (1107202)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=74088151:i=338:bd=all:ins=4:rtra=on_2992 on theBenchmark for (2992ds/338Mi)
% 7.22/1.41 % (1107203)lrs+10_1_sil=128000:si=on:urr=on:random_seed=202895623:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/28Mi)
% 7.22/1.41 % (1107204)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.22/1.41 % (1107169)Instruction limit reached!
% 7.22/1.41 % (1107169)------------------------------
% 7.22/1.41 % (1107169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.22/1.41 % (1107169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.41 % (1107169)CaDiCaL version: 2.1.3
% 7.22/1.41 % (1107169)Termination reason: Instruction limit
% 7.22/1.41 % (1107169)Termination phase: Saturation
% 7.22/1.41 % (1107169)Time elapsed: 0.289 s
% 7.22/1.41 % (1107169)Peak memory usage: 14 MB
% 7.22/1.41 % (1107169)Instructions burned: 877 (million)
% 7.22/1.41 % (1107204)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=1286098582:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2992 on theBenchmark for (2992ds/137Mi)
% 7.22/1.41 % (1107189)Instruction limit reached!
% 7.22/1.41 % (1107189)------------------------------
% 7.22/1.41 % (1107189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.22/1.41 % (1107189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.41 % (1107189)CaDiCaL version: 2.1.3
% 7.22/1.41 % (1107189)Termination reason: Instruction limit
% 7.22/1.41 % (1107189)Termination phase: Saturation
% 7.22/1.41 % (1107189)Time elapsed: 0.135 s
% 7.22/1.41 % (1107189)Peak memory usage: 16 MB
% 7.22/1.41 % (1107189)Instructions burned: 498 (million)
% 7.22/1.41 % (1107203)Instruction limit reached!
% 7.22/1.41 % (1107203)------------------------------
% 7.22/1.41 % (1107203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.22/1.41 % (1107203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.41 % (1107203)CaDiCaL version: 2.1.3
% 7.22/1.41 % (1107203)Termination reason: Instruction limit
% 7.22/1.41 % (1107203)Termination phase: Property scanning
% 7.22/1.41 % (1107203)Time elapsed: 0.013 s
% 7.22/1.41 % (1107203)Peak memory usage: 11 MB
% 7.22/1.41 % (1107203)Instructions burned: 28 (million)
% 7.22/1.41 % (1107209)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2353984804:i=227:sd=1:bd=all:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/227Mi)
% 7.22/1.41 % (1107207)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=2685846772:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2991 on theBenchmark for (2991ds/340Mi)
% 7.22/1.41 % (1107210)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.22/1.41 % (1107209)Refutation not found, incomplete strategy
% 7.22/1.41 % (1107209)------------------------------
% 7.22/1.41 % (1107209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.22/1.41 % (1107209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.41 % (1107209)CaDiCaL version: 2.1.3
% 7.22/1.41 % (1107209)Termination reason: Refutation not found, incomplete strategy
% 7.22/1.41 % (1107209)Time elapsed: 0.010 s
% 7.22/1.41 % (1107209)Peak memory usage: 13 MB
% 7.22/1.41 % (1107209)Instructions burned: 42 (million)
% 7.22/1.41 % (1107209)------------------------------
% 7.22/1.41 % (1107209)------------------------------
% 7.22/1.41 % (1107210)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1362379311:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/373Mi)
% 7.22/1.41 % (1107213)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3573283212:i=116:ep=RSTC:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/116Mi)
% 7.22/1.41 % (1107204)Instruction limit reached!
% 7.22/1.41 % (1107204)------------------------------
% 7.22/1.41 % (1107204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.22/1.41 % (1107204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.41 % (1107204)CaDiCaL version: 2.1.3
% 7.22/1.41 % (1107204)Termination reason: Instruction limit
% 7.22/1.41 % (1107204)Termination phase: Property scanning
% 7.94/1.57 % (1107204)Time elapsed: 0.059 s
% 7.94/1.57 % (1107204)Peak memory usage: 12 MB
% 7.94/1.57 % (1107204)Instructions burned: 139 (million)
% 7.94/1.57 % (1107213)Instruction limit reached!
% 7.94/1.57 % (1107213)------------------------------
% 7.94/1.57 % (1107213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.57 % (1107213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.57 % (1107213)CaDiCaL version: 2.1.3
% 7.94/1.57 % (1107213)Termination reason: Instruction limit
% 7.94/1.57 % (1107213)Termination phase: Saturation
% 7.94/1.57 % (1107213)Time elapsed: 0.028 s
% 7.94/1.57 % (1107213)Peak memory usage: 13 MB
% 7.94/1.57 % (1107213)Instructions burned: 118 (million)
% 7.94/1.57 % (1107188)Instruction limit reached!
% 7.94/1.57 % (1107188)------------------------------
% 7.94/1.57 % (1107188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.57 % (1107188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.57 % (1107188)CaDiCaL version: 2.1.3
% 7.94/1.57 % (1107188)Termination reason: Instruction limit
% 7.94/1.57 % (1107188)Termination phase: Saturation
% 7.94/1.57 % (1107188)Time elapsed: 0.191 s
% 7.94/1.57 % (1107188)Peak memory usage: 15 MB
% 7.94/1.57 % (1107188)Instructions burned: 375 (million)
% 7.94/1.57 % (1107217)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2657907294:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2991 on theBenchmark for (2991ds/270Mi)
% 7.94/1.57 % (1107216)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=3626486132:i=575:rtra=on_2991 on theBenchmark for (2991ds/575Mi)
% 7.94/1.57 % (1107218)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=778152535: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_2991 on theBenchmark for (2991ds/9840Mi)
% 7.94/1.57 % (1107217)Instruction limit reached!
% 7.94/1.57 % (1107217)------------------------------
% 7.94/1.57 % (1107217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.57 % (1107217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.57 % (1107217)CaDiCaL version: 2.1.3
% 7.94/1.57 % (1107217)Termination reason: Instruction limit
% 7.94/1.57 % (1107217)Termination phase: Saturation
% 7.94/1.57 % (1107217)Time elapsed: 0.067 s
% 7.94/1.57 % (1107217)Peak memory usage: 14 MB
% 7.94/1.57 % (1107217)Instructions burned: 272 (million)
% 7.94/1.57 % (1107222)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=1822395324:i=421:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/421Mi)
% 7.94/1.57 % (1107202)Instruction limit reached!
% 7.94/1.57 % (1107202)------------------------------
% 7.94/1.57 % (1107202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.57 % (1107202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.57 % (1107202)CaDiCaL version: 2.1.3
% 7.94/1.57 % (1107202)Termination reason: Instruction limit
% 7.94/1.57 % (1107202)Termination phase: Saturation
% 7.94/1.57 % (1107202)Time elapsed: 0.162 s
% 7.94/1.57 % (1107202)Peak memory usage: 18 MB
% 7.94/1.57 % (1107202)Instructions burned: 338 (million)
% 7.94/1.57 % (1107222)Refutation not found, incomplete strategy
% 7.94/1.57 % (1107222)------------------------------
% 7.94/1.57 % (1107222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.57 % (1107222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.57 % (1107222)CaDiCaL version: 2.1.3
% 7.94/1.57 % (1107222)Termination reason: Refutation not found, incomplete strategy
% 7.94/1.57 % (1107222)Time elapsed: 0.010 s
% 7.94/1.57 % (1107222)Peak memory usage: 13 MB
% 7.94/1.57 % (1107222)Instructions burned: 42 (million)
% 7.94/1.57 % (1107222)------------------------------
% 7.94/1.57 % (1107222)------------------------------
% 7.94/1.57 % (1107224)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
% 7.94/1.57 % (1107225)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=112191086:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/31Mi)
% 7.94/1.57 % (1107224)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=1579827774:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/270Mi)
% 8.60/1.67 % (1107225)Instruction limit reached!
% 8.60/1.67 % (1107225)------------------------------
% 8.60/1.67 % (1107225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107225)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107225)Termination reason: Instruction limit
% 8.60/1.67 % (1107225)Termination phase: shuffling
% 8.60/1.67 % (1107225)Time elapsed: 0.007 s
% 8.60/1.67 % (1107225)Peak memory usage: 11 MB
% 8.60/1.67 % (1107225)Instructions burned: 31 (million)
% 8.60/1.67 % (1107207)Instruction limit reached!
% 8.60/1.67 % (1107207)------------------------------
% 8.60/1.67 % (1107207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107207)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107207)Termination reason: Instruction limit
% 8.60/1.67 % (1107207)Termination phase: Saturation
% 8.60/1.67 % (1107207)Time elapsed: 0.165 s
% 8.60/1.67 % (1107207)Peak memory usage: 15 MB
% 8.60/1.67 % (1107207)Instructions burned: 341 (million)
% 8.60/1.67 % (1107228)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 8.60/1.67 % (1107228)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
% 8.60/1.67 % (1107228)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=1517969573:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2990 on theBenchmark for (2990ds/1440Mi)
% 8.60/1.67 % (1107210)Instruction limit reached!
% 8.60/1.67 % (1107210)------------------------------
% 8.60/1.67 % (1107210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107210)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107210)Termination reason: Instruction limit
% 8.60/1.67 % (1107210)Termination phase: Saturation
% 8.60/1.67 % (1107210)Time elapsed: 0.176 s
% 8.60/1.67 % (1107210)Peak memory usage: 14 MB
% 8.60/1.67 % (1107210)Instructions burned: 374 (million)
% 8.60/1.67 % (1107229)dis+10_2_sil=128000:si=on:random_seed=3530775464:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2989 on theBenchmark for (2989ds/339Mi)
% 8.60/1.67 % (1107232)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2506225983:i=111:add=on:fgj=on:rtra=on:fdi=1024_2989 on theBenchmark for (2989ds/111Mi)
% 8.60/1.67 % (1107232)Instruction limit reached!
% 8.60/1.67 % (1107232)------------------------------
% 8.60/1.67 % (1107232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107232)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107232)Termination reason: Instruction limit
% 8.60/1.67 % (1107232)Termination phase: Saturation
% 8.60/1.67 % (1107232)Time elapsed: 0.050 s
% 8.60/1.67 % (1107232)Peak memory usage: 13 MB
% 8.60/1.67 % (1107232)Instructions burned: 112 (million)
% 8.60/1.67 % (1107234)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=2695499056:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2989 on theBenchmark for (2989ds/122Mi)
% 8.60/1.67 % (1107224)Instruction limit reached!
% 8.60/1.67 % (1107224)------------------------------
% 8.60/1.67 % (1107224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107224)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107224)Termination reason: Instruction limit
% 8.60/1.67 % (1107224)Termination phase: Saturation
% 8.60/1.67 % (1107224)Time elapsed: 0.126 s
% 8.60/1.67 % (1107224)Peak memory usage: 14 MB
% 8.60/1.67 % (1107224)Instructions burned: 271 (million)
% 8.60/1.67 % (1107236)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=3501728502:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/136Mi)
% 8.60/1.67 % (1107229)Instruction limit reached!
% 8.60/1.67 % (1107229)------------------------------
% 8.60/1.67 % (1107229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107229)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107229)Termination reason: Instruction limit
% 8.60/1.67 % (1107229)Termination phase: Saturation
% 8.60/1.67 % (1107229)Time elapsed: 0.135 s
% 8.60/1.67 % (1107229)Peak memory usage: 13 MB
% 8.60/1.67 % (1107229)Instructions burned: 340 (million)
% 8.60/1.67 % (1107234)Instruction limit reached!
% 8.60/1.67 % (1107234)------------------------------
% 8.60/1.67 % (1107234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107234)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107234)Termination reason: Instruction limit
% 8.60/1.67 % (1107234)Termination phase: Saturation
% 8.60/1.67 % (1107234)Time elapsed: 0.059 s
% 8.60/1.67 % (1107234)Peak memory usage: 14 MB
% 8.60/1.67 % (1107234)Instructions burned: 124 (million)
% 8.60/1.67 % (1107238)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1054538021:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2988 on theBenchmark for (2988ds/232Mi)
% 8.60/1.67 % (1107216)Instruction limit reached!
% 8.60/1.67 % (1107216)------------------------------
% 8.60/1.67 % (1107216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107216)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107216)Termination reason: Instruction limit
% 8.60/1.67 % (1107216)Termination phase: Saturation
% 8.60/1.67 % (1107216)Time elapsed: 0.282 s
% 8.60/1.67 % (1107216)Peak memory usage: 17 MB
% 8.60/1.67 % (1107216)Instructions burned: 577 (million)
% 8.60/1.67 % (1107239)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=3695657588:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2988 on theBenchmark for (2988ds/1254Mi)
% 8.60/1.67 % (1107241)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 8.60/1.67 % (1107241)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=324846745:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2988 on theBenchmark for (2988ds/281Mi)
% 8.60/1.67 % (1107236)Instruction limit reached!
% 8.60/1.67 % (1107236)------------------------------
% 8.60/1.67 % (1107236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107236)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107236)Termination reason: Instruction limit
% 8.60/1.67 % (1107236)Termination phase: Saturation
% 8.60/1.67 % (1107236)Time elapsed: 0.062 s
% 8.60/1.67 % (1107236)Peak memory usage: 14 MB
% 8.60/1.67 % (1107236)Instructions burned: 136 (million)
% 8.60/1.67 % (1107244)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1469211572:i=619:add=on:rtra=on_2987 on theBenchmark for (2987ds/619Mi)
% 8.60/1.67 % (1107228)Instruction limit reached!
% 8.60/1.67 % (1107228)------------------------------
% 8.60/1.67 % (1107228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107228)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107228)Termination reason: Instruction limit
% 8.60/1.67 % (1107228)Termination phase: Saturation
% 8.60/1.67 % (1107228)Time elapsed: 0.256 s
% 8.60/1.67 % (1107228)Peak memory usage: 14 MB
% 8.60/1.67 % (1107228)Instructions burned: 1445 (million)
% 8.60/1.67 % (1107246)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=275738257:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/865Mi)
% 8.60/1.67 % (1107238)Instruction limit reached!
% 8.60/1.67 % (1107238)------------------------------
% 8.60/1.67 % (1107238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107238)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107238)Termination reason: Instruction limit
% 8.60/1.67 % (1107238)Termination phase: Saturation
% 8.60/1.67 % (1107238)Time elapsed: 0.120 s
% 8.60/1.67 % (1107238)Peak memory usage: 14 MB
% 8.60/1.67 % (1107238)Instructions burned: 232 (million)
% 8.60/1.67 % (1107248)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2981836546:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2987 on theBenchmark for (2987ds/212Mi)
% 8.60/1.67 % (1107241)Instruction limit reached!
% 8.60/1.67 % (1107241)------------------------------
% 8.60/1.67 % (1107241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107241)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107241)Termination reason: Instruction limit
% 8.60/1.67 % (1107241)Termination phase: Saturation
% 8.60/1.67 % (1107241)Time elapsed: 0.122 s
% 8.60/1.67 % (1107241)Peak memory usage: 14 MB
% 8.60/1.67 % (1107241)Instructions burned: 281 (million)
% 8.60/1.67 % (1107244)Refutation not found, incomplete strategy
% 8.60/1.67 % (1107244)------------------------------
% 8.60/1.67 % (1107244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107244)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107244)Termination reason: Refutation not found, incomplete strategy
% 8.60/1.67 % (1107244)Time elapsed: 0.105 s
% 8.60/1.67 % (1107244)Peak memory usage: 17 MB
% 8.60/1.67 % (1107244)Instructions burned: 230 (million)
% 8.60/1.67 % (1107244)------------------------------
% 8.60/1.67 % (1107244)------------------------------
% 8.60/1.67 % (1107250)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=2929011045:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/130Mi)
% 8.60/1.67 % (1107251)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1417805472:st=1.5:i=346:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/346Mi)
% 8.60/1.67 % (1107248) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1107049-1107248"...
% 8.60/1.67 % (1107248)...printing done.
% 8.60/1.67 % (1107248)Refutation found. Thanks to Tanya!
% 8.60/1.67 % SZS status Theorem for theBenchmark
% 8.60/1.67 % SZS output start Proof for theBenchmark
% 8.60/1.67 thf(type_def_5, type, set_Pr1475944804lle_fm: $tType).
% 8.60/1.67 thf(type_def_6, type, produc1250255278lle_fm: $tType).
% 8.60/1.67 thf(type_def_7, type, set_Pr2012908090lle_tv: $tType).
% 8.60/1.67 thf(type_def_8, type, produc484385668lle_tv: $tType).
% 8.60/1.67 thf(type_def_9, type, set_Pr2061825550lle_tv: $tType).
% 8.60/1.67 thf(type_def_10, type, produc1852595672lle_tv: $tType).
% 8.60/1.67 thf(type_def_11, type, set_Pr1723822845lle_tv: $tType).
% 8.60/1.67 thf(type_def_12, type, set_Pr2120184979lle_fm: $tType).
% 8.60/1.67 thf(type_def_13, type, produc1443694919lle_tv: $tType).
% 8.60/1.67 thf(type_def_14, type, produc696645085lle_fm: $tType).
% 8.60/1.67 thf(type_def_15, type, set_Pr38785645e_tv_o: $tType).
% 8.60/1.67 thf(type_def_16, type, set_Pr2014382200lle_tv: $tType).
% 8.60/1.67 thf(type_def_17, type, set_Pr1019238018lle_fm: $tType).
% 8.60/1.67 thf(type_def_18, type, produc1647334210lle_tv: $tType).
% 8.60/1.67 thf(type_def_19, type, produc450659916lle_fm: $tType).
% 8.60/1.67 thf(type_def_20, type, set_li72793489lle_tv: $tType).
% 8.60/1.67 thf(type_def_21, type, set_Pa1764573435lle_tv: $tType).
% 8.60/1.67 thf(type_def_22, type, set_Pa1499417344lle_fm: $tType).
% 8.60/1.67 thf(type_def_23, type, paraco1605129243lle_tv: $tType).
% 8.60/1.67 thf(type_def_24, type, paraco1604210848lle_fm: $tType).
% 8.60/1.67 thf(type_def_25, type, list_char: $tType).
% 8.60/1.67 thf(type_def_26, type, set_o: $tType).
% 8.60/1.67 thf(type_def_27, type, nat: $tType).
% 8.60/1.67 thf(type_def_28, type, sTfun: ($tType * $tType) > $tType).
% 8.60/1.67 thf(func_def_0, type, the_Pr1724341910lle_fm: ((produc696645085lle_fm > $o) > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_1, type, the_Pr304385787lle_tv: ((produc1647334210lle_tv > $o) > produc1647334210lle_tv)).
% 8.60/1.67 thf(func_def_2, type, if_Par1134130401lle_tv: ($o > paraco1605129243lle_tv > paraco1605129243lle_tv > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_3, type, order_1376767238lle_tv: (set_Pr2014382200lle_tv > paraco1605129243lle_tv > set_Pa1764573435lle_tv)).
% 8.60/1.67 thf(func_def_4, type, order_1434492699lle_tv: (set_Pr2014382200lle_tv > paraco1605129243lle_tv > set_Pa1764573435lle_tv)).
% 8.60/1.67 thf(func_def_5, type, order_1215526505lle_tv: ((paraco1605129243lle_tv > paraco1605129243lle_tv > $o) > set_Pa1764573435lle_tv > set_Pr2014382200lle_tv)).
% 8.60/1.67 thf(func_def_6, type, paraco1325918602e_eval: ((list_char > paraco1605129243lle_tv) > paraco1604210848lle_fm > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_7, type, paraco69239110le_Con: (paraco1604210848lle_fm > paraco1604210848lle_fm > paraco1604210848lle_fm)).
% 8.60/1.67 thf(func_def_8, type, paraco1389086619le_Eql: (paraco1604210848lle_fm > paraco1604210848lle_fm > paraco1604210848lle_fm)).
% 8.60/1.67 thf(func_def_9, type, paraco1745535428le_Eql: (paraco1604210848lle_fm > paraco1604210848lle_fm > paraco1604210848lle_fm)).
% 8.60/1.67 thf(func_def_10, type, paraco445776468le_Neg: (paraco1604210848lle_fm > paraco1604210848lle_fm)).
% 8.60/1.67 thf(func_def_11, type, paraco1480028776le_Pro: (list_char > paraco1604210848lle_fm)).
% 8.60/1.67 thf(func_def_12, type, paraco367965286_Truth: paraco1604210848lle_fm).
% 8.60/1.67 thf(func_def_13, type, paraco1344940915le_Det: ($o > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_14, type, paraco793048302_Indet: (nat > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_15, type, paraco2051596139lle_tv: (($o > paraco1605129243lle_tv) > (nat > paraco1605129243lle_tv) > paraco1605129243lle_tv > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_16, type, paraco327635598_valid: (paraco1604210848lle_fm > $o)).
% 8.60/1.67 thf(func_def_17, type, produc1297923922lle_tv: ((list_char > paraco1605129243lle_tv) > (list_char > paraco1605129243lle_tv) > produc1852595672lle_tv)).
% 8.60/1.67 thf(func_def_18, type, produc1710735575lle_fm: ((list_char > paraco1605129243lle_tv) > paraco1604210848lle_fm > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_19, type, produc1943344577lle_tv: (paraco1604210848lle_fm > (list_char > paraco1605129243lle_tv) > produc1443694919lle_tv)).
% 8.60/1.67 thf(func_def_20, type, produc1126104134lle_fm: (paraco1604210848lle_fm > paraco1604210848lle_fm > produc450659916lle_fm)).
% 8.60/1.67 thf(func_def_21, type, produc2058540732lle_tv: (paraco1605129243lle_tv > paraco1605129243lle_tv > produc1647334210lle_tv)).
% 8.60/1.67 thf(func_def_22, type, produc407632608lle_fm: (produc696645085lle_fm > produc696645085lle_fm > produc1250255278lle_fm)).
% 8.60/1.67 thf(func_def_23, type, produc1537086518lle_tv: (produc1647334210lle_tv > produc1647334210lle_tv > produc484385668lle_tv)).
% 8.60/1.67 thf(func_def_24, type, produc327378790lle_fm: (set_li72793489lle_tv > ((list_char > paraco1605129243lle_tv) > set_Pa1499417344lle_fm) > set_Pr2120184979lle_fm)).
% 8.60/1.67 thf(func_def_25, type, produc559987792lle_tv: (set_Pa1499417344lle_fm > (paraco1604210848lle_fm > set_li72793489lle_tv) > set_Pr1723822845lle_tv)).
% 8.60/1.67 thf(func_def_26, type, produc479904331lle_tv: (set_Pa1764573435lle_tv > (paraco1605129243lle_tv > set_Pa1764573435lle_tv) > set_Pr2014382200lle_tv)).
% 8.60/1.67 thf(func_def_27, type, produc234482697lle_tv: (paraco1605129243lle_tv > paraco1605129243lle_tv > $o > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_28, type, produc1667860344e_tv_o: ((produc1852595672lle_tv > $o) > (list_char > paraco1605129243lle_tv) > (list_char > paraco1605129243lle_tv) > $o)).
% 8.60/1.67 thf(func_def_29, type, produc275353523e_fm_o: ((produc696645085lle_fm > $o) > (list_char > paraco1605129243lle_tv) > paraco1604210848lle_fm > $o)).
% 8.60/1.67 thf(func_def_30, type, produc251170289lle_fm: ((produc696645085lle_fm > produc696645085lle_fm) > (list_char > paraco1605129243lle_tv) > paraco1604210848lle_fm > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_31, type, produc298562633e_tv_o: ((produc1443694919lle_tv > $o) > paraco1604210848lle_fm > (list_char > paraco1605129243lle_tv) > $o)).
% 8.60/1.67 thf(func_def_32, type, produc635060359lle_fm: ((produc1443694919lle_tv > produc696645085lle_fm) > paraco1604210848lle_fm > (list_char > paraco1605129243lle_tv) > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_33, type, produc1339594628e_fm_o: ((produc450659916lle_fm > $o) > paraco1604210848lle_fm > paraco1604210848lle_fm > $o)).
% 8.60/1.67 thf(func_def_34, type, produc2005494902e_tv_o: ((produc1647334210lle_tv > produc1647334210lle_tv > $o) > paraco1605129243lle_tv > paraco1605129243lle_tv > produc1647334210lle_tv > $o)).
% 8.60/1.67 thf(func_def_35, type, produc621423502e_tv_o: ((produc1647334210lle_tv > $o) > paraco1605129243lle_tv > paraco1605129243lle_tv > $o)).
% 8.60/1.67 thf(func_def_36, type, produc724036226lle_tv: ((produc1647334210lle_tv > paraco1605129243lle_tv) > paraco1605129243lle_tv > paraco1605129243lle_tv > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_37, type, produc408556266e_fm_o: ((produc1250255278lle_fm > $o) > produc696645085lle_fm > produc696645085lle_fm > $o)).
% 8.60/1.67 thf(func_def_38, type, produc1113543188e_tv_o: ((produc484385668lle_tv > $o) > produc1647334210lle_tv > produc1647334210lle_tv > $o)).
% 8.60/1.67 thf(func_def_39, type, produc1504058474e_fm_o: (((list_char > paraco1605129243lle_tv) > paraco1604210848lle_fm > $o) > produc696645085lle_fm > $o)).
% 8.60/1.67 thf(func_def_40, type, produc144063912lle_fm: (((list_char > paraco1605129243lle_tv) > paraco1604210848lle_fm > produc696645085lle_fm) > produc696645085lle_fm > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_41, type, produc527953982lle_fm: ((paraco1604210848lle_fm > (list_char > paraco1605129243lle_tv) > produc696645085lle_fm) > produc1443694919lle_tv > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_42, type, produc2050176383e_tv_o: ((paraco1605129243lle_tv > paraco1605129243lle_tv > produc1647334210lle_tv > $o) > produc1647334210lle_tv > produc1647334210lle_tv > $o)).
% 8.60/1.67 thf(func_def_43, type, produc192124683lle_tv: ((paraco1605129243lle_tv > paraco1605129243lle_tv > paraco1605129243lle_tv) > produc1647334210lle_tv > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_44, type, produc323213387e_tv_o: ((produc1647334210lle_tv > produc1647334210lle_tv > $o) > produc484385668lle_tv > $o)).
% 8.60/1.67 thf(func_def_45, type, produc1900967599lle_fm: (((list_char > paraco1605129243lle_tv) > list_char > paraco1605129243lle_tv) > (paraco1604210848lle_fm > paraco1604210848lle_fm) > produc696645085lle_fm > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_46, type, produc918997546lle_tv: (((list_char > paraco1605129243lle_tv) > paraco1605129243lle_tv) > (paraco1604210848lle_fm > paraco1605129243lle_tv) > produc696645085lle_fm > produc1647334210lle_tv)).
% 8.60/1.67 thf(func_def_47, type, produc2008706836lle_fm: ((paraco1605129243lle_tv > list_char > paraco1605129243lle_tv) > (paraco1605129243lle_tv > paraco1604210848lle_fm) > produc1647334210lle_tv > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_48, type, produc1345917071lle_tv: ((paraco1605129243lle_tv > paraco1605129243lle_tv) > (paraco1605129243lle_tv > paraco1605129243lle_tv) > produc1647334210lle_tv > produc1647334210lle_tv)).
% 8.60/1.67 thf(func_def_49, type, produc101320793e_tv_o: (((list_char > paraco1605129243lle_tv) > (list_char > paraco1605129243lle_tv) > $o) > produc1852595672lle_tv > $o)).
% 8.60/1.67 thf(func_def_50, type, produc1949847036lle_tv: (((list_char > paraco1605129243lle_tv) > paraco1604210848lle_fm > list_char > paraco1605129243lle_tv) > produc696645085lle_fm > list_char > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_51, type, produc1221696404e_fm_o: (((list_char > paraco1605129243lle_tv) > paraco1604210848lle_fm > $o) > produc696645085lle_fm > $o)).
% 8.60/1.67 thf(func_def_52, type, produc427355858lle_fm: (((list_char > paraco1605129243lle_tv) > paraco1604210848lle_fm > produc696645085lle_fm) > produc696645085lle_fm > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_53, type, produc401650381lle_tv: (((list_char > paraco1605129243lle_tv) > paraco1604210848lle_fm > produc1647334210lle_tv) > produc696645085lle_fm > produc1647334210lle_tv)).
% 8.60/1.67 thf(func_def_54, type, produc1244905514e_tv_o: ((paraco1604210848lle_fm > (list_char > paraco1605129243lle_tv) > $o) > produc1443694919lle_tv > $o)).
% 8.60/1.67 thf(func_def_55, type, produc811245928lle_fm: ((paraco1604210848lle_fm > (list_char > paraco1605129243lle_tv) > produc696645085lle_fm) > produc1443694919lle_tv > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_56, type, produc1629543915lle_tv: ((paraco1604210848lle_fm > paraco1604210848lle_fm > list_char > paraco1605129243lle_tv) > produc450659916lle_fm > list_char > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_57, type, produc182748835lle_fm: ((paraco1604210848lle_fm > paraco1604210848lle_fm > produc696645085lle_fm) > produc450659916lle_fm > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_58, type, produc1370344801lle_tv: ((paraco1605129243lle_tv > paraco1605129243lle_tv > list_char > paraco1605129243lle_tv) > produc1647334210lle_tv > list_char > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_59, type, produc25129173e_tv_o: ((paraco1605129243lle_tv > paraco1605129243lle_tv > produc1647334210lle_tv > $o) > produc1647334210lle_tv > produc1647334210lle_tv > $o)).
% 8.60/1.67 thf(func_def_60, type, produc852673135e_tv_o: ((paraco1605129243lle_tv > paraco1605129243lle_tv > $o) > produc1647334210lle_tv > $o)).
% 8.60/1.67 thf(func_def_61, type, produc1882560353lle_tv: ((paraco1605129243lle_tv > paraco1605129243lle_tv > paraco1605129243lle_tv) > produc1647334210lle_tv > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_62, type, produc377990317lle_fm: ((paraco1605129243lle_tv > paraco1605129243lle_tv > produc696645085lle_fm) > produc1647334210lle_tv > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_63, type, produc942307752lle_tv: ((paraco1605129243lle_tv > paraco1605129243lle_tv > produc1647334210lle_tv) > produc1647334210lle_tv > produc1647334210lle_tv)).
% 8.60/1.67 thf(func_def_64, type, produc1234307915e_fm_o: ((produc696645085lle_fm > produc696645085lle_fm > $o) > produc1250255278lle_fm > $o)).
% 8.60/1.67 thf(func_def_65, type, produc648306805e_tv_o: ((produc1647334210lle_tv > produc1647334210lle_tv > $o) > produc484385668lle_tv > $o)).
% 8.60/1.67 thf(func_def_66, type, produc29804011lle_fm: (produc696645085lle_fm > list_char > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_67, type, produc262413013lle_tv: (produc1443694919lle_tv > paraco1604210848lle_fm)).
% 8.60/1.67 thf(func_def_68, type, produc488585168lle_tv: (produc1647334210lle_tv > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_69, type, produc148705065lle_fm: (produc696645085lle_fm > paraco1604210848lle_fm)).
% 8.60/1.67 thf(func_def_70, type, produc381314067lle_tv: (produc1443694919lle_tv > list_char > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_71, type, produc1837067022lle_tv: (produc1647334210lle_tv > paraco1605129243lle_tv)).
% 8.60/1.67 thf(func_def_72, type, produc1176291762lle_tv: (produc1852595672lle_tv > produc1852595672lle_tv)).
% 8.60/1.67 thf(func_def_73, type, produc1000205111lle_fm: (produc696645085lle_fm > produc1443694919lle_tv)).
% 8.60/1.67 thf(func_def_74, type, produc1232814113lle_tv: (produc1443694919lle_tv > produc696645085lle_fm)).
% 8.60/1.67 thf(func_def_75, type, produc1426802342lle_fm: (produc450659916lle_fm > produc450659916lle_fm)).
% 8.60/1.67 thf(func_def_76, type, produc211755292lle_tv: (produc1647334210lle_tv > produc1647334210lle_tv)).
% 8.60/1.67 thf(func_def_77, type, produc116249920lle_fm: (produc1250255278lle_fm > produc1250255278lle_fm)).
% 8.60/1.67 thf(func_def_78, type, produc1733045910lle_tv: (produc484385668lle_tv > produc484385668lle_tv)).
% 8.60/1.67 thf(func_def_79, type, inv_im719552961lle_tv: (set_Pr2014382200lle_tv > (paraco1605129243lle_tv > paraco1605129243lle_tv) > set_Pr2014382200lle_tv)).
% 8.60/1.67 thf(func_def_80, type, collec1351702300lle_tv: (((list_char > paraco1605129243lle_tv) > $o) > set_li72793489lle_tv)).
% 8.60/1.67 thf(func_def_81, type, collec1111687558lle_tv: ((paraco1605129243lle_tv > $o) > set_Pa1764573435lle_tv)).
% 8.60/1.67 thf(func_def_82, type, collec1102043437lle_tv: ((produc1852595672lle_tv > $o) > set_Pr2061825550lle_tv)).
% 8.60/1.67 thf(func_def_83, type, collec835549234lle_fm: ((produc696645085lle_fm > $o) > set_Pr2120184979lle_fm)).
% 8.60/1.67 thf(func_def_84, type, collec15260823lle_tv: ((produc1647334210lle_tv > $o) > set_Pr2014382200lle_tv)).
% 8.60/1.67 thf(func_def_85, type, collec1363950211lle_fm: ((produc1250255278lle_fm > $o) > set_Pr1475944804lle_fm)).
% 8.60/1.67 thf(func_def_86, type, collec1900284505lle_tv: ((produc484385668lle_tv > $o) > set_Pr2012908090lle_tv)).
% 8.60/1.67 thf(func_def_87, type, image_305309148lle_tv: ((produc696645085lle_fm > list_char > paraco1605129243lle_tv) > set_Pr2120184979lle_fm > set_li72793489lle_tv)).
% 8.60/1.67 thf(func_def_88, type, image_1402739636e_fm_o: ((produc696645085lle_fm > $o) > set_Pr2120184979lle_fm > set_o)).
% 8.60/1.67 thf(func_def_89, type, image_807538418lle_fm: ((produc696645085lle_fm > produc696645085lle_fm) > set_Pr2120184979lle_fm > set_Pr2120184979lle_fm)).
% 8.60/1.67 thf(func_def_90, type, image_924970994lle_tv: ((produc696645085lle_fm > produc1443694919lle_tv) > set_Pr2120184979lle_fm > set_Pr1723822845lle_tv)).
% 8.60/1.67 thf(func_def_91, type, image_1110913773lle_tv: ((produc696645085lle_fm > produc1647334210lle_tv) > set_Pr2120184979lle_fm > set_Pr2014382200lle_tv)).
% 8.60/1.67 thf(func_def_92, type, image_326034184lle_fm: ((produc1443694919lle_tv > produc696645085lle_fm) > set_Pr1723822845lle_tv > set_Pr2120184979lle_fm)).
% 8.60/1.67 thf(func_def_93, type, image_496052427lle_tv: ((produc450659916lle_fm > list_char > paraco1605129243lle_tv) > set_Pr1019238018lle_fm > set_li72793489lle_tv)).
% 8.60/1.67 thf(func_def_94, type, image_1662022595lle_fm: ((produc450659916lle_fm > produc696645085lle_fm) > set_Pr1019238018lle_fm > set_Pr2120184979lle_fm)).
% 8.60/1.67 thf(func_def_95, type, image_1070648001lle_tv: ((produc1647334210lle_tv > list_char > paraco1605129243lle_tv) > set_Pr2014382200lle_tv > set_li72793489lle_tv)).
% 8.60/1.67 thf(func_def_96, type, image_1015627317e_tv_o: ((produc1647334210lle_tv > produc1647334210lle_tv > $o) > set_Pr2014382200lle_tv > set_Pr38785645e_tv_o)).
% 8.60/1.67 thf(func_def_97, type, image_1263514817lle_tv: ((produc1647334210lle_tv > paraco1605129243lle_tv) > set_Pr2014382200lle_tv > set_Pa1764573435lle_tv)).
% 8.60/1.67 thf(func_def_98, type, image_937396045lle_fm: ((produc1647334210lle_tv > produc696645085lle_fm) > set_Pr2014382200lle_tv > set_Pr2120184979lle_fm)).
% 8.60/1.67 thf(func_def_99, type, image_1221801032lle_tv: ((produc1647334210lle_tv > produc1647334210lle_tv) > set_Pr2014382200lle_tv > set_Pr2014382200lle_tv)).
% 8.60/1.67 thf(func_def_100, type, image_1610089293e_tv_o: ((produc484385668lle_tv > $o) > set_Pr2012908090lle_tv > set_o)).
% 8.60/1.67 thf(func_def_101, type, lex_pr2001015487lle_fm: (set_Pr2061825550lle_tv > set_Pr1019238018lle_fm > set_Pr1475944804lle_fm)).
% 8.60/1.67 thf(func_def_102, type, lex_pr567812260lle_tv: (set_Pr2014382200lle_tv > set_Pr2014382200lle_tv > set_Pr2012908090lle_tv)).
% 8.60/1.67 thf(func_def_103, type, same_f1581085506lle_fm: (((list_char > paraco1605129243lle_tv) > $o) > ((list_char > paraco1605129243lle_tv) > set_Pr1019238018lle_fm) > set_Pr1475944804lle_fm)).
% 8.60/1.67 thf(func_def_104, type, same_f1119076903lle_tv: ((paraco1605129243lle_tv > $o) > (paraco1605129243lle_tv > set_Pr2014382200lle_tv) > set_Pr2012908090lle_tv)).
% 8.60/1.67 thf(func_def_105, type, member894927066lle_tv: ((list_char > paraco1605129243lle_tv) > set_li72793489lle_tv > $o)).
% 8.60/1.67 thf(func_def_106, type, member1832524214e_tv_o: ((produc1647334210lle_tv > $o) > set_Pr38785645e_tv_o > $o)).
% 8.60/1.67 thf(func_def_107, type, member_o: ($o > set_o > $o)).
% 8.60/1.67 thf(func_def_108, type, member265982409lle_fm: (paraco1604210848lle_fm > set_Pa1499417344lle_fm > $o)).
% 8.60/1.67 thf(func_def_109, type, member266900804lle_tv: (paraco1605129243lle_tv > set_Pa1764573435lle_tv > $o)).
% 8.60/1.67 thf(func_def_110, type, member146333935lle_tv: (produc1852595672lle_tv > set_Pr2061825550lle_tv > $o)).
% 8.60/1.67 thf(func_def_111, type, member1474794996lle_fm: (produc696645085lle_fm > set_Pr2120184979lle_fm > $o)).
% 8.60/1.67 thf(func_def_112, type, member74361182lle_tv: (produc1443694919lle_tv > set_Pr1723822845lle_tv > $o)).
% 8.60/1.67 thf(func_def_113, type, member334644067lle_fm: (produc450659916lle_fm > set_Pr1019238018lle_fm > $o)).
% 8.60/1.67 thf(func_def_114, type, member1531318361lle_tv: (produc1647334210lle_tv > set_Pr2014382200lle_tv > $o)).
% 8.60/1.67 thf(func_def_115, type, member1592865093lle_fm: (produc1250255278lle_fm > set_Pr1475944804lle_fm > $o)).
% 8.60/1.67 thf(func_def_116, type, member1074212123lle_tv: (produc484385668lle_tv > set_Pr2012908090lle_tv > $o)).
% 8.60/1.67 thf(func_def_117, type, p: paraco1604210848lle_fm).
% 8.60/1.67 thf(func_def_119, type, db1: !>[X0: $tType]:(X0)).
% 8.60/1.67 thf(func_def_120, type, db0: !>[X0: $tType]:(X0)).
% 8.60/1.67 thf(func_def_121, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 8.60/1.67 thf(func_def_122, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 8.60/1.67 thf(func_def_125, type, vOR: ($o > $o > $o)).
% 8.60/1.67 thf(func_def_126, type, vAND: ($o > $o > $o)).
% 8.60/1.67 thf(func_def_127, type, db2: !>[X0: $tType]:(X0)).
% 8.60/1.67 thf(func_def_128, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 8.60/1.67 thf(func_def_129, type, vNOT: ($o > $o)).
% 8.60/1.67 thf(func_def_130, type, vIMP: ($o > $o > $o)).
% 8.60/1.67 thf(func_def_131, type, db4: !>[X0: $tType]:(X0)).
% 8.60/1.67 thf(func_def_132, type, db3: !>[X0: $tType]:(X0)).
% 8.60/1.67 thf(func_def_133, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 8.60/1.67 thf(func_def_134, type, db5: !>[X0: $tType]:(X0)).
% 8.60/1.67 thf(func_def_135, type, sK0: ((paraco1605129243lle_tv > $o) > $o)).
% 8.60/1.67 thf(func_def_136, type, sK1: ((paraco1605129243lle_tv > $o) > nat)).
% 8.60/1.67 thf(func_def_137, type, sK2: ((paraco1605129243lle_tv > $o) > nat)).
% 8.60/1.67 thf(func_def_138, type, sK3: (paraco1605129243lle_tv > nat)).
% 8.60/1.67 thf(func_def_139, type, sK4: (paraco1605129243lle_tv > $o)).
% 8.60/1.67 thf(func_def_140, type, sK5: (paraco1605129243lle_tv > nat)).
% 8.60/1.67 thf(f1,axiom,(
% 8.60/1.67 ! [X1 : $o,X0 : $o] : ((((paraco1344940915le_Det @ X0)) = ((paraco1344940915le_Det @ X1))) = (X0 = X1))),
% 8.60/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_tv_Oinject_I1_J)).
% 8.60/1.67 thf(f2,axiom,(
% 8.60/1.67 (paraco327635598_valid @ (paraco445776468le_Neg @ p))),
% 8.60/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_assms)).
% 8.60/1.67 thf(f3,axiom,(
% 8.60/1.67 ((^[X0 : paraco1604210848lle_fm] : (! [X1 : (list_char > paraco1605129243lle_tv)] : (((paraco1344940915le_Det @ $true)) = ((paraco1325918602e_eval @ X1 @ X0))))) = paraco327635598_valid)),
% 8.60/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_valid__def)).
% 8.60/1.67 thf(f8,axiom,(
% 8.60/1.67 ! [X1 : paraco1604210848lle_fm,X0 : (list_char > paraco1605129243lle_tv)] : (((((paraco1325918602e_eval @ X0 @ X1)) = ((paraco1344940915le_Det @ $false))) => (((paraco1344940915le_Det @ $true)) = ((paraco1325918602e_eval @ X0 @ (paraco445776468le_Neg @ X1))))) & ((((paraco1344940915le_Det @ $false)) != ((paraco1325918602e_eval @ X0 @ X1))) => (((((paraco1344940915le_Det @ $true)) != ((paraco1325918602e_eval @ X0 @ X1))) => (((paraco1325918602e_eval @ X0 @ (paraco445776468le_Neg @ X1))) = ((paraco1325918602e_eval @ X0 @ X1)))) & ((((paraco1344940915le_Det @ $true)) = ((paraco1325918602e_eval @ X0 @ X1))) => (((paraco1325918602e_eval @ X0 @ (paraco445776468le_Neg @ X1))) = ((paraco1344940915le_Det @ $false)))))))),
% 8.60/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_eval__negation)).
% 8.60/1.67 thf(f358,conjecture,(
% 8.60/1.67 ? [X0 : (list_char > paraco1605129243lle_tv)] : (((paraco1344940915le_Det @ $true)) != ((paraco1325918602e_eval @ X0 @ p)))),
% 8.60/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 8.60/1.67 thf(f359,negated_conjecture,(
% 8.60/1.67 ~ ? [X0 : (list_char > paraco1605129243lle_tv)] : (((paraco1344940915le_Det @ $true)) != ((paraco1325918602e_eval @ X0 @ p)))),
% 8.60/1.67 inference(negated_conjecture,[status(cth)],[f358])).
% 8.60/1.67 thf(f372,plain,(
% 8.60/1.67 ! [X0 : $o,X1 : $o] : ((((paraco1344940915le_Det @ X0)) = ((paraco1344940915le_Det @ X1))) = (X0 = X1))),
% 8.60/1.67 inference(rectify,[],[f1])).
% 8.60/1.67 thf(f373,plain,(
% 8.60/1.67 ! [X0 : $o,X1 : $o] : ((((paraco1344940915le_Det @ X0) = (paraco1344940915le_Det @ X1))) = ((X0 = X1)))),
% 8.60/1.67 inference(fool_elimination,[],[f372])).
% 8.60/1.67 thf(f479,plain,(
% 8.60/1.67 ~ ? [X0 : (list_char > paraco1605129243lle_tv)] : (((paraco1344940915le_Det @ $true)) != ((paraco1325918602e_eval @ X0 @ p)))),
% 8.60/1.67 inference(rectify,[],[f359])).
% 8.60/1.67 thf(f480,plain,(
% 8.60/1.67 ~ ? [X0 : (list_char > paraco1605129243lle_tv)] : (((paraco1325918602e_eval @ X0 @ p)) != ((paraco1344940915le_Det @ $true)))),
% 8.60/1.67 inference(fool_elimination,[],[f479])).
% 8.60/1.67 thf(f610,plain,(
% 8.60/1.67 ((^[X0 : paraco1604210848lle_fm] : (! [X1 : (list_char > paraco1605129243lle_tv)] : (((paraco1344940915le_Det @ $true)) = ((paraco1325918602e_eval @ X1 @ X0))))) = paraco327635598_valid)),
% 8.60/1.67 inference(rectify,[],[f3])).
% 8.60/1.67 thf(f611,plain,(
% 8.60/1.67 (paraco327635598_valid = (^[Y0 : paraco1604210848lle_fm]: (!! @ (list_char > paraco1605129243lle_tv) @ (^[Y1 : list_char > paraco1605129243lle_tv]: ((paraco1344940915le_Det @ $true) = (paraco1325918602e_eval @ Y1 @ Y0))))))),
% 8.60/1.67 inference(fool_elimination,[],[f610])).
% 8.60/1.67 thf(f691,plain,(
% 8.60/1.67 ! [X0 : paraco1604210848lle_fm,X1 : (list_char > paraco1605129243lle_tv)] : (((((paraco1325918602e_eval @ X1 @ X0)) = ((paraco1344940915le_Det @ $false))) => (((paraco1344940915le_Det @ $true)) = ((paraco1325918602e_eval @ X1 @ (paraco445776468le_Neg @ X0))))) & ((((paraco1344940915le_Det @ $false)) != ((paraco1325918602e_eval @ X1 @ X0))) => (((((paraco1344940915le_Det @ $true)) != ((paraco1325918602e_eval @ X1 @ X0))) => (((paraco1325918602e_eval @ X1 @ X0)) = ((paraco1325918602e_eval @ X1 @ (paraco445776468le_Neg @ X0))))) & ((((paraco1344940915le_Det @ $true)) = ((paraco1325918602e_eval @ X1 @ X0))) => (((paraco1325918602e_eval @ X1 @ (paraco445776468le_Neg @ X0))) = ((paraco1344940915le_Det @ $false)))))))),
% 8.60/1.67 inference(rectify,[],[f8])).
% 8.60/1.67 thf(f692,plain,(
% 8.60/1.67 ! [X0 : paraco1604210848lle_fm,X1 : (list_char > paraco1605129243lle_tv)] : (((((paraco1325918602e_eval @ X1 @ X0)) = ((paraco1344940915le_Det @ $false))) => (((paraco1344940915le_Det @ $true)) = ((paraco1325918602e_eval @ X1 @ (paraco445776468le_Neg @ X0))))) & ((((paraco1325918602e_eval @ X1 @ X0)) != ((paraco1344940915le_Det @ $false))) => (((((paraco1325918602e_eval @ X1 @ X0)) = ((paraco1344940915le_Det @ $true))) => (((paraco1344940915le_Det @ $false)) = ((paraco1325918602e_eval @ X1 @ (paraco445776468le_Neg @ X0))))) & ((((paraco1325918602e_eval @ X1 @ X0)) != ((paraco1344940915le_Det @ $true))) => (((paraco1325918602e_eval @ X1 @ X0)) = ((paraco1325918602e_eval @ X1 @ (paraco445776468le_Neg @ X0))))))))),
% 8.60/1.67 inference(fool_elimination,[],[f691])).
% 8.60/1.67 thf(f757,plain,(
% 8.60/1.67 (paraco327635598_valid @ (paraco445776468le_Neg @ p))),
% 8.60/1.67 inference(rectify,[],[f2])).
% 8.60/1.67 thf(f758,plain,(
% 8.60/1.67 (((paraco327635598_valid @ (paraco445776468le_Neg @ p))) = $true)),
% 8.60/1.67 inference(fool_elimination,[],[f757])).
% 8.60/1.67 thf(f788,plain,(
% 8.60/1.67 ! [X0 : (list_char > paraco1605129243lle_tv)] : (((paraco1325918602e_eval @ X0 @ p)) = ((paraco1344940915le_Det @ $true)))),
% 8.60/1.67 inference(ennf_transformation,[],[f480])).
% 8.60/1.67 thf(f789,plain,(
% 8.60/1.67 ! [X1 : (list_char > paraco1605129243lle_tv),X0 : paraco1604210848lle_fm] : (((((paraco1344940915le_Det @ $true)) = ((paraco1325918602e_eval @ X1 @ (paraco445776468le_Neg @ X0)))) | (((paraco1325918602e_eval @ X1 @ X0)) != ((paraco1344940915le_Det @ $false)))) & ((((paraco1325918602e_eval @ X1 @ X0)) = ((paraco1344940915le_Det @ $false))) | (((((paraco1325918602e_eval @ X1 @ X0)) != ((paraco1344940915le_Det @ $true))) | (((paraco1344940915le_Det @ $false)) = ((paraco1325918602e_eval @ X1 @ (paraco445776468le_Neg @ X0))))) & ((((paraco1325918602e_eval @ X1 @ X0)) = ((paraco1325918602e_eval @ X1 @ (paraco445776468le_Neg @ X0)))) | (((paraco1325918602e_eval @ X1 @ X0)) = ((paraco1344940915le_Det @ $true)))))))),
% 8.60/1.67 inference(ennf_transformation,[],[f692])).
% 8.60/1.67 thf(f798,plain,(
% 8.60/1.67 ! [X0 : (list_char > paraco1605129243lle_tv),X1 : paraco1604210848lle_fm] : (((((paraco1325918602e_eval @ X0 @ (paraco445776468le_Neg @ X1))) = ((paraco1344940915le_Det @ $true))) | (((paraco1325918602e_eval @ X0 @ X1)) != ((paraco1344940915le_Det @ $false)))) & ((((paraco1325918602e_eval @ X0 @ X1)) = ((paraco1344940915le_Det @ $false))) | (((((paraco1325918602e_eval @ X0 @ X1)) != ((paraco1344940915le_Det @ $true))) | (((paraco1325918602e_eval @ X0 @ (paraco445776468le_Neg @ X1))) = ((paraco1344940915le_Det @ $false)))) & ((((paraco1325918602e_eval @ X0 @ X1)) = ((paraco1325918602e_eval @ X0 @ (paraco445776468le_Neg @ X1)))) | (((paraco1325918602e_eval @ X0 @ X1)) = ((paraco1344940915le_Det @ $true)))))))),
% 8.60/1.67 inference(rectify,[],[f789])).
% 8.60/1.67 thf(f809,plain,(
% 8.60/1.67 (paraco327635598_valid = (^[Y0 : paraco1604210848lle_fm]: (!! @ (list_char > paraco1605129243lle_tv) @ (^[Y1 : list_char > paraco1605129243lle_tv]: ((paraco1344940915le_Det @ $true) = (paraco1325918602e_eval @ Y1 @ Y0))))))),
% 8.60/1.67 inference(cnf_transformation,[],[f611])).
% 8.60/1.67 thf(f823,plain,(
% 8.60/1.67 ( ! [X0 : (list_char > paraco1605129243lle_tv),X1 : paraco1604210848lle_fm] : ((((paraco1325918602e_eval @ X0 @ X1)) != ((paraco1344940915le_Det @ $true))) | (((paraco1325918602e_eval @ X0 @ X1)) = ((paraco1344940915le_Det @ $false))) | (((paraco1325918602e_eval @ X0 @ (paraco445776468le_Neg @ X1))) = ((paraco1344940915le_Det @ $false)))) )),
% 8.60/1.67 inference(cnf_transformation,[],[f798])).
% 8.60/1.67 thf(f826,plain,(
% 8.60/1.67 ( ! [X0 : (list_char > paraco1605129243lle_tv)] : ((((paraco1325918602e_eval @ X0 @ p)) = ((paraco1344940915le_Det @ $true)))) )),
% 8.60/1.67 inference(cnf_transformation,[],[f788])).
% 8.60/1.67 thf(f828,plain,(
% 8.60/1.67 ( ! [X0 : $o,X1 : $o] : (((((paraco1344940915le_Det @ X0) = (paraco1344940915le_Det @ X1))) = ((X0 = X1)))) )),
% 8.60/1.67 inference(cnf_transformation,[],[f373])).
% 8.60/1.67 thf(f832,plain,(
% 8.60/1.67 (((paraco327635598_valid @ (paraco445776468le_Neg @ p))) = $true)),
% 8.60/1.67 inference(cnf_transformation,[],[f758])).
% 8.60/1.67 thf(f835,definition,(
% 8.60/1.67 ($true != $false)),
% 8.60/1.67 introduced(theory,[fool_distinctness_axiom])).
% 8.60/1.67 thf(f837,plain,(
% 8.60/1.67 ($true = (((^[Y0 : paraco1604210848lle_fm]: (!! @ (list_char > paraco1605129243lle_tv) @ (^[Y1 : list_char > paraco1605129243lle_tv]: ((paraco1344940915le_Det @ $true) = (paraco1325918602e_eval @ Y1 @ Y0))))) @ (paraco445776468le_Neg @ p))))),
% 8.60/1.67 inference(definition_unfolding,[],[f832,f809])).
% 8.60/1.67 thf(f839,plain,(
% 8.60/1.67 ( ! [X0 : $o,X1 : $o] : ((((X0 = X1)) = $true) | ((((paraco1344940915le_Det @ X0) = (paraco1344940915le_Det @ X1))) = $false)) )),
% 8.60/1.67 inference(iff_proxy_clausification,[],[f828])).
% 8.60/1.67 thf(f840,plain,(
% 8.60/1.67 ( ! [X0 : $o,X1 : $o] : (((((paraco1344940915le_Det @ X0) = (paraco1344940915le_Det @ X1))) = $false) | (X0 = X1)) )),
% 8.60/1.67 inference(equality_proxy_clausification,[],[f839])).
% 8.60/1.67 thf(f841,plain,(
% 8.60/1.67 ( ! [X0 : $o,X1 : $o] : ((X0 = X1) | (((paraco1344940915le_Det @ X0)) != ((paraco1344940915le_Det @ X1)))) )),
% 8.60/1.67 inference(equality_proxy_clausification,[],[f840])).
% 8.60/1.67 thf(f843,plain,(
% 8.60/1.67 ( ! [X0 : $o,X1 : $o] : ((((paraco1344940915le_Det @ X0)) != ((paraco1344940915le_Det @ X1))) | ($true = X1) | ($false = X0)) )),
% 8.60/1.67 inference(iff_proxy_clausification,[],[f841])).
% 8.60/1.67 thf(f848,plain,(
% 8.60/1.67 ($true = ((!! @ (list_char > paraco1605129243lle_tv) @ (^[Y0 : list_char > paraco1605129243lle_tv]: ((paraco1344940915le_Det @ $true) = (paraco1325918602e_eval @ Y0 @ (paraco445776468le_Neg @ p)))))))),
% 8.60/1.67 inference(beta-eta_normalization,[],[f837])).
% 8.60/1.67 thf(f849,plain,(
% 8.60/1.67 ( ! [X1 : (list_char > paraco1605129243lle_tv)] : (((((^[Y0 : list_char > paraco1605129243lle_tv]: ((paraco1344940915le_Det @ $true) = (paraco1325918602e_eval @ Y0 @ (paraco445776468le_Neg @ p)))) @ X1)) = $true)) )),
% 8.60/1.67 inference(pi_proxy_clausification,[],[f848])).
% 8.60/1.67 thf(f850,plain,(
% 8.60/1.67 ( ! [X1 : (list_char > paraco1605129243lle_tv)] : (((((paraco1344940915le_Det @ $true) = (paraco1325918602e_eval @ X1 @ (paraco445776468le_Neg @ p)))) = $true)) )),
% 8.60/1.67 inference(beta-eta_normalization,[],[f849])).
% 8.60/1.67 thf(f851,plain,(
% 8.60/1.67 ( ! [X1 : (list_char > paraco1605129243lle_tv)] : ((((paraco1325918602e_eval @ X1 @ (paraco445776468le_Neg @ p))) = ((paraco1344940915le_Det @ $true)))) )),
% 8.60/1.67 inference(equality_proxy_clausification,[],[f850])).
% 8.60/1.67 thf(f862,plain,(
% 8.60/1.67 (((paraco1344940915le_Det @ $true)) != ((paraco1344940915le_Det @ $false)))),
% 8.60/1.67 inference(unit_resulting_resolution,[],[f843,f835,f835])).
% 8.60/1.67 thf(f1893,plain,(
% 8.60/1.67 ( ! [X0 : (list_char > paraco1605129243lle_tv)] : ((((paraco1344940915le_Det @ $false)) = ((paraco1325918602e_eval @ X0 @ (paraco445776468le_Neg @ p)))) | (((paraco1344940915le_Det @ $true)) != ((paraco1344940915le_Det @ $true))) | (((paraco1344940915le_Det @ $true)) = ((paraco1344940915le_Det @ $false)))) )),
% 8.60/1.67 inference(constrained_superposition,[],[f823,f826])).
% 8.60/1.67 thf(f1906,plain,(
% 8.60/1.67 ( ! [X0 : (list_char > paraco1605129243lle_tv)] : ((((paraco1344940915le_Det @ $true)) = ((paraco1344940915le_Det @ $false))) | (((paraco1344940915le_Det @ $false)) = ((paraco1325918602e_eval @ X0 @ (paraco445776468le_Neg @ p))))) )),
% 8.60/1.67 inference(trivial_inequality_removal,[],[f1893])).
% 8.60/1.67 thf(f1912,plain,(
% 8.60/1.67 ( ! [X0 : (list_char > paraco1605129243lle_tv)] : ((((paraco1344940915le_Det @ $false)) = ((paraco1325918602e_eval @ X0 @ (paraco445776468le_Neg @ p))))) )),
% 8.60/1.67 inference(forward_subsumption_resolution,[],[f1906,f862])).
% 8.60/1.67 thf(f1919,plain,(
% 8.60/1.67 (((paraco1344940915le_Det @ $true)) = ((paraco1344940915le_Det @ $false)))),
% 8.60/1.67 inference(constrained_superposition,[],[f1912,f851])).
% 8.60/1.67 thf(f1940,plain,(
% 8.60/1.67 $false),
% 8.60/1.67 inference(forward_subsumption_resolution,[],[f1919,f862])).
% 8.60/1.67 % SZS output end Proof for theBenchmark
% 8.60/1.67 % (1107248)------------------------------
% 8.60/1.67 % (1107248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.60/1.67 % (1107248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/1.67 % (1107248)CaDiCaL version: 2.1.3
% 8.60/1.67 % (1107248)Termination reason: Refutation
% 8.60/1.67 % (1107248)Time elapsed: 0.074 s
% 8.60/1.67 % (1107248)Peak memory usage: 14 MB
% 8.60/1.67 % (1107248)Instructions burned: 143 (million)
% 8.60/1.67 % (1107049)Success in time 1.396 s
% 8.60/1.67 % Vampire exiting
%------------------------------------------------------------------------------