%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM021+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 : n004.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:53 EDT 2022 % Result : Theorem 0.97s 1.19s % Output : Proof 0.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : COM021+4 : TPTP v8.1.0. Released v4.0.0. % 0.10/0.09 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.10/0.29 % Computer : n004.cluster.edu % 0.10/0.29 % Model : x86_64 x86_64 % 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.29 % Memory : 8042.1875MB % 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.29 % CPULimit : 300 % 0.10/0.29 % WCLimit : 600 % 0.10/0.29 % DateTime : Thu Jun 16 16:52:38 EDT 2022 % 0.10/0.29 % CPUTime : % 0.97/1.19 % SZS status Theorem % 0.97/1.19 (* PROOF-FOUND *) % 0.97/1.19 (* BEGIN-PROOF *) % 0.97/1.19 % SZS output start Proof % 0.97/1.19 1. ((xb) != (xb)) ### NotEqual % 0.97/1.19 2. ((xR) != (xR)) ### NotEqual % 0.97/1.19 3. ((xd) = (xx)) ((xx) != (xd)) ### Sym(=) % 0.97/1.19 4. (-. (sdtmndtasgtdt0 (xb) (xR) (xd))) (sdtmndtasgtdt0 (xb) (xR) (xx)) ((xd) = (xx)) ### P-NotP 1 2 3 % 0.97/1.19 5. (aReductOfIn0 (xx) (xd) (xR)) (-. (aReductOfIn0 (xx) (xd) (xR))) ### Axiom % 0.97/1.19 6. (-. (Ex W0, (aReductOfIn0 W0 (xd) (xR)))) (aReductOfIn0 (xx) (xd) (xR)) ### NotExists 5 % 0.97/1.19 7. (aReductOfIn0 T_0 (xd) (xR)) (-. (aReductOfIn0 T_0 (xd) (xR))) ### Axiom % 0.97/1.19 8. (-. (Ex W0, (aReductOfIn0 W0 (xd) (xR)))) (aReductOfIn0 T_0 (xd) (xR)) ### NotExists 7 % 0.97/1.19 9. ((aElement0 T_0) /\ ((aReductOfIn0 T_0 (xd) (xR)) /\ (sdtmndtplgtdt0 T_0 (xR) (xx)))) (-. (Ex W0, (aReductOfIn0 W0 (xd) (xR)))) ### ConjTree 8 % 0.97/1.19 10. (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xd) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xx))))) (-. (Ex W0, (aReductOfIn0 W0 (xd) (xR)))) ### Exists 9 % 0.97/1.19 11. ((aReductOfIn0 (xx) (xd) (xR)) \/ (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xd) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xx)))))) (-. (Ex W0, (aReductOfIn0 W0 (xd) (xR)))) ### Or 6 10 % 0.97/1.19 12. (((aReductOfIn0 (xx) (xd) (xR)) \/ (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xd) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xx)))))) /\ (sdtmndtplgtdt0 (xd) (xR) (xx))) (-. (Ex W0, (aReductOfIn0 W0 (xd) (xR)))) ### And 11 % 0.97/1.19 13. (((xd) = (xx)) \/ (((aReductOfIn0 (xx) (xd) (xR)) \/ (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xd) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xx)))))) /\ (sdtmndtplgtdt0 (xd) (xR) (xx)))) (-. (Ex W0, (aReductOfIn0 W0 (xd) (xR)))) (sdtmndtasgtdt0 (xb) (xR) (xx)) (-. (sdtmndtasgtdt0 (xb) (xR) (xd))) ### Or 4 12 % 0.97/1.19 14. (-. (((xb) = (xd)) \/ ((aReductOfIn0 (xd) (xb) (xR)) \/ ((Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xb) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xd))))) \/ ((sdtmndtplgtdt0 (xb) (xR) (xd)) \/ (sdtmndtasgtdt0 (xb) (xR) (xd))))))) (sdtmndtasgtdt0 (xb) (xR) (xx)) (-. (Ex W0, (aReductOfIn0 W0 (xd) (xR)))) (((xd) = (xx)) \/ (((aReductOfIn0 (xx) (xd) (xR)) \/ (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xd) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xx)))))) /\ (sdtmndtplgtdt0 (xd) (xR) (xx)))) ### ConjTree 13 % 0.97/1.19 15. ((aElement0 (xx)) /\ ((((xb) = (xx)) \/ (((aReductOfIn0 (xx) (xb) (xR)) \/ (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xb) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xx)))))) /\ (sdtmndtplgtdt0 (xb) (xR) (xx)))) /\ ((sdtmndtasgtdt0 (xb) (xR) (xx)) /\ ((((xd) = (xx)) \/ (((aReductOfIn0 (xx) (xd) (xR)) \/ (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xd) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xx)))))) /\ (sdtmndtplgtdt0 (xd) (xR) (xx)))) /\ (sdtmndtasgtdt0 (xd) (xR) (xx)))))) (-. (Ex W0, (aReductOfIn0 W0 (xd) (xR)))) (-. (((xb) = (xd)) \/ ((aReductOfIn0 (xd) (xb) (xR)) \/ ((Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xb) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xd))))) \/ ((sdtmndtplgtdt0 (xb) (xR) (xd)) \/ (sdtmndtasgtdt0 (xb) (xR) (xd))))))) ### ConjTree 14 % 0.97/1.19 16. ((aElement0 (xd)) /\ ((((xw) = (xd)) \/ (((aReductOfIn0 (xd) (xw) (xR)) \/ (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xw) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xd)))))) /\ (sdtmndtplgtdt0 (xw) (xR) (xd)))) /\ ((sdtmndtasgtdt0 (xw) (xR) (xd)) /\ ((-. (Ex W0, (aReductOfIn0 W0 (xd) (xR)))) /\ (aNormalFormOfIn0 (xd) (xw) (xR)))))) (-. (((xb) = (xd)) \/ ((aReductOfIn0 (xd) (xb) (xR)) \/ ((Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xb) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xd))))) \/ ((sdtmndtplgtdt0 (xb) (xR) (xd)) \/ (sdtmndtasgtdt0 (xb) (xR) (xd))))))) ((aElement0 (xx)) /\ ((((xb) = (xx)) \/ (((aReductOfIn0 (xx) (xb) (xR)) \/ (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xb) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xx)))))) /\ (sdtmndtplgtdt0 (xb) (xR) (xx)))) /\ ((sdtmndtasgtdt0 (xb) (xR) (xx)) /\ ((((xd) = (xx)) \/ (((aReductOfIn0 (xx) (xd) (xR)) \/ (Ex W0, ((aElement0 W0) /\ ((aReductOfIn0 W0 (xd) (xR)) /\ (sdtmndtplgtdt0 W0 (xR) (xx)))))) /\ (sdtmndtplgtdt0 (xd) (xR) (xx)))) /\ (sdtmndtasgtdt0 (xd) (xR) (xx)))))) ### ConjTree 15 % 0.97/1.19 % SZS output end Proof % 0.97/1.19 (* END-PROOF *) %------------------------------------------------------------------------------