%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV158+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n010.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:09 EDT 2022 % Result : Theorem 0.43s 0.62s % Output : Proof 0.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV158+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.12/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n010.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Wed Jun 15 02:37:24 EDT 2022 % 0.12/0.34 % CPUTime : % 0.43/0.62 (* PROOF-FOUND *) % 0.43/0.62 % SZS status Theorem % 0.43/0.62 (* BEGIN-PROOF *) % 0.43/0.62 % SZS output start Proof % 0.43/0.62 Theorem cl5_nebula_norm_0008 : ((((pv84) = (sum (n0) (n4) (divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (tptp_sum_index))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (tptp_sum_index)))) (tptp_minus_2)) (times (a_select2 (sigma) (tptp_sum_index)) (a_select2 (sigma) (tptp_sum_index))))) (a_select2 (rho) (tptp_sum_index))) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) (tptp_sum_index))))))/\((leq (n0) (pv10))/\((leq (n0) (pv47))/\((leq (pv10) (n135299))/\((leq (pv47) (n4))/\((forall A : zenon_U, (((leq (n0) A)/\(leq A (pred (pv47))))->((a_select3 (q) (pv10) A) = (divide (divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) A)) (minus (a_select2 (x) (pv10)) (a_select2 (mu) A))) (tptp_minus_2)) (times (a_select2 (sigma) A) (a_select2 (sigma) A)))) (a_select2 (rho) A)) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) A))) (sum (n0) (n4) (divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (tptp_sum_index))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (tptp_sum_index)))) (tptp_minus_2)) (times (a_select2 (sigma) (tptp_sum_index)) (a_select2 (sigma) (tptp_sum_index))))) (a_select2 (rho) (tptp_sum_index))) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) (tptp_sum_index)))))))))/\(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 (pv47)))->(((pv47) = C)->((divide (divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47)))) (tptp_minus_2)) (times (a_select2 (sigma) (pv47)) (a_select2 (sigma) (pv47))))) (a_select2 (rho) (pv47))) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) (pv47)))) (pv84)) = (divide (divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) C)) (minus (a_select2 (x) (pv10)) (a_select2 (mu) C))) (tptp_minus_2)) (times (a_select2 (sigma) C) (a_select2 (sigma) C)))) (a_select2 (rho) C)) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) C))) (sum (n0) (n4) (divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (tptp_sum_index))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (tptp_sum_index)))) (tptp_minus_2)) (times (a_select2 (sigma) (tptp_sum_index)) (a_select2 (sigma) (tptp_sum_index))))) (a_select2 (rho) (tptp_sum_index))) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) (tptp_sum_index))))))))))). % 0.43/0.62 Proof. % 0.43/0.62 assert (zenon_L1_ : forall (zenon_TC_dy : zenon_U), (~((minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47))) = (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy)))) -> ((pv47) = zenon_TC_dy) -> False). % 0.43/0.62 do 1 intro. intros zenon_H64 zenon_H65. % 0.43/0.62 cut (((a_select2 (mu) (pv47)) = (a_select2 (mu) zenon_TC_dy))); [idtac | apply NNPP; zenon_intro zenon_H67]. % 0.43/0.62 cut (((a_select2 (x) (pv10)) = (a_select2 (x) (pv10)))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 0.43/0.62 congruence. % 0.43/0.62 apply zenon_H68. apply refl_equal. % 0.43/0.62 cut (((pv47) = zenon_TC_dy)); [idtac | apply NNPP; zenon_intro zenon_H69]. % 0.43/0.62 cut (((mu) = (mu))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 0.43/0.62 congruence. % 0.43/0.62 apply zenon_H6a. apply refl_equal. % 0.43/0.62 exact (zenon_H69 zenon_H65). % 0.43/0.62 (* end of lemma zenon_L1_ *) % 0.43/0.62 assert (zenon_L2_ : forall (zenon_TC_dy : zenon_U), (~((a_select2 (sigma) (pv47)) = (a_select2 (sigma) zenon_TC_dy))) -> ((pv47) = zenon_TC_dy) -> False). % 0.43/0.62 do 1 intro. intros zenon_H6b zenon_H65. % 0.43/0.62 cut (((pv47) = zenon_TC_dy)); [idtac | apply NNPP; zenon_intro zenon_H69]. % 0.43/0.62 cut (((sigma) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_H6c]. % 0.43/0.62 congruence. % 0.43/0.62 apply zenon_H6c. apply refl_equal. % 0.43/0.62 exact (zenon_H69 zenon_H65). % 0.43/0.62 (* end of lemma zenon_L2_ *) % 0.43/0.62 apply NNPP. intro zenon_G. % 0.43/0.62 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 0.43/0.62 apply (zenon_and_s _ _ zenon_H6e). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 0.43/0.62 apply (zenon_notallex_s (fun C : zenon_U => (((leq (n0) C)/\(leq C (pv47)))->(((pv47) = C)->((divide (divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47)))) (tptp_minus_2)) (times (a_select2 (sigma) (pv47)) (a_select2 (sigma) (pv47))))) (a_select2 (rho) (pv47))) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) (pv47)))) (pv84)) = (divide (divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) C)) (minus (a_select2 (x) (pv10)) (a_select2 (mu) C))) (tptp_minus_2)) (times (a_select2 (sigma) C) (a_select2 (sigma) C)))) (a_select2 (rho) C)) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) C))) (sum (n0) (n4) (divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (tptp_sum_index))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (tptp_sum_index)))) (tptp_minus_2)) (times (a_select2 (sigma) (tptp_sum_index)) (a_select2 (sigma) (tptp_sum_index))))) (a_select2 (rho) (tptp_sum_index))) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) (tptp_sum_index)))))))))) zenon_H6d); [ zenon_intro zenon_H71; idtac ]. % 0.43/0.62 elim zenon_H71. zenon_intro zenon_TC_dy. zenon_intro zenon_H72. % 0.43/0.62 apply (zenon_notimply_s _ _ zenon_H72). zenon_intro zenon_H74. zenon_intro zenon_H73. % 0.43/0.62 apply (zenon_notimply_s _ _ zenon_H73). zenon_intro zenon_H65. zenon_intro zenon_H75. % 0.43/0.62 cut (((pv84) = (sum (n0) (n4) (divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (tptp_sum_index))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (tptp_sum_index)))) (tptp_minus_2)) (times (a_select2 (sigma) (tptp_sum_index)) (a_select2 (sigma) (tptp_sum_index))))) (a_select2 (rho) (tptp_sum_index))) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) (tptp_sum_index))))))); [idtac | apply NNPP; zenon_intro zenon_H76]. % 0.43/0.62 cut (((divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47)))) (tptp_minus_2)) (times (a_select2 (sigma) (pv47)) (a_select2 (sigma) (pv47))))) (a_select2 (rho) (pv47))) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) (pv47)))) = (divide (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy)) (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy))) (tptp_minus_2)) (times (a_select2 (sigma) zenon_TC_dy) (a_select2 (sigma) zenon_TC_dy)))) (a_select2 (rho) zenon_TC_dy)) (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) zenon_TC_dy))))); [idtac | apply NNPP; zenon_intro zenon_H77]. % 0.43/0.62 congruence. % 0.43/0.62 cut (((times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) (pv47))) = (times (sqrt (times (n2) (tptp_pi))) (a_select2 (sigma) zenon_TC_dy)))); [idtac | apply NNPP; zenon_intro zenon_H78]. % 0.43/0.62 cut (((times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47)))) (tptp_minus_2)) (times (a_select2 (sigma) (pv47)) (a_select2 (sigma) (pv47))))) (a_select2 (rho) (pv47))) = (times (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy)) (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy))) (tptp_minus_2)) (times (a_select2 (sigma) zenon_TC_dy) (a_select2 (sigma) zenon_TC_dy)))) (a_select2 (rho) zenon_TC_dy)))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 0.43/0.62 congruence. % 0.43/0.62 cut (((a_select2 (rho) (pv47)) = (a_select2 (rho) zenon_TC_dy))); [idtac | apply NNPP; zenon_intro zenon_H7a]. % 0.43/0.62 cut (((exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47)))) (tptp_minus_2)) (times (a_select2 (sigma) (pv47)) (a_select2 (sigma) (pv47))))) = (exp (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy)) (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy))) (tptp_minus_2)) (times (a_select2 (sigma) zenon_TC_dy) (a_select2 (sigma) zenon_TC_dy)))))); [idtac | apply NNPP; zenon_intro zenon_H7b]. % 0.43/0.62 congruence. % 0.43/0.62 cut (((divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47)))) (tptp_minus_2)) (times (a_select2 (sigma) (pv47)) (a_select2 (sigma) (pv47)))) = (divide (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy)) (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy))) (tptp_minus_2)) (times (a_select2 (sigma) zenon_TC_dy) (a_select2 (sigma) zenon_TC_dy))))); [idtac | apply NNPP; zenon_intro zenon_H7c]. % 0.43/0.62 congruence. % 0.43/0.62 cut (((times (a_select2 (sigma) (pv47)) (a_select2 (sigma) (pv47))) = (times (a_select2 (sigma) zenon_TC_dy) (a_select2 (sigma) zenon_TC_dy)))); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 0.43/0.62 cut (((divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47)))) (tptp_minus_2)) = (divide (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy)) (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy))) (tptp_minus_2)))); [idtac | apply NNPP; zenon_intro zenon_H7e]. % 0.43/0.62 congruence. % 0.43/0.62 cut (((tptp_minus_2) = (tptp_minus_2))); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 0.43/0.62 cut (((times (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47))) (minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47)))) = (times (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy)) (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy))))); [idtac | apply NNPP; zenon_intro zenon_H80]. % 0.43/0.62 congruence. % 0.43/0.62 cut (((minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47))) = (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 0.43/0.62 cut (((minus (a_select2 (x) (pv10)) (a_select2 (mu) (pv47))) = (minus (a_select2 (x) (pv10)) (a_select2 (mu) zenon_TC_dy)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_L1_ zenon_TC_dy); trivial. % 0.43/0.62 apply (zenon_L1_ zenon_TC_dy); trivial. % 0.43/0.62 apply zenon_H7f. apply refl_equal. % 0.43/0.62 cut (((a_select2 (sigma) (pv47)) = (a_select2 (sigma) zenon_TC_dy))); [idtac | apply NNPP; zenon_intro zenon_H6b]. % 0.43/0.62 cut (((a_select2 (sigma) (pv47)) = (a_select2 (sigma) zenon_TC_dy))); [idtac | apply NNPP; zenon_intro zenon_H6b]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_L2_ zenon_TC_dy); trivial. % 0.43/0.62 apply (zenon_L2_ zenon_TC_dy); trivial. % 0.43/0.62 cut (((pv47) = zenon_TC_dy)); [idtac | apply NNPP; zenon_intro zenon_H69]. % 0.43/0.62 cut (((rho) = (rho))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 0.43/0.62 congruence. % 0.43/0.62 apply zenon_H81. apply refl_equal. % 0.43/0.62 exact (zenon_H69 zenon_H65). % 0.43/0.62 cut (((a_select2 (sigma) (pv47)) = (a_select2 (sigma) zenon_TC_dy))); [idtac | apply NNPP; zenon_intro zenon_H6b]. % 0.43/0.62 cut (((sqrt (times (n2) (tptp_pi))) = (sqrt (times (n2) (tptp_pi))))); [idtac | apply NNPP; zenon_intro zenon_H82]. % 0.43/0.62 congruence. % 0.43/0.62 apply zenon_H82. apply refl_equal. % 0.43/0.62 apply (zenon_L2_ zenon_TC_dy); trivial. % 0.43/0.62 exact (zenon_H76 zenon_H70). % 0.43/0.62 Qed. % 0.43/0.62 % SZS output end Proof % 0.43/0.62 (* END-PROOF *) % 0.43/0.62 nodes searched: 4435 % 0.43/0.62 max branch formulas: 936 % 0.43/0.62 proof nodes created: 28 % 0.43/0.62 formulas created: 14895 % 0.43/0.62 %------------------------------------------------------------------------------