%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : RNG092+2 : 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 : n028.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 0.19s 0.48s % Output : Proof 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : RNG092+2 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon May 30 20:21:50 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.48 % SZS status Theorem % 0.19/0.48 (* PROOF-FOUND *) % 0.19/0.48 (* BEGIN-PROOF *) % 0.19/0.48 % SZS output start Proof % 0.19/0.48 1. (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (-. (aElementOf0 T_0 (sdtpldt1 (xI) (xJ)))) ### Axiom % 0.19/0.48 2. (-. ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_0))))) \/ (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) ### NotOr 1 % 0.19/0.48 3. (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) (-. (aElementOf0 T_1 (sdtpldt1 (xI) (xJ)))) ### Axiom % 0.19/0.48 4. (-. ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_1))))) \/ (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))))) (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) ### NotOr 3 % 0.19/0.48 5. (aElement0 (sz10)) (-. (aElement0 (sz10))) ### Axiom % 0.19/0.48 6. (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) ### Axiom % 0.19/0.48 7. ((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 (sz10) T_4) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz10) T_5) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 T_4 T_2) (sdtpldt0 T_5 T_3))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtpldt0 T_0 T_1)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 (sz10) T_0)))))) /\ (aElementOf0 (sdtasdt0 (sz10) T_0) (sdtpldt1 (xI) (xJ)))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### ConjTree 6 % 0.19/0.48 8. (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 (sz10) T_4) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz10) T_5) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 T_4 T_2) (sdtpldt0 T_5 W6))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtpldt0 T_0 T_1)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 (sz10) T_0)))))) /\ (aElementOf0 (sdtasdt0 (sz10) T_0) (sdtpldt1 (xI) (xJ))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### Exists 7 % 0.19/0.48 9. (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 (sz10) T_4) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz10) T_5) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 T_4 W5) (sdtpldt0 T_5 W6))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtpldt0 T_0 T_1)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 (sz10) T_0)))))) /\ (aElementOf0 (sdtasdt0 (sz10) T_0) (sdtpldt1 (xI) (xJ)))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### Exists 8 % 0.19/0.48 10. ((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 (sz10) T_4) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz10) T_5) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 T_4 W5) (sdtpldt0 T_5 W6))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtpldt0 T_0 T_1)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 (sz10) T_0)))))) /\ (aElementOf0 (sdtasdt0 (sz10) T_0) (sdtpldt1 (xI) (xJ))))))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### ConjTree 9 % 0.19/0.48 11. (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 (sz10) T_4) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz10) W4) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 T_4 W5) (sdtpldt0 W4 W6))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtpldt0 T_0 T_1)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 (sz10) T_0)))))) /\ (aElementOf0 (sdtasdt0 (sz10) T_0) (sdtpldt1 (xI) (xJ)))))))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### Exists 10 % 0.19/0.48 12. (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 (sz10) W3) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz10) W4) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtpldt0 T_0 T_1)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 (sz10) T_0)))))) /\ (aElementOf0 (sdtasdt0 (sz10) T_0) (sdtpldt1 (xI) (xJ))))))))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### Exists 11 % 0.19/0.48 13. ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_0))))) \/ (aElementOf0 T_0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_1))))) \/ (aElementOf0 T_1 (sdtpldt1 (xI) (xJ)))) /\ (aElement0 (sz10)))) => (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 (sz10) W3) (xI)) /\ ((aElementOf0 (sdtasdt0 (sz10) W4) (xJ)) /\ (((sdtpldt0 T_0 T_1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtpldt0 T_0 T_1)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 (sz10) T_0)))))) /\ (aElementOf0 (sdtasdt0 (sz10) T_0) (sdtpldt1 (xI) (xJ)))))))))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) (aElement0 (sz10)) (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) ### DisjTree 2 4 5 12 % 0.19/0.48 14. (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_0))))) \/ (aElementOf0 T_0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_1))))) \/ (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))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtpldt0 T_0 T_1)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 T_0)))))) /\ (aElementOf0 (sdtasdt0 W2 T_0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) (aElement0 (sz10)) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### All 13 % 0.19/0.48 15. (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_0))))) \/ (aElementOf0 T_0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 T_0 W1)))))) /\ ((aElementOf0 (sdtpldt0 T_0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 T_0)))))) /\ (aElementOf0 (sdtasdt0 W2 T_0) (sdtpldt1 (xI) (xJ)))))))))))))))))))))))) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) (aElement0 (sz10)) (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) ### All 14 % 0.19/0.48 16. (All W0, (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W0))))) \/ (aElementOf0 W0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 W0 W1)))))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 W0)))))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) (aElement0 (sz10)) (-. (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ)))) ### All 15 % 0.19/0.48 17. (-. ((aElementOf0 T_1 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 T_0 T_1) (sdtpldt1 (xI) (xJ))))) (aElement0 (sz10)) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (All W0, (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W0))))) \/ (aElementOf0 W0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 W0 W1)))))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 W0)))))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))))) ### NotImply 16 % 0.19/0.48 18. (-. (All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 T_0 W1) (sdtpldt1 (xI) (xJ)))))) (All W0, (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W0))))) \/ (aElementOf0 W0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 W0 W1)))))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 W0)))))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (aElement0 (sz10)) ### NotAllEx 17 % 0.19/0.48 19. (aElement0 T_6) (-. (aElement0 T_6)) ### Axiom % 0.19/0.48 20. (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ))) ### Axiom % 0.19/0.48 21. ((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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 T_0 T_0)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtasdt0 T_6 T_0)))))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### ConjTree 20 % 0.19/0.48 22. (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 T_0 T_0)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtasdt0 T_6 T_0)))))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ))))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### Exists 21 % 0.19/0.48 23. (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 T_0 T_0)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtasdt0 T_6 T_0)))))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### Exists 22 % 0.19/0.48 24. ((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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 T_0 T_0)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtasdt0 T_6 T_0)))))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ))))))))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### ConjTree 23 % 0.19/0.49 25. (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 T_0 T_0)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtasdt0 T_6 T_0)))))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))))))))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### Exists 24 % 0.19/0.49 26. (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 T_0 T_0)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtasdt0 T_6 T_0)))))) /\ (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ))))))))))))))))))))) (-. (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ)))) ### Exists 25 % 0.19/0.49 27. ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_0))))) \/ (aElementOf0 T_0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_0))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 T_0 T_0)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ ((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = (sdtasdt0 T_6 T_0)))))) /\ (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 2 2 19 26 % 0.19/0.49 28. (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_0))))) \/ (aElementOf0 T_0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_0))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 T_0 T_0)))))) /\ ((aElementOf0 (sdtpldt0 T_0 T_0) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 T_0)))))) /\ (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 27 % 0.19/0.49 29. (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = T_0))))) \/ (aElementOf0 T_0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 T_0 W1)))))) /\ ((aElementOf0 (sdtpldt0 T_0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 T_0)))))) /\ (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 28 % 0.19/0.49 30. (All W0, (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W0))))) \/ (aElementOf0 W0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 W0 W1)))))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 W0)))))) /\ (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 29 % 0.19/0.49 31. (-. ((aElement0 T_6) => (aElementOf0 (sdtasdt0 T_6 T_0) (sdtpldt1 (xI) (xJ))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (All W0, (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W0))))) \/ (aElementOf0 W0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 W0 W1)))))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 W0)))))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))))) ### NotImply 30 % 0.19/0.49 32. (-. (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 T_0) (sdtpldt1 (xI) (xJ)))))) (All W0, (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W0))))) \/ (aElementOf0 W0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 W0 W1)))))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 W0)))))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))))) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) ### NotAllEx 31 % 0.19/0.49 33. (-. ((All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 T_0 W1) (sdtpldt1 (xI) (xJ))))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 T_0) (sdtpldt1 (xI) (xJ))))))) (aElement0 (sz10)) (aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) (All W0, (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W0))))) \/ (aElementOf0 W0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 W0 W1)))))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 W0)))))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))))) ### NotAnd 18 32 % 0.19/0.49 34. (-. ((aElementOf0 T_0 (sdtpldt1 (xI) (xJ))) => ((All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 T_0 W1) (sdtpldt1 (xI) (xJ))))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 T_0) (sdtpldt1 (xI) (xJ)))))))) (All W0, (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W0))))) \/ (aElementOf0 W0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 W0 W1)))))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 W0)))))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))))) (aElement0 (sz10)) ### NotImply 33 % 0.19/0.49 35. (-. (All W0, ((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) => ((All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (sdtpldt1 (xI) (xJ))))))))) (aElement0 (sz10)) (All W0, (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W0))))) \/ (aElementOf0 W0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 W0 W1)))))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 W0)))))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))))) ### NotAllEx 34 % 0.19/0.49 36. (-. ((All W0, (All W1, (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W0))))) \/ (aElementOf0 W0 (sdtpldt1 (xI) (xJ)))) /\ (((Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W1))))) \/ (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))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtpldt0 W0 W1)))))) /\ ((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))) /\ ((Ex W7, (Ex W8, ((aElementOf0 W7 (xI)) /\ ((aElementOf0 W8 (xJ)) /\ ((sdtpldt0 W7 W8) = (sdtasdt0 W2 W0)))))) /\ (aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ))))))))))))))))))))))))) => (((aSet0 (sdtpldt1 (xI) (xJ))) /\ (All W0, ((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) <=> (Ex W3, (Ex W4, ((aElementOf0 W3 (xI)) /\ ((aElementOf0 W4 (xJ)) /\ ((sdtpldt0 W3 W4) = W0)))))))) => ((All W0, ((aElementOf0 W0 (sdtpldt1 (xI) (xJ))) => ((All W1, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ))) => (aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ))))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (sdtpldt1 (xI) (xJ)))))))) \/ (aIdeal0 (sdtpldt1 (xI) (xJ))))))) (aElement0 (sz10)) ### ConjTree 35 % 0.19/0.49 % SZS output end Proof % 0.19/0.49 (* END-PROOF *) %------------------------------------------------------------------------------