%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KLE129+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n020.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 : Sun Jul 17 02:37:43 EDT 2022 % Result : Theorem 27.55s 27.77s % Output : Proof 27.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.07 % Problem : KLE129+1 : TPTP v8.1.0. Released v4.0.0. % 0.00/0.07 % Command : run_zenon %s %d % 0.06/0.25 % Computer : n020.cluster.edu % 0.06/0.25 % Model : x86_64 x86_64 % 0.06/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.25 % Memory : 8042.1875MB % 0.06/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.26 % CPULimit : 300 % 0.06/0.26 % WCLimit : 600 % 0.06/0.26 % DateTime : Thu Jun 16 09:44:04 EDT 2022 % 0.06/0.26 % CPUTime : % 27.55/27.77 (* PROOF-FOUND *) % 27.55/27.77 % SZS status Theorem % 27.55/27.77 (* BEGIN-PROOF *) % 27.55/27.77 % SZS output start Proof % 27.55/27.77 Theorem goals : (forall X0 : zenon_U, ((forall X1 : zenon_U, (((addition (domain X1) (forward_diamond X0 (domain X1))) = (forward_diamond X0 (domain X1)))->((domain X1) = (zero))))->((divergence X0) = (zero)))). % 27.55/27.77 Proof. % 27.55/27.77 assert (zenon_L1_ : forall (zenon_TX0_bf : zenon_U), (~((antidomain (antidomain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))) = (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))))) -> ((antidomain (antidomain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))) = (divergence zenon_TX0_bf)) -> False). % 27.55/27.77 do 1 intro. intros zenon_H1d zenon_H1e. % 27.55/27.77 cut (((antidomain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) = (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 27.55/27.77 congruence. % 27.55/27.77 cut (((multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))) = (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))); [idtac | apply NNPP; zenon_intro zenon_H21]. % 27.55/27.77 congruence. % 27.55/27.77 cut (((domain (divergence zenon_TX0_bf)) = (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))); [idtac | apply NNPP; zenon_intro zenon_H22]. % 27.55/27.77 cut ((zenon_TX0_bf = zenon_TX0_bf)); [idtac | apply NNPP; zenon_intro zenon_H23]. % 27.55/27.77 congruence. % 27.55/27.77 apply zenon_H23. apply refl_equal. % 27.55/27.77 generalize (domain4 (divergence zenon_TX0_bf)). zenon_intro zenon_H24. % 27.55/27.77 apply (zenon_congruence_lr_s _ (fun zenon_Vq : _ => (~(zenon_Vq = (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))) _ _ zenon_H22 zenon_H24). zenon_intro zenon_H25. % 27.55/27.77 generalize (domain4 (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))). zenon_intro zenon_H26. % 27.55/27.77 apply (zenon_congruence_lr_s _ (fun zenon_Vs : _ => (~((antidomain (antidomain (divergence zenon_TX0_bf))) = zenon_Vs))) _ _ zenon_H25 zenon_H26). zenon_intro zenon_H27. % 27.55/27.77 cut (((antidomain (divergence zenon_TX0_bf)) = (antidomain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))); [idtac | apply NNPP; zenon_intro zenon_H28]. % 27.55/27.77 congruence. % 27.55/27.77 cut (((divergence zenon_TX0_bf) = (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 27.55/27.77 congruence. % 27.55/27.77 generalize (domain4 (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))). zenon_intro zenon_H2a. % 27.55/27.77 apply (zenon_congruence_lr_s _ (fun zenon_Vu : _ => (~((divergence zenon_TX0_bf) = zenon_Vu))) _ _ zenon_H29 zenon_H2a). zenon_intro zenon_H2b. % 27.55/27.77 apply zenon_H2b. apply sym_equal. exact zenon_H1e. % 27.55/27.77 (* end of lemma zenon_L1_ *) % 27.55/27.77 apply NNPP. intro zenon_G. % 27.55/27.77 apply (zenon_notallex_s (fun X0 : zenon_U => ((forall X1 : zenon_U, (((addition (domain X1) (forward_diamond X0 (domain X1))) = (forward_diamond X0 (domain X1)))->((domain X1) = (zero))))->((divergence X0) = (zero)))) zenon_G); [ zenon_intro zenon_H2c; idtac ]. % 27.55/27.77 elim zenon_H2c. zenon_intro zenon_TX0_bf. zenon_intro zenon_H2d. % 27.55/27.77 apply (zenon_notimply_s _ _ zenon_H2d). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 27.55/27.77 generalize (divergence1 zenon_TX0_bf). zenon_intro zenon_H30. % 27.55/27.77 generalize (forward_diamond zenon_TX0_bf). zenon_intro zenon_H31. % 27.55/27.77 generalize (zenon_H31 (divergence zenon_TX0_bf)). zenon_intro zenon_H32. % 27.55/27.77 apply (zenon_congruence_lr_s _ (fun zenon_Vg : _ => (zenon_Vg = (divergence zenon_TX0_bf))) _ _ zenon_H30 zenon_H32). zenon_intro zenon_H33. % 27.55/27.77 generalize (domain4 (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))). zenon_intro zenon_H2a. % 27.55/27.77 apply (zenon_congruence_lr_s _ (fun zenon_Vg : _ => (zenon_Vg = (divergence zenon_TX0_bf))) _ _ zenon_H33 zenon_H2a). zenon_intro zenon_H1e. % 27.55/27.77 elim (classic ((zero) = (zero))); [ zenon_intro zenon_H34 | zenon_intro zenon_H35 ]. % 27.55/27.77 cut (((zero) = (zero)) = ((divergence zenon_TX0_bf) = (zero))). % 27.55/27.77 intro zenon_D_pnotp. % 27.55/27.77 apply zenon_H2e. % 27.55/27.77 rewrite <- zenon_D_pnotp. % 27.55/27.77 exact zenon_H34. % 27.55/27.77 cut (((zero) = (zero))); [idtac | apply NNPP; zenon_intro zenon_H35]. % 27.55/27.77 cut (((zero) = (divergence zenon_TX0_bf))); [idtac | apply NNPP; zenon_intro zenon_H36]. % 27.55/27.77 congruence. % 27.55/27.77 cut (((antidomain (antidomain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))) = (divergence zenon_TX0_bf)) = ((zero) = (divergence zenon_TX0_bf))). % 27.55/27.77 intro zenon_D_pnotp. % 27.55/27.77 apply zenon_H36. % 27.55/27.77 rewrite <- zenon_D_pnotp. % 27.55/27.77 exact zenon_H1e. % 27.55/27.77 cut (((divergence zenon_TX0_bf) = (divergence zenon_TX0_bf))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 27.55/27.77 cut (((antidomain (antidomain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))) = (zero))); [idtac | apply NNPP; zenon_intro zenon_H38]. % 27.55/27.77 congruence. % 27.55/27.77 elim (classic ((zero) = (zero))); [ zenon_intro zenon_H34 | zenon_intro zenon_H35 ]. % 27.55/27.77 cut (((zero) = (zero)) = ((antidomain (antidomain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))) = (zero))). % 27.55/27.77 intro zenon_D_pnotp. % 27.55/27.77 apply zenon_H38. % 27.55/27.77 rewrite <- zenon_D_pnotp. % 27.55/27.77 exact zenon_H34. % 27.55/27.77 cut (((zero) = (zero))); [idtac | apply NNPP; zenon_intro zenon_H35]. % 27.55/27.77 cut (((zero) = (antidomain (antidomain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))); [idtac | apply NNPP; zenon_intro zenon_H39]. % 27.55/27.77 congruence. % 27.55/27.77 generalize (zenon_H2f (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))). zenon_intro zenon_H3a. % 27.55/27.77 apply (zenon_imply_s _ _ zenon_H3a); [ zenon_intro zenon_H3c | zenon_intro zenon_H3b ]. % 27.55/27.77 generalize (forward_diamond zenon_TX0_bf). zenon_intro zenon_H31. % 27.55/27.77 generalize (zenon_H31 (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))). zenon_intro zenon_H3d. % 27.55/27.77 apply (zenon_congruence_lr_s _ (fun zenon_Vk : _ => (~((addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))) = zenon_Vk))) _ _ zenon_H3c zenon_H3d). zenon_intro zenon_H3e. % 27.55/27.77 generalize (domain4 (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))). zenon_intro zenon_H3f. % 27.55/27.77 apply (zenon_congruence_lr_s _ (fun zenon_Vk : _ => (~((addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))) = zenon_Vk))) _ _ zenon_H3e zenon_H3f). zenon_intro zenon_H40. % 27.55/27.77 generalize (additive_idempotence (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))))). zenon_intro zenon_H41. % 27.55/27.77 cut (((addition (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))) (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))))) = (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))))) = ((addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))) = (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))))). % 27.55/27.77 intro zenon_D_pnotp. % 27.55/27.77 apply zenon_H40. % 27.55/27.77 rewrite <- zenon_D_pnotp. % 27.55/27.77 exact zenon_H41. % 27.55/27.77 cut (((antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))) = (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))))); [idtac | apply NNPP; zenon_intro zenon_H42]. % 27.55/27.77 cut (((addition (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))) (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))))) = (addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))); [idtac | apply NNPP; zenon_intro zenon_H43]. % 27.55/27.77 congruence. % 27.55/27.77 elim (classic ((addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))) = (addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))); [ zenon_intro zenon_H44 | zenon_intro zenon_H45 ]. % 27.55/27.77 cut (((addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))) = (addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))) = ((addition (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))) (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))))) = (addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))). % 27.55/27.77 intro zenon_D_pnotp. % 27.55/27.77 apply zenon_H43. % 27.55/27.77 rewrite <- zenon_D_pnotp. % 27.55/27.77 exact zenon_H44. % 27.55/27.77 cut (((addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))) = (addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))); [idtac | apply NNPP; zenon_intro zenon_H45]. % 27.55/27.77 cut (((addition (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) (forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))) = (addition (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))) (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))))))); [idtac | apply NNPP; zenon_intro zenon_H46]. % 27.55/27.77 congruence. % 27.55/27.77 cut (((forward_diamond zenon_TX0_bf (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))) = (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))))); [idtac | apply NNPP; zenon_intro zenon_H47]. % 27.55/27.77 cut (((domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))) = (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))))))))); [idtac | apply NNPP; zenon_intro zenon_H48]. % 27.55/27.77 congruence. % 27.55/27.77 generalize (domain4 (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))). zenon_intro zenon_H2a. % 27.55/27.77 apply (zenon_congruence_lr_s _ (fun zenon_Vo : _ => (~(zenon_Vo = (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))))))) _ _ zenon_H48 zenon_H2a). zenon_intro zenon_H1d. % 27.55/27.77 apply (zenon_L1_ zenon_TX0_bf); trivial. % 27.55/27.77 generalize (forward_diamond zenon_TX0_bf). zenon_intro zenon_H31. % 27.55/27.77 generalize (zenon_H31 (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))). zenon_intro zenon_H3d. % 27.55/27.77 apply (zenon_congruence_lr_s _ (fun zenon_Vo : _ => (~(zenon_Vo = (antidomain (antidomain (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))))))) _ _ zenon_H47 zenon_H3d). zenon_intro zenon_H49. % 27.55/27.77 generalize (domain4 (multiplication zenon_TX0_bf (domain (domain (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf))))))). zenon_intro zenon_H3f. % 27.55/27.79 exact (zenon_H49 zenon_H3f). % 27.55/27.79 apply zenon_H45. apply refl_equal. % 27.55/27.79 apply zenon_H45. apply refl_equal. % 27.55/27.79 apply zenon_H42. apply refl_equal. % 27.55/27.79 generalize (domain4 (multiplication zenon_TX0_bf (domain (divergence zenon_TX0_bf)))). zenon_intro zenon_H2a. % 27.55/27.79 apply (zenon_congruence_lr_s _ (fun zenon_Vz : _ => (zenon_Vz = (zero))) _ _ zenon_H3b zenon_H2a). zenon_intro zenon_H4a. % 27.55/27.79 apply zenon_H39. apply sym_equal. exact zenon_H4a. % 27.55/27.79 apply zenon_H35. apply refl_equal. % 27.55/27.79 apply zenon_H35. apply refl_equal. % 27.55/27.79 apply zenon_H37. apply refl_equal. % 27.55/27.79 apply zenon_H35. apply refl_equal. % 27.55/27.79 apply zenon_H35. apply refl_equal. % 27.55/27.79 Qed. % 27.55/27.79 % SZS output end Proof % 27.55/27.79 (* END-PROOF *) % 27.55/27.79 nodes searched: 53051 % 27.55/27.79 max branch formulas: 5274 % 27.55/27.79 proof nodes created: 2153 % 27.55/27.79 formulas created: 614523 % 27.55/27.79 %------------------------------------------------------------------------------