%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV156+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n021.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 : Wed Jul 20 23:03:08 EDT 2022 % Result : Theorem 6.15s 6.35s % Output : Proof 6.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SWV156+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.04/0.14 % Command : run_zenon %s %d % 0.14/0.35 % Computer : n021.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Wed Jun 15 06:55:13 EDT 2022 % 0.14/0.35 % CPUTime : % 6.15/6.35 (* PROOF-FOUND *) % 6.15/6.35 % SZS status Theorem % 6.15/6.35 (* BEGIN-PROOF *) % 6.15/6.35 % SZS output start Proof % 6.15/6.35 Theorem cl5_nebula_norm_0006 : ((((pv70) = (sum (n0) (n4) (sqrt (times (minus (a_select3 (center) (tptp_sum_index) (n0)) (a_select2 (x) (pv10))) (minus (a_select3 (center) (tptp_sum_index) (n0)) (a_select2 (x) (pv10)))))))/\((leq (n0) (pv10))/\((leq (n0) (pv12))/\((leq (pv10) (n135299))/\((leq (pv12) (n4))/\((forall A : zenon_U, (((leq (n0) A)/\(leq A (pred (pv12))))->((a_select3 (q) (pv10) A) = (divide (sqrt (times (minus (a_select3 (center) A (n0)) (a_select2 (x) (pv10))) (minus (a_select3 (center) A (n0)) (a_select2 (x) (pv10))))) (sum (n0) (n4) (sqrt (times (minus (a_select3 (center) (tptp_sum_index) (n0)) (a_select2 (x) (pv10))) (minus (a_select3 (center) (tptp_sum_index) (n0)) (a_select2 (x) (pv10))))))))))/\(forall B : zenon_U, (((leq (n0) B)/\(leq B (pred (pv10))))->((sum (n0) (n4) (a_select3 (q) B (tptp_sum_index))) = (n1))))))))))->(forall C : zenon_U, (((leq (n0) C)/\(leq C (pred (pv10))))->(((pv10) = C)->((sum (n0) (n4) (cond (tptp_term_equals (pv12) (tptp_sum_index)) (divide (sqrt (times (minus (a_select3 (center) (pv12) (n0)) (a_select2 (x) (pv10))) (minus (a_select3 (center) (pv12) (n0)) (a_select2 (x) (pv10))))) (pv70)) (a_select3 (q) C (tptp_sum_index)))) = (n1)))))). % 6.15/6.35 Proof. % 6.15/6.35 assert (zenon_L1_ : (~((pv10) = (pv10))) -> False). % 6.15/6.35 do 0 intro. intros zenon_H5c. % 6.15/6.35 apply zenon_H5c. apply refl_equal. % 6.15/6.35 (* end of lemma zenon_L1_ *) % 6.15/6.35 assert (zenon_L2_ : (~((pv10) = (succ (pred (pv10))))) -> False). % 6.15/6.35 do 0 intro. intros zenon_H5d. % 6.15/6.35 generalize (succ_pred (pv10)). zenon_intro zenon_H5e. % 6.15/6.35 apply zenon_H5d. apply sym_equal. exact zenon_H5e. % 6.15/6.35 (* end of lemma zenon_L2_ *) % 6.15/6.35 assert (zenon_L3_ : forall (zenon_TC_dv : zenon_U), (gt (succ (pred (pv10))) zenon_TC_dv) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z)))))) -> (~(gt zenon_TC_dv zenon_TC_dv)) -> ((pv10) = zenon_TC_dv) -> False). % 6.15/6.35 do 1 intro. intros zenon_H5f zenon_H60 zenon_H61 zenon_H62. % 6.15/6.35 elim (classic (zenon_TC_dv = (pv10))); [ zenon_intro zenon_H64 | zenon_intro zenon_H65 ]. % 6.15/6.35 elim (classic (gt (pv10) zenon_TC_dv)); [ zenon_intro zenon_H66 | zenon_intro zenon_H67 ]. % 6.15/6.35 cut ((gt (pv10) zenon_TC_dv) = (gt zenon_TC_dv zenon_TC_dv)). % 6.15/6.35 intro zenon_D_pnotp. % 6.15/6.35 apply zenon_H61. % 6.15/6.35 rewrite <- zenon_D_pnotp. % 6.15/6.35 exact zenon_H66. % 6.15/6.35 cut ((zenon_TC_dv = zenon_TC_dv)); [idtac | apply NNPP; zenon_intro zenon_H68]. % 6.15/6.35 cut (((pv10) = zenon_TC_dv)); [idtac | apply NNPP; zenon_intro zenon_H69]. % 6.15/6.35 congruence. % 6.15/6.35 elim (classic (zenon_TC_dv = zenon_TC_dv)); [ zenon_intro zenon_H6a | zenon_intro zenon_H68 ]. % 6.15/6.35 cut ((zenon_TC_dv = zenon_TC_dv) = ((pv10) = zenon_TC_dv)). % 6.15/6.35 intro zenon_D_pnotp. % 6.15/6.35 apply zenon_H69. % 6.15/6.35 rewrite <- zenon_D_pnotp. % 6.15/6.35 exact zenon_H6a. % 6.15/6.35 cut ((zenon_TC_dv = zenon_TC_dv)); [idtac | apply NNPP; zenon_intro zenon_H68]. % 6.15/6.35 cut ((zenon_TC_dv = (pv10))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 6.15/6.35 congruence. % 6.15/6.35 exact (zenon_H65 zenon_H64). % 6.15/6.35 apply zenon_H68. apply refl_equal. % 6.15/6.35 apply zenon_H68. apply refl_equal. % 6.15/6.35 apply zenon_H68. apply refl_equal. % 6.15/6.35 elim (classic ((~((pv10) = (succ (pred (pv10)))))/\(~(gt (pv10) (succ (pred (pv10))))))); [ zenon_intro zenon_H6b | zenon_intro zenon_H6c ]. % 6.15/6.35 apply (zenon_and_s _ _ zenon_H6b). zenon_intro zenon_H5d. zenon_intro zenon_H6d. % 6.15/6.35 apply (zenon_L2_); trivial. % 6.15/6.35 cut ((gt (succ (pred (pv10))) zenon_TC_dv) = (gt (pv10) zenon_TC_dv)). % 6.15/6.35 intro zenon_D_pnotp. % 6.15/6.35 apply zenon_H67. % 6.15/6.35 rewrite <- zenon_D_pnotp. % 6.15/6.35 exact zenon_H5f. % 6.15/6.35 cut ((zenon_TC_dv = zenon_TC_dv)); [idtac | apply NNPP; zenon_intro zenon_H68]. % 6.15/6.35 cut (((succ (pred (pv10))) = (pv10))); [idtac | apply NNPP; zenon_intro zenon_H6e]. % 6.15/6.35 congruence. % 6.15/6.35 apply (zenon_notand_s _ _ zenon_H6c); [ zenon_intro zenon_H70 | zenon_intro zenon_H6f ]. % 6.15/6.35 apply zenon_H70. zenon_intro zenon_H71. % 6.15/6.35 elim (classic ((pv10) = (pv10))); [ zenon_intro zenon_H72 | zenon_intro zenon_H5c ]. % 6.15/6.35 cut (((pv10) = (pv10)) = ((succ (pred (pv10))) = (pv10))). % 6.15/6.35 intro zenon_D_pnotp. % 6.15/6.35 apply zenon_H6e. % 6.15/6.35 rewrite <- zenon_D_pnotp. % 6.15/6.35 exact zenon_H72. % 6.15/6.35 cut (((pv10) = (pv10))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 6.15/6.35 cut (((pv10) = (succ (pred (pv10))))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 6.15/6.35 congruence. % 6.15/6.35 exact (zenon_H5d zenon_H71). % 6.15/6.35 apply zenon_H5c. apply refl_equal. % 6.15/6.35 apply zenon_H5c. apply refl_equal. % 6.15/6.35 apply zenon_H6f. zenon_intro zenon_H73. % 6.15/6.35 generalize (zenon_H60 (pv10)). zenon_intro zenon_H74. % 6.15/6.35 generalize (zenon_H74 (succ (pred (pv10)))). zenon_intro zenon_H75. % 6.15/6.35 generalize (zenon_H75 zenon_TC_dv). zenon_intro zenon_H76. % 6.15/6.35 apply (zenon_imply_s _ _ zenon_H76); [ zenon_intro zenon_H6d | zenon_intro zenon_H77 ]. % 6.15/6.35 exact (zenon_H6d zenon_H73). % 6.15/6.35 apply (zenon_imply_s _ _ zenon_H77); [ zenon_intro zenon_H78 | zenon_intro zenon_H66 ]. % 6.15/6.35 exact (zenon_H78 zenon_H5f). % 6.15/6.35 exact (zenon_H67 zenon_H66). % 6.15/6.35 apply zenon_H68. apply refl_equal. % 6.15/6.35 elim (classic ((pv10) = (pv10))); [ zenon_intro zenon_H72 | zenon_intro zenon_H5c ]. % 6.15/6.35 cut (((pv10) = (pv10)) = (zenon_TC_dv = (pv10))). % 6.15/6.35 intro zenon_D_pnotp. % 6.15/6.35 apply zenon_H65. % 6.15/6.35 rewrite <- zenon_D_pnotp. % 6.15/6.35 exact zenon_H72. % 6.15/6.35 cut (((pv10) = (pv10))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 6.15/6.35 cut (((pv10) = zenon_TC_dv)); [idtac | apply NNPP; zenon_intro zenon_H69]. % 6.15/6.35 congruence. % 6.15/6.35 exact (zenon_H69 zenon_H62). % 6.15/6.35 apply zenon_H5c. apply refl_equal. % 6.15/6.35 apply zenon_H5c. apply refl_equal. % 6.15/6.35 (* end of lemma zenon_L3_ *) % 6.15/6.35 assert (zenon_L4_ : forall (zenon_TC_dv : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z)))))) -> (~(gt (pv10) (pv10))) -> (gt (succ (pred (pv10))) zenon_TC_dv) -> ((pv10) = zenon_TC_dv) -> False). % 6.15/6.35 do 1 intro. intros zenon_H60 zenon_H79 zenon_H5f zenon_H62. % 6.15/6.35 elim (classic (gt zenon_TC_dv (pv10))); [ zenon_intro zenon_H7a | zenon_intro zenon_H7b ]. % 6.15/6.35 cut ((gt zenon_TC_dv (pv10)) = (gt (pv10) (pv10))). % 6.15/6.35 intro zenon_D_pnotp. % 6.15/6.35 apply zenon_H79. % 6.15/6.35 rewrite <- zenon_D_pnotp. % 6.15/6.35 exact zenon_H7a. % 6.15/6.35 cut (((pv10) = (pv10))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 6.15/6.35 cut ((zenon_TC_dv = (pv10))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 6.15/6.35 congruence. % 6.15/6.35 elim (classic ((pv10) = (pv10))); [ zenon_intro zenon_H72 | zenon_intro zenon_H5c ]. % 6.15/6.35 cut (((pv10) = (pv10)) = (zenon_TC_dv = (pv10))). % 6.15/6.35 intro zenon_D_pnotp. % 6.15/6.35 apply zenon_H65. % 6.15/6.35 rewrite <- zenon_D_pnotp. % 6.15/6.35 exact zenon_H72. % 6.15/6.35 cut (((pv10) = (pv10))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 6.15/6.35 cut (((pv10) = zenon_TC_dv)); [idtac | apply NNPP; zenon_intro zenon_H69]. % 6.15/6.35 congruence. % 6.15/6.35 exact (zenon_H69 zenon_H62). % 6.15/6.35 apply zenon_H5c. apply refl_equal. % 6.15/6.35 apply zenon_H5c. apply refl_equal. % 6.15/6.35 apply zenon_H5c. apply refl_equal. % 6.15/6.35 elim (classic (zenon_TC_dv = (pv10))); [ zenon_intro zenon_H64 | zenon_intro zenon_H65 ]. % 6.15/6.35 elim (classic (gt zenon_TC_dv zenon_TC_dv)); [ zenon_intro zenon_H7c | zenon_intro zenon_H61 ]. % 6.15/6.35 cut ((gt zenon_TC_dv zenon_TC_dv) = (gt zenon_TC_dv (pv10))). % 6.15/6.35 intro zenon_D_pnotp. % 6.15/6.35 apply zenon_H7b. % 6.15/6.35 rewrite <- zenon_D_pnotp. % 6.15/6.35 exact zenon_H7c. % 6.15/6.35 cut ((zenon_TC_dv = (pv10))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 6.15/6.35 cut ((zenon_TC_dv = zenon_TC_dv)); [idtac | apply NNPP; zenon_intro zenon_H68]. % 6.15/6.35 congruence. % 6.15/6.35 apply zenon_H68. apply refl_equal. % 6.15/6.35 exact (zenon_H65 zenon_H64). % 6.15/6.35 apply (zenon_L3_ zenon_TC_dv); trivial. % 6.15/6.35 elim (classic ((pv10) = (pv10))); [ zenon_intro zenon_H72 | zenon_intro zenon_H5c ]. % 6.15/6.35 cut (((pv10) = (pv10)) = (zenon_TC_dv = (pv10))). % 6.15/6.35 intro zenon_D_pnotp. % 6.15/6.35 apply zenon_H65. % 6.15/6.35 rewrite <- zenon_D_pnotp. % 6.15/6.35 exact zenon_H72. % 6.15/6.35 cut (((pv10) = (pv10))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 6.15/6.35 cut (((pv10) = zenon_TC_dv)); [idtac | apply NNPP; zenon_intro zenon_H69]. % 6.15/6.35 congruence. % 6.15/6.35 exact (zenon_H69 zenon_H62). % 6.15/6.35 apply zenon_H5c. apply refl_equal. % 6.15/6.35 apply zenon_H5c. apply refl_equal. % 6.15/6.35 (* end of lemma zenon_L4_ *) % 6.15/6.35 apply NNPP. intro zenon_G. % 6.15/6.35 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z))))))); [ zenon_intro zenon_H60 | zenon_intro zenon_H7d ]. % 6.15/6.35 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H7f. zenon_intro zenon_H7e. % 6.15/6.35 apply (zenon_notallex_s (fun C : zenon_U => (((leq (n0) C)/\(leq C (pred (pv10))))->(((pv10) = C)->((sum (n0) (n4) (cond (tptp_term_equals (pv12) (tptp_sum_index)) (divide (sqrt (times (minus (a_select3 (center) (pv12) (n0)) (a_select2 (x) (pv10))) (minus (a_select3 (center) (pv12) (n0)) (a_select2 (x) (pv10))))) (pv70)) (a_select3 (q) C (tptp_sum_index)))) = (n1))))) zenon_H7e); [ zenon_intro zenon_H80; idtac ]. % 6.15/6.35 elim zenon_H80. zenon_intro zenon_TC_dv. zenon_intro zenon_H81. % 6.15/6.35 apply (zenon_notimply_s _ _ zenon_H81). zenon_intro zenon_H83. zenon_intro zenon_H82. % 6.15/6.35 apply (zenon_notimply_s _ _ zenon_H82). zenon_intro zenon_H62. zenon_intro zenon_H84. % 6.15/6.35 apply (zenon_and_s _ _ zenon_H83). zenon_intro zenon_H86. zenon_intro zenon_H85. % 6.15/6.35 generalize (leq_succ_gt_equiv zenon_TC_dv). zenon_intro zenon_H87. % 6.15/6.35 generalize (zenon_H87 (pred (pv10))). zenon_intro zenon_H88. % 6.15/6.35 apply (zenon_equiv_s _ _ zenon_H88); [ zenon_intro zenon_H89; zenon_intro zenon_H78 | zenon_intro zenon_H85; zenon_intro zenon_H5f ]. % 6.15/6.35 exact (zenon_H89 zenon_H85). % 6.15/6.35 generalize (irreflexivity_gt (pv10)). zenon_intro zenon_H79. % 6.15/6.35 apply (zenon_L4_ zenon_TC_dv); trivial. % 6.15/6.35 apply zenon_H7d. zenon_intro zenon_Tx_fi. apply NNPP. zenon_intro zenon_H8b. % 6.15/6.35 apply zenon_H8b. zenon_intro zenon_Ty_fk. apply NNPP. zenon_intro zenon_H8d. % 6.15/6.35 apply zenon_H8d. zenon_intro zenon_Tz_fm. apply NNPP. zenon_intro zenon_H8f. % 6.15/6.35 apply (zenon_notimply_s _ _ zenon_H8f). zenon_intro zenon_H91. zenon_intro zenon_H90. % 6.15/6.35 apply (zenon_notimply_s _ _ zenon_H90). zenon_intro zenon_H93. zenon_intro zenon_H92. % 6.15/6.35 generalize (transitivity_gt zenon_Tx_fi). zenon_intro zenon_H94. % 6.15/6.35 generalize (zenon_H94 zenon_Ty_fk). zenon_intro zenon_H95. % 6.15/6.35 generalize (zenon_H95 zenon_Tz_fm). zenon_intro zenon_H96. % 6.15/6.35 apply (zenon_imply_s _ _ zenon_H96); [ zenon_intro zenon_H98 | zenon_intro zenon_H97 ]. % 6.15/6.35 apply (zenon_notand_s _ _ zenon_H98); [ zenon_intro zenon_H9a | zenon_intro zenon_H99 ]. % 6.15/6.35 exact (zenon_H9a zenon_H91). % 6.15/6.35 exact (zenon_H99 zenon_H93). % 6.15/6.35 exact (zenon_H92 zenon_H97). % 6.15/6.35 Qed. % 6.15/6.35 % SZS output end Proof % 6.15/6.35 (* END-PROOF *) % 6.15/6.35 nodes searched: 371304 % 6.15/6.35 max branch formulas: 8830 % 6.15/6.35 proof nodes created: 1347 % 6.15/6.35 formulas created: 190305 % 6.15/6.35 %------------------------------------------------------------------------------