%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO219^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:47:13 AM UTC 2026
% Result : Theorem 1.33s 0.56s
% Output : Refutation 1.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SYO219^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.25 % Computer : n010.cluster.edu
% 0.13/0.25 % Model : x86_64 x86_64
% 0.13/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.25 % Memory : 8046.5625MB
% 0.13/0.25 % OS : Linux 6.8.0-71-generic
% 0.13/0.25 % CPULimit : 300
% 0.13/0.25 % WCLimit : 300
% 0.13/0.25 % DateTime : Tue Sep 29 16:40:03 UTC 2026
% 0.13/0.25 % CPUTime :
% 0.13/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.29/0.30 Running higher-order theorem proving
% 0.29/0.31 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.58/0.42 % (3110629)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.58/0.42 % (3110636)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=903396756:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.58/0.42 % (3110636)Refutation not found, incomplete strategy
% 0.58/0.42 % (3110636)------------------------------
% 0.58/0.42 % (3110636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.42 % (3110636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.42 % (3110636)CaDiCaL version: 2.1.3
% 0.58/0.42 % (3110636)Termination reason: Refutation not found, incomplete strategy
% 0.58/0.42 % (3110636)Time elapsed: 0.001 s
% 0.58/0.42 % (3110636)Peak memory usage: 12 MB
% 0.58/0.42 % (3110636)------------------------------
% 0.58/0.42 % (3110636)------------------------------
% 0.58/0.42 % (3110640)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.58/0.42 % (3110640)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.58/0.42 % (3110634)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3951327417:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.58/0.42 % (3110635)lrs+10_16_si=on:nwc=1.5:random_seed=3799944302:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.58/0.42 % (3110634)Refutation not found, incomplete strategy
% 0.58/0.42 % (3110634)------------------------------
% 0.58/0.42 % (3110634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.42 % (3110634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.42 % (3110634)CaDiCaL version: 2.1.3
% 0.58/0.42 % (3110634)Termination reason: Refutation not found, incomplete strategy
% 0.58/0.42 % (3110634)Time elapsed: 0.002 s
% 0.58/0.42 % (3110634)Peak memory usage: 12 MB
% 0.58/0.42 % (3110639)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=190622668:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.58/0.42 % (3110635)Refutation not found, incomplete strategy
% 0.58/0.42 % (3110635)------------------------------
% 0.58/0.42 % (3110635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.42 % (3110635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.42 % (3110635)CaDiCaL version: 2.1.3
% 0.58/0.42 % (3110635)Termination reason: Refutation not found, incomplete strategy
% 0.58/0.42 % (3110635)Time elapsed: 0.002 s
% 0.58/0.42 % (3110635)Peak memory usage: 12 MB
% 0.58/0.42 % (3110638)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1927919357:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.58/0.42 % (3110640)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=2143691386:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.58/0.42 % (3110637)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=1766395867: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.58/0.42 % (3110634)------------------------------
% 0.58/0.42 % (3110634)------------------------------
% 0.58/0.42 % (3110635)------------------------------
% 0.58/0.42 % (3110635)------------------------------
% 0.58/0.42 % (3110639)Refutation not found, incomplete strategy
% 0.58/0.42 % (3110639)------------------------------
% 0.58/0.42 % (3110639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.42 % (3110639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.42 % (3110639)CaDiCaL version: 2.1.3
% 0.58/0.42 % (3110639)Termination reason: Refutation not found, incomplete strategy
% 0.58/0.42 % (3110639)Time elapsed: 0.002 s
% 0.58/0.42 % (3110639)Peak memory usage: 12 MB
% 0.58/0.42 % (3110638)Refutation not found, incomplete strategy
% 0.58/0.42 % (3110638)------------------------------
% 0.58/0.42 % (3110638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.42 % (3110638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.44 % (3110638)CaDiCaL version: 2.1.3
% 0.58/0.44 % (3110638)Termination reason: Refutation not found, incomplete strategy
% 0.58/0.44 % (3110638)Time elapsed: 0.001 s
% 0.58/0.44 % (3110638)Peak memory usage: 12 MB
% 0.58/0.44 % (3110640)Refutation not found, incomplete strategy
% 0.58/0.44 % (3110640)------------------------------
% 0.58/0.44 % (3110640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.44 % (3110640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.44 % (3110637)Refutation not found, incomplete strategy
% 0.58/0.44 % (3110637)------------------------------
% 0.58/0.44 % (3110637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.44 % (3110640)CaDiCaL version: 2.1.3
% 0.58/0.44 % (3110640)Termination reason: Refutation not found, incomplete strategy
% 0.58/0.44 % (3110640)Time elapsed: 0.002 s
% 0.58/0.44 % (3110640)Peak memory usage: 12 MB
% 0.58/0.44 % (3110637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.44 % (3110640)Instructions burned: 1 (million)
% 0.58/0.44 % (3110637)CaDiCaL version: 2.1.3
% 0.58/0.44 % (3110637)Termination reason: Refutation not found, incomplete strategy
% 0.58/0.44 % (3110637)Time elapsed: 0.002 s
% 0.58/0.44 % (3110637)Peak memory usage: 12 MB
% 0.58/0.44 % (3110639)------------------------------
% 0.58/0.44 % (3110639)------------------------------
% 0.58/0.44 % (3110638)------------------------------
% 0.58/0.44 % (3110638)------------------------------
% 0.58/0.44 % (3110640)------------------------------
% 0.58/0.44 % (3110640)------------------------------
% 0.58/0.44 % (3110637)------------------------------
% 0.58/0.44 % (3110637)------------------------------
% 0.58/0.44 % (3110642)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=226835593:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.58/0.44 % (3110642)Instruction limit reached!
% 0.58/0.44 % (3110642)------------------------------
% 0.58/0.44 % (3110642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.44 % (3110642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.44 % (3110642)CaDiCaL version: 2.1.3
% 0.58/0.44 % (3110642)Termination reason: Instruction limit
% 0.58/0.44 % (3110642)Termination phase: Saturation
% 0.58/0.44 % (3110642)Time elapsed: 0.002 s
% 0.58/0.44 % (3110642)Peak memory usage: 12 MB
% 0.58/0.44 % (3110642)Instructions burned: 3 (million)
% 0.58/0.44 % (3110656)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.58/0.44 % (3110656)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=1332685227:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.58/0.44 % (3110652)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.58/0.44 % (3110652)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.58/0.44 % (3110656)Instruction limit reached!
% 0.58/0.44 % (3110656)------------------------------
% 0.58/0.44 % (3110656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.44 % (3110656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.44 % (3110656)CaDiCaL version: 2.1.3
% 0.58/0.44 % (3110656)Termination reason: Instruction limit
% 0.58/0.44 % (3110656)Time elapsed: 0.002 s
% 0.58/0.44 % (3110656)Peak memory usage: 12 MB
% 0.58/0.44 % (3110650)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.58/0.44 % (3110656)Instructions burned: 2 (million)
% 0.58/0.44 % (3110649)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2951995783:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.58/0.44 % (3110651)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=58077445:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.58/0.44 % (3110652)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=4221411627: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.58/0.48 % (3110653)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=3569470490:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.58/0.48 % (3110650)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2827908429:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.58/0.48 % (3110651)Refutation not found, incomplete strategy
% 0.58/0.48 % (3110651)------------------------------
% 0.58/0.48 % (3110651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.48 % (3110651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.48 % (3110651)CaDiCaL version: 2.1.3
% 0.58/0.48 % (3110651)Termination reason: Refutation not found, incomplete strategy
% 0.58/0.48 % (3110651)Time elapsed: 0.002 s
% 0.58/0.48 % (3110651)Peak memory usage: 12 MB
% 0.58/0.48 % (3110651)------------------------------
% 0.58/0.48 % (3110651)------------------------------
% 0.58/0.48 % (3110649)Instruction limit reached!
% 0.58/0.48 % (3110649)------------------------------
% 0.58/0.48 % (3110649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.48 % (3110649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.48 % (3110649)CaDiCaL version: 2.1.3
% 0.58/0.48 % (3110649)Termination reason: Instruction limit
% 0.58/0.48 % (3110649)Termination phase: Saturation
% 0.58/0.48 % (3110649)Time elapsed: 0.006 s
% 0.58/0.48 % (3110649)Peak memory usage: 12 MB
% 0.58/0.48 % (3110649)Instructions burned: 5 (million)
% 0.58/0.48 % (3110652)Refutation not found, incomplete strategy
% 0.58/0.48 % (3110652)------------------------------
% 0.58/0.48 % (3110652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.48 % (3110652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.48 % (3110653)Refutation not found, incomplete strategy
% 0.58/0.48 % (3110653)------------------------------
% 0.58/0.48 % (3110653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.48 % (3110652)CaDiCaL version: 2.1.3
% 0.58/0.48 % (3110653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.48 % (3110652)Termination reason: Refutation not found, incomplete strategy
% 0.58/0.48 % (3110652)Time elapsed: 0.004 s
% 0.58/0.48 % (3110652)Peak memory usage: 12 MB
% 0.58/0.48 % (3110653)CaDiCaL version: 2.1.3
% 0.58/0.48 % (3110652)Instructions burned: 3 (million)
% 0.58/0.48 % (3110653)Termination reason: Refutation not found, incomplete strategy
% 0.58/0.48 % (3110653)Time elapsed: 0.004 s
% 0.58/0.48 % (3110653)Peak memory usage: 12 MB
% 0.58/0.48 % (3110653)Instructions burned: 3 (million)
% 0.58/0.48 % (3110655)lrs+10_1_si=on:cs=on:random_seed=1685032054:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.58/0.48 % (3110652)------------------------------
% 0.58/0.48 % (3110652)------------------------------
% 0.58/0.48 % (3110653)------------------------------
% 0.58/0.48 % (3110653)------------------------------
% 0.58/0.48 % (3110655)Refutation not found, incomplete strategy
% 0.58/0.48 % (3110655)------------------------------
% 0.58/0.48 % (3110655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.48 % (3110655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.48 % (3110655)CaDiCaL version: 2.1.3
% 0.58/0.48 % (3110655)Termination reason: Refutation not found, incomplete strategy
% 0.58/0.48 % (3110655)Time elapsed: 0.001 s
% 0.58/0.48 % (3110655)Peak memory usage: 12 MB
% 0.58/0.48 % (3110650)Instruction limit reached!
% 0.58/0.48 % (3110650)------------------------------
% 0.58/0.48 % (3110650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.48 % (3110650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.48 % (3110650)CaDiCaL version: 2.1.3
% 0.58/0.48 % (3110650)Termination reason: Instruction limit
% 0.58/0.48 % (3110650)Termination phase: Saturation
% 0.58/0.48 % (3110650)Time elapsed: 0.008 s
% 0.58/0.48 % (3110650)Peak memory usage: 12 MB
% 0.58/0.48 % (3110650)Instructions burned: 7 (million)
% 0.58/0.48 % (3110655)------------------------------
% 0.58/0.48 % (3110655)------------------------------
% 0.58/0.48 % (3110658)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=210090329:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 1.33/0.49 % (3110658)Refutation not found, incomplete strategy
% 1.33/0.49 % (3110658)------------------------------
% 1.33/0.49 % (3110658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.49 % (3110658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.49 % (3110658)CaDiCaL version: 2.1.3
% 1.33/0.49 % (3110658)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.49 % (3110658)Time elapsed: 0.001 s
% 1.33/0.49 % (3110658)Peak memory usage: 12 MB
% 1.33/0.49 % (3110658)------------------------------
% 1.33/0.49 % (3110658)------------------------------
% 1.33/0.49 % (3110664)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2882546908:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 1.33/0.49 % (3110664)Refutation not found, incomplete strategy
% 1.33/0.49 % (3110664)------------------------------
% 1.33/0.49 % (3110664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.49 % (3110664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.49 % (3110664)CaDiCaL version: 2.1.3
% 1.33/0.49 % (3110664)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.49 % (3110664)Time elapsed: 0.001 s
% 1.33/0.49 % (3110664)Peak memory usage: 12 MB
% 1.33/0.49 % (3110664)------------------------------
% 1.33/0.49 % (3110664)------------------------------
% 1.33/0.49 % (3110665)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3079364342:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 1.33/0.49 % (3110665)Refutation not found, incomplete strategy
% 1.33/0.49 % (3110665)------------------------------
% 1.33/0.49 % (3110665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.49 % (3110667)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=565190248:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 1.33/0.49 % (3110665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.49 % (3110665)CaDiCaL version: 2.1.3
% 1.33/0.49 % (3110665)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.49 % (3110665)Time elapsed: 0.002 s
% 1.33/0.49 % (3110665)Peak memory usage: 12 MB
% 1.33/0.49 % (3110668)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=526002572:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 1.33/0.49 % (3110665)------------------------------
% 1.33/0.49 % (3110665)------------------------------
% 1.33/0.49 % (3110667)Refutation not found, incomplete strategy
% 1.33/0.49 % (3110667)------------------------------
% 1.33/0.49 % (3110667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.49 % (3110668)Refutation not found, incomplete strategy
% 1.33/0.49 % (3110668)------------------------------
% 1.33/0.49 % (3110668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.49 % (3110668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.49 % (3110667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.49 % (3110668)CaDiCaL version: 2.1.3
% 1.33/0.49 % (3110668)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.49 % (3110668)Time elapsed: 0.001 s
% 1.33/0.49 % (3110667)CaDiCaL version: 2.1.3
% 1.33/0.49 % (3110668)Peak memory usage: 12 MB
% 1.33/0.49 % (3110667)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.49 % (3110667)Time elapsed: 0.002 s
% 1.33/0.49 % (3110667)Peak memory usage: 12 MB
% 1.33/0.49 % (3110669)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=822049873:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 1.33/0.49 % (3110670)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1462616847:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.33/0.49 % (3110667)------------------------------
% 1.33/0.49 % (3110667)------------------------------
% 1.33/0.49 % (3110668)------------------------------
% 1.33/0.49 % (3110668)------------------------------
% 1.33/0.49 % (3110669)Refutation not found, incomplete strategy
% 1.33/0.49 % (3110669)------------------------------
% 1.33/0.49 % (3110669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.49 % (3110669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.52 % (3110669)CaDiCaL version: 2.1.3
% 1.33/0.52 % (3110669)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.52 % (3110669)Time elapsed: 0.001 s
% 1.33/0.52 % (3110669)Peak memory usage: 12 MB
% 1.33/0.52 % (3110674)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=699401923:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/23Mi)
% 1.33/0.52 % (3110670)Refutation not found, incomplete strategy
% 1.33/0.52 % (3110670)------------------------------
% 1.33/0.52 % (3110670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.52 % (3110670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.52 % (3110670)CaDiCaL version: 2.1.3
% 1.33/0.52 % (3110670)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.52 % (3110670)Time elapsed: 0.001 s
% 1.33/0.52 % (3110670)Peak memory usage: 12 MB
% 1.33/0.52 % (3110669)------------------------------
% 1.33/0.52 % (3110669)------------------------------
% 1.33/0.52 % (3110674)Refutation not found, incomplete strategy
% 1.33/0.52 % (3110674)------------------------------
% 1.33/0.52 % (3110674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.52 % (3110674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.52 % (3110670)------------------------------
% 1.33/0.52 % (3110670)------------------------------
% 1.33/0.52 % (3110674)CaDiCaL version: 2.1.3
% 1.33/0.52 % (3110674)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.52 % (3110674)Time elapsed: 0.001 s
% 1.33/0.52 % (3110674)Peak memory usage: 12 MB
% 1.33/0.52 % (3110674)------------------------------
% 1.33/0.52 % (3110674)------------------------------
% 1.33/0.52 % (3110672)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1634221404:i=26:ep=R:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/26Mi)
% 1.33/0.52 % (3110672)Refutation not found, incomplete strategy
% 1.33/0.52 % (3110672)------------------------------
% 1.33/0.52 % (3110672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.52 % (3110672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.52 % (3110672)CaDiCaL version: 2.1.3
% 1.33/0.52 % (3110672)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.52 % (3110672)Time elapsed: 0.003 s
% 1.33/0.52 % (3110672)Peak memory usage: 12 MB
% 1.33/0.52 % (3110672)Instructions burned: 2 (million)
% 1.33/0.52 % (3110672)------------------------------
% 1.33/0.52 % (3110672)------------------------------
% 1.33/0.52 % (3110679)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3608024855:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.33/0.52 % (3110679)Refutation not found, incomplete strategy
% 1.33/0.52 % (3110679)------------------------------
% 1.33/0.52 % (3110679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.52 % (3110679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.52 % (3110679)CaDiCaL version: 2.1.3
% 1.33/0.52 % (3110679)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.52 % (3110679)Time elapsed: 0.001 s
% 1.33/0.52 % (3110679)Peak memory usage: 12 MB
% 1.33/0.52 % (3110679)------------------------------
% 1.33/0.52 % (3110679)------------------------------
% 1.33/0.52 % (3110682)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.33/0.52 % (3110682)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.33/0.52 % (3110683)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.33/0.52 % (3110685)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=4014203116:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.33/0.52 % (3110684)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=818514125:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.33/0.52 % (3110682)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=2848729589:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.33/0.55 % (3110686)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=905992313:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.33/0.55 % (3110685)Refutation not found, incomplete strategy
% 1.33/0.55 % (3110685)------------------------------
% 1.33/0.55 % (3110685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.55 % (3110685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.55 % (3110685)CaDiCaL version: 2.1.3
% 1.33/0.55 % (3110685)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.55 % (3110685)Time elapsed: 0.002 s
% 1.33/0.55 % (3110685)Peak memory usage: 12 MB
% 1.33/0.55 % (3110683)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=2960758462:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.33/0.55 % (3110685)------------------------------
% 1.33/0.55 % (3110685)------------------------------
% 1.33/0.55 % (3110684)Refutation not found, incomplete strategy
% 1.33/0.55 % (3110684)------------------------------
% 1.33/0.55 % (3110684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.55 % (3110690)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1181448729:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.33/0.55 % (3110684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.55 % (3110684)CaDiCaL version: 2.1.3
% 1.33/0.55 % (3110684)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.55 % (3110684)Time elapsed: 0.004 s
% 1.33/0.55 % (3110684)Peak memory usage: 12 MB
% 1.33/0.55 % (3110684)Instructions burned: 3 (million)
% 1.33/0.55 % (3110683)Refutation not found, incomplete strategy
% 1.33/0.55 % (3110683)------------------------------
% 1.33/0.55 % (3110683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.55 % (3110683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.55 % (3110683)CaDiCaL version: 2.1.3
% 1.33/0.55 % (3110683)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.55 % (3110683)Time elapsed: 0.002 s
% 1.33/0.55 % (3110683)Peak memory usage: 12 MB
% 1.33/0.55 % (3110683)Instructions burned: 1 (million)
% 1.33/0.55 % (3110684)------------------------------
% 1.33/0.55 % (3110684)------------------------------
% 1.33/0.55 % (3110690)Refutation not found, incomplete strategy
% 1.33/0.55 % (3110690)------------------------------
% 1.33/0.55 % (3110690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.55 % (3110690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.55 % (3110690)CaDiCaL version: 2.1.3
% 1.33/0.55 % (3110690)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.55 % (3110690)Time elapsed: 0.002 s
% 1.33/0.55 % (3110690)Peak memory usage: 11 MB
% 1.33/0.55 % (3110682)Refutation not found, incomplete strategy
% 1.33/0.55 % (3110682)------------------------------
% 1.33/0.55 % (3110682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.55 % (3110690)Instructions burned: 2 (million)
% 1.33/0.55 % (3110682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.55 % (3110682)CaDiCaL version: 2.1.3
% 1.33/0.55 % (3110683)------------------------------
% 1.33/0.55 % (3110683)------------------------------
% 1.33/0.55 % (3110682)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.55 % (3110682)Time elapsed: 0.005 s
% 1.33/0.55 % (3110682)Peak memory usage: 11 MB
% 1.33/0.55 % (3110682)Instructions burned: 3 (million)
% 1.33/0.55 % (3110690)------------------------------
% 1.33/0.55 % (3110690)------------------------------
% 1.33/0.55 % (3110682)------------------------------
% 1.33/0.55 % (3110682)------------------------------
% 1.33/0.55 % (3110688)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3488321558:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.33/0.55 % (3110688)Refutation not found, incomplete strategy
% 1.33/0.55 % (3110688)------------------------------
% 1.33/0.55 % (3110688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.55 % (3110688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.56 % (3110688)CaDiCaL version: 2.1.3
% 1.33/0.56 % (3110688)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.56 % (3110688)Time elapsed: 0.001 s
% 1.33/0.56 % (3110688)Peak memory usage: 12 MB
% 1.33/0.56 % (3110688)------------------------------
% 1.33/0.56 % (3110688)------------------------------
% 1.33/0.56 % (3110686)Instruction limit reached!
% 1.33/0.56 % (3110686)------------------------------
% 1.33/0.56 % (3110686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.56 % (3110686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.56 % (3110686)CaDiCaL version: 2.1.3
% 1.33/0.56 % (3110686)Termination reason: Instruction limit
% 1.33/0.56 % (3110686)Termination phase: Saturation
% 1.33/0.56 % (3110686)Time elapsed: 0.018 s
% 1.33/0.56 % (3110686)Peak memory usage: 11 MB
% 1.33/0.56 % (3110686)Instructions burned: 23 (million)
% 1.33/0.56 % (3110702)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3568818667:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/181Mi)
% 1.33/0.56 % (3110702)Refutation not found, incomplete strategy
% 1.33/0.56 % (3110702)------------------------------
% 1.33/0.56 % (3110702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.56 % (3110702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.56 % (3110702)CaDiCaL version: 2.1.3
% 1.33/0.56 % (3110702)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.56 % (3110702)Time elapsed: 0.001 s
% 1.33/0.56 % (3110702)Peak memory usage: 12 MB
% 1.33/0.56 % (3110701)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.33/0.56 % (3110702)------------------------------
% 1.33/0.56 % (3110702)------------------------------
% 1.33/0.56 % (3110701)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=376047590:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.33/0.56 % (3110697)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1064863502:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.33/0.56 % (3110697)Refutation not found, incomplete strategy
% 1.33/0.56 % (3110697)------------------------------
% 1.33/0.56 % (3110697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.56 % (3110697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.56 % (3110697)CaDiCaL version: 2.1.3
% 1.33/0.56 % (3110697)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.56 % (3110697)Time elapsed: 0.001 s
% 1.33/0.56 % (3110697)Peak memory usage: 12 MB
% 1.33/0.56 % (3110698)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3230801290:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.33/0.56 % (3110697)------------------------------
% 1.33/0.56 % (3110697)------------------------------
% 1.33/0.56 % (3110701)Instruction limit reached!
% 1.33/0.56 % (3110701)------------------------------
% 1.33/0.56 % (3110701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.56 % (3110701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.56 % (3110701)CaDiCaL version: 2.1.3
% 1.33/0.56 % (3110701)Termination reason: Instruction limit
% 1.33/0.56 % (3110701)Termination phase: Saturation
% 1.33/0.56 % (3110701)Time elapsed: 0.005 s
% 1.33/0.56 % (3110701)Peak memory usage: 12 MB
% 1.33/0.56 % (3110701)Instructions burned: 8 (million)
% 1.33/0.56 % (3110698)Refutation not found, incomplete strategy
% 1.33/0.56 % (3110698)------------------------------
% 1.33/0.56 % (3110698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.56 % (3110698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.56 % (3110698)CaDiCaL version: 2.1.3
% 1.33/0.56 % (3110698)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.56 % (3110698)Time elapsed: 0.001 s
% 1.33/0.56 % (3110698)Peak memory usage: 12 MB
% 1.33/0.56 % (3110698)------------------------------
% 1.33/0.56 % (3110698)------------------------------
% 1.33/0.56 % (3110700)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3061424445:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.33/0.56 % (3110703)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=1675650278:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/169Mi)
% 1.33/0.56 % (3110704)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.33/0.56 % (3110703)Refutation not found, incomplete strategy
% 1.33/0.56 % (3110703)------------------------------
% 1.33/0.56 % (3110703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.56 % (3110703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.56 % (3110703)CaDiCaL version: 2.1.3
% 1.33/0.56 % (3110703)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.56 % (3110703)Time elapsed: 0.001 s
% 1.33/0.56 % (3110703)Peak memory usage: 12 MB
% 1.33/0.56 % (3110703)------------------------------
% 1.33/0.56 % (3110703)------------------------------
% 1.33/0.56 % (3110704)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3681611501:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2998 on theBenchmark for (2998ds/6Mi)
% 1.33/0.56 % (3110711)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=257887943:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/316Mi)
% 1.33/0.56 % (3110704)Instruction limit reached!
% 1.33/0.56 % (3110704)------------------------------
% 1.33/0.56 % (3110704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.56 % (3110704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.56 % (3110704)CaDiCaL version: 2.1.3
% 1.33/0.56 % (3110704)Termination reason: Instruction limit
% 1.33/0.56 % (3110704)Termination phase: Saturation
% 1.33/0.56 % (3110704)Time elapsed: 0.007 s
% 1.33/0.56 % (3110704)Peak memory usage: 12 MB
% 1.33/0.56 % (3110704)Instructions burned: 6 (million)
% 1.33/0.56 % (3110711)Refutation not found, incomplete strategy
% 1.33/0.56 % (3110711)------------------------------
% 1.33/0.56 % (3110711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.56 % (3110711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.56 % (3110711)CaDiCaL version: 2.1.3
% 1.33/0.56 % (3110711)Termination reason: Refutation not found, incomplete strategy
% 1.33/0.56 % (3110711)Time elapsed: 0.003 s
% 1.33/0.56 % (3110711)Peak memory usage: 12 MB
% 1.33/0.56 % (3110711)Instructions burned: 4 (million)
% 1.33/0.56 % (3110711)------------------------------
% 1.33/0.56 % (3110711)------------------------------
% 1.33/0.56 % (3110706)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=365425033:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2998 on theBenchmark for (2998ds/22Mi)
% 1.33/0.56 % (3110700) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3110629-3110700"...
% 1.33/0.56 % (3110710)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=537289295:i=19:add=on:rtra=on_2998 on theBenchmark for (2998ds/19Mi)
% 1.33/0.56 % (3110700)...printing done.
% 1.33/0.56 % (3110713)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=2850954818:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2998 on theBenchmark for (2998ds/853Mi)
% 1.33/0.56 % (3110715)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=637742092:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2998 on theBenchmark for (2998ds/45Mi)
% 1.33/0.56 % (3110700)Refutation found. Thanks to Tanya!
% 1.33/0.56 % SZS status Theorem for theBenchmark
% 1.33/0.56 % SZS output start Proof for theBenchmark
% 1.33/0.56 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.33/0.56 thf(func_def_0, type, cS: ($i > $i)).
% 1.33/0.56 thf(func_def_2, type, sK0: ($i > $i > $i)).
% 1.33/0.56 thf(func_def_3, type, sK1: (($i > $i) > $i)).
% 1.33/0.56 thf(func_def_4, type, db0: !>[X0: $tType]:(X0)).
% 1.33/0.56 thf(func_def_5, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.33/0.56 thf(func_def_6, type, db1: !>[X0: $tType]:(X0)).
% 1.33/0.56 thf(func_def_7, type, sK2: (($i > $i) > $i)).
% 1.33/0.56 thf(func_def_8, type, db2: !>[X0: $tType]:(X0)).
% 1.33/0.56 thf(func_def_9, type, db3: !>[X0: $tType]:(X0)).
% 1.33/0.56 thf(func_def_10, type, db4: !>[X0: $tType]:(X0)).
% 1.33/0.56 thf(func_def_11, type, db5: !>[X0: $tType]:(X0)).
% 1.33/0.56 thf(f1,conjecture,(
% 1.33/0.56 ! [X0 : $i] : (((cS @ X0)) != X0) => ~ ? [X1 : ($i > $i > $i)] : ! [X2 : ($i > $i)] : ? [X3 : $i] : (((X1 @ X3)) = X2)),
% 1.33/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM6)).
% 1.33/0.56 thf(f2,negated_conjecture,(
% 1.33/0.56 ~(! [X0 : $i] : (((cS @ X0)) != X0) => ~ ? [X1 : ($i > $i > $i)] : ! [X2 : ($i > $i)] : ? [X3 : $i] : (((X1 @ X3)) = X2))),
% 1.33/0.56 inference(negated_conjecture,[status(cth)],[f1])).
% 1.33/0.56 thf(f3,plain,(
% 1.33/0.56 ? [X1 : ($i > $i > $i)] : ! [X2 : ($i > $i)] : ? [X3 : $i] : (((X1 @ X3)) = X2) & ! [X0 : $i] : (((cS @ X0)) != X0)),
% 1.33/0.56 inference(ennf_transformation,[],[f2])).
% 1.33/0.56 thf(f4,plain,(
% 1.33/0.56 ? [X0 : ($i > $i > $i)] : ! [X1 : ($i > $i)] : ? [X2 : $i] : (((X0 @ X2)) = X1) & ! [X3 : $i] : (((cS @ X3)) != X3)),
% 1.33/0.56 inference(rectify,[],[f3])).
% 1.33/0.56 thf(f5,plain,(
% 1.33/0.56 ! [X1 : ($i > $i)] : (((sK0 @ (sK1 @ X1))) = X1) & ! [X3 : $i] : (((cS @ X3)) != X3)),
% 1.33/0.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,vAPP]),skolemize(X0,sK0),skolemize(X2,sK1 @ X1)],[f4])).
% 1.33/0.56 thf(f6,plain,(
% 1.33/0.56 ( ! [X3 : $i] : ((((cS @ X3)) != X3)) )),
% 1.33/0.56 inference(cnf_transformation,[],[f5])).
% 1.33/0.56 thf(f7,plain,(
% 1.33/0.56 ( ! [X1 : ($i > $i)] : ((((sK0 @ (sK1 @ X1))) = X1)) )),
% 1.33/0.56 inference(cnf_transformation,[],[f5])).
% 1.33/0.56 thf(f9,plain,(
% 1.33/0.56 ( ! [X2 : $i,X1 : ($i > $i)] : ((((sK0 @ (sK1 @ X1) @ X2)) = ((X1 @ X2)))) )),
% 1.33/0.56 inference(argument_congruence,[],[f7])).
% 1.33/0.56 thf(f11,plain,(
% 1.33/0.56 ( ! [X2 : ($i > $i),X3 : $i,X0 : ($i > $i),X1 : $i] : ((((X0 @ X1)) = ((X2 @ X3))) | (X0 != X2) | (X1 != X3)) )),
% 1.33/0.56 inference(constrained_superposition,[],[f9,f9])).
% 1.33/0.56 thf(f16,plain,(
% 1.33/0.56 ( ! [X0 : $i] : ((((sK0 @ (sK1 @ cS) @ X0)) != X0)) )),
% 1.33/0.56 inference(unit_resulting_resolution,[],[f11,f7,f6])).
% 1.33/0.56 thf(f63,plain,(
% 1.33/0.56 ( ! [X0 : $i,X1 : $i] : ((X0 != X1) | ((((^[Y0 : $i]: (cS @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0)) != X1)) )),
% 1.33/0.56 inference(constrained_superposition,[],[f16,f9])).
% 1.33/0.56 thf(f75,plain,(
% 1.33/0.56 ( ! [X0 : $i,X1 : $i] : ((((cS @ X0)) != X1) | (X0 != X1)) )),
% 1.33/0.56 inference(beta-eta_normalization,[],[f63])).
% 1.33/0.56 thf(f81,plain,(
% 1.33/0.56 ( ! [X0 : ($i > $i),X1 : $i] : ((((X0 @ X1)) != ((cS @ (sK0 @ (sK1 @ X0) @ X1))))) )),
% 1.33/0.56 inference(unit_resulting_resolution,[],[f75,f9])).
% 1.33/0.56 thf(f176,plain,(
% 1.33/0.56 $false),
% 1.33/0.56 inference(equality_resolution,[],[f81])).
% 1.33/0.56 % SZS output end Proof for theBenchmark
% 1.33/0.56 % (3110700)------------------------------
% 1.33/0.56 % (3110700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.33/0.56 % (3110700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.33/0.56 % (3110700)CaDiCaL version: 2.1.3
% 1.33/0.56 % (3110700)Termination reason: Refutation
% 1.33/0.56 % (3110700)Time elapsed: 0.027 s
% 1.33/0.56 % (3110700)Peak memory usage: 12 MB
% 1.33/0.56 % (3110700)Instructions burned: 29 (million)
% 1.33/0.56 % (3110629)Success in time 0.225 s
% 1.33/0.56 % Vampire exiting
%------------------------------------------------------------------------------