%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : ITP310_1 : TPTP v9.0.0. Released v8.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n004.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.39s 0.57s
% Output : Proof 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ITP310_1 : TPTP v9.0.0. Released v8.0.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n004.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % 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:44:53 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.39/0.57 % SZS status Theorem
% 0.39/0.57 % SZS output start Proof
% 0.39/0.57 tff(tptp_fun__fun_app_d__type, type, (
% 0.39/0.57 tptp_fun__fun_app_d_: ( |'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_object_ptr_fset_bool_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_object_ptr_fset$'| ) > $o)).
% 0.39/0.57 tff(tptp_fun__fun_app_c__type, type, (
% 0.39/0.57 tptp_fun__fun_app_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_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_object_ptr_fset_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$'| ) > |'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_object_ptr_fset$'|)).
% 0.39/0.57 tff(tptp_fun__h___type, type, (
% 0.39/0.57 tptp_fun__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$'|)).
% 0.39/0.57 tff(tptp_fun__object_ptr_kinds___type, type, (
% 0.39/0.57 tptp_fun__object_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_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_object_ptr_fset_fun$'|)).
% 0.39/0.57 tff(tptp_fun__fmember___type, type, (
% 0.39/0.57 tptp_fun__fmember__: |'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_object_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_object_ptr_fset_bool_fun$'|)).
% 0.39/0.57 tff(tptp_fun__parent_ptr___type, type, (
% 0.39/0.57 tptp_fun__parent_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_object_ptr$'|)).
% 0.39/0.57 tff(tptp_fun__fun_app_a__type, type, (
% 0.39/0.57 tptp_fun__fun_app_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_object_ptr_set_bool_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_object_ptr_set$'| ) > $o)).
% 0.39/0.57 tff(tptp_fun__fun_app_b__type, type, (
% 0.39/0.57 tptp_fun__fun_app_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_object_ptr_fset_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_object_ptr_set_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_object_ptr_fset$'| ) > |'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_object_ptr_set$'|)).
% 0.39/0.57 tff(tptp_fun__fset___type, type, (
% 0.39/0.57 tptp_fun__fset__: |'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_object_ptr_fset_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_object_ptr_set_fun$'|)).
% 0.39/0.57 tff(tptp_fun__member___type, type, (
% 0.39/0.57 tptp_fun__member__: |'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_object_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_object_ptr_set_bool_fun$'|)).
% 0.39/0.57 tff(1,plain,
% 0.39/0.57 (tptp_fun__fun_app_d_(tptp_fun__fmember__(|'parent_ptr$'|), tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(|'parent_ptr$'|), tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|))),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(2,axiom,(tptp_fun__fun_app_d_(tptp_fun__fmember__(|'parent_ptr$'|), tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom2')).
% 0.39/0.57 tff(3,plain,
% 0.39/0.57 (tptp_fun__fun_app_d_(tptp_fun__fmember__(|'parent_ptr$'|), tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[2, 1])).
% 0.39/0.57 tff(4,plain,
% 0.39/0.57 ((~tptp_fun__fun_app_a_(tptp_fun__member__(|'parent_ptr$'|), tptp_fun__fun_app_b_(|'fset$'|, tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|)))) <=> (~tptp_fun__fun_app_a_(tptp_fun__member__(|'parent_ptr$'|), tptp_fun__fun_app_b_(|'fset$'|, tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|))))),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(5,axiom,(~tptp_fun__fun_app_a_(tptp_fun__member__(|'parent_ptr$'|), tptp_fun__fun_app_b_(|'fset$'|, tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','conjecture1')).
% 0.39/0.57 tff(6,plain,
% 0.39/0.57 (~tptp_fun__fun_app_a_(tptp_fun__member__(|'parent_ptr$'|), tptp_fun__fun_app_b_(|'fset$'|, tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|)))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.39/0.57 tff(7,plain,
% 0.39/0.57 ((~(tptp_fun__fun_app_a_(tptp_fun__member__(|'parent_ptr$'|), tptp_fun__fun_app_b_(|'fset$'|, tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|))) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(|'parent_ptr$'|), tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|)))) | tptp_fun__fun_app_a_(tptp_fun__member__(|'parent_ptr$'|), tptp_fun__fun_app_b_(|'fset$'|, tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|))) | (~tptp_fun__fun_app_d_(tptp_fun__fmember__(|'parent_ptr$'|), tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|)))),
% 0.39/0.57 inference(tautology,[status(thm)],[])).
% 0.39/0.57 tff(8,plain,
% 0.39/0.57 (~(tptp_fun__fun_app_a_(tptp_fun__member__(|'parent_ptr$'|), tptp_fun__fun_app_b_(|'fset$'|, tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|))) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(|'parent_ptr$'|), tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|)))),
% 0.39/0.57 inference(unit_resolution,[status(thm)],[7, 6, 3])).
% 0.39/0.58 tff(9,plain,
% 0.39/0.58 (^[A__questionmark_v0: |'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_object_ptr$'|, A__questionmark_v1: |'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_object_ptr_fset$'|] : refl((tptp_fun__fun_app_a_(tptp_fun__member__(A__questionmark_v0), tptp_fun__fun_app_b_(|'fset$'|, A__questionmark_v1)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(A__questionmark_v0), A__questionmark_v1)) <=> (tptp_fun__fun_app_a_(tptp_fun__member__(A__questionmark_v0), tptp_fun__fun_app_b_(|'fset$'|, A__questionmark_v1)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(A__questionmark_v0), A__questionmark_v1)))),
% 0.39/0.58 inference(bind,[status(th)],[])).
% 0.39/0.58 tff(10,plain,
% 0.39/0.58 (![A__questionmark_v0: |'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_object_ptr$'|, A__questionmark_v1: |'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_object_ptr_fset$'|] : (tptp_fun__fun_app_a_(tptp_fun__member__(A__questionmark_v0), tptp_fun__fun_app_b_(|'fset$'|, A__questionmark_v1)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(A__questionmark_v0), A__questionmark_v1)) <=> ![A__questionmark_v0: |'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_object_ptr$'|, A__questionmark_v1: |'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_object_ptr_fset$'|] : (tptp_fun__fun_app_a_(tptp_fun__member__(A__questionmark_v0), tptp_fun__fun_app_b_(|'fset$'|, A__questionmark_v1)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(A__questionmark_v0), A__questionmark_v1))),
% 0.39/0.58 inference(quant_intro,[status(thm)],[9])).
% 0.39/0.58 tff(11,plain,
% 0.39/0.58 (![A__questionmark_v0: |'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_object_ptr$'|, A__questionmark_v1: |'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_object_ptr_fset$'|] : (tptp_fun__fun_app_a_(tptp_fun__member__(A__questionmark_v0), tptp_fun__fun_app_b_(|'fset$'|, A__questionmark_v1)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(A__questionmark_v0), A__questionmark_v1)) <=> ![A__questionmark_v0: |'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_object_ptr$'|, A__questionmark_v1: |'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_object_ptr_fset$'|] : (tptp_fun__fun_app_a_(tptp_fun__member__(A__questionmark_v0), tptp_fun__fun_app_b_(|'fset$'|, A__questionmark_v1)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(A__questionmark_v0), A__questionmark_v1))),
% 0.39/0.58 inference(rewrite,[status(thm)],[])).
% 0.39/0.58 tff(12,axiom,(![A__questionmark_v0: |'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_object_ptr$'|, A__questionmark_v1: |'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_object_ptr_fset$'|] : (tptp_fun__fun_app_a_(tptp_fun__member__(A__questionmark_v0), tptp_fun__fun_app_b_(|'fset$'|, A__questionmark_v1)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(A__questionmark_v0), A__questionmark_v1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom4')).
% 0.39/0.61 tff(13,plain,
% 0.39/0.61 (![A__questionmark_v0: |'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_object_ptr$'|, A__questionmark_v1: |'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_object_ptr_fset$'|] : (tptp_fun__fun_app_a_(tptp_fun__member__(A__questionmark_v0), tptp_fun__fun_app_b_(|'fset$'|, A__questionmark_v1)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(A__questionmark_v0), A__questionmark_v1))),
% 0.39/0.61 inference(modus_ponens,[status(thm)],[12, 11])).
% 0.39/0.61 tff(14,plain,(
% 0.39/0.61 ![A__questionmark_v0: |'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_object_ptr$'|, A__questionmark_v1: |'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_object_ptr_fset$'|] : (tptp_fun__fun_app_a_(tptp_fun__member__(A__questionmark_v0), tptp_fun__fun_app_b_(|'fset$'|, A__questionmark_v1)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(A__questionmark_v0), A__questionmark_v1))),
% 0.39/0.61 inference(skolemize,[status(sab)],[13])).
% 0.39/0.61 tff(15,plain,
% 0.39/0.61 (![A__questionmark_v0: |'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_object_ptr$'|, A__questionmark_v1: |'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_object_ptr_fset$'|] : (tptp_fun__fun_app_a_(tptp_fun__member__(A__questionmark_v0), tptp_fun__fun_app_b_(|'fset$'|, A__questionmark_v1)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(A__questionmark_v0), A__questionmark_v1))),
% 0.39/0.61 inference(modus_ponens,[status(thm)],[14, 10])).
% 0.39/0.61 tff(16,plain,
% 0.39/0.61 ((~![A__questionmark_v0: |'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_object_ptr$'|, A__questionmark_v1: |'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_object_ptr_fset$'|] : (tptp_fun__fun_app_a_(tptp_fun__member__(A__questionmark_v0), tptp_fun__fun_app_b_(|'fset$'|, A__questionmark_v1)) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(A__questionmark_v0), A__questionmark_v1))) | (tptp_fun__fun_app_a_(tptp_fun__member__(|'parent_ptr$'|), tptp_fun__fun_app_b_(|'fset$'|, tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|))) <=> tptp_fun__fun_app_d_(tptp_fun__fmember__(|'parent_ptr$'|), tptp_fun__fun_app_c_(|'object_ptr_kinds$'|, |'h$'|)))),
% 0.39/0.61 inference(quant_inst,[status(thm)],[])).
% 0.39/0.61 tff(17,plain,
% 0.39/0.61 ($false),
% 0.39/0.61 inference(unit_resolution,[status(thm)],[16, 15, 8])).
% 0.39/0.61 % SZS output end Proof
% 0.39/0.62 % E exiting
%------------------------------------------------------------------------------