%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEU139+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n011.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 : Tue Jul 19 15:59:38 EDT 2022 % Result : Theorem 3.96s 4.14s % Output : Proof 3.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU139+2 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n011.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 : Sun Jun 19 01:17:38 EDT 2022 % 0.12/0.33 % CPUTime : % 3.96/4.14 Zenon warning: unused variable (B : zenon_U) in idempotence_k2_xboole_0 % 3.96/4.14 Zenon warning: unused variable (B : zenon_U) in idempotence_k3_xboole_0 % 3.96/4.14 Zenon warning: unused variable (B : zenon_U) in irreflexivity_r2_xboole_0 % 3.96/4.14 Zenon warning: unused variable (B : zenon_U) in reflexivity_r1_tarski % 3.96/4.14 (* PROOF-FOUND *) % 3.96/4.14 % SZS status Theorem % 3.96/4.14 (* BEGIN-PROOF *) % 3.96/4.14 % SZS output start Proof % 3.96/4.14 Theorem t60_xboole_1 : (forall A : zenon_U, (forall B : zenon_U, (~((subset A B)/\(proper_subset B A))))). % 3.96/4.14 Proof. % 3.96/4.14 apply NNPP. intro zenon_G. % 3.96/4.14 apply (zenon_notallex_s (fun A : zenon_U => (forall B : zenon_U, (~((subset A B)/\(proper_subset B A))))) zenon_G); [ zenon_intro zenon_H33; idtac ]. % 3.96/4.14 elim zenon_H33. zenon_intro zenon_TA_ca. zenon_intro zenon_H35. % 3.96/4.14 apply (zenon_notallex_s (fun B : zenon_U => (~((subset zenon_TA_ca B)/\(proper_subset B zenon_TA_ca)))) zenon_H35); [ zenon_intro zenon_H36; idtac ]. % 3.96/4.14 elim zenon_H36. zenon_intro zenon_TB_cd. zenon_intro zenon_H38. % 3.96/4.14 apply zenon_H38. zenon_intro zenon_H39. % 3.96/4.14 apply (zenon_and_s _ _ zenon_H39). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 3.96/4.14 generalize (d8_xboole_0 zenon_TB_cd). zenon_intro zenon_H3c. % 3.96/4.14 generalize (zenon_H3c zenon_TA_ca). zenon_intro zenon_H3d. % 3.96/4.14 apply (zenon_equiv_s _ _ zenon_H3d); [ zenon_intro zenon_H40; zenon_intro zenon_H3f | zenon_intro zenon_H3a; zenon_intro zenon_H3e ]. % 3.96/4.14 exact (zenon_H40 zenon_H3a). % 3.96/4.14 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H42. zenon_intro zenon_H41. % 3.96/4.14 generalize (d10_xboole_0 zenon_TA_ca). zenon_intro zenon_H43. % 3.96/4.14 generalize (zenon_H43 zenon_TB_cd). zenon_intro zenon_H44. % 3.96/4.14 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H48; zenon_intro zenon_H47 | zenon_intro zenon_H46; zenon_intro zenon_H45 ]. % 3.96/4.14 apply (zenon_notand_s _ _ zenon_H47); [ zenon_intro zenon_H4a | zenon_intro zenon_H49 ]. % 3.96/4.14 exact (zenon_H4a zenon_H3b). % 3.96/4.14 exact (zenon_H49 zenon_H42). % 3.96/4.14 apply zenon_H41. apply sym_equal. exact zenon_H46. % 3.96/4.14 Qed. % 3.96/4.14 % SZS output end Proof % 3.96/4.14 (* END-PROOF *) % 3.96/4.14 nodes searched: 266600 % 3.96/4.14 max branch formulas: 9699 % 3.96/4.14 proof nodes created: 2838 % 3.96/4.14 formulas created: 154155 % 3.96/4.14 %------------------------------------------------------------------------------