%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM016+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 : n005.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:51 EDT 2022 % Result : Theorem 0.19s 0.48s % Output : Proof 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM016+1 : TPTP v8.1.0. Released v4.0.0. % 0.13/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.33 % Computer : n005.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:15:08 EDT 2022 % 0.13/0.33 % CPUTime : % 0.19/0.48 % SZS status Theorem % 0.19/0.48 (* PROOF-FOUND *) % 0.19/0.48 (* BEGIN-PROOF *) % 0.19/0.48 % SZS output start Proof % 0.19/0.48 1. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 0.19/0.48 2. (aElement0 (xa)) (-. (aElement0 (xa))) ### Axiom % 0.19/0.48 3. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 0.19/0.48 4. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 0.19/0.48 5. (sdtmndtplgtdt0 (xa) (xR) (xb)) (-. (sdtmndtplgtdt0 (xa) (xR) (xb))) ### Axiom % 0.19/0.48 6. (-. (aReductOfIn0 (xb) (xa) (xR))) (aReductOfIn0 (xb) (xa) (xR)) ### Axiom % 0.19/0.48 7. (aElement0 T_0) (-. (aElement0 T_0)) ### Axiom % 0.19/0.48 8. (aReductOfIn0 T_0 (xa) (xR)) (-. (aReductOfIn0 T_0 (xa) (xR))) ### Axiom % 0.19/0.48 9. (aElement0 T_0) (-. (aElement0 T_0)) ### Axiom % 0.19/0.48 10. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 0.19/0.48 11. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 0.19/0.48 12. (sdtmndtplgtdt0 T_0 (xR) (xb)) (-. (sdtmndtplgtdt0 T_0 (xR) (xb))) ### Axiom % 0.19/0.48 13. (-. ((T_0 = (xb)) \/ (sdtmndtplgtdt0 T_0 (xR) (xb)))) (sdtmndtplgtdt0 T_0 (xR) (xb)) ### NotOr 12 % 0.19/0.48 14. (-. (sdtmndtasgtdt0 T_0 (xR) (xb))) (sdtmndtasgtdt0 T_0 (xR) (xb)) ### Axiom % 0.19/0.48 15. ((sdtmndtasgtdt0 T_0 (xR) (xb)) <=> ((T_0 = (xb)) \/ (sdtmndtplgtdt0 T_0 (xR) (xb)))) (-. (sdtmndtasgtdt0 T_0 (xR) (xb))) (sdtmndtplgtdt0 T_0 (xR) (xb)) ### Equiv 13 14 % 0.19/0.48 16. (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 (xb)))) => ((sdtmndtasgtdt0 T_0 (xR) (xb)) <=> ((T_0 = (xb)) \/ (sdtmndtplgtdt0 T_0 (xR) (xb))))) (sdtmndtplgtdt0 T_0 (xR) (xb)) (-. (sdtmndtasgtdt0 T_0 (xR) (xb))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 T_0) ### DisjTree 9 10 11 15 % 0.19/0.48 17. (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 (xR) W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 (xR) W2))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (aElement0 (xb)) (-. (sdtmndtasgtdt0 T_0 (xR) (xb))) (sdtmndtplgtdt0 T_0 (xR) (xb)) ### All 16 % 0.19/0.48 18. (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (sdtmndtplgtdt0 T_0 (xR) (xb)) (-. (sdtmndtasgtdt0 T_0 (xR) (xb))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 T_0) ### All 17 % 0.19/0.48 19. (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (aElement0 (xb)) (-. (sdtmndtasgtdt0 T_0 (xR) (xb))) (sdtmndtplgtdt0 T_0 (xR) (xb)) ### All 18 % 0.19/0.48 20. (-. ((aElement0 T_0) /\ ((aReductOfIn0 T_0 (xa) (xR)) /\ (sdtmndtasgtdt0 T_0 (xR) (xb))))) (sdtmndtplgtdt0 T_0 (xR) (xb)) (aElement0 (xb)) (aRewritingSystem0 (xR)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aReductOfIn0 T_0 (xa) (xR)) (aElement0 T_0) ### DisjTree 7 8 19 % 0.19/0.48 21. (-. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (aElement0 T_0) (aReductOfIn0 T_0 (xa) (xR)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aRewritingSystem0 (xR)) (aElement0 (xb)) (sdtmndtplgtdt0 T_0 (xR) (xb)) ### NotExists 20 % 0.19/0.48 22. ((aElement0 T_0) /\ ((aReductOfIn0 T_0 (xa) (xR)) /\ (sdtmndtplgtdt0 T_0 (xR) (xb)))) (aElement0 (xb)) (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) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) ### ConjTree 21 % 0.19/0.48 23. (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 (xa) (xR)) /\ (sdtmndtplgtdt0 W3 (xR) (xb))))) (-. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aRewritingSystem0 (xR)) (aElement0 (xb)) ### Exists 22 % 0.19/0.48 24. ((aReductOfIn0 (xb) (xa) (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 (xa) (xR)) /\ (sdtmndtplgtdt0 W3 (xR) (xb)))))) (aElement0 (xb)) (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) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (-. (aReductOfIn0 (xb) (xa) (xR))) ### Or 6 23 % 0.19/0.48 25. ((sdtmndtplgtdt0 (xa) (xR) (xb)) <=> ((aReductOfIn0 (xb) (xa) (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 (xa) (xR)) /\ (sdtmndtplgtdt0 W3 (xR) (xb))))))) (-. (aReductOfIn0 (xb) (xa) (xR))) (-. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aRewritingSystem0 (xR)) (aElement0 (xb)) (sdtmndtplgtdt0 (xa) (xR) (xb)) ### Equiv 5 24 % 0.19/0.48 26. (((aElement0 (xa)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 (xb)))) => ((sdtmndtplgtdt0 (xa) (xR) (xb)) <=> ((aReductOfIn0 (xb) (xa) (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 (xa) (xR)) /\ (sdtmndtplgtdt0 W3 (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))))))) (-. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (-. (aReductOfIn0 (xb) (xa) (xR))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) ### DisjTree 2 3 4 25 % 0.19/0.48 27. (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 (xa) (xR) W2) <=> ((aReductOfIn0 W2 (xa) (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 (xa) (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) (-. (aReductOfIn0 (xb) (xa) (xR))) (-. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtplgtdt0 (xa) (xR) (xb)) ### All 26 % 0.19/0.48 28. (All W1, (All W2, (((aElement0 (xa)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 (xa) W1 W2) <=> ((aReductOfIn0 W2 (xa) W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 (xa) W1) /\ (sdtmndtplgtdt0 W3 W1 W2))))))))) (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))))))) (-. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (-. (aReductOfIn0 (xb) (xa) (xR))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (aElement0 (xa)) ### All 27 % 0.19/0.48 29. (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 W0 W1 W2) <=> ((aReductOfIn0 W2 W0 W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W0 W1) /\ (sdtmndtplgtdt0 W3 W1 W2)))))))))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (aElement0 (xb)) (-. (aReductOfIn0 (xb) (xa) (xR))) (-. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtplgtdt0 (xa) (xR) (xb)) ### All 28 % 0.19/0.48 30. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 0.19/0.48 31. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 0.19/0.48 32. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 0.19/0.48 33. ((xb) != (xb)) ### NotEqual % 0.19/0.48 34. (-. (((xb) = (xb)) \/ (sdtmndtplgtdt0 (xb) (xR) (xb)))) ### NotOr 33 % 0.19/0.48 35. (-. (sdtmndtasgtdt0 (xb) (xR) (xb))) (sdtmndtasgtdt0 (xb) (xR) (xb)) ### Axiom % 0.19/0.48 36. ((sdtmndtasgtdt0 (xb) (xR) (xb)) <=> (((xb) = (xb)) \/ (sdtmndtplgtdt0 (xb) (xR) (xb)))) (-. (sdtmndtasgtdt0 (xb) (xR) (xb))) ### Equiv 34 35 % 0.19/0.48 37. (((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 30 31 32 36 % 0.19/0.48 38. (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 37 % 0.19/0.48 39. (All W1, (All W2, (((aElement0 (xb)) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 (xb) W1 W2) <=> (((xb) = W2) \/ (sdtmndtplgtdt0 (xb) W1 W2)))))) (-. (sdtmndtasgtdt0 (xb) (xR) (xb))) (aRewritingSystem0 (xR)) (aElement0 (xb)) ### All 38 % 0.19/0.48 40. (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (aElement0 (xb)) (aRewritingSystem0 (xR)) (-. (sdtmndtasgtdt0 (xb) (xR) (xb))) ### All 39 % 0.19/0.48 41. (-. ((aElement0 (xb)) /\ ((aReductOfIn0 (xb) (xa) (xR)) /\ (sdtmndtasgtdt0 (xb) (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))))))) (-. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (aRewritingSystem0 (xR)) (aElement0 (xa)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 W0 W1 W2) <=> ((aReductOfIn0 W2 W0 W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W0 W1) /\ (sdtmndtplgtdt0 W3 W1 W2)))))))))) (aElement0 (xb)) ### DisjTree 1 29 40 % 0.19/0.48 42. (aElement0 (xb)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 W0 W1 W2) <=> ((aReductOfIn0 W2 W0 W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W0 W1) /\ (sdtmndtplgtdt0 W3 W1 W2)))))))))) (aElement0 (xa)) (aRewritingSystem0 (xR)) (-. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (sdtmndtplgtdt0 (xa) (xR) (xb)) ### NotExists 41 % 0.19/0.48 43. ((sdtmndtplgtdt0 (xa) (xR) (xb)) /\ (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))))))) (-. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (aRewritingSystem0 (xR)) (aElement0 (xa)) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 W0 W1 W2) <=> ((aReductOfIn0 W2 W0 W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W0 W1) /\ (sdtmndtplgtdt0 W3 W1 W2)))))))))) (aElement0 (xb)) ### And 42 % 0.19/0.48 44. ((aElement0 (xa)) /\ ((aElement0 (xb)) /\ (aElement0 (xc)))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 W0 W1 W2) <=> ((aReductOfIn0 W2 W0 W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W0 W1) /\ (sdtmndtplgtdt0 W3 W1 W2)))))))))) (aRewritingSystem0 (xR)) (-. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xa) (xR)) /\ (sdtmndtasgtdt0 W0 (xR) (xb)))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) ((sdtmndtplgtdt0 (xa) (xR) (xb)) /\ (sdtmndtplgtdt0 (xa) (xR) (xc))) ### ConjTree 43 % 0.19/0.48 % SZS output end Proof % 0.19/0.48 (* END-PROOF *) %------------------------------------------------------------------------------