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