%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : RNG112+4 : 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 : n019.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:42:01 EDT 2022 % Result : Theorem 2.64s 2.85s % Output : Proof 2.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : RNG112+4 : 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 : n019.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 05:25:55 EDT 2022 % 0.12/0.33 % CPUTime : % 2.64/2.85 % SZS status Theorem % 2.64/2.85 (* PROOF-FOUND *) % 2.64/2.85 (* BEGIN-PROOF *) % 2.64/2.85 % SZS output start Proof % 2.64/2.85 1. (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = T_0))))) (-. (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = T_0)))))) ### Axiom % 2.64/2.85 2. (-. ((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = T_0))))) \/ (aElementOf0 T_0 (xI)))) (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = T_0))))) ### NotOr 1 % 2.64/2.85 3. (T_0 != (sz00)) (T_0 = (sz00)) ### Axiom % 2.64/2.85 4. (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_1))))) (-. (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_1)))))) ### Axiom % 2.64/2.85 5. (-. ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_1))))) \/ (aElementOf0 T_1 (xI)))) (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_1))))) ### NotOr 4 % 2.64/2.85 6. (T_1 != (sz00)) (T_1 = (sz00)) ### Axiom % 2.64/2.85 7. (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_2))))) (-. (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_2)))))) ### Axiom % 2.64/2.85 8. (-. ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_2))))) \/ (aElementOf0 T_2 (xI)))) (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_2))))) ### NotOr 7 % 2.64/2.85 9. (T_2 != (sz00)) (T_2 = (sz00)) ### Axiom % 2.64/2.85 10. (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_3))))) (-. (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_3)))))) ### Axiom % 2.64/2.85 11. (-. ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_3))))) \/ (aElementOf0 T_3 (xI)))) (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_3))))) ### NotOr 10 % 2.64/2.85 12. (T_3 != (sz00)) (T_3 = (sz00)) ### Axiom % 2.64/2.85 13. (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_4))))) (-. (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_4)))))) ### Axiom % 2.64/2.85 14. (-. ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_4))))) \/ (aElementOf0 T_4 (xI)))) (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_4))))) ### NotOr 13 % 2.64/2.85 15. (T_4 != (sz00)) (T_4 = (sz00)) ### Axiom % 2.64/2.85 16. (iLess0 (sbrdtbr0 T_4) (sbrdtbr0 T_3)) (-. (iLess0 (sbrdtbr0 T_4) (sbrdtbr0 T_3))) ### Axiom % 2.64/2.85 17. ((((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_4))))) \/ (aElementOf0 T_4 (xI))) /\ (T_4 != (sz00))) => (-. (iLess0 (sbrdtbr0 T_4) (sbrdtbr0 T_3)))) (iLess0 (sbrdtbr0 T_4) (sbrdtbr0 T_3)) (T_4 != (sz00)) (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_4))))) ### DisjTree 14 15 16 % 2.64/2.85 18. (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 T_3))))) (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_4))))) (T_4 != (sz00)) (iLess0 (sbrdtbr0 T_4) (sbrdtbr0 T_3)) ### All 17 % 2.64/2.85 19. (-. (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_4))))) /\ ((aElementOf0 T_4 (xI)) /\ (T_4 != (sz00)))) => (-. (iLess0 (sbrdtbr0 T_4) (sbrdtbr0 T_3))))) (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 T_3))))) ### ConjTree 18 % 2.64/2.85 20. (-. (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 T_3)))))) (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 T_3))))) ### NotAllEx 19 % 2.64/2.85 21. (-. (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_3))))) \/ (aElementOf0 T_3 (xI))) /\ ((T_3 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 T_3)))))))) (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 T_3))))) (T_3 != (sz00)) (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_3))))) ### DisjTree 11 12 20 % 2.64/2.85 22. (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_3))))) (T_3 != (sz00)) (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 T_3))))) ### NotExists 21 % 2.64/2.85 23. ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_3))))) /\ ((aElementOf0 T_3 (xI)) /\ ((T_3 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 T_3)))))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) ### ConjTree 22 % 2.64/2.85 24. (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) ### Exists 23 % 2.64/2.85 25. ((((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_2))))) \/ (aElementOf0 T_2 (xI))) /\ (T_2 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1)))))))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) (T_2 != (sz00)) (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_2))))) ### DisjTree 8 9 24 % 2.64/2.87 26. (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))))) (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_2))))) (T_2 != (sz00)) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) ### All 25 % 2.64/2.87 27. (-. (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_2))))) /\ ((aElementOf0 T_2 (xI)) /\ (T_2 != (sz00)))) => (-. (iLess0 (sbrdtbr0 T_2) (sbrdtbr0 T_1))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))))) ### ConjTree 26 % 2.64/2.87 28. (-. (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 T_1)))))) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) ### NotAllEx 27 % 2.64/2.87 29. (-. (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_1))))) \/ (aElementOf0 T_1 (xI))) /\ ((T_1 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 T_1)))))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))))) (T_1 != (sz00)) (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_1))))) ### DisjTree 5 6 28 % 2.64/2.87 30. (Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_1))))) (T_1 != (sz00)) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) ### NotExists 29 % 2.64/2.87 31. (-. (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = T_1))))) /\ ((aElementOf0 T_1 (xI)) /\ (T_1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 T_1) (sbrdtbr0 T_0))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))))) ### ConjTree 30 % 2.64/2.88 32. (-. (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 T_0)))))) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) ### NotAllEx 31 % 2.64/2.88 33. (-. (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = T_0))))) \/ (aElementOf0 T_0 (xI))) /\ ((T_0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 T_0)))))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))))) (T_0 != (sz00)) (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = T_0))))) ### DisjTree 2 3 32 % 2.64/2.88 34. (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = T_0))))) (T_0 != (sz00)) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) ### NotExists 33 % 2.64/2.88 35. ((All W0, ((aElementOf0 W0 (slsdtgt0 (xa))) <=> (Ex W1, ((aElement0 W1) /\ ((sdtasdt0 (xa) W1) = W0))))) /\ ((All W0, ((aElementOf0 W0 (slsdtgt0 (xb))) <=> (Ex W1, ((aElement0 W1) /\ ((sdtasdt0 (xb) W1) = W0))))) /\ ((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = T_0))))) /\ ((aElementOf0 T_0 (sdtpldt1 (slsdtgt0 (xa)) (slsdtgt0 (xb)))) /\ (T_0 != (sz00)))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))))) ### ConjTree 34 % 2.64/2.88 36. (Ex W0, ((All W0, ((aElementOf0 W0 (slsdtgt0 (xa))) <=> (Ex W1, ((aElement0 W1) /\ ((sdtasdt0 (xa) W1) = W0))))) /\ ((All W0, ((aElementOf0 W0 (slsdtgt0 (xb))) <=> (Ex W1, ((aElement0 W1) /\ ((sdtasdt0 (xb) W1) = W0))))) /\ ((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) /\ ((aElementOf0 W0 (sdtpldt1 (slsdtgt0 (xa)) (slsdtgt0 (xb)))) /\ (W0 != (sz00))))))) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (Ex W1, ((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ ((W1 != (sz00)) /\ (All W2, ((((Ex W3, (Ex W4, ((aElementOf0 W3 (slsdtgt0 (xa))) /\ ((aElementOf0 W4 (slsdtgt0 (xb))) /\ ((sdtpldt0 W3 W4) = W2))))) \/ (aElementOf0 W2 (xI))) /\ (W2 != (sz00))) => (-. (iLess0 (sbrdtbr0 W2) (sbrdtbr0 W1))))))))))) (-. (Ex W0, (((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ ((W0 != (sz00)) /\ (All W1, (((Ex W2, (Ex W3, ((aElementOf0 W2 (slsdtgt0 (xa))) /\ ((aElementOf0 W3 (slsdtgt0 (xb))) /\ ((sdtpldt0 W2 W3) = W1))))) /\ ((aElementOf0 W1 (xI)) /\ (W1 != (sz00)))) => (-. (iLess0 (sbrdtbr0 W1) (sbrdtbr0 W0))))))))) ### Exists 35 % 2.64/2.88 % SZS output end Proof % 2.64/2.88 (* END-PROOF *) %------------------------------------------------------------------------------