SuperZenon---0.0.1.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : SuperZenon---0.0.1
% Problem  : NUM444+6 : TPTP v8.1.0. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_super_zenon -p0 -itptp -om -max-time %d %s

% Computer : n005.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 14:42:31 EDT 2022

% Result   : Theorem 9.80s 9.98s
% Output   : Proof 9.96s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12  % Problem  : NUM444+6 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.12  % Command  : run_super_zenon -p0 -itptp -om -max-time %d %s
% 0.12/0.33  % Computer : n005.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 : Thu Jul  7 13:43:07 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 9.80/9.98  % SZS status Theorem
% 9.80/9.98  (* PROOF-FOUND *)
% 9.80/9.98  (* BEGIN-PROOF *)
% 9.80/9.98  % SZS output start Proof
% 9.80/9.98  1. (aElementOf0 T_0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) (-. (aElementOf0 T_0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))   ### Axiom
% 9.80/9.98  2. (-. (aInteger0 T_0)) (aInteger0 T_0)   ### Axiom
% 9.80/9.98  3. ((aInteger0 T_0) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 T_0 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_0 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 T_0 (xa) (xq))))) (-. (aInteger0 T_0))   ### ConjTree 2
% 9.80/9.98  4. ((aElementOf0 T_0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 T_0) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 T_0 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_0 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 T_0 (xa) (xq)))))) (-. (aInteger0 T_0)) (aElementOf0 T_0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))   ### Imply 1 3
% 9.80/9.98  5. (((aElementOf0 T_0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 T_0) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 T_0 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_0 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 T_0 (xa) (xq)))))) /\ (((aInteger0 T_0) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 T_0 (smndt0 (xa)))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 T_0 (smndt0 (xa)))) \/ (sdteqdtlpzmzozddtrp0 T_0 (xa) (xq))))) => (aElementOf0 T_0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (aElementOf0 T_0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) (-. (aInteger0 T_0))   ### And 4
% 9.80/9.98  6. (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) \/ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) (-. (aInteger0 T_0)) (aElementOf0 T_0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))   ### All 5
% 9.80/9.98  7. (-. (aElementOf0 T_0 (cS1395))) (aElementOf0 T_0 (cS1395))   ### Axiom
% 9.80/9.98  8. ((aElementOf0 T_0 (cS1395)) <=> (aInteger0 T_0)) (-. (aElementOf0 T_0 (cS1395))) (aElementOf0 T_0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) \/ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))   ### Equiv 6 7
% 9.80/9.98  9. (All W0, ((aElementOf0 W0 (cS1395)) <=> (aInteger0 W0))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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 T_0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) (-. (aElementOf0 T_0 (cS1395)))   ### All 8
% 9.80/9.98  10. (-. ((aElementOf0 T_0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => (aElementOf0 T_0 (cS1395)))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) \/ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) (All W0, ((aElementOf0 W0 (cS1395)) <=> (aInteger0 W0)))   ### NotImply 9
% 9.80/9.98  11. (-. (All W0, ((aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => (aElementOf0 W0 (cS1395))))) (All W0, ((aElementOf0 W0 (cS1395)) <=> (aInteger0 W0))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) \/ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))   ### NotAllEx 10
% 9.80/9.98  12. (-. (((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)) /\ (All W0, ((aElementOf0 W0 (cS1395)) <=> (aInteger0 W0)))) => ((All W0, ((aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => (aElementOf0 W0 (cS1395)))) \/ (aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)) (cS1395))))))   ### ConjTree 11
% 9.80/9.98  13. (aInteger0 (xq)) (-. (aInteger0 (xq)))   ### Axiom
% 9.80/9.98  14. ((xq) != (sz00)) ((xq) = (sz00))   ### Axiom
% 9.80/9.98  15. (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (-. (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))))   ### Axiom
% 9.80/9.98  16. (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (-. (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))   ### Axiom
% 9.80/9.98  17. (-. (aInteger0 T_2)) (aInteger0 T_2)   ### Axiom
% 9.80/9.98  18. ((aInteger0 T_2) /\ (-. (aElementOf0 T_2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (-. (aInteger0 T_2))   ### And 17
% 9.80/9.98  19. ((aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 T_2) /\ (-. (aElementOf0 T_2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) (-. (aInteger0 T_2)) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))   ### Equiv 16 18
% 9.80/9.98  20. (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (-. (aInteger0 T_2))   ### All 19
% 9.80/9.98  21. (aInteger0 (xq)) (-. (aInteger0 (xq)))   ### Axiom
% 9.80/9.98  22. ((xq) != (sz00)) ((xq) = (sz00))   ### Axiom
% 9.80/9.98  23. (-. (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq))) (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq))   ### Axiom
% 9.80/9.98  24. (((aInteger0 T_2) /\ ((aInteger0 (xq)) /\ ((xq) != (sz00)))) => (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq))) (-. (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq))) ((xq) != (sz00)) (aInteger0 (xq)) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))   ### DisjTree 20 21 22 23
% 9.80/9.98  25. (All W1, (((aInteger0 T_2) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 T_2 T_2 W1))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (aInteger0 (xq)) ((xq) != (sz00)) (-. (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq)))   ### All 24
% 9.80/9.98  26. (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) (-. (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq))) ((xq) != (sz00)) (aInteger0 (xq)) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))   ### All 25
% 9.80/9.98  27. (-. ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 T_2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 T_2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq))))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (aInteger0 (xq)) ((xq) != (sz00)) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1))))   ### ConjTree 26
% 9.83/10.02  28. (-. (aElementOf0 T_2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))) (aElementOf0 T_2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))   ### Axiom
% 9.83/10.02  29. (((aInteger0 T_2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 T_2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 T_2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq))))) => (aElementOf0 T_2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))) (-. (aElementOf0 T_2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) ((xq) != (sz00)) (aInteger0 (xq)) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))   ### DisjTree 20 27 28
% 9.83/10.02  30. (aInteger0 T_2) (-. (aInteger0 T_2))   ### Axiom
% 9.83/10.02  31. (aInteger0 T_1) (-. (aInteger0 T_1))   ### Axiom
% 9.83/10.02  32. (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (-. (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))   ### Axiom
% 9.83/10.02  33. (-. (((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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 T_2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) \/ (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))   ### ConjTree 32
% 9.83/10.02  34. (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (-. (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))))   ### Axiom
% 9.83/10.02  35. (-. (Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2)))))) (Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2)))))   ### Axiom
% 9.83/10.02  36. ((aInteger0 T_1) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_1 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 T_1 T_2 (xq))))) (-. (Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))))   ### ConjTree 35
% 9.83/10.02  37. ((aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 T_1) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_1 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 T_1 T_2 (xq)))))) (-. (Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2)))))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))   ### Imply 34 36
% 9.83/10.02  38. (((aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 T_1) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_1 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 T_1 T_2 (xq)))))) /\ (((aInteger0 T_1) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 T_1 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 T_1 T_2 (xq))))) => (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (-. (Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))))   ### And 37
% 9.83/10.02  39. (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (-. (Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2)))))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))   ### All 38
% 9.83/10.02  40. (-. ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 T_1 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 T_1 T_2 (xq))))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))))))   ### ConjTree 39
% 9.83/10.02  41. (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))   ### Axiom
% 9.83/10.02  42. ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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 T_1 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) /\ (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))   ### ConjTree 41
% 9.83/10.02  43. (((aInteger0 T_2) /\ (aInteger0 T_1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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 T_2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) \/ (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 T_1 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 T_1 T_2 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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 T_1 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) /\ (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (aInteger0 T_1) (aInteger0 T_2)   ### DisjTree 30 31 33 40 42
% 9.86/10.03  44. (All W1, (((aInteger0 T_2) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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 T_2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) \/ (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W1 T_2 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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 T_2) (aInteger0 T_1) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))   ### All 43
% 9.86/10.03  45. (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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))))))))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (aInteger0 T_1) (aInteger0 T_2)   ### All 44
% 9.86/10.03  46. ((aInteger0 T_2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 T_2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq))))) (aInteger0 T_1) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))))))))   ### ConjTree 45
% 9.86/10.03  47. ((aElementOf0 T_2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 T_2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 T_2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq)))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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))))))))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (aInteger0 T_1) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (aInteger0 (xq)) ((xq) != (sz00)) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) (((aInteger0 T_2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 T_2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 T_2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq))))) => (aElementOf0 T_2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))))   ### Imply 29 46
% 9.86/10.04  48. (((aElementOf0 T_2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 T_2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 T_2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq)))))) /\ (((aInteger0 T_2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 T_2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 T_2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 T_2 T_2 (xq))))) => (aElementOf0 T_2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))))) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) ((xq) != (sz00)) (aInteger0 (xq)) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aInteger0 T_1) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))))))))   ### And 47
% 9.86/10.04  49. (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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))))))))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (aInteger0 T_1) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (aInteger0 (xq)) ((xq) != (sz00)) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1))))   ### All 48
% 9.86/10.05  50. ((aInteger0 T_1) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_1 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 T_1 T_2 (xq))))) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) ((xq) != (sz00)) (aInteger0 (xq)) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))))))))   ### ConjTree 49
% 9.86/10.05  51. ((aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 T_1) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_1 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 T_1 T_2 (xq)))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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))))))))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (aInteger0 (xq)) ((xq) != (sz00)) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))   ### Imply 15 50
% 9.86/10.05  52. (((aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 T_1) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 T_1 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 T_1 T_2 (xq)))))) /\ (((aInteger0 T_1) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 T_1 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 T_1 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 T_1 T_2 (xq))))) => (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) ((xq) != (sz00)) (aInteger0 (xq)) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))))))))   ### And 51
% 9.96/10.16  53. (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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))))))))))) (-. (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (aInteger0 (xq)) ((xq) != (sz00)) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) (aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))   ### All 52
% 9.96/10.16  54. (-. ((aElementOf0 T_1 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => (aElementOf0 T_1 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) ((xq) != (sz00)) (aInteger0 (xq)) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))))))))   ### NotImply 53
% 9.96/10.16  55. (-. (All W2, ((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => (aElementOf0 W2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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))))))))))) (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)))))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (aInteger0 (xq)) ((xq) != (sz00)) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1))))   ### NotAllEx 54
% 9.96/10.16  56. (-. (((aSet0 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))))))) => ((All W2, ((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => (aElementOf0 W2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) \/ (aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)) (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) ((xq) != (sz00)) (aInteger0 (xq)) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))))))))   ### ConjTree 55
% 9.96/10.16  57. (-. ((aInteger0 (xq)) /\ (((xq) != (sz00)) /\ (((aSet0 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 (xq))))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))))))) => ((All W2, ((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq))) => (aElementOf0 W2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) \/ (aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 T_2 (xq)) (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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))))))))))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) ((xq) != (sz00)) (aInteger0 (xq))   ### DisjTree 13 14 56
% 9.96/10.16  58. (-. (Ex W1, ((aInteger0 W1) /\ ((W1 != (sz00)) /\ (((aSet0 (szAzrzSzezqlpdtcmdtrp0 T_2 W1)) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 W1)) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 W1))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 W1)))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 W1)))))) => ((All W2, ((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 W1)) => (aElementOf0 W2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) \/ (aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 T_2 W1) (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))))) (aInteger0 (xq)) ((xq) != (sz00)) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) (aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))))))))   ### NotExists 57
% 9.96/10.16  59. (-. ((aElementOf0 T_2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) => (Ex W1, ((aInteger0 W1) /\ ((W1 != (sz00)) /\ (((aSet0 (szAzrzSzezqlpdtcmdtrp0 T_2 W1)) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 W1)) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 T_2))))) /\ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 T_2))) /\ (sdteqdtlpzmzozddtrp0 W2 T_2 W1))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 T_2))))) \/ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 T_2))) \/ (sdteqdtlpzmzozddtrp0 W2 T_2 W1)))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 W1)))))) => ((All W2, ((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 T_2 W1)) => (aElementOf0 W2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) \/ (aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 T_2 W1) (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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))))))))))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) ((xq) != (sz00)) (aInteger0 (xq))   ### NotImply 58
% 9.96/10.16  60. (-. (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) => (Ex W1, ((aInteger0 W1) /\ ((W1 != (sz00)) /\ (((aSet0 (szAzrzSzezqlpdtcmdtrp0 W0 W1)) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1)) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0))))) /\ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0))) /\ (sdteqdtlpzmzozddtrp0 W2 W0 W1))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0))))) \/ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W2 W0 W1)))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1)))))) => ((All W2, ((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1)) => (aElementOf0 W2 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))) \/ (aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 W0 W1) (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))))))) (aInteger0 (xq)) ((xq) != (sz00)) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))))))))   ### NotAllEx 59
% 9.96/10.16  61. (-. ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))) /\ (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))) => ((All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) => (Ex W1, ((aInteger0 W1) /\ ((W1 != (sz00)) /\ (((aSet0 (szAzrzSzezqlpdtcmdtrp0 W0 W1)) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1)) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0))))) /\ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0))) /\ (sdteqdtlpzmzozddtrp0 W2 W0 W1))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0))))) \/ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W2 W0 W1)))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1)))))) => ((All W2, ((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)))))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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))))))))))) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) ((xq) != (sz00)) (aInteger0 (xq))   ### ConjTree 60
% 9.96/10.17  62. (-. ((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)) /\ (All W0, ((aElementOf0 W0 (cS1395)) <=> (aInteger0 W0)))) => ((All W0, ((aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => (aElementOf0 W0 (cS1395)))) \/ (aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)) (cS1395))))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))) /\ (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))) => ((All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) => (Ex W1, ((aInteger0 W1) /\ ((W1 != (sz00)) /\ (((aSet0 (szAzrzSzezqlpdtcmdtrp0 W0 W1)) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1)) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0))))) /\ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0))) /\ (sdteqdtlpzmzozddtrp0 W2 W0 W1))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0))))) \/ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W2 W0 W1)))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1)))))) => ((All W2, ((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))))))) (aInteger0 (xq)) ((xq) != (sz00)) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))))))))   ### NotAnd 12 61
% 9.96/10.17  63. ((aInteger0 (xa)) /\ ((aInteger0 (xq)) /\ ((xq) != (sz00)))) (All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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))))))))))) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) (-. ((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)) /\ (All W0, ((aElementOf0 W0 (cS1395)) <=> (aInteger0 W0)))) => ((All W0, ((aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => (aElementOf0 W0 (cS1395)))) \/ (aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)) (cS1395))))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))) /\ (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))) => ((All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) => (Ex W1, ((aInteger0 W1) /\ ((W1 != (sz00)) /\ (((aSet0 (szAzrzSzezqlpdtcmdtrp0 W0 W1)) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1)) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0))))) /\ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0))) /\ (sdteqdtlpzmzozddtrp0 W2 W0 W1))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0))))) \/ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W2 W0 W1)))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1)))))) => ((All W2, ((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)))))))   ### ConjTree 62
% 9.96/10.17  64. (-. ((All W0, (All W1, (((aInteger0 W0) /\ (aInteger0 W1)) => (((((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))))) /\ ((Ex W2, ((aInteger0 W2) /\ ((sdtasdt0 (xq) W2) = (sdtpldt0 W1 (smndt0 W0))))) \/ ((aDivisorOf0 (xq) (sdtpldt0 W1 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W1 W0 (xq))))) => ((aSet0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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))) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)) /\ (All W0, ((aElementOf0 W0 (cS1395)) <=> (aInteger0 W0)))) => ((All W0, ((aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => (aElementOf0 W0 (cS1395)))) \/ (aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)) (cS1395))))) /\ ((All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq))) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 (xq) W3) = (sdtpldt0 W2 (smndt0 (xa)))))) /\ ((aDivisorOf0 (xq) (sdtpldt0 W2 (smndt0 (xa)))) /\ (sdteqdtlpzmzozddtrp0 W2 (xa) (xq)))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((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)))) /\ (All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))))))) => ((All W0, ((aElementOf0 W0 (stldt0 (szAzrzSzezqlpdtcmdtrp0 (xa) (xq)))) => (Ex W1, ((aInteger0 W1) /\ ((W1 != (sz00)) /\ (((aSet0 (szAzrzSzezqlpdtcmdtrp0 W0 W1)) /\ (All W2, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1)) => ((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0))))) /\ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0))) /\ (sdteqdtlpzmzozddtrp0 W2 W0 W1))))) /\ (((aInteger0 W2) /\ ((Ex W3, ((aInteger0 W3) /\ ((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 W0))))) \/ ((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 W0))) \/ (sdteqdtlpzmzozddtrp0 W2 W0 W1)))) => (aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 W0 W1)))))) => ((All W2, ((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)))))))) (All W0, (All W1, (((aInteger0 W0) /\ ((aInteger0 W1) /\ (W1 != (sz00)))) => (sdteqdtlpzmzozddtrp0 W0 W0 W1)))) ((aInteger0 (xa)) /\ ((aInteger0 (xq)) /\ ((xq) != (sz00))))   ### NotImply 63
% 9.96/10.17  % SZS output end Proof
% 9.96/10.17  (* END-PROOF *)
%------------------------------------------------------------------------------