%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR255+1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n018.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:57 EDT 2022 % Result : Theorem 8.91s 9.13s % Output : Proof 8.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : CSR255+1 : TPTP v8.1.0. Released v7.3.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n018.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jun 10 14:44:24 EDT 2022 % 0.12/0.33 % CPUTime : % 8.91/9.13 (* PROOF-FOUND *) % 8.91/9.13 % SZS status Theorem % 8.91/9.13 (* BEGIN-PROOF *) % 8.91/9.13 % SZS output start Proof % 8.91/9.13 Theorem subclassEvent0238 : (p__d__subclass (c__Laughing) (c__BodyMotion)). % 8.91/9.13 Proof. % 8.91/9.13 assert (zenon_L1_ : (~((c__Gesture) = (c__Gesture))) -> False). % 8.91/9.13 do 0 intro. intros zenon_H1d07. % 8.91/9.13 apply zenon_H1d07. apply refl_equal. % 8.91/9.13 (* end of lemma zenon_L1_ *) % 8.91/9.13 assert (zenon_L2_ : (~((c__BodyMotion) = (c__BodyMotion))) -> False). % 8.91/9.13 do 0 intro. intros zenon_H1d08. % 8.91/9.13 apply zenon_H1d08. apply refl_equal. % 8.91/9.13 (* end of lemma zenon_L2_ *) % 8.91/9.13 apply NNPP. intro zenon_G. % 8.91/9.13 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_H1d09 | zenon_intro zenon_H1d0a ]. % 8.91/9.13 elim (classic ((~((c__Laughing) = (c__Gesture)))/\(~(p__d__subclass (c__Laughing) (c__Gesture))))); [ zenon_intro zenon_H1d0b | zenon_intro zenon_H1d0c ]. % 8.91/9.13 apply (zenon_and_s _ _ zenon_H1d0b). zenon_intro zenon_H1d0e. zenon_intro zenon_H1d0d. % 8.91/9.13 elim (classic ((~((c__Laughing) = (c__FacialExpression)))/\(~(p__d__subclass (c__Laughing) (c__FacialExpression))))); [ zenon_intro zenon_H1d0f | zenon_intro zenon_H1d10 ]. % 8.91/9.13 apply (zenon_and_s _ _ zenon_H1d0f). zenon_intro zenon_H1d12. zenon_intro zenon_H1d11. % 8.91/9.13 exact (zenon_H1d11 miloA1793). % 8.91/9.13 cut ((p__d__subclass (c__FacialExpression) (c__Gesture)) = (p__d__subclass (c__Laughing) (c__Gesture))). % 8.91/9.13 intro zenon_D_pnotp. % 8.91/9.13 apply zenon_H1d0d. % 8.91/9.13 rewrite <- zenon_D_pnotp. % 8.91/9.13 exact miloA1786. % 8.91/9.13 cut (((c__Gesture) = (c__Gesture))); [idtac | apply NNPP; zenon_intro zenon_H1d07]. % 8.91/9.13 cut (((c__FacialExpression) = (c__Laughing))); [idtac | apply NNPP; zenon_intro zenon_H1d13]. % 8.91/9.13 congruence. % 8.91/9.13 apply (zenon_notand_s _ _ zenon_H1d10); [ zenon_intro zenon_H1d15 | zenon_intro zenon_H1d14 ]. % 8.91/9.13 apply zenon_H1d15. zenon_intro zenon_H1d16. % 8.91/9.13 elim (classic ((c__Laughing) = (c__Laughing))); [ zenon_intro zenon_H1d17 | zenon_intro zenon_H1d18 ]. % 8.91/9.13 cut (((c__Laughing) = (c__Laughing)) = ((c__FacialExpression) = (c__Laughing))). % 8.91/9.13 intro zenon_D_pnotp. % 8.91/9.13 apply zenon_H1d13. % 8.91/9.13 rewrite <- zenon_D_pnotp. % 8.91/9.13 exact zenon_H1d17. % 8.91/9.13 cut (((c__Laughing) = (c__Laughing))); [idtac | apply NNPP; zenon_intro zenon_H1d18]. % 8.91/9.13 cut (((c__Laughing) = (c__FacialExpression))); [idtac | apply NNPP; zenon_intro zenon_H1d12]. % 8.91/9.13 congruence. % 8.91/9.13 exact (zenon_H1d12 zenon_H1d16). % 8.91/9.13 apply zenon_H1d18. apply refl_equal. % 8.91/9.13 apply zenon_H1d18. apply refl_equal. % 8.91/9.13 apply zenon_H1d14. zenon_intro miloA1793. % 8.91/9.13 generalize (zenon_H1d09 (c__Laughing)). zenon_intro zenon_H1d19. % 8.91/9.13 generalize (zenon_H1d19 (c__FacialExpression)). zenon_intro zenon_H1d1a. % 8.91/9.13 generalize (zenon_H1d1a (c__Gesture)). zenon_intro zenon_H1d1b. % 8.91/9.13 apply (zenon_imply_s _ _ zenon_H1d1b); [ zenon_intro zenon_H1d11 | zenon_intro zenon_H1d1c ]. % 8.91/9.13 exact (zenon_H1d11 miloA1793). % 8.91/9.13 apply (zenon_imply_s _ _ zenon_H1d1c); [ zenon_intro zenon_H1d1e | zenon_intro zenon_H1d1d ]. % 8.91/9.13 exact (zenon_H1d1e miloA1786). % 8.91/9.13 exact (zenon_H1d0d zenon_H1d1d). % 8.91/9.13 apply zenon_H1d07. apply refl_equal. % 8.91/9.13 cut ((p__d__subclass (c__Gesture) (c__BodyMotion)) = (p__d__subclass (c__Laughing) (c__BodyMotion))). % 8.91/9.13 intro zenon_D_pnotp. % 8.91/9.13 apply zenon_G. % 8.91/9.13 rewrite <- zenon_D_pnotp. % 8.91/9.13 exact mergeA2714. % 8.91/9.13 cut (((c__BodyMotion) = (c__BodyMotion))); [idtac | apply NNPP; zenon_intro zenon_H1d08]. % 8.91/9.13 cut (((c__Gesture) = (c__Laughing))); [idtac | apply NNPP; zenon_intro zenon_H1d1f]. % 8.91/9.13 congruence. % 8.91/9.13 apply (zenon_notand_s _ _ zenon_H1d0c); [ zenon_intro zenon_H1d21 | zenon_intro zenon_H1d20 ]. % 8.91/9.13 apply zenon_H1d21. zenon_intro zenon_H1d22. % 8.91/9.13 elim (classic ((c__Laughing) = (c__Laughing))); [ zenon_intro zenon_H1d17 | zenon_intro zenon_H1d18 ]. % 8.91/9.13 cut (((c__Laughing) = (c__Laughing)) = ((c__Gesture) = (c__Laughing))). % 8.91/9.13 intro zenon_D_pnotp. % 8.91/9.13 apply zenon_H1d1f. % 8.91/9.13 rewrite <- zenon_D_pnotp. % 8.91/9.13 exact zenon_H1d17. % 8.91/9.13 cut (((c__Laughing) = (c__Laughing))); [idtac | apply NNPP; zenon_intro zenon_H1d18]. % 8.91/9.13 cut (((c__Laughing) = (c__Gesture))); [idtac | apply NNPP; zenon_intro zenon_H1d0e]. % 8.91/9.13 congruence. % 8.91/9.13 exact (zenon_H1d0e zenon_H1d22). % 8.91/9.13 apply zenon_H1d18. apply refl_equal. % 8.91/9.13 apply zenon_H1d18. apply refl_equal. % 8.91/9.13 apply zenon_H1d20. zenon_intro zenon_H1d1d. % 8.91/9.13 generalize (zenon_H1d09 (c__Laughing)). zenon_intro zenon_H1d19. % 8.91/9.13 generalize (zenon_H1d19 (c__Gesture)). zenon_intro zenon_H1d23. % 8.98/9.15 generalize (zenon_H1d23 (c__BodyMotion)). zenon_intro zenon_H1d24. % 8.98/9.15 apply (zenon_imply_s _ _ zenon_H1d24); [ zenon_intro zenon_H1d0d | zenon_intro zenon_H1d25 ]. % 8.98/9.15 exact (zenon_H1d0d zenon_H1d1d). % 8.98/9.15 apply (zenon_imply_s _ _ zenon_H1d25); [ zenon_intro zenon_H1d27 | zenon_intro zenon_H1d26 ]. % 8.98/9.15 exact (zenon_H1d27 mergeA2714). % 8.98/9.15 exact (zenon_G zenon_H1d26). % 8.98/9.15 apply zenon_H1d08. apply refl_equal. % 8.98/9.15 apply zenon_H1d0a. zenon_intro zenon_Tx_lbc. apply NNPP. zenon_intro zenon_H1d29. % 8.98/9.15 apply zenon_H1d29. zenon_intro zenon_Ty_lbe. apply NNPP. zenon_intro zenon_H1d2b. % 8.98/9.15 apply zenon_H1d2b. zenon_intro zenon_Tz_lbg. apply NNPP. zenon_intro zenon_H1d2d. % 8.98/9.15 apply (zenon_notimply_s _ _ zenon_H1d2d). zenon_intro zenon_H1d2f. zenon_intro zenon_H1d2e. % 8.98/9.15 apply (zenon_notimply_s _ _ zenon_H1d2e). zenon_intro zenon_H1d31. zenon_intro zenon_H1d30. % 8.98/9.15 generalize (predefinitionsA8 zenon_Tx_lbc). zenon_intro zenon_H1d32. % 8.98/9.15 generalize (zenon_H1d32 zenon_Ty_lbe). zenon_intro zenon_H1d33. % 8.98/9.15 generalize (zenon_H1d33 zenon_Tz_lbg). zenon_intro zenon_H1d34. % 8.98/9.15 apply (zenon_imply_s _ _ zenon_H1d34); [ zenon_intro zenon_H1d36 | zenon_intro zenon_H1d35 ]. % 8.98/9.15 apply (zenon_notand_s _ _ zenon_H1d36); [ zenon_intro zenon_H1d38 | zenon_intro zenon_H1d37 ]. % 8.98/9.15 exact (zenon_H1d38 zenon_H1d2f). % 8.98/9.15 exact (zenon_H1d37 zenon_H1d31). % 8.98/9.15 exact (zenon_H1d30 zenon_H1d35). % 8.98/9.15 Qed. % 8.98/9.15 % SZS output end Proof % 8.98/9.15 (* END-PROOF *) % 8.98/9.15 nodes searched: 215769 % 8.98/9.15 max branch formulas: 56613 % 8.98/9.15 proof nodes created: 81 % 8.98/9.15 formulas created: 2680246 % 8.98/9.15 %------------------------------------------------------------------------------