%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP171^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:08:39 AM UTC 2026
% Result : Theorem 0.73s 0.50s
% Output : Refutation 0.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP171^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n005.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 20:05:01 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.24/0.35 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.73/0.50 % (2139773)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.73/0.50 % (2139800)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2447816251:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.73/0.50 % (2139802)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.73/0.50 % (2139802)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.73/0.50 % (2139796)lrs+10_16_si=on:nwc=1.5:random_seed=2163676244:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.73/0.50 % (2139799)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2860809062:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.73/0.50 % (2139795)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3827115520:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.73/0.50 % (2139798)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=3412946542: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.73/0.50 % (2139797)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2816262716:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.73/0.50 % (2139802)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=1270336544:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.73/0.50 % (2139797)Instruction limit reached!
% 0.73/0.50 % (2139797)------------------------------
% 0.73/0.50 % (2139797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139797)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139797)Termination reason: Instruction limit
% 0.73/0.50 % (2139797)Termination phase: shuffling
% 0.73/0.50 % (2139797)Time elapsed: 0.002 s
% 0.73/0.50 % (2139797)Peak memory usage: 10 MB
% 0.73/0.50 % (2139797)Instructions burned: 3 (million)
% 0.73/0.50 % (2139796)Instruction limit reached!
% 0.73/0.50 % (2139796)------------------------------
% 0.73/0.50 % (2139796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139796)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139796)Termination reason: Instruction limit
% 0.73/0.50 % (2139796)Termination phase: shuffling
% 0.73/0.50 % (2139796)Time elapsed: 0.008 s
% 0.73/0.50 % (2139796)Peak memory usage: 10 MB
% 0.73/0.50 % (2139796)Instructions burned: 18 (million)
% 0.73/0.50 % (2139799)Instruction limit reached!
% 0.73/0.50 % (2139799)------------------------------
% 0.73/0.50 % (2139799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139799)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139799)Termination reason: Instruction limit
% 0.73/0.50 % (2139799)Termination phase: shuffling
% 0.73/0.50 % (2139799)Time elapsed: 0.012 s
% 0.73/0.50 % (2139799)Peak memory usage: 10 MB
% 0.73/0.50 % (2139799)Instructions burned: 26 (million)
% 0.73/0.50 % (2139800)Instruction limit reached!
% 0.73/0.50 % (2139800)------------------------------
% 0.73/0.50 % (2139800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139800)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139800)Termination reason: Instruction limit
% 0.73/0.50 % (2139800)Termination phase: Preprocessing 2
% 0.73/0.50 % (2139800)Time elapsed: 0.019 s
% 0.73/0.50 % (2139800)Peak memory usage: 11 MB
% 0.73/0.50 % (2139800)Instructions burned: 77 (million)
% 0.73/0.50 % (2139822)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=709434441:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.73/0.50 % (2139815)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4143251402:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.73/0.50 % (2139815)Instruction limit reached!
% 0.73/0.50 % (2139815)------------------------------
% 0.73/0.50 % (2139815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139820)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.73/0.50 % (2139815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139815)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139815)Termination reason: Instruction limit
% 0.73/0.50 % (2139815)Termination phase: shuffling
% 0.73/0.50 % (2139815)Time elapsed: 0.002 s
% 0.73/0.50 % (2139815)Peak memory usage: 10 MB
% 0.73/0.50 % (2139815)Instructions burned: 3 (million)
% 0.73/0.50 % (2139822)Instruction limit reached!
% 0.73/0.50 % (2139822)------------------------------
% 0.73/0.50 % (2139822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139822)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139822)Termination reason: Instruction limit
% 0.73/0.50 % (2139822)Termination phase: shuffling
% 0.73/0.50 % (2139822)Time elapsed: 0.003 s
% 0.73/0.50 % (2139822)Peak memory usage: 10 MB
% 0.73/0.50 % (2139822)Instructions burned: 12 (million)
% 0.73/0.50 % (2139817)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1229944624:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.73/0.50 % (2139820)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3933069947:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.73/0.50 % (2139817)Instruction limit reached!
% 0.73/0.50 % (2139817)------------------------------
% 0.73/0.50 % (2139817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139817)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139817)Termination reason: Instruction limit
% 0.73/0.50 % (2139817)Termination phase: shuffling
% 0.73/0.50 % (2139817)Time elapsed: 0.003 s
% 0.73/0.50 % (2139817)Peak memory usage: 10 MB
% 0.73/0.50 % (2139817)Instructions burned: 5 (million)
% 0.73/0.50 % (2139820)Instruction limit reached!
% 0.73/0.50 % (2139820)------------------------------
% 0.73/0.50 % (2139820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139820)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139820)Termination reason: Instruction limit
% 0.73/0.50 % (2139820)Termination phase: shuffling
% 0.73/0.50 % (2139820)Time elapsed: 0.004 s
% 0.73/0.50 % (2139820)Peak memory usage: 10 MB
% 0.73/0.50 % (2139820)Instructions burned: 8 (million)
% 0.73/0.50 % (2139832)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.73/0.50 % (2139832)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.73/0.50 % (2139832)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=4264951286: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.73/0.50 % (2139795)Instruction limit reached!
% 0.73/0.50 % (2139795)------------------------------
% 0.73/0.50 % (2139795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139795)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139795)Termination reason: Instruction limit
% 0.73/0.50 % (2139795)Termination phase: Preprocessing 3
% 0.73/0.50 % (2139795)Time elapsed: 0.040 s
% 0.73/0.50 % (2139795)Peak memory usage: 12 MB
% 0.73/0.50 % (2139795)Instructions burned: 87 (million)
% 0.73/0.50 % (2139833)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=3355602807:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.73/0.50 % (2139832)Instruction limit reached!
% 0.73/0.50 % (2139832)------------------------------
% 0.73/0.50 % (2139832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139832)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139832)Termination reason: Instruction limit
% 0.73/0.50 % (2139832)Termination phase: shuffling
% 0.73/0.50 % (2139832)Time elapsed: 0.008 s
% 0.73/0.50 % (2139832)Peak memory usage: 11 MB
% 0.73/0.50 % (2139832)Instructions burned: 32 (million)
% 0.73/0.50 % (2139839)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.73/0.50 % (2139838)lrs+10_1_si=on:cs=on:random_seed=3067649794:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.73/0.50 % (2139839)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=3005920016:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.73/0.50 % (2139838)Instruction limit reached!
% 0.73/0.50 % (2139838)------------------------------
% 0.73/0.50 % (2139838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139838)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139838)Termination reason: Instruction limit
% 0.73/0.50 % (2139838)Termination phase: shuffling
% 0.73/0.50 % (2139838)Time elapsed: 0.004 s
% 0.73/0.50 % (2139838)Peak memory usage: 11 MB
% 0.73/0.50 % (2139838)Instructions burned: 8 (million)
% 0.73/0.50 % (2139839)Instruction limit reached!
% 0.73/0.50 % (2139839)------------------------------
% 0.73/0.50 % (2139839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139839)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139839)Termination reason: Instruction limit
% 0.73/0.50 % (2139839)Termination phase: shuffling
% 0.73/0.50 % (2139839)Time elapsed: 0.002 s
% 0.73/0.50 % (2139839)Peak memory usage: 10 MB
% 0.73/0.50 % (2139839)Instructions burned: 3 (million)
% 0.73/0.50 % (2139846)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1995157693:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.73/0.50 % (2139841)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2813624551:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.73/0.50 % (2139802)Instruction limit reached!
% 0.73/0.50 % (2139802)------------------------------
% 0.73/0.50 % (2139802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139802)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139802)Termination reason: Instruction limit
% 0.73/0.50 % (2139802)Termination phase: Property scanning
% 0.73/0.50 % (2139802)Time elapsed: 0.070 s
% 0.73/0.50 % (2139802)Peak memory usage: 13 MB
% 0.73/0.50 % (2139802)Instructions burned: 157 (million)
% 0.73/0.50 % (2139849)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=170886391:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.73/0.50 % (2139851)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1486872466:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.73/0.50 % (2139841)Instruction limit reached!
% 0.73/0.50 % (2139841)------------------------------
% 0.73/0.50 % (2139841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139841)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139841)Termination reason: Instruction limit
% 0.73/0.50 % (2139841)Termination phase: shuffling
% 0.73/0.50 % (2139841)Time elapsed: 0.017 s
% 0.73/0.50 % (2139841)Peak memory usage: 11 MB
% 0.73/0.50 % (2139841)Instructions burned: 40 (million)
% 0.73/0.50 % (2139846) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2139773-2139846"...
% 0.73/0.50 % (2139851)Instruction limit reached!
% 0.73/0.50 % (2139851)------------------------------
% 0.73/0.50 % (2139851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139851)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139851)Termination reason: Instruction limit
% 0.73/0.50 % (2139851)Termination phase: shuffling
% 0.73/0.50 % (2139851)Time elapsed: 0.007 s
% 0.73/0.50 % (2139851)Peak memory usage: 10 MB
% 0.73/0.50 % (2139851)Instructions burned: 16 (million)
% 0.73/0.50 % (2139846)...printing done.
% 0.73/0.50 % (2139833)Instruction limit reached!
% 0.73/0.50 % (2139833)------------------------------
% 0.73/0.50 % (2139833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.50 % (2139833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.50 % (2139833)CaDiCaL version: 2.1.3
% 0.73/0.50 % (2139833)Termination reason: Instruction limit
% 0.73/0.50 % (2139833)Termination phase: Property scanning
% 0.73/0.50 % (2139833)Time elapsed: 0.039 s
% 0.73/0.50 % (2139833)Peak memory usage: 12 MB
% 0.73/0.50 % (2139833)Instructions burned: 87 (million)
% 0.73/0.50 % (2139846)Refutation found. Thanks to Tanya!
% 0.73/0.50 % SZS status Theorem for theBenchmark
% 0.73/0.50 % SZS output start Proof for theBenchmark
% 0.73/0.50 thf(type_def_5, type, heap_E1735400259tr_b_c: $tType).
% 0.73/0.50 thf(type_def_6, type, heap_E1188946203tr_d_e: $tType).
% 0.73/0.50 thf(type_def_7, type, heap_E1770015209t_char: $tType).
% 0.73/0.50 thf(type_def_8, type, heap_E189844335_ptr_d: $tType).
% 0.73/0.50 thf(type_def_9, type, heap_E906991588_ptr_a: $tType).
% 0.73/0.50 thf(type_def_10, type, heap_E1996099391_ptr_b: $tType).
% 0.73/0.50 thf(type_def_11, type, heap_E1661210526_ptr_a: $tType).
% 0.73/0.50 thf(type_def_12, type, heap_E434560396t_char: $tType).
% 0.73/0.50 thf(type_def_13, type, heap_E625070648t_unit: $tType).
% 0.73/0.50 thf(type_def_14, type, heap_E834686006tion_n: $tType).
% 0.73/0.50 thf(type_def_15, type, heap_E826424501tion_m: $tType).
% 0.73/0.50 thf(type_def_16, type, heap_S1465075775_j_k_l: $tType).
% 0.73/0.50 thf(type_def_17, type, rObjec1413572695_j_k_l: $tType).
% 0.73/0.50 thf(type_def_18, type, object945351580_d_e_f: $tType).
% 0.73/0.50 thf(type_def_19, type, option1128016977on_h_i: $tType).
% 0.73/0.50 thf(type_def_20, type, rObjec1922030987on_h_i: $tType).
% 0.73/0.50 thf(type_def_21, type, option841825948on_j_k: $tType).
% 0.73/0.50 thf(type_def_22, type, rObjec1617416918on_j_k: $tType).
% 0.73/0.50 thf(type_def_23, type, option1029218147tion_j: $tType).
% 0.73/0.50 thf(type_def_24, type, rObjec2068690451tion_j: $tType).
% 0.73/0.50 thf(type_def_25, type, option1344508504tr_b_c: $tType).
% 0.73/0.50 thf(type_def_26, type, option392980921tion_g: $tType).
% 0.73/0.50 thf(type_def_27, type, list_n282880152tr_b_c: $tType).
% 0.73/0.50 thf(type_def_28, type, option849832995tion_h: $tType).
% 0.73/0.50 thf(type_def_29, type, node_p1234578834tr_b_c: $tType).
% 0.73/0.50 thf(type_def_30, type, rObjec1875798643tion_g: $tType).
% 0.73/0.50 thf(type_def_31, type, rObjec1148923485tion_h: $tType).
% 0.73/0.50 thf(type_def_32, type, docume1935157360tr_d_e: $tType).
% 0.73/0.50 thf(type_def_33, type, finite1621822014t_char: $tType).
% 0.73/0.50 thf(type_def_34, type, option2061924698_ptr_b: $tType).
% 0.73/0.50 thf(type_def_35, type, option147517124_ptr_d: $tType).
% 0.73/0.50 thf(type_def_36, type, option_element_ptr_a: $tType).
% 0.73/0.50 thf(type_def_37, type, character_data_ptr_b: $tType).
% 0.73/0.50 thf(type_def_38, type, shadow_root_ptr_d: $tType).
% 0.73/0.50 thf(type_def_39, type, element_ptr_a: $tType).
% 0.73/0.50 thf(type_def_40, type, list_char: $tType).
% 0.73/0.50 thf(type_def_41, type, product_unit: $tType).
% 0.73/0.50 thf(type_def_42, type, n: $tType).
% 0.73/0.50 thf(type_def_43, type, m: $tType).
% 0.73/0.50 thf(type_def_44, type, sTfun: ($tType * $tType) > $tType).
% 0.73/0.50 thf(func_def_0, type, l_put_1584770338t_char: ((character_data_ptr_b > heap_S1465075775_j_k_l > option849832995tion_h) > (character_data_ptr_b > rObjec1148923485tion_h > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l) > character_data_ptr_b > ((list_char > list_char) > rObjec1148923485tion_h > rObjec1148923485tion_h) > list_char > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_1, type, l_put_893346794tr_b_c: ((docume1935157360tr_d_e > heap_S1465075775_j_k_l > option841825948on_j_k) > (docume1935157360tr_d_e > rObjec1617416918on_j_k > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l) > docume1935157360tr_d_e > ((list_n282880152tr_b_c > list_n282880152tr_b_c) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > list_n282880152tr_b_c > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_2, type, l_put_821218959t_char: ((docume1935157360tr_d_e > heap_S1465075775_j_k_l > option841825948on_j_k) > (docume1935157360tr_d_e > rObjec1617416918on_j_k > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l) > docume1935157360tr_d_e > ((list_char > list_char) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > list_char > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_3, type, l_put_38398219_ptr_a: ((docume1935157360tr_d_e > heap_S1465075775_j_k_l > option841825948on_j_k) > (docume1935157360tr_d_e > rObjec1617416918on_j_k > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l) > docume1935157360tr_d_e > ((option_element_ptr_a > option_element_ptr_a) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > option_element_ptr_a > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_4, type, l_put_1129034844_j_k_m: ((docume1935157360tr_d_e > heap_S1465075775_j_k_l > option841825948on_j_k) > (docume1935157360tr_d_e > rObjec1617416918on_j_k > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l) > docume1935157360tr_d_e > ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > m > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_5, type, l_put_1129034845_j_k_n: ((docume1935157360tr_d_e > heap_S1465075775_j_k_l > option841825948on_j_k) > (docume1935157360tr_d_e > rObjec1617416918on_j_k > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l) > docume1935157360tr_d_e > ((n > n) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > n > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_6, type, l_put_1666965382t_char: ((element_ptr_a > heap_S1465075775_j_k_l > option392980921tion_g) > (element_ptr_a > rObjec1875798643tion_g > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l) > element_ptr_a > ((finite1621822014t_char > finite1621822014t_char) > rObjec1875798643tion_g > rObjec1875798643tion_g) > finite1621822014t_char > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_7, type, l_put_2122145248tr_b_c: ((element_ptr_a > heap_S1465075775_j_k_l > option392980921tion_g) > (element_ptr_a > rObjec1875798643tion_g > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l) > element_ptr_a > ((list_n282880152tr_b_c > list_n282880152tr_b_c) > rObjec1875798643tion_g > rObjec1875798643tion_g) > list_n282880152tr_b_c > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_8, type, l_put_1449921049t_char: ((element_ptr_a > heap_S1465075775_j_k_l > option392980921tion_g) > (element_ptr_a > rObjec1875798643tion_g > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l) > element_ptr_a > ((list_char > list_char) > rObjec1875798643tion_g > rObjec1875798643tion_g) > list_char > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_9, type, l_put_1103319052_ptr_d: ((element_ptr_a > heap_S1465075775_j_k_l > option392980921tion_g) > (element_ptr_a > rObjec1875798643tion_g > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l) > element_ptr_a > ((option147517124_ptr_d > option147517124_ptr_d) > rObjec1875798643tion_g > rObjec1875798643tion_g) > option147517124_ptr_d > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_10, type, val_option_h: (rObjec1148923485tion_h > list_char)).
% 0.73/0.50 thf(func_def_11, type, val_update_option_h: ((list_char > list_char) > rObjec1148923485tion_h > rObjec1148923485tion_h)).
% 0.73/0.50 thf(func_def_12, type, cast_C1209085999_d_g_i: (rObjec1148923485tion_h > rObjec1922030987on_h_i)).
% 0.73/0.50 thf(func_def_13, type, cast_N1374991725_g_h_i: (rObjec1922030987on_h_i > option849832995tion_h)).
% 0.73/0.50 thf(func_def_14, type, get_C_592656865_j_k_l: (character_data_ptr_b > heap_S1465075775_j_k_l > option849832995tion_h)).
% 0.73/0.50 thf(func_def_15, type, l_type1003141153_j_k_l: (heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_16, type, put_C_229546338_j_k_l: (character_data_ptr_b > rObjec1148923485tion_h > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l)).
% 0.73/0.50 thf(func_def_17, type, type_w1771507213_j_k_l: (heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_18, type, get_M_1865279188_j_k_l: (character_data_ptr_b > (rObjec1148923485tion_h > docume1935157360tr_d_e) > heap_E1188946203tr_d_e)).
% 0.73/0.50 thf(func_def_19, type, get_M_1186169077_j_k_l: (character_data_ptr_b > (rObjec1148923485tion_h > element_ptr_a) > heap_E1661210526_ptr_a)).
% 0.73/0.50 thf(func_def_20, type, get_M_2088872005_j_k_l: (character_data_ptr_b > (rObjec1148923485tion_h > list_char) > heap_E434560396t_char)).
% 0.73/0.50 thf(func_def_21, type, get_M_1903403023_j_k_l: (character_data_ptr_b > (rObjec1148923485tion_h > product_unit) > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_22, type, get_M_1665432076_j_k_l: (character_data_ptr_b > (rObjec1148923485tion_h > m) > heap_E826424501tion_m)).
% 0.73/0.50 thf(func_def_23, type, get_M_1932781581_j_k_l: (character_data_ptr_b > (rObjec1148923485tion_h > n) > heap_E834686006tion_n)).
% 0.73/0.50 thf(func_def_24, type, l_new_410495338_j_k_l: ((heap_S1465075775_j_k_l > $o) > $o)).
% 0.73/0.50 thf(func_def_25, type, new_ch829669006_j_k_l: heap_E1996099391_ptr_b).
% 0.73/0.50 thf(func_def_26, type, put_M_726238649_j_k_l: (character_data_ptr_b > ((docume1935157360tr_d_e > docume1935157360tr_d_e) > rObjec1148923485tion_h > rObjec1148923485tion_h) > docume1935157360tr_d_e > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_27, type, put_M_731120658_j_k_l: (character_data_ptr_b > ((element_ptr_a > element_ptr_a) > rObjec1148923485tion_h > rObjec1148923485tion_h) > element_ptr_a > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_28, type, put_M_1937380872_j_k_l: (character_data_ptr_b > ((list_char > list_char) > rObjec1148923485tion_h > rObjec1148923485tion_h) > list_char > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_29, type, put_M_1374331384_j_k_l: (character_data_ptr_b > ((product_unit > product_unit) > rObjec1148923485tion_h > rObjec1148923485tion_h) > product_unit > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_30, type, put_M_199545403_j_k_l: (character_data_ptr_b > ((m > m) > rObjec1148923485tion_h > rObjec1148923485tion_h) > m > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_31, type, put_M_243508858_j_k_l: (character_data_ptr_b > ((n > n) > rObjec1148923485tion_h > rObjec1148923485tion_h) > n > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_32, type, cast_c164415100_b_a_c: (character_data_ptr_b > node_p1234578834tr_b_c)).
% 0.73/0.50 thf(func_def_33, type, cast_n1518532508_a_b_c: (node_p1234578834tr_b_c > option2061924698_ptr_b)).
% 0.73/0.50 thf(func_def_34, type, is_cha504820986_t_r_b: (character_data_ptr_b > $o)).
% 0.73/0.50 thf(func_def_35, type, is_cha330921893_a_b_c: (node_p1234578834tr_b_c > $o)).
% 0.73/0.50 thf(func_def_36, type, discon866287741on_j_k: (rObjec1617416918on_j_k > list_n282880152tr_b_c)).
% 0.73/0.50 thf(func_def_37, type, discon442323090on_j_k: ((list_n282880152tr_b_c > list_n282880152tr_b_c) > rObjec1617416918on_j_k > rObjec1617416918on_j_k)).
% 0.73/0.50 thf(func_def_38, type, doctyp814403297on_j_k: (rObjec1617416918on_j_k > list_char)).
% 0.73/0.50 thf(func_def_39, type, doctyp68000440on_j_k: ((list_char > list_char) > rObjec1617416918on_j_k > rObjec1617416918on_j_k)).
% 0.73/0.50 thf(func_def_40, type, docume1175131570on_j_k: (rObjec1617416918on_j_k > option_element_ptr_a)).
% 0.73/0.50 thf(func_def_41, type, docume244715269on_j_k: ((option_element_ptr_a > option_element_ptr_a) > rObjec1617416918on_j_k > rObjec1617416918on_j_k)).
% 0.73/0.50 thf(func_def_42, type, cast_D1252964113_h_i_l: (rObjec1617416918on_j_k > rObjec1413572695_j_k_l)).
% 0.73/0.50 thf(func_def_43, type, cast_O1034441233_j_k_l: (rObjec1413572695_j_k_l > option841825948on_j_k)).
% 0.73/0.50 thf(func_def_44, type, get_D_1192261494_j_k_l: (docume1935157360tr_d_e > heap_S1465075775_j_k_l > option841825948on_j_k)).
% 0.73/0.50 thf(func_def_45, type, is_doc1417632087_j_k_l: (rObjec1413572695_j_k_l > $o)).
% 0.73/0.50 thf(func_def_46, type, l_type1130145226_j_k_l: (heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_47, type, put_D_2126422573_h_i_l: (docume1935157360tr_d_e > rObjec1617416918on_j_k > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l)).
% 0.73/0.50 thf(func_def_48, type, type_w1479951274_j_k_l: (heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_49, type, get_M_462148605_h_i_l: (docume1935157360tr_d_e > (rObjec1617416918on_j_k > docume1935157360tr_d_e) > heap_E1188946203tr_d_e)).
% 0.73/0.50 thf(func_def_50, type, get_M_377480556_h_i_l: (docume1935157360tr_d_e > (rObjec1617416918on_j_k > element_ptr_a) > heap_E1661210526_ptr_a)).
% 0.73/0.50 thf(func_def_51, type, get_M_986049031_h_i_l: (docume1935157360tr_d_e > (rObjec1617416918on_j_k > list_n282880152tr_b_c) > heap_E1735400259tr_b_c)).
% 0.73/0.50 thf(func_def_52, type, get_M_1536717772_h_i_l: (docume1935157360tr_d_e > (rObjec1617416918on_j_k > list_char) > heap_E434560396t_char)).
% 0.73/0.50 thf(func_def_53, type, get_M_1723352102_h_i_l: (docume1935157360tr_d_e > (rObjec1617416918on_j_k > option_element_ptr_a) > heap_E906991588_ptr_a)).
% 0.73/0.50 thf(func_def_54, type, get_M_1965837010_h_i_l: (docume1935157360tr_d_e > (rObjec1617416918on_j_k > product_unit) > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_55, type, get_M_1422421269_h_i_l: (docume1935157360tr_d_e > (rObjec1617416918on_j_k > m) > heap_E826424501tion_m)).
% 0.73/0.50 thf(func_def_56, type, get_M_544184404_h_i_l: (docume1935157360tr_d_e > (rObjec1617416918on_j_k > n) > heap_E834686006tion_n)).
% 0.73/0.50 thf(func_def_57, type, l_new_1474790279_j_k_l: ((heap_S1465075775_j_k_l > $o) > $o)).
% 0.73/0.50 thf(func_def_58, type, new_do4779043_j_k_l: heap_E1188946203tr_d_e).
% 0.73/0.50 thf(func_def_59, type, put_M_2097930918_h_i_l: (docume1935157360tr_d_e > ((docume1935157360tr_d_e > docume1935157360tr_d_e) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > docume1935157360tr_d_e > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_60, type, put_M_1789706523_h_i_l: (docume1935157360tr_d_e > ((element_ptr_a > element_ptr_a) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > element_ptr_a > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_61, type, put_M_139724992_h_i_l: (docume1935157360tr_d_e > ((list_n282880152tr_b_c > list_n282880152tr_b_c) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > list_n282880152tr_b_c > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_62, type, put_M_257417239_h_i_l: (docume1935157360tr_d_e > ((list_char > list_char) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > list_char > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_63, type, put_M_1442125025_h_i_l: (docume1935157360tr_d_e > ((option_element_ptr_a > option_element_ptr_a) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > option_element_ptr_a > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_64, type, put_M_1656033077_h_i_l: (docume1935157360tr_d_e > ((product_unit > product_unit) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > product_unit > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_65, type, put_M_674497586_h_i_l: (docume1935157360tr_d_e > ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > m > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_66, type, put_M_168144691_h_i_l: (docume1935157360tr_d_e > ((n > n) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > n > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_67, type, cast_d1608273229_b_c_f: (docume1935157360tr_d_e > object945351580_d_e_f)).
% 0.73/0.50 thf(func_def_68, type, is_doc2037328342tr_d_e: (docume1935157360tr_d_e > $o)).
% 0.73/0.50 thf(func_def_69, type, is_doc45233057_d_e_f: (object945351580_d_e_f > $o)).
% 0.73/0.50 thf(func_def_70, type, attrs_1151927177tion_g: (rObjec1875798643tion_g > finite1621822014t_char)).
% 0.73/0.50 thf(func_def_71, type, attrs_1280717024tion_g: ((finite1621822014t_char > finite1621822014t_char) > rObjec1875798643tion_g > rObjec1875798643tion_g)).
% 0.73/0.50 thf(func_def_72, type, child_768225874tion_g: (rObjec1875798643tion_g > list_n282880152tr_b_c)).
% 0.73/0.50 thf(func_def_73, type, child_1596411111tion_g: ((list_n282880152tr_b_c > list_n282880152tr_b_c) > rObjec1875798643tion_g > rObjec1875798643tion_g)).
% 0.73/0.50 thf(func_def_74, type, shadow1820683706tion_g: (rObjec1875798643tion_g > option147517124_ptr_d)).
% 0.73/0.50 thf(func_def_75, type, shadow1606659473tion_g: ((option147517124_ptr_d > option147517124_ptr_d) > rObjec1875798643tion_g > rObjec1875798643tion_g)).
% 0.73/0.50 thf(func_def_76, type, tag_na866435078tion_g: (rObjec1875798643tion_g > list_char)).
% 0.73/0.50 thf(func_def_77, type, tag_na7058269tion_g: ((list_char > list_char) > rObjec1875798643tion_g > rObjec1875798643tion_g)).
% 0.73/0.50 thf(func_def_78, type, cast_E1779426770on_h_i: (rObjec1875798643tion_g > rObjec1922030987on_h_i)).
% 0.73/0.50 thf(func_def_79, type, cast_N1424394706on_h_i: (rObjec1922030987on_h_i > option392980921tion_g)).
% 0.73/0.50 thf(func_def_80, type, get_E_312738192_j_k_l: (element_ptr_a > heap_S1465075775_j_k_l > option392980921tion_g)).
% 0.73/0.50 thf(func_def_81, type, l_type85280056_j_k_l: (heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_82, type, put_E_1775770377_j_k_l: (element_ptr_a > rObjec1875798643tion_g > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l)).
% 0.73/0.50 thf(func_def_83, type, type_w697503069_j_k_l: (heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_84, type, get_M_650077447_j_k_l: (element_ptr_a > (rObjec1875798643tion_g > docume1935157360tr_d_e) > heap_E1188946203tr_d_e)).
% 0.73/0.50 thf(func_def_85, type, get_M_1338284716_j_k_l: (element_ptr_a > (rObjec1875798643tion_g > element_ptr_a) > heap_E1661210526_ptr_a)).
% 0.73/0.50 thf(func_def_86, type, get_M_685446945_j_k_l: (element_ptr_a > (rObjec1875798643tion_g > finite1621822014t_char) > heap_E1770015209t_char)).
% 0.73/0.50 thf(func_def_87, type, get_M_88885319_j_k_l: (element_ptr_a > (rObjec1875798643tion_g > list_n282880152tr_b_c) > heap_E1735400259tr_b_c)).
% 0.73/0.50 thf(func_def_88, type, get_M_51280086_j_k_l: (element_ptr_a > (rObjec1875798643tion_g > list_char) > heap_E434560396t_char)).
% 0.73/0.50 thf(func_def_89, type, get_M_1154267419_j_k_l: (element_ptr_a > (rObjec1875798643tion_g > option147517124_ptr_d) > heap_E189844335_ptr_d)).
% 0.73/0.50 thf(func_def_90, type, get_M_1238860946_j_k_l: (element_ptr_a > (rObjec1875798643tion_g > product_unit) > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_91, type, get_M_220285781_j_k_l: (element_ptr_a > (rObjec1875798643tion_g > m) > heap_E826424501tion_m)).
% 0.73/0.50 thf(func_def_92, type, get_M_90096148_j_k_l: (element_ptr_a > (rObjec1875798643tion_g > n) > heap_E834686006tion_n)).
% 0.73/0.50 thf(func_def_93, type, l_new_540233301_j_k_l: ((heap_S1465075775_j_k_l > $o) > $o)).
% 0.73/0.50 thf(func_def_94, type, new_el717272935_j_k_l: heap_E1661210526_ptr_a).
% 0.73/0.50 thf(func_def_95, type, put_M_1236788814_j_k_l: (element_ptr_a > ((docume1935157360tr_d_e > docume1935157360tr_d_e) > rObjec1875798643tion_g > rObjec1875798643tion_g) > docume1935157360tr_d_e > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_96, type, put_M_1198351521_j_k_l: (element_ptr_a > ((element_ptr_a > element_ptr_a) > rObjec1875798643tion_g > rObjec1875798643tion_g) > element_ptr_a > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_97, type, put_M_1724091798_j_k_l: (element_ptr_a > ((finite1621822014t_char > finite1621822014t_char) > rObjec1875798643tion_g > rObjec1875798643tion_g) > finite1621822014t_char > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_98, type, put_M_1098917052_j_k_l: (element_ptr_a > ((list_n282880152tr_b_c > list_n282880152tr_b_c) > rObjec1875798643tion_g > rObjec1875798643tion_g) > list_n282880152tr_b_c > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_99, type, put_M_1720094109_j_k_l: (element_ptr_a > ((list_char > list_char) > rObjec1875798643tion_g > rObjec1875798643tion_g) > list_char > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_100, type, put_M_682984464_j_k_l: (element_ptr_a > ((option147517124_ptr_d > option147517124_ptr_d) > rObjec1875798643tion_g > rObjec1875798643tion_g) > option147517124_ptr_d > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_101, type, put_M_1101791239_j_k_l: (element_ptr_a > ((product_unit > product_unit) > rObjec1875798643tion_g > rObjec1875798643tion_g) > product_unit > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_102, type, put_M_1862598346_j_k_l: (element_ptr_a > ((m > m) > rObjec1875798643tion_g > rObjec1875798643tion_g) > m > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_103, type, put_M_2120900233_j_k_l: (element_ptr_a > ((n > n) > rObjec1875798643tion_g > rObjec1875798643tion_g) > n > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_104, type, cast_e316309897tr_b_c: (element_ptr_a > node_p1234578834tr_b_c)).
% 0.73/0.50 thf(func_def_105, type, cast_n269450313tr_b_c: (node_p1234578834tr_b_c > option_element_ptr_a)).
% 0.73/0.50 thf(func_def_106, type, is_ele1129207902_t_r_a: (element_ptr_a > $o)).
% 0.73/0.50 thf(func_def_107, type, is_ele1259807012tr_b_c: (node_p1234578834tr_b_c > $o)).
% 0.73/0.50 thf(func_def_108, type, finite2103212841t_char: finite1621822014t_char).
% 0.73/0.50 thf(func_def_109, type, heap_E1613639261eption: heap_E625070648t_unit).
% 0.73/0.50 thf(func_def_110, type, heap_E808638982tr_d_e: (heap_E1188946203tr_d_e > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_111, type, heap_E73132893_ptr_a: (heap_E1661210526_ptr_a > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_112, type, heap_E1521571831t_unit: (heap_E625070648t_unit > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_113, type, heap_E1683112692tion_m: (heap_E826424501tion_m > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_114, type, heap_E1683112693tion_n: (heap_E834686006tion_n > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_115, type, heap_E1876089495eption: (heap_S1465075775_j_k_l > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_116, type, heap_E1982034951_ptr_b: (heap_S1465075775_j_k_l > heap_E1996099391_ptr_b > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_117, type, heap_E2046843837tr_d_e: (heap_S1465075775_j_k_l > heap_E1188946203tr_d_e > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_118, type, heap_E24690662_ptr_a: (heap_S1465075775_j_k_l > heap_E1661210526_ptr_a > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_119, type, heap_E494191872t_unit: (heap_S1465075775_j_k_l > heap_E625070648t_unit > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_120, type, heap_E1553005821tion_m: (heap_S1465075775_j_k_l > heap_E826424501tion_m > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_121, type, heap_E1553005822tion_n: (heap_S1465075775_j_k_l > heap_E834686006tion_n > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_122, type, heap_E1554207190_ptr_b: (heap_S1465075775_j_k_l > heap_E1996099391_ptr_b > character_data_ptr_b > $o)).
% 0.73/0.50 thf(func_def_123, type, heap_E2101731758tr_d_e: (heap_S1465075775_j_k_l > heap_E1188946203tr_d_e > docume1935157360tr_d_e > $o)).
% 0.73/0.50 thf(func_def_124, type, heap_E1224694197_ptr_a: (heap_S1465075775_j_k_l > heap_E1661210526_ptr_a > element_ptr_a > $o)).
% 0.73/0.50 thf(func_def_125, type, heap_E946351744t_char: (heap_S1465075775_j_k_l > heap_E1770015209t_char > finite1621822014t_char > $o)).
% 0.73/0.50 thf(func_def_126, type, heap_E258692314tr_b_c: (heap_S1465075775_j_k_l > heap_E1735400259tr_b_c > list_n282880152tr_b_c > $o)).
% 0.73/0.50 thf(func_def_127, type, heap_E804379039t_char: (heap_S1465075775_j_k_l > heap_E434560396t_char > list_char > $o)).
% 0.73/0.50 thf(func_def_128, type, heap_E1091541499_ptr_a: (heap_S1465075775_j_k_l > heap_E906991588_ptr_a > option_element_ptr_a > $o)).
% 0.73/0.50 thf(func_def_129, type, heap_E1947147782_ptr_d: (heap_S1465075775_j_k_l > heap_E189844335_ptr_d > option147517124_ptr_d > $o)).
% 0.73/0.50 thf(func_def_130, type, heap_E667013711t_unit: (heap_S1465075775_j_k_l > heap_E625070648t_unit > product_unit > $o)).
% 0.73/0.50 thf(func_def_131, type, heap_E1038710092tion_m: (heap_S1465075775_j_k_l > heap_E826424501tion_m > m > $o)).
% 0.73/0.50 thf(func_def_132, type, heap_E1038710093tion_n: (heap_S1465075775_j_k_l > heap_E834686006tion_n > n > $o)).
% 0.73/0.50 thf(func_def_133, type, heap_E1679280842_ptr_b: (heap_S1465075775_j_k_l > heap_E1996099391_ptr_b > character_data_ptr_b > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_134, type, heap_E1720378810tr_d_e: (heap_S1465075775_j_k_l > heap_E1188946203tr_d_e > docume1935157360tr_d_e > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_135, type, heap_E2092016297_ptr_a: (heap_S1465075775_j_k_l > heap_E1661210526_ptr_a > element_ptr_a > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_136, type, heap_E1993614659t_unit: (heap_S1465075775_j_k_l > heap_E625070648t_unit > product_unit > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_137, type, heap_E1940720704tion_m: (heap_S1465075775_j_k_l > heap_E826424501tion_m > m > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_138, type, heap_E1940720705tion_n: (heap_S1465075775_j_k_l > heap_E834686006tion_n > n > heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_139, type, nil_no279930520tr_b_c: list_n282880152tr_b_c).
% 0.73/0.50 thf(func_def_140, type, nil_char: list_char).
% 0.73/0.50 thf(func_def_141, type, cast_N1183075319_j_k_l: (rObjec1922030987on_h_i > rObjec1413572695_j_k_l)).
% 0.73/0.50 thf(func_def_142, type, cast_O1705702135_j_k_l: (rObjec1413572695_j_k_l > option1128016977on_h_i)).
% 0.73/0.50 thf(func_def_143, type, type_w2078707819_j_k_l: (heap_S1465075775_j_k_l > $o)).
% 0.73/0.50 thf(func_def_144, type, get_M_1644669866_j_k_l: (node_p1234578834tr_b_c > (rObjec1922030987on_h_i > n) > heap_E834686006tion_n)).
% 0.73/0.50 thf(func_def_145, type, cast_n552817316_d_e_f: (node_p1234578834tr_b_c > object945351580_d_e_f)).
% 0.73/0.50 thf(func_def_146, type, cast_o664948310_d_e_f: (object945351580_d_e_f > option1344508504tr_b_c)).
% 0.73/0.50 thf(func_def_147, type, put_O_834343516_j_k_l: (object945351580_d_e_f > rObjec1413572695_j_k_l > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l)).
% 0.73/0.50 thf(func_def_148, type, get_M_421785767_k_l_n: (object945351580_d_e_f > (rObjec1413572695_j_k_l > n) > heap_E834686006tion_n)).
% 0.73/0.50 thf(func_def_149, type, none_element_ptr_a: option_element_ptr_a).
% 0.73/0.50 thf(func_def_150, type, none_R1587534007on_j_k: option841825948on_j_k).
% 0.73/0.50 thf(func_def_151, type, none_R125524722tion_j: option1029218147tion_j).
% 0.73/0.50 thf(func_def_152, type, none_R417230014tion_h: option849832995tion_h).
% 0.73/0.50 thf(func_def_153, type, none_R509380180tion_g: option392980921tion_g).
% 0.73/0.50 thf(func_def_154, type, none_s1706699231_ptr_d: option147517124_ptr_d).
% 0.73/0.50 thf(func_def_155, type, some_c586507257_ptr_b: (character_data_ptr_b > option2061924698_ptr_b)).
% 0.73/0.50 thf(func_def_156, type, some_element_ptr_a: (element_ptr_a > option_element_ptr_a)).
% 0.73/0.50 thf(func_def_157, type, some_R67702331on_j_k: (rObjec1617416918on_j_k > option841825948on_j_k)).
% 0.73/0.50 thf(func_def_158, type, some_R700141678tion_j: (rObjec2068690451tion_j > option1029218147tion_j)).
% 0.73/0.50 thf(func_def_159, type, case_o876177157tr_b_c: ($o > (node_p1234578834tr_b_c > $o) > option1344508504tr_b_c > $o)).
% 0.73/0.50 thf(func_def_160, type, case_o1030391776tion_j: ($o > (rObjec2068690451tion_j > $o) > option1029218147tion_j > $o)).
% 0.73/0.50 thf(func_def_161, type, case_o18599603on_h_i: (option849832995tion_h > (rObjec1922030987on_h_i > option849832995tion_h) > option1128016977on_h_i > option849832995tion_h)).
% 0.73/0.50 thf(func_def_162, type, case_o1144239773on_h_i: (option392980921tion_g > (rObjec1922030987on_h_i > option392980921tion_g) > option1128016977on_h_i > option392980921tion_g)).
% 0.73/0.50 thf(func_def_163, type, the_ch963454248_ptr_b: (option2061924698_ptr_b > character_data_ptr_b)).
% 0.73/0.50 thf(func_def_164, type, the_element_ptr_a: (option_element_ptr_a > element_ptr_a)).
% 0.73/0.50 thf(func_def_165, type, the_RO2055010943tion_j: (option1029218147tion_j > rObjec2068690451tion_j)).
% 0.73/0.50 thf(func_def_166, type, cast_D1046746849_b_j_k: (rObjec1617416918on_j_k > option1029218147tion_j)).
% 0.73/0.50 thf(func_def_167, type, cast_S988036065_b_j_k: (rObjec2068690451tion_j > rObjec1617416918on_j_k)).
% 0.73/0.50 thf(func_def_168, type, is_sha1522929624_b_j_k: (rObjec1617416918on_j_k > $o)).
% 0.73/0.50 thf(func_def_169, type, shadow1068876397_i_k_l: (shadow_root_ptr_d > (rObjec2068690451tion_j > docume1935157360tr_d_e) > heap_E1188946203tr_d_e)).
% 0.73/0.50 thf(func_def_170, type, shadow902827384_i_k_l: (shadow_root_ptr_d > (rObjec2068690451tion_j > element_ptr_a) > heap_E1661210526_ptr_a)).
% 0.73/0.50 thf(func_def_171, type, shadow2050000606_i_k_l: (shadow_root_ptr_d > (rObjec2068690451tion_j > product_unit) > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_172, type, shadow1194684833_i_k_l: (shadow_root_ptr_d > (rObjec2068690451tion_j > m) > heap_E826424501tion_m)).
% 0.73/0.50 thf(func_def_173, type, shadow569799008_i_k_l: (shadow_root_ptr_d > (rObjec2068690451tion_j > n) > heap_E834686006tion_n)).
% 0.73/0.50 thf(func_def_174, type, shadow1464843188_i_k_l: (shadow_root_ptr_d > ((docume1935157360tr_d_e > docume1935157360tr_d_e) > rObjec2068690451tion_j > rObjec2068690451tion_j) > docume1935157360tr_d_e > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_175, type, shadow2015416421_i_k_l: (shadow_root_ptr_d > ((element_ptr_a > element_ptr_a) > rObjec2068690451tion_j > rObjec2068690451tion_j) > element_ptr_a > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_176, type, shadow1110190411_i_k_l: (shadow_root_ptr_d > ((product_unit > product_unit) > rObjec2068690451tion_j > rObjec2068690451tion_j) > product_unit > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_177, type, shadow1030535182_i_k_l: (shadow_root_ptr_d > ((m > m) > rObjec2068690451tion_j > rObjec2068690451tion_j) > m > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_178, type, shadow1843699917_i_k_l: (shadow_root_ptr_d > ((n > n) > rObjec2068690451tion_j > rObjec2068690451tion_j) > n > heap_E625070648t_unit)).
% 0.73/0.50 thf(func_def_179, type, cast_s253715760_r_d_e: (shadow_root_ptr_d > docume1935157360tr_d_e)).
% 0.73/0.50 thf(func_def_180, type, document_ptr: docume1935157360tr_d_e).
% 0.73/0.50 thf(func_def_181, type, getter: (rObjec2068690451tion_j > n)).
% 0.73/0.50 thf(func_def_182, type, h: heap_S1465075775_j_k_l).
% 0.73/0.50 thf(func_def_183, type, h2: heap_S1465075775_j_k_l).
% 0.73/0.50 thf(func_def_184, type, setter: ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k)).
% 0.73/0.50 thf(func_def_185, type, shadow_root_ptr: shadow_root_ptr_d).
% 0.73/0.50 thf(func_def_186, type, v: m).
% 0.73/0.50 thf(func_def_188, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.73/0.50 thf(func_def_191, type, db0: !>[X0: $tType]:(X0)).
% 0.73/0.50 thf(func_def_192, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.73/0.50 thf(func_def_193, type, vNOT: ($o > $o)).
% 0.73/0.50 thf(func_def_194, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.73/0.50 thf(func_def_195, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.73/0.51 thf(func_def_196, type, db1: !>[X0: $tType]:(X0)).
% 0.73/0.51 thf(func_def_197, type, vAND: ($o > $o > $o)).
% 0.73/0.51 thf(func_def_198, type, db3: !>[X0: $tType]:(X0)).
% 0.73/0.51 thf(func_def_199, type, db2: !>[X0: $tType]:(X0)).
% 0.73/0.51 thf(func_def_200, type, vOR: ($o > $o > $o)).
% 0.73/0.51 thf(func_def_201, type, vIMP: ($o > $o > $o)).
% 0.73/0.51 thf(func_def_202, type, sP0: ((option1029218147tion_j > option1029218147tion_j > $o) > option1029218147tion_j > option1029218147tion_j > $o)).
% 0.73/0.51 thf(func_def_203, type, sK1: ((rObjec2068690451tion_j > n) > ((n > n) > rObjec2068690451tion_j > rObjec2068690451tion_j) > n > rObjec2068690451tion_j)).
% 0.73/0.51 thf(func_def_204, type, sK2: (((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > m > (rObjec1617416918on_j_k > n) > rObjec1617416918on_j_k)).
% 0.73/0.51 thf(func_def_205, type, sK3: ((option1029218147tion_j > $o) > rObjec2068690451tion_j)).
% 0.73/0.51 thf(func_def_206, type, sK4: (n > ((n > n) > rObjec2068690451tion_j > rObjec2068690451tion_j) > (rObjec2068690451tion_j > n) > rObjec2068690451tion_j)).
% 0.73/0.51 thf(func_def_207, type, sK5: (option1029218147tion_j > rObjec2068690451tion_j)).
% 0.73/0.51 thf(func_def_208, type, sK6: (m > ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > (rObjec1413572695_j_k_l > n) > rObjec1617416918on_j_k)).
% 0.73/0.51 thf(func_def_209, type, sK7: (n > ((n > n) > rObjec2068690451tion_j > rObjec2068690451tion_j) > (rObjec1413572695_j_k_l > n) > rObjec2068690451tion_j)).
% 0.73/0.51 thf(func_def_210, type, sK8: ((rObjec1617416918on_j_k > n) > n > ((n > n) > rObjec2068690451tion_j > rObjec2068690451tion_j) > rObjec2068690451tion_j)).
% 0.73/0.51 thf(func_def_211, type, sK9: ((rObjec1617416918on_j_k > m) > ((n > n) > rObjec2068690451tion_j > rObjec2068690451tion_j) > n > rObjec2068690451tion_j)).
% 0.73/0.51 thf(func_def_212, type, sK10: (m > (rObjec1617416918on_j_k > m) > ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > rObjec1617416918on_j_k)).
% 0.73/0.51 thf(func_def_213, type, sK11: (((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > (rObjec1617416918on_j_k > m) > m > rObjec1617416918on_j_k)).
% 0.73/0.51 thf(func_def_214, type, sK12: (((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k) > m > (rObjec1413572695_j_k_l > n) > rObjec1617416918on_j_k)).
% 0.73/0.51 thf(func_def_215, type, sK13: ((option1029218147tion_j > option1029218147tion_j > $o) > option1029218147tion_j > option1029218147tion_j > rObjec2068690451tion_j)).
% 0.73/0.51 thf(func_def_216, type, sK14: ((option1029218147tion_j > option1029218147tion_j > $o) > option1029218147tion_j > option1029218147tion_j > rObjec2068690451tion_j)).
% 0.73/0.51 thf(f5,axiom,(
% 0.73/0.51 ! [X0 : shadow_root_ptr_d,X6 : (rObjec2068690451tion_j > n),X2 : heap_S1465075775_j_k_l,X1 : docume1935157360tr_d_e,X5 : heap_S1465075775_j_k_l,X4 : m,X3 : ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k)] : ((((cast_s253715760_r_d_e @ X0)) != X1) => ((heap_E494191872t_unit @ X2 @ (put_M_674497586_h_i_l @ X1 @ X3 @ X4) @ X5) => (heap_E1683112693tion_n @ (shadow569799008_i_k_l @ X0 @ X6) @ X2 @ X5)))),
% 0.73/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_get__M__shadow__root__put__M__document__different__pointers)).
% 0.73/0.51 thf(f340,axiom,(
% 0.73/0.51 (heap_E494191872t_unit @ h @ (put_M_674497586_h_i_l @ document_ptr @ setter @ v) @ h2)),
% 0.73/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 0.73/0.51 thf(f343,axiom,(
% 0.73/0.51 (((cast_s253715760_r_d_e @ shadow_root_ptr)) != document_ptr)),
% 0.73/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_3)).
% 0.73/0.51 thf(f344,conjecture,(
% 0.73/0.51 (heap_E1683112693tion_n @ (shadow569799008_i_k_l @ shadow_root_ptr @ getter) @ h @ h2)),
% 0.73/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_4)).
% 0.73/0.51 thf(f345,negated_conjecture,(
% 0.73/0.51 ~(heap_E1683112693tion_n @ (shadow569799008_i_k_l @ shadow_root_ptr @ getter) @ h @ h2)),
% 0.73/0.51 inference(negated_conjecture,[status(cth)],[f344])).
% 0.73/0.51 thf(f405,plain,(
% 0.73/0.51 ~(heap_E1683112693tion_n @ (shadow569799008_i_k_l @ shadow_root_ptr @ getter) @ h @ h2)),
% 0.73/0.51 inference(rectify,[],[f345])).
% 0.73/0.51 thf(f406,plain,(
% 0.73/0.51 ~ (((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ shadow_root_ptr @ getter) @ h @ h2)) = $true)),
% 0.73/0.51 inference(fool_elimination,[],[f405])).
% 0.73/0.51 thf(f451,plain,(
% 0.73/0.51 (heap_E494191872t_unit @ h @ (put_M_674497586_h_i_l @ document_ptr @ setter @ v) @ h2)),
% 0.73/0.51 inference(rectify,[],[f340])).
% 0.73/0.51 thf(f452,plain,(
% 0.73/0.51 (((heap_E494191872t_unit @ h @ (put_M_674497586_h_i_l @ document_ptr @ setter @ v) @ h2)) = $true)),
% 0.73/0.51 inference(fool_elimination,[],[f451])).
% 0.73/0.51 thf(f610,plain,(
% 0.73/0.51 ! [X0 : shadow_root_ptr_d,X1 : (rObjec2068690451tion_j > n),X2 : heap_S1465075775_j_k_l,X3 : docume1935157360tr_d_e,X4 : heap_S1465075775_j_k_l,X5 : m,X6 : ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k)] : ((((cast_s253715760_r_d_e @ X0)) != X3) => ((heap_E494191872t_unit @ X2 @ (put_M_674497586_h_i_l @ X3 @ X6 @ X5) @ X4) => (heap_E1683112693tion_n @ (shadow569799008_i_k_l @ X0 @ X1) @ X2 @ X4)))),
% 0.73/0.51 inference(rectify,[],[f5])).
% 0.73/0.51 thf(f611,plain,(
% 0.73/0.51 ! [X0 : shadow_root_ptr_d,X3 : docume1935157360tr_d_e,X4 : heap_S1465075775_j_k_l,X6 : ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k),X1 : (rObjec2068690451tion_j > n),X5 : m,X2 : heap_S1465075775_j_k_l] : ((((cast_s253715760_r_d_e @ X0)) != X3) => ((((heap_E494191872t_unit @ X2 @ (put_M_674497586_h_i_l @ X3 @ X6 @ X5) @ X4)) = $true) => ($true = ((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ X0 @ X1) @ X2 @ X4)))))),
% 0.73/0.51 inference(fool_elimination,[],[f610])).
% 0.73/0.51 thf(f917,plain,(
% 0.73/0.51 (((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ shadow_root_ptr @ getter) @ h @ h2)) != $true)),
% 0.73/0.51 inference(flattening,[],[f406])).
% 0.73/0.51 thf(f931,plain,(
% 0.73/0.51 ! [X0 : shadow_root_ptr_d,X3 : docume1935157360tr_d_e,X4 : heap_S1465075775_j_k_l,X6 : ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k),X1 : (rObjec2068690451tion_j > n),X5 : m,X2 : heap_S1465075775_j_k_l] : ((($true = ((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ X0 @ X1) @ X2 @ X4))) | (((heap_E494191872t_unit @ X2 @ (put_M_674497586_h_i_l @ X3 @ X6 @ X5) @ X4)) != $true)) | (((cast_s253715760_r_d_e @ X0)) = X3))),
% 0.73/0.51 inference(ennf_transformation,[],[f611])).
% 0.73/0.51 thf(f932,plain,(
% 0.73/0.51 ! [X5 : m,X3 : docume1935157360tr_d_e,X6 : ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k),X4 : heap_S1465075775_j_k_l,X1 : (rObjec2068690451tion_j > n),X2 : heap_S1465075775_j_k_l,X0 : shadow_root_ptr_d] : (($true = ((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ X0 @ X1) @ X2 @ X4))) | (((cast_s253715760_r_d_e @ X0)) = X3) | (((heap_E494191872t_unit @ X2 @ (put_M_674497586_h_i_l @ X3 @ X6 @ X5) @ X4)) != $true))),
% 0.73/0.51 inference(flattening,[],[f931])).
% 0.73/0.51 thf(f1028,plain,(
% 0.73/0.51 ! [X0 : m,X1 : docume1935157360tr_d_e,X2 : ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k),X3 : heap_S1465075775_j_k_l,X4 : (rObjec2068690451tion_j > n),X5 : heap_S1465075775_j_k_l,X6 : shadow_root_ptr_d] : (($true = ((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ X6 @ X4) @ X5 @ X3))) | (((cast_s253715760_r_d_e @ X6)) = X1) | ($true != ((heap_E494191872t_unit @ X5 @ (put_M_674497586_h_i_l @ X1 @ X2 @ X0) @ X3))))),
% 0.73/0.51 inference(rectify,[],[f932])).
% 0.73/0.51 thf(f1054,plain,(
% 0.73/0.51 (((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ shadow_root_ptr @ getter) @ h @ h2)) != $true)),
% 0.73/0.51 inference(cnf_transformation,[],[f917])).
% 0.73/0.51 thf(f1080,plain,(
% 0.73/0.51 (document_ptr != ((cast_s253715760_r_d_e @ shadow_root_ptr)))),
% 0.73/0.51 inference(cnf_transformation,[],[f343])).
% 0.73/0.51 thf(f1083,plain,(
% 0.73/0.51 ( ! [X2 : ((m > m) > rObjec1617416918on_j_k > rObjec1617416918on_j_k),X3 : heap_S1465075775_j_k_l,X0 : m,X1 : docume1935157360tr_d_e,X6 : shadow_root_ptr_d,X4 : (rObjec2068690451tion_j > n),X5 : heap_S1465075775_j_k_l] : (($true != ((heap_E494191872t_unit @ X5 @ (put_M_674497586_h_i_l @ X1 @ X2 @ X0) @ X3))) | ($true = ((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ X6 @ X4) @ X5 @ X3))) | (((cast_s253715760_r_d_e @ X6)) = X1)) )),
% 0.73/0.51 inference(cnf_transformation,[],[f1028])).
% 0.73/0.51 thf(f1086,plain,(
% 0.73/0.51 (((heap_E494191872t_unit @ h @ (put_M_674497586_h_i_l @ document_ptr @ setter @ v) @ h2)) = $true)),
% 0.73/0.51 inference(cnf_transformation,[],[f452])).
% 0.73/0.51 thf(f1096,definition,(
% 0.73/0.51 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.73/0.51 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.73/0.51 thf(f1122,plain,(
% 0.73/0.51 (((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ shadow_root_ptr @ getter) @ h @ h2)) = $false) | ($true != $true)),
% 0.73/0.51 inference(superposition,[],[f1054,f1096])).
% 0.73/0.51 thf(f1123,plain,(
% 0.73/0.51 (((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ shadow_root_ptr @ getter) @ h @ h2)) = $false)),
% 0.73/0.51 inference(trivial_inequality_removal,[],[f1122])).
% 0.73/0.51 thf(f1147,plain,(
% 0.73/0.51 ( ! [X0 : shadow_root_ptr_d,X1 : (rObjec2068690451tion_j > n)] : ((((cast_s253715760_r_d_e @ X0)) = document_ptr) | ($true = ((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ X0 @ X1) @ h @ h2))) | ($true != $true)) )),
% 0.73/0.51 inference(superposition,[],[f1083,f1086])).
% 0.73/0.51 thf(f1153,plain,(
% 0.73/0.51 ( ! [X0 : shadow_root_ptr_d,X1 : (rObjec2068690451tion_j > n)] : (($true = ((heap_E1683112693tion_n @ (shadow569799008_i_k_l @ X0 @ X1) @ h @ h2))) | (((cast_s253715760_r_d_e @ X0)) = document_ptr)) )),
% 0.73/0.51 inference(trivial_inequality_removal,[],[f1147])).
% 0.73/0.51 thf(f1164,plain,(
% 0.73/0.51 ($true = $false) | (document_ptr = ((cast_s253715760_r_d_e @ shadow_root_ptr)))),
% 0.73/0.51 inference(superposition,[],[f1153,f1123])).
% 0.73/0.51 thf(f1167,plain,(
% 0.73/0.51 (document_ptr = ((cast_s253715760_r_d_e @ shadow_root_ptr)))),
% 0.73/0.51 inference(trivial_inequality_removal,[],[f1164])).
% 0.73/0.51 thf(f1170,plain,(
% 0.73/0.51 $false),
% 0.73/0.51 inference(forward_subsumption_resolution,[],[f1167,f1080])).
% 0.73/0.51 % SZS output end Proof for theBenchmark
% 0.73/0.51 % (2139846)------------------------------
% 0.73/0.51 % (2139846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.73/0.51 % (2139846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.73/0.51 % (2139846)CaDiCaL version: 2.1.3
% 0.73/0.51 % (2139846)Termination reason: Refutation
% 0.73/0.51 % (2139846)Time elapsed: 0.024 s
% 0.73/0.51 % (2139846)Peak memory usage: 14 MB
% 0.73/0.51 % (2139846)Instructions burned: 96 (million)
% 0.73/0.51 % (2139773)Success in time 0.14 s
% 0.73/0.51 % Vampire exiting
%------------------------------------------------------------------------------