%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : ITP173^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 Oct 7 10:24:35 AM UTC 2026
% Result : Theorem 4.98s 1.09s
% Output : CNFRefutation 4.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 14
% Syntax : Number of formulae : 195 ( 72 unt; 0 typ; 0 def)
% Number of atoms : 1351 ( 422 equ; 0 cnn)
% Maximal formula atoms : 3 ( 6 avg)
% Number of connectives : 1617 ( 192 ~; 279 |; 0 &;1119 @)
% ( 0 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Number of types : 35 ( 34 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 165 ( 162 usr; 16 con; 0-5 aty)
% Number of variables : 510 ( 0 ^; 510 !; 0 ?; 510 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_character_data_ptr_b,type,
character_data_ptr_b: $tType ).
thf(tp_docume1935157360tr_d_e,type,
docume1935157360tr_d_e: $tType ).
thf(tp_element_ptr_a,type,
element_ptr_a: $tType ).
thf(tp_finite1621822014t_char,type,
finite1621822014t_char: $tType ).
thf(tp_heap_E1186645633on_j_k,type,
heap_E1186645633on_j_k: $tType ).
thf(tp_heap_E1188946203tr_d_e,type,
heap_E1188946203tr_d_e: $tType ).
thf(tp_heap_E1661210526_ptr_a,type,
heap_E1661210526_ptr_a: $tType ).
thf(tp_heap_E1735400259tr_b_c,type,
heap_E1735400259tr_b_c: $tType ).
thf(tp_heap_E175696076t_mode,type,
heap_E175696076t_mode: $tType ).
thf(tp_heap_E1770015209t_char,type,
heap_E1770015209t_char: $tType ).
thf(tp_heap_E189844335_ptr_d,type,
heap_E189844335_ptr_d: $tType ).
thf(tp_heap_E1996099391_ptr_b,type,
heap_E1996099391_ptr_b: $tType ).
thf(tp_heap_E434560396t_char,type,
heap_E434560396t_char: $tType ).
thf(tp_heap_E490335273_ptr_d,type,
heap_E490335273_ptr_d: $tType ).
thf(tp_heap_E625070648t_unit,type,
heap_E625070648t_unit: $tType ).
thf(tp_heap_E906991588_ptr_a,type,
heap_E906991588_ptr_a: $tType ).
thf(tp_heap_S1465075775_j_k_l,type,
heap_S1465075775_j_k_l: $tType ).
thf(tp_list_char,type,
list_char: $tType ).
thf(tp_list_n282880152tr_b_c,type,
list_n282880152tr_b_c: $tType ).
thf(tp_node_p1234578834tr_b_c,type,
node_p1234578834tr_b_c: $tType ).
thf(tp_object945351580_d_e_f,type,
object945351580_d_e_f: $tType ).
thf(tp_option1029218147tion_j,type,
option1029218147tion_j: $tType ).
thf(tp_option147517124_ptr_d,type,
option147517124_ptr_d: $tType ).
thf(tp_option841825948on_j_k,type,
option841825948on_j_k: $tType ).
thf(tp_option_element_ptr_a,type,
option_element_ptr_a: $tType ).
thf(tp_product_unit,type,
product_unit: $tType ).
thf(tp_rObjec1148923485tion_h,type,
rObjec1148923485tion_h: $tType ).
thf(tp_rObjec1413572695_j_k_l,type,
rObjec1413572695_j_k_l: $tType ).
thf(tp_rObjec1617416918on_j_k,type,
rObjec1617416918on_j_k: $tType ).
thf(tp_rObjec1875798643tion_g,type,
rObjec1875798643tion_g: $tType ).
thf(tp_rObjec1922030987on_h_i,type,
rObjec1922030987on_h_i: $tType ).
thf(tp_rObjec2068690451tion_j,type,
rObjec2068690451tion_j: $tType ).
thf(tp_shadow_root_mode,type,
shadow_root_mode: $tType ).
thf(tp_shadow_root_ptr_d,type,
shadow_root_ptr_d: $tType ).
thf(tp_attrs_1280717024tion_g,type,
attrs_1280717024tion_g: ( finite1621822014t_char > finite1621822014t_char ) > rObjec1875798643tion_g > rObjec1875798643tion_g ).
thf(tp_case_o738567654on_j_k,type,
case_o738567654on_j_k: option1029218147tion_j > ( rObjec1617416918on_j_k > option1029218147tion_j ) > option841825948on_j_k > option1029218147tion_j ).
thf(tp_cast_C1209085999_d_g_i,type,
cast_C1209085999_d_g_i: rObjec1148923485tion_h > rObjec1922030987on_h_i ).
thf(tp_cast_D1046746849_b_j_k,type,
cast_D1046746849_b_j_k: rObjec1617416918on_j_k > option1029218147tion_j ).
thf(tp_cast_D1252964113_h_i_l,type,
cast_D1252964113_h_i_l: rObjec1617416918on_j_k > rObjec1413572695_j_k_l ).
thf(tp_cast_E1779426770on_h_i,type,
cast_E1779426770on_h_i: rObjec1875798643tion_g > rObjec1922030987on_h_i ).
thf(tp_cast_N1183075319_j_k_l,type,
cast_N1183075319_j_k_l: rObjec1922030987on_h_i > rObjec1413572695_j_k_l ).
thf(tp_cast_O1034441233_j_k_l,type,
cast_O1034441233_j_k_l: rObjec1413572695_j_k_l > option841825948on_j_k ).
thf(tp_cast_S988036065_b_j_k,type,
cast_S988036065_b_j_k: rObjec2068690451tion_j > rObjec1617416918on_j_k ).
thf(tp_cast_c164415100_b_a_c,type,
cast_c164415100_b_a_c: character_data_ptr_b > node_p1234578834tr_b_c ).
thf(tp_cast_d1608273229_b_c_f,type,
cast_d1608273229_b_c_f: docume1935157360tr_d_e > object945351580_d_e_f ).
thf(tp_cast_e316309897tr_b_c,type,
cast_e316309897tr_b_c: element_ptr_a > node_p1234578834tr_b_c ).
thf(tp_cast_n552817316_d_e_f,type,
cast_n552817316_d_e_f: node_p1234578834tr_b_c > object945351580_d_e_f ).
thf(tp_cast_s253715760_r_d_e,type,
cast_s253715760_r_d_e: shadow_root_ptr_d > docume1935157360tr_d_e ).
thf(tp_child_1596411111tion_g,type,
child_1596411111tion_g: ( list_n282880152tr_b_c > list_n282880152tr_b_c ) > rObjec1875798643tion_g > rObjec1875798643tion_g ).
thf(tp_child_1619758758tion_j,type,
child_1619758758tion_j: ( list_n282880152tr_b_c > list_n282880152tr_b_c ) > rObjec2068690451tion_j > rObjec2068690451tion_j ).
thf(tp_child_803420283tion_j,type,
child_803420283tion_j: rObjec2068690451tion_j > list_n282880152tr_b_c ).
thf(tp_discon442323090on_j_k,type,
discon442323090on_j_k: ( list_n282880152tr_b_c > list_n282880152tr_b_c ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ).
thf(tp_discon866287741on_j_k,type,
discon866287741on_j_k: rObjec1617416918on_j_k > list_n282880152tr_b_c ).
thf(tp_doctyp68000440on_j_k,type,
doctyp68000440on_j_k: ( list_char > list_char ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ).
thf(tp_doctyp814403297on_j_k,type,
doctyp814403297on_j_k: rObjec1617416918on_j_k > list_char ).
thf(tp_docume1175131570on_j_k,type,
docume1175131570on_j_k: rObjec1617416918on_j_k > option_element_ptr_a ).
thf(tp_docume244715269on_j_k,type,
docume244715269on_j_k: ( option_element_ptr_a > option_element_ptr_a ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ).
thf(tp_document_ptr,type,
document_ptr: docume1935157360tr_d_e ).
thf(tp_get_D_1192261494_j_k_l,type,
get_D_1192261494_j_k_l: docume1935157360tr_d_e > heap_S1465075775_j_k_l > option841825948on_j_k ).
thf(tp_get_M_1030798962on_j_k,type,
get_M_1030798962on_j_k: object945351580_d_e_f > ( rObjec1413572695_j_k_l > rObjec1617416918on_j_k ) > heap_E1186645633on_j_k ).
thf(tp_get_M_1086441344_j_k_l,type,
get_M_1086441344_j_k_l: character_data_ptr_b > ( rObjec1148923485tion_h > shadow_root_ptr_d ) > heap_E490335273_ptr_d ).
thf(tp_get_M_1154267419_j_k_l,type,
get_M_1154267419_j_k_l: element_ptr_a > ( rObjec1875798643tion_g > option147517124_ptr_d ) > heap_E189844335_ptr_d ).
thf(tp_get_M_1238860946_j_k_l,type,
get_M_1238860946_j_k_l: element_ptr_a > ( rObjec1875798643tion_g > product_unit ) > heap_E625070648t_unit ).
thf(tp_get_M_1524345318_j_k_l,type,
get_M_1524345318_j_k_l: element_ptr_a > ( rObjec1875798643tion_g > option_element_ptr_a ) > heap_E906991588_ptr_a ).
thf(tp_get_M_1536717772_h_i_l,type,
get_M_1536717772_h_i_l: docume1935157360tr_d_e > ( rObjec1617416918on_j_k > list_char ) > heap_E434560396t_char ).
thf(tp_get_M_1723352102_h_i_l,type,
get_M_1723352102_h_i_l: docume1935157360tr_d_e > ( rObjec1617416918on_j_k > option_element_ptr_a ) > heap_E906991588_ptr_a ).
thf(tp_get_M_1865279188_j_k_l,type,
get_M_1865279188_j_k_l: character_data_ptr_b > ( rObjec1148923485tion_h > docume1935157360tr_d_e ) > heap_E1188946203tr_d_e ).
thf(tp_get_M_1899318715_j_k_l,type,
get_M_1899318715_j_k_l: character_data_ptr_b > ( rObjec1148923485tion_h > option_element_ptr_a ) > heap_E906991588_ptr_a ).
thf(tp_get_M_1903403023_j_k_l,type,
get_M_1903403023_j_k_l: character_data_ptr_b > ( rObjec1148923485tion_h > product_unit ) > heap_E625070648t_unit ).
thf(tp_get_M_1965837010_h_i_l,type,
get_M_1965837010_h_i_l: docume1935157360tr_d_e > ( rObjec1617416918on_j_k > product_unit ) > heap_E625070648t_unit ).
thf(tp_get_M_1990067849_j_k_l,type,
get_M_1990067849_j_k_l: element_ptr_a > ( rObjec1875798643tion_g > rObjec1617416918on_j_k ) > heap_E1186645633on_j_k ).
thf(tp_get_M_2008432865_j_k_l,type,
get_M_2008432865_j_k_l: element_ptr_a > ( rObjec1875798643tion_g > shadow_root_ptr_d ) > heap_E490335273_ptr_d ).
thf(tp_get_M_2088872005_j_k_l,type,
get_M_2088872005_j_k_l: character_data_ptr_b > ( rObjec1148923485tion_h > list_char ) > heap_E434560396t_char ).
thf(tp_get_M_2133515608_j_k_l,type,
get_M_2133515608_j_k_l: character_data_ptr_b > ( rObjec1148923485tion_h > rObjec1617416918on_j_k ) > heap_E1186645633on_j_k ).
thf(tp_get_M_462148605_h_i_l,type,
get_M_462148605_h_i_l: docume1935157360tr_d_e > ( rObjec1617416918on_j_k > docume1935157360tr_d_e ) > heap_E1188946203tr_d_e ).
thf(tp_get_M_51280086_j_k_l,type,
get_M_51280086_j_k_l: element_ptr_a > ( rObjec1875798643tion_g > list_char ) > heap_E434560396t_char ).
thf(tp_get_M_537718945_h_i_l,type,
get_M_537718945_h_i_l: docume1935157360tr_d_e > ( rObjec1617416918on_j_k > shadow_root_ptr_d ) > heap_E490335273_ptr_d ).
thf(tp_get_M_650077447_j_k_l,type,
get_M_650077447_j_k_l: element_ptr_a > ( rObjec1875798643tion_g > docume1935157360tr_d_e ) > heap_E1188946203tr_d_e ).
thf(tp_get_M_685446945_j_k_l,type,
get_M_685446945_j_k_l: element_ptr_a > ( rObjec1875798643tion_g > finite1621822014t_char ) > heap_E1770015209t_char ).
thf(tp_get_M_88885319_j_k_l,type,
get_M_88885319_j_k_l: element_ptr_a > ( rObjec1875798643tion_g > list_n282880152tr_b_c ) > heap_E1735400259tr_b_c ).
thf(tp_get_M_922904437_j_k_l,type,
get_M_922904437_j_k_l: node_p1234578834tr_b_c > ( rObjec1922030987on_h_i > rObjec1617416918on_j_k ) > heap_E1186645633on_j_k ).
thf(tp_get_M_970800329_h_i_l,type,
get_M_970800329_h_i_l: docume1935157360tr_d_e > ( rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > heap_E1186645633on_j_k ).
thf(tp_get_M_986049031_h_i_l,type,
get_M_986049031_h_i_l: docume1935157360tr_d_e > ( rObjec1617416918on_j_k > list_n282880152tr_b_c ) > heap_E1735400259tr_b_c ).
thf(tp_get_S_806277408_j_k_l,type,
get_S_806277408_j_k_l: shadow_root_ptr_d > heap_S1465075775_j_k_l > option1029218147tion_j ).
thf(tp_h,type,
h: heap_S1465075775_j_k_l ).
thf(tp_h2,type,
h2: heap_S1465075775_j_k_l ).
thf(tp_heap_E1091541499_ptr_a,type,
heap_E1091541499_ptr_a: heap_S1465075775_j_k_l > heap_E906991588_ptr_a > option_element_ptr_a > $o ).
thf(tp_heap_E1224694197_ptr_a,type,
heap_E1224694197_ptr_a: heap_S1465075775_j_k_l > heap_E1661210526_ptr_a > element_ptr_a > $o ).
thf(tp_heap_E1282695852_ptr_a,type,
heap_E1282695852_ptr_a: heap_S1465075775_j_k_l > heap_E906991588_ptr_a > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E1358110656on_j_k,type,
heap_E1358110656on_j_k: heap_E1186645633on_j_k > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E143427264_ptr_d,type,
heap_E143427264_ptr_d: heap_S1465075775_j_k_l > heap_E490335273_ptr_d > shadow_root_ptr_d > $o ).
thf(tp_heap_E1521571831t_unit,type,
heap_E1521571831t_unit: heap_E625070648t_unit > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E1531219875_ptr_a,type,
heap_E1531219875_ptr_a: heap_E906991588_ptr_a > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E1554207190_ptr_b,type,
heap_E1554207190_ptr_b: heap_S1465075775_j_k_l > heap_E1996099391_ptr_b > character_data_ptr_b > $o ).
thf(tp_heap_E1613639261eption,type,
heap_E1613639261eption: heap_E625070648t_unit ).
thf(tp_heap_E1655614900_ptr_d,type,
heap_E1655614900_ptr_d: heap_S1465075775_j_k_l > heap_E490335273_ptr_d > shadow_root_ptr_d > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E1679280842_ptr_b,type,
heap_E1679280842_ptr_b: heap_S1465075775_j_k_l > heap_E1996099391_ptr_b > character_data_ptr_b > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E1720378810tr_d_e,type,
heap_E1720378810tr_d_e: heap_S1465075775_j_k_l > heap_E1188946203tr_d_e > docume1935157360tr_d_e > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E1738949233_ptr_d,type,
heap_E1738949233_ptr_d: heap_S1465075775_j_k_l > heap_E490335273_ptr_d > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E1876089495eption,type,
heap_E1876089495eption: heap_S1465075775_j_k_l > heap_E625070648t_unit ).
thf(tp_heap_E1947147782_ptr_d,type,
heap_E1947147782_ptr_d: heap_S1465075775_j_k_l > heap_E189844335_ptr_d > option147517124_ptr_d > $o ).
thf(tp_heap_E1982034951_ptr_b,type,
heap_E1982034951_ptr_b: heap_S1465075775_j_k_l > heap_E1996099391_ptr_b > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E1993614659t_unit,type,
heap_E1993614659t_unit: heap_S1465075775_j_k_l > heap_E625070648t_unit > product_unit > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E2046843837tr_d_e,type,
heap_E2046843837tr_d_e: heap_S1465075775_j_k_l > heap_E1188946203tr_d_e > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E2092016297_ptr_a,type,
heap_E2092016297_ptr_a: heap_S1465075775_j_k_l > heap_E1661210526_ptr_a > element_ptr_a > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E2101731758tr_d_e,type,
heap_E2101731758tr_d_e: heap_S1465075775_j_k_l > heap_E1188946203tr_d_e > docume1935157360tr_d_e > $o ).
thf(tp_heap_E2123723880_ptr_d,type,
heap_E2123723880_ptr_d: heap_E490335273_ptr_d > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E24690662_ptr_a,type,
heap_E24690662_ptr_a: heap_S1465075775_j_k_l > heap_E1661210526_ptr_a > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E258692314tr_b_c,type,
heap_E258692314tr_b_c: heap_S1465075775_j_k_l > heap_E1735400259tr_b_c > list_n282880152tr_b_c > $o ).
thf(tp_heap_E456877295_ptr_a,type,
heap_E456877295_ptr_a: heap_S1465075775_j_k_l > heap_E906991588_ptr_a > option_element_ptr_a > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E494191872t_unit,type,
heap_E494191872t_unit: heap_S1465075775_j_k_l > heap_E625070648t_unit > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E604544536on_j_k,type,
heap_E604544536on_j_k: heap_S1465075775_j_k_l > heap_E1186645633on_j_k > rObjec1617416918on_j_k > $o ).
thf(tp_heap_E64317923t_mode,type,
heap_E64317923t_mode: heap_S1465075775_j_k_l > heap_E175696076t_mode > shadow_root_mode > $o ).
thf(tp_heap_E648129097on_j_k,type,
heap_E648129097on_j_k: heap_S1465075775_j_k_l > heap_E1186645633on_j_k > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E667013711t_unit,type,
heap_E667013711t_unit: heap_S1465075775_j_k_l > heap_E625070648t_unit > product_unit > $o ).
thf(tp_heap_E804379039t_char,type,
heap_E804379039t_char: heap_S1465075775_j_k_l > heap_E434560396t_char > list_char > $o ).
thf(tp_heap_E808638982tr_d_e,type,
heap_E808638982tr_d_e: heap_E1188946203tr_d_e > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E819109644on_j_k,type,
heap_E819109644on_j_k: heap_S1465075775_j_k_l > heap_E1186645633on_j_k > rObjec1617416918on_j_k > heap_S1465075775_j_k_l > $o ).
thf(tp_heap_E946351744t_char,type,
heap_E946351744t_char: heap_S1465075775_j_k_l > heap_E1770015209t_char > finite1621822014t_char > $o ).
thf(tp_id_ROb1998049991on_j_k,type,
id_ROb1998049991on_j_k: rObjec1617416918on_j_k > rObjec1617416918on_j_k ).
thf(tp_is_cha504820986_t_r_b,type,
is_cha504820986_t_r_b: character_data_ptr_b > $o ).
thf(tp_is_doc1417632087_j_k_l,type,
is_doc1417632087_j_k_l: rObjec1413572695_j_k_l > $o ).
thf(tp_is_doc2037328342tr_d_e,type,
is_doc2037328342tr_d_e: docume1935157360tr_d_e > $o ).
thf(tp_is_doc45233057_d_e_f,type,
is_doc45233057_d_e_f: object945351580_d_e_f > $o ).
thf(tp_is_ele1129207902_t_r_a,type,
is_ele1129207902_t_r_a: element_ptr_a > $o ).
thf(tp_is_sha1522929624_b_j_k,type,
is_sha1522929624_b_j_k: rObjec1617416918on_j_k > $o ).
thf(tp_l_get_1351119336on_j_k,type,
l_get_1351119336on_j_k: ( docume1935157360tr_d_e > heap_S1465075775_j_k_l > option841825948on_j_k ) > docume1935157360tr_d_e > ( rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > heap_E1186645633on_j_k ).
thf(tp_l_get_2096691839_j_k_l,type,
l_get_2096691839_j_k_l: ( heap_S1465075775_j_k_l > $o ) > $o ).
thf(tp_l_get_253860503_j_k_l,type,
l_get_253860503_j_k_l: ( heap_S1465075775_j_k_l > $o ) > $o ).
thf(tp_l_new_1474790279_j_k_l,type,
l_new_1474790279_j_k_l: ( heap_S1465075775_j_k_l > $o ) > $o ).
thf(tp_l_new_410495338_j_k_l,type,
l_new_410495338_j_k_l: ( heap_S1465075775_j_k_l > $o ) > $o ).
thf(tp_l_new_540233301_j_k_l,type,
l_new_540233301_j_k_l: ( heap_S1465075775_j_k_l > $o ) > $o ).
thf(tp_l_put_38398219_ptr_a,type,
l_put_38398219_ptr_a: ( docume1935157360tr_d_e > heap_S1465075775_j_k_l > option841825948on_j_k ) > ( docume1935157360tr_d_e > rObjec1617416918on_j_k > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l ) > docume1935157360tr_d_e > ( ( option_element_ptr_a > option_element_ptr_a ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > option_element_ptr_a > heap_E625070648t_unit ).
thf(tp_l_type1130145226_j_k_l,type,
l_type1130145226_j_k_l: heap_S1465075775_j_k_l > $o ).
thf(tp_l_type648988564_j_k_l,type,
l_type648988564_j_k_l: heap_S1465075775_j_k_l > $o ).
thf(tp_l_type85280056_j_k_l,type,
l_type85280056_j_k_l: heap_S1465075775_j_k_l > $o ).
thf(tp_mode_c_a_b_option_j,type,
mode_c_a_b_option_j: rObjec2068690451tion_j > shadow_root_mode ).
thf(tp_mode_u388060498tion_j,type,
mode_u388060498tion_j: ( shadow_root_mode > shadow_root_mode ) > rObjec2068690451tion_j > rObjec2068690451tion_j ).
thf(tp_new_ch829669006_j_k_l,type,
new_ch829669006_j_k_l: heap_E1996099391_ptr_b ).
thf(tp_new_do4779043_j_k_l,type,
new_do4779043_j_k_l: heap_E1188946203tr_d_e ).
thf(tp_new_el717272935_j_k_l,type,
new_el717272935_j_k_l: heap_E1661210526_ptr_a ).
thf(tp_nil_no279930520tr_b_c,type,
nil_no279930520tr_b_c: list_n282880152tr_b_c ).
thf(tp_none_R125524722tion_j,type,
none_R125524722tion_j: option1029218147tion_j ).
thf(tp_none_R1587534007on_j_k,type,
none_R1587534007on_j_k: option841825948on_j_k ).
thf(tp_put_D_2126422573_h_i_l,type,
put_D_2126422573_h_i_l: docume1935157360tr_d_e > rObjec1617416918on_j_k > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l ).
thf(tp_put_M_1098917052_j_k_l,type,
put_M_1098917052_j_k_l: element_ptr_a > ( ( list_n282880152tr_b_c > list_n282880152tr_b_c ) > rObjec1875798643tion_g > rObjec1875798643tion_g ) > list_n282880152tr_b_c > heap_E625070648t_unit ).
thf(tp_put_M_1101791239_j_k_l,type,
put_M_1101791239_j_k_l: element_ptr_a > ( ( product_unit > product_unit ) > rObjec1875798643tion_g > rObjec1875798643tion_g ) > product_unit > heap_E625070648t_unit ).
thf(tp_put_M_1236788814_j_k_l,type,
put_M_1236788814_j_k_l: element_ptr_a > ( ( docume1935157360tr_d_e > docume1935157360tr_d_e ) > rObjec1875798643tion_g > rObjec1875798643tion_g ) > docume1935157360tr_d_e > heap_E625070648t_unit ).
thf(tp_put_M_1288574284_j_k_l,type,
put_M_1288574284_j_k_l: character_data_ptr_b > ( ( option_element_ptr_a > option_element_ptr_a ) > rObjec1148923485tion_h > rObjec1148923485tion_h ) > option_element_ptr_a > heap_E625070648t_unit ).
thf(tp_put_M_1374331384_j_k_l,type,
put_M_1374331384_j_k_l: character_data_ptr_b > ( ( product_unit > product_unit ) > rObjec1148923485tion_h > rObjec1148923485tion_h ) > product_unit > heap_E625070648t_unit ).
thf(tp_put_M_139724992_h_i_l,type,
put_M_139724992_h_i_l: docume1935157360tr_d_e > ( ( list_n282880152tr_b_c > list_n282880152tr_b_c ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > list_n282880152tr_b_c > heap_E625070648t_unit ).
thf(tp_put_M_1442125025_h_i_l,type,
put_M_1442125025_h_i_l: docume1935157360tr_d_e > ( ( option_element_ptr_a > option_element_ptr_a ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > option_element_ptr_a > heap_E625070648t_unit ).
thf(tp_put_M_1494070654_j_k_l,type,
put_M_1494070654_j_k_l: element_ptr_a > ( ( rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > rObjec1875798643tion_g > rObjec1875798643tion_g ) > rObjec1617416918on_j_k > heap_E625070648t_unit ).
thf(tp_put_M_1534590374_h_i_l,type,
put_M_1534590374_h_i_l: docume1935157360tr_d_e > ( ( shadow_root_ptr_d > shadow_root_ptr_d ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > shadow_root_ptr_d > heap_E625070648t_unit ).
thf(tp_put_M_1656033077_h_i_l,type,
put_M_1656033077_h_i_l: docume1935157360tr_d_e > ( ( product_unit > product_unit ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > product_unit > heap_E625070648t_unit ).
thf(tp_put_M_1672180822_j_k_l,type,
put_M_1672180822_j_k_l: element_ptr_a > ( ( shadow_root_ptr_d > shadow_root_ptr_d ) > rObjec1875798643tion_g > rObjec1875798643tion_g ) > shadow_root_ptr_d > heap_E625070648t_unit ).
thf(tp_put_M_1720094109_j_k_l,type,
put_M_1720094109_j_k_l: element_ptr_a > ( ( list_char > list_char ) > rObjec1875798643tion_g > rObjec1875798643tion_g ) > list_char > heap_E625070648t_unit ).
thf(tp_put_M_1724091798_j_k_l,type,
put_M_1724091798_j_k_l: element_ptr_a > ( ( finite1621822014t_char > finite1621822014t_char ) > rObjec1875798643tion_g > rObjec1875798643tion_g ) > finite1621822014t_char > heap_E625070648t_unit ).
thf(tp_put_M_1888382407_j_k_l,type,
put_M_1888382407_j_k_l: character_data_ptr_b > ( ( shadow_root_ptr_d > shadow_root_ptr_d ) > rObjec1148923485tion_h > rObjec1148923485tion_h ) > shadow_root_ptr_d > heap_E625070648t_unit ).
thf(tp_put_M_1937380872_j_k_l,type,
put_M_1937380872_j_k_l: character_data_ptr_b > ( ( list_char > list_char ) > rObjec1148923485tion_h > rObjec1148923485tion_h ) > list_char > heap_E625070648t_unit ).
thf(tp_put_M_2097930918_h_i_l,type,
put_M_2097930918_h_i_l: docume1935157360tr_d_e > ( ( docume1935157360tr_d_e > docume1935157360tr_d_e ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > docume1935157360tr_d_e > heap_E625070648t_unit ).
thf(tp_put_M_257417239_h_i_l,type,
put_M_257417239_h_i_l: docume1935157360tr_d_e > ( ( list_char > list_char ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > list_char > heap_E625070648t_unit ).
thf(tp_put_M_430230363_j_k_l,type,
put_M_430230363_j_k_l: element_ptr_a > ( ( option_element_ptr_a > option_element_ptr_a ) > rObjec1875798643tion_g > rObjec1875798643tion_g ) > option_element_ptr_a > heap_E625070648t_unit ).
thf(tp_put_M_643150959_j_k_l,type,
put_M_643150959_j_k_l: character_data_ptr_b > ( ( rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > rObjec1148923485tion_h > rObjec1148923485tion_h ) > rObjec1617416918on_j_k > heap_E625070648t_unit ).
thf(tp_put_M_657600638_h_i_l,type,
put_M_657600638_h_i_l: docume1935157360tr_d_e > ( ( rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > rObjec1617416918on_j_k > heap_E625070648t_unit ).
thf(tp_put_M_682984464_j_k_l,type,
put_M_682984464_j_k_l: element_ptr_a > ( ( option147517124_ptr_d > option147517124_ptr_d ) > rObjec1875798643tion_g > rObjec1875798643tion_g ) > option147517124_ptr_d > heap_E625070648t_unit ).
thf(tp_put_M_726238649_j_k_l,type,
put_M_726238649_j_k_l: character_data_ptr_b > ( ( docume1935157360tr_d_e > docume1935157360tr_d_e ) > rObjec1148923485tion_h > rObjec1148923485tion_h ) > docume1935157360tr_d_e > heap_E625070648t_unit ).
thf(tp_put_N_1605479107_j_k_l,type,
put_N_1605479107_j_k_l: node_p1234578834tr_b_c > rObjec1922030987on_h_i > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l ).
thf(tp_put_O_834343516_j_k_l,type,
put_O_834343516_j_k_l: object945351580_d_e_f > rObjec1413572695_j_k_l > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l ).
thf(tp_put_S_1800307733_i_k_l,type,
put_S_1800307733_i_k_l: shadow_root_ptr_d > rObjec2068690451tion_j > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l ).
thf(tp_shadow1068876397_i_k_l,type,
shadow1068876397_i_k_l: shadow_root_ptr_d > ( rObjec2068690451tion_j > docume1935157360tr_d_e ) > heap_E1188946203tr_d_e ).
thf(tp_shadow1110190411_i_k_l,type,
shadow1110190411_i_k_l: shadow_root_ptr_d > ( ( product_unit > product_unit ) > rObjec2068690451tion_j > rObjec2068690451tion_j ) > product_unit > heap_E625070648t_unit ).
thf(tp_shadow1130895149_i_k_l,type,
shadow1130895149_i_k_l: shadow_root_ptr_d > ( rObjec2068690451tion_j > shadow_root_ptr_d ) > heap_E490335273_ptr_d ).
thf(tp_shadow1171208754_i_k_l,type,
shadow1171208754_i_k_l: shadow_root_ptr_d > ( rObjec2068690451tion_j > option_element_ptr_a ) > heap_E906991588_ptr_a ).
thf(tp_shadow1445656130_i_k_l,type,
shadow1445656130_i_k_l: shadow_root_ptr_d > ( ( rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > rObjec2068690451tion_j > rObjec2068690451tion_j ) > rObjec1617416918on_j_k > heap_E625070648t_unit ).
thf(tp_shadow1464843188_i_k_l,type,
shadow1464843188_i_k_l: shadow_root_ptr_d > ( ( docume1935157360tr_d_e > docume1935157360tr_d_e ) > rObjec2068690451tion_j > rObjec2068690451tion_j ) > docume1935157360tr_d_e > heap_E625070648t_unit ).
thf(tp_shadow1606659473tion_g,type,
shadow1606659473tion_g: ( option147517124_ptr_d > option147517124_ptr_d ) > rObjec1875798643tion_g > rObjec1875798643tion_g ).
thf(tp_shadow1961719995_j_k_l,type,
shadow1961719995_j_k_l: shadow_root_ptr_d > heap_E625070648t_unit ).
thf(tp_shadow2050000606_i_k_l,type,
shadow2050000606_i_k_l: shadow_root_ptr_d > ( rObjec2068690451tion_j > product_unit ) > heap_E625070648t_unit ).
thf(tp_shadow2101372501_i_k_l,type,
shadow2101372501_i_k_l: shadow_root_ptr_d > ( rObjec2068690451tion_j > rObjec1617416918on_j_k ) > heap_E1186645633on_j_k ).
thf(tp_shadow46861722_i_k_l,type,
shadow46861722_i_k_l: shadow_root_ptr_d > ( ( shadow_root_ptr_d > shadow_root_ptr_d ) > rObjec2068690451tion_j > rObjec2068690451tion_j ) > shadow_root_ptr_d > heap_E625070648t_unit ).
thf(tp_shadow606335434_i_k_l,type,
shadow606335434_i_k_l: shadow_root_ptr_d > ( rObjec2068690451tion_j > shadow_root_mode ) > heap_E175696076t_mode ).
thf(tp_shadow641561368_j_k_l,type,
shadow641561368_j_k_l: heap_E490335273_ptr_d ).
thf(tp_shadow722206742_j_k_l,type,
shadow722206742_j_k_l: ( heap_S1465075775_j_k_l > $o ) > $o ).
thf(tp_shadow759301011_i_k_l,type,
shadow759301011_i_k_l: shadow_root_ptr_d > ( rObjec2068690451tion_j > list_n282880152tr_b_c ) > heap_E1735400259tr_b_c ).
thf(tp_shadow972335775_i_k_l,type,
shadow972335775_i_k_l: shadow_root_ptr_d > ( ( option_element_ptr_a > option_element_ptr_a ) > rObjec2068690451tion_j > rObjec2068690451tion_j ) > option_element_ptr_a > heap_E625070648t_unit ).
thf(tp_shadow_root_Open,type,
shadow_root_Open: shadow_root_mode ).
thf(tp_tag_na7058269tion_g,type,
tag_na7058269tion_g: ( list_char > list_char ) > rObjec1875798643tion_g > rObjec1875798643tion_g ).
thf(tp_the_RO2055010943tion_j,type,
the_RO2055010943tion_j: option1029218147tion_j > rObjec2068690451tion_j ).
thf(tp_type_w1479951274_j_k_l,type,
type_w1479951274_j_k_l: heap_S1465075775_j_k_l > $o ).
thf(tp_type_w1771507213_j_k_l,type,
type_w1771507213_j_k_l: heap_S1465075775_j_k_l > $o ).
thf(tp_type_w697503069_j_k_l,type,
type_w697503069_j_k_l: heap_S1465075775_j_k_l > $o ).
thf(tp_type_w92696601_j_k_l,type,
type_w92696601_j_k_l: heap_S1465075775_j_k_l > $o ).
thf(tp_v,type,
v: option_element_ptr_a ).
thf(tp_val_update_option_h,type,
val_update_option_h: ( list_char > list_char ) > rObjec1148923485tion_h > rObjec1148923485tion_h ).
thf(tp_x,type,
x: rObjec1617416918on_j_k ).
thf(93,axiom,
! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: option147517124_ptr_d,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_682984464_j_k_l @ Element_ptr @ shadow1606659473tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_262_ElementMonad_Oput__M_092_060_094sub_062E_092_060_094sub_062l_092_060_094sub_062e_092_060_094sub_062m_092_060_094sub_062e_092_060_094sub_062n_092_060_094sub_062t__shadow__root__opt__type__wf__preserved) ).
thf(98,axiom,
l_new_540233301_j_k_l @ type_w697503069_j_k_l,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_257_ElementMonad_Onew__element__is__l__new__element) ).
thf(124,axiom,
! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: list_n282880152tr_b_c,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_1098917052_j_k_l @ Element_ptr @ child_1596411111tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_ElementMonad_Oput__M_092_060_094sub_062E_092_060_094sub_062l_092_060_094sub_062e_092_060_094sub_062m_092_060_094sub_062e_092_060_094sub_062n_092_060_094sub_062t__child__nodes__type__wf__preserved) ).
thf(125,axiom,
! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: list_char,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_1720094109_j_k_l @ Element_ptr @ tag_na7058269tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_ElementMonad_Oput__M_092_060_094sub_062E_092_060_094sub_062l_092_060_094sub_062e_092_060_094sub_062m_092_060_094sub_062e_092_060_094sub_062n_092_060_094sub_062t__tag__name__type__wf__preserved) ).
thf(126,axiom,
! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: finite1621822014t_char,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_1724091798_j_k_l @ Element_ptr @ attrs_1280717024tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_ElementMonad_Oput__M_092_060_094sub_062E_092_060_094sub_062l_092_060_094sub_062e_092_060_094sub_062m_092_060_094sub_062e_092_060_094sub_062n_092_060_094sub_062t__attrs__type__wf__preserved) ).
thf(128,axiom,
! [H: heap_S1465075775_j_k_l,H2: heap_S1465075775_j_k_l] :
( ( heap_E24690662_ptr_a @ H @ new_el717272935_j_k_l @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_ElementMonad_Onew__element__type__wf__preserved) ).
thf(215,axiom,
! [H: heap_S1465075775_j_k_l] :
( ( type_w1771507213_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_CharacterDataClass_Otype__wf_092_060_094sub_062E_092_060_094sub_062l_092_060_094sub_062e_092_060_094sub_062m_092_060_094sub_062e_092_060_094sub_062n_092_060_094sub_062t) ).
thf(307,axiom,
! [H: heap_S1465075775_j_k_l] :
( ( type_w1479951274_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_DocumentClass_Otype__wf_092_060_094sub_062E_092_060_094sub_062l_092_060_094sub_062e_092_060_094sub_062m_092_060_094sub_062e_092_060_094sub_062n_092_060_094sub_062t) ).
thf(311,axiom,
l_get_2096691839_j_k_l @ type_w697503069_j_k_l,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_ElementClass_Ol__get_092_060_094sub_062E_092_060_094sub_062l_092_060_094sub_062e_092_060_094sub_062m_092_060_094sub_062e_092_060_094sub_062n_092_060_094sub_062t__lemmas__axioms) ).
thf(317,axiom,
type_w697503069_j_k_l = l_type85280056_j_k_l,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_ElementClass_Otype__wf__def) ).
thf(349,axiom,
! [H: heap_S1465075775_j_k_l] :
( ( type_w697503069_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_ElementClass_Otype__wf_092_060_094sub_062E_092_060_094sub_062l_092_060_094sub_062e_092_060_094sub_062m_092_060_094sub_062e_092_060_094sub_062n_092_060_094sub_062t) ).
thf(354,axiom,
! [H: heap_S1465075775_j_k_l] :
( ( type_w92696601_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_ShadowRootClass_Otype__wf_092_060_094sub_062E_092_060_094sub_062l_092_060_094sub_062e_092_060_094sub_062m_092_060_094sub_062e_092_060_094sub_062n_092_060_094sub_062t) ).
thf(356,axiom,
type_w92696601_j_k_l @ h,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_2) ).
thf(359,conjecture,
type_w697503069_j_k_l @ h,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_3) ).
thf(360,negated_conjecture,
( ( type_w697503069_j_k_l @ h )
= $false ),
inference(negate_conjecture,[status(cth)],[359]) ).
thf(361,plain,
( ( type_w697503069_j_k_l @ h )
= $false ),
inference(unfold_def,[status(thm)],[360]) ).
thf(362,plain,
( ( ! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: option147517124_ptr_d,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_682984464_j_k_l @ Element_ptr @ shadow1606659473tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[93]) ).
thf(363,plain,
( ( l_new_540233301_j_k_l @ type_w697503069_j_k_l )
= $true ),
inference(unfold_def,[status(thm)],[98]) ).
thf(364,plain,
( ( ! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: list_n282880152tr_b_c,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_1098917052_j_k_l @ Element_ptr @ child_1596411111tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[124]) ).
thf(365,plain,
( ( ! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: list_char,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_1720094109_j_k_l @ Element_ptr @ tag_na7058269tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[125]) ).
thf(366,plain,
( ( ! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: finite1621822014t_char,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_1724091798_j_k_l @ Element_ptr @ attrs_1280717024tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[126]) ).
thf(367,plain,
( ( ! [H: heap_S1465075775_j_k_l,H2: heap_S1465075775_j_k_l] :
( ( heap_E24690662_ptr_a @ H @ new_el717272935_j_k_l @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[128]) ).
thf(368,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w1771507213_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ) )
= $true ),
inference(unfold_def,[status(thm)],[215]) ).
thf(369,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w1479951274_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ) )
= $true ),
inference(unfold_def,[status(thm)],[307]) ).
thf(370,plain,
( ( l_get_2096691839_j_k_l @ type_w697503069_j_k_l )
= $true ),
inference(unfold_def,[status(thm)],[311]) ).
thf(371,plain,
( ( type_w697503069_j_k_l = l_type85280056_j_k_l )
= $true ),
inference(unfold_def,[status(thm)],[317]) ).
thf(372,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w697503069_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ) )
= $true ),
inference(unfold_def,[status(thm)],[349]) ).
thf(373,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w92696601_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ) )
= $true ),
inference(unfold_def,[status(thm)],[354]) ).
thf(374,plain,
( ( type_w92696601_j_k_l @ h )
= $true ),
inference(unfold_def,[status(thm)],[356]) ).
thf(375,plain,
( ( ~ ( type_w697503069_j_k_l @ h ) )
= $true ),
inference(polarity_switch,[status(thm)],[361]) ).
thf(376,plain,
( ( type_w92696601_j_k_l @ h )
= $true ),
inference(copy,[status(thm)],[374]) ).
thf(377,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w92696601_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ) )
= $true ),
inference(copy,[status(thm)],[373]) ).
thf(378,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w697503069_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ) )
= $true ),
inference(copy,[status(thm)],[372]) ).
thf(379,plain,
( ( type_w697503069_j_k_l = l_type85280056_j_k_l )
= $true ),
inference(copy,[status(thm)],[371]) ).
thf(380,plain,
( ( l_get_2096691839_j_k_l @ type_w697503069_j_k_l )
= $true ),
inference(copy,[status(thm)],[370]) ).
thf(381,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w1479951274_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ) )
= $true ),
inference(copy,[status(thm)],[369]) ).
thf(382,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w1771507213_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ) )
= $true ),
inference(copy,[status(thm)],[368]) ).
thf(383,plain,
( ( ! [H: heap_S1465075775_j_k_l,H2: heap_S1465075775_j_k_l] :
( ( heap_E24690662_ptr_a @ H @ new_el717272935_j_k_l @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[367]) ).
thf(384,plain,
( ( ! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: finite1621822014t_char,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_1724091798_j_k_l @ Element_ptr @ attrs_1280717024tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[366]) ).
thf(385,plain,
( ( ! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: list_char,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_1720094109_j_k_l @ Element_ptr @ tag_na7058269tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[365]) ).
thf(386,plain,
( ( ! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: list_n282880152tr_b_c,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_1098917052_j_k_l @ Element_ptr @ child_1596411111tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[364]) ).
thf(387,plain,
( ( l_new_540233301_j_k_l @ type_w697503069_j_k_l )
= $true ),
inference(copy,[status(thm)],[363]) ).
thf(388,plain,
( ( ! [H: heap_S1465075775_j_k_l,Element_ptr: element_ptr_a,V: option147517124_ptr_d,H2: heap_S1465075775_j_k_l] :
( ( heap_E494191872t_unit @ H @ ( put_M_682984464_j_k_l @ Element_ptr @ shadow1606659473tion_g @ V ) @ H2 )
=> ( ( type_w697503069_j_k_l @ H )
= ( type_w697503069_j_k_l @ H2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[362]) ).
thf(389,plain,
( ( ~ ( type_w697503069_j_k_l @ h ) )
= $true ),
inference(copy,[status(thm)],[375]) ).
thf(390,plain,
( ( ! [SX0: heap_S1465075775_j_k_l,SX1: heap_S1465075775_j_k_l] :
( ~ ( heap_E24690662_ptr_a @ SX0 @ new_el717272935_j_k_l @ SX1 )
| ( ( type_w697503069_j_k_l @ SX0 )
= ( type_w697503069_j_k_l @ SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[383]) ).
thf(391,plain,
( ( ! [SX0: heap_S1465075775_j_k_l] :
( ~ ( type_w1771507213_j_k_l @ SX0 )
| ( type_w697503069_j_k_l @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[382]) ).
thf(392,plain,
( ( ! [SX0: heap_S1465075775_j_k_l] :
( ~ ( type_w697503069_j_k_l @ SX0 )
| ( type_w697503069_j_k_l @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[378]) ).
thf(393,plain,
( ( ! [SX0: heap_S1465075775_j_k_l,SX1: element_ptr_a,SX2: finite1621822014t_char,SX3: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SX0 @ ( put_M_1724091798_j_k_l @ SX1 @ attrs_1280717024tion_g @ SX2 ) @ SX3 )
| ( ( type_w697503069_j_k_l @ SX0 )
= ( type_w697503069_j_k_l @ SX3 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[384]) ).
thf(394,plain,
( ( ! [SX0: heap_S1465075775_j_k_l,SX1: element_ptr_a,SX2: option147517124_ptr_d,SX3: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SX0 @ ( put_M_682984464_j_k_l @ SX1 @ shadow1606659473tion_g @ SX2 ) @ SX3 )
| ( ( type_w697503069_j_k_l @ SX0 )
= ( type_w697503069_j_k_l @ SX3 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[388]) ).
thf(395,plain,
( ( ! [SX0: heap_S1465075775_j_k_l] :
( ~ ( type_w1479951274_j_k_l @ SX0 )
| ( type_w697503069_j_k_l @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[381]) ).
thf(396,plain,
( ( ! [SX0: heap_S1465075775_j_k_l] :
( ~ ( type_w92696601_j_k_l @ SX0 )
| ( type_w697503069_j_k_l @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[377]) ).
thf(397,plain,
( ( ! [SX0: heap_S1465075775_j_k_l,SX1: element_ptr_a,SX2: list_char,SX3: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SX0 @ ( put_M_1720094109_j_k_l @ SX1 @ tag_na7058269tion_g @ SX2 ) @ SX3 )
| ( ( type_w697503069_j_k_l @ SX0 )
= ( type_w697503069_j_k_l @ SX3 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[385]) ).
thf(398,plain,
( ( ! [SX0: heap_S1465075775_j_k_l,SX1: element_ptr_a,SX2: list_n282880152tr_b_c,SX3: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SX0 @ ( put_M_1098917052_j_k_l @ SX1 @ child_1596411111tion_g @ SX2 ) @ SX3 )
| ( ( type_w697503069_j_k_l @ SX0 )
= ( type_w697503069_j_k_l @ SX3 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[386]) ).
thf(399,plain,
( ( ! [SV1: heap_S1465075775_j_k_l] :
( ( type_w697503069_j_k_l @ SV1 )
= ( l_type85280056_j_k_l @ SV1 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[379]) ).
thf(400,plain,
( ( type_w697503069_j_k_l = l_type85280056_j_k_l )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[379]) ).
thf(401,plain,
( ( type_w697503069_j_k_l @ h )
= $false ),
inference(extcnf_not_pos,[status(thm)],[389]) ).
thf(402,plain,
! [SV2: heap_S1465075775_j_k_l] :
( ( ! [SY22: heap_S1465075775_j_k_l] :
( ~ ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SY22 )
| ( ( type_w697503069_j_k_l @ SV2 )
= ( type_w697503069_j_k_l @ SY22 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[390]) ).
thf(403,plain,
! [SV3: heap_S1465075775_j_k_l] :
( ( ~ ( type_w1771507213_j_k_l @ SV3 )
| ( type_w697503069_j_k_l @ SV3 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[391]) ).
thf(404,plain,
! [SV4: heap_S1465075775_j_k_l] :
( ( ~ ( type_w697503069_j_k_l @ SV4 )
| ( type_w697503069_j_k_l @ SV4 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[392]) ).
thf(405,plain,
! [SV5: heap_S1465075775_j_k_l] :
( ( ! [SY23: element_ptr_a,SY24: finite1621822014t_char,SY25: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SY23 @ attrs_1280717024tion_g @ SY24 ) @ SY25 )
| ( ( type_w697503069_j_k_l @ SV5 )
= ( type_w697503069_j_k_l @ SY25 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[393]) ).
thf(406,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ! [SY26: element_ptr_a,SY27: option147517124_ptr_d,SY28: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SY26 @ shadow1606659473tion_g @ SY27 ) @ SY28 )
| ( ( type_w697503069_j_k_l @ SV6 )
= ( type_w697503069_j_k_l @ SY28 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[394]) ).
thf(407,plain,
! [SV7: heap_S1465075775_j_k_l] :
( ( ~ ( type_w1479951274_j_k_l @ SV7 )
| ( type_w697503069_j_k_l @ SV7 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[395]) ).
thf(408,plain,
! [SV8: heap_S1465075775_j_k_l] :
( ( ~ ( type_w92696601_j_k_l @ SV8 )
| ( type_w697503069_j_k_l @ SV8 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[396]) ).
thf(409,plain,
! [SV9: heap_S1465075775_j_k_l] :
( ( ! [SY29: element_ptr_a,SY30: list_char,SY31: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SY29 @ tag_na7058269tion_g @ SY30 ) @ SY31 )
| ( ( type_w697503069_j_k_l @ SV9 )
= ( type_w697503069_j_k_l @ SY31 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[397]) ).
thf(410,plain,
! [SV10: heap_S1465075775_j_k_l] :
( ( ! [SY32: element_ptr_a,SY33: list_n282880152tr_b_c,SY34: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SY32 @ child_1596411111tion_g @ SY33 ) @ SY34 )
| ( ( type_w697503069_j_k_l @ SV10 )
= ( type_w697503069_j_k_l @ SY34 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[398]) ).
thf(411,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV11 )
= ( l_type85280056_j_k_l @ SV11 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[399]) ).
thf(412,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ~ ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
| ( ( type_w697503069_j_k_l @ SV2 )
= ( type_w697503069_j_k_l @ SV12 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[402]) ).
thf(413,plain,
! [SV3: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w1771507213_j_k_l @ SV3 ) )
= $true )
| ( ( type_w697503069_j_k_l @ SV3 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[403]) ).
thf(414,plain,
! [SV4: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV4 ) )
= $true )
| ( ( type_w697503069_j_k_l @ SV4 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[404]) ).
thf(415,plain,
! [SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l] :
( ( ! [SY35: finite1621822014t_char,SY36: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SY35 ) @ SY36 )
| ( ( type_w697503069_j_k_l @ SV5 )
= ( type_w697503069_j_k_l @ SY36 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[405]) ).
thf(416,plain,
! [SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l] :
( ( ! [SY37: option147517124_ptr_d,SY38: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SY37 ) @ SY38 )
| ( ( type_w697503069_j_k_l @ SV6 )
= ( type_w697503069_j_k_l @ SY38 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[406]) ).
thf(417,plain,
! [SV7: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w1479951274_j_k_l @ SV7 ) )
= $true )
| ( ( type_w697503069_j_k_l @ SV7 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[407]) ).
thf(418,plain,
! [SV8: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w92696601_j_k_l @ SV8 ) )
= $true )
| ( ( type_w697503069_j_k_l @ SV8 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[408]) ).
thf(419,plain,
! [SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l] :
( ( ! [SY39: list_char,SY40: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SY39 ) @ SY40 )
| ( ( type_w697503069_j_k_l @ SV9 )
= ( type_w697503069_j_k_l @ SY40 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[409]) ).
thf(420,plain,
! [SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l] :
( ( ! [SY41: list_n282880152tr_b_c,SY42: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SY41 ) @ SY42 )
| ( ( type_w697503069_j_k_l @ SV10 )
= ( type_w697503069_j_k_l @ SY42 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[410]) ).
thf(421,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ~ ( ( type_w697503069_j_k_l @ SV11 )
| ( l_type85280056_j_k_l @ SV11 ) )
| ~ ( ~ ( type_w697503069_j_k_l @ SV11 )
| ~ ( l_type85280056_j_k_l @ SV11 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[411]) ).
thf(422,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV11 )
= ( l_type85280056_j_k_l @ SV11 ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[411]) ).
thf(423,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( ~ ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 ) )
= $true )
| ( ( ( type_w697503069_j_k_l @ SV2 )
= ( type_w697503069_j_k_l @ SV12 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[412]) ).
thf(424,plain,
! [SV3: heap_S1465075775_j_k_l] :
( ( ( type_w1771507213_j_k_l @ SV3 )
= $false )
| ( ( type_w697503069_j_k_l @ SV3 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[413]) ).
thf(425,plain,
! [SV4: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV4 )
= $false )
| ( ( type_w697503069_j_k_l @ SV4 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[414]) ).
thf(426,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l] :
( ( ! [SY43: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SY43 )
| ( ( type_w697503069_j_k_l @ SV5 )
= ( type_w697503069_j_k_l @ SY43 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[415]) ).
thf(427,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l] :
( ( ! [SY44: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SY44 )
| ( ( type_w697503069_j_k_l @ SV6 )
= ( type_w697503069_j_k_l @ SY44 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[416]) ).
thf(428,plain,
! [SV7: heap_S1465075775_j_k_l] :
( ( ( type_w1479951274_j_k_l @ SV7 )
= $false )
| ( ( type_w697503069_j_k_l @ SV7 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[417]) ).
thf(429,plain,
! [SV8: heap_S1465075775_j_k_l] :
( ( ( type_w92696601_j_k_l @ SV8 )
= $false )
| ( ( type_w697503069_j_k_l @ SV8 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[418]) ).
thf(430,plain,
! [SV19: list_char,SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l] :
( ( ! [SY45: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SY45 )
| ( ( type_w697503069_j_k_l @ SV9 )
= ( type_w697503069_j_k_l @ SY45 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[419]) ).
thf(431,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l] :
( ( ! [SY46: heap_S1465075775_j_k_l] :
( ~ ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SY46 )
| ( ( type_w697503069_j_k_l @ SV10 )
= ( type_w697503069_j_k_l @ SY46 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[420]) ).
thf(432,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w697503069_j_k_l @ SV11 )
| ( l_type85280056_j_k_l @ SV11 ) ) )
= $true )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV11 )
| ~ ( l_type85280056_j_k_l @ SV11 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[421]) ).
thf(433,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false )
| ( ( ( type_w697503069_j_k_l @ SV2 )
= ( type_w697503069_j_k_l @ SV12 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[423]) ).
thf(434,plain,
! [SV21: heap_S1465075775_j_k_l,SV17: finite1621822014t_char,SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l] :
( ( ~ ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
| ( ( type_w697503069_j_k_l @ SV5 )
= ( type_w697503069_j_k_l @ SV21 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[426]) ).
thf(435,plain,
! [SV22: heap_S1465075775_j_k_l,SV18: option147517124_ptr_d,SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l] :
( ( ~ ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
| ( ( type_w697503069_j_k_l @ SV6 )
= ( type_w697503069_j_k_l @ SV22 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[427]) ).
thf(436,plain,
! [SV23: heap_S1465075775_j_k_l,SV19: list_char,SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l] :
( ( ~ ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
| ( ( type_w697503069_j_k_l @ SV9 )
= ( type_w697503069_j_k_l @ SV23 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[430]) ).
thf(437,plain,
! [SV24: heap_S1465075775_j_k_l,SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l] :
( ( ~ ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
| ( ( type_w697503069_j_k_l @ SV10 )
= ( type_w697503069_j_k_l @ SV24 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[431]) ).
thf(438,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( ( type_w697503069_j_k_l @ SV11 )
| ( l_type85280056_j_k_l @ SV11 ) )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV11 )
| ~ ( l_type85280056_j_k_l @ SV11 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[432]) ).
thf(439,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w697503069_j_k_l @ SV2 )
| ( type_w697503069_j_k_l @ SV12 ) )
| ~ ( ~ ( type_w697503069_j_k_l @ SV2 )
| ~ ( type_w697503069_j_k_l @ SV12 ) ) )
= $true )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[433]) ).
thf(440,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( ( type_w697503069_j_k_l @ SV2 )
= ( type_w697503069_j_k_l @ SV12 ) )
= $true )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[433]) ).
thf(441,plain,
! [SV21: heap_S1465075775_j_k_l,SV17: finite1621822014t_char,SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l] :
( ( ( ~ ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 ) )
= $true )
| ( ( ( type_w697503069_j_k_l @ SV5 )
= ( type_w697503069_j_k_l @ SV21 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[434]) ).
thf(442,plain,
! [SV22: heap_S1465075775_j_k_l,SV18: option147517124_ptr_d,SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 ) )
= $true )
| ( ( ( type_w697503069_j_k_l @ SV6 )
= ( type_w697503069_j_k_l @ SV22 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[435]) ).
thf(443,plain,
! [SV23: heap_S1465075775_j_k_l,SV19: list_char,SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l] :
( ( ( ~ ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 ) )
= $true )
| ( ( ( type_w697503069_j_k_l @ SV9 )
= ( type_w697503069_j_k_l @ SV23 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[436]) ).
thf(444,plain,
! [SV24: heap_S1465075775_j_k_l,SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l] :
( ( ( ~ ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 ) )
= $true )
| ( ( ( type_w697503069_j_k_l @ SV10 )
= ( type_w697503069_j_k_l @ SV24 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[437]) ).
thf(445,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV11 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV11 )
| ~ ( l_type85280056_j_k_l @ SV11 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[438]) ).
thf(446,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( l_type85280056_j_k_l @ SV11 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV11 )
| ~ ( l_type85280056_j_k_l @ SV11 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[438]) ).
thf(447,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w697503069_j_k_l @ SV2 )
| ( type_w697503069_j_k_l @ SV12 ) ) )
= $true )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV2 )
| ~ ( type_w697503069_j_k_l @ SV12 ) ) )
= $true )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[439]) ).
thf(448,plain,
! [SV21: heap_S1465075775_j_k_l,SV17: finite1621822014t_char,SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l] :
( ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false )
| ( ( ( type_w697503069_j_k_l @ SV5 )
= ( type_w697503069_j_k_l @ SV21 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[441]) ).
thf(449,plain,
! [SV22: heap_S1465075775_j_k_l,SV18: option147517124_ptr_d,SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l] :
( ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false )
| ( ( ( type_w697503069_j_k_l @ SV6 )
= ( type_w697503069_j_k_l @ SV22 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[442]) ).
thf(450,plain,
! [SV23: heap_S1465075775_j_k_l,SV19: list_char,SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l] :
( ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false )
| ( ( ( type_w697503069_j_k_l @ SV9 )
= ( type_w697503069_j_k_l @ SV23 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[443]) ).
thf(451,plain,
! [SV24: heap_S1465075775_j_k_l,SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l] :
( ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false )
| ( ( ( type_w697503069_j_k_l @ SV10 )
= ( type_w697503069_j_k_l @ SV24 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[444]) ).
thf(452,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV11 )
| ~ ( l_type85280056_j_k_l @ SV11 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV11 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[445]) ).
thf(453,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV11 )
| ~ ( l_type85280056_j_k_l @ SV11 ) )
= $false )
| ( ( l_type85280056_j_k_l @ SV11 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[446]) ).
thf(454,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( ( type_w697503069_j_k_l @ SV2 )
| ( type_w697503069_j_k_l @ SV12 ) )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV2 )
| ~ ( type_w697503069_j_k_l @ SV12 ) ) )
= $true )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[447]) ).
thf(455,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV21: heap_S1465075775_j_k_l,SV5: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w697503069_j_k_l @ SV5 )
| ( type_w697503069_j_k_l @ SV21 ) )
| ~ ( ~ ( type_w697503069_j_k_l @ SV5 )
| ~ ( type_w697503069_j_k_l @ SV21 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[448]) ).
thf(456,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV21: heap_S1465075775_j_k_l,SV5: heap_S1465075775_j_k_l] :
( ( ( ( type_w697503069_j_k_l @ SV5 )
= ( type_w697503069_j_k_l @ SV21 ) )
= $true )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[448]) ).
thf(457,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV22: heap_S1465075775_j_k_l,SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w697503069_j_k_l @ SV6 )
| ( type_w697503069_j_k_l @ SV22 ) )
| ~ ( ~ ( type_w697503069_j_k_l @ SV6 )
| ~ ( type_w697503069_j_k_l @ SV22 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[449]) ).
thf(458,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV22: heap_S1465075775_j_k_l,SV6: heap_S1465075775_j_k_l] :
( ( ( ( type_w697503069_j_k_l @ SV6 )
= ( type_w697503069_j_k_l @ SV22 ) )
= $true )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[449]) ).
thf(459,plain,
! [SV19: list_char,SV15: element_ptr_a,SV23: heap_S1465075775_j_k_l,SV9: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w697503069_j_k_l @ SV9 )
| ( type_w697503069_j_k_l @ SV23 ) )
| ~ ( ~ ( type_w697503069_j_k_l @ SV9 )
| ~ ( type_w697503069_j_k_l @ SV23 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[450]) ).
thf(460,plain,
! [SV19: list_char,SV15: element_ptr_a,SV23: heap_S1465075775_j_k_l,SV9: heap_S1465075775_j_k_l] :
( ( ( ( type_w697503069_j_k_l @ SV9 )
= ( type_w697503069_j_k_l @ SV23 ) )
= $true )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[450]) ).
thf(461,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV24: heap_S1465075775_j_k_l,SV10: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w697503069_j_k_l @ SV10 )
| ( type_w697503069_j_k_l @ SV24 ) )
| ~ ( ~ ( type_w697503069_j_k_l @ SV10 )
| ~ ( type_w697503069_j_k_l @ SV24 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[451]) ).
thf(462,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV24: heap_S1465075775_j_k_l,SV10: heap_S1465075775_j_k_l] :
( ( ( ( type_w697503069_j_k_l @ SV10 )
= ( type_w697503069_j_k_l @ SV24 ) )
= $true )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[451]) ).
thf(463,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV11 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV11 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[452]) ).
thf(464,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( ~ ( l_type85280056_j_k_l @ SV11 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV11 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[452]) ).
thf(465,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV11 ) )
= $false )
| ( ( l_type85280056_j_k_l @ SV11 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[453]) ).
thf(466,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( ~ ( l_type85280056_j_k_l @ SV11 ) )
= $false )
| ( ( l_type85280056_j_k_l @ SV11 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[453]) ).
thf(467,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV2 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV2 )
| ~ ( type_w697503069_j_k_l @ SV12 ) ) )
= $true )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[454]) ).
thf(468,plain,
! [SV2: heap_S1465075775_j_k_l,SV12: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV12 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV2 )
| ~ ( type_w697503069_j_k_l @ SV12 ) ) )
= $true )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[454]) ).
thf(469,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV21: heap_S1465075775_j_k_l,SV5: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w697503069_j_k_l @ SV5 )
| ( type_w697503069_j_k_l @ SV21 ) ) )
= $true )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV5 )
| ~ ( type_w697503069_j_k_l @ SV21 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[455]) ).
thf(470,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV22: heap_S1465075775_j_k_l,SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w697503069_j_k_l @ SV6 )
| ( type_w697503069_j_k_l @ SV22 ) ) )
= $true )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV6 )
| ~ ( type_w697503069_j_k_l @ SV22 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[457]) ).
thf(471,plain,
! [SV19: list_char,SV15: element_ptr_a,SV23: heap_S1465075775_j_k_l,SV9: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w697503069_j_k_l @ SV9 )
| ( type_w697503069_j_k_l @ SV23 ) ) )
= $true )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV9 )
| ~ ( type_w697503069_j_k_l @ SV23 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[459]) ).
thf(472,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV24: heap_S1465075775_j_k_l,SV10: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w697503069_j_k_l @ SV10 )
| ( type_w697503069_j_k_l @ SV24 ) ) )
= $true )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV10 )
| ~ ( type_w697503069_j_k_l @ SV24 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[461]) ).
thf(473,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV11 )
= $true )
| ( ( type_w697503069_j_k_l @ SV11 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[463]) ).
thf(474,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( l_type85280056_j_k_l @ SV11 )
= $true )
| ( ( type_w697503069_j_k_l @ SV11 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[464]) ).
thf(475,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV11 )
= $true )
| ( ( l_type85280056_j_k_l @ SV11 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[465]) ).
thf(476,plain,
! [SV11: heap_S1465075775_j_k_l] :
( ( ( l_type85280056_j_k_l @ SV11 )
= $true )
| ( ( l_type85280056_j_k_l @ SV11 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[466]) ).
thf(477,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV2 )
| ~ ( type_w697503069_j_k_l @ SV12 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV2 )
= $false )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[467]) ).
thf(478,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV2 )
| ~ ( type_w697503069_j_k_l @ SV12 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV12 )
= $false )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[468]) ).
thf(479,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV21: heap_S1465075775_j_k_l,SV5: heap_S1465075775_j_k_l] :
( ( ( ( type_w697503069_j_k_l @ SV5 )
| ( type_w697503069_j_k_l @ SV21 ) )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV5 )
| ~ ( type_w697503069_j_k_l @ SV21 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[469]) ).
thf(480,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV22: heap_S1465075775_j_k_l,SV6: heap_S1465075775_j_k_l] :
( ( ( ( type_w697503069_j_k_l @ SV6 )
| ( type_w697503069_j_k_l @ SV22 ) )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV6 )
| ~ ( type_w697503069_j_k_l @ SV22 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[470]) ).
thf(481,plain,
! [SV19: list_char,SV15: element_ptr_a,SV23: heap_S1465075775_j_k_l,SV9: heap_S1465075775_j_k_l] :
( ( ( ( type_w697503069_j_k_l @ SV9 )
| ( type_w697503069_j_k_l @ SV23 ) )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV9 )
| ~ ( type_w697503069_j_k_l @ SV23 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[471]) ).
thf(482,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV24: heap_S1465075775_j_k_l,SV10: heap_S1465075775_j_k_l] :
( ( ( ( type_w697503069_j_k_l @ SV10 )
| ( type_w697503069_j_k_l @ SV24 ) )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV10 )
| ~ ( type_w697503069_j_k_l @ SV24 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[472]) ).
thf(483,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV2 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV2 )
= $false )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[477]) ).
thf(484,plain,
! [SV2: heap_S1465075775_j_k_l,SV12: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV12 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV2 )
= $false )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[477]) ).
thf(485,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV2 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV12 )
= $false )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[478]) ).
thf(486,plain,
! [SV2: heap_S1465075775_j_k_l,SV12: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV12 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV12 )
= $false )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[478]) ).
thf(487,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV21: heap_S1465075775_j_k_l,SV5: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV5 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV5 )
| ~ ( type_w697503069_j_k_l @ SV21 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[479]) ).
thf(488,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l,SV21: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV21 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV5 )
| ~ ( type_w697503069_j_k_l @ SV21 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[479]) ).
thf(489,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV22: heap_S1465075775_j_k_l,SV6: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV6 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV6 )
| ~ ( type_w697503069_j_k_l @ SV22 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[480]) ).
thf(490,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l,SV22: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV22 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV6 )
| ~ ( type_w697503069_j_k_l @ SV22 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[480]) ).
thf(491,plain,
! [SV19: list_char,SV15: element_ptr_a,SV23: heap_S1465075775_j_k_l,SV9: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV9 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV9 )
| ~ ( type_w697503069_j_k_l @ SV23 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[481]) ).
thf(492,plain,
! [SV19: list_char,SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l,SV23: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV23 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV9 )
| ~ ( type_w697503069_j_k_l @ SV23 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[481]) ).
thf(493,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV24: heap_S1465075775_j_k_l,SV10: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV10 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV10 )
| ~ ( type_w697503069_j_k_l @ SV24 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[482]) ).
thf(494,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l,SV24: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV24 )
= $false )
| ( ( ~ ( ~ ( type_w697503069_j_k_l @ SV10 )
| ~ ( type_w697503069_j_k_l @ SV24 ) ) )
= $true )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[482]) ).
thf(495,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV2 )
= $true )
| ( ( type_w697503069_j_k_l @ SV2 )
= $false )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[483]) ).
thf(496,plain,
! [SV2: heap_S1465075775_j_k_l,SV12: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV12 )
= $true )
| ( ( type_w697503069_j_k_l @ SV2 )
= $false )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[484]) ).
thf(497,plain,
! [SV12: heap_S1465075775_j_k_l,SV2: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV2 )
= $true )
| ( ( type_w697503069_j_k_l @ SV12 )
= $false )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[485]) ).
thf(498,plain,
! [SV2: heap_S1465075775_j_k_l,SV12: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV12 )
= $true )
| ( ( type_w697503069_j_k_l @ SV12 )
= $false )
| ( ( heap_E24690662_ptr_a @ SV2 @ new_el717272935_j_k_l @ SV12 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[486]) ).
thf(499,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV21: heap_S1465075775_j_k_l,SV5: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV5 )
| ~ ( type_w697503069_j_k_l @ SV21 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV5 )
= $false )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[487]) ).
thf(500,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV21: heap_S1465075775_j_k_l,SV5: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV5 )
| ~ ( type_w697503069_j_k_l @ SV21 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV21 )
= $false )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[488]) ).
thf(501,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV22: heap_S1465075775_j_k_l,SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV6 )
| ~ ( type_w697503069_j_k_l @ SV22 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV6 )
= $false )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[489]) ).
thf(502,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV22: heap_S1465075775_j_k_l,SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV6 )
| ~ ( type_w697503069_j_k_l @ SV22 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV22 )
= $false )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[490]) ).
thf(503,plain,
! [SV19: list_char,SV15: element_ptr_a,SV23: heap_S1465075775_j_k_l,SV9: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV9 )
| ~ ( type_w697503069_j_k_l @ SV23 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV9 )
= $false )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[491]) ).
thf(504,plain,
! [SV19: list_char,SV15: element_ptr_a,SV23: heap_S1465075775_j_k_l,SV9: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV9 )
| ~ ( type_w697503069_j_k_l @ SV23 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV23 )
= $false )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[492]) ).
thf(505,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV24: heap_S1465075775_j_k_l,SV10: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV10 )
| ~ ( type_w697503069_j_k_l @ SV24 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV10 )
= $false )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[493]) ).
thf(506,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV24: heap_S1465075775_j_k_l,SV10: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV10 )
| ~ ( type_w697503069_j_k_l @ SV24 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV24 )
= $false )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[494]) ).
thf(507,plain,
! [SV21: heap_S1465075775_j_k_l,SV17: finite1621822014t_char,SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV5 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV5 )
= $false )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[499]) ).
thf(508,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l,SV21: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV21 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV5 )
= $false )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[499]) ).
thf(509,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV21: heap_S1465075775_j_k_l,SV5: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV5 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV21 )
= $false )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[500]) ).
thf(510,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l,SV21: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV21 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV21 )
= $false )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[500]) ).
thf(511,plain,
! [SV22: heap_S1465075775_j_k_l,SV18: option147517124_ptr_d,SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV6 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV6 )
= $false )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[501]) ).
thf(512,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l,SV22: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV22 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV6 )
= $false )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[501]) ).
thf(513,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV22: heap_S1465075775_j_k_l,SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV6 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV22 )
= $false )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[502]) ).
thf(514,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l,SV22: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV22 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV22 )
= $false )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[502]) ).
thf(515,plain,
! [SV23: heap_S1465075775_j_k_l,SV19: list_char,SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV9 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV9 )
= $false )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[503]) ).
thf(516,plain,
! [SV19: list_char,SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l,SV23: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV23 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV9 )
= $false )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[503]) ).
thf(517,plain,
! [SV19: list_char,SV15: element_ptr_a,SV23: heap_S1465075775_j_k_l,SV9: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV9 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV23 )
= $false )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[504]) ).
thf(518,plain,
! [SV19: list_char,SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l,SV23: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV23 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV23 )
= $false )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[504]) ).
thf(519,plain,
! [SV24: heap_S1465075775_j_k_l,SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV10 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV10 )
= $false )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[505]) ).
thf(520,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l,SV24: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV24 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV10 )
= $false )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[505]) ).
thf(521,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV24: heap_S1465075775_j_k_l,SV10: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV10 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV24 )
= $false )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[506]) ).
thf(522,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l,SV24: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w697503069_j_k_l @ SV24 ) )
= $false )
| ( ( type_w697503069_j_k_l @ SV24 )
= $false )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[506]) ).
thf(523,plain,
! [SV21: heap_S1465075775_j_k_l,SV17: finite1621822014t_char,SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV5 )
= $true )
| ( ( type_w697503069_j_k_l @ SV5 )
= $false )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[507]) ).
thf(524,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l,SV21: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV21 )
= $true )
| ( ( type_w697503069_j_k_l @ SV5 )
= $false )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[508]) ).
thf(525,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV21: heap_S1465075775_j_k_l,SV5: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV5 )
= $true )
| ( ( type_w697503069_j_k_l @ SV21 )
= $false )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[509]) ).
thf(526,plain,
! [SV17: finite1621822014t_char,SV13: element_ptr_a,SV5: heap_S1465075775_j_k_l,SV21: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV21 )
= $true )
| ( ( type_w697503069_j_k_l @ SV21 )
= $false )
| ( ( heap_E494191872t_unit @ SV5 @ ( put_M_1724091798_j_k_l @ SV13 @ attrs_1280717024tion_g @ SV17 ) @ SV21 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[510]) ).
thf(527,plain,
! [SV22: heap_S1465075775_j_k_l,SV18: option147517124_ptr_d,SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV6 )
= $true )
| ( ( type_w697503069_j_k_l @ SV6 )
= $false )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[511]) ).
thf(528,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l,SV22: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV22 )
= $true )
| ( ( type_w697503069_j_k_l @ SV6 )
= $false )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[512]) ).
thf(529,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV22: heap_S1465075775_j_k_l,SV6: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV6 )
= $true )
| ( ( type_w697503069_j_k_l @ SV22 )
= $false )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[513]) ).
thf(530,plain,
! [SV18: option147517124_ptr_d,SV14: element_ptr_a,SV6: heap_S1465075775_j_k_l,SV22: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV22 )
= $true )
| ( ( type_w697503069_j_k_l @ SV22 )
= $false )
| ( ( heap_E494191872t_unit @ SV6 @ ( put_M_682984464_j_k_l @ SV14 @ shadow1606659473tion_g @ SV18 ) @ SV22 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[514]) ).
thf(531,plain,
! [SV23: heap_S1465075775_j_k_l,SV19: list_char,SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV9 )
= $true )
| ( ( type_w697503069_j_k_l @ SV9 )
= $false )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[515]) ).
thf(532,plain,
! [SV19: list_char,SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l,SV23: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV23 )
= $true )
| ( ( type_w697503069_j_k_l @ SV9 )
= $false )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[516]) ).
thf(533,plain,
! [SV19: list_char,SV15: element_ptr_a,SV23: heap_S1465075775_j_k_l,SV9: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV9 )
= $true )
| ( ( type_w697503069_j_k_l @ SV23 )
= $false )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[517]) ).
thf(534,plain,
! [SV19: list_char,SV15: element_ptr_a,SV9: heap_S1465075775_j_k_l,SV23: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV23 )
= $true )
| ( ( type_w697503069_j_k_l @ SV23 )
= $false )
| ( ( heap_E494191872t_unit @ SV9 @ ( put_M_1720094109_j_k_l @ SV15 @ tag_na7058269tion_g @ SV19 ) @ SV23 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[518]) ).
thf(535,plain,
! [SV24: heap_S1465075775_j_k_l,SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV10 )
= $true )
| ( ( type_w697503069_j_k_l @ SV10 )
= $false )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[519]) ).
thf(536,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l,SV24: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV24 )
= $true )
| ( ( type_w697503069_j_k_l @ SV10 )
= $false )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[520]) ).
thf(537,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV24: heap_S1465075775_j_k_l,SV10: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV10 )
= $true )
| ( ( type_w697503069_j_k_l @ SV24 )
= $false )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[521]) ).
thf(538,plain,
! [SV20: list_n282880152tr_b_c,SV16: element_ptr_a,SV10: heap_S1465075775_j_k_l,SV24: heap_S1465075775_j_k_l] :
( ( ( type_w697503069_j_k_l @ SV24 )
= $true )
| ( ( type_w697503069_j_k_l @ SV24 )
= $false )
| ( ( heap_E494191872t_unit @ SV10 @ ( put_M_1098917052_j_k_l @ SV16 @ child_1596411111tion_g @ SV20 ) @ SV24 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[522]) ).
thf(539,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[376,538,537,536,535,534,533,532,531,530,529,528,527,526,525,524,523,498,497,496,495,476,475,474,473,462,460,458,456,440,429,428,425,424,422,401,400,387,380]) ).
thf(540,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[539]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP173^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.20 % Computer : n014.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Oct 6 11:18:56 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.98/1.09 ..
% 4.98/1.09
% 4.98/1.09 No.of.Axioms: 13
% 4.98/1.09
% 4.98/1.09 Length.of.Defs: 0
% 4.98/1.09
% 4.98/1.09 Contains.Choice.Funs: false
% 4.98/1.09 ......
% 4.98/1.09
% 4.98/1.09 ********************************
% 4.98/1.09 * All subproblems solved! *
% 4.98/1.09 ********************************
% 4.98/1.09 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:13,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:539,loop_count:0,foatp_calls:1,translation:fof_full)
% 4.98/1.09
% 4.98/1.09 %**** Beginning of derivation protocol ****
% 4.98/1.09 % SZS output start CNFRefutation
% See solution above
% 4.98/1.09
% 4.98/1.09 %**** End of derivation protocol ****
% 4.98/1.09 %**** no. of clauses in derivation: 195 ****
% 4.98/1.09 %**** clause counter: 539 ****
% 4.98/1.09
% 4.98/1.09 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:13,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:539,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------