%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV094+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n016.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:02:56 EDT 2022 % Result : Theorem 0.18s 0.52s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV094+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.11/0.12 % Command : run_zenon %s %d % 0.11/0.33 % Computer : n016.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Wed Jun 15 16:46:17 EDT 2022 % 0.11/0.33 % CPUTime : % 0.18/0.52 (* PROOF-FOUND *) % 0.18/0.52 % SZS status Theorem % 0.18/0.52 (* BEGIN-PROOF *) % 0.18/0.52 % SZS output start Proof % 0.18/0.52 Theorem quaternion_ds1_inuse_0006 : ((((a_select2 (rho_defuse) (n0)) = (use))/\(((a_select2 (rho_defuse) (n1)) = (use))/\(((a_select2 (rho_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n0)) = (use))/\(((a_select2 (sigma_defuse) (n1)) = (use))/\(((a_select2 (sigma_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n3)) = (use))/\(((a_select2 (sigma_defuse) (n4)) = (use))/\(((a_select2 (sigma_defuse) (n5)) = (use))/\(((a_select3 (u_defuse) (n0) (n0)) = (use))/\(((a_select3 (u_defuse) (n1) (n0)) = (use))/\(((a_select3 (u_defuse) (n2) (n0)) = (use))/\(((a_select2 (xinit_defuse) (n3)) = (use))/\(((a_select2 (xinit_defuse) (n4)) = (use))/\(((a_select2 (xinit_defuse) (n5)) = (use))/\(((a_select2 (xinit_mean_defuse) (n0)) = (use))/\(((a_select2 (xinit_mean_defuse) (n1)) = (use))/\(((a_select2 (xinit_mean_defuse) (n2)) = (use))/\(((a_select2 (xinit_mean_defuse) (n3)) = (use))/\(((a_select2 (xinit_mean_defuse) (n4)) = (use))/\(((a_select2 (xinit_mean_defuse) (n5)) = (use))/\(((a_select2 (xinit_noise_defuse) (n0)) = (use))/\(((a_select2 (xinit_noise_defuse) (n1)) = (use))/\(((a_select2 (xinit_noise_defuse) (n2)) = (use))/\(((a_select2 (xinit_noise_defuse) (n3)) = (use))/\(((a_select2 (xinit_noise_defuse) (n4)) = (use))/\(((a_select2 (xinit_noise_defuse) (n5)) = (use))/\((leq (n0) (pv5))/\((leq (n0) (pv51))/\((leq (n0) (pv52))/\((leq (pv5) (minus (n999) (n1)))/\((leq (pv51) (minus (n6) (n1)))/\((leq (pv52) (minus (n6) (n1)))/\(forall A : zenon_U, (forall B : zenon_U, (((leq (n0) A)/\((leq (n0) B)/\((leq A (n2))/\(leq B (minus (pv5) (n1))))))->(((a_select3 (u_defuse) A B) = (use))/\((a_select3 (z_defuse) A B) = (use)))))))))))))))))))))))))))))))))))))))->(((~((pv51) = (pv52)))->(((a_select2 (rho_defuse) (n0)) = (use))/\(((a_select2 (rho_defuse) (n1)) = (use))/\(((a_select2 (rho_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n0)) = (use))/\(((a_select2 (sigma_defuse) (n1)) = (use))/\(((a_select2 (sigma_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n3)) = (use))/\(((a_select2 (sigma_defuse) (n4)) = (use))/\(((a_select2 (sigma_defuse) (n5)) = (use))/\(((a_select3 (u_defuse) (n0) (n0)) = (use))/\(((a_select3 (u_defuse) (n1) (n0)) = (use))/\(((a_select3 (u_defuse) (n2) (n0)) = (use))/\(((a_select2 (xinit_defuse) (n3)) = (use))/\(((a_select2 (xinit_defuse) (n4)) = (use))/\(((a_select2 (xinit_defuse) (n5)) = (use))/\(((a_select2 (xinit_mean_defuse) (n0)) = (use))/\(((a_select2 (xinit_mean_defuse) (n1)) = (use))/\(((a_select2 (xinit_mean_defuse) (n2)) = (use))/\(((a_select2 (xinit_mean_defuse) (n3)) = (use))/\(((a_select2 (xinit_mean_defuse) (n4)) = (use))/\(((a_select2 (xinit_mean_defuse) (n5)) = (use))/\(((a_select2 (xinit_noise_defuse) (n0)) = (use))/\(((a_select2 (xinit_noise_defuse) (n1)) = (use))/\(((a_select2 (xinit_noise_defuse) (n2)) = (use))/\(((a_select2 (xinit_noise_defuse) (n3)) = (use))/\(((a_select2 (xinit_noise_defuse) (n4)) = (use))/\(((a_select2 (xinit_noise_defuse) (n5)) = (use))/\((leq (n0) (pv5))/\((leq (n0) (pv51))/\((leq (pv5) (minus (n999) (n1)))/\((leq (pv51) (minus (n6) (n1)))/\(forall A : zenon_U, (forall B : zenon_U, (((leq (n0) A)/\((leq (n0) B)/\((leq A (n2))/\(leq B (minus (pv5) (n1))))))->(((a_select3 (u_defuse) A B) = (use))/\((a_select3 (z_defuse) A B) = (use))))))))))))))))))))))))))))))))))))))/\(((pv51) = (pv52))->(((a_select2 (rho_defuse) (n0)) = (use))/\(((a_select2 (rho_defuse) (n1)) = (use))/\(((a_select2 (rho_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n0)) = (use))/\(((a_select2 (sigma_defuse) (n1)) = (use))/\(((a_select2 (sigma_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n3)) = (use))/\(((a_select2 (sigma_defuse) (n4)) = (use))/\(((a_select2 (sigma_defuse) (n5)) = (use))/\(((a_select3 (u_defuse) (n0) (n0)) = (use))/\(((a_select3 (u_defuse) (n1) (n0)) = (use))/\(((a_select3 (u_defuse) (n2) (n0)) = (use))/\(((a_select2 (xinit_defuse) (n3)) = (use))/\(((a_select2 (xinit_defuse) (n4)) = (use))/\(((a_select2 (xinit_defuse) (n5)) = (use))/\(((a_select2 (xinit_mean_defuse) (n0)) = (use))/\(((a_select2 (xinit_mean_defuse) (n1)) = (use))/\(((a_select2 (xinit_mean_defuse) (n2)) = (use))/\(((a_select2 (xinit_mean_defuse) (n3)) = (use))/\(((a_select2 (xinit_mean_defuse) (n4)) = (use))/\(((a_select2 (xinit_mean_defuse) (n5)) = (use))/\(((a_select2 (xinit_noise_defuse) (n0)) = (use))/\(((a_select2 (xinit_noise_defuse) (n1)) = (use))/\(((a_select2 (xinit_noise_defuse) (n2)) = (use))/\(((a_select2 (xinit_noise_defuse) (n3)) = (use))/\(((a_select2 (xinit_noise_defuse) (n4)) = (use))/\(((a_select2 (xinit_noise_defuse) (n5)) = (use))/\((leq (n0) (pv5))/\((leq (n0) (pv51))/\((leq (pv5) (minus (n999) (n1)))/\((leq (pv51) (minus (n6) (n1)))/\(forall A : zenon_U, (forall B : zenon_U, (((leq (n0) A)/\((leq (n0) B)/\((leq A (n2))/\(leq B (minus (pv5) (n1))))))->(((a_select3 (u_defuse) A B) = (use))/\((a_select3 (z_defuse) A B) = (use)))))))))))))))))))))))))))))))))))))))). % 0.18/0.52 Proof. % 0.18/0.52 assert (zenon_L1_ : (~(((a_select2 (rho_defuse) (n0)) = (use))/\(((a_select2 (rho_defuse) (n1)) = (use))/\(((a_select2 (rho_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n0)) = (use))/\(((a_select2 (sigma_defuse) (n1)) = (use))/\(((a_select2 (sigma_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n3)) = (use))/\(((a_select2 (sigma_defuse) (n4)) = (use))/\(((a_select2 (sigma_defuse) (n5)) = (use))/\(((a_select3 (u_defuse) (n0) (n0)) = (use))/\(((a_select3 (u_defuse) (n1) (n0)) = (use))/\(((a_select3 (u_defuse) (n2) (n0)) = (use))/\(((a_select2 (xinit_defuse) (n3)) = (use))/\(((a_select2 (xinit_defuse) (n4)) = (use))/\(((a_select2 (xinit_defuse) (n5)) = (use))/\(((a_select2 (xinit_mean_defuse) (n0)) = (use))/\(((a_select2 (xinit_mean_defuse) (n1)) = (use))/\(((a_select2 (xinit_mean_defuse) (n2)) = (use))/\(((a_select2 (xinit_mean_defuse) (n3)) = (use))/\(((a_select2 (xinit_mean_defuse) (n4)) = (use))/\(((a_select2 (xinit_mean_defuse) (n5)) = (use))/\(((a_select2 (xinit_noise_defuse) (n0)) = (use))/\(((a_select2 (xinit_noise_defuse) (n1)) = (use))/\(((a_select2 (xinit_noise_defuse) (n2)) = (use))/\(((a_select2 (xinit_noise_defuse) (n3)) = (use))/\(((a_select2 (xinit_noise_defuse) (n4)) = (use))/\(((a_select2 (xinit_noise_defuse) (n5)) = (use))/\((leq (n0) (pv5))/\((leq (n0) (pv51))/\((leq (pv5) (minus (n999) (n1)))/\((leq (pv51) (minus (n6) (n1)))/\(forall A : zenon_U, (forall B : zenon_U, (((leq (n0) A)/\((leq (n0) B)/\((leq A (n2))/\(leq B (minus (pv5) (n1))))))->(((a_select3 (u_defuse) A B) = (use))/\((a_select3 (z_defuse) A B) = (use)))))))))))))))))))))))))))))))))))))) -> ((a_select2 (rho_defuse) (n0)) = (use)) -> ((a_select2 (rho_defuse) (n1)) = (use)) -> ((a_select2 (rho_defuse) (n2)) = (use)) -> ((a_select2 (sigma_defuse) (n0)) = (use)) -> ((a_select2 (sigma_defuse) (n1)) = (use)) -> ((a_select2 (sigma_defuse) (n2)) = (use)) -> ((a_select2 (sigma_defuse) (n3)) = (use)) -> ((a_select2 (sigma_defuse) (n4)) = (use)) -> ((a_select2 (sigma_defuse) (n5)) = (use)) -> ((a_select3 (u_defuse) (n0) (n0)) = (use)) -> ((a_select3 (u_defuse) (n1) (n0)) = (use)) -> ((a_select3 (u_defuse) (n2) (n0)) = (use)) -> ((a_select2 (xinit_defuse) (n3)) = (use)) -> ((a_select2 (xinit_defuse) (n4)) = (use)) -> ((a_select2 (xinit_defuse) (n5)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n0)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n1)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n2)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n3)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n4)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n5)) = (use)) -> ((a_select2 (xinit_noise_defuse) (n0)) = (use)) -> ((a_select2 (xinit_noise_defuse) (n1)) = (use)) -> ((a_select2 (xinit_noise_defuse) (n2)) = (use)) -> ((a_select2 (xinit_noise_defuse) (n3)) = (use)) -> ((a_select2 (xinit_noise_defuse) (n4)) = (use)) -> ((a_select2 (xinit_noise_defuse) (n5)) = (use)) -> (gt (succ (pv5)) (n0)) -> (gt (succ (pv51)) (n0)) -> (gt (succ (minus (n999) (n1))) (pv5)) -> (gt (succ (minus (n6) (n1))) (pv51)) -> (forall A : zenon_U, (forall B : zenon_U, (((leq (n0) A)/\((leq (n0) B)/\((leq A (n2))/\(leq B (minus (pv5) (n1))))))->(((a_select3 (u_defuse) A B) = (use))/\((a_select3 (z_defuse) A B) = (use)))))) -> False). % 0.18/0.52 do 0 intro. intros zenon_H66 zenon_H67 zenon_H68 zenon_H69 zenon_H6a zenon_H6b zenon_H6c zenon_H6d zenon_H6e zenon_H6f zenon_H70 zenon_H71 zenon_H72 zenon_H73 zenon_H74 zenon_H75 zenon_H76 zenon_H77 zenon_H78 zenon_H79 zenon_H7a zenon_H7b zenon_H7c zenon_H7d zenon_H7e zenon_H7f zenon_H80 zenon_H81 zenon_H82 zenon_H83 zenon_H84 zenon_H85 zenon_H86. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H66); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 0.18/0.52 exact (zenon_H88 zenon_H67). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 0.18/0.52 exact (zenon_H8a zenon_H68). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H8c | zenon_intro zenon_H8b ]. % 0.18/0.52 exact (zenon_H8c zenon_H69). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H8b); [ zenon_intro zenon_H8e | zenon_intro zenon_H8d ]. % 0.18/0.52 exact (zenon_H8e zenon_H6a). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H8d); [ zenon_intro zenon_H90 | zenon_intro zenon_H8f ]. % 0.18/0.52 exact (zenon_H90 zenon_H6b). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H8f); [ zenon_intro zenon_H92 | zenon_intro zenon_H91 ]. % 0.18/0.52 exact (zenon_H92 zenon_H6c). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H91); [ zenon_intro zenon_H94 | zenon_intro zenon_H93 ]. % 0.18/0.52 exact (zenon_H94 zenon_H6d). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H93); [ zenon_intro zenon_H96 | zenon_intro zenon_H95 ]. % 0.18/0.52 exact (zenon_H96 zenon_H6e). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H95); [ zenon_intro zenon_H98 | zenon_intro zenon_H97 ]. % 0.18/0.52 exact (zenon_H98 zenon_H6f). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H97); [ zenon_intro zenon_H9a | zenon_intro zenon_H99 ]. % 0.18/0.52 exact (zenon_H9a zenon_H70). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H99); [ zenon_intro zenon_H9c | zenon_intro zenon_H9b ]. % 0.18/0.52 exact (zenon_H9c zenon_H71). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9b); [ zenon_intro zenon_H9e | zenon_intro zenon_H9d ]. % 0.18/0.52 exact (zenon_H9e zenon_H72). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9d); [ zenon_intro zenon_Ha0 | zenon_intro zenon_H9f ]. % 0.18/0.52 exact (zenon_Ha0 zenon_H73). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9f); [ zenon_intro zenon_Ha2 | zenon_intro zenon_Ha1 ]. % 0.18/0.52 exact (zenon_Ha2 zenon_H74). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha1); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Ha3 ]. % 0.18/0.52 exact (zenon_Ha4 zenon_H75). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Ha5 ]. % 0.18/0.52 exact (zenon_Ha6 zenon_H76). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha8 | zenon_intro zenon_Ha7 ]. % 0.18/0.52 exact (zenon_Ha8 zenon_H77). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha7); [ zenon_intro zenon_Haa | zenon_intro zenon_Ha9 ]. % 0.18/0.52 exact (zenon_Haa zenon_H78). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha9); [ zenon_intro zenon_Hac | zenon_intro zenon_Hab ]. % 0.18/0.52 exact (zenon_Hac zenon_H79). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hab); [ zenon_intro zenon_Hae | zenon_intro zenon_Had ]. % 0.18/0.52 exact (zenon_Hae zenon_H7a). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Had); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Haf ]. % 0.18/0.52 exact (zenon_Hb0 zenon_H7b). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Haf); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb1 ]. % 0.18/0.52 exact (zenon_Hb2 zenon_H7c). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hb1); [ zenon_intro zenon_Hb4 | zenon_intro zenon_Hb3 ]. % 0.18/0.52 exact (zenon_Hb4 zenon_H7d). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hb3); [ zenon_intro zenon_Hb6 | zenon_intro zenon_Hb5 ]. % 0.18/0.52 exact (zenon_Hb6 zenon_H7e). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb8 | zenon_intro zenon_Hb7 ]. % 0.18/0.52 exact (zenon_Hb8 zenon_H7f). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hb7); [ zenon_intro zenon_Hba | zenon_intro zenon_Hb9 ]. % 0.18/0.52 exact (zenon_Hba zenon_H80). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hb9); [ zenon_intro zenon_Hbc | zenon_intro zenon_Hbb ]. % 0.18/0.52 exact (zenon_Hbc zenon_H81). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_Hbe | zenon_intro zenon_Hbd ]. % 0.18/0.52 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_Hbf. % 0.18/0.52 generalize (zenon_Hbf (pv5)). zenon_intro zenon_Hc0. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_Hc0); [ zenon_intro zenon_Hbe; zenon_intro zenon_Hc2 | zenon_intro zenon_Hc1; zenon_intro zenon_H82 ]. % 0.18/0.52 exact (zenon_Hc2 zenon_H82). % 0.18/0.52 exact (zenon_Hbe zenon_Hc1). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hbd); [ zenon_intro zenon_Hc4 | zenon_intro zenon_Hc3 ]. % 0.18/0.52 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_Hbf. % 0.18/0.52 generalize (zenon_Hbf (pv51)). zenon_intro zenon_Hc5. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_Hc5); [ zenon_intro zenon_Hc4; zenon_intro zenon_Hc7 | zenon_intro zenon_Hc6; zenon_intro zenon_H83 ]. % 0.18/0.52 exact (zenon_Hc7 zenon_H83). % 0.18/0.52 exact (zenon_Hc4 zenon_Hc6). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hc3); [ zenon_intro zenon_Hc9 | zenon_intro zenon_Hc8 ]. % 0.18/0.52 generalize (leq_succ_gt_equiv (pv5)). zenon_intro zenon_Hca. % 0.18/0.52 generalize (zenon_Hca (minus (n999) (n1))). zenon_intro zenon_Hcb. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_Hcb); [ zenon_intro zenon_Hc9; zenon_intro zenon_Hcd | zenon_intro zenon_Hcc; zenon_intro zenon_H84 ]. % 0.18/0.52 exact (zenon_Hcd zenon_H84). % 0.18/0.52 exact (zenon_Hc9 zenon_Hcc). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hc8); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 0.18/0.52 generalize (leq_succ_gt_equiv (pv51)). zenon_intro zenon_Hd0. % 0.18/0.52 generalize (zenon_Hd0 (minus (n6) (n1))). zenon_intro zenon_Hd1. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_Hd1); [ zenon_intro zenon_Hcf; zenon_intro zenon_Hd3 | zenon_intro zenon_Hd2; zenon_intro zenon_H85 ]. % 0.18/0.52 exact (zenon_Hd3 zenon_H85). % 0.18/0.52 exact (zenon_Hcf zenon_Hd2). % 0.18/0.52 exact (zenon_Hce zenon_H86). % 0.18/0.52 (* end of lemma zenon_L1_ *) % 0.18/0.52 apply NNPP. intro zenon_G. % 0.18/0.52 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_Hd5. zenon_intro zenon_Hd4. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hd5). zenon_intro zenon_H67. zenon_intro zenon_Hd6. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hd6). zenon_intro zenon_H68. zenon_intro zenon_Hd7. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hd7). zenon_intro zenon_H69. zenon_intro zenon_Hd8. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hd8). zenon_intro zenon_H6a. zenon_intro zenon_Hd9. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hd9). zenon_intro zenon_H6b. zenon_intro zenon_Hda. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hda). zenon_intro zenon_H6c. zenon_intro zenon_Hdb. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hdb). zenon_intro zenon_H6d. zenon_intro zenon_Hdc. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hdc). zenon_intro zenon_H6e. zenon_intro zenon_Hdd. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hdd). zenon_intro zenon_H6f. zenon_intro zenon_Hde. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hde). zenon_intro zenon_H70. zenon_intro zenon_Hdf. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hdf). zenon_intro zenon_H71. zenon_intro zenon_He0. % 0.18/0.52 apply (zenon_and_s _ _ zenon_He0). zenon_intro zenon_H72. zenon_intro zenon_He1. % 0.18/0.52 apply (zenon_and_s _ _ zenon_He1). zenon_intro zenon_H73. zenon_intro zenon_He2. % 0.18/0.52 apply (zenon_and_s _ _ zenon_He2). zenon_intro zenon_H74. zenon_intro zenon_He3. % 0.18/0.52 apply (zenon_and_s _ _ zenon_He3). zenon_intro zenon_H75. zenon_intro zenon_He4. % 0.18/0.52 apply (zenon_and_s _ _ zenon_He4). zenon_intro zenon_H76. zenon_intro zenon_He5. % 0.18/0.52 apply (zenon_and_s _ _ zenon_He5). zenon_intro zenon_H77. zenon_intro zenon_He6. % 0.18/0.52 apply (zenon_and_s _ _ zenon_He6). zenon_intro zenon_H78. zenon_intro zenon_He7. % 0.18/0.52 apply (zenon_and_s _ _ zenon_He7). zenon_intro zenon_H79. zenon_intro zenon_He8. % 0.18/0.52 apply (zenon_and_s _ _ zenon_He8). zenon_intro zenon_H7a. zenon_intro zenon_He9. % 0.18/0.52 apply (zenon_and_s _ _ zenon_He9). zenon_intro zenon_H7b. zenon_intro zenon_Hea. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hea). zenon_intro zenon_H7c. zenon_intro zenon_Heb. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Heb). zenon_intro zenon_H7d. zenon_intro zenon_Hec. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hec). zenon_intro zenon_H7e. zenon_intro zenon_Hed. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hed). zenon_intro zenon_H7f. zenon_intro zenon_Hee. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hee). zenon_intro zenon_H80. zenon_intro zenon_Hef. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hef). zenon_intro zenon_H81. zenon_intro zenon_Hf0. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hf0). zenon_intro zenon_Hc1. zenon_intro zenon_Hf1. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hf1). zenon_intro zenon_Hc6. zenon_intro zenon_Hf2. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hf2). zenon_intro zenon_Hf4. zenon_intro zenon_Hf3. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hf3). zenon_intro zenon_Hcc. zenon_intro zenon_Hf5. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hf5). zenon_intro zenon_Hd2. zenon_intro zenon_Hf6. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Hf6). zenon_intro zenon_Hf7. zenon_intro zenon_H86. % 0.18/0.52 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_Hbf. % 0.18/0.52 generalize (zenon_Hbf (pv5)). zenon_intro zenon_Hc0. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_Hc0); [ zenon_intro zenon_Hbe; zenon_intro zenon_Hc2 | zenon_intro zenon_Hc1; zenon_intro zenon_H82 ]. % 0.18/0.52 exact (zenon_Hbe zenon_Hc1). % 0.18/0.52 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_Hbf. % 0.18/0.52 generalize (zenon_Hbf (pv51)). zenon_intro zenon_Hc5. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_Hc5); [ zenon_intro zenon_Hc4; zenon_intro zenon_Hc7 | zenon_intro zenon_Hc6; zenon_intro zenon_H83 ]. % 0.18/0.52 exact (zenon_Hc4 zenon_Hc6). % 0.18/0.52 generalize (leq_succ_gt_equiv (pv5)). zenon_intro zenon_Hca. % 0.18/0.52 generalize (zenon_Hca (minus (n999) (n1))). zenon_intro zenon_Hcb. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_Hcb); [ zenon_intro zenon_Hc9; zenon_intro zenon_Hcd | zenon_intro zenon_Hcc; zenon_intro zenon_H84 ]. % 0.18/0.52 exact (zenon_Hc9 zenon_Hcc). % 0.18/0.52 generalize (leq_succ_gt_equiv (pv51)). zenon_intro zenon_Hd0. % 0.18/0.52 generalize (zenon_Hd0 (minus (n6) (n1))). zenon_intro zenon_Hd1. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_Hd1); [ zenon_intro zenon_Hcf; zenon_intro zenon_Hd3 | zenon_intro zenon_Hd2; zenon_intro zenon_H85 ]. % 0.18/0.52 exact (zenon_Hcf zenon_Hd2). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hd4); [ zenon_intro zenon_Hf9 | zenon_intro zenon_Hf8 ]. % 0.18/0.52 apply (zenon_notimply_s _ _ zenon_Hf9). zenon_intro zenon_Hfa. zenon_intro zenon_H66. % 0.18/0.52 apply (zenon_L1_); trivial. % 0.18/0.52 apply (zenon_notimply_s _ _ zenon_Hf8). zenon_intro zenon_Hfb. zenon_intro zenon_H66. % 0.18/0.52 apply (zenon_L1_); trivial. % 0.18/0.52 Qed. % 0.18/0.52 % SZS output end Proof % 0.18/0.52 (* END-PROOF *) % 0.18/0.52 nodes searched: 56 % 0.18/0.52 max branch formulas: 154 % 0.18/0.52 proof nodes created: 45 % 0.18/0.52 formulas created: 3624 % 0.18/0.52 %------------------------------------------------------------------------------