%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO858^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:29 AM UTC 2026
% Result : Theorem 2.69s 0.74s
% Output : Refutation 2.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO858^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n007.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 17:17:11 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running higher-order theorem proving
% 0.08/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.78/0.39 % (3673594)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.78/0.39 % (3673599)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1826342954:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.78/0.39 % (3673605)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.78/0.39 % (3673605)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.78/0.39 % (3673600)lrs+10_16_si=on:nwc=1.5:random_seed=3434098986:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.78/0.39 % (3673601)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4190516242:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.78/0.39 % (3673603)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=515260020:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.78/0.39 % (3673602)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=2373671965: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.78/0.39 % (3673604)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3321892377:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.78/0.39 % (3673605)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=771143898:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.78/0.39 % (3673601)Instruction limit reached!
% 0.78/0.39 % (3673601)------------------------------
% 0.78/0.39 % (3673601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.39 % (3673601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.39 % (3673601)CaDiCaL version: 2.1.3
% 0.78/0.39 % (3673601)Termination reason: Instruction limit
% 0.78/0.39 % (3673601)Termination phase: shuffling
% 0.78/0.39 % (3673601)Time elapsed: 0.002 s
% 0.78/0.39 % (3673601)Peak memory usage: 10 MB
% 0.78/0.39 % (3673601)Instructions burned: 5 (million)
% 0.78/0.39 % (3673600)Instruction limit reached!
% 0.78/0.39 % (3673600)------------------------------
% 0.78/0.39 % (3673600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.39 % (3673600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.39 % (3673600)CaDiCaL version: 2.1.3
% 0.78/0.39 % (3673600)Termination reason: Instruction limit
% 0.78/0.39 % (3673600)Termination phase: Property scanning
% 0.78/0.39 % (3673600)Time elapsed: 0.009 s
% 0.78/0.39 % (3673600)Peak memory usage: 10 MB
% 0.78/0.39 % (3673600)Instructions burned: 20 (million)
% 0.78/0.39 % (3673599)Instruction limit reached!
% 0.78/0.39 % (3673599)------------------------------
% 0.78/0.39 % (3673599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.39 % (3673599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.39 % (3673599)CaDiCaL version: 2.1.3
% 0.78/0.39 % (3673599)Termination reason: Instruction limit
% 0.78/0.39 % (3673599)Termination phase: Property scanning
% 0.78/0.39 % (3673599)Time elapsed: 0.019 s
% 0.78/0.39 % (3673599)Peak memory usage: 11 MB
% 0.78/0.39 % (3673599)Instructions burned: 88 (million)
% 0.78/0.39 % (3673603)Instruction limit reached!
% 0.78/0.39 % (3673603)------------------------------
% 0.78/0.39 % (3673603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.39 % (3673603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.39 % (3673603)CaDiCaL version: 2.1.3
% 0.78/0.39 % (3673603)Termination reason: Instruction limit
% 0.78/0.39 % (3673603)Termination phase: Property scanning
% 0.78/0.39 % (3673603)Time elapsed: 0.011 s
% 0.78/0.39 % (3673603)Peak memory usage: 10 MB
% 0.78/0.39 % (3673603)Instructions burned: 25 (million)
% 0.78/0.39 % (3673615)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.78/0.39 % (3673615)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4254254713:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.78/0.42 % (3673613)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1856501247:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.78/0.42 % (3673615)Instruction limit reached!
% 0.78/0.42 % (3673615)------------------------------
% 0.78/0.42 % (3673615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.42 % (3673615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.42 % (3673615)CaDiCaL version: 2.1.3
% 0.78/0.42 % (3673615)Termination reason: Instruction limit
% 0.78/0.42 % (3673615)Termination phase: shuffling
% 0.78/0.42 % (3673615)Time elapsed: 0.002 s
% 0.78/0.42 % (3673615)Peak memory usage: 10 MB
% 0.78/0.42 % (3673615)Instructions burned: 11 (million)
% 0.78/0.42 % (3673613)Instruction limit reached!
% 0.78/0.42 % (3673613)------------------------------
% 0.78/0.42 % (3673613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.42 % (3673613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.42 % (3673613)CaDiCaL version: 2.1.3
% 0.78/0.42 % (3673613)Termination reason: Instruction limit
% 0.78/0.42 % (3673613)Termination phase: shuffling
% 0.78/0.42 % (3673613)Time elapsed: 0.003 s
% 0.78/0.42 % (3673613)Peak memory usage: 10 MB
% 0.78/0.42 % (3673613)Instructions burned: 6 (million)
% 0.78/0.42 % (3673614)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2923581357:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.78/0.42 % (3673614)Instruction limit reached!
% 0.78/0.42 % (3673614)------------------------------
% 0.78/0.42 % (3673614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.42 % (3673614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.42 % (3673614)CaDiCaL version: 2.1.3
% 0.78/0.42 % (3673614)Termination reason: Instruction limit
% 0.78/0.42 % (3673614)Termination phase: shuffling
% 0.78/0.42 % (3673614)Time elapsed: 0.003 s
% 0.78/0.42 % (3673614)Peak memory usage: 10 MB
% 0.78/0.42 % (3673614)Instructions burned: 6 (million)
% 0.78/0.42 % (3673604)Instruction limit reached!
% 0.78/0.42 % (3673604)------------------------------
% 0.78/0.42 % (3673604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.42 % (3673604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.42 % (3673604)CaDiCaL version: 2.1.3
% 0.78/0.42 % (3673604)Termination reason: Instruction limit
% 0.78/0.42 % (3673604)Termination phase: Function definition elimination
% 0.78/0.42 % (3673604)Time elapsed: 0.032 s
% 0.78/0.42 % (3673604)Peak memory usage: 11 MB
% 0.78/0.42 % (3673604)Instructions burned: 76 (million)
% 0.78/0.42 % (3673619)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.78/0.42 % (3673619)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.78/0.42 % (3673619)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1027687435: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.78/0.42 % (3673616)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2177400879:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.78/0.42 % (3673619)Instruction limit reached!
% 0.78/0.42 % (3673619)------------------------------
% 0.78/0.42 % (3673619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.42 % (3673619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.42 % (3673619)CaDiCaL version: 2.1.3
% 0.78/0.42 % (3673619)Termination reason: Instruction limit
% 0.78/0.42 % (3673619)Termination phase: Property scanning
% 0.78/0.42 % (3673619)Time elapsed: 0.007 s
% 0.78/0.42 % (3673619)Peak memory usage: 10 MB
% 0.78/0.42 % (3673619)Instructions burned: 30 (million)
% 0.78/0.42 % (3673620)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=881121587:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.78/0.42 % (3673623)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.78/0.46 % (3673616)Instruction limit reached!
% 0.78/0.46 % (3673616)------------------------------
% 0.78/0.46 % (3673616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (3673616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (3673616)CaDiCaL version: 2.1.3
% 0.78/0.46 % (3673616)Termination reason: Instruction limit
% 0.78/0.46 % (3673616)Termination phase: shuffling
% 0.78/0.46 % (3673616)Time elapsed: 0.012 s
% 0.78/0.46 % (3673616)Peak memory usage: 10 MB
% 0.78/0.46 % (3673616)Instructions burned: 13 (million)
% 0.78/0.46 % (3673622)lrs+10_1_si=on:cs=on:random_seed=840199740:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.78/0.46 % (3673623)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=1869699630:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.78/0.46 % (3673626)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2326709620:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.78/0.46 % (3673623)Instruction limit reached!
% 0.78/0.46 % (3673623)------------------------------
% 0.78/0.46 % (3673623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (3673623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (3673623)CaDiCaL version: 2.1.3
% 0.78/0.46 % (3673623)Termination reason: Instruction limit
% 0.78/0.46 % (3673623)Termination phase: shuffling
% 0.78/0.46 % (3673623)Time elapsed: 0.002 s
% 0.78/0.46 % (3673623)Peak memory usage: 10 MB
% 0.78/0.46 % (3673623)Instructions burned: 3 (million)
% 0.78/0.46 % (3673622)Instruction limit reached!
% 0.78/0.46 % (3673622)------------------------------
% 0.78/0.46 % (3673622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (3673622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (3673622)CaDiCaL version: 2.1.3
% 0.78/0.46 % (3673622)Termination reason: Instruction limit
% 0.78/0.46 % (3673622)Termination phase: shuffling
% 0.78/0.46 % (3673622)Time elapsed: 0.004 s
% 0.78/0.46 % (3673622)Peak memory usage: 10 MB
% 0.78/0.46 % (3673622)Instructions burned: 9 (million)
% 0.78/0.46 % (3673626)Instruction limit reached!
% 0.78/0.46 % (3673626)------------------------------
% 0.78/0.46 % (3673626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (3673626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (3673626)CaDiCaL version: 2.1.3
% 0.78/0.46 % (3673626)Termination reason: Instruction limit
% 0.78/0.46 % (3673626)Termination phase: Saturation
% 0.78/0.46 % (3673626)Time elapsed: 0.009 s
% 0.78/0.46 % (3673626)Peak memory usage: 12 MB
% 0.78/0.46 % (3673626)Instructions burned: 39 (million)
% 0.78/0.46 % (3673605)Instruction limit reached!
% 0.78/0.46 % (3673605)------------------------------
% 0.78/0.46 % (3673605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (3673605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (3673605)CaDiCaL version: 2.1.3
% 0.78/0.46 % (3673605)Termination reason: Instruction limit
% 0.78/0.46 % (3673605)Termination phase: Saturation
% 0.78/0.46 % (3673605)Time elapsed: 0.065 s
% 0.78/0.46 % (3673605)Peak memory usage: 13 MB
% 0.78/0.46 % (3673605)Instructions burned: 157 (million)
% 0.78/0.46 % (3673634)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=4185893534:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.78/0.46 % (3673632)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1650937812:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.78/0.46 % (3673633)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1377169097:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.78/0.46 % (3673620)Instruction limit reached!
% 0.78/0.46 % (3673620)------------------------------
% 0.78/0.46 % (3673620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (3673620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (3673620)CaDiCaL version: 2.1.3
% 0.78/0.46 % (3673620)Termination reason: Instruction limit
% 0.78/0.46 % (3673620)Termination phase: Property scanning
% 0.78/0.51 % (3673620)Time elapsed: 0.035 s
% 0.78/0.51 % (3673620)Peak memory usage: 11 MB
% 0.78/0.51 % (3673620)Instructions burned: 88 (million)
% 0.78/0.51 % (3673633)Instruction limit reached!
% 0.78/0.51 % (3673633)------------------------------
% 0.78/0.51 % (3673633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.51 % (3673633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.51 % (3673633)CaDiCaL version: 2.1.3
% 0.78/0.51 % (3673633)Termination reason: Instruction limit
% 0.78/0.51 % (3673633)Termination phase: shuffling
% 0.78/0.51 % (3673633)Time elapsed: 0.007 s
% 0.78/0.51 % (3673633)Peak memory usage: 10 MB
% 0.78/0.51 % (3673633)Instructions burned: 14 (million)
% 0.78/0.51 % (3673628)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2606035050:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.78/0.51 % (3673635)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3849652880:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.78/0.51 % (3673632)Instruction limit reached!
% 0.78/0.51 % (3673632)------------------------------
% 0.78/0.51 % (3673632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.51 % (3673632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.51 % (3673632)CaDiCaL version: 2.1.3
% 0.78/0.51 % (3673632)Termination reason: Instruction limit
% 0.78/0.51 % (3673632)Termination phase: Property scanning
% 0.78/0.51 % (3673632)Time elapsed: 0.011 s
% 0.78/0.51 % (3673632)Peak memory usage: 10 MB
% 0.78/0.51 % (3673632)Instructions burned: 25 (million)
% 0.78/0.51 % (3673635)Instruction limit reached!
% 0.78/0.51 % (3673635)------------------------------
% 0.78/0.51 % (3673635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.51 % (3673635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.51 % (3673635)CaDiCaL version: 2.1.3
% 0.78/0.51 % (3673635)Termination reason: Instruction limit
% 0.78/0.51 % (3673635)Termination phase: shuffling
% 0.78/0.51 % (3673635)Time elapsed: 0.007 s
% 0.78/0.51 % (3673635)Peak memory usage: 10 MB
% 0.78/0.51 % (3673635)Instructions burned: 16 (million)
% 0.78/0.51 % (3673639)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2725963826:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.78/0.51 % (3673640)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3135427348:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.78/0.51 % (3673643)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1285449996:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.78/0.51 % (3673639)Instruction limit reached!
% 0.78/0.51 % (3673639)------------------------------
% 0.78/0.51 % (3673639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.51 % (3673639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.51 % (3673639)CaDiCaL version: 2.1.3
% 0.78/0.51 % (3673639)Termination reason: Instruction limit
% 0.78/0.51 % (3673639)Termination phase: shuffling
% 0.78/0.51 % (3673639)Time elapsed: 0.002 s
% 0.78/0.51 % (3673639)Peak memory usage: 10 MB
% 0.78/0.51 % (3673639)Instructions burned: 5 (million)
% 0.78/0.51 % (3673644)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3391104437:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.78/0.51 % (3673640)Instruction limit reached!
% 0.78/0.51 % (3673640)------------------------------
% 0.78/0.51 % (3673640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.51 % (3673640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.51 % (3673640)CaDiCaL version: 2.1.3
% 0.78/0.51 % (3673640)Termination reason: Instruction limit
% 0.78/0.51 % (3673640)Termination phase: shuffling
% 0.78/0.51 % (3673640)Time elapsed: 0.012 s
% 0.78/0.51 % (3673640)Peak memory usage: 10 MB
% 0.78/0.51 % (3673640)Instructions burned: 28 (million)
% 0.78/0.51 % (3673643)Instruction limit reached!
% 0.78/0.51 % (3673643)------------------------------
% 0.78/0.51 % (3673643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.51 % (3673643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.57 % (3673643)CaDiCaL version: 2.1.3
% 1.57/0.57 % (3673643)Termination reason: Instruction limit
% 1.57/0.57 % (3673643)Termination phase: Property scanning
% 1.57/0.57 % (3673643)Time elapsed: 0.010 s
% 1.57/0.57 % (3673643)Peak memory usage: 10 MB
% 1.57/0.57 % (3673643)Instructions burned: 24 (million)
% 1.57/0.57 % (3673648)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.57/0.57 % (3673648)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.57/0.57 % (3673648)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=211601277:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.57/0.57 % (3673650)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.57/0.57 % (3673648)Instruction limit reached!
% 1.57/0.57 % (3673648)------------------------------
% 1.57/0.57 % (3673648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.58 % (3673648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.58 % (3673648)CaDiCaL version: 2.1.3
% 1.57/0.58 % (3673648)Termination reason: Instruction limit
% 1.57/0.58 % (3673648)Termination phase: shuffling
% 1.57/0.58 % (3673648)Time elapsed: 0.007 s
% 1.57/0.58 % (3673648)Peak memory usage: 10 MB
% 1.57/0.58 % (3673648)Instructions burned: 16 (million)
% 1.57/0.58 % (3673651)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=716348633:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.57/0.58 % (3673650)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=1167686292:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.57/0.58 % (3673650)Instruction limit reached!
% 1.57/0.58 % (3673650)------------------------------
% 1.57/0.58 % (3673650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.58 % (3673650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.58 % (3673650)CaDiCaL version: 2.1.3
% 1.57/0.58 % (3673650)Termination reason: Instruction limit
% 1.57/0.58 % (3673650)Termination phase: shuffling
% 1.57/0.58 % (3673650)Time elapsed: 0.004 s
% 1.57/0.58 % (3673650)Peak memory usage: 10 MB
% 1.57/0.58 % (3673650)Instructions burned: 9 (million)
% 1.57/0.58 % (3673644)Instruction limit reached!
% 1.57/0.58 % (3673644)------------------------------
% 1.57/0.58 % (3673644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.58 % (3673644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.58 % (3673644)CaDiCaL version: 2.1.3
% 1.57/0.58 % (3673644)Termination reason: Instruction limit
% 1.57/0.58 % (3673644)Termination phase: Saturation
% 1.57/0.58 % (3673644)Time elapsed: 0.027 s
% 1.57/0.58 % (3673644)Peak memory usage: 12 MB
% 1.57/0.58 % (3673644)Instructions burned: 61 (million)
% 1.57/0.58 % (3673651)Instruction limit reached!
% 1.57/0.58 % (3673651)------------------------------
% 1.57/0.58 % (3673651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.58 % (3673651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.58 % (3673651)CaDiCaL version: 2.1.3
% 1.57/0.58 % (3673651)Termination reason: Instruction limit
% 1.57/0.58 % (3673651)Termination phase: Property scanning
% 1.57/0.58 % (3673651)Time elapsed: 0.014 s
% 1.57/0.58 % (3673651)Peak memory usage: 10 MB
% 1.57/0.58 % (3673651)Instructions burned: 32 (million)
% 1.57/0.58 % (3673634)Instruction limit reached!
% 1.57/0.58 % (3673634)------------------------------
% 1.57/0.58 % (3673634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.58 % (3673634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.58 % (3673634)CaDiCaL version: 2.1.3
% 1.57/0.58 % (3673634)Termination reason: Instruction limit
% 1.57/0.58 % (3673634)Termination phase: Saturation
% 1.57/0.58 % (3673634)Time elapsed: 0.075 s
% 1.57/0.58 % (3673634)Peak memory usage: 15 MB
% 1.57/0.58 % (3673634)Instructions burned: 330 (million)
% 1.57/0.58 % (3673653)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3738258436:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.31/0.64 % (3673653)Instruction limit reached!
% 2.31/0.64 % (3673653)------------------------------
% 2.31/0.64 % (3673653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.64 % (3673653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.64 % (3673653)CaDiCaL version: 2.1.3
% 2.31/0.64 % (3673653)Termination reason: Instruction limit
% 2.31/0.64 % (3673653)Termination phase: shuffling
% 2.31/0.64 % (3673653)Time elapsed: 0.004 s
% 2.31/0.64 % (3673653)Peak memory usage: 10 MB
% 2.31/0.64 % (3673653)Instructions burned: 7 (million)
% 2.31/0.64 % (3673656)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1732280571:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.31/0.64 % (3673657)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=411122815:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.31/0.64 % (3673659)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1004843227:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.31/0.64 % (3673658)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=735587435:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.31/0.64 % (3673657)Instruction limit reached!
% 2.31/0.64 % (3673657)------------------------------
% 2.31/0.64 % (3673657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.64 % (3673657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.64 % (3673657)CaDiCaL version: 2.1.3
% 2.31/0.64 % (3673657)Termination reason: Instruction limit
% 2.31/0.64 % (3673657)Termination phase: Property scanning
% 2.31/0.64 % (3673657)Time elapsed: 0.010 s
% 2.31/0.64 % (3673657)Peak memory usage: 10 MB
% 2.31/0.64 % (3673657)Instructions burned: 22 (million)
% 2.31/0.64 % (3673656)Instruction limit reached!
% 2.31/0.64 % (3673656)------------------------------
% 2.31/0.64 % (3673656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.64 % (3673656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.64 % (3673656)CaDiCaL version: 2.1.3
% 2.31/0.64 % (3673656)Termination reason: Instruction limit
% 2.31/0.64 % (3673656)Termination phase: Property scanning
% 2.31/0.64 % (3673656)Time elapsed: 0.011 s
% 2.31/0.64 % (3673656)Peak memory usage: 10 MB
% 2.31/0.64 % (3673656)Instructions burned: 26 (million)
% 2.31/0.64 % (3673661)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2145596965:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.31/0.64 % (3673667)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.31/0.64 % (3673667)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=488645386:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.31/0.64 % (3673666)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=260061261:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.31/0.64 % (3673659)Instruction limit reached!
% 2.31/0.64 % (3673659)------------------------------
% 2.31/0.64 % (3673659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.64 % (3673659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.64 % (3673659)CaDiCaL version: 2.1.3
% 2.31/0.64 % (3673659)Termination reason: Instruction limit
% 2.31/0.64 % (3673659)Termination phase: Saturation
% 2.31/0.64 % (3673659)Time elapsed: 0.031 s
% 2.31/0.64 % (3673659)Peak memory usage: 12 MB
% 2.31/0.64 % (3673659)Instructions burned: 146 (million)
% 2.31/0.64 % (3673667)Instruction limit reached!
% 2.31/0.64 % (3673667)------------------------------
% 2.31/0.64 % (3673667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.64 % (3673667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.64 % (3673667)CaDiCaL version: 2.1.3
% 2.31/0.64 % (3673667)Termination reason: Instruction limit
% 2.31/0.64 % (3673667)Termination phase: shuffling
% 2.31/0.64 % (3673667)Time elapsed: 0.004 s
% 2.31/0.64 % (3673667)Peak memory usage: 9 MB
% 2.31/0.64 % (3673667)Instructions burned: 9 (million)
% 2.31/0.64 % (3673671)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=725271012:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.69/0.71 % (3673666)Instruction limit reached!
% 2.69/0.71 % (3673666)------------------------------
% 2.69/0.71 % (3673666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.71 % (3673666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.71 % (3673666)CaDiCaL version: 2.1.3
% 2.69/0.71 % (3673666)Termination reason: Instruction limit
% 2.69/0.71 % (3673666)Termination phase: Function definition elimination
% 2.69/0.71 % (3673666)Time elapsed: 0.019 s
% 2.69/0.71 % (3673666)Peak memory usage: 11 MB
% 2.69/0.71 % (3673666)Instructions burned: 45 (million)
% 2.69/0.71 % (3673672)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=818158194: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.69/0.71 % (3673674)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.69/0.71 % (3673674)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=329083320: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.69/0.71 % (3673674)Instruction limit reached!
% 2.69/0.71 % (3673674)------------------------------
% 2.69/0.71 % (3673674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.71 % (3673674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.71 % (3673674)CaDiCaL version: 2.1.3
% 2.69/0.71 % (3673674)Termination reason: Instruction limit
% 2.69/0.71 % (3673674)Termination phase: shuffling
% 2.69/0.71 % (3673674)Time elapsed: 0.003 s
% 2.69/0.71 % (3673674)Peak memory usage: 10 MB
% 2.69/0.71 % (3673674)Instructions burned: 6 (million)
% 2.69/0.71 % (3673628)Instruction limit reached!
% 2.69/0.71 % (3673628)------------------------------
% 2.69/0.71 % (3673628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.71 % (3673628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.71 % (3673628)CaDiCaL version: 2.1.3
% 2.69/0.71 % (3673628)Termination reason: Instruction limit
% 2.69/0.71 % (3673628)Termination phase: Saturation
% 2.69/0.71 % (3673628)Time elapsed: 0.159 s
% 2.69/0.71 % (3673628)Peak memory usage: 14 MB
% 2.69/0.71 % (3673628)Instructions burned: 249 (million)
% 2.69/0.71 % (3673671)Instruction limit reached!
% 2.69/0.71 % (3673671)------------------------------
% 2.69/0.71 % (3673671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.71 % (3673671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.71 % (3673671)CaDiCaL version: 2.1.3
% 2.69/0.71 % (3673671)Termination reason: Instruction limit
% 2.69/0.71 % (3673671)Termination phase: Saturation
% 2.69/0.71 % (3673671)Time elapsed: 0.048 s
% 2.69/0.71 % (3673671)Peak memory usage: 13 MB
% 2.69/0.71 % (3673671)Instructions burned: 184 (million)
% 2.69/0.71 % (3673677)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=819698426:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.69/0.71 % (3673679)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=125798130:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 2.69/0.71 % (3673677)Instruction limit reached!
% 2.69/0.71 % (3673677)------------------------------
% 2.69/0.71 % (3673677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.71 % (3673677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.71 % (3673677)CaDiCaL version: 2.1.3
% 2.69/0.71 % (3673677)Termination reason: Instruction limit
% 2.69/0.71 % (3673677)Termination phase: Property scanning
% 2.69/0.71 % (3673677)Time elapsed: 0.010 s
% 2.69/0.71 % (3673677)Peak memory usage: 10 MB
% 2.69/0.71 % (3673677)Instructions burned: 24 (million)
% 2.69/0.71 % (3673678)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3213738726:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.69/0.71 % (3673661)Instruction limit reached!
% 2.69/0.71 % (3673661)------------------------------
% 2.69/0.71 % (3673661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673661)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673661)Termination reason: Instruction limit
% 2.69/0.74 % (3673661)Termination phase: Saturation
% 2.69/0.74 % (3673661)Time elapsed: 0.096 s
% 2.69/0.74 % (3673661)Peak memory usage: 14 MB
% 2.69/0.74 % (3673661)Instructions burned: 194 (million)
% 2.69/0.74 % (3673678)Instruction limit reached!
% 2.69/0.74 % (3673678)------------------------------
% 2.69/0.74 % (3673678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673678)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673678)Termination reason: Instruction limit
% 2.69/0.74 % (3673678)Termination phase: Property scanning
% 2.69/0.74 % (3673678)Time elapsed: 0.015 s
% 2.69/0.74 % (3673678)Peak memory usage: 10 MB
% 2.69/0.74 % (3673678)Instructions burned: 21 (million)
% 2.69/0.74 % (3673672)Instruction limit reached!
% 2.69/0.74 % (3673672)------------------------------
% 2.69/0.74 % (3673672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673672)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673672)Termination reason: Instruction limit
% 2.69/0.74 % (3673672)Termination phase: Saturation
% 2.69/0.74 % (3673672)Time elapsed: 0.071 s
% 2.69/0.74 % (3673672)Peak memory usage: 13 MB
% 2.69/0.74 % (3673672)Instructions burned: 169 (million)
% 2.69/0.74 % (3673682)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=2891657000:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 2.69/0.74 % (3673684)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=235207015:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 2.69/0.74 % (3673684)Instruction limit reached!
% 2.69/0.74 % (3673684)------------------------------
% 2.69/0.74 % (3673684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673684)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673684)Termination reason: Instruction limit
% 2.69/0.74 % (3673684)Termination phase: Preprocessing 1
% 2.69/0.74 % (3673684)Time elapsed: 0.020 s
% 2.69/0.74 % (3673684)Peak memory usage: 11 MB
% 2.69/0.74 % (3673684)Instructions burned: 45 (million)
% 2.69/0.74 % (3673686)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3211531468:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 2.69/0.74 % (3673688)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2289855895:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 2.69/0.74 % (3673689)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.69/0.74 % (3673688)Instruction limit reached!
% 2.69/0.74 % (3673688)------------------------------
% 2.69/0.74 % (3673688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673688)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673688)Termination reason: Instruction limit
% 2.69/0.74 % (3673688)Termination phase: Property scanning
% 2.69/0.74 % (3673688)Time elapsed: 0.010 s
% 2.69/0.74 % (3673688)Peak memory usage: 10 MB
% 2.69/0.74 % (3673688)Instructions burned: 22 (million)
% 2.69/0.74 % (3673689)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=379614408:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 2.69/0.74 % (3673602)Instruction limit reached!
% 2.69/0.74 % (3673602)------------------------------
% 2.69/0.74 % (3673602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673602)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673602)Termination reason: Instruction limit
% 2.69/0.74 % (3673602)Termination phase: Saturation
% 2.69/0.74 % (3673602)Time elapsed: 0.332 s
% 2.69/0.74 % (3673602)Peak memory usage: 16 MB
% 2.69/0.74 % (3673602)Instructions burned: 634 (million)
% 2.69/0.74 % (3673679)Instruction limit reached!
% 2.69/0.74 % (3673679)------------------------------
% 2.69/0.74 % (3673679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673679)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673679)Termination reason: Instruction limit
% 2.69/0.74 % (3673679)Termination phase: Saturation
% 2.69/0.74 % (3673679)Time elapsed: 0.071 s
% 2.69/0.74 % (3673679)Peak memory usage: 15 MB
% 2.69/0.74 % (3673679)Instructions burned: 318 (million)
% 2.69/0.74 % (3673695)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2889836838:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 2.69/0.74 % (3673692)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3765090818:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 2.69/0.74 % (3673694)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=3902151869:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 2.69/0.74 % (3673692)Instruction limit reached!
% 2.69/0.74 % (3673692)------------------------------
% 2.69/0.74 % (3673692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673692)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673692)Termination reason: Instruction limit
% 2.69/0.74 % (3673692)Termination phase: shuffling
% 2.69/0.74 % (3673692)Time elapsed: 0.007 s
% 2.69/0.74 % (3673692)Peak memory usage: 10 MB
% 2.69/0.74 % (3673692)Instructions burned: 15 (million)
% 2.69/0.74 % (3673695)Instruction limit reached!
% 2.69/0.74 % (3673695)------------------------------
% 2.69/0.74 % (3673695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673695)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673695)Termination reason: Instruction limit
% 2.69/0.74 % (3673695)Termination phase: Function definition elimination
% 2.69/0.74 % (3673695)Time elapsed: 0.012 s
% 2.69/0.74 % (3673695)Peak memory usage: 11 MB
% 2.69/0.74 % (3673695)Instructions burned: 52 (million)
% 2.69/0.74 % (3673700)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3425539494:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 2.69/0.74 % (3673699)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3582092666:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 2.69/0.74 % (3673694)Instruction limit reached!
% 2.69/0.74 % (3673694)------------------------------
% 2.69/0.74 % (3673694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673694)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673694)Termination reason: Instruction limit
% 2.69/0.74 % (3673694)Termination phase: Function definition elimination
% 2.69/0.74 % (3673694)Time elapsed: 0.029 s
% 2.69/0.74 % (3673694)Peak memory usage: 11 MB
% 2.69/0.74 % (3673694)Instructions burned: 68 (million)
% 2.69/0.74 % (3673699)Instruction limit reached!
% 2.69/0.74 % (3673699)------------------------------
% 2.69/0.74 % (3673699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673699)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673699)Termination reason: Instruction limit
% 2.69/0.74 % (3673699)Termination phase: Property scanning
% 2.69/0.74 % (3673699)Time elapsed: 0.014 s
% 2.69/0.74 % (3673699)Peak memory usage: 10 MB
% 2.69/0.74 % (3673699)Instructions burned: 33 (million)
% 2.69/0.74 % (3673703)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=288362513:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 2.69/0.74 % (3673704)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3417323689:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 2.69/0.74 % (3673689)Instruction limit reached!
% 2.69/0.74 % (3673689)------------------------------
% 2.69/0.74 % (3673689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673689)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673689)Termination reason: Instruction limit
% 2.69/0.74 % (3673689)Termination phase: Saturation
% 2.69/0.74 % (3673689)Time elapsed: 0.082 s
% 2.69/0.74 % (3673689)Peak memory usage: 12 MB
% 2.69/0.74 % (3673689)Instructions burned: 202 (million)
% 2.69/0.74 % (3673703)Instruction limit reached!
% 2.69/0.74 % (3673703)------------------------------
% 2.69/0.74 % (3673703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673703)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673703)Termination reason: Instruction limit
% 2.69/0.74 % (3673703)Termination phase: Property scanning
% 2.69/0.74 % (3673703)Time elapsed: 0.012 s
% 2.69/0.74 % (3673703)Peak memory usage: 10 MB
% 2.69/0.74 % (3673703)Instructions burned: 37 (million)
% 2.69/0.74 % (3673700) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3673594-3673700"...
% 2.69/0.74 % (3673700)...printing done.
% 2.69/0.74 % (3673700)Refutation found. Thanks to Tanya!
% 2.69/0.74 % SZS status Theorem for theBenchmark
% 2.69/0.74 % SZS output start Proof for theBenchmark
% 2.69/0.74 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 2.69/0.74 thf(func_def_0, type, c_Eps_i: (($i > $o) > $i)).
% 2.69/0.74 thf(func_def_1, type, c_False: $o).
% 2.69/0.74 thf(func_def_2, type, c_True: $o).
% 2.69/0.74 thf(func_def_3, type, c_not: ($o > $o)).
% 2.69/0.74 thf(func_def_4, type, c_and: ($o > $o > $o)).
% 2.69/0.74 thf(func_def_5, type, c_or: ($o > $o > $o)).
% 2.69/0.74 thf(func_def_6, type, c_iff: ($o > $o > $o)).
% 2.69/0.74 thf(func_def_7, type, c_In: ($i > $i > $o)).
% 2.69/0.74 thf(func_def_8, type, c_Subq: ($i > $i > $o)).
% 2.69/0.74 thf(func_def_10, type, c_Union: ($i > $i)).
% 2.69/0.74 thf(func_def_11, type, c_Power: ($i > $i)).
% 2.69/0.74 thf(func_def_12, type, c_Repl: ($i > ($i > $i) > $i)).
% 2.69/0.74 thf(func_def_13, type, c_TransSet: ($i > $o)).
% 2.69/0.74 thf(func_def_14, type, c_atleast2: ($i > $o)).
% 2.69/0.74 thf(func_def_15, type, c_atleast3: ($i > $o)).
% 2.69/0.74 thf(func_def_16, type, c_atleast4: ($i > $o)).
% 2.69/0.74 thf(func_def_17, type, c_atleast5: ($i > $o)).
% 2.69/0.74 thf(func_def_18, type, c_atleast6: ($i > $o)).
% 2.69/0.74 thf(func_def_19, type, c_exactly2: ($i > $o)).
% 2.69/0.74 thf(func_def_20, type, c_exactly3: ($i > $o)).
% 2.69/0.74 thf(func_def_21, type, c_exactly4: ($i > $o)).
% 2.69/0.74 thf(func_def_22, type, c_exactly5: ($i > $o)).
% 2.69/0.74 thf(func_def_23, type, c_exu_i: (($i > $o) > $o)).
% 2.69/0.74 thf(func_def_24, type, c_reflexive_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_25, type, c_irreflexive_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_26, type, c_symmetric_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_27, type, c_antisymmetric_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_28, type, c_transitive_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_29, type, c_eqreln_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_30, type, c_per_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_31, type, c_linear_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_32, type, c_trichotomous_or_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_33, type, c_partialorder_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_34, type, c_totalorder_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_35, type, c_strictpartialorder_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_36, type, c_stricttotalorder_i: (($i > $i > $o) > $o)).
% 2.69/0.74 thf(func_def_37, type, c_If_i: ($o > $i > $i > $i)).
% 2.69/0.74 thf(func_def_38, type, c_exactly1of2: ($o > $o > $o)).
% 2.69/0.74 thf(func_def_39, type, c_exactly1of3: ($o > $o > $o > $o)).
% 2.69/0.74 thf(func_def_40, type, c_nIn: ($i > $i > $o)).
% 2.69/0.74 thf(func_def_41, type, c_nSubq: ($i > $i > $o)).
% 2.69/0.74 thf(func_def_42, type, c_UPair: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_43, type, c_Sing: ($i > $i)).
% 2.69/0.74 thf(func_def_44, type, c_binunion: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_45, type, c_SetAdjoin: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_46, type, c_famunion: ($i > ($i > $i) > $i)).
% 2.69/0.74 thf(func_def_47, type, c_Sep: ($i > ($i > $o) > $i)).
% 2.69/0.74 thf(func_def_48, type, c_ReplSep: ($i > ($i > $o) > ($i > $i) > $i)).
% 2.69/0.74 thf(func_def_49, type, c_binintersect: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_50, type, c_setminus: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_51, type, c_inj: ($i > $i > ($i > $i) > $o)).
% 2.69/0.74 thf(func_def_52, type, c_bij: ($i > $i > ($i > $i) > $o)).
% 2.69/0.74 thf(func_def_53, type, c_atleastp: ($i > $i > $o)).
% 2.69/0.74 thf(func_def_54, type, c_equip: ($i > $i > $o)).
% 2.69/0.74 thf(func_def_55, type, c_In_rec_poly_G_i: (($i > ($i > $i) > $i) > $i > $i > $o)).
% 2.69/0.74 thf(func_def_56, type, c_In_rec_poly_i: (($i > ($i > $i) > $i) > $i > $i)).
% 2.69/0.74 thf(func_def_57, type, c_ordsucc: ($i > $i)).
% 2.69/0.74 thf(func_def_58, type, c_nat_p: ($i > $o)).
% 2.69/0.74 thf(func_def_59, type, c_nat_primrec: ($i > ($i > $i > $i) > $i > $i)).
% 2.69/0.74 thf(func_def_60, type, c_add_nat: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_61, type, c_mul_nat: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_62, type, c_ordinal: ($i > $o)).
% 2.69/0.74 thf(func_def_63, type, c_V_: ($i > $i)).
% 2.69/0.74 thf(func_def_64, type, c_Inj1: ($i > $i)).
% 2.69/0.74 thf(func_def_65, type, c_Inj0: ($i > $i)).
% 2.69/0.74 thf(func_def_66, type, c_Unj: ($i > $i)).
% 2.69/0.74 thf(func_def_67, type, c_combine_funcs: ($i > $i > ($i > $i) > ($i > $i) > $i > $i)).
% 2.69/0.74 thf(func_def_68, type, c_setsum: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_69, type, c_proj0: ($i > $i)).
% 2.69/0.74 thf(func_def_70, type, c_proj1: ($i > $i)).
% 2.69/0.74 thf(func_def_71, type, c_binrep: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_72, type, c_lam: ($i > ($i > $i) > $i)).
% 2.69/0.74 thf(func_def_73, type, c_setprod: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_74, type, c_ap: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_75, type, c_setsum_p: ($i > $o)).
% 2.69/0.74 thf(func_def_76, type, c_tuple_p: ($i > $i > $o)).
% 2.69/0.74 thf(func_def_77, type, c_Pi: ($i > ($i > $i) > $i)).
% 2.69/0.74 thf(func_def_78, type, c_setexp: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_79, type, c_Sep2: ($i > ($i > $i) > ($i > $i > $o) > $i)).
% 2.69/0.74 thf(func_def_80, type, c_set_of_pairs: ($i > $o)).
% 2.69/0.74 thf(func_def_81, type, c_lam2: ($i > ($i > $i) > ($i > $i > $i) > $i)).
% 2.69/0.74 thf(func_def_82, type, c_PNoEq_: ($i > ($i > $o) > ($i > $o) > $o)).
% 2.69/0.74 thf(func_def_83, type, c_PNoLt_: ($i > ($i > $o) > ($i > $o) > $o)).
% 2.69/0.74 thf(func_def_84, type, c_PNoLt: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 2.69/0.74 thf(func_def_85, type, c_PNoLe: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 2.69/0.74 thf(func_def_86, type, c_PNo_downc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 2.69/0.74 thf(func_def_87, type, c_PNo_upc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 2.69/0.74 thf(func_def_88, type, c_SNoElts_: ($i > $i)).
% 2.69/0.74 thf(func_def_89, type, c_SNo_: ($i > $i > $o)).
% 2.69/0.74 thf(func_def_90, type, c_PSNo: ($i > ($i > $o) > $i)).
% 2.69/0.74 thf(func_def_91, type, c_SNo: ($i > $o)).
% 2.69/0.74 thf(func_def_92, type, c_SNoLev: ($i > $i)).
% 2.69/0.74 thf(func_def_93, type, c_SNoEq_: ($i > $i > $i > $o)).
% 2.69/0.74 thf(func_def_94, type, c_SNoLt: ($i > $i > $o)).
% 2.69/0.74 thf(func_def_95, type, c_SNoLe: ($i > $i > $o)).
% 2.69/0.74 thf(func_def_96, type, c_binop_on: ($i > ($i > $i > $i) > $o)).
% 2.69/0.74 thf(func_def_97, type, c_Loop: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > $o)).
% 2.69/0.74 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)).
% 2.69/0.74 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)).
% 2.69/0.74 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)).
% 2.69/0.74 thf(func_def_101, type, c_combinator: ($i > $o)).
% 2.69/0.74 thf(func_def_102, type, c_combinator_equiv: ($i > $i > $o)).
% 2.69/0.74 thf(func_def_103, type, c_equip_mod: ($i > $i > $i > $o)).
% 2.69/0.74 thf(func_def_105, type, db0: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_106, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.69/0.74 thf(func_def_107, type, vIMP: ($o > $o > $o)).
% 2.69/0.74 thf(func_def_108, type, db1: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_109, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 2.69/0.74 thf(func_def_110, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.69/0.74 thf(func_def_111, type, db2: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_114, type, db3: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_115, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.69/0.74 thf(func_def_116, type, db4: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_117, type, db5: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_118, type, db6: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_119, type, db13: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_120, type, db12: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_121, type, db11: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_122, type, db10: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_123, type, db9: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_124, type, db8: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_125, type, db7: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_126, type, db14: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_127, type, db15: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_128, type, db16: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_129, type, db17: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_130, type, db18: !>[X0: $tType]:(X0)).
% 2.69/0.74 thf(func_def_131, type, sP0: (($i > $o) > $o)).
% 2.69/0.74 thf(func_def_132, type, sP1: (($i > $o) > $o)).
% 2.69/0.74 thf(func_def_133, type, sK2: (($i > $i) > $i > $i)).
% 2.69/0.74 thf(func_def_134, type, sK3: (($i > $i) > ($i > $i) > $i)).
% 2.69/0.74 thf(func_def_135, type, sK4: (($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i)).
% 2.69/0.74 thf(func_def_136, type, sK5: (((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i)).
% 2.69/0.74 thf(func_def_137, type, sK6: (($i > $o) > $i)).
% 2.69/0.74 thf(func_def_138, type, sK7: (($i > $o) > $i)).
% 2.69/0.74 thf(func_def_139, type, sK8: (($i > $o) > $i)).
% 2.69/0.74 thf(func_def_140, type, sK9: (($i > $o) > $i > $i)).
% 2.69/0.74 thf(func_def_141, type, sK10: (($i > $o) > $i)).
% 2.69/0.74 thf(func_def_142, type, sK11: (($i > $o) > $i)).
% 2.69/0.74 thf(func_def_143, type, sK12: (($i > $o) > $i)).
% 2.69/0.74 thf(func_def_151, type, sF20: (($i > $i) > $i)).
% 2.69/0.74 thf(func_def_153, type, sF22: (($i > $i) > $i)).
% 2.69/0.74 thf(func_def_156, type, sF25: (($i > $i) > $i)).
% 2.69/0.74 thf(func_def_157, type, sF26: (($i > $i) > ($i > $i) > $i)).
% 2.69/0.74 thf(func_def_158, type, sF27: (($i > $i) > $i)).
% 2.69/0.74 thf(func_def_160, type, sF29: (($i > ($i > $i > $i) > $i) > $i)).
% 2.69/0.74 thf(func_def_161, type, sF30: (($i > ($i > $i > $i) > $i) > ($i > $i) > $i)).
% 2.69/0.74 thf(func_def_162, type, sF31: (($i > $i) > ($i > ($i > $i > $i) > $i) > ($i > $i) > $i)).
% 2.69/0.74 thf(func_def_163, type, sF32: (($i > ($i > $i > $i) > $i) > ($i > $i) > ($i > $i) > $i)).
% 2.69/0.74 thf(func_def_164, type, sF33: ((($i > $i) > ($i > $i) > $i) > $i)).
% 2.69/0.74 thf(func_def_171, type, sF40: ((($i > $i) > ($i > $i) > $i) > $i)).
% 2.69/0.74 thf(func_def_172, type, sF41: ($i > (($i > $i) > ($i > $i) > $i) > $i)).
% 2.69/0.74 thf(func_def_173, type, sF42: ((($i > $i) > ($i > $i) > $i) > $i > $i)).
% 2.69/0.74 thf(func_def_174, type, sF43: ($i > (($i > $i) > ($i > $i) > $i) > $i)).
% 2.69/0.74 thf(func_def_175, type, sF44: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_176, type, sF45: ($i > $i)).
% 2.69/0.74 thf(func_def_177, type, sF46: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_181, type, sF50: ($i > $i)).
% 2.69/0.74 thf(func_def_182, type, sF51: ($i > $i)).
% 2.69/0.74 thf(func_def_183, type, sF52: ($i > $i)).
% 2.69/0.74 thf(func_def_184, type, sF53: ($i > $i)).
% 2.69/0.74 thf(func_def_185, type, sF54: ($i > $i)).
% 2.69/0.74 thf(func_def_186, type, sF55: ($i > $i > $i)).
% 2.69/0.74 thf(func_def_187, type, sF56: ($i > $i)).
% 2.69/0.74 thf(func_def_188, type, sF57: ($i > $i)).
% 2.69/0.74 thf(func_def_190, type, sF59: ($i > ($i > $i) > $i)).
% 2.69/0.74 thf(func_def_191, type, sF60: (($i > $i) > $i)).
% 2.69/0.74 thf(func_def_192, type, sK61: $o).
% 2.69/0.74 thf(func_def_193, type, sK62: $o).
% 2.69/0.74 thf(func_def_196, type, sK65: ($o > $o > $o)).
% 2.69/0.74 thf(func_def_198, type, sK67: ($i > $i > $i)).
% 2.69/0.74 thf(f2,axiom,(
% 2.69/0.74 ! [X0 : $o] : ((c_not @ (c_not @ X0)) => X0)),
% 2.69/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2)).
% 2.69/0.74 thf(f3,axiom,(
% 2.69/0.74 ! [X1 : $o,X0 : $o] : ((c_iff @ X0 @ X1) => (X0 = X1))),
% 2.69/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3)).
% 2.69/0.74 thf(f5,axiom,(
% 2.69/0.74 (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 2.69/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5)).
% 2.69/0.74 thf(f7,axiom,(
% 2.69/0.74 ! [X1 : $i,X0 : $i] : (c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))),
% 2.69/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7)).
% 2.69/0.74 thf(f13,axiom,(
% 2.69/0.74 ((^[X0 : $o] : (X0 => c_False)) = c_not)),
% 2.69/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13)).
% 2.69/0.74 thf(f17,axiom,(
% 2.69/0.74 ((^[X0 : $i, X1 : $i] : (! [X2 : $i] : ((c_In @ X2 @ X0) => (c_In @ X2 @ X1)))) = c_Subq)),
% 2.69/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17)).
% 2.69/0.74 thf(f109,conjecture,(
% 2.69/0.74 ! [X2 : (((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i),X0 : (($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i),X3 : (($i > $i) > ($i > $i) > $i),X1 : (($i > $i) > $i > $i)] : (! [X4 : ($i > (($i > $i) > $i) > $i),X7 : $i,X6 : ((($i > $i > $i) > ($i > $i) > $i) > $i),X5 : (($i > $i) > $i)] : (((c_Inj1 @ c_Empty)) = ((X3 @ (^[X8 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X8 : $i] : ((c_setsum @ c_Empty @ c_Empty)))))) => (! [X7 : $i,X4 : $i,X5 : $i,X6 : $i] : (((c_setsum @ (X2 @ (^[X8 : (($i > $i > $i > $i) > $i), X9 : $i] : (c_Empty)) @ (X0 @ (^[X8 : $i, X9 : $i, X10 : $i] : ((X3 @ (^[X11 : $i] : (X10)) @ (^[X11 : $i] : (c_Empty))))) @ (^[X8 : $i] : (c_Empty)) @ (^[X8 : ($i > $i > $i)] : (c_Empty)))) @ c_Empty)) = ((X3 @ (^[X8 : $i] : (X6)) @ (^[X8 : $i] : (X7))))) => (! [X5 : ($i > $i > $i),X4 : ($i > $i),X7 : $i,X6 : ($i > $i)] : (X7 = ((X2 @ (^[X8 : (($i > $i > $i > $i) > $i), X9 : $i] : (X7)) @ c_Empty))) => (! [X7 : ($i > $i),X5 : ($i > $i),X4 : ($i > ($i > $i > $i) > $i),X6 : (((($i > $i) > $i) > $i) > $i)] : (((X2 @ (^[X8 : (($i > $i > $i > $i) > $i), X9 : $i] : ((X7 @ (X2 @ (^[X10 : (($i > $i > $i > $i) > $i), X11 : $i] : ((X0 @ (^[X12 : $i, X13 : $i, X14 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X12 : $i] : ((c_Inj0 @ c_Empty))) @ (^[X12 : ($i > $i > $i)] : ((X3 @ (^[X13 : $i] : (c_Empty)) @ (^[X13 : $i] : (c_Empty)))))))) @ (c_Inj0 @ (X0 @ (^[X10 : $i, X11 : $i, X12 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ (^[X10 : ($i > $i > $i)] : (c_Empty)))))))) @ (X3 @ (^[X8 : $i] : ((c_setsum @ X8 @ c_Empty))) @ (^[X8 : $i] : (c_Empty))))) = ((c_setsum @ (X7 @ (X5 @ (X0 @ (^[X8 : $i, X9 : $i, X10 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X8 : $i] : ((X0 @ (^[X9 : $i, X10 : $i, X11 : $i] : (c_Empty)) @ (^[X9 : $i] : (c_Empty)) @ (^[X9 : ($i > $i > $i)] : (c_Empty))))) @ (^[X8 : ($i > $i > $i)] : ((c_setsum @ c_Empty @ c_Empty)))))) @ (X1 @ (^[X8 : $i] : ((X7 @ c_Empty))) @ (X5 @ (X4 @ (X1 @ (^[X8 : $i] : (c_Empty)) @ c_Empty) @ (^[X8 : $i, X9 : $i] : (c_Empty)))))))) => (! [X7 : $i,X5 : $i,X6 : $i,X4 : ((($i > $i) > $i > $i) > $i)] : (((c_Inj0 @ (X2 @ (^[X8 : (($i > $i > $i > $i) > $i), X9 : $i] : (X7)) @ (c_setsum @ c_Empty @ c_Empty)))) = ((X1 @ (^[X8 : $i] : ((c_Inj1 @ (X1 @ (^[X9 : $i] : ((c_Inj0 @ (X0 @ (^[X10 : $i, X11 : $i, X12 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ (^[X10 : ($i > $i > $i)] : (c_Empty)))))) @ (c_Inj1 @ X7))))) @ (c_Inj0 @ (X2 @ (^[X8 : (($i > $i > $i > $i) > $i), X9 : $i] : (X9)) @ X5))))) => (! [X7 : (($i > $i) > ($i > $i) > $i),X4 : ((($i > $i) > $i) > $i),X5 : ($i > $i > ($i > $i) > $i),X6 : $i] : (((X1 @ (^[X8 : $i] : ((X7 @ (^[X9 : $i] : ((c_setsum @ X9 @ X8))) @ (^[X9 : $i] : (c_Empty))))) @ c_Empty)) = ((X7 @ (^[X8 : $i] : ((c_setsum @ (X2 @ (^[X9 : (($i > $i > $i > $i) > $i), X10 : $i] : (c_Empty)) @ (X3 @ (^[X9 : $i] : ((X2 @ (^[X10 : (($i > $i > $i > $i) > $i), X11 : $i] : (c_Empty)) @ c_Empty))) @ (^[X9 : $i] : ((X1 @ (^[X10 : $i] : (c_Empty)) @ c_Empty))))) @ (X2 @ (^[X9 : (($i > $i > $i > $i) > $i), X10 : $i] : (c_Empty)) @ (X2 @ (^[X9 : (($i > $i > $i > $i) > $i), X10 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ (X2 @ (^[X9 : (($i > $i > $i > $i) > $i), X10 : $i] : (c_Empty)) @ c_Empty)))))) @ (^[X8 : $i] : ((c_Inj1 @ (X1 @ (^[X9 : $i] : ((X7 @ (^[X10 : $i] : ((X1 @ (^[X11 : $i] : (c_Empty)) @ c_Empty))) @ (^[X10 : $i] : ((c_Inj1 @ c_Empty)))))) @ X6))))))) => (! [X6 : $i,X7 : $i,X5 : $i,X4 : ($i > (($i > $i) > $i > $i) > $i)] : (((X0 @ (^[X8 : $i, X9 : $i, X10 : $i] : (X7)) @ (^[X8 : $i] : (X6)) @ (^[X8 : ($i > $i > $i)] : (c_Empty)))) = X6) => (! [X6 : ($i > ($i > $i) > $i),X5 : $i,X7 : ($i > $i),X4 : $i] : (((X7 @ X4)) = ((X0 @ (^[X8 : $i, X9 : $i, X10 : $i] : ((X1 @ (^[X11 : $i] : ((X2 @ (^[X12 : (($i > $i > $i > $i) > $i), X13 : $i] : (X10)) @ (X2 @ (^[X12 : (($i > $i > $i > $i) > $i), X13 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ X11)))) @ (c_Inj1 @ c_Empty)))) @ (^[X8 : $i] : ((X7 @ c_Empty))) @ (^[X8 : ($i > $i > $i)] : (c_Empty))))) => c_False))))))))),
% 2.69/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 2.69/0.74 thf(f110,negated_conjecture,(
% 2.69/0.74 ~ ! [X2 : (((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i),X0 : (($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i),X3 : (($i > $i) > ($i > $i) > $i),X1 : (($i > $i) > $i > $i)] : (! [X4 : ($i > (($i > $i) > $i) > $i),X7 : $i,X6 : ((($i > $i > $i) > ($i > $i) > $i) > $i),X5 : (($i > $i) > $i)] : (((c_Inj1 @ c_Empty)) = ((X3 @ (^[X8 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X8 : $i] : ((c_setsum @ c_Empty @ c_Empty)))))) => (! [X7 : $i,X4 : $i,X5 : $i,X6 : $i] : (((c_setsum @ (X2 @ (^[X8 : (($i > $i > $i > $i) > $i), X9 : $i] : (c_Empty)) @ (X0 @ (^[X8 : $i, X9 : $i, X10 : $i] : ((X3 @ (^[X11 : $i] : (X10)) @ (^[X11 : $i] : (c_Empty))))) @ (^[X8 : $i] : (c_Empty)) @ (^[X8 : ($i > $i > $i)] : (c_Empty)))) @ c_Empty)) = ((X3 @ (^[X8 : $i] : (X6)) @ (^[X8 : $i] : (X7))))) => (! [X5 : ($i > $i > $i),X4 : ($i > $i),X7 : $i,X6 : ($i > $i)] : (X7 = ((X2 @ (^[X8 : (($i > $i > $i > $i) > $i), X9 : $i] : (X7)) @ c_Empty))) => (! [X7 : ($i > $i),X5 : ($i > $i),X4 : ($i > ($i > $i > $i) > $i),X6 : (((($i > $i) > $i) > $i) > $i)] : (((X2 @ (^[X8 : (($i > $i > $i > $i) > $i), X9 : $i] : ((X7 @ (X2 @ (^[X10 : (($i > $i > $i > $i) > $i), X11 : $i] : ((X0 @ (^[X12 : $i, X13 : $i, X14 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X12 : $i] : ((c_Inj0 @ c_Empty))) @ (^[X12 : ($i > $i > $i)] : ((X3 @ (^[X13 : $i] : (c_Empty)) @ (^[X13 : $i] : (c_Empty)))))))) @ (c_Inj0 @ (X0 @ (^[X10 : $i, X11 : $i, X12 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ (^[X10 : ($i > $i > $i)] : (c_Empty)))))))) @ (X3 @ (^[X8 : $i] : ((c_setsum @ X8 @ c_Empty))) @ (^[X8 : $i] : (c_Empty))))) = ((c_setsum @ (X7 @ (X5 @ (X0 @ (^[X8 : $i, X9 : $i, X10 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X8 : $i] : ((X0 @ (^[X9 : $i, X10 : $i, X11 : $i] : (c_Empty)) @ (^[X9 : $i] : (c_Empty)) @ (^[X9 : ($i > $i > $i)] : (c_Empty))))) @ (^[X8 : ($i > $i > $i)] : ((c_setsum @ c_Empty @ c_Empty)))))) @ (X1 @ (^[X8 : $i] : ((X7 @ c_Empty))) @ (X5 @ (X4 @ (X1 @ (^[X8 : $i] : (c_Empty)) @ c_Empty) @ (^[X8 : $i, X9 : $i] : (c_Empty)))))))) => (! [X7 : $i,X5 : $i,X6 : $i,X4 : ((($i > $i) > $i > $i) > $i)] : (((c_Inj0 @ (X2 @ (^[X8 : (($i > $i > $i > $i) > $i), X9 : $i] : (X7)) @ (c_setsum @ c_Empty @ c_Empty)))) = ((X1 @ (^[X8 : $i] : ((c_Inj1 @ (X1 @ (^[X9 : $i] : ((c_Inj0 @ (X0 @ (^[X10 : $i, X11 : $i, X12 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ (^[X10 : ($i > $i > $i)] : (c_Empty)))))) @ (c_Inj1 @ X7))))) @ (c_Inj0 @ (X2 @ (^[X8 : (($i > $i > $i > $i) > $i), X9 : $i] : (X9)) @ X5))))) => (! [X7 : (($i > $i) > ($i > $i) > $i),X4 : ((($i > $i) > $i) > $i),X5 : ($i > $i > ($i > $i) > $i),X6 : $i] : (((X1 @ (^[X8 : $i] : ((X7 @ (^[X9 : $i] : ((c_setsum @ X9 @ X8))) @ (^[X9 : $i] : (c_Empty))))) @ c_Empty)) = ((X7 @ (^[X8 : $i] : ((c_setsum @ (X2 @ (^[X9 : (($i > $i > $i > $i) > $i), X10 : $i] : (c_Empty)) @ (X3 @ (^[X9 : $i] : ((X2 @ (^[X10 : (($i > $i > $i > $i) > $i), X11 : $i] : (c_Empty)) @ c_Empty))) @ (^[X9 : $i] : ((X1 @ (^[X10 : $i] : (c_Empty)) @ c_Empty))))) @ (X2 @ (^[X9 : (($i > $i > $i > $i) > $i), X10 : $i] : (c_Empty)) @ (X2 @ (^[X9 : (($i > $i > $i > $i) > $i), X10 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ (X2 @ (^[X9 : (($i > $i > $i > $i) > $i), X10 : $i] : (c_Empty)) @ c_Empty)))))) @ (^[X8 : $i] : ((c_Inj1 @ (X1 @ (^[X9 : $i] : ((X7 @ (^[X10 : $i] : ((X1 @ (^[X11 : $i] : (c_Empty)) @ c_Empty))) @ (^[X10 : $i] : ((c_Inj1 @ c_Empty)))))) @ X6))))))) => (! [X6 : $i,X7 : $i,X5 : $i,X4 : ($i > (($i > $i) > $i > $i) > $i)] : (((X0 @ (^[X8 : $i, X9 : $i, X10 : $i] : (X7)) @ (^[X8 : $i] : (X6)) @ (^[X8 : ($i > $i > $i)] : (c_Empty)))) = X6) => (! [X6 : ($i > ($i > $i) > $i),X5 : $i,X7 : ($i > $i),X4 : $i] : (((X7 @ X4)) = ((X0 @ (^[X8 : $i, X9 : $i, X10 : $i] : ((X1 @ (^[X11 : $i] : ((X2 @ (^[X12 : (($i > $i > $i > $i) > $i), X13 : $i] : (X10)) @ (X2 @ (^[X12 : (($i > $i > $i > $i) > $i), X13 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ X11)))) @ (c_Inj1 @ c_Empty)))) @ (^[X8 : $i] : ((X7 @ c_Empty))) @ (^[X8 : ($i > $i > $i)] : (c_Empty))))) => c_False))))))))),
% 2.69/0.74 inference(negated_conjecture,[status(cth)],[f109])).
% 2.69/0.74 thf(f117,plain,(
% 2.69/0.74 ! [X0 : $i,X1 : $i] : (c_iff @ (c_In @ X0 @ (c_Power @ X1)) @ (c_Subq @ X0 @ X1))),
% 2.69/0.74 inference(rectify,[],[f7])).
% 2.69/0.74 thf(f118,plain,(
% 2.69/0.74 ! [X0 : $i,X1 : $i] : (((c_iff @ (c_In @ X0 @ (c_Power @ X1)) @ (c_Subq @ X0 @ X1))) = $true)),
% 2.69/0.74 inference(fool_elimination,[],[f117])).
% 2.69/0.74 thf(f168,plain,(
% 2.69/0.74 ((^[X0 : $i, X1 : $i] : (! [X2 : $i] : ((c_In @ X2 @ X0) => (c_In @ X2 @ X1)))) = c_Subq)),
% 2.69/0.74 inference(rectify,[],[f17])).
% 2.69/0.74 thf(f169,plain,(
% 2.69/0.74 (c_Subq = (^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))))),
% 2.69/0.74 inference(fool_elimination,[],[f168])).
% 2.69/0.74 thf(f170,plain,(
% 2.69/0.74 (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 2.69/0.74 inference(rectify,[],[f5])).
% 2.69/0.74 thf(f171,plain,(
% 2.69/0.74 (((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))) = $true)),
% 2.69/0.74 inference(fool_elimination,[],[f170])).
% 2.69/0.74 thf(f181,plain,(
% 2.69/0.74 ~ ! [X0 : (((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i),X1 : (($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i),X2 : (($i > $i) > ($i > $i) > $i),X3 : (($i > $i) > $i > $i)] : ((((c_Inj1 @ c_Empty)) = ((X2 @ (^[X8 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X9 : $i] : ((c_setsum @ c_Empty @ c_Empty)))))) => (! [X10 : $i,X13 : $i] : (((c_setsum @ (X0 @ (^[X14 : (($i > $i > $i > $i) > $i), X15 : $i] : (c_Empty)) @ (X1 @ (^[X16 : $i, X17 : $i, X18 : $i] : ((X2 @ (^[X19 : $i] : (X18)) @ (^[X20 : $i] : (c_Empty))))) @ (^[X21 : $i] : (c_Empty)) @ (^[X22 : ($i > $i > $i)] : (c_Empty)))) @ c_Empty)) = ((X2 @ (^[X23 : $i] : (X13)) @ (^[X24 : $i] : (X10))))) => (! [X27 : $i] : (X27 = ((X0 @ (^[X29 : (($i > $i > $i > $i) > $i), X30 : $i] : (X27)) @ c_Empty))) => (! [X31 : ($i > $i),X32 : ($i > $i),X33 : ($i > ($i > $i > $i) > $i)] : (((X0 @ (^[X35 : (($i > $i > $i > $i) > $i), X36 : $i] : ((X31 @ (X0 @ (^[X37 : (($i > $i > $i > $i) > $i), X38 : $i] : ((X1 @ (^[X39 : $i, X40 : $i, X41 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X42 : $i] : ((c_Inj0 @ c_Empty))) @ (^[X43 : ($i > $i > $i)] : ((X2 @ (^[X44 : $i] : (c_Empty)) @ (^[X45 : $i] : (c_Empty)))))))) @ (c_Inj0 @ (X1 @ (^[X46 : $i, X47 : $i, X48 : $i] : (c_Empty)) @ (^[X49 : $i] : (c_Empty)) @ (^[X50 : ($i > $i > $i)] : (c_Empty)))))))) @ (X2 @ (^[X51 : $i] : ((c_setsum @ X51 @ c_Empty))) @ (^[X52 : $i] : (c_Empty))))) = ((c_setsum @ (X31 @ (X32 @ (X1 @ (^[X53 : $i, X54 : $i, X55 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X56 : $i] : ((X1 @ (^[X57 : $i, X58 : $i, X59 : $i] : (c_Empty)) @ (^[X60 : $i] : (c_Empty)) @ (^[X61 : ($i > $i > $i)] : (c_Empty))))) @ (^[X62 : ($i > $i > $i)] : ((c_setsum @ c_Empty @ c_Empty)))))) @ (X3 @ (^[X63 : $i] : ((X31 @ c_Empty))) @ (X32 @ (X33 @ (X3 @ (^[X64 : $i] : (c_Empty)) @ c_Empty) @ (^[X65 : $i, X66 : $i] : (c_Empty)))))))) => (! [X67 : $i,X68 : $i] : (((c_Inj0 @ (X0 @ (^[X71 : (($i > $i > $i > $i) > $i), X72 : $i] : (X67)) @ (c_setsum @ c_Empty @ c_Empty)))) = ((X3 @ (^[X73 : $i] : ((c_Inj1 @ (X3 @ (^[X74 : $i] : ((c_Inj0 @ (X1 @ (^[X75 : $i, X76 : $i, X77 : $i] : (c_Empty)) @ (^[X78 : $i] : (c_Empty)) @ (^[X79 : ($i > $i > $i)] : (c_Empty)))))) @ (c_Inj1 @ X67))))) @ (c_Inj0 @ (X0 @ (^[X80 : (($i > $i > $i > $i) > $i), X81 : $i] : (X81)) @ X68))))) => (! [X82 : (($i > $i) > ($i > $i) > $i),X85 : $i] : (((X3 @ (^[X86 : $i] : ((X82 @ (^[X87 : $i] : ((c_setsum @ X87 @ X86))) @ (^[X88 : $i] : (c_Empty))))) @ c_Empty)) = ((X82 @ (^[X89 : $i] : ((c_setsum @ (X0 @ (^[X90 : (($i > $i > $i > $i) > $i), X91 : $i] : (c_Empty)) @ (X2 @ (^[X92 : $i] : ((X0 @ (^[X93 : (($i > $i > $i > $i) > $i), X94 : $i] : (c_Empty)) @ c_Empty))) @ (^[X95 : $i] : ((X3 @ (^[X96 : $i] : (c_Empty)) @ c_Empty))))) @ (X0 @ (^[X97 : (($i > $i > $i > $i) > $i), X98 : $i] : (c_Empty)) @ (X0 @ (^[X99 : (($i > $i > $i > $i) > $i), X100 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ (X0 @ (^[X101 : (($i > $i > $i > $i) > $i), X102 : $i] : (c_Empty)) @ c_Empty)))))) @ (^[X103 : $i] : ((c_Inj1 @ (X3 @ (^[X104 : $i] : ((X82 @ (^[X105 : $i] : ((X3 @ (^[X106 : $i] : (c_Empty)) @ c_Empty))) @ (^[X107 : $i] : ((c_Inj1 @ c_Empty)))))) @ X85))))))) => (! [X108 : $i,X109 : $i] : (((X1 @ (^[X112 : $i, X113 : $i, X114 : $i] : (X109)) @ (^[X115 : $i] : (X108)) @ (^[X116 : ($i > $i > $i)] : (c_Empty)))) = X108) => (! [X119 : ($i > $i),X120 : $i] : (((X119 @ X120)) = ((X1 @ (^[X121 : $i, X122 : $i, X123 : $i] : ((X3 @ (^[X124 : $i] : ((X0 @ (^[X125 : (($i > $i > $i > $i) > $i), X126 : $i] : (X123)) @ (X0 @ (^[X127 : (($i > $i > $i > $i) > $i), X128 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ X124)))) @ (c_Inj1 @ c_Empty)))) @ (^[X129 : $i] : ((X119 @ c_Empty))) @ (^[X130 : ($i > $i > $i)] : (c_Empty))))) => c_False))))))))),
% 2.69/0.74 inference(rectify,[],[f110])).
% 2.69/0.74 thf(f182,plain,(
% 2.69/0.74 ~ ! [X0 : (((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i),X1 : (($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i),X2 : (($i > $i) > ($i > $i) > $i),X3 : (($i > $i) > $i > $i)] : ((((c_Inj1 @ c_Empty)) = ((X2 @ (^[Y0 : $i]: (c_Inj1 @ c_Empty)) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ c_Empty))))) => (! [X10 : $i,X13 : $i] : (((X2 @ (^[Y0 : $i]: (X13)) @ (^[Y0 : $i]: (X10)))) = ((c_setsum @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (c_Empty)))) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X2 @ (^[Y3 : $i]: (Y2)) @ (^[Y3 : $i]: (c_Empty)))))))) @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) @ c_Empty))) => (! [X27 : $i] : (((X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X27)))) @ c_Empty)) = X27) => (! [X31 : ($i > $i),X32 : ($i > $i),X33 : ($i > ($i > $i > $i) > $i)] : (((X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X31 @ (X0 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (X1 @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y4 : $i]: (c_Inj0 @ c_Empty)) @ (^[Y4 : $i > $i > $i]: (X2 @ (^[Y5 : $i]: (c_Empty)) @ (^[Y5 : $i]: (c_Empty)))))))) @ (c_Inj0 @ (X1 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))))))) @ (X2 @ (^[Y0 : $i]: (c_setsum @ Y0 @ c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) = ((c_setsum @ (X31 @ (X32 @ (X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y0 : $i]: (X1 @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Empty)) @ (^[Y1 : $i > $i > $i]: (c_Empty)))) @ (^[Y0 : $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty))))) @ (X3 @ (^[Y0 : $i]: (X31 @ c_Empty)) @ (X32 @ (X33 @ (X3 @ (^[Y0 : $i]: (c_Empty)) @ c_Empty) @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))))))))) => (! [X67 : $i,X68 : $i] : (((X3 @ (^[Y0 : $i]: (c_Inj1 @ (X3 @ (^[Y1 : $i]: (c_Inj0 @ (X1 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))) @ (c_Inj1 @ X67)))) @ (c_Inj0 @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (Y1)))) @ X68)))) = ((c_Inj0 @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X67)))) @ (c_setsum @ c_Empty @ c_Empty))))) => (! [X82 : (($i > $i) > ($i > $i) > $i),X85 : $i] : (((X82 @ (^[Y0 : $i]: (c_setsum @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: (X0 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty)) @ (^[Y1 : $i]: (X3 @ (^[Y2 : $i]: (c_Empty)) @ c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ c_Empty))))) @ (^[Y0 : $i]: (c_Inj1 @ (X3 @ (^[Y1 : $i]: (X82 @ (^[Y2 : $i]: (X3 @ (^[Y3 : $i]: (c_Empty)) @ c_Empty)) @ (^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ X85))))) = ((X3 @ (^[Y0 : $i]: (X82 @ (^[Y1 : $i]: (c_setsum @ Y1 @ Y0)) @ (^[Y1 : $i]: (c_Empty)))) @ c_Empty))) => (! [X108 : $i,X109 : $i] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X109)))))) @ (^[Y0 : $i]: (X108)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) = X108) => (! [X119 : ($i > $i),X120 : $i] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X3 @ (^[Y3 : $i]: (X0 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (Y2)))) @ (X0 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ Y3))) @ (c_Inj1 @ c_Empty))))))) @ (^[Y0 : $i]: (X119 @ c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) = ((X119 @ X120))) => (c_False = $true)))))))))),
% 2.69/0.74 inference(fool_elimination,[],[f181])).
% 2.69/0.74 thf(f222,plain,(
% 2.69/0.74 ! [X0 : $o] : ((c_not @ (c_not @ X0)) => X0)),
% 2.69/0.74 inference(rectify,[],[f2])).
% 2.69/0.74 thf(f223,plain,(
% 2.69/0.74 ! [X0 : $o] : ((((c_not @ (c_not @ X0))) = $true) => ($true = X0))),
% 2.69/0.74 inference(fool_elimination,[],[f222])).
% 2.69/0.74 thf(f234,plain,(
% 2.69/0.74 ((^[X0 : $o] : (X0 => c_False)) = c_not)),
% 2.69/0.74 inference(rectify,[],[f13])).
% 2.69/0.74 thf(f235,plain,(
% 2.69/0.74 (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 2.69/0.74 inference(fool_elimination,[],[f234])).
% 2.69/0.74 thf(f285,plain,(
% 2.69/0.74 ! [X0 : $o,X1 : $o] : ((c_iff @ X1 @ X0) => (X0 = X1))),
% 2.69/0.74 inference(rectify,[],[f3])).
% 2.69/0.74 thf(f286,plain,(
% 2.69/0.74 ! [X0 : $o,X1 : $o] : ((((c_iff @ X1 @ X0)) = $true) => (X0 = X1))),
% 2.69/0.74 inference(fool_elimination,[],[f285])).
% 2.69/0.74 thf(f309,plain,(
% 2.69/0.74 ~ ! [X2 : (($i > $i) > ($i > $i) > $i),X1 : (($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i),X3 : (($i > $i) > $i > $i),X0 : (((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i)] : ((((c_Inj1 @ c_Empty)) = ((X2 @ (^[Y0 : $i]: (c_Inj1 @ c_Empty)) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ c_Empty))))) => (! [X5 : $i,X4 : $i] : (((X2 @ (^[Y0 : $i]: (X5)) @ (^[Y0 : $i]: (X4)))) = ((c_setsum @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (c_Empty)))) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X2 @ (^[Y3 : $i]: (Y2)) @ (^[Y3 : $i]: (c_Empty)))))))) @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) @ c_Empty))) => (! [X6 : $i] : (((X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X6)))) @ c_Empty)) = X6) => (! [X7 : ($i > $i),X8 : ($i > $i),X9 : ($i > ($i > $i > $i) > $i)] : (((X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X7 @ (X0 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (X1 @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y4 : $i]: (c_Inj0 @ c_Empty)) @ (^[Y4 : $i > $i > $i]: (X2 @ (^[Y5 : $i]: (c_Empty)) @ (^[Y5 : $i]: (c_Empty)))))))) @ (c_Inj0 @ (X1 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))))))) @ (X2 @ (^[Y0 : $i]: (c_setsum @ Y0 @ c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) = ((c_setsum @ (X7 @ (X8 @ (X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y0 : $i]: (X1 @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Empty)) @ (^[Y1 : $i > $i > $i]: (c_Empty)))) @ (^[Y0 : $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty))))) @ (X3 @ (^[Y0 : $i]: (X7 @ c_Empty)) @ (X8 @ (X9 @ (X3 @ (^[Y0 : $i]: (c_Empty)) @ c_Empty) @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))))))))) => (! [X11 : $i,X10 : $i] : (((X3 @ (^[Y0 : $i]: (c_Inj1 @ (X3 @ (^[Y1 : $i]: (c_Inj0 @ (X1 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))) @ (c_Inj1 @ X10)))) @ (c_Inj0 @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (Y1)))) @ X11)))) = ((c_Inj0 @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X10)))) @ (c_setsum @ c_Empty @ c_Empty))))) => (! [X12 : (($i > $i) > ($i > $i) > $i),X13 : $i] : (((X12 @ (^[Y0 : $i]: (c_setsum @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: (X0 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty)) @ (^[Y1 : $i]: (X3 @ (^[Y2 : $i]: (c_Empty)) @ c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ c_Empty))))) @ (^[Y0 : $i]: (c_Inj1 @ (X3 @ (^[Y1 : $i]: (X12 @ (^[Y2 : $i]: (X3 @ (^[Y3 : $i]: (c_Empty)) @ c_Empty)) @ (^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ X13))))) = ((X3 @ (^[Y0 : $i]: (X12 @ (^[Y1 : $i]: (c_setsum @ Y1 @ Y0)) @ (^[Y1 : $i]: (c_Empty)))) @ c_Empty))) => (! [X15 : $i,X14 : $i] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X15)))))) @ (^[Y0 : $i]: (X14)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) = X14) => (! [X17 : $i,X16 : ($i > $i)] : (((X16 @ X17)) = ((X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X3 @ (^[Y3 : $i]: (X0 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (Y2)))) @ (X0 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ Y3))) @ (c_Inj1 @ c_Empty))))))) @ (^[Y0 : $i]: (X16 @ c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty))))) => (c_False = $true)))))))))),
% 2.69/0.74 inference(rectify,[],[f182])).
% 2.69/0.74 thf(f310,plain,(
% 2.69/0.74 ! [X0 : $o] : ((((c_not @ (c_not @ X0))) != $true) | ($true = X0))),
% 2.69/0.74 inference(ennf_transformation,[],[f223])).
% 2.69/0.74 thf(f316,plain,(
% 2.69/0.74 ? [X2 : (($i > $i) > ($i > $i) > $i),X1 : (($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i),X3 : (($i > $i) > $i > $i),X0 : (((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i)] : (((((((((c_False != $true) & ! [X17 : $i,X16 : ($i > $i)] : (((X16 @ X17)) = ((X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X3 @ (^[Y3 : $i]: (X0 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (Y2)))) @ (X0 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ Y3))) @ (c_Inj1 @ c_Empty))))))) @ (^[Y0 : $i]: (X16 @ c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))))) & ! [X15 : $i,X14 : $i] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X15)))))) @ (^[Y0 : $i]: (X14)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) = X14)) & ! [X12 : (($i > $i) > ($i > $i) > $i),X13 : $i] : (((X12 @ (^[Y0 : $i]: (c_setsum @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: (X0 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty)) @ (^[Y1 : $i]: (X3 @ (^[Y2 : $i]: (c_Empty)) @ c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ c_Empty))))) @ (^[Y0 : $i]: (c_Inj1 @ (X3 @ (^[Y1 : $i]: (X12 @ (^[Y2 : $i]: (X3 @ (^[Y3 : $i]: (c_Empty)) @ c_Empty)) @ (^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ X13))))) = ((X3 @ (^[Y0 : $i]: (X12 @ (^[Y1 : $i]: (c_setsum @ Y1 @ Y0)) @ (^[Y1 : $i]: (c_Empty)))) @ c_Empty)))) & ! [X11 : $i,X10 : $i] : (((X3 @ (^[Y0 : $i]: (c_Inj1 @ (X3 @ (^[Y1 : $i]: (c_Inj0 @ (X1 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))) @ (c_Inj1 @ X10)))) @ (c_Inj0 @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (Y1)))) @ X11)))) = ((c_Inj0 @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X10)))) @ (c_setsum @ c_Empty @ c_Empty)))))) & ! [X7 : ($i > $i),X8 : ($i > $i),X9 : ($i > ($i > $i > $i) > $i)] : (((X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X7 @ (X0 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (X1 @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y4 : $i]: (c_Inj0 @ c_Empty)) @ (^[Y4 : $i > $i > $i]: (X2 @ (^[Y5 : $i]: (c_Empty)) @ (^[Y5 : $i]: (c_Empty)))))))) @ (c_Inj0 @ (X1 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))))))) @ (X2 @ (^[Y0 : $i]: (c_setsum @ Y0 @ c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) = ((c_setsum @ (X7 @ (X8 @ (X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y0 : $i]: (X1 @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Empty)) @ (^[Y1 : $i > $i > $i]: (c_Empty)))) @ (^[Y0 : $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty))))) @ (X3 @ (^[Y0 : $i]: (X7 @ c_Empty)) @ (X8 @ (X9 @ (X3 @ (^[Y0 : $i]: (c_Empty)) @ c_Empty) @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty))))))))))) & ! [X6 : $i] : (((X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X6)))) @ c_Empty)) = X6)) & ! [X5 : $i,X4 : $i] : (((X2 @ (^[Y0 : $i]: (X5)) @ (^[Y0 : $i]: (X4)))) = ((c_setsum @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (c_Empty)))) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X2 @ (^[Y3 : $i]: (Y2)) @ (^[Y3 : $i]: (c_Empty)))))))) @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) @ c_Empty)))) & (((c_Inj1 @ c_Empty)) = ((X2 @ (^[Y0 : $i]: (c_Inj1 @ c_Empty)) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ c_Empty))))))),
% 2.69/0.74 inference(ennf_transformation,[],[f309])).
% 2.69/0.74 thf(f317,plain,(
% 2.69/0.74 ? [X3 : (($i > $i) > $i > $i),X2 : (($i > $i) > ($i > $i) > $i),X1 : (($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i),X0 : (((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i)] : (! [X7 : ($i > $i),X8 : ($i > $i),X9 : ($i > ($i > $i > $i) > $i)] : (((X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X7 @ (X0 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (X1 @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y4 : $i]: (c_Inj0 @ c_Empty)) @ (^[Y4 : $i > $i > $i]: (X2 @ (^[Y5 : $i]: (c_Empty)) @ (^[Y5 : $i]: (c_Empty)))))))) @ (c_Inj0 @ (X1 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))))))) @ (X2 @ (^[Y0 : $i]: (c_setsum @ Y0 @ c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) = ((c_setsum @ (X7 @ (X8 @ (X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y0 : $i]: (X1 @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Empty)) @ (^[Y1 : $i > $i > $i]: (c_Empty)))) @ (^[Y0 : $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty))))) @ (X3 @ (^[Y0 : $i]: (X7 @ c_Empty)) @ (X8 @ (X9 @ (X3 @ (^[Y0 : $i]: (c_Empty)) @ c_Empty) @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))))))))) & ! [X12 : (($i > $i) > ($i > $i) > $i),X13 : $i] : (((X12 @ (^[Y0 : $i]: (c_setsum @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: (X0 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty)) @ (^[Y1 : $i]: (X3 @ (^[Y2 : $i]: (c_Empty)) @ c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (X0 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ c_Empty))))) @ (^[Y0 : $i]: (c_Inj1 @ (X3 @ (^[Y1 : $i]: (X12 @ (^[Y2 : $i]: (X3 @ (^[Y3 : $i]: (c_Empty)) @ c_Empty)) @ (^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ X13))))) = ((X3 @ (^[Y0 : $i]: (X12 @ (^[Y1 : $i]: (c_setsum @ Y1 @ Y0)) @ (^[Y1 : $i]: (c_Empty)))) @ c_Empty))) & ! [X15 : $i,X14 : $i] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X15)))))) @ (^[Y0 : $i]: (X14)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) = X14) & ! [X6 : $i] : (((X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X6)))) @ c_Empty)) = X6) & ! [X5 : $i,X4 : $i] : (((X2 @ (^[Y0 : $i]: (X5)) @ (^[Y0 : $i]: (X4)))) = ((c_setsum @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (c_Empty)))) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X2 @ (^[Y3 : $i]: (Y2)) @ (^[Y3 : $i]: (c_Empty)))))))) @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) @ c_Empty))) & ! [X11 : $i,X10 : $i] : (((X3 @ (^[Y0 : $i]: (c_Inj1 @ (X3 @ (^[Y1 : $i]: (c_Inj0 @ (X1 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))) @ (c_Inj1 @ X10)))) @ (c_Inj0 @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (Y1)))) @ X11)))) = ((c_Inj0 @ (X0 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X10)))) @ (c_setsum @ c_Empty @ c_Empty))))) & (((c_Inj1 @ c_Empty)) = ((X2 @ (^[Y0 : $i]: (c_Inj1 @ c_Empty)) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ c_Empty))))) & (c_False != $true) & ! [X17 : $i,X16 : ($i > $i)] : (((X16 @ X17)) = ((X1 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X3 @ (^[Y3 : $i]: (X0 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (Y2)))) @ (X0 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ Y3))) @ (c_Inj1 @ c_Empty))))))) @ (^[Y0 : $i]: (X16 @ c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty))))))),
% 2.69/0.74 inference(flattening,[],[f316])).
% 2.69/0.74 thf(f318,plain,(
% 2.69/0.74 ! [X0 : $o,X1 : $o] : ((((c_iff @ X1 @ X0)) != $true) | (X0 = X1))),
% 2.69/0.74 inference(ennf_transformation,[],[f286])).
% 2.69/0.74 thf(f321,definition,(
% 2.69/0.74 ! [X0 : ($i > $o)] : (? [X1 : $i] : (? [X2 : $i] : ((((X0 @ X2)) != $true) & (((c_In @ X2 @ X1)) = $true)) & (((X0 @ X1)) = $true)) | ~ (((sP1 @ X0)) = $true))),
% 2.69/0.74 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 2.69/0.74 thf(f323,plain,(
% 2.69/0.74 ? [X0 : (($i > $i) > $i > $i),X1 : (($i > $i) > ($i > $i) > $i),X2 : (($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i),X3 : (((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i)] : (! [X4 : ($i > $i),X5 : ($i > $i),X6 : ($i > ($i > $i > $i) > $i)] : (((X3 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X4 @ (X3 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (X2 @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y4 : $i]: (c_Inj0 @ c_Empty)) @ (^[Y4 : $i > $i > $i]: (X1 @ (^[Y5 : $i]: (c_Empty)) @ (^[Y5 : $i]: (c_Empty)))))))) @ (c_Inj0 @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))))))) @ (X1 @ (^[Y0 : $i]: (c_setsum @ Y0 @ c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) = ((c_setsum @ (X4 @ (X5 @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y0 : $i]: (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Empty)) @ (^[Y1 : $i > $i > $i]: (c_Empty)))) @ (^[Y0 : $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty))))) @ (X0 @ (^[Y0 : $i]: (X4 @ c_Empty)) @ (X5 @ (X6 @ (X0 @ (^[Y0 : $i]: (c_Empty)) @ c_Empty) @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))))))))) & ! [X7 : (($i > $i) > ($i > $i) > $i),X8 : $i] : (((X0 @ (^[Y0 : $i]: (X7 @ (^[Y1 : $i]: (c_setsum @ Y1 @ Y0)) @ (^[Y1 : $i]: (c_Empty)))) @ c_Empty)) = ((X7 @ (^[Y0 : $i]: (c_setsum @ (X3 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (X1 @ (^[Y1 : $i]: (X3 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty)) @ (^[Y1 : $i]: (X0 @ (^[Y2 : $i]: (c_Empty)) @ c_Empty)))) @ (X3 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (X3 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (X3 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ c_Empty))))) @ (^[Y0 : $i]: (c_Inj1 @ (X0 @ (^[Y1 : $i]: (X7 @ (^[Y2 : $i]: (X0 @ (^[Y3 : $i]: (c_Empty)) @ c_Empty)) @ (^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ X8)))))) & ! [X9 : $i,X10 : $i] : (((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X9)))))) @ (^[Y0 : $i]: (X10)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) = X10) & ! [X11 : $i] : (((X3 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X11)))) @ c_Empty)) = X11) & ! [X12 : $i,X13 : $i] : (((X1 @ (^[Y0 : $i]: (X12)) @ (^[Y0 : $i]: (X13)))) = ((c_setsum @ (X3 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (c_Empty)))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X1 @ (^[Y3 : $i]: (Y2)) @ (^[Y3 : $i]: (c_Empty)))))))) @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) @ c_Empty))) & ! [X14 : $i,X15 : $i] : (((X0 @ (^[Y0 : $i]: (c_Inj1 @ (X0 @ (^[Y1 : $i]: (c_Inj0 @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))) @ (c_Inj1 @ X15)))) @ (c_Inj0 @ (X3 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (Y1)))) @ X14)))) = ((c_Inj0 @ (X3 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X15)))) @ (c_setsum @ c_Empty @ c_Empty))))) & (((c_Inj1 @ c_Empty)) = ((X1 @ (^[Y0 : $i]: (c_Inj1 @ c_Empty)) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ c_Empty))))) & (c_False != $true) & ! [X16 : $i,X17 : ($i > $i)] : (((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X0 @ (^[Y3 : $i]: (X3 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (Y2)))) @ (X3 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ Y3))) @ (c_Inj1 @ c_Empty))))))) @ (^[Y0 : $i]: (X17 @ c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) = ((X17 @ X16))))),
% 2.69/0.74 inference(rectify,[],[f317])).
% 2.69/0.74 thf(f324,plain,(
% 2.69/0.74 ! [X4 : ($i > $i),X5 : ($i > $i),X6 : ($i > ($i > $i > $i) > $i)] : (((sK5 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X4 @ (sK5 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (sK4 @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y4 : $i]: (c_Inj0 @ c_Empty)) @ (^[Y4 : $i > $i > $i]: (sK3 @ (^[Y5 : $i]: (c_Empty)) @ (^[Y5 : $i]: (c_Empty)))))))) @ (c_Inj0 @ (sK4 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))))))) @ (sK3 @ (^[Y0 : $i]: (c_setsum @ Y0 @ c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) = ((c_setsum @ (X4 @ (X5 @ (sK4 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))))) @ (^[Y0 : $i]: (sK4 @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Empty)) @ (^[Y1 : $i > $i > $i]: (c_Empty)))) @ (^[Y0 : $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty))))) @ (sK2 @ (^[Y0 : $i]: (X4 @ c_Empty)) @ (X5 @ (X6 @ (sK2 @ (^[Y0 : $i]: (c_Empty)) @ c_Empty) @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))))))))) & ! [X7 : (($i > $i) > ($i > $i) > $i),X8 : $i] : (((sK2 @ (^[Y0 : $i]: (X7 @ (^[Y1 : $i]: (c_setsum @ Y1 @ Y0)) @ (^[Y1 : $i]: (c_Empty)))) @ c_Empty)) = ((X7 @ (^[Y0 : $i]: (c_setsum @ (sK5 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (sK3 @ (^[Y1 : $i]: (sK5 @ (^[Y2 : ($i > $i > $i > $i) > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty)) @ (^[Y1 : $i]: (sK2 @ (^[Y2 : $i]: (c_Empty)) @ c_Empty)))) @ (sK5 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ (sK5 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (sK5 @ (^[Y1 : ($i > $i > $i > $i) > $i]: ((^[Y2 : $i]: (c_Empty)))) @ c_Empty))))) @ (^[Y0 : $i]: (c_Inj1 @ (sK2 @ (^[Y1 : $i]: (X7 @ (^[Y2 : $i]: (sK2 @ (^[Y3 : $i]: (c_Empty)) @ c_Empty)) @ (^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ X8)))))) & ! [X9 : $i,X10 : $i] : (((sK4 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (X9)))))) @ (^[Y0 : $i]: (X10)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) = X10) & ! [X11 : $i] : (((sK5 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X11)))) @ c_Empty)) = X11) & ! [X12 : $i,X13 : $i] : (((sK3 @ (^[Y0 : $i]: (X12)) @ (^[Y0 : $i]: (X13)))) = ((c_setsum @ (sK5 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (c_Empty)))) @ (sK4 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (sK3 @ (^[Y3 : $i]: (Y2)) @ (^[Y3 : $i]: (c_Empty)))))))) @ (^[Y0 : $i]: (c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))) @ c_Empty))) & ! [X14 : $i,X15 : $i] : (((sK2 @ (^[Y0 : $i]: (c_Inj1 @ (sK2 @ (^[Y1 : $i]: (c_Inj0 @ (sK4 @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))))) @ (^[Y2 : $i]: (c_Empty)) @ (^[Y2 : $i > $i > $i]: (c_Empty))))) @ (c_Inj1 @ X15)))) @ (c_Inj0 @ (sK5 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (Y1)))) @ X14)))) = ((c_Inj0 @ (sK5 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X15)))) @ (c_setsum @ c_Empty @ c_Empty))))) & (((c_Inj1 @ c_Empty)) = ((sK3 @ (^[Y0 : $i]: (c_Inj1 @ c_Empty)) @ (^[Y0 : $i]: (c_setsum @ c_Empty @ c_Empty))))) & (c_False != $true) & ! [X16 : $i,X17 : ($i > $i)] : (((X17 @ X16)) = ((sK4 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (sK2 @ (^[Y3 : $i]: (sK5 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (Y2)))) @ (sK5 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ Y3))) @ (c_Inj1 @ c_Empty))))))) @ (^[Y0 : $i]: (X17 @ c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))))),
% 2.69/0.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5)],[f323])).
% 2.69/0.74 thf(f326,plain,(
% 2.69/0.74 ! [X0 : ($i > $o)] : (? [X1 : $i] : (? [X2 : $i] : ((((X0 @ X2)) != $true) & (((c_In @ X2 @ X1)) = $true)) & (((X0 @ X1)) = $true)) | (((sP1 @ X0)) != $true))),
% 2.69/0.74 inference(nnf_transformation,[],[f321])).
% 2.69/0.74 thf(f327,plain,(
% 2.69/0.74 ! [X0 : ($i > $o)] : (((($true != ((X0 @ (sK7 @ X0)))) & ($true = ((c_In @ (sK7 @ X0) @ (sK6 @ X0))))) & (((X0 @ (sK6 @ X0))) = $true)) | (((sP1 @ X0)) != $true))),
% 2.69/0.74 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X2,sK7 @ X0),skolemize(X2,sK7 @ X0)],[f326])).
% 2.69/0.74 thf(f357,plain,(
% 2.69/0.74 ( ! [X16 : $i,X17 : ($i > $i)] : ((((X17 @ X16)) = ((sK4 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (sK2 @ (^[Y3 : $i]: (sK5 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (Y2)))) @ (sK5 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (c_setsum @ c_Empty @ c_Empty)))) @ Y3))) @ (c_Inj1 @ c_Empty))))))) @ (^[Y0 : $i]: (X17 @ c_Empty)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))))) )),
% 2.69/0.74 inference(cnf_transformation,[],[f324])).
% 2.69/0.74 thf(f362,plain,(
% 2.69/0.74 ( ! [X11 : $i] : ((((sK5 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X11)))) @ c_Empty)) = X11)) )),
% 2.69/0.74 inference(cnf_transformation,[],[f324])).
% 2.69/0.74 thf(f401,plain,(
% 2.69/0.74 (((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))) = $true)),
% 2.69/0.74 inference(cnf_transformation,[],[f171])).
% 2.69/0.74 thf(f414,plain,(
% 2.69/0.74 (c_Subq = (^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))))),
% 2.69/0.74 inference(cnf_transformation,[],[f169])).
% 2.69/0.74 thf(f421,plain,(
% 2.69/0.74 (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 2.69/0.74 inference(cnf_transformation,[],[f235])).
% 2.69/0.74 thf(f429,plain,(
% 2.69/0.74 ( ! [X0 : $o,X1 : $o] : ((X0 = X1) | (((c_iff @ X1 @ X0)) != $true)) )),
% 2.69/0.74 inference(cnf_transformation,[],[f318])).
% 2.69/0.74 thf(f432,plain,(
% 2.69/0.74 ( ! [X0 : ($i > $o)] : (($true != ((X0 @ (sK7 @ X0)))) | (((sP1 @ X0)) != $true)) )),
% 2.69/0.74 inference(cnf_transformation,[],[f327])).
% 2.69/0.74 thf(f445,plain,(
% 2.69/0.74 ( ! [X0 : $i,X1 : $i] : ((((c_iff @ (c_In @ X0 @ (c_Power @ X1)) @ (c_Subq @ X0 @ X1))) = $true)) )),
% 2.69/0.74 inference(cnf_transformation,[],[f118])).
% 2.69/0.74 thf(f458,plain,(
% 2.69/0.74 ( ! [X0 : $o] : ((((c_not @ (c_not @ X0))) != $true) | ($true = X0)) )),
% 2.69/0.74 inference(cnf_transformation,[],[f310])).
% 2.69/0.74 thf(f464,definition,(
% 2.69/0.74 (sF13 = ((c_Inj1 @ c_Empty)))),
% 2.69/0.74 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 2.69/0.74 thf(f465,plain,(
% 2.69/0.74 (((c_Inj1 @ c_Empty)) = sF13)),
% 2.69/0.74 inference(reorient_equations,[],[f464])).
% 2.69/0.74 thf(f479,definition,(
% 2.69/0.74 (sF23 = ((c_setsum @ c_Empty @ c_Empty)))),
% 2.69/0.74 introduced(definition,[new_symbols(definition,[sF23])],[function_definition])).
% 2.69/0.74 thf(f480,plain,(
% 2.69/0.74 (((c_setsum @ c_Empty @ c_Empty)) = sF23)),
% 2.69/0.74 inference(reorient_equations,[],[f479])).
% 2.69/0.74 thf(f485,definition,(
% 2.69/0.74 ( ! [X4 : ($i > $i)] : ((((sF27 @ X4)) = ((X4 @ c_Empty)))) )),
% 2.69/0.74 introduced(definition,[new_symbols(definition,[sF27])],[function_definition])).
% 2.69/0.74 thf(f512,definition,(
% 2.69/0.74 ( ! [X11 : $i] : ((((sF45 @ X11)) = ((sK5 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X11)))) @ c_Empty)))) )),
% 2.69/0.74 introduced(definition,[new_symbols(definition,[sF45])],[function_definition])).
% 2.69/0.74 thf(f513,plain,(
% 2.69/0.74 ( ! [X11 : $i] : ((((sK5 @ (^[Y0 : ($i > $i > $i > $i) > $i]: ((^[Y1 : $i]: (X11)))) @ c_Empty)) = ((sF45 @ X11)))) )),
% 2.69/0.74 inference(reorient_equations,[],[f512])).
% 2.69/0.74 thf(f514,plain,(
% 2.69/0.74 ( ! [X11 : $i] : ((((sF45 @ X11)) = X11)) )),
% 2.69/0.74 inference(definition_folding,[],[f362,f513])).
% 2.69/0.74 thf(f536,definition,(
% 2.69/0.74 ( ! [X16 : $i,X17 : ($i > $i)] : ((((sF59 @ X16 @ X17)) = ((X17 @ X16)))) )),
% 2.69/0.74 introduced(definition,[new_symbols(definition,[sF59])],[function_definition])).
% 2.69/0.74 thf(f537,plain,(
% 2.69/0.74 ( ! [X16 : $i,X17 : ($i > $i)] : ((((X17 @ X16)) = ((sF59 @ X16 @ X17)))) )),
% 2.69/0.74 inference(reorient_equations,[],[f536])).
% 2.69/0.74 thf(f538,definition,(
% 2.69/0.74 ( ! [X17 : ($i > $i)] : ((((sF60 @ X17)) = ((sK4 @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (sK2 @ (^[Y3 : $i]: (sK5 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (Y2)))) @ (sK5 @ (^[Y4 : ($i > $i > $i > $i) > $i]: ((^[Y5 : $i]: (sF23)))) @ Y3))) @ sF13)))))) @ (^[Y0 : $i]: (sF27 @ X17)) @ (^[Y0 : $i > $i > $i]: (c_Empty)))))) )),
% 2.69/0.74 introduced(definition,[new_symbols(definition,[sF60])],[function_definition])).
% 2.69/0.74 thf(f539,plain,(
% 2.69/0.74 ( ! [X16 : $i,X17 : ($i > $i)] : ((((sF59 @ X16 @ X17)) = ((sF60 @ X17)))) )),
% 2.69/0.74 inference(definition_folding,[],[f357,f538,f485,f465,f480,f537])).
% 2.69/0.74 thf(f553,plain,(
% 2.69/0.74 ( ! [X0 : $o,X1 : $o] : ((((c_iff @ X1 @ X0)) != $true) | ($true = X1) | ($false = X0)) )),
% 2.69/0.74 inference(iff_proxy_clausification,[],[f429])).
% 2.69/0.74 thf(f582,definition,(
% 2.69/0.74 spl63_5 <=> ! [X1 : $o] : ($true = X1)),
% 2.69/0.74 introduced(definition,[new_symbols(definition,[spl63_5])],[avatar_definition])).
% 2.69/0.74 thf(f583,plain,(
% 2.69/0.74 ( ! [X1 : $o] : (($true = X1)) ) | ~spl63_5),
% 2.69/0.74 inference(avatar_component_clause,[],[f582])).
% 2.69/0.74 thf(f619,definition,(
% 2.69/0.74 spl63_9 <=> (((c_not @ $true)) = $true)),
% 2.69/0.74 introduced(definition,[new_symbols(definition,[spl63_9])],[avatar_definition])).
% 2.69/0.74 thf(f621,plain,(
% 2.69/0.74 (((c_not @ $true)) != $true) | spl63_9),
% 2.69/0.74 inference(avatar_component_clause,[],[f619])).
% 2.69/0.74 thf(f629,plain,(
% 2.69/0.74 ( ! [X1 : $o] : ((((c_not @ X1)) = (((^[Y0 : $o]: (Y0 => c_False)) @ X1)))) )),
% 2.69/0.74 inference(argument_congruence,[],[f421])).
% 2.69/0.74 thf(f630,plain,(
% 2.69/0.74 ( ! [X1 : $o] : ((((c_not @ X1)) = $true) | ((((^[Y0 : $o]: (Y0 => c_False)) @ X1)) = $false)) )),
% 2.69/0.74 inference(iff_proxy_clausification,[],[f629])).
% 2.69/0.74 thf(f634,plain,(
% 2.69/0.74 ( ! [X1 : $o] : (($false = ((X1 => c_False))) | (((c_not @ X1)) = $true)) )),
% 2.69/0.74 inference(beta-eta_normalization,[],[f630])).
% 2.69/0.74 thf(f636,plain,(
% 2.69/0.74 ( ! [X1 : $o] : ((((c_not @ X1)) = $true) | ($true = X1)) )),
% 2.69/0.74 inference(imp_proxy_clausification,[],[f634])).
% 2.69/0.74 thf(f644,plain,(
% 2.69/0.74 ( ! [X0 : $o] : (($true = X0) | ($true = X0) | (((c_not @ $true)) != $true)) )),
% 2.69/0.74 inference(constrained_superposition,[],[f458,f636])).
% 2.69/0.74 thf(f646,plain,(
% 2.69/0.74 ( ! [X0 : $o] : (($true = X0) | (((c_not @ $true)) != $true)) )),
% 2.69/0.74 inference(duplicate_literal_removal,[],[f644])).
% 2.69/0.74 thf(f658,plain,(
% 2.69/0.74 ( ! [X0 : ($i > $i),X1 : $i] : ((((sF60 @ X0)) = ((X0 @ X1)))) )),
% 2.69/0.74 inference(constrained_superposition,[],[f537,f539])).
% 2.69/0.74 thf(f672,plain,(
% 2.69/0.74 ( ! [X0 : $i] : ((((sF60 @ sF45)) = X0)) )),
% 2.69/0.74 inference(constrained_superposition,[],[f658,f514])).
% 2.69/0.74 thf(f694,plain,(
% 2.69/0.74 ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) )),
% 2.69/0.74 inference(constrained_superposition,[],[f672,f672])).
% 2.69/0.74 thf(f746,plain,(
% 2.69/0.74 ( ! [X0 : $i,X1 : ($i > $o)] : (($true != ((sP1 @ X1))) | (((X1 @ X0)) != $true)) )),
% 2.69/0.74 inference(constrained_superposition,[],[f432,f694])).
% 2.69/0.74 thf(f753,plain,(
% 2.69/0.74 (((c_not @ $true)) = $true) | (((?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty)))) = $false)),
% 2.69/0.74 inference(fool_paramodulation,[],[f401])).
% 2.69/0.74 thf(f762,plain,(
% 2.69/0.74 ( ! [X1 : $i] : ((((c_not @ $true)) = $true) | ((((^[Y0 : $i]: (c_In @ Y0 @ c_Empty)) @ X1)) = $false)) )),
% 2.69/0.74 inference(pi_proxy_clausification,[],[f753])).
% 2.69/0.74 thf(f763,plain,(
% 2.69/0.74 ( ! [X1 : $i] : ((((c_In @ X1 @ c_Empty)) = $false) | (((c_not @ $true)) = $true)) )),
% 2.69/0.74 inference(beta-eta_normalization,[],[f762])).
% 2.69/0.74 thf(f767,plain,(
% 2.69/0.74 ( ! [X1 : $i] : ((((c_In @ X1 @ c_Empty)) = $false)) ) | spl63_9),
% 2.69/0.74 inference(forward_subsumption_resolution,[],[f763,f621])).
% 2.69/0.74 thf(f768,plain,(
% 2.69/0.74 ( ! [X0 : $i,X1 : $i] : ((((c_In @ X1 @ X0)) = $false)) ) | spl63_9),
% 2.69/0.74 inference(constrained_superposition,[],[f767,f694])).
% 2.69/0.74 thf(f784,plain,(
% 2.69/0.74 ( ! [X0 : $i,X1 : $i] : (($true = ((c_iff @ $false @ (c_Subq @ X0 @ X1))))) ) | spl63_9),
% 2.69/0.74 inference(forward_demodulation,[],[f445,f768])).
% 2.69/0.74 thf(f786,plain,(
% 2.69/0.74 ( ! [X0 : $i,X1 : $i] : ((((c_Subq @ X0 @ X1)) = $false) | ($true != $true) | ($true = $false)) ) | spl63_9),
% 2.69/0.74 inference(constrained_superposition,[],[f553,f784])).
% 2.69/0.74 thf(f787,plain,(
% 2.69/0.74 ( ! [X0 : $i,X1 : $i] : ((((c_Subq @ X0 @ X1)) = $false)) ) | spl63_9),
% 2.69/0.74 inference(trivial_inequality_removal,[],[f786])).
% 2.69/0.74 thf(f793,definition,(
% 2.69/0.74 spl63_11 <=> ! [X0 : $i,X1 : $i] : (((c_Subq @ X0 @ X1)) = $false)),
% 2.69/0.74 introduced(definition,[new_symbols(definition,[spl63_11])],[avatar_definition])).
% 2.69/0.74 thf(f794,plain,(
% 2.69/0.74 ( ! [X0 : $i,X1 : $i] : ((((c_Subq @ X0 @ X1)) = $false)) ) | ~spl63_11),
% 2.69/0.74 inference(avatar_component_clause,[],[f793])).
% 2.69/0.74 thf(f796,plain,(
% 2.69/0.74 spl63_11 | spl63_9),
% 2.69/0.74 inference(avatar_split_clause,[],[f787,f619,f793])).
% 2.69/0.74 thf(f956,plain,(
% 2.69/0.74 ( ! [X1 : ($i > $o)] : (($true != $true) | ($true != ((sP1 @ X1)))) ) | ~spl63_5),
% 2.69/0.74 inference(backward_demodulation,[],[f746,f583])).
% 2.69/0.74 thf(f998,plain,(
% 2.69/0.74 ( ! [X1 : ($i > $o)] : (($true != ((sP1 @ X1)))) ) | ~spl63_5),
% 2.69/0.74 inference(trivial_inequality_removal,[],[f956])).
% 2.69/0.74 thf(f1005,plain,(
% 2.69/0.74 $false | ~spl63_5),
% 2.69/0.74 inference(forward_subsumption_resolution,[],[f998,f583])).
% 2.69/0.74 thf(f1006,plain,(
% 2.69/0.74 ~spl63_5),
% 2.69/0.74 inference(avatar_contradiction_clause,[],[f1005])).
% 2.69/0.74 thf(f1124,plain,(
% 2.69/0.74 ( ! [X1 : $i] : ((((c_Subq @ X1)) = (((^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))) @ X1)))) )),
% 2.69/0.74 inference(argument_congruence,[],[f414])).
% 2.69/0.74 thf(f1125,plain,(
% 2.69/0.74 ( ! [X1 : $i] : ((((c_Subq @ X1)) = (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X1) => (c_In @ Y1 @ Y0))))))) )),
% 2.69/0.74 inference(beta-eta_normalization,[],[f1124])).
% 2.69/0.74 thf(f1260,plain,(
% 2.69/0.74 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X1) => (c_In @ Y1 @ Y0))))) @ X2)) = ((c_Subq @ X1 @ X2)))) )),
% 2.69/0.74 inference(argument_congruence,[],[f1125])).
% 2.69/0.74 thf(f1262,plain,(
% 2.69/0.74 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X1) => (c_In @ Y1 @ Y0))))) @ X2)) = $false) | ($true = ((c_Subq @ X1 @ X2)))) )),
% 2.69/0.74 inference(iff_proxy_clausification,[],[f1260])).
% 2.69/0.74 thf(f1263,plain,(
% 2.69/0.74 ( ! [X2 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X2)))))) | ($true = ((c_Subq @ X1 @ X2)))) )),
% 2.69/0.74 inference(beta-eta_normalization,[],[f1262])).
% 2.69/0.74 thf(f1264,plain,(
% 2.69/0.74 ( ! [X2 : $i,X1 : $i] : (($true = ((c_Subq @ X1 @ X2))) | ($false = (((^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X2))) @ (sK67 @ X1 @ X2))))) )),
% 2.69/0.74 inference(sigma_proxy_clausification,[],[f1263])).
% 2.69/0.74 thf(f1265,plain,(
% 2.69/0.74 ( ! [X2 : $i,X1 : $i] : (($true = ((c_Subq @ X1 @ X2))) | ((((c_In @ (sK67 @ X1 @ X2) @ X1) => (c_In @ (sK67 @ X1 @ X2) @ X2))) = $false)) )),
% 2.69/0.74 inference(beta-eta_normalization,[],[f1264])).
% 2.69/0.74 thf(f1267,plain,(
% 2.69/0.74 ( ! [X2 : $i,X1 : $i] : (($true = ((c_Subq @ X1 @ X2))) | (((c_In @ (sK67 @ X1 @ X2) @ X1)) = $true)) )),
% 2.69/0.74 inference(imp_proxy_clausification,[],[f1265])).
% 2.69/0.74 thf(f1272,plain,(
% 2.69/0.74 ( ! [X2 : $i,X1 : $i] : (($true = ((c_Subq @ X1 @ X2))) | ($true = $false)) ) | spl63_9),
% 2.69/0.74 inference(forward_demodulation,[],[f1267,f768])).
% 2.69/0.74 thf(f1273,plain,(
% 2.69/0.74 ( ! [X2 : $i,X1 : $i] : (($true = ((c_Subq @ X1 @ X2)))) ) | spl63_9),
% 2.69/0.74 inference(trivial_inequality_removal,[],[f1272])).
% 2.69/0.74 thf(f1274,plain,(
% 2.69/0.74 ($true = $false) | (spl63_9 | ~spl63_11)),
% 2.69/0.74 inference(forward_demodulation,[],[f1273,f794])).
% 2.69/0.74 thf(f1275,plain,(
% 2.69/0.74 $false | (spl63_9 | ~spl63_11)),
% 2.69/0.74 inference(trivial_inequality_removal,[],[f1274])).
% 2.69/0.74 thf(f1276,plain,(
% 2.69/0.74 spl63_9 | ~spl63_11),
% 2.69/0.74 inference(avatar_contradiction_clause,[],[f1275])).
% 2.69/0.74 thf(f1297,plain,(
% 2.69/0.74 ~spl63_9 | spl63_5),
% 2.69/0.74 inference(avatar_split_clause,[],[f646,f582,f619])).
% 2.69/0.74 cnf(s9, plain, spl63_9 | spl63_11, inference(sat_conversion,[],[f796])).
% 2.69/0.74 cnf(s26, plain, ~spl63_5, inference(sat_conversion,[],[f1006])).
% 2.69/0.74 cnf(s27, plain, spl63_9 | ~spl63_11, inference(sat_conversion,[],[f1276])).
% 2.69/0.74 cnf(s38, plain, spl63_5 | ~spl63_9, inference(sat_conversion,[],[f1297])).
% 2.69/0.74 cnf(s39, plain, ~spl63_9, inference(rat,[],[s38,s26])).
% 2.69/0.74 cnf(s41, plain, ~spl63_11, inference(rat,[],[s27,s39])).
% 2.69/0.74 cnf(s44, plain, $false, inference(rat,[],[s9,s41,s39])).
% 2.69/0.74 thf(f1298,plain,(
% 2.69/0.74 $false),
% 2.69/0.74 inference(avatar_sat_refutation,[],[s44])).
% 2.69/0.74 % SZS output end Proof for theBenchmark
% 2.69/0.74 % (3673700)------------------------------
% 2.69/0.74 % (3673700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.74 % (3673700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.74 % (3673700)CaDiCaL version: 2.1.3
% 2.69/0.74 % (3673700)Termination reason: Refutation
% 2.69/0.74 % (3673700)Time elapsed: 0.057 s
% 2.69/0.74 % (3673700)Peak memory usage: 14 MB
% 2.69/0.74 % (3673700)Instructions burned: 110 (million)
% 2.69/0.74 % (3673594)Success in time 0.481 s
% 2.69/0.74 % Vampire exiting
%------------------------------------------------------------------------------