%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM012+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 : n020.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 : Fri Jul 15 01:45:49 EDT 2022 % Result : Theorem 0.20s 0.41s % Output : Proof 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : COM012+1 : 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 : n020.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 : Thu Jun 16 19:43:49 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.41 % SZS status Theorem % 0.20/0.41 (* PROOF-FOUND *) % 0.20/0.41 (* BEGIN-PROOF *) % 0.20/0.41 % SZS output start Proof % 0.20/0.41 1. (aElement0 (xx)) (-. (aElement0 (xx))) ### Axiom % 0.20/0.41 2. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 0.20/0.41 3. (aElement0 (xz)) (-. (aElement0 (xz))) ### Axiom % 0.20/0.41 4. ((xx) != (xx)) ### NotEqual % 0.20/0.41 5. ((xR) != (xR)) ### NotEqual % 0.20/0.41 6. (aElement0 (xx)) (-. (aElement0 (xx))) ### Axiom % 0.20/0.41 7. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 0.20/0.41 8. (aElement0 (xy)) (-. (aElement0 (xy))) ### Axiom % 0.20/0.41 9. (aElement0 (xz)) (-. (aElement0 (xz))) ### Axiom % 0.20/0.41 10. (aElement0 (xx)) (-. (aElement0 (xx))) ### Axiom % 0.20/0.41 11. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 0.20/0.41 12. (aElement0 (xy)) (-. (aElement0 (xy))) ### Axiom % 0.20/0.41 13. (sdtmndtasgtdt0 (xx) (xR) (xy)) (-. (sdtmndtasgtdt0 (xx) (xR) (xy))) ### Axiom % 0.20/0.41 14. ((xy) != (xx)) ((xx) = (xy)) ### Sym(=) % 0.20/0.41 15. (-. (sdtmndtplgtdt0 (xx) (xR) (xy))) (sdtmndtplgtdt0 (xx) (xR) (xy)) ### Axiom % 0.20/0.41 16. (((xx) = (xy)) \/ (sdtmndtplgtdt0 (xx) (xR) (xy))) (-. (sdtmndtplgtdt0 (xx) (xR) (xy))) ((xy) != (xx)) ### Or 14 15 % 0.20/0.41 17. ((sdtmndtasgtdt0 (xx) (xR) (xy)) <=> (((xx) = (xy)) \/ (sdtmndtplgtdt0 (xx) (xR) (xy)))) ((xy) != (xx)) (-. (sdtmndtplgtdt0 (xx) (xR) (xy))) (sdtmndtasgtdt0 (xx) (xR) (xy)) ### Equiv 13 16 % 0.20/0.41 18. (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 (xy)))) => ((sdtmndtasgtdt0 (xx) (xR) (xy)) <=> (((xx) = (xy)) \/ (sdtmndtplgtdt0 (xx) (xR) (xy))))) (sdtmndtasgtdt0 (xx) (xR) (xy)) (-. (sdtmndtplgtdt0 (xx) (xR) (xy))) ((xy) != (xx)) (aElement0 (xy)) (aRewritingSystem0 (xR)) (aElement0 (xx)) ### DisjTree 10 11 12 17 % 0.20/0.41 19. (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) (aElement0 (xx)) (aRewritingSystem0 (xR)) (aElement0 (xy)) ((xy) != (xx)) (-. (sdtmndtplgtdt0 (xx) (xR) (xy))) (sdtmndtasgtdt0 (xx) (xR) (xy)) ### All 18 % 0.20/0.41 20. (aElement0 (xy)) (-. (aElement0 (xy))) ### Axiom % 0.20/0.41 21. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 0.20/0.41 22. (aElement0 (xz)) (-. (aElement0 (xz))) ### Axiom % 0.20/0.41 23. (sdtmndtasgtdt0 (xy) (xR) (xz)) (-. (sdtmndtasgtdt0 (xy) (xR) (xz))) ### Axiom % 0.20/0.41 24. ((xy) != (xz)) ((xy) = (xz)) ### Axiom % 0.20/0.41 25. (-. (sdtmndtplgtdt0 (xy) (xR) (xz))) (sdtmndtplgtdt0 (xy) (xR) (xz)) ### Axiom % 0.20/0.41 26. (((xy) = (xz)) \/ (sdtmndtplgtdt0 (xy) (xR) (xz))) (-. (sdtmndtplgtdt0 (xy) (xR) (xz))) ((xy) != (xz)) ### Or 24 25 % 0.20/0.41 27. ((sdtmndtasgtdt0 (xy) (xR) (xz)) <=> (((xy) = (xz)) \/ (sdtmndtplgtdt0 (xy) (xR) (xz)))) ((xy) != (xz)) (-. (sdtmndtplgtdt0 (xy) (xR) (xz))) (sdtmndtasgtdt0 (xy) (xR) (xz)) ### Equiv 23 26 % 0.20/0.41 28. (((aElement0 (xy)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 (xz)))) => ((sdtmndtasgtdt0 (xy) (xR) (xz)) <=> (((xy) = (xz)) \/ (sdtmndtplgtdt0 (xy) (xR) (xz))))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (-. (sdtmndtplgtdt0 (xy) (xR) (xz))) ((xy) != (xz)) (aElement0 (xz)) (aRewritingSystem0 (xR)) (aElement0 (xy)) ### DisjTree 20 21 22 27 % 0.20/0.41 29. (All W2, (((aElement0 (xy)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xy) (xR) W2) <=> (((xy) = W2) \/ (sdtmndtplgtdt0 (xy) (xR) W2))))) (aElement0 (xy)) (aRewritingSystem0 (xR)) (aElement0 (xz)) ((xy) != (xz)) (-. (sdtmndtplgtdt0 (xy) (xR) (xz))) (sdtmndtasgtdt0 (xy) (xR) (xz)) ### All 28 % 0.20/0.41 30. (All W1, (All W2, (((aElement0 (xy)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xy) W1 W2) <=> (((xy) = W2) \/ (sdtmndtplgtdt0 (xy) W1 W2)))))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (-. (sdtmndtplgtdt0 (xy) (xR) (xz))) ((xy) != (xz)) (aElement0 (xz)) (aRewritingSystem0 (xR)) (aElement0 (xy)) ### All 29 % 0.20/0.41 31. (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xy)) (aRewritingSystem0 (xR)) (aElement0 (xz)) ((xy) != (xz)) (-. (sdtmndtplgtdt0 (xy) (xR) (xz))) (sdtmndtasgtdt0 (xy) (xR) (xz)) ### All 30 % 0.20/0.41 32. (-. (sdtmndtplgtdt0 (xx) (xR) (xz))) (sdtmndtplgtdt0 (xx) (xR) (xz)) ### Axiom % 0.20/0.41 33. (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 (xy)) /\ (aElement0 (xz))))) => (((sdtmndtplgtdt0 (xx) (xR) (xy)) /\ (sdtmndtplgtdt0 (xy) (xR) (xz))) => (sdtmndtplgtdt0 (xx) (xR) (xz)))) (-. (sdtmndtplgtdt0 (xx) (xR) (xz))) (sdtmndtasgtdt0 (xy) (xR) (xz)) ((xy) != (xz)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xx) (xR) (xy)) ((xy) != (xx)) (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) (aElement0 (xz)) (aElement0 (xy)) (aRewritingSystem0 (xR)) (aElement0 (xx)) ### DisjTree 6 7 8 9 19 31 32 % 0.20/0.41 34. (All W3, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 (xy)) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 (xx) (xR) (xy)) /\ (sdtmndtplgtdt0 (xy) (xR) W3)) => (sdtmndtplgtdt0 (xx) (xR) W3)))) (aElement0 (xx)) (aRewritingSystem0 (xR)) (aElement0 (xy)) (aElement0 (xz)) (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) ((xy) != (xx)) (sdtmndtasgtdt0 (xx) (xR) (xy)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) ((xy) != (xz)) (sdtmndtasgtdt0 (xy) (xR) (xz)) (-. (sdtmndtplgtdt0 (xx) (xR) (xz))) ### All 33 % 0.20/0.41 35. (All W2, (All W3, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 (xx) (xR) W2) /\ (sdtmndtplgtdt0 W2 (xR) W3)) => (sdtmndtplgtdt0 (xx) (xR) W3))))) (-. (sdtmndtplgtdt0 (xx) (xR) (xz))) (sdtmndtasgtdt0 (xy) (xR) (xz)) ((xy) != (xz)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xx) (xR) (xy)) ((xy) != (xx)) (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) (aElement0 (xz)) (aElement0 (xy)) (aRewritingSystem0 (xR)) (aElement0 (xx)) ### All 34 % 0.20/0.41 36. (-. (sdtmndtasgtdt0 (xx) (xR) (xz))) (aElement0 (xx)) (aRewritingSystem0 (xR)) (aElement0 (xy)) (aElement0 (xz)) (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) ((xy) != (xx)) (sdtmndtasgtdt0 (xx) (xR) (xy)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (-. (sdtmndtplgtdt0 (xx) (xR) (xz))) (All W2, (All W3, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 (xx) (xR) W2) /\ (sdtmndtplgtdt0 W2 (xR) W3)) => (sdtmndtplgtdt0 (xx) (xR) W3))))) ### P-NotP 4 5 35 % 0.20/0.41 37. ((xz) != (xz)) ### NotEqual % 0.20/0.41 38. (All W2, (All W3, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 (xx) (xR) W2) /\ (sdtmndtplgtdt0 W2 (xR) W3)) => (sdtmndtplgtdt0 (xx) (xR) W3))))) (-. (sdtmndtplgtdt0 (xx) (xR) (xz))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xx) (xR) (xy)) (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) (aElement0 (xz)) (aElement0 (xy)) (aRewritingSystem0 (xR)) (aElement0 (xx)) (-. (sdtmndtasgtdt0 (xx) (xR) (xz))) ### P-NotP 36 5 37 % 0.20/0.41 39. (All W1, (All W2, (All W3, (((aElement0 (xx)) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 (xx) W1 W2) /\ (sdtmndtplgtdt0 W2 W1 W3)) => (sdtmndtplgtdt0 (xx) W1 W3)))))) (-. (sdtmndtasgtdt0 (xx) (xR) (xz))) (aElement0 (xx)) (aRewritingSystem0 (xR)) (aElement0 (xy)) (aElement0 (xz)) (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) (sdtmndtasgtdt0 (xx) (xR) (xy)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (-. (sdtmndtplgtdt0 (xx) (xR) (xz))) ### All 38 % 0.20/0.42 40. (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 W0 W1 W2) /\ (sdtmndtplgtdt0 W2 W1 W3)) => (sdtmndtplgtdt0 W0 W1 W3))))))) (-. (sdtmndtplgtdt0 (xx) (xR) (xz))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xx) (xR) (xy)) (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) (aElement0 (xz)) (aElement0 (xy)) (aRewritingSystem0 (xR)) (aElement0 (xx)) (-. (sdtmndtasgtdt0 (xx) (xR) (xz))) ### All 39 % 0.20/0.42 41. (-. (((xx) = (xz)) \/ (sdtmndtplgtdt0 (xx) (xR) (xz)))) (-. (sdtmndtasgtdt0 (xx) (xR) (xz))) (aElement0 (xx)) (aRewritingSystem0 (xR)) (aElement0 (xy)) (aElement0 (xz)) (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) (sdtmndtasgtdt0 (xx) (xR) (xy)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 W0 W1 W2) /\ (sdtmndtplgtdt0 W2 W1 W3)) => (sdtmndtplgtdt0 W0 W1 W3))))))) ### NotOr 40 % 0.20/0.42 42. (-. (sdtmndtasgtdt0 (xx) (xR) (xz))) (sdtmndtasgtdt0 (xx) (xR) (xz)) ### Axiom % 0.20/0.42 43. ((sdtmndtasgtdt0 (xx) (xR) (xz)) <=> (((xx) = (xz)) \/ (sdtmndtplgtdt0 (xx) (xR) (xz)))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 W0 W1 W2) /\ (sdtmndtplgtdt0 W2 W1 W3)) => (sdtmndtplgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xx) (xR) (xy)) (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) (aElement0 (xz)) (aElement0 (xy)) (aRewritingSystem0 (xR)) (aElement0 (xx)) (-. (sdtmndtasgtdt0 (xx) (xR) (xz))) ### Equiv 41 42 % 0.20/0.42 44. (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 (xz)))) => ((sdtmndtasgtdt0 (xx) (xR) (xz)) <=> (((xx) = (xz)) \/ (sdtmndtplgtdt0 (xx) (xR) (xz))))) (-. (sdtmndtasgtdt0 (xx) (xR) (xz))) (aElement0 (xy)) (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) (sdtmndtasgtdt0 (xx) (xR) (xy)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 W0 W1 W2) /\ (sdtmndtplgtdt0 W2 W1 W3)) => (sdtmndtplgtdt0 W0 W1 W3))))))) (aElement0 (xz)) (aRewritingSystem0 (xR)) (aElement0 (xx)) ### DisjTree 1 2 3 43 % 0.20/0.42 45. (aElement0 (xx)) (aRewritingSystem0 (xR)) (aElement0 (xz)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 W0 W1 W2) /\ (sdtmndtplgtdt0 W2 W1 W3)) => (sdtmndtplgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xx) (xR) (xy)) (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) (xR) W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) (xR) W2))))) (aElement0 (xy)) (-. (sdtmndtasgtdt0 (xx) (xR) (xz))) ### All 44 % 0.20/0.42 46. (All W1, (All W2, (((aElement0 (xx)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xx) W1 W2) <=> (((xx) = W2) \/ (sdtmndtplgtdt0 (xx) W1 W2)))))) (-. (sdtmndtasgtdt0 (xx) (xR) (xz))) (aElement0 (xy)) (sdtmndtasgtdt0 (xx) (xR) (xy)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 W0 W1 W2) /\ (sdtmndtplgtdt0 W2 W1 W3)) => (sdtmndtplgtdt0 W0 W1 W3))))))) (aElement0 (xz)) (aRewritingSystem0 (xR)) (aElement0 (xx)) ### All 45 % 0.20/0.42 47. (aElement0 (xx)) (aRewritingSystem0 (xR)) (aElement0 (xz)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 W0 W1 W2) /\ (sdtmndtplgtdt0 W2 W1 W3)) => (sdtmndtplgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xy) (xR) (xz)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xx) (xR) (xy)) (aElement0 (xy)) (-. (sdtmndtasgtdt0 (xx) (xR) (xz))) ### All 46 % 0.20/0.42 48. (-. (((sdtmndtasgtdt0 (xx) (xR) (xy)) /\ (sdtmndtasgtdt0 (xy) (xR) (xz))) => (sdtmndtasgtdt0 (xx) (xR) (xz)))) (aElement0 (xy)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 W0 W1 W2) /\ (sdtmndtplgtdt0 W2 W1 W3)) => (sdtmndtplgtdt0 W0 W1 W3))))))) (aElement0 (xz)) (aRewritingSystem0 (xR)) (aElement0 (xx)) ### ConjTree 47 % 0.20/0.42 49. ((aElement0 (xx)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 (xy)) /\ (aElement0 (xz))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtplgtdt0 W0 W1 W2) /\ (sdtmndtplgtdt0 W2 W1 W3)) => (sdtmndtplgtdt0 W0 W1 W3))))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (-. (((sdtmndtasgtdt0 (xx) (xR) (xy)) /\ (sdtmndtasgtdt0 (xy) (xR) (xz))) => (sdtmndtasgtdt0 (xx) (xR) (xz)))) ### ConjTree 48 % 0.20/0.42 % SZS output end Proof % 0.20/0.42 (* END-PROOF *) %------------------------------------------------------------------------------