%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM657^4 : TPTP v9.3.1. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:18:26 AM UTC 2026
% Result : Theorem 1.20s 0.56s
% Output : Refutation 1.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM657^4 : TPTP v9.3.1. Released v7.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n010.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 12:33:03 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.23/0.27 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.55/0.41 % (2785162)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.55/0.41 % (2785185)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1390800093:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.55/0.41 % (2785192)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.55/0.41 % (2785192)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.55/0.41 % (2785186)lrs+10_16_si=on:nwc=1.5:random_seed=1481083139:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.55/0.41 % (2785192)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=3288320727:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.55/0.41 % (2785191)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1875677238:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.55/0.41 % (2785190)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=587487837:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.55/0.41 % (2785189)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=4193548646: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.55/0.41 % (2785188)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4270714217:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.55/0.41 % (2785188)Instruction limit reached!
% 0.55/0.41 % (2785188)------------------------------
% 0.55/0.41 % (2785188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.41 % (2785188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.41 % (2785188)CaDiCaL version: 2.1.3
% 0.55/0.41 % (2785188)Termination reason: Instruction limit
% 0.55/0.41 % (2785188)Termination phase: shuffling
% 0.55/0.41 % (2785188)Time elapsed: 0.003 s
% 0.55/0.41 % (2785188)Peak memory usage: 10 MB
% 0.55/0.41 % (2785188)Instructions burned: 4 (million)
% 0.55/0.41 % (2785186)Instruction limit reached!
% 0.55/0.41 % (2785186)------------------------------
% 0.55/0.41 % (2785186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.41 % (2785186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.41 % (2785186)CaDiCaL version: 2.1.3
% 0.55/0.41 % (2785186)Termination reason: Instruction limit
% 0.55/0.41 % (2785186)Termination phase: shuffling
% 0.55/0.41 % (2785186)Time elapsed: 0.009 s
% 0.55/0.41 % (2785186)Peak memory usage: 10 MB
% 0.55/0.41 % (2785186)Instructions burned: 20 (million)
% 0.55/0.41 % (2785190)Instruction limit reached!
% 0.55/0.41 % (2785190)------------------------------
% 0.55/0.41 % (2785190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.41 % (2785190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.41 % (2785190)CaDiCaL version: 2.1.3
% 0.55/0.41 % (2785190)Termination reason: Instruction limit
% 0.55/0.41 % (2785190)Termination phase: Property scanning
% 0.55/0.41 % (2785190)Time elapsed: 0.012 s
% 0.55/0.41 % (2785190)Peak memory usage: 10 MB
% 0.55/0.41 % (2785190)Instructions burned: 25 (million)
% 0.55/0.41 % (2785185)Instruction limit reached!
% 0.55/0.41 % (2785185)------------------------------
% 0.55/0.41 % (2785185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.41 % (2785185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.41 % (2785185)CaDiCaL version: 2.1.3
% 0.55/0.41 % (2785185)Termination reason: Instruction limit
% 0.55/0.41 % (2785185)Termination phase: Function definition elimination
% 0.55/0.41 % (2785185)Time elapsed: 0.020 s
% 0.55/0.41 % (2785185)Peak memory usage: 11 MB
% 0.55/0.41 % (2785185)Instructions burned: 87 (million)
% 0.55/0.41 % (2785206)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3492738825:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.55/0.41 % (2785206)Instruction limit reached!
% 0.55/0.41 % (2785206)------------------------------
% 0.55/0.41 % (2785206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.43 % (2785206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.43 % (2785206)CaDiCaL version: 2.1.3
% 0.55/0.43 % (2785206)Termination reason: Instruction limit
% 0.55/0.43 % (2785206)Termination phase: shuffling
% 0.55/0.43 % (2785206)Time elapsed: 0.004 s
% 0.55/0.43 % (2785206)Peak memory usage: 10 MB
% 0.55/0.43 % (2785206)Instructions burned: 14 (million)
% 0.55/0.43 % (2785205)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.55/0.43 % (2785204)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1650515974:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.55/0.43 % (2785203)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2525339071:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.55/0.43 % (2785204)Instruction limit reached!
% 0.55/0.43 % (2785204)------------------------------
% 0.55/0.43 % (2785204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.43 % (2785204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.43 % (2785204)CaDiCaL version: 2.1.3
% 0.55/0.43 % (2785204)Termination reason: Instruction limit
% 0.55/0.43 % (2785204)Termination phase: shuffling
% 0.55/0.43 % (2785204)Time elapsed: 0.003 s
% 0.55/0.43 % (2785204)Peak memory usage: 10 MB
% 0.55/0.43 % (2785204)Instructions burned: 5 (million)
% 0.55/0.43 % (2785203)Instruction limit reached!
% 0.55/0.43 % (2785203)------------------------------
% 0.55/0.43 % (2785203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.43 % (2785203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.43 % (2785203)CaDiCaL version: 2.1.3
% 0.55/0.43 % (2785203)Termination reason: Instruction limit
% 0.55/0.43 % (2785203)Termination phase: shuffling
% 0.55/0.43 % (2785203)Time elapsed: 0.002 s
% 0.55/0.43 % (2785205)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3771022318:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.55/0.43 % (2785203)Peak memory usage: 10 MB
% 0.55/0.43 % (2785203)Instructions burned: 3 (million)
% 0.55/0.43 % (2785191)Instruction limit reached!
% 0.55/0.43 % (2785191)------------------------------
% 0.55/0.43 % (2785191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.43 % (2785191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.43 % (2785191)CaDiCaL version: 2.1.3
% 0.55/0.43 % (2785191)Termination reason: Instruction limit
% 0.55/0.43 % (2785191)Termination phase: Function definition elimination
% 0.55/0.43 % (2785191)Time elapsed: 0.035 s
% 0.55/0.43 % (2785191)Peak memory usage: 11 MB
% 0.55/0.43 % (2785191)Instructions burned: 77 (million)
% 0.55/0.43 % (2785205)Instruction limit reached!
% 0.55/0.43 % (2785205)------------------------------
% 0.55/0.43 % (2785205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.43 % (2785205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.43 % (2785205)CaDiCaL version: 2.1.3
% 0.55/0.43 % (2785205)Termination reason: Instruction limit
% 0.55/0.43 % (2785205)Termination phase: shuffling
% 0.55/0.43 % (2785205)Time elapsed: 0.003 s
% 0.55/0.43 % (2785205)Peak memory usage: 10 MB
% 0.55/0.43 % (2785205)Instructions burned: 7 (million)
% 0.55/0.43 % (2785209)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.55/0.43 % (2785209)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.55/0.43 % (2785209)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2109235286: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.55/0.43 % (2785209)Instruction limit reached!
% 0.55/0.43 % (2785209)------------------------------
% 0.55/0.43 % (2785209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.43 % (2785209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.43 % (2785209)CaDiCaL version: 2.1.3
% 0.55/0.43 % (2785209)Termination reason: Instruction limit
% 0.55/0.47 % (2785209)Termination phase: Property scanning
% 0.55/0.47 % (2785209)Time elapsed: 0.007 s
% 0.55/0.47 % (2785209)Peak memory usage: 10 MB
% 0.55/0.47 % (2785209)Instructions burned: 31 (million)
% 0.55/0.47 % (2785214)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.55/0.47 % (2785212)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=1896874575:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.55/0.47 % (2785213)lrs+10_1_si=on:cs=on:random_seed=2774979559:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.55/0.47 % (2785214)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=2936211031:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.55/0.47 % (2785215)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3521777628:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.55/0.47 % (2785214)Instruction limit reached!
% 0.55/0.47 % (2785214)------------------------------
% 0.55/0.47 % (2785214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.47 % (2785214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.47 % (2785214)CaDiCaL version: 2.1.3
% 0.55/0.47 % (2785214)Termination reason: Instruction limit
% 0.55/0.47 % (2785214)Termination phase: shuffling
% 0.55/0.47 % (2785214)Time elapsed: 0.002 s
% 0.55/0.47 % (2785214)Peak memory usage: 10 MB
% 0.55/0.47 % (2785214)Instructions burned: 4 (million)
% 0.55/0.47 % (2785217)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1285535265:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.55/0.47 % (2785213)Instruction limit reached!
% 0.55/0.47 % (2785213)------------------------------
% 0.55/0.47 % (2785213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.47 % (2785213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.47 % (2785213)CaDiCaL version: 2.1.3
% 0.55/0.47 % (2785213)Termination reason: Instruction limit
% 0.55/0.47 % (2785213)Termination phase: shuffling
% 0.55/0.47 % (2785213)Time elapsed: 0.004 s
% 0.55/0.47 % (2785213)Peak memory usage: 10 MB
% 0.55/0.47 % (2785213)Instructions burned: 9 (million)
% 0.55/0.47 % (2785192)Instruction limit reached!
% 0.55/0.47 % (2785192)------------------------------
% 0.55/0.47 % (2785192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.47 % (2785192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.47 % (2785192)CaDiCaL version: 2.1.3
% 0.55/0.47 % (2785192)Termination reason: Instruction limit
% 0.55/0.47 % (2785192)Termination phase: Function definition elimination
% 0.55/0.47 % (2785192)Time elapsed: 0.065 s
% 0.55/0.47 % (2785192)Peak memory usage: 11 MB
% 0.55/0.47 % (2785192)Instructions burned: 159 (million)
% 0.55/0.47 % (2785217)Refutation not found, incomplete strategy
% 0.55/0.47 % (2785217)------------------------------
% 0.55/0.47 % (2785217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.47 % (2785217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.47 % (2785217)CaDiCaL version: 2.1.3
% 0.55/0.47 % (2785217)Termination reason: Refutation not found, incomplete strategy
% 0.55/0.47 % (2785217)Time elapsed: 0.011 s
% 0.55/0.47 % (2785217)Peak memory usage: 13 MB
% 0.55/0.47 % (2785217)Instructions burned: 44 (million)
% 0.55/0.47 % (2785217)------------------------------
% 0.55/0.47 % (2785217)------------------------------
% 0.55/0.47 % (2785215)Instruction limit reached!
% 0.55/0.47 % (2785215)------------------------------
% 0.55/0.47 % (2785215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.47 % (2785215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.47 % (2785215)CaDiCaL version: 2.1.3
% 0.55/0.47 % (2785215)Termination reason: Instruction limit
% 0.55/0.47 % (2785215)Termination phase: Property scanning
% 0.55/0.47 % (2785215)Time elapsed: 0.018 s
% 0.55/0.47 % (2785215)Peak memory usage: 11 MB
% 0.55/0.47 % (2785215)Instructions burned: 40 (million)
% 0.55/0.47 % (2785223)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3278512455:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.20/0.51 % (2785224)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1204604156:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.20/0.51 % (2785226)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1396539261:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.20/0.51 % (2785225)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3305220030:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.20/0.51 % (2785226)Instruction limit reached!
% 1.20/0.51 % (2785226)------------------------------
% 1.20/0.51 % (2785226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.51 % (2785226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.51 % (2785226)CaDiCaL version: 2.1.3
% 1.20/0.51 % (2785226)Termination reason: Instruction limit
% 1.20/0.51 % (2785226)Termination phase: shuffling
% 1.20/0.51 % (2785226)Time elapsed: 0.004 s
% 1.20/0.51 % (2785226)Peak memory usage: 10 MB
% 1.20/0.51 % (2785226)Instructions burned: 17 (million)
% 1.20/0.51 % (2785224)Instruction limit reached!
% 1.20/0.51 % (2785224)------------------------------
% 1.20/0.51 % (2785224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.51 % (2785224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.51 % (2785224)CaDiCaL version: 2.1.3
% 1.20/0.51 % (2785224)Termination reason: Instruction limit
% 1.20/0.51 % (2785224)Termination phase: shuffling
% 1.20/0.51 % (2785224)Time elapsed: 0.006 s
% 1.20/0.51 % (2785224)Peak memory usage: 10 MB
% 1.20/0.51 % (2785224)Instructions burned: 14 (million)
% 1.20/0.51 % (2785212)Instruction limit reached!
% 1.20/0.51 % (2785212)------------------------------
% 1.20/0.51 % (2785212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.51 % (2785212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.51 % (2785212)CaDiCaL version: 2.1.3
% 1.20/0.51 % (2785212)Termination reason: Instruction limit
% 1.20/0.51 % (2785212)Termination phase: Function definition elimination
% 1.20/0.51 % (2785212)Time elapsed: 0.037 s
% 1.20/0.51 % (2785212)Peak memory usage: 11 MB
% 1.20/0.51 % (2785212)Instructions burned: 87 (million)
% 1.20/0.51 % (2785223)Instruction limit reached!
% 1.20/0.51 % (2785223)------------------------------
% 1.20/0.51 % (2785223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.51 % (2785223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.51 % (2785223)CaDiCaL version: 2.1.3
% 1.20/0.51 % (2785223)Termination reason: Instruction limit
% 1.20/0.51 % (2785223)Termination phase: Property scanning
% 1.20/0.51 % (2785223)Time elapsed: 0.012 s
% 1.20/0.51 % (2785223)Peak memory usage: 10 MB
% 1.20/0.51 % (2785223)Instructions burned: 28 (million)
% 1.20/0.51 % (2785227)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2388312238:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.20/0.51 % (2785232)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3255630562:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.20/0.51 % (2785227)Instruction limit reached!
% 1.20/0.51 % (2785227)------------------------------
% 1.20/0.51 % (2785227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.51 % (2785227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.51 % (2785227)CaDiCaL version: 2.1.3
% 1.20/0.51 % (2785227)Termination reason: Instruction limit
% 1.20/0.51 % (2785227)Termination phase: shuffling
% 1.20/0.51 % (2785227)Time elapsed: 0.002 s
% 1.20/0.51 % (2785227)Peak memory usage: 10 MB
% 1.20/0.51 % (2785227)Instructions burned: 3 (million)
% 1.20/0.51 % (2785232)Instruction limit reached!
% 1.20/0.51 % (2785232)------------------------------
% 1.20/0.51 % (2785232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.51 % (2785232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.51 % (2785232)CaDiCaL version: 2.1.3
% 1.20/0.51 % (2785232)Termination reason: Instruction limit
% 1.20/0.51 % (2785232)Termination phase: Property scanning
% 1.20/0.51 % (2785232)Time elapsed: 0.006 s
% 1.20/0.51 % (2785232)Peak memory usage: 10 MB
% 1.20/0.51 % (2785232)Instructions burned: 27 (million)
% 1.20/0.56 % (2785233)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1084470326:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.20/0.56 % (2785235)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.20/0.56 % (2785235)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.20/0.56 % (2785234)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2526981679:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.20/0.56 % (2785235)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=2962426886:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.20/0.56 % (2785238)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.20/0.56 % (2785239)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=3390414408:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.20/0.56 % (2785238)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=1325510050:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.20/0.56 % (2785235)Instruction limit reached!
% 1.20/0.56 % (2785235)------------------------------
% 1.20/0.56 % (2785235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785235)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785235)Termination reason: Instruction limit
% 1.20/0.56 % (2785235)Termination phase: shuffling
% 1.20/0.56 % (2785235)Time elapsed: 0.007 s
% 1.20/0.56 % (2785235)Peak memory usage: 10 MB
% 1.20/0.56 % (2785235)Instructions burned: 15 (million)
% 1.20/0.56 % (2785233)Instruction limit reached!
% 1.20/0.56 % (2785233)------------------------------
% 1.20/0.56 % (2785233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785233)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785233)Termination reason: Instruction limit
% 1.20/0.56 % (2785233)Termination phase: Property scanning
% 1.20/0.56 % (2785233)Time elapsed: 0.012 s
% 1.20/0.56 % (2785233)Peak memory usage: 10 MB
% 1.20/0.56 % (2785233)Instructions burned: 24 (million)
% 1.20/0.56 % (2785239)Instruction limit reached!
% 1.20/0.56 % (2785239)------------------------------
% 1.20/0.56 % (2785239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785239)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785239)Termination reason: Instruction limit
% 1.20/0.56 % (2785239)Termination phase: Property scanning
% 1.20/0.56 % (2785239)Time elapsed: 0.007 s
% 1.20/0.56 % (2785239)Peak memory usage: 10 MB
% 1.20/0.56 % (2785239)Instructions burned: 31 (million)
% 1.20/0.56 % (2785238)Instruction limit reached!
% 1.20/0.56 % (2785238)------------------------------
% 1.20/0.56 % (2785238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785238)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785238)Termination reason: Instruction limit
% 1.20/0.56 % (2785238)Termination phase: shuffling
% 1.20/0.56 % (2785238)Time elapsed: 0.005 s
% 1.20/0.56 % (2785238)Peak memory usage: 10 MB
% 1.20/0.56 % (2785238)Instructions burned: 9 (million)
% 1.20/0.56 % (2785247)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1788618854:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.20/0.56 % (2785234)Instruction limit reached!
% 1.20/0.56 % (2785234)------------------------------
% 1.20/0.56 % (2785234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785234)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785234)Termination reason: Instruction limit
% 1.20/0.56 % (2785234)Termination phase: Property scanning
% 1.20/0.56 % (2785234)Time elapsed: 0.027 s
% 1.20/0.56 % (2785234)Peak memory usage: 11 MB
% 1.20/0.56 % (2785234)Instructions burned: 60 (million)
% 1.20/0.56 % (2785246)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2853752489:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.20/0.56 % (2785247)Instruction limit reached!
% 1.20/0.56 % (2785247)------------------------------
% 1.20/0.56 % (2785247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785247)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785247)Termination reason: Instruction limit
% 1.20/0.56 % (2785247)Termination phase: Property scanning
% 1.20/0.56 % (2785247)Time elapsed: 0.005 s
% 1.20/0.56 % (2785247)Peak memory usage: 10 MB
% 1.20/0.56 % (2785247)Instructions burned: 22 (million)
% 1.20/0.56 % (2785245)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2778981876:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.20/0.56 % (2785248)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=710510903:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.20/0.56 % (2785245)Instruction limit reached!
% 1.20/0.56 % (2785245)------------------------------
% 1.20/0.56 % (2785245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785245)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785245)Termination reason: Instruction limit
% 1.20/0.56 % (2785245)Termination phase: shuffling
% 1.20/0.56 % (2785245)Time elapsed: 0.004 s
% 1.20/0.56 % (2785245)Peak memory usage: 10 MB
% 1.20/0.56 % (2785245)Instructions burned: 9 (million)
% 1.20/0.56 % (2785251)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1516808384:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.20/0.56 % (2785246)Instruction limit reached!
% 1.20/0.56 % (2785246)------------------------------
% 1.20/0.56 % (2785246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785246)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785246)Termination reason: Instruction limit
% 1.20/0.56 % (2785246)Termination phase: Property scanning
% 1.20/0.56 % (2785246)Time elapsed: 0.011 s
% 1.20/0.56 % (2785246)Peak memory usage: 10 MB
% 1.20/0.56 % (2785246)Instructions burned: 24 (million)
% 1.20/0.56 % (2785253)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=864221270:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.20/0.56 % (2785255)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1866633607:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.20/0.56 % (2785257)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.20/0.56 % (2785257)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1918762038:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 1.20/0.56 % (2785257)Instruction limit reached!
% 1.20/0.56 % (2785257)------------------------------
% 1.20/0.56 % (2785257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785257)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785257)Termination reason: Instruction limit
% 1.20/0.56 % (2785257)Termination phase: shuffling
% 1.20/0.56 % (2785257)Time elapsed: 0.004 s
% 1.20/0.56 % (2785257)Peak memory usage: 10 MB
% 1.20/0.56 % (2785257)Instructions burned: 9 (million)
% 1.20/0.56 % (2785251)Instruction limit reached!
% 1.20/0.56 % (2785251)------------------------------
% 1.20/0.56 % (2785251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785251)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785251)Termination reason: Instruction limit
% 1.20/0.56 % (2785251)Termination phase: Function definition elimination
% 1.20/0.56 % (2785251)Time elapsed: 0.032 s
% 1.20/0.56 % (2785251)Peak memory usage: 11 MB
% 1.20/0.56 % (2785251)Instructions burned: 148 (million)
% 1.20/0.56 % (2785255)Instruction limit reached!
% 1.20/0.56 % (2785255)------------------------------
% 1.20/0.56 % (2785255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785255)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785255)Termination reason: Instruction limit
% 1.20/0.56 % (2785255)Termination phase: Property scanning
% 1.20/0.56 % (2785255)Time elapsed: 0.019 s
% 1.20/0.56 % (2785255)Peak memory usage: 11 MB
% 1.20/0.56 % (2785255)Instructions burned: 44 (million)
% 1.20/0.56 % (2785261)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3042878724:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 1.20/0.56 % (2785262)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=3090548346: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)
% 1.20/0.56 % (2785263)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.20/0.56 % (2785263)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3107561122:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 1.20/0.56 % (2785263)Instruction limit reached!
% 1.20/0.56 % (2785263)------------------------------
% 1.20/0.56 % (2785263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785263)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785263)Termination reason: Instruction limit
% 1.20/0.56 % (2785263)Termination phase: shuffling
% 1.20/0.56 % (2785263)Time elapsed: 0.003 s
% 1.20/0.56 % (2785263)Peak memory usage: 10 MB
% 1.20/0.56 % (2785263)Instructions burned: 7 (million)
% 1.20/0.56 % (2785262)Refutation not found, incomplete strategy
% 1.20/0.56 % (2785262)------------------------------
% 1.20/0.56 % (2785262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785262)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785262)Termination reason: Refutation not found, incomplete strategy
% 1.20/0.56 % (2785262)Time elapsed: 0.018 s
% 1.20/0.56 % (2785262)Peak memory usage: 13 MB
% 1.20/0.56 % (2785262)Instructions burned: 73 (million)
% 1.20/0.56 % (2785262)------------------------------
% 1.20/0.56 % (2785262)------------------------------
% 1.20/0.56 % (2785253) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2785162-2785253"...
% 1.20/0.56 % (2785268)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3183823256:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 1.20/0.56 % (2785267)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=860734215:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 1.20/0.56 % (2785253)...printing done.
% 1.20/0.56 % (2785253)Refutation found. Thanks to Tanya!
% 1.20/0.56 % SZS status Theorem for theBenchmark
% 1.20/0.56 % SZS output start Proof for theBenchmark
% 1.20/0.56 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.20/0.56 thf(func_def_0, type, is_of: ($i > ($i > $o) > $o)).
% 1.20/0.56 thf(func_def_2, type, all_of: (($i > $o) > ($i > $o) > $o)).
% 1.20/0.56 thf(func_def_3, type, eps: (($i > $o) > $i)).
% 1.20/0.56 thf(func_def_4, type, in: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_5, type, d_Subq: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_7, type, union: ($i > $i)).
% 1.20/0.56 thf(func_def_8, type, power: ($i > $i)).
% 1.20/0.56 thf(func_def_9, type, repl: ($i > ($i > $i) > $i)).
% 1.20/0.56 thf(func_def_10, type, d_Union_closed: ($i > $o)).
% 1.20/0.56 thf(func_def_11, type, d_Power_closed: ($i > $o)).
% 1.20/0.56 thf(func_def_12, type, d_Repl_closed: ($i > $o)).
% 1.20/0.56 thf(func_def_13, type, d_ZF_closed: ($i > $o)).
% 1.20/0.56 thf(func_def_14, type, univof: ($i > $i)).
% 1.20/0.56 thf(func_def_15, type, if: ($o > $i > $i > $i)).
% 1.20/0.56 thf(func_def_16, type, nIn: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_17, type, d_UPair: ($i > $i > $i)).
% 1.20/0.56 thf(func_def_18, type, d_Sing: ($i > $i)).
% 1.20/0.56 thf(func_def_19, type, binunion: ($i > $i > $i)).
% 1.20/0.56 thf(func_def_20, type, famunion: ($i > ($i > $i) > $i)).
% 1.20/0.56 thf(func_def_21, type, d_Sep: ($i > ($i > $o) > $i)).
% 1.20/0.56 thf(func_def_22, type, d_ReplSep: ($i > ($i > $o) > ($i > $i) > $i)).
% 1.20/0.56 thf(func_def_23, type, setminus: ($i > $i > $i)).
% 1.20/0.56 thf(func_def_24, type, d_In_rec_G: (($i > ($i > $i) > $i) > $i > $i > $o)).
% 1.20/0.56 thf(func_def_25, type, d_In_rec: (($i > ($i > $i) > $i) > $i > $i)).
% 1.20/0.56 thf(func_def_26, type, ordsucc: ($i > $i)).
% 1.20/0.56 thf(func_def_27, type, nat_p: ($i > $o)).
% 1.20/0.56 thf(func_def_29, type, d_Inj1: ($i > $i)).
% 1.20/0.56 thf(func_def_30, type, d_Inj0: ($i > $i)).
% 1.20/0.56 thf(func_def_31, type, d_Unj: ($i > $i)).
% 1.20/0.56 thf(func_def_32, type, pair: ($i > $i > $i)).
% 1.20/0.56 thf(func_def_33, type, proj0: ($i > $i)).
% 1.20/0.56 thf(func_def_34, type, proj1: ($i > $i)).
% 1.20/0.56 thf(func_def_35, type, d_Sigma: ($i > ($i > $i) > $i)).
% 1.20/0.56 thf(func_def_36, type, setprod: ($i > $i > $i)).
% 1.20/0.56 thf(func_def_37, type, ap: ($i > $i > $i)).
% 1.20/0.56 thf(func_def_38, type, pair_p: ($i > $o)).
% 1.20/0.56 thf(func_def_39, type, d_Pi: ($i > ($i > $i) > $i)).
% 1.20/0.56 thf(func_def_40, type, imp: ($o > $o > $o)).
% 1.20/0.56 thf(func_def_41, type, d_not: ($o > $o)).
% 1.20/0.56 thf(func_def_42, type, wel: ($o > $o)).
% 1.20/0.56 thf(func_def_43, type, obvious: $o).
% 1.20/0.56 thf(func_def_44, type, l_ec: ($o > $o > $o)).
% 1.20/0.56 thf(func_def_45, type, d_and: ($o > $o > $o)).
% 1.20/0.56 thf(func_def_46, type, l_or: ($o > $o > $o)).
% 1.20/0.56 thf(func_def_47, type, orec: ($o > $o > $o)).
% 1.20/0.56 thf(func_def_48, type, l_iff: ($o > $o > $o)).
% 1.20/0.56 thf(func_def_49, type, all: ($i > ($i > $o) > $o)).
% 1.20/0.56 thf(func_def_50, type, non: ($i > ($i > $o) > $i > $o)).
% 1.20/0.56 thf(func_def_51, type, l_some: ($i > ($i > $o) > $o)).
% 1.20/0.56 thf(func_def_52, type, or3: ($o > $o > $o > $o)).
% 1.20/0.56 thf(func_def_53, type, and3: ($o > $o > $o > $o)).
% 1.20/0.56 thf(func_def_54, type, ec3: ($o > $o > $o > $o)).
% 1.20/0.56 thf(func_def_55, type, orec3: ($o > $o > $o > $o)).
% 1.20/0.56 thf(func_def_56, type, e_is: ($i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_57, type, amone: ($i > ($i > $o) > $o)).
% 1.20/0.56 thf(func_def_58, type, one: ($i > ($i > $o) > $o)).
% 1.20/0.56 thf(func_def_59, type, ind: ($i > ($i > $o) > $i)).
% 1.20/0.56 thf(func_def_60, type, injective: ($i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_61, type, image: ($i > $i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_62, type, tofs: ($i > $i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_63, type, soft: ($i > $i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_64, type, inverse: ($i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_65, type, surjective: ($i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_66, type, bijective: ($i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_67, type, invf: ($i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_68, type, inj_h: ($i > $i > $i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_69, type, e_in: ($i > ($i > $o) > $i > $i)).
% 1.20/0.56 thf(func_def_70, type, out: ($i > ($i > $o) > $i > $i)).
% 1.20/0.56 thf(func_def_71, type, d_pair: ($i > $i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_72, type, first: ($i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_73, type, second: ($i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_74, type, prop1: ($o > $i > $i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_75, type, ite: ($o > $i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_76, type, wissel_wa: ($i > $i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_77, type, wissel_wb: ($i > $i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_78, type, wissel: ($i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_79, type, changef: ($i > $i > $i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_80, type, r_ec: ($o > $o > $o)).
% 1.20/0.56 thf(func_def_81, type, esti: ($i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_82, type, empty: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_83, type, nonempty: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_84, type, incl: ($i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_85, type, st_disj: ($i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_86, type, nissetprop: ($i > $i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_87, type, unmore: ($i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_88, type, ecelt: ($i > ($i > $i > $o) > $i > $i)).
% 1.20/0.56 thf(func_def_89, type, ecp: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.20/0.56 thf(func_def_90, type, anec: ($i > ($i > $i > $o) > $i > $o)).
% 1.20/0.56 thf(func_def_91, type, ect: ($i > ($i > $i > $o) > $i)).
% 1.20/0.56 thf(func_def_92, type, ectset: ($i > ($i > $i > $o) > $i > $i)).
% 1.20/0.56 thf(func_def_93, type, ectelt: ($i > ($i > $i > $o) > $i > $i)).
% 1.20/0.56 thf(func_def_94, type, ecect: ($i > ($i > $i > $o) > $i > $i)).
% 1.20/0.56 thf(func_def_95, type, fixfu: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.20/0.56 thf(func_def_96, type, d_10_prop1: ($i > ($i > $i > $o) > $i > $i > $i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_97, type, prop2: ($i > ($i > $i > $o) > $i > $i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_98, type, indeq: ($i > ($i > $i > $o) > $i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_99, type, fixfu2: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.20/0.56 thf(func_def_100, type, d_11_i: ($i > ($i > $i > $o) > $i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_101, type, indeq2: ($i > ($i > $i > $o) > $i > $i > $i > $i > $i)).
% 1.20/0.56 thf(func_def_103, type, n_is: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_104, type, nis: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_105, type, n_in: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_106, type, n_some: (($i > $o) > $o)).
% 1.20/0.56 thf(func_def_107, type, n_all: (($i > $o) > $o)).
% 1.20/0.56 thf(func_def_108, type, n_one: (($i > $o) > $o)).
% 1.20/0.56 thf(func_def_110, type, cond1: ($i > $o)).
% 1.20/0.56 thf(func_def_111, type, cond2: ($i > $o)).
% 1.20/0.56 thf(func_def_112, type, i1_s: (($i > $o) > $i)).
% 1.20/0.56 thf(func_def_113, type, d_22_prop1: ($i > $o)).
% 1.20/0.56 thf(func_def_114, type, d_23_prop1: ($i > $o)).
% 1.20/0.56 thf(func_def_115, type, d_24_prop1: ($i > $o)).
% 1.20/0.56 thf(func_def_116, type, d_24_prop2: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_117, type, prop3: ($i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_118, type, prop4: ($i > $o)).
% 1.20/0.56 thf(func_def_119, type, d_24_g: ($i > $i)).
% 1.20/0.56 thf(func_def_120, type, plus: ($i > $i)).
% 1.20/0.56 thf(func_def_121, type, n_pl: ($i > $i > $i)).
% 1.20/0.56 thf(func_def_122, type, d_25_prop1: ($i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_123, type, d_26_prop1: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_124, type, d_27_prop1: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_125, type, d_28_prop1: ($i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_126, type, diffprop: ($i > $i > $i > $o)).
% 1.20/0.56 thf(func_def_127, type, d_29_ii: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_128, type, iii: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_129, type, d_29_prop1: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_130, type, moreis: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_131, type, lessis: ($i > $i > $o)).
% 1.20/0.56 thf(func_def_132, type, db0: !>[X0: $tType]:(X0)).
% 1.20/0.56 thf(func_def_133, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.20/0.56 thf(func_def_134, type, db1: !>[X0: $tType]:(X0)).
% 1.20/0.56 thf(func_def_137, type, db2: !>[X0: $tType]:(X0)).
% 1.20/0.56 thf(func_def_138, type, db4: !>[X0: $tType]:(X0)).
% 1.20/0.56 thf(func_def_139, type, db3: !>[X0: $tType]:(X0)).
% 1.20/0.56 thf(func_def_140, type, vIMP: ($o > $o > $o)).
% 1.20/0.56 thf(func_def_141, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.20/0.56 thf(func_def_142, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.20/0.56 thf(func_def_143, type, vNOT: ($o > $o)).
% 1.20/0.56 thf(func_def_144, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.20/0.56 thf(func_def_145, type, vAND: ($o > $o > $o)).
% 1.20/0.56 thf(func_def_146, type, db5: !>[X0: $tType]:(X0)).
% 1.20/0.56 thf(func_def_147, type, db6: !>[X0: $tType]:(X0)).
% 1.20/0.56 thf(func_def_148, type, vOR: ($o > $o > $o)).
% 1.20/0.56 thf(func_def_149, type, db7: !>[X0: $tType]:(X0)).
% 1.20/0.56 thf(func_def_150, type, sK0: (($i > $i) > ($i > $i) > $i > $i)).
% 1.20/0.56 thf(func_def_151, type, sK1: (($i > $o) > $i)).
% 1.20/0.56 thf(func_def_154, type, sK4: ($i > $i > $i > $i > $i)).
% 1.20/0.56 thf(f2,axiom,(
% 1.20/0.56 ((^[X0 : ($i > $o), X1 : ($i > $o)] : (! [X2 : $i] : ((is_of @ X2 @ X0) => (X1 @ X2)))) = all_of)),
% 1.20/0.56 file('/export/starexec/sandbox2/benchmark/Axioms/NUM007^0.ax',def_all_of)).
% 1.20/0.56 thf(f74,axiom,(
% 1.20/0.56 (imp = (^[X0 : $o, X1 : $o] : (X0 => X1)))),
% 1.20/0.56 file('/export/starexec/sandbox2/benchmark/Axioms/NUM007^0.ax',def_imp)).
% 1.20/0.56 thf(f81,axiom,(
% 1.20/0.56 (l_or = (^[X0 : $o] : ((imp @ (d_not @ X0)))))),
% 1.20/0.56 file('/export/starexec/sandbox2/benchmark/Axioms/NUM007^0.ax',def_l_or)).
% 1.20/0.56 thf(f157,axiom,(
% 1.20/0.56 (n_is = ((e_is @ nat)))),
% 1.20/0.56 file('/export/starexec/sandbox2/benchmark/Axioms/NUM007^0.ax',def_n_is)).
% 1.20/0.56 thf(f206,axiom,(
% 1.20/0.56 (iii = (^[X0 : $i, X1 : $i] : ((n_some @ (diffprop @ X1 @ X0)))))),
% 1.20/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_iii)).
% 1.20/0.56 thf(f215,axiom,(
% 1.20/0.56 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((iii @ X0 @ X1) => (d_29_ii @ X1 @ X0)))))))),
% 1.20/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',satz12)).
% 1.20/0.56 thf(f216,axiom,(
% 1.20/0.56 ((^[X0 : $i, X1 : $i] : ((l_or @ (d_29_ii @ X0 @ X1) @ (n_is @ X0 @ X1)))) = moreis)),
% 1.20/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_moreis)).
% 1.20/0.56 thf(f217,axiom,(
% 1.20/0.56 ((^[X0 : $i, X1 : $i] : ((l_or @ (iii @ X0 @ X1) @ (n_is @ X0 @ X1)))) = lessis)),
% 1.20/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_lessis)).
% 1.20/0.56 thf(f220,axiom,(
% 1.20/0.56 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((moreis @ X0 @ X1) => (d_not @ (iii @ X0 @ X1))))))))),
% 1.20/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',satz10c)).
% 1.20/0.56 thf(f224,axiom,(
% 1.20/0.56 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((d_29_ii @ X0 @ X1) => (d_not @ (lessis @ X0 @ X1))))))))),
% 1.20/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',satz10g)).
% 1.20/0.56 thf(f225,conjecture,(
% 1.20/0.56 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((iii @ X0 @ X1) => (d_not @ (moreis @ X0 @ X1))))))))),
% 1.20/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',satz10h)).
% 1.20/0.56 thf(f226,negated_conjecture,(
% 1.20/0.56 ~(all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((iii @ X0 @ X1) => (d_not @ (moreis @ X0 @ X1))))))))),
% 1.20/0.56 inference(negated_conjecture,[status(cth)],[f225])).
% 1.20/0.56 thf(f258,plain,(
% 1.20/0.56 (iii = (^[Y0 : $i]: ((^[Y1 : $i]: (n_some @ (diffprop @ Y1 @ Y0))))))),
% 1.20/0.56 inference(fool_elimination,[],[f206])).
% 1.20/0.56 thf(f267,plain,(
% 1.20/0.56 ((^[X0 : ($i > $o), X1 : ($i > $o)] : (! [X2 : $i] : ((is_of @ X2 @ X0) => (X1 @ X2)))) = all_of)),
% 1.20/0.56 inference(rectify,[],[f2])).
% 1.20/0.56 thf(f268,plain,(
% 1.20/0.56 (all_of = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))))),
% 1.20/0.56 inference(fool_elimination,[],[f267])).
% 1.20/0.56 thf(f307,plain,(
% 1.20/0.56 (imp = (^[X0 : $o, X1 : $o] : (X0 => X1)))),
% 1.20/0.56 inference(rectify,[],[f74])).
% 1.20/0.56 thf(f308,plain,(
% 1.20/0.56 (imp = (^[Y0 : $o]: ((^[Y1 : $o]: (Y0 => Y1)))))),
% 1.20/0.56 inference(fool_elimination,[],[f307])).
% 1.20/0.56 thf(f392,plain,(
% 1.20/0.56 (moreis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (d_29_ii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.20/0.56 inference(fool_elimination,[],[f216])).
% 1.20/0.56 thf(f397,plain,(
% 1.20/0.56 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((moreis @ X1 @ X3) => (d_not @ (iii @ X1 @ X3))))))))),
% 1.20/0.56 inference(rectify,[],[f220])).
% 1.20/0.56 thf(f398,plain,(
% 1.20/0.56 (((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((moreis @ Y0 @ Y1) => (d_not @ (iii @ Y0 @ Y1)))))))) = $true)),
% 1.20/0.56 inference(fool_elimination,[],[f397])).
% 1.20/0.56 thf(f422,plain,(
% 1.20/0.56 ~(all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((iii @ X1 @ X3) => (d_not @ (moreis @ X1 @ X3))))))))),
% 1.20/0.56 inference(rectify,[],[f226])).
% 1.20/0.56 thf(f423,plain,(
% 1.20/0.56 ~ (((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((iii @ Y0 @ Y1) => (d_not @ (moreis @ Y0 @ Y1)))))))) = $true)),
% 1.20/0.56 inference(fool_elimination,[],[f422])).
% 1.20/0.56 thf(f494,plain,(
% 1.20/0.56 (lessis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (iii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.20/0.56 inference(fool_elimination,[],[f217])).
% 1.20/0.56 thf(f507,plain,(
% 1.20/0.56 (l_or = (^[Y0 : $o]: (imp @ (d_not @ Y0))))),
% 1.20/0.56 inference(fool_elimination,[],[f81])).
% 1.20/0.56 thf(f546,plain,(
% 1.20/0.56 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((d_29_ii @ X1 @ X3) => (d_not @ (lessis @ X1 @ X3))))))))),
% 1.20/0.56 inference(rectify,[],[f224])).
% 1.20/0.56 thf(f547,plain,(
% 1.20/0.56 (((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_29_ii @ Y0 @ Y1) => (d_not @ (lessis @ Y0 @ Y1)))))))) = $true)),
% 1.20/0.56 inference(fool_elimination,[],[f546])).
% 1.20/0.56 thf(f580,plain,(
% 1.20/0.56 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((iii @ X1 @ X3) => (d_29_ii @ X3 @ X1)))))))),
% 1.20/0.56 inference(rectify,[],[f215])).
% 1.20/0.56 thf(f581,plain,(
% 1.20/0.56 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((iii @ Y0 @ Y1) => (d_29_ii @ Y1 @ Y0))))))))),
% 1.20/0.56 inference(fool_elimination,[],[f580])).
% 1.20/0.56 thf(f584,plain,(
% 1.20/0.56 (((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((iii @ Y0 @ Y1) => (d_not @ (moreis @ Y0 @ Y1)))))))) != $true)),
% 1.20/0.56 inference(flattening,[],[f423])).
% 1.20/0.56 thf(f603,plain,(
% 1.20/0.56 (lessis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (iii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.20/0.56 inference(cnf_transformation,[],[f494])).
% 1.20/0.56 thf(f604,plain,(
% 1.20/0.56 (l_or = (^[Y0 : $o]: (imp @ (d_not @ Y0))))),
% 1.20/0.56 inference(cnf_transformation,[],[f507])).
% 1.20/0.56 thf(f605,plain,(
% 1.20/0.56 (((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((iii @ Y0 @ Y1) => (d_not @ (moreis @ Y0 @ Y1)))))))) != $true)),
% 1.20/0.56 inference(cnf_transformation,[],[f584])).
% 1.20/0.56 thf(f614,plain,(
% 1.20/0.56 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((iii @ Y0 @ Y1) => (d_29_ii @ Y1 @ Y0))))))))),
% 1.20/0.56 inference(cnf_transformation,[],[f581])).
% 1.20/0.56 thf(f619,plain,(
% 1.20/0.56 (imp = (^[Y0 : $o]: ((^[Y1 : $o]: (Y0 => Y1)))))),
% 1.20/0.56 inference(cnf_transformation,[],[f308])).
% 1.20/0.56 thf(f620,plain,(
% 1.20/0.56 (((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((moreis @ Y0 @ Y1) => (d_not @ (iii @ Y0 @ Y1)))))))) = $true)),
% 1.20/0.56 inference(cnf_transformation,[],[f398])).
% 1.20/0.56 thf(f624,plain,(
% 1.20/0.56 (n_is = ((e_is @ nat)))),
% 1.20/0.56 inference(cnf_transformation,[],[f157])).
% 1.20/0.56 thf(f629,plain,(
% 1.20/0.56 (iii = (^[Y0 : $i]: ((^[Y1 : $i]: (n_some @ (diffprop @ Y1 @ Y0))))))),
% 1.20/0.56 inference(cnf_transformation,[],[f258])).
% 1.20/0.56 thf(f632,plain,(
% 1.20/0.56 (((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_29_ii @ Y0 @ Y1) => (d_not @ (lessis @ Y0 @ Y1)))))))) = $true)),
% 1.20/0.56 inference(cnf_transformation,[],[f547])).
% 1.20/0.56 thf(f635,plain,(
% 1.20/0.56 (all_of = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))))),
% 1.20/0.56 inference(cnf_transformation,[],[f268])).
% 1.20/0.56 thf(f636,plain,(
% 1.20/0.56 (moreis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (d_29_ii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.20/0.56 inference(cnf_transformation,[],[f392])).
% 1.20/0.56 thf(f657,definition,(
% 1.20/0.56 ($true != $false)),
% 1.20/0.56 introduced(theory,[fool_distinctness_axiom])).
% 1.20/0.56 thf(f658,definition,(
% 1.20/0.56 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.20/0.56 introduced(theory,[fool_exhaustiveness_axiom])).
% 1.20/0.56 thf(f659,plain,(
% 1.20/0.56 (l_or = (^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: (Y1 => Y2)))) @ (d_not @ Y0))))),
% 1.20/0.56 inference(definition_unfolding,[],[f604,f619])).
% 1.20/0.56 thf(f660,plain,(
% 1.20/0.56 (moreis = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $o]: ((^[Y3 : $o]: ((^[Y4 : $o]: (Y3 => Y4)))) @ (d_not @ Y2))) @ (d_29_ii @ Y0 @ Y1) @ (e_is @ nat @ Y0 @ Y1))))))),
% 1.20/0.56 inference(definition_unfolding,[],[f636,f659,f624])).
% 1.20/0.56 thf(f661,plain,(
% 1.20/0.56 (lessis = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $o]: ((^[Y3 : $o]: ((^[Y4 : $o]: (Y3 => Y4)))) @ (d_not @ Y2))) @ ((^[Y2 : $i]: ((^[Y3 : $i]: (n_some @ (diffprop @ Y3 @ Y2))))) @ Y0 @ Y1) @ (e_is @ nat @ Y0 @ Y1))))))),
% 1.20/0.56 inference(definition_unfolding,[],[f603,f659,f629,f624])).
% 1.20/0.56 thf(f668,plain,(
% 1.20/0.56 ($true != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))) @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: ((is_of @ Y3 @ Y1) => (Y2 @ Y3))))))) @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: (((^[Y2 : $i]: ((^[Y3 : $i]: (n_some @ (diffprop @ Y3 @ Y2))))) @ Y0 @ Y1) => (d_not @ ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $o]: ((^[Y5 : $o]: ((^[Y6 : $o]: (Y5 => Y6)))) @ (d_not @ Y4))) @ (d_29_ii @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y0 @ Y1)))))))))),
% 1.20/0.56 inference(definition_unfolding,[],[f605,f635,f635,f629,f660])).
% 1.20/0.56 thf(f674,plain,(
% 1.20/0.56 ((((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))) @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: ((is_of @ Y3 @ Y1) => (Y2 @ Y3))))))) @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: (((^[Y2 : $i]: ((^[Y3 : $i]: (n_some @ (diffprop @ Y3 @ Y2))))) @ Y0 @ Y1) => (d_29_ii @ Y1 @ Y0))))))) = $true)),
% 1.20/0.56 inference(definition_unfolding,[],[f614,f635,f635,f629])).
% 1.20/0.56 thf(f679,plain,(
% 1.20/0.56 ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))) @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: ((is_of @ Y3 @ Y1) => (Y2 @ Y3))))))) @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: (((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $o]: ((^[Y5 : $o]: ((^[Y6 : $o]: (Y5 => Y6)))) @ (d_not @ Y4))) @ (d_29_ii @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y0 @ Y1) => (d_not @ ((^[Y2 : $i]: ((^[Y3 : $i]: (n_some @ (diffprop @ Y3 @ Y2))))) @ Y0 @ Y1)))))))))),
% 1.20/0.56 inference(definition_unfolding,[],[f620,f635,f635,f660,f629])).
% 1.20/0.56 thf(f685,plain,(
% 1.20/0.56 ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))) @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: ((is_of @ Y3 @ Y1) => (Y2 @ Y3))))))) @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_29_ii @ Y0 @ Y1) => (d_not @ ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $o]: ((^[Y5 : $o]: ((^[Y6 : $o]: (Y5 => Y6)))) @ (d_not @ Y4))) @ ((^[Y4 : $i]: ((^[Y5 : $i]: (n_some @ (diffprop @ Y5 @ Y4))))) @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y0 @ Y1)))))))))),
% 1.20/0.56 inference(definition_unfolding,[],[f632,f635,f635,f661])).
% 1.20/0.56 thf(f728,plain,(
% 1.20/0.56 ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((n_some @ (diffprop @ Y1 @ Y0)) => (d_29_ii @ Y1 @ Y0))))))))))),
% 1.20/0.56 inference(beta-eta_normalization,[],[f674])).
% 1.20/0.56 thf(f729,plain,(
% 1.20/0.56 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((n_some @ (diffprop @ Y1 @ Y0)) => (d_29_ii @ Y1 @ Y0))))))) @ X1)))) )),
% 1.20/0.56 inference(pi_proxy_clausification,[],[f728])).
% 1.20/0.56 thf(f730,plain,(
% 1.20/0.56 ( ! [X1 : $i] : (((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ Y0 @ X1)) => (d_29_ii @ Y0 @ X1))))))) = $true)) )),
% 1.20/0.56 inference(beta-eta_normalization,[],[f729])).
% 1.20/0.56 thf(f731,plain,(
% 1.20/0.56 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ Y0 @ X1)) => (d_29_ii @ Y0 @ X1)))))) = $true)) )),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f730])).
% 1.20/0.56 thf(f732,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ Y0 @ X1)) => (d_29_ii @ Y0 @ X1)))) @ X2))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.20/0.56 inference(pi_proxy_clausification,[],[f731])).
% 1.20/0.56 thf(f733,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((n_some @ (diffprop @ X2 @ X1)) => (d_29_ii @ X2 @ X1)))))) )),
% 1.20/0.56 inference(beta-eta_normalization,[],[f732])).
% 1.20/0.56 thf(f734,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((n_some @ (diffprop @ X2 @ X1)) => (d_29_ii @ X2 @ X1)))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f733])).
% 1.20/0.56 thf(f735,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_29_ii @ X2 @ X1)) = $true) | (((n_some @ (diffprop @ X2 @ X1))) = $false)) )),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f734])).
% 1.20/0.56 thf(f782,plain,(
% 1.20/0.56 ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((d_29_ii @ Y0 @ Y1) => (d_not @ ((d_not @ (n_some @ (diffprop @ Y1 @ Y0))) => (e_is @ nat @ Y0 @ Y1))))))))))))),
% 1.20/0.56 inference(beta-eta_normalization,[],[f685])).
% 1.20/0.56 thf(f783,plain,(
% 1.20/0.56 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((d_29_ii @ Y0 @ Y1) => (d_not @ ((d_not @ (n_some @ (diffprop @ Y1 @ Y0))) => (e_is @ nat @ Y0 @ Y1))))))))) @ X1)) = $true)) )),
% 1.20/0.56 inference(pi_proxy_clausification,[],[f782])).
% 1.20/0.56 thf(f784,plain,(
% 1.20/0.56 ( ! [X1 : $i] : (((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_29_ii @ X1 @ Y0) => (d_not @ ((d_not @ (n_some @ (diffprop @ Y0 @ X1))) => (e_is @ nat @ X1 @ Y0))))))))) = $true)) )),
% 1.20/0.56 inference(beta-eta_normalization,[],[f783])).
% 1.20/0.56 thf(f785,plain,(
% 1.20/0.56 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_29_ii @ X1 @ Y0) => (d_not @ ((d_not @ (n_some @ (diffprop @ Y0 @ X1))) => (e_is @ nat @ X1 @ Y0)))))))))) )),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f784])).
% 1.20/0.56 thf(f786,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_29_ii @ X1 @ Y0) => (d_not @ ((d_not @ (n_some @ (diffprop @ Y0 @ X1))) => (e_is @ nat @ X1 @ Y0)))))) @ X2)))) )),
% 1.20/0.56 inference(pi_proxy_clausification,[],[f785])).
% 1.20/0.56 thf(f787,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((d_29_ii @ X1 @ X2) => (d_not @ ((d_not @ (n_some @ (diffprop @ X2 @ X1))) => (e_is @ nat @ X1 @ X2)))))))) )),
% 1.20/0.56 inference(beta-eta_normalization,[],[f786])).
% 1.20/0.56 thf(f788,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((d_29_ii @ X1 @ X2) => (d_not @ ((d_not @ (n_some @ (diffprop @ X2 @ X1))) => (e_is @ nat @ X1 @ X2))))))) )),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f787])).
% 1.20/0.56 thf(f789,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : ((((d_not @ ((d_not @ (n_some @ (diffprop @ X2 @ X1))) => (e_is @ nat @ X1 @ X2)))) = $true) | (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((d_29_ii @ X1 @ X2)))) )),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f788])).
% 1.20/0.56 thf(f877,plain,(
% 1.20/0.56 (((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => (((d_not @ (d_29_ii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1)) => (d_not @ (n_some @ (diffprop @ Y1 @ Y0))))))))))) = $true)),
% 1.20/0.56 inference(beta-eta_normalization,[],[f679])).
% 1.20/0.56 thf(f878,plain,(
% 1.20/0.56 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => (((d_not @ (d_29_ii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1)) => (d_not @ (n_some @ (diffprop @ Y1 @ Y0))))))))) @ X1)))) )),
% 1.20/0.56 inference(pi_proxy_clausification,[],[f877])).
% 1.20/0.56 thf(f879,plain,(
% 1.20/0.56 ( ! [X1 : $i] : (((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (d_29_ii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (n_some @ (diffprop @ Y0 @ X1))))))))) = $true)) )),
% 1.20/0.56 inference(beta-eta_normalization,[],[f878])).
% 1.20/0.56 thf(f880,plain,(
% 1.20/0.56 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (d_29_ii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (n_some @ (diffprop @ Y0 @ X1))))))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f879])).
% 1.20/0.56 thf(f881,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (d_29_ii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (n_some @ (diffprop @ Y0 @ X1)))))) @ X2)) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.20/0.56 inference(pi_proxy_clausification,[],[f880])).
% 1.20/0.56 thf(f882,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : (($true = (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (((d_not @ (d_29_ii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)) => (d_not @ (n_some @ (diffprop @ X2 @ X1))))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.20/0.56 inference(beta-eta_normalization,[],[f881])).
% 1.20/0.56 thf(f883,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : ((((((d_not @ (d_29_ii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)) => (d_not @ (n_some @ (diffprop @ X2 @ X1))))) = $true) | (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f882])).
% 1.20/0.56 thf(f884,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : ((((d_not @ (n_some @ (diffprop @ X2 @ X1)))) = $true) | ($false = (((d_not @ (d_29_ii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f883])).
% 1.20/0.56 thf(f885,plain,(
% 1.20/0.56 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((e_is @ nat @ X1 @ X2))) | (((d_not @ (n_some @ (diffprop @ X2 @ X1)))) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f884])).
% 1.20/0.56 thf(f894,plain,(
% 1.20/0.56 (((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((n_some @ (diffprop @ Y1 @ Y0)) => (d_not @ ((d_not @ (d_29_ii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1))))))))))) != $true)),
% 1.20/0.56 inference(beta-eta_normalization,[],[f668])).
% 1.20/0.56 thf(f895,plain,(
% 1.20/0.56 ((((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((n_some @ (diffprop @ Y1 @ Y0)) => (d_not @ ((d_not @ (d_29_ii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1))))))))) @ sK2)) = $false)),
% 1.20/0.56 inference(sigma_proxy_clausification,[],[f894])).
% 1.20/0.56 thf(f896,plain,(
% 1.20/0.56 ((((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ Y0 @ sK2)) => (d_not @ ((d_not @ (d_29_ii @ sK2 @ Y0)) => (e_is @ nat @ sK2 @ Y0))))))))) = $false)),
% 1.20/0.56 inference(beta-eta_normalization,[],[f895])).
% 1.20/0.56 thf(f897,plain,(
% 1.20/0.56 (((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ Y0 @ sK2)) => (d_not @ ((d_not @ (d_29_ii @ sK2 @ Y0)) => (e_is @ nat @ sK2 @ Y0)))))))) = $false)),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f896])).
% 1.20/0.56 thf(f898,plain,(
% 1.20/0.56 (((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true)),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f896])).
% 1.20/0.56 thf(f899,plain,(
% 1.20/0.56 ($false = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ Y0 @ sK2)) => (d_not @ ((d_not @ (d_29_ii @ sK2 @ Y0)) => (e_is @ nat @ sK2 @ Y0)))))) @ sK3)))),
% 1.20/0.56 inference(sigma_proxy_clausification,[],[f897])).
% 1.20/0.56 thf(f900,plain,(
% 1.20/0.56 ((((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((n_some @ (diffprop @ sK3 @ sK2)) => (d_not @ ((d_not @ (d_29_ii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3)))))) = $false)),
% 1.20/0.56 inference(beta-eta_normalization,[],[f899])).
% 1.20/0.56 thf(f901,plain,(
% 1.20/0.56 ((((n_some @ (diffprop @ sK3 @ sK2)) => (d_not @ ((d_not @ (d_29_ii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3))))) = $false)),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f900])).
% 1.20/0.56 thf(f902,plain,(
% 1.20/0.56 (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true)),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f900])).
% 1.20/0.56 thf(f903,plain,(
% 1.20/0.56 (((d_not @ ((d_not @ (d_29_ii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3)))) = $false)),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f901])).
% 1.20/0.56 thf(f904,plain,(
% 1.20/0.56 ($true = ((n_some @ (diffprop @ sK3 @ sK2))))),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f901])).
% 1.20/0.56 thf(f978,definition,(
% 1.20/0.56 spl5_1 <=> ($true = $false)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition])).
% 1.20/0.56 thf(f981,plain,(
% 1.20/0.56 ~spl5_1),
% 1.20/0.56 inference(avatar_split_clause,[],[f657,f978])).
% 1.20/0.56 thf(f988,definition,(
% 1.20/0.56 spl5_3 <=> (((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition])).
% 1.20/0.56 thf(f990,plain,(
% 1.20/0.56 (((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true) | ~spl5_3),
% 1.20/0.56 inference(avatar_component_clause,[],[f988])).
% 1.20/0.56 thf(f991,plain,(
% 1.20/0.56 spl5_3),
% 1.20/0.56 inference(avatar_split_clause,[],[f898,f988])).
% 1.20/0.56 thf(f993,definition,(
% 1.20/0.56 spl5_4 <=> (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition])).
% 1.20/0.56 thf(f995,plain,(
% 1.20/0.56 (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true) | ~spl5_4),
% 1.20/0.56 inference(avatar_component_clause,[],[f993])).
% 1.20/0.56 thf(f996,plain,(
% 1.20/0.56 spl5_4),
% 1.20/0.56 inference(avatar_split_clause,[],[f902,f993])).
% 1.20/0.56 thf(f998,definition,(
% 1.20/0.56 spl5_5 <=> ($true = ((n_some @ (diffprop @ sK3 @ sK2))))),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition])).
% 1.20/0.56 thf(f1000,plain,(
% 1.20/0.56 ($true = ((n_some @ (diffprop @ sK3 @ sK2)))) | ~spl5_5),
% 1.20/0.56 inference(avatar_component_clause,[],[f998])).
% 1.20/0.56 thf(f1001,plain,(
% 1.20/0.56 spl5_5),
% 1.20/0.56 inference(avatar_split_clause,[],[f904,f998])).
% 1.20/0.56 thf(f1003,definition,(
% 1.20/0.56 spl5_6 <=> (((d_not @ ((d_not @ (d_29_ii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3)))) = $false)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition])).
% 1.20/0.56 thf(f1005,plain,(
% 1.20/0.56 (((d_not @ ((d_not @ (d_29_ii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3)))) = $false) | ~spl5_6),
% 1.20/0.56 inference(avatar_component_clause,[],[f1003])).
% 1.20/0.56 thf(f1006,plain,(
% 1.20/0.56 spl5_6),
% 1.20/0.56 inference(avatar_split_clause,[],[f903,f1003])).
% 1.20/0.56 thf(f1020,plain,(
% 1.20/0.56 ( ! [X0 : $i] : (($false = ((n_some @ (diffprop @ sK2 @ X0)))) | ($true = $false) | ($true = ((d_29_ii @ sK2 @ X0))) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) ) | ~spl5_3),
% 1.20/0.56 inference(superposition,[],[f990,f735])).
% 1.20/0.56 thf(f1021,plain,(
% 1.20/0.56 ( ! [X0 : $i] : ((((d_29_ii @ sK3 @ X0)) = $true) | ($true = $false) | ($false = ((n_some @ (diffprop @ sK3 @ X0)))) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) ) | ~spl5_4),
% 1.20/0.56 inference(superposition,[],[f995,f735])).
% 1.20/0.56 thf(f1023,plain,(
% 1.20/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($false = ((n_some @ (diffprop @ sK2 @ X0)))) | ($true = ((d_29_ii @ sK2 @ X0)))) ) | ~spl5_3),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1020])).
% 1.20/0.56 thf(f1024,plain,(
% 1.20/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($false = ((n_some @ (diffprop @ sK3 @ X0)))) | (((d_29_ii @ sK3 @ X0)) = $true)) ) | ~spl5_4),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1021])).
% 1.20/0.56 thf(f1033,plain,(
% 1.20/0.56 (((e_is @ nat @ sK2 @ sK3)) = $false) | ($false = ((d_not @ ((d_not @ (d_29_ii @ sK2 @ sK3)) => $true)))) | ~spl5_6),
% 1.20/0.56 inference(superposition,[],[f1005,f658])).
% 1.20/0.56 thf(f1034,plain,(
% 1.20/0.56 (((d_29_ii @ sK2 @ sK3)) = $false) | (((d_not @ ((d_not @ $true) => (e_is @ nat @ sK2 @ sK3)))) = $false) | ~spl5_6),
% 1.20/0.56 inference(superposition,[],[f1005,f658])).
% 1.20/0.56 thf(f1035,plain,(
% 1.20/0.56 ($false = ((d_not @ ($true => (e_is @ nat @ sK2 @ sK3))))) | (((d_not @ (d_29_ii @ sK2 @ sK3))) = $false) | ~spl5_6),
% 1.20/0.56 inference(superposition,[],[f1005,f658])).
% 1.20/0.56 thf(f1036,plain,(
% 1.20/0.56 ($false = ((d_not @ $true))) | ((((d_not @ (d_29_ii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3))) = $false) | ~spl5_6),
% 1.20/0.56 inference(superposition,[],[f1005,f658])).
% 1.20/0.56 thf(f1039,plain,(
% 1.20/0.56 (((d_not @ (e_is @ nat @ sK2 @ sK3))) = $false) | (((d_not @ (d_29_ii @ sK2 @ sK3))) = $false) | ~spl5_6),
% 1.20/0.56 inference(boolean_simplification,[],[f1035])).
% 1.20/0.56 thf(f1041,plain,(
% 1.20/0.56 ($false = ((d_not @ $true))) | (((d_not @ (d_29_ii @ sK2 @ sK3))) = $true) | ~spl5_6),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f1036])).
% 1.20/0.56 thf(f1049,plain,(
% 1.20/0.56 ($false = ((d_not @ $true))) | (((e_is @ nat @ sK2 @ sK3)) = $false) | ~spl5_6),
% 1.20/0.56 inference(boolean_simplification,[],[f1033])).
% 1.20/0.56 thf(f1052,definition,(
% 1.20/0.56 spl5_7 <=> (((d_not @ (d_29_ii @ sK2 @ sK3))) = $false)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition])).
% 1.20/0.56 thf(f1056,definition,(
% 1.20/0.56 spl5_8 <=> (((d_not @ (e_is @ nat @ sK2 @ sK3))) = $false)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition])).
% 1.20/0.56 thf(f1059,plain,(
% 1.20/0.56 spl5_7 | spl5_8 | ~spl5_6),
% 1.20/0.56 inference(avatar_split_clause,[],[f1039,f1003,f1056,f1052])).
% 1.20/0.56 thf(f1061,definition,(
% 1.20/0.56 spl5_9 <=> ($false = ((d_not @ $true)))),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition])).
% 1.20/0.56 thf(f1063,plain,(
% 1.20/0.56 ($false = ((d_not @ $true))) | ~spl5_9),
% 1.20/0.56 inference(avatar_component_clause,[],[f1061])).
% 1.20/0.56 thf(f1065,definition,(
% 1.20/0.56 spl5_10 <=> (((d_not @ (d_29_ii @ sK2 @ sK3))) = $true)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition])).
% 1.20/0.56 thf(f1068,plain,(
% 1.20/0.56 spl5_9 | spl5_10 | ~spl5_6),
% 1.20/0.56 inference(avatar_split_clause,[],[f1041,f1003,f1065,f1061])).
% 1.20/0.56 thf(f1070,definition,(
% 1.20/0.56 spl5_11 <=> (((e_is @ nat @ sK2 @ sK3)) = $false)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition])).
% 1.20/0.56 thf(f1075,definition,(
% 1.20/0.56 spl5_12 <=> (((d_not @ ((d_not @ $true) => (e_is @ nat @ sK2 @ sK3)))) = $false)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition])).
% 1.20/0.56 thf(f1077,plain,(
% 1.20/0.56 (((d_not @ ((d_not @ $true) => (e_is @ nat @ sK2 @ sK3)))) = $false) | ~spl5_12),
% 1.20/0.56 inference(avatar_component_clause,[],[f1075])).
% 1.20/0.56 thf(f1079,definition,(
% 1.20/0.56 spl5_13 <=> (((d_29_ii @ sK2 @ sK3)) = $false)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_13])],[avatar_definition])).
% 1.20/0.56 thf(f1082,plain,(
% 1.20/0.56 spl5_12 | spl5_13 | ~spl5_6),
% 1.20/0.56 inference(avatar_split_clause,[],[f1034,f1003,f1079,f1075])).
% 1.20/0.56 thf(f1083,plain,(
% 1.20/0.56 spl5_11 | spl5_9 | ~spl5_6),
% 1.20/0.56 inference(avatar_split_clause,[],[f1049,f1003,f1061,f1070])).
% 1.20/0.56 thf(f1096,plain,(
% 1.20/0.56 ( ! [X0 : $o] : ((((d_not @ X0)) = $false) | ($false = X0)) ) | ~spl5_9),
% 1.20/0.56 inference(superposition,[],[f1063,f658])).
% 1.20/0.56 thf(f1100,plain,(
% 1.20/0.56 ($true = $false) | (((n_some @ (diffprop @ sK2 @ sK3))) = $false) | (((d_29_ii @ sK2 @ sK3)) = $true) | (~spl5_3 | ~spl5_4)),
% 1.20/0.56 inference(superposition,[],[f1023,f995])).
% 1.20/0.56 thf(f1107,plain,(
% 1.20/0.56 (((n_some @ (diffprop @ sK2 @ sK3))) = $false) | (((d_29_ii @ sK2 @ sK3)) = $true) | (~spl5_3 | ~spl5_4)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1100])).
% 1.20/0.56 thf(f1119,definition,(
% 1.20/0.56 spl5_16 <=> (((n_some @ (diffprop @ sK2 @ sK3))) = $false)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_16])],[avatar_definition])).
% 1.20/0.56 thf(f1121,plain,(
% 1.20/0.56 (((n_some @ (diffprop @ sK2 @ sK3))) = $false) | ~spl5_16),
% 1.20/0.56 inference(avatar_component_clause,[],[f1119])).
% 1.20/0.56 thf(f1123,definition,(
% 1.20/0.56 spl5_17 <=> (((d_29_ii @ sK2 @ sK3)) = $true)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_17])],[avatar_definition])).
% 1.20/0.56 thf(f1127,plain,(
% 1.20/0.56 spl5_17 | spl5_16 | ~spl5_3 | ~spl5_4),
% 1.20/0.56 inference(avatar_split_clause,[],[f1107,f993,f988,f1119,f1123])).
% 1.20/0.56 thf(f1260,plain,(
% 1.20/0.56 ( ! [X0 : $i] : (($false = ((e_is @ nat @ X0 @ sK3))) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($true = $false) | ($true = ((d_not @ (n_some @ (diffprop @ sK3 @ X0)))))) ) | ~spl5_4),
% 1.20/0.56 inference(superposition,[],[f995,f885])).
% 1.20/0.56 thf(f1265,plain,(
% 1.20/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($false = ((e_is @ nat @ X0 @ sK3))) | ($true = ((d_not @ (n_some @ (diffprop @ sK3 @ X0)))))) ) | ~spl5_4),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1260])).
% 1.20/0.56 thf(f1310,plain,(
% 1.20/0.56 ( ! [X0 : $o] : (($false = ((d_not @ ((d_not @ X0) => (e_is @ nat @ sK2 @ sK3))))) | ($false = X0)) ) | ~spl5_12),
% 1.20/0.56 inference(superposition,[],[f1077,f658])).
% 1.20/0.56 thf(f1380,plain,(
% 1.20/0.56 ($true = ((d_29_ii @ sK3 @ sK2))) | (((n_some @ (diffprop @ sK3 @ sK2))) = $false) | ($true = $false) | (~spl5_3 | ~spl5_4)),
% 1.20/0.56 inference(superposition,[],[f1024,f990])).
% 1.20/0.56 thf(f1386,plain,(
% 1.20/0.56 ($true = ((d_29_ii @ sK3 @ sK2))) | (((n_some @ (diffprop @ sK3 @ sK2))) = $false) | (~spl5_3 | ~spl5_4)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1380])).
% 1.20/0.56 thf(f1390,plain,(
% 1.20/0.56 ($true = ((d_29_ii @ sK3 @ sK2))) | ($true = $false) | (~spl5_3 | ~spl5_4 | ~spl5_5)),
% 1.20/0.56 inference(forward_demodulation,[],[f1386,f1000])).
% 1.20/0.56 thf(f1391,plain,(
% 1.20/0.56 ($true = ((d_29_ii @ sK3 @ sK2))) | (~spl5_3 | ~spl5_4 | ~spl5_5)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1390])).
% 1.20/0.56 thf(f1395,definition,(
% 1.20/0.56 spl5_24 <=> ($true = ((d_29_ii @ sK3 @ sK2)))),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_24])],[avatar_definition])).
% 1.20/0.56 thf(f1397,plain,(
% 1.20/0.56 ($true = ((d_29_ii @ sK3 @ sK2))) | ~spl5_24),
% 1.20/0.56 inference(avatar_component_clause,[],[f1395])).
% 1.20/0.56 thf(f1398,plain,(
% 1.20/0.56 spl5_24 | ~spl5_3 | ~spl5_4 | ~spl5_5),
% 1.20/0.56 inference(avatar_split_clause,[],[f1391,f998,f993,f988,f1395])).
% 1.20/0.56 thf(f1415,plain,(
% 1.20/0.56 (((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK2)))) = $true) | (((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((d_29_ii @ sK3 @ sK2))) | ~spl5_16),
% 1.20/0.56 inference(superposition,[],[f789,f1121])).
% 1.20/0.56 thf(f1423,plain,(
% 1.20/0.56 ($true = $false) | (((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((n_some @ (diffprop @ sK3 @ sK2))) = $false) | (((d_29_ii @ sK2 @ sK3)) = $false) | (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ~spl5_12),
% 1.20/0.56 inference(superposition,[],[f1310,f789])).
% 1.20/0.56 thf(f1435,plain,(
% 1.20/0.56 (((d_29_ii @ sK2 @ sK3)) = $false) | (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((n_some @ (diffprop @ sK3 @ sK2))) = $false) | ~spl5_12),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1423])).
% 1.20/0.56 thf(f1448,plain,(
% 1.20/0.56 (((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((n_some @ (diffprop @ sK3 @ sK2))) = $false) | (((d_29_ii @ sK2 @ sK3)) = $false) | ($true = $false) | (~spl5_4 | ~spl5_12)),
% 1.20/0.56 inference(forward_demodulation,[],[f1435,f995])).
% 1.20/0.56 thf(f1449,plain,(
% 1.20/0.56 (((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((n_some @ (diffprop @ sK3 @ sK2))) = $false) | (((d_29_ii @ sK2 @ sK3)) = $false) | (~spl5_4 | ~spl5_12)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1448])).
% 1.20/0.56 thf(f1464,plain,(
% 1.20/0.56 (((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK2)))) = $true) | (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((d_29_ii @ sK3 @ sK2))) | ($true = $false) | (~spl5_3 | ~spl5_16)),
% 1.20/0.56 inference(forward_demodulation,[],[f1415,f990])).
% 1.20/0.56 thf(f1465,plain,(
% 1.20/0.56 ($false = ((d_29_ii @ sK3 @ sK2))) | (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK2)))) = $true) | (~spl5_3 | ~spl5_16)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1464])).
% 1.20/0.56 thf(f1466,plain,(
% 1.20/0.56 ($true = $false) | (((d_29_ii @ sK2 @ sK3)) = $false) | (((n_some @ (diffprop @ sK3 @ sK2))) = $false) | (~spl5_3 | ~spl5_4 | ~spl5_12)),
% 1.20/0.56 inference(forward_demodulation,[],[f1449,f990])).
% 1.20/0.56 thf(f1467,plain,(
% 1.20/0.56 (((d_29_ii @ sK2 @ sK3)) = $false) | (((n_some @ (diffprop @ sK3 @ sK2))) = $false) | (~spl5_3 | ~spl5_4 | ~spl5_12)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1466])).
% 1.20/0.56 thf(f1476,plain,(
% 1.20/0.56 (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK2)))) = $true) | ($true = $false) | (~spl5_3 | ~spl5_16 | ~spl5_24)),
% 1.20/0.56 inference(forward_demodulation,[],[f1465,f1397])).
% 1.20/0.56 thf(f1477,plain,(
% 1.20/0.56 (((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK2)))) = $true) | (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (~spl5_3 | ~spl5_16 | ~spl5_24)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1476])).
% 1.20/0.56 thf(f1478,plain,(
% 1.20/0.56 (((d_29_ii @ sK2 @ sK3)) = $false) | ($true = $false) | (~spl5_3 | ~spl5_4 | ~spl5_5 | ~spl5_12)),
% 1.20/0.56 inference(forward_demodulation,[],[f1467,f1000])).
% 1.20/0.56 thf(f1479,plain,(
% 1.20/0.56 (((d_29_ii @ sK2 @ sK3)) = $false) | (~spl5_3 | ~spl5_4 | ~spl5_5 | ~spl5_12)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1478])).
% 1.20/0.56 thf(f1488,plain,(
% 1.20/0.56 ($true = $false) | (((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK2)))) = $true) | (~spl5_3 | ~spl5_4 | ~spl5_16 | ~spl5_24)),
% 1.20/0.56 inference(forward_demodulation,[],[f1477,f995])).
% 1.20/0.56 thf(f1489,plain,(
% 1.20/0.56 (((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK2)))) = $true) | (~spl5_3 | ~spl5_4 | ~spl5_16 | ~spl5_24)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1488])).
% 1.20/0.56 thf(f1490,plain,(
% 1.20/0.56 spl5_13 | ~spl5_3 | ~spl5_4 | ~spl5_5 | ~spl5_12),
% 1.20/0.56 inference(avatar_split_clause,[],[f1479,f1075,f998,f993,f988,f1079])).
% 1.20/0.56 thf(f1498,definition,(
% 1.20/0.56 spl5_25 <=> (((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK2)))) = $true)),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_25])],[avatar_definition])).
% 1.20/0.56 thf(f1500,plain,(
% 1.20/0.56 (((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK2)))) = $true) | ~spl5_25),
% 1.20/0.56 inference(avatar_component_clause,[],[f1498])).
% 1.20/0.56 thf(f1501,plain,(
% 1.20/0.56 spl5_25 | ~spl5_3 | ~spl5_4 | ~spl5_16 | ~spl5_24),
% 1.20/0.56 inference(avatar_split_clause,[],[f1489,f1395,f1119,f993,f988,f1498])).
% 1.20/0.56 thf(f1502,definition,(
% 1.20/0.56 (((d_29_ii @ sK2 @ sK3)) != $true) | (((d_29_ii @ sK2 @ sK3)) != $false) | ($true = $false)),
% 1.20/0.56 introduced(theory,[theory_tautology_sat_conflict])).
% 1.20/0.56 thf(f1551,plain,(
% 1.20/0.56 ($false = (((d_not @ $false) => (e_is @ nat @ sK3 @ sK2)))) | ($true = $false) | (~spl5_9 | ~spl5_25)),
% 1.20/0.56 inference(superposition,[],[f1500,f1096])).
% 1.20/0.56 thf(f1556,plain,(
% 1.20/0.56 ($true = $false) | ($true = ((d_not @ $false))) | (~spl5_9 | ~spl5_25)),
% 1.20/0.56 inference(imp_proxy_clausification,[],[f1551])).
% 1.20/0.56 thf(f1557,plain,(
% 1.20/0.56 ($true = ((d_not @ $false))) | (~spl5_9 | ~spl5_25)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1556])).
% 1.20/0.56 thf(f1570,definition,(
% 1.20/0.56 spl5_27 <=> ($true = ((d_not @ $false)))),
% 1.20/0.56 introduced(definition,[new_symbols(definition,[spl5_27])],[avatar_definition])).
% 1.20/0.56 thf(f1573,plain,(
% 1.20/0.56 spl5_27 | ~spl5_9 | ~spl5_25),
% 1.20/0.56 inference(avatar_split_clause,[],[f1557,f1498,f1061,f1570])).
% 1.20/0.56 thf(f1670,plain,(
% 1.20/0.56 (((d_not @ (n_some @ (diffprop @ sK3 @ sK2)))) = $true) | ($true = $false) | (((e_is @ nat @ sK2 @ sK3)) = $false) | (~spl5_3 | ~spl5_4)),
% 1.20/0.56 inference(superposition,[],[f990,f1265])).
% 1.20/0.56 thf(f1672,plain,(
% 1.20/0.56 (((d_not @ (n_some @ (diffprop @ sK3 @ sK2)))) = $true) | (((e_is @ nat @ sK2 @ sK3)) = $false) | (~spl5_3 | ~spl5_4)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1670])).
% 1.20/0.56 thf(f1677,plain,(
% 1.20/0.56 ($true = ((d_not @ $true))) | (((e_is @ nat @ sK2 @ sK3)) = $false) | (~spl5_3 | ~spl5_4 | ~spl5_5)),
% 1.20/0.56 inference(forward_demodulation,[],[f1672,f1000])).
% 1.20/0.56 thf(f1681,plain,(
% 1.20/0.56 ($true = $false) | (((e_is @ nat @ sK2 @ sK3)) = $false) | (~spl5_3 | ~spl5_4 | ~spl5_5 | ~spl5_9)),
% 1.20/0.56 inference(forward_demodulation,[],[f1677,f1063])).
% 1.20/0.56 thf(f1682,plain,(
% 1.20/0.56 (((e_is @ nat @ sK2 @ sK3)) = $false) | (~spl5_3 | ~spl5_4 | ~spl5_5 | ~spl5_9)),
% 1.20/0.56 inference(trivial_inequality_removal,[],[f1681])).
% 1.20/0.56 thf(f1685,plain,(
% 1.20/0.56 spl5_11 | ~spl5_3 | ~spl5_4 | ~spl5_5 | ~spl5_9),
% 1.20/0.56 inference(avatar_split_clause,[],[f1682,f1061,f998,f993,f988,f1070])).
% 1.20/0.56 thf(f1688,definition,(
% 1.20/0.56 (((d_29_ii @ sK2 @ sK3)) != $false) | ($true != ((d_not @ $false))) | (((d_not @ (d_29_ii @ sK2 @ sK3))) != $false) | ($true = $false)),
% 1.20/0.56 introduced(theory,[theory_tautology_sat_conflict])).
% 1.20/0.56 thf(f1691,definition,(
% 1.20/0.56 (((d_not @ (d_29_ii @ sK2 @ sK3))) != $false) | (((d_not @ (d_29_ii @ sK2 @ sK3))) != $true) | ($true = $false)),
% 1.20/0.56 introduced(theory,[theory_tautology_sat_conflict])).
% 1.20/0.56 thf(f1696,definition,(
% 1.20/0.56 (((d_29_ii @ sK2 @ sK3)) != $false) | (((e_is @ nat @ sK2 @ sK3)) != $false) | (((d_not @ (e_is @ nat @ sK2 @ sK3))) != $false) | (((d_not @ (d_29_ii @ sK2 @ sK3))) = $false)),
% 1.20/0.56 introduced(theory,[theory_tautology_sat_conflict])).
% 1.20/0.56 cnf(s1, plain, ~spl5_1, inference(sat_conversion,[],[f981])).
% 1.20/0.56 cnf(s3, plain, spl5_3, inference(sat_conversion,[],[f991])).
% 1.20/0.56 cnf(s4, plain, spl5_4, inference(sat_conversion,[],[f996])).
% 1.20/0.56 cnf(s5, plain, spl5_5, inference(sat_conversion,[],[f1001])).
% 1.20/0.56 cnf(s6, plain, spl5_6, inference(sat_conversion,[],[f1006])).
% 1.20/0.56 cnf(s7, plain, ~spl5_6 | spl5_7 | spl5_8, inference(sat_conversion,[],[f1059])).
% 1.20/0.56 cnf(s8, plain, ~spl5_6 | spl5_9 | spl5_10, inference(sat_conversion,[],[f1068])).
% 1.20/0.56 cnf(s10, plain, ~spl5_6 | spl5_12 | spl5_13, inference(sat_conversion,[],[f1082])).
% 1.20/0.56 cnf(s11, plain, ~spl5_6 | spl5_9 | spl5_11, inference(sat_conversion,[],[f1083])).
% 1.20/0.56 cnf(s14, plain, ~spl5_3 | ~spl5_4 | spl5_16 | spl5_17, inference(sat_conversion,[],[f1127])).
% 1.20/0.56 cnf(s35, plain, ~spl5_3 | ~spl5_4 | ~spl5_5 | spl5_24, inference(sat_conversion,[],[f1398])).
% 1.20/0.56 cnf(s37, plain, ~spl5_3 | ~spl5_4 | ~spl5_5 | ~spl5_12 | spl5_13, inference(sat_conversion,[],[f1490])).
% 1.20/0.56 cnf(s42, plain, ~spl5_3 | ~spl5_4 | ~spl5_16 | ~spl5_24 | spl5_25, inference(sat_conversion,[],[f1501])).
% 1.20/0.56 cnf(s43, plain, spl5_1 | ~spl5_13 | ~spl5_17, inference(sat_conversion,[],[f1502])).
% 1.20/0.56 cnf(s48, plain, ~spl5_9 | ~spl5_25 | spl5_27, inference(sat_conversion,[],[f1573])).
% 1.20/0.56 cnf(s56, plain, ~spl5_3 | ~spl5_4 | ~spl5_5 | ~spl5_9 | spl5_11, inference(sat_conversion,[],[f1685])).
% 1.20/0.56 cnf(s60, plain, spl5_1 | ~spl5_7 | ~spl5_13 | ~spl5_27, inference(sat_conversion,[],[f1688])).
% 1.20/0.56 cnf(s63, plain, spl5_1 | ~spl5_7 | ~spl5_10, inference(sat_conversion,[],[f1691])).
% 1.20/0.56 cnf(s68, plain, spl5_7 | ~spl5_8 | ~spl5_11 | ~spl5_13, inference(sat_conversion,[],[f1696])).
% 1.20/0.56 cnf(s72, plain, spl5_24, inference(rat,[],[s35,s4,s5,s3])).
% 1.20/0.56 cnf(s73, plain, spl5_13, inference(rat,[],[s37,s10,s5,s4,s3,s6])).
% 1.20/0.56 cnf(s75, plain, ~spl5_17, inference(rat,[],[s43,s1,s73])).
% 1.20/0.56 cnf(s76, plain, spl5_16, inference(rat,[],[s14,s3,s4,s75])).
% 1.20/0.56 cnf(s77, plain, spl5_11, inference(rat,[],[s56,s11,s5,s4,s3,s6])).
% 1.20/0.56 cnf(s78, plain, spl5_25, inference(rat,[],[s42,s72,s3,s4,s76])).
% 1.20/0.56 cnf(s79, plain, spl5_7, inference(rat,[],[s68,s7,s77,s73,s6])).
% 1.20/0.56 cnf(s80, plain, ~spl5_10, inference(rat,[],[s63,s1,s79])).
% 1.20/0.56 cnf(s81, plain, ~spl5_27, inference(rat,[],[s60,s73,s1,s79])).
% 1.20/0.56 cnf(s83, plain, spl5_9, inference(rat,[],[s8,s6,s80])).
% 1.20/0.56 cnf(s84, plain, $false, inference(rat,[],[s48,s78,s83,s81])).
% 1.20/0.56 thf(f1700,plain,(
% 1.20/0.56 $false),
% 1.20/0.56 inference(avatar_sat_refutation,[],[s84])).
% 1.20/0.56 % SZS output end Proof for theBenchmark
% 1.20/0.56 % (2785253)------------------------------
% 1.20/0.56 % (2785253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.56 % (2785253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.56 % (2785253)CaDiCaL version: 2.1.3
% 1.20/0.56 % (2785253)Termination reason: Refutation
% 1.20/0.56 % (2785253)Time elapsed: 0.066 s
% 1.20/0.56 % (2785253)Peak memory usage: 14 MB
% 1.20/0.56 % (2785253)Instructions burned: 135 (million)
% 1.20/0.56 % (2785162)Success in time 0.281 s
% 1.20/0.56 % Vampire exiting
%------------------------------------------------------------------------------