%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM656^4 : TPTP v9.3.1. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:25 AM UTC 2026
% Result : Theorem 1.85s 0.57s
% Output : Refutation 1.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM656^4 : TPTP v9.3.1. Released v7.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n020.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Tue Sep 29 12:33:20 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running higher-order theorem proving
% 0.09/0.26 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.76/0.40 % (986724)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.76/0.40 % (986735)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.76/0.40 % (986735)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.76/0.40 % (986735)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=207931368:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.76/0.40 % (986730)lrs+10_16_si=on:nwc=1.5:random_seed=2337851529:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.76/0.40 % (986729)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3924836835:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.76/0.40 % (986731)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1368271148:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.76/0.40 % (986732)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=952925704: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.76/0.40 % (986733)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=314275938:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.76/0.40 % (986731)Instruction limit reached!
% 0.76/0.40 % (986731)------------------------------
% 0.76/0.40 % (986731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.40 % (986731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.40 % (986731)CaDiCaL version: 2.1.3
% 0.76/0.40 % (986731)Termination reason: Instruction limit
% 0.76/0.40 % (986731)Termination phase: shuffling
% 0.76/0.40 % (986731)Time elapsed: 0.002 s
% 0.76/0.40 % (986731)Peak memory usage: 10 MB
% 0.76/0.40 % (986731)Instructions burned: 3 (million)
% 0.76/0.40 % (986730)Instruction limit reached!
% 0.76/0.40 % (986730)------------------------------
% 0.76/0.40 % (986730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.40 % (986730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.40 % (986730)CaDiCaL version: 2.1.3
% 0.76/0.40 % (986730)Termination reason: Instruction limit
% 0.76/0.40 % (986730)Termination phase: shuffling
% 0.76/0.40 % (986730)Time elapsed: 0.008 s
% 0.76/0.40 % (986730)Peak memory usage: 10 MB
% 0.76/0.40 % (986730)Instructions burned: 18 (million)
% 0.76/0.40 % (986734)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1690241677:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.76/0.40 % (986733)Instruction limit reached!
% 0.76/0.40 % (986733)------------------------------
% 0.76/0.40 % (986733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.40 % (986733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.40 % (986733)CaDiCaL version: 2.1.3
% 0.76/0.40 % (986733)Termination reason: Instruction limit
% 0.76/0.40 % (986733)Termination phase: Property scanning
% 0.76/0.40 % (986733)Time elapsed: 0.012 s
% 0.76/0.40 % (986733)Peak memory usage: 10 MB
% 0.76/0.40 % (986733)Instructions burned: 26 (million)
% 0.76/0.40 % (986742)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2898079068:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.76/0.40 % (986742)Instruction limit reached!
% 0.76/0.40 % (986742)------------------------------
% 0.76/0.40 % (986742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.40 % (986742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.40 % (986742)CaDiCaL version: 2.1.3
% 0.76/0.40 % (986742)Termination reason: Instruction limit
% 0.76/0.40 % (986742)Termination phase: shuffling
% 0.76/0.40 % (986742)Time elapsed: 0.002 s
% 0.76/0.40 % (986742)Peak memory usage: 10 MB
% 0.76/0.40 % (986742)Instructions burned: 4 (million)
% 0.76/0.40 % (986743)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3706426467:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.76/0.40 % (986745)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.76/0.42 % (986735)Instruction limit reached!
% 0.76/0.42 % (986735)------------------------------
% 0.76/0.42 % (986735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.42 % (986735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.42 % (986735)CaDiCaL version: 2.1.3
% 0.76/0.42 % (986735)Termination reason: Instruction limit
% 0.76/0.42 % (986735)Termination phase: Function definition elimination
% 0.76/0.42 % (986735)Time elapsed: 0.035 s
% 0.76/0.42 % (986735)Peak memory usage: 11 MB
% 0.76/0.42 % (986735)Instructions burned: 162 (million)
% 0.76/0.42 % (986743)Instruction limit reached!
% 0.76/0.42 % (986743)------------------------------
% 0.76/0.42 % (986743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.42 % (986743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.42 % (986743)CaDiCaL version: 2.1.3
% 0.76/0.42 % (986743)Termination reason: Instruction limit
% 0.76/0.42 % (986743)Termination phase: shuffling
% 0.76/0.42 % (986743)Time elapsed: 0.003 s
% 0.76/0.42 % (986743)Peak memory usage: 10 MB
% 0.76/0.42 % (986743)Instructions burned: 6 (million)
% 0.76/0.42 % (986745)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3292233512:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.76/0.42 % (986745)Instruction limit reached!
% 0.76/0.42 % (986745)------------------------------
% 0.76/0.42 % (986745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.42 % (986745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.42 % (986745)CaDiCaL version: 2.1.3
% 0.76/0.42 % (986745)Termination reason: Instruction limit
% 0.76/0.42 % (986745)Termination phase: shuffling
% 0.76/0.42 % (986745)Time elapsed: 0.004 s
% 0.76/0.42 % (986745)Peak memory usage: 10 MB
% 0.76/0.42 % (986745)Instructions burned: 9 (million)
% 0.76/0.42 % (986749)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.76/0.42 % (986749)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.76/0.42 % (986729)Instruction limit reached!
% 0.76/0.42 % (986729)------------------------------
% 0.76/0.42 % (986729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.42 % (986729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.42 % (986729)CaDiCaL version: 2.1.3
% 0.76/0.42 % (986729)Termination reason: Instruction limit
% 0.76/0.42 % (986729)Termination phase: Function definition elimination
% 0.76/0.42 % (986729)Time elapsed: 0.038 s
% 0.76/0.42 % (986729)Peak memory usage: 11 MB
% 0.76/0.42 % (986729)Instructions burned: 89 (million)
% 0.76/0.42 % (986749)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=832958123: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.76/0.42 % (986747)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2050373320:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.76/0.42 % (986749)Instruction limit reached!
% 0.76/0.42 % (986749)------------------------------
% 0.76/0.42 % (986749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.42 % (986749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.42 % (986749)CaDiCaL version: 2.1.3
% 0.76/0.42 % (986749)Termination reason: Instruction limit
% 0.76/0.42 % (986749)Termination phase: Property scanning
% 0.76/0.42 % (986749)Time elapsed: 0.008 s
% 0.76/0.42 % (986749)Peak memory usage: 10 MB
% 0.76/0.42 % (986749)Instructions burned: 32 (million)
% 0.76/0.42 % (986750)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=2375340437:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.76/0.42 % (986747)Instruction limit reached!
% 0.76/0.42 % (986747)------------------------------
% 0.76/0.42 % (986747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.42 % (986747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.45 % (986747)CaDiCaL version: 2.1.3
% 0.76/0.45 % (986747)Termination reason: Instruction limit
% 0.76/0.45 % (986747)Termination phase: shuffling
% 0.76/0.45 % (986747)Time elapsed: 0.006 s
% 0.76/0.45 % (986747)Peak memory usage: 10 MB
% 0.76/0.45 % (986747)Instructions burned: 13 (million)
% 0.76/0.45 % (986754)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.76/0.45 % (986734)Instruction limit reached!
% 0.76/0.45 % (986734)------------------------------
% 0.76/0.45 % (986734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.45 % (986734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.45 % (986734)CaDiCaL version: 2.1.3
% 0.76/0.45 % (986734)Termination reason: Instruction limit
% 0.76/0.45 % (986734)Termination phase: Function definition elimination
% 0.76/0.45 % (986734)Time elapsed: 0.045 s
% 0.76/0.45 % (986734)Peak memory usage: 11 MB
% 0.76/0.45 % (986734)Instructions burned: 75 (million)
% 0.76/0.45 % (986752)lrs+10_1_si=on:cs=on:random_seed=96150833:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.76/0.45 % (986758)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1018829502:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.76/0.45 % (986754)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=689768440:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.76/0.45 % (986752)Instruction limit reached!
% 0.76/0.45 % (986752)------------------------------
% 0.76/0.45 % (986752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.45 % (986752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.45 % (986752)CaDiCaL version: 2.1.3
% 0.76/0.45 % (986752)Termination reason: Instruction limit
% 0.76/0.45 % (986752)Termination phase: shuffling
% 0.76/0.45 % (986752)Time elapsed: 0.005 s
% 0.76/0.45 % (986752)Peak memory usage: 10 MB
% 0.76/0.45 % (986752)Instructions burned: 9 (million)
% 0.76/0.45 % (986754)Instruction limit reached!
% 0.76/0.45 % (986754)------------------------------
% 0.76/0.45 % (986754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.45 % (986754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.45 % (986754)CaDiCaL version: 2.1.3
% 0.76/0.45 % (986754)Termination reason: Instruction limit
% 0.76/0.45 % (986754)Termination phase: shuffling
% 0.76/0.45 % (986754)Time elapsed: 0.003 s
% 0.76/0.45 % (986754)Peak memory usage: 10 MB
% 0.76/0.45 % (986754)Instructions burned: 6 (million)
% 0.76/0.45 % (986758)Instruction limit reached!
% 0.76/0.45 % (986758)------------------------------
% 0.76/0.45 % (986758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.45 % (986758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.76/0.45 % (986758)CaDiCaL version: 2.1.3
% 0.76/0.45 % (986758)Termination reason: Instruction limit
% 0.76/0.45 % (986758)Termination phase: Saturation
% 0.76/0.45 % (986758)Time elapsed: 0.009 s
% 0.76/0.45 % (986758)Peak memory usage: 12 MB
% 0.76/0.45 % (986758)Instructions burned: 39 (million)
% 0.76/0.45 % (986760)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2102118270:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.76/0.45 % (986766)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3962076237:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.76/0.45 % (986768)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2429687394:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.76/0.45 % (986775)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=4021254527:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.76/0.45 % (986769)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=237280012:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.76/0.45 % (986775)Instruction limit reached!
% 0.76/0.45 % (986775)------------------------------
% 0.76/0.45 % (986775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.76/0.45 % (986775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.52 % (986775)CaDiCaL version: 2.1.3
% 1.35/0.52 % (986775)Termination reason: Instruction limit
% 1.35/0.52 % (986775)Termination phase: shuffling
% 1.35/0.52 % (986775)Time elapsed: 0.004 s
% 1.35/0.52 % (986775)Peak memory usage: 10 MB
% 1.35/0.52 % (986775)Instructions burned: 18 (million)
% 1.35/0.52 % (986750)Instruction limit reached!
% 1.35/0.52 % (986750)------------------------------
% 1.35/0.52 % (986750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.52 % (986750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.52 % (986750)CaDiCaL version: 2.1.3
% 1.35/0.52 % (986750)Termination reason: Instruction limit
% 1.35/0.52 % (986750)Termination phase: Function definition elimination
% 1.35/0.52 % (986750)Time elapsed: 0.037 s
% 1.35/0.52 % (986750)Peak memory usage: 11 MB
% 1.35/0.52 % (986750)Instructions burned: 88 (million)
% 1.35/0.52 % (986768)Instruction limit reached!
% 1.35/0.52 % (986768)------------------------------
% 1.35/0.52 % (986768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.52 % (986768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.52 % (986768)CaDiCaL version: 2.1.3
% 1.35/0.52 % (986768)Termination reason: Instruction limit
% 1.35/0.52 % (986768)Termination phase: shuffling
% 1.35/0.52 % (986768)Time elapsed: 0.007 s
% 1.35/0.52 % (986768)Peak memory usage: 10 MB
% 1.35/0.52 % (986768)Instructions burned: 15 (million)
% 1.35/0.52 % (986766)Instruction limit reached!
% 1.35/0.52 % (986766)------------------------------
% 1.35/0.52 % (986766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.52 % (986766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.52 % (986766)CaDiCaL version: 2.1.3
% 1.35/0.52 % (986766)Termination reason: Instruction limit
% 1.35/0.52 % (986766)Termination phase: Property scanning
% 1.35/0.52 % (986766)Time elapsed: 0.012 s
% 1.35/0.52 % (986766)Peak memory usage: 10 MB
% 1.35/0.52 % (986766)Instructions burned: 26 (million)
% 1.35/0.52 % (986760)Refutation not found, incomplete strategy
% 1.35/0.52 % (986760)------------------------------
% 1.35/0.52 % (986760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.52 % (986760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.52 % (986760)CaDiCaL version: 2.1.3
% 1.35/0.52 % (986760)Termination reason: Refutation not found, incomplete strategy
% 1.35/0.52 % (986760)Time elapsed: 0.020 s
% 1.35/0.52 % (986760)Peak memory usage: 13 MB
% 1.35/0.52 % (986760)Instructions burned: 44 (million)
% 1.35/0.52 % (986760)------------------------------
% 1.35/0.52 % (986760)------------------------------
% 1.35/0.52 % (986785)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=4102520157: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.35/0.52 % (986785)Instruction limit reached!
% 1.35/0.52 % (986785)------------------------------
% 1.35/0.52 % (986785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.52 % (986785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.52 % (986785)CaDiCaL version: 2.1.3
% 1.35/0.52 % (986785)Termination reason: Instruction limit
% 1.35/0.52 % (986785)Termination phase: shuffling
% 1.35/0.52 % (986785)Time elapsed: 0.001 s
% 1.35/0.52 % (986785)Peak memory usage: 10 MB
% 1.35/0.52 % (986785)Instructions burned: 4 (million)
% 1.35/0.52 % (986795)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.35/0.52 % (986787)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3823679136:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.35/0.52 % (986792)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.35/0.52 % (986792)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.35/0.52 % (986789)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2992260604:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.35/0.52 % (986795)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=549650660:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.85/0.57 % (986790)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3483038293:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.85/0.57 % (986792)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=464830292:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.85/0.57 % (986795)Instruction limit reached!
% 1.85/0.57 % (986795)------------------------------
% 1.85/0.57 % (986795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986795)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986795)Termination reason: Instruction limit
% 1.85/0.57 % (986795)Termination phase: shuffling
% 1.85/0.57 % (986795)Time elapsed: 0.002 s
% 1.85/0.57 % (986795)Peak memory usage: 10 MB
% 1.85/0.57 % (986795)Instructions burned: 11 (million)
% 1.85/0.57 % (986792)Instruction limit reached!
% 1.85/0.57 % (986792)------------------------------
% 1.85/0.57 % (986792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986792)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986792)Termination reason: Instruction limit
% 1.85/0.57 % (986792)Termination phase: shuffling
% 1.85/0.57 % (986792)Time elapsed: 0.006 s
% 1.85/0.57 % (986792)Peak memory usage: 10 MB
% 1.85/0.57 % (986792)Instructions burned: 14 (million)
% 1.85/0.57 % (986789)Instruction limit reached!
% 1.85/0.57 % (986789)------------------------------
% 1.85/0.57 % (986789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986789)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986789)Termination reason: Instruction limit
% 1.85/0.57 % (986789)Termination phase: Property scanning
% 1.85/0.57 % (986789)Time elapsed: 0.011 s
% 1.85/0.57 % (986789)Peak memory usage: 10 MB
% 1.85/0.57 % (986789)Instructions burned: 24 (million)
% 1.85/0.57 % (986787)Instruction limit reached!
% 1.85/0.57 % (986787)------------------------------
% 1.85/0.57 % (986787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986787)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986787)Termination reason: Instruction limit
% 1.85/0.57 % (986787)Termination phase: Property scanning
% 1.85/0.57 % (986787)Time elapsed: 0.012 s
% 1.85/0.57 % (986787)Peak memory usage: 10 MB
% 1.85/0.57 % (986787)Instructions burned: 27 (million)
% 1.85/0.57 % (986806)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=3336311644:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.85/0.57 % (986806)Instruction limit reached!
% 1.85/0.57 % (986806)------------------------------
% 1.85/0.57 % (986806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986806)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986806)Termination reason: Instruction limit
% 1.85/0.57 % (986806)Termination phase: Property scanning
% 1.85/0.57 % (986806)Time elapsed: 0.008 s
% 1.85/0.57 % (986806)Peak memory usage: 10 MB
% 1.85/0.57 % (986806)Instructions burned: 35 (million)
% 1.85/0.57 % (986809)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=4051507695:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.85/0.57 % (986811)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1188744876:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.85/0.57 % (986812)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1337046282:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.85/0.57 % (986790)Instruction limit reached!
% 1.85/0.57 % (986790)------------------------------
% 1.85/0.57 % (986790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986790)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986790)Termination reason: Instruction limit
% 1.85/0.57 % (986790)Termination phase: Saturation
% 1.85/0.57 % (986790)Time elapsed: 0.030 s
% 1.85/0.57 % (986790)Peak memory usage: 11 MB
% 1.85/0.57 % (986790)Instructions burned: 61 (million)
% 1.85/0.57 % (986819)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3942051358:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.85/0.57 % (986809)Instruction limit reached!
% 1.85/0.57 % (986809)------------------------------
% 1.85/0.57 % (986809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986809)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986809)Termination reason: Instruction limit
% 1.85/0.57 % (986809)Termination phase: shuffling
% 1.85/0.57 % (986809)Time elapsed: 0.004 s
% 1.85/0.57 % (986809)Peak memory usage: 10 MB
% 1.85/0.57 % (986809)Instructions burned: 8 (million)
% 1.85/0.57 % (986812)Instruction limit reached!
% 1.85/0.57 % (986812)------------------------------
% 1.85/0.57 % (986812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986812)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986812)Termination reason: Instruction limit
% 1.85/0.57 % (986812)Termination phase: Property scanning
% 1.85/0.57 % (986812)Time elapsed: 0.010 s
% 1.85/0.57 % (986812)Peak memory usage: 10 MB
% 1.85/0.57 % (986812)Instructions burned: 20 (million)
% 1.85/0.57 % (986811)Instruction limit reached!
% 1.85/0.57 % (986811)------------------------------
% 1.85/0.57 % (986811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986811)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986811)Termination reason: Instruction limit
% 1.85/0.57 % (986811)Termination phase: Property scanning
% 1.85/0.57 % (986811)Time elapsed: 0.011 s
% 1.85/0.57 % (986811)Peak memory usage: 10 MB
% 1.85/0.57 % (986811)Instructions burned: 23 (million)
% 1.85/0.57 % (986831)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1050244188:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.85/0.57 % (986829)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3953706509:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.85/0.57 % (986835)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.85/0.57 % (986834)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=699063667:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.85/0.57 % (986835)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1085989825:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.85/0.57 % (986835)Instruction limit reached!
% 1.85/0.57 % (986835)------------------------------
% 1.85/0.57 % (986835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986835)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986835)Termination reason: Instruction limit
% 1.85/0.57 % (986835)Termination phase: shuffling
% 1.85/0.57 % (986835)Time elapsed: 0.004 s
% 1.85/0.57 % (986835)Peak memory usage: 10 MB
% 1.85/0.57 % (986835)Instructions burned: 9 (million)
% 1.85/0.57 % (986834)Instruction limit reached!
% 1.85/0.57 % (986834)------------------------------
% 1.85/0.57 % (986834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986834)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986834)Termination reason: Instruction limit
% 1.85/0.57 % (986834)Termination phase: Property scanning
% 1.85/0.57 % (986834)Time elapsed: 0.018 s
% 1.85/0.57 % (986834)Peak memory usage: 11 MB
% 1.85/0.57 % (986834)Instructions burned: 42 (million)
% 1.85/0.57 % (986844)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=396322370:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 1.85/0.57 % (986848)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=2102646313: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.85/0.57 % (986829)Instruction limit reached!
% 1.85/0.57 % (986829)------------------------------
% 1.85/0.57 % (986829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986829)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986829)Termination reason: Instruction limit
% 1.85/0.57 % (986829)Termination phase: Function definition elimination
% 1.85/0.57 % (986829)Time elapsed: 0.061 s
% 1.85/0.57 % (986829)Peak memory usage: 11 MB
% 1.85/0.57 % (986829)Instructions burned: 143 (million)
% 1.85/0.57 % (986848)Refutation not found, incomplete strategy
% 1.85/0.57 % (986848)------------------------------
% 1.85/0.57 % (986848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986848)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986848)Termination reason: Refutation not found, incomplete strategy
% 1.85/0.57 % (986848)Time elapsed: 0.032 s
% 1.85/0.57 % (986848)Peak memory usage: 13 MB
% 1.85/0.57 % (986848)Instructions burned: 72 (million)
% 1.85/0.57 % (986866)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.85/0.57 % (986848)------------------------------
% 1.85/0.57 % (986848)------------------------------
% 1.85/0.57 % (986866)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=1377156108: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.85/0.57 % (986831) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-986724-986831"...
% 1.85/0.57 % (986866)Instruction limit reached!
% 1.85/0.57 % (986866)------------------------------
% 1.85/0.57 % (986866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986866)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986866)Termination reason: Instruction limit
% 1.85/0.57 % (986866)Termination phase: shuffling
% 1.85/0.57 % (986866)Time elapsed: 0.003 s
% 1.85/0.57 % (986866)Peak memory usage: 10 MB
% 1.85/0.57 % (986866)Instructions burned: 7 (million)
% 1.85/0.57 % (986769)Instruction limit reached!
% 1.85/0.57 % (986769)------------------------------
% 1.85/0.57 % (986769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986769)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986769)Termination reason: Instruction limit
% 1.85/0.57 % (986769)Termination phase: Saturation
% 1.85/0.57 % (986769)Time elapsed: 0.165 s
% 1.85/0.57 % (986769)Peak memory usage: 15 MB
% 1.85/0.57 % (986769)Instructions burned: 328 (million)
% 1.85/0.57 % (986831)...printing done.
% 1.85/0.57 % (986831)Refutation found. Thanks to Tanya!
% 1.85/0.57 % SZS status Theorem for theBenchmark
% 1.85/0.57 % SZS output start Proof for theBenchmark
% 1.85/0.57 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.85/0.57 thf(func_def_0, type, is_of: ($i > ($i > $o) > $o)).
% 1.85/0.57 thf(func_def_2, type, all_of: (($i > $o) > ($i > $o) > $o)).
% 1.85/0.57 thf(func_def_3, type, eps: (($i > $o) > $i)).
% 1.85/0.57 thf(func_def_4, type, in: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_5, type, d_Subq: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_7, type, union: ($i > $i)).
% 1.85/0.57 thf(func_def_8, type, power: ($i > $i)).
% 1.85/0.57 thf(func_def_9, type, repl: ($i > ($i > $i) > $i)).
% 1.85/0.57 thf(func_def_10, type, d_Union_closed: ($i > $o)).
% 1.85/0.57 thf(func_def_11, type, d_Power_closed: ($i > $o)).
% 1.85/0.57 thf(func_def_12, type, d_Repl_closed: ($i > $o)).
% 1.85/0.57 thf(func_def_13, type, d_ZF_closed: ($i > $o)).
% 1.85/0.57 thf(func_def_14, type, univof: ($i > $i)).
% 1.85/0.57 thf(func_def_15, type, if: ($o > $i > $i > $i)).
% 1.85/0.57 thf(func_def_16, type, nIn: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_17, type, d_UPair: ($i > $i > $i)).
% 1.85/0.57 thf(func_def_18, type, d_Sing: ($i > $i)).
% 1.85/0.57 thf(func_def_19, type, binunion: ($i > $i > $i)).
% 1.85/0.57 thf(func_def_20, type, famunion: ($i > ($i > $i) > $i)).
% 1.85/0.57 thf(func_def_21, type, d_Sep: ($i > ($i > $o) > $i)).
% 1.85/0.57 thf(func_def_22, type, d_ReplSep: ($i > ($i > $o) > ($i > $i) > $i)).
% 1.85/0.57 thf(func_def_23, type, setminus: ($i > $i > $i)).
% 1.85/0.57 thf(func_def_24, type, d_In_rec_G: (($i > ($i > $i) > $i) > $i > $i > $o)).
% 1.85/0.57 thf(func_def_25, type, d_In_rec: (($i > ($i > $i) > $i) > $i > $i)).
% 1.85/0.57 thf(func_def_26, type, ordsucc: ($i > $i)).
% 1.85/0.57 thf(func_def_27, type, nat_p: ($i > $o)).
% 1.85/0.57 thf(func_def_29, type, d_Inj1: ($i > $i)).
% 1.85/0.57 thf(func_def_30, type, d_Inj0: ($i > $i)).
% 1.85/0.57 thf(func_def_31, type, d_Unj: ($i > $i)).
% 1.85/0.57 thf(func_def_32, type, pair: ($i > $i > $i)).
% 1.85/0.57 thf(func_def_33, type, proj0: ($i > $i)).
% 1.85/0.57 thf(func_def_34, type, proj1: ($i > $i)).
% 1.85/0.57 thf(func_def_35, type, d_Sigma: ($i > ($i > $i) > $i)).
% 1.85/0.57 thf(func_def_36, type, setprod: ($i > $i > $i)).
% 1.85/0.57 thf(func_def_37, type, ap: ($i > $i > $i)).
% 1.85/0.57 thf(func_def_38, type, pair_p: ($i > $o)).
% 1.85/0.57 thf(func_def_39, type, d_Pi: ($i > ($i > $i) > $i)).
% 1.85/0.57 thf(func_def_40, type, imp: ($o > $o > $o)).
% 1.85/0.57 thf(func_def_41, type, d_not: ($o > $o)).
% 1.85/0.57 thf(func_def_42, type, wel: ($o > $o)).
% 1.85/0.57 thf(func_def_43, type, obvious: $o).
% 1.85/0.57 thf(func_def_44, type, l_ec: ($o > $o > $o)).
% 1.85/0.57 thf(func_def_45, type, d_and: ($o > $o > $o)).
% 1.85/0.57 thf(func_def_46, type, l_or: ($o > $o > $o)).
% 1.85/0.57 thf(func_def_47, type, orec: ($o > $o > $o)).
% 1.85/0.57 thf(func_def_48, type, l_iff: ($o > $o > $o)).
% 1.85/0.57 thf(func_def_49, type, all: ($i > ($i > $o) > $o)).
% 1.85/0.57 thf(func_def_50, type, non: ($i > ($i > $o) > $i > $o)).
% 1.85/0.57 thf(func_def_51, type, l_some: ($i > ($i > $o) > $o)).
% 1.85/0.57 thf(func_def_52, type, or3: ($o > $o > $o > $o)).
% 1.85/0.57 thf(func_def_53, type, and3: ($o > $o > $o > $o)).
% 1.85/0.57 thf(func_def_54, type, ec3: ($o > $o > $o > $o)).
% 1.85/0.57 thf(func_def_55, type, orec3: ($o > $o > $o > $o)).
% 1.85/0.57 thf(func_def_56, type, e_is: ($i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_57, type, amone: ($i > ($i > $o) > $o)).
% 1.85/0.57 thf(func_def_58, type, one: ($i > ($i > $o) > $o)).
% 1.85/0.57 thf(func_def_59, type, ind: ($i > ($i > $o) > $i)).
% 1.85/0.57 thf(func_def_60, type, injective: ($i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_61, type, image: ($i > $i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_62, type, tofs: ($i > $i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_63, type, soft: ($i > $i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_64, type, inverse: ($i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_65, type, surjective: ($i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_66, type, bijective: ($i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_67, type, invf: ($i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_68, type, inj_h: ($i > $i > $i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_69, type, e_in: ($i > ($i > $o) > $i > $i)).
% 1.85/0.57 thf(func_def_70, type, out: ($i > ($i > $o) > $i > $i)).
% 1.85/0.57 thf(func_def_71, type, d_pair: ($i > $i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_72, type, first: ($i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_73, type, second: ($i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_74, type, prop1: ($o > $i > $i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_75, type, ite: ($o > $i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_76, type, wissel_wa: ($i > $i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_77, type, wissel_wb: ($i > $i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_78, type, wissel: ($i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_79, type, changef: ($i > $i > $i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_80, type, r_ec: ($o > $o > $o)).
% 1.85/0.57 thf(func_def_81, type, esti: ($i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_82, type, empty: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_83, type, nonempty: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_84, type, incl: ($i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_85, type, st_disj: ($i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_86, type, nissetprop: ($i > $i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_87, type, unmore: ($i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_88, type, ecelt: ($i > ($i > $i > $o) > $i > $i)).
% 1.85/0.57 thf(func_def_89, type, ecp: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.85/0.57 thf(func_def_90, type, anec: ($i > ($i > $i > $o) > $i > $o)).
% 1.85/0.57 thf(func_def_91, type, ect: ($i > ($i > $i > $o) > $i)).
% 1.85/0.57 thf(func_def_92, type, ectset: ($i > ($i > $i > $o) > $i > $i)).
% 1.85/0.57 thf(func_def_93, type, ectelt: ($i > ($i > $i > $o) > $i > $i)).
% 1.85/0.57 thf(func_def_94, type, ecect: ($i > ($i > $i > $o) > $i > $i)).
% 1.85/0.57 thf(func_def_95, type, fixfu: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.85/0.57 thf(func_def_96, type, d_10_prop1: ($i > ($i > $i > $o) > $i > $i > $i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_97, type, prop2: ($i > ($i > $i > $o) > $i > $i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_98, type, indeq: ($i > ($i > $i > $o) > $i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_99, type, fixfu2: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.85/0.57 thf(func_def_100, type, d_11_i: ($i > ($i > $i > $o) > $i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_101, type, indeq2: ($i > ($i > $i > $o) > $i > $i > $i > $i > $i)).
% 1.85/0.57 thf(func_def_103, type, n_is: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_104, type, nis: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_105, type, n_in: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_106, type, n_some: (($i > $o) > $o)).
% 1.85/0.57 thf(func_def_107, type, n_all: (($i > $o) > $o)).
% 1.85/0.57 thf(func_def_108, type, n_one: (($i > $o) > $o)).
% 1.85/0.57 thf(func_def_110, type, cond1: ($i > $o)).
% 1.85/0.57 thf(func_def_111, type, cond2: ($i > $o)).
% 1.85/0.57 thf(func_def_112, type, i1_s: (($i > $o) > $i)).
% 1.85/0.57 thf(func_def_113, type, d_22_prop1: ($i > $o)).
% 1.85/0.57 thf(func_def_114, type, d_23_prop1: ($i > $o)).
% 1.85/0.57 thf(func_def_115, type, d_24_prop1: ($i > $o)).
% 1.85/0.57 thf(func_def_116, type, d_24_prop2: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_117, type, prop3: ($i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_118, type, prop4: ($i > $o)).
% 1.85/0.57 thf(func_def_119, type, d_24_g: ($i > $i)).
% 1.85/0.57 thf(func_def_120, type, plus: ($i > $i)).
% 1.85/0.57 thf(func_def_121, type, n_pl: ($i > $i > $i)).
% 1.85/0.57 thf(func_def_122, type, d_25_prop1: ($i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_123, type, d_26_prop1: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_124, type, d_27_prop1: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_125, type, d_28_prop1: ($i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_126, type, diffprop: ($i > $i > $i > $o)).
% 1.85/0.57 thf(func_def_127, type, d_29_ii: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_128, type, iii: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_129, type, d_29_prop1: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_130, type, moreis: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_131, type, lessis: ($i > $i > $o)).
% 1.85/0.57 thf(func_def_132, type, db1: !>[X0: $tType]:(X0)).
% 1.85/0.57 thf(func_def_133, type, db0: !>[X0: $tType]:(X0)).
% 1.85/0.57 thf(func_def_134, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.85/0.57 thf(func_def_135, type, db5: !>[X0: $tType]:(X0)).
% 1.85/0.57 thf(func_def_136, type, db4: !>[X0: $tType]:(X0)).
% 1.85/0.57 thf(func_def_137, type, db3: !>[X0: $tType]:(X0)).
% 1.85/0.57 thf(func_def_138, type, db2: !>[X0: $tType]:(X0)).
% 1.85/0.57 thf(func_def_141, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.85/0.57 thf(func_def_142, type, vIMP: ($o > $o > $o)).
% 1.85/0.57 thf(func_def_143, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.85/0.57 thf(func_def_144, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.85/0.57 thf(func_def_145, type, vAND: ($o > $o > $o)).
% 1.85/0.57 thf(func_def_146, type, vNOT: ($o > $o)).
% 1.85/0.57 thf(func_def_147, type, db6: !>[X0: $tType]:(X0)).
% 1.85/0.57 thf(func_def_148, type, vOR: ($o > $o > $o)).
% 1.85/0.57 thf(func_def_149, type, db7: !>[X0: $tType]:(X0)).
% 1.85/0.57 thf(func_def_150, type, sK0: (($i > $o) > $i)).
% 1.85/0.57 thf(func_def_151, type, sK1: (($i > $i) > $i > ($i > $i) > $i)).
% 1.85/0.57 thf(func_def_154, type, sK4: ($i > $i > $i > $i > $i)).
% 1.85/0.57 thf(f2,axiom,(
% 1.85/0.57 (all_of = (^[X0 : ($i > $o), X1 : ($i > $o)] : (! [X2 : $i] : ((is_of @ X2 @ X0) => (X1 @ X2)))))),
% 1.85/0.57 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_all_of)).
% 1.85/0.57 thf(f74,axiom,(
% 1.85/0.57 ((^[X0 : $o, X1 : $o] : (X0 => X1)) = imp)),
% 1.85/0.57 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_imp)).
% 1.85/0.57 thf(f81,axiom,(
% 1.85/0.57 ((^[X0 : $o] : ((imp @ (d_not @ X0)))) = l_or)),
% 1.85/0.57 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_l_or)).
% 1.85/0.57 thf(f157,axiom,(
% 1.85/0.57 (n_is = ((e_is @ nat)))),
% 1.85/0.57 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_n_is)).
% 1.85/0.57 thf(f205,axiom,(
% 1.85/0.57 ((^[X0 : $i, X1 : $i] : ((n_some @ (diffprop @ X0 @ X1)))) = d_29_ii)),
% 1.85/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_d_29_ii)).
% 1.85/0.57 thf(f214,axiom,(
% 1.85/0.57 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((d_29_ii @ X0 @ X1) => (iii @ X1 @ X0)))))))),
% 1.85/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz11)).
% 1.85/0.57 thf(f215,axiom,(
% 1.85/0.57 (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.85/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz12)).
% 1.85/0.57 thf(f216,axiom,(
% 1.85/0.57 (moreis = (^[X0 : $i, X1 : $i] : ((l_or @ (d_29_ii @ X0 @ X1) @ (n_is @ X0 @ X1)))))),
% 1.85/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_moreis)).
% 1.85/0.57 thf(f217,axiom,(
% 1.85/0.57 (lessis = (^[X0 : $i, X1 : $i] : ((l_or @ (iii @ X0 @ X1) @ (n_is @ X0 @ X1)))))),
% 1.85/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_lessis)).
% 1.85/0.57 thf(f218,axiom,(
% 1.85/0.57 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((moreis @ X0 @ X1) => (lessis @ X1 @ X0)))))))),
% 1.85/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz13)).
% 1.85/0.57 thf(f220,axiom,(
% 1.85/0.57 (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.85/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz10c)).
% 1.85/0.57 thf(f221,axiom,(
% 1.85/0.57 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((lessis @ X0 @ X1) => (d_not @ (d_29_ii @ X0 @ X1))))))))),
% 1.85/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz10d)).
% 1.85/0.57 thf(f222,axiom,(
% 1.85/0.57 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((d_not @ (d_29_ii @ X0 @ X1)) => (lessis @ X0 @ X1)))))))),
% 1.85/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz10e)).
% 1.85/0.57 thf(f224,conjecture,(
% 1.85/0.57 (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.85/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz10g)).
% 1.85/0.57 thf(f225,negated_conjecture,(
% 1.85/0.57 ~(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.85/0.57 inference(negated_conjecture,[status(cth)],[f224])).
% 1.85/0.57 thf(f257,plain,(
% 1.85/0.57 (all_of = (^[X0 : ($i > $o), X1 : ($i > $o)] : (! [X2 : $i] : ((is_of @ X2 @ X0) => (X1 @ X2)))))),
% 1.85/0.57 inference(rectify,[],[f2])).
% 1.85/0.57 thf(f258,plain,(
% 1.85/0.57 (all_of = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))))),
% 1.85/0.57 inference(fool_elimination,[],[f257])).
% 1.85/0.57 thf(f314,plain,(
% 1.85/0.57 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((d_29_ii @ X1 @ X3) => (iii @ X3 @ X1)))))))),
% 1.85/0.57 inference(rectify,[],[f214])).
% 1.85/0.57 thf(f315,plain,(
% 1.85/0.57 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_29_ii @ Y0 @ Y1) => (iii @ Y1 @ Y0))))))))),
% 1.85/0.57 inference(fool_elimination,[],[f314])).
% 1.85/0.57 thf(f316,plain,(
% 1.85/0.57 ~(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.85/0.57 inference(rectify,[],[f225])).
% 1.85/0.57 thf(f317,plain,(
% 1.85/0.57 ~ ($true = ((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)))))))))),
% 1.85/0.57 inference(fool_elimination,[],[f316])).
% 1.85/0.57 thf(f346,plain,(
% 1.85/0.57 (moreis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (d_29_ii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.85/0.57 inference(fool_elimination,[],[f216])).
% 1.85/0.57 thf(f354,plain,(
% 1.85/0.57 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((d_not @ (d_29_ii @ X1 @ X3)) => (lessis @ X1 @ X3)))))))),
% 1.85/0.57 inference(rectify,[],[f222])).
% 1.85/0.57 thf(f355,plain,(
% 1.85/0.57 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_not @ (d_29_ii @ Y0 @ Y1)) => (lessis @ Y0 @ Y1))))))))),
% 1.85/0.57 inference(fool_elimination,[],[f354])).
% 1.85/0.57 thf(f364,plain,(
% 1.85/0.57 (d_29_ii = (^[Y0 : $i]: ((^[Y1 : $i]: (n_some @ (diffprop @ Y0 @ Y1))))))),
% 1.85/0.57 inference(fool_elimination,[],[f205])).
% 1.85/0.57 thf(f380,plain,(
% 1.85/0.57 (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.85/0.57 inference(rectify,[],[f220])).
% 1.85/0.57 thf(f381,plain,(
% 1.85/0.57 ($true = ((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)))))))))),
% 1.85/0.57 inference(fool_elimination,[],[f380])).
% 1.85/0.57 thf(f409,plain,(
% 1.85/0.57 (l_or = (^[Y0 : $o]: (imp @ (d_not @ Y0))))),
% 1.85/0.57 inference(fool_elimination,[],[f81])).
% 1.85/0.57 thf(f427,plain,(
% 1.85/0.57 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((lessis @ X1 @ X3) => (d_not @ (d_29_ii @ X1 @ X3))))))))),
% 1.85/0.57 inference(rectify,[],[f221])).
% 1.85/0.57 thf(f428,plain,(
% 1.85/0.57 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((lessis @ Y0 @ Y1) => (d_not @ (d_29_ii @ Y0 @ Y1)))))))))),
% 1.85/0.57 inference(fool_elimination,[],[f427])).
% 1.85/0.57 thf(f442,plain,(
% 1.85/0.57 ((^[X0 : $o, X1 : $o] : (X0 => X1)) = imp)),
% 1.85/0.57 inference(rectify,[],[f74])).
% 1.85/0.57 thf(f443,plain,(
% 1.85/0.57 (imp = (^[Y0 : $o]: ((^[Y1 : $o]: (Y0 => Y1)))))),
% 1.85/0.57 inference(fool_elimination,[],[f442])).
% 1.85/0.57 thf(f460,plain,(
% 1.85/0.57 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((moreis @ X1 @ X3) => (lessis @ X3 @ X1)))))))),
% 1.85/0.57 inference(rectify,[],[f218])).
% 1.85/0.57 thf(f461,plain,(
% 1.85/0.57 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((moreis @ Y0 @ Y1) => (lessis @ Y1 @ Y0))))))))),
% 1.85/0.57 inference(fool_elimination,[],[f460])).
% 1.85/0.57 thf(f466,plain,(
% 1.85/0.57 (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.85/0.57 inference(rectify,[],[f215])).
% 1.85/0.57 thf(f467,plain,(
% 1.85/0.57 ($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.85/0.57 inference(fool_elimination,[],[f466])).
% 1.85/0.57 thf(f548,plain,(
% 1.85/0.57 (lessis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (iii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.85/0.57 inference(fool_elimination,[],[f217])).
% 1.85/0.57 thf(f581,plain,(
% 1.85/0.57 ($true != ((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)))))))))),
% 1.85/0.57 inference(flattening,[],[f317])).
% 1.85/0.57 thf(f599,plain,(
% 1.85/0.57 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((moreis @ Y0 @ Y1) => (lessis @ Y1 @ Y0))))))))),
% 1.85/0.57 inference(cnf_transformation,[],[f461])).
% 1.85/0.57 thf(f602,plain,(
% 1.85/0.57 (d_29_ii = (^[Y0 : $i]: ((^[Y1 : $i]: (n_some @ (diffprop @ Y0 @ Y1))))))),
% 1.85/0.57 inference(cnf_transformation,[],[f364])).
% 1.85/0.57 thf(f603,plain,(
% 1.85/0.57 (n_is = ((e_is @ nat)))),
% 1.85/0.57 inference(cnf_transformation,[],[f157])).
% 1.85/0.57 thf(f612,plain,(
% 1.85/0.57 (all_of = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))))),
% 1.85/0.57 inference(cnf_transformation,[],[f258])).
% 1.85/0.57 thf(f613,plain,(
% 1.85/0.57 ($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.85/0.57 inference(cnf_transformation,[],[f467])).
% 1.85/0.57 thf(f620,plain,(
% 1.85/0.57 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((lessis @ Y0 @ Y1) => (d_not @ (d_29_ii @ Y0 @ Y1)))))))))),
% 1.85/0.57 inference(cnf_transformation,[],[f428])).
% 1.85/0.57 thf(f622,plain,(
% 1.85/0.57 ($true = ((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)))))))))),
% 1.85/0.57 inference(cnf_transformation,[],[f381])).
% 1.85/0.57 thf(f624,plain,(
% 1.85/0.57 (moreis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (d_29_ii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.85/0.57 inference(cnf_transformation,[],[f346])).
% 1.85/0.57 thf(f629,plain,(
% 1.85/0.57 (imp = (^[Y0 : $o]: ((^[Y1 : $o]: (Y0 => Y1)))))),
% 1.85/0.57 inference(cnf_transformation,[],[f443])).
% 1.85/0.57 thf(f638,plain,(
% 1.85/0.57 ($true != ((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)))))))))),
% 1.85/0.57 inference(cnf_transformation,[],[f581])).
% 1.85/0.57 thf(f644,plain,(
% 1.85/0.57 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_not @ (d_29_ii @ Y0 @ Y1)) => (lessis @ Y0 @ Y1))))))))),
% 1.85/0.57 inference(cnf_transformation,[],[f355])).
% 1.85/0.57 thf(f650,plain,(
% 1.85/0.57 (l_or = (^[Y0 : $o]: (imp @ (d_not @ Y0))))),
% 1.85/0.57 inference(cnf_transformation,[],[f409])).
% 1.85/0.57 thf(f652,plain,(
% 1.85/0.57 (lessis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (iii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.85/0.57 inference(cnf_transformation,[],[f548])).
% 1.85/0.57 thf(f653,plain,(
% 1.85/0.57 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_29_ii @ Y0 @ Y1) => (iii @ Y1 @ Y0))))))))),
% 1.85/0.57 inference(cnf_transformation,[],[f315])).
% 1.85/0.57 thf(f654,definition,(
% 1.85/0.57 ($true != $false)),
% 1.85/0.57 introduced(theory,[fool_distinctness_axiom])).
% 1.85/0.57 thf(f655,definition,(
% 1.85/0.57 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.85/0.57 introduced(theory,[fool_exhaustiveness_axiom])).
% 1.85/0.57 thf(f656,plain,(
% 1.85/0.57 (l_or = (^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: (Y1 => Y2)))) @ (d_not @ Y0))))),
% 1.85/0.57 inference(definition_unfolding,[],[f650,f629])).
% 1.85/0.57 thf(f657,plain,(
% 1.85/0.57 (moreis = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $o]: ((^[Y3 : $o]: ((^[Y4 : $o]: (Y3 => Y4)))) @ (d_not @ Y2))) @ ((^[Y2 : $i]: ((^[Y3 : $i]: (n_some @ (diffprop @ Y2 @ Y3))))) @ Y0 @ Y1) @ (e_is @ nat @ Y0 @ Y1))))))),
% 1.85/0.57 inference(definition_unfolding,[],[f624,f656,f602,f603])).
% 1.85/0.57 thf(f658,plain,(
% 1.85/0.57 (lessis = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $o]: ((^[Y3 : $o]: ((^[Y4 : $o]: (Y3 => Y4)))) @ (d_not @ Y2))) @ (iii @ Y0 @ Y1) @ (e_is @ nat @ Y0 @ Y1))))))),
% 1.85/0.57 inference(definition_unfolding,[],[f652,f656,f603])).
% 1.85/0.57 thf(f662,plain,(
% 1.85/0.57 ($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))) @ ((^[Y4 : $i]: ((^[Y5 : $i]: (n_some @ (diffprop @ Y4 @ Y5))))) @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y0 @ Y1) => ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $o]: ((^[Y5 : $o]: ((^[Y6 : $o]: (Y5 => Y6)))) @ (d_not @ Y4))) @ (iii @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y1 @ Y0))))))))),
% 1.85/0.57 inference(definition_unfolding,[],[f599,f612,f612,f657,f658])).
% 1.85/0.57 thf(f671,plain,(
% 1.85/0.57 ($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]: ((iii @ Y0 @ Y1) => ((^[Y2 : $i]: ((^[Y3 : $i]: (n_some @ (diffprop @ Y2 @ Y3))))) @ Y1 @ Y0))))))))),
% 1.85/0.57 inference(definition_unfolding,[],[f613,f612,f612,f602])).
% 1.85/0.57 thf(f677,plain,(
% 1.85/0.57 ($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))) @ (iii @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y0 @ Y1) => (d_not @ ((^[Y2 : $i]: ((^[Y3 : $i]: (n_some @ (diffprop @ Y2 @ Y3))))) @ Y0 @ Y1)))))))))),
% 1.85/0.57 inference(definition_unfolding,[],[f620,f612,f612,f658,f602])).
% 1.85/0.57 thf(f679,plain,(
% 1.85/0.57 ($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))) @ ((^[Y4 : $i]: ((^[Y5 : $i]: (n_some @ (diffprop @ Y4 @ Y5))))) @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y0 @ Y1) => (d_not @ (iii @ Y0 @ Y1)))))))))),
% 1.85/0.57 inference(definition_unfolding,[],[f622,f612,f612,f657])).
% 1.85/0.57 thf(f688,plain,(
% 1.85/0.57 ($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 @ Y2 @ Y3))))) @ Y0 @ Y1) => (d_not @ ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $o]: ((^[Y5 : $o]: ((^[Y6 : $o]: (Y5 => Y6)))) @ (d_not @ Y4))) @ (iii @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y0 @ Y1)))))))))),
% 1.85/0.57 inference(definition_unfolding,[],[f638,f612,f612,f602,f658])).
% 1.85/0.57 thf(f692,plain,(
% 1.85/0.57 ($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_not @ ((^[Y2 : $i]: ((^[Y3 : $i]: (n_some @ (diffprop @ Y2 @ Y3))))) @ Y0 @ Y1)) => ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $o]: ((^[Y5 : $o]: ((^[Y6 : $o]: (Y5 => Y6)))) @ (d_not @ Y4))) @ (iii @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y0 @ Y1))))))))),
% 1.85/0.57 inference(definition_unfolding,[],[f644,f612,f612,f602,f658])).
% 1.85/0.57 thf(f697,plain,(
% 1.85/0.57 ($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 @ Y2 @ Y3))))) @ Y0 @ Y1) => (iii @ Y1 @ Y0))))))))),
% 1.85/0.57 inference(definition_unfolding,[],[f653,f612,f612,f602])).
% 1.85/0.57 thf(f698,plain,(
% 1.85/0.57 ($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 @ Y0 @ Y1)) => (d_not @ ((d_not @ (iii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1))))))))))))),
% 1.85/0.57 inference(beta-eta_normalization,[],[f688])).
% 1.85/0.57 thf(f699,plain,(
% 1.85/0.57 ((((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((n_some @ (diffprop @ Y0 @ Y1)) => (d_not @ ((d_not @ (iii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1))))))))) @ sK2)) = $false)),
% 1.85/0.57 inference(sigma_proxy_clausification,[],[f698])).
% 1.85/0.57 thf(f700,plain,(
% 1.85/0.57 ((((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ sK2 @ Y0)) => (d_not @ ((d_not @ (iii @ sK2 @ Y0)) => (e_is @ nat @ sK2 @ Y0))))))))) = $false)),
% 1.85/0.57 inference(beta-eta_normalization,[],[f699])).
% 1.85/0.57 thf(f701,plain,(
% 1.85/0.57 (((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ sK2 @ Y0)) => (d_not @ ((d_not @ (iii @ sK2 @ Y0)) => (e_is @ nat @ sK2 @ Y0)))))))) = $false)),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f700])).
% 1.85/0.57 thf(f702,plain,(
% 1.85/0.57 ($true = ((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f700])).
% 1.85/0.57 thf(f703,plain,(
% 1.85/0.57 ((((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ sK2 @ Y0)) => (d_not @ ((d_not @ (iii @ sK2 @ Y0)) => (e_is @ nat @ sK2 @ Y0)))))) @ sK3)) = $false)),
% 1.85/0.57 inference(sigma_proxy_clausification,[],[f701])).
% 1.85/0.57 thf(f704,plain,(
% 1.85/0.57 ((((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((n_some @ (diffprop @ sK2 @ sK3)) => (d_not @ ((d_not @ (iii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3)))))) = $false)),
% 1.85/0.57 inference(beta-eta_normalization,[],[f703])).
% 1.85/0.57 thf(f705,plain,(
% 1.85/0.57 ((((n_some @ (diffprop @ sK2 @ sK3)) => (d_not @ ((d_not @ (iii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3))))) = $false)),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f704])).
% 1.85/0.57 thf(f706,plain,(
% 1.85/0.57 ($true = ((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f704])).
% 1.85/0.57 thf(f707,plain,(
% 1.85/0.57 (((d_not @ ((d_not @ (iii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3)))) = $false)),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f705])).
% 1.85/0.57 thf(f708,plain,(
% 1.85/0.57 ($true = ((n_some @ (diffprop @ sK2 @ sK3))))),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f705])).
% 1.85/0.57 thf(f731,plain,(
% 1.85/0.57 ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => (((d_not @ (n_some @ (diffprop @ Y0 @ Y1))) => (e_is @ nat @ Y0 @ Y1)) => (d_not @ (iii @ Y0 @ Y1)))))))))))),
% 1.85/0.57 inference(beta-eta_normalization,[],[f679])).
% 1.85/0.57 thf(f732,plain,(
% 1.85/0.57 ( ! [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 @ (n_some @ (diffprop @ Y0 @ Y1))) => (e_is @ nat @ Y0 @ Y1)) => (d_not @ (iii @ Y0 @ Y1)))))))) @ X1)))) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f731])).
% 1.85/0.57 thf(f733,plain,(
% 1.85/0.57 ( ! [X1 : $i] : (($true = (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (iii @ X1 @ Y0)))))))))) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f732])).
% 1.85/0.57 thf(f734,plain,(
% 1.85/0.57 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (iii @ X1 @ Y0)))))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f733])).
% 1.85/0.57 thf(f735,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (iii @ X1 @ Y0))))) @ X2))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f734])).
% 1.85/0.57 thf(f736,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : (($true = (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2)) => (d_not @ (iii @ X1 @ X2)))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f735])).
% 1.85/0.57 thf(f737,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : (($true = ((((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2)) => (d_not @ (iii @ X1 @ X2))))) | (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f736])).
% 1.85/0.57 thf(f738,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ((((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2))) = $false) | ($true = ((d_not @ (iii @ X1 @ X2)))) | (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f737])).
% 1.85/0.57 thf(f740,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((d_not @ (iii @ X1 @ X2)))) | ($true = ((d_not @ (n_some @ (diffprop @ X1 @ X2))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f738])).
% 1.85/0.57 thf(f779,plain,(
% 1.85/0.57 ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => (((d_not @ (n_some @ (diffprop @ Y0 @ Y1))) => (e_is @ nat @ Y0 @ Y1)) => ((d_not @ (iii @ Y1 @ Y0)) => (e_is @ nat @ Y1 @ Y0)))))))))))),
% 1.85/0.57 inference(beta-eta_normalization,[],[f662])).
% 1.85/0.57 thf(f780,plain,(
% 1.85/0.57 ( ! [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 @ (n_some @ (diffprop @ Y0 @ Y1))) => (e_is @ nat @ Y0 @ Y1)) => ((d_not @ (iii @ Y1 @ Y0)) => (e_is @ nat @ Y1 @ Y0)))))))) @ X1)))) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f779])).
% 1.85/0.57 thf(f781,plain,(
% 1.85/0.57 ( ! [X1 : $i] : (($true = (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0)) => ((d_not @ (iii @ Y0 @ X1)) => (e_is @ nat @ Y0 @ X1)))))))))) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f780])).
% 1.85/0.57 thf(f782,plain,(
% 1.85/0.57 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0)) => ((d_not @ (iii @ Y0 @ X1)) => (e_is @ nat @ Y0 @ X1))))))))) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f781])).
% 1.85/0.57 thf(f783,plain,(
% 1.85/0.57 ( ! [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_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0)) => ((d_not @ (iii @ Y0 @ X1)) => (e_is @ nat @ Y0 @ X1))))) @ X2)))) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f782])).
% 1.85/0.57 thf(f784,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2)) => ((d_not @ (iii @ X2 @ X1)) => (e_is @ nat @ X2 @ X1))))))) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f783])).
% 1.85/0.57 thf(f785,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2)) => ((d_not @ (iii @ X2 @ X1)) => (e_is @ nat @ X2 @ X1))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f784])).
% 1.85/0.57 thf(f786,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : (((((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2))) = $false) | (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((d_not @ (iii @ X2 @ X1)) => (e_is @ nat @ X2 @ X1))))) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f785])).
% 1.85/0.57 thf(f787,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((e_is @ nat @ X1 @ X2)) = $false) | (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((d_not @ (iii @ X2 @ X1)) => (e_is @ nat @ X2 @ X1))))) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f786])).
% 1.85/0.57 thf(f790,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_not @ (iii @ X2 @ X1))) = $false) | (((e_is @ nat @ X1 @ X2)) = $false) | ($true = ((e_is @ nat @ X2 @ X1))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f787])).
% 1.85/0.57 thf(f791,plain,(
% 1.85/0.57 ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((d_not @ (n_some @ (diffprop @ Y0 @ Y1))) => ((d_not @ (iii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1)))))))))))),
% 1.85/0.57 inference(beta-eta_normalization,[],[f692])).
% 1.85/0.57 thf(f792,plain,(
% 1.85/0.57 ( ! [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 @ (n_some @ (diffprop @ Y0 @ Y1))) => ((d_not @ (iii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1)))))))) @ X1)))) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f791])).
% 1.85/0.57 thf(f793,plain,(
% 1.85/0.57 ( ! [X1 : $i] : (($true = (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => ((d_not @ (iii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0)))))))))) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f792])).
% 1.85/0.57 thf(f794,plain,(
% 1.85/0.57 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => ((d_not @ (iii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0))))))))) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f793])).
% 1.85/0.57 thf(f795,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => ((d_not @ (iii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0))))) @ X2))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f794])).
% 1.85/0.57 thf(f796,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : (($true = (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((d_not @ (n_some @ (diffprop @ X1 @ X2))) => ((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f795])).
% 1.85/0.57 thf(f797,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : (($true = (((d_not @ (n_some @ (diffprop @ X1 @ X2))) => ((d_not @ (iii @ 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.85/0.57 inference(imp_proxy_clausification,[],[f796])).
% 1.85/0.57 thf(f798,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_not @ (n_some @ (diffprop @ X1 @ X2)))) = $false) | ($true = (((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f797])).
% 1.85/0.57 thf(f799,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_not @ (iii @ X1 @ X2))) = $false) | ($true = ((e_is @ nat @ X1 @ X2))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_not @ (n_some @ (diffprop @ X1 @ X2)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f798])).
% 1.85/0.57 thf(f850,plain,(
% 1.85/0.57 ($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 @ Y0 @ Y1)) => (iii @ Y1 @ Y0))))))))))),
% 1.85/0.57 inference(beta-eta_normalization,[],[f697])).
% 1.85/0.57 thf(f851,plain,(
% 1.85/0.57 ( ! [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 @ Y0 @ Y1)) => (iii @ Y1 @ Y0))))))) @ X1)))) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f850])).
% 1.85/0.57 thf(f852,plain,(
% 1.85/0.57 ( ! [X1 : $i] : (($true = (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ X1 @ Y0)) => (iii @ Y0 @ X1))))))))) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f851])).
% 1.85/0.57 thf(f853,plain,(
% 1.85/0.57 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ X1 @ Y0)) => (iii @ Y0 @ X1))))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f852])).
% 1.85/0.57 thf(f854,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ X1 @ Y0)) => (iii @ Y0 @ X1)))) @ X2)))) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f853])).
% 1.85/0.57 thf(f855,plain,(
% 1.85/0.57 ( ! [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 @ X1 @ X2)) => (iii @ X2 @ X1)))))) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f854])).
% 1.85/0.57 thf(f856,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : (($true = (((n_some @ (diffprop @ X1 @ X2)) => (iii @ X2 @ X1)))) | (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f855])).
% 1.85/0.57 thf(f857,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((iii @ X2 @ X1))) | (((n_some @ (diffprop @ X1 @ X2))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f856])).
% 1.85/0.57 thf(f858,plain,(
% 1.85/0.57 ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((iii @ Y0 @ Y1) => (n_some @ (diffprop @ Y1 @ Y0)))))))))))),
% 1.85/0.57 inference(beta-eta_normalization,[],[f671])).
% 1.85/0.57 thf(f859,plain,(
% 1.85/0.57 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((iii @ Y0 @ Y1) => (n_some @ (diffprop @ Y1 @ Y0)))))))) @ X1)))) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f858])).
% 1.85/0.57 thf(f860,plain,(
% 1.85/0.57 ( ! [X1 : $i] : (($true = (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((iii @ X1 @ Y0) => (n_some @ (diffprop @ Y0 @ X1)))))))))) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f859])).
% 1.85/0.57 thf(f861,plain,(
% 1.85/0.57 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((iii @ X1 @ Y0) => (n_some @ (diffprop @ Y0 @ X1)))))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f860])).
% 1.85/0.57 thf(f862,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((iii @ X1 @ Y0) => (n_some @ (diffprop @ Y0 @ X1))))) @ X2))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f861])).
% 1.85/0.57 thf(f863,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((iii @ X1 @ X2) => (n_some @ (diffprop @ X2 @ X1))))))) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f862])).
% 1.85/0.57 thf(f864,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((iii @ X1 @ X2) => (n_some @ (diffprop @ X2 @ X1))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f863])).
% 1.85/0.57 thf(f865,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((iii @ X1 @ X2)) = $false) | ($true = ((n_some @ (diffprop @ X2 @ X1)))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f864])).
% 1.85/0.57 thf(f944,plain,(
% 1.85/0.57 ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => (((d_not @ (iii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1)) => (d_not @ (n_some @ (diffprop @ Y0 @ Y1))))))))))))),
% 1.85/0.57 inference(beta-eta_normalization,[],[f677])).
% 1.85/0.57 thf(f945,plain,(
% 1.85/0.57 ( ! [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 @ (iii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1)) => (d_not @ (n_some @ (diffprop @ Y0 @ Y1))))))))) @ X1)))) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f944])).
% 1.85/0.57 thf(f946,plain,(
% 1.85/0.57 ( ! [X1 : $i] : (($true = (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (iii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (n_some @ (diffprop @ X1 @ Y0))))))))))) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f945])).
% 1.85/0.57 thf(f947,plain,(
% 1.85/0.57 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (iii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (n_some @ (diffprop @ X1 @ Y0)))))))))) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f946])).
% 1.85/0.57 thf(f948,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (iii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (n_some @ (diffprop @ X1 @ Y0)))))) @ X2))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(pi_proxy_clausification,[],[f947])).
% 1.85/0.57 thf(f949,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)) => (d_not @ (n_some @ (diffprop @ X1 @ X2)))))))) )),
% 1.85/0.57 inference(beta-eta_normalization,[],[f948])).
% 1.85/0.57 thf(f950,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)) => (d_not @ (n_some @ (diffprop @ X1 @ X2)))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f949])).
% 1.85/0.57 thf(f951,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ((((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2))) = $false) | ($true = ((d_not @ (n_some @ (diffprop @ X1 @ X2))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f950])).
% 1.85/0.57 thf(f952,plain,(
% 1.85/0.57 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((e_is @ nat @ X1 @ X2)) = $false) | ($true = ((d_not @ (n_some @ (diffprop @ X1 @ X2))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f951])).
% 1.85/0.57 thf(f966,definition,(
% 1.85/0.57 spl5_1 <=> ($true = ((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition])).
% 1.85/0.57 thf(f968,plain,(
% 1.85/0.57 ($true = ((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ~spl5_1),
% 1.85/0.57 inference(avatar_component_clause,[],[f966])).
% 1.85/0.57 thf(f969,plain,(
% 1.85/0.57 spl5_1),
% 1.85/0.57 inference(avatar_split_clause,[],[f702,f966])).
% 1.85/0.57 thf(f971,definition,(
% 1.85/0.57 spl5_2 <=> ($true = ((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition])).
% 1.85/0.57 thf(f973,plain,(
% 1.85/0.57 ($true = ((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ~spl5_2),
% 1.85/0.57 inference(avatar_component_clause,[],[f971])).
% 1.85/0.57 thf(f974,plain,(
% 1.85/0.57 spl5_2),
% 1.85/0.57 inference(avatar_split_clause,[],[f706,f971])).
% 1.85/0.57 thf(f976,definition,(
% 1.85/0.57 spl5_3 <=> ($true = ((n_some @ (diffprop @ sK2 @ sK3))))),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition])).
% 1.85/0.57 thf(f978,plain,(
% 1.85/0.57 ($true = ((n_some @ (diffprop @ sK2 @ sK3)))) | ~spl5_3),
% 1.85/0.57 inference(avatar_component_clause,[],[f976])).
% 1.85/0.57 thf(f979,plain,(
% 1.85/0.57 spl5_3),
% 1.85/0.57 inference(avatar_split_clause,[],[f708,f976])).
% 1.85/0.57 thf(f981,definition,(
% 1.85/0.57 spl5_4 <=> (((d_not @ ((d_not @ (iii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3)))) = $false)),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition])).
% 1.85/0.57 thf(f983,plain,(
% 1.85/0.57 (((d_not @ ((d_not @ (iii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3)))) = $false) | ~spl5_4),
% 1.85/0.57 inference(avatar_component_clause,[],[f981])).
% 1.85/0.57 thf(f984,plain,(
% 1.85/0.57 spl5_4),
% 1.85/0.57 inference(avatar_split_clause,[],[f707,f981])).
% 1.85/0.57 thf(f991,definition,(
% 1.85/0.57 spl5_6 <=> ($true = $false)),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition])).
% 1.85/0.57 thf(f994,plain,(
% 1.85/0.57 ~spl5_6),
% 1.85/0.57 inference(avatar_split_clause,[],[f654,f991])).
% 1.85/0.57 thf(f1006,plain,(
% 1.85/0.57 ( ! [X0 : $i] : (($true = ((e_is @ nat @ X0 @ sK2))) | (((d_not @ (iii @ X0 @ sK2))) = $false) | (((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_not @ (n_some @ (diffprop @ X0 @ sK2)))) = $false) | ($true = $false)) ) | ~spl5_1),
% 1.85/0.57 inference(superposition,[],[f799,f968])).
% 1.85/0.57 thf(f1007,plain,(
% 1.85/0.57 ( ! [X0 : $i] : ((((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((e_is @ nat @ X0 @ sK3))) | (((d_not @ (iii @ X0 @ sK3))) = $false) | ($true = $false) | (((d_not @ (n_some @ (diffprop @ X0 @ sK3)))) = $false)) ) | ~spl5_2),
% 1.85/0.57 inference(superposition,[],[f799,f973])).
% 1.85/0.57 thf(f1012,plain,(
% 1.85/0.57 ( ! [X0 : $i] : ((((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((e_is @ nat @ X0 @ sK2))) | (((d_not @ (n_some @ (diffprop @ X0 @ sK2)))) = $false) | (((d_not @ (iii @ X0 @ sK2))) = $false)) ) | ~spl5_1),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1006])).
% 1.85/0.57 thf(f1013,plain,(
% 1.85/0.57 ( ! [X0 : $i] : ((((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((e_is @ nat @ X0 @ sK3))) | (((d_not @ (iii @ X0 @ sK3))) = $false) | (((d_not @ (n_some @ (diffprop @ X0 @ sK3)))) = $false)) ) | ~spl5_2),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1007])).
% 1.85/0.57 thf(f1023,plain,(
% 1.85/0.57 (((d_not @ ($true => (e_is @ nat @ sK2 @ sK3)))) = $false) | (((d_not @ (iii @ sK2 @ sK3))) = $false) | ~spl5_4),
% 1.85/0.57 inference(superposition,[],[f983,f655])).
% 1.85/0.57 thf(f1024,plain,(
% 1.85/0.57 ((((d_not @ (iii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3))) = $false) | (((d_not @ $true)) = $false) | ~spl5_4),
% 1.85/0.57 inference(superposition,[],[f983,f655])).
% 1.85/0.57 thf(f1036,plain,(
% 1.85/0.57 (((d_not @ (e_is @ nat @ sK2 @ sK3))) = $false) | (((d_not @ (iii @ sK2 @ sK3))) = $false) | ~spl5_4),
% 1.85/0.57 inference(boolean_simplification,[],[f1023])).
% 1.85/0.57 thf(f1037,plain,(
% 1.85/0.57 (((d_not @ $true)) = $false) | (((e_is @ nat @ sK2 @ sK3)) = $false) | ~spl5_4),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f1024])).
% 1.85/0.57 thf(f1038,plain,(
% 1.85/0.57 (((d_not @ $true)) = $false) | ($true = ((d_not @ (iii @ sK2 @ sK3)))) | ~spl5_4),
% 1.85/0.57 inference(imp_proxy_clausification,[],[f1024])).
% 1.85/0.57 thf(f1040,definition,(
% 1.85/0.57 spl5_7 <=> (((d_not @ $true)) = $false)),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition])).
% 1.85/0.57 thf(f1041,plain,(
% 1.85/0.57 (((d_not @ $true)) != $false) | spl5_7),
% 1.85/0.57 inference(avatar_component_clause,[],[f1040])).
% 1.85/0.57 thf(f1042,plain,(
% 1.85/0.57 (((d_not @ $true)) = $false) | ~spl5_7),
% 1.85/0.57 inference(avatar_component_clause,[],[f1040])).
% 1.85/0.57 thf(f1044,definition,(
% 1.85/0.57 spl5_8 <=> (((e_is @ nat @ sK2 @ sK3)) = $false)),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition])).
% 1.85/0.57 thf(f1045,plain,(
% 1.85/0.57 (((e_is @ nat @ sK2 @ sK3)) != $false) | spl5_8),
% 1.85/0.57 inference(avatar_component_clause,[],[f1044])).
% 1.85/0.57 thf(f1046,plain,(
% 1.85/0.57 (((e_is @ nat @ sK2 @ sK3)) = $false) | ~spl5_8),
% 1.85/0.57 inference(avatar_component_clause,[],[f1044])).
% 1.85/0.57 thf(f1049,definition,(
% 1.85/0.57 spl5_9 <=> (((iii @ sK2 @ sK3)) = $false)),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition])).
% 1.85/0.57 thf(f1050,plain,(
% 1.85/0.57 (((iii @ sK2 @ sK3)) != $false) | spl5_9),
% 1.85/0.57 inference(avatar_component_clause,[],[f1049])).
% 1.85/0.57 thf(f1058,definition,(
% 1.85/0.57 spl5_11 <=> (((d_not @ (e_is @ nat @ sK2 @ sK3))) = $false)),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition])).
% 1.85/0.57 thf(f1062,definition,(
% 1.85/0.57 spl5_12 <=> (((d_not @ (iii @ sK2 @ sK3))) = $false)),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition])).
% 1.85/0.57 thf(f1065,plain,(
% 1.85/0.57 spl5_11 | spl5_12 | ~spl5_4),
% 1.85/0.57 inference(avatar_split_clause,[],[f1036,f981,f1062,f1058])).
% 1.85/0.57 thf(f1067,definition,(
% 1.85/0.57 spl5_13 <=> ($true = ((d_not @ (iii @ sK2 @ sK3))))),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_13])],[avatar_definition])).
% 1.85/0.57 thf(f1068,plain,(
% 1.85/0.57 ($true != ((d_not @ (iii @ sK2 @ sK3)))) | spl5_13),
% 1.85/0.57 inference(avatar_component_clause,[],[f1067])).
% 1.85/0.57 thf(f1069,plain,(
% 1.85/0.57 ($true = ((d_not @ (iii @ sK2 @ sK3)))) | ~spl5_13),
% 1.85/0.57 inference(avatar_component_clause,[],[f1067])).
% 1.85/0.57 thf(f1070,plain,(
% 1.85/0.57 spl5_7 | spl5_13 | ~spl5_4),
% 1.85/0.57 inference(avatar_split_clause,[],[f1038,f981,f1067,f1040])).
% 1.85/0.57 thf(f1071,plain,(
% 1.85/0.57 spl5_8 | spl5_7 | ~spl5_4),
% 1.85/0.57 inference(avatar_split_clause,[],[f1037,f981,f1040,f1044])).
% 1.85/0.57 thf(f1072,definition,(
% 1.85/0.57 (((e_is @ nat @ sK2 @ sK3)) != $false) | (((iii @ sK2 @ sK3)) != $false) | ($true != ((d_not @ (iii @ sK2 @ sK3)))) | (((d_not @ (e_is @ nat @ sK2 @ sK3))) != $false) | ($true = $false)),
% 1.85/0.57 introduced(theory,[theory_tautology_sat_conflict])).
% 1.85/0.57 thf(f1073,definition,(
% 1.85/0.57 ($true != ((d_not @ (iii @ sK2 @ sK3)))) | (((d_not @ (iii @ sK2 @ sK3))) != $false) | ($true = $false)),
% 1.85/0.57 introduced(theory,[theory_tautology_sat_conflict])).
% 1.85/0.57 thf(f1088,plain,(
% 1.85/0.57 (((d_not @ (n_some @ (diffprop @ sK3 @ sK2)))) = $false) | ($true = $false) | ($true = ((e_is @ nat @ sK3 @ sK2))) | (((d_not @ (iii @ sK3 @ sK2))) = $false) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(superposition,[],[f1012,f973])).
% 1.85/0.57 thf(f1096,plain,(
% 1.85/0.57 ($true = ((e_is @ nat @ sK3 @ sK2))) | (((d_not @ (iii @ sK3 @ sK2))) = $false) | (((d_not @ (n_some @ (diffprop @ sK3 @ sK2)))) = $false) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1088])).
% 1.85/0.57 thf(f1111,definition,(
% 1.85/0.57 spl5_19 <=> (((d_not @ (iii @ sK3 @ sK2))) = $false)),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_19])],[avatar_definition])).
% 1.85/0.57 thf(f1115,definition,(
% 1.85/0.57 spl5_20 <=> ($true = ((e_is @ nat @ sK3 @ sK2)))),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_20])],[avatar_definition])).
% 1.85/0.57 thf(f1119,definition,(
% 1.85/0.57 spl5_21 <=> (((d_not @ (n_some @ (diffprop @ sK3 @ sK2)))) = $false)),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_21])],[avatar_definition])).
% 1.85/0.57 thf(f1124,plain,(
% 1.85/0.57 spl5_21 | spl5_20 | spl5_19 | ~spl5_1 | ~spl5_2),
% 1.85/0.57 inference(avatar_split_clause,[],[f1096,f971,f966,f1111,f1115,f1119])).
% 1.85/0.57 thf(f1163,plain,(
% 1.85/0.57 ( ! [X0 : $i] : (($true = ((iii @ sK2 @ X0))) | (((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((n_some @ (diffprop @ X0 @ sK2))) = $false) | ($true = $false)) ) | ~spl5_1),
% 1.85/0.57 inference(superposition,[],[f857,f968])).
% 1.85/0.57 thf(f1164,plain,(
% 1.85/0.57 ( ! [X0 : $i] : ((((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((iii @ sK3 @ X0))) | (((n_some @ (diffprop @ X0 @ sK3))) = $false) | ($true = $false)) ) | ~spl5_2),
% 1.85/0.57 inference(superposition,[],[f857,f973])).
% 1.85/0.57 thf(f1169,plain,(
% 1.85/0.57 ( ! [X0 : $i] : ((((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((n_some @ (diffprop @ X0 @ sK2))) = $false) | ($true = ((iii @ sK2 @ X0)))) ) | ~spl5_1),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1163])).
% 1.85/0.57 thf(f1172,plain,(
% 1.85/0.57 ( ! [X0 : $i] : ((((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((iii @ sK3 @ X0))) | (((n_some @ (diffprop @ X0 @ sK3))) = $false)) ) | ~spl5_2),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1164])).
% 1.85/0.57 thf(f1184,plain,(
% 1.85/0.57 ( ! [X0 : $i] : ((((iii @ X0 @ sK3)) = $false) | (((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((n_some @ (diffprop @ sK3 @ X0)))) | ($true = $false)) ) | ~spl5_2),
% 1.85/0.57 inference(superposition,[],[f973,f865])).
% 1.85/0.57 thf(f1186,plain,(
% 1.85/0.57 ( ! [X0 : $i] : ((((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((iii @ X0 @ sK3)) = $false) | ($true = ((n_some @ (diffprop @ sK3 @ X0))))) ) | ~spl5_2),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1184])).
% 1.85/0.57 thf(f1199,plain,(
% 1.85/0.57 ( ! [X0 : $i] : (($true = ((d_not @ (n_some @ (diffprop @ X0 @ sK3))))) | ($true = $false) | (((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((e_is @ nat @ X0 @ sK3)) = $false)) ) | ~spl5_2),
% 1.85/0.57 inference(superposition,[],[f973,f952])).
% 1.85/0.57 thf(f1201,plain,(
% 1.85/0.57 ( ! [X0 : $i] : ((((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((e_is @ nat @ X0 @ sK3)) = $false) | ($true = ((d_not @ (n_some @ (diffprop @ X0 @ sK3)))))) ) | ~spl5_2),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1199])).
% 1.85/0.57 thf(f1232,plain,(
% 1.85/0.57 ( ! [X0 : $i] : (($true = $false) | (((d_not @ (iii @ sK2 @ X0))) = $false) | (((e_is @ nat @ X0 @ sK2)) = $false) | ($true = ((e_is @ nat @ sK2 @ X0))) | (((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) ) | ~spl5_1),
% 1.85/0.57 inference(superposition,[],[f968,f790])).
% 1.85/0.57 thf(f1236,plain,(
% 1.85/0.57 ( ! [X0 : $i] : ((((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_not @ (iii @ sK2 @ X0))) = $false) | ($true = ((e_is @ nat @ sK2 @ X0))) | (((e_is @ nat @ X0 @ sK2)) = $false)) ) | ~spl5_1),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1232])).
% 1.85/0.57 thf(f1245,plain,(
% 1.85/0.57 (((n_some @ (diffprop @ sK3 @ sK2))) = $false) | ($true = $false) | ($true = ((iii @ sK2 @ sK3))) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(superposition,[],[f973,f1169])).
% 1.85/0.57 thf(f1249,plain,(
% 1.85/0.57 ($true = ((iii @ sK2 @ sK3))) | (((n_some @ (diffprop @ sK3 @ sK2))) = $false) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1245])).
% 1.85/0.57 thf(f1266,definition,(
% 1.85/0.57 spl5_24 <=> (((n_some @ (diffprop @ sK3 @ sK2))) = $false)),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_24])],[avatar_definition])).
% 1.85/0.57 thf(f1268,plain,(
% 1.85/0.57 (((n_some @ (diffprop @ sK3 @ sK2))) = $false) | ~spl5_24),
% 1.85/0.57 inference(avatar_component_clause,[],[f1266])).
% 1.85/0.57 thf(f1308,plain,(
% 1.85/0.57 ($true = $false) | (((n_some @ (diffprop @ sK2 @ sK3))) = $false) | ($true = ((iii @ sK3 @ sK2))) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(superposition,[],[f1172,f968])).
% 1.85/0.57 thf(f1313,plain,(
% 1.85/0.57 (((n_some @ (diffprop @ sK2 @ sK3))) = $false) | ($true = ((iii @ sK3 @ sK2))) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1308])).
% 1.85/0.57 thf(f1318,plain,(
% 1.85/0.57 ($true = ((iii @ sK3 @ sK2))) | ($true = $false) | (~spl5_1 | ~spl5_2 | ~spl5_3)),
% 1.85/0.57 inference(forward_demodulation,[],[f1313,f978])).
% 1.85/0.57 thf(f1319,plain,(
% 1.85/0.57 ($true = ((iii @ sK3 @ sK2))) | (~spl5_1 | ~spl5_2 | ~spl5_3)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1318])).
% 1.85/0.57 thf(f1333,definition,(
% 1.85/0.57 spl5_27 <=> ($true = ((iii @ sK3 @ sK2)))),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_27])],[avatar_definition])).
% 1.85/0.57 thf(f1336,plain,(
% 1.85/0.57 spl5_27 | ~spl5_1 | ~spl5_2 | ~spl5_3),
% 1.85/0.57 inference(avatar_split_clause,[],[f1319,f976,f971,f966,f1333])).
% 1.85/0.57 thf(f1340,plain,(
% 1.85/0.57 (((iii @ sK2 @ sK3)) = $false) | ($true = $false) | ($true = ((n_some @ (diffprop @ sK3 @ sK2)))) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(superposition,[],[f968,f1186])).
% 1.85/0.57 thf(f1344,plain,(
% 1.85/0.57 ($true = ((n_some @ (diffprop @ sK3 @ sK2)))) | (((iii @ sK2 @ sK3)) = $false) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1340])).
% 1.85/0.57 thf(f1384,plain,(
% 1.85/0.57 ($true = ((d_not @ (n_some @ (diffprop @ sK2 @ sK3))))) | (((e_is @ nat @ sK2 @ sK3)) = $false) | ($true = $false) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(superposition,[],[f1201,f968])).
% 1.85/0.57 thf(f1389,plain,(
% 1.85/0.57 (((e_is @ nat @ sK2 @ sK3)) = $false) | ($true = ((d_not @ (n_some @ (diffprop @ sK2 @ sK3))))) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1384])).
% 1.85/0.57 thf(f1434,definition,(
% 1.85/0.57 spl5_33 <=> (((e_is @ nat @ sK3 @ sK2)) = $false)),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_33])],[avatar_definition])).
% 1.85/0.57 thf(f1435,plain,(
% 1.85/0.57 (((e_is @ nat @ sK3 @ sK2)) != $false) | spl5_33),
% 1.85/0.57 inference(avatar_component_clause,[],[f1434])).
% 1.85/0.57 thf(f1513,plain,(
% 1.85/0.57 ($true = ((e_is @ nat @ sK2 @ sK3))) | (((d_not @ (iii @ sK2 @ sK3))) = $false) | ($true = $false) | (((e_is @ nat @ sK3 @ sK2)) = $false) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(superposition,[],[f1236,f973])).
% 1.85/0.57 thf(f1517,plain,(
% 1.85/0.57 (((e_is @ nat @ sK3 @ sK2)) = $false) | (((d_not @ (iii @ sK2 @ sK3))) = $false) | ($true = ((e_is @ nat @ sK2 @ sK3))) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1513])).
% 1.85/0.57 thf(f1526,plain,(
% 1.85/0.57 (((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))) = $false) | ($true = $false) | ($true = ((e_is @ nat @ sK2 @ sK3))) | (((d_not @ (iii @ sK2 @ sK3))) = $false) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(superposition,[],[f968,f1013])).
% 1.85/0.57 thf(f1530,plain,(
% 1.85/0.57 (((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))) = $false) | (((d_not @ (iii @ sK2 @ sK3))) = $false) | ($true = ((e_is @ nat @ sK2 @ sK3))) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1526])).
% 1.85/0.57 thf(f1535,plain,(
% 1.85/0.57 ($true = $false) | (((d_not @ (iii @ sK2 @ sK3))) = $false) | (((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))) = $false) | (~spl5_1 | ~spl5_2 | ~spl5_8)),
% 1.85/0.57 inference(forward_demodulation,[],[f1530,f1046])).
% 1.85/0.57 thf(f1536,plain,(
% 1.85/0.57 (((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))) = $false) | (((d_not @ (iii @ sK2 @ sK3))) = $false) | (~spl5_1 | ~spl5_2 | ~spl5_8)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f1535])).
% 1.85/0.57 thf(f1538,plain,(
% 1.85/0.57 (((d_not @ $true)) = $false) | (((d_not @ (iii @ sK2 @ sK3))) = $false) | (~spl5_1 | ~spl5_2 | ~spl5_3 | ~spl5_8)),
% 1.85/0.57 inference(forward_demodulation,[],[f1536,f978])).
% 1.85/0.57 thf(f2088,plain,(
% 1.85/0.57 ( ! [X0 : $i] : (($true = ((d_not @ (n_some @ (diffprop @ X0 @ sK3))))) | ($true = ((d_not @ (iii @ X0 @ sK3)))) | (((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = $false)) ) | ~spl5_2),
% 1.85/0.57 inference(superposition,[],[f973,f740])).
% 1.85/0.57 thf(f2090,plain,(
% 1.85/0.57 ( ! [X0 : $i] : ((((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((d_not @ (n_some @ (diffprop @ X0 @ sK3))))) | ($true = ((d_not @ (iii @ X0 @ sK3))))) ) | ~spl5_2),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f2088])).
% 1.85/0.57 thf(f2145,plain,(
% 1.85/0.57 ($true = $false) | ($true = ((d_not @ (n_some @ (diffprop @ sK2 @ sK3))))) | ($true = ((d_not @ (iii @ sK2 @ sK3)))) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(superposition,[],[f968,f2090])).
% 1.85/0.57 thf(f2147,plain,(
% 1.85/0.57 ($true = ((d_not @ (n_some @ (diffprop @ sK2 @ sK3))))) | ($true = ((d_not @ (iii @ sK2 @ sK3)))) | (~spl5_1 | ~spl5_2)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f2145])).
% 1.85/0.57 thf(f2208,plain,(
% 1.85/0.57 ($true = ((d_not @ $true))) | (((e_is @ nat @ sK2 @ sK3)) = $false) | (~spl5_1 | ~spl5_2 | ~spl5_3)),
% 1.85/0.57 inference(forward_demodulation,[],[f1389,f978])).
% 1.85/0.57 thf(f2228,plain,(
% 1.85/0.57 ($true = ((d_not @ $true))) | (~spl5_1 | ~spl5_2 | ~spl5_3 | spl5_8)),
% 1.85/0.57 inference(forward_subsumption_resolution,[],[f2208,f1045])).
% 1.85/0.57 thf(f2247,plain,(
% 1.85/0.57 ($true = $false) | (~spl5_1 | ~spl5_2 | ~spl5_3 | ~spl5_7 | spl5_8)),
% 1.85/0.57 inference(forward_demodulation,[],[f2228,f1042])).
% 1.85/0.57 thf(f2248,plain,(
% 1.85/0.57 $false | (~spl5_1 | ~spl5_2 | ~spl5_3 | ~spl5_7 | spl5_8)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f2247])).
% 1.85/0.57 thf(f2249,plain,(
% 1.85/0.57 ~spl5_1 | ~spl5_2 | ~spl5_3 | ~spl5_7 | spl5_8),
% 1.85/0.57 inference(avatar_contradiction_clause,[],[f2248])).
% 1.85/0.57 thf(f2314,plain,(
% 1.85/0.57 ($true = ((d_not @ (iii @ sK2 @ sK3)))) | ($true = ((d_not @ $true))) | (~spl5_1 | ~spl5_2 | ~spl5_3)),
% 1.85/0.57 inference(forward_demodulation,[],[f2147,f978])).
% 1.85/0.57 thf(f2322,plain,(
% 1.85/0.57 ($true = ((n_some @ (diffprop @ sK3 @ sK2)))) | (~spl5_1 | ~spl5_2 | spl5_9)),
% 1.85/0.57 inference(forward_subsumption_resolution,[],[f1344,f1050])).
% 1.85/0.57 thf(f2330,plain,(
% 1.85/0.57 ($true = ((d_not @ $true))) | (~spl5_1 | ~spl5_2 | ~spl5_3 | spl5_13)),
% 1.85/0.57 inference(forward_subsumption_resolution,[],[f2314,f1068])).
% 1.85/0.57 thf(f2336,plain,(
% 1.85/0.57 ($true = $false) | (~spl5_1 | ~spl5_2 | spl5_9 | ~spl5_24)),
% 1.85/0.57 inference(forward_demodulation,[],[f2322,f1268])).
% 1.85/0.57 thf(f2337,plain,(
% 1.85/0.57 $false | (~spl5_1 | ~spl5_2 | spl5_9 | ~spl5_24)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f2336])).
% 1.85/0.57 thf(f2338,plain,(
% 1.85/0.57 ~spl5_1 | ~spl5_2 | spl5_9 | ~spl5_24),
% 1.85/0.57 inference(avatar_contradiction_clause,[],[f2337])).
% 1.85/0.57 thf(f2342,plain,(
% 1.85/0.57 ($true = $false) | (~spl5_1 | ~spl5_2 | ~spl5_3 | ~spl5_7 | spl5_13)),
% 1.85/0.57 inference(forward_demodulation,[],[f2330,f1042])).
% 1.85/0.57 thf(f2343,plain,(
% 1.85/0.57 $false | (~spl5_1 | ~spl5_2 | ~spl5_3 | ~spl5_7 | spl5_13)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f2342])).
% 1.85/0.57 thf(f2344,plain,(
% 1.85/0.57 ~spl5_1 | ~spl5_2 | ~spl5_3 | ~spl5_7 | spl5_13),
% 1.85/0.57 inference(avatar_contradiction_clause,[],[f2343])).
% 1.85/0.57 thf(f2354,definition,(
% 1.85/0.57 spl5_76 <=> ($true = ((iii @ sK2 @ sK3)))),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_76])],[avatar_definition])).
% 1.85/0.57 thf(f2359,definition,(
% 1.85/0.57 spl5_77 <=> ($true = ((n_some @ (diffprop @ sK3 @ sK2))))),
% 1.85/0.57 introduced(definition,[new_symbols(definition,[spl5_77])],[avatar_definition])).
% 1.85/0.57 thf(f2362,plain,(
% 1.85/0.57 spl5_77 | ~spl5_1 | ~spl5_2 | spl5_9),
% 1.85/0.57 inference(avatar_split_clause,[],[f2322,f1049,f971,f966,f2359])).
% 1.85/0.57 thf(f2392,plain,(
% 1.85/0.57 spl5_76 | spl5_24 | ~spl5_1 | ~spl5_2),
% 1.85/0.57 inference(avatar_split_clause,[],[f1249,f971,f966,f1266,f2354])).
% 1.85/0.57 thf(f2444,definition,(
% 1.85/0.57 ($true != ((iii @ sK3 @ sK2))) | ($true != ((iii @ sK2 @ sK3))) | ($true != ((n_some @ (diffprop @ sK3 @ sK2)))) | ($true != ((d_not @ (iii @ sK2 @ sK3)))) | (((d_not @ (iii @ sK3 @ sK2))) != $false) | (((n_some @ (diffprop @ sK3 @ sK2))) = $false)),
% 1.85/0.57 introduced(theory,[theory_tautology_sat_conflict])).
% 1.85/0.57 thf(f2494,definition,(
% 1.85/0.57 ($true != ((iii @ sK2 @ sK3))) | (((d_not @ (n_some @ (diffprop @ sK3 @ sK2)))) != $false) | ($true != ((d_not @ (iii @ sK2 @ sK3)))) | ($true != ((n_some @ (diffprop @ sK3 @ sK2)))) | (((n_some @ (diffprop @ sK3 @ sK2))) = $false)),
% 1.85/0.57 introduced(theory,[theory_tautology_sat_conflict])).
% 1.85/0.57 thf(f2497,definition,(
% 1.85/0.57 (((e_is @ nat @ sK3 @ sK2)) != $false) | ($true != ((e_is @ nat @ sK3 @ sK2))) | ($true = $false)),
% 1.85/0.57 introduced(theory,[theory_tautology_sat_conflict])).
% 1.85/0.57 thf(f2509,plain,(
% 1.85/0.57 ($true = $false) | (((d_not @ $true)) = $false) | (~spl5_1 | ~spl5_2 | ~spl5_3 | ~spl5_8 | ~spl5_13)),
% 1.85/0.57 inference(forward_demodulation,[],[f1538,f1069])).
% 1.85/0.57 thf(f2510,plain,(
% 1.85/0.57 (((d_not @ $true)) = $false) | (~spl5_1 | ~spl5_2 | ~spl5_3 | ~spl5_8 | ~spl5_13)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f2509])).
% 1.85/0.57 thf(f2528,plain,(
% 1.85/0.57 (((d_not @ (iii @ sK2 @ sK3))) = $false) | ($true = ((e_is @ nat @ sK2 @ sK3))) | (~spl5_1 | ~spl5_2 | spl5_33)),
% 1.85/0.57 inference(forward_subsumption_resolution,[],[f1517,f1435])).
% 1.85/0.57 thf(f2552,plain,(
% 1.85/0.57 $false | (~spl5_1 | ~spl5_2 | ~spl5_3 | spl5_7 | ~spl5_8 | ~spl5_13)),
% 1.85/0.57 inference(forward_subsumption_resolution,[],[f2510,f1041])).
% 1.85/0.57 thf(f2553,plain,(
% 1.85/0.57 ~spl5_1 | ~spl5_2 | ~spl5_3 | spl5_7 | ~spl5_8 | ~spl5_13),
% 1.85/0.57 inference(avatar_contradiction_clause,[],[f2552])).
% 1.85/0.57 thf(f2563,plain,(
% 1.85/0.57 ($true = ((e_is @ nat @ sK2 @ sK3))) | ($true = $false) | (~spl5_1 | ~spl5_2 | ~spl5_13 | spl5_33)),
% 1.85/0.57 inference(forward_demodulation,[],[f2528,f1069])).
% 1.85/0.57 thf(f2564,plain,(
% 1.85/0.57 ($true = ((e_is @ nat @ sK2 @ sK3))) | (~spl5_1 | ~spl5_2 | ~spl5_13 | spl5_33)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f2563])).
% 1.85/0.57 thf(f2591,plain,(
% 1.85/0.57 ($true = $false) | (~spl5_1 | ~spl5_2 | ~spl5_8 | ~spl5_13 | spl5_33)),
% 1.85/0.57 inference(forward_demodulation,[],[f2564,f1046])).
% 1.85/0.57 thf(f2592,plain,(
% 1.85/0.57 $false | (~spl5_1 | ~spl5_2 | ~spl5_8 | ~spl5_13 | spl5_33)),
% 1.85/0.57 inference(trivial_inequality_removal,[],[f2591])).
% 1.85/0.57 thf(f2593,plain,(
% 1.85/0.57 ~spl5_1 | ~spl5_2 | ~spl5_8 | ~spl5_13 | spl5_33),
% 1.85/0.57 inference(avatar_contradiction_clause,[],[f2592])).
% 1.85/0.57 cnf(s1, plain, spl5_1, inference(sat_conversion,[],[f969])).
% 1.85/0.57 cnf(s2, plain, spl5_2, inference(sat_conversion,[],[f974])).
% 1.85/0.57 cnf(s3, plain, spl5_3, inference(sat_conversion,[],[f979])).
% 1.85/0.57 cnf(s4, plain, spl5_4, inference(sat_conversion,[],[f984])).
% 1.85/0.57 cnf(s6, plain, ~spl5_6, inference(sat_conversion,[],[f994])).
% 1.85/0.57 cnf(s9, plain, ~spl5_4 | spl5_11 | spl5_12, inference(sat_conversion,[],[f1065])).
% 1.85/0.57 cnf(s10, plain, ~spl5_4 | spl5_7 | spl5_13, inference(sat_conversion,[],[f1070])).
% 1.85/0.57 cnf(s11, plain, ~spl5_4 | spl5_7 | spl5_8, inference(sat_conversion,[],[f1071])).
% 1.85/0.57 cnf(s12, plain, spl5_6 | ~spl5_8 | ~spl5_9 | ~spl5_11 | ~spl5_13, inference(sat_conversion,[],[f1072])).
% 1.85/0.57 cnf(s13, plain, spl5_6 | ~spl5_12 | ~spl5_13, inference(sat_conversion,[],[f1073])).
% 1.85/0.57 cnf(s19, plain, ~spl5_1 | ~spl5_2 | spl5_19 | spl5_20 | spl5_21, inference(sat_conversion,[],[f1124])).
% 1.85/0.57 cnf(s26, plain, ~spl5_1 | ~spl5_2 | ~spl5_3 | spl5_27, inference(sat_conversion,[],[f1336])).
% 1.85/0.57 cnf(s118, plain, ~spl5_1 | ~spl5_2 | ~spl5_3 | ~spl5_7 | spl5_8, inference(sat_conversion,[],[f2249])).
% 1.85/0.57 cnf(s140, plain, ~spl5_1 | ~spl5_2 | spl5_9 | ~spl5_24, inference(sat_conversion,[],[f2338])).
% 1.85/0.57 cnf(s143, plain, ~spl5_1 | ~spl5_2 | ~spl5_3 | ~spl5_7 | spl5_13, inference(sat_conversion,[],[f2344])).
% 1.85/0.57 cnf(s147, plain, ~spl5_1 | ~spl5_2 | spl5_9 | spl5_77, inference(sat_conversion,[],[f2362])).
% 1.85/0.57 cnf(s155, plain, ~spl5_1 | ~spl5_2 | spl5_24 | spl5_76, inference(sat_conversion,[],[f2392])).
% 1.85/0.57 cnf(s172, plain, ~spl5_13 | ~spl5_19 | spl5_24 | ~spl5_27 | ~spl5_76 | ~spl5_77, inference(sat_conversion,[],[f2444])).
% 1.85/0.57 cnf(s222, plain, ~spl5_13 | ~spl5_21 | spl5_24 | ~spl5_76 | ~spl5_77, inference(sat_conversion,[],[f2494])).
% 1.85/0.57 cnf(s225, plain, spl5_6 | ~spl5_20 | ~spl5_33, inference(sat_conversion,[],[f2497])).
% 1.85/0.57 cnf(s235, plain, ~spl5_1 | ~spl5_2 | ~spl5_3 | spl5_7 | ~spl5_8 | ~spl5_13, inference(sat_conversion,[],[f2553])).
% 1.85/0.57 cnf(s244, plain, ~spl5_1 | ~spl5_2 | ~spl5_8 | ~spl5_13 | spl5_33, inference(sat_conversion,[],[f2593])).
% 1.85/0.57 cnf(s256, plain, spl5_27, inference(rat,[],[s26,s2,s3,s1])).
% 1.85/0.57 cnf(s257, plain, spl5_7, inference(rat,[],[s235,s10,s11,s3,s2,s1,s4])).
% 1.85/0.57 cnf(s258, plain, spl5_13, inference(rat,[],[s143,s1,s2,s3,s257])).
% 1.85/0.57 cnf(s259, plain, spl5_8, inference(rat,[],[s118,s1,s2,s3,s257])).
% 1.85/0.57 cnf(s260, plain, ~spl5_12, inference(rat,[],[s13,s6,s258])).
% 1.85/0.57 cnf(s262, plain, spl5_33, inference(rat,[],[s244,s258,s1,s2,s259])).
% 1.85/0.57 cnf(s265, plain, spl5_11, inference(rat,[],[s9,s4,s260])).
% 1.85/0.57 cnf(s266, plain, ~spl5_20, inference(rat,[],[s225,s6,s262])).
% 1.85/0.57 cnf(s270, plain, ~spl5_9, inference(rat,[],[s12,s258,s259,s6,s265])).
% 1.85/0.57 cnf(s272, plain, spl5_77, inference(rat,[],[s147,s1,s2,s270])).
% 1.85/0.57 cnf(s273, plain, ~spl5_24, inference(rat,[],[s140,s1,s2,s270])).
% 1.85/0.57 cnf(s276, plain, spl5_76, inference(rat,[],[s155,s1,s2,s273])).
% 1.85/0.57 cnf(s277, plain, ~spl5_21, inference(rat,[],[s222,s272,s276,s258,s273])).
% 1.85/0.57 cnf(s278, plain, ~spl5_19, inference(rat,[],[s172,s272,s276,s256,s258,s273])).
% 1.85/0.57 cnf(s279, plain, $false, inference(rat,[],[s19,s266,s1,s2,s277,s278])).
% 1.85/0.57 thf(f2610,plain,(
% 1.85/0.57 $false),
% 1.85/0.57 inference(avatar_sat_refutation,[],[s279])).
% 1.85/0.57 % SZS output end Proof for theBenchmark
% 1.85/0.57 % (986831)------------------------------
% 1.85/0.57 % (986831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.85/0.57 % (986831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.85/0.57 % (986831)CaDiCaL version: 2.1.3
% 1.85/0.57 % (986831)Termination reason: Refutation
% 1.85/0.57 % (986831)Time elapsed: 0.093 s
% 1.85/0.57 % (986831)Peak memory usage: 14 MB
% 1.85/0.57 % (986831)Instructions burned: 183 (million)
% 1.85/0.57 % (986724)Success in time 0.302 s
% 1.85/0.57 % Vampire exiting
%------------------------------------------------------------------------------