%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP006^1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:07:38 AM UTC 2026
% Result : Theorem 0.55s 0.28s
% Output : Refutation 0.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ITP006^1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.12 % Computer : n012.cluster.edu
% 0.06/0.12 % Model : x86_64 x86_64
% 0.06/0.12 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.12 % Memory : 8046.5625MB
% 0.06/0.12 % OS : Linux 6.8.0-71-generic
% 0.06/0.12 % CPULimit : 300
% 0.06/0.12 % WCLimit : 300
% 0.06/0.12 % DateTime : Tue Sep 29 19:22:24 UTC 2026
% 0.06/0.12 % CPUTime :
% 0.06/0.12 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.13 Running higher-order theorem proving
% 0.06/0.15 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.55/0.25 % (556915)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.55/0.25 % (556937)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.55/0.25 % (556937)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.55/0.25 % (556935)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1856315940:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.55/0.25 % (556933)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3467224004:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.55/0.25 % (556931)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1294317817:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.55/0.25 % (556936)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=279051226:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.55/0.25 % (556932)lrs+10_16_si=on:nwc=1.5:random_seed=1471212260:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.55/0.25 % (556937)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=1035396950:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.55/0.25 % (556934)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=3408827909:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.55/0.25 % (556933)Instruction limit reached!
% 0.55/0.25 % (556933)------------------------------
% 0.55/0.25 % (556933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.25 % (556933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.25 % (556933)CaDiCaL version: 2.1.3
% 0.55/0.25 % (556933)Termination reason: Instruction limit
% 0.55/0.25 % (556933)Termination phase: shuffling
% 0.55/0.25 % (556933)Time elapsed: 0.001 s
% 0.55/0.25 % (556933)Peak memory usage: 10 MB
% 0.55/0.25 % (556933)Instructions burned: 6 (million)
% 0.55/0.25 % (556932)Instruction limit reached!
% 0.55/0.25 % (556932)------------------------------
% 0.55/0.25 % (556932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.25 % (556932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.25 % (556932)CaDiCaL version: 2.1.3
% 0.55/0.25 % (556932)Termination reason: Instruction limit
% 0.55/0.25 % (556932)Termination phase: Property scanning
% 0.55/0.25 % (556932)Time elapsed: 0.004 s
% 0.55/0.25 % (556932)Peak memory usage: 10 MB
% 0.55/0.25 % (556932)Instructions burned: 19 (million)
% 0.55/0.25 % (556935)Instruction limit reached!
% 0.55/0.25 % (556935)------------------------------
% 0.55/0.25 % (556935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.25 % (556935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.25 % (556935)CaDiCaL version: 2.1.3
% 0.55/0.25 % (556935)Termination reason: Instruction limit
% 0.55/0.25 % (556935)Termination phase: Property scanning
% 0.55/0.25 % (556935)Time elapsed: 0.005 s
% 0.55/0.25 % (556935)Peak memory usage: 10 MB
% 0.55/0.25 % (556935)Instructions burned: 24 (million)
% 0.55/0.25 % (556949)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4270921622:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.55/0.25 % (556949)Instruction limit reached!
% 0.55/0.25 % (556949)------------------------------
% 0.55/0.25 % (556949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.25 % (556949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.25 % (556949)CaDiCaL version: 2.1.3
% 0.55/0.25 % (556949)Termination reason: Instruction limit
% 0.55/0.25 % (556949)Termination phase: Property scanning
% 0.55/0.25 % (556949)Time elapsed: 0.001 s
% 0.55/0.25 % (556949)Peak memory usage: 10 MB
% 0.55/0.25 % (556949)Instructions burned: 5 (million)
% 0.55/0.25 % (556953)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.55/0.25 % (556952)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1659178695:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.55/0.28 % (556953)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2401302035:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.55/0.28 % (556952)Instruction limit reached!
% 0.55/0.28 % (556952)------------------------------
% 0.55/0.28 % (556952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556952)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556952)Termination reason: Instruction limit
% 0.55/0.28 % (556952)Termination phase: Property scanning
% 0.55/0.28 % (556952)Time elapsed: 0.001 s
% 0.55/0.28 % (556952)Peak memory usage: 10 MB
% 0.55/0.28 % (556952)Instructions burned: 7 (million)
% 0.55/0.28 % (556953)Instruction limit reached!
% 0.55/0.28 % (556953)------------------------------
% 0.55/0.28 % (556953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556953)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556953)Termination reason: Instruction limit
% 0.55/0.28 % (556953)Termination phase: shuffling
% 0.55/0.28 % (556953)Time elapsed: 0.002 s
% 0.55/0.28 % (556953)Peak memory usage: 10 MB
% 0.55/0.28 % (556953)Instructions burned: 10 (million)
% 0.55/0.28 % (556936)Instruction limit reached!
% 0.55/0.28 % (556936)------------------------------
% 0.55/0.28 % (556936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556936)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556936)Termination reason: Instruction limit
% 0.55/0.28 % (556936)Termination phase: Saturation
% 0.55/0.28 % (556936)Time elapsed: 0.018 s
% 0.55/0.28 % (556936)Peak memory usage: 13 MB
% 0.55/0.28 % (556936)Instructions burned: 75 (million)
% 0.55/0.28 % (556931)Instruction limit reached!
% 0.55/0.28 % (556931)------------------------------
% 0.55/0.28 % (556931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556931)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556931)Termination reason: Instruction limit
% 0.55/0.28 % (556931)Termination phase: Saturation
% 0.55/0.28 % (556931)Time elapsed: 0.023 s
% 0.55/0.28 % (556931)Peak memory usage: 13 MB
% 0.55/0.28 % (556931)Instructions burned: 89 (million)
% 0.55/0.28 % (556955)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=482073235:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.55/0.28 % (556958)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.55/0.28 % (556958)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.55/0.28 % (556958)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1858645092:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.55/0.28 % (556955)Instruction limit reached!
% 0.55/0.28 % (556955)------------------------------
% 0.55/0.28 % (556955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556955)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556955)Termination reason: Instruction limit
% 0.55/0.28 % (556955)Termination phase: Naming
% 0.55/0.28 % (556955)Time elapsed: 0.006 s
% 0.55/0.28 % (556955)Peak memory usage: 10 MB
% 0.55/0.28 % (556955)Instructions burned: 13 (million)
% 0.55/0.28 % (556963)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=2804609865:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.55/0.28 % (556964)lrs+10_1_si=on:cs=on:random_seed=3193275702:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.55/0.28 % (556964)Instruction limit reached!
% 0.55/0.28 % (556964)------------------------------
% 0.55/0.28 % (556964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556964)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556964)Termination reason: Instruction limit
% 0.55/0.28 % (556964)Termination phase: Property scanning
% 0.55/0.28 % (556964)Time elapsed: 0.003 s
% 0.55/0.28 % (556964)Peak memory usage: 10 MB
% 0.55/0.28 % (556964)Instructions burned: 8 (million)
% 0.55/0.28 % (556958)Instruction limit reached!
% 0.55/0.28 % (556958)------------------------------
% 0.55/0.28 % (556958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556958)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556958)Termination reason: Instruction limit
% 0.55/0.28 % (556958)Termination phase: Function definition elimination
% 0.55/0.28 % (556958)Time elapsed: 0.012 s
% 0.55/0.28 % (556958)Peak memory usage: 10 MB
% 0.55/0.28 % (556958)Instructions burned: 30 (million)
% 0.55/0.28 % (556966)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.55/0.28 % (556966)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=550799154:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.55/0.28 % (556979)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2148511192:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.55/0.28 % (556966)Instruction limit reached!
% 0.55/0.28 % (556966)------------------------------
% 0.55/0.28 % (556966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556966)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556966)Termination reason: Instruction limit
% 0.55/0.28 % (556966)Termination phase: shuffling
% 0.55/0.28 % (556966)Time elapsed: 0.002 s
% 0.55/0.28 % (556966)Peak memory usage: 10 MB
% 0.55/0.28 % (556966)Instructions burned: 4 (million)
% 0.55/0.28 % (556978)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4202444953:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.55/0.28 % (556978)Refutation not found, incomplete strategy
% 0.55/0.28 % (556978)------------------------------
% 0.55/0.28 % (556978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556978)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556978)Termination reason: Refutation not found, incomplete strategy
% 0.55/0.28 % (556978)Time elapsed: 0.005 s
% 0.55/0.28 % (556978)Peak memory usage: 12 MB
% 0.55/0.28 % (556978)Instructions burned: 15 (million)
% 0.55/0.28 % (556978)------------------------------
% 0.55/0.28 % (556978)------------------------------
% 0.55/0.28 % (556937)Instruction limit reached!
% 0.55/0.28 % (556937)------------------------------
% 0.55/0.28 % (556937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556937)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556937)Termination reason: Instruction limit
% 0.55/0.28 % (556937)Termination phase: Saturation
% 0.55/0.28 % (556937)Time elapsed: 0.058 s
% 0.55/0.28 % (556937)Peak memory usage: 13 MB
% 0.55/0.28 % (556937)Instructions burned: 157 (million)
% 0.55/0.28 % (556982)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2577873336:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.55/0.28 % (556992)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=4148193673:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.55/0.28 % (556963)Instruction limit reached!
% 0.55/0.28 % (556963)------------------------------
% 0.55/0.28 % (556963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556963)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556963)Termination reason: Instruction limit
% 0.55/0.28 % (556963)Termination phase: Saturation
% 0.55/0.28 % (556963)Time elapsed: 0.039 s
% 0.55/0.28 % (556963)Peak memory usage: 13 MB
% 0.55/0.28 % (556963)Instructions burned: 86 (million)
% 0.55/0.28 % (556996)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=612397317:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 0.55/0.28 % (556982)Instruction limit reached!
% 0.55/0.28 % (556982)------------------------------
% 0.55/0.28 % (556982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556982)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556982)Termination reason: Instruction limit
% 0.55/0.28 % (556982)Termination phase: Property scanning
% 0.55/0.28 % (556982)Time elapsed: 0.011 s
% 0.55/0.28 % (556982)Peak memory usage: 11 MB
% 0.55/0.28 % (556982)Instructions burned: 26 (million)
% 0.55/0.28 % (556995)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2496044361:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.55/0.28 % (556992)Instruction limit reached!
% 0.55/0.28 % (556992)------------------------------
% 0.55/0.28 % (556992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556992)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556992)Termination reason: Instruction limit
% 0.55/0.28 % (556992)Termination phase: Preprocessing 3
% 0.55/0.28 % (556992)Time elapsed: 0.007 s
% 0.55/0.28 % (556992)Peak memory usage: 10 MB
% 0.55/0.28 % (556992)Instructions burned: 15 (million)
% 0.55/0.28 % (556996)Instruction limit reached!
% 0.55/0.28 % (556996)------------------------------
% 0.55/0.28 % (556996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556996)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556996)Termination reason: Instruction limit
% 0.55/0.28 % (556996)Termination phase: Preprocessing 3
% 0.55/0.28 % (556996)Time elapsed: 0.006 s
% 0.55/0.28 % (556996)Peak memory usage: 10 MB
% 0.55/0.28 % (556996)Instructions burned: 15 (million)
% 0.55/0.28 % (557006)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3560493373:i=26:ep=R:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/26Mi)
% 0.55/0.28 % (557005)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=4041661751:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.55/0.28 % (557006)Instruction limit reached!
% 0.55/0.28 % (557006)------------------------------
% 0.55/0.28 % (557006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (557006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (557006)CaDiCaL version: 2.1.3
% 0.55/0.28 % (557006)Termination reason: Instruction limit
% 0.55/0.28 % (557006)Termination phase: Property scanning
% 0.55/0.28 % (557006)Time elapsed: 0.006 s
% 0.55/0.28 % (557006)Peak memory usage: 10 MB
% 0.55/0.28 % (557006)Instructions burned: 28 (million)
% 0.55/0.28 % (557005)Instruction limit reached!
% 0.55/0.28 % (557005)------------------------------
% 0.55/0.28 % (557005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (557005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (557005)CaDiCaL version: 2.1.3
% 0.55/0.28 % (557005)Termination reason: Instruction limit
% 0.55/0.28 % (557005)Termination phase: Property scanning
% 0.55/0.28 % (557005)Time elapsed: 0.002 s
% 0.55/0.28 % (557005)Peak memory usage: 10 MB
% 0.55/0.28 % (557005)Instructions burned: 4 (million)
% 0.55/0.28 % (557010)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3734595996:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/23Mi)
% 0.55/0.28 % (556979) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-556915-556979"...
% 0.55/0.28 % (557011)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2068233514:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.55/0.28 % (557019)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
% 0.55/0.28 % (557019)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.55/0.28 % (556979)...printing done.
% 0.55/0.28 % (556979)Refutation found. Thanks to Tanya!
% 0.55/0.28 % SZS status Theorem for theBenchmark
% 0.55/0.28 % SZS output start Proof for theBenchmark
% 0.55/0.28 thf(type_def_5, type, u: $tType).
% 0.55/0.28 thf(type_def_6, type, d: $tType).
% 0.55/0.28 thf(type_def_7, type, du: $tType).
% 0.55/0.28 thf(type_def_8, type, sTfun: ($tType * $tType) > $tType).
% 0.55/0.28 thf(func_def_0, type, tyop_2Emin_2Ebool: d).
% 0.55/0.28 thf(func_def_1, type, tyop_2Emin_2Efun: (d > d > d)).
% 0.55/0.28 thf(func_def_2, type, s: (d > u > du)).
% 0.55/0.28 thf(func_def_3, type, app_2E2: (du > du > u)).
% 0.55/0.28 thf(func_def_4, type, combin_i_2E0: u).
% 0.55/0.28 thf(func_def_5, type, combin_k_2E0: u).
% 0.55/0.28 thf(func_def_6, type, combin_s_2E0: u).
% 0.55/0.28 thf(func_def_7, type, c_2Ebool_2E_21_2E0: u).
% 0.55/0.28 thf(func_def_8, type, c_2Ebool_2E_21_2E1: (du > u)).
% 0.55/0.28 thf(func_def_9, type, c_2Ebool_2E_2F_5C_2E0: u).
% 0.55/0.28 thf(func_def_10, type, c_2Ebool_2E_2F_5C_2E2: (du > du > u)).
% 0.55/0.28 thf(func_def_11, type, c_2Emin_2E_3D_2E0: u).
% 0.55/0.28 thf(func_def_12, type, c_2Emin_2E_3D_2E2: (du > du > u)).
% 0.55/0.28 thf(func_def_13, type, c_2Emin_2E_3D_3D_3E_2E0: u).
% 0.55/0.28 thf(func_def_14, type, c_2Emin_2E_3D_3D_3E_2E2: (du > du > u)).
% 0.55/0.28 thf(func_def_15, type, c_2Ebool_2E_3F_2E0: u).
% 0.55/0.28 thf(func_def_16, type, c_2Ebool_2E_3F_2E1: (du > u)).
% 0.55/0.28 thf(func_def_17, type, c_2Ebool_2EF_2E0: u).
% 0.55/0.28 thf(func_def_18, type, c_2EquantHeuristics_2EGUESS__EXISTS_2E0: u).
% 0.55/0.28 thf(func_def_19, type, c_2EquantHeuristics_2EGUESS__EXISTS_2E2: (du > du > u)).
% 0.55/0.28 thf(func_def_20, type, c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E0: u).
% 0.55/0.28 thf(func_def_21, type, c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2: (du > du > u)).
% 0.55/0.28 thf(func_def_22, type, c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E0: u).
% 0.55/0.28 thf(func_def_23, type, c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2: (du > du > u)).
% 0.55/0.28 thf(func_def_24, type, c_2EquantHeuristics_2EGUESS__FORALL_2E0: u).
% 0.55/0.28 thf(func_def_25, type, c_2EquantHeuristics_2EGUESS__FORALL_2E2: (du > du > u)).
% 0.55/0.28 thf(func_def_26, type, c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E0: u).
% 0.55/0.28 thf(func_def_27, type, c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2: (du > du > u)).
% 0.55/0.28 thf(func_def_28, type, c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0: u).
% 0.55/0.28 thf(func_def_29, type, c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2: (du > du > u)).
% 0.55/0.28 thf(func_def_30, type, c_2Ebool_2ET_2E0: u).
% 0.55/0.28 thf(func_def_31, type, c_2Ebool_2E_5C_2F_2E0: u).
% 0.55/0.28 thf(func_def_32, type, c_2Ebool_2E_5C_2F_2E2: (du > du > u)).
% 0.55/0.28 thf(func_def_33, type, c_2Ebool_2E_7E_2E0: u).
% 0.55/0.28 thf(func_def_34, type, c_2Ebool_2E_7E_2E1: (du > u)).
% 0.55/0.28 thf(func_def_35, type, mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool: (($o > $o) > $o > $o)).
% 0.55/0.28 thf(func_def_36, type, mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: (($o > $o > $o) > $o > $o > $o)).
% 0.55/0.28 thf(func_def_37, type, mono_2Ec_2Ebool_2E_2F_5C: ($o > $o > $o)).
% 0.55/0.28 thf(func_def_38, type, mono_2Ec_2Emin_2E_3D_3D_3E: ($o > $o > $o)).
% 0.55/0.28 thf(func_def_39, type, mono_2Ec_2Ebool_2EF: $o).
% 0.55/0.28 thf(func_def_40, type, mono_2Ec_2Ebool_2ET: $o).
% 0.55/0.28 thf(func_def_41, type, mono_2Ec_2Ebool_2E_5C_2F: ($o > $o > $o)).
% 0.55/0.28 thf(func_def_42, type, mono_2Ec_2Ebool_2E_7E: ($o > $o)).
% 0.55/0.28 thf(func_def_43, type, i_mono_2Etyop_2Emin_2Ebool: ($o > u)).
% 0.55/0.28 thf(func_def_44, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: (($o > $o) > u)).
% 0.55/0.28 thf(func_def_45, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: (($o > $o > $o) > u)).
% 0.55/0.28 thf(func_def_46, type, j_mono_2Etyop_2Emin_2Ebool: (du > $o)).
% 0.55/0.28 thf(func_def_47, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: (du > $o > $o)).
% 0.55/0.28 thf(func_def_48, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: (du > $o > $o > $o)).
% 0.55/0.28 thf(func_def_50, type, vNOT: ($o > $o)).
% 0.55/0.28 thf(func_def_53, type, vOR: ($o > $o > $o)).
% 0.55/0.28 thf(func_def_54, type, vIMP: ($o > $o > $o)).
% 0.55/0.28 thf(func_def_55, type, sP0: ($o > $o > $o > $o)).
% 0.55/0.28 thf(func_def_56, type, sP1: ($o > $o > $o > $o)).
% 0.55/0.28 thf(func_def_57, type, sP2: ($o > $o > $o > $o)).
% 0.55/0.28 thf(func_def_58, type, sP3: ($o > $o > $o > $o)).
% 0.55/0.28 thf(func_def_59, type, sP4: ($o > $o > $o > $o)).
% 0.55/0.28 thf(func_def_60, type, sP5: ($o > $o > $o > $o)).
% 0.55/0.28 thf(func_def_61, type, sP6: ($o > $o > $o > $o)).
% 0.55/0.28 thf(func_def_62, type, sP7: ($o > $o > $o > $o)).
% 0.55/0.28 thf(func_def_63, type, sK8: d).
% 0.55/0.28 thf(func_def_64, type, sK9: u).
% 0.55/0.28 thf(func_def_65, type, sK10: d).
% 0.55/0.28 thf(func_def_66, type, sK11: u).
% 0.55/0.28 thf(func_def_67, type, sK12: u).
% 0.55/0.28 thf(func_def_68, type, sK13: (u > u > d > d > u)).
% 0.55/0.28 thf(func_def_69, type, sK14: (u > u > d > d > u)).
% 0.55/0.28 thf(func_def_70, type, sK15: (u > u > d > d > u)).
% 0.55/0.28 thf(func_def_71, type, sK16: (u > u > d > d > u)).
% 0.55/0.28 thf(func_def_72, type, sK17: (u > u > d > d > u)).
% 0.55/0.28 thf(func_def_73, type, sK18: (d > d > u > u > u)).
% 0.55/0.28 thf(func_def_74, type, sK19: (d > d > u > u > u)).
% 0.55/0.28 thf(func_def_75, type, sK20: (u > u > d > d > u)).
% 0.55/0.28 thf(func_def_76, type, sK21: (u > u > d > d > u)).
% 0.55/0.28 thf(func_def_77, type, sK22: (d > d > u > u > u)).
% 0.55/0.28 thf(func_def_78, type, sK23: (d > d > u > u > u)).
% 0.55/0.28 thf(f39,axiom,(
% 0.55/0.28 ! [X0 : d,X1 : d,X2 : u,X3 : u] : (! [X11 : u,X12 : u] : (! [X13 : u] : (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X12) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X11) @ (s @ X0 @ X13))))))) <=> (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X11) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X12))))) & (! [X6 : u] : ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X6))))) => ? [X7 : u] : (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X7)))))))) <=> (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) & ! [X14 : u,X15 : u] : (! [X16 : u] : ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15) @ (s @ X1 @ X16)))) => ? [X17 : u] : (((s @ X1 @ X16)) = ((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X14) @ (s @ X0 @ X17)))))) <=> (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X14) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15))))) & ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3)))) <=> ! [X4 : u] : ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X4)))) => ? [X5 : u] : (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X5)))))))) & ! [X19 : u,X18 : u] : ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X18) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X19)))) <=> ! [X20 : u] : ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X19) @ (s @ X1 @ X20))))) => ? [X21 : u] : (((s @ X1 @ X20)) = ((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X18) @ (s @ X0 @ X21))))))) & ! [X8 : u,X9 : u] : (! [X10 : u] : (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X9) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X8) @ (s @ X0 @ X10)))))) <=> (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X8) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X9))))))),
% 0.55/0.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EquantHeuristics_2EGUESS__REWRITES)).
% 0.55/0.28 thf(f51,conjecture,(
% 0.55/0.28 ! [X0 : d,X1 : d,X3 : u,X4 : u,X2 : u] : (! [X5 : u] : ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X4) @ (s @ X0 @ X5)))) => (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X0 @ X5))))) => ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X2) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3)))) => (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X2) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X4))))))),
% 0.55/0.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 0.55/0.28 thf(f52,negated_conjecture,(
% 0.55/0.28 ~ ! [X0 : d,X1 : d,X3 : u,X4 : u,X2 : u] : (! [X5 : u] : ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X4) @ (s @ X0 @ X5)))) => (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X0 @ X5))))) => ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X2) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3)))) => (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X2) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X4))))))),
% 0.55/0.28 inference(negated_conjecture,[status(cth)],[f51])).
% 0.55/0.28 thf(f77,plain,(
% 0.55/0.28 ~ ! [X0 : d,X1 : d,X2 : u,X3 : u,X4 : u] : (! [X5 : u] : ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X0 @ X5)))) => (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2) @ (s @ X0 @ X5))))) => ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X4) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2)))) => (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X4) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3))))))),
% 0.55/0.28 inference(rectify,[],[f52])).
% 0.55/0.28 thf(f78,plain,(
% 0.55/0.28 ~ ! [X0 : d,X4 : u,X3 : u,X1 : d,X2 : u] : (! [X5 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X0 @ X5))))) = $true) => ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2) @ (s @ X0 @ X5))))))) => ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X4) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2))))) = $true) => (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X4) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3))))) = $true)))),
% 0.55/0.28 inference(fool_elimination,[],[f77])).
% 0.55/0.28 thf(f103,plain,(
% 0.55/0.28 ! [X0 : d,X1 : d,X2 : u,X3 : u] : (! [X4 : u,X5 : u] : (! [X6 : u] : (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ X0 @ X6))))))) <=> (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5))))) & (! [X7 : u] : ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X7))))) => ? [X8 : u] : (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X8)))))))) <=> (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) & ! [X9 : u,X10 : u] : (! [X11 : u] : ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10) @ (s @ X1 @ X11)))) => ? [X12 : u] : (((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ X0 @ X12)))) = ((s @ X1 @ X11)))) <=> (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10))))) & ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3)))) <=> ! [X13 : u] : ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X13)))) => ? [X14 : u] : (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X14)))))))) & ! [X15 : u,X16 : u] : ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15)))) <=> ! [X17 : u] : ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15) @ (s @ X1 @ X17))))) => ? [X18 : u] : (((s @ X1 @ X17)) = ((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ X0 @ X18))))))) & ! [X19 : u,X20 : u] : (! [X21 : u] : (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ X0 @ X21)))))) <=> (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20))))))),
% 0.55/0.28 inference(rectify,[],[f39])).
% 0.55/0.28 thf(f104,plain,(
% 0.55/0.28 ! [X3 : u,X0 : d,X1 : d,X2 : u] : ((! [X13 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X13))))) = $true) => ? [X14 : u] : ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X14))))))))) <=> (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) = $true)) & ! [X19 : u,X20 : u] : (! [X21 : u] : (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ X0 @ X21))))))) = $true) <=> (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20))))) = $true)) & ! [X15 : u,X16 : u] : (! [X17 : u] : (($true = ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15) @ (s @ X1 @ X17))))))) => ? [X18 : u] : (((s @ X1 @ X17)) = ((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ X0 @ X18)))))) <=> ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15))))))) & ! [X9 : u,X10 : u] : (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10)))))) <=> ! [X11 : u] : (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10) @ (s @ X1 @ X11)))))) => ? [X12 : u] : (((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ X0 @ X12)))) = ((s @ X1 @ X11))))) & ! [X4 : u,X5 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5))))) = $true) <=> ! [X6 : u] : ($true = ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ X0 @ X6)))))))))) & (! [X7 : u] : (($true = ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X7))))))) => ? [X8 : u] : (((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X8)))))))) = $true)) <=> (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) = $true)))),
% 0.55/0.28 inference(fool_elimination,[],[f103])).
% 0.55/0.28 thf(f110,plain,(
% 0.55/0.28 ! [X3 : u,X2 : u,X1 : d,X0 : d] : (! [X19 : u,X20 : u] : (! [X21 : u] : (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ X0 @ X21))))))) = $true) <=> (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20))))) = $true)) & ! [X4 : u,X5 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5))))) = $true) <=> ! [X6 : u] : ($true = ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ X0 @ X6)))))))))) & ! [X15 : u,X16 : u] : (! [X17 : u] : (($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15) @ (s @ X1 @ X17))))))) | ? [X18 : u] : (((s @ X1 @ X17)) = ((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ X0 @ X18)))))) <=> ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15))))))) & ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) = $true) <=> ! [X7 : u] : (? [X8 : u] : (((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X8)))))))) = $true) | ($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X7))))))))) & ! [X10 : u,X9 : u] : (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10)))))) <=> ! [X11 : u] : (? [X12 : u] : (((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ X0 @ X12)))) = ((s @ X1 @ X11))) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10) @ (s @ X1 @ X11)))))))) & (! [X13 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X13))))) != $true) | ? [X14 : u] : ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X14))))))))) <=> (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) = $true)))),
% 0.55/0.28 inference(ennf_transformation,[],[f104])).
% 0.55/0.28 thf(f111,plain,(
% 0.55/0.28 ? [X0 : d,X4 : u,X3 : u,X1 : d,X2 : u] : (((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X4) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3))))) != $true) & (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X4) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2))))) = $true)) & ! [X5 : u] : (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2) @ (s @ X0 @ X5)))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X0 @ X5))))) != $true)))),
% 0.55/0.28 inference(ennf_transformation,[],[f78])).
% 0.55/0.28 thf(f112,plain,(
% 0.55/0.28 ? [X0 : d,X4 : u,X1 : d,X3 : u,X2 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X4) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2))))) = $true) & ! [X5 : u] : (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2) @ (s @ X0 @ X5)))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X0 @ X5))))) != $true)) & (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X4) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3))))) != $true))),
% 0.55/0.28 inference(flattening,[],[f111])).
% 0.55/0.28 thf(f133,plain,(
% 0.55/0.28 ? [X0 : d,X1 : u,X2 : d,X3 : u,X4 : u] : (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ X0) @ X1) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X4)))))) & ! [X5 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X4) @ (s @ X0 @ X5))))) = $true) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X0 @ X5))))) != $true)) & (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ X0) @ X1) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X3))))) != $true))),
% 0.55/0.28 inference(rectify,[],[f112])).
% 0.55/0.28 thf(f134,plain,(
% 0.55/0.28 ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ sK10 @ sK8) @ sK9) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12)))))) & ! [X5 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12) @ (s @ sK8 @ X5))))) = $true) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11) @ (s @ sK8 @ X5))))))) & (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ sK10 @ sK8) @ sK9) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11))))) != $true)),
% 0.55/0.28 inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10,sK11,sK12]),skolemize(X0,sK8),skolemize(X1,sK9),skolemize(X2,sK10),skolemize(X3,sK11),skolemize(X4,sK12)],[f133])).
% 0.55/0.28 thf(f152,plain,(
% 0.55/0.28 ! [X3 : u,X2 : u,X1 : d,X0 : d] : (! [X19 : u,X20 : u] : ((! [X21 : u] : (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ X0 @ X21))))))) = $true) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20))))) != $true)) & ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20))))) = $true) | ? [X21 : u] : (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ X0 @ X21))))))) != $true))) & ! [X4 : u,X5 : u] : (((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5))))) = $true) | ? [X6 : u] : ($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ X0 @ X6)))))))))) & (! [X6 : u] : ($true = ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ X0 @ X6))))))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5))))) != $true))) & ! [X15 : u,X16 : u] : ((! [X17 : u] : (($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15) @ (s @ X1 @ X17))))))) | ? [X18 : u] : (((s @ X1 @ X17)) = ((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ X0 @ X18)))))) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15))))))) & (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15)))))) | ? [X17 : u] : (($true = ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15) @ (s @ X1 @ X17))))))) & ! [X18 : u] : (((s @ X1 @ X17)) != ((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ X0 @ X18)))))))) & (((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) = $true) | ? [X7 : u] : (! [X8 : u] : (((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X8)))))))) != $true) & ($true = ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X7))))))))) & (! [X7 : u] : (? [X8 : u] : (((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X8)))))))) = $true) | ($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X7)))))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) != $true))) & ! [X10 : u,X9 : u] : ((($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10)))))) | ? [X11 : u] : (! [X12 : u] : (((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ X0 @ X12)))) != ((s @ X1 @ X11))) & ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10) @ (s @ X1 @ X11)))))))) & (! [X11 : u] : (? [X12 : u] : (((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ X0 @ X12)))) = ((s @ X1 @ X11))) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10) @ (s @ X1 @ X11))))))) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10)))))))) & ((! [X13 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X13))))) != $true) | ? [X14 : u] : ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X14))))))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) != $true)) & ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) = $true) | ? [X13 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X13))))) = $true) & ! [X14 : u] : ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X14))))))))))))),
% 0.55/0.28 inference(nnf_transformation,[],[f110])).
% 0.55/0.28 thf(f153,plain,(
% 0.55/0.28 ! [X3 : u,X2 : u,X1 : d,X0 : d] : (! [X19 : u,X20 : u] : ((! [X21 : u] : (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ X0 @ X21))))))) = $true) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20))))) != $true)) & ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20))))) = $true) | ? [X21 : u] : (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X20) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X19) @ (s @ X0 @ X21))))))) != $true))) & ! [X4 : u,X5 : u] : (((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5))))) = $true) | ? [X6 : u] : ($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ X0 @ X6)))))))))) & (! [X6 : u] : ($true = ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ X0 @ X6))))))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X4) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X5))))) != $true))) & ! [X15 : u,X16 : u] : ((! [X17 : u] : (($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15) @ (s @ X1 @ X17))))))) | ? [X18 : u] : (((s @ X1 @ X17)) = ((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ X0 @ X18)))))) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15))))))) & (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15)))))) | ? [X17 : u] : (($true = ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X15) @ (s @ X1 @ X17))))))) & ! [X18 : u] : (((s @ X1 @ X17)) != ((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X16) @ (s @ X0 @ X18)))))))) & ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) = $true) | ? [X7 : u] : (! [X8 : u] : (((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X8)))))))) != $true) & ($true = ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X7))))))))) & (! [X7 : u] : (? [X8 : u] : (((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X8)))))))) = $true) | ($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X7)))))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) != $true)) & ! [X10 : u,X9 : u] : ((($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10)))))) | ? [X11 : u] : (! [X12 : u] : (((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ X0 @ X12)))) != ((s @ X1 @ X11))) & ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10) @ (s @ X1 @ X11)))))))) & (! [X11 : u] : (? [X12 : u] : (((s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ X0 @ X12)))) = ((s @ X1 @ X11))) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10) @ (s @ X1 @ X11))))))) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X9) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X10)))))))) & (! [X13 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X13))))) != $true) | ? [X14 : u] : ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X14))))))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) != $true)) & ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3))))) = $true) | ? [X13 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ X13))))) = $true) & ! [X14 : u] : ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ X1 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X1) @ X2) @ (s @ X0 @ X14)))))))))))),
% 0.55/0.28 inference(flattening,[],[f152])).
% 0.55/0.28 thf(f154,plain,(
% 0.55/0.28 ! [X0 : u,X1 : u,X2 : d,X3 : d] : (! [X4 : u,X5 : u] : ((! [X6 : u] : ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X5) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X4) @ (s @ X3 @ X6)))))))) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X4) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X5))))))) & (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X4) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X5)))))) | ? [X7 : u] : (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X5) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X4) @ (s @ X3 @ X7))))))) != $true))) & ! [X8 : u,X9 : u] : ((($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9)))))) | ? [X10 : u] : ($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ X3 @ X10)))))))))) & (! [X11 : u] : (((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ X3 @ X11)))))))) = $true) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9)))))))) & ! [X12 : u,X13 : u] : ((! [X14 : u] : ((((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X12) @ (s @ X2 @ X14)))))) != $true) | ? [X15 : u] : (((s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X13) @ (s @ X3 @ X15)))) = ((s @ X2 @ X14)))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X13) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X12))))) != $true)) & ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X13) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X12))))) = $true) | ? [X16 : u] : ((((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X12) @ (s @ X2 @ X16)))))) = $true) & ! [X17 : u] : (((s @ X2 @ X16)) != ((s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X13) @ (s @ X3 @ X17)))))))) & ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0))))) = $true) | ? [X18 : u] : (! [X19 : u] : ($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ X3 @ X19))))))))) & ($true = ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ X18))))))))) & (! [X20 : u] : (? [X21 : u] : (((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ X3 @ X21)))))))) = $true) | ($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ X20)))))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0))))) != $true)) & ! [X22 : u,X23 : u] : ((($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X23) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X22)))))) | ? [X24 : u] : (! [X25 : u] : (((s @ X2 @ X24)) != ((s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X23) @ (s @ X3 @ X25))))) & (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X22) @ (s @ X2 @ X24))))) = $true))) & (! [X26 : u] : (? [X27 : u] : (((s @ X2 @ X26)) = ((s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X23) @ (s @ X3 @ X27))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X22) @ (s @ X2 @ X26))))) != $true)) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X23) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X22)))))))) & (! [X28 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ X28))))) != $true) | ? [X29 : u] : (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ X3 @ X29))))))) = $true)) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0))))))) & (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0)))))) | ? [X30 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ X30))))) = $true) & ! [X31 : u] : ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ X3 @ X31)))))))))))),
% 0.55/0.28 inference(rectify,[],[f153])).
% 0.55/0.28 thf(f155,plain,(
% 0.55/0.28 ! [X0 : u,X1 : u,X2 : d,X3 : d] : (! [X4 : u,X5 : u] : ((! [X6 : u] : ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X5) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X4) @ (s @ X3 @ X6)))))))) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X4) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X5))))))) & (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X4) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X5)))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X5) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X4) @ (s @ X3 @ (sK14 @ X5 @ X4 @ X3 @ X2)))))))) != $true))) & ! [X8 : u,X9 : u] : ((($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9)))))) | ($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ X3 @ (sK15 @ X9 @ X8 @ X3 @ X2))))))))))) & (! [X11 : u] : (((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ X3 @ X11)))))))) = $true) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9)))))))) & ! [X12 : u,X13 : u] : ((! [X14 : u] : ((((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X12) @ (s @ X2 @ X14)))))) != $true) | (((s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X13) @ (s @ X3 @ (sK16 @ X14 @ X13 @ X3 @ X2))))) = ((s @ X2 @ X14)))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X13) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X12))))) != $true)) & ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X13) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X12))))) = $true) | ((((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X12) @ (s @ X2 @ (sK17 @ X13 @ X12 @ X3 @ X2))))))) = $true) & ! [X17 : u] : (((s @ X2 @ (sK17 @ X13 @ X12 @ X3 @ X2))) != ((s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X13) @ (s @ X3 @ X17)))))))) & ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0))))) = $true) | (! [X19 : u] : ($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ X3 @ X19))))))))) & (((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ (sK18 @ X3 @ X2 @ X1 @ X0))))))) = $true))) & (! [X20 : u] : ((((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ X3 @ (sK19 @ X3 @ X2 @ X1 @ X0))))))))) = $true) | ($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ X20)))))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0))))) != $true)) & ! [X22 : u,X23 : u] : ((($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X23) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X22)))))) | (! [X25 : u] : (((s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X23) @ (s @ X3 @ X25)))) != ((s @ X2 @ (sK20 @ X23 @ X22 @ X3 @ X2)))) & ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X22) @ (s @ X2 @ (sK20 @ X23 @ X22 @ X3 @ X2))))))))) & (! [X26 : u] : ((((s @ X2 @ X26)) = ((s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X23) @ (s @ X3 @ (sK21 @ X26 @ X23 @ X3 @ X2)))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X22) @ (s @ X2 @ X26))))) != $true)) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X23) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X22)))))))) & (! [X28 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ X28))))) != $true) | ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ X3 @ (sK22 @ X3 @ X2 @ X1 @ X0)))))))))) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0))))))) & (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__EXISTS_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0)))))) | (($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ (sK23 @ X3 @ X2 @ X1 @ X0))))))) & ! [X31 : u] : ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X0) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X1) @ (s @ X3 @ X31)))))))))))),
% 0.55/0.28 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP]),skolemize(X4,sK13 @ X3 @ X2 @ X1 @ X0),skolemize(X4,sK13 @ X3 @ X2 @ X1 @ X0),skolemize(X4,sK13 @ X3 @ X2 @ X1 @ X0),skolemize(X4,sK13 @ X3 @ X2 @ X1 @ X0),skolemize(X4,sK13 @ X3 @ X2 @ X1 @ X0),skolemize(X4,sK13 @ X3 @ X2 @ X1 @ X0),skolemize(X4,sK13 @ X3 @ X2 @ X1 @ X0),skolemize(X4,sK13 @ X3 @ X2 @ X1 @ X0),skolemize(X4,sK13 @ X3 @ X2 @ X1 @ X0),skolemize(X4,sK13 @ X3 @ X2 @ X1 @ X0)],[f154])).
% 0.55/0.28 thf(f190,plain,(
% 0.55/0.28 (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ sK10 @ sK8) @ sK9) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11))))) != $true)),
% 0.55/0.28 inference(cnf_transformation,[],[f134])).
% 0.55/0.28 thf(f191,plain,(
% 0.55/0.28 ( ! [X5 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12) @ (s @ sK8 @ X5))))) = $true) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11) @ (s @ sK8 @ X5))))))) )),
% 0.55/0.28 inference(cnf_transformation,[],[f134])).
% 0.55/0.28 thf(f192,plain,(
% 0.55/0.28 ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ sK10 @ sK8) @ sK9) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12))))))),
% 0.55/0.28 inference(cnf_transformation,[],[f134])).
% 0.55/0.28 thf(f237,plain,(
% 0.55/0.28 ( ! [X2 : d,X3 : d,X11 : u,X8 : u,X9 : u] : ((((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ X3 @ X11)))))))) = $true) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9))))))) )),
% 0.55/0.28 inference(cnf_transformation,[],[f155])).
% 0.55/0.28 thf(f238,plain,(
% 0.55/0.28 ( ! [X2 : d,X3 : d,X8 : u,X9 : u] : (($true != ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9) @ (s @ X2 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ X3 @ (sK15 @ X9 @ X8 @ X3 @ X2)))))))))) | ($true = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X3 @ X2) @ X8) @ (s @ (tyop_2Emin_2Efun @ X2 @ tyop_2Emin_2Ebool) @ X9))))))) )),
% 0.55/0.28 inference(cnf_transformation,[],[f155])).
% 0.55/0.28 thf(f288,definition,(
% 0.55/0.28 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.55/0.28 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.55/0.28 thf(f378,plain,(
% 0.55/0.28 ($false = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ sK10 @ sK8) @ sK9) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11)))))) | ($true != $true)),
% 0.55/0.28 inference(superposition,[],[f190,f288])).
% 0.55/0.28 thf(f379,plain,(
% 0.55/0.28 ($false = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ sK10 @ sK8) @ sK9) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11))))))),
% 0.55/0.28 inference(trivial_inequality_removal,[],[f378])).
% 0.55/0.28 thf(f393,plain,(
% 0.55/0.28 ( ! [X2 : u,X0 : d,X1 : u] : ((((~ $true)) = $true) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11) @ (s @ sK8 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ X0 @ X2))))))) != $true) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12))))))) )),
% 0.55/0.28 inference(superposition,[],[f237,f191])).
% 0.55/0.28 thf(f402,plain,(
% 0.55/0.28 ( ! [X2 : u,X0 : d,X1 : u] : (($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12)))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11) @ (s @ sK8 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ X0 @ X2))))))) != $true) | ($false = $true)) )),
% 0.55/0.28 inference(not_proxy_clausification,[],[f393])).
% 0.55/0.28 thf(f403,plain,(
% 0.55/0.28 ( ! [X2 : u,X0 : d,X1 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11) @ (s @ sK8 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ X0 @ X2))))))) != $true) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12))))))) )),
% 0.55/0.28 inference(trivial_inequality_removal,[],[f402])).
% 0.55/0.28 thf(f473,plain,(
% 0.55/0.28 ( ! [X2 : u,X0 : d,X1 : u] : (($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12)))))) | ($false = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11) @ (s @ sK8 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ X0 @ X2)))))))) | ($true != $true)) )),
% 0.55/0.28 inference(superposition,[],[f403,f288])).
% 0.55/0.28 thf(f479,plain,(
% 0.55/0.28 ( ! [X2 : u,X0 : d,X1 : u] : (($false = ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11) @ (s @ sK8 @ (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ X0 @ X2)))))))) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12))))))) )),
% 0.55/0.28 inference(trivial_inequality_removal,[],[f473])).
% 0.55/0.28 thf(f767,plain,(
% 0.55/0.28 ( ! [X0 : d,X1 : u] : ((((~ $false)) != $true) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12)))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11))))) = $true)) )),
% 0.55/0.28 inference(superposition,[],[f238,f479])).
% 0.55/0.28 thf(f780,plain,(
% 0.55/0.28 ( ! [X0 : d,X1 : u] : (($false = $true) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12)))))) | (((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11))))) = $true)) )),
% 0.55/0.28 inference(not_proxy_clausification,[],[f767])).
% 0.55/0.28 thf(f781,plain,(
% 0.55/0.28 ( ! [X0 : d,X1 : u] : ((((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK11))))) = $true) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ sK8) @ X1) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12))))))) )),
% 0.55/0.28 inference(trivial_inequality_removal,[],[f780])).
% 0.55/0.28 thf(f835,plain,(
% 0.55/0.28 ($false = $true) | ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ sK10 @ sK8) @ sK9) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12))))))),
% 0.55/0.28 inference(superposition,[],[f379,f781])).
% 0.55/0.28 thf(f838,plain,(
% 0.55/0.28 ($true != ((j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2 @ (s @ (tyop_2Emin_2Efun @ sK10 @ sK8) @ sK9) @ (s @ (tyop_2Emin_2Efun @ sK8 @ tyop_2Emin_2Ebool) @ sK12))))))),
% 0.55/0.28 inference(trivial_inequality_removal,[],[f835])).
% 0.55/0.28 thf(f841,plain,(
% 0.55/0.28 $false),
% 0.55/0.28 inference(forward_subsumption_resolution,[],[f838,f192])).
% 0.55/0.28 % SZS output end Proof for theBenchmark
% 0.55/0.28 % (556979)------------------------------
% 0.55/0.28 % (556979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.28 % (556979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.28 % (556979)CaDiCaL version: 2.1.3
% 0.55/0.28 % (556979)Termination reason: Refutation
% 0.55/0.28 % (556979)Time elapsed: 0.055 s
% 0.55/0.28 % (556979)Peak memory usage: 13 MB
% 0.55/0.28 % (556979)Instructions burned: 130 (million)
% 0.55/0.28 % (556915)Success in time 0.129 s
% 0.55/0.28 % Vampire exiting
%------------------------------------------------------------------------------