%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : RNG123+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 : n017.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:02 EDT 2022 % Result : Theorem 16.80s 17.00s % Output : Proof 16.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : RNG123+4 : TPTP v8.1.0. Released v4.0.0. % 0.12/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.15/0.35 % Computer : n017.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 600 % 0.15/0.35 % DateTime : Mon May 30 10:50:55 EDT 2022 % 0.15/0.35 % CPUTime : % 16.80/17.00 % SZS status Theorem % 16.80/17.00 (* PROOF-FOUND *) % 16.80/17.00 (* BEGIN-PROOF *) % 16.80/17.00 % SZS output start Proof % 16.80/17.00 1. ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00)) ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) = (sz00)) ### Axiom % 16.80/17.00 2. ((xr) = (sz00)) ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00)) ### Definition-Pseudo(xr) 1 % 16.80/17.00 3. (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI)) (-. (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI))) ### Axiom % 16.80/17.00 4. (aElementOf0 (xb) (xI)) (-. (aElementOf0 (xb) (xI))) ### Axiom % 16.80/17.00 5. (-. (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) (xI))) (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) (xI)) ### Axiom % 16.80/17.00 6. ((aElementOf0 (xb) (xI)) => (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) (xI))) (-. (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) (xI))) (aElementOf0 (xb) (xI)) ### Imply 4 5 % 16.80/17.00 7. (All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) W1) (xI)))) (aElementOf0 (xb) (xI)) (-. (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) (xI))) ### All 6 % 16.80/17.00 8. ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 (smndt0 (sdtasdt0 (xq) (xu)))) (xI))))) (-. (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) (xI))) (aElementOf0 (xb) (xI)) ### And 7 % 16.80/17.00 9. ((aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI)) => ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 (smndt0 (sdtasdt0 (xq) (xu)))) (xI)))))) (aElementOf0 (xb) (xI)) (-. (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) (xI))) (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI)) ### Imply 3 8 % 16.80/17.00 10. (All W0, ((aElementOf0 W0 (xI)) => ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 W0 W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (xI))))))) (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI)) (-. (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) (xI))) (aElementOf0 (xb) (xI)) ### All 9 % 16.80/17.00 11. (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb))))))) (-. (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)))))))) ### Axiom % 16.80/17.00 12. (-. ((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb))))))) \/ (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) (xI)))) (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb))))))) ### NotOr 11 % 16.80/17.00 13. ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00)) ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) = (sz00)) ### Axiom % 16.80/17.00 14. ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb))) ### Refl(=) % 16.80/17.00 15. ((xr) != (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb))) ### Definition-Pseudo(xr) 14 % 16.80/17.00 16. ((sbrdtbr0 (xr)) != (sbrdtbr0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)))) ### NotEqual 15 % 16.80/17.00 17. ((sbrdtbr0 (xu)) != (sbrdtbr0 (xu))) ### Refl(=) % 16.80/17.00 18. (-. (iLess0 (sbrdtbr0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb))) (sbrdtbr0 (xu)))) (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu))) ### P-NotP 16 17 % 16.80/17.00 19. ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb))))))) \/ (aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) (xI))) /\ ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00))) => (-. (iLess0 (sbrdtbr0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb))) (sbrdtbr0 (xu))))) (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu))) ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00)) (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb))))))) ### DisjTree 12 13 18 % 16.80/17.00 20. (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (-. (iLess0 (sbrdtbr0 W0) (sbrdtbr0 (xu)))))) (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb))))))) ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00)) (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu))) ### All 19 % 16.80/17.00 21. ((aElementOf0 (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) (xI)) <=> (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = (sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)))))))) (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu))) ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00)) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (-. (iLess0 (sbrdtbr0 W0) (sbrdtbr0 (xu)))))) (aElementOf0 (xb) (xI)) (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI)) (All W0, ((aElementOf0 W0 (xI)) => ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 W0 W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (xI))))))) ### Equiv 10 20 % 16.80/17.00 22. (All W0, ((aElementOf0 W0 (xI)) <=> (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))))) (All W0, ((aElementOf0 W0 (xI)) => ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 W0 W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (xI))))))) (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI)) (aElementOf0 (xb) (xI)) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (-. (iLess0 (sbrdtbr0 W0) (sbrdtbr0 (xu)))))) ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00)) (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu))) ### All 21 % 16.80/17.00 23. (((xr) = (sz00)) \/ (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu)))) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (-. (iLess0 (sbrdtbr0 W0) (sbrdtbr0 (xu)))))) (aElementOf0 (xb) (xI)) (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI)) (All W0, ((aElementOf0 W0 (xI)) => ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 W0 W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (xI))))))) (All W0, ((aElementOf0 W0 (xI)) <=> (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))))) ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00)) ### Or 2 22 % 16.80/17.00 24. ((aSet0 (xI)) /\ ((All W0, ((aElementOf0 W0 (xI)) => ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 W0 W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (xI))))))) /\ ((aIdeal0 (xI)) /\ ((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))))) /\ ((All W0, ((aElementOf0 W0 (xI)) <=> (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))))) /\ ((xI) = (sdtpldt1 (slsdtgt0 (xa)) (slsdtgt0 (xb)))))))))) ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00)) (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI)) (aElementOf0 (xb) (xI)) (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (-. (iLess0 (sbrdtbr0 W0) (sbrdtbr0 (xu)))))) (((xr) = (sz00)) \/ (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu)))) ### ConjTree 23 % 16.80/17.00 25. ((Ex W0, (Ex W1, ((aElementOf0 W0 (slsdtgt0 (xa))) /\ ((aElementOf0 W1 (slsdtgt0 (xb))) /\ ((sdtpldt0 W0 W1) = (xu)))))) /\ ((aElementOf0 (xu) (xI)) /\ (((xu) != (sz00)) /\ (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (-. (iLess0 (sbrdtbr0 W0) (sbrdtbr0 (xu))))))))) (((xr) = (sz00)) \/ (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu)))) (aElementOf0 (xb) (xI)) (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI)) ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00)) ((aSet0 (xI)) /\ ((All W0, ((aElementOf0 W0 (xI)) => ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 W0 W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (xI))))))) /\ ((aIdeal0 (xI)) /\ ((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))))) /\ ((All W0, ((aElementOf0 W0 (xI)) <=> (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))))) /\ ((xI) = (sdtpldt1 (slsdtgt0 (xa)) (slsdtgt0 (xb)))))))))) ### ConjTree 24 % 16.83/17.01 26. ((aElement0 (xq)) /\ ((aElement0 (xr)) /\ (((xb) = (sdtpldt0 (sdtasdt0 (xq) (xu)) (xr))) /\ (((xr) = (sz00)) \/ (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu))))))) ((aSet0 (xI)) /\ ((All W0, ((aElementOf0 W0 (xI)) => ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 W0 W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (xI))))))) /\ ((aIdeal0 (xI)) /\ ((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))))) /\ ((All W0, ((aElementOf0 W0 (xI)) <=> (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))))) /\ ((xI) = (sdtpldt1 (slsdtgt0 (xa)) (slsdtgt0 (xb)))))))))) ((sdtpldt0 (smndt0 (sdtasdt0 (xq) (xu))) (xb)) != (sz00)) (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI)) (aElementOf0 (xb) (xI)) ((Ex W0, (Ex W1, ((aElementOf0 W0 (slsdtgt0 (xa))) /\ ((aElementOf0 W1 (slsdtgt0 (xb))) /\ ((sdtpldt0 W0 W1) = (xu)))))) /\ ((aElementOf0 (xu) (xI)) /\ (((xu) != (sz00)) /\ (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (-. (iLess0 (sbrdtbr0 W0) (sbrdtbr0 (xu))))))))) ### ConjTree 25 % 16.83/17.01 27. ((xr) != (sz00)) ((Ex W0, (Ex W1, ((aElementOf0 W0 (slsdtgt0 (xa))) /\ ((aElementOf0 W1 (slsdtgt0 (xb))) /\ ((sdtpldt0 W0 W1) = (xu)))))) /\ ((aElementOf0 (xu) (xI)) /\ (((xu) != (sz00)) /\ (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (-. (iLess0 (sbrdtbr0 W0) (sbrdtbr0 (xu))))))))) (aElementOf0 (xb) (xI)) (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI)) ((aSet0 (xI)) /\ ((All W0, ((aElementOf0 W0 (xI)) => ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 W0 W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (xI))))))) /\ ((aIdeal0 (xI)) /\ ((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))))) /\ ((All W0, ((aElementOf0 W0 (xI)) <=> (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))))) /\ ((xI) = (sdtpldt1 (slsdtgt0 (xa)) (slsdtgt0 (xb)))))))))) ((aElement0 (xq)) /\ ((aElement0 (xr)) /\ (((xb) = (sdtpldt0 (sdtasdt0 (xq) (xu)) (xr))) /\ (((xr) = (sz00)) \/ (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu))))))) ### Definition-Pseudo(xr) 26 % 16.83/17.01 28. ((Ex W0, (Ex W1, ((aElementOf0 W0 (slsdtgt0 (xa))) /\ ((aElementOf0 W1 (slsdtgt0 (xb))) /\ ((sdtpldt0 W0 W1) = (smndt0 (sdtasdt0 (xq) (xu)))))))) /\ (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI))) ((aElement0 (xq)) /\ ((aElement0 (xr)) /\ (((xb) = (sdtpldt0 (sdtasdt0 (xq) (xu)) (xr))) /\ (((xr) = (sz00)) \/ (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu))))))) ((aSet0 (xI)) /\ ((All W0, ((aElementOf0 W0 (xI)) => ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 W0 W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (xI))))))) /\ ((aIdeal0 (xI)) /\ ((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))))) /\ ((All W0, ((aElementOf0 W0 (xI)) <=> (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))))) /\ ((xI) = (sdtpldt1 (slsdtgt0 (xa)) (slsdtgt0 (xb)))))))))) (aElementOf0 (xb) (xI)) ((Ex W0, (Ex W1, ((aElementOf0 W0 (slsdtgt0 (xa))) /\ ((aElementOf0 W1 (slsdtgt0 (xb))) /\ ((sdtpldt0 W0 W1) = (xu)))))) /\ ((aElementOf0 (xu) (xI)) /\ (((xu) != (sz00)) /\ (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (-. (iLess0 (sbrdtbr0 W0) (sbrdtbr0 (xu))))))))) ((xr) != (sz00)) ### And 27 % 16.83/17.01 29. ((Ex W0, (Ex W1, ((aElementOf0 W0 (slsdtgt0 (xa))) /\ ((aElementOf0 W1 (slsdtgt0 (xb))) /\ ((sdtpldt0 W0 W1) = (xb)))))) /\ ((Ex W0, (Ex W1, ((aElementOf0 W0 (slsdtgt0 (xa))) /\ ((aElementOf0 W1 (slsdtgt0 (xb))) /\ ((sdtpldt0 W0 W1) = (xb)))))) /\ (aElementOf0 (xb) (xI)))) ((xr) != (sz00)) ((Ex W0, (Ex W1, ((aElementOf0 W0 (slsdtgt0 (xa))) /\ ((aElementOf0 W1 (slsdtgt0 (xb))) /\ ((sdtpldt0 W0 W1) = (xu)))))) /\ ((aElementOf0 (xu) (xI)) /\ (((xu) != (sz00)) /\ (All W0, ((((Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))) \/ (aElementOf0 W0 (xI))) /\ (W0 != (sz00))) => (-. (iLess0 (sbrdtbr0 W0) (sbrdtbr0 (xu))))))))) ((aSet0 (xI)) /\ ((All W0, ((aElementOf0 W0 (xI)) => ((All W1, ((aElementOf0 W1 (xI)) => (aElementOf0 (sdtpldt0 W0 W1) (xI)))) /\ (All W1, ((aElement0 W1) => (aElementOf0 (sdtasdt0 W1 W0) (xI))))))) /\ ((aIdeal0 (xI)) /\ ((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))))) /\ ((All W0, ((aElementOf0 W0 (xI)) <=> (Ex W1, (Ex W2, ((aElementOf0 W1 (slsdtgt0 (xa))) /\ ((aElementOf0 W2 (slsdtgt0 (xb))) /\ ((sdtpldt0 W1 W2) = W0))))))) /\ ((xI) = (sdtpldt1 (slsdtgt0 (xa)) (slsdtgt0 (xb)))))))))) ((aElement0 (xq)) /\ ((aElement0 (xr)) /\ (((xb) = (sdtpldt0 (sdtasdt0 (xq) (xu)) (xr))) /\ (((xr) = (sz00)) \/ (iLess0 (sbrdtbr0 (xr)) (sbrdtbr0 (xu))))))) ((Ex W0, (Ex W1, ((aElementOf0 W0 (slsdtgt0 (xa))) /\ ((aElementOf0 W1 (slsdtgt0 (xb))) /\ ((sdtpldt0 W0 W1) = (smndt0 (sdtasdt0 (xq) (xu)))))))) /\ (aElementOf0 (smndt0 (sdtasdt0 (xq) (xu))) (xI))) ### ConjTree 28 % 16.83/17.01 % SZS output end Proof % 16.83/17.01 (* END-PROOF *) %------------------------------------------------------------------------------