%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM022+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 : n003.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:54 EDT 2022 % Result : Theorem 28.27s 28.43s % Output : Proof 28.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : COM022+1 : TPTP v8.1.0. Released v4.0.0. % 0.12/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.33 % Computer : n003.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Thu Jun 16 19:57:12 EDT 2022 % 0.13/0.33 % CPUTime : % 28.27/28.43 % SZS status Theorem % 28.27/28.43 (* PROOF-FOUND *) % 28.27/28.43 (* BEGIN-PROOF *) % 28.27/28.43 % SZS output start Proof % 28.27/28.43 1. (aElement0 (xc)) (-. (aElement0 (xc))) ### Axiom % 28.27/28.43 2. (aElement0 (xa)) (-. (aElement0 (xa))) ### Axiom % 28.27/28.43 3. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 28.27/28.43 4. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 28.27/28.43 5. (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtasgtdt0 (xa) (xR) (xb))) ### Axiom % 28.27/28.43 6. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 28.27/28.43 7. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 28.27/28.43 8. (aElement0 (xa)) (-. (aElement0 (xa))) ### Axiom % 28.27/28.43 9. ((xa) = (xb)) ((xb) != (xa)) ### Sym(=) % 28.27/28.43 10. (-. (((xb) = (xa)) \/ (sdtmndtplgtdt0 (xb) (xR) (xa)))) ((xa) = (xb)) ### NotOr 9 % 28.27/28.43 11. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 28.27/28.43 12. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 28.27/28.43 13. (aElement0 (xa)) (-. (aElement0 (xa))) ### Axiom % 28.27/28.43 14. (aElement0 (xc)) (-. (aElement0 (xc))) ### Axiom % 28.27/28.43 15. (sdtmndtasgtdt0 (xb) (xR) (xa)) (-. (sdtmndtasgtdt0 (xb) (xR) (xa))) ### Axiom % 28.27/28.43 16. (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtasgtdt0 (xa) (xR) (xc))) ### Axiom % 28.27/28.43 17. (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (sdtmndtasgtdt0 (xb) (xR) (xc)) ### Axiom % 28.27/28.43 18. (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 (xa)) /\ (aElement0 (xc))))) => (((sdtmndtasgtdt0 (xb) (xR) (xa)) /\ (sdtmndtasgtdt0 (xa) (xR) (xc))) => (sdtmndtasgtdt0 (xb) (xR) (xc)))) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (sdtmndtasgtdt0 (xb) (xR) (xa)) (aElement0 (xc)) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) ### DisjTree 11 12 13 14 15 16 17 % 28.27/28.43 19. (All W3, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 (xa)) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xb) (xR) (xa)) /\ (sdtmndtasgtdt0 (xa) (xR) W3)) => (sdtmndtasgtdt0 (xb) (xR) W3)))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (aElement0 (xc)) (sdtmndtasgtdt0 (xb) (xR) (xa)) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) ### All 18 % 28.27/28.43 20. (All W2, (All W3, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xb) (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 (xb) (xR) W3))))) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (sdtmndtasgtdt0 (xb) (xR) (xa)) (aElement0 (xc)) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) ### All 19 % 28.27/28.43 21. ((sdtmndtasgtdt0 (xb) (xR) (xa)) <=> (((xb) = (xa)) \/ (sdtmndtplgtdt0 (xb) (xR) (xa)))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (aElement0 (xc)) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (All W2, (All W3, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xb) (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 (xb) (xR) W3))))) ((xa) = (xb)) ### Equiv 10 20 % 28.27/28.43 22. (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 (xa)))) => ((sdtmndtasgtdt0 (xb) (xR) (xa)) <=> (((xb) = (xa)) \/ (sdtmndtplgtdt0 (xb) (xR) (xa))))) ((xa) = (xb)) (All W2, (All W3, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xb) (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 (xb) (xR) W3))))) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (aElement0 (xc)) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) ### DisjTree 6 7 8 21 % 28.27/28.43 23. (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) (xR) W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) (xR) W2))))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (aElement0 (xc)) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (All W2, (All W3, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xb) (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 (xb) (xR) W3))))) ((xa) = (xb)) ### All 22 % 28.27/28.43 24. (All W1, (All W2, (All W3, (((aElement0 (xb)) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xb) W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 (xb) W1 W3)))))) ((xa) = (xb)) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (aElement0 (xc)) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) (xR) W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) (xR) W2))))) ### All 23 % 28.27/28.43 25. (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (sdtmndtplgtdt0 (xa) (xR) (xb)) ### Axiom % 28.27/28.43 26. (((xa) = (xb)) \/ (sdtmndtplgtdt0 (xa) (xR) (xb))) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) (xR) W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) (xR) W2))))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (aElement0 (xc)) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (All W1, (All W2, (All W3, (((aElement0 (xb)) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xb) W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 (xb) W1 W3)))))) ### Or 24 25 % 28.27/28.43 27. ((sdtmndtasgtdt0 (xa) (xR) (xb)) <=> (((xa) = (xb)) \/ (sdtmndtplgtdt0 (xa) (xR) (xb)))) (All W1, (All W2, (All W3, (((aElement0 (xb)) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xb) W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 (xb) W1 W3)))))) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (aElement0 (xc)) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) (xR) W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) (xR) W2))))) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) ### Equiv 5 26 % 28.27/28.43 28. (((aElement0 (xa)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 (xb)))) => ((sdtmndtasgtdt0 (xa) (xR) (xb)) <=> (((xa) = (xb)) \/ (sdtmndtplgtdt0 (xa) (xR) (xb))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) (xR) W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) (xR) W2))))) (aElement0 (xc)) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (All W1, (All W2, (All W3, (((aElement0 (xb)) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xb) W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 (xb) W1 W3)))))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) ### DisjTree 2 3 4 27 % 28.27/28.43 29. (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) (xR) W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) (xR) W2))))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) (All W1, (All W2, (All W3, (((aElement0 (xb)) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xb) W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 (xb) W1 W3)))))) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (aElement0 (xc)) (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) (xR) W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) (xR) W2))))) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) ### All 28 % 28.27/28.43 30. (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) (xR) W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) (xR) W2))))) (aElement0 (xc)) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) (xR) W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) (xR) W2))))) ### All 29 % 28.27/28.43 31. (All W1, (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) W1 W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) W1 W2)))))) (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) (xR) W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) (xR) W2))))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (aElement0 (xc)) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) ### All 30 % 28.27/28.43 32. (All W1, (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) W1 W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) W1 W2)))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (aElement0 (xc)) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (All W1, (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) W1 W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) W1 W2)))))) ### All 31 % 28.27/28.43 33. (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) (-. (sdtmndtasgtdt0 (xb) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (aElement0 (xc)) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W1, (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) W1 W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) W1 W2)))))) ### All 32 % 28.27/28.43 34. (aElement0 (xc)) (-. (aElement0 (xc))) ### Axiom % 28.27/28.43 35. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 28.27/28.43 36. (aElement0 (xc)) (-. (aElement0 (xc))) ### Axiom % 28.27/28.43 37. ((xc) != (xc)) ### NotEqual % 28.27/28.43 38. (-. (((xc) = (xc)) \/ (sdtmndtplgtdt0 (xc) (xR) (xc)))) ### NotOr 37 % 28.27/28.43 39. (-. (sdtmndtasgtdt0 (xc) (xR) (xc))) (sdtmndtasgtdt0 (xc) (xR) (xc)) ### Axiom % 28.27/28.43 40. ((sdtmndtasgtdt0 (xc) (xR) (xc)) <=> (((xc) = (xc)) \/ (sdtmndtplgtdt0 (xc) (xR) (xc)))) (-. (sdtmndtasgtdt0 (xc) (xR) (xc))) ### Equiv 38 39 % 28.27/28.43 41. (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 (xc)))) => ((sdtmndtasgtdt0 (xc) (xR) (xc)) <=> (((xc) = (xc)) \/ (sdtmndtplgtdt0 (xc) (xR) (xc))))) (-. (sdtmndtasgtdt0 (xc) (xR) (xc))) (aRewritingSystem0 (xR)) (aElement0 (xc)) ### DisjTree 34 35 36 40 % 28.27/28.43 42. (All W2, (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xc) (xR) W2) <=> (((xc) = W2) \/ (sdtmndtplgtdt0 (xc) (xR) W2))))) (aElement0 (xc)) (aRewritingSystem0 (xR)) (-. (sdtmndtasgtdt0 (xc) (xR) (xc))) ### All 41 % 28.27/28.43 43. (-. ((aElement0 (xc)) /\ ((sdtmndtasgtdt0 (xb) (xR) (xc)) /\ (sdtmndtasgtdt0 (xc) (xR) (xc))))) (All W2, (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xc) (xR) W2) <=> (((xc) = W2) \/ (sdtmndtplgtdt0 (xc) (xR) W2))))) (All W1, (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) W1 W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) W1 W2)))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xc)) ### DisjTree 1 33 42 % 28.27/28.43 44. (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (aElement0 (xc)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W1, (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) W1 W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) W1 W2)))))) (All W2, (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xc) (xR) W2) <=> (((xc) = W2) \/ (sdtmndtplgtdt0 (xc) (xR) W2))))) ### NotExists 43 % 28.27/28.43 45. (All W1, (All W2, (((aElement0 (xc)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xc) W1 W2) <=> (((xc) = W2) \/ (sdtmndtplgtdt0 (xc) W1 W2)))))) (All W1, (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) W1 W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) W1 W2)))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xc)) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) ### All 44 % 28.27/28.43 46. (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (aElement0 (xc)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W1, (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) W1 W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) W1 W2)))))) ### All 45 % 28.27/28.43 47. (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xc)) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) ### All 46 % 28.27/28.43 48. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 28.27/28.43 49. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 28.27/28.43 50. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 28.27/28.43 51. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 28.27/28.43 52. ((xb) != (xb)) ### NotEqual % 28.27/28.43 53. (-. (((xb) = (xb)) \/ (sdtmndtplgtdt0 (xb) (xR) (xb)))) ### NotOr 52 % 28.27/28.43 54. (-. (sdtmndtasgtdt0 (xb) (xR) (xb))) (sdtmndtasgtdt0 (xb) (xR) (xb)) ### Axiom % 28.27/28.43 55. ((sdtmndtasgtdt0 (xb) (xR) (xb)) <=> (((xb) = (xb)) \/ (sdtmndtplgtdt0 (xb) (xR) (xb)))) (-. (sdtmndtasgtdt0 (xb) (xR) (xb))) ### Equiv 53 54 % 28.27/28.43 56. (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 (xb)))) => ((sdtmndtasgtdt0 (xb) (xR) (xb)) <=> (((xb) = (xb)) \/ (sdtmndtplgtdt0 (xb) (xR) (xb))))) (-. (sdtmndtasgtdt0 (xb) (xR) (xb))) (aRewritingSystem0 (xR)) (aElement0 (xb)) ### DisjTree 49 50 51 55 % 28.27/28.43 57. (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) (xR) W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) (xR) W2))))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (-. (sdtmndtasgtdt0 (xb) (xR) (xb))) ### All 56 % 28.27/28.43 58. (aElement0 (xa)) (-. (aElement0 (xa))) ### Axiom % 28.27/28.43 59. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 28.27/28.43 60. (aElement0 (xc)) (-. (aElement0 (xc))) ### Axiom % 28.27/28.43 61. (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtasgtdt0 (xa) (xR) (xc))) ### Axiom % 28.27/28.43 62. (aElement0 (xc)) (-. (aElement0 (xc))) ### Axiom % 28.27/28.43 63. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 28.27/28.43 64. (aElement0 (xa)) (-. (aElement0 (xa))) ### Axiom % 28.27/28.43 65. ((xa) = (xc)) ((xc) != (xa)) ### Sym(=) % 28.27/28.43 66. (-. (((xc) = (xa)) \/ (sdtmndtplgtdt0 (xc) (xR) (xa)))) ((xa) = (xc)) ### NotOr 65 % 28.27/28.43 67. (aElement0 (xc)) (-. (aElement0 (xc))) ### Axiom % 28.27/28.43 68. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 28.27/28.43 69. (aElement0 (xa)) (-. (aElement0 (xa))) ### Axiom % 28.27/28.43 70. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 28.27/28.43 71. (sdtmndtasgtdt0 (xc) (xR) (xa)) (-. (sdtmndtasgtdt0 (xc) (xR) (xa))) ### Axiom % 28.27/28.43 72. (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtasgtdt0 (xa) (xR) (xb))) ### Axiom % 28.27/28.43 73. (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (sdtmndtasgtdt0 (xc) (xR) (xb)) ### Axiom % 28.27/28.43 74. (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 (xa)) /\ (aElement0 (xb))))) => (((sdtmndtasgtdt0 (xc) (xR) (xa)) /\ (sdtmndtasgtdt0 (xa) (xR) (xb))) => (sdtmndtasgtdt0 (xc) (xR) (xb)))) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (sdtmndtasgtdt0 (xc) (xR) (xa)) (aElement0 (xb)) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xc)) ### DisjTree 67 68 69 70 71 72 73 % 28.27/28.43 75. (All W3, (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 (xa)) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xc) (xR) (xa)) /\ (sdtmndtasgtdt0 (xa) (xR) W3)) => (sdtmndtasgtdt0 (xc) (xR) W3)))) (aElement0 (xc)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (aElement0 (xb)) (sdtmndtasgtdt0 (xc) (xR) (xa)) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) ### All 74 % 28.27/28.43 76. ((sdtmndtasgtdt0 (xc) (xR) (xa)) <=> (((xc) = (xa)) \/ (sdtmndtplgtdt0 (xc) (xR) (xa)))) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (aElement0 (xb)) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xc)) (All W3, (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 (xa)) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xc) (xR) (xa)) /\ (sdtmndtasgtdt0 (xa) (xR) W3)) => (sdtmndtasgtdt0 (xc) (xR) W3)))) ((xa) = (xc)) ### Equiv 66 75 % 28.27/28.43 77. (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 (xa)))) => ((sdtmndtasgtdt0 (xc) (xR) (xa)) <=> (((xc) = (xa)) \/ (sdtmndtplgtdt0 (xc) (xR) (xa))))) ((xa) = (xc)) (All W3, (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 (xa)) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xc) (xR) (xa)) /\ (sdtmndtasgtdt0 (xa) (xR) W3)) => (sdtmndtasgtdt0 (xc) (xR) W3)))) (aElement0 (xb)) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xc)) ### DisjTree 62 63 64 76 % 28.27/28.43 78. (All W2, (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xc) (xR) W2) <=> (((xc) = W2) \/ (sdtmndtplgtdt0 (xc) (xR) W2))))) (aElement0 (xc)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (aElement0 (xb)) (All W3, (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 (xa)) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xc) (xR) (xa)) /\ (sdtmndtasgtdt0 (xa) (xR) W3)) => (sdtmndtasgtdt0 (xc) (xR) W3)))) ((xa) = (xc)) ### All 77 % 28.27/28.43 79. (All W2, (All W3, (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xc) (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 (xc) (xR) W3))))) ((xa) = (xc)) (aElement0 (xb)) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xc)) (All W2, (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xc) (xR) W2) <=> (((xc) = W2) \/ (sdtmndtplgtdt0 (xc) (xR) W2))))) ### All 78 % 28.27/28.43 80. (All W1, (All W2, (((aElement0 (xc)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xc) W1 W2) <=> (((xc) = W2) \/ (sdtmndtplgtdt0 (xc) W1 W2)))))) (aElement0 (xc)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (aElement0 (xb)) ((xa) = (xc)) (All W2, (All W3, (((aElement0 (xc)) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xc) (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 (xc) (xR) W3))))) ### All 79 % 28.27/28.43 81. (All W1, (All W2, (All W3, (((aElement0 (xc)) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 (xc) W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 (xc) W1 W3)))))) ((xa) = (xc)) (aElement0 (xb)) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xc)) (All W1, (All W2, (((aElement0 (xc)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xc) W1 W2) <=> (((xc) = W2) \/ (sdtmndtplgtdt0 (xc) W1 W2)))))) ### All 80 % 28.27/28.43 82. (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W1, (All W2, (((aElement0 (xc)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xc) W1 W2) <=> (((xc) = W2) \/ (sdtmndtplgtdt0 (xc) W1 W2)))))) (aElement0 (xc)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (aElement0 (xb)) ((xa) = (xc)) ### All 81 % 28.27/28.43 83. (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) ((xa) = (xc)) (aElement0 (xb)) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xc)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) ### All 82 % 28.27/28.43 84. (-. (sdtmndtplgtdt0 (xa) (xR) (xc))) (sdtmndtplgtdt0 (xa) (xR) (xc)) ### Axiom % 28.27/28.43 85. (((xa) = (xc)) \/ (sdtmndtplgtdt0 (xa) (xR) (xc))) (-. (sdtmndtplgtdt0 (xa) (xR) (xc))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (aElement0 (xc)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (aElement0 (xb)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) ### Or 83 84 % 28.27/28.43 86. ((sdtmndtasgtdt0 (xa) (xR) (xc)) <=> (((xa) = (xc)) \/ (sdtmndtplgtdt0 (xa) (xR) (xc)))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xb)) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xc)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (-. (sdtmndtplgtdt0 (xa) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) ### Equiv 61 85 % 28.27/28.43 87. (((aElement0 (xa)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 (xc)))) => ((sdtmndtasgtdt0 (xa) (xR) (xc)) <=> (((xa) = (xc)) \/ (sdtmndtplgtdt0 (xa) (xR) (xc))))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtplgtdt0 (xa) (xR) (xc))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (aElement0 (xb)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xc)) (aRewritingSystem0 (xR)) (aElement0 (xa)) ### DisjTree 58 59 60 86 % 28.27/28.43 88. (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) (xR) W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) (xR) W2))))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xc)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xb)) (sdtmndtasgtdt0 (xa) (xR) (xb)) (-. (sdtmndtasgtdt0 (xc) (xR) (xb))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (-. (sdtmndtplgtdt0 (xa) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) ### All 87 % 28.27/28.43 89. (-. ((aElement0 (xb)) /\ ((sdtmndtasgtdt0 (xb) (xR) (xb)) /\ (sdtmndtasgtdt0 (xc) (xR) (xb))))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtplgtdt0 (xa) (xR) (xc))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xc)) (aElement0 (xa)) (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) (xR) W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) (xR) W2))))) (aRewritingSystem0 (xR)) (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) (xR) W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) (xR) W2))))) (aElement0 (xb)) ### DisjTree 48 57 88 % 28.27/28.43 90. (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (aElement0 (xb)) (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) (xR) W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) (xR) W2))))) (aRewritingSystem0 (xR)) (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) (xR) W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) (xR) W2))))) (aElement0 (xa)) (aElement0 (xc)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (-. (sdtmndtplgtdt0 (xa) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) ### NotExists 89 % 28.27/28.43 91. (All W1, (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) W1 W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) W1 W2)))))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtplgtdt0 (xa) (xR) (xc))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xc)) (aElement0 (xa)) (aRewritingSystem0 (xR)) (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) (xR) W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) (xR) W2))))) (aElement0 (xb)) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) ### All 90 % 28.27/28.43 92. (All W1, (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) W1 W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) W1 W2)))))) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (aElement0 (xc)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (-. (sdtmndtplgtdt0 (xa) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (All W1, (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) W1 W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) W1 W2)))))) ### All 91 % 28.27/28.43 93. (All W1, (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xa) W1 W2) <=> (((xa) = W2) \/ (sdtmndtplgtdt0 (xa) W1 W2)))))) (sdtmndtasgtdt0 (xa) (xR) (xc)) (-. (sdtmndtplgtdt0 (xa) (xR) (xc))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xc)) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) ### All 92 % 28.27/28.43 94. (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) (aElement0 (xc)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (-. (sdtmndtplgtdt0 (xa) (xR) (xc))) (sdtmndtasgtdt0 (xa) (xR) (xc)) ### All 93 % 28.27/28.43 95. (aElement0 T_0) (-. (aElement0 T_0)) ### Axiom % 28.27/28.43 96. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 28.27/28.43 97. (aNormalFormOfIn0 T_1 T_0 (xR)) (-. (aNormalFormOfIn0 T_1 T_0 (xR))) ### Axiom % 28.27/28.43 98. (-. (aElement0 T_1)) (aElement0 T_1) ### Axiom % 28.27/28.43 99. ((aElement0 T_1) /\ ((sdtmndtasgtdt0 T_0 (xR) T_1) /\ (-. (Ex W3, (aReductOfIn0 W3 T_1 (xR)))))) (-. (aElement0 T_1)) ### ConjTree 98 % 28.27/28.43 100. ((aNormalFormOfIn0 T_1 T_0 (xR)) <=> ((aElement0 T_1) /\ ((sdtmndtasgtdt0 T_0 (xR) T_1) /\ (-. (Ex W3, (aReductOfIn0 W3 T_1 (xR))))))) (-. (aElement0 T_1)) (aNormalFormOfIn0 T_1 T_0 (xR)) ### Equiv 97 99 % 28.27/28.45 101. (All W2, ((aNormalFormOfIn0 W2 T_0 (xR)) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 T_0 (xR) W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))))))) (aNormalFormOfIn0 T_1 T_0 (xR)) (-. (aElement0 T_1)) ### All 100 % 28.27/28.45 102. (((aElement0 T_0) /\ (aRewritingSystem0 (xR))) => (All W2, ((aNormalFormOfIn0 W2 T_0 (xR)) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 T_0 (xR) W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 (xR))))))))) (-. (aElement0 T_1)) (aNormalFormOfIn0 T_1 T_0 (xR)) (aRewritingSystem0 (xR)) (aElement0 T_0) ### DisjTree 95 96 101 % 28.27/28.45 103. (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 T_0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 T_0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1))))))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (aNormalFormOfIn0 T_1 T_0 (xR)) (-. (aElement0 T_1)) ### All 102 % 28.27/28.45 104. (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (-. (aElement0 T_1)) (aNormalFormOfIn0 T_1 T_0 (xR)) (aRewritingSystem0 (xR)) (aElement0 T_0) ### All 103 % 28.27/28.45 105. (sdtmndtasgtdt0 (xb) (xR) T_1) (-. (sdtmndtasgtdt0 (xb) (xR) T_1)) ### Axiom % 28.27/28.45 106. (sdtmndtasgtdt0 (xc) (xR) T_1) (-. (sdtmndtasgtdt0 (xc) (xR) T_1)) ### Axiom % 28.27/28.45 107. (-. ((aElement0 T_1) /\ ((sdtmndtasgtdt0 (xb) (xR) T_1) /\ (sdtmndtasgtdt0 (xc) (xR) T_1)))) (sdtmndtasgtdt0 (xc) (xR) T_1) (sdtmndtasgtdt0 (xb) (xR) T_1) (aElement0 T_0) (aRewritingSystem0 (xR)) (aNormalFormOfIn0 T_1 T_0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) ### DisjTree 104 105 106 % 28.27/28.45 108. (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (aNormalFormOfIn0 T_1 T_0 (xR)) (aRewritingSystem0 (xR)) (aElement0 T_0) (sdtmndtasgtdt0 (xb) (xR) T_1) (sdtmndtasgtdt0 (xc) (xR) T_1) ### NotExists 107 % 28.27/28.45 109. ((aNormalFormOfIn0 T_1 T_0 (xR)) /\ ((sdtmndtasgtdt0 (xb) (xR) T_1) /\ (sdtmndtasgtdt0 (xc) (xR) T_1))) (aElement0 T_0) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) ### ConjTree 108 % 28.27/28.45 110. (Ex W3, ((aNormalFormOfIn0 W3 T_0 (xR)) /\ ((sdtmndtasgtdt0 (xb) (xR) W3) /\ (sdtmndtasgtdt0 (xc) (xR) W3)))) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (aRewritingSystem0 (xR)) (aElement0 T_0) ### Exists 109 % 28.27/28.45 111. ((aElement0 T_0) /\ ((sdtmndtasgtdt0 T_2 (xR) T_0) /\ ((sdtmndtasgtdt0 T_3 (xR) T_0) /\ (Ex W3, ((aNormalFormOfIn0 W3 T_0 (xR)) /\ ((sdtmndtasgtdt0 (xb) (xR) W3) /\ (sdtmndtasgtdt0 (xc) (xR) W3))))))) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) ### ConjTree 110 % 28.27/28.45 112. (Ex W2, ((aElement0 W2) /\ ((sdtmndtasgtdt0 T_2 (xR) W2) /\ ((sdtmndtasgtdt0 T_3 (xR) W2) /\ (Ex W3, ((aNormalFormOfIn0 W3 W2 (xR)) /\ ((sdtmndtasgtdt0 (xb) (xR) W3) /\ (sdtmndtasgtdt0 (xc) (xR) W3)))))))) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (aRewritingSystem0 (xR)) ### Exists 111 % 28.27/28.45 113. ((aElement0 T_3) /\ ((aReductOfIn0 T_3 (xa) (xR)) /\ ((sdtmndtasgtdt0 T_3 (xR) (xc)) /\ (Ex W2, ((aElement0 W2) /\ ((sdtmndtasgtdt0 T_2 (xR) W2) /\ ((sdtmndtasgtdt0 T_3 (xR) W2) /\ (Ex W3, ((aNormalFormOfIn0 W3 W2 (xR)) /\ ((sdtmndtasgtdt0 (xb) (xR) W3) /\ (sdtmndtasgtdt0 (xc) (xR) W3))))))))))) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) ### ConjTree 112 % 28.27/28.45 114. (Ex W1, ((aElement0 W1) /\ ((aReductOfIn0 W1 (xa) (xR)) /\ ((sdtmndtasgtdt0 W1 (xR) (xc)) /\ (Ex W2, ((aElement0 W2) /\ ((sdtmndtasgtdt0 T_2 (xR) W2) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ (Ex W3, ((aNormalFormOfIn0 W3 W2 (xR)) /\ ((sdtmndtasgtdt0 (xb) (xR) W3) /\ (sdtmndtasgtdt0 (xc) (xR) W3)))))))))))) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (aRewritingSystem0 (xR)) ### Exists 113 % 28.27/28.45 115. ((aElement0 T_2) /\ ((aReductOfIn0 T_2 (xa) (xR)) /\ ((sdtmndtasgtdt0 T_2 (xR) (xb)) /\ (Ex W1, ((aElement0 W1) /\ ((aReductOfIn0 W1 (xa) (xR)) /\ ((sdtmndtasgtdt0 W1 (xR) (xc)) /\ (Ex W2, ((aElement0 W2) /\ ((sdtmndtasgtdt0 T_2 (xR) W2) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ (Ex W3, ((aNormalFormOfIn0 W3 W2 (xR)) /\ ((sdtmndtasgtdt0 (xb) (xR) W3) /\ (sdtmndtasgtdt0 (xc) (xR) W3))))))))))))))) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) ### ConjTree 114 % 28.27/28.45 116. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ ((sdtmndtasgtdt0 W0 (xR) (xb)) /\ (Ex W1, ((aElement0 W1) /\ ((aReductOfIn0 W1 (xa) (xR)) /\ ((sdtmndtasgtdt0 W1 (xR) (xc)) /\ (Ex W2, ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 (xR) W2) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ (Ex W3, ((aNormalFormOfIn0 W3 W2 (xR)) /\ ((sdtmndtasgtdt0 (xb) (xR) W3) /\ (sdtmndtasgtdt0 (xc) (xR) W3)))))))))))))))) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (aRewritingSystem0 (xR)) ### Exists 115 % 28.27/28.45 117. (((sdtmndtplgtdt0 (xa) (xR) (xb)) /\ (sdtmndtplgtdt0 (xa) (xR) (xc))) => (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ ((sdtmndtasgtdt0 W0 (xR) (xb)) /\ (Ex W1, ((aElement0 W1) /\ ((aReductOfIn0 W1 (xa) (xR)) /\ ((sdtmndtasgtdt0 W1 (xR) (xc)) /\ (Ex W2, ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 (xR) W2) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ (Ex W3, ((aNormalFormOfIn0 W3 W2 (xR)) /\ ((sdtmndtasgtdt0 (xb) (xR) W3) /\ (sdtmndtasgtdt0 (xc) (xR) W3))))))))))))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (aElement0 (xc)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) (sdtmndtasgtdt0 (xa) (xR) (xc)) (sdtmndtasgtdt0 (xa) (xR) (xb)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) ### DisjTree 47 94 116 % 28.27/28.45 118. ((aElement0 (xa)) /\ ((aElement0 (xb)) /\ (aElement0 (xc)))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (sdtmndtasgtdt0 (xa) (xR) (xb)) (sdtmndtasgtdt0 (xa) (xR) (xc)) (aRewritingSystem0 (xR)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (-. (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (((sdtmndtplgtdt0 (xa) (xR) (xb)) /\ (sdtmndtplgtdt0 (xa) (xR) (xc))) => (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ ((sdtmndtasgtdt0 W0 (xR) (xb)) /\ (Ex W1, ((aElement0 W1) /\ ((aReductOfIn0 W1 (xa) (xR)) /\ ((sdtmndtasgtdt0 W1 (xR) (xc)) /\ (Ex W2, ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 (xR) W2) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ (Ex W3, ((aNormalFormOfIn0 W3 W2 (xR)) /\ ((sdtmndtasgtdt0 (xb) (xR) W3) /\ (sdtmndtasgtdt0 (xc) (xR) W3))))))))))))))))) ### ConjTree 117 % 28.27/28.45 119. (-. ((((sdtmndtplgtdt0 (xa) (xR) (xb)) /\ (sdtmndtplgtdt0 (xa) (xR) (xc))) => (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ ((sdtmndtasgtdt0 W0 (xR) (xb)) /\ (Ex W1, ((aElement0 W1) /\ ((aReductOfIn0 W1 (xa) (xR)) /\ ((sdtmndtasgtdt0 W1 (xR) (xc)) /\ (Ex W2, ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 (xR) W2) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ (Ex W3, ((aNormalFormOfIn0 W3 W2 (xR)) /\ ((sdtmndtasgtdt0 (xb) (xR) W3) /\ (sdtmndtasgtdt0 (xc) (xR) W3))))))))))))))))) => (((sdtmndtasgtdt0 (xa) (xR) (xb)) /\ (sdtmndtasgtdt0 (xa) (xR) (xc))) => (Ex W0, ((aElement0 W0) /\ ((sdtmndtasgtdt0 (xb) (xR) W0) /\ (sdtmndtasgtdt0 (xc) (xR) W0))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aNormalFormOfIn0 W2 W0 W1) <=> ((aElement0 W2) /\ ((sdtmndtasgtdt0 W0 W1 W2) /\ (-. (Ex W3, (aReductOfIn0 W3 W2 W1)))))))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aRewritingSystem0 (xR)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) ((aElement0 (xa)) /\ ((aElement0 (xb)) /\ (aElement0 (xc)))) ### ConjTree 118 % 28.27/28.45 % SZS output end Proof % 28.27/28.45 (* END-PROOF *) %------------------------------------------------------------------------------