%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO338^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:47:28 AM UTC 2026
% Result : Theorem 7.39s 1.48s
% Output : Refutation 7.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO338^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n003.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 16:49:44 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.09/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.36 % (2740084)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.82/0.36 % (2740094)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=980414556:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.82/0.36 % (2740095)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.82/0.36 % (2740095)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.82/0.36 % (2740090)lrs+10_16_si=on:nwc=1.5:random_seed=3294943284:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.82/0.36 % (2740089)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1231265788:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.82/0.36 % (2740091)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1132290099:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.82/0.36 % (2740092)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=2280411284: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.82/0.36 % (2740093)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3483508523:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.82/0.36 % (2740095)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=1888839146:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.82/0.36 % (2740091)Instruction limit reached!
% 0.82/0.36 % (2740091)------------------------------
% 0.82/0.36 % (2740091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.36 % (2740091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.36 % (2740091)CaDiCaL version: 2.1.3
% 0.82/0.36 % (2740091)Termination reason: Instruction limit
% 0.82/0.36 % (2740091)Termination phase: Saturation
% 0.82/0.36 % (2740091)Time elapsed: 0.002 s
% 0.82/0.36 % (2740091)Peak memory usage: 11 MB
% 0.82/0.36 % (2740091)Instructions burned: 3 (million)
% 0.82/0.36 % (2740090)Instruction limit reached!
% 0.82/0.36 % (2740090)------------------------------
% 0.82/0.36 % (2740090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.36 % (2740090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.36 % (2740090)CaDiCaL version: 2.1.3
% 0.82/0.36 % (2740090)Termination reason: Instruction limit
% 0.82/0.36 % (2740090)Termination phase: Saturation
% 0.82/0.36 % (2740090)Time elapsed: 0.010 s
% 0.82/0.36 % (2740090)Peak memory usage: 12 MB
% 0.82/0.36 % (2740090)Instructions burned: 18 (million)
% 0.82/0.36 % (2740093)Instruction limit reached!
% 0.82/0.36 % (2740093)------------------------------
% 0.82/0.36 % (2740093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.36 % (2740093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.36 % (2740093)CaDiCaL version: 2.1.3
% 0.82/0.36 % (2740093)Termination reason: Instruction limit
% 0.82/0.36 % (2740093)Termination phase: Saturation
% 0.82/0.36 % (2740093)Time elapsed: 0.014 s
% 0.82/0.36 % (2740093)Peak memory usage: 12 MB
% 0.82/0.36 % (2740093)Instructions burned: 25 (million)
% 0.82/0.36 % (2740094)Instruction limit reached!
% 0.82/0.36 % (2740094)------------------------------
% 0.82/0.36 % (2740094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.36 % (2740094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.36 % (2740094)CaDiCaL version: 2.1.3
% 0.82/0.36 % (2740094)Termination reason: Instruction limit
% 0.82/0.36 % (2740094)Termination phase: Saturation
% 0.82/0.36 % (2740094)Time elapsed: 0.022 s
% 0.82/0.36 % (2740094)Peak memory usage: 12 MB
% 0.82/0.36 % (2740094)Instructions burned: 79 (million)
% 0.82/0.36 % (2740103)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2399783982:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.82/0.36 % (2740103)Instruction limit reached!
% 0.82/0.36 % (2740103)------------------------------
% 0.82/0.36 % (2740103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.40 % (2740103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.40 % (2740103)CaDiCaL version: 2.1.3
% 0.82/0.40 % (2740103)Termination reason: Instruction limit
% 0.82/0.40 % (2740103)Termination phase: Saturation
% 0.82/0.40 % (2740103)Time elapsed: 0.002 s
% 0.82/0.40 % (2740103)Peak memory usage: 12 MB
% 0.82/0.40 % (2740103)Instructions burned: 3 (million)
% 0.82/0.40 % (2740106)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1460149641:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.82/0.40 % (2740104)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2331530623:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.82/0.40 % (2740106)Instruction limit reached!
% 0.82/0.40 % (2740106)------------------------------
% 0.82/0.40 % (2740106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.40 % (2740106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.40 % (2740106)CaDiCaL version: 2.1.3
% 0.82/0.40 % (2740106)Termination reason: Instruction limit
% 0.82/0.40 % (2740106)Termination phase: Saturation
% 0.82/0.40 % (2740106)Time elapsed: 0.004 s
% 0.82/0.40 % (2740106)Peak memory usage: 12 MB
% 0.82/0.40 % (2740106)Instructions burned: 13 (million)
% 0.82/0.40 % (2740105)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.82/0.40 % (2740104)Instruction limit reached!
% 0.82/0.40 % (2740104)------------------------------
% 0.82/0.40 % (2740104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.40 % (2740104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.40 % (2740104)CaDiCaL version: 2.1.3
% 0.82/0.40 % (2740104)Termination reason: Instruction limit
% 0.82/0.40 % (2740104)Termination phase: Saturation
% 0.82/0.40 % (2740104)Time elapsed: 0.003 s
% 0.82/0.40 % (2740104)Peak memory usage: 12 MB
% 0.82/0.40 % (2740104)Instructions burned: 5 (million)
% 0.82/0.40 % (2740105)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=37779042:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.82/0.40 % (2740108)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.82/0.40 % (2740108)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.82/0.40 % (2740105)Instruction limit reached!
% 0.82/0.40 % (2740105)------------------------------
% 0.82/0.40 % (2740105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.40 % (2740105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.40 % (2740105)CaDiCaL version: 2.1.3
% 0.82/0.40 % (2740105)Termination reason: Instruction limit
% 0.82/0.40 % (2740105)Termination phase: Saturation
% 0.82/0.40 % (2740105)Time elapsed: 0.004 s
% 0.82/0.40 % (2740105)Peak memory usage: 12 MB
% 0.82/0.40 % (2740105)Instructions burned: 8 (million)
% 0.82/0.40 % (2740111)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=3193376763:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.82/0.40 % (2740108)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=156628899: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.82/0.40 % (2740089)Instruction limit reached!
% 0.82/0.40 % (2740089)------------------------------
% 0.82/0.40 % (2740089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.40 % (2740089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.40 % (2740089)CaDiCaL version: 2.1.3
% 0.82/0.40 % (2740089)Termination reason: Instruction limit
% 0.82/0.40 % (2740089)Termination phase: Saturation
% 0.82/0.40 % (2740089)Time elapsed: 0.046 s
% 0.82/0.40 % (2740089)Peak memory usage: 12 MB
% 0.82/0.40 % (2740089)Instructions burned: 87 (million)
% 0.82/0.40 % (2740112)lrs+10_1_si=on:cs=on:random_seed=3755957582:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.82/0.40 % (2740114)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.82/0.44 % (2740112)Instruction limit reached!
% 0.82/0.44 % (2740112)------------------------------
% 0.82/0.44 % (2740112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.44 % (2740112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.44 % (2740112)CaDiCaL version: 2.1.3
% 0.82/0.44 % (2740112)Termination reason: Instruction limit
% 0.82/0.44 % (2740112)Termination phase: Saturation
% 0.82/0.44 % (2740112)Time elapsed: 0.005 s
% 0.82/0.44 % (2740112)Peak memory usage: 12 MB
% 0.82/0.44 % (2740112)Instructions burned: 8 (million)
% 0.82/0.44 % (2740108)Instruction limit reached!
% 0.82/0.44 % (2740108)------------------------------
% 0.82/0.44 % (2740108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.44 % (2740108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.44 % (2740108)CaDiCaL version: 2.1.3
% 0.82/0.44 % (2740108)Termination reason: Instruction limit
% 0.82/0.44 % (2740108)Termination phase: Saturation
% 0.82/0.44 % (2740108)Time elapsed: 0.015 s
% 0.82/0.44 % (2740108)Peak memory usage: 12 MB
% 0.82/0.44 % (2740108)Instructions burned: 29 (million)
% 0.82/0.44 % (2740114)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=1939291788:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.82/0.44 % (2740114)Instruction limit reached!
% 0.82/0.44 % (2740114)------------------------------
% 0.82/0.44 % (2740114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.44 % (2740114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.44 % (2740114)CaDiCaL version: 2.1.3
% 0.82/0.44 % (2740114)Termination reason: Instruction limit
% 0.82/0.44 % (2740114)Termination phase: Saturation
% 0.82/0.44 % (2740114)Time elapsed: 0.003 s
% 0.82/0.44 % (2740114)Peak memory usage: 11 MB
% 0.82/0.44 % (2740114)Instructions burned: 6 (million)
% 0.82/0.44 % (2740111)Instruction limit reached!
% 0.82/0.44 % (2740111)------------------------------
% 0.82/0.44 % (2740111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.44 % (2740111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.44 % (2740111)CaDiCaL version: 2.1.3
% 0.82/0.44 % (2740111)Termination reason: Instruction limit
% 0.82/0.44 % (2740111)Termination phase: Saturation
% 0.82/0.44 % (2740111)Time elapsed: 0.023 s
% 0.82/0.44 % (2740111)Peak memory usage: 12 MB
% 0.82/0.44 % (2740111)Instructions burned: 87 (million)
% 0.82/0.44 % (2740117)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=183060638:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.82/0.44 % (2740119)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2258343767:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.82/0.44 % (2740123)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3310146663:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.82/0.44 % (2740121)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=956368716:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.82/0.44 % (2740122)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3454894994:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.82/0.44 % (2740095)Instruction limit reached!
% 0.82/0.44 % (2740095)------------------------------
% 0.82/0.44 % (2740095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.44 % (2740095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.44 % (2740095)CaDiCaL version: 2.1.3
% 0.82/0.44 % (2740095)Termination reason: Instruction limit
% 0.82/0.44 % (2740095)Termination phase: Saturation
% 0.82/0.44 % (2740095)Time elapsed: 0.082 s
% 0.82/0.44 % (2740095)Peak memory usage: 13 MB
% 0.82/0.44 % (2740095)Instructions burned: 158 (million)
% 0.82/0.44 % (2740117)Instruction limit reached!
% 0.82/0.44 % (2740117)------------------------------
% 0.82/0.44 % (2740117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.44 % (2740117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.49 % (2740117)CaDiCaL version: 2.1.3
% 1.54/0.49 % (2740117)Termination reason: Instruction limit
% 1.54/0.49 % (2740117)Termination phase: Saturation
% 1.54/0.49 % (2740117)Time elapsed: 0.023 s
% 1.54/0.49 % (2740117)Peak memory usage: 12 MB
% 1.54/0.49 % (2740117)Instructions burned: 42 (million)
% 1.54/0.49 % (2740122)Instruction limit reached!
% 1.54/0.49 % (2740122)------------------------------
% 1.54/0.49 % (2740122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.49 % (2740122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.49 % (2740122)CaDiCaL version: 2.1.3
% 1.54/0.49 % (2740122)Termination reason: Instruction limit
% 1.54/0.49 % (2740122)Termination phase: Saturation
% 1.54/0.49 % (2740122)Time elapsed: 0.009 s
% 1.54/0.49 % (2740122)Peak memory usage: 12 MB
% 1.54/0.49 % (2740122)Instructions burned: 15 (million)
% 1.54/0.49 % (2740121)Instruction limit reached!
% 1.54/0.49 % (2740121)------------------------------
% 1.54/0.49 % (2740121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.49 % (2740121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.49 % (2740121)CaDiCaL version: 2.1.3
% 1.54/0.49 % (2740121)Termination reason: Instruction limit
% 1.54/0.49 % (2740121)Termination phase: Saturation
% 1.54/0.49 % (2740121)Time elapsed: 0.014 s
% 1.54/0.49 % (2740121)Peak memory usage: 12 MB
% 1.54/0.49 % (2740121)Instructions burned: 25 (million)
% 1.54/0.49 % (2740129)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1273597956:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.54/0.49 % (2740130)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3572347888: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.54/0.49 % (2740131)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3160062612:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.54/0.49 % (2740132)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1755446963:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.54/0.49 % (2740130)Instruction limit reached!
% 1.54/0.49 % (2740130)------------------------------
% 1.54/0.49 % (2740130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.49 % (2740130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.49 % (2740130)CaDiCaL version: 2.1.3
% 1.54/0.49 % (2740130)Termination reason: Instruction limit
% 1.54/0.49 % (2740130)Termination phase: Saturation
% 1.54/0.49 % (2740130)Time elapsed: 0.002 s
% 1.54/0.49 % (2740130)Peak memory usage: 12 MB
% 1.54/0.49 % (2740130)Instructions burned: 3 (million)
% 1.54/0.49 % (2740129)Instruction limit reached!
% 1.54/0.49 % (2740129)------------------------------
% 1.54/0.49 % (2740129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.49 % (2740129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.49 % (2740129)CaDiCaL version: 2.1.3
% 1.54/0.49 % (2740129)Termination reason: Instruction limit
% 1.54/0.49 % (2740129)Termination phase: Saturation
% 1.54/0.49 % (2740129)Time elapsed: 0.008 s
% 1.54/0.49 % (2740129)Peak memory usage: 12 MB
% 1.54/0.49 % (2740129)Instructions burned: 14 (million)
% 1.54/0.49 % (2740132)Instruction limit reached!
% 1.54/0.49 % (2740132)------------------------------
% 1.54/0.49 % (2740132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.49 % (2740132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.49 % (2740132)CaDiCaL version: 2.1.3
% 1.54/0.49 % (2740132)Termination reason: Instruction limit
% 1.54/0.49 % (2740132)Termination phase: Saturation
% 1.54/0.49 % (2740132)Time elapsed: 0.012 s
% 1.54/0.49 % (2740132)Peak memory usage: 11 MB
% 1.54/0.49 % (2740132)Instructions burned: 23 (million)
% 1.54/0.49 % (2740131)Instruction limit reached!
% 1.54/0.49 % (2740131)------------------------------
% 1.54/0.49 % (2740131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.49 % (2740131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.49 % (2740131)CaDiCaL version: 2.1.3
% 1.54/0.49 % (2740131)Termination reason: Instruction limit
% 1.54/0.49 % (2740131)Termination phase: Saturation
% 1.54/0.49 % (2740131)Time elapsed: 0.014 s
% 1.54/0.49 % (2740131)Peak memory usage: 12 MB
% 1.54/0.49 % (2740131)Instructions burned: 26 (million)
% 1.54/0.52 % (2740138)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.54/0.52 % (2740138)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.54/0.52 % (2740137)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=4231145600:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.54/0.52 % (2740138)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=2209555158:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.54/0.52 % (2740139)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.54/0.52 % (2740138)Instruction limit reached!
% 1.54/0.52 % (2740138)------------------------------
% 1.54/0.52 % (2740138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.52 % (2740138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.52 % (2740138)CaDiCaL version: 2.1.3
% 1.54/0.52 % (2740138)Termination reason: Instruction limit
% 1.54/0.52 % (2740138)Termination phase: Saturation
% 1.54/0.52 % (2740138)Time elapsed: 0.008 s
% 1.54/0.52 % (2740138)Peak memory usage: 12 MB
% 1.54/0.52 % (2740138)Instructions burned: 16 (million)
% 1.54/0.52 % (2740139)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=3141633261:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.54/0.52 % (2740140)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=2142654123:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.54/0.52 % (2740139)Instruction limit reached!
% 1.54/0.52 % (2740139)------------------------------
% 1.54/0.52 % (2740139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.52 % (2740139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.52 % (2740139)CaDiCaL version: 2.1.3
% 1.54/0.52 % (2740139)Termination reason: Instruction limit
% 1.54/0.52 % (2740139)Termination phase: Saturation
% 1.54/0.52 % (2740139)Time elapsed: 0.005 s
% 1.54/0.52 % (2740139)Peak memory usage: 12 MB
% 1.54/0.52 % (2740139)Instructions burned: 8 (million)
% 1.54/0.52 % (2740140)Instruction limit reached!
% 1.54/0.52 % (2740140)------------------------------
% 1.54/0.52 % (2740140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.52 % (2740140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.52 % (2740140)CaDiCaL version: 2.1.3
% 1.54/0.52 % (2740140)Termination reason: Instruction limit
% 1.54/0.52 % (2740140)Termination phase: Saturation
% 1.54/0.52 % (2740140)Time elapsed: 0.016 s
% 1.54/0.52 % (2740140)Peak memory usage: 12 MB
% 1.54/0.52 % (2740140)Instructions burned: 31 (million)
% 1.54/0.52 % (2740143)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3376059152:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.54/0.52 % (2740137)Instruction limit reached!
% 1.54/0.52 % (2740137)------------------------------
% 1.54/0.52 % (2740137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.52 % (2740137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.52 % (2740137)CaDiCaL version: 2.1.3
% 1.54/0.52 % (2740137)Termination reason: Instruction limit
% 1.54/0.52 % (2740137)Termination phase: Saturation
% 1.54/0.52 % (2740137)Time elapsed: 0.033 s
% 1.54/0.52 % (2740137)Peak memory usage: 12 MB
% 1.54/0.52 % (2740137)Instructions burned: 62 (million)
% 1.54/0.52 % (2740123)Instruction limit reached!
% 1.54/0.52 % (2740123)------------------------------
% 1.54/0.52 % (2740123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.52 % (2740123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.52 % (2740123)CaDiCaL version: 2.1.3
% 1.54/0.52 % (2740123)Termination reason: Instruction limit
% 1.54/0.52 % (2740123)Termination phase: Saturation
% 1.54/0.52 % (2740123)Time elapsed: 0.089 s
% 1.54/0.52 % (2740123)Peak memory usage: 13 MB
% 1.54/0.52 % (2740123)Instructions burned: 329 (million)
% 2.27/0.59 % (2740146)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=4002748447:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.27/0.59 % (2740143)Instruction limit reached!
% 2.27/0.59 % (2740143)------------------------------
% 2.27/0.59 % (2740143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.59 % (2740143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.59 % (2740143)CaDiCaL version: 2.1.3
% 2.27/0.59 % (2740143)Termination reason: Instruction limit
% 2.27/0.59 % (2740143)Termination phase: Saturation
% 2.27/0.59 % (2740143)Time elapsed: 0.006 s
% 2.27/0.59 % (2740143)Peak memory usage: 12 MB
% 2.27/0.59 % (2740143)Instructions burned: 8 (million)
% 2.27/0.59 % (2740146)Instruction limit reached!
% 2.27/0.59 % (2740146)------------------------------
% 2.27/0.59 % (2740146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.59 % (2740146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.59 % (2740146)CaDiCaL version: 2.1.3
% 2.27/0.59 % (2740146)Termination reason: Instruction limit
% 2.27/0.59 % (2740146)Termination phase: Saturation
% 2.27/0.59 % (2740146)Time elapsed: 0.010 s
% 2.27/0.59 % (2740146)Peak memory usage: 11 MB
% 2.27/0.59 % (2740146)Instructions burned: 25 (million)
% 2.27/0.59 % (2740147)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2113947774:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.27/0.59 % (2740152)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2634760190:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.27/0.59 % (2740149)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=338869879:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.27/0.59 % (2740151)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=334249636:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.27/0.59 % (2740147)Instruction limit reached!
% 2.27/0.59 % (2740147)------------------------------
% 2.27/0.59 % (2740147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.59 % (2740147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.59 % (2740147)CaDiCaL version: 2.1.3
% 2.27/0.59 % (2740147)Termination reason: Instruction limit
% 2.27/0.59 % (2740147)Termination phase: Saturation
% 2.27/0.59 % (2740147)Time elapsed: 0.012 s
% 2.27/0.59 % (2740147)Peak memory usage: 12 MB
% 2.27/0.59 % (2740147)Instructions burned: 21 (million)
% 2.27/0.59 % (2740153)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3825948322:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 2.27/0.59 % (2740119)Instruction limit reached!
% 2.27/0.59 % (2740119)------------------------------
% 2.27/0.59 % (2740119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.59 % (2740119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.59 % (2740119)CaDiCaL version: 2.1.3
% 2.27/0.59 % (2740119)Termination reason: Instruction limit
% 2.27/0.59 % (2740119)Termination phase: Saturation
% 2.27/0.59 % (2740119)Time elapsed: 0.127 s
% 2.27/0.59 % (2740119)Peak memory usage: 13 MB
% 2.27/0.59 % (2740119)Instructions burned: 250 (million)
% 2.27/0.59 % (2740158)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.27/0.59 % (2740092)Instruction limit reached!
% 2.27/0.59 % (2740092)------------------------------
% 2.27/0.59 % (2740092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.59 % (2740092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.59 % (2740092)CaDiCaL version: 2.1.3
% 2.27/0.59 % (2740092)Termination reason: Instruction limit
% 2.27/0.59 % (2740092)Termination phase: Saturation
% 2.27/0.59 % (2740092)Time elapsed: 0.207 s
% 2.27/0.59 % (2740092)Peak memory usage: 12 MB
% 2.27/0.59 % (2740092)Instructions burned: 637 (million)
% 2.27/0.59 % (2740158)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3937524352:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.27/0.59 % (2740158)Instruction limit reached!
% 2.27/0.59 % (2740158)------------------------------
% 2.27/0.59 % (2740158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.67 % (2740158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.67 % (2740158)CaDiCaL version: 2.1.3
% 2.60/0.67 % (2740158)Termination reason: Instruction limit
% 2.60/0.67 % (2740158)Termination phase: Saturation
% 2.60/0.67 % (2740158)Time elapsed: 0.004 s
% 2.60/0.67 % (2740158)Peak memory usage: 12 MB
% 2.60/0.67 % (2740158)Instructions burned: 8 (million)
% 2.60/0.67 % (2740153)Instruction limit reached!
% 2.60/0.67 % (2740153)------------------------------
% 2.60/0.67 % (2740153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.67 % (2740153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.67 % (2740153)CaDiCaL version: 2.1.3
% 2.60/0.67 % (2740153)Termination reason: Instruction limit
% 2.60/0.67 % (2740153)Termination phase: Saturation
% 2.60/0.67 % (2740153)Time elapsed: 0.023 s
% 2.60/0.67 % (2740153)Peak memory usage: 12 MB
% 2.60/0.67 % (2740153)Instructions burned: 42 (million)
% 2.60/0.67 % (2740160)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=333138842:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.60/0.67 % (2740161)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=1913157641:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.60/0.67 % (2740163)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.60/0.67 % (2740163)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=465433142:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.60/0.67 % (2740152)Instruction limit reached!
% 2.60/0.67 % (2740152)------------------------------
% 2.60/0.67 % (2740152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.67 % (2740152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.67 % (2740152)CaDiCaL version: 2.1.3
% 2.60/0.67 % (2740152)Termination reason: Instruction limit
% 2.60/0.67 % (2740152)Termination phase: Saturation
% 2.60/0.67 % (2740152)Time elapsed: 0.054 s
% 2.60/0.67 % (2740152)Peak memory usage: 13 MB
% 2.60/0.67 % (2740152)Instructions burned: 195 (million)
% 2.60/0.67 % (2740163)Instruction limit reached!
% 2.60/0.67 % (2740163)------------------------------
% 2.60/0.67 % (2740163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.67 % (2740163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.67 % (2740163)CaDiCaL version: 2.1.3
% 2.60/0.67 % (2740163)Termination reason: Instruction limit
% 2.60/0.67 % (2740163)Termination phase: Saturation
% 2.60/0.67 % (2740163)Time elapsed: 0.003 s
% 2.60/0.67 % (2740163)Peak memory usage: 11 MB
% 2.60/0.67 % (2740163)Instructions burned: 6 (million)
% 2.60/0.67 % (2740164)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=510463018:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.60/0.67 % (2740168)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2344718991:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.60/0.67 % (2740164)Instruction limit reached!
% 2.60/0.67 % (2740164)------------------------------
% 2.60/0.67 % (2740164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.67 % (2740164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.67 % (2740164)CaDiCaL version: 2.1.3
% 2.60/0.67 % (2740164)Termination reason: Instruction limit
% 2.60/0.67 % (2740164)Termination phase: Saturation
% 2.60/0.67 % (2740164)Time elapsed: 0.009 s
% 2.60/0.67 % (2740164)Peak memory usage: 12 MB
% 2.60/0.67 % (2740164)Instructions burned: 22 (million)
% 2.60/0.67 % (2740168)Instruction limit reached!
% 2.60/0.67 % (2740168)------------------------------
% 2.60/0.67 % (2740168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.67 % (2740168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.67 % (2740168)CaDiCaL version: 2.1.3
% 2.60/0.67 % (2740168)Termination reason: Instruction limit
% 2.60/0.67 % (2740168)Termination phase: Saturation
% 2.60/0.67 % (2740168)Time elapsed: 0.006 s
% 2.60/0.67 % (2740168)Peak memory usage: 12 MB
% 3.02/0.79 % (2740168)Instructions burned: 22 (million)
% 3.02/0.79 % (2740169)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=1483814449:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 3.02/0.79 % (2740151)Instruction limit reached!
% 3.02/0.79 % (2740151)------------------------------
% 3.02/0.79 % (2740151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.02/0.79 % (2740151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/0.79 % (2740151)CaDiCaL version: 2.1.3
% 3.02/0.79 % (2740151)Termination reason: Instruction limit
% 3.02/0.79 % (2740151)Termination phase: Saturation
% 3.02/0.79 % (2740151)Time elapsed: 0.075 s
% 3.02/0.79 % (2740151)Peak memory usage: 13 MB
% 3.02/0.79 % (2740151)Instructions burned: 143 (million)
% 3.02/0.79 % (2740173)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=4237158369:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 3.02/0.79 % (2740172)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=3927800699:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 3.02/0.79 % (2740173)Instruction limit reached!
% 3.02/0.79 % (2740173)------------------------------
% 3.02/0.79 % (2740173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.02/0.79 % (2740173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/0.79 % (2740173)CaDiCaL version: 2.1.3
% 3.02/0.79 % (2740173)Termination reason: Instruction limit
% 3.02/0.79 % (2740173)Termination phase: Saturation
% 3.02/0.79 % (2740173)Time elapsed: 0.014 s
% 3.02/0.79 % (2740173)Peak memory usage: 12 MB
% 3.02/0.79 % (2740173)Instructions burned: 47 (million)
% 3.02/0.79 % (2740176)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2698198601:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 3.02/0.79 % (2740178)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=4019748110:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2997 on theBenchmark for (2997ds/21Mi)
% 3.02/0.79 % (2740178)Instruction limit reached!
% 3.02/0.79 % (2740178)------------------------------
% 3.02/0.79 % (2740178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.02/0.79 % (2740178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/0.79 % (2740178)CaDiCaL version: 2.1.3
% 3.02/0.79 % (2740178)Termination reason: Instruction limit
% 3.02/0.79 % (2740178)Termination phase: Saturation
% 3.02/0.79 % (2740178)Time elapsed: 0.007 s
% 3.02/0.79 % (2740178)Peak memory usage: 12 MB
% 3.02/0.79 % (2740178)Instructions burned: 24 (million)
% 3.02/0.79 % (2740181)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.02/0.79 % (2740181)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=213338903:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.02/0.79 % (2740161)Instruction limit reached!
% 3.02/0.79 % (2740161)------------------------------
% 3.02/0.79 % (2740161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.02/0.79 % (2740161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/0.79 % (2740161)CaDiCaL version: 2.1.3
% 3.02/0.79 % (2740161)Termination reason: Instruction limit
% 3.02/0.79 % (2740161)Termination phase: Saturation
% 3.02/0.79 % (2740161)Time elapsed: 0.082 s
% 3.02/0.79 % (2740161)Peak memory usage: 12 MB
% 3.02/0.79 % (2740161)Instructions burned: 170 (million)
% 3.02/0.79 % (2740160)Instruction limit reached!
% 3.02/0.79 % (2740160)------------------------------
% 3.02/0.79 % (2740160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.02/0.79 % (2740160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/0.79 % (2740160)CaDiCaL version: 2.1.3
% 3.02/0.79 % (2740160)Termination reason: Instruction limit
% 3.02/0.79 % (2740160)Termination phase: Saturation
% 3.02/0.79 % (2740160)Time elapsed: 0.093 s
% 4.22/0.97 % (2740160)Peak memory usage: 13 MB
% 4.22/0.97 % (2740160)Instructions burned: 182 (million)
% 4.22/0.97 % (2740183)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2022397556:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 4.22/0.97 % (2740184)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=108629378:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 4.22/0.97 % (2740183)Instruction limit reached!
% 4.22/0.97 % (2740183)------------------------------
% 4.22/0.97 % (2740183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.22/0.97 % (2740183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/0.97 % (2740183)CaDiCaL version: 2.1.3
% 4.22/0.97 % (2740183)Termination reason: Instruction limit
% 4.22/0.97 % (2740183)Termination phase: Saturation
% 4.22/0.97 % (2740183)Time elapsed: 0.007 s
% 4.22/0.97 % (2740183)Peak memory usage: 12 MB
% 4.22/0.97 % (2740183)Instructions burned: 13 (million)
% 4.22/0.97 % (2740187)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1719149381:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 4.22/0.97 % (2740181)Instruction limit reached!
% 4.22/0.97 % (2740181)------------------------------
% 4.22/0.97 % (2740181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.22/0.97 % (2740181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/0.97 % (2740181)CaDiCaL version: 2.1.3
% 4.22/0.97 % (2740181)Termination reason: Instruction limit
% 4.22/0.97 % (2740181)Termination phase: Saturation
% 4.22/0.97 % (2740181)Time elapsed: 0.052 s
% 4.22/0.97 % (2740181)Peak memory usage: 12 MB
% 4.22/0.97 % (2740181)Instructions burned: 202 (million)
% 4.22/0.97 % (2740189)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=4005426731:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 4.22/0.97 % (2740184)Instruction limit reached!
% 4.22/0.97 % (2740184)------------------------------
% 4.22/0.97 % (2740184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.22/0.97 % (2740184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/0.97 % (2740184)CaDiCaL version: 2.1.3
% 4.22/0.97 % (2740184)Termination reason: Instruction limit
% 4.22/0.97 % (2740184)Termination phase: Saturation
% 4.22/0.97 % (2740184)Time elapsed: 0.037 s
% 4.22/0.97 % (2740184)Peak memory usage: 13 MB
% 4.22/0.97 % (2740184)Instructions burned: 66 (million)
% 4.22/0.97 % (2740189)Instruction limit reached!
% 4.22/0.97 % (2740189)------------------------------
% 4.22/0.97 % (2740189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.22/0.97 % (2740189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/0.97 % (2740189)CaDiCaL version: 2.1.3
% 4.22/0.97 % (2740189)Termination reason: Instruction limit
% 4.22/0.97 % (2740189)Termination phase: Saturation
% 4.22/0.97 % (2740189)Time elapsed: 0.009 s
% 4.22/0.97 % (2740189)Peak memory usage: 12 MB
% 4.22/0.97 % (2740189)Instructions burned: 35 (million)
% 4.22/0.97 % (2740187)Instruction limit reached!
% 4.22/0.97 % (2740187)------------------------------
% 4.22/0.97 % (2740187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.22/0.97 % (2740187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/0.97 % (2740187)CaDiCaL version: 2.1.3
% 4.22/0.97 % (2740187)Termination reason: Instruction limit
% 4.22/0.97 % (2740187)Termination phase: Saturation
% 4.22/0.97 % (2740187)Time elapsed: 0.027 s
% 4.22/0.97 % (2740187)Peak memory usage: 12 MB
% 4.22/0.97 % (2740187)Instructions burned: 51 (million)
% 4.22/0.97 % (2740191)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1050819073:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2996 on theBenchmark for (2996ds/137Mi)
% 4.22/0.97 % (2740192)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=1171491430:cond=on:i=34:hud=10:nm=10:rtra=on_2996 on theBenchmark for (2996ds/34Mi)
% 4.22/0.97 % (2740192)Instruction limit reached!
% 4.22/0.97 % (2740192)------------------------------
% 4.22/0.97 % (2740192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.22/0.97 % (2740192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.05 % (2740192)CaDiCaL version: 2.1.3
% 5.60/1.05 % (2740192)Termination reason: Instruction limit
% 5.60/1.05 % (2740192)Termination phase: Saturation
% 5.60/1.05 % (2740192)Time elapsed: 0.010 s
% 5.60/1.05 % (2740192)Peak memory usage: 12 MB
% 5.60/1.05 % (2740192)Instructions burned: 35 (million)
% 5.60/1.05 % (2740193)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=1630009738:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 5.60/1.05 % (2740196)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.60/1.05 % (2740196)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2304264183:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 5.60/1.05 % (2740169)Instruction limit reached!
% 5.60/1.05 % (2740169)------------------------------
% 5.60/1.05 % (2740169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.60/1.05 % (2740169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.05 % (2740169)CaDiCaL version: 2.1.3
% 5.60/1.05 % (2740169)Termination reason: Instruction limit
% 5.60/1.05 % (2740169)Termination phase: Saturation
% 5.60/1.05 % (2740169)Time elapsed: 0.162 s
% 5.60/1.05 % (2740169)Peak memory usage: 14 MB
% 5.60/1.05 % (2740169)Instructions burned: 317 (million)
% 5.60/1.05 % (2740199)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=686929753:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 5.60/1.05 % (2740193)Instruction limit reached!
% 5.60/1.05 % (2740193)------------------------------
% 5.60/1.05 % (2740193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.60/1.05 % (2740193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.05 % (2740193)CaDiCaL version: 2.1.3
% 5.60/1.05 % (2740193)Termination reason: Instruction limit
% 5.60/1.05 % (2740193)Termination phase: Saturation
% 5.60/1.05 % (2740193)Time elapsed: 0.036 s
% 5.60/1.05 % (2740193)Peak memory usage: 12 MB
% 5.60/1.05 % (2740193)Instructions burned: 67 (million)
% 5.60/1.05 % (2740191)Instruction limit reached!
% 5.60/1.05 % (2740191)------------------------------
% 5.60/1.05 % (2740191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.60/1.05 % (2740191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.05 % (2740191)CaDiCaL version: 2.1.3
% 5.60/1.05 % (2740191)Termination reason: Instruction limit
% 5.60/1.05 % (2740191)Termination phase: Saturation
% 5.60/1.05 % (2740191)Time elapsed: 0.061 s
% 5.60/1.05 % (2740191)Peak memory usage: 12 MB
% 5.60/1.05 % (2740191)Instructions burned: 137 (million)
% 5.60/1.05 % (2740196)Instruction limit reached!
% 5.60/1.05 % (2740196)------------------------------
% 5.60/1.05 % (2740196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.60/1.05 % (2740196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.05 % (2740196)CaDiCaL version: 2.1.3
% 5.60/1.05 % (2740196)Termination reason: Instruction limit
% 5.60/1.05 % (2740196)Termination phase: Saturation
% 5.60/1.05 % (2740196)Time elapsed: 0.047 s
% 5.60/1.05 % (2740196)Peak memory usage: 13 MB
% 5.60/1.05 % (2740196)Instructions burned: 184 (million)
% 5.60/1.05 % (2740201)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=125097452:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 5.60/1.05 % (2740203)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1022165309:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 5.60/1.05 % (2740202)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=4083223102:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 5.60/1.05 % (2740201)Instruction limit reached!
% 5.60/1.05 % (2740201)------------------------------
% 5.60/1.05 % (2740201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.60/1.05 % (2740201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.05 % (2740201)CaDiCaL version: 2.1.3
% 5.60/1.05 % (2740201)Termination reason: Instruction limit
% 5.60/1.05 % (2740201)Termination phase: Saturation
% 5.60/1.05 % (2740201)Time elapsed: 0.050 s
% 5.60/1.05 % (2740201)Peak memory usage: 12 MB
% 5.60/1.05 % (2740201)Instructions burned: 96 (million)
% 5.60/1.05 % (2740176)Instruction limit reached!
% 5.60/1.05 % (2740176)------------------------------
% 5.60/1.05 % (2740176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.14 % (2740176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.14 % (2740176)CaDiCaL version: 2.1.3
% 5.98/1.14 % (2740176)Termination reason: Instruction limit
% 5.98/1.14 % (2740176)Termination phase: Saturation
% 5.98/1.14 % (2740176)Time elapsed: 0.238 s
% 5.98/1.14 % (2740176)Peak memory usage: 13 MB
% 5.98/1.14 % (2740176)Instructions burned: 480 (million)
% 5.98/1.14 % (2740207)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2152256015:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 5.98/1.14 % (2740208)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1123440201:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 5.98/1.14 % (2740199)Instruction limit reached!
% 5.98/1.14 % (2740199)------------------------------
% 5.98/1.14 % (2740199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.14 % (2740199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.14 % (2740199)CaDiCaL version: 2.1.3
% 5.98/1.14 % (2740199)Termination reason: Instruction limit
% 5.98/1.14 % (2740199)Termination phase: Saturation
% 5.98/1.14 % (2740199)Time elapsed: 0.125 s
% 5.98/1.14 % (2740199)Peak memory usage: 12 MB
% 5.98/1.14 % (2740199)Instructions burned: 246 (million)
% 5.98/1.14 % (2740211)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3909124539:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 5.98/1.14 % (2740211)Instruction limit reached!
% 5.98/1.14 % (2740211)------------------------------
% 5.98/1.14 % (2740211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.14 % (2740211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.14 % (2740211)CaDiCaL version: 2.1.3
% 5.98/1.14 % (2740211)Termination reason: Instruction limit
% 5.98/1.14 % (2740211)Termination phase: Saturation
% 5.98/1.14 % (2740211)Time elapsed: 0.023 s
% 5.98/1.14 % (2740211)Peak memory usage: 12 MB
% 5.98/1.14 % (2740211)Instructions burned: 45 (million)
% 5.98/1.14 % (2740208)Instruction limit reached!
% 5.98/1.14 % (2740208)------------------------------
% 5.98/1.14 % (2740208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.15 % (2740208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.15 % (2740208)CaDiCaL version: 2.1.3
% 5.98/1.15 % (2740208)Termination reason: Instruction limit
% 5.98/1.15 % (2740208)Termination phase: Saturation
% 5.98/1.15 % (2740208)Time elapsed: 0.067 s
% 5.98/1.15 % (2740208)Peak memory usage: 12 MB
% 5.98/1.15 % (2740208)Instructions burned: 131 (million)
% 5.98/1.15 % (2740213)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3723748301:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 5.98/1.15 % (2740214)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3904720258:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 5.98/1.15 % (2740172)Instruction limit reached!
% 5.98/1.15 % (2740172)------------------------------
% 5.98/1.15 % (2740172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.15 % (2740172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.15 % (2740172)CaDiCaL version: 2.1.3
% 5.98/1.15 % (2740172)Termination reason: Instruction limit
% 5.98/1.15 % (2740172)Termination phase: Saturation
% 5.98/1.15 % (2740172)Time elapsed: 0.411 s
% 5.98/1.15 % (2740172)Peak memory usage: 16 MB
% 5.98/1.15 % (2740172)Instructions burned: 853 (million)
% 5.98/1.15 % (2740202)Instruction limit reached!
% 5.98/1.15 % (2740202)------------------------------
% 5.98/1.15 % (2740202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.15 % (2740202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.15 % (2740202)CaDiCaL version: 2.1.3
% 5.98/1.15 % (2740202)Termination reason: Instruction limit
% 5.98/1.15 % (2740202)Termination phase: Saturation
% 5.98/1.15 % (2740202)Time elapsed: 0.215 s
% 5.98/1.15 % (2740202)Peak memory usage: 14 MB
% 5.98/1.15 % (2740202)Instructions burned: 427 (million)
% 5.98/1.15 % (2740203)Instruction limit reached!
% 5.98/1.15 % (2740203)------------------------------
% 5.98/1.15 % (2740203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.15 % (2740203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.26/1.27 % (2740203)CaDiCaL version: 2.1.3
% 6.26/1.27 % (2740203)Termination reason: Instruction limit
% 6.26/1.27 % (2740203)Termination phase: Saturation
% 6.26/1.27 % (2740203)Time elapsed: 0.225 s
% 6.26/1.27 % (2740203)Peak memory usage: 14 MB
% 6.26/1.27 % (2740203)Instructions burned: 878 (million)
% 6.26/1.27 % (2740217)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=476206787:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 6.26/1.27 % (2740218)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=1651434116:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2992 on theBenchmark for (2992ds/65Mi)
% 6.26/1.27 % (2740219)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=2651174046:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2992 on theBenchmark for (2992ds/105Mi)
% 6.26/1.27 % (2740218)Instruction limit reached!
% 6.26/1.27 % (2740218)------------------------------
% 6.26/1.27 % (2740218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.26/1.27 % (2740218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.26/1.27 % (2740218)CaDiCaL version: 2.1.3
% 6.26/1.27 % (2740218)Termination reason: Instruction limit
% 6.26/1.27 % (2740218)Termination phase: Saturation
% 6.26/1.27 % (2740218)Time elapsed: 0.035 s
% 6.26/1.27 % (2740218)Peak memory usage: 12 MB
% 6.26/1.27 % (2740218)Instructions burned: 66 (million)
% 6.26/1.27 % (2740219)Instruction limit reached!
% 6.26/1.27 % (2740219)------------------------------
% 6.26/1.27 % (2740219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.26/1.27 % (2740219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.26/1.27 % (2740219)CaDiCaL version: 2.1.3
% 6.26/1.27 % (2740219)Termination reason: Instruction limit
% 6.26/1.27 % (2740219)Termination phase: Saturation
% 6.26/1.27 % (2740219)Time elapsed: 0.037 s
% 6.26/1.27 % (2740219)Peak memory usage: 13 MB
% 6.26/1.27 % (2740219)Instructions burned: 106 (million)
% 6.26/1.27 % (2740217)Instruction limit reached!
% 6.26/1.27 % (2740217)------------------------------
% 6.26/1.27 % (2740217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.26/1.27 % (2740217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.26/1.27 % (2740217)CaDiCaL version: 2.1.3
% 6.26/1.27 % (2740217)Termination reason: Instruction limit
% 6.26/1.27 % (2740217)Termination phase: Saturation
% 6.26/1.27 % (2740217)Time elapsed: 0.054 s
% 6.26/1.27 % (2740217)Peak memory usage: 12 MB
% 6.26/1.27 % (2740217)Instructions burned: 96 (million)
% 6.26/1.27 % (2740223)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=4154857646:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2992 on theBenchmark for (2992ds/5755Mi)
% 6.26/1.27 % (2740224)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=4178516679:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 6.26/1.27 % (2740225)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2980322446:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/495Mi)
% 6.26/1.27 % (2740207)Instruction limit reached!
% 6.26/1.27 % (2740207)------------------------------
% 6.26/1.27 % (2740207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.26/1.27 % (2740207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.26/1.27 % (2740207)CaDiCaL version: 2.1.3
% 6.26/1.27 % (2740207)Termination reason: Instruction limit
% 6.26/1.27 % (2740207)Termination phase: Saturation
% 6.26/1.27 % (2740207)Time elapsed: 0.248 s
% 6.26/1.27 % (2740207)Peak memory usage: 18 MB
% 6.26/1.27 % (2740207)Instructions burned: 516 (million)
% 6.26/1.27 % (2740149)Instruction limit reached!
% 6.26/1.27 % (2740149)------------------------------
% 6.26/1.27 % (2740149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.26/1.27 % (2740149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.26/1.27 % (2740149)CaDiCaL version: 2.1.3
% 6.26/1.27 % (2740149)Termination reason: Instruction limit
% 6.73/1.36 % (2740149)Termination phase: Saturation
% 6.73/1.36 % (2740149)Time elapsed: 0.594 s
% 6.73/1.36 % (2740149)Peak memory usage: 15 MB
% 6.73/1.36 % (2740149)Instructions burned: 1242 (million)
% 6.73/1.36 % (2740229)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=1059475046:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 6.73/1.36 % (2740230)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=3488721884:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/91Mi)
% 6.73/1.36 % (2740229)Instruction limit reached!
% 6.73/1.36 % (2740229)------------------------------
% 6.73/1.36 % (2740229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.73/1.36 % (2740229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.36 % (2740229)CaDiCaL version: 2.1.3
% 6.73/1.36 % (2740229)Termination reason: Instruction limit
% 6.73/1.36 % (2740229)Termination phase: Saturation
% 6.73/1.36 % (2740229)Time elapsed: 0.018 s
% 6.73/1.36 % (2740229)Peak memory usage: 12 MB
% 6.73/1.36 % (2740229)Instructions burned: 34 (million)
% 6.73/1.36 % (2740233)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2973560220:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2991 on theBenchmark for (2991ds/66Mi)
% 6.73/1.36 % (2740214)Instruction limit reached!
% 6.73/1.36 % (2740214)------------------------------
% 6.73/1.36 % (2740214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.73/1.36 % (2740214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.36 % (2740214)CaDiCaL version: 2.1.3
% 6.73/1.36 % (2740214)Termination reason: Instruction limit
% 6.73/1.36 % (2740214)Termination phase: Saturation
% 6.73/1.36 % (2740214)Time elapsed: 0.215 s
% 6.73/1.36 % (2740214)Peak memory usage: 13 MB
% 6.73/1.36 % (2740214)Instructions burned: 450 (million)
% 6.73/1.36 % (2740230)Instruction limit reached!
% 6.73/1.36 % (2740230)------------------------------
% 6.73/1.36 % (2740230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.73/1.36 % (2740230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.36 % (2740230)CaDiCaL version: 2.1.3
% 6.73/1.36 % (2740230)Termination reason: Instruction limit
% 6.73/1.36 % (2740230)Termination phase: Saturation
% 6.73/1.36 % (2740230)Time elapsed: 0.047 s
% 6.73/1.36 % (2740230)Peak memory usage: 12 MB
% 6.73/1.36 % (2740230)Instructions burned: 91 (million)
% 6.73/1.36 % (2740224)Instruction limit reached!
% 6.73/1.36 % (2740224)------------------------------
% 6.73/1.36 % (2740224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.73/1.36 % (2740224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.36 % (2740224)CaDiCaL version: 2.1.3
% 6.73/1.36 % (2740224)Termination reason: Instruction limit
% 6.73/1.36 % (2740224)Termination phase: Saturation
% 6.73/1.36 % (2740224)Time elapsed: 0.098 s
% 6.73/1.36 % (2740224)Peak memory usage: 13 MB
% 6.73/1.36 % (2740224)Instructions burned: 377 (million)
% 6.73/1.36 % (2740235)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1263830922:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 6.73/1.36 % (2740236)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=3233415034:i=338:bd=all:ins=4:rtra=on_2991 on theBenchmark for (2991ds/338Mi)
% 6.73/1.36 % (2740238)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2382158172:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/28Mi)
% 6.73/1.36 % (2740235)Instruction limit reached!
% 6.73/1.36 % (2740235)------------------------------
% 6.73/1.36 % (2740235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.73/1.36 % (2740235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.36 % (2740235)CaDiCaL version: 2.1.3
% 6.73/1.36 % (2740235)Termination reason: Instruction limit
% 6.73/1.36 % (2740235)Termination phase: Saturation
% 6.73/1.36 % (2740235)Time elapsed: 0.009 s
% 6.73/1.36 % (2740235)Peak memory usage: 12 MB
% 6.73/1.36 % (2740235)Instructions burned: 22 (million)
% 6.73/1.36 % (2740233)Instruction limit reached!
% 6.73/1.36 % (2740233)------------------------------
% 6.73/1.36 % (2740233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.73/1.36 % (2740233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740233)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740233)Termination reason: Instruction limit
% 7.39/1.48 % (2740233)Termination phase: Saturation
% 7.39/1.48 % (2740233)Time elapsed: 0.037 s
% 7.39/1.48 % (2740233)Peak memory usage: 13 MB
% 7.39/1.48 % (2740233)Instructions burned: 66 (million)
% 7.39/1.48 % (2740238)Instruction limit reached!
% 7.39/1.48 % (2740238)------------------------------
% 7.39/1.48 % (2740238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740238)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740238)Termination reason: Instruction limit
% 7.39/1.48 % (2740238)Termination phase: Saturation
% 7.39/1.48 % (2740238)Time elapsed: 0.009 s
% 7.39/1.48 % (2740238)Peak memory usage: 12 MB
% 7.39/1.48 % (2740238)Instructions burned: 31 (million)
% 7.39/1.48 % (2740241)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.39/1.48 % (2740241)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=2248951094:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2991 on theBenchmark for (2991ds/137Mi)
% 7.39/1.48 % (2740243)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=305844773:i=227:sd=1:bd=all:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/227Mi)
% 7.39/1.48 % (2740242)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=1096050875:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2991 on theBenchmark for (2991ds/340Mi)
% 7.39/1.48 % (2740213)Instruction limit reached!
% 7.39/1.48 % (2740213)------------------------------
% 7.39/1.48 % (2740213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740213)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740213)Termination reason: Instruction limit
% 7.39/1.48 % (2740213)Termination phase: Saturation
% 7.39/1.48 % (2740213)Time elapsed: 0.273 s
% 7.39/1.48 % (2740213)Peak memory usage: 14 MB
% 7.39/1.48 % (2740213)Instructions burned: 572 (million)
% 7.39/1.48 % (2740247)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.39/1.48 % (2740247)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=3099079211:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/373Mi)
% 7.39/1.48 % (2740243)Instruction limit reached!
% 7.39/1.48 % (2740243)------------------------------
% 7.39/1.48 % (2740243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740243)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740243)Termination reason: Instruction limit
% 7.39/1.48 % (2740243)Termination phase: Saturation
% 7.39/1.48 % (2740243)Time elapsed: 0.060 s
% 7.39/1.48 % (2740243)Peak memory usage: 13 MB
% 7.39/1.48 % (2740243)Instructions burned: 227 (million)
% 7.39/1.48 % (2740249)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2067757074:i=116:ep=RSTC:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/116Mi)
% 7.39/1.48 % (2740241)Instruction limit reached!
% 7.39/1.48 % (2740241)------------------------------
% 7.39/1.48 % (2740241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740241)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740241)Termination reason: Instruction limit
% 7.39/1.48 % (2740241)Termination phase: Saturation
% 7.39/1.48 % (2740241)Time elapsed: 0.073 s
% 7.39/1.48 % (2740241)Peak memory usage: 12 MB
% 7.39/1.48 % (2740241)Instructions burned: 138 (million)
% 7.39/1.48 % (2740251)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=736913007:i=575:rtra=on_2990 on theBenchmark for (2990ds/575Mi)
% 7.39/1.48 % (2740249)Instruction limit reached!
% 7.39/1.48 % (2740249)------------------------------
% 7.39/1.48 % (2740249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740249)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740249)Termination reason: Instruction limit
% 7.39/1.48 % (2740249)Termination phase: Saturation
% 7.39/1.48 % (2740249)Time elapsed: 0.032 s
% 7.39/1.48 % (2740249)Peak memory usage: 12 MB
% 7.39/1.48 % (2740249)Instructions burned: 118 (million)
% 7.39/1.48 % (2740253)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=4226598067:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2989 on theBenchmark for (2989ds/270Mi)
% 7.39/1.48 % (2740225)Instruction limit reached!
% 7.39/1.48 % (2740225)------------------------------
% 7.39/1.48 % (2740225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740225)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740225)Termination reason: Instruction limit
% 7.39/1.48 % (2740225)Termination phase: Saturation
% 7.39/1.48 % (2740225)Time elapsed: 0.241 s
% 7.39/1.48 % (2740225)Peak memory usage: 14 MB
% 7.39/1.48 % (2740225)Instructions burned: 496 (million)
% 7.39/1.48 % (2740255)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=3192045089: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_2989 on theBenchmark for (2989ds/9840Mi)
% 7.39/1.48 % (2740236)Instruction limit reached!
% 7.39/1.48 % (2740236)------------------------------
% 7.39/1.48 % (2740236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740236)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740236)Termination reason: Instruction limit
% 7.39/1.48 % (2740236)Termination phase: Saturation
% 7.39/1.48 % (2740236)Time elapsed: 0.171 s
% 7.39/1.48 % (2740236)Peak memory usage: 14 MB
% 7.39/1.48 % (2740236)Instructions burned: 338 (million)
% 7.39/1.48 % (2740242)Instruction limit reached!
% 7.39/1.48 % (2740242)------------------------------
% 7.39/1.48 % (2740242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740242)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740242)Termination reason: Instruction limit
% 7.39/1.48 % (2740242)Termination phase: Saturation
% 7.39/1.48 % (2740242)Time elapsed: 0.160 s
% 7.39/1.48 % (2740242)Peak memory usage: 13 MB
% 7.39/1.48 % (2740242)Instructions burned: 342 (million)
% 7.39/1.48 % (2740257)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=817288781:i=421:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/421Mi)
% 7.39/1.48 % (2740258)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.39/1.48 % (2740258)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=3168206689:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/270Mi)
% 7.39/1.48 % (2740253)Instruction limit reached!
% 7.39/1.48 % (2740253)------------------------------
% 7.39/1.48 % (2740253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740253)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740253)Termination reason: Instruction limit
% 7.39/1.48 % (2740253)Termination phase: Saturation
% 7.39/1.48 % (2740253)Time elapsed: 0.069 s
% 7.39/1.48 % (2740253)Peak memory usage: 13 MB
% 7.39/1.48 % (2740253)Instructions burned: 271 (million)
% 7.39/1.48 % (2740247)Instruction limit reached!
% 7.39/1.48 % (2740247)------------------------------
% 7.39/1.48 % (2740247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740247)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740247)Termination reason: Instruction limit
% 7.39/1.48 % (2740247)Termination phase: Saturation
% 7.39/1.48 % (2740247)Time elapsed: 0.163 s
% 7.39/1.48 % (2740247)Peak memory usage: 14 MB
% 7.39/1.48 % (2740247)Instructions burned: 373 (million)
% 7.39/1.48 % (2740261)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=532884099:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/31Mi)
% 7.39/1.48 % (2740261)Instruction limit reached!
% 7.39/1.48 % (2740261)------------------------------
% 7.39/1.48 % (2740261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740261)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740261)Termination reason: Instruction limit
% 7.39/1.48 % (2740261)Termination phase: Saturation
% 7.39/1.48 % (2740261)Time elapsed: 0.008 s
% 7.39/1.48 % (2740261)Peak memory usage: 12 MB
% 7.39/1.48 % (2740261)Instructions burned: 31 (million)
% 7.39/1.48 % (2740262)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 7.39/1.48 % (2740262)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
% 7.39/1.48 % (2740262)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=3235229793:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2988 on theBenchmark for (2988ds/1440Mi)
% 7.39/1.48 % (2740264)dis+10_2_sil=128000:si=on:random_seed=2284959395:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2988 on theBenchmark for (2988ds/339Mi)
% 7.39/1.48 % (2740264)Instruction limit reached!
% 7.39/1.48 % (2740264)------------------------------
% 7.39/1.48 % (2740264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740264)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740264)Termination reason: Instruction limit
% 7.39/1.48 % (2740264)Termination phase: Saturation
% 7.39/1.48 % (2740264)Time elapsed: 0.086 s
% 7.39/1.48 % (2740264)Peak memory usage: 13 MB
% 7.39/1.48 % (2740264)Instructions burned: 340 (million)
% 7.39/1.48 % (2740267)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=3677427849:i=111:add=on:fgj=on:rtra=on:fdi=1024_2987 on theBenchmark for (2987ds/111Mi)
% 7.39/1.48 % (2740258) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2740084-2740258"...
% 7.39/1.48 % (2740258)...printing done.
% 7.39/1.48 % (2740258)Refutation found. Thanks to Tanya!
% 7.39/1.48 % SZS status Theorem for theBenchmark
% 7.39/1.48 % SZS output start Proof for theBenchmark
% 7.39/1.48 thf(type_def_5, type, a: $tType).
% 7.39/1.48 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 7.39/1.48 thf(func_def_3, type, sK0: ((a > $o) > a)).
% 7.39/1.48 thf(func_def_4, type, sK1: (a > a > $o)).
% 7.39/1.48 thf(func_def_5, type, sK2: (a > a)).
% 7.39/1.48 thf(func_def_6, type, sK3: (a > (a > $o) > a)).
% 7.39/1.48 thf(func_def_7, type, sF4: (a > a > $o)).
% 7.39/1.48 thf(func_def_8, type, sF5: (a > a)).
% 7.39/1.48 thf(func_def_9, type, sF6: (a > $o)).
% 7.39/1.48 thf(func_def_10, type, sF7: (a > $o)).
% 7.39/1.48 thf(func_def_11, type, sF8: (a > a > $o)).
% 7.39/1.48 thf(func_def_12, type, sF9: ((a > $o) > a)).
% 7.39/1.48 thf(func_def_13, type, sF10: ((a > $o) > a > $o)).
% 7.39/1.48 thf(func_def_14, type, sF11: (a > (a > $o) > $o)).
% 7.39/1.48 thf(func_def_15, type, sF12: ((a > $o) > a > a)).
% 7.39/1.48 thf(func_def_16, type, sF13: (a > (a > $o) > $o)).
% 7.39/1.48 thf(func_def_17, type, sF14: (a > (a > $o) > $o)).
% 7.39/1.48 thf(func_def_18, type, sF15: (a > (a > $o) > $o)).
% 7.39/1.48 thf(func_def_19, type, vNOT: ($o > $o)).
% 7.39/1.48 thf(func_def_20, type, db0: !>[X0: $tType]:(X0)).
% 7.39/1.48 thf(func_def_21, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 7.39/1.48 thf(f1,conjecture,(
% 7.39/1.48 ! [X0 : (a > a > $o),X1 : ((a > $o) > a)] : (! [X9 : (a > a)] : (? [X12 : a] : (((X0 @ (X9 @ X12) @ X12) | (X0 @ (X9 @ X12) @ X12)) & ((X0 @ X12 @ (X9 @ X12)) | (X0 @ X12 @ (X9 @ X12)))) | ? [X11 : a,X10 : a] : ((~(X0 @ (X9 @ X10) @ (X9 @ X11)) | ~(X0 @ (X9 @ X10) @ (X9 @ X11))) & ((X0 @ X10 @ X11) | (X0 @ X10 @ X11)))) | ? [X5 : (a > $o)] : (? [X7 : a] : ((~(X0 @ (X1 @ X5) @ X7) | ~(X0 @ (X1 @ X5) @ X7)) & ! [X8 : a] : (~(X5 @ X8) | (X0 @ X8 @ X7) | (X0 @ X8 @ X7) | ~(X5 @ X8))) | ? [X6 : a] : (((X5 @ X6) | (X5 @ X6)) & (~(X0 @ X6 @ (X1 @ X5)) | ~(X0 @ X6 @ (X1 @ X5))))) | ? [X3 : a,X2 : a,X4 : a] : (((X0 @ X2 @ X3) | (X0 @ X2 @ X3)) & ((X0 @ X3 @ X4) | (X0 @ X3 @ X4)) & (~(X0 @ X2 @ X4) | ~(X0 @ X2 @ X4))))),
% 7.39/1.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cT145_DOUBLE)).
% 7.39/1.48 thf(f2,negated_conjecture,(
% 7.39/1.48 ~ ! [X0 : (a > a > $o),X1 : ((a > $o) > a)] : (! [X9 : (a > a)] : (? [X12 : a] : (((X0 @ (X9 @ X12) @ X12) | (X0 @ (X9 @ X12) @ X12)) & ((X0 @ X12 @ (X9 @ X12)) | (X0 @ X12 @ (X9 @ X12)))) | ? [X11 : a,X10 : a] : ((~(X0 @ (X9 @ X10) @ (X9 @ X11)) | ~(X0 @ (X9 @ X10) @ (X9 @ X11))) & ((X0 @ X10 @ X11) | (X0 @ X10 @ X11)))) | ? [X5 : (a > $o)] : (? [X7 : a] : ((~(X0 @ (X1 @ X5) @ X7) | ~(X0 @ (X1 @ X5) @ X7)) & ! [X8 : a] : (~(X5 @ X8) | (X0 @ X8 @ X7) | (X0 @ X8 @ X7) | ~(X5 @ X8))) | ? [X6 : a] : (((X5 @ X6) | (X5 @ X6)) & (~(X0 @ X6 @ (X1 @ X5)) | ~(X0 @ X6 @ (X1 @ X5))))) | ? [X3 : a,X2 : a,X4 : a] : (((X0 @ X2 @ X3) | (X0 @ X2 @ X3)) & ((X0 @ X3 @ X4) | (X0 @ X3 @ X4)) & (~(X0 @ X2 @ X4) | ~(X0 @ X2 @ X4))))),
% 7.39/1.48 inference(negated_conjecture,[status(cth)],[f1])).
% 7.39/1.48 thf(f3,plain,(
% 7.39/1.48 ~ ! [X0 : (a > a > $o),X1 : ((a > $o) > a)] : (! [X2 : (a > a)] : (? [X3 : a] : (((X0 @ (X2 @ X3) @ X3) | (X0 @ (X2 @ X3) @ X3)) & ((X0 @ X3 @ (X2 @ X3)) | (X0 @ X3 @ (X2 @ X3)))) | ? [X4 : a,X5 : a] : ((~(X0 @ (X2 @ X5) @ (X2 @ X4)) | ~(X0 @ (X2 @ X5) @ (X2 @ X4))) & ((X0 @ X5 @ X4) | (X0 @ X5 @ X4)))) | ? [X6 : (a > $o)] : (? [X7 : a] : ((~(X0 @ (X1 @ X6) @ X7) | ~(X0 @ (X1 @ X6) @ X7)) & ! [X8 : a] : (~(X6 @ X8) | (X0 @ X8 @ X7) | (X0 @ X8 @ X7) | ~(X6 @ X8))) | ? [X9 : a] : (((X6 @ X9) | (X6 @ X9)) & (~(X0 @ X9 @ (X1 @ X6)) | ~(X0 @ X9 @ (X1 @ X6))))) | ? [X10 : a,X11 : a,X12 : a] : (((X0 @ X11 @ X10) | (X0 @ X11 @ X10)) & ((X0 @ X10 @ X12) | (X0 @ X10 @ X12)) & (~(X0 @ X11 @ X12) | ~(X0 @ X11 @ X12))))),
% 7.39/1.48 inference(rectify,[],[f2])).
% 7.39/1.48 thf(f4,plain,(
% 7.39/1.48 ~ ! [X0 : (a > a > $o),X1 : ((a > $o) > a)] : (! [X2 : (a > a)] : (? [X3 : a] : (((((X0 @ (X2 @ X3) @ X3)) = $true) | (((X0 @ (X2 @ X3) @ X3)) = $true)) & ((((X0 @ X3 @ (X2 @ X3))) = $true) | (((X0 @ X3 @ (X2 @ X3))) = $true))) | ? [X4 : a,X5 : a] : ((~ (((X0 @ (X2 @ X5) @ (X2 @ X4))) = $true) | ~ (((X0 @ (X2 @ X5) @ (X2 @ X4))) = $true)) & ((((X0 @ X5 @ X4)) = $true) | (((X0 @ X5 @ X4)) = $true)))) | ? [X6 : (a > $o)] : (? [X7 : a] : ((~ (((X0 @ (X1 @ X6) @ X7)) = $true) | ~ (((X0 @ (X1 @ X6) @ X7)) = $true)) & ! [X8 : a] : (~ (((X6 @ X8)) = $true) | (((X0 @ X8 @ X7)) = $true) | (((X0 @ X8 @ X7)) = $true) | ~ (((X6 @ X8)) = $true))) | ? [X9 : a] : (((((X6 @ X9)) = $true) | (((X6 @ X9)) = $true)) & (~ (((X0 @ X9 @ (X1 @ X6))) = $true) | ~ (((X0 @ X9 @ (X1 @ X6))) = $true)))) | ? [X10 : a,X11 : a,X12 : a] : (((((X0 @ X11 @ X10)) = $true) | (((X0 @ X11 @ X10)) = $true)) & ((((X0 @ X10 @ X12)) = $true) | (((X0 @ X10 @ X12)) = $true)) & (~ (((X0 @ X11 @ X12)) = $true) | ~ (((X0 @ X11 @ X12)) = $true))))),
% 7.39/1.48 inference(fool_elimination,[],[f3])).
% 7.39/1.48 thf(f5,plain,(
% 7.39/1.48 ~ ! [X1 : ((a > $o) > a),X0 : (a > a > $o)] : (! [X2 : (a > a)] : (? [X5 : a,X4 : a] : (((((X0 @ (X2 @ X5) @ (X2 @ X4))) != $true) | (((X0 @ (X2 @ X5) @ (X2 @ X4))) != $true)) & ((((X0 @ X5 @ X4)) = $true) | (((X0 @ X5 @ X4)) = $true))) | ? [X3 : a] : (((((X0 @ (X2 @ X3) @ X3)) = $true) | (((X0 @ (X2 @ X3) @ X3)) = $true)) & ((((X0 @ X3 @ (X2 @ X3))) = $true) | (((X0 @ X3 @ (X2 @ X3))) = $true)))) | ? [X6 : (a > $o)] : (? [X7 : a] : (! [X8 : a] : ((((X6 @ X8)) != $true) | (((X0 @ X8 @ X7)) = $true) | (((X6 @ X8)) != $true) | (((X0 @ X8 @ X7)) = $true)) & ((((X0 @ (X1 @ X6) @ X7)) != $true) | (((X0 @ (X1 @ X6) @ X7)) != $true))) | ? [X9 : a] : (((((X0 @ X9 @ (X1 @ X6))) != $true) | (((X0 @ X9 @ (X1 @ X6))) != $true)) & ((((X6 @ X9)) = $true) | (((X6 @ X9)) = $true)))) | ? [X10 : a,X11 : a,X12 : a] : (((((X0 @ X11 @ X12)) != $true) | (((X0 @ X11 @ X12)) != $true)) & ((((X0 @ X10 @ X12)) = $true) | (((X0 @ X10 @ X12)) = $true)) & ((((X0 @ X11 @ X10)) = $true) | (((X0 @ X11 @ X10)) = $true))))),
% 7.39/1.48 inference(flattening,[],[f4])).
% 7.39/1.48 thf(f6,plain,(
% 7.39/1.48 ? [X1 : ((a > $o) > a),X0 : (a > a > $o)] : (! [X12 : a,X10 : a,X11 : a] : (((((X0 @ X11 @ X10)) != $true) & (((X0 @ X11 @ X10)) != $true)) | ((((X0 @ X10 @ X12)) != $true) & (((X0 @ X10 @ X12)) != $true)) | ((((X0 @ X11 @ X12)) = $true) & (((X0 @ X11 @ X12)) = $true))) & ? [X2 : (a > a)] : (! [X3 : a] : (((((X0 @ (X2 @ X3) @ X3)) != $true) & (((X0 @ (X2 @ X3) @ X3)) != $true)) | ((((X0 @ X3 @ (X2 @ X3))) != $true) & (((X0 @ X3 @ (X2 @ X3))) != $true))) & ! [X5 : a,X4 : a] : (((((X0 @ (X2 @ X5) @ (X2 @ X4))) = $true) & (((X0 @ (X2 @ X5) @ (X2 @ X4))) = $true)) | ((((X0 @ X5 @ X4)) != $true) & (((X0 @ X5 @ X4)) != $true)))) & ! [X6 : (a > $o)] : (! [X9 : a] : (((((X0 @ X9 @ (X1 @ X6))) = $true) & (((X0 @ X9 @ (X1 @ X6))) = $true)) | ((((X6 @ X9)) != $true) & (((X6 @ X9)) != $true))) & ! [X7 : a] : (? [X8 : a] : ((((X6 @ X8)) = $true) & (((X0 @ X8 @ X7)) != $true) & (((X0 @ X8 @ X7)) != $true) & (((X6 @ X8)) = $true)) | ((((X0 @ (X1 @ X6) @ X7)) = $true) & (((X0 @ (X1 @ X6) @ X7)) = $true)))))),
% 7.39/1.48 inference(ennf_transformation,[],[f5])).
% 7.39/1.48 thf(f7,plain,(
% 7.39/1.48 ? [X0 : ((a > $o) > a),X1 : (a > a > $o)] : (! [X2 : a,X3 : a,X4 : a] : (((((X1 @ X4 @ X3)) != $true) & (((X1 @ X4 @ X3)) != $true)) | ((((X1 @ X3 @ X2)) != $true) & (((X1 @ X3 @ X2)) != $true)) | ((((X1 @ X4 @ X2)) = $true) & (((X1 @ X4 @ X2)) = $true))) & ? [X5 : (a > a)] : (! [X6 : a] : (((((X1 @ (X5 @ X6) @ X6)) != $true) & (((X1 @ (X5 @ X6) @ X6)) != $true)) | (($true != ((X1 @ X6 @ (X5 @ X6)))) & ($true != ((X1 @ X6 @ (X5 @ X6)))))) & ! [X7 : a,X8 : a] : (((((X1 @ (X5 @ X7) @ (X5 @ X8))) = $true) & (((X1 @ (X5 @ X7) @ (X5 @ X8))) = $true)) | ((((X1 @ X7 @ X8)) != $true) & (((X1 @ X7 @ X8)) != $true)))) & ! [X9 : (a > $o)] : (! [X10 : a] : (((((X1 @ X10 @ (X0 @ X9))) = $true) & (((X1 @ X10 @ (X0 @ X9))) = $true)) | ((((X9 @ X10)) != $true) & (((X9 @ X10)) != $true))) & ! [X11 : a] : (? [X12 : a] : (($true = ((X9 @ X12))) & (((X1 @ X12 @ X11)) != $true) & (((X1 @ X12 @ X11)) != $true) & ($true = ((X9 @ X12)))) | (($true = ((X1 @ (X0 @ X9) @ X11))) & ($true = ((X1 @ (X0 @ X9) @ X11)))))))),
% 7.39/1.48 inference(rectify,[],[f6])).
% 7.39/1.48 thf(f8,plain,(
% 7.39/1.48 ! [X2 : a,X3 : a,X4 : a] : (((((sK1 @ X4 @ X3)) != $true) & (((sK1 @ X4 @ X3)) != $true)) | ((((sK1 @ X3 @ X2)) != $true) & (((sK1 @ X3 @ X2)) != $true)) | ((((sK1 @ X4 @ X2)) = $true) & (((sK1 @ X4 @ X2)) = $true))) & (! [X6 : a] : ((($true != ((sK1 @ (sK2 @ X6) @ X6))) & ($true != ((sK1 @ (sK2 @ X6) @ X6)))) | ((((sK1 @ X6 @ (sK2 @ X6))) != $true) & (((sK1 @ X6 @ (sK2 @ X6))) != $true))) & ! [X7 : a,X8 : a] : (((((sK1 @ (sK2 @ X7) @ (sK2 @ X8))) = $true) & (((sK1 @ (sK2 @ X7) @ (sK2 @ X8))) = $true)) | ((((sK1 @ X7 @ X8)) != $true) & (((sK1 @ X7 @ X8)) != $true)))) & ! [X9 : (a > $o)] : (! [X10 : a] : (((((sK1 @ X10 @ (sK0 @ X9))) = $true) & (((sK1 @ X10 @ (sK0 @ X9))) = $true)) | ((((X9 @ X10)) != $true) & (((X9 @ X10)) != $true))) & ! [X11 : a] : ((($true = ((X9 @ (sK3 @ X11 @ X9)))) & (((sK1 @ (sK3 @ X11 @ X9) @ X11)) != $true) & (((sK1 @ (sK3 @ X11 @ X9) @ X11)) != $true) & ($true = ((X9 @ (sK3 @ X11 @ X9))))) | ((((sK1 @ (sK0 @ X9) @ X11)) = $true) & (((sK1 @ (sK0 @ X9) @ X11)) = $true))))),
% 7.39/1.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,vAPP]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X5,sK2),skolemize(X12,sK3 @ X11 @ X9)],[f7])).
% 7.39/1.48 thf(f10,plain,(
% 7.39/1.48 ( ! [X11 : a,X9 : (a > $o)] : (($true = ((X9 @ (sK3 @ X11 @ X9)))) | (((sK1 @ (sK0 @ X9) @ X11)) = $true)) )),
% 7.39/1.48 inference(cnf_transformation,[],[f8])).
% 7.39/1.48 thf(f12,plain,(
% 7.39/1.48 ( ! [X11 : a,X9 : (a > $o)] : ((((sK1 @ (sK3 @ X11 @ X9) @ X11)) != $true) | (((sK1 @ (sK0 @ X9) @ X11)) = $true)) )),
% 7.39/1.48 inference(cnf_transformation,[],[f8])).
% 7.39/1.48 thf(f20,plain,(
% 7.39/1.48 ( ! [X10 : a,X9 : (a > $o)] : ((((sK1 @ X10 @ (sK0 @ X9))) = $true) | (((X9 @ X10)) != $true)) )),
% 7.39/1.48 inference(cnf_transformation,[],[f8])).
% 7.39/1.48 thf(f23,plain,(
% 7.39/1.48 ( ! [X8 : a,X7 : a] : ((((sK1 @ (sK2 @ X7) @ (sK2 @ X8))) = $true) | (((sK1 @ X7 @ X8)) != $true)) )),
% 7.39/1.48 inference(cnf_transformation,[],[f8])).
% 7.39/1.48 thf(f27,plain,(
% 7.39/1.48 ( ! [X6 : a] : (($true != ((sK1 @ (sK2 @ X6) @ X6))) | (((sK1 @ X6 @ (sK2 @ X6))) != $true)) )),
% 7.39/1.48 inference(cnf_transformation,[],[f8])).
% 7.39/1.48 thf(f35,plain,(
% 7.39/1.48 ( ! [X2 : a,X3 : a,X4 : a] : ((((sK1 @ X4 @ X3)) != $true) | (((sK1 @ X3 @ X2)) != $true) | (((sK1 @ X4 @ X2)) = $true)) )),
% 7.39/1.48 inference(cnf_transformation,[],[f8])).
% 7.39/1.48 thf(f39,definition,(
% 7.39/1.48 ( ! [X3 : a,X4 : a] : ((((sF4 @ X3 @ X4)) = ((sK1 @ X4 @ X3)))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 7.39/1.48 thf(f41,plain,(
% 7.39/1.48 ( ! [X2 : a,X3 : a,X4 : a] : ((((sF4 @ X3 @ X4)) != $true) | (((sF4 @ X2 @ X4)) = $true) | (((sF4 @ X2 @ X3)) != $true)) )),
% 7.39/1.48 inference(definition_folding,[],[f35,f39,f39,f39])).
% 7.39/1.48 thf(f48,definition,(
% 7.39/1.48 ( ! [X6 : a] : ((((sF5 @ X6)) = ((sK2 @ X6)))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 7.39/1.48 thf(f49,definition,(
% 7.39/1.48 ( ! [X6 : a] : ((((sF6 @ X6)) = ((sK1 @ (sF5 @ X6) @ X6)))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 7.39/1.48 thf(f50,definition,(
% 7.39/1.48 ( ! [X6 : a] : ((((sF7 @ X6)) = ((sK1 @ X6 @ (sF5 @ X6))))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 7.39/1.48 thf(f51,plain,(
% 7.39/1.48 ( ! [X6 : a] : ((((sK1 @ X6 @ (sF5 @ X6))) = ((sF7 @ X6)))) )),
% 7.39/1.48 inference(reorient_equations,[],[f50])).
% 7.39/1.48 thf(f53,plain,(
% 7.39/1.48 ( ! [X6 : a] : ((((sF7 @ X6)) != $true) | (((sF6 @ X6)) != $true)) )),
% 7.39/1.48 inference(definition_folding,[],[f27,f51,f48,f49,f48])).
% 7.39/1.48 thf(f56,definition,(
% 7.39/1.48 ( ! [X8 : a,X7 : a] : ((((sF8 @ X8 @ X7)) = ((sK1 @ (sF5 @ X7) @ (sF5 @ X8))))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 7.39/1.48 thf(f57,plain,(
% 7.39/1.48 ( ! [X8 : a,X7 : a] : ((((sK1 @ (sF5 @ X7) @ (sF5 @ X8))) = ((sF8 @ X8 @ X7)))) )),
% 7.39/1.48 inference(reorient_equations,[],[f56])).
% 7.39/1.48 thf(f59,plain,(
% 7.39/1.48 ( ! [X8 : a,X7 : a] : (($true != ((sF4 @ X8 @ X7))) | ($true = ((sF8 @ X8 @ X7)))) )),
% 7.39/1.48 inference(definition_folding,[],[f23,f39,f57,f48,f48])).
% 7.39/1.48 thf(f62,definition,(
% 7.39/1.48 ( ! [X9 : (a > $o)] : ((((sF9 @ X9)) = ((sK0 @ X9)))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 7.39/1.48 thf(f63,plain,(
% 7.39/1.48 ( ! [X9 : (a > $o)] : ((((sK0 @ X9)) = ((sF9 @ X9)))) )),
% 7.39/1.48 inference(reorient_equations,[],[f62])).
% 7.39/1.48 thf(f64,definition,(
% 7.39/1.48 ( ! [X10 : a,X9 : (a > $o)] : ((((sF10 @ X9 @ X10)) = ((sK1 @ X10 @ (sF9 @ X9))))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 7.39/1.48 thf(f65,plain,(
% 7.39/1.48 ( ! [X10 : a,X9 : (a > $o)] : ((((sK1 @ X10 @ (sF9 @ X9))) = ((sF10 @ X9 @ X10)))) )),
% 7.39/1.48 inference(reorient_equations,[],[f64])).
% 7.39/1.48 thf(f66,definition,(
% 7.39/1.48 ( ! [X10 : a,X9 : (a > $o)] : ((((sF11 @ X10 @ X9)) = ((X9 @ X10)))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 7.39/1.48 thf(f67,plain,(
% 7.39/1.48 ( ! [X10 : a,X9 : (a > $o)] : ((((X9 @ X10)) = ((sF11 @ X10 @ X9)))) )),
% 7.39/1.48 inference(reorient_equations,[],[f66])).
% 7.39/1.48 thf(f68,plain,(
% 7.39/1.48 ( ! [X10 : a,X9 : (a > $o)] : ((((sF11 @ X10 @ X9)) != $true) | (((sF10 @ X9 @ X10)) = $true)) )),
% 7.39/1.48 inference(definition_folding,[],[f20,f67,f65,f63])).
% 7.39/1.48 thf(f72,definition,(
% 7.39/1.48 ( ! [X11 : a,X9 : (a > $o)] : ((((sF12 @ X9 @ X11)) = ((sK3 @ X11 @ X9)))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 7.39/1.48 thf(f73,definition,(
% 7.39/1.48 ( ! [X11 : a,X9 : (a > $o)] : ((((sF13 @ X11 @ X9)) = ((X9 @ (sF12 @ X9 @ X11))))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 7.39/1.48 thf(f74,definition,(
% 7.39/1.48 ( ! [X11 : a,X9 : (a > $o)] : ((((sF14 @ X11 @ X9)) = ((sK1 @ (sF9 @ X9) @ X11)))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 7.39/1.48 thf(f75,plain,(
% 7.39/1.48 ( ! [X11 : a,X9 : (a > $o)] : ((((sK1 @ (sF9 @ X9) @ X11)) = ((sF14 @ X11 @ X9)))) )),
% 7.39/1.48 inference(reorient_equations,[],[f74])).
% 7.39/1.48 thf(f78,definition,(
% 7.39/1.48 ( ! [X11 : a,X9 : (a > $o)] : ((((sF15 @ X11 @ X9)) = ((sK1 @ (sF12 @ X9 @ X11) @ X11)))) )),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 7.39/1.48 thf(f81,plain,(
% 7.39/1.48 ( ! [X11 : a,X9 : (a > $o)] : ((((sF15 @ X11 @ X9)) != $true) | (((sF14 @ X11 @ X9)) = $true)) )),
% 7.39/1.48 inference(definition_folding,[],[f12,f75,f63,f78,f72])).
% 7.39/1.48 thf(f83,plain,(
% 7.39/1.48 ( ! [X11 : a,X9 : (a > $o)] : ((((sF14 @ X11 @ X9)) = $true) | (((sF13 @ X11 @ X9)) = $true)) )),
% 7.39/1.48 inference(definition_folding,[],[f10,f75,f63,f73,f72])).
% 7.39/1.48 thf(f85,plain,(
% 7.39/1.48 ( ! [X10 : a,X9 : (a > $o)] : ((((X9 @ X10)) != $true) | (((sF10 @ X9 @ X10)) = $true)) )),
% 7.39/1.48 inference(forward_demodulation,[],[f68,f67])).
% 7.39/1.48 thf(f121,plain,(
% 7.39/1.48 ( ! [X0 : a,X1 : a] : ((((sK1 @ X0 @ X1)) != $true) | (((sF8 @ X1 @ X0)) = $true)) )),
% 7.39/1.48 inference(superposition,[],[f59,f39])).
% 7.39/1.48 thf(f123,plain,(
% 7.39/1.48 ( ! [X0 : a] : ((((sF7 @ X0)) != $true) | (((sF8 @ (sF5 @ X0) @ X0)) = $true)) )),
% 7.39/1.48 inference(superposition,[],[f121,f51])).
% 7.39/1.48 thf(f127,plain,(
% 7.39/1.48 ( ! [X0 : a] : ((((sF7 @ (sF5 @ X0))) = ((sF8 @ (sF5 @ X0) @ X0)))) )),
% 7.39/1.48 inference(superposition,[],[f57,f51])).
% 7.39/1.48 thf(f133,plain,(
% 7.39/1.48 ( ! [X0 : a,X1 : a] : ((((sF4 @ (sF5 @ X0) @ (sF5 @ X1))) = ((sF8 @ X0 @ X1)))) )),
% 7.39/1.48 inference(superposition,[],[f39,f57])).
% 7.39/1.48 thf(f137,plain,(
% 7.39/1.48 ( ! [X0 : (a > $o)] : ((((sF6 @ (sF9 @ X0))) = ((sF10 @ X0 @ (sF5 @ (sF9 @ X0)))))) )),
% 7.39/1.48 inference(superposition,[],[f65,f49])).
% 7.39/1.48 thf(f140,plain,(
% 7.39/1.48 ( ! [X0 : (a > $o),X1 : a] : ((((sF10 @ X0 @ X1)) != $true) | (((sF8 @ (sF9 @ X0) @ X1)) = $true)) )),
% 7.39/1.48 inference(superposition,[],[f121,f65])).
% 7.39/1.48 thf(f162,plain,(
% 7.39/1.48 ( ! [X0 : a] : ((((sF8 @ (sF5 @ (sF12 @ sF7 @ X0)) @ (sF12 @ sF7 @ X0))) = $true) | (((sF13 @ X0 @ sF7)) != $true)) )),
% 7.39/1.48 inference(superposition,[],[f123,f73])).
% 7.39/1.48 thf(f177,plain,(
% 7.39/1.48 ( ! [X0 : a] : ((((sF13 @ X0 @ sF7)) != $true) | (((sF7 @ (sF5 @ (sF12 @ sF7 @ X0)))) = $true)) )),
% 7.39/1.48 inference(forward_demodulation,[],[f162,f127])).
% 7.39/1.48 thf(f179,plain,(
% 7.39/1.48 ( ! [X0 : (a > $o)] : ((((sF14 @ (sF5 @ (sF9 @ X0)) @ X0)) = ((sF7 @ (sF9 @ X0))))) )),
% 7.39/1.48 inference(superposition,[],[f75,f51])).
% 7.39/1.48 thf(f244,plain,(
% 7.39/1.48 ( ! [X2 : a,X0 : a,X1 : a] : ((((sF4 @ X2 @ X1)) != $true) | (((sF4 @ X2 @ X0)) = $true) | (((sK1 @ X0 @ X1)) != $true)) )),
% 7.39/1.48 inference(superposition,[],[f41,f39])).
% 7.39/1.48 thf(f416,plain,(
% 7.39/1.48 ( ! [X0 : (a > $o)] : (($true = ((sF13 @ (sF5 @ (sF9 @ X0)) @ X0))) | (((sF7 @ (sF9 @ X0))) = $true)) )),
% 7.39/1.48 inference(superposition,[],[f179,f83])).
% 7.39/1.48 thf(f543,plain,(
% 7.39/1.48 ( ! [X0 : a,X1 : (a > $o)] : ((((sF15 @ X0 @ X1)) = ((sF4 @ X0 @ (sF12 @ X1 @ X0))))) )),
% 7.39/1.48 inference(superposition,[],[f78,f39])).
% 7.39/1.48 thf(f650,plain,(
% 7.39/1.48 ( ! [X2 : a,X0 : a,X1 : a] : ((((sK1 @ X2 @ X0)) != $true) | (((sK1 @ X0 @ X1)) != $true) | (((sF4 @ X1 @ X2)) = $true)) )),
% 7.39/1.48 inference(superposition,[],[f244,f39])).
% 7.39/1.48 thf(f738,plain,(
% 7.39/1.48 ( ! [X0 : a,X1 : a] : ((((sK1 @ (sF5 @ X0) @ X1)) != $true) | (((sF7 @ X0)) != $true) | (((sF4 @ X1 @ X0)) = $true)) )),
% 7.39/1.48 inference(superposition,[],[f650,f51])).
% 7.39/1.48 thf(f747,plain,(
% 7.39/1.48 ( ! [X0 : a,X1 : a] : ((((sF8 @ X0 @ X1)) != $true) | (((sF7 @ X1)) != $true) | (((sF4 @ (sF5 @ X0) @ X1)) = $true)) )),
% 7.39/1.48 inference(superposition,[],[f738,f57])).
% 7.39/1.48 thf(f1252,plain,(
% 7.39/1.48 (((sF7 @ (sF9 @ sF7))) = $true) | (((sF7 @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) = $true) | ($true != $true)),
% 7.39/1.48 inference(superposition,[],[f177,f416])).
% 7.39/1.48 thf(f1253,plain,(
% 7.39/1.48 (((sF7 @ (sF9 @ sF7))) = $true) | (((sF7 @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) = $true)),
% 7.39/1.48 inference(trivial_inequality_removal,[],[f1252])).
% 7.39/1.48 thf(f1255,definition,(
% 7.39/1.48 spl16_12 <=> (((sF7 @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) = $true)),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[spl16_12])],[avatar_definition])).
% 7.39/1.48 thf(f1257,plain,(
% 7.39/1.48 (((sF7 @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) = $true) | ~spl16_12),
% 7.39/1.48 inference(avatar_component_clause,[],[f1255])).
% 7.39/1.48 thf(f1259,definition,(
% 7.39/1.48 spl16_13 <=> (((sF7 @ (sF9 @ sF7))) = $true)),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[spl16_13])],[avatar_definition])).
% 7.39/1.48 thf(f1260,plain,(
% 7.39/1.48 (((sF7 @ (sF9 @ sF7))) != $true) | spl16_13),
% 7.39/1.48 inference(avatar_component_clause,[],[f1259])).
% 7.39/1.48 thf(f1261,plain,(
% 7.39/1.48 (((sF7 @ (sF9 @ sF7))) = $true) | ~spl16_13),
% 7.39/1.48 inference(avatar_component_clause,[],[f1259])).
% 7.39/1.48 thf(f1262,plain,(
% 7.39/1.48 spl16_12 | spl16_13),
% 7.39/1.48 inference(avatar_split_clause,[],[f1253,f1259,f1255])).
% 7.39/1.48 thf(f1453,plain,(
% 7.39/1.48 (((sF10 @ sF7 @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) = $true) | ($true != $true) | ~spl16_12),
% 7.39/1.48 inference(superposition,[],[f85,f1257])).
% 7.39/1.48 thf(f1460,plain,(
% 7.39/1.48 (((sF10 @ sF7 @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) = $true) | ~spl16_12),
% 7.39/1.48 inference(trivial_inequality_removal,[],[f1453])).
% 7.39/1.48 thf(f1468,definition,(
% 7.39/1.48 spl16_14 <=> (((sF13 @ (sF5 @ (sF9 @ sF7)) @ sF7)) = $true)),
% 7.39/1.48 introduced(definition,[new_symbols(definition,[spl16_14])],[avatar_definition])).
% 7.39/1.48 thf(f1469,plain,(
% 7.39/1.48 (((sF13 @ (sF5 @ (sF9 @ sF7)) @ sF7)) = $true) | ~spl16_14),
% 7.39/1.48 inference(avatar_component_clause,[],[f1468])).
% 7.39/1.48 thf(f1470,plain,(
% 7.39/1.48 (((sF13 @ (sF5 @ (sF9 @ sF7)) @ sF7)) != $true) | spl16_14),
% 7.39/1.48 inference(avatar_component_clause,[],[f1468])).
% 7.39/1.48 thf(f1476,plain,(
% 7.39/1.48 ($true != $true) | (((sF7 @ (sF9 @ sF7))) = $true) | spl16_14),
% 7.39/1.48 inference(superposition,[],[f1470,f416])).
% 7.39/1.48 thf(f1477,plain,(
% 7.39/1.48 (((sF7 @ (sF9 @ sF7))) = $true) | spl16_14),
% 7.39/1.48 inference(trivial_inequality_removal,[],[f1476])).
% 7.39/1.48 thf(f1478,plain,(
% 7.39/1.48 spl16_13 | spl16_14),
% 7.39/1.48 inference(avatar_split_clause,[],[f1477,f1468,f1259])).
% 7.39/1.48 thf(f1482,plain,(
% 7.39/1.48 ($true != $true) | (((sF8 @ (sF5 @ (sF9 @ sF7)) @ (sF9 @ sF7))) = $true) | ~spl16_13),
% 7.39/1.48 inference(superposition,[],[f123,f1261])).
% 7.39/1.48 thf(f1483,plain,(
% 7.39/1.48 ($true != $true) | (((sF6 @ (sF9 @ sF7))) != $true) | ~spl16_13),
% 7.39/1.48 inference(superposition,[],[f53,f1261])).
% 7.39/1.48 thf(f1486,plain,(
% 7.39/1.48 (((sF8 @ (sF5 @ (sF9 @ sF7)) @ (sF9 @ sF7))) = $true) | ~spl16_13),
% 7.39/1.48 inference(trivial_inequality_removal,[],[f1482])).
% 7.39/1.48 thf(f1487,plain,(
% 7.39/1.48 (((sF6 @ (sF9 @ sF7))) != $true) | ~spl16_13),
% 7.39/1.48 inference(trivial_inequality_removal,[],[f1483])).
% 7.39/1.48 thf(f1493,plain,(
% 7.39/1.48 (((sF7 @ (sF5 @ (sF9 @ sF7)))) = $true) | ~spl16_13),
% 7.39/1.48 inference(forward_demodulation,[],[f1486,f127])).
% 7.39/1.48 thf(f1504,plain,(
% 7.39/1.48 (((sF10 @ sF7 @ (sF5 @ (sF9 @ sF7)))) = $true) | ($true != $true) | ~spl16_13),
% 7.39/1.48 inference(superposition,[],[f85,f1493])).
% 7.39/1.48 thf(f1507,plain,(
% 7.39/1.48 (((sF10 @ sF7 @ (sF5 @ (sF9 @ sF7)))) = $true) | ~spl16_13),
% 7.39/1.48 inference(trivial_inequality_removal,[],[f1504])).
% 7.39/1.48 thf(f1515,plain,(
% 7.39/1.48 (((sF6 @ (sF9 @ sF7))) = $true) | ~spl16_13),
% 7.39/1.48 inference(forward_demodulation,[],[f1507,f137])).
% 7.39/1.48 thf(f1519,plain,(
% 7.39/1.48 $false | ~spl16_13),
% 7.39/1.48 inference(forward_subsumption_resolution,[],[f1515,f1487])).
% 7.39/1.48 thf(f1520,plain,(
% 7.39/1.48 ~spl16_13),
% 7.39/1.48 inference(avatar_contradiction_clause,[],[f1519])).
% 7.39/1.48 thf(f1930,plain,(
% 7.39/1.48 ($true != $true) | (((sF8 @ (sF9 @ sF7) @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) = $true) | ~spl16_12),
% 7.39/1.48 inference(superposition,[],[f140,f1460])).
% 7.39/1.48 thf(f1934,plain,(
% 7.39/1.48 (((sF8 @ (sF9 @ sF7) @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) = $true) | ~spl16_12),
% 7.39/1.48 inference(trivial_inequality_removal,[],[f1930])).
% 7.39/1.48 thf(f2513,plain,(
% 7.39/1.48 ($true != $true) | (((sF4 @ (sF5 @ (sF9 @ sF7)) @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) = $true) | (((sF7 @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) != $true) | ~spl16_12),
% 7.39/1.48 inference(superposition,[],[f747,f1934])).
% 7.39/1.48 thf(f2521,plain,(
% 7.39/1.48 (((sF4 @ (sF5 @ (sF9 @ sF7)) @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) = $true) | (((sF7 @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) != $true) | ~spl16_12),
% 7.39/1.48 inference(trivial_inequality_removal,[],[f2513])).
% 7.39/1.48 thf(f2524,plain,(
% 7.39/1.48 (((sF4 @ (sF5 @ (sF9 @ sF7)) @ (sF5 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7)))))) = $true) | ~spl16_12),
% 7.39/1.48 inference(forward_subsumption_resolution,[],[f2521,f1257])).
% 7.39/1.48 thf(f2525,plain,(
% 7.39/1.48 (((sF8 @ (sF9 @ sF7) @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7))))) = $true) | ~spl16_12),
% 7.39/1.48 inference(forward_demodulation,[],[f2524,f133])).
% 7.39/1.48 thf(f2526,plain,(
% 7.39/1.48 (((sF4 @ (sF5 @ (sF9 @ sF7)) @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7))))) = $true) | (((sF7 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7))))) != $true) | ($true != $true) | ~spl16_12),
% 7.39/1.48 inference(superposition,[],[f747,f2525])).
% 7.39/1.48 thf(f2533,plain,(
% 7.39/1.48 (((sF7 @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7))))) != $true) | (((sF4 @ (sF5 @ (sF9 @ sF7)) @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7))))) = $true) | ~spl16_12),
% 7.39/1.48 inference(trivial_inequality_removal,[],[f2526])).
% 7.39/1.48 thf(f2536,plain,(
% 7.39/1.48 (((sF13 @ (sF5 @ (sF9 @ sF7)) @ sF7)) != $true) | (((sF4 @ (sF5 @ (sF9 @ sF7)) @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7))))) = $true) | ~spl16_12),
% 7.39/1.48 inference(forward_demodulation,[],[f2533,f73])).
% 7.39/1.48 thf(f2538,plain,(
% 7.39/1.48 (((sF4 @ (sF5 @ (sF9 @ sF7)) @ (sF12 @ sF7 @ (sF5 @ (sF9 @ sF7))))) = $true) | (~spl16_12 | ~spl16_14)),
% 7.39/1.48 inference(forward_subsumption_resolution,[],[f2536,f1469])).
% 7.39/1.48 thf(f2539,plain,(
% 7.39/1.48 ($true = ((sF15 @ (sF5 @ (sF9 @ sF7)) @ sF7))) | (~spl16_12 | ~spl16_14)),
% 7.39/1.48 inference(forward_demodulation,[],[f2538,f543])).
% 7.39/1.48 thf(f2540,plain,(
% 7.39/1.48 ($true != $true) | (((sF14 @ (sF5 @ (sF9 @ sF7)) @ sF7)) = $true) | (~spl16_12 | ~spl16_14)),
% 7.39/1.48 inference(superposition,[],[f81,f2539])).
% 7.39/1.48 thf(f2541,plain,(
% 7.39/1.48 (((sF14 @ (sF5 @ (sF9 @ sF7)) @ sF7)) = $true) | (~spl16_12 | ~spl16_14)),
% 7.39/1.48 inference(trivial_inequality_removal,[],[f2540])).
% 7.39/1.48 thf(f2542,plain,(
% 7.39/1.48 (((sF7 @ (sF9 @ sF7))) = $true) | (~spl16_12 | ~spl16_14)),
% 7.39/1.48 inference(forward_demodulation,[],[f2541,f179])).
% 7.39/1.48 thf(f2543,plain,(
% 7.39/1.48 $false | (~spl16_12 | spl16_13 | ~spl16_14)),
% 7.39/1.48 inference(forward_subsumption_resolution,[],[f2542,f1260])).
% 7.39/1.48 thf(f2544,plain,(
% 7.39/1.48 ~spl16_12 | spl16_13 | ~spl16_14),
% 7.39/1.48 inference(avatar_contradiction_clause,[],[f2543])).
% 7.39/1.48 cnf(s8, plain, spl16_12 | spl16_13, inference(sat_conversion,[],[f1262])).
% 7.39/1.48 cnf(s10, plain, spl16_13 | spl16_14, inference(sat_conversion,[],[f1478])).
% 7.39/1.48 cnf(s11, plain, ~spl16_13, inference(sat_conversion,[],[f1520])).
% 7.39/1.48 cnf(s16, plain, ~spl16_12 | spl16_13 | ~spl16_14, inference(sat_conversion,[],[f2544])).
% 7.39/1.48 cnf(s17, plain, spl16_14, inference(rat,[],[s10,s11])).
% 7.39/1.48 cnf(s18, plain, ~spl16_12, inference(rat,[],[s16,s11,s17])).
% 7.39/1.48 cnf(s19, plain, $false, inference(rat,[],[s8,s11,s18])).
% 7.39/1.48 thf(f2545,plain,(
% 7.39/1.48 $false),
% 7.39/1.48 inference(avatar_sat_refutation,[],[s19])).
% 7.39/1.48 % SZS output end Proof for theBenchmark
% 7.39/1.48 % (2740258)------------------------------
% 7.39/1.48 % (2740258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.48 % (2740258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.48 % (2740258)CaDiCaL version: 2.1.3
% 7.39/1.48 % (2740258)Termination reason: Refutation
% 7.39/1.48 % (2740258)Time elapsed: 0.136 s
% 7.39/1.48 % (2740258)Peak memory usage: 14 MB
% 7.39/1.48 % (2740258)Instructions burned: 254 (million)
% 7.39/1.48 % (2740084)Success in time 1.228 s
% 7.39/1.48 % Vampire exiting
%------------------------------------------------------------------------------