%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM659^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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:18:26 AM UTC 2026
% Result : Theorem 1.49s 0.54s
% Output : Refutation 1.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM659^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.18 % Computer : n003.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 12:34:44 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/0.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.67/0.39 % (2443559)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.67/0.39 % (2443569)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3147034789:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.67/0.39 % (2443570)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.67/0.39 % (2443570)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.67/0.39 % (2443567)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=397254140: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.67/0.39 % (2443564)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=911118671:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.67/0.39 % (2443565)lrs+10_16_si=on:nwc=1.5:random_seed=3266377377:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.67/0.39 % (2443566)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2842502162:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.67/0.39 % (2443568)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=4139335307:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.67/0.39 % (2443570)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=3476174655:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.67/0.39 % (2443566)Instruction limit reached!
% 0.67/0.39 % (2443566)------------------------------
% 0.67/0.39 % (2443566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.39 % (2443566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.39 % (2443566)CaDiCaL version: 2.1.3
% 0.67/0.39 % (2443566)Termination reason: Instruction limit
% 0.67/0.39 % (2443566)Termination phase: shuffling
% 0.67/0.39 % (2443566)Time elapsed: 0.003 s
% 0.67/0.39 % (2443566)Peak memory usage: 10 MB
% 0.67/0.39 % (2443566)Instructions burned: 5 (million)
% 0.67/0.39 % (2443565)Instruction limit reached!
% 0.67/0.39 % (2443565)------------------------------
% 0.67/0.39 % (2443565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.39 % (2443565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.39 % (2443565)CaDiCaL version: 2.1.3
% 0.67/0.39 % (2443565)Termination reason: Instruction limit
% 0.67/0.39 % (2443565)Termination phase: shuffling
% 0.67/0.39 % (2443565)Time elapsed: 0.009 s
% 0.67/0.39 % (2443565)Peak memory usage: 10 MB
% 0.67/0.39 % (2443565)Instructions burned: 20 (million)
% 0.67/0.39 % (2443569)Instruction limit reached!
% 0.67/0.39 % (2443569)------------------------------
% 0.67/0.39 % (2443569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.39 % (2443569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.39 % (2443569)CaDiCaL version: 2.1.3
% 0.67/0.39 % (2443569)Termination reason: Instruction limit
% 0.67/0.39 % (2443569)Termination phase: Function definition elimination
% 0.67/0.39 % (2443569)Time elapsed: 0.019 s
% 0.67/0.39 % (2443569)Peak memory usage: 11 MB
% 0.67/0.39 % (2443569)Instructions burned: 80 (million)
% 0.67/0.39 % (2443568)Instruction limit reached!
% 0.67/0.39 % (2443568)------------------------------
% 0.67/0.39 % (2443568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.39 % (2443568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.39 % (2443568)CaDiCaL version: 2.1.3
% 0.67/0.39 % (2443568)Termination reason: Instruction limit
% 0.67/0.39 % (2443568)Termination phase: Property scanning
% 0.67/0.39 % (2443568)Time elapsed: 0.012 s
% 0.67/0.39 % (2443568)Peak memory usage: 10 MB
% 0.67/0.39 % (2443568)Instructions burned: 26 (million)
% 0.67/0.39 % (2443580)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.67/0.39 % (2443578)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3199295068:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.67/0.43 % (2443580)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=101749597:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.67/0.43 % (2443578)Instruction limit reached!
% 0.67/0.43 % (2443578)------------------------------
% 0.67/0.43 % (2443578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.43 % (2443578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.43 % (2443578)CaDiCaL version: 2.1.3
% 0.67/0.43 % (2443578)Termination reason: Instruction limit
% 0.67/0.43 % (2443578)Termination phase: shuffling
% 0.67/0.43 % (2443578)Time elapsed: 0.003 s
% 0.67/0.43 % (2443578)Peak memory usage: 10 MB
% 0.67/0.43 % (2443578)Instructions burned: 6 (million)
% 0.67/0.43 % (2443580)Instruction limit reached!
% 0.67/0.43 % (2443580)------------------------------
% 0.67/0.43 % (2443580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.43 % (2443580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.43 % (2443580)CaDiCaL version: 2.1.3
% 0.67/0.43 % (2443580)Termination reason: Instruction limit
% 0.67/0.43 % (2443580)Termination phase: shuffling
% 0.67/0.43 % (2443580)Time elapsed: 0.002 s
% 0.67/0.43 % (2443580)Peak memory usage: 10 MB
% 0.67/0.43 % (2443580)Instructions burned: 8 (million)
% 0.67/0.43 % (2443581)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1554505708:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.67/0.43 % (2443584)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.67/0.43 % (2443584)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.67/0.43 % (2443584)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=4157625533: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.67/0.43 % (2443564)Instruction limit reached!
% 0.67/0.43 % (2443564)------------------------------
% 0.67/0.43 % (2443564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.43 % (2443564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.43 % (2443564)CaDiCaL version: 2.1.3
% 0.67/0.43 % (2443564)Termination reason: Instruction limit
% 0.67/0.43 % (2443564)Termination phase: Function definition elimination
% 0.67/0.43 % (2443564)Time elapsed: 0.038 s
% 0.67/0.43 % (2443564)Peak memory usage: 11 MB
% 0.67/0.43 % (2443564)Instructions burned: 88 (million)
% 0.67/0.43 % (2443581)Instruction limit reached!
% 0.67/0.43 % (2443581)------------------------------
% 0.67/0.43 % (2443581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.43 % (2443581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.43 % (2443581)CaDiCaL version: 2.1.3
% 0.67/0.43 % (2443581)Termination reason: Instruction limit
% 0.67/0.43 % (2443581)Termination phase: shuffling
% 0.67/0.43 % (2443581)Time elapsed: 0.007 s
% 0.67/0.43 % (2443581)Peak memory usage: 10 MB
% 0.67/0.43 % (2443581)Instructions burned: 15 (million)
% 0.67/0.43 % (2443579)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2927365081:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.67/0.43 % (2443579)Instruction limit reached!
% 0.67/0.43 % (2443579)------------------------------
% 0.67/0.43 % (2443579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.43 % (2443579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.43 % (2443579)CaDiCaL version: 2.1.3
% 0.67/0.43 % (2443579)Termination reason: Instruction limit
% 0.67/0.43 % (2443579)Termination phase: shuffling
% 0.67/0.43 % (2443579)Time elapsed: 0.003 s
% 0.67/0.43 % (2443579)Peak memory usage: 9 MB
% 0.67/0.43 % (2443579)Instructions burned: 5 (million)
% 0.67/0.43 % (2443584)Instruction limit reached!
% 0.67/0.43 % (2443584)------------------------------
% 0.67/0.43 % (2443584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.43 % (2443584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.43 % (2443584)CaDiCaL version: 2.1.3
% 0.67/0.43 % (2443584)Termination reason: Instruction limit
% 0.67/0.47 % (2443584)Termination phase: Property scanning
% 0.67/0.47 % (2443584)Time elapsed: 0.008 s
% 0.67/0.47 % (2443584)Peak memory usage: 10 MB
% 0.67/0.47 % (2443584)Instructions burned: 33 (million)
% 0.67/0.47 % (2443585)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=1630361208:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.67/0.47 % (2443592)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3095577573:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.67/0.47 % (2443588)lrs+10_1_si=on:cs=on:random_seed=3203923671:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.67/0.47 % (2443588)Instruction limit reached!
% 0.67/0.47 % (2443588)------------------------------
% 0.67/0.47 % (2443588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.47 % (2443588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.47 % (2443588)CaDiCaL version: 2.1.3
% 0.67/0.47 % (2443588)Termination reason: Instruction limit
% 0.67/0.47 % (2443588)Termination phase: shuffling
% 0.67/0.47 % (2443588)Time elapsed: 0.005 s
% 0.67/0.47 % (2443588)Peak memory usage: 10 MB
% 0.67/0.47 % (2443588)Instructions burned: 10 (million)
% 0.67/0.47 % (2443591)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2297474188:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.67/0.47 % (2443570)Instruction limit reached!
% 0.67/0.47 % (2443570)------------------------------
% 0.67/0.47 % (2443570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.47 % (2443570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.47 % (2443570)CaDiCaL version: 2.1.3
% 0.67/0.47 % (2443570)Termination reason: Instruction limit
% 0.67/0.47 % (2443570)Termination phase: Function definition elimination
% 0.67/0.47 % (2443570)Time elapsed: 0.064 s
% 0.67/0.47 % (2443570)Peak memory usage: 11 MB
% 0.67/0.47 % (2443570)Instructions burned: 158 (million)
% 0.67/0.47 % (2443589)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.67/0.47 % (2443592)Refutation not found, incomplete strategy
% 0.67/0.47 % (2443592)------------------------------
% 0.67/0.47 % (2443592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.47 % (2443592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.47 % (2443592)CaDiCaL version: 2.1.3
% 0.67/0.47 % (2443592)Termination reason: Refutation not found, incomplete strategy
% 0.67/0.47 % (2443592)Time elapsed: 0.011 s
% 0.67/0.47 % (2443592)Peak memory usage: 13 MB
% 0.67/0.47 % (2443592)Instructions burned: 45 (million)
% 0.67/0.47 % (2443592)------------------------------
% 0.67/0.47 % (2443592)------------------------------
% 0.67/0.47 % (2443589)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=3893976974:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.67/0.47 % (2443589)Instruction limit reached!
% 0.67/0.47 % (2443589)------------------------------
% 0.67/0.47 % (2443589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.47 % (2443589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.47 % (2443589)CaDiCaL version: 2.1.3
% 0.67/0.47 % (2443589)Termination reason: Instruction limit
% 0.67/0.47 % (2443589)Termination phase: shuffling
% 0.67/0.47 % (2443589)Time elapsed: 0.002 s
% 0.67/0.47 % (2443589)Peak memory usage: 9 MB
% 0.67/0.47 % (2443589)Instructions burned: 4 (million)
% 0.67/0.47 % (2443599)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1066728504:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.67/0.47 % (2443596)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3122294720:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.67/0.47 % (2443591)Instruction limit reached!
% 0.67/0.47 % (2443591)------------------------------
% 0.67/0.47 % (2443591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.47 % (2443591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.47 % (2443591)CaDiCaL version: 2.1.3
% 1.49/0.50 % (2443591)Termination reason: Instruction limit
% 1.49/0.50 % (2443591)Termination phase: Saturation
% 1.49/0.50 % (2443591)Time elapsed: 0.018 s
% 1.49/0.50 % (2443591)Peak memory usage: 12 MB
% 1.49/0.50 % (2443591)Instructions burned: 39 (million)
% 1.49/0.50 % (2443598)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=460767035:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.49/0.50 % (2443585)Instruction limit reached!
% 1.49/0.50 % (2443585)------------------------------
% 1.49/0.50 % (2443585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.50 % (2443585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.50 % (2443585)CaDiCaL version: 2.1.3
% 1.49/0.50 % (2443585)Termination reason: Instruction limit
% 1.49/0.50 % (2443585)Termination phase: Function definition elimination
% 1.49/0.50 % (2443585)Time elapsed: 0.036 s
% 1.49/0.50 % (2443585)Peak memory usage: 11 MB
% 1.49/0.50 % (2443585)Instructions burned: 86 (million)
% 1.49/0.50 % (2443598)Instruction limit reached!
% 1.49/0.50 % (2443598)------------------------------
% 1.49/0.50 % (2443598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.50 % (2443598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.50 % (2443598)CaDiCaL version: 2.1.3
% 1.49/0.50 % (2443598)Termination reason: Instruction limit
% 1.49/0.50 % (2443598)Termination phase: shuffling
% 1.49/0.50 % (2443598)Time elapsed: 0.006 s
% 1.49/0.50 % (2443598)Peak memory usage: 10 MB
% 1.49/0.50 % (2443598)Instructions burned: 14 (million)
% 1.49/0.50 % (2443601)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2083819894:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.49/0.50 % (2443596)Instruction limit reached!
% 1.49/0.50 % (2443596)------------------------------
% 1.49/0.50 % (2443596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.50 % (2443596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.50 % (2443596)CaDiCaL version: 2.1.3
% 1.49/0.50 % (2443596)Termination reason: Instruction limit
% 1.49/0.50 % (2443596)Termination phase: Property scanning
% 1.49/0.50 % (2443596)Time elapsed: 0.012 s
% 1.49/0.50 % (2443596)Peak memory usage: 10 MB
% 1.49/0.50 % (2443596)Instructions burned: 26 (million)
% 1.49/0.50 % (2443601)Instruction limit reached!
% 1.49/0.50 % (2443601)------------------------------
% 1.49/0.50 % (2443601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.50 % (2443601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.50 % (2443601)CaDiCaL version: 2.1.3
% 1.49/0.50 % (2443601)Termination reason: Instruction limit
% 1.49/0.50 % (2443601)Termination phase: shuffling
% 1.49/0.50 % (2443601)Time elapsed: 0.007 s
% 1.49/0.50 % (2443601)Peak memory usage: 10 MB
% 1.49/0.50 % (2443601)Instructions burned: 16 (million)
% 1.49/0.50 % (2443604)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3945663093: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.49/0.50 % (2443604)Instruction limit reached!
% 1.49/0.50 % (2443604)------------------------------
% 1.49/0.50 % (2443604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.50 % (2443604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.50 % (2443604)CaDiCaL version: 2.1.3
% 1.49/0.50 % (2443604)Termination reason: Instruction limit
% 1.49/0.50 % (2443604)Termination phase: shuffling
% 1.49/0.50 % (2443604)Time elapsed: 0.002 s
% 1.49/0.50 % (2443604)Peak memory usage: 10 MB
% 1.49/0.50 % (2443604)Instructions burned: 3 (million)
% 1.49/0.50 % (2443607)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1725550605:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.49/0.50 % (2443609)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1594599553:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.49/0.50 % (2443610)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.49/0.50 % (2443610)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.49/0.54 % (2443610)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=3576896262:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.49/0.54 % (2443612)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.49/0.54 % (2443607)Instruction limit reached!
% 1.49/0.54 % (2443607)------------------------------
% 1.49/0.54 % (2443607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443607)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443607)Termination reason: Instruction limit
% 1.49/0.54 % (2443607)Termination phase: Property scanning
% 1.49/0.54 % (2443607)Time elapsed: 0.011 s
% 1.49/0.54 % (2443607)Peak memory usage: 10 MB
% 1.49/0.54 % (2443607)Instructions burned: 24 (million)
% 1.49/0.54 % (2443606)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=4040302819:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.49/0.54 % (2443612)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=2958465854:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.49/0.54 % (2443610)Instruction limit reached!
% 1.49/0.54 % (2443610)------------------------------
% 1.49/0.54 % (2443610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443610)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443610)Termination reason: Instruction limit
% 1.49/0.54 % (2443610)Termination phase: shuffling
% 1.49/0.54 % (2443610)Time elapsed: 0.006 s
% 1.49/0.54 % (2443610)Peak memory usage: 10 MB
% 1.49/0.54 % (2443610)Instructions burned: 14 (million)
% 1.49/0.54 % (2443612)Instruction limit reached!
% 1.49/0.54 % (2443612)------------------------------
% 1.49/0.54 % (2443612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443612)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443612)Termination reason: Instruction limit
% 1.49/0.54 % (2443612)Termination phase: shuffling
% 1.49/0.54 % (2443612)Time elapsed: 0.004 s
% 1.49/0.54 % (2443612)Peak memory usage: 10 MB
% 1.49/0.54 % (2443612)Instructions burned: 9 (million)
% 1.49/0.54 % (2443616)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=3551174754:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.49/0.54 % (2443609)Instruction limit reached!
% 1.49/0.54 % (2443609)------------------------------
% 1.49/0.54 % (2443609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443609)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443609)Termination reason: Instruction limit
% 1.49/0.54 % (2443609)Termination phase: Property scanning
% 1.49/0.54 % (2443609)Time elapsed: 0.026 s
% 1.49/0.54 % (2443609)Peak memory usage: 11 MB
% 1.49/0.54 % (2443609)Instructions burned: 61 (million)
% 1.49/0.54 % (2443606)Instruction limit reached!
% 1.49/0.54 % (2443606)------------------------------
% 1.49/0.54 % (2443606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443606)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443606)Termination reason: Instruction limit
% 1.49/0.54 % (2443606)Termination phase: Property scanning
% 1.49/0.54 % (2443606)Time elapsed: 0.022 s
% 1.49/0.54 % (2443606)Peak memory usage: 10 MB
% 1.49/0.54 % (2443606)Instructions burned: 26 (million)
% 1.49/0.54 % (2443620)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3440493967:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.49/0.54 % (2443616)Instruction limit reached!
% 1.49/0.54 % (2443616)------------------------------
% 1.49/0.54 % (2443616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443616)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443616)Termination reason: Instruction limit
% 1.49/0.54 % (2443616)Termination phase: Property scanning
% 1.49/0.54 % (2443616)Time elapsed: 0.014 s
% 1.49/0.54 % (2443616)Peak memory usage: 10 MB
% 1.49/0.54 % (2443616)Instructions burned: 32 (million)
% 1.49/0.54 % (2443619)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3456277498:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.49/0.54 % (2443620)Instruction limit reached!
% 1.49/0.54 % (2443620)------------------------------
% 1.49/0.54 % (2443620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443620)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443620)Termination reason: Instruction limit
% 1.49/0.54 % (2443620)Termination phase: Property scanning
% 1.49/0.54 % (2443620)Time elapsed: 0.011 s
% 1.49/0.54 % (2443620)Peak memory usage: 10 MB
% 1.49/0.54 % (2443620)Instructions burned: 24 (million)
% 1.49/0.54 % (2443622)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3036384837:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.49/0.54 % (2443619)Instruction limit reached!
% 1.49/0.54 % (2443619)------------------------------
% 1.49/0.54 % (2443619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443619)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443619)Termination reason: Instruction limit
% 1.49/0.54 % (2443619)Termination phase: shuffling
% 1.49/0.54 % (2443619)Time elapsed: 0.007 s
% 1.49/0.54 % (2443619)Peak memory usage: 10 MB
% 1.49/0.54 % (2443619)Instructions burned: 8 (million)
% 1.49/0.54 % (2443623)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3178851643:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.49/0.54 % (2443599)Instruction limit reached!
% 1.49/0.54 % (2443599)------------------------------
% 1.49/0.54 % (2443599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443599)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443599)Termination reason: Instruction limit
% 1.49/0.54 % (2443599)Termination phase: Saturation
% 1.49/0.54 % (2443599)Time elapsed: 0.088 s
% 1.49/0.54 % (2443599)Peak memory usage: 14 MB
% 1.49/0.54 % (2443599)Instructions burned: 330 (million)
% 1.49/0.54 % (2443622)Instruction limit reached!
% 1.49/0.54 % (2443622)------------------------------
% 1.49/0.54 % (2443622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443622)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443622)Termination reason: Instruction limit
% 1.49/0.54 % (2443622)Termination phase: Property scanning
% 1.49/0.54 % (2443622)Time elapsed: 0.009 s
% 1.49/0.54 % (2443622)Peak memory usage: 10 MB
% 1.49/0.54 % (2443622)Instructions burned: 21 (million)
% 1.49/0.54 % (2443625)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2890282959:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.49/0.54 % (2443631)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.49/0.54 % (2443631)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2936605374:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 1.49/0.54 % (2443631)Instruction limit reached!
% 1.49/0.54 % (2443631)------------------------------
% 1.49/0.54 % (2443631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443631)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443631)Termination reason: Instruction limit
% 1.49/0.54 % (2443631)Termination phase: shuffling
% 1.49/0.54 % (2443631)Time elapsed: 0.002 s
% 1.49/0.54 % (2443631)Peak memory usage: 10 MB
% 1.49/0.54 % (2443631)Instructions burned: 7 (million)
% 1.49/0.54 % (2443628)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2045921571:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 1.49/0.54 % (2443632)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2727937983:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 1.49/0.54 % (2443630)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2003003892:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 1.49/0.54 % (2443635)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=1125733068: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.49/0.54 % (2443630)Instruction limit reached!
% 1.49/0.54 % (2443630)------------------------------
% 1.49/0.54 % (2443630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443630)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443630)Termination reason: Instruction limit
% 1.49/0.54 % (2443630)Termination phase: Property scanning
% 1.49/0.54 % (2443630)Time elapsed: 0.018 s
% 1.49/0.54 % (2443630)Peak memory usage: 11 MB
% 1.49/0.54 % (2443630)Instructions burned: 42 (million)
% 1.49/0.54 % (2443628) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2443559-2443628"...
% 1.49/0.54 % (2443628)...printing done.
% 1.49/0.54 % (2443628)Refutation found. Thanks to Tanya!
% 1.49/0.54 % SZS status Theorem for theBenchmark
% 1.49/0.54 % SZS output start Proof for theBenchmark
% 1.49/0.54 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.49/0.54 thf(func_def_0, type, is_of: ($i > ($i > $o) > $o)).
% 1.49/0.54 thf(func_def_2, type, all_of: (($i > $o) > ($i > $o) > $o)).
% 1.49/0.54 thf(func_def_3, type, eps: (($i > $o) > $i)).
% 1.49/0.54 thf(func_def_4, type, in: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_5, type, d_Subq: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_7, type, union: ($i > $i)).
% 1.49/0.54 thf(func_def_8, type, power: ($i > $i)).
% 1.49/0.54 thf(func_def_9, type, repl: ($i > ($i > $i) > $i)).
% 1.49/0.54 thf(func_def_10, type, d_Union_closed: ($i > $o)).
% 1.49/0.54 thf(func_def_11, type, d_Power_closed: ($i > $o)).
% 1.49/0.54 thf(func_def_12, type, d_Repl_closed: ($i > $o)).
% 1.49/0.54 thf(func_def_13, type, d_ZF_closed: ($i > $o)).
% 1.49/0.54 thf(func_def_14, type, univof: ($i > $i)).
% 1.49/0.54 thf(func_def_15, type, if: ($o > $i > $i > $i)).
% 1.49/0.54 thf(func_def_16, type, nIn: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_17, type, d_UPair: ($i > $i > $i)).
% 1.49/0.54 thf(func_def_18, type, d_Sing: ($i > $i)).
% 1.49/0.54 thf(func_def_19, type, binunion: ($i > $i > $i)).
% 1.49/0.54 thf(func_def_20, type, famunion: ($i > ($i > $i) > $i)).
% 1.49/0.54 thf(func_def_21, type, d_Sep: ($i > ($i > $o) > $i)).
% 1.49/0.54 thf(func_def_22, type, d_ReplSep: ($i > ($i > $o) > ($i > $i) > $i)).
% 1.49/0.54 thf(func_def_23, type, setminus: ($i > $i > $i)).
% 1.49/0.54 thf(func_def_24, type, d_In_rec_G: (($i > ($i > $i) > $i) > $i > $i > $o)).
% 1.49/0.54 thf(func_def_25, type, d_In_rec: (($i > ($i > $i) > $i) > $i > $i)).
% 1.49/0.54 thf(func_def_26, type, ordsucc: ($i > $i)).
% 1.49/0.54 thf(func_def_27, type, nat_p: ($i > $o)).
% 1.49/0.54 thf(func_def_29, type, d_Inj1: ($i > $i)).
% 1.49/0.54 thf(func_def_30, type, d_Inj0: ($i > $i)).
% 1.49/0.54 thf(func_def_31, type, d_Unj: ($i > $i)).
% 1.49/0.54 thf(func_def_32, type, pair: ($i > $i > $i)).
% 1.49/0.54 thf(func_def_33, type, proj0: ($i > $i)).
% 1.49/0.54 thf(func_def_34, type, proj1: ($i > $i)).
% 1.49/0.54 thf(func_def_35, type, d_Sigma: ($i > ($i > $i) > $i)).
% 1.49/0.54 thf(func_def_36, type, setprod: ($i > $i > $i)).
% 1.49/0.54 thf(func_def_37, type, ap: ($i > $i > $i)).
% 1.49/0.54 thf(func_def_38, type, pair_p: ($i > $o)).
% 1.49/0.54 thf(func_def_39, type, d_Pi: ($i > ($i > $i) > $i)).
% 1.49/0.54 thf(func_def_40, type, imp: ($o > $o > $o)).
% 1.49/0.54 thf(func_def_41, type, d_not: ($o > $o)).
% 1.49/0.54 thf(func_def_42, type, wel: ($o > $o)).
% 1.49/0.54 thf(func_def_43, type, obvious: $o).
% 1.49/0.54 thf(func_def_44, type, l_ec: ($o > $o > $o)).
% 1.49/0.54 thf(func_def_45, type, d_and: ($o > $o > $o)).
% 1.49/0.54 thf(func_def_46, type, l_or: ($o > $o > $o)).
% 1.49/0.54 thf(func_def_47, type, orec: ($o > $o > $o)).
% 1.49/0.54 thf(func_def_48, type, l_iff: ($o > $o > $o)).
% 1.49/0.54 thf(func_def_49, type, all: ($i > ($i > $o) > $o)).
% 1.49/0.54 thf(func_def_50, type, non: ($i > ($i > $o) > $i > $o)).
% 1.49/0.54 thf(func_def_51, type, l_some: ($i > ($i > $o) > $o)).
% 1.49/0.54 thf(func_def_52, type, or3: ($o > $o > $o > $o)).
% 1.49/0.54 thf(func_def_53, type, and3: ($o > $o > $o > $o)).
% 1.49/0.54 thf(func_def_54, type, ec3: ($o > $o > $o > $o)).
% 1.49/0.54 thf(func_def_55, type, orec3: ($o > $o > $o > $o)).
% 1.49/0.54 thf(func_def_56, type, e_is: ($i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_57, type, amone: ($i > ($i > $o) > $o)).
% 1.49/0.54 thf(func_def_58, type, one: ($i > ($i > $o) > $o)).
% 1.49/0.54 thf(func_def_59, type, ind: ($i > ($i > $o) > $i)).
% 1.49/0.54 thf(func_def_60, type, injective: ($i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_61, type, image: ($i > $i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_62, type, tofs: ($i > $i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_63, type, soft: ($i > $i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_64, type, inverse: ($i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_65, type, surjective: ($i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_66, type, bijective: ($i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_67, type, invf: ($i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_68, type, inj_h: ($i > $i > $i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_69, type, e_in: ($i > ($i > $o) > $i > $i)).
% 1.49/0.54 thf(func_def_70, type, out: ($i > ($i > $o) > $i > $i)).
% 1.49/0.54 thf(func_def_71, type, d_pair: ($i > $i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_72, type, first: ($i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_73, type, second: ($i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_74, type, prop1: ($o > $i > $i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_75, type, ite: ($o > $i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_76, type, wissel_wa: ($i > $i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_77, type, wissel_wb: ($i > $i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_78, type, wissel: ($i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_79, type, changef: ($i > $i > $i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_80, type, r_ec: ($o > $o > $o)).
% 1.49/0.54 thf(func_def_81, type, esti: ($i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_82, type, empty: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_83, type, nonempty: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_84, type, incl: ($i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_85, type, st_disj: ($i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_86, type, nissetprop: ($i > $i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_87, type, unmore: ($i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_88, type, ecelt: ($i > ($i > $i > $o) > $i > $i)).
% 1.49/0.54 thf(func_def_89, type, ecp: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.49/0.54 thf(func_def_90, type, anec: ($i > ($i > $i > $o) > $i > $o)).
% 1.49/0.54 thf(func_def_91, type, ect: ($i > ($i > $i > $o) > $i)).
% 1.49/0.54 thf(func_def_92, type, ectset: ($i > ($i > $i > $o) > $i > $i)).
% 1.49/0.54 thf(func_def_93, type, ectelt: ($i > ($i > $i > $o) > $i > $i)).
% 1.49/0.54 thf(func_def_94, type, ecect: ($i > ($i > $i > $o) > $i > $i)).
% 1.49/0.54 thf(func_def_95, type, fixfu: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.49/0.54 thf(func_def_96, type, d_10_prop1: ($i > ($i > $i > $o) > $i > $i > $i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_97, type, prop2: ($i > ($i > $i > $o) > $i > $i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_98, type, indeq: ($i > ($i > $i > $o) > $i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_99, type, fixfu2: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.49/0.54 thf(func_def_100, type, d_11_i: ($i > ($i > $i > $o) > $i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_101, type, indeq2: ($i > ($i > $i > $o) > $i > $i > $i > $i > $i)).
% 1.49/0.54 thf(func_def_103, type, n_is: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_104, type, nis: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_105, type, n_in: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_106, type, n_some: (($i > $o) > $o)).
% 1.49/0.54 thf(func_def_107, type, n_all: (($i > $o) > $o)).
% 1.49/0.54 thf(func_def_108, type, n_one: (($i > $o) > $o)).
% 1.49/0.54 thf(func_def_110, type, cond1: ($i > $o)).
% 1.49/0.54 thf(func_def_111, type, cond2: ($i > $o)).
% 1.49/0.54 thf(func_def_112, type, i1_s: (($i > $o) > $i)).
% 1.49/0.54 thf(func_def_113, type, d_22_prop1: ($i > $o)).
% 1.49/0.54 thf(func_def_114, type, d_23_prop1: ($i > $o)).
% 1.49/0.54 thf(func_def_115, type, d_24_prop1: ($i > $o)).
% 1.49/0.54 thf(func_def_116, type, d_24_prop2: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_117, type, prop3: ($i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_118, type, prop4: ($i > $o)).
% 1.49/0.54 thf(func_def_119, type, d_24_g: ($i > $i)).
% 1.49/0.54 thf(func_def_120, type, plus: ($i > $i)).
% 1.49/0.54 thf(func_def_121, type, n_pl: ($i > $i > $i)).
% 1.49/0.54 thf(func_def_122, type, d_25_prop1: ($i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_123, type, d_26_prop1: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_124, type, d_27_prop1: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_125, type, d_28_prop1: ($i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_126, type, diffprop: ($i > $i > $i > $o)).
% 1.49/0.54 thf(func_def_127, type, d_29_ii: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_128, type, iii: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_129, type, d_29_prop1: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_130, type, moreis: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_131, type, lessis: ($i > $i > $o)).
% 1.49/0.54 thf(func_def_132, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.49/0.54 thf(func_def_133, type, vIMP: ($o > $o > $o)).
% 1.49/0.54 thf(func_def_134, type, db0: !>[X0: $tType]:(X0)).
% 1.49/0.54 thf(func_def_135, type, db1: !>[X0: $tType]:(X0)).
% 1.49/0.54 thf(func_def_136, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.49/0.54 thf(func_def_139, type, db2: !>[X0: $tType]:(X0)).
% 1.49/0.54 thf(func_def_140, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.49/0.54 thf(func_def_141, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.49/0.54 thf(func_def_142, type, db6: !>[X0: $tType]:(X0)).
% 1.49/0.54 thf(func_def_143, type, db5: !>[X0: $tType]:(X0)).
% 1.49/0.54 thf(func_def_144, type, db4: !>[X0: $tType]:(X0)).
% 1.49/0.54 thf(func_def_145, type, db3: !>[X0: $tType]:(X0)).
% 1.49/0.54 thf(func_def_146, type, vAND: ($o > $o > $o)).
% 1.49/0.54 thf(func_def_147, type, vNOT: ($o > $o)).
% 1.49/0.54 thf(func_def_148, type, db7: !>[X0: $tType]:(X0)).
% 1.49/0.54 thf(func_def_149, type, vOR: ($o > $o > $o)).
% 1.49/0.54 thf(func_def_150, type, sK0: (($i > $i) > $i > ($i > $i) > $i)).
% 1.49/0.54 thf(func_def_151, type, sK1: (($i > $o) > $i)).
% 1.49/0.54 thf(func_def_152, type, sK2: ($i > $i > $i > $i > $i)).
% 1.49/0.54 thf(f2,axiom,(
% 1.49/0.54 (all_of = (^[X0 : ($i > $o), X1 : ($i > $o)] : (! [X2 : $i] : ((is_of @ X2 @ X0) => (X1 @ X2)))))),
% 1.49/0.54 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_all_of)).
% 1.49/0.54 thf(f74,axiom,(
% 1.49/0.54 (imp = (^[X0 : $o, X1 : $o] : (X0 => X1)))),
% 1.49/0.54 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_imp)).
% 1.49/0.54 thf(f81,axiom,(
% 1.49/0.54 (l_or = (^[X0 : $o] : ((imp @ (d_not @ X0)))))),
% 1.49/0.54 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_l_or)).
% 1.49/0.54 thf(f157,axiom,(
% 1.49/0.54 (n_is = ((e_is @ nat)))),
% 1.49/0.54 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_n_is)).
% 1.49/0.54 thf(f205,axiom,(
% 1.49/0.54 ((^[X0 : $i, X1 : $i] : ((n_some @ (diffprop @ X0 @ X1)))) = d_29_ii)),
% 1.49/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_d_29_ii)).
% 1.49/0.54 thf(f214,axiom,(
% 1.49/0.54 (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.49/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz11)).
% 1.49/0.54 thf(f215,axiom,(
% 1.49/0.54 (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.49/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz12)).
% 1.49/0.54 thf(f216,axiom,(
% 1.49/0.54 ((^[X0 : $i, X1 : $i] : ((l_or @ (d_29_ii @ X0 @ X1) @ (n_is @ X0 @ X1)))) = moreis)),
% 1.49/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_moreis)).
% 1.49/0.54 thf(f217,axiom,(
% 1.49/0.54 (lessis = (^[X0 : $i, X1 : $i] : ((l_or @ (iii @ X0 @ X1) @ (n_is @ X0 @ X1)))))),
% 1.49/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_lessis)).
% 1.49/0.54 thf(f221,axiom,(
% 1.49/0.54 (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.49/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz10d)).
% 1.49/0.54 thf(f224,axiom,(
% 1.49/0.54 (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.49/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz10g)).
% 1.49/0.54 thf(f226,axiom,(
% 1.49/0.54 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((d_not @ (moreis @ X0 @ X1)) => (iii @ X0 @ X1)))))))),
% 1.49/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz10j)).
% 1.49/0.54 thf(f227,conjecture,(
% 1.49/0.54 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((d_not @ (lessis @ X0 @ X1)) => (d_29_ii @ X0 @ X1)))))))),
% 1.49/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz10k)).
% 1.49/0.54 thf(f228,negated_conjecture,(
% 1.49/0.54 ~(all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((d_not @ (lessis @ X0 @ X1)) => (d_29_ii @ X0 @ X1)))))))),
% 1.49/0.54 inference(negated_conjecture,[status(cth)],[f227])).
% 1.49/0.54 thf(f304,plain,(
% 1.49/0.54 (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.49/0.54 inference(rectify,[],[f214])).
% 1.49/0.54 thf(f305,plain,(
% 1.49/0.54 (((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))))))) = $true)),
% 1.49/0.54 inference(fool_elimination,[],[f304])).
% 1.49/0.54 thf(f306,plain,(
% 1.49/0.54 (all_of = (^[X0 : ($i > $o), X1 : ($i > $o)] : (! [X2 : $i] : ((is_of @ X2 @ X0) => (X1 @ X2)))))),
% 1.49/0.54 inference(rectify,[],[f2])).
% 1.49/0.54 thf(f307,plain,(
% 1.49/0.54 (all_of = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))))),
% 1.49/0.54 inference(fool_elimination,[],[f306])).
% 1.49/0.54 thf(f342,plain,(
% 1.49/0.54 (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.49/0.54 inference(rectify,[],[f215])).
% 1.49/0.54 thf(f343,plain,(
% 1.49/0.54 (((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))))))) = $true)),
% 1.49/0.54 inference(fool_elimination,[],[f342])).
% 1.49/0.54 thf(f374,plain,(
% 1.49/0.54 (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.49/0.54 inference(rectify,[],[f224])).
% 1.49/0.54 thf(f375,plain,(
% 1.49/0.54 (((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_29_ii @ Y0 @ Y1) => (d_not @ (lessis @ Y0 @ Y1)))))))) = $true)),
% 1.49/0.54 inference(fool_elimination,[],[f374])).
% 1.49/0.54 thf(f411,plain,(
% 1.49/0.54 (imp = (^[X0 : $o, X1 : $o] : (X0 => X1)))),
% 1.49/0.54 inference(rectify,[],[f74])).
% 1.49/0.54 thf(f412,plain,(
% 1.49/0.54 (imp = (^[Y0 : $o]: ((^[Y1 : $o]: (Y0 => Y1)))))),
% 1.49/0.54 inference(fool_elimination,[],[f411])).
% 1.49/0.54 thf(f431,plain,(
% 1.49/0.54 (d_29_ii = (^[Y0 : $i]: ((^[Y1 : $i]: (n_some @ (diffprop @ Y0 @ Y1))))))),
% 1.49/0.54 inference(fool_elimination,[],[f205])).
% 1.49/0.54 thf(f436,plain,(
% 1.49/0.54 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((d_not @ (moreis @ X1 @ X3)) => (iii @ X1 @ X3)))))))),
% 1.49/0.54 inference(rectify,[],[f226])).
% 1.49/0.54 thf(f437,plain,(
% 1.49/0.54 (((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_not @ (moreis @ Y0 @ Y1)) => (iii @ Y0 @ Y1))))))) = $true)),
% 1.49/0.54 inference(fool_elimination,[],[f436])).
% 1.49/0.54 thf(f460,plain,(
% 1.49/0.54 (lessis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (iii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.49/0.54 inference(fool_elimination,[],[f217])).
% 1.49/0.54 thf(f461,plain,(
% 1.49/0.54 ~(all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((d_not @ (lessis @ X1 @ X3)) => (d_29_ii @ X1 @ X3)))))))),
% 1.49/0.54 inference(rectify,[],[f228])).
% 1.49/0.54 thf(f462,plain,(
% 1.49/0.54 ~ ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_not @ (lessis @ Y0 @ Y1)) => (d_29_ii @ Y0 @ Y1))))))))),
% 1.49/0.54 inference(fool_elimination,[],[f461])).
% 1.49/0.54 thf(f541,plain,(
% 1.49/0.54 (l_or = (^[Y0 : $o]: (imp @ (d_not @ Y0))))),
% 1.49/0.54 inference(fool_elimination,[],[f81])).
% 1.49/0.54 thf(f551,plain,(
% 1.49/0.54 (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.49/0.54 inference(rectify,[],[f221])).
% 1.49/0.54 thf(f552,plain,(
% 1.49/0.54 ($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.49/0.54 inference(fool_elimination,[],[f551])).
% 1.49/0.54 thf(f555,plain,(
% 1.49/0.54 (moreis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (d_29_ii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.49/0.54 inference(fool_elimination,[],[f216])).
% 1.49/0.54 thf(f590,plain,(
% 1.49/0.54 ($true != ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_not @ (lessis @ Y0 @ Y1)) => (d_29_ii @ Y0 @ Y1))))))))),
% 1.49/0.54 inference(flattening,[],[f462])).
% 1.49/0.54 thf(f610,plain,(
% 1.49/0.54 ($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.49/0.54 inference(cnf_transformation,[],[f552])).
% 1.49/0.54 thf(f611,plain,(
% 1.49/0.54 (d_29_ii = (^[Y0 : $i]: ((^[Y1 : $i]: (n_some @ (diffprop @ Y0 @ Y1))))))),
% 1.49/0.54 inference(cnf_transformation,[],[f431])).
% 1.49/0.54 thf(f622,plain,(
% 1.49/0.54 (moreis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (d_29_ii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.49/0.54 inference(cnf_transformation,[],[f555])).
% 1.49/0.54 thf(f625,plain,(
% 1.49/0.54 (n_is = ((e_is @ nat)))),
% 1.49/0.54 inference(cnf_transformation,[],[f157])).
% 1.49/0.54 thf(f627,plain,(
% 1.49/0.54 (all_of = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))))),
% 1.49/0.54 inference(cnf_transformation,[],[f307])).
% 1.49/0.54 thf(f631,plain,(
% 1.49/0.54 (((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_29_ii @ Y0 @ Y1) => (d_not @ (lessis @ Y0 @ Y1)))))))) = $true)),
% 1.49/0.54 inference(cnf_transformation,[],[f375])).
% 1.49/0.54 thf(f633,plain,(
% 1.49/0.54 (l_or = (^[Y0 : $o]: (imp @ (d_not @ Y0))))),
% 1.49/0.54 inference(cnf_transformation,[],[f541])).
% 1.49/0.54 thf(f637,plain,(
% 1.49/0.54 (lessis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (iii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.49/0.54 inference(cnf_transformation,[],[f460])).
% 1.49/0.54 thf(f638,plain,(
% 1.49/0.54 (((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))))))) = $true)),
% 1.49/0.54 inference(cnf_transformation,[],[f343])).
% 1.49/0.54 thf(f647,plain,(
% 1.49/0.54 (((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))))))) = $true)),
% 1.49/0.54 inference(cnf_transformation,[],[f305])).
% 1.49/0.54 thf(f651,plain,(
% 1.49/0.54 (((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_not @ (moreis @ Y0 @ Y1)) => (iii @ Y0 @ Y1))))))) = $true)),
% 1.49/0.54 inference(cnf_transformation,[],[f437])).
% 1.49/0.54 thf(f654,plain,(
% 1.49/0.54 ($true != ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_not @ (lessis @ Y0 @ Y1)) => (d_29_ii @ Y0 @ Y1))))))))),
% 1.49/0.54 inference(cnf_transformation,[],[f590])).
% 1.49/0.54 thf(f662,plain,(
% 1.49/0.54 (imp = (^[Y0 : $o]: ((^[Y1 : $o]: (Y0 => Y1)))))),
% 1.49/0.54 inference(cnf_transformation,[],[f412])).
% 1.49/0.54 thf(f665,definition,(
% 1.49/0.54 ($false != $true)),
% 1.49/0.54 introduced(theory,[fool_distinctness_axiom])).
% 1.49/0.54 thf(f666,definition,(
% 1.49/0.54 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.49/0.54 introduced(theory,[fool_exhaustiveness_axiom])).
% 1.49/0.54 thf(f667,plain,(
% 1.49/0.54 (l_or = (^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: (Y1 => Y2)))) @ (d_not @ Y0))))),
% 1.49/0.54 inference(definition_unfolding,[],[f633,f662])).
% 1.49/0.54 thf(f668,plain,(
% 1.49/0.54 (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.49/0.54 inference(definition_unfolding,[],[f622,f667,f611,f625])).
% 1.49/0.54 thf(f669,plain,(
% 1.49/0.54 (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.49/0.54 inference(definition_unfolding,[],[f637,f667,f625])).
% 1.49/0.54 thf(f673,plain,(
% 1.49/0.54 ((((^[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)))))))) = $true)),
% 1.49/0.54 inference(definition_unfolding,[],[f610,f627,f627,f669,f611])).
% 1.49/0.54 thf(f684,plain,(
% 1.49/0.54 ((((^[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)))))))) = $true)),
% 1.49/0.54 inference(definition_unfolding,[],[f631,f627,f627,f611,f669])).
% 1.49/0.54 thf(f689,plain,(
% 1.49/0.54 ((((^[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))))))) = $true)),
% 1.49/0.54 inference(definition_unfolding,[],[f638,f627,f627,f611])).
% 1.49/0.54 thf(f696,plain,(
% 1.49/0.54 ((((^[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))))))) = $true)),
% 1.49/0.54 inference(definition_unfolding,[],[f647,f627,f627,f611])).
% 1.49/0.54 thf(f700,plain,(
% 1.49/0.54 ((((^[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]: ((^[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)) => (iii @ Y0 @ Y1))))))) = $true)),
% 1.49/0.54 inference(definition_unfolding,[],[f651,f627,f627,f668])).
% 1.49/0.54 thf(f702,plain,(
% 1.49/0.54 ((((^[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]: ((^[Y4 : $o]: ((^[Y5 : $o]: ((^[Y6 : $o]: (Y5 => Y6)))) @ (d_not @ Y4))) @ (iii @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y0 @ Y1)) => ((^[Y2 : $i]: ((^[Y3 : $i]: (n_some @ (diffprop @ Y2 @ Y3))))) @ Y0 @ Y1))))))) != $true)),
% 1.49/0.54 inference(definition_unfolding,[],[f654,f627,f627,f669,f611])).
% 1.49/0.54 thf(f723,plain,(
% 1.49/0.54 ($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.49/0.54 inference(beta-eta_normalization,[],[f689])).
% 1.49/0.54 thf(f724,plain,(
% 1.49/0.54 ( ! [X1 : $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)))))))) @ X1)) = $true)) )),
% 1.49/0.54 inference(pi_proxy_clausification,[],[f723])).
% 1.49/0.54 thf(f725,plain,(
% 1.49/0.54 ( ! [X1 : $i] : (((((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)))))))) = $true)) )),
% 1.49/0.54 inference(beta-eta_normalization,[],[f724])).
% 1.49/0.54 thf(f726,plain,(
% 1.49/0.54 ( ! [X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((iii @ X1 @ Y0) => (n_some @ (diffprop @ Y0 @ X1))))))) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f725])).
% 1.49/0.54 thf(f727,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ((((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((iii @ X1 @ Y0) => (n_some @ (diffprop @ Y0 @ X1))))) @ X2)) = $true)) )),
% 1.49/0.54 inference(pi_proxy_clausification,[],[f726])).
% 1.49/0.54 thf(f728,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((iii @ X1 @ X2) => (n_some @ (diffprop @ X2 @ X1))))) = $true)) )),
% 1.49/0.54 inference(beta-eta_normalization,[],[f727])).
% 1.49/0.54 thf(f729,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ((((iii @ X1 @ X2) => (n_some @ (diffprop @ X2 @ X1)))) = $true)) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f728])).
% 1.49/0.54 thf(f730,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((n_some @ (diffprop @ X2 @ X1))) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((iii @ X1 @ X2)))) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f729])).
% 1.49/0.54 thf(f804,plain,(
% 1.49/0.54 (((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((d_not @ ((d_not @ (iii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1))) => (n_some @ (diffprop @ Y0 @ Y1)))))))))) != $true)),
% 1.49/0.54 inference(beta-eta_normalization,[],[f702])).
% 1.49/0.54 thf(f805,plain,(
% 1.49/0.54 ($false = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((d_not @ ((d_not @ (iii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1))) => (n_some @ (diffprop @ Y0 @ Y1)))))))) @ sK3)))),
% 1.49/0.54 inference(sigma_proxy_clausification,[],[f804])).
% 1.49/0.54 thf(f806,plain,(
% 1.49/0.54 ($false = (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_not @ ((d_not @ (iii @ sK3 @ Y0)) => (e_is @ nat @ sK3 @ Y0))) => (n_some @ (diffprop @ sK3 @ Y0)))))))))),
% 1.49/0.54 inference(beta-eta_normalization,[],[f805])).
% 1.49/0.54 thf(f807,plain,(
% 1.49/0.54 ($false = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_not @ ((d_not @ (iii @ sK3 @ Y0)) => (e_is @ nat @ sK3 @ Y0))) => (n_some @ (diffprop @ sK3 @ Y0))))))))),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f806])).
% 1.49/0.54 thf(f808,plain,(
% 1.49/0.54 ($true = ((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f806])).
% 1.49/0.54 thf(f809,plain,(
% 1.49/0.54 ($false = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_not @ ((d_not @ (iii @ sK3 @ Y0)) => (e_is @ nat @ sK3 @ Y0))) => (n_some @ (diffprop @ sK3 @ Y0))))) @ sK4)))),
% 1.49/0.54 inference(sigma_proxy_clausification,[],[f807])).
% 1.49/0.54 thf(f810,plain,(
% 1.49/0.54 ($false = (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((d_not @ ((d_not @ (iii @ sK3 @ sK4)) => (e_is @ nat @ sK3 @ sK4))) => (n_some @ (diffprop @ sK3 @ sK4))))))),
% 1.49/0.54 inference(beta-eta_normalization,[],[f809])).
% 1.49/0.54 thf(f811,plain,(
% 1.49/0.54 ($false = (((d_not @ ((d_not @ (iii @ sK3 @ sK4)) => (e_is @ nat @ sK3 @ sK4))) => (n_some @ (diffprop @ sK3 @ sK4)))))),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f810])).
% 1.49/0.54 thf(f812,plain,(
% 1.49/0.54 (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true)),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f810])).
% 1.49/0.54 thf(f813,plain,(
% 1.49/0.54 ($false = ((n_some @ (diffprop @ sK3 @ sK4))))),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f811])).
% 1.49/0.54 thf(f814,plain,(
% 1.49/0.54 (((d_not @ ((d_not @ (iii @ sK3 @ sK4)) => (e_is @ nat @ sK3 @ sK4)))) = $true)),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f811])).
% 1.49/0.54 thf(f822,plain,(
% 1.49/0.54 ($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.49/0.54 inference(beta-eta_normalization,[],[f673])).
% 1.49/0.54 thf(f823,plain,(
% 1.49/0.54 ( ! [X1 : $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))))))))) @ X1)) = $true)) )),
% 1.49/0.54 inference(pi_proxy_clausification,[],[f822])).
% 1.49/0.54 thf(f824,plain,(
% 1.49/0.54 ( ! [X1 : $i] : (((((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))))))))) = $true)) )),
% 1.49/0.54 inference(beta-eta_normalization,[],[f823])).
% 1.49/0.54 thf(f825,plain,(
% 1.49/0.54 ( ! [X1 : $i] : ((((!! @ $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)))))))) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f824])).
% 1.49/0.54 thf(f826,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $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)))))) @ X2)) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.49/0.54 inference(pi_proxy_clausification,[],[f825])).
% 1.49/0.54 thf(f827,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ((((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)))))) = $true)) )),
% 1.49/0.54 inference(beta-eta_normalization,[],[f826])).
% 1.49/0.54 thf(f828,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)) => (d_not @ (n_some @ (diffprop @ X1 @ X2))))) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f827])).
% 1.49/0.54 thf(f829,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_not @ (n_some @ (diffprop @ X1 @ X2)))) = $true) | ($false = (((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2))))) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f828])).
% 1.49/0.54 thf(f830,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((e_is @ nat @ X1 @ X2))) | (((d_not @ (n_some @ (diffprop @ X1 @ X2)))) = $true)) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f829])).
% 1.49/0.54 thf(f831,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((d_not @ (n_some @ (diffprop @ X1 @ X2)))) = $true) | (((d_not @ (iii @ X1 @ X2))) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f829])).
% 1.49/0.54 thf(f869,plain,(
% 1.49/0.54 (((!! @ $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))))))))))) = $true)),
% 1.49/0.54 inference(beta-eta_normalization,[],[f684])).
% 1.49/0.54 thf(f870,plain,(
% 1.49/0.54 ( ! [X1 : $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))))))))) @ X1)) = $true)) )),
% 1.49/0.54 inference(pi_proxy_clausification,[],[f869])).
% 1.49/0.54 thf(f871,plain,(
% 1.49/0.54 ( ! [X1 : $i] : (((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ X1 @ Y0)) => (d_not @ ((d_not @ (iii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0))))))))) = $true)) )),
% 1.49/0.54 inference(beta-eta_normalization,[],[f870])).
% 1.49/0.54 thf(f872,plain,(
% 1.49/0.54 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ X1 @ Y0)) => (d_not @ ((d_not @ (iii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0)))))))))) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f871])).
% 1.49/0.54 thf(f873,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ((((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ X1 @ Y0)) => (d_not @ ((d_not @ (iii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0)))))) @ X2)) = $true)) )),
% 1.49/0.54 inference(pi_proxy_clausification,[],[f872])).
% 1.49/0.54 thf(f874,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((n_some @ (diffprop @ X1 @ X2)) => (d_not @ ((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)))))) = $true)) )),
% 1.49/0.54 inference(beta-eta_normalization,[],[f873])).
% 1.49/0.54 thf(f875,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ((((n_some @ (diffprop @ X1 @ X2)) => (d_not @ ((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2))))) = $true)) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f874])).
% 1.49/0.54 thf(f876,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((d_not @ ((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)))) = $true) | (((n_some @ (diffprop @ X1 @ X2))) = $false) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f875])).
% 1.49/0.54 thf(f910,plain,(
% 1.49/0.54 (((!! @ $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))))))))) = $true)),
% 1.49/0.54 inference(beta-eta_normalization,[],[f696])).
% 1.49/0.54 thf(f911,plain,(
% 1.49/0.54 ( ! [X1 : $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))))))) @ X1)) = $true)) )),
% 1.49/0.54 inference(pi_proxy_clausification,[],[f910])).
% 1.49/0.54 thf(f912,plain,(
% 1.49/0.54 ( ! [X1 : $i] : (((((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))))))) = $true)) )),
% 1.49/0.54 inference(beta-eta_normalization,[],[f911])).
% 1.49/0.54 thf(f913,plain,(
% 1.49/0.54 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ X1 @ Y0)) => (iii @ Y0 @ X1)))))) = $true)) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f912])).
% 1.49/0.54 thf(f914,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ X1 @ Y0)) => (iii @ Y0 @ X1)))) @ X2)) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.49/0.54 inference(pi_proxy_clausification,[],[f913])).
% 1.49/0.54 thf(f915,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((n_some @ (diffprop @ X1 @ X2)) => (iii @ X2 @ X1)))) = $true)) )),
% 1.49/0.54 inference(beta-eta_normalization,[],[f914])).
% 1.49/0.54 thf(f916,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($true = (((n_some @ (diffprop @ X1 @ X2)) => (iii @ X2 @ X1))))) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f915])).
% 1.49/0.54 thf(f917,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((n_some @ (diffprop @ X1 @ X2))) = $false) | ($true = ((iii @ X2 @ X1)))) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f916])).
% 1.49/0.54 thf(f939,plain,(
% 1.49/0.54 (((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((d_not @ ((d_not @ (n_some @ (diffprop @ Y0 @ Y1))) => (e_is @ nat @ Y0 @ Y1))) => (iii @ Y0 @ Y1))))))))) = $true)),
% 1.49/0.54 inference(beta-eta_normalization,[],[f700])).
% 1.49/0.54 thf(f940,plain,(
% 1.49/0.54 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((d_not @ ((d_not @ (n_some @ (diffprop @ Y0 @ Y1))) => (e_is @ nat @ Y0 @ Y1))) => (iii @ Y0 @ Y1))))))) @ X1)) = $true)) )),
% 1.49/0.54 inference(pi_proxy_clausification,[],[f939])).
% 1.49/0.54 thf(f941,plain,(
% 1.49/0.54 ( ! [X1 : $i] : (((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_not @ ((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0))) => (iii @ X1 @ Y0))))))) = $true)) )),
% 1.49/0.54 inference(beta-eta_normalization,[],[f940])).
% 1.49/0.54 thf(f942,plain,(
% 1.49/0.54 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_not @ ((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0))) => (iii @ X1 @ Y0)))))) = $true)) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f941])).
% 1.49/0.54 thf(f943,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ((((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((d_not @ ((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0))) => (iii @ X1 @ Y0)))) @ X2)) = $true)) )),
% 1.49/0.54 inference(pi_proxy_clausification,[],[f942])).
% 1.49/0.54 thf(f944,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((d_not @ ((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2))) => (iii @ X1 @ X2)))) = $true)) )),
% 1.49/0.54 inference(beta-eta_normalization,[],[f943])).
% 1.49/0.54 thf(f945,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ((((d_not @ ((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2))) => (iii @ X1 @ X2))) = $true)) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f944])).
% 1.49/0.54 thf(f946,plain,(
% 1.49/0.54 ( ! [X2 : $i,X1 : $i] : (($false = ((d_not @ ((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2))))) | (((iii @ X1 @ X2)) = $true) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f945])).
% 1.49/0.54 thf(f1000,definition,(
% 1.49/0.54 spl5_1 <=> ($false = $true)),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition])).
% 1.49/0.54 thf(f1003,plain,(
% 1.49/0.54 ~spl5_1),
% 1.49/0.54 inference(avatar_split_clause,[],[f665,f1000])).
% 1.49/0.54 thf(f1005,definition,(
% 1.49/0.54 spl5_2 <=> ($true = ((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition])).
% 1.49/0.54 thf(f1007,plain,(
% 1.49/0.54 ($true = ((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ~spl5_2),
% 1.49/0.54 inference(avatar_component_clause,[],[f1005])).
% 1.49/0.54 thf(f1008,plain,(
% 1.49/0.54 spl5_2),
% 1.49/0.54 inference(avatar_split_clause,[],[f808,f1005])).
% 1.49/0.54 thf(f1010,definition,(
% 1.49/0.54 spl5_3 <=> (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true)),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition])).
% 1.49/0.54 thf(f1012,plain,(
% 1.49/0.54 (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true) | ~spl5_3),
% 1.49/0.54 inference(avatar_component_clause,[],[f1010])).
% 1.49/0.54 thf(f1013,plain,(
% 1.49/0.54 spl5_3),
% 1.49/0.54 inference(avatar_split_clause,[],[f812,f1010])).
% 1.49/0.54 thf(f1015,definition,(
% 1.49/0.54 spl5_4 <=> (((d_not @ ((d_not @ (iii @ sK3 @ sK4)) => (e_is @ nat @ sK3 @ sK4)))) = $true)),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition])).
% 1.49/0.54 thf(f1017,plain,(
% 1.49/0.54 (((d_not @ ((d_not @ (iii @ sK3 @ sK4)) => (e_is @ nat @ sK3 @ sK4)))) = $true) | ~spl5_4),
% 1.49/0.54 inference(avatar_component_clause,[],[f1015])).
% 1.49/0.54 thf(f1018,plain,(
% 1.49/0.54 spl5_4),
% 1.49/0.54 inference(avatar_split_clause,[],[f814,f1015])).
% 1.49/0.54 thf(f1020,definition,(
% 1.49/0.54 spl5_5 <=> ($false = ((n_some @ (diffprop @ sK3 @ sK4))))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition])).
% 1.49/0.54 thf(f1022,plain,(
% 1.49/0.54 ($false = ((n_some @ (diffprop @ sK3 @ sK4)))) | ~spl5_5),
% 1.49/0.54 inference(avatar_component_clause,[],[f1020])).
% 1.49/0.54 thf(f1023,plain,(
% 1.49/0.54 spl5_5),
% 1.49/0.54 inference(avatar_split_clause,[],[f813,f1020])).
% 1.49/0.54 thf(f1037,plain,(
% 1.49/0.54 ( ! [X0 : $i] : (($false = $true) | (((n_some @ (diffprop @ sK3 @ X0))) = $true) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($false = ((iii @ X0 @ sK3)))) ) | ~spl5_2),
% 1.49/0.54 inference(superposition,[],[f1007,f730])).
% 1.49/0.54 thf(f1038,plain,(
% 1.49/0.54 ( ! [X0 : $i] : (($false = ((iii @ X0 @ sK4))) | ($false = $true) | (((n_some @ (diffprop @ sK4 @ X0))) = $true) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) ) | ~spl5_3),
% 1.49/0.54 inference(superposition,[],[f1012,f730])).
% 1.49/0.54 thf(f1040,plain,(
% 1.49/0.54 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((n_some @ (diffprop @ sK4 @ X0))) = $true) | ($false = ((iii @ X0 @ sK4)))) ) | ~spl5_3),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1038])).
% 1.49/0.54 thf(f1042,plain,(
% 1.49/0.54 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((n_some @ (diffprop @ sK3 @ X0))) = $true) | ($false = ((iii @ X0 @ sK3)))) ) | ~spl5_2),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1037])).
% 1.49/0.54 thf(f1053,plain,(
% 1.49/0.54 ($true = ((d_not @ ($true => (e_is @ nat @ sK3 @ sK4))))) | ($false = ((d_not @ (iii @ sK3 @ sK4)))) | ~spl5_4),
% 1.49/0.54 inference(superposition,[],[f1017,f666])).
% 1.49/0.54 thf(f1054,plain,(
% 1.49/0.54 ((((d_not @ (iii @ sK3 @ sK4)) => (e_is @ nat @ sK3 @ sK4))) = $false) | ($true = ((d_not @ $true))) | ~spl5_4),
% 1.49/0.54 inference(superposition,[],[f1017,f666])).
% 1.49/0.54 thf(f1060,plain,(
% 1.49/0.54 (((d_not @ (e_is @ nat @ sK3 @ sK4))) = $true) | ($false = ((d_not @ (iii @ sK3 @ sK4)))) | ~spl5_4),
% 1.49/0.54 inference(boolean_simplification,[],[f1053])).
% 1.49/0.54 thf(f1063,plain,(
% 1.49/0.54 ($true = ((d_not @ $true))) | (((d_not @ (iii @ sK3 @ sK4))) = $true) | ~spl5_4),
% 1.49/0.54 inference(imp_proxy_clausification,[],[f1054])).
% 1.49/0.54 thf(f1073,definition,(
% 1.49/0.54 spl5_7 <=> ($false = ((iii @ sK3 @ sK4)))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition])).
% 1.49/0.54 thf(f1074,plain,(
% 1.49/0.54 ($false != ((iii @ sK3 @ sK4))) | spl5_7),
% 1.49/0.54 inference(avatar_component_clause,[],[f1073])).
% 1.49/0.54 thf(f1075,plain,(
% 1.49/0.54 ($false = ((iii @ sK3 @ sK4))) | ~spl5_7),
% 1.49/0.54 inference(avatar_component_clause,[],[f1073])).
% 1.49/0.54 thf(f1078,definition,(
% 1.49/0.54 spl5_8 <=> ($false = ((d_not @ (iii @ sK3 @ sK4))))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition])).
% 1.49/0.54 thf(f1080,plain,(
% 1.49/0.54 ($false = ((d_not @ (iii @ sK3 @ sK4)))) | ~spl5_8),
% 1.49/0.54 inference(avatar_component_clause,[],[f1078])).
% 1.49/0.54 thf(f1082,definition,(
% 1.49/0.54 spl5_9 <=> (((d_not @ (e_is @ nat @ sK3 @ sK4))) = $true)),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition])).
% 1.49/0.54 thf(f1084,plain,(
% 1.49/0.54 (((d_not @ (e_is @ nat @ sK3 @ sK4))) = $true) | ~spl5_9),
% 1.49/0.54 inference(avatar_component_clause,[],[f1082])).
% 1.49/0.54 thf(f1085,plain,(
% 1.49/0.54 spl5_8 | spl5_9 | ~spl5_4),
% 1.49/0.54 inference(avatar_split_clause,[],[f1060,f1015,f1082,f1078])).
% 1.49/0.54 thf(f1087,definition,(
% 1.49/0.54 spl5_10 <=> ($true = ((d_not @ $true)))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition])).
% 1.49/0.54 thf(f1088,plain,(
% 1.49/0.54 ($true != ((d_not @ $true))) | spl5_10),
% 1.49/0.54 inference(avatar_component_clause,[],[f1087])).
% 1.49/0.54 thf(f1089,plain,(
% 1.49/0.54 ($true = ((d_not @ $true))) | ~spl5_10),
% 1.49/0.54 inference(avatar_component_clause,[],[f1087])).
% 1.49/0.54 thf(f1091,definition,(
% 1.49/0.54 spl5_11 <=> ($false = ((e_is @ nat @ sK3 @ sK4)))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition])).
% 1.49/0.54 thf(f1092,plain,(
% 1.49/0.54 ($false != ((e_is @ nat @ sK3 @ sK4))) | spl5_11),
% 1.49/0.54 inference(avatar_component_clause,[],[f1091])).
% 1.49/0.54 thf(f1096,definition,(
% 1.49/0.54 spl5_12 <=> (((d_not @ (iii @ sK3 @ sK4))) = $true)),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition])).
% 1.49/0.54 thf(f1099,plain,(
% 1.49/0.54 spl5_10 | spl5_12 | ~spl5_4),
% 1.49/0.54 inference(avatar_split_clause,[],[f1063,f1015,f1096,f1087])).
% 1.49/0.54 thf(f1101,plain,(
% 1.49/0.54 ($false = ((d_not @ $false))) | (~spl5_7 | ~spl5_8)),
% 1.49/0.54 inference(forward_demodulation,[],[f1080,f1075])).
% 1.49/0.54 thf(f1103,definition,(
% 1.49/0.54 spl5_13 <=> ($false = ((d_not @ $false)))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_13])],[avatar_definition])).
% 1.49/0.54 thf(f1105,plain,(
% 1.49/0.54 ($false = ((d_not @ $false))) | ~spl5_13),
% 1.49/0.54 inference(avatar_component_clause,[],[f1103])).
% 1.49/0.54 thf(f1106,plain,(
% 1.49/0.54 spl5_13 | ~spl5_7 | ~spl5_8),
% 1.49/0.54 inference(avatar_split_clause,[],[f1101,f1078,f1073,f1103])).
% 1.49/0.54 thf(f1110,definition,(
% 1.49/0.54 ($false != ((d_not @ (iii @ sK3 @ sK4)))) | (((d_not @ (iii @ sK3 @ sK4))) != $true) | ($false = $true)),
% 1.49/0.54 introduced(theory,[theory_tautology_sat_conflict])).
% 1.49/0.54 thf(f1112,plain,(
% 1.49/0.54 ( ! [X0 : $i] : ((((iii @ sK3 @ X0)) = $true) | ($false = $true) | ($false = ((n_some @ (diffprop @ X0 @ sK3)))) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) ) | ~spl5_2),
% 1.49/0.54 inference(superposition,[],[f917,f1007])).
% 1.49/0.54 thf(f1119,plain,(
% 1.49/0.54 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((iii @ sK3 @ X0)) = $true) | ($false = ((n_some @ (diffprop @ X0 @ sK3))))) ) | ~spl5_2),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1112])).
% 1.49/0.54 thf(f1125,plain,(
% 1.49/0.54 ($false = ((d_not @ $true))) | ($true != $true) | spl5_10),
% 1.49/0.54 inference(superposition,[],[f1088,f666])).
% 1.49/0.54 thf(f1126,plain,(
% 1.49/0.54 ($false = ((d_not @ $true))) | spl5_10),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1125])).
% 1.49/0.54 thf(f1131,definition,(
% 1.49/0.54 spl5_14 <=> ($false = ((d_not @ $true)))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_14])],[avatar_definition])).
% 1.49/0.54 thf(f1134,plain,(
% 1.49/0.54 spl5_14 | spl5_10),
% 1.49/0.54 inference(avatar_split_clause,[],[f1126,f1087,f1131])).
% 1.49/0.54 thf(f1154,plain,(
% 1.49/0.54 (((n_some @ (diffprop @ sK3 @ sK4))) = $true) | ($false = $true) | (((iii @ sK4 @ sK3)) = $false) | (~spl5_2 | ~spl5_3)),
% 1.49/0.54 inference(superposition,[],[f1012,f1042])).
% 1.49/0.54 thf(f1157,plain,(
% 1.49/0.54 (((iii @ sK4 @ sK3)) = $false) | (((n_some @ (diffprop @ sK3 @ sK4))) = $true) | (~spl5_2 | ~spl5_3)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1154])).
% 1.49/0.54 thf(f1170,plain,(
% 1.49/0.54 ($false = $true) | (((iii @ sK4 @ sK3)) = $false) | (~spl5_2 | ~spl5_3 | ~spl5_5)),
% 1.49/0.54 inference(forward_demodulation,[],[f1157,f1022])).
% 1.49/0.54 thf(f1171,plain,(
% 1.49/0.54 (((iii @ sK4 @ sK3)) = $false) | (~spl5_2 | ~spl5_3 | ~spl5_5)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1170])).
% 1.49/0.54 thf(f1175,definition,(
% 1.49/0.54 spl5_17 <=> (((iii @ sK4 @ sK3)) = $false)),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_17])],[avatar_definition])).
% 1.49/0.54 thf(f1177,plain,(
% 1.49/0.54 (((iii @ sK4 @ sK3)) = $false) | ~spl5_17),
% 1.49/0.54 inference(avatar_component_clause,[],[f1175])).
% 1.49/0.54 thf(f1178,plain,(
% 1.49/0.54 spl5_17 | ~spl5_2 | ~spl5_3 | ~spl5_5),
% 1.49/0.54 inference(avatar_split_clause,[],[f1171,f1020,f1010,f1005,f1175])).
% 1.49/0.54 thf(f1184,plain,(
% 1.49/0.54 ($true = ((iii @ sK3 @ sK4))) | ($false = $true) | ($false = ((n_some @ (diffprop @ sK4 @ sK3)))) | (~spl5_2 | ~spl5_3)),
% 1.49/0.54 inference(superposition,[],[f1119,f1012])).
% 1.49/0.54 thf(f1192,plain,(
% 1.49/0.54 ($true = ((iii @ sK3 @ sK4))) | ($false = ((n_some @ (diffprop @ sK4 @ sK3)))) | (~spl5_2 | ~spl5_3)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1184])).
% 1.49/0.54 thf(f1194,definition,(
% 1.49/0.54 spl5_18 <=> ($true = ((iii @ sK3 @ sK4)))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_18])],[avatar_definition])).
% 1.49/0.54 thf(f1198,definition,(
% 1.49/0.54 spl5_19 <=> ($false = ((n_some @ (diffprop @ sK4 @ sK3))))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_19])],[avatar_definition])).
% 1.49/0.54 thf(f1200,plain,(
% 1.49/0.54 ($false = ((n_some @ (diffprop @ sK4 @ sK3)))) | ~spl5_19),
% 1.49/0.54 inference(avatar_component_clause,[],[f1198])).
% 1.49/0.54 thf(f1206,plain,(
% 1.49/0.54 spl5_19 | spl5_18 | ~spl5_2 | ~spl5_3),
% 1.49/0.54 inference(avatar_split_clause,[],[f1192,f1010,f1005,f1194,f1198])).
% 1.49/0.54 thf(f1243,plain,(
% 1.49/0.54 ($false = ((n_some @ (diffprop @ sK4 @ sK3)))) | ($true = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK4 @ sK3))))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ~spl5_17),
% 1.49/0.54 inference(superposition,[],[f876,f1177])).
% 1.49/0.54 thf(f1245,plain,(
% 1.49/0.54 ($false = $true) | ($false = ((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($false = ((n_some @ (diffprop @ sK4 @ sK3)))) | ($true = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK4 @ sK3))))) | (~spl5_3 | ~spl5_17)),
% 1.49/0.54 inference(forward_demodulation,[],[f1243,f1012])).
% 1.49/0.54 thf(f1246,plain,(
% 1.49/0.54 ($false = ((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($true = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK4 @ sK3))))) | ($false = ((n_some @ (diffprop @ sK4 @ sK3)))) | (~spl5_3 | ~spl5_17)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1245])).
% 1.49/0.54 thf(f1247,plain,(
% 1.49/0.54 ($true = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK4 @ sK3))))) | ($false = ((n_some @ (diffprop @ sK4 @ sK3)))) | ($false = $true) | (~spl5_2 | ~spl5_3 | ~spl5_17)),
% 1.49/0.54 inference(forward_demodulation,[],[f1246,f1007])).
% 1.49/0.54 thf(f1248,plain,(
% 1.49/0.54 ($false = ((n_some @ (diffprop @ sK4 @ sK3)))) | ($true = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK4 @ sK3))))) | (~spl5_2 | ~spl5_3 | ~spl5_17)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1247])).
% 1.49/0.54 thf(f1250,definition,(
% 1.49/0.54 spl5_22 <=> ($true = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK4 @ sK3)))))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_22])],[avatar_definition])).
% 1.49/0.54 thf(f1252,plain,(
% 1.49/0.54 ($true = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK4 @ sK3))))) | ~spl5_22),
% 1.49/0.54 inference(avatar_component_clause,[],[f1250])).
% 1.49/0.54 thf(f1253,plain,(
% 1.49/0.54 spl5_22 | spl5_19 | ~spl5_2 | ~spl5_3 | ~spl5_17),
% 1.49/0.54 inference(avatar_split_clause,[],[f1248,f1175,f1010,f1005,f1198,f1250])).
% 1.49/0.54 thf(f1330,plain,(
% 1.49/0.54 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($true = ((d_not @ (iii @ X0 @ sK4)))) | (((d_not @ (n_some @ (diffprop @ X0 @ sK4)))) = $true) | ($false = $true)) ) | ~spl5_3),
% 1.49/0.54 inference(superposition,[],[f831,f1012])).
% 1.49/0.54 thf(f1338,plain,(
% 1.49/0.54 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((d_not @ (n_some @ (diffprop @ X0 @ sK4)))) = $true) | ($true = ((d_not @ (iii @ X0 @ sK4))))) ) | ~spl5_3),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1330])).
% 1.49/0.54 thf(f1361,plain,(
% 1.49/0.54 ( ! [X0 : $i] : (($false = $true) | (((e_is @ nat @ X0 @ sK4)) = $false) | (((d_not @ (n_some @ (diffprop @ X0 @ sK4)))) = $true) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) ) | ~spl5_3),
% 1.49/0.54 inference(superposition,[],[f1012,f830])).
% 1.49/0.54 thf(f1364,plain,(
% 1.49/0.54 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((d_not @ (n_some @ (diffprop @ X0 @ sK4)))) = $true) | (((e_is @ nat @ X0 @ sK4)) = $false)) ) | ~spl5_3),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1361])).
% 1.49/0.54 thf(f1412,definition,(
% 1.49/0.54 spl5_28 <=> ($true = ((d_not @ $false)))),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_28])],[avatar_definition])).
% 1.49/0.54 thf(f1413,plain,(
% 1.49/0.54 ($true != ((d_not @ $false))) | spl5_28),
% 1.49/0.54 inference(avatar_component_clause,[],[f1412])).
% 1.49/0.54 thf(f1414,plain,(
% 1.49/0.54 ($true = ((d_not @ $false))) | ~spl5_28),
% 1.49/0.54 inference(avatar_component_clause,[],[f1412])).
% 1.49/0.54 thf(f1498,plain,(
% 1.49/0.54 ($false = ((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($false = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK4))))) | ($true = ((iii @ sK3 @ sK4))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ~spl5_5),
% 1.49/0.54 inference(superposition,[],[f946,f1022])).
% 1.49/0.54 thf(f1536,plain,(
% 1.49/0.54 ($true = ((iii @ sK3 @ sK4))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK4))))) | ($false = $true) | (~spl5_2 | ~spl5_5)),
% 1.49/0.54 inference(forward_demodulation,[],[f1498,f1007])).
% 1.49/0.54 thf(f1537,plain,(
% 1.49/0.54 ($true = ((iii @ sK3 @ sK4))) | ($false = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK4))))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (~spl5_2 | ~spl5_5)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1536])).
% 1.49/0.54 thf(f1540,plain,(
% 1.49/0.54 ($true = ((iii @ sK3 @ sK4))) | ($false = ((d_not @ ($true => (e_is @ nat @ sK3 @ sK4))))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (~spl5_2 | ~spl5_5 | ~spl5_28)),
% 1.49/0.54 inference(forward_demodulation,[],[f1537,f1414])).
% 1.49/0.54 thf(f1541,plain,(
% 1.49/0.54 (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((iii @ sK3 @ sK4))) | (((d_not @ (e_is @ nat @ sK3 @ sK4))) = $false) | (~spl5_2 | ~spl5_5 | ~spl5_28)),
% 1.49/0.54 inference(boolean_simplification,[],[f1540])).
% 1.49/0.54 thf(f1544,plain,(
% 1.49/0.54 (((d_not @ (e_is @ nat @ sK3 @ sK4))) = $false) | ($false = $true) | ($true = ((iii @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_28)),
% 1.49/0.54 inference(forward_demodulation,[],[f1541,f1012])).
% 1.49/0.54 thf(f1545,plain,(
% 1.49/0.54 (((d_not @ (e_is @ nat @ sK3 @ sK4))) = $false) | ($true = ((iii @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_28)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1544])).
% 1.49/0.54 thf(f1548,plain,(
% 1.49/0.54 ($true = ((iii @ sK3 @ sK4))) | ($false = $true) | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_9 | ~spl5_28)),
% 1.49/0.54 inference(forward_demodulation,[],[f1545,f1084])).
% 1.49/0.54 thf(f1549,plain,(
% 1.49/0.54 ($true = ((iii @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_9 | ~spl5_28)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1548])).
% 1.49/0.54 thf(f1551,definition,(
% 1.49/0.54 spl5_30 <=> (((d_not @ (e_is @ nat @ sK4 @ sK3))) = $false)),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_30])],[avatar_definition])).
% 1.49/0.54 thf(f1552,plain,(
% 1.49/0.54 (((d_not @ (e_is @ nat @ sK4 @ sK3))) != $false) | spl5_30),
% 1.49/0.54 inference(avatar_component_clause,[],[f1551])).
% 1.49/0.54 thf(f1553,plain,(
% 1.49/0.54 (((d_not @ (e_is @ nat @ sK4 @ sK3))) = $false) | ~spl5_30),
% 1.49/0.54 inference(avatar_component_clause,[],[f1551])).
% 1.49/0.54 thf(f1555,plain,(
% 1.49/0.54 ($false = $true) | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | ~spl5_9 | ~spl5_28)),
% 1.49/0.54 inference(forward_demodulation,[],[f1549,f1075])).
% 1.49/0.54 thf(f1556,plain,(
% 1.49/0.54 $false | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | ~spl5_9 | ~spl5_28)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1555])).
% 1.49/0.54 thf(f1557,plain,(
% 1.49/0.54 ~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | ~spl5_9 | ~spl5_28),
% 1.49/0.54 inference(avatar_contradiction_clause,[],[f1556])).
% 1.49/0.54 thf(f1604,plain,(
% 1.49/0.54 ($false = $true) | (((n_some @ (diffprop @ sK4 @ sK3))) = $true) | ($false = ((iii @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3)),
% 1.49/0.54 inference(superposition,[],[f1007,f1040])).
% 1.49/0.54 thf(f1610,plain,(
% 1.49/0.54 (((n_some @ (diffprop @ sK4 @ sK3))) = $true) | ($false = ((iii @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1604])).
% 1.49/0.54 thf(f1612,plain,(
% 1.49/0.54 (((n_some @ (diffprop @ sK4 @ sK3))) = $true) | (~spl5_2 | ~spl5_3 | spl5_7)),
% 1.49/0.54 inference(forward_subsumption_resolution,[],[f1610,f1074])).
% 1.49/0.54 thf(f1616,plain,(
% 1.49/0.54 ($false = $true) | (~spl5_2 | ~spl5_3 | spl5_7 | ~spl5_19)),
% 1.49/0.54 inference(forward_demodulation,[],[f1612,f1200])).
% 1.49/0.54 thf(f1617,plain,(
% 1.49/0.54 $false | (~spl5_2 | ~spl5_3 | spl5_7 | ~spl5_19)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1616])).
% 1.49/0.54 thf(f1618,plain,(
% 1.49/0.54 ~spl5_2 | ~spl5_3 | spl5_7 | ~spl5_19),
% 1.49/0.54 inference(avatar_contradiction_clause,[],[f1617])).
% 1.49/0.54 thf(f1619,plain,(
% 1.49/0.54 (((d_not @ ($true => (e_is @ nat @ sK4 @ sK3)))) = $true) | (~spl5_22 | ~spl5_28)),
% 1.49/0.54 inference(forward_demodulation,[],[f1252,f1414])).
% 1.49/0.54 thf(f1620,plain,(
% 1.49/0.54 (((d_not @ (e_is @ nat @ sK4 @ sK3))) = $true) | (~spl5_22 | ~spl5_28)),
% 1.49/0.54 inference(boolean_simplification,[],[f1619])).
% 1.49/0.54 thf(f1622,definition,(
% 1.49/0.54 spl5_33 <=> (((n_some @ (diffprop @ sK4 @ sK3))) = $true)),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_33])],[avatar_definition])).
% 1.49/0.54 thf(f1624,plain,(
% 1.49/0.54 (((n_some @ (diffprop @ sK4 @ sK3))) = $true) | ~spl5_33),
% 1.49/0.54 inference(avatar_component_clause,[],[f1622])).
% 1.49/0.54 thf(f1625,plain,(
% 1.49/0.54 spl5_33 | ~spl5_2 | ~spl5_3 | spl5_7),
% 1.49/0.54 inference(avatar_split_clause,[],[f1612,f1073,f1010,f1005,f1622])).
% 1.49/0.54 thf(f1626,plain,(
% 1.49/0.54 ($false = $true) | (~spl5_22 | ~spl5_28 | ~spl5_30)),
% 1.49/0.54 inference(forward_demodulation,[],[f1620,f1553])).
% 1.49/0.54 thf(f1627,plain,(
% 1.49/0.54 $false | (~spl5_22 | ~spl5_28 | ~spl5_30)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1626])).
% 1.49/0.54 thf(f1628,plain,(
% 1.49/0.54 ~spl5_22 | ~spl5_28 | ~spl5_30),
% 1.49/0.54 inference(avatar_contradiction_clause,[],[f1627])).
% 1.49/0.54 thf(f1646,plain,(
% 1.49/0.54 ($false = ((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((d_not @ ((d_not @ $true) => (e_is @ nat @ sK4 @ sK3))))) | (((iii @ sK4 @ sK3)) = $true) | ~spl5_33),
% 1.49/0.54 inference(superposition,[],[f946,f1624])).
% 1.49/0.54 thf(f1648,plain,(
% 1.49/0.54 ($false = $true) | (((iii @ sK4 @ sK3)) = $true) | ($false = ((d_not @ ((d_not @ $true) => (e_is @ nat @ sK4 @ sK3))))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (~spl5_2 | ~spl5_33)),
% 1.49/0.54 inference(forward_demodulation,[],[f1646,f1007])).
% 1.49/0.54 thf(f1649,plain,(
% 1.49/0.54 (((iii @ sK4 @ sK3)) = $true) | ($false = ((d_not @ ((d_not @ $true) => (e_is @ nat @ sK4 @ sK3))))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (~spl5_2 | ~spl5_33)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1648])).
% 1.49/0.54 thf(f1650,plain,(
% 1.49/0.54 ($false = ((d_not @ ((d_not @ $true) => (e_is @ nat @ sK4 @ sK3))))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = $true) | (~spl5_2 | ~spl5_17 | ~spl5_33)),
% 1.49/0.54 inference(forward_demodulation,[],[f1649,f1177])).
% 1.49/0.54 thf(f1651,plain,(
% 1.49/0.54 ($false = ((d_not @ ((d_not @ $true) => (e_is @ nat @ sK4 @ sK3))))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (~spl5_2 | ~spl5_17 | ~spl5_33)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1650])).
% 1.49/0.54 thf(f1652,plain,(
% 1.49/0.54 ($false = ((d_not @ ($true => (e_is @ nat @ sK4 @ sK3))))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (~spl5_2 | ~spl5_10 | ~spl5_17 | ~spl5_33)),
% 1.49/0.54 inference(forward_demodulation,[],[f1651,f1089])).
% 1.49/0.54 thf(f1653,plain,(
% 1.49/0.54 (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_not @ (e_is @ nat @ sK4 @ sK3))) = $false) | (~spl5_2 | ~spl5_10 | ~spl5_17 | ~spl5_33)),
% 1.49/0.54 inference(boolean_simplification,[],[f1652])).
% 1.49/0.54 thf(f1654,plain,(
% 1.49/0.54 (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (~spl5_2 | ~spl5_10 | ~spl5_17 | spl5_30 | ~spl5_33)),
% 1.49/0.54 inference(forward_subsumption_resolution,[],[f1653,f1552])).
% 1.49/0.54 thf(f1656,definition,(
% 1.49/0.54 spl5_35 <=> (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)),
% 1.49/0.54 introduced(definition,[new_symbols(definition,[spl5_35])],[avatar_definition])).
% 1.49/0.54 thf(f1659,plain,(
% 1.49/0.54 spl5_35 | ~spl5_2 | ~spl5_10 | ~spl5_17 | spl5_30 | ~spl5_33),
% 1.49/0.54 inference(avatar_split_clause,[],[f1654,f1622,f1551,f1175,f1087,f1005,f1656])).
% 1.49/0.54 thf(f1660,definition,(
% 1.49/0.54 (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) != $false) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) != $true) | ($false = $true)),
% 1.49/0.54 introduced(theory,[theory_tautology_sat_conflict])).
% 1.49/0.54 thf(f1663,definition,(
% 1.49/0.54 ($true != ((iii @ sK3 @ sK4))) | ($false != ((d_not @ $true))) | ($false = ((d_not @ (iii @ sK3 @ sK4))))),
% 1.49/0.54 introduced(theory,[theory_tautology_sat_conflict])).
% 1.49/0.54 thf(f1754,plain,(
% 1.49/0.54 (((d_not @ (iii @ sK3 @ sK4))) = $true) | (((d_not @ (n_some @ (diffprop @ sK3 @ sK4)))) = $true) | ($false = $true) | (~spl5_2 | ~spl5_3)),
% 1.49/0.54 inference(superposition,[],[f1007,f1338])).
% 1.49/0.54 thf(f1758,plain,(
% 1.49/0.54 (((d_not @ (iii @ sK3 @ sK4))) = $true) | (((d_not @ (n_some @ (diffprop @ sK3 @ sK4)))) = $true) | (~spl5_2 | ~spl5_3)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1754])).
% 1.49/0.54 thf(f1819,plain,(
% 1.49/0.54 ($false = $true) | (((d_not @ (n_some @ (diffprop @ sK3 @ sK4)))) = $true) | ($false = ((e_is @ nat @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3)),
% 1.49/0.54 inference(superposition,[],[f1364,f1007])).
% 1.49/0.54 thf(f1827,plain,(
% 1.49/0.54 ($false = ((e_is @ nat @ sK3 @ sK4))) | (((d_not @ (n_some @ (diffprop @ sK3 @ sK4)))) = $true) | (~spl5_2 | ~spl5_3)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1819])).
% 1.49/0.54 thf(f1832,plain,(
% 1.49/0.54 (((d_not @ (n_some @ (diffprop @ sK3 @ sK4)))) = $true) | (~spl5_2 | ~spl5_3 | spl5_11)),
% 1.49/0.54 inference(forward_subsumption_resolution,[],[f1827,f1092])).
% 1.49/0.54 thf(f1834,plain,(
% 1.49/0.54 ($true = ((d_not @ $false))) | (~spl5_2 | ~spl5_3 | ~spl5_5 | spl5_11)),
% 1.49/0.54 inference(forward_demodulation,[],[f1832,f1022])).
% 1.49/0.54 thf(f1837,plain,(
% 1.49/0.54 $false | (~spl5_2 | ~spl5_3 | ~spl5_5 | spl5_11 | spl5_28)),
% 1.49/0.54 inference(forward_subsumption_resolution,[],[f1834,f1413])).
% 1.49/0.54 thf(f1838,plain,(
% 1.49/0.54 ~spl5_2 | ~spl5_3 | ~spl5_5 | spl5_11 | spl5_28),
% 1.49/0.54 inference(avatar_contradiction_clause,[],[f1837])).
% 1.49/0.54 thf(f1840,definition,(
% 1.49/0.54 ($true != ((iii @ sK3 @ sK4))) | ($true != ((d_not @ $true))) | (((d_not @ (iii @ sK3 @ sK4))) = $true)),
% 1.49/0.54 introduced(theory,[theory_tautology_sat_conflict])).
% 1.49/0.54 thf(f1841,definition,(
% 1.49/0.54 ($false != ((e_is @ nat @ sK3 @ sK4))) | (((d_not @ (e_is @ nat @ sK3 @ sK4))) != $true) | ($true = ((d_not @ $false)))),
% 1.49/0.54 introduced(theory,[theory_tautology_sat_conflict])).
% 1.49/0.54 thf(f1854,plain,(
% 1.49/0.54 ($true = ((d_not @ $false))) | (((d_not @ (n_some @ (diffprop @ sK3 @ sK4)))) = $true) | (~spl5_2 | ~spl5_3 | ~spl5_7)),
% 1.49/0.54 inference(forward_demodulation,[],[f1758,f1075])).
% 1.49/0.54 thf(f1861,plain,(
% 1.49/0.54 ($false = $true) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK4))))) | (~spl5_2 | ~spl5_5 | ~spl5_7)),
% 1.49/0.54 inference(forward_demodulation,[],[f1537,f1075])).
% 1.49/0.54 thf(f1862,plain,(
% 1.49/0.54 (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK4))))) | (~spl5_2 | ~spl5_5 | ~spl5_7)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1861])).
% 1.49/0.54 thf(f1866,plain,(
% 1.49/0.54 (((d_not @ (n_some @ (diffprop @ sK3 @ sK4)))) = $true) | (~spl5_2 | ~spl5_3 | ~spl5_7 | spl5_28)),
% 1.49/0.54 inference(forward_subsumption_resolution,[],[f1854,f1413])).
% 1.49/0.54 thf(f1874,plain,(
% 1.49/0.54 ($false = $true) | ($false = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK4))))) | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7)),
% 1.49/0.54 inference(forward_demodulation,[],[f1862,f1012])).
% 1.49/0.54 thf(f1875,plain,(
% 1.49/0.54 ($false = ((d_not @ ((d_not @ $false) => (e_is @ nat @ sK3 @ sK4))))) | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7)),
% 1.49/0.54 inference(trivial_inequality_removal,[],[f1874])).
% 1.49/0.54 thf(f1882,plain,(
% 1.49/0.54 ($true = ((d_not @ $false))) | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | spl5_28)),
% 1.49/0.54 inference(forward_demodulation,[],[f1866,f1022])).
% 1.49/0.54 thf(f1885,plain,(
% 1.49/0.54 (((d_not @ ($false => (e_is @ nat @ sK3 @ sK4)))) = $false) | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | ~spl5_13)),
% 1.49/0.54 inference(forward_demodulation,[],[f1875,f1105])).
% 1.49/0.54 thf(f1886,plain,(
% 1.49/0.54 ($false = ((d_not @ $true))) | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | ~spl5_13)),
% 1.49/0.54 inference(boolean_simplification,[],[f1885])).
% 1.49/0.54 thf(f1889,plain,(
% 1.49/0.54 $false | (~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | spl5_28)),
% 1.49/0.54 inference(forward_subsumption_resolution,[],[f1882,f1413])).
% 1.49/0.54 thf(f1890,plain,(
% 1.49/0.54 ~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | spl5_28),
% 1.49/0.54 inference(avatar_contradiction_clause,[],[f1889])).
% 1.49/0.54 thf(f1895,plain,(
% 1.49/0.54 spl5_14 | ~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | ~spl5_13),
% 1.49/0.54 inference(avatar_split_clause,[],[f1886,f1103,f1073,f1020,f1010,f1005,f1131])).
% 1.49/0.54 thf(f1897,definition,(
% 1.49/0.54 (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) != $true) | ($true != ((d_not @ $true))) | ($false != ((d_not @ $true))) | (((is_of @ sK4 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)),
% 1.49/0.54 introduced(theory,[theory_tautology_sat_conflict])).
% 1.49/0.54 cnf(s1, plain, ~spl5_1, inference(sat_conversion,[],[f1003])).
% 1.49/0.54 cnf(s2, plain, spl5_2, inference(sat_conversion,[],[f1008])).
% 1.49/0.54 cnf(s3, plain, spl5_3, inference(sat_conversion,[],[f1013])).
% 1.49/0.54 cnf(s4, plain, spl5_4, inference(sat_conversion,[],[f1018])).
% 1.49/0.54 cnf(s5, plain, spl5_5, inference(sat_conversion,[],[f1023])).
% 1.49/0.54 cnf(s7, plain, ~spl5_4 | spl5_8 | spl5_9, inference(sat_conversion,[],[f1085])).
% 1.49/0.54 cnf(s9, plain, ~spl5_4 | spl5_10 | spl5_12, inference(sat_conversion,[],[f1099])).
% 1.49/0.54 cnf(s11, plain, ~spl5_7 | ~spl5_8 | spl5_13, inference(sat_conversion,[],[f1106])).
% 1.49/0.54 cnf(s13, plain, spl5_1 | ~spl5_8 | ~spl5_12, inference(sat_conversion,[],[f1110])).
% 1.49/0.54 cnf(s14, plain, spl5_10 | spl5_14, inference(sat_conversion,[],[f1134])).
% 1.49/0.54 cnf(s17, plain, ~spl5_2 | ~spl5_3 | ~spl5_5 | spl5_17, inference(sat_conversion,[],[f1178])).
% 1.49/0.54 cnf(s20, plain, ~spl5_2 | ~spl5_3 | spl5_18 | spl5_19, inference(sat_conversion,[],[f1206])).
% 1.49/0.54 cnf(s30, plain, ~spl5_2 | ~spl5_3 | ~spl5_17 | spl5_19 | spl5_22, inference(sat_conversion,[],[f1253])).
% 1.49/0.54 cnf(s48, plain, ~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | ~spl5_9 | ~spl5_28, inference(sat_conversion,[],[f1557])).
% 1.49/0.54 cnf(s53, plain, ~spl5_2 | ~spl5_3 | spl5_7 | ~spl5_19, inference(sat_conversion,[],[f1618])).
% 1.49/0.54 cnf(s54, plain, ~spl5_2 | ~spl5_3 | spl5_7 | spl5_33, inference(sat_conversion,[],[f1625])).
% 1.49/0.54 cnf(s56, plain, ~spl5_22 | ~spl5_28 | ~spl5_30, inference(sat_conversion,[],[f1628])).
% 1.49/0.54 cnf(s58, plain, ~spl5_2 | ~spl5_10 | ~spl5_17 | spl5_30 | ~spl5_33 | spl5_35, inference(sat_conversion,[],[f1659])).
% 1.49/0.54 cnf(s59, plain, spl5_1 | ~spl5_3 | ~spl5_35, inference(sat_conversion,[],[f1660])).
% 1.49/0.54 cnf(s62, plain, spl5_8 | ~spl5_14 | ~spl5_18, inference(sat_conversion,[],[f1663])).
% 1.49/0.54 cnf(s95, plain, ~spl5_2 | ~spl5_3 | ~spl5_5 | spl5_11 | spl5_28, inference(sat_conversion,[],[f1838])).
% 1.49/0.54 cnf(s97, plain, ~spl5_10 | spl5_12 | ~spl5_18, inference(sat_conversion,[],[f1840])).
% 1.49/0.54 cnf(s98, plain, ~spl5_9 | ~spl5_11 | spl5_28, inference(sat_conversion,[],[f1841])).
% 1.49/0.54 cnf(s105, plain, ~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | spl5_28, inference(sat_conversion,[],[f1890])).
% 1.49/0.54 cnf(s108, plain, ~spl5_2 | ~spl5_3 | ~spl5_5 | ~spl5_7 | ~spl5_13 | spl5_14, inference(sat_conversion,[],[f1895])).
% 1.49/0.54 cnf(s110, plain, ~spl5_3 | ~spl5_10 | ~spl5_14 | spl5_35, inference(sat_conversion,[],[f1897])).
% 1.49/0.54 cnf(s111, plain, spl5_17, inference(rat,[],[s17,s3,s5,s2])).
% 1.49/0.54 cnf(s112, plain, ~spl5_35, inference(rat,[],[s59,s3,s1])).
% 1.49/0.54 cnf(s113, plain, ~spl5_7 | ~spl5_28, inference(rat,[],[s110,s108,s9,s11,s13,s7,s48,s1,s4,s2,s5,s112,s3])).
% 1.49/0.54 cnf(s114, plain, ~spl5_7, inference(rat,[],[s113,s105,s5,s3,s2])).
% 1.49/0.54 cnf(s116, plain, spl5_33, inference(rat,[],[s54,s2,s3,s114])).
% 1.49/0.54 cnf(s117, plain, ~spl5_19, inference(rat,[],[s53,s2,s3,s114])).
% 1.49/0.54 cnf(s119, plain, spl5_22, inference(rat,[],[s30,s111,s2,s3,s117])).
% 1.49/0.54 cnf(s120, plain, spl5_18, inference(rat,[],[s20,s2,s3,s117])).
% 1.49/0.54 cnf(s121, plain, spl5_8, inference(rat,[],[s98,s95,s56,s58,s14,s7,s62,s5,s3,s2,s119,s111,s116,s112,s4,s120])).
% 1.49/0.54 cnf(s122, plain, ~spl5_12, inference(rat,[],[s13,s1,s121])).
% 1.49/0.54 cnf(s123, plain, ~spl5_10, inference(rat,[],[s97,s120,s122])).
% 1.49/0.54 cnf(s124, plain, $false, inference(rat,[],[s9,s4,s122,s123])).
% 1.49/0.54 thf(f1898,plain,(
% 1.49/0.54 $false),
% 1.49/0.54 inference(avatar_sat_refutation,[],[s124])).
% 1.49/0.54 % SZS output end Proof for theBenchmark
% 1.49/0.54 % (2443628)------------------------------
% 1.49/0.54 % (2443628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.54 % (2443628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.54 % (2443628)CaDiCaL version: 2.1.3
% 1.49/0.54 % (2443628)Termination reason: Refutation
% 1.49/0.54 % (2443628)Time elapsed: 0.040 s
% 1.49/0.54 % (2443628)Peak memory usage: 14 MB
% 1.49/0.54 % (2443628)Instructions burned: 155 (million)
% 1.49/0.54 % (2443559)Success in time 0.272 s
% 1.49/0.54 % Vampire exiting
%------------------------------------------------------------------------------