%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR256+1 : TPTP v8.1.0. Released v7.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 : Sat Jul 16 00:03:58 EDT 2022 % Result : Theorem 8.47s 8.67s % Output : Proof 8.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : CSR256+1 : TPTP v8.1.0. Released v7.3.0. % 0.12/0.12 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n021.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 : Sat Jun 11 05:01:24 EDT 2022 % 0.12/0.34 % CPUTime : % 8.47/8.67 (* PROOF-FOUND *) % 8.47/8.67 % SZS status Theorem % 8.47/8.67 (* BEGIN-PROOF *) % 8.47/8.67 % SZS output start Proof % 8.47/8.67 Theorem subclassEvent0321 : (p__d__subclass (c__Funding) (c__SocialInteraction)). % 8.47/8.67 Proof. % 8.47/8.67 assert (zenon_L1_ : (~((c__ChangeOfPossession) = (c__ChangeOfPossession))) -> False). % 8.47/8.67 do 0 intro. intros zenon_H1d07. % 8.47/8.67 apply zenon_H1d07. apply refl_equal. % 8.47/8.67 (* end of lemma zenon_L1_ *) % 8.47/8.67 apply NNPP. intro zenon_G. % 8.47/8.67 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((p__d__subclass x y)->((p__d__subclass y z)->(p__d__subclass x z))))))); [ zenon_intro zenon_H1d08 | zenon_intro zenon_H1d09 ]. % 8.47/8.67 elim (classic ((~((c__Funding) = (c__ChangeOfPossession)))/\(~(p__d__subclass (c__Funding) (c__ChangeOfPossession))))); [ zenon_intro zenon_H1d0a | zenon_intro zenon_H1d0b ]. % 8.47/8.67 apply (zenon_and_s _ _ zenon_H1d0a). zenon_intro zenon_H1d0d. zenon_intro zenon_H1d0c. % 8.47/8.67 elim (classic ((~((c__Funding) = (c__Giving)))/\(~(p__d__subclass (c__Funding) (c__Giving))))); [ zenon_intro zenon_H1d0e | zenon_intro zenon_H1d0f ]. % 8.47/8.67 apply (zenon_and_s _ _ zenon_H1d0e). zenon_intro zenon_H1d11. zenon_intro zenon_H1d10. % 8.47/8.67 exact (zenon_H1d10 mergeA2526). % 8.47/8.67 cut ((p__d__subclass (c__Giving) (c__ChangeOfPossession)) = (p__d__subclass (c__Funding) (c__ChangeOfPossession))). % 8.47/8.67 intro zenon_D_pnotp. % 8.47/8.67 apply zenon_H1d0c. % 8.47/8.67 rewrite <- zenon_D_pnotp. % 8.47/8.67 exact mergeA2523. % 8.47/8.67 cut (((c__ChangeOfPossession) = (c__ChangeOfPossession))); [idtac | apply NNPP; zenon_intro zenon_H1d07]. % 8.47/8.67 cut (((c__Giving) = (c__Funding))); [idtac | apply NNPP; zenon_intro zenon_H1d12]. % 8.47/8.67 congruence. % 8.47/8.67 apply (zenon_notand_s _ _ zenon_H1d0f); [ zenon_intro zenon_H1d14 | zenon_intro zenon_H1d13 ]. % 8.47/8.67 apply zenon_H1d14. zenon_intro zenon_H1d15. % 8.47/8.67 elim (classic ((c__Funding) = (c__Funding))); [ zenon_intro zenon_H1d16 | zenon_intro zenon_H1d17 ]. % 8.47/8.67 cut (((c__Funding) = (c__Funding)) = ((c__Giving) = (c__Funding))). % 8.47/8.67 intro zenon_D_pnotp. % 8.47/8.67 apply zenon_H1d12. % 8.47/8.67 rewrite <- zenon_D_pnotp. % 8.47/8.67 exact zenon_H1d16. % 8.47/8.67 cut (((c__Funding) = (c__Funding))); [idtac | apply NNPP; zenon_intro zenon_H1d17]. % 8.47/8.67 cut (((c__Funding) = (c__Giving))); [idtac | apply NNPP; zenon_intro zenon_H1d11]. % 8.47/8.67 congruence. % 8.47/8.67 exact (zenon_H1d11 zenon_H1d15). % 8.47/8.67 apply zenon_H1d17. apply refl_equal. % 8.47/8.67 apply zenon_H1d17. apply refl_equal. % 8.47/8.67 apply zenon_H1d13. zenon_intro mergeA2526. % 8.47/8.67 generalize (zenon_H1d08 (c__Funding)). zenon_intro zenon_H1d18. % 8.47/8.67 generalize (zenon_H1d18 (c__Giving)). zenon_intro zenon_H1d19. % 8.47/8.67 generalize (zenon_H1d19 (c__ChangeOfPossession)). zenon_intro zenon_H1d1a. % 8.47/8.67 apply (zenon_imply_s _ _ zenon_H1d1a); [ zenon_intro zenon_H1d10 | zenon_intro zenon_H1d1b ]. % 8.47/8.67 exact (zenon_H1d10 mergeA2526). % 8.47/8.67 apply (zenon_imply_s _ _ zenon_H1d1b); [ zenon_intro zenon_H1d1d | zenon_intro zenon_H1d1c ]. % 8.47/8.67 exact (zenon_H1d1d mergeA2523). % 8.47/8.67 exact (zenon_H1d0c zenon_H1d1c). % 8.47/8.67 apply zenon_H1d07. apply refl_equal. % 8.47/8.67 cut ((p__d__subclass (c__ChangeOfPossession) (c__SocialInteraction)) = (p__d__subclass (c__Funding) (c__SocialInteraction))). % 8.47/8.67 intro zenon_D_pnotp. % 8.47/8.67 apply zenon_G. % 8.47/8.67 rewrite <- zenon_D_pnotp. % 8.47/8.67 exact mergeA2519. % 8.47/8.67 cut (((c__SocialInteraction) = (c__SocialInteraction))); [idtac | apply NNPP; zenon_intro zenon_H1d1e]. % 8.47/8.67 cut (((c__ChangeOfPossession) = (c__Funding))); [idtac | apply NNPP; zenon_intro zenon_H1d1f]. % 8.47/8.67 congruence. % 8.47/8.67 apply (zenon_notand_s _ _ zenon_H1d0b); [ zenon_intro zenon_H1d21 | zenon_intro zenon_H1d20 ]. % 8.47/8.67 apply zenon_H1d21. zenon_intro zenon_H1d22. % 8.47/8.67 elim (classic ((c__Funding) = (c__Funding))); [ zenon_intro zenon_H1d16 | zenon_intro zenon_H1d17 ]. % 8.47/8.67 cut (((c__Funding) = (c__Funding)) = ((c__ChangeOfPossession) = (c__Funding))). % 8.47/8.67 intro zenon_D_pnotp. % 8.47/8.67 apply zenon_H1d1f. % 8.47/8.67 rewrite <- zenon_D_pnotp. % 8.47/8.67 exact zenon_H1d16. % 8.47/8.67 cut (((c__Funding) = (c__Funding))); [idtac | apply NNPP; zenon_intro zenon_H1d17]. % 8.47/8.67 cut (((c__Funding) = (c__ChangeOfPossession))); [idtac | apply NNPP; zenon_intro zenon_H1d0d]. % 8.47/8.67 congruence. % 8.47/8.67 exact (zenon_H1d0d zenon_H1d22). % 8.47/8.67 apply zenon_H1d17. apply refl_equal. % 8.47/8.67 apply zenon_H1d17. apply refl_equal. % 8.47/8.67 apply zenon_H1d20. zenon_intro zenon_H1d1c. % 8.47/8.67 generalize (zenon_H1d08 (c__Funding)). zenon_intro zenon_H1d18. % 8.47/8.67 generalize (zenon_H1d18 (c__ChangeOfPossession)). zenon_intro zenon_H1d23. % 8.47/8.67 generalize (zenon_H1d23 (c__SocialInteraction)). zenon_intro zenon_H1d24. % 8.47/8.69 apply (zenon_imply_s _ _ zenon_H1d24); [ zenon_intro zenon_H1d0c | zenon_intro zenon_H1d25 ]. % 8.47/8.69 exact (zenon_H1d0c zenon_H1d1c). % 8.47/8.69 apply (zenon_imply_s _ _ zenon_H1d25); [ zenon_intro zenon_H1d27 | zenon_intro zenon_H1d26 ]. % 8.47/8.69 exact (zenon_H1d27 mergeA2519). % 8.47/8.69 exact (zenon_G zenon_H1d26). % 8.47/8.69 apply zenon_H1d1e. apply refl_equal. % 8.47/8.69 apply zenon_H1d09. zenon_intro zenon_Tx_lbc. apply NNPP. zenon_intro zenon_H1d29. % 8.47/8.69 apply zenon_H1d29. zenon_intro zenon_Ty_lbe. apply NNPP. zenon_intro zenon_H1d2b. % 8.47/8.69 apply zenon_H1d2b. zenon_intro zenon_Tz_lbg. apply NNPP. zenon_intro zenon_H1d2d. % 8.47/8.69 apply (zenon_notimply_s _ _ zenon_H1d2d). zenon_intro zenon_H1d2f. zenon_intro zenon_H1d2e. % 8.47/8.69 apply (zenon_notimply_s _ _ zenon_H1d2e). zenon_intro zenon_H1d31. zenon_intro zenon_H1d30. % 8.47/8.69 generalize (predefinitionsA8 zenon_Tx_lbc). zenon_intro zenon_H1d32. % 8.47/8.69 generalize (zenon_H1d32 zenon_Ty_lbe). zenon_intro zenon_H1d33. % 8.47/8.69 generalize (zenon_H1d33 zenon_Tz_lbg). zenon_intro zenon_H1d34. % 8.47/8.69 apply (zenon_imply_s _ _ zenon_H1d34); [ zenon_intro zenon_H1d36 | zenon_intro zenon_H1d35 ]. % 8.47/8.69 apply (zenon_notand_s _ _ zenon_H1d36); [ zenon_intro zenon_H1d38 | zenon_intro zenon_H1d37 ]. % 8.47/8.69 exact (zenon_H1d38 zenon_H1d2f). % 8.47/8.69 exact (zenon_H1d37 zenon_H1d31). % 8.47/8.69 exact (zenon_H1d30 zenon_H1d35). % 8.47/8.69 Qed. % 8.47/8.69 % SZS output end Proof % 8.47/8.69 (* END-PROOF *) % 8.47/8.69 nodes searched: 215765 % 8.47/8.69 max branch formulas: 56581 % 8.47/8.69 proof nodes created: 86 % 8.47/8.69 formulas created: 2706427 % 8.47/8.69 %------------------------------------------------------------------------------