%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU972^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:32:03 AM UTC 2026
% Result : Theorem 19.92s 3.29s
% Output : Refutation 19.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU972^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.28 % Computer : n011.cluster.edu
% 0.12/0.28 % Model : x86_64 x86_64
% 0.12/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.28 % Memory : 8046.5625MB
% 0.12/0.28 % OS : Linux 6.8.0-71-generic
% 0.12/0.28 % CPULimit : 300
% 0.12/0.28 % WCLimit : 300
% 0.12/0.28 % DateTime : Tue Sep 29 14:54:46 UTC 2026
% 0.12/0.28 % CPUTime :
% 0.12/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.29/0.32 Running higher-order theorem proving
% 0.29/0.34 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.08/0.55 % (186926)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.08/0.55 % (186932)lrs+10_16_si=on:nwc=1.5:random_seed=3672566187:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 1.08/0.55 % (186932)Instruction limit reached!
% 1.08/0.55 % (186932)------------------------------
% 1.08/0.55 % (186932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.55 % (186932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.55 % (186932)CaDiCaL version: 2.1.3
% 1.08/0.55 % (186932)Termination reason: Instruction limit
% 1.08/0.55 % (186932)Termination phase: Saturation
% 1.08/0.55 % (186932)Time elapsed: 0.009 s
% 1.08/0.55 % (186932)Peak memory usage: 12 MB
% 1.08/0.55 % (186932)Instructions burned: 18 (million)
% 1.08/0.55 % (186937)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.08/0.55 % (186937)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.08/0.55 % (186931)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4252708351:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 1.08/0.55 % (186935)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2730045384:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 1.08/0.55 % (186933)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3137880298:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 1.08/0.55 % (186934)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=3403667581: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)
% 1.08/0.55 % (186936)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=277767149:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 1.08/0.55 % (186937)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=533420024:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 1.08/0.55 % (186933)Instruction limit reached!
% 1.08/0.55 % (186933)------------------------------
% 1.08/0.55 % (186933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.55 % (186933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.55 % (186933)CaDiCaL version: 2.1.3
% 1.08/0.55 % (186933)Termination reason: Instruction limit
% 1.08/0.55 % (186933)Termination phase: Saturation
% 1.08/0.55 % (186933)Time elapsed: 0.004 s
% 1.08/0.55 % (186933)Peak memory usage: 12 MB
% 1.08/0.55 % (186933)Instructions burned: 4 (million)
% 1.08/0.55 % (186939)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2861599373:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.08/0.55 % (186939)Instruction limit reached!
% 1.08/0.55 % (186939)------------------------------
% 1.08/0.55 % (186939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.55 % (186939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.55 % (186939)CaDiCaL version: 2.1.3
% 1.08/0.55 % (186939)Termination reason: Instruction limit
% 1.08/0.55 % (186939)Termination phase: Saturation
% 1.08/0.55 % (186939)Time elapsed: 0.002 s
% 1.08/0.55 % (186939)Peak memory usage: 12 MB
% 1.08/0.55 % (186939)Instructions burned: 3 (million)
% 1.08/0.55 % (186935)Instruction limit reached!
% 1.08/0.55 % (186935)------------------------------
% 1.08/0.55 % (186935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.55 % (186935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.55 % (186935)CaDiCaL version: 2.1.3
% 1.08/0.55 % (186935)Termination reason: Instruction limit
% 1.08/0.55 % (186935)Termination phase: Saturation
% 1.08/0.55 % (186935)Time elapsed: 0.022 s
% 1.08/0.55 % (186935)Peak memory usage: 11 MB
% 1.08/0.55 % (186935)Instructions burned: 24 (million)
% 1.08/0.55 % (186946)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2645742424:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.08/0.55 % (186946)Instruction limit reached!
% 1.08/0.63 % (186946)------------------------------
% 1.08/0.63 % (186946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.63 % (186946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.63 % (186946)CaDiCaL version: 2.1.3
% 1.08/0.63 % (186946)Termination reason: Instruction limit
% 1.08/0.63 % (186946)Termination phase: Saturation
% 1.08/0.63 % (186946)Time elapsed: 0.006 s
% 1.08/0.63 % (186946)Peak memory usage: 12 MB
% 1.08/0.63 % (186946)Instructions burned: 5 (million)
% 1.08/0.63 % (186948)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.08/0.63 % (186948)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3062059045:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.08/0.63 % (186949)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1208507295:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.08/0.63 % (186949)Instruction limit reached!
% 1.08/0.63 % (186949)------------------------------
% 1.08/0.63 % (186949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.63 % (186949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.63 % (186949)CaDiCaL version: 2.1.3
% 1.08/0.63 % (186949)Termination reason: Instruction limit
% 1.08/0.63 % (186949)Termination phase: Saturation
% 1.08/0.63 % (186949)Time elapsed: 0.012 s
% 1.08/0.63 % (186949)Peak memory usage: 12 MB
% 1.08/0.63 % (186949)Instructions burned: 12 (million)
% 1.08/0.63 % (186948)Instruction limit reached!
% 1.08/0.63 % (186948)------------------------------
% 1.08/0.63 % (186948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.63 % (186948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.63 % (186948)CaDiCaL version: 2.1.3
% 1.08/0.63 % (186948)Termination reason: Instruction limit
% 1.08/0.63 % (186948)Termination phase: Saturation
% 1.08/0.63 % (186948)Time elapsed: 0.015 s
% 1.08/0.63 % (186948)Peak memory usage: 12 MB
% 1.08/0.63 % (186948)Instructions burned: 8 (million)
% 1.08/0.63 % (186936)Instruction limit reached!
% 1.08/0.63 % (186936)------------------------------
% 1.08/0.63 % (186936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.63 % (186936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.63 % (186936)CaDiCaL version: 2.1.3
% 1.08/0.63 % (186936)Termination reason: Instruction limit
% 1.08/0.63 % (186936)Termination phase: Saturation
% 1.08/0.63 % (186936)Time elapsed: 0.069 s
% 1.08/0.63 % (186936)Peak memory usage: 12 MB
% 1.08/0.63 % (186936)Instructions burned: 75 (million)
% 1.08/0.63 % (186951)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.08/0.63 % (186951)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.08/0.63 % (186951)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=596083681:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.08/0.64 % (186931)Instruction limit reached!
% 1.08/0.64 % (186931)------------------------------
% 1.08/0.64 % (186931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.64 % (186931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.64 % (186931)CaDiCaL version: 2.1.3
% 1.08/0.64 % (186931)Termination reason: Instruction limit
% 1.08/0.64 % (186931)Termination phase: Saturation
% 1.08/0.64 % (186931)Time elapsed: 0.080 s
% 1.08/0.64 % (186931)Peak memory usage: 12 MB
% 1.08/0.64 % (186931)Instructions burned: 88 (million)
% 1.08/0.64 % (186955)lrs+10_1_si=on:cs=on:random_seed=2685309824:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.08/0.64 % (186955)Instruction limit reached!
% 1.08/0.64 % (186955)------------------------------
% 1.08/0.64 % (186955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.64 % (186955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.64 % (186955)CaDiCaL version: 2.1.3
% 1.08/0.64 % (186955)Termination reason: Instruction limit
% 1.08/0.64 % (186955)Termination phase: Saturation
% 2.06/0.68 % (186955)Time elapsed: 0.005 s
% 2.06/0.68 % (186955)Peak memory usage: 12 MB
% 2.06/0.68 % (186955)Instructions burned: 10 (million)
% 2.06/0.68 % (186956)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 2.06/0.68 % (186954)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=3144951511:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 2.06/0.68 % (186956)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=4179589600:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.06/0.68 % (186951)Instruction limit reached!
% 2.06/0.68 % (186951)------------------------------
% 2.06/0.68 % (186951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.06/0.68 % (186956)Instruction limit reached!
% 2.06/0.68 % (186956)------------------------------
% 2.06/0.68 % (186956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.06/0.68 % (186951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/0.68 % (186956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/0.68 % (186951)CaDiCaL version: 2.1.3
% 2.06/0.68 % (186956)CaDiCaL version: 2.1.3
% 2.06/0.68 % (186951)Termination reason: Instruction limit
% 2.06/0.68 % (186951)Termination phase: Saturation
% 2.06/0.68 % (186956)Termination reason: Instruction limit
% 2.06/0.68 % (186956)Termination phase: Saturation
% 2.06/0.68 % (186951)Time elapsed: 0.027 s
% 2.06/0.68 % (186956)Time elapsed: 0.002 s
% 2.06/0.68 % (186951)Peak memory usage: 12 MB
% 2.06/0.68 % (186956)Peak memory usage: 10 MB
% 2.06/0.68 % (186951)Instructions burned: 28 (million)
% 2.06/0.68 % (186956)Instructions burned: 2 (million)
% 2.06/0.68 % (186960)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3608583804:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 2.06/0.68 % (186958)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4111893400:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 2.06/0.68 % (186963)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3803160174:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 2.06/0.68 % (186964)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2840704255:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.06/0.68 % (186937)Instruction limit reached!
% 2.06/0.68 % (186937)------------------------------
% 2.06/0.68 % (186937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.06/0.68 % (186937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/0.68 % (186937)CaDiCaL version: 2.1.3
% 2.06/0.68 % (186937)Termination reason: Instruction limit
% 2.06/0.68 % (186937)Termination phase: Saturation
% 2.06/0.68 % (186937)Time elapsed: 0.144 s
% 2.06/0.68 % (186937)Peak memory usage: 13 MB
% 2.06/0.68 % (186937)Instructions burned: 157 (million)
% 2.06/0.68 % (186958)Refutation not found, incomplete strategy
% 2.06/0.68 % (186958)------------------------------
% 2.06/0.68 % (186958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.06/0.68 % (186958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/0.68 % (186958)CaDiCaL version: 2.1.3
% 2.06/0.68 % (186958)Termination reason: Refutation not found, incomplete strategy
% 2.06/0.68 % (186958)Time elapsed: 0.035 s
% 2.06/0.68 % (186958)Peak memory usage: 12 MB
% 2.06/0.68 % (186958)Instructions burned: 36 (million)
% 2.06/0.68 % (186958)------------------------------
% 2.06/0.68 % (186958)------------------------------
% 2.06/0.68 % (186963)Refutation not found, incomplete strategy
% 2.06/0.68 % (186963)------------------------------
% 2.06/0.68 % (186963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.06/0.68 % (186963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/0.68 % (186963)CaDiCaL version: 2.1.3
% 2.06/0.68 % (186963)Termination reason: Refutation not found, incomplete strategy
% 2.06/0.68 % (186963)Time elapsed: 0.009 s
% 2.06/0.68 % (186963)Peak memory usage: 12 MB
% 2.06/0.68 % (186963)Instructions burned: 7 (million)
% 2.46/0.80 % (186963)------------------------------
% 2.46/0.80 % (186963)------------------------------
% 2.46/0.80 % (186964)Instruction limit reached!
% 2.46/0.80 % (186964)------------------------------
% 2.46/0.80 % (186964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.80 % (186964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.80 % (186964)CaDiCaL version: 2.1.3
% 2.46/0.80 % (186964)Termination reason: Instruction limit
% 2.46/0.80 % (186964)Termination phase: Saturation
% 2.46/0.80 % (186964)Time elapsed: 0.016 s
% 2.46/0.80 % (186964)Peak memory usage: 12 MB
% 2.46/0.80 % (186964)Instructions burned: 15 (million)
% 2.46/0.80 % (186954)Instruction limit reached!
% 2.46/0.80 % (186954)------------------------------
% 2.46/0.80 % (186954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.80 % (186954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.80 % (186954)CaDiCaL version: 2.1.3
% 2.46/0.80 % (186954)Termination reason: Instruction limit
% 2.46/0.80 % (186954)Termination phase: Saturation
% 2.46/0.80 % (186954)Time elapsed: 0.075 s
% 2.46/0.80 % (186954)Peak memory usage: 12 MB
% 2.46/0.80 % (186954)Instructions burned: 87 (million)
% 2.46/0.80 % (186969)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3128466497:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.46/0.80 % (186970)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=114324223:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.46/0.80 % (186972)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3965435405:i=26:ep=R:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/26Mi)
% 2.46/0.80 % (186970)Instruction limit reached!
% 2.46/0.80 % (186970)------------------------------
% 2.46/0.80 % (186970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.80 % (186970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.80 % (186970)CaDiCaL version: 2.1.3
% 2.46/0.80 % (186970)Termination reason: Instruction limit
% 2.46/0.80 % (186970)Termination phase: Saturation
% 2.46/0.80 % (186970)Time elapsed: 0.015 s
% 2.46/0.80 % (186970)Peak memory usage: 12 MB
% 2.46/0.80 % (186970)Instructions burned: 15 (million)
% 2.46/0.80 % (186973)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3447136506:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.46/0.80 % (186971)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=445558490: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)
% 2.46/0.80 % (186972)Instruction limit reached!
% 2.46/0.80 % (186972)------------------------------
% 2.46/0.80 % (186972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.80 % (186972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.80 % (186972)CaDiCaL version: 2.1.3
% 2.46/0.80 % (186972)Termination reason: Instruction limit
% 2.46/0.80 % (186972)Termination phase: Saturation
% 2.46/0.80 % (186972)Time elapsed: 0.025 s
% 2.46/0.80 % (186972)Peak memory usage: 12 MB
% 2.46/0.80 % (186972)Instructions burned: 27 (million)
% 2.46/0.80 % (186971)Instruction limit reached!
% 2.46/0.80 % (186971)------------------------------
% 2.46/0.80 % (186971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.80 % (186971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.80 % (186971)CaDiCaL version: 2.1.3
% 2.46/0.80 % (186971)Termination reason: Instruction limit
% 2.46/0.80 % (186971)Termination phase: Property scanning
% 2.46/0.80 % (186971)Time elapsed: 0.006 s
% 2.46/0.80 % (186971)Peak memory usage: 11 MB
% 2.46/0.80 % (186971)Instructions burned: 2 (million)
% 2.46/0.80 % (186960)Instruction limit reached!
% 2.46/0.80 % (186960)------------------------------
% 2.46/0.80 % (186960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.80 % (186960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.80 % (186960)CaDiCaL version: 2.1.3
% 2.46/0.80 % (186960)Termination reason: Instruction limit
% 2.46/0.80 % (186960)Termination phase: Saturation
% 2.46/0.80 % (186960)Time elapsed: 0.114 s
% 2.46/0.80 % (186960)Peak memory usage: 13 MB
% 2.46/0.80 % (186960)Instructions burned: 249 (million)
% 2.46/0.80 % (186973)Instruction limit reached!
% 2.46/0.80 % (186973)------------------------------
% 3.53/0.91 % (186973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.91 % (186973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.91 % (186973)CaDiCaL version: 2.1.3
% 3.53/0.91 % (186973)Termination reason: Instruction limit
% 3.53/0.91 % (186973)Termination phase: Saturation
% 3.53/0.91 % (186973)Time elapsed: 0.022 s
% 3.53/0.91 % (186973)Peak memory usage: 11 MB
% 3.53/0.91 % (186973)Instructions burned: 23 (million)
% 3.53/0.91 % (186977)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1883613371:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 3.53/0.91 % (186982)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=726998910:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 3.53/0.91 % (186980)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 3.53/0.91 % (186980)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 3.53/0.91 % (186981)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 3.53/0.91 % (186980)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=3322006220:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 3.53/0.91 % (186981)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=201151513:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 3.53/0.91 % (186982)Instruction limit reached!
% 3.53/0.91 % (186982)------------------------------
% 3.53/0.91 % (186982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.91 % (186982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.91 % (186982)CaDiCaL version: 2.1.3
% 3.53/0.91 % (186982)Termination reason: Instruction limit
% 3.53/0.91 % (186982)Termination phase: Saturation
% 3.53/0.91 % (186982)Time elapsed: 0.015 s
% 3.53/0.91 % (186982)Peak memory usage: 12 MB
% 3.53/0.91 % (186982)Instructions burned: 32 (million)
% 3.53/0.91 % (186984)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1344977703:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 3.53/0.91 % (186981)Instruction limit reached!
% 3.53/0.91 % (186981)------------------------------
% 3.53/0.91 % (186981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.91 % (186981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.91 % (186981)CaDiCaL version: 2.1.3
% 3.53/0.91 % (186981)Termination reason: Instruction limit
% 3.53/0.91 % (186981)Termination phase: Saturation
% 3.53/0.91 % (186981)Time elapsed: 0.010 s
% 3.53/0.91 % (186981)Peak memory usage: 12 MB
% 3.53/0.91 % (186981)Instructions burned: 8 (million)
% 3.53/0.91 % (186980)Instruction limit reached!
% 3.53/0.91 % (186980)------------------------------
% 3.53/0.91 % (186980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.91 % (186980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.91 % (186980)CaDiCaL version: 2.1.3
% 3.53/0.91 % (186980)Termination reason: Instruction limit
% 3.53/0.91 % (186980)Termination phase: Saturation
% 3.53/0.91 % (186980)Time elapsed: 0.014 s
% 3.53/0.91 % (186980)Peak memory usage: 12 MB
% 3.53/0.91 % (186980)Instructions burned: 14 (million)
% 3.53/0.91 % (186984)Instruction limit reached!
% 3.53/0.91 % (186984)------------------------------
% 3.53/0.91 % (186984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.91 % (186984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.91 % (186984)CaDiCaL version: 2.1.3
% 3.53/0.91 % (186984)Termination reason: Instruction limit
% 3.53/0.91 % (186984)Termination phase: Saturation
% 3.53/0.91 % (186984)Time elapsed: 0.009 s
% 3.53/0.91 % (186984)Peak memory usage: 12 MB
% 3.53/0.91 % (186984)Instructions burned: 8 (million)
% 3.53/0.91 % (186988)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2321523967:i=23:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/23Mi)
% 3.53/1.01 % (186977)Instruction limit reached!
% 3.53/1.01 % (186977)------------------------------
% 3.53/1.01 % (186977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/1.01 % (186977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.01 % (186977)CaDiCaL version: 2.1.3
% 3.53/1.01 % (186977)Termination reason: Instruction limit
% 3.53/1.01 % (186977)Termination phase: Saturation
% 3.53/1.01 % (186977)Time elapsed: 0.055 s
% 3.53/1.01 % (186977)Peak memory usage: 12 MB
% 3.53/1.01 % (186977)Instructions burned: 60 (million)
% 3.53/1.01 % (186988)Instruction limit reached!
% 3.53/1.01 % (186988)------------------------------
% 3.53/1.01 % (186988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/1.01 % (186988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.01 % (186988)CaDiCaL version: 2.1.3
% 3.53/1.01 % (186988)Termination reason: Instruction limit
% 3.53/1.01 % (186988)Termination phase: Saturation
% 3.53/1.01 % (186988)Time elapsed: 0.009 s
% 3.53/1.01 % (186988)Peak memory usage: 11 MB
% 3.53/1.01 % (186988)Instructions burned: 23 (million)
% 3.53/1.01 % (186990)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1125064578:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/20Mi)
% 3.53/1.01 % (186992)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3716801221:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 3.53/1.01 % (186995)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2609712783:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.53/1.01 % (186991)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=710551457:i=1240:rtra=on:ixr=off_2996 on theBenchmark for (2996ds/1240Mi)
% 3.53/1.01 % (186994)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1106634655:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.53/1.01 % (186990)Instruction limit reached!
% 3.53/1.01 % (186990)------------------------------
% 3.53/1.01 % (186990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/1.01 % (186990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.01 % (186990)CaDiCaL version: 2.1.3
% 3.53/1.01 % (186990)Termination reason: Instruction limit
% 3.53/1.01 % (186990)Termination phase: Saturation
% 3.53/1.01 % (186990)Time elapsed: 0.021 s
% 3.53/1.01 % (186990)Peak memory usage: 12 MB
% 3.53/1.01 % (186990)Instructions burned: 21 (million)
% 3.53/1.01 % (186995)Instruction limit reached!
% 3.53/1.01 % (186995)------------------------------
% 3.53/1.01 % (186995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/1.01 % (186995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.01 % (186995)CaDiCaL version: 2.1.3
% 3.53/1.01 % (186995)Termination reason: Instruction limit
% 3.53/1.01 % (186995)Termination phase: Saturation
% 3.53/1.01 % (186995)Time elapsed: 0.020 s
% 3.53/1.01 % (186995)Peak memory usage: 12 MB
% 3.53/1.01 % (186995)Instructions burned: 44 (million)
% 3.53/1.01 % (187002)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3154120551:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.53/1.01 % (187001)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.53/1.01 % (187001)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3637555228:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.53/1.01 % (187001)Instruction limit reached!
% 3.53/1.01 % (187001)------------------------------
% 3.53/1.01 % (187001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/1.01 % (187001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.01 % (187001)CaDiCaL version: 2.1.3
% 3.53/1.01 % (187001)Termination reason: Instruction limit
% 3.53/1.01 % (187001)Termination phase: Saturation
% 3.53/1.01 % (187001)Time elapsed: 0.007 s
% 3.53/1.01 % (187001)Peak memory usage: 12 MB
% 3.53/1.01 % (187001)Instructions burned: 8 (million)
% 3.53/1.01 % (187005)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=375177909:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2995 on theBenchmark for (2995ds/169Mi)
% 5.06/1.17 % (187002)Instruction limit reached!
% 5.06/1.17 % (187002)------------------------------
% 5.06/1.17 % (187002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.06/1.17 % (187002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.17 % (187002)CaDiCaL version: 2.1.3
% 5.06/1.17 % (187002)Termination reason: Instruction limit
% 5.06/1.17 % (187002)Termination phase: Saturation
% 5.06/1.17 % (187002)Time elapsed: 0.084 s
% 5.06/1.17 % (187002)Peak memory usage: 13 MB
% 5.06/1.17 % (187002)Instructions burned: 181 (million)
% 5.06/1.17 % (186992)Instruction limit reached!
% 5.06/1.17 % (186992)------------------------------
% 5.06/1.17 % (186992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.06/1.17 % (186992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.17 % (186992)CaDiCaL version: 2.1.3
% 5.06/1.17 % (186992)Termination reason: Instruction limit
% 5.06/1.17 % (186992)Termination phase: Saturation
% 5.06/1.17 % (186992)Time elapsed: 0.129 s
% 5.06/1.17 % (186992)Peak memory usage: 13 MB
% 5.06/1.17 % (186992)Instructions burned: 144 (million)
% 5.06/1.17 % (187007)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 5.06/1.17 % (186969)Instruction limit reached!
% 5.06/1.17 % (186969)------------------------------
% 5.06/1.17 % (186969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.06/1.17 % (186969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.17 % (186969)CaDiCaL version: 2.1.3
% 5.06/1.17 % (186969)Termination reason: Instruction limit
% 5.06/1.17 % (186969)Termination phase: Saturation
% 5.06/1.17 % (186969)Time elapsed: 0.280 s
% 5.06/1.17 % (186969)Peak memory usage: 13 MB
% 5.06/1.17 % (186969)Instructions burned: 327 (million)
% 5.06/1.17 % (187007)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=299711766:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2995 on theBenchmark for (2995ds/6Mi)
% 5.06/1.17 % (187008)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2316386855:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 5.06/1.17 % (187007)Instruction limit reached!
% 5.06/1.17 % (187007)------------------------------
% 5.06/1.17 % (187007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.06/1.17 % (187007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.17 % (187007)CaDiCaL version: 2.1.3
% 5.06/1.17 % (187007)Termination reason: Instruction limit
% 5.06/1.17 % (187007)Termination phase: Saturation
% 5.06/1.17 % (187007)Time elapsed: 0.007 s
% 5.06/1.17 % (187007)Peak memory usage: 11 MB
% 5.06/1.17 % (187007)Instructions burned: 6 (million)
% 5.06/1.17 % (187008)Instruction limit reached!
% 5.06/1.17 % (187008)------------------------------
% 5.06/1.17 % (187008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.06/1.17 % (187008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.17 % (187008)CaDiCaL version: 2.1.3
% 5.06/1.17 % (187008)Termination reason: Instruction limit
% 5.06/1.17 % (187008)Termination phase: Saturation
% 5.06/1.17 % (187008)Time elapsed: 0.019 s
% 5.06/1.17 % (187008)Peak memory usage: 12 MB
% 5.06/1.17 % (187008)Instructions burned: 22 (million)
% 5.06/1.17 % (186994)Instruction limit reached!
% 5.06/1.17 % (186994)------------------------------
% 5.06/1.17 % (186994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.06/1.17 % (186994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.17 % (186994)CaDiCaL version: 2.1.3
% 5.06/1.17 % (186994)Termination reason: Instruction limit
% 5.06/1.17 % (186994)Termination phase: Saturation
% 5.06/1.17 % (186994)Time elapsed: 0.169 s
% 5.06/1.17 % (186994)Peak memory usage: 13 MB
% 5.06/1.17 % (186994)Instructions burned: 193 (million)
% 5.06/1.17 % (187009)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=4216345530:i=19:add=on:rtra=on_2994 on theBenchmark for (2994ds/19Mi)
% 5.06/1.17 % (187009)Instruction limit reached!
% 5.06/1.17 % (187009)------------------------------
% 5.06/1.17 % (187009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.06/1.17 % (187009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.35 % (187009)CaDiCaL version: 2.1.3
% 6.37/1.35 % (187009)Termination reason: Instruction limit
% 6.37/1.35 % (187009)Termination phase: Saturation
% 6.37/1.35 % (187009)Time elapsed: 0.018 s
% 6.37/1.35 % (187009)Peak memory usage: 12 MB
% 6.37/1.35 % (187009)Instructions burned: 19 (million)
% 6.37/1.35 % (187012)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=3132887002:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/316Mi)
% 6.37/1.35 % (187013)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=4198209881:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2994 on theBenchmark for (2994ds/853Mi)
% 6.37/1.35 % (187014)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=3513887648:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2994 on theBenchmark for (2994ds/45Mi)
% 6.37/1.35 % (186934)Instruction limit reached!
% 6.37/1.35 % (186934)------------------------------
% 6.37/1.35 % (186934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.35 % (186934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.35 % (186934)CaDiCaL version: 2.1.3
% 6.37/1.35 % (186934)Termination reason: Instruction limit
% 6.37/1.35 % (186934)Termination phase: Saturation
% 6.37/1.35 % (186934)Time elapsed: 0.523 s
% 6.37/1.35 % (186934)Peak memory usage: 13 MB
% 6.37/1.35 % (186934)Instructions burned: 634 (million)
% 6.37/1.35 % (187017)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=314978499:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 6.37/1.35 % (187005)Instruction limit reached!
% 6.37/1.35 % (187005)------------------------------
% 6.37/1.35 % (187005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.35 % (187005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.35 % (187005)CaDiCaL version: 2.1.3
% 6.37/1.35 % (187005)Termination reason: Instruction limit
% 6.37/1.35 % (187005)Termination phase: Saturation
% 6.37/1.35 % (187005)Time elapsed: 0.158 s
% 6.37/1.35 % (187005)Peak memory usage: 13 MB
% 6.37/1.35 % (187005)Instructions burned: 169 (million)
% 6.37/1.35 % (187020)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1287605198:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 6.37/1.35 % (187014)Instruction limit reached!
% 6.37/1.35 % (187014)------------------------------
% 6.37/1.35 % (187014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.35 % (187014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.35 % (187014)CaDiCaL version: 2.1.3
% 6.37/1.35 % (187014)Termination reason: Instruction limit
% 6.37/1.35 % (187014)Termination phase: Saturation
% 6.37/1.35 % (187014)Time elapsed: 0.043 s
% 6.37/1.35 % (187014)Peak memory usage: 12 MB
% 6.37/1.35 % (187014)Instructions burned: 45 (million)
% 6.37/1.35 % (187020)Instruction limit reached!
% 6.37/1.35 % (187020)------------------------------
% 6.37/1.35 % (187020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.35 % (187020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.35 % (187020)CaDiCaL version: 2.1.3
% 6.37/1.35 % (187020)Termination reason: Instruction limit
% 6.37/1.35 % (187020)Termination phase: Saturation
% 6.37/1.35 % (187020)Time elapsed: 0.020 s
% 6.37/1.35 % (187020)Peak memory usage: 12 MB
% 6.37/1.35 % (187020)Instructions burned: 21 (million)
% 6.37/1.35 % (187022)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 6.37/1.35 % (187022)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3794910939:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/200Mi)
% 6.37/1.35 % (187024)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2198226263:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2993 on theBenchmark for (2993ds/13Mi)
% 6.37/1.35 % (187025)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=2324249621:i=66:s2at=3:nm=2:rtra=on:rawr=on_2993 on theBenchmark for (2993ds/66Mi)
% 7.52/1.52 % (187024)Instruction limit reached!
% 7.52/1.52 % (187024)------------------------------
% 7.52/1.52 % (187024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.52/1.52 % (187024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.52 % (187024)CaDiCaL version: 2.1.3
% 7.52/1.52 % (187024)Termination reason: Instruction limit
% 7.52/1.52 % (187024)Termination phase: Saturation
% 7.52/1.52 % (187024)Time elapsed: 0.013 s
% 7.52/1.52 % (187024)Peak memory usage: 12 MB
% 7.52/1.52 % (187024)Instructions burned: 13 (million)
% 7.52/1.52 % (187029)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3702383950:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 7.52/1.52 % (187025)Instruction limit reached!
% 7.52/1.52 % (187025)------------------------------
% 7.52/1.52 % (187025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.52/1.52 % (187025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.52 % (187025)CaDiCaL version: 2.1.3
% 7.52/1.52 % (187025)Termination reason: Instruction limit
% 7.52/1.52 % (187025)Termination phase: Saturation
% 7.52/1.52 % (187025)Time elapsed: 0.062 s
% 7.52/1.52 % (187025)Peak memory usage: 13 MB
% 7.52/1.52 % (187025)Instructions burned: 66 (million)
% 7.52/1.52 % (187029)Instruction limit reached!
% 7.52/1.52 % (187029)------------------------------
% 7.52/1.52 % (187029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.52/1.52 % (187029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.52 % (187029)CaDiCaL version: 2.1.3
% 7.52/1.52 % (187029)Termination reason: Instruction limit
% 7.52/1.52 % (187029)Termination phase: Saturation
% 7.52/1.52 % (187029)Time elapsed: 0.049 s
% 7.52/1.52 % (187029)Peak memory usage: 12 MB
% 7.52/1.52 % (187029)Instructions burned: 51 (million)
% 7.52/1.52 % (187031)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1972894157:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/31Mi)
% 7.52/1.52 % (187032)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3417250588:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2992 on theBenchmark for (2992ds/137Mi)
% 7.52/1.52 % (187031)Refutation not found, incomplete strategy
% 7.52/1.52 % (187031)------------------------------
% 7.52/1.52 % (187031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.52/1.52 % (187031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.52 % (187031)CaDiCaL version: 2.1.3
% 7.52/1.52 % (187031)Termination reason: Refutation not found, incomplete strategy
% 7.52/1.52 % (187031)Time elapsed: 0.024 s
% 7.52/1.52 % (187031)Peak memory usage: 13 MB
% 7.52/1.52 % (187031)Instructions burned: 27 (million)
% 7.52/1.52 % (187031)------------------------------
% 7.52/1.52 % (187031)------------------------------
% 7.52/1.52 % (187012)Instruction limit reached!
% 7.52/1.52 % (187012)------------------------------
% 7.52/1.52 % (187012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.52/1.52 % (187012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.52 % (187012)CaDiCaL version: 2.1.3
% 7.52/1.52 % (187012)Termination reason: Instruction limit
% 7.52/1.52 % (187012)Termination phase: Saturation
% 7.52/1.52 % (187012)Time elapsed: 0.226 s
% 7.52/1.52 % (187012)Peak memory usage: 14 MB
% 7.52/1.52 % (187012)Instructions burned: 318 (million)
% 7.52/1.52 % (187036)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=994516801:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2992 on theBenchmark for (2992ds/67Mi)
% 7.52/1.52 % (187022)Instruction limit reached!
% 7.52/1.52 % (187022)------------------------------
% 7.52/1.52 % (187022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.52/1.52 % (187022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.52 % (187022)CaDiCaL version: 2.1.3
% 7.52/1.52 % (187022)Termination reason: Instruction limit
% 7.52/1.52 % (187022)Termination phase: Saturation
% 7.52/1.52 % (187022)Time elapsed: 0.175 s
% 7.52/1.52 % (187022)Peak memory usage: 12 MB
% 7.52/1.52 % (187022)Instructions burned: 200 (million)
% 7.52/1.52 % (187035)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=1970832818:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 8.50/1.72 % (187038)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 8.50/1.72 % (187036)Instruction limit reached!
% 8.50/1.72 % (187036)------------------------------
% 8.50/1.72 % (187036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.50/1.72 % (187036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.50/1.72 % (187036)CaDiCaL version: 2.1.3
% 8.50/1.72 % (187036)Termination reason: Instruction limit
% 8.50/1.72 % (187036)Termination phase: Saturation
% 8.50/1.72 % (187036)Time elapsed: 0.035 s
% 8.50/1.72 % (187036)Peak memory usage: 12 MB
% 8.50/1.72 % (187036)Instructions burned: 68 (million)
% 8.50/1.72 % (187035)Instruction limit reached!
% 8.50/1.72 % (187035)------------------------------
% 8.50/1.72 % (187035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.50/1.72 % (187035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.50/1.72 % (187035)CaDiCaL version: 2.1.3
% 8.50/1.72 % (187035)Termination reason: Instruction limit
% 8.50/1.72 % (187035)Termination phase: Saturation
% 8.50/1.72 % (187035)Time elapsed: 0.030 s
% 8.50/1.72 % (187035)Peak memory usage: 12 MB
% 8.50/1.72 % (187035)Instructions burned: 34 (million)
% 8.50/1.72 % (187038)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=288267962:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2991 on theBenchmark for (2991ds/180Mi)
% 8.50/1.72 % (187040)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1731018794:st=2:i=246:sd=3:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/246Mi)
% 8.50/1.72 % (187041)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1516364722:cond=on:i=96:bd=all:rtra=on_2991 on theBenchmark for (2991ds/96Mi)
% 8.50/1.72 % (187032)Instruction limit reached!
% 8.50/1.72 % (187032)------------------------------
% 8.50/1.72 % (187032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.50/1.72 % (187032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.50/1.72 % (187032)CaDiCaL version: 2.1.3
% 8.50/1.72 % (187032)Termination reason: Instruction limit
% 8.50/1.72 % (187032)Termination phase: Saturation
% 8.50/1.72 % (187032)Time elapsed: 0.122 s
% 8.50/1.72 % (187032)Peak memory usage: 12 MB
% 8.50/1.72 % (187032)Instructions burned: 137 (million)
% 8.50/1.72 % (187045)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3641172652:i=427:sd=1:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/427Mi)
% 8.50/1.72 % (187040)Instruction limit reached!
% 8.50/1.72 % (187040)------------------------------
% 8.50/1.72 % (187040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.50/1.72 % (187040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.50/1.72 % (187040)CaDiCaL version: 2.1.3
% 8.50/1.72 % (187040)Termination reason: Instruction limit
% 8.50/1.72 % (187040)Termination phase: Saturation
% 8.50/1.72 % (187040)Time elapsed: 0.113 s
% 8.50/1.72 % (187040)Peak memory usage: 13 MB
% 8.50/1.72 % (187040)Instructions burned: 246 (million)
% 8.50/1.72 % (187041)Instruction limit reached!
% 8.50/1.72 % (187041)------------------------------
% 8.50/1.72 % (187041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.50/1.72 % (187041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.50/1.72 % (187041)CaDiCaL version: 2.1.3
% 8.50/1.72 % (187041)Termination reason: Instruction limit
% 8.50/1.72 % (187041)Termination phase: Saturation
% 8.50/1.72 % (187041)Time elapsed: 0.099 s
% 8.50/1.72 % (187041)Peak memory usage: 12 MB
% 8.50/1.72 % (187041)Instructions burned: 96 (million)
% 8.50/1.72 % (187017)Instruction limit reached!
% 8.50/1.72 % (187017)------------------------------
% 8.50/1.72 % (187017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.50/1.72 % (187017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.50/1.72 % (187017)CaDiCaL version: 2.1.3
% 8.50/1.72 % (187017)Termination reason: Instruction limit
% 8.50/1.72 % (187017)Termination phase: Saturation
% 8.50/1.72 % (187017)Time elapsed: 0.397 s
% 8.50/1.72 % (187017)Peak memory usage: 13 MB
% 8.50/1.72 % (187017)Instructions burned: 480 (million)
% 8.50/1.72 % (187038)Instruction limit reached!
% 8.50/1.72 % (187038)------------------------------
% 8.50/1.72 % (187038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.84 % (187038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.84 % (187038)CaDiCaL version: 2.1.3
% 8.80/1.84 % (187038)Termination reason: Instruction limit
% 8.80/1.84 % (187038)Termination phase: Saturation
% 8.80/1.84 % (187038)Time elapsed: 0.148 s
% 8.80/1.84 % (187038)Peak memory usage: 14 MB
% 8.80/1.84 % (187038)Instructions burned: 180 (million)
% 8.80/1.84 % (187048)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=237005362:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/515Mi)
% 8.80/1.84 % (187047)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3340888202:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/874Mi)
% 8.80/1.84 % (187050)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2495286406:i=44:ep=R:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/44Mi)
% 8.80/1.84 % (187049)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=4292576801:st=1.5:i=130:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/130Mi)
% 8.80/1.84 % (187050)Instruction limit reached!
% 8.80/1.84 % (187050)------------------------------
% 8.80/1.84 % (187050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.84 % (187050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.84 % (187050)CaDiCaL version: 2.1.3
% 8.80/1.84 % (187050)Termination reason: Instruction limit
% 8.80/1.84 % (187050)Termination phase: Saturation
% 8.80/1.84 % (187050)Time elapsed: 0.022 s
% 8.80/1.84 % (187050)Peak memory usage: 12 MB
% 8.80/1.84 % (187050)Instructions burned: 45 (million)
% 8.80/1.84 % (187055)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2047024679:s2a=on:i=571:nm=16:rtra=on_2989 on theBenchmark for (2989ds/571Mi)
% 8.80/1.84 % (187055)Refutation not found, incomplete strategy
% 8.80/1.84 % (187055)------------------------------
% 8.80/1.84 % (187055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.84 % (187055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.84 % (187055)CaDiCaL version: 2.1.3
% 8.80/1.84 % (187055)Termination reason: Refutation not found, incomplete strategy
% 8.80/1.84 % (187055)Time elapsed: 0.018 s
% 8.80/1.84 % (187055)Peak memory usage: 12 MB
% 8.80/1.84 % (187055)Instructions burned: 35 (million)
% 8.80/1.84 % (187055)------------------------------
% 8.80/1.84 % (187055)------------------------------
% 8.80/1.84 % (187057)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=2651956169:i=450:rtra=on:ixr=off:ntd=on_2989 on theBenchmark for (2989ds/450Mi)
% 8.80/1.84 % (187057)Refutation not found, incomplete strategy
% 8.80/1.84 % (187057)------------------------------
% 8.80/1.84 % (187057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.84 % (187057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.84 % (187057)CaDiCaL version: 2.1.3
% 8.80/1.84 % (187057)Termination reason: Refutation not found, incomplete strategy
% 8.80/1.84 % (187057)Time elapsed: 0.009 s
% 8.80/1.84 % (187057)Peak memory usage: 12 MB
% 8.80/1.84 % (187057)Instructions burned: 17 (million)
% 8.80/1.84 % (187057)------------------------------
% 8.80/1.84 % (187057)------------------------------
% 8.80/1.84 % (187059)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1319805332:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/95Mi)
% 8.80/1.84 % (187049)Instruction limit reached!
% 8.80/1.84 % (187049)------------------------------
% 8.80/1.84 % (187049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.84 % (187049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.84 % (187049)CaDiCaL version: 2.1.3
% 8.80/1.84 % (187049)Termination reason: Instruction limit
% 8.80/1.84 % (187049)Termination phase: Saturation
% 8.80/1.84 % (187049)Time elapsed: 0.113 s
% 8.80/1.84 % (187049)Peak memory usage: 12 MB
% 8.80/1.84 % (187049)Instructions burned: 130 (million)
% 8.80/1.84 % (187061)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=2313465192:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2988 on theBenchmark for (2988ds/65Mi)
% 8.80/1.84 % (187059)Instruction limit reached!
% 8.80/1.84 % (187059)------------------------------
% 8.80/1.84 % (187059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.02/2.09 % (187059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.09 % (187059)CaDiCaL version: 2.1.3
% 12.02/2.09 % (187059)Termination reason: Instruction limit
% 12.02/2.09 % (187059)Termination phase: Saturation
% 12.02/2.09 % (187059)Time elapsed: 0.045 s
% 12.02/2.09 % (187059)Peak memory usage: 12 MB
% 12.02/2.09 % (187059)Instructions burned: 96 (million)
% 12.02/2.09 % (187063)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=2716362849:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2988 on theBenchmark for (2988ds/105Mi)
% 12.02/2.09 % (187061)Instruction limit reached!
% 12.02/2.09 % (187061)------------------------------
% 12.02/2.09 % (187061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.02/2.09 % (187061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.09 % (187061)CaDiCaL version: 2.1.3
% 12.02/2.09 % (187061)Termination reason: Instruction limit
% 12.02/2.09 % (187061)Termination phase: Saturation
% 12.02/2.09 % (187061)Time elapsed: 0.059 s
% 12.02/2.09 % (187061)Peak memory usage: 12 MB
% 12.02/2.09 % (187061)Instructions burned: 65 (million)
% 12.02/2.09 % (187063)Instruction limit reached!
% 12.02/2.09 % (187063)------------------------------
% 12.02/2.09 % (187063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.02/2.09 % (187063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.09 % (187063)CaDiCaL version: 2.1.3
% 12.02/2.09 % (187063)Termination reason: Instruction limit
% 12.02/2.09 % (187063)Termination phase: Saturation
% 12.02/2.09 % (187063)Time elapsed: 0.047 s
% 12.02/2.09 % (187063)Peak memory usage: 13 MB
% 12.02/2.09 % (187063)Instructions burned: 107 (million)
% 12.02/2.09 % (187066)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=987125136:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/375Mi)
% 12.02/2.09 % (187065)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=3366061834:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2987 on theBenchmark for (2987ds/5755Mi)
% 12.02/2.09 % (187013)Instruction limit reached!
% 12.02/2.09 % (187013)------------------------------
% 12.02/2.09 % (187013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.02/2.09 % (187013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.09 % (187013)CaDiCaL version: 2.1.3
% 12.02/2.09 % (187013)Termination reason: Instruction limit
% 12.02/2.09 % (187013)Termination phase: Saturation
% 12.02/2.09 % (187013)Time elapsed: 0.707 s
% 12.02/2.09 % (187013)Peak memory usage: 18 MB
% 12.02/2.09 % (187013)Instructions burned: 854 (million)
% 12.02/2.09 % (187069)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2372440216:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2987 on theBenchmark for (2987ds/495Mi)
% 12.02/2.09 % (187045)Instruction limit reached!
% 12.02/2.09 % (187045)------------------------------
% 12.02/2.09 % (187045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.02/2.09 % (187045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.09 % (187045)CaDiCaL version: 2.1.3
% 12.02/2.09 % (187045)Termination reason: Instruction limit
% 12.02/2.09 % (187045)Termination phase: Saturation
% 12.02/2.09 % (187045)Time elapsed: 0.370 s
% 12.02/2.09 % (187045)Peak memory usage: 13 MB
% 12.02/2.09 % (187045)Instructions burned: 427 (million)
% 12.02/2.09 % (187071)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=2445133607:cond=on:i=34:hud=10:nm=10:rtra=on_2986 on theBenchmark for (2986ds/34Mi)
% 12.02/2.09 % (186991)Instruction limit reached!
% 12.02/2.09 % (186991)------------------------------
% 12.02/2.09 % (186991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.02/2.09 % (186991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.09 % (186991)CaDiCaL version: 2.1.3
% 12.02/2.09 % (186991)Termination reason: Instruction limit
% 12.02/2.09 % (186991)Termination phase: Saturation
% 12.02/2.09 % (186991)Time elapsed: 1.007 s
% 12.02/2.09 % (186991)Peak memory usage: 14 MB
% 12.56/2.23 % (186991)Instructions burned: 1240 (million)
% 12.56/2.23 % (187071)Instruction limit reached!
% 12.56/2.23 % (187071)------------------------------
% 12.56/2.23 % (187071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.23 % (187071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.23 % (187071)CaDiCaL version: 2.1.3
% 12.56/2.23 % (187071)Termination reason: Instruction limit
% 12.56/2.23 % (187071)Termination phase: Saturation
% 12.56/2.23 % (187071)Time elapsed: 0.031 s
% 12.56/2.23 % (187071)Peak memory usage: 12 MB
% 12.56/2.23 % (187071)Instructions burned: 35 (million)
% 12.56/2.23 % (187073)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1006155744:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2986 on theBenchmark for (2986ds/91Mi)
% 12.56/2.23 % (187074)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2843182052:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2986 on theBenchmark for (2986ds/66Mi)
% 12.56/2.23 % (187066)Instruction limit reached!
% 12.56/2.23 % (187066)------------------------------
% 12.56/2.23 % (187066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.23 % (187066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.23 % (187066)CaDiCaL version: 2.1.3
% 12.56/2.23 % (187066)Termination reason: Instruction limit
% 12.56/2.23 % (187066)Termination phase: Saturation
% 12.56/2.23 % (187066)Time elapsed: 0.177 s
% 12.56/2.23 % (187066)Peak memory usage: 13 MB
% 12.56/2.23 % (187066)Instructions burned: 376 (million)
% 12.56/2.23 % (187077)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3321029389:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2985 on theBenchmark for (2985ds/22Mi)
% 12.56/2.23 % (187048)Instruction limit reached!
% 12.56/2.23 % (187048)------------------------------
% 12.56/2.23 % (187048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.23 % (187048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.23 % (187048)CaDiCaL version: 2.1.3
% 12.56/2.23 % (187048)Termination reason: Instruction limit
% 12.56/2.23 % (187048)Termination phase: Saturation
% 12.56/2.23 % (187048)Time elapsed: 0.438 s
% 12.56/2.23 % (187048)Peak memory usage: 14 MB
% 12.56/2.23 % (187048)Instructions burned: 515 (million)
% 12.56/2.23 % (187077)Instruction limit reached!
% 12.56/2.23 % (187077)------------------------------
% 12.56/2.23 % (187077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.23 % (187077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.23 % (187077)CaDiCaL version: 2.1.3
% 12.56/2.23 % (187077)Termination reason: Instruction limit
% 12.56/2.23 % (187077)Termination phase: Saturation
% 12.56/2.23 % (187077)Time elapsed: 0.011 s
% 12.56/2.23 % (187077)Peak memory usage: 12 MB
% 12.56/2.23 % (187077)Instructions burned: 23 (million)
% 12.56/2.23 % (187074)Instruction limit reached!
% 12.56/2.23 % (187074)------------------------------
% 12.56/2.23 % (187074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.23 % (187074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.23 % (187074)CaDiCaL version: 2.1.3
% 12.56/2.23 % (187074)Termination reason: Instruction limit
% 12.56/2.23 % (187074)Termination phase: Saturation
% 12.56/2.23 % (187074)Time elapsed: 0.062 s
% 12.56/2.23 % (187074)Peak memory usage: 12 MB
% 12.56/2.23 % (187074)Instructions burned: 66 (million)
% 12.56/2.23 % (187080)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3783562653:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/28Mi)
% 12.56/2.23 % (187073)Instruction limit reached!
% 12.56/2.23 % (187073)------------------------------
% 12.56/2.23 % (187073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.23 % (187073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.23 % (187073)CaDiCaL version: 2.1.3
% 12.56/2.23 % (187073)Termination reason: Instruction limit
% 12.56/2.23 % (187073)Termination phase: Saturation
% 12.56/2.23 % (187073)Time elapsed: 0.082 s
% 12.56/2.23 % (187073)Peak memory usage: 12 MB
% 12.56/2.23 % (187073)Instructions burned: 91 (million)
% 12.56/2.23 % (187079)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=2311804963:i=338:bd=all:ins=4:rtra=on_2985 on theBenchmark for (2985ds/338Mi)
% 12.56/2.23 % (187080)Instruction limit reached!
% 12.56/2.23 % (187080)------------------------------
% 13.61/2.53 % (187080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.61/2.53 % (187080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/2.53 % (187080)CaDiCaL version: 2.1.3
% 13.61/2.53 % (187080)Termination reason: Instruction limit
% 13.61/2.53 % (187080)Termination phase: Saturation
% 13.61/2.53 % (187080)Time elapsed: 0.014 s
% 13.61/2.53 % (187080)Peak memory usage: 12 MB
% 13.61/2.53 % (187080)Instructions burned: 28 (million)
% 13.61/2.53 % (187081)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 13.61/2.53 % (187081)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=4061333816:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2985 on theBenchmark for (2985ds/137Mi)
% 13.61/2.53 % (187085)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=1194950839:i=227:sd=1:bd=all:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/227Mi)
% 13.61/2.53 % (187083)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=3876425818:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2985 on theBenchmark for (2985ds/340Mi)
% 13.61/2.54 % (187085)Instruction limit reached!
% 13.61/2.54 % (187085)------------------------------
% 13.61/2.54 % (187085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.61/2.54 % (187085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/2.54 % (187085)CaDiCaL version: 2.1.3
% 13.61/2.54 % (187085)Termination reason: Instruction limit
% 13.61/2.54 % (187085)Termination phase: Saturation
% 13.61/2.54 % (187085)Time elapsed: 0.102 s
% 13.61/2.54 % (187085)Peak memory usage: 13 MB
% 13.61/2.54 % (187085)Instructions burned: 228 (million)
% 13.61/2.54 % (187081)Instruction limit reached!
% 13.61/2.54 % (187081)------------------------------
% 13.61/2.54 % (187081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.61/2.54 % (187081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/2.54 % (187081)CaDiCaL version: 2.1.3
% 13.61/2.54 % (187081)Termination reason: Instruction limit
% 13.61/2.54 % (187081)Termination phase: Saturation
% 13.61/2.54 % (187081)Time elapsed: 0.122 s
% 13.61/2.54 % (187081)Peak memory usage: 13 MB
% 13.61/2.54 % (187081)Instructions burned: 137 (million)
% 13.61/2.54 % (187089)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 13.61/2.54 % (187089)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2501766638:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/373Mi)
% 13.61/2.54 % (187090)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=869245932:i=116:ep=RSTC:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/116Mi)
% 13.61/2.54 % (187090)Refutation not found, incomplete strategy
% 13.61/2.54 % (187090)------------------------------
% 13.61/2.54 % (187090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.61/2.54 % (187090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/2.54 % (187090)CaDiCaL version: 2.1.3
% 13.61/2.54 % (187090)Termination reason: Refutation not found, incomplete strategy
% 13.61/2.54 % (187090)Time elapsed: 0.014 s
% 13.61/2.54 % (187090)Peak memory usage: 12 MB
% 13.61/2.54 % (187090)Instructions burned: 14 (million)
% 13.61/2.54 % (187090)------------------------------
% 13.61/2.54 % (187090)------------------------------
% 13.61/2.54 % (187093)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=2050175139:i=575:rtra=on_2983 on theBenchmark for (2983ds/575Mi)
% 13.61/2.54 % (187069)Instruction limit reached!
% 13.61/2.54 % (187069)------------------------------
% 13.61/2.54 % (187069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.61/2.54 % (187069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/2.54 % (187069)CaDiCaL version: 2.1.3
% 13.61/2.54 % (187069)Termination reason: Instruction limit
% 13.61/2.54 % (187069)Termination phase: Saturation
% 13.61/2.54 % (187069)Time elapsed: 0.408 s
% 13.61/2.54 % (187069)Peak memory usage: 14 MB
% 13.61/2.54 % (187069)Instructions burned: 496 (million)
% 13.61/2.54 % (187047)Instruction limit reached!
% 13.61/2.54 % (187047)------------------------------
% 13.61/2.54 % (187047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.17/3.10 % (187047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.10 % (187047)CaDiCaL version: 2.1.3
% 19.17/3.10 % (187047)Termination reason: Instruction limit
% 19.17/3.10 % (187047)Termination phase: Saturation
% 19.17/3.10 % (187047)Time elapsed: 0.722 s
% 19.17/3.10 % (187047)Peak memory usage: 14 MB
% 19.17/3.10 % (187047)Instructions burned: 875 (million)
% 19.17/3.10 % (187095)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2825415458:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2982 on theBenchmark for (2982ds/270Mi)
% 19.17/3.10 % (187096)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=2481592016: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_2982 on theBenchmark for (2982ds/9840Mi)
% 19.17/3.10 % (187079)Instruction limit reached!
% 19.17/3.10 % (187079)------------------------------
% 19.17/3.10 % (187079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.17/3.10 % (187079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.10 % (187079)CaDiCaL version: 2.1.3
% 19.17/3.10 % (187079)Termination reason: Instruction limit
% 19.17/3.10 % (187079)Termination phase: Saturation
% 19.17/3.10 % (187079)Time elapsed: 0.297 s
% 19.17/3.10 % (187079)Peak memory usage: 14 MB
% 19.17/3.10 % (187079)Instructions burned: 339 (million)
% 19.17/3.10 % (187089)Instruction limit reached!
% 19.17/3.10 % (187089)------------------------------
% 19.17/3.10 % (187089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.17/3.10 % (187089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.10 % (187089)CaDiCaL version: 2.1.3
% 19.17/3.10 % (187089)Termination reason: Instruction limit
% 19.17/3.10 % (187089)Termination phase: Saturation
% 19.17/3.10 % (187089)Time elapsed: 0.158 s
% 19.17/3.10 % (187089)Peak memory usage: 14 MB
% 19.17/3.10 % (187089)Instructions burned: 375 (million)
% 19.17/3.10 % (187083)Instruction limit reached!
% 19.17/3.10 % (187083)------------------------------
% 19.17/3.10 % (187083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.17/3.10 % (187083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.10 % (187083)CaDiCaL version: 2.1.3
% 19.17/3.10 % (187083)Termination reason: Instruction limit
% 19.17/3.10 % (187083)Termination phase: Saturation
% 19.17/3.10 % (187083)Time elapsed: 0.282 s
% 19.17/3.10 % (187083)Peak memory usage: 13 MB
% 19.17/3.10 % (187083)Instructions burned: 340 (million)
% 19.17/3.10 % (187100)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
% 19.17/3.10 % (187100)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=1070596942:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/270Mi)
% 19.17/3.10 % (187099)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=326030291:i=421:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/421Mi)
% 19.17/3.10 % (187101)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=74173901:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/31Mi)
% 19.17/3.10 % (187101)Refutation not found, incomplete strategy
% 19.17/3.10 % (187101)------------------------------
% 19.17/3.10 % (187101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.17/3.10 % (187101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.10 % (187101)CaDiCaL version: 2.1.3
% 19.17/3.10 % (187101)Termination reason: Refutation not found, incomplete strategy
% 19.17/3.10 % (187101)Time elapsed: 0.025 s
% 19.17/3.10 % (187101)Peak memory usage: 12 MB
% 19.17/3.10 % (187101)Instructions burned: 27 (million)
% 19.17/3.10 % (187101)------------------------------
% 19.17/3.10 % (187101)------------------------------
% 19.17/3.10 % (187105)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 19.17/3.10 % (187105)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
% 19.92/3.29 % (187105)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=4112643923:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2981 on theBenchmark for (2981ds/1440Mi)
% 19.92/3.29 % (187100)Instruction limit reached!
% 19.92/3.29 % (187100)------------------------------
% 19.92/3.29 % (187100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187100)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187100)Termination reason: Instruction limit
% 19.92/3.29 % (187100)Termination phase: Saturation
% 19.92/3.29 % (187100)Time elapsed: 0.126 s
% 19.92/3.29 % (187100)Peak memory usage: 13 MB
% 19.92/3.29 % (187100)Instructions burned: 271 (million)
% 19.92/3.29 % (187107)dis+10_2_sil=128000:si=on:random_seed=1495503885:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2980 on theBenchmark for (2980ds/339Mi)
% 19.92/3.29 % (187095)Instruction limit reached!
% 19.92/3.29 % (187095)------------------------------
% 19.92/3.29 % (187095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187095)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187095)Termination reason: Instruction limit
% 19.92/3.29 % (187095)Termination phase: Saturation
% 19.92/3.29 % (187095)Time elapsed: 0.211 s
% 19.92/3.29 % (187095)Peak memory usage: 13 MB
% 19.92/3.29 % (187095)Instructions burned: 270 (million)
% 19.92/3.29 % (187109)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2357200453:i=111:add=on:fgj=on:rtra=on:fdi=1024_2980 on theBenchmark for (2980ds/111Mi)
% 19.92/3.29 % (187109)Instruction limit reached!
% 19.92/3.29 % (187109)------------------------------
% 19.92/3.29 % (187109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187109)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187109)Termination reason: Instruction limit
% 19.92/3.29 % (187109)Termination phase: Saturation
% 19.92/3.29 % (187109)Time elapsed: 0.096 s
% 19.92/3.29 % (187109)Peak memory usage: 12 MB
% 19.92/3.29 % (187109)Instructions burned: 111 (million)
% 19.92/3.29 % (187107)Instruction limit reached!
% 19.92/3.29 % (187107)------------------------------
% 19.92/3.29 % (187107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187107)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187107)Termination reason: Instruction limit
% 19.92/3.29 % (187107)Termination phase: Saturation
% 19.92/3.29 % (187107)Time elapsed: 0.148 s
% 19.92/3.29 % (187107)Peak memory usage: 12 MB
% 19.92/3.29 % (187107)Instructions burned: 339 (million)
% 19.92/3.29 % (187112)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=896056394:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2979 on theBenchmark for (2979ds/136Mi)
% 19.92/3.29 % (187111)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=2819947261:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2979 on theBenchmark for (2979ds/122Mi)
% 19.92/3.29 % (187099)Instruction limit reached!
% 19.92/3.29 % (187099)------------------------------
% 19.92/3.29 % (187099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187099)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187099)Termination reason: Instruction limit
% 19.92/3.29 % (187099)Termination phase: Saturation
% 19.92/3.29 % (187099)Time elapsed: 0.361 s
% 19.92/3.29 % (187099)Peak memory usage: 13 MB
% 19.92/3.29 % (187099)Instructions burned: 421 (million)
% 19.92/3.29 % (187112)Instruction limit reached!
% 19.92/3.29 % (187112)------------------------------
% 19.92/3.29 % (187112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187112)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187112)Termination reason: Instruction limit
% 19.92/3.29 % (187112)Termination phase: Saturation
% 19.92/3.29 % (187112)Time elapsed: 0.066 s
% 19.92/3.29 % (187112)Peak memory usage: 12 MB
% 19.92/3.29 % (187112)Instructions burned: 137 (million)
% 19.92/3.29 % (187116)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=2251869075:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2978 on theBenchmark for (2978ds/1254Mi)
% 19.92/3.29 % (187093)Instruction limit reached!
% 19.92/3.29 % (187093)------------------------------
% 19.92/3.29 % (187093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187093)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187093)Termination reason: Instruction limit
% 19.92/3.29 % (187093)Termination phase: Saturation
% 19.92/3.29 % (187093)Time elapsed: 0.496 s
% 19.92/3.29 % (187093)Peak memory usage: 14 MB
% 19.92/3.29 % (187093)Instructions burned: 576 (million)
% 19.92/3.29 % (187115)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3531382876:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2978 on theBenchmark for (2978ds/232Mi)
% 19.92/3.29 % (187115)Refutation not found, incomplete strategy
% 19.92/3.29 % (187115)------------------------------
% 19.92/3.29 % (187115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187115)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187115)Termination reason: Refutation not found, incomplete strategy
% 19.92/3.29 % (187115)Time elapsed: 0.008 s
% 19.92/3.29 % (187115)Peak memory usage: 12 MB
% 19.92/3.29 % (187115)Instructions burned: 7 (million)
% 19.92/3.29 % (187115)------------------------------
% 19.92/3.29 % (187115)------------------------------
% 19.92/3.29 % (187111)Instruction limit reached!
% 19.92/3.29 % (187111)------------------------------
% 19.92/3.29 % (187111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187111)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187111)Termination reason: Instruction limit
% 19.92/3.29 % (187111)Termination phase: Saturation
% 19.92/3.29 % (187111)Time elapsed: 0.110 s
% 19.92/3.29 % (187111)Peak memory usage: 12 MB
% 19.92/3.29 % (187111)Instructions burned: 123 (million)
% 19.92/3.29 % (187119)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 19.92/3.29 % (187119)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=991124353:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2977 on theBenchmark for (2977ds/281Mi)
% 19.92/3.29 % (187120)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1694330338:i=619:add=on:rtra=on_2977 on theBenchmark for (2977ds/619Mi)
% 19.92/3.29 % (187121)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=3705494687:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2977 on theBenchmark for (2977ds/865Mi)
% 19.92/3.29 % (187119)Instruction limit reached!
% 19.92/3.29 % (187119)------------------------------
% 19.92/3.29 % (187119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187119)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187119)Termination reason: Instruction limit
% 19.92/3.29 % (187119)Termination phase: Saturation
% 19.92/3.29 % (187119)Time elapsed: 0.253 s
% 19.92/3.29 % (187119)Peak memory usage: 13 MB
% 19.92/3.29 % (187119)Instructions burned: 281 (million)
% 19.92/3.29 % (187125)lrs+10_1_sil=128000:si=on:urr=on:random_seed=4163776408:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/212Mi)
% 19.92/3.29 % (187125)Instruction limit reached!
% 19.92/3.29 % (187125)------------------------------
% 19.92/3.29 % (187125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187125)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187125)Termination reason: Instruction limit
% 19.92/3.29 % (187125)Termination phase: Saturation
% 19.92/3.29 % (187125)Time elapsed: 0.184 s
% 19.92/3.29 % (187125)Peak memory usage: 13 MB
% 19.92/3.29 % (187125)Instructions burned: 213 (million)
% 19.92/3.29 % (187116)Instruction limit reached!
% 19.92/3.29 % (187116)------------------------------
% 19.92/3.29 % (187116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187116)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187116)Termination reason: Instruction limit
% 19.92/3.29 % (187116)Termination phase: Saturation
% 19.92/3.29 % (187116)Time elapsed: 0.544 s
% 19.92/3.29 % (187116)Peak memory usage: 15 MB
% 19.92/3.29 % (187116)Instructions burned: 1254 (million)
% 19.92/3.29 % (187127)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=300571352:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/130Mi)
% 19.92/3.29 % (187128)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=984345721:st=1.5:i=346:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/346Mi)
% 19.92/3.29 % (187120)Instruction limit reached!
% 19.92/3.29 % (187120)------------------------------
% 19.92/3.29 % (187120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187120)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187120)Termination reason: Instruction limit
% 19.92/3.29 % (187120)Termination phase: Saturation
% 19.92/3.29 % (187120)Time elapsed: 0.516 s
% 19.92/3.29 % (187120)Peak memory usage: 14 MB
% 19.92/3.29 % (187120)Instructions burned: 619 (million)
% 19.92/3.29 % (187131)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=912048671:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2972 on theBenchmark for (2972ds/152Mi)
% 19.92/3.29 % (187127)Instruction limit reached!
% 19.92/3.29 % (187127)------------------------------
% 19.92/3.29 % (187127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187127)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187127)Termination reason: Instruction limit
% 19.92/3.29 % (187127)Termination phase: Saturation
% 19.92/3.29 % (187127)Time elapsed: 0.133 s
% 19.92/3.29 % (187127)Peak memory usage: 12 MB
% 19.92/3.29 % (187127)Instructions burned: 130 (million)
% 19.92/3.29 % (187128)Instruction limit reached!
% 19.92/3.29 % (187128)------------------------------
% 19.92/3.29 % (187128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.29 % (187128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.29 % (187128)CaDiCaL version: 2.1.3
% 19.92/3.29 % (187128)Termination reason: Instruction limit
% 19.92/3.29 % (187128)Termination phase: Saturation
% 19.92/3.29 % (187128)Time elapsed: 0.152 s
% 19.92/3.29 % (187128)Peak memory usage: 13 MB
% 19.92/3.29 % (187128)Instructions burned: 347 (million)
% 19.92/3.29 % (187133)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=523209859:i=75:ep=R:rtra=on:ntd=on_2971 on theBenchmark for (2971ds/75Mi)
% 19.92/3.29 % (187131) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-186926-187131"...
% 19.92/3.29 % (187134)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=1936424931:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/387Mi)
% 19.92/3.29 % (187131)...printing done.
% 19.92/3.29 % (187131)Refutation found. Thanks to Tanya!
% 19.92/3.29 % SZS status Theorem for theBenchmark
% 19.92/3.29 % SZS output start Proof for theBenchmark
% 19.92/3.29 thf(type_def_5, type, a: $tType).
% 19.92/3.29 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 19.92/3.29 thf(func_def_0, type, cR: (a > a)).
% 19.92/3.29 thf(func_def_1, type, cP: (a > a > a)).
% 19.92/3.29 thf(func_def_2, type, cL: (a > a)).
% 19.92/3.29 thf(func_def_3, type, cZ: a).
% 19.92/3.29 thf(func_def_7, type, sK0: a).
% 19.92/3.29 thf(func_def_8, type, sK1: ((a > $o) > a)).
% 19.92/3.29 thf(func_def_9, type, sK2: ((a > $o) > a)).
% 19.92/3.29 thf(func_def_10, type, sK3: ((a > $o) > a)).
% 19.92/3.29 thf(func_def_11, type, sK4: ((a > $o) > a)).
% 19.92/3.29 thf(func_def_12, type, sP5: ($o > $o)).
% 19.92/3.29 thf(func_def_13, type, sP6: ($o > $o)).
% 19.92/3.29 thf(func_def_14, type, sP7: ($o > $o)).
% 19.92/3.29 thf(func_def_15, type, sP8: ($o > $o)).
% 19.92/3.29 thf(func_def_16, type, sP9: (a > $o)).
% 19.92/3.29 thf(func_def_17, type, sP10: ($o > $o)).
% 19.92/3.29 thf(func_def_18, type, sP11: ($o > $o)).
% 19.92/3.29 thf(func_def_19, type, sP12: ($o > $o)).
% 19.92/3.29 thf(func_def_20, type, sP13: ($o > $o)).
% 19.92/3.29 thf(func_def_21, type, sP14: ($o > $o)).
% 19.92/3.29 thf(func_def_22, type, sP15: ($o > $o)).
% 19.92/3.29 thf(func_def_23, type, sP16: ($o > $o)).
% 19.92/3.29 thf(func_def_24, type, sP17: (a > $o)).
% 19.92/3.29 thf(func_def_25, type, sP18: (a > $o)).
% 19.92/3.29 thf(func_def_26, type, sP19: ($o > $o)).
% 19.92/3.29 thf(func_def_27, type, sP20: ($o > $o)).
% 19.92/3.29 thf(func_def_28, type, sP21: ($o > $o)).
% 19.92/3.29 thf(func_def_29, type, sP22: ($o > $o)).
% 19.92/3.29 thf(func_def_30, type, sP23: (a > $o)).
% 19.92/3.29 thf(func_def_31, type, vNOT: ($o > $o)).
% 19.92/3.29 thf(func_def_32, type, db0: !>[X0: $tType]:(X0)).
% 19.92/3.29 thf(func_def_33, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 19.92/3.29 thf(func_def_35, type, db1: !>[X0: $tType]:(X0)).
% 19.92/3.29 thf(func_def_36, type, sK25: ((a > $o) > a)).
% 19.92/3.29 thf(func_def_37, type, db2: !>[X0: $tType]:(X0)).
% 19.92/3.29 thf(f1,conjecture,(
% 19.92/3.29 ((((cL @ cZ)) = cZ) & ! [X1 : a,X0 : a] : (((cR @ (cP @ X0 @ X1))) = X1) & ! [X1 : a,X0 : a] : (((cL @ (cP @ X0 @ X1))) = X0) & ! [X2 : a] : ((X2 = ((cP @ (cL @ X2) @ (cR @ X2)))) <=> (X2 != cZ)) & (((cR @ cZ)) = cZ) & ! [X3 : (a > $o)] : (! [X4 : a,X2 : a] : ((X3 @ (cP @ X2 @ X4)) => (((X2 = cZ) <=> (X4 = cZ)) & (X3 @ (cP @ (cL @ X2) @ (cL @ X4))) & (X3 @ (cP @ (cR @ X2) @ (cR @ X4))))) => ! [X4 : a,X2 : a] : ((X3 @ (cP @ X2 @ X4)) => (X2 = X4)))) => ! [X2 : a] : ? [X3 : (a > $o)] : (! [X5 : a,X4 : a] : ((X3 @ (cP @ X5 @ X4)) => (((X4 = cZ) => (X5 = cZ)) & (X3 @ (cP @ (cR @ X5) @ (cR @ X4))) & (X3 @ (cP @ (cL @ X5) @ (cL @ X4))))) & (X3 @ (cP @ cZ @ X2)))),
% 19.92/3.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cPU_LEM2E_pme)).
% 19.92/3.29 thf(f2,negated_conjecture,(
% 19.92/3.29 ~(((((cL @ cZ)) = cZ) & ! [X1 : a,X0 : a] : (((cR @ (cP @ X0 @ X1))) = X1) & ! [X1 : a,X0 : a] : (((cL @ (cP @ X0 @ X1))) = X0) & ! [X2 : a] : ((X2 = ((cP @ (cL @ X2) @ (cR @ X2)))) <=> (X2 != cZ)) & (((cR @ cZ)) = cZ) & ! [X3 : (a > $o)] : (! [X4 : a,X2 : a] : ((X3 @ (cP @ X2 @ X4)) => (((X2 = cZ) <=> (X4 = cZ)) & (X3 @ (cP @ (cL @ X2) @ (cL @ X4))) & (X3 @ (cP @ (cR @ X2) @ (cR @ X4))))) => ! [X4 : a,X2 : a] : ((X3 @ (cP @ X2 @ X4)) => (X2 = X4)))) => ! [X2 : a] : ? [X3 : (a > $o)] : (! [X5 : a,X4 : a] : ((X3 @ (cP @ X5 @ X4)) => (((X4 = cZ) => (X5 = cZ)) & (X3 @ (cP @ (cR @ X5) @ (cR @ X4))) & (X3 @ (cP @ (cL @ X5) @ (cL @ X4))))) & (X3 @ (cP @ cZ @ X2))))),
% 19.92/3.29 inference(negated_conjecture,[status(cth)],[f1])).
% 19.92/3.29 thf(f3,plain,(
% 19.92/3.29 ~(((((cL @ cZ)) = cZ) & ! [X0 : a,X1 : a] : (((cR @ (cP @ X1 @ X0))) = X0) & ! [X2 : a,X3 : a] : (((cL @ (cP @ X3 @ X2))) = X3) & ! [X4 : a] : ((((cP @ (cL @ X4) @ (cR @ X4))) = X4) <=> (cZ != X4)) & (((cR @ cZ)) = cZ) & ! [X5 : (a > $o)] : (! [X6 : a,X7 : a] : ((X5 @ (cP @ X7 @ X6)) => (((cZ = X7) <=> (cZ = X6)) & (X5 @ (cP @ (cL @ X7) @ (cL @ X6))) & (X5 @ (cP @ (cR @ X7) @ (cR @ X6))))) => ! [X8 : a,X9 : a] : ((X5 @ (cP @ X9 @ X8)) => (X8 = X9)))) => ! [X10 : a] : ? [X11 : (a > $o)] : (! [X12 : a,X13 : a] : ((X11 @ (cP @ X12 @ X13)) => (((cZ = X13) => (cZ = X12)) & (X11 @ (cP @ (cR @ X12) @ (cR @ X13))) & (X11 @ (cP @ (cL @ X12) @ (cL @ X13))))) & (X11 @ (cP @ cZ @ X10))))),
% 19.92/3.29 inference(rectify,[],[f2])).
% 19.92/3.29 thf(f4,plain,(
% 19.92/3.29 ~((! [X0 : a,X1 : a] : (((cR @ (cP @ X1 @ X0))) = X0) & ! [X4 : a] : ((cZ != X4) <=> (((cP @ (cL @ X4) @ (cR @ X4))) = X4)) & ! [X5 : (a > $o)] : (! [X6 : a,X7 : a] : ((((X5 @ (cP @ X7 @ X6))) = $true) => ((((X5 @ (cP @ (cR @ X7) @ (cR @ X6)))) = $true) & ((cZ = X6) <=> (cZ = X7)) & (((X5 @ (cP @ (cL @ X7) @ (cL @ X6)))) = $true))) => ! [X8 : a,X9 : a] : (($true = ((X5 @ (cP @ X9 @ X8)))) => (X8 = X9))) & (cZ = ((cL @ cZ))) & ! [X3 : a,X2 : a] : (((cL @ (cP @ X3 @ X2))) = X3) & (cZ = ((cR @ cZ)))) => ! [X10 : a] : ? [X11 : (a > $o)] : (! [X12 : a,X13 : a] : (($true = ((X11 @ (cP @ X12 @ X13)))) => (($true = ((X11 @ (cP @ (cR @ X12) @ (cR @ X13))))) & ((cZ = X13) => (cZ = X12)) & (((X11 @ (cP @ (cL @ X12) @ (cL @ X13)))) = $true))) & ($true = ((X11 @ (cP @ cZ @ X10))))))),
% 19.92/3.29 inference(fool_elimination,[],[f3])).
% 19.92/3.29 thf(f5,plain,(
% 19.92/3.29 ? [X10 : a] : ! [X11 : (a > $o)] : (? [X12 : a,X13 : a] : (($true = ((X11 @ (cP @ X12 @ X13)))) & (($true != ((X11 @ (cP @ (cR @ X12) @ (cR @ X13))))) | (((X11 @ (cP @ (cL @ X12) @ (cL @ X13)))) != $true) | ((cZ != X12) & (cZ = X13)))) | ($true != ((X11 @ (cP @ cZ @ X10))))) & (! [X0 : a,X1 : a] : (((cR @ (cP @ X1 @ X0))) = X0) & ! [X4 : a] : ((cZ != X4) <=> (((cP @ (cL @ X4) @ (cR @ X4))) = X4)) & ! [X5 : (a > $o)] : (! [X8 : a,X9 : a] : (($true != ((X5 @ (cP @ X9 @ X8)))) | (X8 = X9)) | ? [X7 : a,X6 : a] : (((((X5 @ (cP @ (cR @ X7) @ (cR @ X6)))) != $true) | (((X5 @ (cP @ (cL @ X7) @ (cL @ X6)))) != $true) | ((cZ = X6) <~> (cZ = X7))) & (((X5 @ (cP @ X7 @ X6))) = $true))) & (cZ = ((cL @ cZ))) & ! [X3 : a,X2 : a] : (((cL @ (cP @ X3 @ X2))) = X3) & (cZ = ((cR @ cZ))))),
% 19.92/3.29 inference(ennf_transformation,[],[f4])).
% 19.92/3.29 thf(f6,plain,(
% 19.92/3.29 (cZ = ((cL @ cZ))) & ! [X0 : a,X1 : a] : (((cR @ (cP @ X1 @ X0))) = X0) & ! [X3 : a,X2 : a] : (((cL @ (cP @ X3 @ X2))) = X3) & ? [X10 : a] : ! [X11 : (a > $o)] : (? [X12 : a,X13 : a] : (($true = ((X11 @ (cP @ X12 @ X13)))) & (($true != ((X11 @ (cP @ (cR @ X12) @ (cR @ X13))))) | (((X11 @ (cP @ (cL @ X12) @ (cL @ X13)))) != $true) | ((cZ != X12) & (cZ = X13)))) | ($true != ((X11 @ (cP @ cZ @ X10))))) & ! [X5 : (a > $o)] : (! [X8 : a,X9 : a] : (($true != ((X5 @ (cP @ X9 @ X8)))) | (X8 = X9)) | ? [X7 : a,X6 : a] : (((((X5 @ (cP @ (cR @ X7) @ (cR @ X6)))) != $true) | (((X5 @ (cP @ (cL @ X7) @ (cL @ X6)))) != $true) | ((cZ = X6) <~> (cZ = X7))) & (((X5 @ (cP @ X7 @ X6))) = $true))) & (cZ = ((cR @ cZ))) & ! [X4 : a] : ((cZ != X4) <=> (((cP @ (cL @ X4) @ (cR @ X4))) = X4))),
% 19.92/3.29 inference(flattening,[],[f5])).
% 19.92/3.29 thf(f7,plain,(
% 19.92/3.29 (cZ = ((cL @ cZ))) & ! [X0 : a,X1 : a] : (((cR @ (cP @ X1 @ X0))) = X0) & ! [X3 : a,X2 : a] : (((cL @ (cP @ X3 @ X2))) = X3) & ? [X10 : a] : ! [X11 : (a > $o)] : (? [X12 : a,X13 : a] : (($true = ((X11 @ (cP @ X12 @ X13)))) & (($true != ((X11 @ (cP @ (cR @ X12) @ (cR @ X13))))) | (((X11 @ (cP @ (cL @ X12) @ (cL @ X13)))) != $true) | ((cZ != X12) & (cZ = X13)))) | ($true != ((X11 @ (cP @ cZ @ X10))))) & ! [X5 : (a > $o)] : (! [X8 : a,X9 : a] : (($true != ((X5 @ (cP @ X9 @ X8)))) | (X8 = X9)) | ? [X7 : a,X6 : a] : (((((X5 @ (cP @ (cR @ X7) @ (cR @ X6)))) != $true) | (((X5 @ (cP @ (cL @ X7) @ (cL @ X6)))) != $true) | (((cZ != X7) | (cZ != X6)) & ((cZ = X7) | (cZ = X6)))) & (((X5 @ (cP @ X7 @ X6))) = $true))) & (cZ = ((cR @ cZ))) & ! [X4 : a] : (((cZ != X4) | (((cP @ (cL @ X4) @ (cR @ X4))) != X4)) & ((((cP @ (cL @ X4) @ (cR @ X4))) = X4) | (cZ = X4)))),
% 19.92/3.29 inference(nnf_transformation,[],[f6])).
% 19.92/3.29 thf(f8,plain,(
% 19.92/3.29 (cZ = ((cL @ cZ))) & ! [X0 : a,X1 : a] : (((cR @ (cP @ X1 @ X0))) = X0) & ! [X2 : a,X3 : a] : (((cL @ (cP @ X2 @ X3))) = X2) & ? [X4 : a] : ! [X5 : (a > $o)] : (? [X6 : a,X7 : a] : ((((X5 @ (cP @ X6 @ X7))) = $true) & (($true != ((X5 @ (cP @ (cR @ X6) @ (cR @ X7))))) | ($true != ((X5 @ (cP @ (cL @ X6) @ (cL @ X7))))) | ((cZ != X6) & (cZ = X7)))) | ($true != ((X5 @ (cP @ cZ @ X4))))) & ! [X8 : (a > $o)] : (! [X9 : a,X10 : a] : ((((X8 @ (cP @ X10 @ X9))) != $true) | (X9 = X10)) | ? [X11 : a,X12 : a] : ((($true != ((X8 @ (cP @ (cR @ X11) @ (cR @ X12))))) | ($true != ((X8 @ (cP @ (cL @ X11) @ (cL @ X12))))) | (((cZ != X11) | (cZ != X12)) & ((cZ = X11) | (cZ = X12)))) & ($true = ((X8 @ (cP @ X11 @ X12)))))) & (cZ = ((cR @ cZ))) & ! [X13 : a] : (((cZ != X13) | (((cP @ (cL @ X13) @ (cR @ X13))) != X13)) & ((((cP @ (cL @ X13) @ (cR @ X13))) = X13) | (cZ = X13)))),
% 19.92/3.29 inference(rectify,[],[f7])).
% 19.92/3.29 thf(f9,plain,(
% 19.92/3.29 (cZ = ((cL @ cZ))) & ! [X0 : a,X1 : a] : (((cR @ (cP @ X1 @ X0))) = X0) & ! [X2 : a,X3 : a] : (((cL @ (cP @ X2 @ X3))) = X2) & ! [X5 : (a > $o)] : (((((X5 @ (cP @ (sK1 @ X5) @ (sK2 @ X5)))) = $true) & ((((X5 @ (cP @ (cR @ (sK1 @ X5)) @ (cR @ (sK2 @ X5))))) != $true) | ($true != ((X5 @ (cP @ (cL @ (sK1 @ X5)) @ (cL @ (sK2 @ X5)))))) | ((cZ != ((sK1 @ X5))) & (cZ = ((sK2 @ X5)))))) | ($true != ((X5 @ (cP @ cZ @ sK0))))) & ! [X8 : (a > $o)] : (! [X9 : a,X10 : a] : ((((X8 @ (cP @ X10 @ X9))) != $true) | (X9 = X10)) | ((($true != ((X8 @ (cP @ (cR @ (sK3 @ X8)) @ (cR @ (sK4 @ X8)))))) | ($true != ((X8 @ (cP @ (cL @ (sK3 @ X8)) @ (cL @ (sK4 @ X8)))))) | (((cZ != ((sK3 @ X8))) | (cZ != ((sK4 @ X8)))) & ((cZ = ((sK3 @ X8))) | (cZ = ((sK4 @ X8)))))) & (((X8 @ (cP @ (sK3 @ X8) @ (sK4 @ X8)))) = $true))) & (cZ = ((cR @ cZ))) & ! [X13 : a] : (((cZ != X13) | (((cP @ (cL @ X13) @ (cR @ X13))) != X13)) & ((((cP @ (cL @ X13) @ (cR @ X13))) = X13) | (cZ = X13)))),
% 19.92/3.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,vAPP,vAPP,vAPP,vAPP]),skolemize(X4,sK0),skolemize(X12,sK4 @ X8),skolemize(X12,sK4 @ X8),skolemize(X12,sK4 @ X8),skolemize(X12,sK4 @ X8)],[f8])).
% 19.92/3.29 thf(f10,plain,(
% 19.92/3.29 ( ! [X13 : a] : ((((cP @ (cL @ X13) @ (cR @ X13))) = X13) | (cZ = X13)) )),
% 19.92/3.29 inference(cnf_transformation,[],[f9])).
% 19.92/3.29 thf(f11,plain,(
% 19.92/3.29 ( ! [X13 : a] : ((cZ != X13) | (((cP @ (cL @ X13) @ (cR @ X13))) != X13)) )),
% 19.92/3.29 inference(cnf_transformation,[],[f9])).
% 19.92/3.29 thf(f12,plain,(
% 19.92/3.29 (cZ = ((cR @ cZ)))),
% 19.92/3.29 inference(cnf_transformation,[],[f9])).
% 19.92/3.29 thf(f17,plain,(
% 19.92/3.29 ( ! [X5 : (a > $o)] : ((((X5 @ (cP @ (cR @ (sK1 @ X5)) @ (cR @ (sK2 @ X5))))) != $true) | ($true != ((X5 @ (cP @ (cL @ (sK1 @ X5)) @ (cL @ (sK2 @ X5)))))) | (cZ != ((sK1 @ X5))) | ($true != ((X5 @ (cP @ cZ @ sK0))))) )),
% 19.92/3.29 inference(cnf_transformation,[],[f9])).
% 19.92/3.29 thf(f18,plain,(
% 19.92/3.29 ( ! [X5 : (a > $o)] : ((((X5 @ (cP @ (sK1 @ X5) @ (sK2 @ X5)))) = $true) | ($true != ((X5 @ (cP @ cZ @ sK0))))) )),
% 19.92/3.29 inference(cnf_transformation,[],[f9])).
% 19.92/3.29 thf(f19,plain,(
% 19.92/3.29 ( ! [X2 : a,X3 : a] : ((((cL @ (cP @ X2 @ X3))) = X2)) )),
% 19.92/3.29 inference(cnf_transformation,[],[f9])).
% 19.92/3.29 thf(f21,plain,(
% 19.92/3.29 (cZ = ((cL @ cZ)))),
% 19.92/3.29 inference(cnf_transformation,[],[f9])).
% 19.92/3.29 thf(f26,definition,(
% 19.92/3.29 (((sP6 @ $true)) = $false)),
% 19.92/3.29 introduced(definition,[new_symbols(definition,[sP6])],[inequality_splitting_name_introduction])).
% 19.92/3.29 thf(f27,plain,(
% 19.92/3.29 ( ! [X5 : (a > $o)] : ((((X5 @ (cP @ (sK1 @ X5) @ (sK2 @ X5)))) = $true) | ($true = ((sP6 @ (X5 @ (cP @ cZ @ sK0)))))) )),
% 19.92/3.29 inference(inequality_splitting,[],[f18,f26])).
% 19.92/3.29 thf(f28,definition,(
% 19.92/3.29 (((sP7 @ $true)) = $false)),
% 19.92/3.29 introduced(definition,[new_symbols(definition,[sP7])],[inequality_splitting_name_introduction])).
% 19.92/3.29 thf(f29,definition,(
% 19.92/3.29 ($false = ((sP8 @ $true)))),
% 19.92/3.29 introduced(definition,[new_symbols(definition,[sP8])],[inequality_splitting_name_introduction])).
% 19.92/3.29 thf(f30,definition,(
% 19.92/3.29 (((sP9 @ cZ)) = $false)),
% 19.92/3.29 introduced(definition,[new_symbols(definition,[sP9])],[inequality_splitting_name_introduction])).
% 19.92/3.29 thf(f31,definition,(
% 19.92/3.29 (((sP10 @ $true)) = $false)),
% 19.92/3.29 introduced(definition,[new_symbols(definition,[sP10])],[inequality_splitting_name_introduction])).
% 19.92/3.29 thf(f32,plain,(
% 19.92/3.29 ( ! [X5 : (a > $o)] : (($true = ((sP7 @ (X5 @ (cP @ (cR @ (sK1 @ X5)) @ (cR @ (sK2 @ X5))))))) | ($true = ((sP10 @ (X5 @ (cP @ cZ @ sK0))))) | ($true = ((sP9 @ (sK1 @ X5)))) | (((sP8 @ (X5 @ (cP @ (cL @ (sK1 @ X5)) @ (cL @ (sK2 @ X5)))))) = $true)) )),
% 19.92/3.29 inference(inequality_splitting,[],[f17,f31,f30,f29,f28])).
% 19.92/3.29 thf(f49,definition,(
% 19.92/3.29 ($false = ((sP23 @ cZ)))),
% 19.92/3.29 introduced(definition,[new_symbols(definition,[sP23])],[inequality_splitting_name_introduction])).
% 19.92/3.29 thf(f50,plain,(
% 19.92/3.29 ( ! [X13 : a] : ((((cP @ (cL @ X13) @ (cR @ X13))) != X13) | ($true = ((sP23 @ X13)))) )),
% 19.92/3.29 inference(inequality_splitting,[],[f11,f49])).
% 19.92/3.29 thf(f57,plain,(
% 19.92/3.29 ( ! [X0 : a] : (($true = ((sP23 @ X0))) | (X0 != X0) | (cZ = X0)) )),
% 19.92/3.29 inference(constrained_superposition,[],[f50,f10])).
% 19.92/3.29 thf(f58,plain,(
% 19.92/3.29 ( ! [X0 : a] : (($true = ((sP23 @ X0))) | (cZ = X0)) )),
% 19.92/3.29 inference(trivial_inequality_removal,[],[f57])).
% 19.92/3.29 thf(f71,plain,(
% 19.92/3.29 ( ! [X6 : (a > $o)] : (($true = ((sP6 @ ((^[Y0 : a]: (~ (X6 @ Y0))) @ (cP @ cZ @ sK0))))) | ($true = (((^[Y0 : a]: (~ (X6 @ Y0))) @ (cP @ (sK1 @ (^[Y0 : a]: (~ (X6 @ Y0)))) @ (sK2 @ (^[Y0 : a]: (~ (X6 @ Y0))))))))) )),
% 19.92/3.30 inference(primitive_instantiation,[],[f27])).
% 19.92/3.30 thf(f90,plain,(
% 19.92/3.30 ( ! [X6 : (a > $o)] : ((((sP6 @ (~ (X6 @ (cP @ cZ @ sK0))))) = $true) | ($true = ((~ (X6 @ (cP @ (sK1 @ (^[Y0 : a]: (~ (X6 @ Y0)))) @ (sK2 @ (^[Y0 : a]: (~ (X6 @ Y0)))))))))) )),
% 19.92/3.30 inference(beta-eta_normalization,[],[f71])).
% 19.92/3.30 thf(f91,plain,(
% 19.92/3.30 ( ! [X6 : (a > $o)] : ((((X6 @ (cP @ (sK1 @ (^[Y0 : a]: (~ (X6 @ Y0)))) @ (sK2 @ (^[Y0 : a]: (~ (X6 @ Y0))))))) = $false) | (((sP6 @ (~ (X6 @ (cP @ cZ @ sK0))))) = $true)) )),
% 19.92/3.30 inference(not_proxy_clausification,[],[f90])).
% 19.92/3.30 thf(f303,plain,(
% 19.92/3.30 ( ! [X0 : (a > a),X1 : a] : ((((X0 @ (cP @ (sK1 @ (^[Y0 : a]: (~ (sP23 @ (X0 @ Y0))))) @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (X0 @ Y0)))))))) != X1) | ($true = $false) | ($true = ((sP6 @ (~ ((^[Y0 : a]: (sP23 @ (X0 @ Y0))) @ (cP @ cZ @ sK0)))))) | (cZ = X1)) )),
% 19.92/3.30 inference(constrained_superposition,[],[f91,f58])).
% 19.92/3.30 thf(f329,plain,(
% 19.92/3.30 ( ! [X0 : (a > a),X1 : a] : (($true = ((sP6 @ (~ ((^[Y0 : a]: (sP23 @ (X0 @ Y0))) @ (cP @ cZ @ sK0)))))) | (cZ = X1) | (((X0 @ (cP @ (sK1 @ (^[Y0 : a]: (~ (sP23 @ (X0 @ Y0))))) @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (X0 @ Y0)))))))) != X1)) )),
% 19.92/3.30 inference(trivial_inequality_removal,[],[f303])).
% 19.92/3.30 thf(f330,plain,(
% 19.92/3.30 ( ! [X0 : (a > a),X1 : a] : (($true = ((sP6 @ (~ (sP23 @ (X0 @ (cP @ cZ @ sK0))))))) | (cZ = X1) | (((X0 @ (cP @ (sK1 @ (^[Y0 : a]: (~ (sP23 @ (X0 @ Y0))))) @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (X0 @ Y0)))))))) != X1)) )),
% 19.92/3.30 inference(beta-eta_normalization,[],[f329])).
% 19.92/3.30 thf(f942,plain,(
% 19.92/3.30 ( ! [X0 : a] : (((((^[Y0 : a]: (cL @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (cP @ (sK1 @ (^[Y0 : a]: (~ (sP23 @ ((^[Y1 : a]: (cL @ ((^[Y2 : a]: (Y2)) @ Y1))) @ Y0))))) @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ ((^[Y1 : a]: (cL @ ((^[Y2 : a]: (Y2)) @ Y1))) @ Y0)))))))) != X0) | ($true = ((sP6 @ (~ (sP23 @ cZ))))) | (cZ = X0)) )),
% 19.92/3.30 inference(constrained_superposition,[],[f330,f19])).
% 19.92/3.30 thf(f969,plain,(
% 19.92/3.30 ( ! [X0 : a] : ((cZ = X0) | ($true = ((sP6 @ (~ (sP23 @ cZ))))) | (((cL @ (cP @ (sK1 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))) @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0)))))))) != X0)) )),
% 19.92/3.30 inference(beta-eta_normalization,[],[f942])).
% 19.92/3.30 thf(f1008,plain,(
% 19.92/3.30 ( ! [X0 : a] : ((((cL @ (cP @ (sK1 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))) @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0)))))))) != X0) | (cZ = X0) | ($true = ((sP6 @ (~ $false))))) )),
% 19.92/3.30 inference(forward_demodulation,[],[f969,f49])).
% 19.92/3.30 thf(f1009,plain,(
% 19.92/3.30 ( ! [X0 : a] : ((cZ = X0) | ($true = ((sP6 @ $true))) | (((cL @ (cP @ (sK1 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))) @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0)))))))) != X0)) )),
% 19.92/3.30 inference(boolean_simplification,[],[f1008])).
% 19.92/3.30 thf(f1033,plain,(
% 19.92/3.30 ( ! [X0 : a] : (($true = $false) | (cZ = X0) | (((cL @ (cP @ (sK1 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))) @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0)))))))) != X0)) )),
% 19.92/3.30 inference(forward_demodulation,[],[f1009,f26])).
% 19.92/3.30 thf(f1034,plain,(
% 19.92/3.30 ( ! [X0 : a] : ((((cL @ (cP @ (sK1 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))) @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0)))))))) != X0) | (cZ = X0)) )),
% 19.92/3.30 inference(trivial_inequality_removal,[],[f1033])).
% 19.92/3.30 thf(f1039,plain,(
% 19.92/3.30 ( ! [X0 : a] : ((((sK1 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0)))))) != X0) | (cZ = X0)) )),
% 19.92/3.30 inference(forward_demodulation,[],[f1034,f19])).
% 19.92/3.30 thf(f1538,plain,(
% 19.92/3.30 (cZ = ((sK1 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0)))))))),
% 19.92/3.30 inference(equality_resolution,[],[f1039])).
% 19.92/3.30 thf(f1540,plain,(
% 19.92/3.30 ($true = ((sP7 @ ((^[Y0 : a]: (~ (sP23 @ (cL @ Y0)))) @ (cP @ (cR @ cZ) @ (cR @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))))))))) | ($true = ((sP8 @ ((^[Y0 : a]: (~ (sP23 @ (cL @ Y0)))) @ (cP @ (cL @ cZ) @ (cL @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))))))))) | ($true = ((sP9 @ cZ))) | (((sP10 @ ((^[Y0 : a]: (~ (sP23 @ (cL @ Y0)))) @ (cP @ cZ @ sK0)))) = $true)),
% 19.92/3.30 inference(constrained_superposition,[],[f32,f1538])).
% 19.92/3.30 thf(f1550,plain,(
% 19.92/3.30 ($true = ((sP8 @ (~ (sP23 @ (cL @ (cP @ (cL @ cZ) @ (cL @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))))))))))) | ($true = ((sP9 @ cZ))) | ($true = ((sP7 @ (~ (sP23 @ (cL @ (cP @ (cR @ cZ) @ (cR @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))))))))))) | (((sP10 @ (~ (sP23 @ (cL @ (cP @ cZ @ sK0)))))) = $true)),
% 19.92/3.30 inference(beta-eta_normalization,[],[f1540])).
% 19.92/3.30 thf(f1554,plain,(
% 19.92/3.30 (((sP10 @ (~ (sP23 @ (cL @ (cP @ cZ @ sK0)))))) = $true) | ($true = ((sP9 @ cZ))) | ($true = ((sP8 @ (~ (sP23 @ (cL @ cZ)))))) | ($true = ((sP7 @ (~ (sP23 @ (cL @ (cP @ (cR @ cZ) @ (cR @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0)))))))))))))),
% 19.92/3.30 inference(forward_demodulation,[],[f1550,f19])).
% 19.92/3.30 thf(f1557,plain,(
% 19.92/3.30 (((sP10 @ (~ (sP23 @ cZ)))) = $true) | ($true = ((sP9 @ cZ))) | ($true = ((sP7 @ (~ (sP23 @ (cL @ (cP @ (cR @ cZ) @ (cR @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))))))))))) | ($true = ((sP8 @ (~ (sP23 @ (cL @ cZ))))))),
% 19.92/3.30 inference(forward_demodulation,[],[f1554,f19])).
% 19.92/3.30 thf(f1559,plain,(
% 19.92/3.30 ($true = ((sP7 @ (~ (sP23 @ (cL @ (cP @ (cR @ cZ) @ (cR @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))))))))))) | ($true = ((sP8 @ (~ (sP23 @ (cL @ cZ)))))) | ($true = ((sP9 @ cZ))) | ($true = ((sP10 @ (~ $false))))),
% 19.92/3.30 inference(forward_demodulation,[],[f1557,f49])).
% 19.92/3.30 thf(f1560,plain,(
% 19.92/3.30 ($true = ((sP7 @ (~ (sP23 @ (cL @ (cP @ (cR @ cZ) @ (cR @ (sK2 @ (^[Y0 : a]: (~ (sP23 @ (cL @ Y0))))))))))))) | ($true = ((sP9 @ cZ))) | ($true = ((sP8 @ (~ (sP23 @ (cL @ cZ)))))) | ($true = ((sP10 @ $true)))),
% 19.92/3.30 inference(boolean_simplification,[],[f1559])).
% 19.92/3.30 thf(f1562,plain,(
% 19.92/3.30 ($true = ((sP7 @ (~ (sP23 @ (cR @ cZ)))))) | ($true = ((sP10 @ $true))) | ($true = ((sP8 @ (~ (sP23 @ (cL @ cZ)))))) | ($true = ((sP9 @ cZ)))),
% 19.92/3.30 inference(forward_demodulation,[],[f1560,f19])).
% 19.92/3.30 thf(f1565,plain,(
% 19.92/3.30 ($true = ((sP8 @ (~ (sP23 @ (cL @ cZ)))))) | ($true = ((sP9 @ cZ))) | (((sP7 @ (~ (sP23 @ cZ)))) = $true) | ($true = ((sP10 @ $true)))),
% 19.92/3.30 inference(forward_demodulation,[],[f1562,f12])).
% 19.92/3.30 thf(f1568,plain,(
% 19.92/3.30 (((sP7 @ (~ (sP23 @ cZ)))) = $true) | ($true = ((sP9 @ cZ))) | ($true = ((sP8 @ (~ (sP23 @ cZ))))) | ($true = ((sP10 @ $true)))),
% 19.92/3.30 inference(forward_demodulation,[],[f1565,f21])).
% 19.92/3.30 thf(f1571,plain,(
% 19.92/3.30 ($true = ((sP10 @ $true))) | ($true = ((sP8 @ (~ (sP23 @ cZ))))) | ($true = ((sP9 @ cZ))) | ($true = ((sP7 @ (~ $false))))),
% 19.92/3.30 inference(forward_demodulation,[],[f1568,f49])).
% 19.92/3.30 thf(f1572,plain,(
% 19.92/3.30 ($true = ((sP9 @ cZ))) | ($true = ((sP8 @ (~ (sP23 @ cZ))))) | ($true = ((sP7 @ $true))) | ($true = ((sP10 @ $true)))),
% 19.92/3.30 inference(boolean_simplification,[],[f1571])).
% 19.92/3.30 thf(f1575,plain,(
% 19.92/3.30 ($true = ((sP8 @ (~ (sP23 @ cZ))))) | ($true = $false) | ($true = ((sP7 @ $true))) | ($true = ((sP10 @ $true)))),
% 19.92/3.30 inference(forward_demodulation,[],[f1572,f30])).
% 19.92/3.30 thf(f1576,plain,(
% 19.92/3.30 ($true = ((sP10 @ $true))) | ($true = ((sP8 @ (~ (sP23 @ cZ))))) | ($true = ((sP7 @ $true)))),
% 19.92/3.30 inference(trivial_inequality_removal,[],[f1575])).
% 19.92/3.30 thf(f1578,plain,(
% 19.92/3.30 ($true = ((sP8 @ (~ (sP23 @ cZ))))) | ($true = ((sP7 @ $true))) | ($true = $false)),
% 19.92/3.30 inference(forward_demodulation,[],[f1576,f31])).
% 19.92/3.30 thf(f1579,plain,(
% 19.92/3.30 ($true = ((sP8 @ (~ (sP23 @ cZ))))) | ($true = ((sP7 @ $true)))),
% 19.92/3.30 inference(trivial_inequality_removal,[],[f1578])).
% 19.92/3.30 thf(f1582,plain,(
% 19.92/3.30 ($true = ((sP7 @ $true))) | (((sP8 @ (~ $false))) = $true)),
% 19.92/3.30 inference(forward_demodulation,[],[f1579,f49])).
% 19.92/3.30 thf(f1583,plain,(
% 19.92/3.30 ($true = ((sP7 @ $true))) | ($true = ((sP8 @ $true)))),
% 19.92/3.30 inference(boolean_simplification,[],[f1582])).
% 19.92/3.30 thf(f1586,plain,(
% 19.92/3.30 ($true = ((sP8 @ $true))) | ($true = $false)),
% 19.92/3.30 inference(forward_demodulation,[],[f1583,f28])).
% 19.92/3.30 thf(f1587,plain,(
% 19.92/3.30 ($true = ((sP8 @ $true)))),
% 19.92/3.30 inference(trivial_inequality_removal,[],[f1586])).
% 19.92/3.30 thf(f1588,plain,(
% 19.92/3.30 ($true = $false)),
% 19.92/3.30 inference(forward_demodulation,[],[f1587,f29])).
% 19.92/3.30 thf(f1589,plain,(
% 19.92/3.30 $false),
% 19.92/3.30 inference(trivial_inequality_removal,[],[f1588])).
% 19.92/3.30 % SZS output end Proof for theBenchmark
% 19.92/3.30 % (187131)------------------------------
% 19.92/3.30 % (187131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.92/3.30 % (187131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.30 % (187131)CaDiCaL version: 2.1.3
% 19.92/3.30 % (187131)Termination reason: Refutation
% 19.92/3.30 % (187131)Time elapsed: 0.130 s
% 19.92/3.30 % (187131)Peak memory usage: 13 MB
% 19.92/3.30 % (187131)Instructions burned: 145 (million)
% 19.92/3.30 % (186926)Success in time 2.937 s
% 19.92/3.30 % Vampire exiting
%------------------------------------------------------------------------------