%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : RNG092+1 : 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 : n024.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 20:41:58 EDT 2022 % Result : Theorem 36.61s 36.85s % Output : Proof 36.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : RNG092+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n024.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 : Mon May 30 06:54:06 EDT 2022 % 0.12/0.34 % CPUTime : % 36.61/36.85 % SZS status Theorem % 36.61/36.85 (* PROOF-FOUND *) % 36.61/36.85 (* BEGIN-PROOF *) % 36.61/36.85 % SZS output start Proof % 36.61/36.85 1. (aSet0 (xI)) (-. (aSet0 (xI))) ### Axiom % 36.61/36.85 2. (aSet0 (xJ)) (-. (aSet0 (xJ))) ### Axiom % 36.61/36.85 3. ((sdtpldt1 (xI) (xJ)) != (sdtpldt1 (xI) (xJ))) ### Refl(=) % 36.61/36.85 4. (-. (aSet0 (sdtpldt1 (xI) (xJ)))) (aSet0 (sdtpldt1 (xI) (xJ))) ### Axiom % 36.61/36.85 5. ((aSet0 (sdtpldt1 (xI) (xJ))) /\ (All W3, ((aElementOf0 W3 (sdtpldt1 (xI) (xJ))) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 (xI)) /\ ((aElementOf0 W5 (xJ)) /\ ((sdtpldt0 W4 W5) = W3)))))))) (-. (aSet0 (sdtpldt1 (xI) (xJ)))) ### And 4 % 36.61/36.85 6. (((sdtpldt1 (xI) (xJ)) = (sdtpldt1 (xI) (xJ))) <=> ((aSet0 (sdtpldt1 (xI) (xJ))) /\ (All W3, ((aElementOf0 W3 (sdtpldt1 (xI) (xJ))) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 (xI)) /\ ((aElementOf0 W5 (xJ)) /\ ((sdtpldt0 W4 W5) = W3))))))))) (-. (aSet0 (sdtpldt1 (xI) (xJ)))) ### Equiv 3 5 % 36.61/36.85 7. (All W2, ((W2 = (sdtpldt1 (xI) (xJ))) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 (xI)) /\ ((aElementOf0 W5 (xJ)) /\ ((sdtpldt0 W4 W5) = W3)))))))))) (-. (aSet0 (sdtpldt1 (xI) (xJ)))) ### All 6 % 36.61/36.85 8. (((aSet0 (xI)) /\ (aSet0 (xJ))) => (All W2, ((W2 = (sdtpldt1 (xI) (xJ))) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 (xI)) /\ ((aElementOf0 W5 (xJ)) /\ ((sdtpldt0 W4 W5) = W3))))))))))) (-. (aSet0 (sdtpldt1 (xI) (xJ)))) (aSet0 (xJ)) (aSet0 (xI)) ### DisjTree 1 2 7 % 36.61/36.85 9. (All W1, (((aSet0 (xI)) /\ (aSet0 W1)) => (All W2, ((W2 = (sdtpldt1 (xI) W1)) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 (xI)) /\ ((aElementOf0 W5 W1) /\ ((sdtpldt0 W4 W5) = W3)))))))))))) (aSet0 (xI)) (aSet0 (xJ)) (-. (aSet0 (sdtpldt1 (xI) (xJ)))) ### All 8 % 36.61/36.85 10. (All W0, (All W1, (((aSet0 W0) /\ (aSet0 W1)) => (All W2, ((W2 = (sdtpldt1 W0 W1)) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 W0) /\ ((aElementOf0 W5 W1) /\ ((sdtpldt0 W4 W5) = W3))))))))))))) (-. (aSet0 (sdtpldt1 (xI) (xJ)))) (aSet0 (xJ)) (aSet0 (xI)) ### All 9 % 36.61/36.85 11. (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (-. (aElementOf0 T_0 (sdtpldt1 (xI) (xJ)))) ### Axiom % 36.61/36.85 12. (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) (-. (aElementOf0 T_1 (sdtpldt1 (xI) (xJ)))) ### Axiom % 36.61/36.85 13. (aElement0 (sz00)) (-. (aElement0 (sz00))) ### Axiom % 36.61/36.85 14. (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) ### Axiom % 36.61/36.85 15. ((aElementOf0 T_2 (xI)) /\ ((aElementOf0 T_3 (xJ)) /\ ((T_1 = (sdtpldt0 T_2 T_3)) /\ ((aElementOf0 (sdtpldt0 T_4 T_2) (xI)) /\ ((aElementOf0 (sdtpldt0 T_5 T_3) (xJ)) /\ ((aElementOf0 (sdtasdt0 (sz00) T_4) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz00) T_5) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 T_4 T_2) (sdtpldt0 T_5 T_3))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 (sz00) T_0) (sdtpldt1 (xI) (xJ)))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### ConjTree 14 % 36.61/36.85 16. (Ex W6, ((aElementOf0 T_2 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_1 = (sdtpldt0 T_2 W6)) /\ ((aElementOf0 (sdtpldt0 T_4 T_2) (xI)) /\ ((aElementOf0 (sdtpldt0 T_5 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 (sz00) T_4) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz00) T_5) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 T_4 T_2) (sdtpldt0 T_5 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 (sz00) T_0) (sdtpldt1 (xI) (xJ))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### Exists 15 % 36.61/36.85 17. (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 T_4 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 T_5 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 (sz00) T_4) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz00) T_5) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 T_4 W5) (sdtpldt0 T_5 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 (sz00) T_0) (sdtpldt1 (xI) (xJ)))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### Exists 16 % 36.61/36.85 18. ((aElementOf0 T_4 (xI)) /\ ((aElementOf0 T_5 (xJ)) /\ ((T_0 = (sdtpldt0 T_4 T_5)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 T_4 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 T_5 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 (sz00) T_4) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz00) T_5) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 T_4 W5) (sdtpldt0 T_5 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 (sz00) T_0) (sdtpldt1 (xI) (xJ))))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### ConjTree 17 % 36.61/36.85 19. (Ex W4, ((aElementOf0 T_4 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((T_0 = (sdtpldt0 T_4 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 T_4 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 (sz00) T_4) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz00) W4) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 T_4 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 (sz00) T_0) (sdtpldt1 (xI) (xJ)))))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### Exists 18 % 36.61/36.85 20. (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((T_0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 (sz00) W3) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz00) W4) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 (sz00) T_0) (sdtpldt1 (xI) (xJ))))))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### Exists 19 % 36.61/36.85 21. (((aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 (sz00)))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((T_0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 (sz00) W3) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz00) W4) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 (sz00) T_0) (sdtpldt1 (xI) (xJ)))))))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) (aElement0 (sz00)) (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) ### DisjTree 11 12 13 20 % 36.61/36.85 22. (All W2, (((aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((T_0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 T_0) (sdtpldt1 (xI) (xJ))))))))))))))))))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) (aElement0 (sz00)) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### All 21 % 36.61/36.85 23. (All W1, (All W2, (((aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((T_0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 T_0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 T_0) (sdtpldt1 (xI) (xJ)))))))))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) (aElement0 (sz00)) (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) ### All 22 % 36.70/36.88 24. (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) (aElement0 (sz00)) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### All 23 % 36.70/36.88 25. (-. ((aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))))) (aElement0 (sz00)) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) ### NotImply 24 % 36.70/36.88 26. (-. (All W2, ((aElementOf0 W2 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 T_0 W2) (sdtpldt1 (xI) (xJ)))))) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (aElement0 (sz00)) ### NotAllEx 25 % 36.70/36.88 27. (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (-. (aElementOf0 T_0 (sdtpldt1 (xI) (xJ)))) ### Axiom % 36.70/36.88 28. (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (-. (aElementOf0 T_0 (sdtpldt1 (xI) (xJ)))) ### Axiom % 36.70/36.88 29. (aElement0 T_6) (-. (aElement0 T_6)) ### Axiom % 36.70/36.88 30. (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ))) ### Axiom % 36.70/36.88 31. ((aElementOf0 T_7 (xI)) /\ ((aElementOf0 T_8 (xJ)) /\ ((T_0 = (sdtpldt0 T_7 T_8)) /\ ((aElementOf0 (sdtpldt0 T_9 T_7) (xI)) /\ ((aElementOf0 (sdtpldt0 T_10 T_8) (xJ)) /\ ((aElementOf0 (sdtasdt0 T_6 T_9) (xI)) /\ ((aElementOf0 (sdtasdt0 T_6 T_10) (xJ)) /\ (((sdtpldt0 T_0 T_0) = (sdtpldt0 (sdtpldt0 T_9 T_7) (sdtpldt0 T_10 T_8))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### ConjTree 30 % 36.70/36.88 32. (Ex W6, ((aElementOf0 T_7 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_0 = (sdtpldt0 T_7 W6)) /\ ((aElementOf0 (sdtpldt0 T_9 T_7) (xI)) /\ ((aElementOf0 (sdtpldt0 T_10 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 T_6 T_9) (xI)) /\ ((aElementOf0 (sdtasdt0 T_6 T_10) (xJ)) /\ (((sdtpldt0 T_0 T_0) = (sdtpldt0 (sdtpldt0 T_9 T_7) (sdtpldt0 T_10 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### Exists 31 % 36.70/36.88 33. (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_0 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 T_9 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 T_10 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 T_6 T_9) (xI)) /\ ((aElementOf0 (sdtasdt0 T_6 T_10) (xJ)) /\ (((sdtpldt0 T_0 T_0) = (sdtpldt0 (sdtpldt0 T_9 W5) (sdtpldt0 T_10 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### Exists 32 % 36.70/36.88 34. ((aElementOf0 T_9 (xI)) /\ ((aElementOf0 T_10 (xJ)) /\ ((T_0 = (sdtpldt0 T_9 T_10)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_0 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 T_9 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 T_10 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 T_6 T_9) (xI)) /\ ((aElementOf0 (sdtasdt0 T_6 T_10) (xJ)) /\ (((sdtpldt0 T_0 T_0) = (sdtpldt0 (sdtpldt0 T_9 W5) (sdtpldt0 T_10 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ))))))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### ConjTree 33 % 36.70/36.88 35. (Ex W4, ((aElementOf0 T_9 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((T_0 = (sdtpldt0 T_9 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_0 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 T_9 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 T_6 T_9) (xI)) /\ ((aElementOf0 (sdtasdt0 T_6 W4) (xJ)) /\ (((sdtpldt0 T_0 T_0) = (sdtpldt0 (sdtpldt0 T_9 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))))))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### Exists 34 % 36.70/36.88 36. (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((T_0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_0 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 T_6 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 T_6 W4) (xJ)) /\ (((sdtpldt0 T_0 T_0) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ))))))))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### Exists 35 % 36.70/36.88 37. (((aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) /\ (aElement0 T_6))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((T_0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_0 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 T_6 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 T_6 W4) (xJ)) /\ (((sdtpldt0 T_0 T_0) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))))))))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) (aElement0 T_6) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) ### DisjTree 27 28 29 36 % 36.70/36.88 38. (All W2, (((aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((T_0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((T_0 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 T_0 T_0) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 T_0) (sdtpldt1 (xI) (xJ))))))))))))))))))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (aElement0 T_6) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### All 37 % 36.70/36.89 39. (All W1, (All W2, (((aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((T_0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 T_0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 T_0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 T_0) (sdtpldt1 (xI) (xJ)))))))))))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) (aElement0 T_6) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) ### All 38 % 36.70/36.89 40. (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (aElement0 T_6) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### All 39 % 36.70/36.89 41. (-. ((aElement0 T_6) => (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) ### NotImply 40 % 36.70/36.89 42. (-. (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 T_0) (sdtpldt1 (xI) (xJ)))))) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) ### NotAllEx 41 % 36.70/36.89 43. (-. ((All W2, ((aElementOf0 W2 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 T_0 W2) (sdtpldt1 (xI) (xJ))))) /\ (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 T_0) (sdtpldt1 (xI) (xJ))))))) (aElement0 (sz00)) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) ### NotAnd 26 42 % 36.70/36.89 44. (-. ((aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) => ((All W2, ((aElementOf0 W2 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 T_0 W2) (sdtpldt1 (xI) (xJ))))) /\ (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 T_0) (sdtpldt1 (xI) (xJ)))))))) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (aElement0 (sz00)) ### NotImply 43 % 36.70/36.89 45. (-. (All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => ((All W2, ((aElementOf0 W2 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 W1 W2) (sdtpldt1 (xI) (xJ))))) /\ (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 W1) (sdtpldt1 (xI) (xJ))))))))) (aElement0 (sz00)) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) ### NotAllEx 44 % 36.70/36.89 46. (-. ((aSet0 (sdtpldt1 (xI) (xJ))) /\ (All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => ((All W2, ((aElementOf0 W2 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 W1 W2) (sdtpldt1 (xI) (xJ))))) /\ (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 W1) (sdtpldt1 (xI) (xJ)))))))))) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (aElement0 (sz00)) (aSet0 (xI)) (aSet0 (xJ)) (All W0, (All W1, (((aSet0 W0) /\ (aSet0 W1)) => (All W2, ((W2 = (sdtpldt1 W0 W1)) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 W0) /\ ((aElementOf0 W5 W1) /\ ((sdtpldt0 W4 W5) = W3))))))))))))) ### NotAnd 10 45 % 36.70/36.89 47. ((aSet0 (xJ)) /\ (All W1, ((aElementOf0 W1 (xJ)) => ((All W2, ((aElementOf0 W2 (xJ)) => (aElementOf0 (sdtpldt0 W1 W2) (xJ)))) /\ (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 W1) (xJ)))))))) (All W0, (All W1, (((aSet0 W0) /\ (aSet0 W1)) => (All W2, ((W2 = (sdtpldt1 W0 W1)) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 W0) /\ ((aElementOf0 W5 W1) /\ ((sdtpldt0 W4 W5) = W3))))))))))))) (aSet0 (xI)) (aElement0 (sz00)) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (-. ((aSet0 (sdtpldt1 (xI) (xJ))) /\ (All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => ((All W2, ((aElementOf0 W2 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 W1 W2) (sdtpldt1 (xI) (xJ))))) /\ (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 W1) (sdtpldt1 (xI) (xJ)))))))))) ### And 46 % 36.70/36.89 48. (aIdeal0 (xJ)) (-. ((aSet0 (sdtpldt1 (xI) (xJ))) /\ (All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => ((All W2, ((aElementOf0 W2 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 W1 W2) (sdtpldt1 (xI) (xJ))))) /\ (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 W1) (sdtpldt1 (xI) (xJ)))))))))) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (aElement0 (sz00)) (aSet0 (xI)) (All W0, (All W1, (((aSet0 W0) /\ (aSet0 W1)) => (All W2, ((W2 = (sdtpldt1 W0 W1)) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 W0) /\ ((aElementOf0 W5 W1) /\ ((sdtpldt0 W4 W5) = W3))))))))))))) ### Definition-Pseudo(aIdeal0) 47 % 36.70/36.89 49. ((aSet0 (xI)) /\ (All W1, ((aElementOf0 W1 (xI)) => ((All W2, ((aElementOf0 W2 (xI)) => (aElementOf0 (sdtpldt0 W1 W2) (xI)))) /\ (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 W1) (xI)))))))) (All W0, (All W1, (((aSet0 W0) /\ (aSet0 W1)) => (All W2, ((W2 = (sdtpldt1 W0 W1)) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 W0) /\ ((aElementOf0 W5 W1) /\ ((sdtpldt0 W4 W5) = W3))))))))))))) (aElement0 (sz00)) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (-. ((aSet0 (sdtpldt1 (xI) (xJ))) /\ (All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => ((All W2, ((aElementOf0 W2 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 W1 W2) (sdtpldt1 (xI) (xJ))))) /\ (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 W1) (sdtpldt1 (xI) (xJ)))))))))) (aIdeal0 (xJ)) ### And 48 % 36.70/36.89 50. (aIdeal0 (xI)) (aIdeal0 (xJ)) (-. ((aSet0 (sdtpldt1 (xI) (xJ))) /\ (All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => ((All W2, ((aElementOf0 W2 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 W1 W2) (sdtpldt1 (xI) (xJ))))) /\ (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 W1) (sdtpldt1 (xI) (xJ)))))))))) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (aElement0 (sz00)) (All W0, (All W1, (((aSet0 W0) /\ (aSet0 W1)) => (All W2, ((W2 = (sdtpldt1 W0 W1)) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 W0) /\ ((aElementOf0 W5 W1) /\ ((sdtpldt0 W4 W5) = W3))))))))))))) ### Definition-Pseudo(aIdeal0) 49 % 36.70/36.89 51. ((aIdeal0 (xI)) /\ (aIdeal0 (xJ))) (All W0, (All W1, (((aSet0 W0) /\ (aSet0 W1)) => (All W2, ((W2 = (sdtpldt1 W0 W1)) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 W0) /\ ((aElementOf0 W5 W1) /\ ((sdtpldt0 W4 W5) = W3))))))))))))) (aElement0 (sz00)) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (-. ((aSet0 (sdtpldt1 (xI) (xJ))) /\ (All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => ((All W2, ((aElementOf0 W2 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 W1 W2) (sdtpldt1 (xI) (xJ))))) /\ (All W2, ((aElement0 W2) => (aElementOf0 (sdtasdt0 W2 W1) (sdtpldt1 (xI) (xJ)))))))))) ### And 50 % 36.70/36.89 52. (-. (aIdeal0 (sdtpldt1 (xI) (xJ)))) (All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (aElement0 (sz00)) (All W0, (All W1, (((aSet0 W0) /\ (aSet0 W1)) => (All W2, ((W2 = (sdtpldt1 W0 W1)) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 W0) /\ ((aElementOf0 W5 W1) /\ ((sdtpldt0 W4 W5) = W3))))))))))))) ((aIdeal0 (xI)) /\ (aIdeal0 (xJ))) ### Definition-Pseudo(aIdeal0) 51 % 36.70/36.89 53. (-. ((All W0, (All W1, (All W2, (((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) /\ ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) /\ (aElement0 W2))) => (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((W0 = (sdtpldt0 W3 W4)) /\ (Ex W5, (Ex W6, ((aElementOf0 W5 (xI)) /\ ((aElementOf0 W6 (xJ)) /\ ((W1 = (sdtpldt0 W5 W6)) /\ ((aElementOf0 (sdtpldt0 W3 W5) (xI)) /\ ((aElementOf0 (sdtpldt0 W4 W6) (xJ)) /\ ((aElementOf0 (sdtasdt0 W2 W3) (xI)) /\ ((aElementOf0 (sdtasdt0 W2 W4) (xJ)) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) => (aIdeal0 (sdtpldt1 (xI) (xJ))))) ((aIdeal0 (xI)) /\ (aIdeal0 (xJ))) (All W0, (All W1, (((aSet0 W0) /\ (aSet0 W1)) => (All W2, ((W2 = (sdtpldt1 W0 W1)) <=> ((aSet0 W2) /\ (All W3, ((aElementOf0 W3 W2) <=> (Ex W4, (Ex W5, ((aElementOf0 W4 W0) /\ ((aElementOf0 W5 W1) /\ ((sdtpldt0 W4 W5) = W3))))))))))))) (aElement0 (sz00)) ### NotImply 52 % 36.70/36.89 % SZS output end Proof % 36.70/36.89 (* END-PROOF *) %------------------------------------------------------------------------------