%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : ITP174^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/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 7 10:24:35 AM UTC 2026
% Result : Theorem 7.20s 1.44s
% Output : CNFRefutation 7.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 10
% Syntax : Number of formulae : 70 ( 41 unt; 0 typ; 0 def)
% Number of atoms : 308 ( 88 equ; 0 cnn)
% Maximal formula atoms : 2 ( 4 avg)
% Number of connectives : 212 ( 39 ~; 41 |; 0 &; 120 @)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Number of types : 36 ( 35 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 164 ( 161 usr; 15 con; 0-5 aty)
% Number of variables : 46 ( 0 ^; 46 !; 0 ?; 46 :)
% 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_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_option1330818496tr_d_e,type,
option1330818496tr_d_e: $tType ).
thf(tp_option147517124_ptr_d,type,
option147517124_ptr_d: $tType ).
thf(tp_option1749760295_j_k_l,type,
option1749760295_j_k_l: $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_o516720829tr_d_e,type,
case_o516720829tr_d_e: $o > ( docume1935157360tr_d_e > $o ) > option1330818496tr_d_e > $o ).
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_o761049241_d_e_f,type,
cast_o761049241_d_e_f: object945351580_d_e_f > option1330818496tr_d_e ).
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_768225874tion_g,type,
child_768225874tion_g: rObjec1875798643tion_g > list_n282880152tr_b_c ).
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_1125451418_j_k_l,type,
get_M_1125451418_j_k_l: character_data_ptr_b > ( rObjec1148923485tion_h > list_n282880152tr_b_c ) > heap_E1735400259tr_b_c ).
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_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_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_O_623850005_j_k_l,type,
get_O_623850005_j_k_l: object945351580_d_e_f > heap_S1465075775_j_k_l > option1749760295_j_k_l ).
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_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_E1361235918tr_b_c,type,
heap_E1361235918tr_b_c: heap_S1465075775_j_k_l > heap_E1735400259tr_b_c > list_n282880152tr_b_c > 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_E1516284546tr_b_c,type,
heap_E1516284546tr_b_c: heap_E1735400259tr_b_c > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l > $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_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_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_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_heap_E959625611tr_b_c,type,
heap_E959625611tr_b_c: heap_S1465075775_j_k_l > heap_E1735400259tr_b_c > heap_S1465075775_j_k_l > $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_sha1302775417_r_d_e,type,
is_sha1302775417_r_d_e: docume1935157360tr_d_e > $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_2113179812_j_k_l,type,
l_get_2113179812_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_893346794tr_b_c,type,
l_put_893346794tr_b_c: ( docume1935157360tr_d_e > heap_S1465075775_j_k_l > option841825948on_j_k ) > ( docume1935157360tr_d_e > rObjec1617416918on_j_k > heap_S1465075775_j_k_l > heap_S1465075775_j_k_l ) > docume1935157360tr_d_e > ( ( list_n282880152tr_b_c > list_n282880152tr_b_c ) > rObjec1617416918on_j_k > rObjec1617416918on_j_k ) > list_n282880152tr_b_c > heap_E625070648t_unit ).
thf(tp_l_type1003141153_j_k_l,type,
l_type1003141153_j_k_l: heap_S1465075775_j_k_l > $o ).
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_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_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_318275117_j_k_l,type,
put_M_318275117_j_k_l: character_data_ptr_b > ( ( list_n282880152tr_b_c > list_n282880152tr_b_c ) > rObjec1148923485tion_h > rObjec1148923485tion_h ) > list_n282880152tr_b_c > 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_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_shadow505265920_i_k_l,type,
shadow505265920_i_k_l: shadow_root_ptr_d > ( ( list_n282880152tr_b_c > list_n282880152tr_b_c ) > rObjec2068690451tion_j > rObjec2068690451tion_j ) > list_n282880152tr_b_c > heap_E625070648t_unit ).
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_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_the_do1700004572tr_d_e,type,
the_do1700004572tr_d_e: option1330818496tr_d_e > docume1935157360tr_d_e ).
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: list_n282880152tr_b_c ).
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(92,axiom,
! [H: heap_S1465075775_j_k_l] :
( ( type_w1771507213_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_263_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(104,axiom,
l_new_410495338_j_k_l @ type_w1771507213_j_k_l,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_251_CharacterDataMonad_Onew__character__data__is__l__new__character__data) ).
thf(105,axiom,
l_new_540233301_j_k_l @ type_w1771507213_j_k_l,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_250_CharacterDataMonad_Onew__element__is__l__new__element) ).
thf(307,axiom,
! [H: heap_S1465075775_j_k_l] :
( ( type_w1479951274_j_k_l @ H )
=> ( type_w1771507213_j_k_l @ H ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_48_DocumentClass_Otype__wf_092_060_094sub_062C_092_060_094sub_062h_092_060_094sub_062a_092_060_094sub_062r_092_060_094sub_062a_092_060_094sub_062c_092_060_094sub_062t_092_060_094sub_062e_092_060_094sub_062r_092_060_094sub_062D_092_060_094sub_062a_092_060_094sub_062t_092_060_094sub_062a) ).
thf(311,axiom,
l_get_2113179812_j_k_l @ type_w1771507213_j_k_l,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_44_CharacterDataClass_Ol__get_092_060_094sub_062C_092_060_094sub_062h_092_060_094sub_062a_092_060_094sub_062r_092_060_094sub_062a_092_060_094sub_062c_092_060_094sub_062t_092_060_094sub_062e_092_060_094sub_062r_092_060_094sub_062D_092_060_094sub_062a_092_060_094sub_062t_092_060_094sub_062a__lemmas__axioms) ).
thf(317,axiom,
type_w1771507213_j_k_l = l_type1003141153_j_k_l,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_38_CharacterDataClass_Otype__wf__def) ).
thf(349,axiom,
! [H: heap_S1465075775_j_k_l] :
( ( type_w1771507213_j_k_l @ H )
=> ( type_w1771507213_j_k_l @ H ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_CharacterDataClass_Otype__wf_092_060_094sub_062C_092_060_094sub_062h_092_060_094sub_062a_092_060_094sub_062r_092_060_094sub_062a_092_060_094sub_062c_092_060_094sub_062t_092_060_094sub_062e_092_060_094sub_062r_092_060_094sub_062D_092_060_094sub_062a_092_060_094sub_062t_092_060_094sub_062a) ).
thf(354,axiom,
! [H: heap_S1465075775_j_k_l] :
( ( type_w92696601_j_k_l @ H )
=> ( type_w1771507213_j_k_l @ H ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_ShadowRootClass_Otype__wf_092_060_094sub_062C_092_060_094sub_062h_092_060_094sub_062a_092_060_094sub_062r_092_060_094sub_062a_092_060_094sub_062c_092_060_094sub_062t_092_060_094sub_062e_092_060_094sub_062r_092_060_094sub_062D_092_060_094sub_062a_092_060_094sub_062t_092_060_094sub_062a) ).
thf(356,axiom,
type_w92696601_j_k_l @ h,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_2) ).
thf(359,conjecture,
type_w1771507213_j_k_l @ h,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_3) ).
thf(360,negated_conjecture,
( ( type_w1771507213_j_k_l @ h )
= $false ),
inference(negate_conjecture,[status(cth)],[359]) ).
thf(361,plain,
( ( type_w1771507213_j_k_l @ h )
= $false ),
inference(unfold_def,[status(thm)],[360]) ).
thf(362,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)],[92]) ).
thf(363,plain,
( ( l_new_410495338_j_k_l @ type_w1771507213_j_k_l )
= $true ),
inference(unfold_def,[status(thm)],[104]) ).
thf(364,plain,
( ( l_new_540233301_j_k_l @ type_w1771507213_j_k_l )
= $true ),
inference(unfold_def,[status(thm)],[105]) ).
thf(365,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w1479951274_j_k_l @ H )
=> ( type_w1771507213_j_k_l @ H ) ) )
= $true ),
inference(unfold_def,[status(thm)],[307]) ).
thf(366,plain,
( ( l_get_2113179812_j_k_l @ type_w1771507213_j_k_l )
= $true ),
inference(unfold_def,[status(thm)],[311]) ).
thf(367,plain,
( ( type_w1771507213_j_k_l = l_type1003141153_j_k_l )
= $true ),
inference(unfold_def,[status(thm)],[317]) ).
thf(368,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w1771507213_j_k_l @ H )
=> ( type_w1771507213_j_k_l @ H ) ) )
= $true ),
inference(unfold_def,[status(thm)],[349]) ).
thf(369,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w92696601_j_k_l @ H )
=> ( type_w1771507213_j_k_l @ H ) ) )
= $true ),
inference(unfold_def,[status(thm)],[354]) ).
thf(370,plain,
( ( type_w92696601_j_k_l @ h )
= $true ),
inference(unfold_def,[status(thm)],[356]) ).
thf(371,plain,
( ( ~ ( type_w1771507213_j_k_l @ h ) )
= $true ),
inference(polarity_switch,[status(thm)],[361]) ).
thf(372,plain,
( ( type_w92696601_j_k_l @ h )
= $true ),
inference(copy,[status(thm)],[370]) ).
thf(373,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w92696601_j_k_l @ H )
=> ( type_w1771507213_j_k_l @ H ) ) )
= $true ),
inference(copy,[status(thm)],[369]) ).
thf(374,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w1771507213_j_k_l @ H )
=> ( type_w1771507213_j_k_l @ H ) ) )
= $true ),
inference(copy,[status(thm)],[368]) ).
thf(375,plain,
( ( type_w1771507213_j_k_l = l_type1003141153_j_k_l )
= $true ),
inference(copy,[status(thm)],[367]) ).
thf(376,plain,
( ( l_get_2113179812_j_k_l @ type_w1771507213_j_k_l )
= $true ),
inference(copy,[status(thm)],[366]) ).
thf(377,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w1479951274_j_k_l @ H )
=> ( type_w1771507213_j_k_l @ H ) ) )
= $true ),
inference(copy,[status(thm)],[365]) ).
thf(378,plain,
( ( l_new_540233301_j_k_l @ type_w1771507213_j_k_l )
= $true ),
inference(copy,[status(thm)],[364]) ).
thf(379,plain,
( ( l_new_410495338_j_k_l @ type_w1771507213_j_k_l )
= $true ),
inference(copy,[status(thm)],[363]) ).
thf(380,plain,
( ( ! [H: heap_S1465075775_j_k_l] :
( ( type_w1771507213_j_k_l @ H )
=> ( type_w697503069_j_k_l @ H ) ) )
= $true ),
inference(copy,[status(thm)],[362]) ).
thf(381,plain,
( ( ~ ( type_w1771507213_j_k_l @ h ) )
= $true ),
inference(copy,[status(thm)],[371]) ).
thf(382,plain,
( ( ! [SX0: heap_S1465075775_j_k_l] :
( ~ ( type_w92696601_j_k_l @ SX0 )
| ( type_w1771507213_j_k_l @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[373]) ).
thf(383,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)],[380]) ).
thf(384,plain,
( ( ! [SX0: heap_S1465075775_j_k_l] :
( ~ ( type_w1771507213_j_k_l @ SX0 )
| ( type_w1771507213_j_k_l @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[374]) ).
thf(385,plain,
( ( ! [SX0: heap_S1465075775_j_k_l] :
( ~ ( type_w1479951274_j_k_l @ SX0 )
| ( type_w1771507213_j_k_l @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[377]) ).
thf(386,plain,
( ( ! [SV1: heap_S1465075775_j_k_l] :
( ( type_w1771507213_j_k_l @ SV1 )
= ( l_type1003141153_j_k_l @ SV1 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[375]) ).
thf(387,plain,
( ( type_w1771507213_j_k_l = l_type1003141153_j_k_l )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[375]) ).
thf(388,plain,
( ( type_w1771507213_j_k_l @ h )
= $false ),
inference(extcnf_not_pos,[status(thm)],[381]) ).
thf(389,plain,
! [SV2: heap_S1465075775_j_k_l] :
( ( ~ ( type_w92696601_j_k_l @ SV2 )
| ( type_w1771507213_j_k_l @ SV2 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[382]) ).
thf(390,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)],[383]) ).
thf(391,plain,
! [SV4: heap_S1465075775_j_k_l] :
( ( ~ ( type_w1771507213_j_k_l @ SV4 )
| ( type_w1771507213_j_k_l @ SV4 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[384]) ).
thf(392,plain,
! [SV5: heap_S1465075775_j_k_l] :
( ( ~ ( type_w1479951274_j_k_l @ SV5 )
| ( type_w1771507213_j_k_l @ SV5 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[385]) ).
thf(393,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( type_w1771507213_j_k_l @ SV6 )
= ( l_type1003141153_j_k_l @ SV6 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[386]) ).
thf(394,plain,
! [SV2: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w92696601_j_k_l @ SV2 ) )
= $true )
| ( ( type_w1771507213_j_k_l @ SV2 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[389]) ).
thf(395,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)],[390]) ).
thf(396,plain,
! [SV4: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w1771507213_j_k_l @ SV4 ) )
= $true )
| ( ( type_w1771507213_j_k_l @ SV4 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[391]) ).
thf(397,plain,
! [SV5: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w1479951274_j_k_l @ SV5 ) )
= $true )
| ( ( type_w1771507213_j_k_l @ SV5 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[392]) ).
thf(398,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ~ ( ( type_w1771507213_j_k_l @ SV6 )
| ( l_type1003141153_j_k_l @ SV6 ) )
| ~ ( ~ ( type_w1771507213_j_k_l @ SV6 )
| ~ ( l_type1003141153_j_k_l @ SV6 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[393]) ).
thf(399,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( type_w1771507213_j_k_l @ SV6 )
= ( l_type1003141153_j_k_l @ SV6 ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[393]) ).
thf(400,plain,
! [SV2: heap_S1465075775_j_k_l] :
( ( ( type_w92696601_j_k_l @ SV2 )
= $false )
| ( ( type_w1771507213_j_k_l @ SV2 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[394]) ).
thf(401,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)],[395]) ).
thf(402,plain,
! [SV4: heap_S1465075775_j_k_l] :
( ( ( type_w1771507213_j_k_l @ SV4 )
= $false )
| ( ( type_w1771507213_j_k_l @ SV4 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[396]) ).
thf(403,plain,
! [SV5: heap_S1465075775_j_k_l] :
( ( ( type_w1479951274_j_k_l @ SV5 )
= $false )
| ( ( type_w1771507213_j_k_l @ SV5 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[397]) ).
thf(404,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( ( type_w1771507213_j_k_l @ SV6 )
| ( l_type1003141153_j_k_l @ SV6 ) ) )
= $true )
| ( ( ~ ( ~ ( type_w1771507213_j_k_l @ SV6 )
| ~ ( l_type1003141153_j_k_l @ SV6 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[398]) ).
thf(405,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( ( type_w1771507213_j_k_l @ SV6 )
| ( l_type1003141153_j_k_l @ SV6 ) )
= $false )
| ( ( ~ ( ~ ( type_w1771507213_j_k_l @ SV6 )
| ~ ( l_type1003141153_j_k_l @ SV6 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[404]) ).
thf(406,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( type_w1771507213_j_k_l @ SV6 )
= $false )
| ( ( ~ ( ~ ( type_w1771507213_j_k_l @ SV6 )
| ~ ( l_type1003141153_j_k_l @ SV6 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[405]) ).
thf(407,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( l_type1003141153_j_k_l @ SV6 )
= $false )
| ( ( ~ ( ~ ( type_w1771507213_j_k_l @ SV6 )
| ~ ( l_type1003141153_j_k_l @ SV6 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[405]) ).
thf(408,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w1771507213_j_k_l @ SV6 )
| ~ ( l_type1003141153_j_k_l @ SV6 ) )
= $false )
| ( ( type_w1771507213_j_k_l @ SV6 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[406]) ).
thf(409,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w1771507213_j_k_l @ SV6 )
| ~ ( l_type1003141153_j_k_l @ SV6 ) )
= $false )
| ( ( l_type1003141153_j_k_l @ SV6 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[407]) ).
thf(410,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w1771507213_j_k_l @ SV6 ) )
= $false )
| ( ( type_w1771507213_j_k_l @ SV6 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[408]) ).
thf(411,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( l_type1003141153_j_k_l @ SV6 ) )
= $false )
| ( ( type_w1771507213_j_k_l @ SV6 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[408]) ).
thf(412,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( type_w1771507213_j_k_l @ SV6 ) )
= $false )
| ( ( l_type1003141153_j_k_l @ SV6 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[409]) ).
thf(413,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( ~ ( l_type1003141153_j_k_l @ SV6 ) )
= $false )
| ( ( l_type1003141153_j_k_l @ SV6 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[409]) ).
thf(414,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( type_w1771507213_j_k_l @ SV6 )
= $true )
| ( ( type_w1771507213_j_k_l @ SV6 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[410]) ).
thf(415,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( l_type1003141153_j_k_l @ SV6 )
= $true )
| ( ( type_w1771507213_j_k_l @ SV6 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[411]) ).
thf(416,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( type_w1771507213_j_k_l @ SV6 )
= $true )
| ( ( l_type1003141153_j_k_l @ SV6 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[412]) ).
thf(417,plain,
! [SV6: heap_S1465075775_j_k_l] :
( ( ( l_type1003141153_j_k_l @ SV6 )
= $true )
| ( ( l_type1003141153_j_k_l @ SV6 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[413]) ).
thf(418,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[372,417,416,415,414,403,402,401,400,399,388,387,379,378,376]) ).
thf(419,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[418]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP174^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/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.19 % Computer : n005.cluster.edu
% 0.12/0.19 % Model : x86_64 x86_64
% 0.12/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.19 % Memory : 8046.5625MB
% 0.12/0.19 % OS : Linux 6.8.0-71-generic
% 0.12/0.19 % CPULimit : 300
% 0.12/0.19 % WCLimit : 300
% 0.12/0.19 % DateTime : Tue Oct 6 11:19:00 UTC 2026
% 0.12/0.20 % CPUTime :
% 0.12/0.20 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.20/1.44 ..
% 7.20/1.44
% 7.20/1.44 No.of.Axioms: 9
% 7.20/1.44
% 7.20/1.44 Length.of.Defs: 0
% 7.20/1.44
% 7.20/1.44 Contains.Choice.Funs: false
% 7.20/1.44 ....
% 7.20/1.44
% 7.20/1.44 ********************************
% 7.20/1.44 * All subproblems solved! *
% 7.20/1.44 ********************************
% 7.20/1.44 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:9,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:418,loop_count:0,foatp_calls:1,translation:fof_full)
% 7.20/1.44
% 7.20/1.44 %**** Beginning of derivation protocol ****
% 7.20/1.44 % SZS output start CNFRefutation
% See solution above
% 7.20/1.44
% 7.20/1.44 %**** End of derivation protocol ****
% 7.20/1.44 %**** no. of clauses in derivation: 70 ****
% 7.20/1.44 %**** clause counter: 418 ****
% 7.20/1.44
% 7.20/1.44 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:9,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:418,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------