%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV529^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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:38:48 AM UTC 2026
% Result : Theorem 3.09s 0.89s
% Output : Refutation 3.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV529^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n002.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 15:59:52 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.25 Running higher-order theorem proving
% 0.21/0.28 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.72/0.41 % (1464364)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.72/0.41 % (1464375)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.72/0.41 % (1464375)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.72/0.41 % (1464375)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=1636299827:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.72/0.41 % (1464371)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3959202192:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.72/0.41 % (1464370)lrs+10_16_si=on:nwc=1.5:random_seed=2222600460:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.72/0.41 % (1464369)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3196132916:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.72/0.42 % (1464373)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=872032167:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.72/0.42 % (1464372)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=3107299318: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.72/0.42 % (1464374)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=850441377:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.72/0.42 % (1464371)Instruction limit reached!
% 0.72/0.42 % (1464371)------------------------------
% 0.72/0.42 % (1464371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.42 % (1464371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.42 % (1464371)CaDiCaL version: 2.1.3
% 0.72/0.42 % (1464371)Termination reason: Instruction limit
% 0.72/0.42 % (1464371)Termination phase: shuffling
% 0.72/0.42 % (1464371)Time elapsed: 0.003 s
% 0.72/0.42 % (1464371)Peak memory usage: 10 MB
% 0.72/0.42 % (1464371)Instructions burned: 5 (million)
% 0.72/0.42 % (1464370)Instruction limit reached!
% 0.72/0.42 % (1464370)------------------------------
% 0.72/0.42 % (1464370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.42 % (1464370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.42 % (1464370)CaDiCaL version: 2.1.3
% 0.72/0.42 % (1464370)Termination reason: Instruction limit
% 0.72/0.42 % (1464370)Termination phase: Property scanning
% 0.72/0.42 % (1464370)Time elapsed: 0.009 s
% 0.72/0.42 % (1464370)Peak memory usage: 10 MB
% 0.72/0.42 % (1464370)Instructions burned: 19 (million)
% 0.72/0.42 % (1464373)Instruction limit reached!
% 0.72/0.42 % (1464373)------------------------------
% 0.72/0.42 % (1464373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.42 % (1464373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.42 % (1464373)CaDiCaL version: 2.1.3
% 0.72/0.42 % (1464373)Termination reason: Instruction limit
% 0.72/0.42 % (1464373)Termination phase: Property scanning
% 0.72/0.42 % (1464373)Time elapsed: 0.011 s
% 0.72/0.42 % (1464373)Peak memory usage: 10 MB
% 0.72/0.42 % (1464373)Instructions burned: 25 (million)
% 0.72/0.42 % (1464383)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2278214156:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.72/0.42 % (1464375)Instruction limit reached!
% 0.72/0.42 % (1464375)------------------------------
% 0.72/0.42 % (1464375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.42 % (1464375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.42 % (1464375)CaDiCaL version: 2.1.3
% 0.72/0.42 % (1464375)Termination reason: Instruction limit
% 0.72/0.42 % (1464375)Termination phase: Property scanning
% 0.72/0.42 % (1464375)Time elapsed: 0.033 s
% 0.72/0.42 % (1464375)Peak memory usage: 12 MB
% 0.72/0.42 % (1464375)Instructions burned: 158 (million)
% 0.72/0.42 % (1464383)Instruction limit reached!
% 0.72/0.42 % (1464383)------------------------------
% 0.72/0.42 % (1464383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.45 % (1464383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.45 % (1464383)CaDiCaL version: 2.1.3
% 0.72/0.45 % (1464383)Termination reason: Instruction limit
% 0.72/0.45 % (1464383)Termination phase: shuffling
% 0.72/0.45 % (1464383)Time elapsed: 0.003 s
% 0.72/0.45 % (1464383)Peak memory usage: 10 MB
% 0.72/0.45 % (1464383)Instructions burned: 6 (million)
% 0.72/0.45 % (1464385)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.72/0.45 % (1464384)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2714265110:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.72/0.45 % (1464385)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2765365202:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.72/0.45 % (1464384)Instruction limit reached!
% 0.72/0.45 % (1464384)------------------------------
% 0.72/0.45 % (1464384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.45 % (1464384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.45 % (1464384)CaDiCaL version: 2.1.3
% 0.72/0.45 % (1464384)Termination reason: Instruction limit
% 0.72/0.45 % (1464384)Termination phase: shuffling
% 0.72/0.45 % (1464384)Time elapsed: 0.003 s
% 0.72/0.45 % (1464384)Peak memory usage: 10 MB
% 0.72/0.45 % (1464384)Instructions burned: 5 (million)
% 0.72/0.45 % (1464374)Instruction limit reached!
% 0.72/0.45 % (1464374)------------------------------
% 0.72/0.45 % (1464374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.45 % (1464374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.45 % (1464374)CaDiCaL version: 2.1.3
% 0.72/0.45 % (1464374)Termination reason: Instruction limit
% 0.72/0.45 % (1464374)Termination phase: Function definition elimination
% 0.72/0.45 % (1464374)Time elapsed: 0.033 s
% 0.72/0.45 % (1464374)Peak memory usage: 11 MB
% 0.72/0.45 % (1464374)Instructions burned: 77 (million)
% 0.72/0.45 % (1464385)Instruction limit reached!
% 0.72/0.45 % (1464385)------------------------------
% 0.72/0.45 % (1464385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.45 % (1464385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.45 % (1464385)CaDiCaL version: 2.1.3
% 0.72/0.45 % (1464385)Termination reason: Instruction limit
% 0.72/0.45 % (1464385)Termination phase: shuffling
% 0.72/0.45 % (1464385)Time elapsed: 0.004 s
% 0.72/0.45 % (1464385)Peak memory usage: 10 MB
% 0.72/0.45 % (1464385)Instructions burned: 8 (million)
% 0.72/0.45 % (1464387)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3122071884:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.72/0.45 % (1464387)Instruction limit reached!
% 0.72/0.45 % (1464387)------------------------------
% 0.72/0.45 % (1464387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.45 % (1464387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.45 % (1464387)CaDiCaL version: 2.1.3
% 0.72/0.45 % (1464387)Termination reason: Instruction limit
% 0.72/0.45 % (1464387)Termination phase: shuffling
% 0.72/0.45 % (1464387)Time elapsed: 0.004 s
% 0.72/0.45 % (1464387)Peak memory usage: 10 MB
% 0.72/0.45 % (1464387)Instructions burned: 15 (million)
% 0.72/0.45 % (1464388)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.72/0.45 % (1464388)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.72/0.45 % (1464388)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2331486897: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.72/0.45 % (1464393)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.72/0.45 % (1464391)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=4239231793:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.72/0.47 % (1464395)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1269809926:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.72/0.47 % (1464392)lrs+10_1_si=on:cs=on:random_seed=2643561878:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.72/0.47 % (1464393)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=3732748618:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.72/0.47 % (1464393)Instruction limit reached!
% 0.72/0.47 % (1464393)------------------------------
% 0.72/0.47 % (1464393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (1464393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (1464393)CaDiCaL version: 2.1.3
% 0.72/0.47 % (1464393)Termination reason: Instruction limit
% 0.72/0.47 % (1464393)Termination phase: shuffling
% 0.72/0.47 % (1464393)Time elapsed: 0.004 s
% 0.72/0.47 % (1464393)Peak memory usage: 10 MB
% 0.72/0.47 % (1464392)Instruction limit reached!
% 0.72/0.47 % (1464392)------------------------------
% 0.72/0.47 % (1464392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (1464393)Instructions burned: 7 (million)
% 0.72/0.47 % (1464392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (1464392)CaDiCaL version: 2.1.3
% 0.72/0.47 % (1464392)Termination reason: Instruction limit
% 0.72/0.47 % (1464392)Termination phase: shuffling
% 0.72/0.47 % (1464392)Time elapsed: 0.004 s
% 0.72/0.47 % (1464392)Peak memory usage: 10 MB
% 0.72/0.47 % (1464392)Instructions burned: 8 (million)
% 0.72/0.47 % (1464388)Instruction limit reached!
% 0.72/0.47 % (1464388)------------------------------
% 0.72/0.47 % (1464388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (1464388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (1464388)CaDiCaL version: 2.1.3
% 0.72/0.47 % (1464388)Termination reason: Instruction limit
% 0.72/0.47 % (1464388)Termination phase: Property scanning
% 0.72/0.47 % (1464388)Time elapsed: 0.013 s
% 0.72/0.47 % (1464388)Peak memory usage: 10 MB
% 0.72/0.47 % (1464388)Instructions burned: 30 (million)
% 0.72/0.47 % (1464395)Instruction limit reached!
% 0.72/0.47 % (1464395)------------------------------
% 0.72/0.47 % (1464395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (1464395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (1464395)CaDiCaL version: 2.1.3
% 0.72/0.47 % (1464395)Termination reason: Instruction limit
% 0.72/0.47 % (1464395)Termination phase: Saturation
% 0.72/0.47 % (1464395)Time elapsed: 0.009 s
% 0.72/0.47 % (1464395)Peak memory usage: 11 MB
% 0.72/0.47 % (1464395)Instructions burned: 39 (million)
% 0.72/0.47 % (1464369)Instruction limit reached!
% 0.72/0.47 % (1464369)------------------------------
% 0.72/0.47 % (1464369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (1464369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (1464369)CaDiCaL version: 2.1.3
% 0.72/0.47 % (1464369)Termination reason: Instruction limit
% 0.72/0.47 % (1464369)Termination phase: Function definition elimination
% 0.72/0.47 % (1464369)Time elapsed: 0.069 s
% 0.72/0.47 % (1464369)Peak memory usage: 11 MB
% 0.72/0.47 % (1464369)Instructions burned: 88 (million)
% 0.72/0.47 % (1464404)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2991383759:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.72/0.47 % (1464401)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3685869684:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.72/0.47 % (1464402)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3127094101:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.72/0.47 % (1464403)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3840014966:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.72/0.47 % (1464403)Instruction limit reached!
% 0.72/0.47 % (1464403)------------------------------
% 0.72/0.47 % (1464403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (1464403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.51 % (1464403)CaDiCaL version: 2.1.3
% 1.42/0.51 % (1464403)Termination reason: Instruction limit
% 1.42/0.51 % (1464403)Termination phase: shuffling
% 1.42/0.51 % (1464403)Time elapsed: 0.007 s
% 1.42/0.51 % (1464403)Peak memory usage: 10 MB
% 1.42/0.51 % (1464403)Instructions burned: 15 (million)
% 1.42/0.51 % (1464391)Instruction limit reached!
% 1.42/0.51 % (1464391)------------------------------
% 1.42/0.51 % (1464391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.51 % (1464391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.51 % (1464391)CaDiCaL version: 2.1.3
% 1.42/0.51 % (1464391)Termination reason: Instruction limit
% 1.42/0.51 % (1464391)Termination phase: Property scanning
% 1.42/0.51 % (1464391)Time elapsed: 0.035 s
% 1.42/0.51 % (1464391)Peak memory usage: 11 MB
% 1.42/0.51 % (1464391)Instructions burned: 88 (million)
% 1.42/0.51 % (1464405)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1672911067:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.42/0.51 % (1464402)Instruction limit reached!
% 1.42/0.51 % (1464402)------------------------------
% 1.42/0.51 % (1464402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.51 % (1464402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.51 % (1464402)CaDiCaL version: 2.1.3
% 1.42/0.51 % (1464402)Termination reason: Instruction limit
% 1.42/0.51 % (1464402)Termination phase: SInE selection
% 1.42/0.51 % (1464402)Time elapsed: 0.012 s
% 1.42/0.51 % (1464402)Peak memory usage: 10 MB
% 1.42/0.51 % (1464402)Instructions burned: 27 (million)
% 1.42/0.51 % (1464405)Instruction limit reached!
% 1.42/0.51 % (1464405)------------------------------
% 1.42/0.51 % (1464405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.51 % (1464405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.51 % (1464405)CaDiCaL version: 2.1.3
% 1.42/0.51 % (1464405)Termination reason: Instruction limit
% 1.42/0.51 % (1464405)Termination phase: shuffling
% 1.42/0.51 % (1464405)Time elapsed: 0.007 s
% 1.42/0.51 % (1464405)Peak memory usage: 10 MB
% 1.42/0.51 % (1464405)Instructions burned: 16 (million)
% 1.42/0.51 % (1464410)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=462567110:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.42/0.51 % (1464411)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2216490631:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.42/0.51 % (1464410)Instruction limit reached!
% 1.42/0.51 % (1464410)------------------------------
% 1.42/0.51 % (1464410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.51 % (1464410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.51 % (1464410)CaDiCaL version: 2.1.3
% 1.42/0.51 % (1464410)Termination reason: Instruction limit
% 1.42/0.51 % (1464410)Termination phase: shuffling
% 1.42/0.51 % (1464410)Time elapsed: 0.001 s
% 1.42/0.51 % (1464410)Peak memory usage: 10 MB
% 1.42/0.51 % (1464410)Instructions burned: 2 (million)
% 1.42/0.51 % (1464413)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=786452511:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.42/0.51 % (1464401)Refutation not found, incomplete strategy
% 1.42/0.51 % (1464401)------------------------------
% 1.42/0.51 % (1464401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.51 % (1464401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.51 % (1464401)CaDiCaL version: 2.1.3
% 1.42/0.51 % (1464401)Termination reason: Refutation not found, incomplete strategy
% 1.42/0.51 % (1464401)Time elapsed: 0.034 s
% 1.42/0.51 % (1464401)Peak memory usage: 13 MB
% 1.42/0.51 % (1464401)Instructions burned: 74 (million)
% 1.42/0.51 % (1464401)------------------------------
% 1.42/0.51 % (1464401)------------------------------
% 1.42/0.51 % (1464414)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=915130059:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.42/0.51 % (1464411)Instruction limit reached!
% 1.42/0.51 % (1464411)------------------------------
% 1.42/0.51 % (1464411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.09/0.60 % (1464411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.09/0.60 % (1464411)CaDiCaL version: 2.1.3
% 2.09/0.60 % (1464411)Termination reason: Instruction limit
% 2.09/0.60 % (1464411)Termination phase: Property scanning
% 2.09/0.60 % (1464411)Time elapsed: 0.011 s
% 2.09/0.60 % (1464411)Peak memory usage: 10 MB
% 2.09/0.60 % (1464411)Instructions burned: 27 (million)
% 2.09/0.60 % (1464413)Instruction limit reached!
% 2.09/0.60 % (1464413)------------------------------
% 2.09/0.60 % (1464413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.09/0.60 % (1464413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.09/0.60 % (1464413)CaDiCaL version: 2.1.3
% 2.09/0.60 % (1464413)Termination reason: Instruction limit
% 2.09/0.60 % (1464413)Termination phase: Property scanning
% 2.09/0.60 % (1464413)Time elapsed: 0.011 s
% 2.09/0.60 % (1464413)Peak memory usage: 10 MB
% 2.09/0.60 % (1464413)Instructions burned: 24 (million)
% 2.09/0.60 % (1464417)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
% 2.09/0.60 % (1464417)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.09/0.60 % (1464417)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=2637313734:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.09/0.60 % (1464419)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.09/0.60 % (1464419)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=2696599728:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.09/0.60 % (1464417)Instruction limit reached!
% 2.09/0.60 % (1464417)------------------------------
% 2.09/0.60 % (1464417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.09/0.60 % (1464417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.09/0.60 % (1464417)CaDiCaL version: 2.1.3
% 2.09/0.60 % (1464417)Termination reason: Instruction limit
% 2.09/0.60 % (1464417)Termination phase: shuffling
% 2.09/0.60 % (1464417)Time elapsed: 0.006 s
% 2.09/0.60 % (1464417)Peak memory usage: 10 MB
% 2.09/0.60 % (1464417)Instructions burned: 15 (million)
% 2.09/0.60 % (1464419)Instruction limit reached!
% 2.09/0.60 % (1464419)------------------------------
% 2.09/0.60 % (1464419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.09/0.60 % (1464419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.09/0.60 % (1464419)CaDiCaL version: 2.1.3
% 2.09/0.60 % (1464419)Termination reason: Instruction limit
% 2.09/0.60 % (1464419)Termination phase: shuffling
% 2.09/0.60 % (1464419)Time elapsed: 0.004 s
% 2.09/0.60 % (1464419)Peak memory usage: 10 MB
% 2.09/0.60 % (1464419)Instructions burned: 9 (million)
% 2.09/0.60 % (1464421)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=1261688832:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.09/0.60 % (1464404)Instruction limit reached!
% 2.09/0.60 % (1464404)------------------------------
% 2.09/0.60 % (1464404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.09/0.60 % (1464404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.09/0.60 % (1464404)CaDiCaL version: 2.1.3
% 2.09/0.60 % (1464404)Termination reason: Instruction limit
% 2.09/0.60 % (1464404)Termination phase: Saturation
% 2.09/0.60 % (1464404)Time elapsed: 0.070 s
% 2.09/0.60 % (1464404)Peak memory usage: 12 MB
% 2.09/0.60 % (1464404)Instructions burned: 330 (million)
% 2.09/0.60 % (1464414)Instruction limit reached!
% 2.09/0.60 % (1464414)------------------------------
% 2.09/0.60 % (1464414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.09/0.60 % (1464414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.09/0.60 % (1464414)CaDiCaL version: 2.1.3
% 2.09/0.60 % (1464414)Termination reason: Instruction limit
% 2.09/0.60 % (1464414)Termination phase: Saturation
% 2.09/0.60 % (1464414)Time elapsed: 0.027 s
% 2.09/0.60 % (1464414)Peak memory usage: 12 MB
% 2.09/0.60 % (1464414)Instructions burned: 61 (million)
% 2.35/0.67 % (1464422)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2279140752:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.35/0.67 % (1464421)Instruction limit reached!
% 2.35/0.67 % (1464421)------------------------------
% 2.35/0.67 % (1464421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.67 % (1464421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.67 % (1464421)CaDiCaL version: 2.1.3
% 2.35/0.67 % (1464421)Termination reason: Instruction limit
% 2.35/0.67 % (1464421)Termination phase: Property scanning
% 2.35/0.67 % (1464421)Time elapsed: 0.013 s
% 2.35/0.67 % (1464421)Peak memory usage: 10 MB
% 2.35/0.67 % (1464421)Instructions burned: 31 (million)
% 2.35/0.67 % (1464428)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2882839994:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.35/0.67 % (1464422)Instruction limit reached!
% 2.35/0.67 % (1464422)------------------------------
% 2.35/0.67 % (1464422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.67 % (1464425)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3024416067:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.35/0.67 % (1464422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.67 % (1464422)CaDiCaL version: 2.1.3
% 2.35/0.67 % (1464422)Termination reason: Instruction limit
% 2.35/0.67 % (1464422)Termination phase: shuffling
% 2.35/0.67 % (1464422)Time elapsed: 0.006 s
% 2.35/0.67 % (1464422)Peak memory usage: 10 MB
% 2.35/0.67 % (1464422)Instructions burned: 7 (million)
% 2.35/0.67 % (1464427)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=99149987:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.35/0.67 % (1464429)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3026462415:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.35/0.67 % (1464425)Instruction limit reached!
% 2.35/0.67 % (1464425)------------------------------
% 2.35/0.67 % (1464425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.67 % (1464425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.67 % (1464425)CaDiCaL version: 2.1.3
% 2.35/0.67 % (1464425)Termination reason: Instruction limit
% 2.35/0.67 % (1464425)Termination phase: Property scanning
% 2.35/0.67 % (1464425)Time elapsed: 0.010 s
% 2.35/0.67 % (1464425)Peak memory usage: 10 MB
% 2.35/0.67 % (1464425)Instructions burned: 23 (million)
% 2.35/0.67 % (1464427)Instruction limit reached!
% 2.35/0.67 % (1464427)------------------------------
% 2.35/0.67 % (1464427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.67 % (1464427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.67 % (1464427)CaDiCaL version: 2.1.3
% 2.35/0.67 % (1464427)Termination reason: Instruction limit
% 2.35/0.67 % (1464427)Termination phase: Property scanning
% 2.35/0.67 % (1464427)Time elapsed: 0.009 s
% 2.35/0.67 % (1464427)Peak memory usage: 10 MB
% 2.35/0.67 % (1464427)Instructions burned: 21 (million)
% 2.35/0.67 % (1464437)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.35/0.67 % (1464431)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=661058791:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.35/0.67 % (1464437)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1630047901:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.35/0.67 % (1464438)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1997960524:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.35/0.67 % (1464435)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=348377115:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 2.35/0.67 % (1464437)Instruction limit reached!
% 2.35/0.67 % (1464437)------------------------------
% 2.35/0.67 % (1464437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.67 % (1464437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.72 % (1464437)CaDiCaL version: 2.1.3
% 2.56/0.72 % (1464437)Termination reason: Instruction limit
% 2.56/0.72 % (1464437)Termination phase: shuffling
% 2.56/0.72 % (1464437)Time elapsed: 0.003 s
% 2.56/0.72 % (1464437)Peak memory usage: 10 MB
% 2.56/0.72 % (1464437)Instructions burned: 7 (million)
% 2.56/0.72 % (1464435)Instruction limit reached!
% 2.56/0.72 % (1464435)------------------------------
% 2.56/0.72 % (1464435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.56/0.72 % (1464435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.72 % (1464435)CaDiCaL version: 2.1.3
% 2.56/0.72 % (1464435)Termination reason: Instruction limit
% 2.56/0.72 % (1464435)Termination phase: Function definition elimination
% 2.56/0.72 % (1464435)Time elapsed: 0.018 s
% 2.56/0.72 % (1464435)Peak memory usage: 11 MB
% 2.56/0.72 % (1464435)Instructions burned: 43 (million)
% 2.56/0.72 % (1464443)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=1715498329:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.56/0.72 % (1464444)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.56/0.72 % (1464429)Instruction limit reached!
% 2.56/0.72 % (1464429)------------------------------
% 2.56/0.72 % (1464429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.56/0.72 % (1464429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.72 % (1464429)CaDiCaL version: 2.1.3
% 2.56/0.72 % (1464429)Termination reason: Instruction limit
% 2.56/0.72 % (1464429)Termination phase: Twee Goal Transformation
% 2.56/0.72 % (1464429)Time elapsed: 0.056 s
% 2.56/0.72 % (1464429)Peak memory usage: 11 MB
% 2.56/0.72 % (1464429)Instructions burned: 143 (million)
% 2.56/0.72 % (1464444)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=291179597:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.56/0.72 % (1464444)Instruction limit reached!
% 2.56/0.72 % (1464444)------------------------------
% 2.56/0.72 % (1464444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.56/0.72 % (1464444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.72 % (1464444)CaDiCaL version: 2.1.3
% 2.56/0.72 % (1464444)Termination reason: Instruction limit
% 2.56/0.72 % (1464444)Termination phase: shuffling
% 2.56/0.72 % (1464444)Time elapsed: 0.003 s
% 2.56/0.72 % (1464444)Peak memory usage: 10 MB
% 2.56/0.72 % (1464444)Instructions burned: 7 (million)
% 2.56/0.72 % (1464446)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3619178340:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.56/0.72 % (1464448)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2666577576:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.56/0.72 % (1464446)Instruction limit reached!
% 2.56/0.72 % (1464446)------------------------------
% 2.56/0.72 % (1464446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.56/0.72 % (1464446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.72 % (1464446)CaDiCaL version: 2.1.3
% 2.56/0.72 % (1464446)Termination reason: Instruction limit
% 2.56/0.72 % (1464446)Termination phase: Property scanning
% 2.56/0.72 % (1464446)Time elapsed: 0.010 s
% 2.56/0.72 % (1464446)Peak memory usage: 10 MB
% 2.56/0.72 % (1464446)Instructions burned: 23 (million)
% 2.56/0.72 % (1464448)Instruction limit reached!
% 2.56/0.72 % (1464448)------------------------------
% 2.56/0.72 % (1464448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.56/0.72 % (1464448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.72 % (1464448)CaDiCaL version: 2.1.3
% 2.56/0.72 % (1464448)Termination reason: Instruction limit
% 2.56/0.72 % (1464448)Termination phase: Property scanning
% 2.56/0.72 % (1464448)Time elapsed: 0.010 s
% 2.56/0.72 % (1464448)Peak memory usage: 10 MB
% 2.56/0.72 % (1464448)Instructions burned: 21 (million)
% 2.56/0.72 % (1464451)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=4152299241:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 3.09/0.81 % (1464443)Instruction limit reached!
% 3.09/0.81 % (1464443)------------------------------
% 3.09/0.81 % (1464443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.81 % (1464443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.81 % (1464443)CaDiCaL version: 2.1.3
% 3.09/0.81 % (1464443)Termination reason: Instruction limit
% 3.09/0.81 % (1464443)Termination phase: Saturation
% 3.09/0.81 % (1464443)Time elapsed: 0.068 s
% 3.09/0.81 % (1464443)Peak memory usage: 12 MB
% 3.09/0.81 % (1464443)Instructions burned: 169 (million)
% 3.09/0.81 % (1464438)Instruction limit reached!
% 3.09/0.81 % (1464438)------------------------------
% 3.09/0.81 % (1464438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.81 % (1464438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.81 % (1464438)CaDiCaL version: 2.1.3
% 3.09/0.81 % (1464438)Termination reason: Instruction limit
% 3.09/0.81 % (1464438)Termination phase: Saturation
% 3.09/0.81 % (1464438)Time elapsed: 0.091 s
% 3.09/0.81 % (1464438)Peak memory usage: 14 MB
% 3.09/0.81 % (1464438)Instructions burned: 181 (million)
% 3.09/0.81 % (1464452)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=3066759315:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 3.09/0.81 % (1464454)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=244871255:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.09/0.81 % (1464455)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1740060349:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.09/0.81 % (1464454)Instruction limit reached!
% 3.09/0.81 % (1464454)------------------------------
% 3.09/0.81 % (1464454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.81 % (1464454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.81 % (1464454)CaDiCaL version: 2.1.3
% 3.09/0.81 % (1464454)Termination reason: Instruction limit
% 3.09/0.81 % (1464454)Termination phase: Preprocessing 3
% 3.09/0.81 % (1464454)Time elapsed: 0.020 s
% 3.09/0.81 % (1464454)Peak memory usage: 11 MB
% 3.09/0.81 % (1464454)Instructions burned: 46 (million)
% 3.09/0.81 % (1464372)Instruction limit reached!
% 3.09/0.81 % (1464372)------------------------------
% 3.09/0.81 % (1464372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.81 % (1464372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.81 % (1464372)CaDiCaL version: 2.1.3
% 3.09/0.81 % (1464372)Termination reason: Instruction limit
% 3.09/0.81 % (1464372)Termination phase: Saturation
% 3.09/0.81 % (1464372)Time elapsed: 0.320 s
% 3.09/0.81 % (1464372)Peak memory usage: 16 MB
% 3.09/0.81 % (1464372)Instructions burned: 634 (million)
% 3.09/0.81 % (1464455)Refutation not found, incomplete strategy
% 3.09/0.81 % (1464455)------------------------------
% 3.09/0.81 % (1464455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.81 % (1464455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.81 % (1464455)CaDiCaL version: 2.1.3
% 3.09/0.81 % (1464455)Termination reason: Refutation not found, incomplete strategy
% 3.09/0.81 % (1464455)Time elapsed: 0.026 s
% 3.09/0.81 % (1464455)Peak memory usage: 13 MB
% 3.09/0.81 % (1464455)Instructions burned: 55 (million)
% 3.09/0.81 % (1464455)------------------------------
% 3.09/0.81 % (1464455)------------------------------
% 3.09/0.81 % (1464459)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=692954962:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 3.09/0.81 % (1464460)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.09/0.81 % (1464431)Instruction limit reached!
% 3.09/0.81 % (1464431)------------------------------
% 3.09/0.81 % (1464431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.81 % (1464431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.81 % (1464431)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464431)Termination reason: Instruction limit
% 3.09/0.89 % (1464431)Termination phase: Saturation
% 3.09/0.89 % (1464431)Time elapsed: 0.157 s
% 3.09/0.89 % (1464431)Peak memory usage: 14 MB
% 3.09/0.89 % (1464431)Instructions burned: 193 (million)
% 3.09/0.89 % (1464460)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=734930317:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.09/0.89 % (1464461)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2533060923:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.09/0.89 % (1464459)Instruction limit reached!
% 3.09/0.89 % (1464459)------------------------------
% 3.09/0.89 % (1464459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464459)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464459)Termination reason: Instruction limit
% 3.09/0.89 % (1464459)Termination phase: Property scanning
% 3.09/0.89 % (1464459)Time elapsed: 0.009 s
% 3.09/0.89 % (1464459)Peak memory usage: 10 MB
% 3.09/0.89 % (1464459)Instructions burned: 21 (million)
% 3.09/0.89 % (1464461)Instruction limit reached!
% 3.09/0.89 % (1464461)------------------------------
% 3.09/0.89 % (1464461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464461)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464461)Termination reason: Instruction limit
% 3.09/0.89 % (1464461)Termination phase: shuffling
% 3.09/0.89 % (1464461)Time elapsed: 0.007 s
% 3.09/0.89 % (1464461)Peak memory usage: 10 MB
% 3.09/0.89 % (1464461)Instructions burned: 14 (million)
% 3.09/0.89 % (1464463)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=621284718:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.09/0.89 % (1464466)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3585805813:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.09/0.89 % (1464467)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1592025160:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 3.09/0.89 % (1464467)Instruction limit reached!
% 3.09/0.89 % (1464467)------------------------------
% 3.09/0.89 % (1464467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464467)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464467)Termination reason: Instruction limit
% 3.09/0.89 % (1464467)Termination phase: Property scanning
% 3.09/0.89 % (1464467)Time elapsed: 0.013 s
% 3.09/0.89 % (1464467)Peak memory usage: 10 MB
% 3.09/0.89 % (1464467)Instructions burned: 31 (million)
% 3.09/0.89 % (1464466)Instruction limit reached!
% 3.09/0.89 % (1464466)------------------------------
% 3.09/0.89 % (1464466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464466)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464466)Termination reason: Instruction limit
% 3.09/0.89 % (1464466)Termination phase: Function definition elimination
% 3.09/0.89 % (1464466)Time elapsed: 0.022 s
% 3.09/0.89 % (1464466)Peak memory usage: 11 MB
% 3.09/0.89 % (1464466)Instructions burned: 53 (million)
% 3.09/0.89 % (1464463)Instruction limit reached!
% 3.09/0.89 % (1464463)------------------------------
% 3.09/0.89 % (1464463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464463)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464463)Termination reason: Instruction limit
% 3.09/0.89 % (1464463)Termination phase: Function definition elimination
% 3.09/0.89 % (1464463)Time elapsed: 0.028 s
% 3.09/0.89 % (1464463)Peak memory usage: 11 MB
% 3.09/0.89 % (1464463)Instructions burned: 67 (million)
% 3.09/0.89 % (1464451)Instruction limit reached!
% 3.09/0.89 % (1464451)------------------------------
% 3.09/0.89 % (1464451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464451)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464451)Termination reason: Instruction limit
% 3.09/0.89 % (1464451)Termination phase: Saturation
% 3.09/0.89 % (1464451)Time elapsed: 0.125 s
% 3.09/0.89 % (1464451)Peak memory usage: 12 MB
% 3.09/0.89 % (1464451)Instructions burned: 317 (million)
% 3.09/0.89 % (1464471)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2724102256:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.09/0.89 % (1464472)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=2479638922:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.09/0.89 % (1464473)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2310683941:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.09/0.89 % (1464474)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.09/0.89 % (1464474)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2612653962:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 3.09/0.89 % (1464472)Instruction limit reached!
% 3.09/0.89 % (1464472)------------------------------
% 3.09/0.89 % (1464472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464472)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464472)Termination reason: Instruction limit
% 3.09/0.89 % (1464472)Termination phase: Property scanning
% 3.09/0.89 % (1464472)Time elapsed: 0.015 s
% 3.09/0.89 % (1464472)Peak memory usage: 10 MB
% 3.09/0.89 % (1464472)Instructions burned: 36 (million)
% 3.09/0.89 % (1464460)Instruction limit reached!
% 3.09/0.89 % (1464460)------------------------------
% 3.09/0.89 % (1464460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464460)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464460)Termination reason: Instruction limit
% 3.09/0.89 % (1464460)Termination phase: Saturation
% 3.09/0.89 % (1464460)Time elapsed: 0.079 s
% 3.09/0.89 % (1464460)Peak memory usage: 12 MB
% 3.09/0.89 % (1464460)Instructions burned: 202 (million)
% 3.09/0.89 % (1464473)Instruction limit reached!
% 3.09/0.89 % (1464473)------------------------------
% 3.09/0.89 % (1464473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464473)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464473)Termination reason: Instruction limit
% 3.09/0.89 % (1464473)Termination phase: Function definition elimination
% 3.09/0.89 % (1464473)Time elapsed: 0.028 s
% 3.09/0.89 % (1464473)Peak memory usage: 11 MB
% 3.09/0.89 % (1464473)Instructions burned: 68 (million)
% 3.09/0.89 % (1464428)Instruction limit reached!
% 3.09/0.89 % (1464428)------------------------------
% 3.09/0.89 % (1464428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464428)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464428)Termination reason: Instruction limit
% 3.09/0.89 % (1464428)Termination phase: Saturation
% 3.09/0.89 % (1464428)Time elapsed: 0.283 s
% 3.09/0.89 % (1464428)Peak memory usage: 34 MB
% 3.09/0.89 % (1464428)Instructions burned: 1245 (million)
% 3.09/0.89 % (1464479)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2947125387:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 3.09/0.89 % (1464480)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=425414858:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 3.09/0.89 % (1464483)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2732606011:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 3.09/0.89 % (1464481)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=470817527:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 3.09/0.89 % (1464471)Instruction limit reached!
% 3.09/0.89 % (1464471)------------------------------
% 3.09/0.89 % (1464471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464471)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464471)Termination reason: Instruction limit
% 3.09/0.89 % (1464471)Termination phase: Saturation
% 3.09/0.89 % (1464471)Time elapsed: 0.074 s
% 3.09/0.89 % (1464471)Peak memory usage: 13 MB
% 3.09/0.89 % (1464471)Instructions burned: 137 (million)
% 3.09/0.89 % (1464480)Instruction limit reached!
% 3.09/0.89 % (1464480)------------------------------
% 3.09/0.89 % (1464480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464480)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464480)Termination reason: Instruction limit
% 3.09/0.89 % (1464480)Termination phase: Twee Goal Transformation
% 3.09/0.89 % (1464480)Time elapsed: 0.039 s
% 3.09/0.89 % (1464480)Peak memory usage: 11 MB
% 3.09/0.89 % (1464480)Instructions burned: 97 (million)
% 3.09/0.89 % (1464474)Instruction limit reached!
% 3.09/0.89 % (1464474)------------------------------
% 3.09/0.89 % (1464474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464474)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464474)Termination reason: Instruction limit
% 3.09/0.89 % (1464474)Termination phase: Property scanning
% 3.09/0.89 % (1464474)Time elapsed: 0.070 s
% 3.09/0.89 % (1464474)Peak memory usage: 11 MB
% 3.09/0.89 % (1464474)Instructions burned: 181 (million)
% 3.09/0.89 % (1464487)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=477008026:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 3.09/0.89 % (1464488)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=455590970:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 3.09/0.89 % (1464489)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2265668638:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 3.09/0.89 % (1464489)Instruction limit reached!
% 3.09/0.89 % (1464489)------------------------------
% 3.09/0.89 % (1464489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464489)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464489)Termination reason: Instruction limit
% 3.09/0.89 % (1464489)Termination phase: Function definition elimination
% 3.09/0.89 % (1464489)Time elapsed: 0.019 s
% 3.09/0.89 % (1464489)Peak memory usage: 10 MB
% 3.09/0.89 % (1464489)Instructions burned: 45 (million)
% 3.09/0.89 % (1464479)Instruction limit reached!
% 3.09/0.89 % (1464479)------------------------------
% 3.09/0.89 % (1464479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464479)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464479)Termination reason: Instruction limit
% 3.09/0.89 % (1464479)Termination phase: Saturation
% 3.09/0.89 % (1464479)Time elapsed: 0.099 s
% 3.09/0.89 % (1464479)Peak memory usage: 12 MB
% 3.09/0.89 % (1464479)Instructions burned: 248 (million)
% 3.09/0.89 % (1464493)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=716065564:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 3.09/0.89 % (1464481) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1464364-1464481"...
% 3.09/0.89 % (1464494)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=1671795654:i=450:rtra=on:ixr=off:ntd=on_2994 on theBenchmark for (2994ds/450Mi)
% 3.09/0.89 % (1464481)...printing done.
% 3.09/0.89 % (1464481)Refutation found. Thanks to Tanya!
% 3.09/0.89 % SZS status Theorem for theBenchmark
% 3.09/0.89 % SZS output start Proof for theBenchmark
% 3.09/0.89 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 3.09/0.89 thf(func_def_0, type, c_Eps_i: (($i > $o) > $i)).
% 3.09/0.89 thf(func_def_1, type, c_False: $o).
% 3.09/0.89 thf(func_def_2, type, c_True: $o).
% 3.09/0.89 thf(func_def_3, type, c_not: ($o > $o)).
% 3.09/0.89 thf(func_def_4, type, c_and: ($o > $o > $o)).
% 3.09/0.89 thf(func_def_5, type, c_or: ($o > $o > $o)).
% 3.09/0.89 thf(func_def_6, type, c_iff: ($o > $o > $o)).
% 3.09/0.89 thf(func_def_7, type, c_In: ($i > $i > $o)).
% 3.09/0.89 thf(func_def_8, type, c_Subq: ($i > $i > $o)).
% 3.09/0.89 thf(func_def_10, type, c_Union: ($i > $i)).
% 3.09/0.89 thf(func_def_11, type, c_Power: ($i > $i)).
% 3.09/0.89 thf(func_def_12, type, c_Repl: ($i > ($i > $i) > $i)).
% 3.09/0.89 thf(func_def_13, type, c_TransSet: ($i > $o)).
% 3.09/0.89 thf(func_def_14, type, c_atleast2: ($i > $o)).
% 3.09/0.89 thf(func_def_15, type, c_atleast3: ($i > $o)).
% 3.09/0.89 thf(func_def_16, type, c_atleast4: ($i > $o)).
% 3.09/0.89 thf(func_def_17, type, c_atleast5: ($i > $o)).
% 3.09/0.89 thf(func_def_18, type, c_atleast6: ($i > $o)).
% 3.09/0.89 thf(func_def_19, type, c_exactly2: ($i > $o)).
% 3.09/0.89 thf(func_def_20, type, c_exactly3: ($i > $o)).
% 3.09/0.89 thf(func_def_21, type, c_exactly4: ($i > $o)).
% 3.09/0.89 thf(func_def_22, type, c_exactly5: ($i > $o)).
% 3.09/0.89 thf(func_def_23, type, c_exu_i: (($i > $o) > $o)).
% 3.09/0.89 thf(func_def_24, type, c_reflexive_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_25, type, c_irreflexive_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_26, type, c_symmetric_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_27, type, c_antisymmetric_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_28, type, c_transitive_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_29, type, c_eqreln_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_30, type, c_per_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_31, type, c_linear_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_32, type, c_trichotomous_or_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_33, type, c_partialorder_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_34, type, c_totalorder_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_35, type, c_strictpartialorder_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_36, type, c_stricttotalorder_i: (($i > $i > $o) > $o)).
% 3.09/0.89 thf(func_def_37, type, c_If_i: ($o > $i > $i > $i)).
% 3.09/0.89 thf(func_def_38, type, c_exactly1of2: ($o > $o > $o)).
% 3.09/0.89 thf(func_def_39, type, c_exactly1of3: ($o > $o > $o > $o)).
% 3.09/0.89 thf(func_def_40, type, c_nIn: ($i > $i > $o)).
% 3.09/0.89 thf(func_def_41, type, c_nSubq: ($i > $i > $o)).
% 3.09/0.89 thf(func_def_42, type, c_UPair: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_43, type, c_Sing: ($i > $i)).
% 3.09/0.89 thf(func_def_44, type, c_binunion: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_45, type, c_SetAdjoin: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_46, type, c_famunion: ($i > ($i > $i) > $i)).
% 3.09/0.89 thf(func_def_47, type, c_Sep: ($i > ($i > $o) > $i)).
% 3.09/0.89 thf(func_def_48, type, c_ReplSep: ($i > ($i > $o) > ($i > $i) > $i)).
% 3.09/0.89 thf(func_def_49, type, c_binintersect: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_50, type, c_setminus: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_51, type, c_inj: ($i > $i > ($i > $i) > $o)).
% 3.09/0.89 thf(func_def_52, type, c_bij: ($i > $i > ($i > $i) > $o)).
% 3.09/0.89 thf(func_def_53, type, c_atleastp: ($i > $i > $o)).
% 3.09/0.89 thf(func_def_54, type, c_equip: ($i > $i > $o)).
% 3.09/0.89 thf(func_def_55, type, c_In_rec_poly_G_i: (($i > ($i > $i) > $i) > $i > $i > $o)).
% 3.09/0.89 thf(func_def_56, type, c_In_rec_poly_i: (($i > ($i > $i) > $i) > $i > $i)).
% 3.09/0.89 thf(func_def_57, type, c_ordsucc: ($i > $i)).
% 3.09/0.89 thf(func_def_58, type, c_nat_p: ($i > $o)).
% 3.09/0.89 thf(func_def_59, type, c_nat_primrec: ($i > ($i > $i > $i) > $i > $i)).
% 3.09/0.89 thf(func_def_60, type, c_add_nat: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_61, type, c_mul_nat: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_62, type, c_ordinal: ($i > $o)).
% 3.09/0.89 thf(func_def_63, type, c_V_: ($i > $i)).
% 3.09/0.89 thf(func_def_64, type, c_Inj1: ($i > $i)).
% 3.09/0.89 thf(func_def_65, type, c_Inj0: ($i > $i)).
% 3.09/0.89 thf(func_def_66, type, c_Unj: ($i > $i)).
% 3.09/0.89 thf(func_def_67, type, c_combine_funcs: ($i > $i > ($i > $i) > ($i > $i) > $i > $i)).
% 3.09/0.89 thf(func_def_68, type, c_setsum: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_69, type, c_proj0: ($i > $i)).
% 3.09/0.89 thf(func_def_70, type, c_proj1: ($i > $i)).
% 3.09/0.89 thf(func_def_71, type, c_binrep: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_72, type, c_lam: ($i > ($i > $i) > $i)).
% 3.09/0.89 thf(func_def_73, type, c_setprod: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_74, type, c_ap: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_75, type, c_setsum_p: ($i > $o)).
% 3.09/0.89 thf(func_def_76, type, c_tuple_p: ($i > $i > $o)).
% 3.09/0.89 thf(func_def_77, type, c_Pi: ($i > ($i > $i) > $i)).
% 3.09/0.89 thf(func_def_78, type, c_setexp: ($i > $i > $i)).
% 3.09/0.89 thf(func_def_79, type, c_Sep2: ($i > ($i > $i) > ($i > $i > $o) > $i)).
% 3.09/0.89 thf(func_def_80, type, c_set_of_pairs: ($i > $o)).
% 3.09/0.89 thf(func_def_81, type, c_lam2: ($i > ($i > $i) > ($i > $i > $i) > $i)).
% 3.09/0.89 thf(func_def_82, type, c_PNoEq_: ($i > ($i > $o) > ($i > $o) > $o)).
% 3.09/0.89 thf(func_def_83, type, c_PNoLt_: ($i > ($i > $o) > ($i > $o) > $o)).
% 3.09/0.89 thf(func_def_84, type, c_PNoLt: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 3.09/0.89 thf(func_def_85, type, c_PNoLe: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 3.09/0.89 thf(func_def_86, type, c_PNo_downc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 3.09/0.89 thf(func_def_87, type, c_PNo_upc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 3.09/0.89 thf(func_def_88, type, c_SNoElts_: ($i > $i)).
% 3.09/0.89 thf(func_def_89, type, c_SNo_: ($i > $i > $o)).
% 3.09/0.89 thf(func_def_90, type, c_PSNo: ($i > ($i > $o) > $i)).
% 3.09/0.89 thf(func_def_91, type, c_SNo: ($i > $o)).
% 3.09/0.89 thf(func_def_92, type, c_SNoLev: ($i > $i)).
% 3.09/0.89 thf(func_def_93, type, c_SNoEq_: ($i > $i > $i > $o)).
% 3.09/0.89 thf(func_def_94, type, c_SNoLt: ($i > $i > $o)).
% 3.09/0.89 thf(func_def_95, type, c_SNoLe: ($i > $i > $o)).
% 3.09/0.89 thf(func_def_96, type, c_binop_on: ($i > ($i > $i > $i) > $o)).
% 3.09/0.89 thf(func_def_97, type, c_Loop: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > $o)).
% 3.09/0.89 thf(func_def_98, type, c_Loop_with_defs: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 3.09/0.89 thf(func_def_99, type, c_Loop_with_defs_cex1: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 3.09/0.89 thf(func_def_100, type, c_Loop_with_defs_cex2: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 3.09/0.89 thf(func_def_101, type, c_combinator: ($i > $o)).
% 3.09/0.89 thf(func_def_102, type, c_combinator_equiv: ($i > $i > $o)).
% 3.09/0.89 thf(func_def_103, type, c_equip_mod: ($i > $i > $i > $o)).
% 3.09/0.89 thf(func_def_105, type, db2: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_106, type, db0: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_107, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.09/0.89 thf(func_def_108, type, db1: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_109, type, db13: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_110, type, db12: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_111, type, db11: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_112, type, db10: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_113, type, db9: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_114, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.09/0.89 thf(func_def_115, type, vIMP: ($o > $o > $o)).
% 3.09/0.89 thf(func_def_116, type, db14: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_117, type, db15: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_118, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.09/0.89 thf(func_def_119, type, db16: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_120, type, db8: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_121, type, db5: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_122, type, db4: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_123, type, db3: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_124, type, db7: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_125, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.09/0.89 thf(func_def_128, type, db6: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_129, type, db17: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_130, type, db18: !>[X0: $tType]:(X0)).
% 3.09/0.89 thf(func_def_131, type, sK0: ((($i > (($i > $i) > $i) > $i) > $i > $i > ($i > $i) > $i > $i) > $i > (($i > $i) > $i > $i) > $o)).
% 3.09/0.89 thf(func_def_132, type, sK1: (($i > $i > $i) > (($i > $i) > $i) > $o)).
% 3.09/0.89 thf(func_def_133, type, sK2: ((($i > $i) > $i) > ($i > $i) > ($i > $i) > $i > $o)).
% 3.09/0.89 thf(func_def_134, type, sK3: (($i > $i) > $i > $o)).
% 3.09/0.89 thf(func_def_135, type, sK4: (($i > $o) > $i)).
% 3.09/0.89 thf(func_def_136, type, vNOT: ($o > $o)).
% 3.09/0.89 thf(func_def_138, type, sK6: (($i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i)).
% 3.09/0.89 thf(func_def_139, type, sK7: ((($i > $i) > (($i > $i) > $i > $i) > $i > $i) > $i)).
% 3.09/0.89 thf(func_def_140, type, sK8: (($i > $i) > ($i > $i > $i) > ($i > ($i > $i) > $i) > ($i > $i > $i) > $i > $i)).
% 3.09/0.89 thf(func_def_142, type, sK10: (($i > ($i > $i) > $i > $i) > ($i > $i) > ($i > ($i > (($i > $i) > $i) > $i) > $i > $i > ($i > $i) > $i > $i) > ($i > ($i > $i) > $i > $i) > $i > (($i > $i) > $i) > $i)).
% 3.09/0.89 thf(func_def_143, type, sK11: ((($i > $i) > (($i > $i) > $i > $i) > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i > $i) > $i)).
% 3.09/0.89 thf(func_def_144, type, sK12: (($i > $i) > ($i > $i > $i) > $i)).
% 3.09/0.89 thf(func_def_145, type, sK13: ((($i > $i) > (($i > $i) > $i > $i) > $i) > $i)).
% 3.09/0.89 thf(f5,axiom,(
% 3.09/0.89 (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 3.09/0.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5)).
% 3.09/0.89 thf(f13,axiom,(
% 3.09/0.89 (c_not = (^[X0 : $o] : (X0 => c_False)))),
% 3.09/0.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13)).
% 3.09/0.89 thf(f70,axiom,(
% 3.09/0.89 (c_Inj0 = (^[X0 : $i] : ((c_Repl @ X0 @ (^[X1 : $i] : ((c_Inj1 @ X1)))))))),
% 3.09/0.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax70)).
% 3.09/0.89 thf(f73,axiom,(
% 3.09/0.89 ((^[X0 : $i, X1 : $i] : ((c_binunion @ (c_Repl @ X0 @ (^[X2 : $i] : ((c_Inj0 @ X2)))) @ (c_Repl @ X1 @ (^[X2 : $i] : ((c_Inj1 @ X2))))))) = c_setsum)),
% 3.09/0.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax73)).
% 3.09/0.89 thf(f109,conjecture,(
% 3.09/0.89 ! [X0 : (($i > $i) > $i > $o),X3 : ((($i > $i) > $i) > ($i > $i) > ($i > $i) > $i > $o),X1 : (($i > $i > $i) > (($i > $i) > $i) > $o),X2 : ((($i > (($i > $i) > $i) > $i) > $i > $i > ($i > $i) > $i > $i) > $i > (($i > $i) > $i > $i) > $o)] : (! [X5 : $i,X4 : $i,X6 : ($i > ($i > $i) > $i),X7 : $i] : (X3 @ (^[X8 : ($i > $i)] : ((c_Inj0 @ (X8 @ c_Empty)))) @ (^[X8 : $i] : (X5)) @ (^[X8 : $i] : ((X6 @ c_Empty @ (^[X9 : $i] : (c_Empty))))) @ (c_Inj1 @ c_Empty)) => (! [X5 : $i,X4 : ($i > ($i > $i) > $i > $i > $i),X7 : $i,X6 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i)] : ((X3 @ (^[X8 : ($i > $i)] : ((c_Inj1 @ (c_Inj1 @ (X6 @ (^[X9 : (($i > $i) > $i), X10 : ($i > $i), X11 : $i] : ((c_setsum @ c_Empty @ c_Empty)))))))) @ (^[X8 : $i] : ((c_setsum @ c_Empty @ (c_Inj1 @ X8)))) @ (^[X8 : $i] : (c_Empty)) @ (c_Inj0 @ (c_Inj1 @ c_Empty))) => (c_In @ (c_Inj1 @ c_Empty) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ c_Empty))) => (! [X7 : (($i > $i > $i > $i) > $i),X5 : ((($i > $i > $i) > $i) > $i),X4 : ($i > $i > $i),X6 : ($i > ($i > $i > $i) > $i)] : (X2 @ (^[X8 : ($i > (($i > $i) > $i) > $i), X9 : $i, X10 : $i, X11 : ($i > $i), X12 : $i] : ((c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ X12)))) @ (c_setsum @ (c_Inj1 @ (c_Inj1 @ c_Empty)) @ c_Empty) @ (^[X8 : ($i > $i), X9 : $i] : ((c_setsum @ X9 @ (X7 @ (^[X10 : $i, X11 : $i, X12 : $i] : (c_Empty))))))) => (! [X4 : (($i > ($i > $i) > $i > $i) > $i),X5 : $i,X6 : ($i > (($i > $i) > $i > $i) > $i > $i),X7 : $i] : ((c_In @ (c_Inj0 @ (c_Inj1 @ X7)) @ (X4 @ (^[X8 : $i, X9 : ($i > $i), X10 : $i] : (c_Empty)))) => ((X2 @ (^[X8 : ($i > (($i > $i) > $i) > $i), X9 : $i, X10 : $i, X11 : ($i > $i), X12 : $i] : ((c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty)))))) @ (c_setsum @ (X4 @ (^[X8 : $i, X9 : ($i > $i), X10 : $i] : (c_Empty))) @ c_Empty) @ (^[X8 : ($i > $i), X9 : $i] : ((c_Inj1 @ c_Empty)))) => (X2 @ (^[X8 : ($i > (($i > $i) > $i) > $i), X9 : $i, X10 : $i, X11 : ($i > $i), X12 : $i] : ((c_Inj0 @ (c_Inj0 @ c_Empty)))) @ c_Empty @ (^[X8 : ($i > $i), X9 : $i] : ((c_Inj0 @ (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty)))))))) => (! [X7 : ($i > $i),X6 : (($i > $i > $i > $i) > $i),X4 : $i,X5 : (($i > $i > $i) > $i > $i)] : ((c_In @ (X6 @ (^[X8 : $i, X9 : $i, X10 : $i] : ((c_Inj1 @ X9)))) @ (c_setsum @ (c_Inj0 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty))))) => ((X0 @ (^[X8 : $i] : (X8)) @ (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj1 @ (c_Inj1 @ c_Empty)))) => (X1 @ (^[X8 : $i, X9 : $i] : ((c_setsum @ (c_setsum @ (c_Inj1 @ X9) @ (c_Inj1 @ c_Empty)) @ (c_setsum @ c_Empty @ (X7 @ (X7 @ c_Empty)))))) @ (^[X8 : ($i > $i)] : (c_Empty))))) => (! [X6 : ($i > $i),X7 : $i,X4 : $i,X5 : $i] : ((X1 @ (^[X8 : $i, X9 : $i] : (X8)) @ (^[X8 : ($i > $i)] : ((c_setsum @ (c_setsum @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj0 @ (c_Inj0 @ (c_Inj1 @ c_Empty))))))) => c_False) => (! [X4 : $i,X5 : $i,X6 : (($i > ($i > $i) > $i > $i) > (($i > $i) > $i) > $i > $i),X7 : ($i > $i)] : (X0 @ (^[X8 : $i] : (X8)) @ (c_Inj0 @ c_Empty)) => (! [X7 : $i,X5 : ($i > $i > $i),X6 : ($i > $i > $i > $i),X4 : (($i > $i) > (($i > $i) > $i > $i) > $i)] : ((X0 @ (^[X8 : $i] : (X8)) @ (X6 @ (c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X5 @ c_Empty @ c_Empty)) @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ (X6 @ (c_Inj0 @ c_Empty) @ (c_Inj1 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (X4 @ (^[X8 : $i] : (c_Empty)) @ (^[X8 : ($i > $i), X9 : $i] : ((c_setsum @ X9 @ (c_setsum @ c_Empty @ c_Empty))))))) => (c_In @ (c_Inj0 @ c_Empty) @ (X4 @ (^[X8 : $i] : (X8)) @ (^[X8 : ($i > $i), X9 : $i] : (c_Empty))))) => c_False))))))))),
% 3.09/0.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 3.09/0.89 thf(f110,negated_conjecture,(
% 3.09/0.89 ~ ! [X0 : (($i > $i) > $i > $o),X3 : ((($i > $i) > $i) > ($i > $i) > ($i > $i) > $i > $o),X1 : (($i > $i > $i) > (($i > $i) > $i) > $o),X2 : ((($i > (($i > $i) > $i) > $i) > $i > $i > ($i > $i) > $i > $i) > $i > (($i > $i) > $i > $i) > $o)] : (! [X5 : $i,X4 : $i,X6 : ($i > ($i > $i) > $i),X7 : $i] : (X3 @ (^[X8 : ($i > $i)] : ((c_Inj0 @ (X8 @ c_Empty)))) @ (^[X8 : $i] : (X5)) @ (^[X8 : $i] : ((X6 @ c_Empty @ (^[X9 : $i] : (c_Empty))))) @ (c_Inj1 @ c_Empty)) => (! [X5 : $i,X4 : ($i > ($i > $i) > $i > $i > $i),X7 : $i,X6 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i)] : ((X3 @ (^[X8 : ($i > $i)] : ((c_Inj1 @ (c_Inj1 @ (X6 @ (^[X9 : (($i > $i) > $i), X10 : ($i > $i), X11 : $i] : ((c_setsum @ c_Empty @ c_Empty)))))))) @ (^[X8 : $i] : ((c_setsum @ c_Empty @ (c_Inj1 @ X8)))) @ (^[X8 : $i] : (c_Empty)) @ (c_Inj0 @ (c_Inj1 @ c_Empty))) => (c_In @ (c_Inj1 @ c_Empty) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ c_Empty))) => (! [X7 : (($i > $i > $i > $i) > $i),X5 : ((($i > $i > $i) > $i) > $i),X4 : ($i > $i > $i),X6 : ($i > ($i > $i > $i) > $i)] : (X2 @ (^[X8 : ($i > (($i > $i) > $i) > $i), X9 : $i, X10 : $i, X11 : ($i > $i), X12 : $i] : ((c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ X12)))) @ (c_setsum @ (c_Inj1 @ (c_Inj1 @ c_Empty)) @ c_Empty) @ (^[X8 : ($i > $i), X9 : $i] : ((c_setsum @ X9 @ (X7 @ (^[X10 : $i, X11 : $i, X12 : $i] : (c_Empty))))))) => (! [X4 : (($i > ($i > $i) > $i > $i) > $i),X5 : $i,X6 : ($i > (($i > $i) > $i > $i) > $i > $i),X7 : $i] : ((c_In @ (c_Inj0 @ (c_Inj1 @ X7)) @ (X4 @ (^[X8 : $i, X9 : ($i > $i), X10 : $i] : (c_Empty)))) => ((X2 @ (^[X8 : ($i > (($i > $i) > $i) > $i), X9 : $i, X10 : $i, X11 : ($i > $i), X12 : $i] : ((c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty)))))) @ (c_setsum @ (X4 @ (^[X8 : $i, X9 : ($i > $i), X10 : $i] : (c_Empty))) @ c_Empty) @ (^[X8 : ($i > $i), X9 : $i] : ((c_Inj1 @ c_Empty)))) => (X2 @ (^[X8 : ($i > (($i > $i) > $i) > $i), X9 : $i, X10 : $i, X11 : ($i > $i), X12 : $i] : ((c_Inj0 @ (c_Inj0 @ c_Empty)))) @ c_Empty @ (^[X8 : ($i > $i), X9 : $i] : ((c_Inj0 @ (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty)))))))) => (! [X7 : ($i > $i),X6 : (($i > $i > $i > $i) > $i),X4 : $i,X5 : (($i > $i > $i) > $i > $i)] : ((c_In @ (X6 @ (^[X8 : $i, X9 : $i, X10 : $i] : ((c_Inj1 @ X9)))) @ (c_setsum @ (c_Inj0 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty))))) => ((X0 @ (^[X8 : $i] : (X8)) @ (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj1 @ (c_Inj1 @ c_Empty)))) => (X1 @ (^[X8 : $i, X9 : $i] : ((c_setsum @ (c_setsum @ (c_Inj1 @ X9) @ (c_Inj1 @ c_Empty)) @ (c_setsum @ c_Empty @ (X7 @ (X7 @ c_Empty)))))) @ (^[X8 : ($i > $i)] : (c_Empty))))) => (! [X6 : ($i > $i),X7 : $i,X4 : $i,X5 : $i] : ((X1 @ (^[X8 : $i, X9 : $i] : (X8)) @ (^[X8 : ($i > $i)] : ((c_setsum @ (c_setsum @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj0 @ (c_Inj0 @ (c_Inj1 @ c_Empty))))))) => c_False) => (! [X4 : $i,X5 : $i,X6 : (($i > ($i > $i) > $i > $i) > (($i > $i) > $i) > $i > $i),X7 : ($i > $i)] : (X0 @ (^[X8 : $i] : (X8)) @ (c_Inj0 @ c_Empty)) => (! [X7 : $i,X5 : ($i > $i > $i),X6 : ($i > $i > $i > $i),X4 : (($i > $i) > (($i > $i) > $i > $i) > $i)] : ((X0 @ (^[X8 : $i] : (X8)) @ (X6 @ (c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X5 @ c_Empty @ c_Empty)) @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ (X6 @ (c_Inj0 @ c_Empty) @ (c_Inj1 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (X4 @ (^[X8 : $i] : (c_Empty)) @ (^[X8 : ($i > $i), X9 : $i] : ((c_setsum @ X9 @ (c_setsum @ c_Empty @ c_Empty))))))) => (c_In @ (c_Inj0 @ c_Empty) @ (X4 @ (^[X8 : $i] : (X8)) @ (^[X8 : ($i > $i), X9 : $i] : (c_Empty))))) => c_False))))))))),
% 3.09/0.89 inference(negated_conjecture,[status(cth)],[f109])).
% 3.09/0.89 thf(f129,plain,(
% 3.09/0.89 (c_not = (^[X0 : $o] : (X0 => c_False)))),
% 3.09/0.89 inference(rectify,[],[f13])).
% 3.09/0.89 thf(f130,plain,(
% 3.09/0.89 (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 3.09/0.89 inference(fool_elimination,[],[f129])).
% 3.09/0.89 thf(f151,plain,(
% 3.09/0.89 ((^[X0 : $i, X1 : $i] : ((c_binunion @ (c_Repl @ X0 @ (^[X2 : $i] : ((c_Inj0 @ X2)))) @ (c_Repl @ X1 @ (^[X3 : $i] : ((c_Inj1 @ X3))))))) = c_setsum)),
% 3.09/0.89 inference(rectify,[],[f73])).
% 3.09/0.89 thf(f152,plain,(
% 3.09/0.89 (c_setsum = (^[Y0 : $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y0 @ (^[Y2 : $i]: (c_Inj0 @ Y2))) @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Inj1 @ Y2))))))))),
% 3.09/0.89 inference(fool_elimination,[],[f151])).
% 3.09/0.89 thf(f175,plain,(
% 3.09/0.89 (c_Inj0 = (^[X0 : $i] : ((c_Repl @ X0 @ (^[X1 : $i] : ((c_Inj1 @ X1)))))))),
% 3.09/0.89 inference(rectify,[],[f70])).
% 3.09/0.89 thf(f176,plain,(
% 3.09/0.89 (c_Inj0 = (^[Y0 : $i]: (c_Repl @ Y0 @ (^[Y1 : $i]: (c_Inj1 @ Y1)))))),
% 3.09/0.89 inference(fool_elimination,[],[f175])).
% 3.09/0.89 thf(f222,plain,(
% 3.09/0.89 (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 3.09/0.89 inference(rectify,[],[f5])).
% 3.09/0.89 thf(f223,plain,(
% 3.09/0.89 (((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))) = $true)),
% 3.09/0.89 inference(fool_elimination,[],[f222])).
% 3.09/0.89 thf(f259,plain,(
% 3.09/0.89 ~ ! [X0 : (($i > $i) > $i > $o),X1 : ((($i > $i) > $i) > ($i > $i) > ($i > $i) > $i > $o),X2 : (($i > $i > $i) > (($i > $i) > $i) > $o),X3 : ((($i > (($i > $i) > $i) > $i) > $i > $i > ($i > $i) > $i > $i) > $i > (($i > $i) > $i > $i) > $o)] : (! [X4 : $i,X6 : ($i > ($i > $i) > $i)] : (X1 @ (^[X8 : ($i > $i)] : ((c_Inj0 @ (X8 @ c_Empty)))) @ (^[X9 : $i] : (X4)) @ (^[X10 : $i] : ((X6 @ c_Empty @ (^[X11 : $i] : (c_Empty))))) @ (c_Inj1 @ c_Empty)) => (! [X15 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i)] : ((X1 @ (^[X16 : ($i > $i)] : ((c_Inj1 @ (c_Inj1 @ (X15 @ (^[X17 : (($i > $i) > $i), X18 : ($i > $i), X19 : $i] : ((c_setsum @ c_Empty @ c_Empty)))))))) @ (^[X20 : $i] : ((c_setsum @ c_Empty @ (c_Inj1 @ X20)))) @ (^[X21 : $i] : (c_Empty)) @ (c_Inj0 @ (c_Inj1 @ c_Empty))) => (c_In @ (c_Inj1 @ c_Empty) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ c_Empty))) => (! [X22 : (($i > $i > $i > $i) > $i)] : (X3 @ (^[X26 : ($i > (($i > $i) > $i) > $i), X27 : $i, X28 : $i, X29 : ($i > $i), X30 : $i] : ((c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ X30)))) @ (c_setsum @ (c_Inj1 @ (c_Inj1 @ c_Empty)) @ c_Empty) @ (^[X31 : ($i > $i), X32 : $i] : ((c_setsum @ X32 @ (X22 @ (^[X33 : $i, X34 : $i, X35 : $i] : (c_Empty))))))) => (! [X36 : (($i > ($i > $i) > $i > $i) > $i),X39 : $i] : ((c_In @ (c_Inj0 @ (c_Inj1 @ X39)) @ (X36 @ (^[X40 : $i, X41 : ($i > $i), X42 : $i] : (c_Empty)))) => ((X3 @ (^[X43 : ($i > (($i > $i) > $i) > $i), X44 : $i, X45 : $i, X46 : ($i > $i), X47 : $i] : ((c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty)))))) @ (c_setsum @ (X36 @ (^[X48 : $i, X49 : ($i > $i), X50 : $i] : (c_Empty))) @ c_Empty) @ (^[X51 : ($i > $i), X52 : $i] : ((c_Inj1 @ c_Empty)))) => (X3 @ (^[X53 : ($i > (($i > $i) > $i) > $i), X54 : $i, X55 : $i, X56 : ($i > $i), X57 : $i] : ((c_Inj0 @ (c_Inj0 @ c_Empty)))) @ c_Empty @ (^[X58 : ($i > $i), X59 : $i] : ((c_Inj0 @ (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty)))))))) => (! [X60 : ($i > $i),X61 : (($i > $i > $i > $i) > $i)] : ((c_In @ (X61 @ (^[X64 : $i, X65 : $i, X66 : $i] : ((c_Inj1 @ X65)))) @ (c_setsum @ (c_Inj0 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty))))) => ((X0 @ (^[X67 : $i] : (X67)) @ (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj1 @ (c_Inj1 @ c_Empty)))) => (X2 @ (^[X68 : $i, X69 : $i] : ((c_setsum @ (c_setsum @ (c_Inj1 @ X69) @ (c_Inj1 @ c_Empty)) @ (c_setsum @ c_Empty @ (X60 @ (X60 @ c_Empty)))))) @ (^[X70 : ($i > $i)] : (c_Empty))))) => (((X2 @ (^[X75 : $i, X76 : $i] : (X75)) @ (^[X77 : ($i > $i)] : ((c_setsum @ (c_setsum @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj0 @ (c_Inj0 @ (c_Inj1 @ c_Empty))))))) => c_False) => ((X0 @ (^[X82 : $i] : (X82)) @ (c_Inj0 @ c_Empty)) => (! [X84 : ($i > $i > $i),X85 : ($i > $i > $i > $i),X86 : (($i > $i) > (($i > $i) > $i > $i) > $i)] : ((X0 @ (^[X87 : $i] : (X87)) @ (X85 @ (c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X84 @ c_Empty @ c_Empty)) @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ (X85 @ (c_Inj0 @ c_Empty) @ (c_Inj1 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (X86 @ (^[X88 : $i] : (c_Empty)) @ (^[X89 : ($i > $i), X90 : $i] : ((c_setsum @ X90 @ (c_setsum @ c_Empty @ c_Empty))))))) => (c_In @ (c_Inj0 @ c_Empty) @ (X86 @ (^[X91 : $i] : (X91)) @ (^[X92 : ($i > $i), X93 : $i] : (c_Empty))))) => c_False))))))))),
% 3.09/0.89 inference(rectify,[],[f110])).
% 3.09/0.89 thf(f260,plain,(
% 3.09/0.89 ~ ! [X0 : (($i > $i) > $i > $o),X1 : ((($i > $i) > $i) > ($i > $i) > ($i > $i) > $i > $o),X2 : (($i > $i > $i) > (($i > $i) > $i) > $o),X3 : ((($i > (($i > $i) > $i) > $i) > $i > $i > ($i > $i) > $i > $i) > $i > (($i > $i) > $i > $i) > $o)] : (! [X4 : $i,X6 : ($i > ($i > $i) > $i)] : ($true = ((X1 @ (^[Y0 : $i > $i]: (c_Inj0 @ (Y0 @ c_Empty))) @ (^[Y0 : $i]: (X4)) @ (^[Y0 : $i]: (X6 @ c_Empty @ (^[Y1 : $i]: (c_Empty)))) @ (c_Inj1 @ c_Empty)))) => (! [X15 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i)] : (($true = ((X1 @ (^[Y0 : $i > $i]: (c_Inj1 @ (c_Inj1 @ (X15 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ c_Empty)))))))))) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ (c_Inj1 @ Y0))) @ (^[Y0 : $i]: (c_Empty)) @ (c_Inj0 @ (c_Inj1 @ c_Empty))))) => (((c_In @ (c_Inj1 @ c_Empty) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ c_Empty))) = $true)) => (! [X22 : (($i > $i > $i > $i) > $i)] : (((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ Y4))))))))))) @ (c_setsum @ (c_Inj1 @ (c_Inj1 @ c_Empty)) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (X22 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty))))))))))))) = $true) => (! [X36 : (($i > ($i > $i) > $i > $i) > $i),X39 : $i] : (($true = ((c_In @ (c_Inj0 @ (c_Inj1 @ X39)) @ (X36 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty)))))))))) => (($true = ((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty))))))))))))) @ (c_setsum @ (X36 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty))))))) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty))))))) => ($true = ((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ c_Empty))))))))))) @ c_Empty @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty))))))))))) => (! [X60 : ($i > $i),X61 : (($i > $i > $i > $i) > $i)] : (($true = ((c_In @ (X61 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ Y1))))))) @ (c_setsum @ (c_Inj0 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty))))))) => (($true = ((X0 @ (^[Y0 : $i]: (Y0)) @ (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj1 @ (c_Inj1 @ c_Empty)))))) => (((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ (c_setsum @ (c_Inj1 @ Y1) @ (c_Inj1 @ c_Empty)) @ (c_setsum @ c_Empty @ (X60 @ (X60 @ c_Empty))))))) @ (^[Y0 : $i > $i]: (c_Empty)))) = $true))) => (((((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y0)))) @ (^[Y0 : $i > $i]: (c_setsum @ (c_setsum @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj0 @ (c_Inj0 @ (c_Inj1 @ c_Empty))))))) = $true) => (c_False = $true)) => (($true = ((X0 @ (^[Y0 : $i]: (Y0)) @ (c_Inj0 @ c_Empty)))) => (! [X84 : ($i > $i > $i),X85 : ($i > $i > $i > $i),X86 : (($i > $i) > (($i > $i) > $i > $i) > $i)] : (($true = ((X0 @ (^[Y0 : $i]: (Y0)) @ (X85 @ (c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X84 @ c_Empty @ c_Empty)) @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ (X85 @ (c_Inj0 @ c_Empty) @ (c_Inj1 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (X86 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (c_setsum @ c_Empty @ c_Empty)))))))))) => ($true = ((c_In @ (c_Inj0 @ c_Empty) @ (X86 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty))))))))) => (c_False = $true)))))))))),
% 3.09/0.89 inference(fool_elimination,[],[f259])).
% 3.09/0.89 thf(f308,plain,(
% 3.09/0.89 ~ ! [X3 : ((($i > (($i > $i) > $i) > $i) > $i > $i > ($i > $i) > $i > $i) > $i > (($i > $i) > $i > $i) > $o),X1 : ((($i > $i) > $i) > ($i > $i) > ($i > $i) > $i > $o),X2 : (($i > $i > $i) > (($i > $i) > $i) > $o),X0 : (($i > $i) > $i > $o)] : (! [X5 : ($i > ($i > $i) > $i),X4 : $i] : ($true = ((X1 @ (^[Y0 : $i > $i]: (c_Inj0 @ (Y0 @ c_Empty))) @ (^[Y0 : $i]: (X4)) @ (^[Y0 : $i]: (X5 @ c_Empty @ (^[Y1 : $i]: (c_Empty)))) @ (c_Inj1 @ c_Empty)))) => (! [X6 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i)] : (($true = ((X1 @ (^[Y0 : $i > $i]: (c_Inj1 @ (c_Inj1 @ (X6 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ c_Empty)))))))))) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ (c_Inj1 @ Y0))) @ (^[Y0 : $i]: (c_Empty)) @ (c_Inj0 @ (c_Inj1 @ c_Empty))))) => (((c_In @ (c_Inj1 @ c_Empty) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ c_Empty))) = $true)) => (! [X7 : (($i > $i > $i > $i) > $i)] : (((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ Y4))))))))))) @ (c_setsum @ (c_Inj1 @ (c_Inj1 @ c_Empty)) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (X7 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty))))))))))))) = $true) => (! [X9 : $i,X8 : (($i > ($i > $i) > $i > $i) > $i)] : (($true = ((c_In @ (c_Inj0 @ (c_Inj1 @ X9)) @ (X8 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty)))))))))) => (($true = ((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty))))))))))))) @ (c_setsum @ (X8 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty))))))) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty))))))) => ($true = ((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ c_Empty))))))))))) @ c_Empty @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty))))))))))) => (! [X11 : (($i > $i > $i > $i) > $i),X10 : ($i > $i)] : (($true = ((c_In @ (X11 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ Y1))))))) @ (c_setsum @ (c_Inj0 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty))))))) => (($true = ((X0 @ (^[Y0 : $i]: (Y0)) @ (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj1 @ (c_Inj1 @ c_Empty)))))) => ($true = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ (c_setsum @ (c_Inj1 @ Y1) @ (c_Inj1 @ c_Empty)) @ (c_setsum @ c_Empty @ (X10 @ (X10 @ c_Empty))))))) @ (^[Y0 : $i > $i]: (c_Empty))))))) => (((((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y0)))) @ (^[Y0 : $i > $i]: (c_setsum @ (c_setsum @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj0 @ (c_Inj0 @ (c_Inj1 @ c_Empty))))))) = $true) => (c_False = $true)) => (($true = ((X0 @ (^[Y0 : $i]: (Y0)) @ (c_Inj0 @ c_Empty)))) => (! [X12 : ($i > $i > $i),X13 : ($i > $i > $i > $i),X14 : (($i > $i) > (($i > $i) > $i > $i) > $i)] : ((((X0 @ (^[Y0 : $i]: (Y0)) @ (X13 @ (c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X12 @ c_Empty @ c_Empty)) @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ (X13 @ (c_Inj0 @ c_Empty) @ (c_Inj1 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (X14 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (c_setsum @ c_Empty @ c_Empty))))))))) = $true) => (((c_In @ (c_Inj0 @ c_Empty) @ (X14 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty))))))) = $true)) => (c_False = $true)))))))))),
% 3.09/0.89 inference(rectify,[],[f260])).
% 3.09/0.89 thf(f313,plain,(
% 3.09/0.89 ? [X3 : ((($i > (($i > $i) > $i) > $i) > $i > $i > ($i > $i) > $i > $i) > $i > (($i > $i) > $i > $i) > $o),X1 : ((($i > $i) > $i) > ($i > $i) > ($i > $i) > $i > $o),X2 : (($i > $i > $i) > (($i > $i) > $i) > $o),X0 : (($i > $i) > $i > $o)] : (((((((((c_False != $true) & ! [X13 : ($i > $i > $i > $i),X12 : ($i > $i > $i),X14 : (($i > $i) > (($i > $i) > $i > $i) > $i)] : ((((c_In @ (c_Inj0 @ c_Empty) @ (X14 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty))))))) = $true) | (((X0 @ (^[Y0 : $i]: (Y0)) @ (X13 @ (c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X12 @ c_Empty @ c_Empty)) @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ (X13 @ (c_Inj0 @ c_Empty) @ (c_Inj1 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (X14 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (c_setsum @ c_Empty @ c_Empty))))))))) != $true))) & ($true = ((X0 @ (^[Y0 : $i]: (Y0)) @ (c_Inj0 @ c_Empty))))) & ((((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y0)))) @ (^[Y0 : $i > $i]: (c_setsum @ (c_setsum @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj0 @ (c_Inj0 @ (c_Inj1 @ c_Empty))))))) != $true) | (c_False = $true))) & ! [X11 : (($i > $i > $i > $i) > $i),X10 : ($i > $i)] : ((($true = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ (c_setsum @ (c_Inj1 @ Y1) @ (c_Inj1 @ c_Empty)) @ (c_setsum @ c_Empty @ (X10 @ (X10 @ c_Empty))))))) @ (^[Y0 : $i > $i]: (c_Empty))))) | ($true != ((X0 @ (^[Y0 : $i]: (Y0)) @ (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj1 @ (c_Inj1 @ c_Empty))))))) | ($true != ((c_In @ (X11 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ Y1))))))) @ (c_setsum @ (c_Inj0 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty))))))))) & ! [X9 : $i,X8 : (($i > ($i > $i) > $i > $i) > $i)] : ((($true = ((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ c_Empty))))))))))) @ c_Empty @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty))))))))) | ($true != ((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty))))))))))))) @ (c_setsum @ (X8 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty))))))) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty)))))))) | ($true != ((c_In @ (c_Inj0 @ (c_Inj1 @ X9)) @ (X8 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty)))))))))))) & ! [X7 : (($i > $i > $i > $i) > $i)] : (((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ Y4))))))))))) @ (c_setsum @ (c_Inj1 @ (c_Inj1 @ c_Empty)) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (X7 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty))))))))))))) = $true)) & ! [X6 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i)] : ((((c_In @ (c_Inj1 @ c_Empty) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ c_Empty))) = $true) | ($true != ((X1 @ (^[Y0 : $i > $i]: (c_Inj1 @ (c_Inj1 @ (X6 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ c_Empty)))))))))) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ (c_Inj1 @ Y0))) @ (^[Y0 : $i]: (c_Empty)) @ (c_Inj0 @ (c_Inj1 @ c_Empty))))))) & ! [X5 : ($i > ($i > $i) > $i),X4 : $i] : ($true = ((X1 @ (^[Y0 : $i > $i]: (c_Inj0 @ (Y0 @ c_Empty))) @ (^[Y0 : $i]: (X4)) @ (^[Y0 : $i]: (X5 @ c_Empty @ (^[Y1 : $i]: (c_Empty)))) @ (c_Inj1 @ c_Empty)))))),
% 3.09/0.89 inference(ennf_transformation,[],[f308])).
% 3.09/0.89 thf(f314,plain,(
% 3.09/0.89 ? [X3 : ((($i > (($i > $i) > $i) > $i) > $i > $i > ($i > $i) > $i > $i) > $i > (($i > $i) > $i > $i) > $o),X2 : (($i > $i > $i) > (($i > $i) > $i) > $o),X1 : ((($i > $i) > $i) > ($i > $i) > ($i > $i) > $i > $o),X0 : (($i > $i) > $i > $o)] : (! [X6 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i)] : ((((c_In @ (c_Inj1 @ c_Empty) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ c_Empty))) = $true) | ($true != ((X1 @ (^[Y0 : $i > $i]: (c_Inj1 @ (c_Inj1 @ (X6 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ c_Empty)))))))))) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ (c_Inj1 @ Y0))) @ (^[Y0 : $i]: (c_Empty)) @ (c_Inj0 @ (c_Inj1 @ c_Empty)))))) & ! [X5 : ($i > ($i > $i) > $i),X4 : $i] : ($true = ((X1 @ (^[Y0 : $i > $i]: (c_Inj0 @ (Y0 @ c_Empty))) @ (^[Y0 : $i]: (X4)) @ (^[Y0 : $i]: (X5 @ c_Empty @ (^[Y1 : $i]: (c_Empty)))) @ (c_Inj1 @ c_Empty)))) & ((((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y0)))) @ (^[Y0 : $i > $i]: (c_setsum @ (c_setsum @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj0 @ (c_Inj0 @ (c_Inj1 @ c_Empty))))))) != $true) | (c_False = $true)) & ! [X8 : (($i > ($i > $i) > $i > $i) > $i),X9 : $i] : (($true != ((c_In @ (c_Inj0 @ (c_Inj1 @ X9)) @ (X8 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty)))))))))) | ($true != ((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty))))))))))))) @ (c_setsum @ (X8 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty))))))) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty))))))) | ($true = ((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ c_Empty))))))))))) @ c_Empty @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty)))))))))) & ! [X10 : ($i > $i),X11 : (($i > $i > $i > $i) > $i)] : (($true = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ (c_setsum @ (c_Inj1 @ Y1) @ (c_Inj1 @ c_Empty)) @ (c_setsum @ c_Empty @ (X10 @ (X10 @ c_Empty))))))) @ (^[Y0 : $i > $i]: (c_Empty))))) | ($true != ((c_In @ (X11 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ Y1))))))) @ (c_setsum @ (c_Inj0 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty))))))) | ($true != ((X0 @ (^[Y0 : $i]: (Y0)) @ (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj1 @ (c_Inj1 @ c_Empty))))))) & ! [X7 : (($i > $i > $i > $i) > $i)] : (((X3 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ Y4))))))))))) @ (c_setsum @ (c_Inj1 @ (c_Inj1 @ c_Empty)) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (X7 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty))))))))))))) = $true) & ($true = ((X0 @ (^[Y0 : $i]: (Y0)) @ (c_Inj0 @ c_Empty)))) & (c_False != $true) & ! [X13 : ($i > $i > $i > $i),X12 : ($i > $i > $i),X14 : (($i > $i) > (($i > $i) > $i > $i) > $i)] : ((((c_In @ (c_Inj0 @ c_Empty) @ (X14 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty))))))) = $true) | (((X0 @ (^[Y0 : $i]: (Y0)) @ (X13 @ (c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X12 @ c_Empty @ c_Empty)) @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ (X13 @ (c_Inj0 @ c_Empty) @ (c_Inj1 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (X14 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (c_setsum @ c_Empty @ c_Empty))))))))) != $true)))),
% 3.09/0.89 inference(flattening,[],[f313])).
% 3.09/0.89 thf(f315,plain,(
% 3.09/0.89 ? [X0 : ((($i > (($i > $i) > $i) > $i) > $i > $i > ($i > $i) > $i > $i) > $i > (($i > $i) > $i > $i) > $o),X1 : (($i > $i > $i) > (($i > $i) > $i) > $o),X2 : ((($i > $i) > $i) > ($i > $i) > ($i > $i) > $i > $o),X3 : (($i > $i) > $i > $o)] : (! [X4 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i)] : ((((c_In @ (c_Inj1 @ c_Empty) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ c_Empty))) = $true) | ($true != ((X2 @ (^[Y0 : $i > $i]: (c_Inj1 @ (c_Inj1 @ (X4 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ c_Empty)))))))))) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ (c_Inj1 @ Y0))) @ (^[Y0 : $i]: (c_Empty)) @ (c_Inj0 @ (c_Inj1 @ c_Empty)))))) & ! [X5 : ($i > ($i > $i) > $i),X6 : $i] : ($true = ((X2 @ (^[Y0 : $i > $i]: (c_Inj0 @ (Y0 @ c_Empty))) @ (^[Y0 : $i]: (X6)) @ (^[Y0 : $i]: (X5 @ c_Empty @ (^[Y1 : $i]: (c_Empty)))) @ (c_Inj1 @ c_Empty)))) & ((((X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y0)))) @ (^[Y0 : $i > $i]: (c_setsum @ (c_setsum @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj0 @ (c_Inj0 @ (c_Inj1 @ c_Empty))))))) != $true) | (c_False = $true)) & ! [X7 : (($i > ($i > $i) > $i > $i) > $i),X8 : $i] : ((((c_In @ (c_Inj0 @ (c_Inj1 @ X8)) @ (X7 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty))))))))) != $true) | ($true != ((X0 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty))))))))))))) @ (c_setsum @ (X7 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty))))))) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty))))))) | ($true = ((X0 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ c_Empty))))))))))) @ c_Empty @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty)))))))))) & ! [X9 : ($i > $i),X10 : (($i > $i > $i > $i) > $i)] : (($true = ((X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ (c_setsum @ (c_Inj1 @ Y1) @ (c_Inj1 @ c_Empty)) @ (c_setsum @ c_Empty @ (X9 @ (X9 @ c_Empty))))))) @ (^[Y0 : $i > $i]: (c_Empty))))) | (((c_In @ (X10 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ Y1))))))) @ (c_setsum @ (c_Inj0 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)))))) != $true) | (((X3 @ (^[Y0 : $i]: (Y0)) @ (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj1 @ (c_Inj1 @ c_Empty))))) != $true)) & ! [X11 : (($i > $i > $i > $i) > $i)] : ($true = ((X0 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ Y4))))))))))) @ (c_setsum @ (c_Inj1 @ (c_Inj1 @ c_Empty)) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (X11 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))))))))))) & ($true = ((X3 @ (^[Y0 : $i]: (Y0)) @ (c_Inj0 @ c_Empty)))) & (c_False != $true) & ! [X12 : ($i > $i > $i > $i),X13 : ($i > $i > $i),X14 : (($i > $i) > (($i > $i) > $i > $i) > $i)] : ((((c_In @ (c_Inj0 @ c_Empty) @ (X14 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty))))))) = $true) | ($true != ((X3 @ (^[Y0 : $i]: (Y0)) @ (X12 @ (c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X13 @ c_Empty @ c_Empty)) @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ (X12 @ (c_Inj0 @ c_Empty) @ (c_Inj1 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (X14 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (c_setsum @ c_Empty @ c_Empty))))))))))))),
% 3.09/0.89 inference(rectify,[],[f314])).
% 3.09/0.89 thf(f316,plain,(
% 3.09/0.89 ! [X4 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i)] : ((((c_In @ (c_Inj1 @ c_Empty) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ c_Empty))) = $true) | ($true != ((sK2 @ (^[Y0 : $i > $i]: (c_Inj1 @ (c_Inj1 @ (X4 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ c_Empty)))))))))) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ (c_Inj1 @ Y0))) @ (^[Y0 : $i]: (c_Empty)) @ (c_Inj0 @ (c_Inj1 @ c_Empty)))))) & ! [X5 : ($i > ($i > $i) > $i),X6 : $i] : ($true = ((sK2 @ (^[Y0 : $i > $i]: (c_Inj0 @ (Y0 @ c_Empty))) @ (^[Y0 : $i]: (X6)) @ (^[Y0 : $i]: (X5 @ c_Empty @ (^[Y1 : $i]: (c_Empty)))) @ (c_Inj1 @ c_Empty)))) & ((((sK1 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y0)))) @ (^[Y0 : $i > $i]: (c_setsum @ (c_setsum @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj0 @ (c_Inj0 @ (c_Inj1 @ c_Empty))))))) != $true) | (c_False = $true)) & ! [X7 : (($i > ($i > $i) > $i > $i) > $i),X8 : $i] : ((((c_In @ (c_Inj0 @ (c_Inj1 @ X8)) @ (X7 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty))))))))) != $true) | (((sK0 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty))))))))))))) @ (c_setsum @ (X7 @ (^[Y0 : $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty))))))) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty)))))) != $true) | (((sK0 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_Inj0 @ (c_Inj0 @ c_Empty))))))))))) @ c_Empty @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj0 @ (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty)))))))) = $true)) & ! [X9 : ($i > $i),X10 : (($i > $i > $i > $i) > $i)] : ((((sK1 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ (c_setsum @ (c_Inj1 @ Y1) @ (c_Inj1 @ c_Empty)) @ (c_setsum @ c_Empty @ (X9 @ (X9 @ c_Empty))))))) @ (^[Y0 : $i > $i]: (c_Empty)))) = $true) | (((c_In @ (X10 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ Y1))))))) @ (c_setsum @ (c_Inj0 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)))))) != $true) | (((sK3 @ (^[Y0 : $i]: (Y0)) @ (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ c_Empty) @ (c_Inj1 @ (c_Inj1 @ c_Empty))))) != $true)) & ! [X11 : (($i > $i > $i > $i) > $i)] : (((sK0 @ (^[Y0 : $i > (($i > $i) > $i) > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: ((^[Y4 : $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ Y4))))))))))) @ (c_setsum @ (c_Inj1 @ (c_Inj1 @ c_Empty)) @ c_Empty) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (X11 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty))))))))))))) = $true) & ($true = ((sK3 @ (^[Y0 : $i]: (Y0)) @ (c_Inj0 @ c_Empty)))) & (c_False != $true) & ! [X12 : ($i > $i > $i > $i),X13 : ($i > $i > $i),X14 : (($i > $i) > (($i > $i) > $i > $i) > $i)] : ((((c_In @ (c_Inj0 @ c_Empty) @ (X14 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty))))))) = $true) | ($true != ((sK3 @ (^[Y0 : $i]: (Y0)) @ (X12 @ (c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X13 @ c_Empty @ c_Empty)) @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ (X12 @ (c_Inj0 @ c_Empty) @ (c_Inj1 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (X14 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (c_setsum @ c_Empty @ c_Empty)))))))))))),
% 3.09/0.89 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f315])).
% 3.09/0.89 thf(f320,plain,(
% 3.09/0.89 ( ! [X14 : (($i > $i) > (($i > $i) > $i > $i) > $i),X12 : ($i > $i > $i > $i),X13 : ($i > $i > $i)] : ((((c_In @ (c_Inj0 @ c_Empty) @ (X14 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty))))))) = $true) | ($true != ((sK3 @ (^[Y0 : $i]: (Y0)) @ (X12 @ (c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X13 @ c_Empty @ c_Empty)) @ (c_setsum @ (c_setsum @ c_Empty @ (c_setsum @ c_Empty @ c_Empty)) @ (X12 @ (c_Inj0 @ c_Empty) @ (c_Inj1 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (X14 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_setsum @ Y1 @ (c_setsum @ c_Empty @ c_Empty))))))))))) )),
% 3.09/0.89 inference(cnf_transformation,[],[f316])).
% 3.09/0.89 thf(f321,plain,(
% 3.09/0.89 (c_False != $true)),
% 3.09/0.89 inference(cnf_transformation,[],[f316])).
% 3.09/0.89 thf(f322,plain,(
% 3.09/0.89 ($true = ((sK3 @ (^[Y0 : $i]: (Y0)) @ (c_Inj0 @ c_Empty))))),
% 3.09/0.89 inference(cnf_transformation,[],[f316])).
% 3.09/0.89 thf(f329,plain,(
% 3.09/0.89 (c_Inj0 = (^[Y0 : $i]: (c_Repl @ Y0 @ (^[Y1 : $i]: (c_Inj1 @ Y1)))))),
% 3.09/0.89 inference(cnf_transformation,[],[f176])).
% 3.09/0.89 thf(f330,plain,(
% 3.09/0.89 (c_setsum = (^[Y0 : $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y0 @ (^[Y2 : $i]: (c_Inj0 @ Y2))) @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Inj1 @ Y2))))))))),
% 3.09/0.89 inference(cnf_transformation,[],[f152])).
% 3.09/0.89 thf(f336,plain,(
% 3.09/0.89 (((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))) = $true)),
% 3.09/0.89 inference(cnf_transformation,[],[f223])).
% 3.09/0.89 thf(f337,plain,(
% 3.09/0.89 (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 3.09/0.89 inference(cnf_transformation,[],[f130])).
% 3.09/0.89 thf(f339,definition,(
% 3.09/0.89 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.09/0.89 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.09/0.89 thf(f340,plain,(
% 3.09/0.89 (c_setsum = (^[Y0 : $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y0 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Repl @ Y3 @ (^[Y4 : $i]: (c_Inj1 @ Y4)))) @ Y2))) @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Inj1 @ Y2))))))))),
% 3.09/0.89 inference(definition_unfolding,[],[f330,f329])).
% 3.09/0.89 thf(f347,plain,(
% 3.09/0.89 ($true = ((sK3 @ (^[Y0 : $i]: (Y0)) @ ((^[Y0 : $i]: (c_Repl @ Y0 @ (^[Y1 : $i]: (c_Inj1 @ Y1)))) @ c_Empty))))),
% 3.09/0.89 inference(definition_unfolding,[],[f322,f329])).
% 3.09/0.89 thf(f348,plain,(
% 3.09/0.89 ( ! [X14 : (($i > $i) > (($i > $i) > $i > $i) > $i),X12 : ($i > $i > $i > $i),X13 : ($i > $i > $i)] : (($true = ((c_In @ ((^[Y0 : $i]: (c_Repl @ Y0 @ (^[Y1 : $i]: (c_Inj1 @ Y1)))) @ c_Empty) @ (X14 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty)))))))) | ($true != ((sK3 @ (^[Y0 : $i]: (Y0)) @ (X12 @ ((^[Y0 : $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y0 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Repl @ Y3 @ (^[Y4 : $i]: (c_Inj1 @ Y4)))) @ Y2))) @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Inj1 @ Y2))))))) @ (c_Inj1 @ ((^[Y0 : $i]: (c_Repl @ Y0 @ (^[Y1 : $i]: (c_Inj1 @ Y1)))) @ c_Empty)) @ (X13 @ c_Empty @ c_Empty)) @ ((^[Y0 : $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y0 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Repl @ Y3 @ (^[Y4 : $i]: (c_Inj1 @ Y4)))) @ Y2))) @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Inj1 @ Y2))))))) @ ((^[Y0 : $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y0 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Repl @ Y3 @ (^[Y4 : $i]: (c_Inj1 @ Y4)))) @ Y2))) @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Inj1 @ Y2))))))) @ c_Empty @ ((^[Y0 : $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y0 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Repl @ Y3 @ (^[Y4 : $i]: (c_Inj1 @ Y4)))) @ Y2))) @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Inj1 @ Y2))))))) @ c_Empty @ c_Empty)) @ (X12 @ ((^[Y0 : $i]: (c_Repl @ Y0 @ (^[Y1 : $i]: (c_Inj1 @ Y1)))) @ c_Empty) @ (c_Inj1 @ c_Empty) @ ((^[Y0 : $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y0 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Repl @ Y3 @ (^[Y4 : $i]: (c_Inj1 @ Y4)))) @ Y2))) @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Inj1 @ Y2))))))) @ c_Empty @ c_Empty))) @ (X14 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: (c_binunion @ (c_Repl @ Y2 @ (^[Y4 : $i]: ((^[Y5 : $i]: (c_Repl @ Y5 @ (^[Y6 : $i]: (c_Inj1 @ Y6)))) @ Y4))) @ (c_Repl @ Y3 @ (^[Y4 : $i]: (c_Inj1 @ Y4))))))) @ Y1 @ ((^[Y2 : $i]: ((^[Y3 : $i]: (c_binunion @ (c_Repl @ Y2 @ (^[Y4 : $i]: ((^[Y5 : $i]: (c_Repl @ Y5 @ (^[Y6 : $i]: (c_Inj1 @ Y6)))) @ Y4))) @ (c_Repl @ Y3 @ (^[Y4 : $i]: (c_Inj1 @ Y4))))))) @ c_Empty @ c_Empty))))))))))) )),
% 3.09/0.89 inference(definition_unfolding,[],[f320,f329,f340,f329,f340,f340,f340,f329,f340,f340,f340])).
% 3.09/0.89 thf(f350,plain,(
% 3.09/0.89 ($true = (((^[Y0 : $o]: (Y0 => c_False)) @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 3.09/0.89 inference(definition_unfolding,[],[f336,f337])).
% 3.09/0.89 thf(f351,plain,(
% 3.09/0.89 ($true = (((?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))) => c_False)))),
% 3.09/0.89 inference(beta-eta_normalization,[],[f350])).
% 3.09/0.89 thf(f357,plain,(
% 3.09/0.89 (((sK3 @ (^[Y0 : $i]: (Y0)) @ (c_Repl @ c_Empty @ c_Inj1))) = $true)),
% 3.09/0.89 inference(beta-eta_normalization,[],[f347])).
% 3.09/0.89 thf(f360,plain,(
% 3.09/0.89 ( ! [X14 : (($i > $i) > (($i > $i) > $i > $i) > $i),X12 : ($i > $i > $i > $i),X13 : ($i > $i > $i)] : (($true != ((sK3 @ (^[Y0 : $i]: (Y0)) @ (X12 @ (c_binunion @ (c_Repl @ (c_Inj1 @ (c_Repl @ c_Empty @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (X13 @ c_Empty @ c_Empty) @ c_Inj1)) @ (c_binunion @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (X12 @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1))) @ c_Inj1)) @ (X14 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)))))))))) | (((c_In @ (c_Repl @ c_Empty @ c_Inj1) @ (X14 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty))))))) = $true)) )),
% 3.09/0.89 inference(beta-eta_normalization,[],[f348])).
% 3.09/0.89 thf(f370,definition,(
% 3.09/0.89 spl5_3 <=> (c_False = $true)),
% 3.09/0.89 introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition])).
% 3.09/0.89 thf(f371,plain,(
% 3.09/0.89 (c_False != $true) | spl5_3),
% 3.09/0.89 inference(avatar_component_clause,[],[f370])).
% 3.09/0.89 thf(f397,plain,(
% 3.09/0.89 ~spl5_3),
% 3.09/0.89 inference(avatar_split_clause,[],[f321,f370])).
% 3.09/0.89 thf(f398,plain,(
% 3.09/0.89 (c_False = $false) | spl5_3),
% 3.09/0.89 inference(unit_resulting_resolution,[],[f339,f371])).
% 3.09/0.89 thf(f411,plain,(
% 3.09/0.89 ($true = (((?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))) => $false))) | spl5_3),
% 3.09/0.89 inference(constrained_superposition,[],[f351,f398])).
% 3.09/0.89 thf(f418,plain,(
% 3.09/0.89 ($true = $false) | ($false = ((?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))) | spl5_3),
% 3.09/0.89 inference(imp_proxy_clausification,[],[f411])).
% 3.09/0.89 thf(f419,plain,(
% 3.09/0.89 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (c_In @ Y0 @ c_Empty)) @ X1))) | ($true = $false)) ) | spl5_3),
% 3.09/0.89 inference(pi_proxy_clausification,[],[f418])).
% 3.09/0.89 thf(f420,plain,(
% 3.09/0.89 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (c_In @ Y0 @ c_Empty)) @ X1)))) ) | spl5_3),
% 3.09/0.89 inference(trivial_inequality_removal,[],[f419])).
% 3.09/0.89 thf(f421,plain,(
% 3.09/0.89 ( ! [X1 : $i] : ((((c_In @ X1 @ c_Empty)) = $false)) ) | spl5_3),
% 3.09/0.89 inference(beta-eta_normalization,[],[f420])).
% 3.09/0.89 thf(f497,plain,(
% 3.09/0.89 ( ! [X2 : ($i > $i > $i > $i > $i),X3 : ($i > $i > $i > $i),X0 : ($i > $i > $i),X4 : (($i > $i) > (($i > $i) > $i > $i) > $i)] : (($true = ((c_In @ (c_Repl @ c_Empty @ c_Inj1) @ (X4 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty)))))))) | ($true != $true) | (c_Empty != ((X3 @ (c_binunion @ (c_Repl @ (c_Inj1 @ (c_Repl @ c_Empty @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (X0 @ c_Empty @ c_Empty) @ c_Inj1)) @ (c_binunion @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_Repl @ (X3 @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1))) @ (^[Y0 : $i]: (c_Inj1 @ (X2 @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y1 : $i]: (c_Repl @ Y1 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ Y0)))) @ c_Inj1)) @ (X4 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1))))))))) | (((X2 @ (c_binunion @ (c_Repl @ (c_Inj1 @ (c_Repl @ c_Empty @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (X0 @ c_Empty @ c_Empty) @ c_Inj1)) @ (c_binunion @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_Repl @ (X3 @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1))) @ (^[Y0 : $i]: (c_Inj1 @ (X2 @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y1 : $i]: (c_Repl @ Y1 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ Y0)))) @ c_Inj1)) @ (X4 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)))))))) != (^[Y0 : $i]: (Y0)))) )),
% 3.09/0.89 inference(constrained_superposition,[],[f360,f357])).
% 3.09/0.89 thf(f502,plain,(
% 3.09/0.89 ( ! [X2 : ($i > $i > $i > $i > $i),X3 : ($i > $i > $i > $i),X0 : ($i > $i > $i),X4 : (($i > $i) > (($i > $i) > $i > $i) > $i)] : ((((X2 @ (c_binunion @ (c_Repl @ (c_Inj1 @ (c_Repl @ c_Empty @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (X0 @ c_Empty @ c_Empty) @ c_Inj1)) @ (c_binunion @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_Repl @ (X3 @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1))) @ (^[Y0 : $i]: (c_Inj1 @ (X2 @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y1 : $i]: (c_Repl @ Y1 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ Y0)))) @ c_Inj1)) @ (X4 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)))))))) != (^[Y0 : $i]: (Y0))) | ($true = ((c_In @ (c_Repl @ c_Empty @ c_Inj1) @ (X4 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty)))))))) | (c_Empty != ((X3 @ (c_binunion @ (c_Repl @ (c_Inj1 @ (c_Repl @ c_Empty @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (X0 @ c_Empty @ c_Empty) @ c_Inj1)) @ (c_binunion @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_Repl @ (X3 @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1))) @ (^[Y0 : $i]: (c_Inj1 @ (X2 @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y1 : $i]: (c_Repl @ Y1 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ Y0)))) @ c_Inj1)) @ (X4 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)))))))))) )),
% 3.09/0.89 inference(trivial_inequality_removal,[],[f497])).
% 3.09/0.89 thf(f681,plain,(
% 3.09/0.89 ( ! [X2 : ($i > $i > $i),X0 : (($i > $i) > (($i > $i) > $i > $i) > $i),X1 : ($i > $i > $i > $i)] : (($true = ((c_In @ (c_Repl @ c_Empty @ c_Inj1) @ (X0 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty)))))))) | (c_Empty != ((X1 @ (c_binunion @ (c_Repl @ (c_Inj1 @ (c_Repl @ c_Empty @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (X2 @ c_Empty @ c_Empty) @ c_Inj1)) @ (c_binunion @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_Repl @ (X1 @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1))) @ (^[Y0 : $i]: (c_Inj1 @ ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (Y4)))))))) @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y1 : $i]: (c_Repl @ Y1 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ Y0)))) @ c_Inj1)) @ (X0 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)))))))))) )),
% 3.09/0.89 inference(equality_resolution,[],[f502])).
% 3.09/0.89 thf(f682,plain,(
% 3.09/0.89 ( ! [X2 : ($i > $i > $i),X0 : (($i > $i) > (($i > $i) > $i > $i) > $i),X1 : ($i > $i > $i > $i)] : ((c_Empty != ((X1 @ (c_binunion @ (c_Repl @ (c_Inj1 @ (c_Repl @ c_Empty @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (X2 @ c_Empty @ c_Empty) @ c_Inj1)) @ (c_binunion @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1)) @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ (c_Repl @ (X1 @ (c_Repl @ c_Empty @ c_Inj1) @ (c_Inj1 @ c_Empty) @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y0 : $i]: (c_Repl @ Y0 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1))) @ c_Inj1) @ c_Inj1)) @ (X0 @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_binunion @ (c_Repl @ Y1 @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ (c_binunion @ (c_Repl @ c_Empty @ (^[Y2 : $i]: (c_Repl @ Y2 @ c_Inj1))) @ (c_Repl @ c_Empty @ c_Inj1)) @ c_Inj1))))))))) | ($true = ((c_In @ (c_Repl @ c_Empty @ c_Inj1) @ (X0 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty))))))))) )),
% 3.09/0.89 inference(beta-eta_normalization,[],[f681])).
% 3.09/0.89 thf(f820,plain,(
% 3.09/0.89 ($true = ((c_In @ (c_Repl @ c_Empty @ c_Inj1) @ ((^[Y0 : $i > $i]: ((^[Y1 : ($i > $i) > $i > $i]: (c_Empty)))) @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Empty))))))))),
% 3.09/0.89 inference(equality_resolution,[],[f682])).
% 3.09/0.89 thf(f823,plain,(
% 3.09/0.89 ($true = ((c_In @ (c_Repl @ c_Empty @ c_Inj1) @ c_Empty)))),
% 3.09/0.89 inference(beta-eta_normalization,[],[f820])).
% 3.09/0.89 thf(f825,plain,(
% 3.09/0.89 ($true = $false) | spl5_3),
% 3.09/0.89 inference(forward_demodulation,[],[f823,f421])).
% 3.09/0.89 thf(f826,plain,(
% 3.09/0.89 $false | spl5_3),
% 3.09/0.89 inference(trivial_inequality_removal,[],[f825])).
% 3.09/0.89 thf(f827,plain,(
% 3.09/0.89 spl5_3),
% 3.09/0.89 inference(avatar_contradiction_clause,[],[f826])).
% 3.09/0.89 cnf(s5, plain, ~spl5_3, inference(sat_conversion,[],[f397])).
% 3.09/0.89 cnf(s9, plain, spl5_3, inference(sat_conversion,[],[f827])).
% 3.09/0.89 cnf(s11, plain, $false, inference(rat,[],[s5,s9])).
% 3.09/0.89 thf(f828,plain,(
% 3.09/0.89 $false),
% 3.09/0.89 inference(avatar_sat_refutation,[],[s11])).
% 3.09/0.89 % SZS output end Proof for theBenchmark
% 3.09/0.89 % (1464481)------------------------------
% 3.09/0.89 % (1464481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.09/0.89 % (1464481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.89 % (1464481)CaDiCaL version: 2.1.3
% 3.09/0.89 % (1464481)Termination reason: Refutation
% 3.09/0.89 % (1464481)Time elapsed: 0.104 s
% 3.09/0.89 % (1464481)Peak memory usage: 15 MB
% 3.09/0.89 % (1464481)Instructions burned: 210 (million)
% 3.09/0.89 % (1464364)Success in time 0.601 s
% 3.09/0.89 % Vampire exiting
%------------------------------------------------------------------------------