%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO560^1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:48:25 AM UTC 2026
% Result : Theorem 5.17s 1.05s
% Output : Refutation 5.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO560^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n019.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 17:15:18 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.09/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.37 % (1099840)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.22/0.37 % (1099851)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.22/0.37 % (1099851)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.22/0.37 % (1099850)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1855996975:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.22/0.37 % (1099846)lrs+10_16_si=on:nwc=1.5:random_seed=2837283747:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.22/0.37 % (1099848)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=2126488490:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.22/0.37 % (1099847)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3508288772:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.22/0.37 % (1099845)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3398213228:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.22/0.37 % (1099851)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=1781656786:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.22/0.37 % (1099847)Instruction limit reached!
% 0.22/0.37 % (1099847)------------------------------
% 0.22/0.37 % (1099847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.37 % (1099847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.37 % (1099847)CaDiCaL version: 2.1.3
% 0.22/0.37 % (1099847)Termination reason: Instruction limit
% 0.22/0.37 % (1099847)Termination phase: Saturation
% 0.22/0.37 % (1099847)Time elapsed: 0.003 s
% 0.22/0.37 % (1099847)Peak memory usage: 12 MB
% 0.22/0.37 % (1099847)Instructions burned: 4 (million)
% 0.22/0.37 % (1099851)Refutation not found, incomplete strategy
% 0.22/0.37 % (1099851)------------------------------
% 0.22/0.37 % (1099851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.37 % (1099851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.37 % (1099851)CaDiCaL version: 2.1.3
% 0.22/0.37 % (1099851)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.37 % (1099851)Time elapsed: 0.004 s
% 0.22/0.37 % (1099851)Peak memory usage: 12 MB
% 0.22/0.37 % (1099851)Instructions burned: 5 (million)
% 0.22/0.37 % (1099851)------------------------------
% 0.22/0.37 % (1099851)------------------------------
% 0.22/0.37 % (1099848)Refutation not found, incomplete strategy
% 0.22/0.37 % (1099848)------------------------------
% 0.22/0.37 % (1099848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.37 % (1099848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.37 % (1099848)CaDiCaL version: 2.1.3
% 0.22/0.37 % (1099848)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.37 % (1099848)Time elapsed: 0.008 s
% 0.22/0.37 % (1099848)Peak memory usage: 12 MB
% 0.22/0.37 % (1099848)Instructions burned: 11 (million)
% 0.22/0.37 % (1099848)------------------------------
% 0.22/0.37 % (1099848)------------------------------
% 0.22/0.37 % (1099846)Instruction limit reached!
% 0.22/0.37 % (1099846)------------------------------
% 0.22/0.37 % (1099846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.37 % (1099846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.37 % (1099846)CaDiCaL version: 2.1.3
% 0.22/0.37 % (1099846)Termination reason: Instruction limit
% 0.22/0.37 % (1099846)Termination phase: Saturation
% 0.22/0.37 % (1099846)Time elapsed: 0.011 s
% 0.22/0.37 % (1099846)Peak memory usage: 12 MB
% 0.22/0.37 % (1099846)Instructions burned: 18 (million)
% 0.22/0.37 % (1099849)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3229122088:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.22/0.37 % (1099858)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2792046074:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.77/0.40 % (1099861)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.77/0.40 % (1099859)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2864591115:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.77/0.40 % (1099858)Instruction limit reached!
% 0.77/0.40 % (1099858)------------------------------
% 0.77/0.40 % (1099858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (1099858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (1099858)CaDiCaL version: 2.1.3
% 0.77/0.40 % (1099858)Termination reason: Instruction limit
% 0.77/0.40 % (1099858)Termination phase: Saturation
% 0.77/0.40 % (1099858)Time elapsed: 0.002 s
% 0.77/0.40 % (1099858)Peak memory usage: 12 MB
% 0.77/0.40 % (1099858)Instructions burned: 2 (million)
% 0.77/0.40 % (1099861)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=808359276:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.77/0.40 % (1099850)Instruction limit reached!
% 0.77/0.40 % (1099850)------------------------------
% 0.77/0.40 % (1099850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (1099850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (1099850)CaDiCaL version: 2.1.3
% 0.77/0.40 % (1099850)Termination reason: Instruction limit
% 0.77/0.40 % (1099850)Termination phase: Saturation
% 0.77/0.40 % (1099850)Time elapsed: 0.031 s
% 0.77/0.40 % (1099850)Peak memory usage: 12 MB
% 0.77/0.40 % (1099850)Instructions burned: 77 (million)
% 0.77/0.40 % (1099862)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3003886016:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.77/0.40 % (1099859)Instruction limit reached!
% 0.77/0.40 % (1099859)------------------------------
% 0.77/0.40 % (1099859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (1099859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (1099859)CaDiCaL version: 2.1.3
% 0.77/0.40 % (1099859)Termination reason: Instruction limit
% 0.77/0.40 % (1099859)Termination phase: Saturation
% 0.77/0.40 % (1099859)Time elapsed: 0.004 s
% 0.77/0.40 % (1099859)Peak memory usage: 11 MB
% 0.77/0.40 % (1099859)Instructions burned: 6 (million)
% 0.77/0.40 % (1099861)Instruction limit reached!
% 0.77/0.40 % (1099861)------------------------------
% 0.77/0.40 % (1099861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (1099861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (1099861)CaDiCaL version: 2.1.3
% 0.77/0.40 % (1099861)Termination reason: Instruction limit
% 0.77/0.40 % (1099861)Termination phase: Saturation
% 0.77/0.40 % (1099861)Time elapsed: 0.004 s
% 0.77/0.40 % (1099861)Peak memory usage: 12 MB
% 0.77/0.40 % (1099861)Instructions burned: 7 (million)
% 0.77/0.40 % (1099849)Instruction limit reached!
% 0.77/0.40 % (1099849)------------------------------
% 0.77/0.40 % (1099849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (1099849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (1099849)CaDiCaL version: 2.1.3
% 0.77/0.40 % (1099849)Termination reason: Instruction limit
% 0.77/0.40 % (1099849)Termination phase: Saturation
% 0.77/0.40 % (1099849)Time elapsed: 0.023 s
% 0.77/0.40 % (1099849)Peak memory usage: 12 MB
% 0.77/0.40 % (1099849)Instructions burned: 25 (million)
% 0.77/0.40 % (1099862)Instruction limit reached!
% 0.77/0.40 % (1099862)------------------------------
% 0.77/0.40 % (1099862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (1099862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (1099862)CaDiCaL version: 2.1.3
% 0.77/0.40 % (1099862)Termination reason: Instruction limit
% 0.77/0.40 % (1099862)Termination phase: Saturation
% 0.77/0.40 % (1099862)Time elapsed: 0.008 s
% 0.77/0.40 % (1099862)Peak memory usage: 12 MB
% 0.77/0.40 % (1099862)Instructions burned: 12 (million)
% 0.77/0.40 % (1099845)Instruction limit reached!
% 0.77/0.40 % (1099845)------------------------------
% 0.77/0.40 % (1099845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (1099845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.43 % (1099845)CaDiCaL version: 2.1.3
% 0.77/0.43 % (1099845)Termination reason: Instruction limit
% 0.77/0.43 % (1099845)Termination phase: Saturation
% 0.77/0.43 % (1099845)Time elapsed: 0.046 s
% 0.77/0.43 % (1099845)Peak memory usage: 12 MB
% 0.77/0.43 % (1099845)Instructions burned: 88 (million)
% 0.77/0.43 % (1099870)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.77/0.43 % (1099869)lrs+10_1_si=on:cs=on:random_seed=1968698631:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.77/0.43 % (1099870)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=1733054431:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.77/0.43 % (1099870)Instruction limit reached!
% 0.77/0.43 % (1099870)------------------------------
% 0.77/0.43 % (1099870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.43 % (1099870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.43 % (1099870)CaDiCaL version: 2.1.3
% 0.77/0.44 % (1099870)Termination reason: Instruction limit
% 0.77/0.44 % (1099870)Termination phase: Saturation
% 0.77/0.44 % (1099870)Time elapsed: 0.002 s
% 0.77/0.44 % (1099870)Peak memory usage: 12 MB
% 0.77/0.44 % (1099870)Instructions burned: 2 (million)
% 0.77/0.44 % (1099869)Instruction limit reached!
% 0.77/0.44 % (1099869)------------------------------
% 0.77/0.44 % (1099869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.44 % (1099869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.44 % (1099869)CaDiCaL version: 2.1.3
% 0.77/0.44 % (1099869)Termination reason: Instruction limit
% 0.77/0.44 % (1099869)Termination phase: Saturation
% 0.77/0.44 % (1099869)Time elapsed: 0.005 s
% 0.77/0.44 % (1099869)Peak memory usage: 12 MB
% 0.77/0.44 % (1099869)Instructions burned: 8 (million)
% 0.77/0.44 % (1099865)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.77/0.44 % (1099865)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.77/0.44 % (1099872)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2935090216:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.77/0.44 % (1099868)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=2606219963:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.77/0.44 % (1099865)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2929206653:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.77/0.44 % (1099872)Refutation not found, incomplete strategy
% 0.77/0.44 % (1099872)------------------------------
% 0.77/0.44 % (1099872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.44 % (1099872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.44 % (1099872)CaDiCaL version: 2.1.3
% 0.77/0.44 % (1099872)Termination reason: Refutation not found, incomplete strategy
% 0.77/0.44 % (1099872)Time elapsed: 0.001 s
% 0.77/0.44 % (1099872)Peak memory usage: 12 MB
% 0.77/0.44 % (1099872)Instructions burned: 1 (million)
% 0.77/0.44 % (1099872)------------------------------
% 0.77/0.44 % (1099872)------------------------------
% 0.77/0.44 % (1099876)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3246080055:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.77/0.44 % (1099871)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=82718499:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.77/0.44 % (1099877)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3707280056:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.77/0.44 % (1099873)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1274046247:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.77/0.44 % (1099873)Refutation not found, incomplete strategy
% 0.77/0.48 % (1099873)------------------------------
% 0.77/0.48 % (1099873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.48 % (1099873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.48 % (1099873)CaDiCaL version: 2.1.3
% 0.77/0.48 % (1099873)Termination reason: Refutation not found, incomplete strategy
% 0.77/0.48 % (1099873)Time elapsed: 0.002 s
% 0.77/0.48 % (1099873)Peak memory usage: 12 MB
% 0.77/0.48 % (1099873)Instructions burned: 1 (million)
% 0.77/0.48 % (1099873)------------------------------
% 0.77/0.48 % (1099873)------------------------------
% 0.77/0.48 % (1099876)Instruction limit reached!
% 0.77/0.48 % (1099876)------------------------------
% 0.77/0.48 % (1099876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.48 % (1099876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.48 % (1099876)CaDiCaL version: 2.1.3
% 0.77/0.48 % (1099876)Termination reason: Instruction limit
% 0.77/0.48 % (1099876)Termination phase: Saturation
% 0.77/0.48 % (1099876)Time elapsed: 0.010 s
% 0.77/0.48 % (1099876)Peak memory usage: 12 MB
% 0.77/0.48 % (1099876)Instructions burned: 15 (million)
% 0.77/0.48 % (1099871)Refutation not found, incomplete strategy
% 0.77/0.48 % (1099871)------------------------------
% 0.77/0.48 % (1099871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.48 % (1099871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.48 % (1099871)CaDiCaL version: 2.1.3
% 0.77/0.48 % (1099871)Termination reason: Refutation not found, incomplete strategy
% 0.77/0.48 % (1099871)Time elapsed: 0.011 s
% 0.77/0.48 % (1099871)Peak memory usage: 12 MB
% 0.77/0.48 % (1099871)Instructions burned: 9 (million)
% 0.77/0.48 % (1099881)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=331059714:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.77/0.48 % (1099871)------------------------------
% 0.77/0.48 % (1099871)------------------------------
% 0.77/0.48 % (1099881)Refutation not found, incomplete strategy
% 0.77/0.48 % (1099881)------------------------------
% 0.77/0.48 % (1099881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.48 % (1099881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.48 % (1099881)CaDiCaL version: 2.1.3
% 0.77/0.48 % (1099881)Termination reason: Refutation not found, incomplete strategy
% 0.77/0.48 % (1099881)Time elapsed: 0.005 s
% 0.77/0.48 % (1099881)Peak memory usage: 12 MB
% 0.77/0.48 % (1099881)Instructions burned: 6 (million)
% 0.77/0.48 % (1099865)Instruction limit reached!
% 0.77/0.48 % (1099865)------------------------------
% 0.77/0.48 % (1099865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.48 % (1099865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.48 % (1099865)CaDiCaL version: 2.1.3
% 0.77/0.48 % (1099865)Termination reason: Instruction limit
% 0.77/0.48 % (1099865)Termination phase: Saturation
% 0.77/0.48 % (1099865)Time elapsed: 0.026 s
% 0.77/0.48 % (1099865)Peak memory usage: 12 MB
% 0.77/0.48 % (1099865)Instructions burned: 28 (million)
% 0.77/0.48 % (1099881)------------------------------
% 0.77/0.48 % (1099881)------------------------------
% 0.77/0.48 % (1099886)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2065999842: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)
% 0.77/0.48 % (1099889)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3697285875:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.77/0.48 % (1099886)Instruction limit reached!
% 0.77/0.48 % (1099886)------------------------------
% 0.77/0.48 % (1099886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.48 % (1099886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.48 % (1099886)CaDiCaL version: 2.1.3
% 0.77/0.48 % (1099886)Termination reason: Instruction limit
% 0.77/0.48 % (1099886)Termination phase: Saturation
% 0.77/0.48 % (1099886)Time elapsed: 0.002 s
% 0.77/0.48 % (1099886)Peak memory usage: 12 MB
% 0.77/0.48 % (1099886)Instructions burned: 2 (million)
% 0.77/0.48 % (1099887)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2109796913:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.77/0.48 % (1099887)Refutation not found, incomplete strategy
% 1.48/0.53 % (1099887)------------------------------
% 1.48/0.53 % (1099887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.53 % (1099887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.53 % (1099887)CaDiCaL version: 2.1.3
% 1.48/0.53 % (1099887)Termination reason: Refutation not found, incomplete strategy
% 1.48/0.53 % (1099887)Time elapsed: 0.003 s
% 1.48/0.53 % (1099887)Peak memory usage: 12 MB
% 1.48/0.53 % (1099887)Instructions burned: 3 (million)
% 1.48/0.53 % (1099887)------------------------------
% 1.48/0.53 % (1099887)------------------------------
% 1.48/0.53 % (1099889)Instruction limit reached!
% 1.48/0.53 % (1099889)------------------------------
% 1.48/0.53 % (1099889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.53 % (1099889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.53 % (1099889)CaDiCaL version: 2.1.3
% 1.48/0.53 % (1099889)Termination reason: Instruction limit
% 1.48/0.53 % (1099889)Termination phase: Saturation
% 1.48/0.53 % (1099889)Time elapsed: 0.009 s
% 1.48/0.53 % (1099889)Peak memory usage: 12 MB
% 1.48/0.53 % (1099889)Instructions burned: 23 (million)
% 1.48/0.53 % (1099894)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.48/0.53 % (1099891)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.48/0.53 % (1099891)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.48/0.53 % (1099894)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=3619003144:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.48/0.53 % (1099894)Refutation not found, incomplete strategy
% 1.48/0.53 % (1099894)------------------------------
% 1.48/0.53 % (1099894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.53 % (1099894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.53 % (1099894)CaDiCaL version: 2.1.3
% 1.48/0.53 % (1099894)Termination reason: Refutation not found, incomplete strategy
% 1.48/0.53 % (1099894)Time elapsed: 0.002 s
% 1.48/0.53 % (1099894)Peak memory usage: 12 MB
% 1.48/0.53 % (1099894)Instructions burned: 1 (million)
% 1.48/0.53 % (1099894)------------------------------
% 1.48/0.53 % (1099894)------------------------------
% 1.48/0.53 % (1099868)Instruction limit reached!
% 1.48/0.53 % (1099868)------------------------------
% 1.48/0.53 % (1099868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.53 % (1099868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.53 % (1099868)CaDiCaL version: 2.1.3
% 1.48/0.53 % (1099868)Termination reason: Instruction limit
% 1.48/0.53 % (1099868)Termination phase: Saturation
% 1.48/0.53 % (1099868)Time elapsed: 0.062 s
% 1.48/0.53 % (1099868)Peak memory usage: 12 MB
% 1.48/0.53 % (1099868)Instructions burned: 88 (million)
% 1.48/0.53 % (1099891)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=701854023:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.48/0.53 % (1099890)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1966707403:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.48/0.53 % (1099891)Instruction limit reached!
% 1.48/0.53 % (1099891)------------------------------
% 1.48/0.53 % (1099891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.53 % (1099891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.53 % (1099891)CaDiCaL version: 2.1.3
% 1.48/0.53 % (1099891)Termination reason: Instruction limit
% 1.48/0.53 % (1099891)Termination phase: Saturation
% 1.48/0.53 % (1099891)Time elapsed: 0.010 s
% 1.48/0.53 % (1099891)Peak memory usage: 12 MB
% 1.48/0.53 % (1099891)Instructions burned: 15 (million)
% 1.48/0.53 % (1099896)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=2964910714:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.48/0.61 % (1099897)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2007915122:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.48/0.61 % (1099899)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=599879672:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.48/0.61 % (1099897)Instruction limit reached!
% 1.48/0.61 % (1099897)------------------------------
% 1.48/0.61 % (1099897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.61 % (1099897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.61 % (1099897)CaDiCaL version: 2.1.3
% 1.48/0.61 % (1099897)Termination reason: Instruction limit
% 1.48/0.61 % (1099897)Termination phase: Saturation
% 1.48/0.61 % (1099897)Time elapsed: 0.004 s
% 1.48/0.61 % (1099897)Peak memory usage: 12 MB
% 1.48/0.61 % (1099897)Instructions burned: 7 (million)
% 1.48/0.61 % (1099900)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=695056608:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.48/0.61 % (1099896)Instruction limit reached!
% 1.48/0.61 % (1099896)------------------------------
% 1.48/0.61 % (1099896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.61 % (1099896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.61 % (1099896)CaDiCaL version: 2.1.3
% 1.48/0.61 % (1099896)Termination reason: Instruction limit
% 1.48/0.61 % (1099896)Termination phase: Saturation
% 1.48/0.61 % (1099896)Time elapsed: 0.013 s
% 1.48/0.61 % (1099896)Peak memory usage: 12 MB
% 1.48/0.61 % (1099896)Instructions burned: 32 (million)
% 1.48/0.61 % (1099900)Instruction limit reached!
% 1.48/0.61 % (1099900)------------------------------
% 1.48/0.61 % (1099900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.61 % (1099900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.61 % (1099900)CaDiCaL version: 2.1.3
% 1.48/0.61 % (1099900)Termination reason: Instruction limit
% 1.48/0.61 % (1099900)Termination phase: Saturation
% 1.48/0.61 % (1099900)Time elapsed: 0.012 s
% 1.48/0.61 % (1099900)Peak memory usage: 12 MB
% 1.48/0.61 % (1099900)Instructions burned: 20 (million)
% 1.48/0.61 % (1099899)Instruction limit reached!
% 1.48/0.61 % (1099899)------------------------------
% 1.48/0.61 % (1099899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.61 % (1099899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.61 % (1099899)CaDiCaL version: 2.1.3
% 1.48/0.61 % (1099899)Termination reason: Instruction limit
% 1.48/0.61 % (1099899)Termination phase: Saturation
% 1.48/0.61 % (1099899)Time elapsed: 0.012 s
% 1.48/0.61 % (1099899)Peak memory usage: 12 MB
% 1.48/0.61 % (1099899)Instructions burned: 23 (million)
% 1.48/0.61 % (1099904)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=4088922037:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.48/0.61 % (1099908)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=491397009:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.48/0.61 % (1099911)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.48/0.61 % (1099910)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2328731888:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.48/0.61 % (1099911)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2209320775:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.48/0.61 % (1099911)Instruction limit reached!
% 1.48/0.61 % (1099911)------------------------------
% 1.48/0.61 % (1099911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.61 % (1099911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.61 % (1099911)CaDiCaL version: 2.1.3
% 1.48/0.61 % (1099911)Termination reason: Instruction limit
% 1.48/0.61 % (1099911)Termination phase: Saturation
% 1.48/0.61 % (1099911)Time elapsed: 0.004 s
% 1.48/0.61 % (1099911)Peak memory usage: 12 MB
% 1.48/0.61 % (1099911)Instructions burned: 7 (million)
% 1.48/0.61 % (1099890)Instruction limit reached!
% 1.48/0.61 % (1099890)------------------------------
% 1.48/0.61 % (1099890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.68 % (1099890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.68 % (1099890)CaDiCaL version: 2.1.3
% 2.61/0.68 % (1099890)Termination reason: Instruction limit
% 2.61/0.68 % (1099890)Termination phase: Saturation
% 2.61/0.68 % (1099890)Time elapsed: 0.055 s
% 2.61/0.68 % (1099890)Peak memory usage: 12 MB
% 2.61/0.68 % (1099890)Instructions burned: 60 (million)
% 2.61/0.68 % (1099909)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2764655847:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.61/0.68 % (1099910)Instruction limit reached!
% 2.61/0.68 % (1099910)------------------------------
% 2.61/0.68 % (1099910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.68 % (1099910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.68 % (1099910)CaDiCaL version: 2.1.3
% 2.61/0.68 % (1099910)Termination reason: Instruction limit
% 2.61/0.68 % (1099910)Termination phase: Saturation
% 2.61/0.68 % (1099910)Time elapsed: 0.021 s
% 2.61/0.68 % (1099910)Peak memory usage: 12 MB
% 2.61/0.68 % (1099910)Instructions burned: 42 (million)
% 2.61/0.68 % (1099916)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3976882766:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.61/0.68 % (1099919)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.61/0.68 % (1099917)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=302930979:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.61/0.68 % (1099917)Refutation not found, incomplete strategy
% 2.61/0.68 % (1099917)------------------------------
% 2.61/0.68 % (1099917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.68 % (1099917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.68 % (1099917)CaDiCaL version: 2.1.3
% 2.61/0.68 % (1099917)Termination reason: Refutation not found, incomplete strategy
% 2.61/0.68 % (1099917)Time elapsed: 0.001 s
% 2.61/0.68 % (1099917)Peak memory usage: 12 MB
% 2.61/0.68 % (1099917)Instructions burned: 1 (million)
% 2.61/0.68 % (1099917)------------------------------
% 2.61/0.68 % (1099917)------------------------------
% 2.61/0.68 % (1099919)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3023160138:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.61/0.68 % (1099919)Instruction limit reached!
% 2.61/0.68 % (1099919)------------------------------
% 2.61/0.68 % (1099919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.68 % (1099919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.68 % (1099919)CaDiCaL version: 2.1.3
% 2.61/0.68 % (1099919)Termination reason: Instruction limit
% 2.61/0.68 % (1099919)Termination phase: Saturation
% 2.61/0.68 % (1099919)Time elapsed: 0.004 s
% 2.61/0.68 % (1099919)Peak memory usage: 12 MB
% 2.61/0.68 % (1099919)Instructions burned: 7 (million)
% 2.61/0.68 % (1099877)Instruction limit reached!
% 2.61/0.68 % (1099877)------------------------------
% 2.61/0.68 % (1099877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.68 % (1099877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.68 % (1099877)CaDiCaL version: 2.1.3
% 2.61/0.68 % (1099877)Termination reason: Instruction limit
% 2.61/0.68 % (1099877)Termination phase: Saturation
% 2.61/0.68 % (1099877)Time elapsed: 0.159 s
% 2.61/0.68 % (1099877)Peak memory usage: 13 MB
% 2.61/0.68 % (1099877)Instructions burned: 327 (million)
% 2.61/0.68 % (1099923)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1516341351:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.61/0.68 % (1099924)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=4064595410:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.61/0.68 % (1099924)Refutation not found, incomplete strategy
% 2.61/0.68 % (1099924)------------------------------
% 2.61/0.68 % (1099924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.68 % (1099924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.76 % (1099924)CaDiCaL version: 2.1.3
% 2.76/0.76 % (1099924)Termination reason: Refutation not found, incomplete strategy
% 2.76/0.76 % (1099924)Time elapsed: 0.001 s
% 2.76/0.76 % (1099924)Peak memory usage: 12 MB
% 2.76/0.76 % (1099924)Instructions burned: 1 (million)
% 2.76/0.76 % (1099924)------------------------------
% 2.76/0.76 % (1099924)------------------------------
% 2.76/0.76 % (1099923)Instruction limit reached!
% 2.76/0.76 % (1099923)------------------------------
% 2.76/0.76 % (1099923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.76 % (1099923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.76 % (1099923)CaDiCaL version: 2.1.3
% 2.76/0.76 % (1099923)Termination reason: Instruction limit
% 2.76/0.76 % (1099923)Termination phase: Saturation
% 2.76/0.76 % (1099923)Time elapsed: 0.011 s
% 2.76/0.76 % (1099923)Peak memory usage: 12 MB
% 2.76/0.76 % (1099923)Instructions burned: 22 (million)
% 2.76/0.76 % (1099925)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=3612591827:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.76/0.76 % (1099928)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=1041482724:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 2.76/0.76 % (1099929)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=1517495388:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 2.76/0.76 % (1099916)Instruction limit reached!
% 2.76/0.76 % (1099916)------------------------------
% 2.76/0.76 % (1099916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.76 % (1099916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.76 % (1099916)CaDiCaL version: 2.1.3
% 2.76/0.76 % (1099916)Termination reason: Instruction limit
% 2.76/0.76 % (1099916)Termination phase: Saturation
% 2.76/0.76 % (1099916)Time elapsed: 0.092 s
% 2.76/0.76 % (1099916)Peak memory usage: 13 MB
% 2.76/0.76 % (1099916)Instructions burned: 182 (million)
% 2.76/0.76 % (1099909)Instruction limit reached!
% 2.76/0.76 % (1099909)------------------------------
% 2.76/0.76 % (1099909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.76 % (1099909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.76 % (1099909)CaDiCaL version: 2.1.3
% 2.76/0.76 % (1099909)Termination reason: Instruction limit
% 2.76/0.76 % (1099909)Termination phase: Saturation
% 2.76/0.76 % (1099909)Time elapsed: 0.108 s
% 2.76/0.76 % (1099909)Peak memory usage: 13 MB
% 2.76/0.76 % (1099909)Instructions burned: 193 (million)
% 2.76/0.76 % (1099908)Instruction limit reached!
% 2.76/0.76 % (1099908)------------------------------
% 2.76/0.76 % (1099908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.76 % (1099908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.76 % (1099908)CaDiCaL version: 2.1.3
% 2.76/0.76 % (1099908)Termination reason: Instruction limit
% 2.76/0.76 % (1099908)Termination phase: Saturation
% 2.76/0.76 % (1099908)Time elapsed: 0.135 s
% 2.76/0.76 % (1099908)Peak memory usage: 13 MB
% 2.76/0.76 % (1099908)Instructions burned: 143 (million)
% 2.76/0.76 % (1099933)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2523672687:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 2.76/0.76 % (1099934)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1928803569:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 2.76/0.76 % (1099933)Refutation not found, incomplete strategy
% 2.76/0.76 % (1099933)------------------------------
% 2.76/0.76 % (1099933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.76 % (1099933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.76 % (1099933)CaDiCaL version: 2.1.3
% 2.76/0.76 % (1099933)Termination reason: Refutation not found, incomplete strategy
% 2.76/0.76 % (1099933)Time elapsed: 0.001 s
% 2.76/0.76 % (1099933)Peak memory usage: 12 MB
% 2.76/0.76 % (1099933)Instructions burned: 1 (million)
% 3.25/0.87 % (1099933)------------------------------
% 3.25/0.87 % (1099933)------------------------------
% 3.25/0.87 % (1099934)Instruction limit reached!
% 3.25/0.87 % (1099934)------------------------------
% 3.25/0.87 % (1099934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1099934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1099934)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1099934)Termination reason: Instruction limit
% 3.25/0.87 % (1099934)Termination phase: Saturation
% 3.25/0.87 % (1099934)Time elapsed: 0.011 s
% 3.25/0.87 % (1099934)Peak memory usage: 12 MB
% 3.25/0.87 % (1099934)Instructions burned: 21 (million)
% 3.25/0.87 % (1099935)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.25/0.87 % (1099938)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3055655589:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.25/0.87 % (1099935)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2320085151:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.25/0.87 % (1099938)Instruction limit reached!
% 3.25/0.87 % (1099938)------------------------------
% 3.25/0.87 % (1099938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1099938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1099938)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1099938)Termination reason: Instruction limit
% 3.25/0.87 % (1099938)Termination phase: Saturation
% 3.25/0.87 % (1099938)Time elapsed: 0.008 s
% 3.25/0.87 % (1099938)Peak memory usage: 12 MB
% 3.25/0.87 % (1099938)Instructions burned: 14 (million)
% 3.25/0.87 % (1099929)Instruction limit reached!
% 3.25/0.87 % (1099929)------------------------------
% 3.25/0.87 % (1099929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1099939)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=2315960089:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.25/0.87 % (1099929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1099929)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1099929)Termination reason: Instruction limit
% 3.25/0.87 % (1099929)Termination phase: Saturation
% 3.25/0.87 % (1099929)Time elapsed: 0.057 s
% 3.25/0.87 % (1099929)Peak memory usage: 12 MB
% 3.25/0.87 % (1099929)Instructions burned: 45 (million)
% 3.25/0.87 % (1099942)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=882263978:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.25/0.87 % (1099942)Refutation not found, incomplete strategy
% 3.25/0.87 % (1099942)------------------------------
% 3.25/0.87 % (1099942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1099942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1099942)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1099942)Termination reason: Refutation not found, incomplete strategy
% 3.25/0.87 % (1099942)Time elapsed: 0.001 s
% 3.25/0.87 % (1099942)Peak memory usage: 12 MB
% 3.25/0.87 % (1099942)Instructions burned: 1 (million)
% 3.25/0.87 % (1099944)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=797417282:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 3.25/0.87 % (1099942)------------------------------
% 3.25/0.87 % (1099942)------------------------------
% 3.25/0.87 % (1099944)Refutation not found, incomplete strategy
% 3.25/0.87 % (1099944)------------------------------
% 3.25/0.87 % (1099944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1099944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1099944)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1099944)Termination reason: Refutation not found, incomplete strategy
% 3.25/0.87 % (1099944)Time elapsed: 0.002 s
% 3.25/0.87 % (1099944)Peak memory usage: 12 MB
% 3.25/0.87 % (1099944)Instructions burned: 2 (million)
% 3.25/0.87 % (1099944)------------------------------
% 3.25/0.87 % (1099944)------------------------------
% 3.25/0.87 % (1099947)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1812031518:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.91/0.96 % (1099947)Refutation not found, incomplete strategy
% 3.91/0.96 % (1099947)------------------------------
% 3.91/0.96 % (1099947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.96 % (1099947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/0.96 % (1099947)CaDiCaL version: 2.1.3
% 3.91/0.96 % (1099947)Termination reason: Refutation not found, incomplete strategy
% 3.91/0.96 % (1099947)Time elapsed: 0.005 s
% 3.91/0.96 % (1099947)Peak memory usage: 12 MB
% 3.91/0.96 % (1099947)Instructions burned: 6 (million)
% 3.91/0.96 % (1099939)Instruction limit reached!
% 3.91/0.96 % (1099939)------------------------------
% 3.91/0.96 % (1099939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.96 % (1099939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/0.96 % (1099939)CaDiCaL version: 2.1.3
% 3.91/0.96 % (1099939)Termination reason: Instruction limit
% 3.91/0.96 % (1099939)Termination phase: Saturation
% 3.91/0.96 % (1099939)Time elapsed: 0.045 s
% 3.91/0.96 % (1099939)Peak memory usage: 12 MB
% 3.91/0.96 % (1099939)Instructions burned: 66 (million)
% 3.91/0.96 % (1099947)------------------------------
% 3.91/0.96 % (1099947)------------------------------
% 3.91/0.96 % (1099948)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=4194414640:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.91/0.96 % (1099953)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.91/0.96 % (1099952)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=1119899086:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.91/0.96 % (1099953)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=875836087:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 3.91/0.96 % (1099925)Instruction limit reached!
% 3.91/0.96 % (1099925)------------------------------
% 3.91/0.96 % (1099925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.96 % (1099925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/0.96 % (1099925)CaDiCaL version: 2.1.3
% 3.91/0.96 % (1099925)Termination reason: Instruction limit
% 3.91/0.96 % (1099925)Termination phase: Saturation
% 3.91/0.96 % (1099925)Time elapsed: 0.164 s
% 3.91/0.96 % (1099925)Peak memory usage: 13 MB
% 3.91/0.96 % (1099925)Instructions burned: 316 (million)
% 3.91/0.96 % (1099948)Instruction limit reached!
% 3.91/0.96 % (1099948)------------------------------
% 3.91/0.96 % (1099948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.96 % (1099948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/0.96 % (1099948)CaDiCaL version: 2.1.3
% 3.91/0.96 % (1099948)Termination reason: Instruction limit
% 3.91/0.96 % (1099948)Termination phase: Saturation
% 3.91/0.96 % (1099948)Time elapsed: 0.030 s
% 3.91/0.96 % (1099948)Peak memory usage: 12 MB
% 3.91/0.96 % (1099948)Instructions burned: 34 (million)
% 3.91/0.96 % (1099956)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=3013028591:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 3.91/0.96 % (1099952)Instruction limit reached!
% 3.91/0.96 % (1099952)------------------------------
% 3.91/0.96 % (1099952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.96 % (1099952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/0.96 % (1099952)CaDiCaL version: 2.1.3
% 3.91/0.96 % (1099952)Termination reason: Instruction limit
% 3.91/0.96 % (1099952)Termination phase: Saturation
% 3.91/0.96 % (1099952)Time elapsed: 0.036 s
% 3.91/0.96 % (1099952)Peak memory usage: 12 MB
% 3.91/0.96 % (1099952)Instructions burned: 69 (million)
% 3.91/0.96 % (1099957)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=2177328743:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 3.91/0.96 % (1099959)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=2004116394:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 3.91/0.96 % (1099959)Refutation not found, incomplete strategy
% 3.91/0.96 % (1099959)------------------------------
% 3.91/0.96 % (1099959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.96 % (1099959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099959)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099959)Termination reason: Refutation not found, incomplete strategy
% 5.17/1.05 % (1099959)Time elapsed: 0.002 s
% 5.17/1.05 % (1099959)Peak memory usage: 12 MB
% 5.17/1.05 % (1099959)Instructions burned: 3 (million)
% 5.17/1.05 % (1099959)------------------------------
% 5.17/1.05 % (1099959)------------------------------
% 5.17/1.05 % (1099962)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1635445134:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 5.17/1.05 % (1099953)Instruction limit reached!
% 5.17/1.05 % (1099953)------------------------------
% 5.17/1.05 % (1099953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099953)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099953)Termination reason: Instruction limit
% 5.17/1.05 % (1099953)Termination phase: Saturation
% 5.17/1.05 % (1099953)Time elapsed: 0.089 s
% 5.17/1.05 % (1099953)Peak memory usage: 14 MB
% 5.17/1.05 % (1099953)Instructions burned: 181 (million)
% 5.17/1.05 % (1099935)Instruction limit reached!
% 5.17/1.05 % (1099935)------------------------------
% 5.17/1.05 % (1099935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099935)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099935)Termination reason: Instruction limit
% 5.17/1.05 % (1099935)Termination phase: Saturation
% 5.17/1.05 % (1099935)Time elapsed: 0.171 s
% 5.17/1.05 % (1099935)Peak memory usage: 13 MB
% 5.17/1.05 % (1099935)Instructions burned: 200 (million)
% 5.17/1.05 % (1099957)Instruction limit reached!
% 5.17/1.05 % (1099957)------------------------------
% 5.17/1.05 % (1099957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099957)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099957)Termination reason: Instruction limit
% 5.17/1.05 % (1099957)Termination phase: Saturation
% 5.17/1.05 % (1099957)Time elapsed: 0.057 s
% 5.17/1.05 % (1099957)Peak memory usage: 12 MB
% 5.17/1.05 % (1099957)Instructions burned: 98 (million)
% 5.17/1.05 % (1099964)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3761256120:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 5.17/1.05 % (1099965)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2546295289:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 5.17/1.05 % (1099966)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2421392778:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 5.17/1.05 % (1099966)Refutation not found, incomplete strategy
% 5.17/1.05 % (1099966)------------------------------
% 5.17/1.05 % (1099966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099966)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099966)Termination reason: Refutation not found, incomplete strategy
% 5.17/1.05 % (1099966)Time elapsed: 0.003 s
% 5.17/1.05 % (1099966)Peak memory usage: 12 MB
% 5.17/1.05 % (1099966)Instructions burned: 3 (million)
% 5.17/1.05 % (1099966)------------------------------
% 5.17/1.05 % (1099966)------------------------------
% 5.17/1.05 % (1099970)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3558267813:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 5.17/1.05 % (1099970)Refutation not found, incomplete strategy
% 5.17/1.05 % (1099970)------------------------------
% 5.17/1.05 % (1099970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099970)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099970)Termination reason: Refutation not found, incomplete strategy
% 5.17/1.05 % (1099970)Time elapsed: 0.001 s
% 5.17/1.05 % (1099970)Peak memory usage: 12 MB
% 5.17/1.05 % (1099970)Instructions burned: 1 (million)
% 5.17/1.05 % (1099970)------------------------------
% 5.17/1.05 % (1099970)------------------------------
% 5.17/1.05 % (1099972)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=421850813:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 5.17/1.05 % (1099972)Refutation not found, incomplete strategy
% 5.17/1.05 % (1099972)------------------------------
% 5.17/1.05 % (1099972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099972)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099972)Termination reason: Refutation not found, incomplete strategy
% 5.17/1.05 % (1099972)Time elapsed: 0.004 s
% 5.17/1.05 % (1099972)Peak memory usage: 12 MB
% 5.17/1.05 % (1099972)Instructions burned: 5 (million)
% 5.17/1.05 % (1099972)------------------------------
% 5.17/1.05 % (1099972)------------------------------
% 5.17/1.05 % (1099904)Instruction limit reached!
% 5.17/1.05 % (1099904)------------------------------
% 5.17/1.05 % (1099904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099904)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099904)Termination reason: Instruction limit
% 5.17/1.05 % (1099904)Termination phase: Saturation
% 5.17/1.05 % (1099904)Time elapsed: 0.440 s
% 5.17/1.05 % (1099904)Peak memory usage: 15 MB
% 5.17/1.05 % (1099904)Instructions burned: 1241 (million)
% 5.17/1.05 % (1099965)Instruction limit reached!
% 5.17/1.05 % (1099965)------------------------------
% 5.17/1.05 % (1099965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099965)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099965)Termination reason: Instruction limit
% 5.17/1.05 % (1099965)Termination phase: Saturation
% 5.17/1.05 % (1099965)Time elapsed: 0.071 s
% 5.17/1.05 % (1099965)Peak memory usage: 13 MB
% 5.17/1.05 % (1099965)Instructions burned: 130 (million)
% 5.17/1.05 % (1099974)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=2476023052:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 5.17/1.05 % (1099976)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=3399471543:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2993 on theBenchmark for (2993ds/105Mi)
% 5.17/1.05 % (1099975)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=3677108219:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 5.17/1.05 % (1099974)Instruction limit reached!
% 5.17/1.05 % (1099974)------------------------------
% 5.17/1.05 % (1099974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099974)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099974)Termination reason: Instruction limit
% 5.17/1.05 % (1099974)Termination phase: Saturation
% 5.17/1.05 % (1099974)Time elapsed: 0.042 s
% 5.17/1.05 % (1099974)Peak memory usage: 12 MB
% 5.17/1.05 % (1099974)Instructions burned: 96 (million)
% 5.17/1.05 % (1099956)Instruction limit reached!
% 5.17/1.05 % (1099956)------------------------------
% 5.17/1.05 % (1099956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099956)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099956)Termination reason: Instruction limit
% 5.17/1.05 % (1099956)Termination phase: Saturation
% 5.17/1.05 % (1099956)Time elapsed: 0.217 s
% 5.17/1.05 % (1099956)Peak memory usage: 12 MB
% 5.17/1.05 % (1099956)Instructions burned: 246 (million)
% 5.17/1.05 % (1099980)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=344459262:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2993 on theBenchmark for (2993ds/5755Mi)
% 5.17/1.05 % (1099975)Instruction limit reached!
% 5.17/1.05 % (1099975)------------------------------
% 5.17/1.05 % (1099975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099975)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099975)Termination reason: Instruction limit
% 5.17/1.05 % (1099975)Termination phase: Saturation
% 5.17/1.05 % (1099975)Time elapsed: 0.046 s
% 5.17/1.05 % (1099975)Peak memory usage: 12 MB
% 5.17/1.05 % (1099975)Instructions burned: 65 (million)
% 5.17/1.05 % (1099976)Instruction limit reached!
% 5.17/1.05 % (1099976)------------------------------
% 5.17/1.05 % (1099976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099976)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099976)Termination reason: Instruction limit
% 5.17/1.05 % (1099976)Termination phase: Saturation
% 5.17/1.05 % (1099976)Time elapsed: 0.054 s
% 5.17/1.05 % (1099976)Peak memory usage: 12 MB
% 5.17/1.05 % (1099976)Instructions burned: 107 (million)
% 5.17/1.05 % (1099928)Instruction limit reached!
% 5.17/1.05 % (1099928)------------------------------
% 5.17/1.05 % (1099928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099928)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099928)Termination reason: Instruction limit
% 5.17/1.05 % (1099928)Termination phase: Saturation
% 5.17/1.05 % (1099928)Time elapsed: 0.424 s
% 5.17/1.05 % (1099928)Peak memory usage: 15 MB
% 5.17/1.05 % (1099928)Instructions burned: 855 (million)
% 5.17/1.05 % (1099981)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=3277897320:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 5.17/1.05 % (1099984)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=2785167217:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 5.17/1.05 % (1099983)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2485613227:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/495Mi)
% 5.17/1.05 % (1099985)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=211774324:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/91Mi)
% 5.17/1.05 % (1099984)Instruction limit reached!
% 5.17/1.05 % (1099984)------------------------------
% 5.17/1.05 % (1099984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099984)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099984)Termination reason: Instruction limit
% 5.17/1.05 % (1099984)Termination phase: Saturation
% 5.17/1.05 % (1099984)Time elapsed: 0.027 s
% 5.17/1.05 % (1099984)Peak memory usage: 12 MB
% 5.17/1.05 % (1099984)Instructions burned: 35 (million)
% 5.17/1.05 % (1099985) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1099840-1099985"...
% 5.17/1.05 % (1099990)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2990587505:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2992 on theBenchmark for (2992ds/66Mi)
% 5.17/1.05 % (1099985)...printing done.
% 5.17/1.05 % (1099985)Refutation found. Thanks to Tanya!
% 5.17/1.05 % SZS status Theorem for theBenchmark
% 5.17/1.05 % SZS output start Proof for theBenchmark
% 5.17/1.05 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 5.17/1.05 thf(func_def_0, type, epso: (($o > $o) > $o)).
% 5.17/1.05 thf(func_def_2, type, epsoo: ((($o > $o) > $o) > $o > $o)).
% 5.17/1.05 thf(func_def_3, type, q: (($o > $o) > $o)).
% 5.17/1.05 thf(func_def_6, type, db0: !>[X0: $tType]:(X0)).
% 5.17/1.05 thf(func_def_7, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 5.17/1.05 thf(func_def_8, type, sF0: ($o > $o)).
% 5.17/1.05 thf(func_def_9, type, sF1: $o).
% 5.17/1.05 thf(func_def_10, type, vOR: ($o > $o > $o)).
% 5.17/1.05 thf(func_def_12, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 5.17/1.05 thf(func_def_13, type, vNOT: ($o > $o)).
% 5.17/1.05 thf(func_def_14, type, db1: !>[X0: $tType]:(X0)).
% 5.17/1.05 thf(func_def_15, type, sK3: $o).
% 5.17/1.05 thf(func_def_16, type, sK4: $o).
% 5.17/1.05 thf(func_def_17, type, db2: !>[X0: $tType]:(X0)).
% 5.17/1.05 thf(func_def_18, type, sK5: (($o > $o) > $o)).
% 5.17/1.05 thf(func_def_19, type, sK6: $o).
% 5.17/1.05 thf(func_def_20, type, sK7: (($o > $o) > $o)).
% 5.17/1.05 thf(f1,axiom,(
% 5.17/1.05 ! [X0 : ($o > $o)] : (? [X1 : $o] : (X0 @ X1) => (X0 @ (epso @ X0)))),
% 5.17/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',choiceaxo)).
% 5.17/1.05 thf(f2,axiom,(
% 5.17/1.05 ! [X0 : (($o > $o) > $o)] : (? [X1 : ($o > $o)] : (X0 @ X1) => (X0 @ (epsoo @ X0)))),
% 5.17/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',choiceaxoo)).
% 5.17/1.05 thf(f3,axiom,(
% 5.17/1.05 (q @ (^[X0 : $o] : ($true)))),
% 5.17/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qkt)).
% 5.17/1.05 thf(f4,axiom,(
% 5.17/1.05 (q @ (^[X0 : $o] : ($false)))),
% 5.17/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qkf)).
% 5.17/1.05 thf(f5,axiom,(
% 5.17/1.05 (q @ (^[X0 : $o] : (X0)))),
% 5.17/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qid)).
% 5.17/1.05 thf(f6,conjecture,(
% 5.17/1.05 (q @ (epsoo @ epso))),
% 5.17/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c)).
% 5.17/1.05 thf(f7,negated_conjecture,(
% 5.17/1.05 ~(q @ (epsoo @ epso))),
% 5.17/1.05 inference(negated_conjecture,[status(cth)],[f6])).
% 5.17/1.05 thf(f8,plain,(
% 5.17/1.05 ! [X0 : (($o > $o) > $o)] : (? [X1 : ($o > $o)] : (X0 @ X1) => (X0 @ (epsoo @ X0)))),
% 5.17/1.05 inference(rectify,[],[f2])).
% 5.17/1.05 thf(f9,plain,(
% 5.17/1.05 ! [X0 : (($o > $o) > $o)] : (? [X1 : ($o > $o)] : (((X0 @ X1)) = $true) => (((X0 @ (epsoo @ X0))) = $true))),
% 5.17/1.05 inference(fool_elimination,[],[f8])).
% 5.17/1.05 thf(f10,plain,(
% 5.17/1.05 ! [X0 : ($o > $o)] : (? [X1 : $o] : (X0 @ X1) => (X0 @ (epso @ X0)))),
% 5.17/1.05 inference(rectify,[],[f1])).
% 5.17/1.05 thf(f11,plain,(
% 5.17/1.05 ! [X0 : ($o > $o)] : (? [X1 : $o] : (((X0 @ X1)) = $true) => (((X0 @ (epso @ X0))) = $true))),
% 5.17/1.05 inference(fool_elimination,[],[f10])).
% 5.17/1.05 thf(f12,plain,(
% 5.17/1.05 (q @ (^[X0 : $o] : (X0)))),
% 5.17/1.05 inference(rectify,[],[f5])).
% 5.17/1.05 thf(f13,plain,(
% 5.17/1.05 (((q @ (^[Y0 : $o]: (Y0)))) = $true)),
% 5.17/1.05 inference(fool_elimination,[],[f12])).
% 5.17/1.05 thf(f14,plain,(
% 5.17/1.05 ~(q @ (epsoo @ epso))),
% 5.17/1.05 inference(rectify,[],[f7])).
% 5.17/1.05 thf(f15,plain,(
% 5.17/1.05 ~ (((q @ (epsoo @ epso))) = $true)),
% 5.17/1.05 inference(fool_elimination,[],[f14])).
% 5.17/1.05 thf(f16,plain,(
% 5.17/1.05 (q @ (^[X0 : $o] : ($false)))),
% 5.17/1.05 inference(rectify,[],[f4])).
% 5.17/1.05 thf(f17,plain,(
% 5.17/1.05 ($true = ((q @ (^[Y0 : $o]: ($false)))))),
% 5.17/1.05 inference(fool_elimination,[],[f16])).
% 5.17/1.05 thf(f18,plain,(
% 5.17/1.05 (q @ (^[X0 : $o] : ($true)))),
% 5.17/1.05 inference(rectify,[],[f3])).
% 5.17/1.05 thf(f19,plain,(
% 5.17/1.05 (((q @ (^[Y0 : $o]: ($true)))) = $true)),
% 5.17/1.05 inference(fool_elimination,[],[f18])).
% 5.17/1.05 thf(f20,plain,(
% 5.17/1.05 (((q @ (epsoo @ epso))) != $true)),
% 5.17/1.05 inference(flattening,[],[f15])).
% 5.17/1.05 thf(f21,plain,(
% 5.17/1.05 ! [X0 : ($o > $o)] : ((((X0 @ (epso @ X0))) = $true) | ! [X1 : $o] : (((X0 @ X1)) != $true))),
% 5.17/1.05 inference(ennf_transformation,[],[f11])).
% 5.17/1.05 thf(f22,plain,(
% 5.17/1.05 ! [X0 : (($o > $o) > $o)] : ((((X0 @ (epsoo @ X0))) = $true) | ! [X1 : ($o > $o)] : (((X0 @ X1)) != $true))),
% 5.17/1.05 inference(ennf_transformation,[],[f9])).
% 5.17/1.05 thf(f23,plain,(
% 5.17/1.05 (((q @ (^[Y0 : $o]: (Y0)))) = $true)),
% 5.17/1.05 inference(cnf_transformation,[],[f13])).
% 5.17/1.05 thf(f24,plain,(
% 5.17/1.05 ( ! [X0 : (($o > $o) > $o),X1 : ($o > $o)] : ((((X0 @ (epsoo @ X0))) = $true) | (((X0 @ X1)) != $true)) )),
% 5.17/1.05 inference(cnf_transformation,[],[f22])).
% 5.17/1.05 thf(f25,plain,(
% 5.17/1.05 ( ! [X0 : ($o > $o),X1 : $o] : ((((X0 @ (epso @ X0))) = $true) | (((X0 @ X1)) != $true)) )),
% 5.17/1.05 inference(cnf_transformation,[],[f21])).
% 5.17/1.05 thf(f26,plain,(
% 5.17/1.05 (((q @ (^[Y0 : $o]: ($true)))) = $true)),
% 5.17/1.05 inference(cnf_transformation,[],[f19])).
% 5.17/1.05 thf(f27,plain,(
% 5.17/1.05 ($true = ((q @ (^[Y0 : $o]: ($false)))))),
% 5.17/1.05 inference(cnf_transformation,[],[f17])).
% 5.17/1.05 thf(f28,plain,(
% 5.17/1.05 (((q @ (epsoo @ epso))) != $true)),
% 5.17/1.05 inference(cnf_transformation,[],[f20])).
% 5.17/1.05 thf(f30,definition,(
% 5.17/1.05 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 5.17/1.05 introduced(theory,[fool_exhaustiveness_axiom])).
% 5.17/1.05 thf(f31,definition,(
% 5.17/1.05 (sF0 = ((epsoo @ epso)))),
% 5.17/1.05 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 5.17/1.05 thf(f32,plain,(
% 5.17/1.05 (((epsoo @ epso)) = sF0)),
% 5.17/1.05 inference(reorient_equations,[],[f31])).
% 5.17/1.05 thf(f33,definition,(
% 5.17/1.05 (sF1 = ((q @ sF0)))),
% 5.17/1.05 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 5.17/1.05 thf(f34,plain,(
% 5.17/1.05 (sF1 != $true)),
% 5.17/1.05 inference(definition_folding,[],[f28,f33,f32])).
% 5.17/1.05 thf(f35,plain,(
% 5.17/1.05 ($false = ((q @ sF0))) | (sF1 = $true)),
% 5.17/1.05 inference(iff_proxy_clausification,[],[f33])).
% 5.17/1.05 thf(f46,plain,(
% 5.17/1.05 ($false = ((q @ sF0)))),
% 5.17/1.05 inference(forward_subsumption_resolution,[],[f35,f34])).
% 5.17/1.05 thf(f106,plain,(
% 5.17/1.05 ( ! [X2 : $o,X3 : ($o > $o),X0 : ($o > $o),X1 : (($o > $o) > $o > $o)] : ((((X1 @ (epsoo @ (^[Y0 : $o > $o]: (epso @ (X1 @ Y0)))))) != X0) | ($true = ((X0 @ $true))) | ((((^[Y0 : $o > $o]: (epso @ (X1 @ Y0))) @ X3)) != $true) | (((X0 @ X2)) != $true)) )),
% 5.17/1.05 inference(constrained_superposition,[],[f25,f24])).
% 5.17/1.05 thf(f112,plain,(
% 5.17/1.05 ( ! [X2 : $o,X3 : ($o > $o),X0 : ($o > $o),X1 : (($o > $o) > $o > $o)] : (($true != ((epso @ (X1 @ X3)))) | (((X0 @ X2)) != $true) | ($true = ((X0 @ $true))) | (((X1 @ (epsoo @ (^[Y0 : $o > $o]: (epso @ (X1 @ Y0)))))) != X0)) )),
% 5.17/1.05 inference(beta-eta_normalization,[],[f106])).
% 5.17/1.05 thf(f128,plain,(
% 5.17/1.05 ($true = $false) | (sF0 != (^[Y0 : $o]: ($true)))),
% 5.17/1.05 inference(constrained_superposition,[],[f26,f46])).
% 5.17/1.05 thf(f130,plain,(
% 5.17/1.05 (sF0 != (^[Y0 : $o]: ($true)))),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f128])).
% 5.17/1.05 thf(f132,plain,(
% 5.17/1.05 (((sF0 @ sK3)) != (((^[Y0 : $o]: ($true)) @ sK3)))),
% 5.17/1.05 inference(negative_extensionality,[],[f130])).
% 5.17/1.05 thf(f134,plain,(
% 5.17/1.05 ($false = ((sF0 @ sK3))) | ($false = (((^[Y0 : $o]: ($true)) @ sK3)))),
% 5.17/1.05 inference(xor_proxy_clausification,[],[f132])).
% 5.17/1.05 thf(f135,plain,(
% 5.17/1.05 ($false = ((sF0 @ sK3))) | ($true = $false)),
% 5.17/1.05 inference(beta-eta_normalization,[],[f134])).
% 5.17/1.05 thf(f136,plain,(
% 5.17/1.05 ($false = ((sF0 @ sK3)))),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f135])).
% 5.17/1.05 thf(f138,plain,(
% 5.17/1.05 (sK3 = $false) | (((sF0 @ $true)) = $false)),
% 5.17/1.05 inference(constrained_superposition,[],[f136,f30])).
% 5.17/1.05 thf(f158,definition,(
% 5.17/1.05 spl2_3 <=> (((sF0 @ $true)) = $false)),
% 5.17/1.05 introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition])).
% 5.17/1.05 thf(f159,plain,(
% 5.17/1.05 (((sF0 @ $true)) != $false) | spl2_3),
% 5.17/1.05 inference(avatar_component_clause,[],[f158])).
% 5.17/1.05 thf(f160,plain,(
% 5.17/1.05 (((sF0 @ $true)) = $false) | ~spl2_3),
% 5.17/1.05 inference(avatar_component_clause,[],[f158])).
% 5.17/1.05 thf(f171,definition,(
% 5.17/1.05 spl2_5 <=> (sK3 = $false)),
% 5.17/1.05 introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition])).
% 5.17/1.05 thf(f173,plain,(
% 5.17/1.05 (sK3 = $false) | ~spl2_5),
% 5.17/1.05 inference(avatar_component_clause,[],[f171])).
% 5.17/1.05 thf(f174,plain,(
% 5.17/1.05 spl2_3 | spl2_5),
% 5.17/1.05 inference(avatar_split_clause,[],[f138,f171,f158])).
% 5.17/1.05 thf(f247,definition,(
% 5.17/1.05 spl2_7 <=> ! [X0 : $o] : ($false = X0)),
% 5.17/1.05 introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition])).
% 5.17/1.05 thf(f248,plain,(
% 5.17/1.05 ( ! [X0 : $o] : (($false = X0)) ) | ~spl2_7),
% 5.17/1.05 inference(avatar_component_clause,[],[f247])).
% 5.17/1.05 thf(f262,plain,(
% 5.17/1.05 ($false = ((sF0 @ $false))) | ~spl2_5),
% 5.17/1.05 inference(constrained_superposition,[],[f136,f173])).
% 5.17/1.05 thf(f276,plain,(
% 5.17/1.05 ( ! [X0 : $o] : ((((sF0 @ X0)) != $false) | ($false = X0)) ) | spl2_3),
% 5.17/1.05 inference(constrained_superposition,[],[f159,f30])).
% 5.17/1.05 thf(f330,definition,(
% 5.17/1.05 spl2_12 <=> ! [X3 : $o] : ($true != X3)),
% 5.17/1.05 introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition])).
% 5.17/1.05 thf(f331,plain,(
% 5.17/1.05 ( ! [X3 : $o] : (($true != X3)) ) | ~spl2_12),
% 5.17/1.05 inference(avatar_component_clause,[],[f330])).
% 5.17/1.05 thf(f356,plain,(
% 5.17/1.05 ($true = $false) | (sF0 != (^[Y0 : $o]: ($false)))),
% 5.17/1.05 inference(constrained_superposition,[],[f27,f46])).
% 5.17/1.05 thf(f358,plain,(
% 5.17/1.05 (sF0 != (^[Y0 : $o]: ($false)))),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f356])).
% 5.17/1.05 thf(f361,plain,(
% 5.17/1.05 (((sF0 @ sK4)) != (((^[Y0 : $o]: ($false)) @ sK4)))),
% 5.17/1.05 inference(negative_extensionality,[],[f358])).
% 5.17/1.05 thf(f363,plain,(
% 5.17/1.05 ($true = ((sF0 @ sK4))) | ($true = (((^[Y0 : $o]: ($false)) @ sK4)))),
% 5.17/1.05 inference(xor_proxy_clausification,[],[f361])).
% 5.17/1.05 thf(f366,plain,(
% 5.17/1.05 ($true = ((sF0 @ sK4))) | ($true = $false)),
% 5.17/1.05 inference(beta-eta_normalization,[],[f363])).
% 5.17/1.05 thf(f367,plain,(
% 5.17/1.05 ($true = ((sF0 @ sK4)))),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f366])).
% 5.17/1.05 thf(f404,plain,(
% 5.17/1.05 ( ! [X2 : $o,X3 : $o,X1 : ($o > $o)] : (((((^[Y0 : $o]: (Y0)) @ X3)) != $true) | ($true != $true) | ((((^[Y0 : $o > $o]: ((^[Y1 : $o]: (Y0 @ ((^[Y2 : $o > $o]: ((^[Y3 : $o]: (Y3)))) @ Y0 @ Y1))))) @ (epsoo @ (^[Y0 : $o > $o]: (epso @ ((^[Y1 : $o > $o]: ((^[Y2 : $o]: (Y1 @ ((^[Y3 : $o > $o]: ((^[Y4 : $o]: (Y4)))) @ Y1 @ Y2))))) @ Y0)))))) != X1) | ($true != ((X1 @ X2))) | ($true = ((X1 @ $true)))) )),
% 5.17/1.05 inference(constrained_superposition,[],[f112,f25])).
% 5.17/1.05 thf(f419,plain,(
% 5.17/1.05 ( ! [X2 : $o,X3 : $o,X1 : ($o > $o)] : (((((^[Y0 : $o > $o]: ((^[Y1 : $o]: (Y0 @ ((^[Y2 : $o > $o]: ((^[Y3 : $o]: (Y3)))) @ Y0 @ Y1))))) @ (epsoo @ (^[Y0 : $o > $o]: (epso @ ((^[Y1 : $o > $o]: ((^[Y2 : $o]: (Y1 @ ((^[Y3 : $o > $o]: ((^[Y4 : $o]: (Y4)))) @ Y1 @ Y2))))) @ Y0)))))) != X1) | ((((^[Y0 : $o]: (Y0)) @ X3)) != $true) | ($true != ((X1 @ X2))) | ($true = ((X1 @ $true)))) )),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f404])).
% 5.17/1.05 thf(f420,plain,(
% 5.17/1.05 ( ! [X2 : $o,X3 : $o,X1 : ($o > $o)] : ((((epsoo @ epso)) != X1) | ($true != X3) | ($true = ((X1 @ $true))) | ($true != ((X1 @ X2)))) )),
% 5.17/1.05 inference(beta-eta_normalization,[],[f419])).
% 5.17/1.05 thf(f439,plain,(
% 5.17/1.05 ( ! [X2 : $o,X3 : $o,X1 : ($o > $o)] : (($true != ((X1 @ X2))) | ($true = ((X1 @ $true))) | (sF0 != X1) | ($true != X3)) )),
% 5.17/1.05 inference(forward_demodulation,[],[f420,f32])).
% 5.17/1.05 thf(f461,definition,(
% 5.17/1.05 spl2_23 <=> ! [X2 : $o,X1 : ($o > $o)] : (($true != ((X1 @ X2))) | (sF0 != X1) | ($true = ((X1 @ $true))))),
% 5.17/1.05 introduced(definition,[new_symbols(definition,[spl2_23])],[avatar_definition])).
% 5.17/1.05 thf(f462,plain,(
% 5.17/1.05 ( ! [X2 : $o,X1 : ($o > $o)] : (($true = ((X1 @ $true))) | ($true != ((X1 @ X2))) | (sF0 != X1)) ) | ~spl2_23),
% 5.17/1.05 inference(avatar_component_clause,[],[f461])).
% 5.17/1.05 thf(f463,plain,(
% 5.17/1.05 spl2_23 | spl2_12),
% 5.17/1.05 inference(avatar_split_clause,[],[f439,f330,f461])).
% 5.17/1.05 thf(f468,plain,(
% 5.17/1.05 ( ! [X0 : $o,X1 : $o] : (($false = X0) | (X0 != X1)) ) | ~spl2_12),
% 5.17/1.05 inference(constrained_superposition,[],[f331,f30])).
% 5.17/1.05 thf(f472,plain,(
% 5.17/1.05 ( ! [X0 : $o,X1 : $o] : (($false = X0) | ($false = X0) | ($false = X1)) ) | ~spl2_12),
% 5.17/1.05 inference(xor_proxy_clausification,[],[f468])).
% 5.17/1.05 thf(f473,plain,(
% 5.17/1.05 ( ! [X0 : $o,X1 : $o] : (($false = X0) | ($false = X1)) ) | ~spl2_12),
% 5.17/1.05 inference(duplicate_literal_removal,[],[f472])).
% 5.17/1.05 thf(f474,plain,(
% 5.17/1.05 spl2_7 | spl2_7 | ~spl2_12),
% 5.17/1.05 inference(avatar_split_clause,[],[f473,f330,f247,f247])).
% 5.17/1.05 thf(f490,plain,(
% 5.17/1.05 (sF0 != (^[Y0 : $o]: (Y0))) | ($true = $false)),
% 5.17/1.05 inference(constrained_superposition,[],[f46,f23])).
% 5.17/1.05 thf(f491,plain,(
% 5.17/1.05 (sF0 != (^[Y0 : $o]: (Y0)))),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f490])).
% 5.17/1.05 thf(f501,plain,(
% 5.17/1.05 ((((^[Y0 : $o]: (Y0)) @ sK6)) != ((sF0 @ sK6)))),
% 5.17/1.05 inference(negative_extensionality,[],[f491])).
% 5.17/1.05 thf(f503,plain,(
% 5.17/1.05 ($true = ((sF0 @ sK6))) | ($true = (((^[Y0 : $o]: (Y0)) @ sK6)))),
% 5.17/1.05 inference(xor_proxy_clausification,[],[f501])).
% 5.17/1.05 thf(f504,plain,(
% 5.17/1.05 ($false = ((sF0 @ sK6))) | ($false = (((^[Y0 : $o]: (Y0)) @ sK6)))),
% 5.17/1.05 inference(xor_proxy_clausification,[],[f501])).
% 5.17/1.05 thf(f505,plain,(
% 5.17/1.05 (sK6 = $false) | ($false = ((sF0 @ sK6)))),
% 5.17/1.05 inference(beta-eta_normalization,[],[f504])).
% 5.17/1.05 thf(f506,plain,(
% 5.17/1.05 (sK6 = $true) | ($true = ((sF0 @ sK6)))),
% 5.17/1.05 inference(beta-eta_normalization,[],[f503])).
% 5.17/1.05 thf(f507,plain,(
% 5.17/1.05 (sK6 = $false) | spl2_3),
% 5.17/1.05 inference(forward_subsumption_resolution,[],[f505,f276])).
% 5.17/1.05 thf(f509,definition,(
% 5.17/1.05 spl2_24 <=> (sK6 = $true)),
% 5.17/1.05 introduced(definition,[new_symbols(definition,[spl2_24])],[avatar_definition])).
% 5.17/1.05 thf(f511,plain,(
% 5.17/1.05 (sK6 = $true) | ~spl2_24),
% 5.17/1.05 inference(avatar_component_clause,[],[f509])).
% 5.17/1.05 thf(f513,definition,(
% 5.17/1.05 spl2_25 <=> ($true = ((sF0 @ sK6)))),
% 5.17/1.05 introduced(definition,[new_symbols(definition,[spl2_25])],[avatar_definition])).
% 5.17/1.05 thf(f515,plain,(
% 5.17/1.05 ($true = ((sF0 @ sK6))) | ~spl2_25),
% 5.17/1.05 inference(avatar_component_clause,[],[f513])).
% 5.17/1.05 thf(f516,plain,(
% 5.17/1.05 spl2_24 | spl2_25),
% 5.17/1.05 inference(avatar_split_clause,[],[f506,f513,f509])).
% 5.17/1.05 thf(f518,plain,(
% 5.17/1.05 ($true = $false) | (spl2_3 | ~spl2_24)),
% 5.17/1.05 inference(forward_demodulation,[],[f511,f507])).
% 5.17/1.05 thf(f519,plain,(
% 5.17/1.05 $false | (spl2_3 | ~spl2_24)),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f518])).
% 5.17/1.05 thf(f520,plain,(
% 5.17/1.05 spl2_3 | ~spl2_24),
% 5.17/1.05 inference(avatar_contradiction_clause,[],[f519])).
% 5.17/1.05 thf(f526,plain,(
% 5.17/1.05 ( ! [X0 : ($o > $o),X1 : $o] : ((((X0 @ X1)) != $true) | ($true = ((X0 @ $false)))) ) | ~spl2_7),
% 5.17/1.05 inference(constrained_superposition,[],[f25,f248])).
% 5.17/1.05 thf(f565,plain,(
% 5.17/1.05 ( ! [X0 : ($o > $o),X1 : $o] : (($true = ((X0 @ $false))) | (((X0 @ X1)) != $false)) ) | ~spl2_7),
% 5.17/1.05 inference(forward_demodulation,[],[f526,f248])).
% 5.17/1.05 thf(f571,plain,(
% 5.17/1.05 ( ! [X0 : ($o > $o)] : (($true = ((X0 @ $false)))) ) | ~spl2_7),
% 5.17/1.05 inference(forward_subsumption_resolution,[],[f565,f248])).
% 5.17/1.05 thf(f576,plain,(
% 5.17/1.05 ($true = $false) | ~spl2_7),
% 5.17/1.05 inference(forward_demodulation,[],[f571,f248])).
% 5.17/1.05 thf(f577,plain,(
% 5.17/1.05 $false | ~spl2_7),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f576])).
% 5.17/1.05 thf(f578,plain,(
% 5.17/1.05 ~spl2_7),
% 5.17/1.05 inference(avatar_contradiction_clause,[],[f577])).
% 5.17/1.05 thf(f797,plain,(
% 5.17/1.05 ($true = ((sF0 @ $false))) | (spl2_3 | ~spl2_25)),
% 5.17/1.05 inference(constrained_superposition,[],[f515,f507])).
% 5.17/1.05 thf(f800,plain,(
% 5.17/1.05 ($true = $false) | (spl2_3 | ~spl2_5 | ~spl2_25)),
% 5.17/1.05 inference(forward_demodulation,[],[f797,f262])).
% 5.17/1.05 thf(f801,plain,(
% 5.17/1.05 $false | (spl2_3 | ~spl2_5 | ~spl2_25)),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f800])).
% 5.17/1.05 thf(f802,plain,(
% 5.17/1.05 spl2_3 | ~spl2_5 | ~spl2_25),
% 5.17/1.05 inference(avatar_contradiction_clause,[],[f801])).
% 5.17/1.05 thf(f979,plain,(
% 5.17/1.05 ( ! [X0 : $o] : (($true != (((^[Y0 : $o]: (sF0 @ ((^[Y1 : $o]: (Y1)) @ Y0))) @ X0))) | (sF0 != (^[Y0 : $o]: (sF0 @ ((^[Y1 : $o]: (Y1)) @ Y0)))) | ($true = $false)) ) | (~spl2_3 | ~spl2_23)),
% 5.17/1.05 inference(constrained_superposition,[],[f462,f160])).
% 5.17/1.05 thf(f986,plain,(
% 5.17/1.05 ( ! [X0 : $o] : ((sF0 != (^[Y0 : $o]: (sF0 @ ((^[Y1 : $o]: (Y1)) @ Y0)))) | ($true != (((^[Y0 : $o]: (sF0 @ ((^[Y1 : $o]: (Y1)) @ Y0))) @ X0)))) ) | (~spl2_3 | ~spl2_23)),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f979])).
% 5.17/1.05 thf(f987,plain,(
% 5.17/1.05 ( ! [X0 : $o] : ((sF0 != sF0) | (((sF0 @ X0)) != $true)) ) | (~spl2_3 | ~spl2_23)),
% 5.17/1.05 inference(beta-eta_normalization,[],[f986])).
% 5.17/1.05 thf(f988,plain,(
% 5.17/1.05 ( ! [X0 : $o] : ((((sF0 @ X0)) != $true)) ) | (~spl2_3 | ~spl2_23)),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f987])).
% 5.17/1.05 thf(f1026,plain,(
% 5.17/1.05 ($true != $true) | (~spl2_3 | ~spl2_23)),
% 5.17/1.05 inference(constrained_superposition,[],[f988,f367])).
% 5.17/1.05 thf(f1044,plain,(
% 5.17/1.05 $false | (~spl2_3 | ~spl2_23)),
% 5.17/1.05 inference(trivial_inequality_removal,[],[f1026])).
% 5.17/1.05 thf(f1045,plain,(
% 5.17/1.05 ~spl2_3 | ~spl2_23),
% 5.17/1.05 inference(avatar_contradiction_clause,[],[f1044])).
% 5.17/1.05 cnf(s4, plain, spl2_3 | spl2_5, inference(sat_conversion,[],[f174])).
% 5.17/1.05 cnf(s20, plain, spl2_12 | spl2_23, inference(sat_conversion,[],[f463])).
% 5.17/1.05 cnf(s24, plain, spl2_7 | spl2_7 | ~spl2_12, inference(sat_conversion,[],[f474])).
% 5.17/1.05 cnf(s25, plain, spl2_7 | ~spl2_12, inference(rat,[],[s24])).
% 5.17/1.05 cnf(s26, plain, spl2_24 | spl2_25, inference(sat_conversion,[],[f516])).
% 5.17/1.05 cnf(s27, plain, spl2_3 | ~spl2_24, inference(sat_conversion,[],[f520])).
% 5.17/1.05 cnf(s37, plain, ~spl2_7, inference(sat_conversion,[],[f578])).
% 5.17/1.05 cnf(s51, plain, spl2_3 | ~spl2_5 | ~spl2_25, inference(sat_conversion,[],[f802])).
% 5.17/1.05 cnf(s58, plain, ~spl2_3 | ~spl2_23, inference(sat_conversion,[],[f1045])).
% 5.17/1.05 cnf(s60, plain, ~spl2_12, inference(rat,[],[s25,s37])).
% 5.17/1.05 cnf(s62, plain, spl2_23, inference(rat,[],[s20,s60])).
% 5.17/1.05 cnf(s63, plain, ~spl2_3, inference(rat,[],[s58,s62])).
% 5.17/1.05 cnf(s64, plain, ~spl2_24, inference(rat,[],[s27,s63])).
% 5.17/1.05 cnf(s65, plain, spl2_25, inference(rat,[],[s26,s64])).
% 5.17/1.05 cnf(s66, plain, ~spl2_5, inference(rat,[],[s51,s63,s65])).
% 5.17/1.05 cnf(s71, plain, $false, inference(rat,[],[s4,s66,s63])).
% 5.17/1.05 thf(f1054,plain,(
% 5.17/1.05 $false),
% 5.17/1.05 inference(avatar_sat_refutation,[],[s71])).
% 5.17/1.05 % SZS output end Proof for theBenchmark
% 5.17/1.05 % (1099985)------------------------------
% 5.17/1.05 % (1099985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.05 % (1099985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.05 % (1099985)CaDiCaL version: 2.1.3
% 5.17/1.05 % (1099985)Termination reason: Refutation
% 5.17/1.05 % (1099985)Time elapsed: 0.046 s
% 5.17/1.05 % (1099985)Peak memory usage: 13 MB
% 5.17/1.05 % (1099985)Instructions burned: 83 (million)
% 5.17/1.05 % (1099840)Success in time 0.794 s
% 5.17/1.05 % Vampire exiting
%------------------------------------------------------------------------------