%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO881^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:48:32 AM UTC 2026
% Result : Theorem 5.51s 1.08s
% Output : Refutation 5.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO881^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n026.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 17:26:51 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.77/0.36 % (906303)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.77/0.36 % (906314)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.77/0.36 % (906314)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.77/0.36 % (906314)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=3306047923:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.77/0.36 % (906308)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2601471230:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.77/0.36 % (906309)lrs+10_16_si=on:nwc=1.5:random_seed=2011676050:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.77/0.36 % (906310)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1241977244:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.77/0.36 % (906312)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=205031717:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.77/0.36 % (906311)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=3277508617: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.77/0.36 % (906313)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3861765603:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.77/0.36 % (906310)Instruction limit reached!
% 0.77/0.36 % (906310)------------------------------
% 0.77/0.36 % (906310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.36 % (906310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.36 % (906310)CaDiCaL version: 2.1.3
% 0.77/0.36 % (906310)Termination reason: Instruction limit
% 0.77/0.36 % (906310)Termination phase: shuffling
% 0.77/0.36 % (906310)Time elapsed: 0.002 s
% 0.77/0.36 % (906310)Peak memory usage: 10 MB
% 0.77/0.36 % (906310)Instructions burned: 4 (million)
% 0.77/0.36 % (906309)Instruction limit reached!
% 0.77/0.36 % (906309)------------------------------
% 0.77/0.36 % (906309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.36 % (906309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.36 % (906309)CaDiCaL version: 2.1.3
% 0.77/0.36 % (906309)Termination reason: Instruction limit
% 0.77/0.36 % (906309)Termination phase: Property scanning
% 0.77/0.36 % (906309)Time elapsed: 0.008 s
% 0.77/0.36 % (906309)Peak memory usage: 10 MB
% 0.77/0.36 % (906309)Instructions burned: 18 (million)
% 0.77/0.36 % (906312)Instruction limit reached!
% 0.77/0.36 % (906312)------------------------------
% 0.77/0.36 % (906312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.36 % (906312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.36 % (906312)CaDiCaL version: 2.1.3
% 0.77/0.36 % (906312)Termination reason: Instruction limit
% 0.77/0.37 % (906312)Termination phase: Property scanning
% 0.77/0.37 % (906312)Time elapsed: 0.011 s
% 0.77/0.37 % (906312)Peak memory usage: 10 MB
% 0.77/0.37 % (906312)Instructions burned: 24 (million)
% 0.77/0.37 % (906322)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1905476219:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.77/0.37 % (906322)Instruction limit reached!
% 0.77/0.37 % (906322)------------------------------
% 0.77/0.37 % (906322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.37 % (906322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.37 % (906322)CaDiCaL version: 2.1.3
% 0.77/0.37 % (906322)Termination reason: Instruction limit
% 0.77/0.37 % (906322)Termination phase: shuffling
% 0.77/0.37 % (906322)Time elapsed: 0.002 s
% 0.77/0.37 % (906322)Peak memory usage: 10 MB
% 0.77/0.37 % (906322)Instructions burned: 4 (million)
% 0.77/0.37 % (906324)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.77/0.37 % (906323)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2060429300:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.77/0.39 % (906324)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2930372964:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.77/0.39 % (906323)Instruction limit reached!
% 0.77/0.39 % (906323)------------------------------
% 0.77/0.39 % (906323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.39 % (906323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.39 % (906323)CaDiCaL version: 2.1.3
% 0.77/0.39 % (906323)Termination reason: Instruction limit
% 0.77/0.39 % (906323)Termination phase: shuffling
% 0.77/0.39 % (906323)Time elapsed: 0.003 s
% 0.77/0.39 % (906323)Peak memory usage: 10 MB
% 0.77/0.39 % (906323)Instructions burned: 6 (million)
% 0.77/0.39 % (906313)Instruction limit reached!
% 0.77/0.39 % (906313)------------------------------
% 0.77/0.39 % (906313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.39 % (906313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.39 % (906313)CaDiCaL version: 2.1.3
% 0.77/0.39 % (906313)Termination reason: Instruction limit
% 0.77/0.39 % (906313)Termination phase: Property scanning
% 0.77/0.39 % (906313)Time elapsed: 0.032 s
% 0.77/0.39 % (906313)Peak memory usage: 11 MB
% 0.77/0.39 % (906313)Instructions burned: 76 (million)
% 0.77/0.39 % (906314)Instruction limit reached!
% 0.77/0.39 % (906314)------------------------------
% 0.77/0.39 % (906314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.39 % (906314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.39 % (906314)CaDiCaL version: 2.1.3
% 0.77/0.39 % (906314)Termination reason: Instruction limit
% 0.77/0.39 % (906314)Termination phase: Saturation
% 0.77/0.39 % (906314)Time elapsed: 0.042 s
% 0.77/0.39 % (906314)Peak memory usage: 14 MB
% 0.77/0.39 % (906314)Instructions burned: 160 (million)
% 0.77/0.39 % (906324)Instruction limit reached!
% 0.77/0.39 % (906324)------------------------------
% 0.77/0.39 % (906324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.39 % (906324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.39 % (906324)CaDiCaL version: 2.1.3
% 0.77/0.39 % (906324)Termination reason: Instruction limit
% 0.77/0.39 % (906324)Termination phase: shuffling
% 0.77/0.39 % (906324)Time elapsed: 0.004 s
% 0.77/0.39 % (906324)Peak memory usage: 10 MB
% 0.77/0.39 % (906324)Instructions burned: 9 (million)
% 0.77/0.39 % (906308)Instruction limit reached!
% 0.77/0.39 % (906308)------------------------------
% 0.77/0.39 % (906308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.39 % (906308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.39 % (906308)CaDiCaL version: 2.1.3
% 0.77/0.39 % (906308)Termination reason: Instruction limit
% 0.77/0.39 % (906308)Termination phase: Saturation
% 0.77/0.39 % (906308)Time elapsed: 0.040 s
% 0.77/0.39 % (906308)Peak memory usage: 13 MB
% 0.77/0.39 % (906308)Instructions burned: 88 (million)
% 0.77/0.39 % (906326)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=618625245:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.77/0.39 % (906331)lrs+10_1_si=on:cs=on:random_seed=2521090670:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.77/0.39 % (906329)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.77/0.39 % (906329)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.77/0.39 % (906331)Instruction limit reached!
% 0.77/0.39 % (906331)------------------------------
% 0.77/0.39 % (906331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.39 % (906331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.39 % (906331)CaDiCaL version: 2.1.3
% 0.77/0.39 % (906331)Termination reason: Instruction limit
% 0.77/0.39 % (906331)Termination phase: shuffling
% 0.77/0.39 % (906331)Time elapsed: 0.002 s
% 0.77/0.39 % (906331)Peak memory usage: 10 MB
% 0.77/0.39 % (906331)Instructions burned: 8 (million)
% 0.77/0.39 % (906329)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=454089243:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.77/0.42 % (906332)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.77/0.42 % (906330)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=3610711425:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.77/0.42 % (906326)Instruction limit reached!
% 0.77/0.42 % (906326)------------------------------
% 0.77/0.42 % (906326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.42 % (906326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.42 % (906326)CaDiCaL version: 2.1.3
% 0.77/0.42 % (906326)Termination reason: Instruction limit
% 0.77/0.42 % (906326)Termination phase: Property scanning
% 0.77/0.42 % (906326)Time elapsed: 0.010 s
% 0.77/0.42 % (906326)Peak memory usage: 10 MB
% 0.77/0.42 % (906326)Instructions burned: 18 (million)
% 0.77/0.42 % (906332)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=3643578552:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.77/0.42 % (906332)Instruction limit reached!
% 0.77/0.42 % (906332)------------------------------
% 0.77/0.42 % (906332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.42 % (906332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.42 % (906332)CaDiCaL version: 2.1.3
% 0.77/0.42 % (906332)Termination reason: Instruction limit
% 0.77/0.42 % (906332)Termination phase: shuffling
% 0.77/0.42 % (906332)Time elapsed: 0.002 s
% 0.77/0.42 % (906332)Peak memory usage: 10 MB
% 0.77/0.42 % (906332)Instructions burned: 5 (million)
% 0.77/0.42 % (906333)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3147890480:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.77/0.42 % (906336)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3378097577:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.77/0.42 % (906329)Instruction limit reached!
% 0.77/0.42 % (906329)------------------------------
% 0.77/0.42 % (906329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.42 % (906329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.42 % (906329)CaDiCaL version: 2.1.3
% 0.77/0.42 % (906329)Termination reason: Instruction limit
% 0.77/0.42 % (906329)Termination phase: Property scanning
% 0.77/0.42 % (906329)Time elapsed: 0.014 s
% 0.77/0.42 % (906329)Peak memory usage: 10 MB
% 0.77/0.42 % (906329)Instructions burned: 34 (million)
% 0.77/0.42 % (906336)Refutation not found, incomplete strategy
% 0.77/0.42 % (906336)------------------------------
% 0.77/0.42 % (906336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.42 % (906336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.42 % (906336)CaDiCaL version: 2.1.3
% 0.77/0.42 % (906336)Termination reason: Refutation not found, incomplete strategy
% 0.77/0.42 % (906336)Time elapsed: 0.012 s
% 0.77/0.42 % (906336)Peak memory usage: 13 MB
% 0.77/0.42 % (906336)Instructions burned: 48 (million)
% 0.77/0.42 % (906336)------------------------------
% 0.77/0.42 % (906336)------------------------------
% 0.77/0.42 % (906339)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1959825168:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.77/0.42 % (906333)Instruction limit reached!
% 0.77/0.42 % (906333)------------------------------
% 0.77/0.42 % (906333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.42 % (906333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.42 % (906333)CaDiCaL version: 2.1.3
% 0.77/0.42 % (906333)Termination reason: Instruction limit
% 0.77/0.42 % (906333)Termination phase: Saturation
% 0.77/0.42 % (906333)Time elapsed: 0.019 s
% 0.77/0.42 % (906333)Peak memory usage: 12 MB
% 0.77/0.42 % (906333)Instructions burned: 40 (million)
% 0.77/0.42 % (906343)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1208584219:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.52/0.47 % (906346)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2119689282:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.52/0.47 % (906344)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=246869868:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.52/0.47 % (906339)Instruction limit reached!
% 1.52/0.47 % (906339)------------------------------
% 1.52/0.47 % (906339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.47 % (906339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.47 % (906339)CaDiCaL version: 2.1.3
% 1.52/0.47 % (906339)Termination reason: Instruction limit
% 1.52/0.47 % (906339)Termination phase: Property scanning
% 1.52/0.47 % (906339)Time elapsed: 0.011 s
% 1.52/0.47 % (906339)Peak memory usage: 10 MB
% 1.52/0.47 % (906339)Instructions burned: 25 (million)
% 1.52/0.47 % (906343)Instruction limit reached!
% 1.52/0.47 % (906343)------------------------------
% 1.52/0.47 % (906343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.47 % (906343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.47 % (906343)CaDiCaL version: 2.1.3
% 1.52/0.47 % (906343)Termination reason: Instruction limit
% 1.52/0.47 % (906343)Termination phase: Property scanning
% 1.52/0.47 % (906343)Time elapsed: 0.007 s
% 1.52/0.47 % (906343)Peak memory usage: 10 MB
% 1.52/0.47 % (906343)Instructions burned: 16 (million)
% 1.52/0.47 % (906346)Instruction limit reached!
% 1.52/0.47 % (906346)------------------------------
% 1.52/0.47 % (906346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.47 % (906346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.47 % (906346)CaDiCaL version: 2.1.3
% 1.52/0.47 % (906346)Termination reason: Instruction limit
% 1.52/0.47 % (906346)Termination phase: Property scanning
% 1.52/0.47 % (906346)Time elapsed: 0.004 s
% 1.52/0.47 % (906346)Peak memory usage: 10 MB
% 1.52/0.47 % (906346)Instructions burned: 18 (million)
% 1.52/0.47 % (906330)Instruction limit reached!
% 1.52/0.47 % (906330)------------------------------
% 1.52/0.47 % (906330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.47 % (906330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.47 % (906330)CaDiCaL version: 2.1.3
% 1.52/0.47 % (906330)Termination reason: Instruction limit
% 1.52/0.47 % (906330)Termination phase: Saturation
% 1.52/0.47 % (906330)Time elapsed: 0.038 s
% 1.52/0.47 % (906330)Peak memory usage: 13 MB
% 1.52/0.47 % (906330)Instructions burned: 87 (million)
% 1.52/0.47 % (906347)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2373130793: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.52/0.47 % (906353)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3389493570:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.52/0.47 % (906347)Instruction limit reached!
% 1.52/0.47 % (906347)------------------------------
% 1.52/0.47 % (906347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.47 % (906347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.47 % (906347)CaDiCaL version: 2.1.3
% 1.52/0.47 % (906347)Termination reason: Instruction limit
% 1.52/0.47 % (906347)Termination phase: shuffling
% 1.52/0.47 % (906347)Time elapsed: 0.002 s
% 1.52/0.47 % (906347)Peak memory usage: 10 MB
% 1.52/0.47 % (906347)Instructions burned: 4 (million)
% 1.52/0.47 % (906351)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3931863055:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.52/0.47 % (906354)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.52/0.47 % (906354)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.52/0.47 % (906352)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3105183744:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.52/0.47 % (906354)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=2772605821:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.52/0.53 % (906353)Instruction limit reached!
% 1.52/0.53 % (906353)------------------------------
% 1.52/0.53 % (906353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.53 % (906353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.53 % (906353)CaDiCaL version: 2.1.3
% 1.52/0.53 % (906353)Termination reason: Instruction limit
% 1.52/0.53 % (906353)Termination phase: Saturation
% 1.52/0.53 % (906353)Time elapsed: 0.014 s
% 1.52/0.53 % (906353)Peak memory usage: 12 MB
% 1.52/0.53 % (906353)Instructions burned: 60 (million)
% 1.52/0.53 % (906357)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.52/0.53 % (906351)Instruction limit reached!
% 1.52/0.53 % (906351)------------------------------
% 1.52/0.53 % (906351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.53 % (906351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.53 % (906351)CaDiCaL version: 2.1.3
% 1.52/0.53 % (906351)Termination reason: Instruction limit
% 1.52/0.53 % (906351)Termination phase: Property scanning
% 1.52/0.53 % (906351)Time elapsed: 0.012 s
% 1.52/0.53 % (906351)Peak memory usage: 10 MB
% 1.52/0.53 % (906351)Instructions burned: 27 (million)
% 1.52/0.53 % (906354)Instruction limit reached!
% 1.52/0.53 % (906354)------------------------------
% 1.52/0.53 % (906354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.53 % (906354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.53 % (906354)CaDiCaL version: 2.1.3
% 1.52/0.53 % (906354)Termination reason: Instruction limit
% 1.52/0.53 % (906354)Termination phase: shuffling
% 1.52/0.53 % (906354)Time elapsed: 0.007 s
% 1.52/0.53 % (906354)Peak memory usage: 10 MB
% 1.52/0.53 % (906354)Instructions burned: 15 (million)
% 1.52/0.53 % (906352)Instruction limit reached!
% 1.52/0.53 % (906352)------------------------------
% 1.52/0.53 % (906352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.53 % (906352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.53 % (906352)CaDiCaL version: 2.1.3
% 1.52/0.53 % (906352)Termination reason: Instruction limit
% 1.52/0.53 % (906352)Termination phase: Property scanning
% 1.52/0.53 % (906352)Time elapsed: 0.011 s
% 1.52/0.53 % (906352)Peak memory usage: 10 MB
% 1.52/0.53 % (906352)Instructions burned: 24 (million)
% 1.52/0.53 % (906357)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=2823954964:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.52/0.53 % (906357)Instruction limit reached!
% 1.52/0.53 % (906357)------------------------------
% 1.52/0.53 % (906357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.53 % (906357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.53 % (906357)CaDiCaL version: 2.1.3
% 1.52/0.53 % (906357)Termination reason: Instruction limit
% 1.52/0.53 % (906357)Termination phase: shuffling
% 1.52/0.53 % (906357)Time elapsed: 0.004 s
% 1.52/0.53 % (906357)Peak memory usage: 10 MB
% 1.52/0.53 % (906357)Instructions burned: 9 (million)
% 1.52/0.53 % (906361)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=3650210325:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.52/0.53 % (906361)Instruction limit reached!
% 1.52/0.53 % (906361)------------------------------
% 1.52/0.53 % (906361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.53 % (906361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.53 % (906361)CaDiCaL version: 2.1.3
% 1.52/0.53 % (906361)Termination reason: Instruction limit
% 1.52/0.53 % (906361)Termination phase: Property scanning
% 1.52/0.53 % (906361)Time elapsed: 0.007 s
% 1.52/0.53 % (906361)Peak memory usage: 10 MB
% 1.52/0.53 % (906361)Instructions burned: 34 (million)
% 1.52/0.53 % (906362)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=22649586:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.52/0.53 % (906363)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2680701713:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.19/0.60 % (906364)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2931788330:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.19/0.60 % (906362)Instruction limit reached!
% 2.19/0.60 % (906362)------------------------------
% 2.19/0.60 % (906362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.60 % (906362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.60 % (906362)CaDiCaL version: 2.1.3
% 2.19/0.60 % (906362)Termination reason: Instruction limit
% 2.19/0.60 % (906362)Termination phase: shuffling
% 2.19/0.60 % (906362)Time elapsed: 0.004 s
% 2.19/0.60 % (906362)Peak memory usage: 10 MB
% 2.19/0.60 % (906362)Instructions burned: 9 (million)
% 2.19/0.60 % (906368)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3472411436:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.19/0.60 % (906367)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3728084299:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.19/0.60 % (906363)Instruction limit reached!
% 2.19/0.60 % (906363)------------------------------
% 2.19/0.60 % (906363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.60 % (906363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.60 % (906363)CaDiCaL version: 2.1.3
% 2.19/0.60 % (906363)Termination reason: Instruction limit
% 2.19/0.60 % (906363)Termination phase: Property scanning
% 2.19/0.60 % (906363)Time elapsed: 0.010 s
% 2.19/0.60 % (906363)Peak memory usage: 10 MB
% 2.19/0.60 % (906363)Instructions burned: 24 (million)
% 2.19/0.60 % (906364)Instruction limit reached!
% 2.19/0.60 % (906364)------------------------------
% 2.19/0.60 % (906364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.60 % (906364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.60 % (906364)CaDiCaL version: 2.1.3
% 2.19/0.60 % (906364)Termination reason: Instruction limit
% 2.19/0.60 % (906364)Termination phase: SInE selection
% 2.19/0.60 % (906364)Time elapsed: 0.013 s
% 2.19/0.60 % (906364)Peak memory usage: 10 MB
% 2.19/0.60 % (906364)Instructions burned: 29 (million)
% 2.19/0.60 % (906372)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3380465023:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.19/0.60 % (906375)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=392084057:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 2.19/0.60 % (906376)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.19/0.60 % (906376)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1488699753:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 2.19/0.60 % (906376)Instruction limit reached!
% 2.19/0.60 % (906376)------------------------------
% 2.19/0.60 % (906376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.60 % (906376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.60 % (906376)CaDiCaL version: 2.1.3
% 2.19/0.60 % (906376)Termination reason: Instruction limit
% 2.19/0.60 % (906376)Termination phase: shuffling
% 2.19/0.60 % (906376)Time elapsed: 0.003 s
% 2.19/0.60 % (906376)Peak memory usage: 10 MB
% 2.19/0.60 % (906376)Instructions burned: 7 (million)
% 2.19/0.60 % (906368)Instruction limit reached!
% 2.19/0.60 % (906368)------------------------------
% 2.19/0.60 % (906368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.60 % (906368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.60 % (906368)CaDiCaL version: 2.1.3
% 2.19/0.60 % (906368)Termination reason: Instruction limit
% 2.19/0.60 % (906368)Termination phase: Saturation
% 2.19/0.60 % (906368)Time elapsed: 0.036 s
% 2.19/0.60 % (906368)Peak memory usage: 13 MB
% 2.19/0.60 % (906368)Instructions burned: 144 (million)
% 2.19/0.60 % (906375)Instruction limit reached!
% 2.19/0.60 % (906375)------------------------------
% 2.19/0.60 % (906375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.60 % (906375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.60 % (906375)CaDiCaL version: 2.1.3
% 2.64/0.66 % (906375)Termination reason: Instruction limit
% 2.64/0.66 % (906375)Termination phase: Function definition elimination
% 2.64/0.66 % (906375)Time elapsed: 0.018 s
% 2.64/0.66 % (906375)Peak memory usage: 11 MB
% 2.64/0.66 % (906375)Instructions burned: 43 (million)
% 2.64/0.66 % (906381)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=3550296950: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.64/0.66 % (906380)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1733120623:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.64/0.66 % (906382)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.64/0.66 % (906381)Refutation not found, incomplete strategy
% 2.64/0.66 % (906381)------------------------------
% 2.64/0.66 % (906381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.66 % (906381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.66 % (906381)CaDiCaL version: 2.1.3
% 2.64/0.66 % (906381)Termination reason: Refutation not found, incomplete strategy
% 2.64/0.66 % (906381)Time elapsed: 0.011 s
% 2.64/0.66 % (906381)Peak memory usage: 12 MB
% 2.64/0.66 % (906381)Instructions burned: 44 (million)
% 2.64/0.66 % (906381)------------------------------
% 2.64/0.66 % (906381)------------------------------
% 2.64/0.66 % (906382)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3395549186: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.64/0.66 % (906382)Instruction limit reached!
% 2.64/0.66 % (906382)------------------------------
% 2.64/0.66 % (906382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.66 % (906382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.66 % (906382)CaDiCaL version: 2.1.3
% 2.64/0.66 % (906382)Termination reason: Instruction limit
% 2.64/0.66 % (906382)Termination phase: shuffling
% 2.64/0.66 % (906382)Time elapsed: 0.003 s
% 2.64/0.66 % (906382)Peak memory usage: 10 MB
% 2.64/0.66 % (906382)Instructions burned: 6 (million)
% 2.64/0.66 % (906385)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1314055376:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.64/0.66 % (906385)Instruction limit reached!
% 2.64/0.66 % (906385)------------------------------
% 2.64/0.66 % (906385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.66 % (906385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.66 % (906385)CaDiCaL version: 2.1.3
% 2.64/0.66 % (906385)Termination reason: Instruction limit
% 2.64/0.66 % (906385)Termination phase: Property scanning
% 2.64/0.66 % (906385)Time elapsed: 0.005 s
% 2.64/0.66 % (906385)Peak memory usage: 10 MB
% 2.64/0.66 % (906385)Instructions burned: 23 (million)
% 2.64/0.66 % (906387)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2139097846:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.64/0.66 % (906389)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=167823799:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.64/0.66 % (906387)Instruction limit reached!
% 2.64/0.66 % (906387)------------------------------
% 2.64/0.66 % (906387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.66 % (906387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.66 % (906387)CaDiCaL version: 2.1.3
% 2.64/0.66 % (906387)Termination reason: Instruction limit
% 2.64/0.66 % (906387)Termination phase: Property scanning
% 2.64/0.66 % (906387)Time elapsed: 0.008 s
% 2.64/0.66 % (906387)Peak memory usage: 10 MB
% 2.64/0.66 % (906387)Instructions burned: 19 (million)
% 2.64/0.66 % (906344)Instruction limit reached!
% 2.64/0.66 % (906344)------------------------------
% 2.64/0.66 % (906344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.66 % (906344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.66 % (906344)CaDiCaL version: 2.1.3
% 2.64/0.66 % (906344)Termination reason: Instruction limit
% 3.12/0.73 % (906344)Termination phase: Saturation
% 3.12/0.73 % (906344)Time elapsed: 0.164 s
% 3.12/0.73 % (906344)Peak memory usage: 14 MB
% 3.12/0.73 % (906344)Instructions burned: 328 (million)
% 3.12/0.73 % (906392)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=2558767069: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.12/0.73 % (906372)Instruction limit reached!
% 3.12/0.73 % (906372)------------------------------
% 3.12/0.73 % (906372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.73 % (906372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.73 % (906372)CaDiCaL version: 2.1.3
% 3.12/0.73 % (906372)Termination reason: Instruction limit
% 3.12/0.73 % (906372)Termination phase: Saturation
% 3.12/0.73 % (906372)Time elapsed: 0.092 s
% 3.12/0.73 % (906372)Peak memory usage: 15 MB
% 3.12/0.73 % (906372)Instructions burned: 193 (million)
% 3.12/0.73 % (906393)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=2336263255:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 3.12/0.73 % (906395)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3731737505:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 3.12/0.73 % (906380)Instruction limit reached!
% 3.12/0.73 % (906380)------------------------------
% 3.12/0.73 % (906380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.73 % (906380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.73 % (906380)CaDiCaL version: 2.1.3
% 3.12/0.73 % (906380)Termination reason: Instruction limit
% 3.12/0.73 % (906380)Termination phase: Saturation
% 3.12/0.73 % (906380)Time elapsed: 0.092 s
% 3.12/0.73 % (906380)Peak memory usage: 14 MB
% 3.12/0.73 % (906380)Instructions burned: 182 (million)
% 3.12/0.73 % (906393)Instruction limit reached!
% 3.12/0.73 % (906393)------------------------------
% 3.12/0.73 % (906393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.73 % (906393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.73 % (906393)CaDiCaL version: 2.1.3
% 3.12/0.73 % (906393)Termination reason: Instruction limit
% 3.12/0.73 % (906393)Termination phase: Property scanning
% 3.12/0.73 % (906393)Time elapsed: 0.021 s
% 3.12/0.73 % (906393)Peak memory usage: 11 MB
% 3.12/0.73 % (906393)Instructions burned: 46 (million)
% 3.12/0.73 % (906395)Refutation not found, incomplete strategy
% 3.12/0.73 % (906395)------------------------------
% 3.12/0.73 % (906395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.73 % (906395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.73 % (906395)CaDiCaL version: 2.1.3
% 3.12/0.73 % (906395)Termination reason: Refutation not found, incomplete strategy
% 3.12/0.73 % (906395)Time elapsed: 0.026 s
% 3.12/0.73 % (906395)Peak memory usage: 13 MB
% 3.12/0.73 % (906395)Instructions burned: 54 (million)
% 3.12/0.73 % (906395)------------------------------
% 3.12/0.73 % (906395)------------------------------
% 3.12/0.73 % (906389)Instruction limit reached!
% 3.12/0.73 % (906389)------------------------------
% 3.12/0.73 % (906389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.73 % (906389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.73 % (906389)CaDiCaL version: 2.1.3
% 3.12/0.73 % (906389)Termination reason: Instruction limit
% 3.12/0.73 % (906389)Termination phase: Saturation
% 3.12/0.73 % (906389)Time elapsed: 0.075 s
% 3.12/0.73 % (906389)Peak memory usage: 18 MB
% 3.12/0.73 % (906389)Instructions burned: 320 (million)
% 3.12/0.73 % (906398)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=883799570: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.12/0.73 % (906399)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.12/0.73 % (906399)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1076748611:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.12/0.73 % (906401)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=3978287171:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.62/0.88 % (906398)Instruction limit reached!
% 3.62/0.88 % (906398)------------------------------
% 3.62/0.88 % (906398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.88 % (906398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.88 % (906398)CaDiCaL version: 2.1.3
% 3.62/0.88 % (906398)Termination reason: Instruction limit
% 3.62/0.88 % (906398)Termination phase: Property scanning
% 3.62/0.88 % (906398)Time elapsed: 0.010 s
% 3.62/0.88 % (906398)Peak memory usage: 10 MB
% 3.62/0.88 % (906398)Instructions burned: 22 (million)
% 3.62/0.88 % (906400)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2047551269:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.62/0.88 % (906400)Instruction limit reached!
% 3.62/0.88 % (906400)------------------------------
% 3.62/0.88 % (906400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.88 % (906400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.88 % (906400)CaDiCaL version: 2.1.3
% 3.62/0.88 % (906400)Termination reason: Instruction limit
% 3.62/0.88 % (906400)Termination phase: shuffling
% 3.62/0.88 % (906400)Time elapsed: 0.006 s
% 3.62/0.88 % (906400)Peak memory usage: 10 MB
% 3.62/0.88 % (906400)Instructions burned: 14 (million)
% 3.62/0.88 % (906401)Instruction limit reached!
% 3.62/0.88 % (906401)------------------------------
% 3.62/0.88 % (906401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.88 % (906401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.88 % (906401)CaDiCaL version: 2.1.3
% 3.62/0.88 % (906401)Termination reason: Instruction limit
% 3.62/0.88 % (906401)Termination phase: Function definition elimination
% 3.62/0.88 % (906401)Time elapsed: 0.014 s
% 3.62/0.88 % (906401)Peak memory usage: 11 MB
% 3.62/0.88 % (906401)Instructions burned: 67 (million)
% 3.62/0.88 % (906405)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1207000606:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.62/0.88 % (906408)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1258952080:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2996 on theBenchmark for (2996ds/137Mi)
% 3.62/0.88 % (906407)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2354914415:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 3.62/0.88 % (906407)Instruction limit reached!
% 3.62/0.88 % (906407)------------------------------
% 3.62/0.88 % (906407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.88 % (906407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.88 % (906407)CaDiCaL version: 2.1.3
% 3.62/0.88 % (906407)Termination reason: Instruction limit
% 3.62/0.88 % (906407)Termination phase: Property scanning
% 3.62/0.88 % (906407)Time elapsed: 0.013 s
% 3.62/0.88 % (906407)Peak memory usage: 10 MB
% 3.62/0.88 % (906407)Instructions burned: 31 (million)
% 3.62/0.88 % (906405)Instruction limit reached!
% 3.62/0.88 % (906405)------------------------------
% 3.62/0.88 % (906405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.88 % (906405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.88 % (906405)CaDiCaL version: 2.1.3
% 3.62/0.88 % (906405)Termination reason: Instruction limit
% 3.62/0.88 % (906405)Termination phase: Function definition elimination
% 3.62/0.88 % (906405)Time elapsed: 0.022 s
% 3.62/0.88 % (906405)Peak memory usage: 11 MB
% 3.62/0.88 % (906405)Instructions burned: 52 (million)
% 3.62/0.88 % (906311)Instruction limit reached!
% 3.62/0.88 % (906311)------------------------------
% 3.62/0.88 % (906311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.88 % (906311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.88 % (906311)CaDiCaL version: 2.1.3
% 3.62/0.88 % (906311)Termination reason: Instruction limit
% 3.62/0.88 % (906311)Termination phase: Saturation
% 3.62/0.88 % (906311)Time elapsed: 0.365 s
% 3.62/0.88 % (906311)Peak memory usage: 17 MB
% 3.62/0.88 % (906311)Instructions burned: 636 (million)
% 3.62/0.88 % (906413)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=707190845:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2996 on theBenchmark for (2996ds/67Mi)
% 4.10/1.00 % (906412)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=421390288:cond=on:i=34:hud=10:nm=10:rtra=on_2996 on theBenchmark for (2996ds/34Mi)
% 4.10/1.00 % (906408)Instruction limit reached!
% 4.10/1.00 % (906408)------------------------------
% 4.10/1.00 % (906408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/1.00 % (906408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.00 % (906408)CaDiCaL version: 2.1.3
% 4.10/1.00 % (906408)Termination reason: Instruction limit
% 4.10/1.00 % (906408)Termination phase: Saturation
% 4.10/1.00 % (906408)Time elapsed: 0.039 s
% 4.10/1.00 % (906408)Peak memory usage: 13 MB
% 4.10/1.00 % (906408)Instructions burned: 138 (million)
% 4.10/1.00 % (906414)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 4.10/1.00 % (906414)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3659992577:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 4.10/1.00 % (906417)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=597580624:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 4.10/1.00 % (906412)Instruction limit reached!
% 4.10/1.00 % (906412)------------------------------
% 4.10/1.00 % (906412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/1.00 % (906412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.00 % (906412)CaDiCaL version: 2.1.3
% 4.10/1.00 % (906412)Termination reason: Instruction limit
% 4.10/1.00 % (906412)Termination phase: Property scanning
% 4.10/1.00 % (906412)Time elapsed: 0.014 s
% 4.10/1.00 % (906412)Peak memory usage: 10 MB
% 4.10/1.00 % (906412)Instructions burned: 34 (million)
% 4.10/1.00 % (906413)Instruction limit reached!
% 4.10/1.00 % (906413)------------------------------
% 4.10/1.00 % (906413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/1.00 % (906413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.00 % (906413)CaDiCaL version: 2.1.3
% 4.10/1.00 % (906413)Termination reason: Instruction limit
% 4.10/1.00 % (906413)Termination phase: Property scanning
% 4.10/1.00 % (906413)Time elapsed: 0.029 s
% 4.10/1.00 % (906413)Peak memory usage: 11 MB
% 4.10/1.00 % (906413)Instructions burned: 69 (million)
% 4.10/1.00 % (906399)Instruction limit reached!
% 4.10/1.00 % (906399)------------------------------
% 4.10/1.00 % (906399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/1.00 % (906399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.00 % (906399)CaDiCaL version: 2.1.3
% 4.10/1.00 % (906399)Termination reason: Instruction limit
% 4.10/1.00 % (906399)Termination phase: Saturation
% 4.10/1.00 % (906399)Time elapsed: 0.096 s
% 4.10/1.00 % (906399)Peak memory usage: 13 MB
% 4.10/1.00 % (906399)Instructions burned: 202 (million)
% 4.10/1.00 % (906420)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3366438896:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 4.10/1.00 % (906421)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3069335967:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 4.10/1.00 % (906422)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3645148129:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 4.10/1.00 % (906414)Refutation not found, incomplete strategy
% 4.10/1.00 % (906414)------------------------------
% 4.10/1.00 % (906414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/1.00 % (906414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.00 % (906414)CaDiCaL version: 2.1.3
% 4.10/1.00 % (906414)Termination reason: Refutation not found, incomplete strategy
% 4.10/1.00 % (906414)Time elapsed: 0.042 s
% 4.10/1.00 % (906414)Peak memory usage: 13 MB
% 4.10/1.00 % (906414)Instructions burned: 100 (million)
% 4.10/1.00 % (906414)------------------------------
% 4.10/1.00 % (906414)------------------------------
% 4.10/1.00 % (906426)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=311509577:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/515Mi)
% 4.10/1.00 % (906421)Refutation not found, incomplete strategy
% 4.10/1.00 % (906421)------------------------------
% 5.51/1.08 % (906421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906421)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906421)Termination reason: Refutation not found, incomplete strategy
% 5.51/1.08 % (906421)Time elapsed: 0.023 s
% 5.51/1.08 % (906421)Peak memory usage: 13 MB
% 5.51/1.08 % (906421)Instructions burned: 49 (million)
% 5.51/1.08 % (906421)------------------------------
% 5.51/1.08 % (906421)------------------------------
% 5.51/1.08 % (906420)Instruction limit reached!
% 5.51/1.08 % (906420)------------------------------
% 5.51/1.08 % (906420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906420)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906420)Termination reason: Instruction limit
% 5.51/1.08 % (906420)Termination phase: Saturation
% 5.51/1.08 % (906420)Time elapsed: 0.042 s
% 5.51/1.08 % (906420)Peak memory usage: 13 MB
% 5.51/1.08 % (906420)Instructions burned: 96 (million)
% 5.51/1.08 % (906417)Instruction limit reached!
% 5.51/1.08 % (906417)------------------------------
% 5.51/1.08 % (906417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906417)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906417)Termination reason: Instruction limit
% 5.51/1.08 % (906417)Termination phase: Saturation
% 5.51/1.08 % (906417)Time elapsed: 0.067 s
% 5.51/1.08 % (906417)Peak memory usage: 14 MB
% 5.51/1.08 % (906417)Instructions burned: 248 (million)
% 5.51/1.08 % (906430)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2496207790:s2a=on:i=571:nm=16:rtra=on_2995 on theBenchmark for (2995ds/571Mi)
% 5.51/1.08 % (906428)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1116693546:st=1.5:i=130:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/130Mi)
% 5.51/1.08 % (906429)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=752758081:i=44:ep=R:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/44Mi)
% 5.51/1.08 % (906429)Instruction limit reached!
% 5.51/1.08 % (906429)------------------------------
% 5.51/1.08 % (906429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906429)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906429)Termination reason: Instruction limit
% 5.51/1.08 % (906429)Termination phase: Function definition elimination
% 5.51/1.08 % (906429)Time elapsed: 0.019 s
% 5.51/1.08 % (906429)Peak memory usage: 11 MB
% 5.51/1.08 % (906429)Instructions burned: 45 (million)
% 5.51/1.08 % (906434)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=2479746994:i=450:rtra=on:ixr=off:ntd=on_2994 on theBenchmark for (2994ds/450Mi)
% 5.51/1.08 % (906428)Instruction limit reached!
% 5.51/1.08 % (906428)------------------------------
% 5.51/1.08 % (906428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906428)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906428)Termination reason: Instruction limit
% 5.51/1.08 % (906428)Termination phase: Saturation
% 5.51/1.08 % (906428)Time elapsed: 0.065 s
% 5.51/1.08 % (906428)Peak memory usage: 15 MB
% 5.51/1.08 % (906428)Instructions burned: 130 (million)
% 5.51/1.08 % (906436)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=2692069723:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/95Mi)
% 5.51/1.08 % (906430)Instruction limit reached!
% 5.51/1.08 % (906430)------------------------------
% 5.51/1.08 % (906430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906430)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906430)Termination reason: Instruction limit
% 5.51/1.08 % (906430)Termination phase: Saturation
% 5.51/1.08 % (906430)Time elapsed: 0.125 s
% 5.51/1.08 % (906430)Peak memory usage: 15 MB
% 5.51/1.08 % (906430)Instructions burned: 572 (million)
% 5.51/1.08 % (906436)Instruction limit reached!
% 5.51/1.08 % (906436)------------------------------
% 5.51/1.08 % (906436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906436)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906436)Termination reason: Instruction limit
% 5.51/1.08 % (906436)Termination phase: Saturation
% 5.51/1.08 % (906436)Time elapsed: 0.042 s
% 5.51/1.08 % (906436)Peak memory usage: 13 MB
% 5.51/1.08 % (906436)Instructions burned: 95 (million)
% 5.51/1.08 % (906438)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=342888347:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 5.51/1.08 % (906439)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=755122589:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2993 on theBenchmark for (2993ds/105Mi)
% 5.51/1.08 % (906438)Instruction limit reached!
% 5.51/1.08 % (906438)------------------------------
% 5.51/1.08 % (906438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906438)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906438)Termination reason: Instruction limit
% 5.51/1.08 % (906438)Termination phase: Function definition elimination
% 5.51/1.08 % (906438)Time elapsed: 0.015 s
% 5.51/1.08 % (906438)Peak memory usage: 11 MB
% 5.51/1.08 % (906438)Instructions burned: 68 (million)
% 5.51/1.08 % (906442)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=2605489410:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2993 on theBenchmark for (2993ds/5755Mi)
% 5.51/1.08 % (906392)Instruction limit reached!
% 5.51/1.08 % (906392)------------------------------
% 5.51/1.08 % (906392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906392)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906392)Termination reason: Instruction limit
% 5.51/1.08 % (906392)Termination phase: Saturation
% 5.51/1.08 % (906392)Time elapsed: 0.406 s
% 5.51/1.08 % (906392)Peak memory usage: 16 MB
% 5.51/1.08 % (906392)Instructions burned: 854 (million)
% 5.51/1.08 % (906439)Instruction limit reached!
% 5.51/1.08 % (906439)------------------------------
% 5.51/1.08 % (906439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906439)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906439)Termination reason: Instruction limit
% 5.51/1.08 % (906439)Termination phase: Saturation
% 5.51/1.08 % (906439)Time elapsed: 0.047 s
% 5.51/1.08 % (906439)Peak memory usage: 13 MB
% 5.51/1.08 % (906439)Instructions burned: 106 (million)
% 5.51/1.08 % (906444)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=3571850427:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 5.51/1.08 % (906445)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2301915381:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/495Mi)
% 5.51/1.08 % (906426)Instruction limit reached!
% 5.51/1.08 % (906426)------------------------------
% 5.51/1.08 % (906426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906426)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906426)Termination reason: Instruction limit
% 5.51/1.08 % (906426)Termination phase: Saturation
% 5.51/1.08 % (906426)Time elapsed: 0.248 s
% 5.51/1.08 % (906426)Peak memory usage: 16 MB
% 5.51/1.08 % (906426)Instructions burned: 515 (million)
% 5.51/1.08 % (906448)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=1117176315:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 5.51/1.08 % (906434)Instruction limit reached!
% 5.51/1.08 % (906434)------------------------------
% 5.51/1.08 % (906434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906434)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906434)Termination reason: Instruction limit
% 5.51/1.08 % (906434)Termination phase: Saturation
% 5.51/1.08 % (906434)Time elapsed: 0.205 s
% 5.51/1.08 % (906434)Peak memory usage: 15 MB
% 5.51/1.08 % (906434)Instructions burned: 450 (million)
% 5.51/1.08 % (906448)Instruction limit reached!
% 5.51/1.08 % (906448)------------------------------
% 5.51/1.08 % (906448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906448)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906448)Termination reason: Instruction limit
% 5.51/1.08 % (906448)Termination phase: Property scanning
% 5.51/1.08 % (906448)Time elapsed: 0.015 s
% 5.51/1.08 % (906448)Peak memory usage: 10 MB
% 5.51/1.08 % (906448)Instructions burned: 35 (million)
% 5.51/1.08 % (906450)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1982199704:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/91Mi)
% 5.51/1.08 % (906451)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=1196287947:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2992 on theBenchmark for (2992ds/66Mi)
% 5.51/1.08 % (906445) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-906303-906445"...
% 5.51/1.08 % (906450)Instruction limit reached!
% 5.51/1.08 % (906450)------------------------------
% 5.51/1.08 % (906450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906450)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906450)Termination reason: Instruction limit
% 5.51/1.08 % (906450)Termination phase: Saturation
% 5.51/1.08 % (906450)Time elapsed: 0.046 s
% 5.51/1.08 % (906450)Peak memory usage: 13 MB
% 5.51/1.08 % (906450)Instructions burned: 92 (million)
% 5.51/1.08 % (906451)Instruction limit reached!
% 5.51/1.08 % (906451)------------------------------
% 5.51/1.08 % (906451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906451)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906451)Termination reason: Instruction limit
% 5.51/1.08 % (906451)Termination phase: Saturation
% 5.51/1.08 % (906451)Time elapsed: 0.030 s
% 5.51/1.08 % (906451)Peak memory usage: 13 MB
% 5.51/1.08 % (906451)Instructions burned: 66 (million)
% 5.51/1.08 % (906445)...printing done.
% 5.51/1.08 % (906445)Refutation found. Thanks to Tanya!
% 5.51/1.08 % SZS status Theorem for theBenchmark
% 5.51/1.08 % SZS output start Proof for theBenchmark
% 5.51/1.08 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 5.51/1.08 thf(func_def_0, type, c_Eps_i: (($i > $o) > $i)).
% 5.51/1.08 thf(func_def_1, type, c_False: $o).
% 5.51/1.08 thf(func_def_2, type, c_True: $o).
% 5.51/1.08 thf(func_def_3, type, c_not: ($o > $o)).
% 5.51/1.08 thf(func_def_4, type, c_and: ($o > $o > $o)).
% 5.51/1.08 thf(func_def_5, type, c_or: ($o > $o > $o)).
% 5.51/1.08 thf(func_def_6, type, c_iff: ($o > $o > $o)).
% 5.51/1.08 thf(func_def_7, type, c_In: ($i > $i > $o)).
% 5.51/1.08 thf(func_def_8, type, c_Subq: ($i > $i > $o)).
% 5.51/1.08 thf(func_def_10, type, c_Union: ($i > $i)).
% 5.51/1.08 thf(func_def_11, type, c_Power: ($i > $i)).
% 5.51/1.08 thf(func_def_12, type, c_Repl: ($i > ($i > $i) > $i)).
% 5.51/1.08 thf(func_def_13, type, c_TransSet: ($i > $o)).
% 5.51/1.08 thf(func_def_14, type, c_atleast2: ($i > $o)).
% 5.51/1.08 thf(func_def_15, type, c_atleast3: ($i > $o)).
% 5.51/1.08 thf(func_def_16, type, c_atleast4: ($i > $o)).
% 5.51/1.08 thf(func_def_17, type, c_atleast5: ($i > $o)).
% 5.51/1.08 thf(func_def_18, type, c_atleast6: ($i > $o)).
% 5.51/1.08 thf(func_def_19, type, c_exactly2: ($i > $o)).
% 5.51/1.08 thf(func_def_20, type, c_exactly3: ($i > $o)).
% 5.51/1.08 thf(func_def_21, type, c_exactly4: ($i > $o)).
% 5.51/1.08 thf(func_def_22, type, c_exactly5: ($i > $o)).
% 5.51/1.08 thf(func_def_23, type, c_exu_i: (($i > $o) > $o)).
% 5.51/1.08 thf(func_def_24, type, c_reflexive_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_25, type, c_irreflexive_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_26, type, c_symmetric_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_27, type, c_antisymmetric_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_28, type, c_transitive_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_29, type, c_eqreln_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_30, type, c_per_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_31, type, c_linear_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_32, type, c_trichotomous_or_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_33, type, c_partialorder_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_34, type, c_totalorder_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_35, type, c_strictpartialorder_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_36, type, c_stricttotalorder_i: (($i > $i > $o) > $o)).
% 5.51/1.08 thf(func_def_37, type, c_If_i: ($o > $i > $i > $i)).
% 5.51/1.08 thf(func_def_38, type, c_exactly1of2: ($o > $o > $o)).
% 5.51/1.08 thf(func_def_39, type, c_exactly1of3: ($o > $o > $o > $o)).
% 5.51/1.08 thf(func_def_40, type, c_nIn: ($i > $i > $o)).
% 5.51/1.08 thf(func_def_41, type, c_nSubq: ($i > $i > $o)).
% 5.51/1.08 thf(func_def_42, type, c_UPair: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_43, type, c_Sing: ($i > $i)).
% 5.51/1.08 thf(func_def_44, type, c_binunion: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_45, type, c_SetAdjoin: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_46, type, c_famunion: ($i > ($i > $i) > $i)).
% 5.51/1.08 thf(func_def_47, type, c_Sep: ($i > ($i > $o) > $i)).
% 5.51/1.08 thf(func_def_48, type, c_ReplSep: ($i > ($i > $o) > ($i > $i) > $i)).
% 5.51/1.08 thf(func_def_49, type, c_binintersect: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_50, type, c_setminus: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_51, type, c_inj: ($i > $i > ($i > $i) > $o)).
% 5.51/1.08 thf(func_def_52, type, c_bij: ($i > $i > ($i > $i) > $o)).
% 5.51/1.08 thf(func_def_53, type, c_atleastp: ($i > $i > $o)).
% 5.51/1.08 thf(func_def_54, type, c_equip: ($i > $i > $o)).
% 5.51/1.08 thf(func_def_55, type, c_In_rec_poly_G_i: (($i > ($i > $i) > $i) > $i > $i > $o)).
% 5.51/1.08 thf(func_def_56, type, c_In_rec_poly_i: (($i > ($i > $i) > $i) > $i > $i)).
% 5.51/1.08 thf(func_def_57, type, c_ordsucc: ($i > $i)).
% 5.51/1.08 thf(func_def_58, type, c_nat_p: ($i > $o)).
% 5.51/1.08 thf(func_def_59, type, c_nat_primrec: ($i > ($i > $i > $i) > $i > $i)).
% 5.51/1.08 thf(func_def_60, type, c_add_nat: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_61, type, c_mul_nat: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_62, type, c_ordinal: ($i > $o)).
% 5.51/1.08 thf(func_def_63, type, c_V_: ($i > $i)).
% 5.51/1.08 thf(func_def_64, type, c_Inj1: ($i > $i)).
% 5.51/1.08 thf(func_def_65, type, c_Inj0: ($i > $i)).
% 5.51/1.08 thf(func_def_66, type, c_Unj: ($i > $i)).
% 5.51/1.08 thf(func_def_67, type, c_combine_funcs: ($i > $i > ($i > $i) > ($i > $i) > $i > $i)).
% 5.51/1.08 thf(func_def_68, type, c_setsum: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_69, type, c_proj0: ($i > $i)).
% 5.51/1.08 thf(func_def_70, type, c_proj1: ($i > $i)).
% 5.51/1.08 thf(func_def_71, type, c_binrep: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_72, type, c_lam: ($i > ($i > $i) > $i)).
% 5.51/1.08 thf(func_def_73, type, c_setprod: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_74, type, c_ap: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_75, type, c_setsum_p: ($i > $o)).
% 5.51/1.08 thf(func_def_76, type, c_tuple_p: ($i > $i > $o)).
% 5.51/1.08 thf(func_def_77, type, c_Pi: ($i > ($i > $i) > $i)).
% 5.51/1.08 thf(func_def_78, type, c_setexp: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_79, type, c_Sep2: ($i > ($i > $i) > ($i > $i > $o) > $i)).
% 5.51/1.08 thf(func_def_80, type, c_set_of_pairs: ($i > $o)).
% 5.51/1.08 thf(func_def_81, type, c_lam2: ($i > ($i > $i) > ($i > $i > $i) > $i)).
% 5.51/1.08 thf(func_def_82, type, c_PNoEq_: ($i > ($i > $o) > ($i > $o) > $o)).
% 5.51/1.08 thf(func_def_83, type, c_PNoLt_: ($i > ($i > $o) > ($i > $o) > $o)).
% 5.51/1.08 thf(func_def_84, type, c_PNoLt: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 5.51/1.08 thf(func_def_85, type, c_PNoLe: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 5.51/1.08 thf(func_def_86, type, c_PNo_downc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 5.51/1.08 thf(func_def_87, type, c_PNo_upc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 5.51/1.08 thf(func_def_88, type, c_SNoElts_: ($i > $i)).
% 5.51/1.08 thf(func_def_89, type, c_SNo_: ($i > $i > $o)).
% 5.51/1.08 thf(func_def_90, type, c_PSNo: ($i > ($i > $o) > $i)).
% 5.51/1.08 thf(func_def_91, type, c_SNo: ($i > $o)).
% 5.51/1.08 thf(func_def_92, type, c_SNoLev: ($i > $i)).
% 5.51/1.08 thf(func_def_93, type, c_SNoEq_: ($i > $i > $i > $o)).
% 5.51/1.08 thf(func_def_94, type, c_SNoLt: ($i > $i > $o)).
% 5.51/1.08 thf(func_def_95, type, c_SNoLe: ($i > $i > $o)).
% 5.51/1.08 thf(func_def_96, type, c_binop_on: ($i > ($i > $i > $i) > $o)).
% 5.51/1.08 thf(func_def_97, type, c_Loop: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > $o)).
% 5.51/1.08 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)).
% 5.51/1.08 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)).
% 5.51/1.08 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)).
% 5.51/1.08 thf(func_def_101, type, c_combinator: ($i > $o)).
% 5.51/1.08 thf(func_def_102, type, c_combinator_equiv: ($i > $i > $o)).
% 5.51/1.08 thf(func_def_103, type, c_equip_mod: ($i > $i > $i > $o)).
% 5.51/1.08 thf(func_def_105, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 5.51/1.08 thf(func_def_106, type, db2: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_107, type, db1: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_108, type, db0: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_109, type, db4: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_110, type, db3: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_111, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 5.51/1.08 thf(func_def_112, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 5.51/1.08 thf(func_def_115, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 5.51/1.08 thf(func_def_116, type, vIMP: ($o > $o > $o)).
% 5.51/1.08 thf(func_def_117, type, db13: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_118, type, db12: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_119, type, db11: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_120, type, db10: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_121, type, db9: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_122, type, db8: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_123, type, db7: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_124, type, db6: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_125, type, db5: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_126, type, db14: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_127, type, db15: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_128, type, db16: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_129, type, db17: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_130, type, db18: !>[X0: $tType]:(X0)).
% 5.51/1.08 thf(func_def_131, type, sP0: (($i > $o) > $o)).
% 5.51/1.08 thf(func_def_132, type, sP1: (($i > $o) > $o)).
% 5.51/1.08 thf(func_def_133, type, sK2: (($i > $o) > $i)).
% 5.51/1.08 thf(func_def_134, type, sK3: (($i > $o) > $i > $i)).
% 5.51/1.08 thf(func_def_135, type, sK4: (($i > $o) > $i)).
% 5.51/1.08 thf(func_def_136, type, sK5: (($i > $o) > $i)).
% 5.51/1.08 thf(func_def_137, type, sK6: (($i > $o) > $i)).
% 5.51/1.08 thf(func_def_138, type, sK7: (($i > $o) > $i)).
% 5.51/1.08 thf(func_def_139, type, sK8: (($i > $o) > $i)).
% 5.51/1.08 thf(func_def_140, type, sK9: $o).
% 5.51/1.08 thf(func_def_141, type, sK10: $o).
% 5.51/1.08 thf(func_def_142, type, vNOT: ($o > $o)).
% 5.51/1.08 thf(func_def_143, type, sK11: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_144, type, sK12: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_145, type, sK13: ($o > $o > $o)).
% 5.51/1.08 thf(func_def_146, type, sK14: ($o > $o > $o)).
% 5.51/1.08 thf(func_def_147, type, sK15: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_148, type, sK16: (($i > $i) > $i > $i > $i)).
% 5.51/1.08 thf(func_def_149, type, sK17: (($i > $i) > $i > $i > $i > $o)).
% 5.51/1.08 thf(func_def_150, type, sK18: ($i > $i > $i)).
% 5.51/1.08 thf(func_def_151, type, sK19: ($i > $i > $i > $o)).
% 5.51/1.08 thf(f5,axiom,(
% 5.51/1.08 (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 5.51/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5)).
% 5.51/1.08 thf(f7,axiom,(
% 5.51/1.08 ! [X0 : $i,X1 : $i] : (c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))),
% 5.51/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7)).
% 5.51/1.08 thf(f13,axiom,(
% 5.51/1.08 ((^[X0 : $o] : (X0 => c_False)) = c_not)),
% 5.51/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13)).
% 5.51/1.08 thf(f14,axiom,(
% 5.51/1.08 (c_and = (^[X0 : $o, X1 : $o] : (! [X2 : $o] : ((X0 => (X1 => X2)) => X2))))),
% 5.51/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14)).
% 5.51/1.08 thf(f16,axiom,(
% 5.51/1.08 (c_iff = (^[X0 : $o, X1 : $o] : ((c_and @ X0 => X1 @ X1 => X0))))),
% 5.51/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16)).
% 5.51/1.08 thf(f17,axiom,(
% 5.51/1.08 (c_Subq = (^[X0 : $i, X1 : $i] : (! [X2 : $i] : ((c_In @ X2 @ X0) => (c_In @ X2 @ X1)))))),
% 5.51/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17)).
% 5.51/1.08 thf(f109,conjecture,(
% 5.51/1.08 (c_not @ ! [X1 : ($i > $i > $i),X7 : $i,X2 : ($i > $o),X4 : ($i > $i),X5 : $i,X6 : $i,X3 : ($i > $o),X0 : ($i > $i > $o)] : (((X4 @ (X1 @ (X1 @ (X1 @ (X1 @ (X1 @ (X1 @ X6 @ X5) @ (X1 @ (X1 @ (X1 @ X6 @ X5) @ (X1 @ X7 @ (X1 @ (X1 @ (X1 @ X5 @ X5) @ (X1 @ (X1 @ (X1 @ (X1 @ X5 @ (X1 @ (X1 @ X6 @ (X1 @ X5 @ (X1 @ X5 @ X7))) @ X5)) @ X7) @ (X1 @ (X4 @ X6) @ X7)) @ (X1 @ (X1 @ (X1 @ (X1 @ X5 @ (X4 @ (X1 @ X7 @ X5))) @ (X1 @ X6 @ X6)) @ (X1 @ X6 @ (X1 @ X7 @ X5))) @ X5))) @ X7))) @ X5)) @ X6) @ (X1 @ X6 @ (X1 @ X5 @ (X1 @ (X1 @ (X4 @ X5) @ (X1 @ (X1 @ X6 @ X6) @ X6)) @ X5)))) @ (X4 @ (X4 @ X6))) @ X5))) = ((X4 @ (X4 @ X7)))))),
% 5.51/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 5.51/1.08 thf(f110,negated_conjecture,(
% 5.51/1.08 ~(c_not @ ! [X1 : ($i > $i > $i),X7 : $i,X2 : ($i > $o),X4 : ($i > $i),X5 : $i,X6 : $i,X3 : ($i > $o),X0 : ($i > $i > $o)] : (((X4 @ (X1 @ (X1 @ (X1 @ (X1 @ (X1 @ (X1 @ X6 @ X5) @ (X1 @ (X1 @ (X1 @ X6 @ X5) @ (X1 @ X7 @ (X1 @ (X1 @ (X1 @ X5 @ X5) @ (X1 @ (X1 @ (X1 @ (X1 @ X5 @ (X1 @ (X1 @ X6 @ (X1 @ X5 @ (X1 @ X5 @ X7))) @ X5)) @ X7) @ (X1 @ (X4 @ X6) @ X7)) @ (X1 @ (X1 @ (X1 @ (X1 @ X5 @ (X4 @ (X1 @ X7 @ X5))) @ (X1 @ X6 @ X6)) @ (X1 @ X6 @ (X1 @ X7 @ X5))) @ X5))) @ X7))) @ X5)) @ X6) @ (X1 @ X6 @ (X1 @ X5 @ (X1 @ (X1 @ (X4 @ X5) @ (X1 @ (X1 @ X6 @ X6) @ X6)) @ X5)))) @ (X4 @ (X4 @ X6))) @ X5))) = ((X4 @ (X4 @ X7)))))),
% 5.51/1.08 inference(negated_conjecture,[status(cth)],[f109])).
% 5.51/1.08 thf(f111,plain,(
% 5.51/1.08 ~(c_not @ ! [X0 : ($i > $i > $i),X1 : $i,X3 : ($i > $i),X4 : $i,X5 : $i] : (((X3 @ (X3 @ X1))) = ((X3 @ (X0 @ (X0 @ (X0 @ (X0 @ (X0 @ (X0 @ X5 @ X4) @ (X0 @ (X0 @ (X0 @ X5 @ X4) @ (X0 @ X1 @ (X0 @ (X0 @ (X0 @ X4 @ X4) @ (X0 @ (X0 @ (X0 @ (X0 @ X4 @ (X0 @ (X0 @ X5 @ (X0 @ X4 @ (X0 @ X4 @ X1))) @ X4)) @ X1) @ (X0 @ (X3 @ X5) @ X1)) @ (X0 @ (X0 @ (X0 @ (X0 @ X4 @ (X3 @ (X0 @ X1 @ X4))) @ (X0 @ X5 @ X5)) @ (X0 @ X5 @ (X0 @ X1 @ X4))) @ X4))) @ X1))) @ X4)) @ X5) @ (X0 @ X5 @ (X0 @ X4 @ (X0 @ (X0 @ (X3 @ X4) @ (X0 @ (X0 @ X5 @ X5) @ X5)) @ X4)))) @ (X3 @ (X3 @ X5))) @ X4)))))),
% 5.51/1.08 inference(rectify,[],[f110])).
% 5.51/1.08 thf(f112,plain,(
% 5.51/1.08 ~ ($true = ((c_not @ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $i) @ (^[Y2 : $i > $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ ($i > $i > $i) @ (^[Y4 : $i > $i > $i]: ((Y2 @ (Y2 @ Y3)) = (Y2 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ Y3 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ Y1 @ Y3))) @ Y1)) @ Y3) @ (Y4 @ (Y2 @ Y0) @ Y3)) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y2 @ (Y4 @ Y3 @ Y1))) @ (Y4 @ Y0 @ Y0)) @ (Y4 @ Y0 @ (Y4 @ Y3 @ Y1))) @ Y1))) @ Y3))) @ Y1)) @ Y0) @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ (Y2 @ Y1) @ (Y4 @ (Y4 @ Y0 @ Y0) @ Y0)) @ Y1)))) @ (Y2 @ (Y2 @ Y0))) @ Y1))))))))))))))))),
% 5.51/1.08 inference(fool_elimination,[],[f111])).
% 5.51/1.08 thf(f219,plain,(
% 5.51/1.08 ! [X0 : $i,X1 : $i] : (c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))),
% 5.51/1.08 inference(rectify,[],[f7])).
% 5.51/1.08 thf(f220,plain,(
% 5.51/1.08 ! [X1 : $i,X0 : $i] : (((c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))) = $true)),
% 5.51/1.08 inference(fool_elimination,[],[f219])).
% 5.51/1.08 thf(f237,plain,(
% 5.51/1.08 ((^[X0 : $o] : (X0 => c_False)) = c_not)),
% 5.51/1.08 inference(rectify,[],[f13])).
% 5.51/1.08 thf(f238,plain,(
% 5.51/1.08 (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 5.51/1.08 inference(fool_elimination,[],[f237])).
% 5.51/1.08 thf(f239,plain,(
% 5.51/1.08 (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 5.51/1.08 inference(rectify,[],[f5])).
% 5.51/1.08 thf(f240,plain,(
% 5.51/1.08 ($true = ((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 5.51/1.08 inference(fool_elimination,[],[f239])).
% 5.51/1.08 thf(f256,plain,(
% 5.51/1.08 (c_iff = (^[X0 : $o, X1 : $o] : ((c_and @ X0 => X1 @ X1 => X0))))),
% 5.51/1.08 inference(rectify,[],[f16])).
% 5.51/1.08 thf(f257,plain,(
% 5.51/1.08 (c_iff = (^[Y0 : $o]: ((^[Y1 : $o]: (c_and @ (Y0 => Y1) @ (Y1 => Y0))))))),
% 5.51/1.08 inference(fool_elimination,[],[f256])).
% 5.51/1.08 thf(f262,plain,(
% 5.51/1.08 (c_Subq = (^[X0 : $i, X1 : $i] : (! [X2 : $i] : ((c_In @ X2 @ X0) => (c_In @ X2 @ X1)))))),
% 5.51/1.08 inference(rectify,[],[f17])).
% 5.51/1.08 thf(f263,plain,(
% 5.51/1.08 (c_Subq = (^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))))),
% 5.51/1.08 inference(fool_elimination,[],[f262])).
% 5.51/1.08 thf(f290,plain,(
% 5.51/1.08 (c_and = (^[X0 : $o, X1 : $o] : (! [X2 : $o] : ((X0 => (X1 => X2)) => X2))))),
% 5.51/1.08 inference(rectify,[],[f14])).
% 5.51/1.08 thf(f291,plain,(
% 5.51/1.08 (c_and = (^[Y0 : $o]: ((^[Y1 : $o]: (!! @ $o @ (^[Y2 : $o]: ((Y0 => (Y1 => Y2)) => Y2)))))))),
% 5.51/1.08 inference(fool_elimination,[],[f290])).
% 5.51/1.08 thf(f308,plain,(
% 5.51/1.08 ($true != ((c_not @ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $i) @ (^[Y2 : $i > $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ ($i > $i > $i) @ (^[Y4 : $i > $i > $i]: ((Y2 @ (Y2 @ Y3)) = (Y2 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ Y3 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ Y1 @ Y3))) @ Y1)) @ Y3) @ (Y4 @ (Y2 @ Y0) @ Y3)) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y2 @ (Y4 @ Y3 @ Y1))) @ (Y4 @ Y0 @ Y0)) @ (Y4 @ Y0 @ (Y4 @ Y3 @ Y1))) @ Y1))) @ Y3))) @ Y1)) @ Y0) @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ (Y2 @ Y1) @ (Y4 @ (Y4 @ Y0 @ Y0) @ Y0)) @ Y1)))) @ (Y2 @ (Y2 @ Y0))) @ Y1))))))))))))))))),
% 5.51/1.08 inference(flattening,[],[f112])).
% 5.51/1.08 thf(f329,plain,(
% 5.51/1.08 ! [X0 : $i,X1 : $i] : (((c_iff @ (c_In @ X0 @ (c_Power @ X1)) @ (c_Subq @ X0 @ X1))) = $true)),
% 5.51/1.08 inference(rectify,[],[f220])).
% 5.51/1.08 thf(f339,plain,(
% 5.51/1.08 (c_Subq = (^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))))),
% 5.51/1.08 inference(cnf_transformation,[],[f263])).
% 5.51/1.08 thf(f348,plain,(
% 5.51/1.08 ($true = ((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 5.51/1.08 inference(cnf_transformation,[],[f240])).
% 5.51/1.08 thf(f373,plain,(
% 5.51/1.08 (c_and = (^[Y0 : $o]: ((^[Y1 : $o]: (!! @ $o @ (^[Y2 : $o]: ((Y0 => (Y1 => Y2)) => Y2)))))))),
% 5.51/1.08 inference(cnf_transformation,[],[f291])).
% 5.51/1.08 thf(f376,plain,(
% 5.51/1.08 ( ! [X0 : $i,X1 : $i] : ((((c_iff @ (c_In @ X0 @ (c_Power @ X1)) @ (c_Subq @ X0 @ X1))) = $true)) )),
% 5.51/1.08 inference(cnf_transformation,[],[f329])).
% 5.51/1.08 thf(f391,plain,(
% 5.51/1.08 (c_iff = (^[Y0 : $o]: ((^[Y1 : $o]: (c_and @ (Y0 => Y1) @ (Y1 => Y0))))))),
% 5.51/1.08 inference(cnf_transformation,[],[f257])).
% 5.51/1.08 thf(f404,plain,(
% 5.51/1.08 (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 5.51/1.08 inference(cnf_transformation,[],[f238])).
% 5.51/1.08 thf(f409,plain,(
% 5.51/1.08 ($true != ((c_not @ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $i) @ (^[Y2 : $i > $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ ($i > $i > $i) @ (^[Y4 : $i > $i > $i]: ((Y2 @ (Y2 @ Y3)) = (Y2 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ Y3 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ Y1 @ Y3))) @ Y1)) @ Y3) @ (Y4 @ (Y2 @ Y0) @ Y3)) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y2 @ (Y4 @ Y3 @ Y1))) @ (Y4 @ Y0 @ Y0)) @ (Y4 @ Y0 @ (Y4 @ Y3 @ Y1))) @ Y1))) @ Y3))) @ Y1)) @ Y0) @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ (Y2 @ Y1) @ (Y4 @ (Y4 @ Y0 @ Y0) @ Y0)) @ Y1)))) @ (Y2 @ (Y2 @ Y0))) @ Y1))))))))))))))))),
% 5.51/1.08 inference(cnf_transformation,[],[f308])).
% 5.51/1.08 thf(f463,plain,(
% 5.51/1.08 (c_iff = (^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: ((^[Y3 : $o]: (!! @ $o @ (^[Y4 : $o]: ((Y2 => (Y3 => Y4)) => Y4)))))) @ (Y0 => Y1) @ (Y1 => Y0))))))),
% 5.51/1.08 inference(definition_unfolding,[],[f391,f373])).
% 5.51/1.08 thf(f548,plain,(
% 5.51/1.08 ($true = (((^[Y0 : $o]: (Y0 => c_False)) @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 5.51/1.08 inference(definition_unfolding,[],[f348,f404])).
% 5.51/1.08 thf(f549,plain,(
% 5.51/1.08 ( ! [X0 : $i,X1 : $i] : (((((^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: ((^[Y3 : $o]: (!! @ $o @ (^[Y4 : $o]: ((Y2 => (Y3 => Y4)) => Y4)))))) @ (Y0 => Y1) @ (Y1 => Y0))))) @ (c_In @ X0 @ (c_Power @ X1)) @ ((^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))) @ X0 @ X1))) = $true)) )),
% 5.51/1.08 inference(definition_unfolding,[],[f376,f463,f339])).
% 5.51/1.08 thf(f551,plain,(
% 5.51/1.08 ($true != (((^[Y0 : $o]: (Y0 => c_False)) @ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $i) @ (^[Y2 : $i > $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ ($i > $i > $i) @ (^[Y4 : $i > $i > $i]: ((Y2 @ (Y2 @ Y3)) = (Y2 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ Y3 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ Y1 @ Y3))) @ Y1)) @ Y3) @ (Y4 @ (Y2 @ Y0) @ Y3)) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y2 @ (Y4 @ Y3 @ Y1))) @ (Y4 @ Y0 @ Y0)) @ (Y4 @ Y0 @ (Y4 @ Y3 @ Y1))) @ Y1))) @ Y3))) @ Y1)) @ Y0) @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ (Y2 @ Y1) @ (Y4 @ (Y4 @ Y0 @ Y0) @ Y0)) @ Y1)))) @ (Y2 @ (Y2 @ Y0))) @ Y1))))))))))))))))),
% 5.51/1.08 inference(definition_unfolding,[],[f409,f404])).
% 5.51/1.08 thf(f608,plain,(
% 5.51/1.08 ($true = (((?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))) => c_False)))),
% 5.51/1.08 inference(beta-eta_normalization,[],[f548])).
% 5.51/1.08 thf(f609,plain,(
% 5.51/1.08 (c_False = $true) | ($false = ((?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty)))))),
% 5.51/1.08 inference(imp_proxy_clausification,[],[f608])).
% 5.51/1.08 thf(f610,plain,(
% 5.51/1.08 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (c_In @ Y0 @ c_Empty)) @ X1))) | (c_False = $true)) )),
% 5.51/1.08 inference(pi_proxy_clausification,[],[f609])).
% 5.51/1.08 thf(f611,plain,(
% 5.51/1.08 ( ! [X1 : $i] : (($false = ((c_In @ X1 @ c_Empty))) | (c_False = $true)) )),
% 5.51/1.08 inference(beta-eta_normalization,[],[f610])).
% 5.51/1.08 thf(f612,plain,(
% 5.51/1.08 ($true != (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $i) @ (^[Y2 : $i > $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ ($i > $i > $i) @ (^[Y4 : $i > $i > $i]: ((Y2 @ (Y2 @ Y3)) = (Y2 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ Y3 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ Y1 @ Y3))) @ Y1)) @ Y3) @ (Y4 @ (Y2 @ Y0) @ Y3)) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y2 @ (Y4 @ Y3 @ Y1))) @ (Y4 @ Y0 @ Y0)) @ (Y4 @ Y0 @ (Y4 @ Y3 @ Y1))) @ Y1))) @ Y3))) @ Y1)) @ Y0) @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ (Y2 @ Y1) @ (Y4 @ (Y4 @ Y0 @ Y0) @ Y0)) @ Y1)))) @ (Y2 @ (Y2 @ Y0))) @ Y1))))))))))))) => c_False)))),
% 5.51/1.08 inference(beta-eta_normalization,[],[f551])).
% 5.51/1.08 thf(f613,plain,(
% 5.51/1.08 (c_False = $false)),
% 5.51/1.08 inference(imp_proxy_clausification,[],[f612])).
% 5.51/1.08 thf(f614,plain,(
% 5.51/1.08 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $i) @ (^[Y2 : $i > $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ ($i > $i > $i) @ (^[Y4 : $i > $i > $i]: ((Y2 @ (Y2 @ Y3)) = (Y2 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ Y3 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ Y1 @ Y3))) @ Y1)) @ Y3) @ (Y4 @ (Y2 @ Y0) @ Y3)) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y2 @ (Y4 @ Y3 @ Y1))) @ (Y4 @ Y0 @ Y0)) @ (Y4 @ Y0 @ (Y4 @ Y3 @ Y1))) @ Y1))) @ Y3))) @ Y1)) @ Y0) @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ (Y2 @ Y1) @ (Y4 @ (Y4 @ Y0 @ Y0) @ Y0)) @ Y1)))) @ (Y2 @ (Y2 @ Y0))) @ Y1)))))))))))))) = $true)),
% 5.51/1.08 inference(imp_proxy_clausification,[],[f612])).
% 5.51/1.08 thf(f615,plain,(
% 5.51/1.08 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $i) @ (^[Y2 : $i > $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ ($i > $i > $i) @ (^[Y4 : $i > $i > $i]: ((Y2 @ (Y2 @ Y3)) = (Y2 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ Y0 @ Y1) @ (Y4 @ Y3 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ Y1) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ Y1 @ Y3))) @ Y1)) @ Y3) @ (Y4 @ (Y2 @ Y0) @ Y3)) @ (Y4 @ (Y4 @ (Y4 @ (Y4 @ Y1 @ (Y2 @ (Y4 @ Y3 @ Y1))) @ (Y4 @ Y0 @ Y0)) @ (Y4 @ Y0 @ (Y4 @ Y3 @ Y1))) @ Y1))) @ Y3))) @ Y1)) @ Y0) @ (Y4 @ Y0 @ (Y4 @ Y1 @ (Y4 @ (Y4 @ (Y2 @ Y1) @ (Y4 @ (Y4 @ Y0 @ Y0) @ Y0)) @ Y1)))) @ (Y2 @ (Y2 @ Y0))) @ Y1)))))))))))) @ X1)))) )),
% 5.51/1.08 inference(pi_proxy_clausification,[],[f614])).
% 5.51/1.08 thf(f616,plain,(
% 5.51/1.08 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $i) @ (^[Y1 : $i > $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i > $i) @ (^[Y3 : $i > $i > $i]: ((Y1 @ (Y1 @ Y2)) = (Y1 @ (Y3 @ (Y3 @ (Y3 @ (Y3 @ (Y3 @ (Y3 @ X1 @ Y0) @ (Y3 @ (Y3 @ (Y3 @ X1 @ Y0) @ (Y3 @ Y2 @ (Y3 @ (Y3 @ (Y3 @ Y0 @ Y0) @ (Y3 @ (Y3 @ (Y3 @ (Y3 @ Y0 @ (Y3 @ (Y3 @ X1 @ (Y3 @ Y0 @ (Y3 @ Y0 @ Y2))) @ Y0)) @ Y2) @ (Y3 @ (Y1 @ X1) @ Y2)) @ (Y3 @ (Y3 @ (Y3 @ (Y3 @ Y0 @ (Y1 @ (Y3 @ Y2 @ Y0))) @ (Y3 @ X1 @ X1)) @ (Y3 @ X1 @ (Y3 @ Y2 @ Y0))) @ Y0))) @ Y2))) @ Y0)) @ X1) @ (Y3 @ X1 @ (Y3 @ Y0 @ (Y3 @ (Y3 @ (Y1 @ Y0) @ (Y3 @ (Y3 @ X1 @ X1) @ X1)) @ Y0)))) @ (Y1 @ (Y1 @ X1))) @ Y0)))))))))))))) )),
% 5.51/1.08 inference(beta-eta_normalization,[],[f615])).
% 5.51/1.08 thf(f617,plain,(
% 5.51/1.08 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ ($i > $i) @ (^[Y1 : $i > $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i > $i) @ (^[Y3 : $i > $i > $i]: ((Y1 @ (Y1 @ Y2)) = (Y1 @ (Y3 @ (Y3 @ (Y3 @ (Y3 @ (Y3 @ (Y3 @ X1 @ Y0) @ (Y3 @ (Y3 @ (Y3 @ X1 @ Y0) @ (Y3 @ Y2 @ (Y3 @ (Y3 @ (Y3 @ Y0 @ Y0) @ (Y3 @ (Y3 @ (Y3 @ (Y3 @ Y0 @ (Y3 @ (Y3 @ X1 @ (Y3 @ Y0 @ (Y3 @ Y0 @ Y2))) @ Y0)) @ Y2) @ (Y3 @ (Y1 @ X1) @ Y2)) @ (Y3 @ (Y3 @ (Y3 @ (Y3 @ Y0 @ (Y1 @ (Y3 @ Y2 @ Y0))) @ (Y3 @ X1 @ X1)) @ (Y3 @ X1 @ (Y3 @ Y2 @ Y0))) @ Y0))) @ Y2))) @ Y0)) @ X1) @ (Y3 @ X1 @ (Y3 @ Y0 @ (Y3 @ (Y3 @ (Y1 @ Y0) @ (Y3 @ (Y3 @ X1 @ X1) @ X1)) @ Y0)))) @ (Y1 @ (Y1 @ X1))) @ Y0)))))))))) @ X2)))) )),
% 5.51/1.08 inference(pi_proxy_clausification,[],[f616])).
% 5.51/1.08 thf(f618,plain,(
% 5.51/1.08 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ ($i > $i) @ (^[Y0 : $i > $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $i > $i) @ (^[Y2 : $i > $i > $i]: ((Y0 @ (Y0 @ Y1)) = (Y0 @ (Y2 @ (Y2 @ (Y2 @ (Y2 @ (Y2 @ (Y2 @ X1 @ X2) @ (Y2 @ (Y2 @ (Y2 @ X1 @ X2) @ (Y2 @ Y1 @ (Y2 @ (Y2 @ (Y2 @ X2 @ X2) @ (Y2 @ (Y2 @ (Y2 @ (Y2 @ X2 @ (Y2 @ (Y2 @ X1 @ (Y2 @ X2 @ (Y2 @ X2 @ Y1))) @ X2)) @ Y1) @ (Y2 @ (Y0 @ X1) @ Y1)) @ (Y2 @ (Y2 @ (Y2 @ (Y2 @ X2 @ (Y0 @ (Y2 @ Y1 @ X2))) @ (Y2 @ X1 @ X1)) @ (Y2 @ X1 @ (Y2 @ Y1 @ X2))) @ X2))) @ Y1))) @ X2)) @ X1) @ (Y2 @ X1 @ (Y2 @ X2 @ (Y2 @ (Y2 @ (Y0 @ X2) @ (Y2 @ (Y2 @ X1 @ X1) @ X1)) @ X2)))) @ (Y0 @ (Y0 @ X1))) @ X2)))))))))))) )),
% 5.51/1.08 inference(beta-eta_normalization,[],[f617])).
% 5.51/1.08 thf(f619,plain,(
% 5.51/1.08 ( ! [X2 : $i,X3 : ($i > $i),X1 : $i] : (($true = (((^[Y0 : $i > $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $i > $i) @ (^[Y2 : $i > $i > $i]: ((Y0 @ (Y0 @ Y1)) = (Y0 @ (Y2 @ (Y2 @ (Y2 @ (Y2 @ (Y2 @ (Y2 @ X1 @ X2) @ (Y2 @ (Y2 @ (Y2 @ X1 @ X2) @ (Y2 @ Y1 @ (Y2 @ (Y2 @ (Y2 @ X2 @ X2) @ (Y2 @ (Y2 @ (Y2 @ (Y2 @ X2 @ (Y2 @ (Y2 @ X1 @ (Y2 @ X2 @ (Y2 @ X2 @ Y1))) @ X2)) @ Y1) @ (Y2 @ (Y0 @ X1) @ Y1)) @ (Y2 @ (Y2 @ (Y2 @ (Y2 @ X2 @ (Y0 @ (Y2 @ Y1 @ X2))) @ (Y2 @ X1 @ X1)) @ (Y2 @ X1 @ (Y2 @ Y1 @ X2))) @ X2))) @ Y1))) @ X2)) @ X1) @ (Y2 @ X1 @ (Y2 @ X2 @ (Y2 @ (Y2 @ (Y0 @ X2) @ (Y2 @ (Y2 @ X1 @ X1) @ X1)) @ X2)))) @ (Y0 @ (Y0 @ X1))) @ X2)))))))) @ X3)))) )),
% 5.51/1.08 inference(pi_proxy_clausification,[],[f618])).
% 5.51/1.08 thf(f620,plain,(
% 5.51/1.08 ( ! [X2 : $i,X3 : ($i > $i),X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $i > $i) @ (^[Y1 : $i > $i > $i]: ((X3 @ (X3 @ Y0)) = (X3 @ (Y1 @ (Y1 @ (Y1 @ (Y1 @ (Y1 @ (Y1 @ X1 @ X2) @ (Y1 @ (Y1 @ (Y1 @ X1 @ X2) @ (Y1 @ Y0 @ (Y1 @ (Y1 @ (Y1 @ X2 @ X2) @ (Y1 @ (Y1 @ (Y1 @ (Y1 @ X2 @ (Y1 @ (Y1 @ X1 @ (Y1 @ X2 @ (Y1 @ X2 @ Y0))) @ X2)) @ Y0) @ (Y1 @ (X3 @ X1) @ Y0)) @ (Y1 @ (Y1 @ (Y1 @ (Y1 @ X2 @ (X3 @ (Y1 @ Y0 @ X2))) @ (Y1 @ X1 @ X1)) @ (Y1 @ X1 @ (Y1 @ Y0 @ X2))) @ X2))) @ Y0))) @ X2)) @ X1) @ (Y1 @ X1 @ (Y1 @ X2 @ (Y1 @ (Y1 @ (X3 @ X2) @ (Y1 @ (Y1 @ X1 @ X1) @ X1)) @ X2)))) @ (X3 @ (X3 @ X1))) @ X2)))))))) = $true)) )),
% 5.51/1.08 inference(beta-eta_normalization,[],[f619])).
% 5.51/1.08 thf(f621,plain,(
% 5.51/1.08 ( ! [X2 : $i,X3 : ($i > $i),X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ ($i > $i > $i) @ (^[Y1 : $i > $i > $i]: ((X3 @ (X3 @ Y0)) = (X3 @ (Y1 @ (Y1 @ (Y1 @ (Y1 @ (Y1 @ (Y1 @ X1 @ X2) @ (Y1 @ (Y1 @ (Y1 @ X1 @ X2) @ (Y1 @ Y0 @ (Y1 @ (Y1 @ (Y1 @ X2 @ X2) @ (Y1 @ (Y1 @ (Y1 @ (Y1 @ X2 @ (Y1 @ (Y1 @ X1 @ (Y1 @ X2 @ (Y1 @ X2 @ Y0))) @ X2)) @ Y0) @ (Y1 @ (X3 @ X1) @ Y0)) @ (Y1 @ (Y1 @ (Y1 @ (Y1 @ X2 @ (X3 @ (Y1 @ Y0 @ X2))) @ (Y1 @ X1 @ X1)) @ (Y1 @ X1 @ (Y1 @ Y0 @ X2))) @ X2))) @ Y0))) @ X2)) @ X1) @ (Y1 @ X1 @ (Y1 @ X2 @ (Y1 @ (Y1 @ (X3 @ X2) @ (Y1 @ (Y1 @ X1 @ X1) @ X1)) @ X2)))) @ (X3 @ (X3 @ X1))) @ X2)))))) @ X4)))) )),
% 5.51/1.08 inference(pi_proxy_clausification,[],[f620])).
% 5.51/1.08 thf(f622,plain,(
% 5.51/1.08 ( ! [X2 : $i,X3 : ($i > $i),X1 : $i,X4 : $i] : ((((!! @ ($i > $i > $i) @ (^[Y0 : $i > $i > $i]: ((X3 @ (X3 @ X4)) = (X3 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ X1 @ X2) @ (Y0 @ (Y0 @ (Y0 @ X1 @ X2) @ (Y0 @ X4 @ (Y0 @ (Y0 @ (Y0 @ X2 @ X2) @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ X2 @ (Y0 @ (Y0 @ X1 @ (Y0 @ X2 @ (Y0 @ X2 @ X4))) @ X2)) @ X4) @ (Y0 @ (X3 @ X1) @ X4)) @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ X2 @ (X3 @ (Y0 @ X4 @ X2))) @ (Y0 @ X1 @ X1)) @ (Y0 @ X1 @ (Y0 @ X4 @ X2))) @ X2))) @ X4))) @ X2)) @ X1) @ (Y0 @ X1 @ (Y0 @ X2 @ (Y0 @ (Y0 @ (X3 @ X2) @ (Y0 @ (Y0 @ X1 @ X1) @ X1)) @ X2)))) @ (X3 @ (X3 @ X1))) @ X2)))))) = $true)) )),
% 5.51/1.08 inference(beta-eta_normalization,[],[f621])).
% 5.51/1.08 thf(f623,plain,(
% 5.51/1.08 ( ! [X2 : $i,X3 : ($i > $i),X1 : $i,X4 : $i,X5 : ($i > $i > $i)] : (((((^[Y0 : $i > $i > $i]: ((X3 @ (X3 @ X4)) = (X3 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ X1 @ X2) @ (Y0 @ (Y0 @ (Y0 @ X1 @ X2) @ (Y0 @ X4 @ (Y0 @ (Y0 @ (Y0 @ X2 @ X2) @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ X2 @ (Y0 @ (Y0 @ X1 @ (Y0 @ X2 @ (Y0 @ X2 @ X4))) @ X2)) @ X4) @ (Y0 @ (X3 @ X1) @ X4)) @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ X2 @ (X3 @ (Y0 @ X4 @ X2))) @ (Y0 @ X1 @ X1)) @ (Y0 @ X1 @ (Y0 @ X4 @ X2))) @ X2))) @ X4))) @ X2)) @ X1) @ (Y0 @ X1 @ (Y0 @ X2 @ (Y0 @ (Y0 @ (X3 @ X2) @ (Y0 @ (Y0 @ X1 @ X1) @ X1)) @ X2)))) @ (X3 @ (X3 @ X1))) @ X2)))) @ X5)) = $true)) )),
% 5.51/1.08 inference(pi_proxy_clausification,[],[f622])).
% 5.51/1.08 thf(f624,plain,(
% 5.51/1.08 ( ! [X2 : $i,X3 : ($i > $i),X1 : $i,X4 : $i,X5 : ($i > $i > $i)] : (($true = (((X3 @ (X3 @ X4)) = (X3 @ (X5 @ (X5 @ (X5 @ (X5 @ (X5 @ (X5 @ X1 @ X2) @ (X5 @ (X5 @ (X5 @ X1 @ X2) @ (X5 @ X4 @ (X5 @ (X5 @ (X5 @ X2 @ X2) @ (X5 @ (X5 @ (X5 @ (X5 @ X2 @ (X5 @ (X5 @ X1 @ (X5 @ X2 @ (X5 @ X2 @ X4))) @ X2)) @ X4) @ (X5 @ (X3 @ X1) @ X4)) @ (X5 @ (X5 @ (X5 @ (X5 @ X2 @ (X3 @ (X5 @ X4 @ X2))) @ (X5 @ X1 @ X1)) @ (X5 @ X1 @ (X5 @ X4 @ X2))) @ X2))) @ X4))) @ X2)) @ X1) @ (X5 @ X1 @ (X5 @ X2 @ (X5 @ (X5 @ (X3 @ X2) @ (X5 @ (X5 @ X1 @ X1) @ X1)) @ X2)))) @ (X3 @ (X3 @ X1))) @ X2)))))) )),
% 5.51/1.08 inference(beta-eta_normalization,[],[f623])).
% 5.51/1.08 thf(f625,plain,(
% 5.51/1.08 ( ! [X2 : $i,X3 : ($i > $i),X1 : $i,X4 : $i,X5 : ($i > $i > $i)] : ((((X3 @ (X5 @ (X5 @ (X5 @ (X5 @ (X5 @ (X5 @ X1 @ X2) @ (X5 @ (X5 @ (X5 @ X1 @ X2) @ (X5 @ X4 @ (X5 @ (X5 @ (X5 @ X2 @ X2) @ (X5 @ (X5 @ (X5 @ (X5 @ X2 @ (X5 @ (X5 @ X1 @ (X5 @ X2 @ (X5 @ X2 @ X4))) @ X2)) @ X4) @ (X5 @ (X3 @ X1) @ X4)) @ (X5 @ (X5 @ (X5 @ (X5 @ X2 @ (X3 @ (X5 @ X4 @ X2))) @ (X5 @ X1 @ X1)) @ (X5 @ X1 @ (X5 @ X4 @ X2))) @ X2))) @ X4))) @ X2)) @ X1) @ (X5 @ X1 @ (X5 @ X2 @ (X5 @ (X5 @ (X3 @ X2) @ (X5 @ (X5 @ X1 @ X1) @ X1)) @ X2)))) @ (X3 @ (X3 @ X1))) @ X2))) = ((X3 @ (X3 @ X4))))) )),
% 5.51/1.08 inference(equality_proxy_clausification,[],[f624])).
% 5.51/1.08 thf(f626,plain,(
% 5.51/1.08 ( ! [X0 : $i,X1 : $i] : (($true = ((!! @ $o @ (^[Y0 : $o]: ((((c_In @ X0 @ (c_Power @ X1)) => (!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X0) => (c_In @ Y1 @ X1))))) => (((!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X0) => (c_In @ Y1 @ X1)))) => (c_In @ X0 @ (c_Power @ X1))) => Y0)) => Y0)))))) )),
% 5.51/1.08 inference(beta-eta_normalization,[],[f549])).
% 5.51/1.08 thf(f627,plain,(
% 5.51/1.08 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = (((^[Y0 : $o]: ((((c_In @ X0 @ (c_Power @ X1)) => (!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X0) => (c_In @ Y1 @ X1))))) => (((!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X0) => (c_In @ Y1 @ X1)))) => (c_In @ X0 @ (c_Power @ X1))) => Y0)) => Y0)) @ X2)))) )),
% 5.51/1.08 inference(pi_proxy_clausification,[],[f626])).
% 5.51/1.08 thf(f628,plain,(
% 5.51/1.08 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = (((((c_In @ X0 @ (c_Power @ X1)) => (!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X0) => (c_In @ Y0 @ X1))))) => (((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X0) => (c_In @ Y0 @ X1)))) => (c_In @ X0 @ (c_Power @ X1))) => X2)) => X2)))) )),
% 5.51/1.08 inference(beta-eta_normalization,[],[f627])).
% 5.51/1.08 thf(f629,plain,(
% 5.51/1.08 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = ((((c_In @ X0 @ (c_Power @ X1)) => (!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X0) => (c_In @ Y0 @ X1))))) => (((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X0) => (c_In @ Y0 @ X1)))) => (c_In @ X0 @ (c_Power @ X1))) => X2)))) | ($true = X2)) )),
% 5.51/1.08 inference(imp_proxy_clausification,[],[f628])).
% 5.51/1.08 thf(f630,plain,(
% 5.51/1.08 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = ((((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X0) => (c_In @ Y0 @ X1)))) => (c_In @ X0 @ (c_Power @ X1))) => X2))) | ($true = X2)) )),
% 5.51/1.08 inference(imp_proxy_clausification,[],[f629])).
% 5.51/1.08 thf(f637,plain,(
% 5.51/1.08 ( ! [X2 : $o,X0 : $i,X1 : $i] : (((((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X0) => (c_In @ Y0 @ X1)))) => (c_In @ X0 @ (c_Power @ X1)))) = $true) | ($true = X2)) )),
% 5.51/1.08 inference(imp_proxy_clausification,[],[f630])).
% 5.51/1.08 thf(f638,plain,(
% 5.51/1.08 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X0) => (c_In @ Y0 @ X1)))))) | ($true = ((c_In @ X0 @ (c_Power @ X1)))) | ($true = X2)) )),
% 5.51/1.08 inference(imp_proxy_clausification,[],[f637])).
% 5.51/1.08 thf(f639,plain,(
% 5.51/1.08 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = ((c_In @ X0 @ (c_Power @ X1)))) | ($false = (((^[Y0 : $i]: ((c_In @ Y0 @ X0) => (c_In @ Y0 @ X1))) @ (sK15 @ X1 @ X0)))) | ($true = X2)) )),
% 5.51/1.08 inference(sigma_proxy_clausification,[],[f638])).
% 5.51/1.08 thf(f640,plain,(
% 5.51/1.08 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = X2) | ($false = (((c_In @ (sK15 @ X1 @ X0) @ X0) => (c_In @ (sK15 @ X1 @ X0) @ X1)))) | ($true = ((c_In @ X0 @ (c_Power @ X1))))) )),
% 5.51/1.08 inference(beta-eta_normalization,[],[f639])).
% 5.51/1.08 thf(f642,plain,(
% 5.51/1.08 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = ((c_In @ (sK15 @ X1 @ X0) @ X0))) | ($true = X2) | ($true = ((c_In @ X0 @ (c_Power @ X1))))) )),
% 5.51/1.08 inference(imp_proxy_clausification,[],[f640])).
% 5.51/1.08 thf(f708,definition,(
% 5.51/1.08 spl20_3 <=> (c_False = $false)),
% 5.51/1.08 introduced(definition,[new_symbols(definition,[spl20_3])],[avatar_definition])).
% 5.51/1.08 thf(f709,plain,(
% 5.51/1.08 (c_False = $false) | ~spl20_3),
% 5.51/1.08 inference(avatar_component_clause,[],[f708])).
% 5.51/1.08 thf(f711,definition,(
% 5.51/1.08 spl20_4 <=> ! [X0 : $o] : ($true = X0)),
% 5.51/1.08 introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition])).
% 5.51/1.08 thf(f712,plain,(
% 5.51/1.08 ( ! [X0 : $o] : (($true = X0)) ) | ~spl20_4),
% 5.51/1.08 inference(avatar_component_clause,[],[f711])).
% 5.51/1.08 thf(f715,definition,(
% 5.51/1.08 spl20_5 <=> ! [X1 : $i] : ($false = ((c_In @ X1 @ c_Empty)))),
% 5.51/1.08 introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition])).
% 5.51/1.08 thf(f716,plain,(
% 5.51/1.08 ( ! [X1 : $i] : (($false = ((c_In @ X1 @ c_Empty)))) ) | ~spl20_5),
% 5.51/1.08 inference(avatar_component_clause,[],[f715])).
% 5.51/1.08 thf(f718,definition,(
% 5.51/1.08 spl20_6 <=> (c_False = $true)),
% 5.51/1.08 introduced(definition,[new_symbols(definition,[spl20_6])],[avatar_definition])).
% 5.51/1.08 thf(f719,plain,(
% 5.51/1.08 (c_False = $true) | ~spl20_6),
% 5.51/1.08 inference(avatar_component_clause,[],[f718])).
% 5.51/1.08 thf(f720,plain,(
% 5.51/1.08 spl20_5 | spl20_6),
% 5.51/1.08 inference(avatar_split_clause,[],[f611,f718,f715])).
% 5.51/1.08 thf(f721,plain,(
% 5.51/1.08 spl20_3),
% 5.51/1.08 inference(avatar_split_clause,[],[f613,f708])).
% 5.51/1.08 thf(f727,definition,(
% 5.51/1.08 spl20_8 <=> ! [X0 : $i,X1 : $i] : (($true = ((c_In @ (sK15 @ X1 @ X0) @ X0))) | ($true = ((c_In @ X0 @ (c_Power @ X1)))))),
% 5.51/1.08 introduced(definition,[new_symbols(definition,[spl20_8])],[avatar_definition])).
% 5.51/1.08 thf(f728,plain,(
% 5.51/1.08 ( ! [X0 : $i,X1 : $i] : (($true = ((c_In @ (sK15 @ X1 @ X0) @ X0))) | ($true = ((c_In @ X0 @ (c_Power @ X1))))) ) | ~spl20_8),
% 5.51/1.08 inference(avatar_component_clause,[],[f727])).
% 5.51/1.08 thf(f729,plain,(
% 5.51/1.08 spl20_4 | spl20_8),
% 5.51/1.08 inference(avatar_split_clause,[],[f642,f727,f711])).
% 5.51/1.08 thf(f734,plain,(
% 5.51/1.08 (c_False != $true) | spl20_6),
% 5.51/1.08 inference(avatar_component_clause,[],[f718])).
% 5.51/1.08 thf(f774,plain,(
% 5.51/1.08 ($false = $true) | (~spl20_3 | ~spl20_6)),
% 5.51/1.08 inference(backward_demodulation,[],[f719,f709])).
% 5.51/1.08 thf(f775,plain,(
% 5.51/1.08 $false | (~spl20_3 | ~spl20_6)),
% 5.51/1.08 inference(trivial_inequality_removal,[],[f774])).
% 5.51/1.08 thf(f776,plain,(
% 5.51/1.08 ~spl20_3 | ~spl20_6),
% 5.51/1.08 inference(avatar_contradiction_clause,[],[f775])).
% 5.51/1.08 thf(f780,plain,(
% 5.51/1.08 $false | (~spl20_4 | spl20_6)),
% 5.51/1.08 inference(forward_subsumption_resolution,[],[f734,f712])).
% 5.51/1.08 thf(f781,plain,(
% 5.51/1.08 ~spl20_4 | spl20_6),
% 5.51/1.08 inference(avatar_contradiction_clause,[],[f780])).
% 5.51/1.08 thf(f887,plain,(
% 5.51/1.08 ( ! [X0 : $i,X1 : $i] : (($false = ((c_In @ X1 @ ((^[Y0 : $i]: (Y0)) @ ((^[Y0 : $i]: (Y0)) @ X0)))))) ) | ~spl20_5),
% 5.51/1.08 inference(constrained_superposition,[],[f716,f625])).
% 5.51/1.08 thf(f901,plain,(
% 5.51/1.08 ( ! [X0 : $i,X1 : $i] : ((((c_In @ X1 @ X0)) = $false)) ) | ~spl20_5),
% 5.51/1.08 inference(beta-eta_normalization,[],[f887])).
% 5.51/1.08 thf(f909,definition,(
% 5.51/1.08 spl20_19 <=> ! [X0 : $i,X1 : $i] : (((c_In @ X1 @ X0)) = $false)),
% 5.51/1.08 introduced(definition,[new_symbols(definition,[spl20_19])],[avatar_definition])).
% 5.51/1.08 thf(f910,plain,(
% 5.51/1.08 ( ! [X0 : $i,X1 : $i] : ((((c_In @ X1 @ X0)) = $false)) ) | ~spl20_19),
% 5.51/1.08 inference(avatar_component_clause,[],[f909])).
% 5.51/1.08 thf(f943,plain,(
% 5.51/1.08 spl20_19 | ~spl20_5),
% 5.51/1.08 inference(avatar_split_clause,[],[f901,f715,f909])).
% 5.51/1.08 thf(f968,plain,(
% 5.51/1.08 ( ! [X0 : $i,X1 : $i] : (($true = ((c_In @ X0 @ (c_Power @ X1)))) | ($false = $true)) ) | (~spl20_8 | ~spl20_19)),
% 5.51/1.08 inference(backward_demodulation,[],[f728,f910])).
% 5.51/1.08 thf(f986,plain,(
% 5.51/1.08 ( ! [X0 : $i,X1 : $i] : (($true = ((c_In @ X0 @ (c_Power @ X1))))) ) | (~spl20_8 | ~spl20_19)),
% 5.51/1.08 inference(trivial_inequality_removal,[],[f968])).
% 5.51/1.08 thf(f989,plain,(
% 5.51/1.08 ($false = $true) | (~spl20_8 | ~spl20_19)),
% 5.51/1.08 inference(forward_demodulation,[],[f986,f910])).
% 5.51/1.08 thf(f990,plain,(
% 5.51/1.08 $false | (~spl20_8 | ~spl20_19)),
% 5.51/1.08 inference(trivial_inequality_removal,[],[f989])).
% 5.51/1.08 thf(f991,plain,(
% 5.51/1.08 ~spl20_8 | ~spl20_19),
% 5.51/1.08 inference(avatar_contradiction_clause,[],[f990])).
% 5.51/1.08 cnf(s3, plain, spl20_5 | spl20_6, inference(sat_conversion,[],[f720])).
% 5.51/1.08 cnf(s4, plain, spl20_3, inference(sat_conversion,[],[f721])).
% 5.51/1.08 cnf(s6, plain, spl20_4 | spl20_8, inference(sat_conversion,[],[f729])).
% 5.51/1.08 cnf(s23, plain, ~spl20_3 | ~spl20_6, inference(sat_conversion,[],[f776])).
% 5.51/1.08 cnf(s25, plain, ~spl20_4 | spl20_6, inference(sat_conversion,[],[f781])).
% 5.51/1.08 cnf(s29, plain, ~spl20_5 | spl20_19, inference(sat_conversion,[],[f943])).
% 5.51/1.08 cnf(s32, plain, ~spl20_8 | ~spl20_19, inference(sat_conversion,[],[f991])).
% 5.51/1.08 cnf(s33, plain, ~spl20_6, inference(rat,[],[s23,s4])).
% 5.51/1.08 cnf(s34, plain, ~spl20_4, inference(rat,[],[s25,s33])).
% 5.51/1.08 cnf(s45, plain, spl20_8, inference(rat,[],[s6,s34])).
% 5.51/1.08 cnf(s47, plain, ~spl20_19, inference(rat,[],[s32,s45])).
% 5.51/1.08 cnf(s48, plain, ~spl20_5, inference(rat,[],[s29,s47])).
% 5.51/1.08 cnf(s49, plain, $false, inference(rat,[],[s3,s33,s48])).
% 5.51/1.08 thf(f994,plain,(
% 5.51/1.08 $false),
% 5.51/1.08 inference(avatar_sat_refutation,[],[s49])).
% 5.51/1.08 % SZS output end Proof for theBenchmark
% 5.51/1.08 % (906445)------------------------------
% 5.51/1.08 % (906445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.08 % (906445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.08 % (906445)CaDiCaL version: 2.1.3
% 5.51/1.08 % (906445)Termination reason: Refutation
% 5.51/1.08 % (906445)Time elapsed: 0.109 s
% 5.51/1.08 % (906445)Peak memory usage: 15 MB
% 5.51/1.08 % (906445)Instructions burned: 241 (million)
% 5.51/1.08 % (906303)Success in time 0.838 s
% 5.51/1.08 % Vampire exiting
%------------------------------------------------------------------------------