%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO556^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 : n017.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 0.21s 0.36s
% Output : Refutation 0.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO556^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 : n017.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:10:07 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.21/0.35 % (625593)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.35 % (625607)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=967682184: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.21/0.35 % (625611)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.35 % (625611)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.21/0.35 % (625607)Refutation not found, incomplete strategy
% 0.21/0.35 % (625607)------------------------------
% 0.21/0.35 % (625607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (625607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (625607)CaDiCaL version: 2.1.3
% 0.21/0.35 % (625607)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.35 % (625607)Time elapsed: 0.004 s
% 0.21/0.35 % (625607)Peak memory usage: 12 MB
% 0.21/0.35 % (625607)Instructions burned: 8 (million)
% 0.21/0.35 % (625607)------------------------------
% 0.21/0.35 % (625607)------------------------------
% 0.21/0.35 % (625604)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3065608830:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.35 % (625605)lrs+10_16_si=on:nwc=1.5:random_seed=2767115883:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.35 % (625610)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=112834845:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.35 % (625609)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1459031372:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.35 % (625611)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=3732769043:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.35 % (625606)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3587882243:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.35 % (625604)Refutation not found, incomplete strategy
% 0.21/0.35 % (625604)------------------------------
% 0.21/0.35 % (625604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (625604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (625604)CaDiCaL version: 2.1.3
% 0.21/0.35 % (625604)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.35 % (625604)Time elapsed: 0.003 s
% 0.21/0.35 % (625604)Peak memory usage: 12 MB
% 0.21/0.35 % (625604)Instructions burned: 4 (million)
% 0.21/0.35 % (625604)------------------------------
% 0.21/0.35 % (625604)------------------------------
% 0.21/0.35 % (625606)Refutation not found, incomplete strategy
% 0.21/0.35 % (625606)------------------------------
% 0.21/0.35 % (625606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (625606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (625606)CaDiCaL version: 2.1.3
% 0.21/0.35 % (625606)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.35 % (625606)Time elapsed: 0.003 s
% 0.21/0.35 % (625606)Peak memory usage: 12 MB
% 0.21/0.35 % (625606)Instructions burned: 2 (million)
% 0.21/0.35 % (625611)Refutation not found, incomplete strategy
% 0.21/0.35 % (625611)------------------------------
% 0.21/0.35 % (625611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (625611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (625611)CaDiCaL version: 2.1.3
% 0.21/0.35 % (625611)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.35 % (625611)Time elapsed: 0.004 s
% 0.21/0.35 % (625611)Peak memory usage: 12 MB
% 0.21/0.35 % (625611)Instructions burned: 4 (million)
% 0.21/0.35 % (625611)------------------------------
% 0.21/0.35 % (625611)------------------------------
% 0.21/0.35 % (625606)------------------------------
% 0.21/0.35 % (625606)------------------------------
% 0.21/0.35 % (625609)Refutation not found, incomplete strategy
% 0.21/0.36 % (625609)------------------------------
% 0.21/0.36 % (625609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625609)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625609)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.36 % (625609)Time elapsed: 0.006 s
% 0.21/0.36 % (625609)Peak memory usage: 12 MB
% 0.21/0.36 % (625609)Instructions burned: 8 (million)
% 0.21/0.36 % (625609)------------------------------
% 0.21/0.36 % (625609)------------------------------
% 0.21/0.36 % (625615)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2615011630:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.36 % (625615)Instruction limit reached!
% 0.21/0.36 % (625615)------------------------------
% 0.21/0.36 % (625615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625615)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625615)Termination reason: Instruction limit
% 0.21/0.36 % (625615)Termination phase: Saturation
% 0.21/0.36 % (625615)Time elapsed: 0.001 s
% 0.21/0.36 % (625615)Peak memory usage: 12 MB
% 0.21/0.36 % (625615)Instructions burned: 2 (million)
% 0.21/0.36 % (625605)Instruction limit reached!
% 0.21/0.36 % (625605)------------------------------
% 0.21/0.36 % (625605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625605)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625605)Termination reason: Instruction limit
% 0.21/0.36 % (625605)Termination phase: Saturation
% 0.21/0.36 % (625605)Time elapsed: 0.011 s
% 0.21/0.36 % (625605)Peak memory usage: 12 MB
% 0.21/0.36 % (625605)Instructions burned: 18 (million)
% 0.21/0.36 % (625623)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.36 % (625627)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=130240397:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.21/0.36 % (625625)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.21/0.36 % (625625)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.36 % (625622)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3259806735:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.21/0.36 % (625624)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3275617272:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.21/0.36 % (625623)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2684064317:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.21/0.36 % (625625)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1773099865: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.21/0.36 % (625622)Instruction limit reached!
% 0.21/0.36 % (625622)------------------------------
% 0.21/0.36 % (625622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625622)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625622)Termination reason: Instruction limit
% 0.21/0.36 % (625622)Termination phase: Saturation
% 0.21/0.36 % (625622)Time elapsed: 0.004 s
% 0.21/0.36 % (625622)Peak memory usage: 12 MB
% 0.21/0.36 % (625622)Instructions burned: 6 (million)
% 0.21/0.36 % (625623)Instruction limit reached!
% 0.21/0.36 % (625623)------------------------------
% 0.21/0.36 % (625623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625623)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625623)Termination reason: Instruction limit
% 0.21/0.36 % (625623)Termination phase: Saturation
% 0.21/0.36 % (625623)Time elapsed: 0.004 s
% 0.21/0.36 % (625623)Peak memory usage: 12 MB
% 0.21/0.36 % (625623)Instructions burned: 7 (million)
% 0.21/0.36 % (625628)lrs+10_1_si=on:cs=on:random_seed=447905243:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.21/0.36 % (625625)Refutation not found, incomplete strategy
% 0.21/0.36 % (625625)------------------------------
% 0.21/0.36 % (625625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625625)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625625)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.36 % (625625)Time elapsed: 0.006 s
% 0.21/0.36 % (625625)Peak memory usage: 12 MB
% 0.21/0.36 % (625625)Instructions burned: 9 (million)
% 0.21/0.36 % (625624)Refutation not found, incomplete strategy
% 0.21/0.36 % (625624)------------------------------
% 0.21/0.36 % (625624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625624)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625624)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.36 % (625624)Time elapsed: 0.008 s
% 0.21/0.36 % (625624)Peak memory usage: 12 MB
% 0.21/0.36 % (625624)Instructions burned: 13 (million)
% 0.21/0.36 % (625625)------------------------------
% 0.21/0.36 % (625625)------------------------------
% 0.21/0.36 % (625624)------------------------------
% 0.21/0.36 % (625624)------------------------------
% 0.21/0.36 % (625628)Instruction limit reached!
% 0.21/0.36 % (625628)------------------------------
% 0.21/0.36 % (625628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625628)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625628)Termination reason: Instruction limit
% 0.21/0.36 % (625628)Termination phase: Saturation
% 0.21/0.36 % (625628)Time elapsed: 0.009 s
% 0.21/0.36 % (625628)Peak memory usage: 12 MB
% 0.21/0.36 % (625628)Instructions burned: 13 (million)
% 0.21/0.36 % (625610)Instruction limit reached!
% 0.21/0.36 % (625610)------------------------------
% 0.21/0.36 % (625610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625610)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625610)Termination reason: Instruction limit
% 0.21/0.36 % (625610)Termination phase: Saturation
% 0.21/0.36 % (625610)Time elapsed: 0.043 s
% 0.21/0.36 % (625610)Peak memory usage: 12 MB
% 0.21/0.36 % (625610)Instructions burned: 75 (million)
% 0.21/0.36 % (625634)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.21/0.36 % (625627)Instruction limit reached!
% 0.21/0.36 % (625627)------------------------------
% 0.21/0.36 % (625627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625627)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625627)Termination reason: Instruction limit
% 0.21/0.36 % (625627)Termination phase: Saturation
% 0.21/0.36 % (625627)Time elapsed: 0.024 s
% 0.21/0.36 % (625627)Peak memory usage: 13 MB
% 0.21/0.36 % (625627)Instructions burned: 87 (million)
% 0.21/0.36 % (625634)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=324992759:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.36 % (625635)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=199181411:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.21/0.36 % (625635)Refutation not found, incomplete strategy
% 0.21/0.36 % (625635)------------------------------
% 0.21/0.36 % (625635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625635)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625635)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.36 % (625635)Time elapsed: 0.001 s
% 0.21/0.36 % (625635)Peak memory usage: 12 MB
% 0.21/0.36 % (625635)------------------------------
% 0.21/0.36 % (625635)------------------------------
% 0.21/0.36 % (625634)Instruction limit reached!
% 0.21/0.36 % (625634)------------------------------
% 0.21/0.36 % (625634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625634)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625634)Termination reason: Instruction limit
% 0.21/0.36 % (625634)Termination phase: Saturation
% 0.21/0.36 % (625634)Time elapsed: 0.004 s
% 0.21/0.36 % (625634)Peak memory usage: 12 MB
% 0.21/0.36 % (625634)Instructions burned: 5 (million)
% 0.21/0.36 % (625637)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=276546162:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.21/0.36 % (625638)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1638186165:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.21/0.36 % (625637)Refutation not found, incomplete strategy
% 0.21/0.36 % (625637)------------------------------
% 0.21/0.36 % (625637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625637)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625637)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.36 % (625637)Time elapsed: 0.001 s
% 0.21/0.36 % (625637)Peak memory usage: 12 MB
% 0.21/0.36 % (625637)Instructions burned: 1 (million)
% 0.21/0.36 % (625638)Refutation not found, incomplete strategy
% 0.21/0.36 % (625638)------------------------------
% 0.21/0.36 % (625638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625637)------------------------------
% 0.21/0.36 % (625637)------------------------------
% 0.21/0.36 % (625638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625638)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625638)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.36 % (625638)Time elapsed: 0.002 s
% 0.21/0.36 % (625638)Peak memory usage: 12 MB
% 0.21/0.36 % (625638)Instructions burned: 2 (million)
% 0.21/0.36 % (625641)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=523468886:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 0.21/0.36 % (625638)------------------------------
% 0.21/0.36 % (625638)------------------------------
% 0.21/0.36 % (625639)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3024814467:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.21/0.36 % (625641) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-625593-625641"...
% 0.21/0.36 % (625640)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3314483091:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.21/0.36 % (625639)Refutation not found, incomplete strategy
% 0.21/0.36 % (625639)------------------------------
% 0.21/0.36 % (625639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (625639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (625639)CaDiCaL version: 2.1.3
% 0.21/0.36 % (625639)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.36 % (625639)Time elapsed: 0.003 s
% 0.21/0.36 % (625639)Peak memory usage: 12 MB
% 0.21/0.36 % (625639)Instructions burned: 4 (million)
% 0.21/0.36 % (625639)------------------------------
% 0.21/0.36 % (625639)------------------------------
% 0.21/0.36 % (625641)...printing done.
% 0.21/0.36 % (625641)Refutation found. Thanks to Tanya!
% 0.21/0.36 % SZS status Theorem for theBenchmark
% 0.21/0.36 % SZS output start Proof for theBenchmark
% 0.21/0.36 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.21/0.36 thf(func_def_0, type, eps: (($i > $o) > $i)).
% 0.21/0.36 thf(func_def_2, type, if: ($o > $i > $i > $i)).
% 0.21/0.36 thf(func_def_5, type, vOR: ($o > $o > $o)).
% 0.21/0.36 thf(func_def_6, type, vAND: ($o > $o > $o)).
% 0.21/0.36 thf(func_def_7, type, vNOT: ($o > $o)).
% 0.21/0.36 thf(func_def_8, type, db3: !>[X0: $tType]:(X0)).
% 0.21/0.36 thf(func_def_9, type, db1: !>[X0: $tType]:(X0)).
% 0.21/0.36 thf(func_def_10, type, db0: !>[X0: $tType]:(X0)).
% 0.21/0.36 thf(func_def_11, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.21/0.36 thf(func_def_12, type, db2: !>[X0: $tType]:(X0)).
% 0.21/0.36 thf(func_def_13, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.21/0.36 thf(func_def_14, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.21/0.36 thf(func_def_15, type, sK0: ($i > $o)).
% 0.21/0.36 thf(f2,axiom,(
% 0.70/0.36 (if = (^[X0 : $o, X1 : $i, X2 : $i] : ((eps @ (^[X3 : $i] : (((X3 = X1) & X0) | ((X3 = X2) & ~X0)))))))),
% 0.70/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifd)).
% 0.70/0.36 thf(f3,conjecture,(
% 0.70/0.36 ! [X0 : ($i > $o)] : (((if @ ? [X1 : $i] : (X0 @ X1) @ (eps @ X0) @ (eps @ (^[X1 : $i] : ($false))))) = ((eps @ X0)))),
% 0.70/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 0.70/0.36 thf(f4,negated_conjecture,(
% 0.70/0.36 ~ ! [X0 : ($i > $o)] : (((if @ ? [X1 : $i] : (X0 @ X1) @ (eps @ X0) @ (eps @ (^[X1 : $i] : ($false))))) = ((eps @ X0)))),
% 0.70/0.36 inference(negated_conjecture,[status(cth)],[f3])).
% 0.70/0.36 thf(f7,plain,(
% 0.70/0.36 (if = (^[X0 : $o, X1 : $i, X2 : $i] : ((eps @ (^[X3 : $i] : (((X3 = X1) & X0) | ((X3 = X2) & ~X0)))))))),
% 0.70/0.36 inference(rectify,[],[f2])).
% 0.70/0.36 thf(f8,plain,(
% 0.70/0.36 (if = (^[Y0 : $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (eps @ (^[Y3 : $i]: (((~ Y0) & (Y2 = Y3)) | (Y0 & (Y1 = Y3)))))))))))),
% 0.70/0.36 inference(fool_elimination,[],[f7])).
% 0.70/0.36 thf(f9,plain,(
% 0.70/0.36 ~ ! [X0 : ($i > $o)] : (((if @ ? [X1 : $i] : (X0 @ X1) @ (eps @ X0) @ (eps @ (^[X2 : $i] : ($false))))) = ((eps @ X0)))),
% 0.70/0.36 inference(rectify,[],[f4])).
% 0.70/0.36 thf(f10,plain,(
% 0.70/0.36 ~ ! [X0 : ($i > $o)] : (((eps @ X0)) = ((if @ (?? @ $i @ (^[Y0 : $i]: (X0 @ Y0))) @ (eps @ X0) @ (eps @ (^[Y0 : $i]: ($false))))))),
% 0.70/0.36 inference(fool_elimination,[],[f9])).
% 0.70/0.36 thf(f11,plain,(
% 0.70/0.36 ? [X0 : ($i > $o)] : (((eps @ X0)) != ((if @ (?? @ $i @ (^[Y0 : $i]: (X0 @ Y0))) @ (eps @ X0) @ (eps @ (^[Y0 : $i]: ($false))))))),
% 0.70/0.36 inference(ennf_transformation,[],[f10])).
% 0.70/0.36 thf(f13,plain,(
% 0.70/0.36 (((eps @ sK0)) != ((if @ (?? @ $i @ (^[Y0 : $i]: (sK0 @ Y0))) @ (eps @ sK0) @ (eps @ (^[Y0 : $i]: ($false))))))),
% 0.70/0.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f11])).
% 0.70/0.36 thf(f14,plain,(
% 0.70/0.36 (if = (^[Y0 : $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (eps @ (^[Y3 : $i]: (((~ Y0) & (Y2 = Y3)) | (Y0 & (Y1 = Y3)))))))))))),
% 0.70/0.36 inference(cnf_transformation,[],[f8])).
% 0.70/0.36 thf(f16,plain,(
% 0.70/0.36 (((eps @ sK0)) != ((if @ (?? @ $i @ (^[Y0 : $i]: (sK0 @ Y0))) @ (eps @ sK0) @ (eps @ (^[Y0 : $i]: ($false))))))),
% 0.70/0.36 inference(cnf_transformation,[],[f13])).
% 0.70/0.36 thf(f19,plain,(
% 0.70/0.36 ((((^[Y0 : $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (eps @ (^[Y3 : $i]: (((~ Y0) & (Y2 = Y3)) | (Y0 & (Y1 = Y3)))))))))) @ (?? @ $i @ (^[Y0 : $i]: (sK0 @ Y0))) @ (eps @ sK0) @ (eps @ (^[Y0 : $i]: ($false))))) != ((eps @ sK0)))),
% 0.70/0.36 inference(definition_unfolding,[],[f16,f14])).
% 0.70/0.36 thf(f20,plain,(
% 0.70/0.36 (((eps @ sK0)) != ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))))))),
% 0.70/0.36 inference(beta-eta_normalization,[],[f19])).
% 0.70/0.36 thf(f30,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) @ (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))))))) | ($false = (((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) @ X1)))) )),
% 0.70/0.36 introduced(theory,[Hilbert's_choice_axiom_instance])).
% 0.70/0.36 thf(f31,plain,(
% 0.70/0.36 ((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) != sK0)),
% 0.70/0.36 inference(equality_resolution,[],[f20])).
% 0.70/0.36 thf(f33,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (($false = ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = X1)) | ((?? @ $i @ sK0) & ((eps @ sK0) = X1))))) | (((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | ((?? @ $i @ sK0) & ((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))))) = $true)) )),
% 0.70/0.36 inference(beta-eta_normalization,[],[f30])).
% 0.70/0.36 thf(f34,plain,(
% 0.70/0.36 ( ! [X1 : $i] : ((((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | ((?? @ $i @ sK0) & ((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))))) = $true) | ((((?? @ $i @ sK0) & ((eps @ sK0) = X1))) = $false)) )),
% 0.70/0.36 inference(or_proxy_clausification,[],[f33])).
% 0.70/0.36 thf(f35,plain,(
% 0.70/0.36 ( ! [X1 : $i] : ((((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | ((?? @ $i @ sK0) & ((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))))) = $true) | ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = X1))) = $false)) )),
% 0.70/0.36 inference(or_proxy_clausification,[],[f33])).
% 0.70/0.36 thf(f36,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (($true = (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))))) | ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = X1))) = $false) | ($true = (((?? @ $i @ sK0) & ((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))))))))) )),
% 0.70/0.36 inference(or_proxy_clausification,[],[f35])).
% 0.70/0.36 thf(f37,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (($true = (((?? @ $i @ sK0) & ((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))))) | ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = X1))) = $false) | ($true = (((eps @ (^[Y0 : $i]: ($false))) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))))) )),
% 0.70/0.36 inference(and_proxy_clausification,[],[f36])).
% 0.70/0.36 thf(f55,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (((((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) = $true) | ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = X1))) = $false) | ($true = (((eps @ (^[Y0 : $i]: ($false))) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))))) )),
% 0.70/0.36 inference(and_proxy_clausification,[],[f37])).
% 0.70/0.36 thf(f63,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (($true = (((eps @ (^[Y0 : $i]: ($false))) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))))))) | (((eps @ sK0)) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = X1))) = $false)) )),
% 0.70/0.36 inference(equality_proxy_clausification,[],[f55])).
% 0.70/0.36 thf(f64,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = X1))) = $false) | (((eps @ (^[Y0 : $i]: ($false)))) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | (((eps @ sK0)) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))))))) )),
% 0.70/0.36 inference(equality_proxy_clausification,[],[f63])).
% 0.70/0.36 thf(f65,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (($false = ((~ (?? @ $i @ sK0)))) | (((eps @ (^[Y0 : $i]: ($false)))) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | (((eps @ sK0)) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | ((((eps @ (^[Y0 : $i]: ($false))) = X1)) = $false)) )),
% 0.70/0.36 inference(and_proxy_clausification,[],[f64])).
% 0.70/0.36 thf(f66,plain,(
% 0.70/0.36 ( ! [X1 : $i] : ((((eps @ sK0)) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | ((((eps @ (^[Y0 : $i]: ($false))) = X1)) = $false) | (((eps @ (^[Y0 : $i]: ($false)))) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | ($true = ((?? @ $i @ sK0)))) )),
% 0.70/0.36 inference(not_proxy_clausification,[],[f65])).
% 0.70/0.36 thf(f67,plain,(
% 0.70/0.36 ( ! [X1 : $i] : ((((eps @ (^[Y0 : $i]: ($false)))) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | (((eps @ (^[Y0 : $i]: ($false)))) != X1) | (((eps @ sK0)) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | ($true = ((?? @ $i @ sK0)))) )),
% 0.70/0.36 inference(equality_proxy_clausification,[],[f66])).
% 0.70/0.36 thf(f68,plain,(
% 0.70/0.36 ( ! [X1 : $i] : ((((eps @ (^[Y0 : $i]: ($false)))) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | (((eps @ sK0)) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | (((sK0 @ sK5)) = $true) | (((eps @ (^[Y0 : $i]: ($false)))) != X1)) )),
% 0.70/0.36 inference(sigma_proxy_clausification,[],[f67])).
% 0.70/0.36 thf(f69,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (($true = (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))))) | ($true = (((?? @ $i @ sK0) & ((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))))) | ((((?? @ $i @ sK0) & ((eps @ sK0) = X1))) = $false)) )),
% 0.70/0.36 inference(or_proxy_clausification,[],[f34])).
% 0.70/0.36 thf(f71,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (($true = ((~ (?? @ $i @ sK0)))) | ((((?? @ $i @ sK0) & ((eps @ sK0) = X1))) = $false) | ($true = (((?? @ $i @ sK0) & ((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))))))))) )),
% 0.70/0.36 inference(and_proxy_clausification,[],[f69])).
% 0.70/0.36 thf(f72,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (($true = (((?? @ $i @ sK0) & ((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))))) | ((((?? @ $i @ sK0) & ((eps @ sK0) = X1))) = $false) | ($false = ((?? @ $i @ sK0)))) )),
% 0.70/0.36 inference(not_proxy_clausification,[],[f71])).
% 0.70/0.36 thf(f73,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (((((?? @ $i @ sK0) & ((eps @ sK0) = X1))) = $false) | ((((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) = $true) | ($false = ((?? @ $i @ sK0)))) )),
% 0.70/0.36 inference(and_proxy_clausification,[],[f72])).
% 0.70/0.36 thf(f80,plain,(
% 0.70/0.36 ( ! [X1 : $i] : (($false = ((?? @ $i @ sK0))) | ($false = (((eps @ sK0) = X1))) | ((((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) = $true) | ($false = ((?? @ $i @ sK0)))) )),
% 0.70/0.36 inference(and_proxy_clausification,[],[f73])).
% 0.70/0.36 thf(f81,plain,(
% 0.70/0.36 ( ! [X2 : $i,X1 : $i] : (($false = ((sK0 @ X2))) | ($false = (((eps @ sK0) = X1))) | ($false = ((sK0 @ X2))) | ((((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) = $true)) )),
% 0.70/0.36 inference(pi_proxy_clausification,[],[f80])).
% 0.70/0.36 thf(f82,plain,(
% 0.70/0.36 ( ! [X2 : $i,X1 : $i] : ((((eps @ sK0)) != X1) | ($false = ((sK0 @ X2))) | ((((eps @ sK0) = (eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) = $true) | ($false = ((sK0 @ X2)))) )),
% 0.70/0.36 inference(equality_proxy_clausification,[],[f81])).
% 0.70/0.36 thf(f83,plain,(
% 0.70/0.36 ( ! [X2 : $i,X1 : $i] : (($false = ((sK0 @ X2))) | ($false = ((sK0 @ X2))) | (((eps @ sK0)) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | (((eps @ sK0)) != X1)) )),
% 0.70/0.36 inference(equality_proxy_clausification,[],[f82])).
% 0.70/0.36 thf(f84,plain,(
% 0.70/0.36 ( ! [X2 : $i,X1 : $i] : ((((eps @ sK0)) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | (((eps @ sK0)) != X1) | ($false = ((sK0 @ X2)))) )),
% 0.70/0.36 inference(duplicate_literal_removal,[],[f83])).
% 0.70/0.36 thf(f100,definition,(
% 0.70/0.36 spl8_2 <=> ! [X1 : $i] : (((sK0 @ X1)) = $false)),
% 0.70/0.36 introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition])).
% 0.70/0.36 thf(f101,plain,(
% 0.70/0.36 ( ! [X1 : $i] : ((((sK0 @ X1)) = $false)) ) | ~spl8_2),
% 0.70/0.36 inference(avatar_component_clause,[],[f100])).
% 0.70/0.36 thf(f104,definition,(
% 0.70/0.36 spl8_3 <=> ! [X1 : $i] : (((eps @ (^[Y0 : $i]: ($false)))) != X1)),
% 0.70/0.36 introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition])).
% 0.70/0.36 thf(f105,plain,(
% 0.70/0.36 ( ! [X1 : $i] : ((((eps @ (^[Y0 : $i]: ($false)))) != X1)) ) | ~spl8_3),
% 0.70/0.36 inference(avatar_component_clause,[],[f104])).
% 0.70/0.36 thf(f118,definition,(
% 0.70/0.36 spl8_7 <=> (((eps @ (^[Y0 : $i]: ($false)))) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))))))),
% 0.70/0.36 introduced(definition,[new_symbols(definition,[spl8_7])],[avatar_definition])).
% 0.70/0.36 thf(f119,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | ~spl8_7),
% 0.70/0.36 inference(avatar_component_clause,[],[f118])).
% 0.70/0.36 thf(f121,plain,(
% 0.70/0.36 ( ! [X1 : $i] : ((((eps @ (^[Y0 : $i]: ($false)))) != X1) | (((eps @ (^[Y0 : $i]: ($false)))) = ((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))))) | (((sK0 @ sK5)) = $true)) )),
% 0.70/0.36 inference(forward_subsumption_resolution,[],[f68,f20])).
% 0.70/0.36 thf(f126,definition,(
% 0.70/0.36 spl8_9 <=> ! [X1 : $i] : (((eps @ sK0)) != X1)),
% 0.70/0.36 introduced(definition,[new_symbols(definition,[spl8_9])],[avatar_definition])).
% 0.70/0.36 thf(f127,plain,(
% 0.70/0.36 ( ! [X1 : $i] : ((((eps @ sK0)) != X1)) ) | ~spl8_9),
% 0.70/0.36 inference(avatar_component_clause,[],[f126])).
% 0.70/0.36 thf(f129,plain,(
% 0.70/0.36 ( ! [X2 : $i,X1 : $i] : ((((eps @ sK0)) != X1) | ($false = ((sK0 @ X2)))) )),
% 0.70/0.36 inference(forward_subsumption_resolution,[],[f84,f20])).
% 0.70/0.36 thf(f140,definition,(
% 0.70/0.36 spl8_12 <=> (((sK0 @ sK5)) = $true)),
% 0.70/0.36 introduced(definition,[new_symbols(definition,[spl8_12])],[avatar_definition])).
% 0.70/0.36 thf(f141,plain,(
% 0.70/0.36 (((sK0 @ sK5)) = $true) | ~spl8_12),
% 0.70/0.36 inference(avatar_component_clause,[],[f140])).
% 0.70/0.36 thf(f142,plain,(
% 0.70/0.36 spl8_12 | spl8_3 | spl8_7),
% 0.70/0.36 inference(avatar_split_clause,[],[f121,f118,f104,f140])).
% 0.70/0.36 thf(f143,plain,(
% 0.70/0.36 spl8_2 | spl8_9),
% 0.70/0.36 inference(avatar_split_clause,[],[f129,f126,f100])).
% 0.70/0.36 thf(f149,plain,(
% 0.70/0.36 ((((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) @ sK9)) != ((sK0 @ sK9)))),
% 0.70/0.36 inference(negative_extensionality,[],[f31])).
% 0.70/0.36 thf(f151,plain,(
% 0.70/0.36 ($true = ((sK0 @ sK9))) | ((((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) @ sK9)) = $true)),
% 0.70/0.36 inference(xor_proxy_clausification,[],[f149])).
% 0.70/0.36 thf(f163,plain,(
% 0.70/0.36 ($true = ((sK0 @ sK9))) | ($true = ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK9)) | ((?? @ $i @ sK0) & ((eps @ sK0) = sK9)))))),
% 0.70/0.36 inference(beta-eta_normalization,[],[f151])).
% 0.70/0.36 thf(f164,plain,(
% 0.70/0.36 ($true = (((?? @ $i @ sK0) & ((eps @ sK0) = sK9)))) | ($true = ((sK0 @ sK9))) | ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK9))) = $true)),
% 0.70/0.36 inference(or_proxy_clausification,[],[f163])).
% 0.70/0.36 thf(f166,plain,(
% 0.70/0.36 ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK9))) = $true) | ($true = ((?? @ $i @ sK0))) | ($true = ((sK0 @ sK9)))),
% 0.70/0.36 inference(and_proxy_clausification,[],[f164])).
% 0.70/0.36 thf(f167,plain,(
% 0.70/0.36 ($true = (((eps @ (^[Y0 : $i]: ($false))) = sK9))) | ($true = ((sK0 @ sK9))) | ($true = ((?? @ $i @ sK0)))),
% 0.70/0.36 inference(and_proxy_clausification,[],[f166])).
% 0.70/0.36 thf(f172,plain,(
% 0.70/0.36 ($true = ((?? @ $i @ sK0))) | (((eps @ (^[Y0 : $i]: ($false)))) = sK9) | ($true = ((sK0 @ sK9)))),
% 0.70/0.36 inference(equality_proxy_clausification,[],[f167])).
% 0.70/0.36 thf(f173,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) = sK9) | ($true = ((sK0 @ sK9))) | (((sK0 @ sK12)) = $true)),
% 0.70/0.36 inference(sigma_proxy_clausification,[],[f172])).
% 0.70/0.36 thf(f180,plain,(
% 0.70/0.36 ($true = $false) | ($true = ((sK0 @ sK9))) | (((eps @ (^[Y0 : $i]: ($false)))) = sK9) | ~spl8_2),
% 0.70/0.36 inference(forward_demodulation,[],[f173,f101])).
% 0.70/0.36 thf(f181,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) = sK9) | ($true = ((sK0 @ sK9))) | ~spl8_2),
% 0.70/0.36 inference(trivial_inequality_removal,[],[f180])).
% 0.70/0.36 thf(f184,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) = sK9) | ($true = $false) | ~spl8_2),
% 0.70/0.36 inference(forward_demodulation,[],[f181,f101])).
% 0.70/0.36 thf(f185,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) = sK9) | ~spl8_2),
% 0.70/0.36 inference(trivial_inequality_removal,[],[f184])).
% 0.70/0.36 thf(f187,definition,(
% 0.70/0.36 spl8_13 <=> (((eps @ (^[Y0 : $i]: ($false)))) = sK9)),
% 0.70/0.36 introduced(definition,[new_symbols(definition,[spl8_13])],[avatar_definition])).
% 0.70/0.36 thf(f188,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) = sK9) | ~spl8_13),
% 0.70/0.36 inference(avatar_component_clause,[],[f187])).
% 0.70/0.36 thf(f190,definition,(
% 0.70/0.36 spl8_14 <=> (((eps @ sK0)) = sK9)),
% 0.70/0.36 introduced(definition,[new_symbols(definition,[spl8_14])],[avatar_definition])).
% 0.70/0.36 thf(f193,plain,(
% 0.70/0.36 spl8_13 | ~spl8_2),
% 0.70/0.36 inference(avatar_split_clause,[],[f185,f100,f187])).
% 0.70/0.36 thf(f209,plain,(
% 0.70/0.36 (((eps @ sK0)) != sK9) | spl8_14),
% 0.70/0.36 inference(avatar_component_clause,[],[f190])).
% 0.70/0.36 thf(f220,plain,(
% 0.70/0.36 $false | ~spl8_9),
% 0.70/0.36 inference(equality_resolution,[],[f127])).
% 0.70/0.36 thf(f221,plain,(
% 0.70/0.36 ~spl8_9),
% 0.70/0.36 inference(avatar_contradiction_clause,[],[f220])).
% 0.70/0.36 thf(f240,plain,(
% 0.70/0.36 $false | ~spl8_3),
% 0.70/0.36 inference(equality_resolution,[],[f105])).
% 0.70/0.36 thf(f241,plain,(
% 0.70/0.36 ~spl8_3),
% 0.70/0.36 inference(avatar_contradiction_clause,[],[f240])).
% 0.70/0.36 thf(f245,plain,(
% 0.70/0.36 (sK9 != sK9) | ((^[Y0 : $i]: ($false)) != sK0) | (~spl8_13 | spl8_14)),
% 0.70/0.36 inference(constrained_superposition,[],[f209,f188])).
% 0.70/0.36 thf(f247,plain,(
% 0.70/0.36 ((^[Y0 : $i]: ($false)) != sK0) | (~spl8_13 | spl8_14)),
% 0.70/0.36 inference(trivial_inequality_removal,[],[f245])).
% 0.70/0.36 thf(f249,definition,(
% 0.70/0.36 spl8_20 <=> ((^[Y0 : $i]: ($false)) = sK0)),
% 0.70/0.36 introduced(definition,[new_symbols(definition,[spl8_20])],[avatar_definition])).
% 0.70/0.36 thf(f250,plain,(
% 0.70/0.36 ((^[Y0 : $i]: ($false)) != sK0) | spl8_20),
% 0.70/0.36 inference(avatar_component_clause,[],[f249])).
% 0.70/0.36 thf(f251,plain,(
% 0.70/0.36 ~spl8_20 | ~spl8_13 | spl8_14),
% 0.70/0.36 inference(avatar_split_clause,[],[f247,f190,f187,f249])).
% 0.70/0.36 thf(f252,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & (sK9 = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))))) = sK9) | (~spl8_7 | ~spl8_13)),
% 0.70/0.36 inference(forward_demodulation,[],[f119,f188])).
% 0.70/0.36 thf(f254,definition,(
% 0.70/0.36 spl8_21 <=> (((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & (sK9 = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))))) = sK9)),
% 0.70/0.36 introduced(definition,[new_symbols(definition,[spl8_21])],[avatar_definition])).
% 0.70/0.36 thf(f255,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & (sK9 = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))))) = sK9) | ~spl8_21),
% 0.70/0.36 inference(avatar_component_clause,[],[f254])).
% 0.70/0.36 thf(f256,plain,(
% 0.70/0.36 spl8_21 | ~spl8_7 | ~spl8_13),
% 0.70/0.36 inference(avatar_split_clause,[],[f252,f187,f118,f254])).
% 0.70/0.36 thf(f260,plain,(
% 0.70/0.36 ($true = $false) | (~spl8_2 | ~spl8_12)),
% 0.70/0.36 inference(forward_demodulation,[],[f141,f101])).
% 0.70/0.36 thf(f261,plain,(
% 0.70/0.36 $false | (~spl8_2 | ~spl8_12)),
% 0.70/0.36 inference(trivial_inequality_removal,[],[f260])).
% 0.70/0.36 thf(f262,plain,(
% 0.70/0.36 ~spl8_2 | ~spl8_12),
% 0.70/0.36 inference(avatar_contradiction_clause,[],[f261])).
% 0.70/0.36 thf(f264,plain,(
% 0.70/0.36 ((((^[Y0 : $i]: ($false)) @ sK13)) != ((sK0 @ sK13))) | spl8_20),
% 0.70/0.36 inference(negative_extensionality,[],[f250])).
% 0.70/0.36 thf(f265,plain,(
% 0.70/0.36 ($true = ((sK0 @ sK13))) | ((((^[Y0 : $i]: ($false)) @ sK13)) = $true) | spl8_20),
% 0.70/0.36 inference(xor_proxy_clausification,[],[f264])).
% 0.70/0.36 thf(f268,plain,(
% 0.70/0.36 ($true = ((sK0 @ sK13))) | ($true = $false) | spl8_20),
% 0.70/0.36 inference(beta-eta_normalization,[],[f265])).
% 0.70/0.36 thf(f269,plain,(
% 0.70/0.36 ($true = ((sK0 @ sK13))) | spl8_20),
% 0.70/0.36 inference(trivial_inequality_removal,[],[f268])).
% 0.70/0.36 thf(f270,plain,(
% 0.70/0.36 ($true = $false) | (~spl8_2 | spl8_20)),
% 0.70/0.36 inference(forward_demodulation,[],[f269,f101])).
% 0.70/0.36 thf(f271,plain,(
% 0.70/0.36 $false | (~spl8_2 | spl8_20)),
% 0.70/0.36 inference(trivial_inequality_removal,[],[f270])).
% 0.70/0.36 thf(f272,plain,(
% 0.70/0.36 ~spl8_2 | spl8_20),
% 0.70/0.36 inference(avatar_contradiction_clause,[],[f271])).
% 0.70/0.36 thf(f279,plain,(
% 0.70/0.36 (((eps @ sK0)) != sK9) | ((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) != (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & (sK9 = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))) | ~spl8_21),
% 0.70/0.36 inference(constrained_superposition,[],[f20,f255])).
% 0.70/0.36 thf(f334,definition,(
% 0.70/0.36 spl8_23 <=> ((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) = (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & (sK9 = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))))),
% 0.70/0.36 introduced(definition,[new_symbols(definition,[spl8_23])],[avatar_definition])).
% 0.70/0.36 thf(f335,plain,(
% 0.70/0.36 ((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) != (^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & (sK9 = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0))))) | spl8_23),
% 0.70/0.36 inference(avatar_component_clause,[],[f334])).
% 0.70/0.36 thf(f336,plain,(
% 0.70/0.36 ~spl8_14 | ~spl8_23 | ~spl8_21),
% 0.70/0.36 inference(avatar_split_clause,[],[f279,f254,f334,f190])).
% 0.70/0.36 thf(f341,plain,(
% 0.70/0.36 ((((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) @ sK19)) != (((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & (sK9 = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) @ sK19))) | spl8_23),
% 0.70/0.36 inference(negative_extensionality,[],[f335])).
% 0.70/0.36 thf(f343,plain,(
% 0.70/0.36 ((((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) @ sK19)) = $true) | ($true = (((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & (sK9 = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) @ sK19))) | spl8_23),
% 0.70/0.36 inference(xor_proxy_clausification,[],[f341])).
% 0.70/0.36 thf(f344,plain,(
% 0.70/0.36 ($false = (((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & (sK9 = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) @ sK19))) | ((((^[Y0 : $i]: (((~ (?? @ $i @ sK0)) & ((eps @ (^[Y1 : $i]: ($false))) = Y0)) | ((?? @ $i @ sK0) & ((eps @ sK0) = Y0)))) @ sK19)) = $false) | spl8_23),
% 0.70/0.36 inference(xor_proxy_clausification,[],[f341])).
% 0.70/0.36 thf(f345,plain,(
% 0.70/0.36 ($false = ((((~ (?? @ $i @ sK0)) & (sK9 = sK19)) | ((?? @ $i @ sK0) & ((eps @ sK0) = sK19))))) | ($false = ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK19)) | ((?? @ $i @ sK0) & ((eps @ sK0) = sK19))))) | spl8_23),
% 0.70/0.36 inference(beta-eta_normalization,[],[f344])).
% 0.70/0.36 thf(f347,plain,(
% 0.70/0.36 ($false = ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK19)) | ((?? @ $i @ sK0) & ((eps @ sK0) = sK19))))) | ((((~ (?? @ $i @ sK0)) & (sK9 = sK19))) = $false) | spl8_23),
% 0.70/0.36 inference(or_proxy_clausification,[],[f345])).
% 0.70/0.36 thf(f349,plain,(
% 0.70/0.36 ((((~ (?? @ $i @ sK0)) & (sK9 = sK19))) = $false) | ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK19))) = $false) | spl8_23),
% 0.70/0.36 inference(or_proxy_clausification,[],[f347])).
% 0.70/0.36 thf(f350,plain,(
% 0.70/0.36 ($false = ((~ (?? @ $i @ sK0)))) | ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK19))) = $false) | ($false = ((sK9 = sK19))) | spl8_23),
% 0.70/0.36 inference(and_proxy_clausification,[],[f349])).
% 0.70/0.36 thf(f351,plain,(
% 0.70/0.36 ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK19))) = $false) | ($false = ((sK9 = sK19))) | ($true = ((?? @ $i @ sK0))) | spl8_23),
% 0.70/0.36 inference(not_proxy_clausification,[],[f350])).
% 0.70/0.36 thf(f352,plain,(
% 0.70/0.36 ($false = (((eps @ (^[Y0 : $i]: ($false))) = sK19))) | ($false = ((~ (?? @ $i @ sK0)))) | ($false = ((sK9 = sK19))) | ($true = ((?? @ $i @ sK0))) | spl8_23),
% 0.70/0.36 inference(and_proxy_clausification,[],[f351])).
% 0.70/0.36 thf(f353,plain,(
% 0.70/0.36 ($true = ((?? @ $i @ sK0))) | ($false = ((sK9 = sK19))) | ($false = ((~ (?? @ $i @ sK0)))) | (((eps @ (^[Y0 : $i]: ($false)))) != sK19) | spl8_23),
% 0.70/0.36 inference(equality_proxy_clausification,[],[f352])).
% 0.70/0.36 thf(f354,plain,(
% 0.70/0.36 (((sK0 @ sK20)) = $true) | ($false = ((~ (?? @ $i @ sK0)))) | (((eps @ (^[Y0 : $i]: ($false)))) != sK19) | ($false = ((sK9 = sK19))) | spl8_23),
% 0.70/0.36 inference(sigma_proxy_clausification,[],[f353])).
% 0.70/0.36 thf(f355,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) != sK19) | ($false = ((sK9 = sK19))) | ($true = ((?? @ $i @ sK0))) | (((sK0 @ sK20)) = $true) | spl8_23),
% 0.70/0.36 inference(not_proxy_clausification,[],[f354])).
% 0.70/0.36 thf(f356,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) != sK19) | (((sK0 @ sK20)) = $true) | ($true = ((?? @ $i @ sK0))) | (sK9 != sK19) | spl8_23),
% 0.70/0.36 inference(equality_proxy_clausification,[],[f355])).
% 0.70/0.36 thf(f357,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) != sK19) | ($true = ((sK0 @ sK21))) | (sK9 != sK19) | (((sK0 @ sK20)) = $true) | spl8_23),
% 0.70/0.36 inference(sigma_proxy_clausification,[],[f356])).
% 0.70/0.36 thf(f379,plain,(
% 0.70/0.36 ($true = ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK19)) | ((?? @ $i @ sK0) & ((eps @ sK0) = sK19))))) | ($true = ((((~ (?? @ $i @ sK0)) & (sK9 = sK19)) | ((?? @ $i @ sK0) & ((eps @ sK0) = sK19))))) | spl8_23),
% 0.70/0.36 inference(beta-eta_normalization,[],[f343])).
% 0.70/0.36 thf(f380,plain,(
% 0.70/0.36 ((((?? @ $i @ sK0) & ((eps @ sK0) = sK19))) = $true) | ($true = ((((~ (?? @ $i @ sK0)) & (sK9 = sK19)) | ((?? @ $i @ sK0) & ((eps @ sK0) = sK19))))) | ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK19))) = $true) | spl8_23),
% 0.70/0.36 inference(or_proxy_clausification,[],[f379])).
% 0.70/0.36 thf(f382,plain,(
% 0.70/0.36 ($true = ((?? @ $i @ sK0))) | ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK19))) = $true) | ($true = ((((~ (?? @ $i @ sK0)) & (sK9 = sK19)) | ((?? @ $i @ sK0) & ((eps @ sK0) = sK19))))) | spl8_23),
% 0.70/0.36 inference(and_proxy_clausification,[],[f380])).
% 0.70/0.36 thf(f383,plain,(
% 0.70/0.36 ((((~ (?? @ $i @ sK0)) & ((eps @ (^[Y0 : $i]: ($false))) = sK19))) = $true) | ($true = ((((~ (?? @ $i @ sK0)) & (sK9 = sK19)) | ((?? @ $i @ sK0) & ((eps @ sK0) = sK19))))) | (((sK0 @ sK24)) = $true) | spl8_23),
% 0.70/0.36 inference(sigma_proxy_clausification,[],[f382])).
% 0.70/0.36 thf(f384,plain,(
% 0.70/0.36 ($true = (((eps @ (^[Y0 : $i]: ($false))) = sK19))) | ($true = ((((~ (?? @ $i @ sK0)) & (sK9 = sK19)) | ((?? @ $i @ sK0) & ((eps @ sK0) = sK19))))) | (((sK0 @ sK24)) = $true) | spl8_23),
% 0.70/0.36 inference(and_proxy_clausification,[],[f383])).
% 0.70/0.36 thf(f405,plain,(
% 0.70/0.36 ($true = ((((~ (?? @ $i @ sK0)) & (sK9 = sK19)) | ((?? @ $i @ sK0) & ((eps @ sK0) = sK19))))) | (((eps @ (^[Y0 : $i]: ($false)))) = sK19) | (((sK0 @ sK24)) = $true) | spl8_23),
% 0.70/0.36 inference(equality_proxy_clausification,[],[f384])).
% 0.70/0.36 thf(f406,plain,(
% 0.70/0.36 ((((?? @ $i @ sK0) & ((eps @ sK0) = sK19))) = $true) | (((eps @ (^[Y0 : $i]: ($false)))) = sK19) | ((((~ (?? @ $i @ sK0)) & (sK9 = sK19))) = $true) | (((sK0 @ sK24)) = $true) | spl8_23),
% 0.70/0.36 inference(or_proxy_clausification,[],[f405])).
% 0.70/0.36 thf(f408,plain,(
% 0.70/0.36 ($true = ((?? @ $i @ sK0))) | ((((~ (?? @ $i @ sK0)) & (sK9 = sK19))) = $true) | (((eps @ (^[Y0 : $i]: ($false)))) = sK19) | (((sK0 @ sK24)) = $true) | spl8_23),
% 0.70/0.36 inference(and_proxy_clausification,[],[f406])).
% 0.70/0.36 thf(f409,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) = sK19) | ((((~ (?? @ $i @ sK0)) & (sK9 = sK19))) = $true) | (((sK0 @ sK24)) = $true) | ($true = ((sK0 @ sK27))) | spl8_23),
% 0.70/0.36 inference(sigma_proxy_clausification,[],[f408])).
% 0.70/0.36 thf(f410,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) = sK19) | ($true = ((sK9 = sK19))) | (((sK0 @ sK24)) = $true) | ($true = ((sK0 @ sK27))) | spl8_23),
% 0.70/0.36 inference(and_proxy_clausification,[],[f409])).
% 0.70/0.36 thf(f414,plain,(
% 0.70/0.36 ($true = ((sK0 @ sK27))) | (((sK0 @ sK24)) = $true) | (sK9 = sK19) | (((eps @ (^[Y0 : $i]: ($false)))) = sK19) | spl8_23),
% 0.70/0.36 inference(equality_proxy_clausification,[],[f410])).
% 0.70/0.36 thf(f468,plain,(
% 0.70/0.36 (((sK0 @ sK20)) = $true) | (sK9 != sK19) | (sK9 != sK19) | ($true = ((sK0 @ sK21))) | (~spl8_13 | spl8_23)),
% 0.70/0.36 inference(forward_demodulation,[],[f357,f188])).
% 0.70/0.36 thf(f469,plain,(
% 0.70/0.36 (((sK0 @ sK20)) = $true) | ($true = ((sK0 @ sK21))) | (sK9 != sK19) | (~spl8_13 | spl8_23)),
% 0.70/0.36 inference(duplicate_literal_removal,[],[f468])).
% 0.70/0.36 thf(f470,plain,(
% 0.70/0.36 (((eps @ (^[Y0 : $i]: ($false)))) = sK19) | (((sK0 @ sK24)) = $true) | ($true = $false) | (sK9 = sK19) | (~spl8_2 | spl8_23)),
% 0.70/0.36 inference(forward_demodulation,[],[f414,f101])).
% 0.70/0.36 thf(f471,plain,(
% 0.70/0.36 (((sK0 @ sK24)) = $true) | (((eps @ (^[Y0 : $i]: ($false)))) = sK19) | (sK9 = sK19) | (~spl8_2 | spl8_23)),
% 0.70/0.36 inference(trivial_inequality_removal,[],[f470])).
% 0.70/0.36 thf(f478,plain,(
% 0.70/0.36 (sK9 != sK19) | ($true = ((sK0 @ sK21))) | ($true = $false) | (~spl8_2 | ~spl8_13 | spl8_23)),
% 0.70/0.36 inference(forward_demodulation,[],[f469,f101])).
% 0.70/0.36 thf(f479,plain,(
% 0.70/0.36 ($true = ((sK0 @ sK21))) | (sK9 != sK19) | (~spl8_2 | ~spl8_13 | spl8_23)),
% 0.70/0.36 inference(trivial_inequality_removal,[],[f478])).
% 0.70/0.36 thf(f480,plain,(
% 0.70/0.36 (sK9 = sK19) | ($true = $false) | (((eps @ (^[Y0 : $i]: ($false)))) = sK19) | (~spl8_2 | spl8_23)),
% 0.70/0.36 inference(forward_demodulation,[],[f471,f101])).
% 0.70/0.36 thf(f481,plain,(
% 0.70/0.36 (sK9 = sK19) | (((eps @ (^[Y0 : $i]: ($false)))) = sK19) | (~spl8_2 | spl8_23)),
% 0.70/0.36 inference(trivial_inequality_removal,[],[f480])).
% 0.70/0.36 thf(f488,plain,(
% 0.70/0.36 (sK9 != sK19) | ($true = $false) | (~spl8_2 | ~spl8_13 | spl8_23)),
% 0.70/0.36 inference(forward_demodulation,[],[f479,f101])).
% 0.70/0.36 thf(f489,plain,(
% 0.70/0.36 (sK9 != sK19) | (~spl8_2 | ~spl8_13 | spl8_23)),
% 0.70/0.36 inference(trivial_inequality_removal,[],[f488])).
% 0.70/0.36 thf(f490,plain,(
% 0.70/0.36 (sK9 = sK19) | (sK9 = sK19) | (~spl8_2 | ~spl8_13 | spl8_23)),
% 0.70/0.36 inference(forward_demodulation,[],[f481,f188])).
% 0.70/0.36 thf(f491,plain,(
% 0.70/0.36 (sK9 = sK19) | (~spl8_2 | ~spl8_13 | spl8_23)),
% 0.70/0.36 inference(duplicate_literal_removal,[],[f490])).
% 0.70/0.36 thf(f497,definition,(
% 0.70/0.36 spl8_24 <=> (sK9 = sK19)),
% 0.70/0.36 introduced(definition,[new_symbols(definition,[spl8_24])],[avatar_definition])).
% 0.70/0.36 thf(f501,plain,(
% 0.70/0.36 ~spl8_24 | ~spl8_2 | ~spl8_13 | spl8_23),
% 0.70/0.36 inference(avatar_split_clause,[],[f489,f334,f187,f100,f497])).
% 0.70/0.36 thf(f502,plain,(
% 0.70/0.36 spl8_24 | ~spl8_2 | ~spl8_13 | spl8_23),
% 0.70/0.36 inference(avatar_split_clause,[],[f491,f334,f187,f100,f497])).
% 0.70/0.36 cnf(s8, plain, spl8_3 | spl8_7 | spl8_12, inference(sat_conversion,[],[f142])).
% 0.70/0.36 cnf(s9, plain, spl8_2 | spl8_9, inference(sat_conversion,[],[f143])).
% 0.70/0.36 cnf(s12, plain, ~spl8_2 | spl8_13, inference(sat_conversion,[],[f193])).
% 0.70/0.36 cnf(s20, plain, ~spl8_9, inference(sat_conversion,[],[f221])).
% 0.70/0.36 cnf(s25, plain, ~spl8_3, inference(sat_conversion,[],[f241])).
% 0.70/0.36 cnf(s26, plain, ~spl8_13 | spl8_14 | ~spl8_20, inference(sat_conversion,[],[f251])).
% 0.70/0.36 cnf(s27, plain, ~spl8_7 | ~spl8_13 | spl8_21, inference(sat_conversion,[],[f256])).
% 0.70/0.36 cnf(s29, plain, ~spl8_2 | ~spl8_12, inference(sat_conversion,[],[f262])).
% 0.70/0.36 cnf(s32, plain, ~spl8_2 | spl8_20, inference(sat_conversion,[],[f272])).
% 0.70/0.36 cnf(s34, plain, ~spl8_14 | ~spl8_21 | ~spl8_23, inference(sat_conversion,[],[f336])).
% 0.70/0.36 cnf(s36, plain, ~spl8_2 | ~spl8_13 | spl8_23 | ~spl8_24, inference(sat_conversion,[],[f501])).
% 0.70/0.36 cnf(s37, plain, ~spl8_2 | ~spl8_13 | spl8_23 | spl8_24, inference(sat_conversion,[],[f502])).
% 0.70/0.36 cnf(s41, plain, spl8_2, inference(rat,[],[s9,s20])).
% 0.70/0.36 cnf(s42, plain, spl8_20, inference(rat,[],[s32,s41])).
% 0.70/0.36 cnf(s43, plain, ~spl8_12, inference(rat,[],[s29,s41])).
% 0.70/0.36 cnf(s46, plain, spl8_13, inference(rat,[],[s12,s41])).
% 0.70/0.36 cnf(s47, plain, spl8_14, inference(rat,[],[s26,s42,s46])).
% 0.70/0.36 cnf(s49, plain, spl8_7, inference(rat,[],[s8,s43,s25])).
% 0.70/0.36 cnf(s50, plain, spl8_21, inference(rat,[],[s27,s46,s49])).
% 0.70/0.36 cnf(s51, plain, ~spl8_23, inference(rat,[],[s34,s47,s50])).
% 0.70/0.36 cnf(s52, plain, spl8_24, inference(rat,[],[s37,s46,s41,s51])).
% 0.70/0.36 cnf(s53, plain, $false, inference(rat,[],[s36,s46,s41,s52,s51])).
% 0.70/0.36 thf(f504,plain,(
% 0.70/0.36 $false),
% 0.70/0.36 inference(avatar_sat_refutation,[],[s53])).
% 0.70/0.36 % SZS output end Proof for theBenchmark
% 0.70/0.36 % (625641)------------------------------
% 0.70/0.36 % (625641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.70/0.36 % (625641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.70/0.36 % (625641)CaDiCaL version: 2.1.3
% 0.70/0.36 % (625641)Termination reason: Refutation
% 0.70/0.36 % (625641)Time elapsed: 0.007 s
% 0.70/0.36 % (625641)Peak memory usage: 13 MB
% 0.70/0.36 % (625641)Instructions burned: 23 (million)
% 0.70/0.36 % (625593)Success in time 0.105 s
% 0.70/0.36 % Vampire exiting
%------------------------------------------------------------------------------