%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP310_1 : TPTP v9.2.0. Released v8.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n023.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 : Fri Oct 3 07:52:07 PM UTC 2025 % Result : Theorem 13.06s 13.30s % Output : Proof 13.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : ITP310_1 : TPTP v9.2.0. Released v8.0.0. % 0.11/0.13 % Command : duper %s % 0.13/0.35 % Computer : n023.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Oct 2 23:32:08 EDT 2025 % 0.13/0.35 % CPUTime : % 13.06/13.30 SZS status Theorem for theBenchmark.p % 13.06/13.30 SZS output start Proof for theBenchmark.p % 13.06/13.30 Clause #1 (by assumption #[]): Eq (Not («fun_app$a» («member$» «parent_ptr$») («fun_app$b» «fset$» («fun_app$c» «object_ptr_kinds$» «h$»)))) True % 13.06/13.30 Clause #2 (by assumption #[]): Eq («fun_app$d» («fmember$» «parent_ptr$») («fun_app$c» «object_ptr_kinds$» «h$»)) True % 13.06/13.30 Clause #4 (by assumption #[]): Eq % 13.06/13.30 (∀ % 13.06/13.30 (A__questionmark_v0 : % 13.06/13.30 «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$») % 13.06/13.30 (A__questionmark_v1 : % 13.06/13.30 «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$»), % 13.06/13.30 Iff («fun_app$a» («member$» A__questionmark_v0) («fun_app$b» «fset$» A__questionmark_v1)) % 13.06/13.30 («fun_app$d» («fmember$» A__questionmark_v0) A__questionmark_v1)) % 13.06/13.30 True % 13.06/13.30 Clause #565 (by clausification #[1]): Eq («fun_app$a» («member$» «parent_ptr$») («fun_app$b» «fset$» («fun_app$c» «object_ptr_kinds$» «h$»))) False % 13.06/13.30 Clause #619 (by clausification #[4]): ∀ % 13.06/13.30 (a : % 13.06/13.30 «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$»), % 13.06/13.30 Eq % 13.06/13.30 (∀ % 13.06/13.30 (A__questionmark_v1 : % 13.06/13.30 «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$»), % 13.06/13.30 Iff («fun_app$a» («member$» a) («fun_app$b» «fset$» A__questionmark_v1)) % 13.06/13.30 («fun_app$d» («fmember$» a) A__questionmark_v1)) % 13.06/13.30 True % 13.06/13.30 Clause #620 (by clausification #[619]): ∀ % 13.06/13.30 (a : % 13.06/13.30 «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$») % 13.06/13.30 (a_1 : % 13.06/13.30 «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$»), % 13.06/13.30 Eq (Iff («fun_app$a» («member$» a) («fun_app$b» «fset$» a_1)) («fun_app$d» («fmember$» a) a_1)) True % 13.06/13.30 Clause #621 (by clausification #[620]): ∀ % 13.06/13.30 (a : % 13.06/13.30 «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$») % 13.06/13.30 (a_1 : % 13.06/13.30 «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$»), % 13.06/13.30 Or (Eq («fun_app$a» («member$» a) («fun_app$b» «fset$» a_1)) True) (Eq («fun_app$d» («fmember$» a) a_1) False) % 13.06/13.30 Clause #623 (by superposition #[621, 2]): Or (Eq («fun_app$a» («member$» «parent_ptr$») («fun_app$b» «fset$» («fun_app$c» «object_ptr_kinds$» «h$»))) True) % 13.06/13.30 (Eq False True) % 13.06/13.30 Clause #3133 (by clausification #[623]): Eq («fun_app$a» («member$» «parent_ptr$») («fun_app$b» «fset$» («fun_app$c» «object_ptr_kinds$» «h$»))) True % 13.06/13.30 Clause #3134 (by superposition #[3133, 565]): Eq True False % 13.06/13.30 Clause #3146 (by clausification #[3134]): False % 13.06/13.30 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------