%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : ITP311_1 : TPTP v9.0.0. Released v8.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:12:42 AM UTC 2025
% Result : Theorem 0.48s 0.65s
% Output : Proof 0.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ITP311_1 : TPTP v9.0.0. Released v8.0.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.32 % Computer : n010.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 19 18:46:56 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.48/0.65 % SZS status Theorem
% 0.48/0.65 % SZS output start Proof
% 0.48/0.65 tff(tptp_fun__fun_app_aj__type, type, (
% 0.48/0.65 tptp_fun__fun_app_aj_: ( |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap_bool_fun$'| * |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'| ) > $o)).
% 0.48/0.65 tff(tptp_fun__pure___type, type, (
% 0.48/0.65 tptp_fun__pure__: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap_exception_a_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_list_prog$'| > |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap_bool_fun$'|)).
% 0.48/0.65 tff(tptp_fun__fun_app_x__type, type, (
% 0.48/0.65 tptp_fun__fun_app_x_: ( |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr_a_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap_exception_a_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_list_prog_fun$'| * |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'| ) > |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap_exception_a_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_list_prog$'|)).
% 0.48/0.65 tff(tptp_fun__get_child_nodes___type, type, (
% 0.48/0.65 tptp_fun__get_child_nodes__: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr_a_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap_exception_a_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_list_prog_fun$'|)).
% 0.48/0.65 tff(tptp_fun__h___type, type, (
% 0.48/0.65 tptp_fun__h__: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'|)).
% 0.48/0.65 tff(tptp_fun__parent___type, type, (
% 0.48/0.65 tptp_fun__parent__: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'|)).
% 0.48/0.65 tff(1,plain,
% 0.48/0.65 (^[A__questionmark_v0: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'|, A__questionmark_v1: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'|] : refl(tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, A__questionmark_v0)), A__questionmark_v1) <=> tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, A__questionmark_v0)), A__questionmark_v1))),
% 0.48/0.65 inference(bind,[status(th)],[])).
% 0.48/0.65 tff(2,plain,
% 0.48/0.65 (![A__questionmark_v0: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'|, A__questionmark_v1: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'|] : tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, A__questionmark_v0)), A__questionmark_v1) <=> ![A__questionmark_v0: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'|, A__questionmark_v1: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'|] : tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, A__questionmark_v0)), A__questionmark_v1)),
% 0.48/0.65 inference(quant_intro,[status(thm)],[1])).
% 0.48/0.65 tff(3,plain,
% 0.48/0.65 (![A__questionmark_v0: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'|, A__questionmark_v1: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'|] : tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, A__questionmark_v0)), A__questionmark_v1) <=> ![A__questionmark_v0: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'|, A__questionmark_v1: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'|] : tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, A__questionmark_v0)), A__questionmark_v1)),
% 0.48/0.65 inference(rewrite,[status(thm)],[])).
% 0.48/0.65 tff(4,axiom,(![A__questionmark_v0: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'|, A__questionmark_v1: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'|] : tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, A__questionmark_v0)), A__questionmark_v1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom69')).
% 0.48/0.65 tff(5,plain,
% 0.48/0.65 (![A__questionmark_v0: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'|, A__questionmark_v1: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'|] : tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, A__questionmark_v0)), A__questionmark_v1)),
% 0.48/0.65 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.48/0.65 tff(6,plain,(
% 0.48/0.65 ![A__questionmark_v0: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'|, A__questionmark_v1: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'|] : tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, A__questionmark_v0)), A__questionmark_v1)),
% 0.48/0.65 inference(skolemize,[status(sab)],[5])).
% 0.48/0.65 tff(7,plain,
% 0.48/0.65 (![A__questionmark_v0: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'|, A__questionmark_v1: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'|] : tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, A__questionmark_v0)), A__questionmark_v1)),
% 0.50/0.71 inference(modus_ponens,[status(thm)],[6, 2])).
% 0.50/0.71 tff(8,plain,
% 0.50/0.71 ((~tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, |'parent$'|)), |'h$'|)) <=> (~tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, |'parent$'|)), |'h$'|))),
% 0.50/0.71 inference(rewrite,[status(thm)],[])).
% 0.50/0.71 tff(9,axiom,(~tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, |'parent$'|)), |'h$'|)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','conjecture59')).
% 0.50/0.71 tff(10,plain,
% 0.50/0.71 (~tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, |'parent$'|)), |'h$'|)),
% 0.50/0.71 inference(modus_ponens,[status(thm)],[9, 8])).
% 0.50/0.71 tff(11,plain,
% 0.50/0.71 ((~![A__questionmark_v0: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_object_ptr$'|, A__questionmark_v1: |'A_element_ptr_b_character_data_ptr_c_sum_sum_node_ptr_d_document_ptr_e_shadow_root_ptr_f_sum_sum_sum_c_a_b_e_g_option_RElement_ext_h_option_RCharacterData_ext_i_sum_sum_RNode_ext_c_a_b_j_option_RDocument_ext_k_sum_sum_heap$'|] : tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, A__questionmark_v0)), A__questionmark_v1)) | tptp_fun__fun_app_aj_(tptp_fun__pure__(tptp_fun__fun_app_x_(|'get_child_nodes$'|, |'parent$'|)), |'h$'|)),
% 0.50/0.71 inference(quant_inst,[status(thm)],[])).
% 0.50/0.71 tff(12,plain,
% 0.50/0.71 ($false),
% 0.50/0.71 inference(unit_resolution,[status(thm)],[11, 10, 7])).
% 0.50/0.71 % SZS output end Proof
% 0.50/0.72 % E exiting
%------------------------------------------------------------------------------