%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP171^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 1.72s 0.84s
% Output : Refutation 1.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP171^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n009.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 20:05:45 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running higher-order theorem proving
% 0.41/0.49 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.65/0.68 % (290691)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.65/0.68 % (290700)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2389863192:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.65/0.68 % (290702)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.65/0.68 % (290702)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.65/0.68 % (290700)Instruction limit reached!
% 0.65/0.68 % (290700)------------------------------
% 0.65/0.68 % (290700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.65/0.68 % (290700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.68 % (290700)CaDiCaL version: 2.1.3
% 0.65/0.68 % (290700)Termination reason: Instruction limit
% 0.65/0.68 % (290700)Termination phase: shuffling
% 0.65/0.68 % (290700)Time elapsed: 0.006 s
% 0.65/0.68 % (290700)Peak memory usage: 11 MB
% 0.65/0.68 % (290700)Instructions burned: 25 (million)
% 0.65/0.68 % (290697)lrs+10_16_si=on:nwc=1.5:random_seed=68425412:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.65/0.68 % (290696)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3164971183:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.65/0.68 % (290698)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1340920956:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.65/0.68 % (290699)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=796996649: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.65/0.68 % (290701)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3365001261:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.65/0.68 % (290702)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=3779638337:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.65/0.68 % (290698)Instruction limit reached!
% 0.65/0.68 % (290698)------------------------------
% 0.65/0.68 % (290698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.65/0.68 % (290698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.68 % (290698)CaDiCaL version: 2.1.3
% 0.65/0.68 % (290698)Termination reason: Instruction limit
% 0.65/0.68 % (290698)Termination phase: shuffling
% 0.65/0.68 % (290698)Time elapsed: 0.002 s
% 0.65/0.68 % (290698)Peak memory usage: 10 MB
% 0.65/0.68 % (290698)Instructions burned: 4 (million)
% 0.65/0.68 % (290697)Instruction limit reached!
% 0.65/0.68 % (290697)------------------------------
% 0.65/0.68 % (290697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.65/0.68 % (290697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.68 % (290697)CaDiCaL version: 2.1.3
% 0.65/0.68 % (290697)Termination reason: Instruction limit
% 0.65/0.68 % (290697)Termination phase: shuffling
% 0.65/0.68 % (290697)Time elapsed: 0.010 s
% 0.65/0.68 % (290697)Peak memory usage: 11 MB
% 0.65/0.68 % (290697)Instructions burned: 20 (million)
% 0.65/0.68 % (290705)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=321577433:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.65/0.68 % (290705)Instruction limit reached!
% 0.65/0.68 % (290705)------------------------------
% 0.65/0.68 % (290705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.65/0.68 % (290705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.68 % (290705)CaDiCaL version: 2.1.3
% 0.65/0.68 % (290705)Termination reason: Instruction limit
% 0.65/0.68 % (290705)Termination phase: shuffling
% 0.65/0.68 % (290705)Time elapsed: 0.002 s
% 0.65/0.68 % (290705)Peak memory usage: 10 MB
% 0.65/0.68 % (290705)Instructions burned: 6 (million)
% 0.65/0.68 % (290711)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3402134820:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2998 on theBenchmark for (2998ds/5Mi)
% 0.65/0.68 % (290714)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=25746653:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/12Mi)
% 1.14/0.72 % (290712)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.14/0.72 % (290711)Instruction limit reached!
% 1.14/0.72 % (290711)------------------------------
% 1.14/0.72 % (290711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.72 % (290711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.72 % (290711)CaDiCaL version: 2.1.3
% 1.14/0.72 % (290711)Termination reason: Instruction limit
% 1.14/0.72 % (290711)Termination phase: shuffling
% 1.14/0.72 % (290711)Time elapsed: 0.003 s
% 1.14/0.72 % (290711)Peak memory usage: 10 MB
% 1.14/0.72 % (290711)Instructions burned: 5 (million)
% 1.14/0.72 % (290714)Instruction limit reached!
% 1.14/0.72 % (290714)------------------------------
% 1.14/0.72 % (290714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.72 % (290714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.72 % (290714)CaDiCaL version: 2.1.3
% 1.14/0.72 % (290714)Termination reason: Instruction limit
% 1.14/0.72 % (290714)Termination phase: shuffling
% 1.14/0.72 % (290714)Time elapsed: 0.004 s
% 1.14/0.72 % (290714)Peak memory usage: 11 MB
% 1.14/0.72 % (290714)Instructions burned: 16 (million)
% 1.14/0.72 % (290712)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1776505411:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.14/0.72 % (290712)Instruction limit reached!
% 1.14/0.72 % (290712)------------------------------
% 1.14/0.72 % (290712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.72 % (290712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.72 % (290712)CaDiCaL version: 2.1.3
% 1.14/0.72 % (290712)Termination reason: Instruction limit
% 1.14/0.72 % (290712)Termination phase: shuffling
% 1.14/0.72 % (290712)Time elapsed: 0.004 s
% 1.14/0.72 % (290712)Peak memory usage: 10 MB
% 1.14/0.72 % (290712)Instructions burned: 7 (million)
% 1.14/0.72 % (290701)Instruction limit reached!
% 1.14/0.72 % (290701)------------------------------
% 1.14/0.72 % (290701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.72 % (290701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.72 % (290701)CaDiCaL version: 2.1.3
% 1.14/0.72 % (290701)Termination reason: Instruction limit
% 1.14/0.72 % (290701)Termination phase: shuffling
% 1.14/0.72 % (290701)Time elapsed: 0.034 s
% 1.14/0.72 % (290701)Peak memory usage: 12 MB
% 1.14/0.72 % (290701)Instructions burned: 75 (million)
% 1.14/0.72 % (290696)Instruction limit reached!
% 1.14/0.72 % (290696)------------------------------
% 1.14/0.72 % (290696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.72 % (290696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.72 % (290696)CaDiCaL version: 2.1.3
% 1.14/0.72 % (290696)Termination reason: Instruction limit
% 1.14/0.72 % (290696)Termination phase: shuffling
% 1.14/0.72 % (290696)Time elapsed: 0.039 s
% 1.14/0.72 % (290696)Peak memory usage: 12 MB
% 1.14/0.72 % (290696)Instructions burned: 89 (million)
% 1.14/0.72 % (290718)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=3256395792:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.14/0.72 % (290717)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
% 1.14/0.72 % (290717)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.14/0.72 % (290717)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1370394026:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2998 on theBenchmark for (2998ds/28Mi)
% 1.14/0.72 % (290721)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.14/0.72 % (290720)lrs+10_1_si=on:cs=on:random_seed=3476887684:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.14/0.72 % (290721)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=3256316165:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.14/0.75 % (290721)Instruction limit reached!
% 1.14/0.75 % (290721)------------------------------
% 1.14/0.75 % (290721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.75 % (290721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.75 % (290721)CaDiCaL version: 2.1.3
% 1.14/0.75 % (290721)Termination reason: Instruction limit
% 1.14/0.75 % (290721)Termination phase: shuffling
% 1.14/0.75 % (290721)Time elapsed: 0.002 s
% 1.14/0.75 % (290721)Peak memory usage: 10 MB
% 1.14/0.75 % (290721)Instructions burned: 3 (million)
% 1.14/0.75 % (290720)Instruction limit reached!
% 1.14/0.75 % (290720)------------------------------
% 1.14/0.75 % (290720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.75 % (290720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.75 % (290720)CaDiCaL version: 2.1.3
% 1.14/0.75 % (290720)Termination reason: Instruction limit
% 1.14/0.75 % (290720)Termination phase: shuffling
% 1.14/0.75 % (290720)Time elapsed: 0.004 s
% 1.14/0.75 % (290720)Peak memory usage: 10 MB
% 1.14/0.75 % (290720)Instructions burned: 8 (million)
% 1.14/0.75 % (290723)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=720770556:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.14/0.75 % (290717)Instruction limit reached!
% 1.14/0.75 % (290717)------------------------------
% 1.14/0.75 % (290717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.75 % (290717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.75 % (290717)CaDiCaL version: 2.1.3
% 1.14/0.75 % (290717)Termination reason: Instruction limit
% 1.14/0.75 % (290717)Termination phase: shuffling
% 1.14/0.75 % (290717)Time elapsed: 0.014 s
% 1.14/0.75 % (290717)Peak memory usage: 11 MB
% 1.14/0.75 % (290717)Instructions burned: 29 (million)
% 1.14/0.75 % (290718)Instruction limit reached!
% 1.14/0.75 % (290718)------------------------------
% 1.14/0.75 % (290718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.75 % (290718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.75 % (290718)CaDiCaL version: 2.1.3
% 1.14/0.75 % (290718)Termination reason: Instruction limit
% 1.14/0.75 % (290718)Termination phase: shuffling
% 1.14/0.75 % (290718)Time elapsed: 0.022 s
% 1.14/0.75 % (290718)Peak memory usage: 12 MB
% 1.14/0.75 % (290718)Instructions burned: 89 (million)
% 1.14/0.75 % (290702)Instruction limit reached!
% 1.14/0.75 % (290702)------------------------------
% 1.14/0.75 % (290702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.75 % (290702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.75 % (290702)CaDiCaL version: 2.1.3
% 1.14/0.75 % (290702)Termination reason: Instruction limit
% 1.14/0.75 % (290702)Termination phase: shuffling
% 1.14/0.75 % (290702)Time elapsed: 0.068 s
% 1.14/0.75 % (290702)Peak memory usage: 14 MB
% 1.14/0.75 % (290702)Instructions burned: 159 (million)
% 1.14/0.75 % (290731)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=987655292:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.14/0.75 % (290727)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=886979864:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.14/0.75 % (290728)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1917773177:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.14/0.75 % (290723)Instruction limit reached!
% 1.14/0.75 % (290723)------------------------------
% 1.14/0.75 % (290723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.75 % (290723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.75 % (290723)CaDiCaL version: 2.1.3
% 1.14/0.75 % (290723)Termination reason: Instruction limit
% 1.14/0.75 % (290723)Termination phase: shuffling
% 1.14/0.75 % (290723)Time elapsed: 0.018 s
% 1.14/0.75 % (290723)Peak memory usage: 11 MB
% 1.14/0.75 % (290723)Instructions burned: 40 (million)
% 1.14/0.75 % (290730)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=4166382012:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.14/0.80 % (290730)Instruction limit reached!
% 1.14/0.80 % (290730)------------------------------
% 1.14/0.80 % (290730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.80 % (290730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.80 % (290730)CaDiCaL version: 2.1.3
% 1.14/0.80 % (290730)Termination reason: Instruction limit
% 1.14/0.80 % (290730)Termination phase: shuffling
% 1.14/0.80 % (290730)Time elapsed: 0.007 s
% 1.14/0.80 % (290730)Peak memory usage: 11 MB
% 1.14/0.80 % (290730)Instructions burned: 14 (million)
% 1.14/0.80 % (290728)Instruction limit reached!
% 1.14/0.80 % (290728)------------------------------
% 1.14/0.80 % (290728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.80 % (290732)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2370739271:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.14/0.80 % (290728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.80 % (290728)CaDiCaL version: 2.1.3
% 1.14/0.80 % (290728)Termination reason: Instruction limit
% 1.14/0.80 % (290728)Termination phase: shuffling
% 1.14/0.80 % (290728)Time elapsed: 0.012 s
% 1.14/0.80 % (290728)Peak memory usage: 11 MB
% 1.14/0.80 % (290728)Instructions burned: 26 (million)
% 1.14/0.80 % (290736)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=905961369:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.14/0.80 % (290732)Instruction limit reached!
% 1.14/0.80 % (290732)------------------------------
% 1.14/0.80 % (290732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.80 % (290732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.80 % (290732)CaDiCaL version: 2.1.3
% 1.14/0.80 % (290732)Termination reason: Instruction limit
% 1.14/0.80 % (290732)Termination phase: shuffling
% 1.14/0.80 % (290732)Time elapsed: 0.007 s
% 1.14/0.80 % (290732)Peak memory usage: 11 MB
% 1.14/0.80 % (290732)Instructions burned: 15 (million)
% 1.14/0.80 % (290736)Instruction limit reached!
% 1.14/0.80 % (290736)------------------------------
% 1.14/0.80 % (290736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.80 % (290736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.80 % (290736)CaDiCaL version: 2.1.3
% 1.14/0.80 % (290736)Termination reason: Instruction limit
% 1.14/0.80 % (290736)Termination phase: shuffling
% 1.14/0.80 % (290736)Time elapsed: 0.002 s
% 1.14/0.80 % (290736)Peak memory usage: 10 MB
% 1.14/0.80 % (290736)Instructions burned: 3 (million)
% 1.14/0.80 % (290738)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2393762510:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.14/0.80 % (290740)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1081713919:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.14/0.80 % (290743)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.14/0.80 % (290743)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.14/0.80 % (290742)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=4131605033:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.14/0.80 % (290743)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=4105825540:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.14/0.80 % (290738)Instruction limit reached!
% 1.14/0.80 % (290738)------------------------------
% 1.14/0.80 % (290738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.80 % (290738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.80 % (290738)CaDiCaL version: 2.1.3
% 1.14/0.80 % (290738)Termination reason: Instruction limit
% 1.14/0.80 % (290738)Termination phase: shuffling
% 1.14/0.80 % (290738)Time elapsed: 0.013 s
% 1.14/0.80 % (290738)Peak memory usage: 11 MB
% 1.14/0.80 % (290738)Instructions burned: 26 (million)
% 1.14/0.80 % (290740)Instruction limit reached!
% 1.72/0.84 % (290740)------------------------------
% 1.72/0.84 % (290740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290740)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290740)Termination reason: Instruction limit
% 1.72/0.84 % (290740)Termination phase: shuffling
% 1.72/0.84 % (290740)Time elapsed: 0.011 s
% 1.72/0.84 % (290740)Peak memory usage: 11 MB
% 1.72/0.84 % (290740)Instructions burned: 23 (million)
% 1.72/0.84 % (290743)Instruction limit reached!
% 1.72/0.84 % (290743)------------------------------
% 1.72/0.84 % (290743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290743)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290743)Termination reason: Instruction limit
% 1.72/0.84 % (290743)Termination phase: shuffling
% 1.72/0.84 % (290743)Time elapsed: 0.007 s
% 1.72/0.84 % (290743)Peak memory usage: 10 MB
% 1.72/0.84 % (290743)Instructions burned: 15 (million)
% 1.72/0.84 % (290748)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.72/0.84 % (290748)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=4228225490:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 1.72/0.84 % (290749)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=2583244187:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 1.72/0.84 % (290742)Instruction limit reached!
% 1.72/0.84 % (290742)------------------------------
% 1.72/0.84 % (290742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290742)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290742)Termination reason: Instruction limit
% 1.72/0.84 % (290742)Termination phase: shuffling
% 1.72/0.84 % (290742)Time elapsed: 0.027 s
% 1.72/0.84 % (290742)Peak memory usage: 12 MB
% 1.72/0.84 % (290742)Instructions burned: 62 (million)
% 1.72/0.84 % (290748)Instruction limit reached!
% 1.72/0.84 % (290748)------------------------------
% 1.72/0.84 % (290748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290748)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290748)Termination reason: Instruction limit
% 1.72/0.84 % (290748)Termination phase: shuffling
% 1.72/0.84 % (290748)Time elapsed: 0.004 s
% 1.72/0.84 % (290748)Peak memory usage: 10 MB
% 1.72/0.84 % (290748)Instructions burned: 8 (million)
% 1.72/0.84 % (290750)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=173429111:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 1.72/0.84 % (290750)Instruction limit reached!
% 1.72/0.84 % (290750)------------------------------
% 1.72/0.84 % (290750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290750)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290750)Termination reason: Instruction limit
% 1.72/0.84 % (290750)Termination phase: shuffling
% 1.72/0.84 % (290750)Time elapsed: 0.004 s
% 1.72/0.84 % (290750)Peak memory usage: 10 MB
% 1.72/0.84 % (290750)Instructions burned: 8 (million)
% 1.72/0.84 % (290731)Instruction limit reached!
% 1.72/0.84 % (290731)------------------------------
% 1.72/0.84 % (290731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290731)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290731)Termination reason: Instruction limit
% 1.72/0.84 % (290731)Termination phase: Property scanning
% 1.72/0.84 % (290731)Time elapsed: 0.078 s
% 1.72/0.84 % (290731)Peak memory usage: 16 MB
% 1.72/0.84 % (290731)Instructions burned: 332 (million)
% 1.72/0.84 % (290749)Instruction limit reached!
% 1.72/0.84 % (290749)------------------------------
% 1.72/0.84 % (290749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290749)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290749)Termination reason: Instruction limit
% 1.72/0.84 % (290749)Termination phase: shuffling
% 1.72/0.84 % (290749)Time elapsed: 0.015 s
% 1.72/0.84 % (290749)Peak memory usage: 11 MB
% 1.72/0.84 % (290749)Instructions burned: 32 (million)
% 1.72/0.84 % (290757)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=680021708:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 1.72/0.84 % (290753)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=774325979:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 1.72/0.84 % (290754)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3178471892:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 1.72/0.84 % (290756)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=693673702:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 1.72/0.84 % (290754)Instruction limit reached!
% 1.72/0.84 % (290754)------------------------------
% 1.72/0.84 % (290754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290754)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290754)Termination reason: Instruction limit
% 1.72/0.84 % (290754)Termination phase: shuffling
% 1.72/0.84 % (290754)Time elapsed: 0.009 s
% 1.72/0.84 % (290754)Peak memory usage: 11 MB
% 1.72/0.84 % (290754)Instructions burned: 20 (million)
% 1.72/0.84 % (290758)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=4014342576:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 1.72/0.84 % (290753)Instruction limit reached!
% 1.72/0.84 % (290753)------------------------------
% 1.72/0.84 % (290753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290753)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290753)Termination reason: Instruction limit
% 1.72/0.84 % (290753)Termination phase: shuffling
% 1.72/0.84 % (290753)Time elapsed: 0.012 s
% 1.72/0.84 % (290753)Peak memory usage: 11 MB
% 1.72/0.84 % (290753)Instructions burned: 24 (million)
% 1.72/0.84 % (290727)Instruction limit reached!
% 1.72/0.84 % (290727)------------------------------
% 1.72/0.84 % (290727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290727)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290727)Termination reason: Instruction limit
% 1.72/0.84 % (290727)Termination phase: Saturation
% 1.72/0.84 % (290727)Time elapsed: 0.110 s
% 1.72/0.84 % (290727)Peak memory usage: 16 MB
% 1.72/0.84 % (290727)Instructions burned: 250 (million)
% 1.72/0.84 % (290765)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.72/0.84 % (290764)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=580009632:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 1.72/0.84 % (290765)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1743705554:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 1.72/0.84 % (290757)Instruction limit reached!
% 1.72/0.84 % (290757)------------------------------
% 1.72/0.84 % (290757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290757)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290757)Termination reason: Instruction limit
% 1.72/0.84 % (290757)Termination phase: shuffling
% 1.72/0.84 % (290757)Time elapsed: 0.033 s
% 1.72/0.84 % (290757)Peak memory usage: 14 MB
% 1.72/0.84 % (290757)Instructions burned: 146 (million)
% 1.72/0.84 % (290765)Instruction limit reached!
% 1.72/0.84 % (290765)------------------------------
% 1.72/0.84 % (290765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290765)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290765)Termination reason: Instruction limit
% 1.72/0.84 % (290765)Termination phase: shuffling
% 1.72/0.84 % (290765)Time elapsed: 0.004 s
% 1.72/0.84 % (290765)Peak memory usage: 10 MB
% 1.72/0.84 % (290765)Instructions burned: 7 (million)
% 1.72/0.84 % (290766)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3417358736:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 1.72/0.84 % (290769)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=412252061:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 1.72/0.84 % (290764)Instruction limit reached!
% 1.72/0.84 % (290764)------------------------------
% 1.72/0.84 % (290764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290764)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290764)Termination reason: Instruction limit
% 1.72/0.84 % (290764)Termination phase: shuffling
% 1.72/0.84 % (290764)Time elapsed: 0.019 s
% 1.72/0.84 % (290764)Peak memory usage: 11 MB
% 1.72/0.84 % (290764)Instructions burned: 44 (million)
% 1.72/0.84 % (290770)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.72/0.84 % (290770)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2368831536:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 1.72/0.84 % (290770)Instruction limit reached!
% 1.72/0.84 % (290770)------------------------------
% 1.72/0.84 % (290770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290770)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290770)Termination reason: Instruction limit
% 1.72/0.84 % (290770)Termination phase: shuffling
% 1.72/0.84 % (290770)Time elapsed: 0.004 s
% 1.72/0.84 % (290770)Peak memory usage: 10 MB
% 1.72/0.84 % (290770)Instructions burned: 8 (million)
% 1.72/0.84 % (290699) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-290691-290699"...
% 1.72/0.84 % (290773)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3349269803:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 1.72/0.84 % (290699)...printing done.
% 1.72/0.84 % (290699)Refutation found. Thanks to Tanya!
% 1.72/0.84 % SZS status Theorem for theBenchmark
% 1.72/0.84 % SZS output start Proof for theBenchmark
% 1.72/0.84 thf(type_def_5, type, rCharacterData_ext: $tType > $tType).
% 1.72/0.84 thf(type_def_6, type, rShadowRoot_ext: ($tType * $tType * $tType * $tType) > $tType).
% 1.72/0.84 thf(type_def_7, type, character_data_ptr: $tType > $tType).
% 1.72/0.84 thf(type_def_8, type, rDocument_ext: ($tType * $tType * $tType * $tType) > $tType).
% 1.72/0.84 thf(type_def_9, type, rElement_ext: ($tType * $tType * $tType * $tType * $tType) > $tType).
% 1.72/0.84 thf(type_def_10, type, shadow_root_ptr: $tType > $tType).
% 1.72/0.84 thf(type_def_11, type, rObject_ext: $tType > $tType).
% 1.72/0.84 thf(type_def_12, type, document_ptr: $tType > $tType).
% 1.72/0.84 thf(type_def_13, type, rNode_ext: $tType > $tType).
% 1.72/0.84 thf(type_def_14, type, element_ptr: $tType > $tType).
% 1.72/0.84 thf(type_def_15, type, object_ptr: $tType > $tType).
% 1.72/0.84 thf(type_def_16, type, heap_Error_prog: ($tType * $tType * $tType) > $tType).
% 1.72/0.84 thf(type_def_17, type, node_ptr: $tType > $tType).
% 1.72/0.84 thf(type_def_18, type, exception: $tType).
% 1.72/0.84 thf(type_def_19, type, product_unit: $tType).
% 1.72/0.84 thf(type_def_20, type, heap: ($tType * $tType) > $tType).
% 1.72/0.84 thf(type_def_21, type, finite_fmap: ($tType * $tType) > $tType).
% 1.72/0.84 thf(type_def_22, type, sum_sum: ($tType * $tType) > $tType).
% 1.72/0.84 thf(type_def_23, type, option: $tType > $tType).
% 1.72/0.84 thf(type_def_24, type, char: $tType).
% 1.72/0.84 thf(type_def_25, type, list: $tType > $tType).
% 1.72/0.84 thf(type_def_26, type, n: $tType).
% 1.72/0.84 thf(type_def_27, type, m: $tType).
% 1.72/0.84 thf(type_def_28, type, l: $tType).
% 1.72/0.84 thf(type_def_29, type, k: $tType).
% 1.72/0.84 thf(type_def_30, type, j: $tType).
% 1.72/0.84 thf(type_def_31, type, i: $tType).
% 1.72/0.84 thf(type_def_32, type, h: $tType).
% 1.72/0.84 thf(type_def_33, type, g: $tType).
% 1.72/0.84 thf(type_def_34, type, f: $tType).
% 1.72/0.84 thf(type_def_35, type, e: $tType).
% 1.72/0.84 thf(type_def_36, type, d: $tType).
% 1.72/0.84 thf(type_def_37, type, c: $tType).
% 1.72/0.84 thf(type_def_38, type, b: $tType).
% 1.72/0.84 thf(type_def_39, type, a: $tType).
% 1.72/0.84 thf(type_def_40, type, sTfun: ($tType * $tType) > $tType).
% 1.72/0.84 thf(func_def_0, type, l_put_a_put_M: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((X0 > X1 > option @ X2) > (X0 > X2 > X1 > X1) > X0 > ((X3 > X3) > X2 > X2) > X3 > heap_Error_prog @ X1 @ exception @ product_unit))).
% 1.72/0.84 thf(func_def_1, type, val: !>[X0: $tType]:((rObject_ext @ rNode_ext @ rCharacterData_ext @ X0 > list @ char))).
% 1.72/0.84 thf(func_def_2, type, val_update: !>[X0: $tType]:(((list @ char > list @ char) > rObject_ext @ rNode_ext @ rCharacterData_ext @ X0 > rObject_ext @ rNode_ext @ rCharacterData_ext @ X0))).
% 1.72/0.84 thf(func_def_3, type, cast_C1206507959_o_d_e: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X0 > rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X1 @ X2 @ X3 @ X4 @ option @ X5 @ sum_sum @ rCharacterData_ext @ option @ X0 @ X6))).
% 1.72/0.84 thf(func_def_4, type, cast_N331463351_a_t_a: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ option @ X4 @ sum_sum @ rCharacterData_ext @ option @ X5 @ X6 > option @ rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X5))).
% 1.72/0.84 thf(func_def_5, type, get_C_796961872_a_t_a: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:((character_data_ptr @ X0 > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X0 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X1 @ X0 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X8 @ X9 > option @ rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X7))).
% 1.72/0.84 thf(func_def_6, type, is_cha448255042_o_d_e: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ option @ X4 @ sum_sum @ rCharacterData_ext @ option @ X5 @ X6 > $o))).
% 1.72/0.84 thf(func_def_7, type, l_type942687182ype_wf: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X8 @ X9 > $o))).
% 1.72/0.84 thf(func_def_8, type, put_C_1264771785_a_t_a: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:((character_data_ptr @ X0 > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X1 > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X3 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X4 @ X5 @ X6 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X3 @ X2 @ X0 @ X4 @ option @ X7 @ sum_sum @ rCharacterData_ext @ option @ X1 @ X8 @ X9 > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X3 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X4 @ X5 @ X6 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X3 @ X2 @ X0 @ X4 @ option @ X7 @ sum_sum @ rCharacterData_ext @ option @ X1 @ X8 @ X9))).
% 1.72/0.84 thf(func_def_9, type, type_wf: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X8 @ X9 > $o))).
% 1.72/0.84 thf(func_def_10, type, get_M_1540554666_a_t_a: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:((character_data_ptr @ X0 > (rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X1 > X2) > heap_Error_prog @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X0 @ X4 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X5 @ X6 @ X7 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X3 @ X0 @ X5 @ option @ X8 @ sum_sum @ rCharacterData_ext @ option @ X1 @ X9 @ X10 @ exception @ X2))).
% 1.72/0.84 thf(func_def_11, type, l_new_character_data: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:(((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X8 @ X9 > $o) > $o))).
% 1.72/0.84 thf(func_def_12, type, new_character_data: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:(heap_Error_prog @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X8 @ X9 @ exception @ character_data_ptr @ X1)).
% 1.72/0.84 thf(func_def_13, type, put_M_926020593_a_t_a: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:((character_data_ptr @ X0 > ((X1 > X1) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X2 > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X2) > X1 > heap_Error_prog @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X0 @ X4 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X5 @ X6 @ X7 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X3 @ X0 @ X5 @ option @ X8 @ sum_sum @ rCharacterData_ext @ option @ X2 @ X9 @ X10 @ exception @ product_unit))).
% 1.72/0.84 thf(func_def_14, type, cast_c1817826148_p_t_r: !>[X0: $tType, X1: $tType, X2: $tType]:((character_data_ptr @ X0 > node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X0 @ X2))).
% 1.72/0.84 thf(func_def_15, type, cast_n458720130_p_t_r: !>[X0: $tType, X1: $tType, X2: $tType]:((node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 > option @ character_data_ptr @ X1))).
% 1.72/0.84 thf(func_def_16, type, is_cha1694415012_p_t_r: !>[X0: $tType]:((character_data_ptr @ X0 > $o))).
% 1.72/0.84 thf(func_def_17, type, is_cha614540985_p_t_r: !>[X0: $tType, X1: $tType, X2: $tType]:((node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 > $o))).
% 1.72/0.84 thf(func_def_18, type, disconnected_nodes: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ X3 > list @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X2 @ X0))).
% 1.72/0.84 thf(func_def_19, type, discon1635973971update: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((list @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 > list @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2) > rObject_ext @ rDocument_ext @ X2 @ X0 @ X1 @ X3 > rObject_ext @ rDocument_ext @ X2 @ X0 @ X1 @ X3))).
% 1.72/0.84 thf(func_def_20, type, doctype: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ X3 > list @ char))).
% 1.72/0.84 thf(func_def_21, type, doctype_update: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((list @ char > list @ char) > rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ X3 > rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ X3))).
% 1.72/0.84 thf(func_def_22, type, document_element: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ X3 > option @ element_ptr @ X1))).
% 1.72/0.84 thf(func_def_23, type, docume446011358update: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((option @ element_ptr @ X0 > option @ element_ptr @ X0) > rObject_ext @ rDocument_ext @ X1 @ X0 @ X2 @ X3 > rObject_ext @ rDocument_ext @ X1 @ X0 @ X2 @ X3))).
% 1.72/0.84 thf(func_def_24, type, cast_D42511940_e_c_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:((rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ option @ X3 > rObject_ext @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X0 @ X1 @ X2 @ X4 @ option @ X5 @ sum_sum @ rCharacterData_ext @ option @ X6 @ X7 @ sum_sum @ rDocument_ext @ X0 @ X1 @ X2 @ option @ X3 @ X8))).
% 1.72/0.84 thf(func_def_25, type, cast_O1159777348_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:((rObject_ext @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ option @ X4 @ sum_sum @ rCharacterData_ext @ option @ X5 @ X6 @ sum_sum @ rDocument_ext @ X0 @ X1 @ X2 @ option @ X7 @ X8 > option @ rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ option @ X7))).
% 1.72/0.84 thf(func_def_26, type, get_D_o_c_u_m_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:((document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X1 > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X3 @ X4 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X1 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X2 @ X3 @ X0 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X8 @ sum_sum @ rDocument_ext @ X4 @ X2 @ X3 @ option @ X9 @ X10 > option @ rObject_ext @ rDocument_ext @ X4 @ X2 @ X3 @ option @ X9))).
% 1.72/0.84 thf(func_def_27, type, is_document_kind: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:((rObject_ext @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ option @ X4 @ sum_sum @ rCharacterData_ext @ option @ X5 @ X6 @ sum_sum @ rDocument_ext @ X0 @ X1 @ X2 @ option @ X7 @ X8 > $o))).
% 1.72/0.84 thf(func_def_28, type, l_type1694037370ype_wf: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X8 @ sum_sum @ rDocument_ext @ X2 @ X0 @ X1 @ option @ X9 @ X10 > $o))).
% 1.72/0.84 thf(func_def_29, type, put_D_o_c_u_m_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:((document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X1 > rObject_ext @ rDocument_ext @ X2 @ X3 @ X4 @ option @ X5 > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X4 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X1 @ X6 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X3 @ X4 @ X0 @ option @ X7 @ sum_sum @ rCharacterData_ext @ option @ X8 @ X9 @ sum_sum @ rDocument_ext @ X2 @ X3 @ X4 @ option @ X5 @ X10 > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X4 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X1 @ X6 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X3 @ X4 @ X0 @ option @ X7 @ sum_sum @ rCharacterData_ext @ option @ X8 @ X9 @ sum_sum @ rDocument_ext @ X2 @ X3 @ X4 @ option @ X5 @ X10))).
% 1.72/0.84 thf(func_def_30, type, type_wf2: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X8 @ sum_sum @ rDocument_ext @ X2 @ X0 @ X1 @ option @ X9 @ X10 > $o))).
% 1.72/0.84 thf(func_def_31, type, get_M_1744428286_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType, X11: $tType]:((document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X1 > (rObject_ext @ rDocument_ext @ X2 @ X3 @ X4 @ option @ X5 > X6) > heap_Error_prog @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X4 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X1 @ X7 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X3 @ X4 @ X0 @ option @ X8 @ sum_sum @ rCharacterData_ext @ option @ X9 @ X10 @ sum_sum @ rDocument_ext @ X2 @ X3 @ X4 @ option @ X5 @ X11 @ exception @ X6))).
% 1.72/0.84 thf(func_def_32, type, l_new_document: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:(((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X8 @ sum_sum @ rDocument_ext @ X2 @ X0 @ X1 @ option @ X9 @ X10 > $o) > $o))).
% 1.72/0.84 thf(func_def_33, type, new_document: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:(heap_Error_prog @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X8 @ sum_sum @ rDocument_ext @ X2 @ X0 @ X1 @ option @ X9 @ X10 @ exception @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4)).
% 1.72/0.84 thf(func_def_34, type, put_M_950607941_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType, X11: $tType]:((document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X1 > ((X2 > X2) > rObject_ext @ rDocument_ext @ X3 @ X4 @ X5 @ option @ X6 > rObject_ext @ rDocument_ext @ X3 @ X4 @ X5 @ option @ X6) > X2 > heap_Error_prog @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X4 @ sum_sum @ character_data_ptr @ X5 @ X3 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X1 @ X7 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X3 @ X4 @ X5 @ X0 @ option @ X8 @ sum_sum @ rCharacterData_ext @ option @ X9 @ X10 @ sum_sum @ rDocument_ext @ X3 @ X4 @ X5 @ option @ X6 @ X11 @ exception @ product_unit))).
% 1.72/0.84 thf(func_def_35, type, cast_d1427782271_p_t_r: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((document_ptr @ X0 > object_ptr @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X2 @ X3 @ sum_sum @ document_ptr @ X0 @ X4))).
% 1.72/0.84 thf(func_def_36, type, is_doc697300620_p_t_r: !>[X0: $tType]:((document_ptr @ X0 > $o))).
% 1.72/0.84 thf(func_def_37, type, is_document_ptr_kind: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((object_ptr @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ X3 @ X4 > $o))).
% 1.72/0.84 thf(func_def_38, type, attrs: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ X4 > finite_fmap @ list @ char @ list @ char))).
% 1.72/0.84 thf(func_def_39, type, attrs_update: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((finite_fmap @ list @ char @ list @ char > finite_fmap @ list @ char @ list @ char) > rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ X4 > rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ X4))).
% 1.72/0.84 thf(func_def_40, type, child_nodes: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ X4 > list @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X2 @ X0))).
% 1.72/0.84 thf(func_def_41, type, child_nodes_update: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((list @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 > list @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2) > rObject_ext @ rNode_ext @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ X4 > rObject_ext @ rNode_ext @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ X4))).
% 1.72/0.84 thf(func_def_42, type, shadow_root_opt: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ X4 > option @ shadow_root_ptr @ X3))).
% 1.72/0.84 thf(func_def_43, type, shadow1355209752update: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((option @ shadow_root_ptr @ X0 > option @ shadow_root_ptr @ X0) > rObject_ext @ rNode_ext @ rElement_ext @ X1 @ X2 @ X3 @ X0 @ X4 > rObject_ext @ rNode_ext @ rElement_ext @ X1 @ X2 @ X3 @ X0 @ X4))).
% 1.72/0.84 thf(func_def_44, type, tag_name: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ X4 > list @ char))).
% 1.72/0.84 thf(func_def_45, type, tag_name_update: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((list @ char > list @ char) > rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ X4 > rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ X4))).
% 1.72/0.84 thf(func_def_46, type, cast_E624595161_o_d_e: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ option @ X4 > rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ option @ X4 @ X5))).
% 1.72/0.84 thf(func_def_47, type, cast_N1919872217_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ option @ X4 @ X5 > option @ rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ option @ X4))).
% 1.72/0.84 thf(func_def_48, type, get_E_l_e_m_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:((element_ptr @ X0 > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ X7 @ X8 > option @ rObject_ext @ rNode_ext @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6))).
% 1.72/0.84 thf(func_def_49, type, is_ele641449972_o_d_e: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X0 @ X1 @ X2 @ X3 @ option @ X4 @ X5 > $o))).
% 1.72/0.84 thf(func_def_50, type, known_ptr: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((object_ptr @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 > $o))).
% 1.72/0.84 thf(func_def_51, type, l_know358518967wn_ptr: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((object_ptr @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 > $o))).
% 1.72/0.84 thf(func_def_52, type, l_type512970796ype_wf: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ X7 @ X8 > $o))).
% 1.72/0.84 thf(func_def_53, type, put_E_l_e_m_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:((element_ptr @ X0 > rObject_ext @ rNode_ext @ rElement_ext @ X1 @ X0 @ X2 @ X3 @ option @ X4 > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X2 @ X1 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X5 @ X6 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X1 @ X0 @ X2 @ X3 @ option @ X4 @ X7 @ X8 > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X2 @ X1 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X5 @ X6 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X1 @ X0 @ X2 @ X3 @ option @ X4 @ X7 @ X8))).
% 1.72/0.84 thf(func_def_54, type, type_wf3: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ X7 @ X8 > $o))).
% 1.72/0.84 thf(func_def_55, type, get_M_E_l_e_m_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:((element_ptr @ X0 > (rObject_ext @ rNode_ext @ rElement_ext @ X1 @ X0 @ X2 @ X3 @ option @ X4 > X5) > heap_Error_prog @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X2 @ X1 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X6 @ X7 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X1 @ X0 @ X2 @ X3 @ option @ X4 @ X8 @ X9 @ exception @ X5))).
% 1.72/0.84 thf(func_def_56, type, l_new_element: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:(((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ X7 @ X8 > $o) > $o))).
% 1.72/0.84 thf(func_def_57, type, new_element: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:(heap_Error_prog @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X4 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X1 @ X3 @ option @ X6 @ X7 @ X8 @ exception @ element_ptr @ X0)).
% 1.72/0.84 thf(func_def_58, type, put_M_E_l_e_m_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:((element_ptr @ X0 > ((X1 > X1) > rObject_ext @ rNode_ext @ rElement_ext @ X2 @ X0 @ X3 @ X4 @ option @ X5 > rObject_ext @ rNode_ext @ rElement_ext @ X2 @ X0 @ X3 @ X4 @ option @ X5) > X1 > heap_Error_prog @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X3 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X4 @ X6 @ X7 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X0 @ X3 @ X4 @ option @ X5 @ X8 @ X9 @ exception @ product_unit))).
% 1.72/0.84 thf(func_def_59, type, cast_e2129487814_p_t_r: !>[X0: $tType, X1: $tType]:((element_ptr @ X0 > node_ptr @ sum_sum @ element_ptr @ X0 @ X1))).
% 1.72/0.84 thf(func_def_60, type, cast_n1001364742_p_t_r: !>[X0: $tType, X1: $tType]:((node_ptr @ sum_sum @ element_ptr @ X0 @ X1 > option @ element_ptr @ X0))).
% 1.72/0.84 thf(func_def_61, type, is_ele1630183935_p_t_r: !>[X0: $tType]:((element_ptr @ X0 > $o))).
% 1.72/0.84 thf(func_def_62, type, is_ele497529067_p_t_r: !>[X0: $tType, X1: $tType]:((node_ptr @ sum_sum @ element_ptr @ X0 @ X1 > $o))).
% 1.72/0.84 thf(func_def_63, type, finite_fmempty: !>[X0: $tType, X1: $tType]:(finite_fmap @ X0 @ X1)).
% 1.72/0.84 thf(func_def_64, type, heap_Error_noop: !>[X0: $tType, X1: $tType]:(heap_Error_prog @ X0 @ X1 @ product_unit)).
% 1.72/0.84 thf(func_def_65, type, heap_Error_preserved: !>[X0: $tType, X1: $tType, X2: $tType]:((heap_Error_prog @ X0 @ X1 @ X2 > X0 > X0 > $o))).
% 1.72/0.84 thf(func_def_66, type, heap_E381990939n_heap: !>[X0: $tType, X1: $tType]:((X0 > heap_Error_prog @ X0 @ X1 @ product_unit))).
% 1.72/0.84 thf(func_def_67, type, heap_E940394160s_heap: !>[X0: $tType, X1: $tType, X2: $tType]:((X0 > heap_Error_prog @ X0 @ X1 @ X2 > X0 > $o))).
% 1.72/0.84 thf(func_def_68, type, heap_E1989005601result: !>[X0: $tType, X1: $tType, X2: $tType]:((X0 > heap_Error_prog @ X0 @ X1 @ X2 > X2 > $o))).
% 1.72/0.84 thf(func_def_69, type, heap_E56519469t_heap: !>[X0: $tType, X1: $tType, X2: $tType]:((X0 > heap_Error_prog @ X0 @ X1 @ X2 > X2 > X0 > $o))).
% 1.72/0.84 thf(func_def_70, type, if: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 1.72/0.84 thf(func_def_71, type, nil: !>[X0: $tType]:(list @ X0)).
% 1.72/0.84 thf(func_def_72, type, cast_N414129940_e_c_t: !>[X0: $tType, X1: $tType]:((rObject_ext @ rNode_ext @ X0 > rObject_ext @ sum_sum @ rNode_ext @ X0 @ X1))).
% 1.72/0.84 thf(func_def_73, type, cast_O268912148_o_d_e: !>[X0: $tType, X1: $tType]:((rObject_ext @ sum_sum @ rNode_ext @ X0 @ X1 > option @ rObject_ext @ rNode_ext @ X0))).
% 1.72/0.84 thf(func_def_74, type, is_node_kind: !>[X0: $tType, X1: $tType]:((rObject_ext @ sum_sum @ rNode_ext @ X0 @ X1 > $o))).
% 1.72/0.84 thf(func_def_75, type, known_ptr2: !>[X0: $tType, X1: $tType]:((object_ptr @ sum_sum @ node_ptr @ X0 @ X1 > $o))).
% 1.72/0.84 thf(func_def_76, type, put_N_o_d_e: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((node_ptr @ X0 > rObject_ext @ rNode_ext @ X1 > heap @ sum_sum @ node_ptr @ X0 @ X2 @ sum_sum @ rNode_ext @ X1 @ X3 > heap @ sum_sum @ node_ptr @ X0 @ X2 @ sum_sum @ rNode_ext @ X1 @ X3))).
% 1.72/0.84 thf(func_def_77, type, type_wf4: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((heap @ sum_sum @ node_ptr @ X0 @ X1 @ sum_sum @ rNode_ext @ X2 @ X3 > $o))).
% 1.72/0.84 thf(func_def_78, type, get_M_N_o_d_e: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((node_ptr @ X0 > (rObject_ext @ rNode_ext @ X1 > X2) > heap_Error_prog @ heap @ sum_sum @ node_ptr @ X0 @ X3 @ sum_sum @ rNode_ext @ X1 @ X4 @ exception @ X2))).
% 1.72/0.84 thf(func_def_79, type, put_M_N_o_d_e: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((node_ptr @ X0 > ((X1 > X1) > rObject_ext @ rNode_ext @ X2 > rObject_ext @ rNode_ext @ X2) > X1 > heap_Error_prog @ heap @ sum_sum @ node_ptr @ X0 @ X3 @ sum_sum @ rNode_ext @ X2 @ X4 @ exception @ product_unit))).
% 1.72/0.84 thf(func_def_80, type, cast_n1885620943_p_t_r: !>[X0: $tType, X1: $tType]:((node_ptr @ X0 > object_ptr @ sum_sum @ node_ptr @ X0 @ X1))).
% 1.72/0.84 thf(func_def_81, type, cast_o573710209_p_t_r: !>[X0: $tType, X1: $tType]:((object_ptr @ sum_sum @ node_ptr @ X0 @ X1 > option @ node_ptr @ X0))).
% 1.72/0.84 thf(func_def_82, type, put_O_b_j_e_c_t: !>[X0: $tType, X1: $tType]:((object_ptr @ X0 > rObject_ext @ X1 > heap @ X0 @ X1 > heap @ X0 @ X1))).
% 1.72/0.84 thf(func_def_83, type, get_M_O_b_j_e_c_t: !>[X0: $tType, X1: $tType, X2: $tType]:((object_ptr @ X0 > (rObject_ext @ X1 > X2) > heap_Error_prog @ heap @ X0 @ X1 @ exception @ X2))).
% 1.72/0.84 thf(func_def_84, type, put_M_O_b_j_e_c_t: !>[X0: $tType, X1: $tType, X2: $tType]:((object_ptr @ X0 > ((X1 > X1) > rObject_ext @ X2 > rObject_ext @ X2) > X1 > heap_Error_prog @ heap @ X0 @ X2 @ exception @ product_unit))).
% 1.72/0.84 thf(func_def_85, type, none: !>[X0: $tType]:(option @ X0)).
% 1.72/0.84 thf(func_def_86, type, some: !>[X0: $tType]:((X0 > option @ X0))).
% 1.72/0.84 thf(func_def_87, type, case_option: !>[X0: $tType, X1: $tType]:((X0 > (X1 > X0) > option @ X1 > X0))).
% 1.72/0.84 thf(func_def_88, type, the: !>[X0: $tType]:((option @ X0 > X0))).
% 1.72/0.84 thf(func_def_89, type, cast_D1220047104_o_o_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X0 @ X1 @ X2 @ option @ X3 @ X4 > option @ rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ rShadowRoot_ext @ X0 @ X1 @ X2 @ option @ X3))).
% 1.72/0.84 thf(func_def_90, type, cast_S69733376_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ rShadowRoot_ext @ X0 @ X1 @ X2 @ option @ X3 > rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X0 @ X1 @ X2 @ option @ X3 @ X4))).
% 1.72/0.84 thf(func_def_91, type, is_sha596430153_e_n_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X0 @ X1 @ X2 @ option @ X3 @ X4 > $o))).
% 1.72/0.84 thf(func_def_92, type, shadow1195525443_o_o_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType, X11: $tType, X12: $tType]:((shadow_root_ptr @ X0 > (rObject_ext @ rDocument_ext @ X1 @ X2 @ X3 @ rShadowRoot_ext @ X1 @ X2 @ X3 @ option @ X4 > X5) > heap_Error_prog @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X3 @ X1 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X6 @ X7 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X1 @ X2 @ X3 @ X0 @ option @ X8 @ sum_sum @ rCharacterData_ext @ option @ X9 @ X10 @ sum_sum @ rDocument_ext @ X1 @ X2 @ X3 @ option @ sum_sum @ rShadowRoot_ext @ X1 @ X2 @ X3 @ option @ X4 @ X11 @ X12 @ exception @ X5))).
% 1.72/0.84 thf(func_def_93, type, shadow2002649738_o_o_t: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType, X11: $tType, X12: $tType]:((shadow_root_ptr @ X0 > ((X1 > X1) > rObject_ext @ rDocument_ext @ X2 @ X3 @ X4 @ rShadowRoot_ext @ X2 @ X3 @ X4 @ option @ X5 > rObject_ext @ rDocument_ext @ X2 @ X3 @ X4 @ rShadowRoot_ext @ X2 @ X3 @ X4 @ option @ X5) > X1 > heap_Error_prog @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X4 @ X2 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X6 @ X7 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X3 @ X4 @ X0 @ option @ X8 @ sum_sum @ rCharacterData_ext @ option @ X9 @ X10 @ sum_sum @ rDocument_ext @ X2 @ X3 @ X4 @ option @ sum_sum @ rShadowRoot_ext @ X2 @ X3 @ X4 @ option @ X5 @ X11 @ X12 @ exception @ product_unit))).
% 1.72/0.84 thf(func_def_94, type, cast_s636919983_p_t_r: !>[X0: $tType, X1: $tType]:((shadow_root_ptr @ X0 > document_ptr @ sum_sum @ shadow_root_ptr @ X0 @ X1))).
% 1.72/0.84 thf(func_def_95, type, document_ptr2: document_ptr @ sum_sum @ shadow_root_ptr @ d @ e).
% 1.72/0.84 thf(func_def_96, type, getter: (rObject_ext @ rDocument_ext @ c @ a @ b @ rShadowRoot_ext @ c @ a @ b @ option @ j > n)).
% 1.72/0.84 thf(func_def_97, type, h2: heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l).
% 1.72/0.84 thf(func_def_98, type, h3: heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l).
% 1.72/0.84 thf(func_def_99, type, setter: ((m > m) > rObject_ext @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k > rObject_ext @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k)).
% 1.72/0.84 thf(func_def_100, type, shadow_root_ptr2: shadow_root_ptr @ d).
% 1.72/0.84 thf(func_def_101, type, v: m).
% 1.72/0.84 thf(func_def_105, type, db0: !>[X0: $tType]:(X0)).
% 1.72/0.84 thf(func_def_106, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.72/0.84 thf(func_def_107, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.72/0.84 thf(func_def_108, type, db2: !>[X0: $tType]:(X0)).
% 1.72/0.84 thf(func_def_109, type, db1: !>[X0: $tType]:(X0)).
% 1.72/0.84 thf(func_def_110, type, vOR: ($o > $o > $o)).
% 1.72/0.84 thf(func_def_111, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.72/0.84 thf(func_def_112, type, db3: !>[X0: $tType]:(X0)).
% 1.72/0.84 thf(func_def_113, type, vIMP: ($o > $o > $o)).
% 1.72/0.84 thf(func_def_114, type, vNOT: ($o > $o)).
% 1.72/0.84 thf(func_def_115, type, vAND: ($o > $o > $o)).
% 1.72/0.84 thf(func_def_116, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.72/0.84 thf(func_def_117, type, sK0: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType]:(((rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X7 @ X5 @ X6 @ option @ X1 @ X0 > X2) > ((X3 > X3) > rObject_ext @ rNode_ext @ rElement_ext @ X4 @ X7 @ X5 @ X6 @ option @ X1 > rObject_ext @ rNode_ext @ rElement_ext @ X4 @ X7 @ X5 @ X6 @ option @ X1) > X3 > rObject_ext @ rNode_ext @ rElement_ext @ X4 @ X7 @ X5 @ X6 @ option @ X1))).
% 1.72/0.84 thf(func_def_118, type, sK1: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType, X11: $tType]:((((X10 > X10) > rObject_ext @ rDocument_ext @ X2 @ X3 @ X1 @ rShadowRoot_ext @ X2 @ X3 @ X1 @ option @ X8 > rObject_ext @ rDocument_ext @ X2 @ X3 @ X1 @ rShadowRoot_ext @ X2 @ X3 @ X1 @ option @ X8) > (rObject_ext @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X3 @ X1 @ X11 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X5 @ X0 @ sum_sum @ rDocument_ext @ X2 @ X3 @ X1 @ option @ sum_sum @ rShadowRoot_ext @ X2 @ X3 @ X1 @ option @ X8 @ X7 @ X4 > X9) > X10 > rObject_ext @ rDocument_ext @ X2 @ X3 @ X1 @ rShadowRoot_ext @ X2 @ X3 @ X1 @ option @ X8))).
% 1.72/0.84 thf(func_def_119, type, sK2: !>[X0: $tType, X1: $tType, X2: $tType]:((X2 > (X1 > X2 > X0) > (X1 > X2 > X0) > option @ X1 > X1))).
% 1.72/0.84 thf(func_def_120, type, sK3: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((rObject_ext @ rDocument_ext @ X1 @ X3 @ X0 @ option @ X4 > X2) > ((X2 > X2) > rObject_ext @ rDocument_ext @ X1 @ X3 @ X0 @ option @ X4 > rObject_ext @ rDocument_ext @ X1 @ X3 @ X0 @ option @ X4) > X2 > rObject_ext @ rDocument_ext @ X1 @ X3 @ X0 @ option @ X4))).
% 1.72/0.84 thf(func_def_121, type, sK4: (finite_fmap @ list @ char @ list @ char > (finite_fmap @ list @ char @ list @ char > finite_fmap @ list @ char @ list @ char) > (finite_fmap @ list @ char @ list @ char > finite_fmap @ list @ char @ list @ char) > finite_fmap @ list @ char @ list @ char)).
% 1.72/0.84 thf(func_def_122, type, sK5: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:((X0 > ((X0 > X0) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X3 > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X3) > (rObject_ext @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X4 @ X7 @ X9 @ option @ X8 @ sum_sum @ rCharacterData_ext @ option @ X3 @ X1 @ X5 > X2) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X3))).
% 1.72/0.84 thf(func_def_123, type, sK6: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((X0 > (rObject_ext @ rDocument_ext @ X5 @ X6 @ X4 @ option @ sum_sum @ rShadowRoot_ext @ X5 @ X6 @ X4 @ option @ X2 @ X1 > X3) > ((X0 > X0) > rObject_ext @ rDocument_ext @ X5 @ X6 @ X4 @ rShadowRoot_ext @ X5 @ X6 @ X4 @ option @ X2 > rObject_ext @ rDocument_ext @ X5 @ X6 @ X4 @ rShadowRoot_ext @ X5 @ X6 @ X4 @ option @ X2) > rObject_ext @ rDocument_ext @ X5 @ X6 @ X4 @ rShadowRoot_ext @ X5 @ X6 @ X4 @ option @ X2))).
% 1.72/0.84 thf(func_def_124, type, sK7: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:(((rObject_ext @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X5 @ X8 @ X3 @ X0 @ option @ X1 @ X6 @ X4 > X7) > ((X2 > X2) > rObject_ext @ rNode_ext @ rElement_ext @ X5 @ X8 @ X3 @ X0 @ option @ X1 > rObject_ext @ rNode_ext @ rElement_ext @ X5 @ X8 @ X3 @ X0 @ option @ X1) > X2 > rObject_ext @ rNode_ext @ rElement_ext @ X5 @ X8 @ X3 @ X0 @ option @ X1))).
% 1.72/0.84 thf(func_def_125, type, sK8: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:((rObject_ext @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X1 @ X2 @ X3 @ option @ X5 @ sum_sum @ rCharacterData_ext @ option @ X4 @ X7 @ sum_sum @ rDocument_ext @ X6 @ X1 @ X2 @ option @ X8 @ X0 > rObject_ext @ rDocument_ext @ X6 @ X1 @ X2 @ option @ X8))).
% 1.72/0.84 thf(func_def_126, type, sK9: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((X5 > (rObject_ext @ rDocument_ext @ X3 @ X4 @ X2 @ option @ X0 > X1) > ((X5 > X5) > rObject_ext @ rDocument_ext @ X3 @ X4 @ X2 @ option @ X0 > rObject_ext @ rDocument_ext @ X3 @ X4 @ X2 @ option @ X0) > rObject_ext @ rDocument_ext @ X3 @ X4 @ X2 @ option @ X0))).
% 1.72/0.84 thf(func_def_127, type, sK10: ((list @ char > list @ char) > list @ char > (list @ char > list @ char) > list @ char)).
% 1.72/0.84 thf(func_def_128, type, sK11: !>[X0: $tType]:(((option @ X0 > $o) > X0))).
% 1.72/0.84 thf(func_def_129, type, sK12: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((rObject_ext @ rDocument_ext @ X3 @ X4 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X3 @ X4 @ X2 @ option @ X1 @ X0 > rObject_ext @ rDocument_ext @ X3 @ X4 @ X2 @ rShadowRoot_ext @ X3 @ X4 @ X2 @ option @ X1))).
% 1.72/0.84 thf(func_def_130, type, sK13: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((X5 > ((X5 > X5) > rObject_ext @ rNode_ext @ rElement_ext @ X3 @ X1 @ X2 @ X4 @ option @ X0 > rObject_ext @ rNode_ext @ rElement_ext @ X3 @ X1 @ X2 @ X4 @ option @ X0) > (rObject_ext @ rNode_ext @ rElement_ext @ X3 @ X1 @ X2 @ X4 @ option @ X0 > X5) > rObject_ext @ rNode_ext @ rElement_ext @ X3 @ X1 @ X2 @ X4 @ option @ X0))).
% 1.72/0.84 thf(func_def_131, type, sK14: (list @ char > (list @ char > list @ char) > (list @ char > list @ char) > list @ char)).
% 1.72/0.84 thf(func_def_132, type, sK15: !>[X0: $tType, X1: $tType, X2: $tType]:((node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X0 @ X2 > character_data_ptr @ X0))).
% 1.72/0.84 thf(func_def_133, type, sK16: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X1 @ X4 @ X5 @ option @ X3 @ X0 > rObject_ext @ rNode_ext @ rElement_ext @ X2 @ X1 @ X4 @ X5 @ option @ X3))).
% 1.72/0.84 thf(func_def_134, type, sK17: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:(((rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X7 @ X8 @ X0 @ option @ X5 @ sum_sum @ rCharacterData_ext @ option @ X4 @ X1 > X3) > X2 > ((X2 > X2) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X4 > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X4) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X4))).
% 1.72/0.84 thf(func_def_135, type, sK18: !>[X0: $tType]:(((option @ shadow_root_ptr @ X0 > option @ shadow_root_ptr @ X0) > option @ shadow_root_ptr @ X0 > (option @ shadow_root_ptr @ X0 > option @ shadow_root_ptr @ X0) > option @ shadow_root_ptr @ X0))).
% 1.72/0.84 thf(func_def_136, type, sK19: !>[X0: $tType]:(((option @ element_ptr @ X0 > option @ element_ptr @ X0) > option @ element_ptr @ X0 > (option @ element_ptr @ X0 > option @ element_ptr @ X0) > option @ element_ptr @ X0))).
% 1.72/0.84 thf(func_def_137, type, sK20: !>[X0: $tType, X1: $tType, X2: $tType]:(((list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X1 @ X0 > list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X1 @ X0) > (list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X1 @ X0 > list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X1 @ X0) > list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X1 @ X0 > list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X1 @ X0))).
% 1.72/0.84 thf(func_def_138, type, sK21: ((list @ char > list @ char) > list @ char > (list @ char > list @ char) > list @ char)).
% 1.72/0.84 thf(func_def_139, type, sK22: !>[X0: $tType, X1: $tType]:(((X1 > $o) > (X1 > X0) > (X0 > $o) > X1))).
% 1.72/0.84 thf(func_def_140, type, sK23: !>[X0: $tType]:((option @ X0 > X0))).
% 1.72/0.84 thf(func_def_141, type, sK24: !>[X0: $tType]:((option @ X0 > X0))).
% 1.72/0.84 thf(func_def_142, type, sK25: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((((X1 > X1) > rObject_ext @ rNode_ext @ rElement_ext @ X6 @ X2 @ X5 @ X3 @ option @ X0 > rObject_ext @ rNode_ext @ rElement_ext @ X6 @ X2 @ X5 @ X3 @ option @ X0) > (rObject_ext @ rNode_ext @ rElement_ext @ X6 @ X2 @ X5 @ X3 @ option @ X0 > X4) > X1 > rObject_ext @ rNode_ext @ rElement_ext @ X6 @ X2 @ X5 @ X3 @ option @ X0))).
% 1.72/0.84 thf(func_def_143, type, sK26: !>[X0: $tType, X1: $tType]:((X0 > ((X0 > X0) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X1 > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X1) > (rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X1 > X0) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X1))).
% 1.72/0.84 thf(func_def_144, type, sK27: ((list @ char > list @ char) > (list @ char > list @ char) > list @ char > list @ char)).
% 1.72/0.84 thf(func_def_145, type, sK28: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((rObject_ext @ rDocument_ext @ X5 @ X4 @ X1 @ rShadowRoot_ext @ X5 @ X4 @ X1 @ option @ X2 > X3) > ((X0 > X0) > rObject_ext @ rDocument_ext @ X5 @ X4 @ X1 @ rShadowRoot_ext @ X5 @ X4 @ X1 @ option @ X2 > rObject_ext @ rDocument_ext @ X5 @ X4 @ X1 @ rShadowRoot_ext @ X5 @ X4 @ X1 @ option @ X2) > X0 > rObject_ext @ rDocument_ext @ X5 @ X4 @ X1 @ rShadowRoot_ext @ X5 @ X4 @ X1 @ option @ X2))).
% 1.72/0.84 thf(func_def_146, type, sK29: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:(((rObject_ext @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X0 @ X9 @ X8 @ option @ X2 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X10 @ sum_sum @ rDocument_ext @ X4 @ X0 @ X9 @ option @ X5 @ X3 > X1) > ((X6 > X6) > rObject_ext @ rDocument_ext @ X4 @ X0 @ X9 @ option @ X5 > rObject_ext @ rDocument_ext @ X4 @ X0 @ X9 @ option @ X5) > X6 > rObject_ext @ rDocument_ext @ X4 @ X0 @ X9 @ option @ X5))).
% 1.72/0.84 thf(func_def_147, type, sK30: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > X0))).
% 1.72/0.84 thf(func_def_148, type, sK31: !>[X0: $tType]:((option @ shadow_root_ptr @ X0 > (option @ shadow_root_ptr @ X0 > option @ shadow_root_ptr @ X0) > (option @ shadow_root_ptr @ X0 > option @ shadow_root_ptr @ X0) > option @ shadow_root_ptr @ X0))).
% 1.72/0.84 thf(func_def_149, type, sK32: !>[X0: $tType]:((option @ element_ptr @ X0 > (option @ element_ptr @ X0 > option @ element_ptr @ X0) > (option @ element_ptr @ X0 > option @ element_ptr @ X0) > option @ element_ptr @ X0))).
% 1.72/0.84 thf(func_def_150, type, sK33: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X2 @ X3 @ X0 @ X5 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X1 @ X4 > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X1))).
% 1.72/0.84 thf(func_def_151, type, sK34: !>[X0: $tType]:((option @ X0 > X0))).
% 1.72/0.84 thf(func_def_152, type, sK35: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:(((rObject_ext @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X0 @ X5 @ X1 @ X4 @ option @ X6 @ X7 @ X8 > X2) > ((X3 > X3) > rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X5 @ X1 @ X4 @ option @ X6 > rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X5 @ X1 @ X4 @ option @ X6) > X3 > rObject_ext @ rNode_ext @ rElement_ext @ X0 @ X5 @ X1 @ X4 @ option @ X6))).
% 1.72/0.84 thf(func_def_153, type, sK36: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:((((X6 > X6) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X3 > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X3) > X6 > (rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X2 @ X0 @ X7 @ option @ X5 @ sum_sum @ rCharacterData_ext @ option @ X3 @ X1 > X8) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X3))).
% 1.72/0.84 thf(func_def_154, type, sK37: !>[X0: $tType, X1: $tType, X2: $tType]:((((X1 > X1) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X2 > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X2) > (rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X2 > X0) > X1 > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X2))).
% 1.72/0.84 thf(func_def_155, type, sK38: !>[X0: $tType, X1: $tType]:((node_ptr @ sum_sum @ element_ptr @ X0 @ X1 > element_ptr @ X0))).
% 1.72/0.84 thf(func_def_156, type, sK39: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:(((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X10 @ sum_sum @ character_data_ptr @ X5 @ X7 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X0 @ X1 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X7 @ X10 @ X5 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X9 @ X8 @ sum_sum @ rDocument_ext @ X7 @ X10 @ X5 @ option @ X2 @ X4 > $o) > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X10 @ sum_sum @ character_data_ptr @ X5 @ X7 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X0 @ X1 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X7 @ X10 @ X5 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X9 @ X8 @ sum_sum @ rDocument_ext @ X7 @ X10 @ X5 @ option @ X2 @ X4))).
% 1.72/0.84 thf(func_def_157, type, sK40: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:(((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X10 @ sum_sum @ character_data_ptr @ X5 @ X7 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X0 @ X1 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X7 @ X10 @ X5 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X9 @ X8 @ sum_sum @ rDocument_ext @ X7 @ X10 @ X5 @ option @ X2 @ X4 > $o) > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X10 @ sum_sum @ character_data_ptr @ X5 @ X7 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X3 @ X0 @ X1 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X7 @ X10 @ X5 @ X3 @ option @ X6 @ sum_sum @ rCharacterData_ext @ option @ X9 @ X8 @ sum_sum @ rDocument_ext @ X7 @ X10 @ X5 @ option @ X2 @ X4))).
% 1.72/0.84 thf(func_def_158, type, sK41: !>[X0: $tType]:(((X0 > $o) > option @ X0 > X0))).
% 1.72/0.84 thf(func_def_159, type, sK42: ((list @ char > list @ char) > list @ char > (list @ char > list @ char) > list @ char)).
% 1.72/0.84 thf(func_def_160, type, sK43: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:((X7 > (rObject_ext @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X0 @ X8 @ X4 @ X9 @ option @ X5 @ sum_sum @ rCharacterData_ext @ option @ X2 @ X1 @ X6 > X3) > ((X7 > X7) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X2 > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X2) > rObject_ext @ rNode_ext @ rCharacterData_ext @ option @ X2))).
% 1.72/0.84 thf(func_def_161, type, sK44: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((((X4 > X4) > rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ rShadowRoot_ext @ X0 @ X1 @ X2 @ option @ X3 > rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ rShadowRoot_ext @ X0 @ X1 @ X2 @ option @ X3) > (rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ rShadowRoot_ext @ X0 @ X1 @ X2 @ option @ X3 > X4) > X4 > rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ rShadowRoot_ext @ X0 @ X1 @ X2 @ option @ X3))).
% 1.72/0.84 thf(func_def_162, type, sK45: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:(((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X3 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X1 @ X6 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X3 @ X2 @ X0 @ X1 @ option @ X8 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X9 @ X4 > $o) > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X3 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X1 @ X6 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X3 @ X2 @ X0 @ X1 @ option @ X8 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X9 @ X4))).
% 1.72/0.84 thf(func_def_163, type, sK46: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:(((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X3 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X1 @ X6 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X3 @ X2 @ X0 @ X1 @ option @ X8 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X9 @ X4 > $o) > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X3 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X1 @ X6 @ X5 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X3 @ X2 @ X0 @ X1 @ option @ X8 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X9 @ X4))).
% 1.72/0.84 thf(func_def_164, type, sK47: !>[X0: $tType, X1: $tType]:((rObject_ext @ sum_sum @ rNode_ext @ X1 @ X0 > rObject_ext @ rNode_ext @ X1))).
% 1.72/0.84 thf(func_def_165, type, sK48: (finite_fmap @ list @ char @ list @ char > (finite_fmap @ list @ char @ list @ char > finite_fmap @ list @ char @ list @ char) > (finite_fmap @ list @ char @ list @ char > finite_fmap @ list @ char @ list @ char) > finite_fmap @ list @ char @ list @ char)).
% 1.72/0.84 thf(func_def_166, type, sK49: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:(((rObject_ext @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X8 @ X3 @ X2 @ X0 @ option @ X9 @ sum_sum @ rCharacterData_ext @ option @ X7 @ X6 @ sum_sum @ rDocument_ext @ X8 @ X3 @ X2 @ option @ X5 @ X1 > X10) > X4 > ((X4 > X4) > rObject_ext @ rDocument_ext @ X8 @ X3 @ X2 @ option @ X5 > rObject_ext @ rDocument_ext @ X8 @ X3 @ X2 @ option @ X5) > rObject_ext @ rDocument_ext @ X8 @ X3 @ X2 @ option @ X5))).
% 1.72/0.84 thf(func_def_167, type, sK50: !>[X0: $tType, X1: $tType]:((option @ X0 > (option @ X0 > option @ X1 > $o) > option @ X1 > X0))).
% 1.72/0.84 thf(func_def_168, type, sK51: !>[X0: $tType, X1: $tType]:((option @ X0 > (option @ X0 > option @ X1 > $o) > option @ X1 > X1))).
% 1.72/0.84 thf(func_def_169, type, sK52: !>[X0: $tType, X1: $tType, X2: $tType]:((list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X1 > (list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X1 > list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X1) > (list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X1 > list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X1) > list @ node_ptr @ sum_sum @ element_ptr @ X2 @ sum_sum @ character_data_ptr @ X0 @ X1))).
% 1.72/0.84 thf(func_def_170, type, sK53: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType]:((((X7 > X7) > rObject_ext @ rNode_ext @ rElement_ext @ X1 @ X0 @ X5 @ X2 @ option @ X4 > rObject_ext @ rNode_ext @ rElement_ext @ X1 @ X0 @ X5 @ X2 @ option @ X4) > X7 > (rObject_ext @ rNode_ext @ sum_sum @ rElement_ext @ X1 @ X0 @ X5 @ X2 @ option @ X4 @ X6 > X3) > rObject_ext @ rNode_ext @ rElement_ext @ X1 @ X0 @ X5 @ X2 @ option @ X4))).
% 1.72/0.84 thf(func_def_171, type, sK54: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((((X2 > X2) > rObject_ext @ rNode_ext @ X1 > rObject_ext @ rNode_ext @ X1) > X2 > (rObject_ext @ sum_sum @ rNode_ext @ X1 @ X0 > X3) > rObject_ext @ rNode_ext @ X1))).
% 1.72/0.84 thf(func_def_172, type, sK55: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((X1 > (rObject_ext @ sum_sum @ rNode_ext @ X3 @ X0 > X2) > ((X1 > X1) > rObject_ext @ rNode_ext @ X3 > rObject_ext @ rNode_ext @ X3) > rObject_ext @ rNode_ext @ X3))).
% 1.72/0.84 thf(func_def_173, type, sK56: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:(((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X5 @ X8 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X4 @ X2 @ X0 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X8 @ X1 @ X5 @ X4 @ option @ X3 @ X7 @ X6 > $o) > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X5 @ X8 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X4 @ X2 @ X0 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X8 @ X1 @ X5 @ X4 @ option @ X3 @ X7 @ X6))).
% 1.72/0.84 thf(func_def_174, type, sK57: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:(((heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X5 @ X8 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X4 @ X2 @ X0 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X8 @ X1 @ X5 @ X4 @ option @ X3 @ X7 @ X6 > $o) > heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X5 @ X8 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X4 @ X2 @ X0 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X8 @ X1 @ X5 @ X4 @ option @ X3 @ X7 @ X6))).
% 1.72/0.84 thf(func_def_175, type, sK58: (list @ char > (list @ char > list @ char) > (list @ char > list @ char) > list @ char)).
% 1.72/0.84 thf(func_def_176, type, sK59: !>[X0: $tType, X1: $tType, X2: $tType]:(((list @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X2 @ X0 > list @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X2 @ X0) > list @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X2 @ X0 > (list @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X2 @ X0 > list @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X2 @ X0) > list @ node_ptr @ sum_sum @ element_ptr @ X1 @ sum_sum @ character_data_ptr @ X2 @ X0))).
% 1.72/0.84 thf(func_def_177, type, sK60: !>[X0: $tType, X1: $tType, X2: $tType]:(((list @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 > list @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2) > list @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 > (list @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2 > list @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2) > list @ node_ptr @ sum_sum @ element_ptr @ X0 @ sum_sum @ character_data_ptr @ X1 @ X2))).
% 1.72/0.84 thf(func_def_179, type, inv_cast_S69733376_e_n_t_62: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X0 @ X1 @ X2 @ option @ X3 @ X4 > rObject_ext @ rDocument_ext @ X0 @ X1 @ X2 @ rShadowRoot_ext @ X0 @ X1 @ X2 @ option @ X3))).
% 1.72/0.84 thf(f1,axiom,(
% 1.72/0.84 ! [X25 : $tType,X16 : $tType,X18 : $tType,X17 : $tType,X30 : $tType,X24 : $tType,X19 : $tType,X27 : $tType,X23 : $tType,X20 : $tType,X22 : $tType,X21 : $tType,X31 : $tType,X15 : $tType,X37 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X17 @ sum_sum @ character_data_ptr @ X18 @ X19 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X15 @ X16 @ X20 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X19 @ X17 @ X18 @ X15 @ option @ X21 @ sum_sum @ rCharacterData_ext @ option @ X22 @ X23 @ sum_sum @ rDocument_ext @ X19 @ X17 @ X18 @ option @ sum_sum @ rShadowRoot_ext @ X19 @ X17 @ X18 @ option @ X24 @ X25 @ X27,X36 : X30,X38 : (rObject_ext @ rDocument_ext @ X19 @ X17 @ X18 @ rShadowRoot_ext @ X19 @ X17 @ X18 @ option @ X24 > X31),X33 : document_ptr @ sum_sum @ shadow_root_ptr @ X15 @ X16,X32 : shadow_root_ptr @ X15,X35 : ((X30 > X30) > rObject_ext @ rDocument_ext @ X19 @ X17 @ X18 @ option @ sum_sum @ rShadowRoot_ext @ X19 @ X17 @ X18 @ option @ X24 @ X25 > rObject_ext @ rDocument_ext @ X19 @ X17 @ X18 @ option @ sum_sum @ rShadowRoot_ext @ X19 @ X17 @ X18 @ option @ X24 @ X25),X34 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X17 @ sum_sum @ character_data_ptr @ X18 @ X19 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X15 @ X16 @ X20 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X19 @ X17 @ X18 @ X15 @ option @ X21 @ sum_sum @ rCharacterData_ext @ option @ X22 @ X23 @ sum_sum @ rDocument_ext @ X19 @ X17 @ X18 @ option @ sum_sum @ rShadowRoot_ext @ X19 @ X17 @ X18 @ option @ X24 @ X25 @ X27] : ((((cast_s636919983_p_t_r @ X15 @ X16 @ X32)) != X33) => ((heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X17 @ sum_sum @ character_data_ptr @ X18 @ X19 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X15 @ X16 @ X20 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X19 @ X17 @ X18 @ X15 @ option @ X21 @ sum_sum @ rCharacterData_ext @ option @ X22 @ X23 @ sum_sum @ rDocument_ext @ X19 @ X17 @ X18 @ option @ sum_sum @ rShadowRoot_ext @ X19 @ X17 @ X18 @ option @ X24 @ X25 @ X27 @ exception @ product_unit @ X34 @ (put_M_950607941_e_n_t @ X15 @ X16 @ X30 @ X19 @ X17 @ X18 @ sum_sum @ rShadowRoot_ext @ X19 @ X17 @ X18 @ option @ X24 @ X25 @ X20 @ X21 @ X22 @ X23 @ X27 @ X33 @ X35 @ X36) @ X37) => (heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X17 @ sum_sum @ character_data_ptr @ X18 @ X19 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X15 @ X16 @ X20 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X19 @ X17 @ X18 @ X15 @ option @ X21 @ sum_sum @ rCharacterData_ext @ option @ X22 @ X23 @ sum_sum @ rDocument_ext @ X19 @ X17 @ X18 @ option @ sum_sum @ rShadowRoot_ext @ X19 @ X17 @ X18 @ option @ X24 @ X25 @ X27 @ exception @ X31 @ (shadow1195525443_o_o_t @ X15 @ X19 @ X17 @ X18 @ X24 @ X31 @ X16 @ X20 @ X21 @ X22 @ X23 @ X25 @ X27 @ X32 @ X38) @ X34 @ X37)))),
% 1.72/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_get__M__shadow__root__put__M__document__different__pointers)).
% 1.72/0.84 thf(f259,axiom,(
% 1.72/0.84 (heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ product_unit @ h2 @ (put_M_950607941_e_n_t @ d @ e @ m @ c @ a @ b @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ f @ g @ h @ i @ l @ document_ptr2 @ setter @ v) @ h3)),
% 1.72/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 1.72/0.84 thf(f262,axiom,(
% 1.72/0.84 (((cast_s636919983_p_t_r @ d @ e @ shadow_root_ptr2)) != document_ptr2)),
% 1.72/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_3)).
% 1.72/0.84 thf(f263,conjecture,(
% 1.72/0.84 (heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ n @ (shadow1195525443_o_o_t @ d @ c @ a @ b @ j @ n @ e @ f @ g @ h @ i @ k @ l @ shadow_root_ptr2 @ getter) @ h2 @ h3)),
% 1.72/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_4)).
% 1.72/0.84 thf(f264,negated_conjecture,(
% 1.72/0.84 ~(heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ n @ (shadow1195525443_o_o_t @ d @ c @ a @ b @ j @ n @ e @ f @ g @ h @ i @ k @ l @ shadow_root_ptr2 @ getter) @ h2 @ h3)),
% 1.72/0.84 inference(negated_conjecture,[status(cth)],[f263])).
% 1.72/0.84 thf(f469,plain,(
% 1.72/0.84 ! [X0 : $tType,X1 : $tType,X2 : $tType,X3 : $tType,X4 : $tType,X5 : $tType,X6 : $tType,X7 : $tType,X8 : $tType,X9 : $tType,X10 : $tType,X11 : $tType,X12 : $tType,X13 : $tType,X14 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7,X15 : X4,X16 : (rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 > X12),X17 : document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1,X18 : shadow_root_ptr @ X13,X19 : ((X4 > X4) > rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 > rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0),X20 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7] : ((((cast_s636919983_p_t_r @ X13 @ X1 @ X18)) != X17) => ((heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7 @ exception @ product_unit @ X20 @ (put_M_950607941_e_n_t @ X13 @ X1 @ X4 @ X6 @ X3 @ X2 @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X9 @ X11 @ X10 @ X8 @ X7 @ X17 @ X19 @ X15) @ X14) => (heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7 @ exception @ X12 @ (shadow1195525443_o_o_t @ X13 @ X6 @ X3 @ X2 @ X5 @ X12 @ X1 @ X9 @ X11 @ X10 @ X8 @ X0 @ X7 @ X18 @ X16) @ X20 @ X14)))),
% 1.72/0.84 inference(rectify,[],[f1])).
% 1.72/0.84 thf(f470,plain,(
% 1.72/0.84 ! [X3 : $tType,X10 : $tType,X0 : $tType,X6 : $tType,X9 : $tType,X13 : $tType,X12 : $tType,X2 : $tType,X7 : $tType,X5 : $tType,X1 : $tType,X11 : $tType,X8 : $tType,X4 : $tType,X20 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7,X19 : ((X4 > X4) > rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 > rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0),X14 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7,X16 : (rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 > X12),X15 : X4,X17 : document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1,X18 : shadow_root_ptr @ X13] : ((((cast_s636919983_p_t_r @ X13 @ X1 @ X18)) != X17) => ((((heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7 @ exception @ product_unit @ X20 @ (put_M_950607941_e_n_t @ X13 @ X1 @ X4 @ X6 @ X3 @ X2 @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X9 @ X11 @ X10 @ X8 @ X7 @ X17 @ X19 @ X15) @ X14)) = $true) => ($true = ((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7 @ exception @ X12 @ (shadow1195525443_o_o_t @ X13 @ X6 @ X3 @ X2 @ X5 @ X12 @ X1 @ X9 @ X11 @ X10 @ X8 @ X0 @ X7 @ X18 @ X16) @ X20 @ X14)))))),
% 1.72/0.84 inference(fool_elimination,[],[f469])).
% 1.72/0.84 thf(f497,plain,(
% 1.72/0.84 (heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ product_unit @ h2 @ (put_M_950607941_e_n_t @ d @ e @ m @ c @ a @ b @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ f @ g @ h @ i @ l @ document_ptr2 @ setter @ v) @ h3)),
% 1.72/0.84 inference(rectify,[],[f259])).
% 1.72/0.84 thf(f498,plain,(
% 1.72/0.84 (((heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ product_unit @ h2 @ (put_M_950607941_e_n_t @ d @ e @ m @ c @ a @ b @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ f @ g @ h @ i @ l @ document_ptr2 @ setter @ v) @ h3)) = $true)),
% 1.72/0.84 inference(fool_elimination,[],[f497])).
% 1.72/0.84 thf(f529,plain,(
% 1.72/0.84 ~(heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ n @ (shadow1195525443_o_o_t @ d @ c @ a @ b @ j @ n @ e @ f @ g @ h @ i @ k @ l @ shadow_root_ptr2 @ getter) @ h2 @ h3)),
% 1.72/0.84 inference(rectify,[],[f264])).
% 1.72/0.84 thf(f530,plain,(
% 1.72/0.84 ~ (((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ n @ (shadow1195525443_o_o_t @ d @ c @ a @ b @ j @ n @ e @ f @ g @ h @ i @ k @ l @ shadow_root_ptr2 @ getter) @ h2 @ h3)) = $true)),
% 1.72/0.84 inference(fool_elimination,[],[f529])).
% 1.72/0.84 thf(f700,plain,(
% 1.72/0.84 (((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ n @ (shadow1195525443_o_o_t @ d @ c @ a @ b @ j @ n @ e @ f @ g @ h @ i @ k @ l @ shadow_root_ptr2 @ getter) @ h2 @ h3)) != $true)),
% 1.72/0.84 inference(flattening,[],[f530])).
% 1.72/0.84 thf(f787,plain,(
% 1.72/0.84 ! [X3 : $tType,X10 : $tType,X0 : $tType,X6 : $tType,X9 : $tType,X13 : $tType,X12 : $tType,X2 : $tType,X7 : $tType,X5 : $tType,X1 : $tType,X11 : $tType,X8 : $tType,X4 : $tType,X20 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7,X19 : ((X4 > X4) > rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 > rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0),X14 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7,X16 : (rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 > X12),X15 : X4,X17 : document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1,X18 : shadow_root_ptr @ X13] : ((($true = ((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7 @ exception @ X12 @ (shadow1195525443_o_o_t @ X13 @ X6 @ X3 @ X2 @ X5 @ X12 @ X1 @ X9 @ X11 @ X10 @ X8 @ X0 @ X7 @ X18 @ X16) @ X20 @ X14))) | (((heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7 @ exception @ product_unit @ X20 @ (put_M_950607941_e_n_t @ X13 @ X1 @ X4 @ X6 @ X3 @ X2 @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X9 @ X11 @ X10 @ X8 @ X7 @ X17 @ X19 @ X15) @ X14)) != $true)) | (((cast_s636919983_p_t_r @ X13 @ X1 @ X18)) = X17))),
% 1.72/0.84 inference(ennf_transformation,[],[f470])).
% 1.72/0.84 thf(f788,plain,(
% 1.72/0.84 ! [X10 : $tType,X7 : $tType,X0 : $tType,X11 : $tType,X6 : $tType,X1 : $tType,X8 : $tType,X3 : $tType,X4 : $tType,X12 : $tType,X5 : $tType,X2 : $tType,X9 : $tType,X13 : $tType,X16 : (rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 > X12),X17 : document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1,X15 : X4,X14 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7,X20 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7,X18 : shadow_root_ptr @ X13,X19 : ((X4 > X4) > rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 > rObject_ext @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0)] : ((((cast_s636919983_p_t_r @ X13 @ X1 @ X18)) = X17) | (((heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7 @ exception @ product_unit @ X20 @ (put_M_950607941_e_n_t @ X13 @ X1 @ X4 @ X6 @ X3 @ X2 @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X9 @ X11 @ X10 @ X8 @ X7 @ X17 @ X19 @ X15) @ X14)) != $true) | ($true = ((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X3 @ sum_sum @ character_data_ptr @ X2 @ X6 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X1 @ X9 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X6 @ X3 @ X2 @ X13 @ option @ X11 @ sum_sum @ rCharacterData_ext @ option @ X10 @ X8 @ sum_sum @ rDocument_ext @ X6 @ X3 @ X2 @ option @ sum_sum @ rShadowRoot_ext @ X6 @ X3 @ X2 @ option @ X5 @ X0 @ X7 @ exception @ X12 @ (shadow1195525443_o_o_t @ X13 @ X6 @ X3 @ X2 @ X5 @ X12 @ X1 @ X9 @ X11 @ X10 @ X8 @ X0 @ X7 @ X18 @ X16) @ X20 @ X14))))),
% 1.72/0.84 inference(flattening,[],[f787])).
% 1.72/0.84 thf(f1205,plain,(
% 1.72/0.84 ! [X0 : $tType,X1 : $tType,X2 : $tType,X3 : $tType,X4 : $tType,X5 : $tType,X6 : $tType,X7 : $tType,X8 : $tType,X9 : $tType,X10 : $tType,X11 : $tType,X12 : $tType,X13 : $tType,X14 : (rObject_ext @ rDocument_ext @ X4 @ X7 @ X11 @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 > X9),X15 : document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X5,X16 : X8,X17 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X7 @ sum_sum @ character_data_ptr @ X11 @ X4 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X5 @ X12 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X7 @ X11 @ X13 @ option @ X3 @ sum_sum @ rCharacterData_ext @ option @ X0 @ X6 @ sum_sum @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 @ X1,X18 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X7 @ sum_sum @ character_data_ptr @ X11 @ X4 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X5 @ X12 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X7 @ X11 @ X13 @ option @ X3 @ sum_sum @ rCharacterData_ext @ option @ X0 @ X6 @ sum_sum @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 @ X1,X19 : shadow_root_ptr @ X13,X20 : ((X8 > X8) > rObject_ext @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 > rObject_ext @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2)] : ((((cast_s636919983_p_t_r @ X13 @ X5 @ X19)) = X15) | (((heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X7 @ sum_sum @ character_data_ptr @ X11 @ X4 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X5 @ X12 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X7 @ X11 @ X13 @ option @ X3 @ sum_sum @ rCharacterData_ext @ option @ X0 @ X6 @ sum_sum @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 @ X1 @ exception @ product_unit @ X18 @ (put_M_950607941_e_n_t @ X13 @ X5 @ X8 @ X4 @ X7 @ X11 @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 @ X12 @ X3 @ X0 @ X6 @ X1 @ X15 @ X20 @ X16) @ X17)) != $true) | ($true = ((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X7 @ sum_sum @ character_data_ptr @ X11 @ X4 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X5 @ X12 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X7 @ X11 @ X13 @ option @ X3 @ sum_sum @ rCharacterData_ext @ option @ X0 @ X6 @ sum_sum @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 @ X1 @ exception @ X9 @ (shadow1195525443_o_o_t @ X13 @ X4 @ X7 @ X11 @ X10 @ X9 @ X5 @ X12 @ X3 @ X0 @ X6 @ X2 @ X1 @ X19 @ X14) @ X18 @ X17))))),
% 1.72/0.84 inference(rectify,[],[f788])).
% 1.72/0.84 thf(f1434,plain,(
% 1.72/0.84 (((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ n @ (shadow1195525443_o_o_t @ d @ c @ a @ b @ j @ n @ e @ f @ g @ h @ i @ k @ l @ shadow_root_ptr2 @ getter) @ h2 @ h3)) != $true)),
% 1.72/0.84 inference(cnf_transformation,[],[f700])).
% 1.72/0.84 thf(f1532,plain,(
% 1.72/0.84 ( ! [X13 : $tType,X12 : $tType,X5 : $tType,X9 : $tType,X4 : $tType,X7 : $tType,X8 : $tType,X6 : $tType,X1 : $tType,X11 : $tType,X0 : $tType,X10 : $tType,X3 : $tType,X2 : $tType,X18 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X7 @ sum_sum @ character_data_ptr @ X11 @ X4 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X5 @ X12 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X7 @ X11 @ X13 @ option @ X3 @ sum_sum @ rCharacterData_ext @ option @ X0 @ X6 @ sum_sum @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 @ X1,X16 : X8,X19 : shadow_root_ptr @ X13,X14 : (rObject_ext @ rDocument_ext @ X4 @ X7 @ X11 @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 > X9),X17 : heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X7 @ sum_sum @ character_data_ptr @ X11 @ X4 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X5 @ X12 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X7 @ X11 @ X13 @ option @ X3 @ sum_sum @ rCharacterData_ext @ option @ X0 @ X6 @ sum_sum @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 @ X1,X15 : document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X5,X20 : ((X8 > X8) > rObject_ext @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 > rObject_ext @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2)] : ((((heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X7 @ sum_sum @ character_data_ptr @ X11 @ X4 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X5 @ X12 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X7 @ X11 @ X13 @ option @ X3 @ sum_sum @ rCharacterData_ext @ option @ X0 @ X6 @ sum_sum @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 @ X1 @ exception @ product_unit @ X18 @ (put_M_950607941_e_n_t @ X13 @ X5 @ X8 @ X4 @ X7 @ X11 @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 @ X12 @ X3 @ X0 @ X6 @ X1 @ X15 @ X20 @ X16) @ X17)) != $true) | (((cast_s636919983_p_t_r @ X13 @ X5 @ X19)) = X15) | ($true = ((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ X7 @ sum_sum @ character_data_ptr @ X11 @ X4 @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ X13 @ X5 @ X12 @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ X4 @ X7 @ X11 @ X13 @ option @ X3 @ sum_sum @ rCharacterData_ext @ option @ X0 @ X6 @ sum_sum @ rDocument_ext @ X4 @ X7 @ X11 @ option @ sum_sum @ rShadowRoot_ext @ X4 @ X7 @ X11 @ option @ X10 @ X2 @ X1 @ exception @ X9 @ (shadow1195525443_o_o_t @ X13 @ X4 @ X7 @ X11 @ X10 @ X9 @ X5 @ X12 @ X3 @ X0 @ X6 @ X2 @ X1 @ X19 @ X14) @ X18 @ X17)))) )),
% 1.72/0.84 inference(cnf_transformation,[],[f1205])).
% 1.72/0.84 thf(f1535,plain,(
% 1.72/0.84 (((heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ product_unit @ h2 @ (put_M_950607941_e_n_t @ d @ e @ m @ c @ a @ b @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ f @ g @ h @ i @ l @ document_ptr2 @ setter @ v) @ h3)) = $true)),
% 1.72/0.84 inference(cnf_transformation,[],[f498])).
% 1.72/0.84 thf(f1662,plain,(
% 1.72/0.84 (document_ptr2 != ((cast_s636919983_p_t_r @ d @ e @ shadow_root_ptr2)))),
% 1.72/0.84 inference(cnf_transformation,[],[f262])).
% 1.72/0.84 thf(f1841,definition,(
% 1.72/0.84 spl61_1 <=> (((heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ product_unit @ h2 @ (put_M_950607941_e_n_t @ d @ e @ m @ c @ a @ b @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ f @ g @ h @ i @ l @ document_ptr2 @ setter @ v) @ h3)) = $true)),
% 1.72/0.84 introduced(definition,[new_symbols(definition,[spl61_1])],[avatar_definition])).
% 1.72/0.84 thf(f1843,plain,(
% 1.72/0.84 (((heap_E940394160s_heap @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ product_unit @ h2 @ (put_M_950607941_e_n_t @ d @ e @ m @ c @ a @ b @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ f @ g @ h @ i @ l @ document_ptr2 @ setter @ v) @ h3)) = $true) | ~spl61_1),
% 1.72/0.84 inference(avatar_component_clause,[],[f1841])).
% 1.72/0.84 thf(f1844,plain,(
% 1.72/0.84 spl61_1),
% 1.72/0.84 inference(avatar_split_clause,[],[f1535,f1841])).
% 1.72/0.84 thf(f1846,definition,(
% 1.72/0.84 spl61_2 <=> (document_ptr2 = ((cast_s636919983_p_t_r @ d @ e @ shadow_root_ptr2)))),
% 1.72/0.84 introduced(definition,[new_symbols(definition,[spl61_2])],[avatar_definition])).
% 1.72/0.84 thf(f1848,plain,(
% 1.72/0.84 (document_ptr2 != ((cast_s636919983_p_t_r @ d @ e @ shadow_root_ptr2))) | spl61_2),
% 1.72/0.84 inference(avatar_component_clause,[],[f1846])).
% 1.72/0.84 thf(f1849,plain,(
% 1.72/0.84 ~spl61_2),
% 1.72/0.84 inference(avatar_split_clause,[],[f1662,f1846])).
% 1.72/0.84 thf(f1851,definition,(
% 1.72/0.84 spl61_3 <=> (((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ n @ (shadow1195525443_o_o_t @ d @ c @ a @ b @ j @ n @ e @ f @ g @ h @ i @ k @ l @ shadow_root_ptr2 @ getter) @ h2 @ h3)) = $true)),
% 1.72/0.84 introduced(definition,[new_symbols(definition,[spl61_3])],[avatar_definition])).
% 1.72/0.84 thf(f1853,plain,(
% 1.72/0.84 (((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ n @ (shadow1195525443_o_o_t @ d @ c @ a @ b @ j @ n @ e @ f @ g @ h @ i @ k @ l @ shadow_root_ptr2 @ getter) @ h2 @ h3)) != $true) | spl61_3),
% 1.72/0.84 inference(avatar_component_clause,[],[f1851])).
% 1.72/0.84 thf(f1854,plain,(
% 1.72/0.84 ~spl61_3),
% 1.72/0.84 inference(avatar_split_clause,[],[f1434,f1851])).
% 1.72/0.84 thf(f1863,plain,(
% 1.72/0.84 ( ! [X1 : $tType,X2 : (rObject_ext @ rDocument_ext @ c @ a @ b @ rShadowRoot_ext @ c @ a @ b @ option @ j > X1),X0 : shadow_root_ptr @ d] : (($true = ((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ X1 @ (shadow1195525443_o_o_t @ d @ c @ a @ b @ j @ X1 @ e @ f @ g @ h @ i @ k @ l @ X0 @ X2) @ h2 @ h3))) | (document_ptr2 = ((cast_s636919983_p_t_r @ d @ e @ X0))) | ($true != $true)) ) | ~spl61_1),
% 1.72/0.84 inference(superposition,[],[f1532,f1843])).
% 1.72/0.84 thf(f1864,plain,(
% 1.72/0.84 ( ! [X1 : $tType,X2 : (rObject_ext @ rDocument_ext @ c @ a @ b @ rShadowRoot_ext @ c @ a @ b @ option @ j > X1),X0 : shadow_root_ptr @ d] : (($true = ((heap_Error_preserved @ heap @ sum_sum @ node_ptr @ sum_sum @ element_ptr @ a @ sum_sum @ character_data_ptr @ b @ c @ sum_sum @ document_ptr @ sum_sum @ shadow_root_ptr @ d @ e @ f @ sum_sum @ rNode_ext @ sum_sum @ rElement_ext @ c @ a @ b @ d @ option @ g @ sum_sum @ rCharacterData_ext @ option @ h @ i @ sum_sum @ rDocument_ext @ c @ a @ b @ option @ sum_sum @ rShadowRoot_ext @ c @ a @ b @ option @ j @ k @ l @ exception @ X1 @ (shadow1195525443_o_o_t @ d @ c @ a @ b @ j @ X1 @ e @ f @ g @ h @ i @ k @ l @ X0 @ X2) @ h2 @ h3))) | (document_ptr2 = ((cast_s636919983_p_t_r @ d @ e @ X0)))) ) | ~spl61_1),
% 1.72/0.84 inference(trivial_inequality_removal,[],[f1863])).
% 1.72/0.84 thf(f1891,plain,(
% 1.72/0.84 (document_ptr2 = ((cast_s636919983_p_t_r @ d @ e @ shadow_root_ptr2))) | ($true != $true) | (~spl61_1 | spl61_3)),
% 1.72/0.84 inference(superposition,[],[f1853,f1864])).
% 1.72/0.84 thf(f1892,plain,(
% 1.72/0.84 (document_ptr2 = ((cast_s636919983_p_t_r @ d @ e @ shadow_root_ptr2))) | (~spl61_1 | spl61_3)),
% 1.72/0.84 inference(trivial_inequality_removal,[],[f1891])).
% 1.72/0.84 thf(f1893,plain,(
% 1.72/0.84 $false | (~spl61_1 | spl61_2 | spl61_3)),
% 1.72/0.84 inference(forward_subsumption_resolution,[],[f1892,f1848])).
% 1.72/0.84 thf(f1894,plain,(
% 1.72/0.84 ~spl61_1 | spl61_2 | spl61_3),
% 1.72/0.84 inference(avatar_contradiction_clause,[],[f1893])).
% 1.72/0.84 cnf(s1, plain, spl61_1, inference(sat_conversion,[],[f1844])).
% 1.72/0.84 cnf(s2, plain, ~spl61_2, inference(sat_conversion,[],[f1849])).
% 1.72/0.84 cnf(s3, plain, ~spl61_3, inference(sat_conversion,[],[f1854])).
% 1.72/0.84 cnf(s4, plain, ~spl61_1 | spl61_2 | spl61_3, inference(sat_conversion,[],[f1894])).
% 1.72/0.84 cnf(s5, plain, ~spl61_1, inference(rat,[],[s4,s3,s2])).
% 1.72/0.84 cnf(s6, plain, $false, inference(rat,[],[s1,s5])).
% 1.72/0.84 thf(f1895,plain,(
% 1.72/0.84 $false),
% 1.72/0.84 inference(avatar_sat_refutation,[],[s6])).
% 1.72/0.84 % SZS output end Proof for theBenchmark
% 1.72/0.84 % (290699)------------------------------
% 1.72/0.84 % (290699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.84 % (290699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.84 % (290699)CaDiCaL version: 2.1.3
% 1.72/0.84 % (290699)Termination reason: Refutation
% 1.72/0.84 % (290699)Time elapsed: 0.233 s
% 1.72/0.84 % (290699)Peak memory usage: 19 MB
% 1.72/0.84 % (290699)Instructions burned: 507 (million)
% 1.72/0.84 % (290691)Success in time 0.337 s
% 1.72/0.84 % Vampire exiting
%------------------------------------------------------------------------------