%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM653^4 : TPTP v9.3.1. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:18:24 AM UTC 2026
% Result : Theorem 1.28s 0.55s
% Output : Refutation 1.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM653^4 : TPTP v9.3.1. Released v7.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 % Computer : n020.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Tue Sep 29 12:33:05 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.22 Running higher-order theorem proving
% 0.23/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.61/0.39 % (985818)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.61/0.39 % (985842)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2082034321:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.61/0.39 % (985842)Instruction limit reached!
% 0.61/0.39 % (985842)------------------------------
% 0.61/0.39 % (985842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.39 % (985842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.39 % (985842)CaDiCaL version: 2.1.3
% 0.61/0.39 % (985842)Termination reason: Instruction limit
% 0.61/0.39 % (985842)Termination phase: shuffling
% 0.61/0.39 % (985842)Time elapsed: 0.002 s
% 0.61/0.39 % (985842)Peak memory usage: 10 MB
% 0.61/0.39 % (985842)Instructions burned: 8 (million)
% 0.61/0.39 % (985846)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.61/0.39 % (985846)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.61/0.39 % (985840)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4107369514:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.61/0.39 % (985841)lrs+10_16_si=on:nwc=1.5:random_seed=3837150556:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.61/0.39 % (985843)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=2331101292: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.61/0.39 % (985844)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1826926977:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.61/0.39 % (985845)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2101941351:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.61/0.39 % (985846)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=2871867885:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.61/0.39 % (985852)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3106352480:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.61/0.39 % (985852)Instruction limit reached!
% 0.61/0.39 % (985852)------------------------------
% 0.61/0.39 % (985852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.39 % (985852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.39 % (985852)CaDiCaL version: 2.1.3
% 0.61/0.39 % (985852)Termination reason: Instruction limit
% 0.61/0.39 % (985852)Termination phase: shuffling
% 0.61/0.39 % (985852)Time elapsed: 0.001 s
% 0.61/0.39 % (985852)Peak memory usage: 10 MB
% 0.61/0.39 % (985852)Instructions burned: 6 (million)
% 0.61/0.39 % (985841)Instruction limit reached!
% 0.61/0.39 % (985841)------------------------------
% 0.61/0.39 % (985841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.39 % (985841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.39 % (985841)CaDiCaL version: 2.1.3
% 0.61/0.39 % (985841)Termination reason: Instruction limit
% 0.61/0.39 % (985841)Termination phase: shuffling
% 0.61/0.39 % (985841)Time elapsed: 0.008 s
% 0.61/0.39 % (985841)Peak memory usage: 10 MB
% 0.61/0.39 % (985841)Instructions burned: 18 (million)
% 0.61/0.39 % (985844)Instruction limit reached!
% 0.61/0.39 % (985844)------------------------------
% 0.61/0.39 % (985844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.39 % (985844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.39 % (985844)CaDiCaL version: 2.1.3
% 0.61/0.39 % (985844)Termination reason: Instruction limit
% 0.61/0.39 % (985844)Termination phase: Property scanning
% 0.61/0.39 % (985844)Time elapsed: 0.011 s
% 0.61/0.39 % (985844)Peak memory usage: 10 MB
% 0.61/0.39 % (985844)Instructions burned: 25 (million)
% 0.61/0.39 % (985860)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=881564144:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.61/0.39 % (985860)Instruction limit reached!
% 0.61/0.42 % (985860)------------------------------
% 0.61/0.42 % (985860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.42 % (985860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.42 % (985860)CaDiCaL version: 2.1.3
% 0.61/0.42 % (985860)Termination reason: Instruction limit
% 0.61/0.42 % (985860)Termination phase: shuffling
% 0.61/0.42 % (985860)Time elapsed: 0.002 s
% 0.61/0.42 % (985860)Peak memory usage: 10 MB
% 0.61/0.42 % (985860)Instructions burned: 8 (million)
% 0.61/0.42 % (985862)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.61/0.42 % (985868)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.61/0.42 % (985868)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.61/0.42 % (985868)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=595460212: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.61/0.42 % (985862)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2832912850:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.61/0.42 % (985864)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3876810489:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.61/0.42 % (985845)Instruction limit reached!
% 0.61/0.42 % (985845)------------------------------
% 0.61/0.42 % (985845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.42 % (985845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.42 % (985845)CaDiCaL version: 2.1.3
% 0.61/0.42 % (985845)Termination reason: Instruction limit
% 0.61/0.42 % (985845)Termination phase: Function definition elimination
% 0.61/0.42 % (985845)Time elapsed: 0.033 s
% 0.61/0.42 % (985845)Peak memory usage: 11 MB
% 0.61/0.42 % (985845)Instructions burned: 76 (million)
% 0.61/0.42 % (985862)Instruction limit reached!
% 0.61/0.42 % (985862)------------------------------
% 0.61/0.42 % (985862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.42 % (985862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.42 % (985862)CaDiCaL version: 2.1.3
% 0.61/0.42 % (985862)Termination reason: Instruction limit
% 0.61/0.42 % (985862)Termination phase: shuffling
% 0.61/0.42 % (985862)Time elapsed: 0.004 s
% 0.61/0.42 % (985862)Peak memory usage: 10 MB
% 0.61/0.42 % (985862)Instructions burned: 8 (million)
% 0.61/0.42 % (985868)Instruction limit reached!
% 0.61/0.42 % (985868)------------------------------
% 0.61/0.42 % (985868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.42 % (985868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.42 % (985868)CaDiCaL version: 2.1.3
% 0.61/0.42 % (985868)Termination reason: Instruction limit
% 0.61/0.42 % (985868)Termination phase: Property scanning
% 0.61/0.42 % (985868)Time elapsed: 0.007 s
% 0.61/0.42 % (985868)Peak memory usage: 10 MB
% 0.61/0.42 % (985868)Instructions burned: 30 (million)
% 0.61/0.42 % (985864)Instruction limit reached!
% 0.61/0.42 % (985864)------------------------------
% 0.61/0.42 % (985864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.42 % (985864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.42 % (985864)CaDiCaL version: 2.1.3
% 0.61/0.42 % (985864)Termination reason: Instruction limit
% 0.61/0.42 % (985864)Termination phase: shuffling
% 0.61/0.42 % (985864)Time elapsed: 0.006 s
% 0.61/0.42 % (985864)Peak memory usage: 10 MB
% 0.61/0.42 % (985864)Instructions burned: 12 (million)
% 0.61/0.42 % (985840)Instruction limit reached!
% 0.61/0.42 % (985840)------------------------------
% 0.61/0.42 % (985840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.42 % (985840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.42 % (985840)CaDiCaL version: 2.1.3
% 0.61/0.42 % (985840)Termination reason: Instruction limit
% 0.61/0.42 % (985840)Termination phase: Function definition elimination
% 0.61/0.42 % (985840)Time elapsed: 0.038 s
% 0.61/0.45 % (985840)Peak memory usage: 11 MB
% 0.61/0.45 % (985840)Instructions burned: 87 (million)
% 0.61/0.45 % (985878)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.61/0.45 % (985878)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=2354283339:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.61/0.45 % (985878)Instruction limit reached!
% 0.61/0.45 % (985878)------------------------------
% 0.61/0.45 % (985878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.45 % (985878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.45 % (985878)CaDiCaL version: 2.1.3
% 0.61/0.45 % (985878)Termination reason: Instruction limit
% 0.61/0.45 % (985878)Termination phase: shuffling
% 0.61/0.45 % (985878)Time elapsed: 0.001 s
% 0.61/0.45 % (985878)Peak memory usage: 10 MB
% 0.61/0.45 % (985878)Instructions burned: 3 (million)
% 0.61/0.45 % (985875)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=431003289:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.61/0.45 % (985876)lrs+10_1_si=on:cs=on:random_seed=2442403591:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.61/0.45 % (985881)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3723159709:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.61/0.45 % (985876)Instruction limit reached!
% 0.61/0.45 % (985876)------------------------------
% 0.61/0.45 % (985876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.45 % (985876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.45 % (985876)CaDiCaL version: 2.1.3
% 0.61/0.45 % (985876)Termination reason: Instruction limit
% 0.61/0.45 % (985876)Termination phase: shuffling
% 0.61/0.45 % (985876)Time elapsed: 0.004 s
% 0.61/0.45 % (985876)Peak memory usage: 10 MB
% 0.61/0.45 % (985876)Instructions burned: 8 (million)
% 0.61/0.45 % (985882)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=4114290543:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.61/0.45 % (985846)Instruction limit reached!
% 0.61/0.45 % (985846)------------------------------
% 0.61/0.45 % (985846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.45 % (985846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.45 % (985846)CaDiCaL version: 2.1.3
% 0.61/0.45 % (985846)Termination reason: Instruction limit
% 0.61/0.45 % (985846)Termination phase: Function definition elimination
% 0.61/0.45 % (985846)Time elapsed: 0.063 s
% 0.61/0.45 % (985846)Peak memory usage: 11 MB
% 0.61/0.45 % (985846)Instructions burned: 157 (million)
% 0.61/0.45 % (985886)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=994438599:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.61/0.45 % (985881)Instruction limit reached!
% 0.61/0.45 % (985881)------------------------------
% 0.61/0.45 % (985881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.45 % (985881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.45 % (985881)CaDiCaL version: 2.1.3
% 0.61/0.45 % (985881)Termination reason: Instruction limit
% 0.61/0.45 % (985881)Termination phase: Saturation
% 0.61/0.45 % (985881)Time elapsed: 0.018 s
% 0.61/0.45 % (985881)Peak memory usage: 12 MB
% 0.61/0.45 % (985881)Instructions burned: 39 (million)
% 0.61/0.45 % (985895)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3584050017:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.61/0.45 % (985886)Instruction limit reached!
% 0.61/0.45 % (985886)------------------------------
% 0.61/0.45 % (985886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.61/0.45 % (985886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.61/0.45 % (985886)CaDiCaL version: 2.1.3
% 0.61/0.45 % (985886)Termination reason: Instruction limit
% 0.61/0.45 % (985886)Termination phase: Property scanning
% 0.61/0.45 % (985886)Time elapsed: 0.011 s
% 0.61/0.45 % (985886)Peak memory usage: 10 MB
% 0.61/0.45 % (985886)Instructions burned: 25 (million)
% 1.28/0.50 % (985882)Refutation not found, incomplete strategy
% 1.28/0.50 % (985882)------------------------------
% 1.28/0.50 % (985882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.50 % (985882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.50 % (985882)CaDiCaL version: 2.1.3
% 1.28/0.50 % (985882)Termination reason: Refutation not found, incomplete strategy
% 1.28/0.50 % (985882)Time elapsed: 0.020 s
% 1.28/0.50 % (985882)Peak memory usage: 13 MB
% 1.28/0.50 % (985882)Instructions burned: 43 (million)
% 1.28/0.50 % (985882)------------------------------
% 1.28/0.50 % (985882)------------------------------
% 1.28/0.50 % (985900)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=457541375:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.28/0.50 % (985895)Instruction limit reached!
% 1.28/0.50 % (985895)------------------------------
% 1.28/0.50 % (985895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.50 % (985895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.50 % (985895)CaDiCaL version: 2.1.3
% 1.28/0.50 % (985895)Termination reason: Instruction limit
% 1.28/0.50 % (985895)Termination phase: shuffling
% 1.28/0.50 % (985895)Time elapsed: 0.007 s
% 1.28/0.50 % (985895)Peak memory usage: 10 MB
% 1.28/0.50 % (985895)Instructions burned: 16 (million)
% 1.28/0.50 % (985875)Instruction limit reached!
% 1.28/0.50 % (985875)------------------------------
% 1.28/0.50 % (985875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.50 % (985875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.50 % (985875)CaDiCaL version: 2.1.3
% 1.28/0.50 % (985875)Termination reason: Instruction limit
% 1.28/0.50 % (985875)Termination phase: Function definition elimination
% 1.28/0.50 % (985875)Time elapsed: 0.036 s
% 1.28/0.50 % (985875)Peak memory usage: 11 MB
% 1.28/0.50 % (985875)Instructions burned: 87 (million)
% 1.28/0.50 % (985909)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3936511367:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.28/0.50 % (985911)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=4118675406: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.28/0.50 % (985911)Instruction limit reached!
% 1.28/0.50 % (985911)------------------------------
% 1.28/0.50 % (985911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.50 % (985911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.50 % (985911)CaDiCaL version: 2.1.3
% 1.28/0.50 % (985911)Termination reason: Instruction limit
% 1.28/0.50 % (985911)Termination phase: shuffling
% 1.28/0.50 % (985911)Time elapsed: 0.002 s
% 1.28/0.50 % (985911)Peak memory usage: 10 MB
% 1.28/0.50 % (985911)Instructions burned: 4 (million)
% 1.28/0.50 % (985913)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1136282785:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.28/0.50 % (985916)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1018081175:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.28/0.50 % (985909)Instruction limit reached!
% 1.28/0.50 % (985909)------------------------------
% 1.28/0.50 % (985909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.50 % (985909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.50 % (985909)CaDiCaL version: 2.1.3
% 1.28/0.50 % (985909)Termination reason: Instruction limit
% 1.28/0.50 % (985909)Termination phase: shuffling
% 1.28/0.50 % (985909)Time elapsed: 0.007 s
% 1.28/0.50 % (985909)Peak memory usage: 10 MB
% 1.28/0.50 % (985909)Instructions burned: 16 (million)
% 1.28/0.50 % (985915)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=4100637292:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.28/0.50 % (985913)Instruction limit reached!
% 1.28/0.50 % (985913)------------------------------
% 1.28/0.50 % (985913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.50 % (985913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.50 % (985913)CaDiCaL version: 2.1.3
% 1.28/0.50 % (985913)Termination reason: Instruction limit
% 1.28/0.50 % (985913)Termination phase: Property scanning
% 1.28/0.55 % (985913)Time elapsed: 0.012 s
% 1.28/0.55 % (985913)Peak memory usage: 10 MB
% 1.28/0.55 % (985913)Instructions burned: 26 (million)
% 1.28/0.55 % (985920)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.28/0.55 % (985920)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.28/0.55 % (985915)Instruction limit reached!
% 1.28/0.55 % (985915)------------------------------
% 1.28/0.55 % (985915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985915)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985915)Termination reason: Instruction limit
% 1.28/0.55 % (985915)Termination phase: Property scanning
% 1.28/0.55 % (985915)Time elapsed: 0.010 s
% 1.28/0.55 % (985915)Peak memory usage: 10 MB
% 1.28/0.55 % (985915)Instructions burned: 24 (million)
% 1.28/0.55 % (985916)Instruction limit reached!
% 1.28/0.55 % (985916)------------------------------
% 1.28/0.55 % (985916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985916)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985916)Termination reason: Instruction limit
% 1.28/0.55 % (985916)Termination phase: Saturation
% 1.28/0.55 % (985916)Time elapsed: 0.014 s
% 1.28/0.55 % (985916)Peak memory usage: 12 MB
% 1.28/0.55 % (985916)Instructions burned: 60 (million)
% 1.28/0.55 % (985922)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.28/0.55 % (985920)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=1578293576:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.28/0.55 % (985922)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=2078237016:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.28/0.55 % (985932)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3077497290:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.28/0.55 % (985922)Instruction limit reached!
% 1.28/0.55 % (985922)------------------------------
% 1.28/0.55 % (985922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985922)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985922)Termination reason: Instruction limit
% 1.28/0.55 % (985922)Termination phase: shuffling
% 1.28/0.55 % (985922)Time elapsed: 0.005 s
% 1.28/0.55 % (985922)Peak memory usage: 10 MB
% 1.28/0.55 % (985922)Instructions burned: 10 (million)
% 1.28/0.55 % (985920)Instruction limit reached!
% 1.28/0.55 % (985920)------------------------------
% 1.28/0.55 % (985920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985920)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985920)Termination reason: Instruction limit
% 1.28/0.55 % (985920)Termination phase: shuffling
% 1.28/0.55 % (985920)Time elapsed: 0.007 s
% 1.28/0.55 % (985920)Peak memory usage: 10 MB
% 1.28/0.55 % (985920)Instructions burned: 15 (million)
% 1.28/0.55 % (985929)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=637118025:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.28/0.55 % (985931)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=4190584996:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.28/0.55 % (985932)Instruction limit reached!
% 1.28/0.55 % (985932)------------------------------
% 1.28/0.55 % (985932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985932)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985932)Termination reason: Instruction limit
% 1.28/0.55 % (985932)Termination phase: Property scanning
% 1.28/0.55 % (985932)Time elapsed: 0.010 s
% 1.28/0.55 % (985932)Peak memory usage: 10 MB
% 1.28/0.55 % (985932)Instructions burned: 23 (million)
% 1.28/0.55 % (985931)Instruction limit reached!
% 1.28/0.55 % (985931)------------------------------
% 1.28/0.55 % (985931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985931)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985931)Termination reason: Instruction limit
% 1.28/0.55 % (985931)Termination phase: shuffling
% 1.28/0.55 % (985931)Time elapsed: 0.004 s
% 1.28/0.55 % (985931)Peak memory usage: 10 MB
% 1.28/0.55 % (985931)Instructions burned: 8 (million)
% 1.28/0.55 % (985936)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4039848763:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.28/0.55 % (985936)Instruction limit reached!
% 1.28/0.55 % (985936)------------------------------
% 1.28/0.55 % (985936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985936)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985936)Termination reason: Instruction limit
% 1.28/0.55 % (985936)Termination phase: Property scanning
% 1.28/0.55 % (985936)Time elapsed: 0.005 s
% 1.28/0.55 % (985936)Peak memory usage: 10 MB
% 1.28/0.55 % (985936)Instructions burned: 23 (million)
% 1.28/0.55 % (985929)Instruction limit reached!
% 1.28/0.55 % (985929)------------------------------
% 1.28/0.55 % (985929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985929)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985929)Termination reason: Instruction limit
% 1.28/0.55 % (985929)Termination phase: Property scanning
% 1.28/0.55 % (985929)Time elapsed: 0.014 s
% 1.28/0.55 % (985929)Peak memory usage: 10 MB
% 1.28/0.55 % (985929)Instructions burned: 32 (million)
% 1.28/0.55 % (985937)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=4104758974:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.28/0.55 % (985946)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3292620266:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.28/0.55 % (985942)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1909535623:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.28/0.55 % (985945)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1961392786:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.28/0.55 % (985947)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.28/0.55 % (985947)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2831601161:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.28/0.55 % (985946)Instruction limit reached!
% 1.28/0.55 % (985946)------------------------------
% 1.28/0.55 % (985946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985946)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985946)Termination reason: Instruction limit
% 1.28/0.55 % (985946)Termination phase: Property scanning
% 1.28/0.55 % (985946)Time elapsed: 0.010 s
% 1.28/0.55 % (985946)Peak memory usage: 11 MB
% 1.28/0.55 % (985946)Instructions burned: 46 (million)
% 1.28/0.55 % (985947)Instruction limit reached!
% 1.28/0.55 % (985947)------------------------------
% 1.28/0.55 % (985947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985947)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985947)Termination reason: Instruction limit
% 1.28/0.55 % (985947)Termination phase: shuffling
% 1.28/0.55 % (985947)Time elapsed: 0.004 s
% 1.28/0.55 % (985947)Peak memory usage: 10 MB
% 1.28/0.55 % (985947)Instructions burned: 9 (million)
% 1.28/0.55 % (985956)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=4037884393:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 1.28/0.55 % (985959)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=837746253: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.28/0.55 % (985942)Instruction limit reached!
% 1.28/0.55 % (985942)------------------------------
% 1.28/0.55 % (985942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985942)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985942)Termination reason: Instruction limit
% 1.28/0.55 % (985942)Termination phase: Function definition elimination
% 1.28/0.55 % (985942)Time elapsed: 0.059 s
% 1.28/0.55 % (985942)Peak memory usage: 11 MB
% 1.28/0.55 % (985942)Instructions burned: 146 (million)
% 1.28/0.55 % (985959)Refutation not found, incomplete strategy
% 1.28/0.55 % (985959)------------------------------
% 1.28/0.55 % (985959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985959)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985959)Termination reason: Refutation not found, incomplete strategy
% 1.28/0.55 % (985959)Time elapsed: 0.034 s
% 1.28/0.55 % (985959)Peak memory usage: 13 MB
% 1.28/0.55 % (985959)Instructions burned: 75 (million)
% 1.28/0.55 % (985959)------------------------------
% 1.28/0.55 % (985959)------------------------------
% 1.28/0.55 % (985956)Instruction limit reached!
% 1.28/0.55 % (985956)------------------------------
% 1.28/0.55 % (985956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985956)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985956)Termination reason: Instruction limit
% 1.28/0.55 % (985956)Termination phase: Saturation
% 1.28/0.55 % (985956)Time elapsed: 0.048 s
% 1.28/0.55 % (985956)Peak memory usage: 14 MB
% 1.28/0.55 % (985956)Instructions burned: 183 (million)
% 1.28/0.55 % (985945) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-985818-985945"...
% 1.28/0.55 % (985900)Instruction limit reached!
% 1.28/0.55 % (985900)------------------------------
% 1.28/0.55 % (985900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.55 % (985900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.55 % (985900)CaDiCaL version: 2.1.3
% 1.28/0.55 % (985900)Termination reason: Instruction limit
% 1.28/0.55 % (985900)Termination phase: Saturation
% 1.28/0.55 % (985900)Time elapsed: 0.148 s
% 1.28/0.55 % (985900)Peak memory usage: 14 MB
% 1.28/0.55 % (985900)Instructions burned: 328 (million)
% 1.28/0.55 % (985974)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.28/0.55 % (985977)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2373284934:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 1.28/0.55 % (985945)...printing done.
% 1.28/0.55 % (985945)Refutation found. Thanks to Tanya!
% 1.28/0.55 % SZS status Theorem for theBenchmark
% 1.28/0.55 % SZS output start Proof for theBenchmark
% 1.28/0.55 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.28/0.55 thf(func_def_0, type, is_of: ($i > ($i > $o) > $o)).
% 1.28/0.55 thf(func_def_2, type, all_of: (($i > $o) > ($i > $o) > $o)).
% 1.28/0.55 thf(func_def_3, type, eps: (($i > $o) > $i)).
% 1.28/0.55 thf(func_def_4, type, in: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_5, type, d_Subq: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_7, type, union: ($i > $i)).
% 1.28/0.55 thf(func_def_8, type, power: ($i > $i)).
% 1.28/0.55 thf(func_def_9, type, repl: ($i > ($i > $i) > $i)).
% 1.28/0.55 thf(func_def_10, type, d_Union_closed: ($i > $o)).
% 1.28/0.55 thf(func_def_11, type, d_Power_closed: ($i > $o)).
% 1.28/0.55 thf(func_def_12, type, d_Repl_closed: ($i > $o)).
% 1.28/0.55 thf(func_def_13, type, d_ZF_closed: ($i > $o)).
% 1.28/0.55 thf(func_def_14, type, univof: ($i > $i)).
% 1.28/0.55 thf(func_def_15, type, if: ($o > $i > $i > $i)).
% 1.28/0.55 thf(func_def_16, type, nIn: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_17, type, d_UPair: ($i > $i > $i)).
% 1.28/0.55 thf(func_def_18, type, d_Sing: ($i > $i)).
% 1.28/0.55 thf(func_def_19, type, binunion: ($i > $i > $i)).
% 1.28/0.55 thf(func_def_20, type, famunion: ($i > ($i > $i) > $i)).
% 1.28/0.55 thf(func_def_21, type, d_Sep: ($i > ($i > $o) > $i)).
% 1.28/0.55 thf(func_def_22, type, d_ReplSep: ($i > ($i > $o) > ($i > $i) > $i)).
% 1.28/0.55 thf(func_def_23, type, setminus: ($i > $i > $i)).
% 1.28/0.55 thf(func_def_24, type, d_In_rec_G: (($i > ($i > $i) > $i) > $i > $i > $o)).
% 1.28/0.55 thf(func_def_25, type, d_In_rec: (($i > ($i > $i) > $i) > $i > $i)).
% 1.28/0.55 thf(func_def_26, type, ordsucc: ($i > $i)).
% 1.28/0.55 thf(func_def_27, type, nat_p: ($i > $o)).
% 1.28/0.55 thf(func_def_29, type, d_Inj1: ($i > $i)).
% 1.28/0.55 thf(func_def_30, type, d_Inj0: ($i > $i)).
% 1.28/0.55 thf(func_def_31, type, d_Unj: ($i > $i)).
% 1.28/0.55 thf(func_def_32, type, pair: ($i > $i > $i)).
% 1.28/0.55 thf(func_def_33, type, proj0: ($i > $i)).
% 1.28/0.55 thf(func_def_34, type, proj1: ($i > $i)).
% 1.28/0.55 thf(func_def_35, type, d_Sigma: ($i > ($i > $i) > $i)).
% 1.28/0.55 thf(func_def_36, type, setprod: ($i > $i > $i)).
% 1.28/0.55 thf(func_def_37, type, ap: ($i > $i > $i)).
% 1.28/0.55 thf(func_def_38, type, pair_p: ($i > $o)).
% 1.28/0.55 thf(func_def_39, type, d_Pi: ($i > ($i > $i) > $i)).
% 1.28/0.55 thf(func_def_40, type, imp: ($o > $o > $o)).
% 1.28/0.55 thf(func_def_41, type, d_not: ($o > $o)).
% 1.28/0.55 thf(func_def_42, type, wel: ($o > $o)).
% 1.28/0.55 thf(func_def_43, type, obvious: $o).
% 1.28/0.55 thf(func_def_44, type, l_ec: ($o > $o > $o)).
% 1.28/0.55 thf(func_def_45, type, d_and: ($o > $o > $o)).
% 1.28/0.55 thf(func_def_46, type, l_or: ($o > $o > $o)).
% 1.28/0.55 thf(func_def_47, type, orec: ($o > $o > $o)).
% 1.28/0.55 thf(func_def_48, type, l_iff: ($o > $o > $o)).
% 1.28/0.55 thf(func_def_49, type, all: ($i > ($i > $o) > $o)).
% 1.28/0.55 thf(func_def_50, type, non: ($i > ($i > $o) > $i > $o)).
% 1.28/0.55 thf(func_def_51, type, l_some: ($i > ($i > $o) > $o)).
% 1.28/0.55 thf(func_def_52, type, or3: ($o > $o > $o > $o)).
% 1.28/0.55 thf(func_def_53, type, and3: ($o > $o > $o > $o)).
% 1.28/0.55 thf(func_def_54, type, ec3: ($o > $o > $o > $o)).
% 1.28/0.55 thf(func_def_55, type, orec3: ($o > $o > $o > $o)).
% 1.28/0.55 thf(func_def_56, type, e_is: ($i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_57, type, amone: ($i > ($i > $o) > $o)).
% 1.28/0.55 thf(func_def_58, type, one: ($i > ($i > $o) > $o)).
% 1.28/0.55 thf(func_def_59, type, ind: ($i > ($i > $o) > $i)).
% 1.28/0.55 thf(func_def_60, type, injective: ($i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_61, type, image: ($i > $i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_62, type, tofs: ($i > $i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_63, type, soft: ($i > $i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_64, type, inverse: ($i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_65, type, surjective: ($i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_66, type, bijective: ($i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_67, type, invf: ($i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_68, type, inj_h: ($i > $i > $i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_69, type, e_in: ($i > ($i > $o) > $i > $i)).
% 1.28/0.55 thf(func_def_70, type, out: ($i > ($i > $o) > $i > $i)).
% 1.28/0.55 thf(func_def_71, type, d_pair: ($i > $i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_72, type, first: ($i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_73, type, second: ($i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_74, type, prop1: ($o > $i > $i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_75, type, ite: ($o > $i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_76, type, wissel_wa: ($i > $i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_77, type, wissel_wb: ($i > $i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_78, type, wissel: ($i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_79, type, changef: ($i > $i > $i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_80, type, r_ec: ($o > $o > $o)).
% 1.28/0.55 thf(func_def_81, type, esti: ($i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_82, type, empty: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_83, type, nonempty: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_84, type, incl: ($i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_85, type, st_disj: ($i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_86, type, nissetprop: ($i > $i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_87, type, unmore: ($i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_88, type, ecelt: ($i > ($i > $i > $o) > $i > $i)).
% 1.28/0.55 thf(func_def_89, type, ecp: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.28/0.55 thf(func_def_90, type, anec: ($i > ($i > $i > $o) > $i > $o)).
% 1.28/0.55 thf(func_def_91, type, ect: ($i > ($i > $i > $o) > $i)).
% 1.28/0.55 thf(func_def_92, type, ectset: ($i > ($i > $i > $o) > $i > $i)).
% 1.28/0.55 thf(func_def_93, type, ectelt: ($i > ($i > $i > $o) > $i > $i)).
% 1.28/0.55 thf(func_def_94, type, ecect: ($i > ($i > $i > $o) > $i > $i)).
% 1.28/0.55 thf(func_def_95, type, fixfu: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.28/0.55 thf(func_def_96, type, d_10_prop1: ($i > ($i > $i > $o) > $i > $i > $i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_97, type, prop2: ($i > ($i > $i > $o) > $i > $i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_98, type, indeq: ($i > ($i > $i > $o) > $i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_99, type, fixfu2: ($i > ($i > $i > $o) > $i > $i > $o)).
% 1.28/0.55 thf(func_def_100, type, d_11_i: ($i > ($i > $i > $o) > $i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_101, type, indeq2: ($i > ($i > $i > $o) > $i > $i > $i > $i > $i)).
% 1.28/0.55 thf(func_def_103, type, n_is: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_104, type, nis: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_105, type, n_in: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_106, type, n_some: (($i > $o) > $o)).
% 1.28/0.55 thf(func_def_107, type, n_all: (($i > $o) > $o)).
% 1.28/0.55 thf(func_def_108, type, n_one: (($i > $o) > $o)).
% 1.28/0.55 thf(func_def_110, type, cond1: ($i > $o)).
% 1.28/0.55 thf(func_def_111, type, cond2: ($i > $o)).
% 1.28/0.55 thf(func_def_112, type, i1_s: (($i > $o) > $i)).
% 1.28/0.55 thf(func_def_113, type, d_22_prop1: ($i > $o)).
% 1.28/0.55 thf(func_def_114, type, d_23_prop1: ($i > $o)).
% 1.28/0.55 thf(func_def_115, type, d_24_prop1: ($i > $o)).
% 1.28/0.55 thf(func_def_116, type, d_24_prop2: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_117, type, prop3: ($i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_118, type, prop4: ($i > $o)).
% 1.28/0.55 thf(func_def_119, type, d_24_g: ($i > $i)).
% 1.28/0.55 thf(func_def_120, type, plus: ($i > $i)).
% 1.28/0.55 thf(func_def_121, type, n_pl: ($i > $i > $i)).
% 1.28/0.55 thf(func_def_122, type, d_25_prop1: ($i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_123, type, d_26_prop1: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_124, type, d_27_prop1: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_125, type, d_28_prop1: ($i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_126, type, diffprop: ($i > $i > $i > $o)).
% 1.28/0.55 thf(func_def_127, type, d_29_ii: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_128, type, iii: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_129, type, d_29_prop1: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_130, type, moreis: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_131, type, lessis: ($i > $i > $o)).
% 1.28/0.55 thf(func_def_134, type, db3: !>[X0: $tType]:(X0)).
% 1.28/0.55 thf(func_def_135, type, db1: !>[X0: $tType]:(X0)).
% 1.28/0.55 thf(func_def_136, type, db2: !>[X0: $tType]:(X0)).
% 1.28/0.55 thf(func_def_137, type, db0: !>[X0: $tType]:(X0)).
% 1.28/0.55 thf(func_def_138, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.28/0.55 thf(func_def_139, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.28/0.55 thf(func_def_140, type, vNOT: ($o > $o)).
% 1.28/0.55 thf(func_def_141, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.28/0.55 thf(func_def_142, type, vAND: ($o > $o > $o)).
% 1.28/0.55 thf(func_def_143, type, db4: !>[X0: $tType]:(X0)).
% 1.28/0.55 thf(func_def_144, type, vIMP: ($o > $o > $o)).
% 1.28/0.55 thf(func_def_145, type, db5: !>[X0: $tType]:(X0)).
% 1.28/0.55 thf(func_def_146, type, vOR: ($o > $o > $o)).
% 1.28/0.55 thf(func_def_147, type, db6: !>[X0: $tType]:(X0)).
% 1.28/0.55 thf(func_def_148, type, db7: !>[X0: $tType]:(X0)).
% 1.28/0.55 thf(func_def_149, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.28/0.55 thf(func_def_150, type, sK0: (($i > $o) > $i)).
% 1.28/0.55 thf(func_def_151, type, sK1: ($i > ($i > $i) > ($i > $i) > $i)).
% 1.28/0.55 thf(func_def_154, type, sK4: ($i > $i > $i > $i > $i)).
% 1.28/0.55 thf(f2,axiom,(
% 1.28/0.55 ((^[X0 : ($i > $o), X1 : ($i > $o)] : (! [X2 : $i] : ((is_of @ X2 @ X0) => (X1 @ X2)))) = all_of)),
% 1.28/0.55 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_all_of)).
% 1.28/0.55 thf(f74,axiom,(
% 1.28/0.55 (imp = (^[X0 : $o, X1 : $o] : (X0 => X1)))),
% 1.28/0.55 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_imp)).
% 1.28/0.55 thf(f81,axiom,(
% 1.28/0.55 (l_or = (^[X0 : $o] : ((imp @ (d_not @ X0)))))),
% 1.28/0.55 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_l_or)).
% 1.28/0.55 thf(f157,axiom,(
% 1.28/0.55 (n_is = ((e_is @ nat)))),
% 1.28/0.55 file('/export/starexec/sandbox/benchmark/Axioms/NUM007^0.ax',def_n_is)).
% 1.28/0.55 thf(f205,axiom,(
% 1.28/0.55 (d_29_ii = (^[X0 : $i, X1 : $i] : ((n_some @ (diffprop @ X0 @ X1)))))),
% 1.28/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_d_29_ii)).
% 1.28/0.55 thf(f214,axiom,(
% 1.28/0.55 (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.28/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz11)).
% 1.28/0.55 thf(f215,axiom,(
% 1.28/0.55 (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.28/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz12)).
% 1.28/0.55 thf(f216,axiom,(
% 1.28/0.55 (moreis = (^[X0 : $i, X1 : $i] : ((l_or @ (d_29_ii @ X0 @ X1) @ (n_is @ X0 @ X1)))))),
% 1.28/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_moreis)).
% 1.28/0.55 thf(f217,axiom,(
% 1.28/0.55 ((^[X0 : $i, X1 : $i] : ((l_or @ (iii @ X0 @ X1) @ (n_is @ X0 @ X1)))) = lessis)),
% 1.28/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_lessis)).
% 1.28/0.55 thf(f219,axiom,(
% 1.28/0.55 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((lessis @ X0 @ X1) => (moreis @ X1 @ X0)))))))),
% 1.28/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz14)).
% 1.28/0.55 thf(f220,axiom,(
% 1.28/0.55 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X0 : $i] : ((all_of @ (^[X1 : $i] : ((in @ X1 @ nat))) @ (^[X1 : $i] : ((moreis @ X0 @ X1) => (d_not @ (iii @ X0 @ X1))))))))),
% 1.28/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz10c)).
% 1.28/0.55 thf(f221,conjecture,(
% 1.28/0.55 (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.28/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz10d)).
% 1.28/0.55 thf(f222,negated_conjecture,(
% 1.28/0.55 ~(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.28/0.55 inference(negated_conjecture,[status(cth)],[f221])).
% 1.28/0.55 thf(f300,plain,(
% 1.28/0.55 (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.28/0.55 inference(rectify,[],[f215])).
% 1.28/0.55 thf(f301,plain,(
% 1.28/0.55 (((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.28/0.55 inference(fool_elimination,[],[f300])).
% 1.28/0.55 thf(f350,plain,(
% 1.28/0.55 (d_29_ii = (^[Y0 : $i]: ((^[Y1 : $i]: (n_some @ (diffprop @ Y0 @ Y1))))))),
% 1.28/0.55 inference(fool_elimination,[],[f205])).
% 1.28/0.55 thf(f398,plain,(
% 1.28/0.55 (moreis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (d_29_ii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.28/0.55 inference(fool_elimination,[],[f216])).
% 1.28/0.55 thf(f461,plain,(
% 1.28/0.55 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((lessis @ X1 @ X3) => (moreis @ X3 @ X1)))))))),
% 1.28/0.55 inference(rectify,[],[f219])).
% 1.28/0.55 thf(f462,plain,(
% 1.28/0.55 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((lessis @ Y0 @ Y1) => (moreis @ Y1 @ Y0))))))))),
% 1.28/0.55 inference(fool_elimination,[],[f461])).
% 1.28/0.55 thf(f463,plain,(
% 1.28/0.55 (imp = (^[X0 : $o, X1 : $o] : (X0 => X1)))),
% 1.28/0.55 inference(rectify,[],[f74])).
% 1.28/0.55 thf(f464,plain,(
% 1.28/0.55 (imp = (^[Y0 : $o]: ((^[Y1 : $o]: (Y0 => Y1)))))),
% 1.28/0.55 inference(fool_elimination,[],[f463])).
% 1.28/0.55 thf(f476,plain,(
% 1.28/0.55 (all_of @ (^[X0 : $i] : ((in @ X0 @ nat))) @ (^[X1 : $i] : ((all_of @ (^[X2 : $i] : ((in @ X2 @ nat))) @ (^[X3 : $i] : ((moreis @ X1 @ X3) => (d_not @ (iii @ X1 @ X3))))))))),
% 1.28/0.55 inference(rectify,[],[f220])).
% 1.28/0.55 thf(f477,plain,(
% 1.28/0.55 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((moreis @ Y0 @ Y1) => (d_not @ (iii @ Y0 @ Y1)))))))))),
% 1.28/0.55 inference(fool_elimination,[],[f476])).
% 1.28/0.55 thf(f478,plain,(
% 1.28/0.55 ~(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.28/0.55 inference(rectify,[],[f222])).
% 1.28/0.55 thf(f479,plain,(
% 1.28/0.55 ~ ($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.28/0.55 inference(fool_elimination,[],[f478])).
% 1.28/0.55 thf(f521,plain,(
% 1.28/0.55 (l_or = (^[Y0 : $o]: (imp @ (d_not @ Y0))))),
% 1.28/0.55 inference(fool_elimination,[],[f81])).
% 1.28/0.55 thf(f540,plain,(
% 1.28/0.55 (lessis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (iii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.28/0.55 inference(fool_elimination,[],[f217])).
% 1.28/0.55 thf(f547,plain,(
% 1.28/0.55 ((^[X0 : ($i > $o), X1 : ($i > $o)] : (! [X2 : $i] : ((is_of @ X2 @ X0) => (X1 @ X2)))) = all_of)),
% 1.28/0.55 inference(rectify,[],[f2])).
% 1.28/0.55 thf(f548,plain,(
% 1.28/0.55 (all_of = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))))),
% 1.28/0.55 inference(fool_elimination,[],[f547])).
% 1.28/0.55 thf(f553,plain,(
% 1.28/0.55 (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.28/0.55 inference(rectify,[],[f214])).
% 1.28/0.55 thf(f554,plain,(
% 1.28/0.55 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_29_ii @ Y0 @ Y1) => (iii @ Y1 @ Y0))))))))),
% 1.28/0.55 inference(fool_elimination,[],[f553])).
% 1.28/0.55 thf(f572,plain,(
% 1.28/0.55 ($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.28/0.55 inference(flattening,[],[f479])).
% 1.28/0.55 thf(f588,plain,(
% 1.28/0.55 (all_of = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))))),
% 1.28/0.55 inference(cnf_transformation,[],[f548])).
% 1.28/0.55 thf(f590,plain,(
% 1.28/0.55 (l_or = (^[Y0 : $o]: (imp @ (d_not @ Y0))))),
% 1.28/0.55 inference(cnf_transformation,[],[f521])).
% 1.28/0.55 thf(f600,plain,(
% 1.28/0.55 ($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.28/0.55 inference(cnf_transformation,[],[f572])).
% 1.28/0.55 thf(f602,plain,(
% 1.28/0.55 (imp = (^[Y0 : $o]: ((^[Y1 : $o]: (Y0 => Y1)))))),
% 1.28/0.55 inference(cnf_transformation,[],[f464])).
% 1.28/0.55 thf(f608,plain,(
% 1.28/0.55 (((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.28/0.55 inference(cnf_transformation,[],[f301])).
% 1.28/0.55 thf(f613,plain,(
% 1.28/0.55 (n_is = ((e_is @ nat)))),
% 1.28/0.55 inference(cnf_transformation,[],[f157])).
% 1.28/0.55 thf(f620,plain,(
% 1.28/0.55 (d_29_ii = (^[Y0 : $i]: ((^[Y1 : $i]: (n_some @ (diffprop @ Y0 @ Y1))))))),
% 1.28/0.55 inference(cnf_transformation,[],[f350])).
% 1.28/0.55 thf(f622,plain,(
% 1.28/0.55 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((moreis @ Y0 @ Y1) => (d_not @ (iii @ Y0 @ Y1)))))))))),
% 1.28/0.55 inference(cnf_transformation,[],[f477])).
% 1.28/0.55 thf(f627,plain,(
% 1.28/0.55 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((d_29_ii @ Y0 @ Y1) => (iii @ Y1 @ Y0))))))))),
% 1.28/0.55 inference(cnf_transformation,[],[f554])).
% 1.28/0.55 thf(f629,plain,(
% 1.28/0.55 (moreis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (d_29_ii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.28/0.55 inference(cnf_transformation,[],[f398])).
% 1.28/0.55 thf(f636,plain,(
% 1.28/0.55 ($true = ((all_of @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: (all_of @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((lessis @ Y0 @ Y1) => (moreis @ Y1 @ Y0))))))))),
% 1.28/0.55 inference(cnf_transformation,[],[f462])).
% 1.28/0.55 thf(f640,plain,(
% 1.28/0.55 (lessis = (^[Y0 : $i]: ((^[Y1 : $i]: (l_or @ (iii @ Y0 @ Y1) @ (n_is @ Y0 @ Y1))))))),
% 1.28/0.55 inference(cnf_transformation,[],[f540])).
% 1.28/0.55 thf(f642,definition,(
% 1.28/0.55 ($false != $true)),
% 1.28/0.55 introduced(theory,[fool_distinctness_axiom])).
% 1.28/0.55 thf(f643,definition,(
% 1.28/0.55 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.28/0.55 introduced(theory,[fool_exhaustiveness_axiom])).
% 1.28/0.55 thf(f644,plain,(
% 1.28/0.55 (l_or = (^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: (Y1 => Y2)))) @ (d_not @ Y0))))),
% 1.28/0.55 inference(definition_unfolding,[],[f590,f602])).
% 1.28/0.55 thf(f645,plain,(
% 1.28/0.55 (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.28/0.55 inference(definition_unfolding,[],[f629,f644,f620,f613])).
% 1.28/0.55 thf(f646,plain,(
% 1.28/0.55 (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.28/0.55 inference(definition_unfolding,[],[f640,f644,f613])).
% 1.28/0.55 thf(f660,plain,(
% 1.28/0.55 ((((^[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.28/0.55 inference(definition_unfolding,[],[f600,f588,f588,f646,f620])).
% 1.28/0.55 thf(f664,plain,(
% 1.28/0.55 ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))) @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: ((is_of @ Y3 @ Y1) => (Y2 @ Y3))))))) @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: ((iii @ Y0 @ Y1) => ((^[Y2 : $i]: ((^[Y3 : $i]: (n_some @ (diffprop @ Y2 @ Y3))))) @ Y1 @ Y0))))))))),
% 1.28/0.55 inference(definition_unfolding,[],[f608,f588,f588,f620])).
% 1.28/0.55 thf(f674,plain,(
% 1.28/0.55 ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))) @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: ((is_of @ Y3 @ Y1) => (Y2 @ Y3))))))) @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: (((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $o]: ((^[Y5 : $o]: ((^[Y6 : $o]: (Y5 => Y6)))) @ (d_not @ Y4))) @ ((^[Y4 : $i]: ((^[Y5 : $i]: (n_some @ (diffprop @ Y4 @ Y5))))) @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y0 @ Y1) => (d_not @ (iii @ Y0 @ Y1)))))))))),
% 1.28/0.55 inference(definition_unfolding,[],[f622,f588,f588,f645])).
% 1.28/0.55 thf(f676,plain,(
% 1.28/0.55 ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))) @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: ((is_of @ Y3 @ Y1) => (Y2 @ Y3))))))) @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: (((^[Y2 : $i]: ((^[Y3 : $i]: (n_some @ (diffprop @ Y2 @ Y3))))) @ Y0 @ Y1) => (iii @ Y1 @ Y0))))))))),
% 1.28/0.55 inference(definition_unfolding,[],[f627,f588,f588,f620])).
% 1.28/0.55 thf(f680,plain,(
% 1.28/0.55 ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((is_of @ Y2 @ Y0) => (Y1 @ Y2))))))) @ (^[Y0 : $i]: (in @ Y0 @ nat)) @ (^[Y0 : $i]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: ((is_of @ Y3 @ Y1) => (Y2 @ Y3))))))) @ (^[Y1 : $i]: (in @ Y1 @ nat)) @ (^[Y1 : $i]: (((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $o]: ((^[Y5 : $o]: ((^[Y6 : $o]: (Y5 => Y6)))) @ (d_not @ Y4))) @ (iii @ Y2 @ Y3) @ (e_is @ nat @ Y2 @ Y3))))) @ Y0 @ Y1) => ((^[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))))) @ Y1 @ Y0))))))))),
% 1.28/0.55 inference(definition_unfolding,[],[f636,f588,f588,f646,f645])).
% 1.28/0.55 thf(f741,plain,(
% 1.28/0.55 ($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.28/0.55 inference(beta-eta_normalization,[],[f660])).
% 1.28/0.55 thf(f742,plain,(
% 1.28/0.55 ($false = (((^[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))))))))) @ sK2)))),
% 1.28/0.55 inference(sigma_proxy_clausification,[],[f741])).
% 1.28/0.55 thf(f743,plain,(
% 1.28/0.55 ((((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (iii @ sK2 @ Y0)) => (e_is @ nat @ sK2 @ Y0)) => (d_not @ (n_some @ (diffprop @ sK2 @ Y0))))))))) = $false)),
% 1.28/0.55 inference(beta-eta_normalization,[],[f742])).
% 1.28/0.55 thf(f744,plain,(
% 1.28/0.55 ($false = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (iii @ sK2 @ Y0)) => (e_is @ nat @ sK2 @ Y0)) => (d_not @ (n_some @ (diffprop @ sK2 @ Y0)))))))))),
% 1.28/0.55 inference(imp_proxy_clausification,[],[f743])).
% 1.28/0.55 thf(f745,plain,(
% 1.28/0.55 ($true = ((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))),
% 1.28/0.55 inference(imp_proxy_clausification,[],[f743])).
% 1.28/0.55 thf(f746,plain,(
% 1.28/0.55 ($false = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (iii @ sK2 @ Y0)) => (e_is @ nat @ sK2 @ Y0)) => (d_not @ (n_some @ (diffprop @ sK2 @ Y0)))))) @ sK3)))),
% 1.28/0.55 inference(sigma_proxy_clausification,[],[f744])).
% 1.28/0.55 thf(f747,plain,(
% 1.28/0.55 ($false = (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (((d_not @ (iii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3)) => (d_not @ (n_some @ (diffprop @ sK2 @ sK3)))))))),
% 1.28/0.55 inference(beta-eta_normalization,[],[f746])).
% 1.28/0.55 thf(f748,plain,(
% 1.28/0.55 (((((d_not @ (iii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3)) => (d_not @ (n_some @ (diffprop @ sK2 @ sK3))))) = $false)),
% 1.28/0.55 inference(imp_proxy_clausification,[],[f747])).
% 1.28/0.55 thf(f749,plain,(
% 1.28/0.55 (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true)),
% 1.28/0.55 inference(imp_proxy_clausification,[],[f747])).
% 1.28/0.55 thf(f750,plain,(
% 1.28/0.55 ($false = ((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))))),
% 1.28/0.55 inference(imp_proxy_clausification,[],[f748])).
% 1.28/0.55 thf(f751,plain,(
% 1.28/0.55 ($true = (((d_not @ (iii @ sK2 @ sK3)) => (e_is @ nat @ sK2 @ sK3))))),
% 1.28/0.55 inference(imp_proxy_clausification,[],[f748])).
% 1.28/0.55 thf(f752,plain,(
% 1.28/0.55 ($false = ((d_not @ (iii @ sK2 @ sK3)))) | ($true = ((e_is @ nat @ sK2 @ sK3)))),
% 1.28/0.55 inference(imp_proxy_clausification,[],[f751])).
% 1.28/0.55 thf(f771,plain,(
% 1.28/0.55 ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => (((d_not @ (n_some @ (diffprop @ Y0 @ Y1))) => (e_is @ nat @ Y0 @ Y1)) => (d_not @ (iii @ Y0 @ Y1)))))))))))),
% 1.28/0.55 inference(beta-eta_normalization,[],[f674])).
% 1.28/0.55 thf(f772,plain,(
% 1.28/0.55 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => (((d_not @ (n_some @ (diffprop @ Y0 @ Y1))) => (e_is @ nat @ Y0 @ Y1)) => (d_not @ (iii @ Y0 @ Y1)))))))) @ X1)))) )),
% 1.28/0.55 inference(pi_proxy_clausification,[],[f771])).
% 1.28/0.55 thf(f773,plain,(
% 1.28/0.55 ( ! [X1 : $i] : (($true = (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (iii @ X1 @ Y0)))))))))) )),
% 1.28/0.56 inference(beta-eta_normalization,[],[f772])).
% 1.28/0.56 thf(f774,plain,(
% 1.28/0.56 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (iii @ X1 @ Y0))))))))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f773])).
% 1.28/0.56 thf(f775,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (n_some @ (diffprop @ X1 @ Y0))) => (e_is @ nat @ X1 @ Y0)) => (d_not @ (iii @ X1 @ Y0))))) @ X2))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.28/0.56 inference(pi_proxy_clausification,[],[f774])).
% 1.28/0.56 thf(f776,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2)) => (d_not @ (iii @ X1 @ X2))))) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.28/0.56 inference(beta-eta_normalization,[],[f775])).
% 1.28/0.56 thf(f777,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2)) => (d_not @ (iii @ X1 @ X2))))) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f776])).
% 1.28/0.56 thf(f778,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($false = (((d_not @ (n_some @ (diffprop @ X1 @ X2))) => (e_is @ nat @ X1 @ X2)))) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($true = ((d_not @ (iii @ X1 @ X2)))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f777])).
% 1.28/0.56 thf(f779,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($true = ((d_not @ (iii @ X1 @ X2)))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((e_is @ nat @ X1 @ X2)))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f778])).
% 1.28/0.56 thf(f780,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($true = ((d_not @ (iii @ X1 @ X2)))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((d_not @ (n_some @ (diffprop @ X1 @ X2)))) = $true)) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f778])).
% 1.28/0.56 thf(f823,plain,(
% 1.28/0.56 (((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => (((d_not @ (iii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1)) => ((d_not @ (n_some @ (diffprop @ Y1 @ Y0))) => (e_is @ nat @ Y1 @ Y0)))))))))) = $true)),
% 1.28/0.56 inference(beta-eta_normalization,[],[f680])).
% 1.28/0.56 thf(f824,plain,(
% 1.28/0.56 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => (((d_not @ (iii @ Y0 @ Y1)) => (e_is @ nat @ Y0 @ Y1)) => ((d_not @ (n_some @ (diffprop @ Y1 @ Y0))) => (e_is @ nat @ Y1 @ Y0)))))))) @ X1)))) )),
% 1.28/0.56 inference(pi_proxy_clausification,[],[f823])).
% 1.28/0.56 thf(f825,plain,(
% 1.28/0.56 ( ! [X1 : $i] : (((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (((d_not @ (iii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0)) => ((d_not @ (n_some @ (diffprop @ Y0 @ X1))) => (e_is @ nat @ Y0 @ X1)))))))) = $true)) )),
% 1.28/0.56 inference(beta-eta_normalization,[],[f824])).
% 1.28/0.56 thf(f826,plain,(
% 1.28/0.56 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((!! @ $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 @ Y0 @ X1))) => (e_is @ nat @ Y0 @ X1))))))) = $true)) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f825])).
% 1.28/0.56 thf(f827,plain,(
% 1.28/0.56 ( ! [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 @ (iii @ X1 @ Y0)) => (e_is @ nat @ X1 @ Y0)) => ((d_not @ (n_some @ (diffprop @ Y0 @ X1))) => (e_is @ nat @ Y0 @ X1))))) @ X2)) = $true)) )),
% 1.28/0.56 inference(pi_proxy_clausification,[],[f826])).
% 1.28/0.56 thf(f828,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($true = (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)) => ((d_not @ (n_some @ (diffprop @ X2 @ X1))) => (e_is @ nat @ X2 @ X1)))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.28/0.56 inference(beta-eta_normalization,[],[f827])).
% 1.28/0.56 thf(f829,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)) => ((d_not @ (n_some @ (diffprop @ X2 @ X1))) => (e_is @ nat @ X2 @ X1)))) = $true) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f828])).
% 1.28/0.56 thf(f830,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($true = (((d_not @ (n_some @ (diffprop @ X2 @ X1))) => (e_is @ nat @ X2 @ X1)))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = (((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)))) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f829])).
% 1.28/0.56 thf(f831,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($false = (((d_not @ (iii @ X1 @ X2)) => (e_is @ nat @ X1 @ X2)))) | ($false = ((d_not @ (n_some @ (diffprop @ X2 @ X1))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | (((e_is @ nat @ X2 @ X1)) = $true) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f830])).
% 1.28/0.56 thf(f832,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((e_is @ nat @ X2 @ X1)) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((d_not @ (n_some @ (diffprop @ X2 @ X1))))) | ($false = ((e_is @ nat @ X1 @ X2)))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f831])).
% 1.28/0.56 thf(f862,plain,(
% 1.28/0.56 ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((n_some @ (diffprop @ Y0 @ Y1)) => (iii @ Y1 @ Y0))))))))))),
% 1.28/0.56 inference(beta-eta_normalization,[],[f676])).
% 1.28/0.56 thf(f863,plain,(
% 1.28/0.56 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((n_some @ (diffprop @ Y0 @ Y1)) => (iii @ Y1 @ Y0))))))) @ X1)))) )),
% 1.28/0.56 inference(pi_proxy_clausification,[],[f862])).
% 1.28/0.56 thf(f864,plain,(
% 1.28/0.56 ( ! [X1 : $i] : (($true = (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ X1 @ Y0)) => (iii @ Y0 @ X1))))))))) )),
% 1.28/0.56 inference(beta-eta_normalization,[],[f863])).
% 1.28/0.56 thf(f865,plain,(
% 1.28/0.56 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ X1 @ Y0)) => (iii @ Y0 @ X1)))))))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f864])).
% 1.28/0.56 thf(f866,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((n_some @ (diffprop @ X1 @ Y0)) => (iii @ Y0 @ X1)))) @ X2))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.28/0.56 inference(pi_proxy_clausification,[],[f865])).
% 1.28/0.56 thf(f867,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((n_some @ (diffprop @ X1 @ X2)) => (iii @ X2 @ X1)))))) )),
% 1.28/0.56 inference(beta-eta_normalization,[],[f866])).
% 1.28/0.56 thf(f868,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = (((n_some @ (diffprop @ X1 @ X2)) => (iii @ X2 @ X1))))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f867])).
% 1.28/0.56 thf(f869,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((n_some @ (diffprop @ X1 @ X2)))) | ($true = ((iii @ X2 @ X1)))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f868])).
% 1.28/0.56 thf(f916,plain,(
% 1.28/0.56 (((!! @ $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)))))))))) = $true)),
% 1.28/0.56 inference(beta-eta_normalization,[],[f664])).
% 1.28/0.56 thf(f917,plain,(
% 1.28/0.56 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => (!! @ $i @ (^[Y1 : $i]: ((is_of @ Y1 @ (^[Y2 : $i]: (in @ Y2 @ nat))) => ((iii @ Y0 @ Y1) => (n_some @ (diffprop @ Y1 @ Y0)))))))) @ X1)) = $true)) )),
% 1.28/0.56 inference(pi_proxy_clausification,[],[f916])).
% 1.28/0.56 thf(f918,plain,(
% 1.28/0.56 ( ! [X1 : $i] : (($true = (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => (!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((iii @ X1 @ Y0) => (n_some @ (diffprop @ Y0 @ X1)))))))))) )),
% 1.28/0.56 inference(beta-eta_normalization,[],[f917])).
% 1.28/0.56 thf(f919,plain,(
% 1.28/0.56 ( ! [X1 : $i] : ((((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((is_of @ Y0 @ (^[Y1 : $i]: (in @ Y1 @ nat))) => ((iii @ X1 @ Y0) => (n_some @ (diffprop @ Y0 @ X1))))))))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f918])).
% 1.28/0.56 thf(f920,plain,(
% 1.28/0.56 ( ! [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.28/0.56 inference(pi_proxy_clausification,[],[f919])).
% 1.28/0.56 thf(f921,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (((((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))) => ((iii @ X1 @ X2) => (n_some @ (diffprop @ X2 @ X1))))) = $true) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false)) )),
% 1.28/0.56 inference(beta-eta_normalization,[],[f920])).
% 1.28/0.56 thf(f922,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($true = (((iii @ X1 @ X2) => (n_some @ (diffprop @ X2 @ X1))))) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f921])).
% 1.28/0.56 thf(f923,plain,(
% 1.28/0.56 ( ! [X2 : $i,X1 : $i] : (($false = ((is_of @ X2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((iii @ X1 @ X2)) = $false) | (((is_of @ X1 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $false) | ($true = ((n_some @ (diffprop @ X2 @ X1))))) )),
% 1.28/0.56 inference(imp_proxy_clausification,[],[f922])).
% 1.28/0.56 thf(f930,definition,(
% 1.28/0.56 spl5_2 <=> ($true = ((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat)))))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition])).
% 1.28/0.56 thf(f932,plain,(
% 1.28/0.56 ($true = ((is_of @ sK2 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ~spl5_2),
% 1.28/0.56 inference(avatar_component_clause,[],[f930])).
% 1.28/0.56 thf(f933,plain,(
% 1.28/0.56 spl5_2),
% 1.28/0.56 inference(avatar_split_clause,[],[f745,f930])).
% 1.28/0.56 thf(f935,definition,(
% 1.28/0.56 spl5_3 <=> (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true)),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition])).
% 1.28/0.56 thf(f937,plain,(
% 1.28/0.56 (((is_of @ sK3 @ (^[Y0 : $i]: (in @ Y0 @ nat)))) = $true) | ~spl5_3),
% 1.28/0.56 inference(avatar_component_clause,[],[f935])).
% 1.28/0.56 thf(f938,plain,(
% 1.28/0.56 spl5_3),
% 1.28/0.56 inference(avatar_split_clause,[],[f749,f935])).
% 1.28/0.56 thf(f940,definition,(
% 1.28/0.56 spl5_4 <=> ($false = ((d_not @ (iii @ sK2 @ sK3))))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition])).
% 1.28/0.56 thf(f944,definition,(
% 1.28/0.56 spl5_5 <=> ($true = ((e_is @ nat @ sK2 @ sK3)))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition])).
% 1.28/0.56 thf(f947,plain,(
% 1.28/0.56 spl5_4 | spl5_5),
% 1.28/0.56 inference(avatar_split_clause,[],[f752,f944,f940])).
% 1.28/0.56 thf(f949,definition,(
% 1.28/0.56 spl5_6 <=> ($false = ((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition])).
% 1.28/0.56 thf(f951,plain,(
% 1.28/0.56 ($false = ((d_not @ (n_some @ (diffprop @ sK2 @ sK3))))) | ~spl5_6),
% 1.28/0.56 inference(avatar_component_clause,[],[f949])).
% 1.28/0.56 thf(f952,plain,(
% 1.28/0.56 spl5_6),
% 1.28/0.56 inference(avatar_split_clause,[],[f750,f949])).
% 1.28/0.56 thf(f954,definition,(
% 1.28/0.56 spl5_7 <=> ($false = $true)),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition])).
% 1.28/0.56 thf(f957,plain,(
% 1.28/0.56 ~spl5_7),
% 1.28/0.56 inference(avatar_split_clause,[],[f642,f954])).
% 1.28/0.56 thf(f971,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = ((n_some @ (diffprop @ X0 @ sK2)))) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((iii @ sK2 @ X0)) = $true) | ($false = $true)) ) | ~spl5_2),
% 1.28/0.56 inference(superposition,[],[f932,f869])).
% 1.28/0.56 thf(f972,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = ((n_some @ (diffprop @ X0 @ sK3)))) | ($false = $true) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($true = ((iii @ sK3 @ X0)))) ) | ~spl5_3),
% 1.28/0.56 inference(superposition,[],[f937,f869])).
% 1.28/0.56 thf(f974,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($true = ((iii @ sK3 @ X0))) | ($false = ((n_some @ (diffprop @ X0 @ sK3))))) ) | ~spl5_3),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f972])).
% 1.28/0.56 thf(f976,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((iii @ sK2 @ X0)) = $true) | ($false = ((n_some @ (diffprop @ X0 @ sK2))))) ) | ~spl5_2),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f971])).
% 1.28/0.56 thf(f985,plain,(
% 1.28/0.56 (((n_some @ (diffprop @ sK2 @ sK3))) = $false) | ($false = ((d_not @ $true))) | ~spl5_6),
% 1.28/0.56 inference(superposition,[],[f951,f643])).
% 1.28/0.56 thf(f996,definition,(
% 1.28/0.56 spl5_8 <=> (((n_some @ (diffprop @ sK2 @ sK3))) = $false)),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition])).
% 1.28/0.56 thf(f998,plain,(
% 1.28/0.56 (((n_some @ (diffprop @ sK2 @ sK3))) = $false) | ~spl5_8),
% 1.28/0.56 inference(avatar_component_clause,[],[f996])).
% 1.28/0.56 thf(f1000,definition,(
% 1.28/0.56 spl5_9 <=> ($false = ((d_not @ $true)))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition])).
% 1.28/0.56 thf(f1001,plain,(
% 1.28/0.56 ($false != ((d_not @ $true))) | spl5_9),
% 1.28/0.56 inference(avatar_component_clause,[],[f1000])).
% 1.28/0.56 thf(f1002,plain,(
% 1.28/0.56 ($false = ((d_not @ $true))) | ~spl5_9),
% 1.28/0.56 inference(avatar_component_clause,[],[f1000])).
% 1.28/0.56 thf(f1003,plain,(
% 1.28/0.56 spl5_8 | spl5_9 | ~spl5_6),
% 1.28/0.56 inference(avatar_split_clause,[],[f985,f949,f1000,f996])).
% 1.28/0.56 thf(f1004,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($true = ((n_some @ (diffprop @ sK2 @ X0)))) | ($false = ((iii @ X0 @ sK2))) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($false = $true)) ) | ~spl5_2),
% 1.28/0.56 inference(superposition,[],[f923,f932])).
% 1.28/0.56 thf(f1005,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($false = ((iii @ X0 @ sK3))) | ($false = $true) | (((n_some @ (diffprop @ sK3 @ X0))) = $true)) ) | ~spl5_3),
% 1.28/0.56 inference(superposition,[],[f923,f937])).
% 1.28/0.56 thf(f1010,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((n_some @ (diffprop @ sK3 @ X0))) = $true) | ($false = ((iii @ X0 @ sK3)))) ) | ~spl5_3),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1005])).
% 1.28/0.56 thf(f1013,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($true = ((n_some @ (diffprop @ sK2 @ X0)))) | ($false = ((iii @ X0 @ sK2)))) ) | ~spl5_2),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1004])).
% 1.28/0.56 thf(f1017,plain,(
% 1.28/0.56 ($false = ((d_not @ $false))) | (~spl5_6 | ~spl5_8)),
% 1.28/0.56 inference(superposition,[],[f951,f998])).
% 1.28/0.56 thf(f1020,definition,(
% 1.28/0.56 spl5_10 <=> ($false = ((d_not @ $false)))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition])).
% 1.28/0.56 thf(f1021,plain,(
% 1.28/0.56 ($false != ((d_not @ $false))) | spl5_10),
% 1.28/0.56 inference(avatar_component_clause,[],[f1020])).
% 1.28/0.56 thf(f1022,plain,(
% 1.28/0.56 ($false = ((d_not @ $false))) | ~spl5_10),
% 1.28/0.56 inference(avatar_component_clause,[],[f1020])).
% 1.28/0.56 thf(f1023,plain,(
% 1.28/0.56 spl5_10 | ~spl5_6 | ~spl5_8),
% 1.28/0.56 inference(avatar_split_clause,[],[f1017,f996,f949,f1020])).
% 1.28/0.56 thf(f1043,plain,(
% 1.28/0.56 ($true = ((iii @ sK2 @ sK3))) | ($false = ((n_some @ (diffprop @ sK3 @ sK2)))) | ($false = $true) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(superposition,[],[f937,f976])).
% 1.28/0.56 thf(f1046,plain,(
% 1.28/0.56 ($false = ((n_some @ (diffprop @ sK3 @ sK2)))) | ($true = ((iii @ sK2 @ sK3))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1043])).
% 1.28/0.56 thf(f1050,definition,(
% 1.28/0.56 spl5_11 <=> ($true = ((iii @ sK2 @ sK3)))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition])).
% 1.28/0.56 thf(f1052,plain,(
% 1.28/0.56 ($true = ((iii @ sK2 @ sK3))) | ~spl5_11),
% 1.28/0.56 inference(avatar_component_clause,[],[f1050])).
% 1.28/0.56 thf(f1054,definition,(
% 1.28/0.56 spl5_12 <=> ($false = ((n_some @ (diffprop @ sK3 @ sK2))))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition])).
% 1.28/0.56 thf(f1056,plain,(
% 1.28/0.56 ($false = ((n_some @ (diffprop @ sK3 @ sK2)))) | ~spl5_12),
% 1.28/0.56 inference(avatar_component_clause,[],[f1054])).
% 1.28/0.56 thf(f1067,plain,(
% 1.28/0.56 spl5_11 | spl5_12 | ~spl5_2 | ~spl5_3),
% 1.28/0.56 inference(avatar_split_clause,[],[f1046,f935,f930,f1054,f1050])).
% 1.28/0.56 thf(f1075,plain,(
% 1.28/0.56 ($false = $true) | (((n_some @ (diffprop @ sK2 @ sK3))) = $true) | ($false = ((iii @ sK3 @ sK2))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(superposition,[],[f937,f1013])).
% 1.28/0.56 thf(f1078,plain,(
% 1.28/0.56 (((n_some @ (diffprop @ sK2 @ sK3))) = $true) | ($false = ((iii @ sK3 @ sK2))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1075])).
% 1.28/0.56 thf(f1082,definition,(
% 1.28/0.56 spl5_15 <=> (((n_some @ (diffprop @ sK2 @ sK3))) = $true)),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_15])],[avatar_definition])).
% 1.28/0.56 thf(f1086,definition,(
% 1.28/0.56 spl5_16 <=> ($false = ((iii @ sK3 @ sK2)))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_16])],[avatar_definition])).
% 1.28/0.56 thf(f1088,plain,(
% 1.28/0.56 ($false = ((iii @ sK3 @ sK2))) | ~spl5_16),
% 1.28/0.56 inference(avatar_component_clause,[],[f1086])).
% 1.28/0.56 thf(f1092,plain,(
% 1.28/0.56 spl5_15 | spl5_16 | ~spl5_2 | ~spl5_3),
% 1.28/0.56 inference(avatar_split_clause,[],[f1078,f935,f930,f1086,f1082])).
% 1.28/0.56 thf(f1121,definition,(
% 1.28/0.56 spl5_19 <=> ($true = ((e_is @ nat @ sK3 @ sK2)))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_19])],[avatar_definition])).
% 1.28/0.56 thf(f1122,plain,(
% 1.28/0.56 ($true != ((e_is @ nat @ sK3 @ sK2))) | spl5_19),
% 1.28/0.56 inference(avatar_component_clause,[],[f1121])).
% 1.28/0.56 thf(f1123,plain,(
% 1.28/0.56 ($true = ((e_is @ nat @ sK3 @ sK2))) | ~spl5_19),
% 1.28/0.56 inference(avatar_component_clause,[],[f1121])).
% 1.28/0.56 thf(f1271,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($false = $true) | ($false = ((e_is @ nat @ X0 @ sK3))) | ($true = ((e_is @ nat @ sK3 @ X0))) | ($false = ((d_not @ (n_some @ (diffprop @ sK3 @ X0)))))) ) | ~spl5_3),
% 1.28/0.56 inference(superposition,[],[f937,f832])).
% 1.28/0.56 thf(f1274,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($false = ((e_is @ nat @ X0 @ sK3))) | ($true = ((e_is @ nat @ sK3 @ X0))) | ($false = ((d_not @ (n_some @ (diffprop @ sK3 @ X0)))))) ) | ~spl5_3),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1271])).
% 1.28/0.56 thf(f1284,plain,(
% 1.28/0.56 ($true = ((iii @ sK3 @ sK2))) | ($false = $true) | (((n_some @ (diffprop @ sK2 @ sK3))) = $false) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(superposition,[],[f932,f974])).
% 1.28/0.56 thf(f1290,plain,(
% 1.28/0.56 ($true = ((iii @ sK3 @ sK2))) | (((n_some @ (diffprop @ sK2 @ sK3))) = $false) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1284])).
% 1.28/0.56 thf(f1294,definition,(
% 1.28/0.56 spl5_27 <=> ($true = ((iii @ sK3 @ sK2)))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_27])],[avatar_definition])).
% 1.28/0.56 thf(f1296,plain,(
% 1.28/0.56 ($true = ((iii @ sK3 @ sK2))) | ~spl5_27),
% 1.28/0.56 inference(avatar_component_clause,[],[f1294])).
% 1.28/0.56 thf(f1298,definition,(
% 1.28/0.56 (((n_some @ (diffprop @ sK2 @ sK3))) != $false) | (((n_some @ (diffprop @ sK2 @ sK3))) != $true) | ($false = $true)),
% 1.28/0.56 introduced(theory,[theory_tautology_sat_conflict])).
% 1.28/0.56 thf(f1310,plain,(
% 1.28/0.56 ($false = ((iii @ sK2 @ sK3))) | ($false = $true) | ($true = ((n_some @ (diffprop @ sK3 @ sK2)))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(superposition,[],[f932,f1010])).
% 1.28/0.56 thf(f1312,plain,(
% 1.28/0.56 ($false = ((iii @ sK2 @ sK3))) | ($true = ((n_some @ (diffprop @ sK3 @ sK2)))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1310])).
% 1.28/0.56 thf(f1322,definition,(
% 1.28/0.56 spl5_28 <=> ($true = ((n_some @ (diffprop @ sK3 @ sK2))))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_28])],[avatar_definition])).
% 1.28/0.56 thf(f1324,plain,(
% 1.28/0.56 ($true = ((n_some @ (diffprop @ sK3 @ sK2)))) | ~spl5_28),
% 1.28/0.56 inference(avatar_component_clause,[],[f1322])).
% 1.28/0.56 thf(f1327,definition,(
% 1.28/0.56 spl5_29 <=> ($false = ((iii @ sK2 @ sK3)))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_29])],[avatar_definition])).
% 1.28/0.56 thf(f1329,plain,(
% 1.28/0.56 ($false = ((iii @ sK2 @ sK3))) | ~spl5_29),
% 1.28/0.56 inference(avatar_component_clause,[],[f1327])).
% 1.28/0.56 thf(f1331,plain,(
% 1.28/0.56 ($false = $true) | ($false = ((iii @ sK2 @ sK3))) | (~spl5_2 | ~spl5_3 | ~spl5_12)),
% 1.28/0.56 inference(forward_demodulation,[],[f1312,f1056])).
% 1.28/0.56 thf(f1332,plain,(
% 1.28/0.56 ($false = ((iii @ sK2 @ sK3))) | (~spl5_2 | ~spl5_3 | ~spl5_12)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1331])).
% 1.28/0.56 thf(f1333,plain,(
% 1.28/0.56 spl5_29 | ~spl5_2 | ~spl5_3 | ~spl5_12),
% 1.28/0.56 inference(avatar_split_clause,[],[f1332,f1054,f935,f930,f1327])).
% 1.28/0.56 thf(f1336,plain,(
% 1.28/0.56 spl5_28 | spl5_29 | ~spl5_2 | ~spl5_3),
% 1.28/0.56 inference(avatar_split_clause,[],[f1312,f935,f930,f1327,f1322])).
% 1.28/0.56 thf(f1432,plain,(
% 1.28/0.56 ($false = ((e_is @ nat @ sK2 @ sK3))) | ($false = $true) | ($true = ((e_is @ nat @ sK3 @ sK2))) | ($false = ((d_not @ (n_some @ (diffprop @ sK3 @ sK2))))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(superposition,[],[f1274,f932])).
% 1.28/0.56 thf(f1435,plain,(
% 1.28/0.56 ($false = $true) | ($true = ((e_is @ nat @ sK3 @ sK2))) | ($false = ((e_is @ nat @ sK2 @ sK3))) | ($false = ((d_not @ (n_some @ (diffprop @ sK3 @ sK2))))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(superposition,[],[f932,f1274])).
% 1.28/0.56 thf(f1438,plain,(
% 1.28/0.56 ($false = ((e_is @ nat @ sK2 @ sK3))) | ($true = ((e_is @ nat @ sK3 @ sK2))) | ($false = ((d_not @ (n_some @ (diffprop @ sK3 @ sK2))))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1432])).
% 1.28/0.56 thf(f1441,plain,(
% 1.28/0.56 ($true = ((e_is @ nat @ sK3 @ sK2))) | ($false = ((e_is @ nat @ sK2 @ sK3))) | ($false = ((d_not @ (n_some @ (diffprop @ sK3 @ sK2))))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1435])).
% 1.28/0.56 thf(f1518,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = $true) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($true = ((d_not @ (iii @ X0 @ sK2)))) | ($false = ((e_is @ nat @ X0 @ sK2)))) ) | ~spl5_2),
% 1.28/0.56 inference(superposition,[],[f779,f932])).
% 1.28/0.56 thf(f1525,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | ($false = ((e_is @ nat @ X0 @ sK2))) | ($true = ((d_not @ (iii @ X0 @ sK2))))) ) | ~spl5_2),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1518])).
% 1.28/0.56 thf(f1531,plain,(
% 1.28/0.56 ($false = ((e_is @ nat @ sK3 @ sK2))) | ($true = ((d_not @ (iii @ sK3 @ sK2)))) | ($false = $true) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(superposition,[],[f1525,f937])).
% 1.28/0.56 thf(f1534,plain,(
% 1.28/0.56 ($false = ((e_is @ nat @ sK3 @ sK2))) | ($false = $true) | ($true = ((d_not @ (iii @ sK3 @ sK2)))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(superposition,[],[f937,f1525])).
% 1.28/0.56 thf(f1536,plain,(
% 1.28/0.56 ($false = ((e_is @ nat @ sK3 @ sK2))) | ($true = ((d_not @ (iii @ sK3 @ sK2)))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1531])).
% 1.28/0.56 thf(f1538,plain,(
% 1.28/0.56 ($true = ((d_not @ (iii @ sK3 @ sK2)))) | ($false = ((e_is @ nat @ sK3 @ sK2))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1534])).
% 1.28/0.56 thf(f1543,plain,(
% 1.28/0.56 ($false = $true) | ($true = ((d_not @ (iii @ sK3 @ sK2)))) | (~spl5_2 | ~spl5_3 | ~spl5_19)),
% 1.28/0.56 inference(forward_demodulation,[],[f1538,f1123])).
% 1.28/0.56 thf(f1544,plain,(
% 1.28/0.56 ($true = ((d_not @ (iii @ sK3 @ sK2)))) | (~spl5_2 | ~spl5_3 | ~spl5_19)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1543])).
% 1.28/0.56 thf(f1551,plain,(
% 1.28/0.56 (((d_not @ $false)) = $true) | (~spl5_2 | ~spl5_3 | ~spl5_16 | ~spl5_19)),
% 1.28/0.56 inference(forward_demodulation,[],[f1544,f1088])).
% 1.28/0.56 thf(f1560,plain,(
% 1.28/0.56 ($false = $true) | (~spl5_2 | ~spl5_3 | ~spl5_10 | ~spl5_16 | ~spl5_19)),
% 1.28/0.56 inference(forward_demodulation,[],[f1551,f1022])).
% 1.28/0.56 thf(f1561,plain,(
% 1.28/0.56 $false | (~spl5_2 | ~spl5_3 | ~spl5_10 | ~spl5_16 | ~spl5_19)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1560])).
% 1.28/0.56 thf(f1562,plain,(
% 1.28/0.56 ~spl5_2 | ~spl5_3 | ~spl5_10 | ~spl5_16 | ~spl5_19),
% 1.28/0.56 inference(avatar_contradiction_clause,[],[f1561])).
% 1.28/0.56 thf(f1570,definition,(
% 1.28/0.56 spl5_34 <=> (((d_not @ $false)) = $true)),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_34])],[avatar_definition])).
% 1.28/0.56 thf(f1577,plain,(
% 1.28/0.56 ($false = $true) | ($true = ((d_not @ (iii @ sK3 @ sK2)))) | (~spl5_2 | ~spl5_3 | ~spl5_19)),
% 1.28/0.56 inference(forward_demodulation,[],[f1536,f1123])).
% 1.28/0.56 thf(f1578,plain,(
% 1.28/0.56 ($true = ((d_not @ (iii @ sK3 @ sK2)))) | (~spl5_2 | ~spl5_3 | ~spl5_19)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1577])).
% 1.28/0.56 thf(f1582,plain,(
% 1.28/0.56 ($true = ((d_not @ $true))) | (~spl5_2 | ~spl5_3 | ~spl5_19 | ~spl5_27)),
% 1.28/0.56 inference(forward_demodulation,[],[f1578,f1296])).
% 1.28/0.56 thf(f1583,plain,(
% 1.28/0.56 ($false = $true) | (~spl5_2 | ~spl5_3 | ~spl5_9 | ~spl5_19 | ~spl5_27)),
% 1.28/0.56 inference(forward_demodulation,[],[f1582,f1002])).
% 1.28/0.56 thf(f1584,plain,(
% 1.28/0.56 $false | (~spl5_2 | ~spl5_3 | ~spl5_9 | ~spl5_19 | ~spl5_27)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1583])).
% 1.28/0.56 thf(f1585,plain,(
% 1.28/0.56 ~spl5_2 | ~spl5_3 | ~spl5_9 | ~spl5_19 | ~spl5_27),
% 1.28/0.56 inference(avatar_contradiction_clause,[],[f1584])).
% 1.28/0.56 thf(f1587,plain,(
% 1.28/0.56 ($false = ((d_not @ $true))) | ($true = ((e_is @ nat @ sK3 @ sK2))) | ($false = ((e_is @ nat @ sK2 @ sK3))) | (~spl5_2 | ~spl5_3 | ~spl5_28)),
% 1.28/0.56 inference(forward_demodulation,[],[f1438,f1324])).
% 1.28/0.56 thf(f1643,plain,(
% 1.28/0.56 spl5_8 | spl5_27 | ~spl5_2 | ~spl5_3),
% 1.28/0.56 inference(avatar_split_clause,[],[f1290,f935,f930,f1294,f996])).
% 1.28/0.56 thf(f1661,plain,(
% 1.28/0.56 ($false = ((d_not @ $true))) | ($false = ((e_is @ nat @ sK2 @ sK3))) | (~spl5_2 | ~spl5_3 | spl5_19 | ~spl5_28)),
% 1.28/0.56 inference(forward_subsumption_resolution,[],[f1587,f1122])).
% 1.28/0.56 thf(f1672,plain,(
% 1.28/0.56 ($false = ((e_is @ nat @ sK2 @ sK3))) | (~spl5_2 | ~spl5_3 | spl5_9 | spl5_19 | ~spl5_28)),
% 1.28/0.56 inference(forward_subsumption_resolution,[],[f1661,f1001])).
% 1.28/0.56 thf(f1676,definition,(
% 1.28/0.56 spl5_38 <=> ($false = ((e_is @ nat @ sK2 @ sK3)))),
% 1.28/0.56 introduced(definition,[new_symbols(definition,[spl5_38])],[avatar_definition])).
% 1.28/0.56 thf(f1679,plain,(
% 1.28/0.56 spl5_38 | ~spl5_2 | ~spl5_3 | spl5_9 | spl5_19 | ~spl5_28),
% 1.28/0.56 inference(avatar_split_clause,[],[f1672,f1322,f1121,f1000,f935,f930,f1676])).
% 1.28/0.56 thf(f1746,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($true = ((d_not @ (n_some @ (diffprop @ X0 @ sK3))))) | ($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((d_not @ (iii @ X0 @ sK3))) = $true) | ($false = $true)) ) | ~spl5_3),
% 1.28/0.56 inference(superposition,[],[f937,f780])).
% 1.28/0.56 thf(f1750,plain,(
% 1.28/0.56 ( ! [X0 : $i] : (($false = ((is_of @ X0 @ (^[Y0 : $i]: (in @ Y0 @ nat))))) | (((d_not @ (iii @ X0 @ sK3))) = $true) | ($true = ((d_not @ (n_some @ (diffprop @ X0 @ sK3)))))) ) | ~spl5_3),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1746])).
% 1.28/0.56 thf(f1882,plain,(
% 1.28/0.56 (((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))) = $true) | ($true = ((d_not @ (iii @ sK2 @ sK3)))) | ($false = $true) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(superposition,[],[f1750,f932])).
% 1.28/0.56 thf(f1885,plain,(
% 1.28/0.56 ($true = ((d_not @ (iii @ sK2 @ sK3)))) | (((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))) = $true) | ($false = $true) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(superposition,[],[f932,f1750])).
% 1.28/0.56 thf(f1888,plain,(
% 1.28/0.56 ($true = ((d_not @ (iii @ sK2 @ sK3)))) | (((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))) = $true) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1882])).
% 1.28/0.56 thf(f1890,plain,(
% 1.28/0.56 (((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))) = $true) | ($true = ((d_not @ (iii @ sK2 @ sK3)))) | (~spl5_2 | ~spl5_3)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1885])).
% 1.28/0.56 thf(f1895,plain,(
% 1.28/0.56 (((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))) = $true) | ($true = ((d_not @ $true))) | (~spl5_2 | ~spl5_3 | ~spl5_11)),
% 1.28/0.56 inference(forward_demodulation,[],[f1890,f1052])).
% 1.28/0.56 thf(f1902,plain,(
% 1.28/0.56 ($false = $true) | ($true = ((d_not @ $true))) | (~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_11)),
% 1.28/0.56 inference(forward_demodulation,[],[f1895,f951])).
% 1.28/0.56 thf(f1903,plain,(
% 1.28/0.56 ($true = ((d_not @ $true))) | (~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_11)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1902])).
% 1.28/0.56 thf(f1909,plain,(
% 1.28/0.56 ($false = $true) | (~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_9 | ~spl5_11)),
% 1.28/0.56 inference(forward_demodulation,[],[f1903,f1002])).
% 1.28/0.56 thf(f1910,plain,(
% 1.28/0.56 $false | (~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_9 | ~spl5_11)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1909])).
% 1.28/0.56 thf(f1911,plain,(
% 1.28/0.56 ~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_9 | ~spl5_11),
% 1.28/0.56 inference(avatar_contradiction_clause,[],[f1910])).
% 1.28/0.56 thf(f1932,plain,(
% 1.28/0.56 ($false = $true) | ($true = ((d_not @ (iii @ sK2 @ sK3)))) | (~spl5_2 | ~spl5_3 | ~spl5_6)),
% 1.28/0.56 inference(forward_demodulation,[],[f1890,f951])).
% 1.28/0.56 thf(f1933,plain,(
% 1.28/0.56 ($true = ((d_not @ (iii @ sK2 @ sK3)))) | (~spl5_2 | ~spl5_3 | ~spl5_6)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1932])).
% 1.28/0.56 thf(f1943,plain,(
% 1.28/0.56 (((d_not @ (n_some @ (diffprop @ sK2 @ sK3)))) = $true) | (((d_not @ $false)) = $true) | (~spl5_2 | ~spl5_3 | ~spl5_29)),
% 1.28/0.56 inference(forward_demodulation,[],[f1888,f1329])).
% 1.28/0.56 thf(f1948,plain,(
% 1.28/0.56 (((d_not @ $false)) = $true) | (~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_29)),
% 1.28/0.56 inference(forward_demodulation,[],[f1933,f1329])).
% 1.28/0.56 thf(f1954,plain,(
% 1.28/0.56 ($false = $true) | (((d_not @ $false)) = $true) | (~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_29)),
% 1.28/0.56 inference(forward_demodulation,[],[f1943,f951])).
% 1.28/0.56 thf(f1955,plain,(
% 1.28/0.56 (((d_not @ $false)) = $true) | (~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_29)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1954])).
% 1.28/0.56 thf(f1965,plain,(
% 1.28/0.56 ($false = $true) | (~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_10 | ~spl5_29)),
% 1.28/0.56 inference(forward_demodulation,[],[f1955,f1022])).
% 1.28/0.56 thf(f1966,plain,(
% 1.28/0.56 $false | (~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_10 | ~spl5_29)),
% 1.28/0.56 inference(trivial_inequality_removal,[],[f1965])).
% 1.28/0.56 thf(f1967,plain,(
% 1.28/0.56 ~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_10 | ~spl5_29),
% 1.28/0.56 inference(avatar_contradiction_clause,[],[f1966])).
% 1.28/0.56 thf(f1969,definition,(
% 1.28/0.56 ($true != ((iii @ sK2 @ sK3))) | ($false != ((d_not @ (iii @ sK2 @ sK3)))) | ($false = ((d_not @ $true)))),
% 1.28/0.56 introduced(theory,[theory_tautology_sat_conflict])).
% 1.28/0.56 thf(f1972,definition,(
% 1.28/0.56 ($false != ((e_is @ nat @ sK2 @ sK3))) | ($true != ((e_is @ nat @ sK2 @ sK3))) | ($false = $true)),
% 1.28/0.56 introduced(theory,[theory_tautology_sat_conflict])).
% 1.28/0.56 thf(f2023,plain,(
% 1.28/0.56 ($false = ((d_not @ (n_some @ (diffprop @ sK3 @ sK2))))) | ($false = ((e_is @ nat @ sK2 @ sK3))) | (~spl5_2 | ~spl5_3 | spl5_19)),
% 1.28/0.56 inference(forward_subsumption_resolution,[],[f1441,f1122])).
% 1.28/0.56 thf(f2027,plain,(
% 1.28/0.56 spl5_34 | ~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_29),
% 1.28/0.56 inference(avatar_split_clause,[],[f1948,f1327,f949,f935,f930,f1570])).
% 1.28/0.56 thf(f2042,plain,(
% 1.28/0.56 ($false = ((e_is @ nat @ sK2 @ sK3))) | ($false = ((d_not @ $false))) | (~spl5_2 | ~spl5_3 | ~spl5_12 | spl5_19)),
% 1.28/0.56 inference(forward_demodulation,[],[f2023,f1056])).
% 1.28/0.56 thf(f2053,plain,(
% 1.28/0.56 ($false = ((e_is @ nat @ sK2 @ sK3))) | (~spl5_2 | ~spl5_3 | spl5_10 | ~spl5_12 | spl5_19)),
% 1.28/0.56 inference(forward_subsumption_resolution,[],[f2042,f1021])).
% 1.28/0.56 thf(f2057,plain,(
% 1.28/0.56 spl5_38 | ~spl5_2 | ~spl5_3 | spl5_10 | ~spl5_12 | spl5_19),
% 1.28/0.56 inference(avatar_split_clause,[],[f2053,f1121,f1054,f1020,f935,f930,f1676])).
% 1.28/0.56 thf(f2059,definition,(
% 1.28/0.56 ($false != ((iii @ sK2 @ sK3))) | (((d_not @ $false)) != $true) | ($false != ((d_not @ (iii @ sK2 @ sK3)))) | ($false = $true)),
% 1.28/0.56 introduced(theory,[theory_tautology_sat_conflict])).
% 1.28/0.56 cnf(s2, plain, spl5_2, inference(sat_conversion,[],[f933])).
% 1.28/0.56 cnf(s3, plain, spl5_3, inference(sat_conversion,[],[f938])).
% 1.28/0.56 cnf(s4, plain, spl5_4 | spl5_5, inference(sat_conversion,[],[f947])).
% 1.28/0.56 cnf(s5, plain, spl5_6, inference(sat_conversion,[],[f952])).
% 1.28/0.56 cnf(s6, plain, ~spl5_7, inference(sat_conversion,[],[f957])).
% 1.28/0.56 cnf(s7, plain, ~spl5_6 | spl5_8 | spl5_9, inference(sat_conversion,[],[f1003])).
% 1.28/0.56 cnf(s8, plain, ~spl5_6 | ~spl5_8 | spl5_10, inference(sat_conversion,[],[f1023])).
% 1.28/0.56 cnf(s11, plain, ~spl5_2 | ~spl5_3 | spl5_11 | spl5_12, inference(sat_conversion,[],[f1067])).
% 1.28/0.56 cnf(s14, plain, ~spl5_2 | ~spl5_3 | spl5_15 | spl5_16, inference(sat_conversion,[],[f1092])).
% 1.28/0.56 cnf(s36, plain, spl5_7 | ~spl5_8 | ~spl5_15, inference(sat_conversion,[],[f1298])).
% 1.28/0.56 cnf(s40, plain, ~spl5_2 | ~spl5_3 | ~spl5_12 | spl5_29, inference(sat_conversion,[],[f1333])).
% 1.28/0.56 cnf(s41, plain, ~spl5_2 | ~spl5_3 | spl5_28 | spl5_29, inference(sat_conversion,[],[f1336])).
% 1.28/0.56 cnf(s50, plain, ~spl5_2 | ~spl5_3 | ~spl5_10 | ~spl5_16 | ~spl5_19, inference(sat_conversion,[],[f1562])).
% 1.28/0.56 cnf(s55, plain, ~spl5_2 | ~spl5_3 | ~spl5_9 | ~spl5_19 | ~spl5_27, inference(sat_conversion,[],[f1585])).
% 1.28/0.56 cnf(s63, plain, ~spl5_2 | ~spl5_3 | spl5_8 | spl5_27, inference(sat_conversion,[],[f1643])).
% 1.28/0.56 cnf(s69, plain, ~spl5_2 | ~spl5_3 | spl5_9 | spl5_19 | ~spl5_28 | spl5_38, inference(sat_conversion,[],[f1679])).
% 1.28/0.56 cnf(s108, plain, ~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_9 | ~spl5_11, inference(sat_conversion,[],[f1911])).
% 1.28/0.56 cnf(s118, plain, ~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_10 | ~spl5_29, inference(sat_conversion,[],[f1967])).
% 1.28/0.56 cnf(s120, plain, ~spl5_4 | spl5_9 | ~spl5_11, inference(sat_conversion,[],[f1969])).
% 1.28/0.56 cnf(s123, plain, ~spl5_5 | spl5_7 | ~spl5_38, inference(sat_conversion,[],[f1972])).
% 1.28/0.56 cnf(s155, plain, ~spl5_2 | ~spl5_3 | ~spl5_6 | ~spl5_29 | spl5_34, inference(sat_conversion,[],[f2027])).
% 1.28/0.56 cnf(s169, plain, ~spl5_2 | ~spl5_3 | spl5_10 | ~spl5_12 | spl5_19 | spl5_38, inference(sat_conversion,[],[f2057])).
% 1.28/0.56 cnf(s173, plain, ~spl5_4 | spl5_7 | ~spl5_29 | ~spl5_34, inference(sat_conversion,[],[f2059])).
% 1.28/0.56 cnf(s184, plain, spl5_8 | spl5_38, inference(rat,[],[s118,s169,s40,s11,s55,s108,s63,s7,s5,s3,s2])).
% 1.28/0.56 cnf(s185, plain, spl5_38, inference(rat,[],[s108,s11,s69,s40,s41,s50,s118,s14,s8,s36,s184,s5,s3,s2,s6])).
% 1.28/0.56 cnf(s186, plain, ~spl5_5, inference(rat,[],[s123,s6,s185])).
% 1.28/0.56 cnf(s187, plain, spl5_4, inference(rat,[],[s4,s186])).
% 1.28/0.56 cnf(s189, plain, ~spl5_29, inference(rat,[],[s155,s173,s5,s3,s2,s6,s187])).
% 1.28/0.56 cnf(s191, plain, ~spl5_12, inference(rat,[],[s40,s2,s3,s189])).
% 1.28/0.56 cnf(s192, plain, spl5_11, inference(rat,[],[s11,s2,s3,s191])).
% 1.28/0.56 cnf(s193, plain, ~spl5_9, inference(rat,[],[s108,s2,s3,s5,s192])).
% 1.28/0.56 cnf(s194, plain, $false, inference(rat,[],[s120,s187,s193,s192])).
% 1.28/0.56 thf(f2070,plain,(
% 1.28/0.56 $false),
% 1.28/0.56 inference(avatar_sat_refutation,[],[s194])).
% 1.28/0.56 % SZS output end Proof for theBenchmark
% 1.28/0.56 % (985945)------------------------------
% 1.28/0.56 % (985945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.28/0.56 % (985945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.28/0.56 % (985945)CaDiCaL version: 2.1.3
% 1.28/0.56 % (985945)Termination reason: Refutation
% 1.28/0.56 % (985945)Time elapsed: 0.077 s
% 1.28/0.56 % (985945)Peak memory usage: 14 MB
% 1.28/0.56 % (985945)Instructions burned: 156 (million)
% 1.28/0.56 % (985818)Success in time 0.289 s
% 1.28/0.56 % Vampire exiting
%------------------------------------------------------------------------------