%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWW245+1 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % 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 : 600s % DateTime : Thu Jul 21 02:21:24 EDT 2022 % Result : Theorem 0.48s 0.64s % Output : Proof 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SWW245+1 : TPTP v8.1.0. Released v5.2.0. % 0.04/0.13 % Command : run_zenon %s %d % 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 : 600 % 0.13/0.35 % DateTime : Mon Jun 6 06:40:09 EDT 2022 % 0.13/0.35 % CPUTime : % 0.48/0.64 (* PROOF-FOUND *) % 0.48/0.64 % SZS status Theorem % 0.48/0.64 (* BEGIN-PROOF *) % 0.48/0.64 % SZS output start Proof % 0.48/0.64 Theorem conj_0 : (exists B_k : zenon_U, (exists B_a : zenon_U, ((~(B_a = (c_Groups_Ozero__class_Ozero (t_a))))/\(exists B_q : zenon_U, ((((c_Polynomial_OpCons (t_a) (v_c____) (v_cs____)) = (c_Groups_Ozero__class_Ozero (tc_Polynomial_Opoly (t_a))))->((c_Nat_OSuc (c_Groups_Oplus__class_Oplus (tc_Nat_Onat) (c_If (tc_Nat_Onat) (c_fequal B_q (c_Groups_Ozero__class_Ozero (tc_Polynomial_Opoly (t_a)))) (c_Groups_Ozero__class_Ozero (tc_Nat_Onat)) (c_Nat_OSuc (c_Polynomial_Odegree (t_a) B_q))) B_k)) = (c_Groups_Ozero__class_Ozero (tc_Nat_Onat))))/\(((~((c_Polynomial_OpCons (t_a) (v_c____) (v_cs____)) = (c_Groups_Ozero__class_Ozero (tc_Polynomial_Opoly (t_a)))))->((c_Nat_OSuc (c_Groups_Oplus__class_Oplus (tc_Nat_Onat) (c_If (tc_Nat_Onat) (c_fequal B_q (c_Groups_Ozero__class_Ozero (tc_Polynomial_Opoly (t_a)))) (c_Groups_Ozero__class_Ozero (tc_Nat_Onat)) (c_Nat_OSuc (c_Polynomial_Odegree (t_a) B_q))) B_k)) = (c_Nat_OSuc (c_Polynomial_Odegree (t_a) (c_Polynomial_OpCons (t_a) (v_c____) (v_cs____))))))/\(forall B_z : zenon_U, ((hAPP (c_Polynomial_Opoly (t_a) (c_Polynomial_OpCons (t_a) (v_c____) (v_cs____))) B_z) = (hAPP (hAPP (c_Groups_Otimes__class_Otimes (t_a)) (hAPP (hAPP (c_Power_Opower__class_Opower (t_a)) B_z) B_k)) (hAPP (c_Polynomial_Opoly (t_a) (c_Polynomial_OpCons (t_a) B_a B_q)) B_z)))))))))). % 0.48/0.64 Proof. % 0.48/0.64 apply NNPP. intro zenon_G. % 0.48/0.64 apply (zenon_imply_s _ _ fact__096c_A_126_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096); [ zenon_intro zenon_H472 | zenon_intro zenon_H471 ]. % 0.48/0.64 exact (zenon_H472 tfree_0). % 0.48/0.64 apply (zenon_imply_s _ _ zenon_H471); [ zenon_intro zenon_H474 | zenon_intro zenon_H473 ]. % 0.48/0.64 apply zenon_H474. zenon_intro zenon_H475. % 0.48/0.64 apply (zenon_imply_s _ _ fact__096c_A_061_A_I0_058_058_Ha_J_061_061_062_AEX_Ak_Aa_Aq_O_Aa_A_126_061_A_I0_058_058_Ha_J_A_G_ASuc_A_I_Iif_Aq_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_Aq_J_J_A_L_Ak_J_A_061_A_Iif_ApCons_Ac_Acs_A_061_A0_Athen_A0_Aelse_ASuc_A_Idegree_A_IpCons_Ac_Acs_J_J_J_A_G_A_IALL_Az_O_Apoly_A_IpCons_Ac_Acs_J_Az_A_061_Az_A_094_Ak_A_K_Apoly_A_IpCons_Aa_Aq_J_Az_J_096); [ zenon_intro zenon_H472 | zenon_intro zenon_H476 ]. % 0.48/0.64 exact (zenon_H472 tfree_0). % 0.48/0.64 apply (zenon_imply_s _ _ zenon_H476); [ zenon_intro zenon_H477 | zenon_intro zenon_H473 ]. % 0.48/0.64 exact (zenon_H477 zenon_H475). % 0.48/0.64 exact (zenon_G zenon_H473). % 0.48/0.64 exact (zenon_G zenon_H473). % 0.48/0.64 Qed. % 0.48/0.64 % SZS output end Proof % 0.48/0.64 (* END-PROOF *) % 0.48/0.64 nodes searched: 25 % 0.48/0.64 max branch formulas: 1157 % 0.48/0.64 proof nodes created: 7 % 0.48/0.64 formulas created: 18543 % 0.48/0.64 %------------------------------------------------------------------------------