%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP312_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 : Thu Sep 24 12:55:24 PM UTC 2026
% Result : Theorem 4.66s 1.50s
% Output : CNFRefutation 4.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 18
% Syntax : Number of formulae : 76 ( 29 unt; 0 typ; 0 def)
% Number of atoms : 155 ( 44 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 137 ( 58 ~; 57 |; 7 &)
% ( 5 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of types : 10 ( 9 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 4 usr; 2 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-3 aty)
% Number of variables : 104 ( 0 sgn 104 !; 0 ?; 104 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$': $tType ).
tff(decl_sort2,type,
'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$': $tType ).
tff(decl_sort3,type,
'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_bool_fun$': $tType ).
tff(decl_sort4,type,
'Document_ptr_document_ptr_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog_fun$': $tType ).
tff(decl_sort5,type,
'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$': $tType ).
tff(decl_sort6,type,
'Exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_prod_sum$': $tType ).
tff(decl_sort7,type,
'Document_ptr_document_ptr_fset$': $tType ).
tff(decl_sort8,type,
'Document_ptr_document_ptr$': $tType ).
tff(decl_sort9,type,
'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_bool_fun$': $tType ).
tff(decl_33,type,
'execute$': ( 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$' * 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' ) > 'Exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_prod_sum$' ).
tff(decl_35,type,
'h2$': 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' ).
tff(decl_39,type,
'document_ptr_kinds$': 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' > 'Document_ptr_document_ptr_fset$' ).
tff(decl_43,type,
'h3$': 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' ).
tff(decl_51,type,
'type_wf$': 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_bool_fun$' ).
tff(decl_82,type,
'get_disconnected_nodes$': 'Document_ptr_document_ptr_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog_fun$' ).
tff(decl_96,type,
'select_result$': 'Exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_prod_sum$' > 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$' ).
tff(decl_109,type,
'fun_app$f': ( 'Document_ptr_document_ptr$' * 'Document_ptr_document_ptr_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog_fun$' ) > 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$' ).
tff(decl_128,type,
'fun_app$i': ( 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$' * 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_bool_fun$' ) > $o ).
tff(decl_154,type,
'fun_app$e': ( 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' * 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_bool_fun$' ) > $o ).
tff(decl_160,type,
'returns_result$b': ( 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$' * 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' ) > 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_bool_fun$' ).
tff(decl_167,type,
'fmember$b': ( 'Document_ptr_document_ptr_fset$' * 'Document_ptr_document_ptr$' ) > $o ).
tff(decl_229,type,
'document_ptr$': 'Document_ptr_document_ptr$' ).
tff(decl_255,type,
'doc_ptr$': 'Document_ptr_document_ptr$' ).
tff(decl_290,type,
'h$': 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' ).
tff(decl_291,type,
'h$a': 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' ).
tff(decl_292,type,
'is_OK$c': ( 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$' * 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' ) > $o ).
tff(decl_310,type,
esk1_3: ( 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' * ( 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$' * 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' ) ) > 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$' ).
tff(decl_313,type,
esk4_2: ( 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$' * 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$' ) > 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$' ).
tff(axiom86,axiom,
! [X160: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X161: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$'] :
( ( ! [X162: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( 'fun_app$i'('returns_result$b'(X160,X161),X162)
=> ~ $true )
& 'is_OK$c'(X160,X161) )
=> ~ $true ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom86) ).
tff(axiom45,axiom,
! [X64: 'Document_ptr_document_ptr$',X65: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( 'fun_app$i'('returns_result$b'('h$a','fun_app$f'('get_disconnected_nodes$',X64)),X65)
<=> 'fun_app$i'('returns_result$b'('h2$','fun_app$f'('get_disconnected_nodes$',X64)),X65) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom45) ).
tff(axiom12,axiom,
! [X26: 'Document_ptr_document_ptr$',X27: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ( 'document_ptr$' != X26 )
=> ( 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X26)),X27)
<=> 'fun_app$i'('returns_result$b'('h$','fun_app$f'('get_disconnected_nodes$',X26)),X27) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom12) ).
tff(axiom25,axiom,
! [X42: 'Document_ptr_document_ptr$',X43: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( 'fun_app$i'('returns_result$b'('h2$','fun_app$f'('get_disconnected_nodes$',X42)),X43)
<=> 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X42)),X43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom25) ).
tff(axiom23,axiom,
! [X36: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X37: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$',X38: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( 'fun_app$i'('returns_result$b'(X36,X37),X38)
=> ( 'select_result$'('execute$'(X36,X37)) = X38 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom23) ).
tff(axiom44,axiom,
! [X63: 'Document_ptr_document_ptr$'] : ( 'select_result$'('execute$'('h$a','fun_app$f'('get_disconnected_nodes$',X63))) = 'select_result$'('execute$'('h2$','fun_app$f'('get_disconnected_nodes$',X63))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom44) ).
tff(axiom14,axiom,
! [X28: 'Document_ptr_document_ptr$'] : ( 'select_result$'('execute$'('h2$','fun_app$f'('get_disconnected_nodes$',X28))) = 'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$',X28))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom14) ).
tff(conjecture6,conjecture,
'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$','doc_ptr$'))) = 'select_result$'('execute$'('h$','fun_app$f'('get_disconnected_nodes$','doc_ptr$'))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture6) ).
tff(axiom53,axiom,
! [X82: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X83: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$'] :
( 'is_OK$c'(X82,X83)
=> 'fun_app$i'('returns_result$b'(X82,X83),'select_result$'('execute$'(X82,X83))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom53) ).
tff(hypothesis7,hypothesis,
'document_ptr$' != 'doc_ptr$',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis7) ).
tff(axiom98,axiom,
! [X188: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X189: 'Document_ptr_document_ptr$'] :
( ( 'fmember$b'(X189,'document_ptr_kinds$'(X188))
& 'fun_app$e'('type_wf$',X188) )
=> 'is_OK$c'(X188,'fun_app$f'('get_disconnected_nodes$',X189)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom98) ).
tff(axiom47,axiom,
'document_ptr_kinds$'('h2$') = 'document_ptr_kinds$'('h$a'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom47) ).
tff(axiom34,axiom,
'document_ptr_kinds$'('h3$') = 'document_ptr_kinds$'('h2$'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom34) ).
tff(axiom101,axiom,
! [X193: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X194: 'Document_ptr_document_ptr$'] :
( 'is_OK$c'(X193,'fun_app$f'('get_disconnected_nodes$',X194))
=> 'fmember$b'(X194,'document_ptr_kinds$'(X193)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom101) ).
tff(axiom71,axiom,
! [X133: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X134: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$',X135: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( 'fun_app$i'('returns_result$b'(X133,X134),X135)
=> 'is_OK$c'(X133,X134) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom71) ).
tff(axiom10,axiom,
! [X20: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X21: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$',X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$'] :
( ! [X22: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( 'fun_app$i'('returns_result$b'(X20,X21),X22)
<=> 'fun_app$i'('returns_result$b'(X13,X21),X22) )
=> ( 'select_result$'('execute$'(X20,X21)) = 'select_result$'('execute$'(X13,X21)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom10) ).
tff(axiom39,axiom,
'fun_app$e'('type_wf$','h$a'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom39) ).
tff(axiom17,axiom,
'document_ptr_kinds$'('h$') = 'document_ptr_kinds$'('h3$'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom17) ).
tff(c_0_18,plain,
! [X3068: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X3069: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$'] :
( ( ~ $true
| ~ 'is_OK$c'(X3068,X3069)
| $true )
& ( ~ $true
| ~ 'is_OK$c'(X3068,X3069)
| 'fun_app$i'('returns_result$b'(X3068,X3069),esk4_2(X3068,X3069)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom86])])])])])])]) ).
tff(c_0_19,plain,
! [X3123: 'Document_ptr_document_ptr$',X3124: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ( 'fun_app$i'('returns_result$b'('h$a','fun_app$f'('get_disconnected_nodes$',X3123)),X3124)
| ~ 'fun_app$i'('returns_result$b'('h2$','fun_app$f'('get_disconnected_nodes$',X3123)),X3124) )
& ( 'fun_app$i'('returns_result$b'('h2$','fun_app$f'('get_disconnected_nodes$',X3123)),X3124)
| ~ 'fun_app$i'('returns_result$b'('h$a','fun_app$f'('get_disconnected_nodes$',X3123)),X3124) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom45])])]) ).
tcf(c_0_20,plain,
! [X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X21: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$'] :
( ~ $true
| ~ 'is_OK$c'(X13,X21)
| 'fun_app$i'('returns_result$b'(X13,X21),esk4_2(X13,X21)) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
tff(c_0_21,plain,
! [X26: 'Document_ptr_document_ptr$',X27: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ( 'document_ptr$' != X26 )
=> ( 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X26)),X27)
<=> 'fun_app$i'('returns_result$b'('h$','fun_app$f'('get_disconnected_nodes$',X26)),X27) ) ),
inference(fof_simplification,[status(thm)],[axiom12]) ).
tff(c_0_22,plain,
! [X3054: 'Document_ptr_document_ptr$',X3055: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ( 'fun_app$i'('returns_result$b'('h2$','fun_app$f'('get_disconnected_nodes$',X3054)),X3055)
| ~ 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X3054)),X3055) )
& ( 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X3054)),X3055)
| ~ 'fun_app$i'('returns_result$b'('h2$','fun_app$f'('get_disconnected_nodes$',X3054)),X3055) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom25])])]) ).
tcf(c_0_23,plain,
! [X26: 'Document_ptr_document_ptr$',X22: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ~ 'fun_app$i'('returns_result$b'('h$a','fun_app$f'('get_disconnected_nodes$',X26)),X22)
| 'fun_app$i'('returns_result$b'('h2$','fun_app$f'('get_disconnected_nodes$',X26)),X22) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
tcf(c_0_24,plain,
! [X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X21: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$'] :
( ~ 'is_OK$c'(X13,X21)
| 'fun_app$i'('returns_result$b'(X13,X21),esk4_2(X13,X21)) ),
inference(cn,[status(thm)],[c_0_20]) ).
tff(c_0_25,plain,
! [X3029: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X3030: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$',X3031: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ( 'select_result$'('execute$'(X3029,X3030)) = X3031 )
| ~ 'fun_app$i'('returns_result$b'(X3029,X3030),X3031) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom23])])]) ).
tff(c_0_26,plain,
! [X3122: 'Document_ptr_document_ptr$'] : ( 'select_result$'('execute$'('h$a','fun_app$f'('get_disconnected_nodes$',X3122))) = 'select_result$'('execute$'('h2$','fun_app$f'('get_disconnected_nodes$',X3122))) ),
inference(variable_rename,[status(thm)],[axiom44]) ).
tff(c_0_27,plain,
! [X3053: 'Document_ptr_document_ptr$'] : ( 'select_result$'('execute$'('h2$','fun_app$f'('get_disconnected_nodes$',X3053))) = 'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$',X3053))) ),
inference(variable_rename,[status(thm)],[axiom14]) ).
tff(c_0_28,negated_conjecture,
'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$','doc_ptr$'))) != 'select_result$'('execute$'('h$','fun_app$f'('get_disconnected_nodes$','doc_ptr$'))),
inference(assume_negation,[status(cth)],[conjecture6]) ).
tff(c_0_29,plain,
! [X3048: 'Document_ptr_document_ptr$',X3049: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ( ( 'document_ptr$' = X3048 )
| 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X3048)),X3049)
| ~ 'fun_app$i'('returns_result$b'('h$','fun_app$f'('get_disconnected_nodes$',X3048)),X3049) )
& ( ( 'document_ptr$' = X3048 )
| 'fun_app$i'('returns_result$b'('h$','fun_app$f'('get_disconnected_nodes$',X3048)),X3049)
| ~ 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X3048)),X3049) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_21])])])]) ).
tcf(c_0_30,plain,
! [X26: 'Document_ptr_document_ptr$',X22: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ~ 'fun_app$i'('returns_result$b'('h2$','fun_app$f'('get_disconnected_nodes$',X26)),X22)
| 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X26)),X22) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
tcf(c_0_31,plain,
! [X26: 'Document_ptr_document_ptr$'] :
( ~ 'is_OK$c'('h$a','fun_app$f'('get_disconnected_nodes$',X26))
| 'fun_app$i'('returns_result$b'('h2$','fun_app$f'('get_disconnected_nodes$',X26)),esk4_2('h$a','fun_app$f'('get_disconnected_nodes$',X26))) ),
inference(spm,[status(thm)],[c_0_23,c_0_24]) ).
tcf(c_0_32,plain,
! [X21: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$',X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X22: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ~ 'fun_app$i'('returns_result$b'(X13,X21),X22)
| ( 'select_result$'('execute$'(X13,X21)) = X22 ) ),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
tcf(c_0_33,plain,
! [X26: 'Document_ptr_document_ptr$'] : 'select_result$'('execute$'('h$a','fun_app$f'('get_disconnected_nodes$',X26))) = 'select_result$'('execute$'('h2$','fun_app$f'('get_disconnected_nodes$',X26))),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
tcf(c_0_34,plain,
! [X26: 'Document_ptr_document_ptr$'] : 'select_result$'('execute$'('h2$','fun_app$f'('get_disconnected_nodes$',X26))) = 'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$',X26))),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
tff(c_0_35,plain,
! [X3032: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X3033: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$'] :
( 'fun_app$i'('returns_result$b'(X3032,X3033),'select_result$'('execute$'(X3032,X3033)))
| ~ 'is_OK$c'(X3032,X3033) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom53])])]) ).
tff(c_0_36,negated_conjecture,
'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$','doc_ptr$'))) != 'select_result$'('execute$'('h$','fun_app$f'('get_disconnected_nodes$','doc_ptr$'))),
inference(fof_simplification,[status(thm)],[c_0_28]) ).
tcf(c_0_37,plain,
! [X26: 'Document_ptr_document_ptr$',X22: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ~ 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X26)),X22)
| ( 'document_ptr$' = X26 )
| 'fun_app$i'('returns_result$b'('h$','fun_app$f'('get_disconnected_nodes$',X26)),X22) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
tcf(c_0_38,plain,
! [X26: 'Document_ptr_document_ptr$'] :
( ~ 'is_OK$c'('h$a','fun_app$f'('get_disconnected_nodes$',X26))
| 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X26)),esk4_2('h$a','fun_app$f'('get_disconnected_nodes$',X26))) ),
inference(spm,[status(thm)],[c_0_30,c_0_31]) ).
tcf(c_0_39,plain,
! [X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X21: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$'] :
( ~ 'is_OK$c'(X13,X21)
| ( esk4_2(X13,X21) = 'select_result$'('execute$'(X13,X21)) ) ),
inference(spm,[status(thm)],[c_0_32,c_0_24]) ).
tcf(c_0_40,plain,
! [X26: 'Document_ptr_document_ptr$'] : 'select_result$'('execute$'('h$a','fun_app$f'('get_disconnected_nodes$',X26))) = 'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$',X26))),
inference(rw,[status(thm)],[c_0_33,c_0_34]) ).
tff(c_0_41,hypothesis,
'document_ptr$' != 'doc_ptr$',
inference(fof_simplification,[status(thm)],[hypothesis7]) ).
tff(c_0_42,plain,
! [X3044: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X3045: 'Document_ptr_document_ptr$'] :
( 'is_OK$c'(X3044,'fun_app$f'('get_disconnected_nodes$',X3045))
| ~ 'fmember$b'(X3045,'document_ptr_kinds$'(X3044))
| ~ 'fun_app$e'('type_wf$',X3044) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom98])])]) ).
tcf(c_0_43,plain,
'document_ptr_kinds$'('h2$') = 'document_ptr_kinds$'('h$a'),
inference(split_conjunct,[status(thm)],[axiom47]) ).
tcf(c_0_44,plain,
'document_ptr_kinds$'('h3$') = 'document_ptr_kinds$'('h2$'),
inference(split_conjunct,[status(thm)],[axiom34]) ).
tff(c_0_45,plain,
! [X3046: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X3047: 'Document_ptr_document_ptr$'] :
( 'fmember$b'(X3047,'document_ptr_kinds$'(X3046))
| ~ 'is_OK$c'(X3046,'fun_app$f'('get_disconnected_nodes$',X3047)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom101])])]) ).
tff(c_0_46,plain,
! [X3065: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X3066: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$',X3067: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( 'is_OK$c'(X3065,X3066)
| ~ 'fun_app$i'('returns_result$b'(X3065,X3066),X3067) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom71])])]) ).
tff(c_0_47,plain,
! [X3025: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X3026: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$',X3027: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$'] :
( ( ( 'select_result$'('execute$'(X3025,X3026)) = 'select_result$'('execute$'(X3027,X3026)) )
| 'fun_app$i'('returns_result$b'(X3027,X3026),esk1_3(X3025,X3026,X3027))
| 'fun_app$i'('returns_result$b'(X3025,X3026),esk1_3(X3025,X3026,X3027)) )
& ( ( 'select_result$'('execute$'(X3025,X3026)) = 'select_result$'('execute$'(X3027,X3026)) )
| ~ 'fun_app$i'('returns_result$b'(X3027,X3026),esk1_3(X3025,X3026,X3027))
| ~ 'fun_app$i'('returns_result$b'(X3025,X3026),esk1_3(X3025,X3026,X3027)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom10])])])])]) ).
tcf(c_0_48,plain,
! [X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X21: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$'] :
( ~ 'is_OK$c'(X13,X21)
| 'fun_app$i'('returns_result$b'(X13,X21),'select_result$'('execute$'(X13,X21))) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
tff(c_0_49,negated_conjecture,
'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$','doc_ptr$'))) != 'select_result$'('execute$'('h$','fun_app$f'('get_disconnected_nodes$','doc_ptr$'))),
inference(fof_nnf,[status(thm)],[c_0_36]) ).
tcf(c_0_50,plain,
! [X26: 'Document_ptr_document_ptr$',X22: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ~ 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X26)),X22)
| ( 'document_ptr$' = X26 )
| ( 'select_result$'('execute$'('h$','fun_app$f'('get_disconnected_nodes$',X26))) = X22 ) ),
inference(spm,[status(thm)],[c_0_32,c_0_37]) ).
tcf(c_0_51,plain,
! [X26: 'Document_ptr_document_ptr$'] :
( ~ 'is_OK$c'('h$a','fun_app$f'('get_disconnected_nodes$',X26))
| 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X26)),'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$',X26)))) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38,c_0_39]),c_0_40]) ).
tff(c_0_52,hypothesis,
'document_ptr$' != 'doc_ptr$',
inference(fof_nnf,[status(thm)],[c_0_41]) ).
tcf(c_0_53,plain,
! [X26: 'Document_ptr_document_ptr$',X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$'] :
( ~ 'fmember$b'(X26,'document_ptr_kinds$'(X13))
| ~ 'fun_app$e'('type_wf$',X13)
| 'is_OK$c'(X13,'fun_app$f'('get_disconnected_nodes$',X26)) ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
tcf(c_0_54,plain,
'document_ptr_kinds$'('h$a') = 'document_ptr_kinds$'('h3$'),
inference(rw,[status(thm)],[c_0_43,c_0_44]) ).
tcf(c_0_55,plain,
'fun_app$e'('type_wf$','h$a'),
inference(split_conjunct,[status(thm)],[axiom39]) ).
tcf(c_0_56,plain,
! [X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X26: 'Document_ptr_document_ptr$'] :
( ~ 'is_OK$c'(X13,'fun_app$f'('get_disconnected_nodes$',X26))
| 'fmember$b'(X26,'document_ptr_kinds$'(X13)) ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
tcf(c_0_57,plain,
'document_ptr_kinds$'('h$') = 'document_ptr_kinds$'('h3$'),
inference(split_conjunct,[status(thm)],[axiom17]) ).
tcf(c_0_58,plain,
! [X21: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$',X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X22: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ~ 'fun_app$i'('returns_result$b'(X13,X21),X22)
| 'is_OK$c'(X13,X21) ),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
tcf(c_0_59,plain,
! [X26: 'Document_ptr_document_ptr$',X22: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ~ 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X26)),X22)
| 'fun_app$i'('returns_result$b'('h2$','fun_app$f'('get_disconnected_nodes$',X26)),X22) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
tcf(c_0_60,plain,
! [X14: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X21: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$'] :
( ( 'select_result$'('execute$'(X13,X21)) = 'select_result$'('execute$'(X14,X21)) )
| 'fun_app$i'('returns_result$b'(X14,X21),esk1_3(X13,X21,X14))
| 'fun_app$i'('returns_result$b'(X13,X21),esk1_3(X13,X21,X14)) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
tcf(c_0_61,plain,
! [X26: 'Document_ptr_document_ptr$'] :
( ~ 'is_OK$c'('h2$','fun_app$f'('get_disconnected_nodes$',X26))
| 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X26)),'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$',X26)))) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30,c_0_48]),c_0_34]) ).
tcf(c_0_62,negated_conjecture,
'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$','doc_ptr$'))) != 'select_result$'('execute$'('h$','fun_app$f'('get_disconnected_nodes$','doc_ptr$'))),
inference(split_conjunct,[status(thm)],[c_0_49]) ).
tcf(c_0_63,plain,
! [X26: 'Document_ptr_document_ptr$'] :
( ~ 'is_OK$c'('h$a','fun_app$f'('get_disconnected_nodes$',X26))
| ( 'document_ptr$' = X26 )
| ( 'select_result$'('execute$'('h$','fun_app$f'('get_disconnected_nodes$',X26))) = 'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$',X26))) ) ),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
tcf(c_0_64,hypothesis,
'document_ptr$' != 'doc_ptr$',
inference(split_conjunct,[status(thm)],[c_0_52]) ).
tcf(c_0_65,plain,
! [X26: 'Document_ptr_document_ptr$'] :
( ~ 'fmember$b'(X26,'document_ptr_kinds$'('h3$'))
| 'is_OK$c'('h$a','fun_app$f'('get_disconnected_nodes$',X26)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_54]),c_0_55])]) ).
tcf(c_0_66,plain,
! [X26: 'Document_ptr_document_ptr$'] :
( ~ 'is_OK$c'('h$','fun_app$f'('get_disconnected_nodes$',X26))
| 'fmember$b'(X26,'document_ptr_kinds$'('h3$')) ),
inference(spm,[status(thm)],[c_0_56,c_0_57]) ).
tcf(c_0_67,plain,
! [X26: 'Document_ptr_document_ptr$',X22: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list$'] :
( ~ 'fun_app$i'('returns_result$b'('h3$','fun_app$f'('get_disconnected_nodes$',X26)),X22)
| 'is_OK$c'('h2$','fun_app$f'('get_disconnected_nodes$',X26)) ),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
tcf(c_0_68,plain,
! [X21: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap_exception_element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_list_prog$',X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X14: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$'] :
( 'fun_app$i'('returns_result$b'(X13,X21),esk1_3(X13,X21,X14))
| 'is_OK$c'(X14,X21)
| ( 'select_result$'('execute$'(X13,X21)) = 'select_result$'('execute$'(X14,X21)) ) ),
inference(spm,[status(thm)],[c_0_58,c_0_60]) ).
tcf(c_0_69,plain,
! [X26: 'Document_ptr_document_ptr$'] :
( ~ 'is_OK$c'('h2$','fun_app$f'('get_disconnected_nodes$',X26))
| ( 'document_ptr$' = X26 )
| ( 'select_result$'('execute$'('h$','fun_app$f'('get_disconnected_nodes$',X26))) = 'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$',X26))) ) ),
inference(spm,[status(thm)],[c_0_50,c_0_61]) ).
tcf(c_0_70,negated_conjecture,
~ 'is_OK$c'('h$a','fun_app$f'('get_disconnected_nodes$','doc_ptr$')),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_62,c_0_63]),c_0_64]) ).
tcf(c_0_71,plain,
! [X26: 'Document_ptr_document_ptr$'] :
( ~ 'is_OK$c'('h$','fun_app$f'('get_disconnected_nodes$',X26))
| 'is_OK$c'('h$a','fun_app$f'('get_disconnected_nodes$',X26)) ),
inference(spm,[status(thm)],[c_0_65,c_0_66]) ).
tcf(c_0_72,plain,
! [X13: 'Element_ptr_element_ptr_character_data_ptr_character_data_ptr_node_ptr_sum_sum_node_ptr_document_ptr_document_ptr_shadow_root_ptr_shadow_root_ptr_object_ptr_sum_sum_sum_node_ptr_element_ptr_character_data_ptr_shadow_root_ptr_Element_option_RElement_ext_CharacterData_option_RCharacterData_ext_Node_sum_sum_RNode_ext_node_ptr_element_ptr_character_data_ptr_Document_option_RDocument_ext_Object_sum_sum_heap$',X26: 'Document_ptr_document_ptr$'] :
( 'is_OK$c'(X13,'fun_app$f'('get_disconnected_nodes$',X26))
| 'is_OK$c'('h2$','fun_app$f'('get_disconnected_nodes$',X26))
| ( 'select_result$'('execute$'('h3$','fun_app$f'('get_disconnected_nodes$',X26))) = 'select_result$'('execute$'(X13,'fun_app$f'('get_disconnected_nodes$',X26))) ) ),
inference(spm,[status(thm)],[c_0_67,c_0_68]) ).
tcf(c_0_73,negated_conjecture,
~ 'is_OK$c'('h2$','fun_app$f'('get_disconnected_nodes$','doc_ptr$')),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_62,c_0_69]),c_0_64]) ).
tcf(c_0_74,negated_conjecture,
~ 'is_OK$c'('h$','fun_app$f'('get_disconnected_nodes$','doc_ptr$')),
inference(spm,[status(thm)],[c_0_70,c_0_71]) ).
cnf(c_0_75,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_62,c_0_72]),c_0_73]),c_0_74]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP312_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.55 % Computer : n002.cluster.edu
% 0.11/0.55 % Model : x86_64 x86_64
% 0.11/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.55 % Memory : 8046.5625MB
% 0.11/0.55 % OS : Linux 6.8.0-71-generic
% 0.11/0.55 % CPULimit : 300
% 0.11/0.55 % WCLimit : 300
% 0.11/0.55 % DateTime : Sun Sep 20 22:36:18 UTC 2026
% 0.11/0.55 % CPUTime :
% 0.11/0.55 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.59 Running first-order theorem proving
% 0.15/0.59 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.66/1.50 % Version: 3.5.1
% 4.66/1.50 % Preprocessing class: FMLMSMSMSSSNFFN.
% 4.66/1.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 4.66/1.50 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 4.66/1.50 % Starting new_bool_3 with 300s (1) cores
% 4.66/1.50 % Starting new_bool_1 with 300s (1) cores
% 4.66/1.50 % Starting sh5l with 300s (1) cores
% 4.66/1.50 % new_bool_1 with pid 1848242 completed with status 0
% 4.66/1.50 % Result found by new_bool_1
% 4.66/1.50 % Preprocessing class: FMLMSMSMSSSNFFN.
% 4.66/1.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 4.66/1.50 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 4.66/1.50 % Starting new_bool_3 with 300s (1) cores
% 4.66/1.50 % Starting new_bool_1 with 300s (1) cores
% 4.66/1.50 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 4.66/1.50 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 4.66/1.50 % Search class: FGUSM-FSLM31-MFFFFFNN
% 4.66/1.50 % partial match(1): FGHSM-FSLM31-MFFFFFNN
% 4.66/1.50 % Scheduled 8 strats onto 1 cores with 300 seconds (300 total)
% 4.66/1.50 % Starting SubtermCWHack with 28s (1) cores
% 4.66/1.50 % SubtermCWHack with pid 1848245 completed with status 0
% 4.66/1.50 % Result found by SubtermCWHack
% 4.66/1.50 % Preprocessing class: FMLMSMSMSSSNFFN.
% 4.66/1.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 4.66/1.50 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 4.66/1.50 % Starting new_bool_3 with 300s (1) cores
% 4.66/1.50 % Starting new_bool_1 with 300s (1) cores
% 4.66/1.50 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 4.66/1.50 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 4.66/1.50 % Search class: FGUSM-FSLM31-MFFFFFNN
% 4.66/1.50 % partial match(1): FGHSM-FSLM31-MFFFFFNN
% 4.66/1.50 % Scheduled 8 strats onto 1 cores with 300 seconds (300 total)
% 4.66/1.50 % Starting SubtermCWHack with 28s (1) cores
% 4.66/1.50 % Preprocessing time : 0.006 s
% 4.66/1.50
% 4.66/1.50 % Proof found!
% 4.66/1.50 % SZS status Theorem
% 4.66/1.50 % SZS output start CNFRefutation
% See solution above
% 4.66/1.50 % Parsed axioms : 1053
% 4.66/1.50 % Removed by relevancy pruning/SinE : 904
% 4.66/1.50 % Initial clauses : 225
% 4.66/1.50 % Removed in clause preprocessing : 48
% 4.66/1.50 % Initial clauses in saturation : 177
% 4.66/1.50 % Processed clauses : 5781
% 4.66/1.50 % ...of these trivial : 2
% 4.66/1.50 % ...subsumed : 4566
% 4.66/1.50 % ...remaining for further processing : 1213
% 4.66/1.50 % Other redundant clauses eliminated : 14
% 4.66/1.50 % Clauses deleted for lack of memory : 0
% 4.66/1.50 % Backward-subsumed : 6
% 4.66/1.50 % Backward-rewritten : 1
% 4.66/1.50 % Generated clauses : 28080
% 4.66/1.50 % ...of the previous two non-redundant : 25591
% 4.66/1.50 % ...aggressively subsumed : 0
% 4.66/1.50 % Contextual simplify-reflections : 65
% 4.66/1.50 % Paramodulations : 28035
% 4.66/1.50 % Factorizations : 29
% 4.66/1.50 % NegExts : 0
% 4.66/1.50 % Equation resolutions : 16
% 4.66/1.50 % Disequality decompositions : 0
% 4.66/1.50 % Total rewrite steps : 7974
% 4.66/1.50 % ...of those cached : 7931
% 4.66/1.50 % Propositional unsat checks : 0
% 4.66/1.50 % Propositional check models : 0
% 4.66/1.50 % Propositional check unsatisfiable : 0
% 4.66/1.50 % Propositional clauses : 0
% 4.66/1.50 % Propositional clauses after purity: 0
% 4.66/1.50 % Propositional unsat core size : 0
% 4.66/1.50 % Propositional preprocessing time : 0.000
% 4.66/1.50 % Propositional encoding time : 0.000
% 4.66/1.50 % Propositional solver time : 0.000
% 4.66/1.50 % Success case prop preproc time : 0.000
% 4.66/1.50 % Success case prop encoding time : 0.000
% 4.66/1.50 % Success case prop solver time : 0.000
% 4.66/1.50 % Current number of processed clauses : 1192
% 4.66/1.50 % Positive orientable unit clauses : 47
% 4.66/1.50 % Positive unorientable unit clauses: 0
% 4.66/1.50 % Negative unit clauses : 6
% 4.66/1.50 % Non-unit-clauses : 1139
% 4.66/1.50 % Current number of unprocessed clauses: 19966
% 4.66/1.50 % ...number of literals in the above : 89001
% 4.66/1.50 % Current number of archived formulas : 0
% 4.66/1.50 % Current number of archived clauses : 7
% 4.66/1.50 % Clause-clause subsumption calls (NU) : 181224
% 4.66/1.50 % Rec. Clause-clause subsumption calls : 145504
% 4.66/1.50 % Non-unit clause-clause subsumptions : 4631
% 4.66/1.50 % Unit Clause-clause subsumption calls : 126
% 4.66/1.50 % Rewrite failures with RHS unbound : 0
% 4.66/1.50 % BW rewrite match attempts : 4
% 4.66/1.50 % BW rewrite match successes : 1
% 4.66/1.50 % Condensation attempts : 0
% 4.66/1.50 % Condensation successes : 0
% 4.66/1.50 % Termbank termtop insertions : 725634
% 4.66/1.50 % Search garbage collected termcells : 13682
% 4.66/1.50
% 4.66/1.50 % -------------------------------------------------
% 4.66/1.50 % User time : 0.696 s
% 4.66/1.50 % System time : 0.033 s
% 4.66/1.50 % Total time : 0.729 s
% 4.66/1.50 % Maximum resident set size: 7528 pages
% 4.66/1.50
% 4.66/1.50 % -------------------------------------------------
% 4.66/1.50 % User time : 0.831 s
% 4.66/1.50 % System time : 0.049 s
% 4.66/1.50 % Total time : 0.880 s
% 4.66/1.50 % Maximum resident set size: 7936 pages
% 4.66/1.50 % E exiting
%------------------------------------------------------------------------------