%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM444+6 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n004.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 : Mon Jul 18 15:55:43 EDT 2022 % Result : Theorem 30.64s 30.84s % Output : Proof 30.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : NUM444+6 : TPTP v8.1.0. Released v4.0.0. % 0.11/0.12 % Command : run_zenon %s %d % 0.11/0.33 % Computer : n004.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 : Thu Jul 7 13:39:37 EDT 2022 % 0.11/0.33 % CPUTime : % 30.64/30.84 (* PROOF-FOUND *) % 30.64/30.84 % SZS status Theorem % 30.64/30.84 (* BEGIN-PROOF *) % 30.64/30.84 % SZS output start Proof % 30.64/30.84 Theorem m__ : ((forall W0 : zenon_U, (forall W1 : zenon_U, (((aInteger0 W0)/\(aInteger0 W1))->(((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))/\(forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))/\(sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))\/(sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))->((~(aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))\/(aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))/\((exists W2 : zenon_U, ((aInteger0 W2)/\((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0)))))\/((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0)))\/(sdteqdtlpzmzozddtrp0 W1 W0 (xq)))))->((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))/\((forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))/\(sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))\/(sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))/\((~(aElementOf0 W1 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))/\(aElementOf0 W1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))))))->((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))/\(forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))/\(sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))\/(sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))->(((aSet0 (cS1395))/\(forall W0 : zenon_U, ((aElementOf0 W0 (cS1395))<->(aInteger0 W0))))->((forall W0 : zenon_U, ((aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->(aElementOf0 W0 (cS1395))))\/(aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)) (cS1395)))))/\((forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))/\(sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))\/(sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))->((((aSet0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))/\(forall W0 : zenon_U, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))<->((aInteger0 W0)/\(~(aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))))->((forall W0 : zenon_U, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))->(exists W1 : zenon_U, ((aInteger0 W1)/\((~(W1 = (sz00)))/\(((aSet0 (szAzrzSzezqlpdtcmdtrp0 W0 W1))/\(forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0)))))/\((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0)))/\(sdteqdtlpzmzozddtrp0 W2 W0 W1)))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0)))))\/((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0)))\/(sdteqdtlpzmzozddtrp0 W2 W0 W1))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1))))))->((forall W2 : zenon_U, ((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1))->(aElementOf0 W2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))\/(aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 W0 W1) (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))))))\/(isOpen0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))\/(isClosed0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))). % 30.64/30.84 Proof. % 30.64/30.84 assert (zenon_L1_ : forall (zenon_TW0_bt : zenon_U), (forall W0 : zenon_U, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))<->((aInteger0 W0)/\(~(aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) -> (aElementOf0 zenon_TW0_bt (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) -> (~(aInteger0 zenon_TW0_bt)) -> False). % 30.64/30.84 do 1 intro. intros zenon_H2a zenon_H2b zenon_H2c. % 30.64/30.84 generalize (zenon_H2a zenon_TW0_bt). zenon_intro zenon_H2e. % 30.64/30.84 apply (zenon_equiv_s _ _ zenon_H2e); [ zenon_intro zenon_H31; zenon_intro zenon_H30 | zenon_intro zenon_H2b; zenon_intro zenon_H2f ]. % 30.64/30.84 exact (zenon_H31 zenon_H2b). % 30.64/30.84 apply (zenon_and_s _ _ zenon_H2f). zenon_intro zenon_H33. zenon_intro zenon_H32. % 30.64/30.84 exact (zenon_H2c zenon_H33). % 30.64/30.84 (* end of lemma zenon_L1_ *) % 30.64/30.84 assert (zenon_L2_ : forall (zenon_TW0_bt : zenon_U), (~(((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))/\(forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))/\(sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))\/(sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))->((~(aElementOf0 zenon_TW0_bt (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))\/(aElementOf0 zenon_TW0_bt (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) -> (~(aElementOf0 zenon_TW0_bt (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) -> False). % 30.64/30.84 do 1 intro. intros zenon_H34 zenon_H32. % 30.64/30.84 apply (zenon_notimply_s _ _ zenon_H34). zenon_intro zenon_H36. zenon_intro zenon_H35. % 30.64/30.84 apply (zenon_notor_s _ _ zenon_H35). zenon_intro zenon_H37. zenon_intro zenon_H31. % 30.64/30.84 exact (zenon_H37 zenon_H32). % 30.64/30.84 (* end of lemma zenon_L2_ *) % 30.64/30.84 assert (zenon_L3_ : forall (zenon_TW2_cg : zenon_U), ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))/\((forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))/\(sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))\/(sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))/\((~(aElementOf0 zenon_TW2_cg (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))/\(aElementOf0 zenon_TW2_cg (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) -> (aElementOf0 zenon_TW2_cg (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) -> False). % 30.64/30.84 do 1 intro. intros zenon_H38 zenon_H39. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H38). zenon_intro zenon_H3c. zenon_intro zenon_H3b. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H3b). zenon_intro zenon_H3e. zenon_intro zenon_H3d. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H3d). zenon_intro zenon_H40. zenon_intro zenon_H3f. % 30.64/30.84 exact (zenon_H40 zenon_H39). % 30.64/30.84 (* end of lemma zenon_L3_ *) % 30.64/30.84 assert (zenon_L4_ : forall (zenon_TW2_cg : zenon_U) (zenon_TW0_bt : zenon_U), (forall W0 : zenon_U, (forall W1 : zenon_U, (((aInteger0 W0)/\(aInteger0 W1))->(((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))/\(forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))/\(sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))\/(sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))->((~(aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))\/(aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))/\((exists W2 : zenon_U, ((aInteger0 W2)/\((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0)))))\/((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0)))\/(sdteqdtlpzmzozddtrp0 W1 W0 (xq)))))->((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))/\((forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))/\(sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))\/(sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))/\((~(aElementOf0 W1 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))/\(aElementOf0 W1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))))))) -> (aInteger0 zenon_TW0_bt) -> (aInteger0 zenon_TW2_cg) -> (aElementOf0 zenon_TW2_cg (szAzrzSzezqlpdtcmdtrp0 zenon_TW0_bt (xq))) -> (forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 zenon_TW0_bt (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 zenon_TW0_bt)))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 zenon_TW0_bt)))/\(sdteqdtlpzmzozddtrp0 W2 zenon_TW0_bt (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 zenon_TW0_bt)))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 zenon_TW0_bt)))\/(sdteqdtlpzmzozddtrp0 W2 zenon_TW0_bt (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 zenon_TW0_bt (xq)))))) -> (aElementOf0 zenon_TW2_cg (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) -> (aElementOf0 zenon_TW0_bt (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) -> (forall W0 : zenon_U, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))<->((aInteger0 W0)/\(~(aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) -> False). % 30.64/30.84 do 2 intro. intros zenon_H41 zenon_H33 zenon_H42 zenon_H43 zenon_H44 zenon_H39 zenon_H2b zenon_H2a. % 30.64/30.84 generalize (zenon_H41 zenon_TW0_bt). zenon_intro zenon_H45. % 30.64/30.84 generalize (zenon_H2a zenon_TW0_bt). zenon_intro zenon_H2e. % 30.64/30.84 apply (zenon_equiv_s _ _ zenon_H2e); [ zenon_intro zenon_H31; zenon_intro zenon_H30 | zenon_intro zenon_H2b; zenon_intro zenon_H2f ]. % 30.64/30.84 exact (zenon_H31 zenon_H2b). % 30.64/30.84 apply (zenon_and_s _ _ zenon_H2f). zenon_intro zenon_H33. zenon_intro zenon_H32. % 30.64/30.84 generalize (zenon_H45 zenon_TW2_cg). zenon_intro zenon_H46. % 30.64/30.84 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 30.64/30.84 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H2c | zenon_intro zenon_H49 ]. % 30.64/30.84 exact (zenon_H2c zenon_H33). % 30.64/30.84 exact (zenon_H49 zenon_H42). % 30.64/30.84 apply (zenon_imply_s _ _ zenon_H47); [ zenon_intro zenon_H4a | zenon_intro zenon_H38 ]. % 30.64/30.84 apply (zenon_notand_s _ _ zenon_H4a); [ zenon_intro zenon_H34 | zenon_intro zenon_H4b ]. % 30.64/30.84 apply (zenon_L2_ zenon_TW0_bt); trivial. % 30.64/30.84 apply (zenon_notor_s _ _ zenon_H4b). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 30.64/30.84 generalize (zenon_H44 zenon_TW2_cg). zenon_intro zenon_H4e. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H4e). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 30.64/30.84 apply (zenon_imply_s _ _ zenon_H50); [ zenon_intro zenon_H52 | zenon_intro zenon_H51 ]. % 30.64/30.84 exact (zenon_H52 zenon_H43). % 30.64/30.84 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H42. zenon_intro zenon_H53. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H53). zenon_intro zenon_H55. zenon_intro zenon_H54. % 30.64/30.84 exact (zenon_H4d zenon_H55). % 30.64/30.84 apply (zenon_L3_ zenon_TW2_cg); trivial. % 30.64/30.84 (* end of lemma zenon_L4_ *) % 30.64/30.84 assert (zenon_L5_ : forall (zenon_TW0_bt : zenon_U) (zenon_TW2_cg : zenon_U), (forall W0 : zenon_U, (forall W1 : zenon_U, (((aInteger0 W0)/\(aInteger0 W1))->(((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))/\(forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))/\(sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))\/(sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))->((~(aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))\/(aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))/\((exists W2 : zenon_U, ((aInteger0 W2)/\((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0)))))\/((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0)))\/(sdteqdtlpzmzozddtrp0 W1 W0 (xq)))))->((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))/\((forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))/\(sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa))))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa))))\/(sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))/\((~(aElementOf0 W1 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))/\(aElementOf0 W1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))))))) -> (aInteger0 zenon_TW2_cg) -> (aElementOf0 zenon_TW2_cg (szAzrzSzezqlpdtcmdtrp0 zenon_TW0_bt (xq))) -> (forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 zenon_TW0_bt (xq)))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 zenon_TW0_bt)))))/\((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 zenon_TW0_bt)))/\(sdteqdtlpzmzozddtrp0 W2 zenon_TW0_bt (xq))))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 zenon_TW0_bt)))))\/((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 zenon_TW0_bt)))\/(sdteqdtlpzmzozddtrp0 W2 zenon_TW0_bt (xq)))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 zenon_TW0_bt (xq)))))) -> (aElementOf0 zenon_TW2_cg (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) -> (forall W0 : zenon_U, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))<->((aInteger0 W0)/\(~(aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) -> (aElementOf0 zenon_TW0_bt (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) -> (aInteger0 (xq)) -> (~((xq) = (sz00))) -> False). % 30.64/30.84 do 2 intro. intros zenon_H41 zenon_H42 zenon_H43 zenon_H44 zenon_H39 zenon_H2a zenon_H2b zenon_H56 zenon_H57. % 30.64/30.84 generalize (zenon_H44 zenon_TW0_bt). zenon_intro zenon_H58. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 30.64/30.84 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 30.64/30.84 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H5e | zenon_intro zenon_H5d ]. % 30.64/30.84 apply (zenon_notand_s _ _ zenon_H5e); [ zenon_intro zenon_H2c | zenon_intro zenon_H5f ]. % 30.64/30.84 apply (zenon_L1_ zenon_TW0_bt); trivial. % 30.64/30.84 apply (zenon_notor_s _ _ zenon_H5f). zenon_intro zenon_H61. zenon_intro zenon_H60. % 30.64/30.84 apply (zenon_notor_s _ _ zenon_H60). zenon_intro zenon_H63. zenon_intro zenon_H62. % 30.64/30.84 generalize (mEquModRef zenon_TW0_bt). zenon_intro zenon_H64. % 30.64/30.84 generalize (zenon_H64 (xq)). zenon_intro zenon_H65. % 30.64/30.84 apply (zenon_imply_s _ _ zenon_H65); [ zenon_intro zenon_H67 | zenon_intro zenon_H66 ]. % 30.64/30.84 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H2c | zenon_intro zenon_H68 ]. % 30.64/30.84 apply (zenon_L1_ zenon_TW0_bt); trivial. % 30.64/30.84 apply (zenon_notand_s _ _ zenon_H68); [ zenon_intro zenon_H6a | zenon_intro zenon_H69 ]. % 30.64/30.84 exact (zenon_H6a zenon_H56). % 30.64/30.84 exact (zenon_H69 zenon_H57). % 30.64/30.84 exact (zenon_H62 zenon_H66). % 30.64/30.84 exact (zenon_H5c zenon_H5d). % 30.64/30.84 apply (zenon_and_s _ _ zenon_H5b). zenon_intro zenon_H33. zenon_intro zenon_H6b. % 30.64/30.84 apply (zenon_L4_ zenon_TW2_cg zenon_TW0_bt); trivial. % 30.64/30.84 (* end of lemma zenon_L5_ *) % 30.64/30.84 apply NNPP. intro zenon_G. % 30.64/30.84 apply (zenon_and_s _ _ m__1962). zenon_intro zenon_H6d. zenon_intro zenon_H6c. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H6c). zenon_intro zenon_H56. zenon_intro zenon_H57. % 30.64/30.84 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H41. zenon_intro zenon_H6e. % 30.64/30.84 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H70 | zenon_intro zenon_H6f ]. % 30.64/30.84 apply (zenon_notimply_s _ _ zenon_H70). zenon_intro zenon_H36. zenon_intro zenon_H71. % 30.64/30.84 apply (zenon_notimply_s _ _ zenon_H71). zenon_intro zenon_H73. zenon_intro zenon_H72. % 30.64/30.84 apply (zenon_notor_s _ _ zenon_H72). zenon_intro zenon_H75. zenon_intro zenon_H74. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H73). zenon_intro zenon_H77. zenon_intro zenon_H76. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H3c. zenon_intro zenon_H3e. % 30.64/30.84 apply (zenon_notallex_s (fun W0 : zenon_U => ((aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))->(aElementOf0 W0 (cS1395)))) zenon_H75); [ zenon_intro zenon_H78; idtac ]. % 30.64/30.84 elim zenon_H78. zenon_intro zenon_TW0_er. zenon_intro zenon_H7a. % 30.64/30.84 apply (zenon_notimply_s _ _ zenon_H7a). zenon_intro zenon_H7c. zenon_intro zenon_H7b. % 30.64/30.84 generalize (zenon_H76 zenon_TW0_er). zenon_intro zenon_H7d. % 30.64/30.84 apply (zenon_equiv_s _ _ zenon_H7d); [ zenon_intro zenon_H7b; zenon_intro zenon_H80 | zenon_intro zenon_H7f; zenon_intro zenon_H7e ]. % 30.64/30.84 generalize (zenon_H3e zenon_TW0_er). zenon_intro zenon_H81. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H81). zenon_intro zenon_H83. zenon_intro zenon_H82. % 30.64/30.84 apply (zenon_imply_s _ _ zenon_H83); [ zenon_intro zenon_H85 | zenon_intro zenon_H84 ]. % 30.64/30.84 exact (zenon_H85 zenon_H7c). % 30.64/30.84 apply (zenon_and_s _ _ zenon_H84). zenon_intro zenon_H7e. zenon_intro zenon_H86. % 30.64/30.84 exact (zenon_H80 zenon_H7e). % 30.64/30.84 exact (zenon_H7b zenon_H7f). % 30.64/30.84 apply (zenon_notimply_s _ _ zenon_H6f). zenon_intro zenon_H3e. zenon_intro zenon_H87. % 30.64/30.84 apply (zenon_notor_s _ _ zenon_H87). zenon_intro zenon_H89. zenon_intro zenon_H88. % 30.64/30.84 apply (zenon_notimply_s _ _ zenon_H89). zenon_intro zenon_H8b. zenon_intro zenon_H8a. % 30.64/30.84 apply (zenon_notor_s _ _ zenon_H8a). zenon_intro zenon_H8d. zenon_intro zenon_H8c. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H8b). zenon_intro zenon_H8e. zenon_intro zenon_H2a. % 30.64/30.84 apply (zenon_notallex_s (fun W0 : zenon_U => ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))->(exists W1 : zenon_U, ((aInteger0 W1)/\((~(W1 = (sz00)))/\(((aSet0 (szAzrzSzezqlpdtcmdtrp0 W0 W1))/\(forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0)))))/\((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0)))/\(sdteqdtlpzmzozddtrp0 W2 W0 W1)))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0)))))\/((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0)))\/(sdteqdtlpzmzozddtrp0 W2 W0 W1))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1))))))->((forall W2 : zenon_U, ((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1))->(aElementOf0 W2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))\/(aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 W0 W1) (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))))))) zenon_H8d); [ zenon_intro zenon_H8f; idtac ]. % 30.64/30.84 elim zenon_H8f. zenon_intro zenon_TW0_bt. zenon_intro zenon_H90. % 30.64/30.84 apply (zenon_notimply_s _ _ zenon_H90). zenon_intro zenon_H2b. zenon_intro zenon_H91. % 30.64/30.84 apply zenon_H91. exists (xq). apply NNPP. zenon_intro zenon_H92. % 30.64/30.84 apply (zenon_notand_s _ _ zenon_H92); [ zenon_intro zenon_H6a | zenon_intro zenon_H93 ]. % 30.64/30.84 exact (zenon_H6a zenon_H56). % 30.64/30.84 apply (zenon_notand_s _ _ zenon_H93); [ zenon_intro zenon_H69 | zenon_intro zenon_H94 ]. % 30.64/30.84 exact (zenon_H69 zenon_H57). % 30.64/30.84 apply (zenon_notimply_s _ _ zenon_H94). zenon_intro zenon_H96. zenon_intro zenon_H95. % 30.64/30.84 apply (zenon_notor_s _ _ zenon_H95). zenon_intro zenon_H98. zenon_intro zenon_H97. % 30.64/30.84 apply (zenon_and_s _ _ zenon_H96). zenon_intro zenon_H99. zenon_intro zenon_H44. % 30.64/30.84 apply (zenon_notallex_s (fun W2 : zenon_U => ((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 zenon_TW0_bt (xq)))->(aElementOf0 W2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) zenon_H98); [ zenon_intro zenon_H9a; idtac ]. % 30.64/30.84 elim zenon_H9a. zenon_intro zenon_TW2_cg. zenon_intro zenon_H9b. % 30.64/30.84 apply (zenon_notimply_s _ _ zenon_H9b). zenon_intro zenon_H43. zenon_intro zenon_H9c. % 30.64/30.84 generalize (zenon_H2a zenon_TW2_cg). zenon_intro zenon_H9d. % 30.64/30.84 apply (zenon_equiv_s _ _ zenon_H9d); [ zenon_intro zenon_H9c; zenon_intro zenon_H9f | zenon_intro zenon_H3f; zenon_intro zenon_H9e ]. % 30.64/30.84 apply (zenon_notand_s _ _ zenon_H9f); [ zenon_intro zenon_H49 | zenon_intro zenon_Ha0 ]. % 30.64/30.87 generalize (zenon_H44 zenon_TW2_cg). zenon_intro zenon_H4e. % 30.64/30.87 apply (zenon_and_s _ _ zenon_H4e). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 30.64/30.87 apply (zenon_imply_s _ _ zenon_H50); [ zenon_intro zenon_H52 | zenon_intro zenon_H51 ]. % 30.64/30.87 exact (zenon_H52 zenon_H43). % 30.64/30.87 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H42. zenon_intro zenon_H53. % 30.64/30.87 exact (zenon_H49 zenon_H42). % 30.64/30.87 apply zenon_Ha0. zenon_intro zenon_H39. % 30.64/30.87 generalize (zenon_H44 zenon_TW2_cg). zenon_intro zenon_H4e. % 30.64/30.87 apply (zenon_and_s _ _ zenon_H4e). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 30.64/30.87 apply (zenon_imply_s _ _ zenon_H50); [ zenon_intro zenon_H52 | zenon_intro zenon_H51 ]. % 30.64/30.87 exact (zenon_H52 zenon_H43). % 30.64/30.87 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H42. zenon_intro zenon_H53. % 30.64/30.87 apply (zenon_L5_ zenon_TW0_bt zenon_TW2_cg); trivial. % 30.64/30.87 exact (zenon_H9c zenon_H3f). % 30.64/30.87 Qed. % 30.64/30.87 % SZS output end Proof % 30.64/30.87 (* END-PROOF *) % 30.64/30.87 nodes searched: 179822 % 30.64/30.87 max branch formulas: 32366 % 30.64/30.87 proof nodes created: 9427 % 30.64/30.87 formulas created: 1152049 % 30.64/30.87 %------------------------------------------------------------------------------