%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS147+1 : TPTP v8.1.0. Released v3.1.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 : Sun Jul 17 03:32:02 EDT 2022 % Result : Theorem 0.21s 0.54s % Output : Proof 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS147+1 : TPTP v8.1.0. Released v3.1.0. % 0.11/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.34 % Computer : n026.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Tue Jun 7 12:07:16 EDT 2022 % 0.14/0.34 % CPUTime : % 0.21/0.54 % SZS status Theorem % 0.21/0.54 (* PROOF-FOUND *) % 0.21/0.54 (* BEGIN-PROOF *) % 0.21/0.54 % SZS output start Proof % 0.21/0.54 1. (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (All X, ((cowlThing X) /\ (-. (cowlNothing X))))) ### Axiom % 0.21/0.54 2. (-. (xsd_integer T_0)) (xsd_integer T_0) ### Axiom % 0.21/0.54 3. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### NotNot 2 % 0.21/0.54 4. (-. (xsd_string T_0)) (-. (xsd_integer T_0)) ### Definition-Pseudo(xsd_string) 3 % 0.21/0.54 5. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### Axiom % 0.21/0.54 6. (xsd_string T_0) (-. (-. (xsd_integer T_0))) ### Definition-Pseudo(xsd_string) 5 % 0.21/0.54 7. (-. ((xsd_string T_0) <=> (-. (xsd_integer T_0)))) ### NotEquiv 4 6 % 0.21/0.54 8. (-. (All X, ((xsd_string X) <=> (-. (xsd_integer X))))) ### NotAllEx 7 % 0.21/0.54 9. (rR1 (iV8467) (iV8468)) (-. (rR1 (iV8467) (iV8468))) ### Axiom % 0.21/0.54 10. (-. (cC2 (iV8468))) (cC2 (iV8468)) ### Axiom % 0.21/0.54 11. (-. (-. (cC2 (iV8468)))) (-. (cC2 (iV8468))) ### NotNot 10 % 0.21/0.54 12. (-. ((rR1 (iV8467) (iV8468)) /\ (-. (cC2 (iV8468))))) (-. (cC2 (iV8468))) (rR1 (iV8467) (iV8468)) ### NotAnd 9 11 % 0.21/0.54 13. (-. (Ex Y, ((rR1 (iV8467) Y) /\ (-. (cC2 Y))))) (rR1 (iV8467) (iV8468)) (-. (cC2 (iV8468))) ### NotExists 12 % 0.21/0.54 14. (-. (cC4 (iV8467))) (-. (cC2 (iV8468))) (rR1 (iV8467) (iV8468)) ### Definition-Pseudo(cC4) 13 % 0.21/0.54 15. (rR1 (iV8467) (iV8469)) (-. (rR1 (iV8467) (iV8469))) ### Axiom % 0.21/0.54 16. (-. (Ex Y, ((rR1 (iV8469) Y) /\ (-. (cC2 Y))))) (Ex Y, ((rR1 (iV8469) Y) /\ (-. (cC2 Y)))) ### Axiom % 0.21/0.54 17. (cC6 (iV8469)) (-. (Ex Y, ((rR1 (iV8469) Y) /\ (-. (cC2 Y))))) ### Definition-Pseudo(cC6) 16 % 0.21/0.54 18. (-. (-. (cC6 (iV8469)))) (-. (Ex Y, ((rR1 (iV8469) Y) /\ (-. (cC2 Y))))) ### NotNot 17 % 0.21/0.54 19. (-. ((rR1 (iV8467) (iV8469)) /\ (-. (cC6 (iV8469))))) (-. (Ex Y, ((rR1 (iV8469) Y) /\ (-. (cC2 Y))))) (rR1 (iV8467) (iV8469)) ### NotAnd 15 18 % 0.21/0.54 20. (-. (Ex Y, ((rR1 (iV8467) Y) /\ (-. (cC6 Y))))) (rR1 (iV8467) (iV8469)) (-. (Ex Y, ((rR1 (iV8469) Y) /\ (-. (cC2 Y))))) ### NotExists 19 % 0.21/0.54 21. (-. (cC8 (iV8467))) (-. (Ex Y, ((rR1 (iV8469) Y) /\ (-. (cC2 Y))))) (rR1 (iV8467) (iV8469)) ### Definition-Pseudo(cC8) 20 % 0.21/0.54 22. (-. ((cC4 (iV8467)) /\ (cC8 (iV8467)))) (rR1 (iV8467) (iV8469)) (-. (Ex Y, ((rR1 (iV8469) Y) /\ (-. (cC2 Y))))) (rR1 (iV8467) (iV8468)) (-. (cC2 (iV8468))) ### NotAnd 14 21 % 0.21/0.54 23. (-. (cC10 (iV8467))) (-. (cC2 (iV8468))) (rR1 (iV8467) (iV8468)) (-. (Ex Y, ((rR1 (iV8469) Y) /\ (-. (cC2 Y))))) (rR1 (iV8467) (iV8469)) ### Definition-Pseudo(cC10) 22 % 0.21/0.54 24. (-. (cC48 (iV8467))) (-. (cC2 (iV8468))) (rR1 (iV8467) (iV8468)) ### Definition-Pseudo(cC48) 13 % 0.21/0.54 25. (rR1 (iV8467) (iV8471)) (-. (rR1 (iV8467) (iV8471))) ### Axiom % 0.21/0.54 26. (-. (cC2 (iV8471))) (cC2 (iV8471)) ### Axiom % 0.21/0.54 27. (-. (-. (cC2 (iV8471)))) (-. (cC2 (iV8471))) ### NotNot 26 % 0.21/0.54 28. (-. (Ex Y, ((rR1 (iV8471) Y) /\ (-. (cC2 Y))))) (Ex Y, ((rR1 (iV8471) Y) /\ (-. (cC2 Y)))) ### Axiom % 0.21/0.54 29. (cC78 (iV8471)) (-. (Ex Y, ((rR1 (iV8471) Y) /\ (-. (cC2 Y))))) ### Definition-Pseudo(cC78) 28 % 0.21/0.54 30. (-. (-. (cC78 (iV8471)))) (-. (Ex Y, ((rR1 (iV8471) Y) /\ (-. (cC2 Y))))) ### NotNot 29 % 0.21/0.54 31. (-. ((-. (cC2 (iV8471))) /\ (-. (cC78 (iV8471))))) (-. (Ex Y, ((rR1 (iV8471) Y) /\ (-. (cC2 Y))))) (-. (cC2 (iV8471))) ### NotAnd 27 30 % 0.21/0.54 32. (-. (cC80 (iV8471))) (-. (cC2 (iV8471))) (-. (Ex Y, ((rR1 (iV8471) Y) /\ (-. (cC2 Y))))) ### Definition-Pseudo(cC80) 31 % 0.21/0.54 33. (-. ((rR1 (iV8467) (iV8471)) /\ (cC80 (iV8471)))) (-. (Ex Y, ((rR1 (iV8471) Y) /\ (-. (cC2 Y))))) (-. (cC2 (iV8471))) (rR1 (iV8467) (iV8471)) ### NotAnd 25 32 % 0.21/0.54 34. (-. (Ex Y, ((rR1 (iV8467) Y) /\ (cC80 Y)))) (rR1 (iV8467) (iV8471)) (-. (cC2 (iV8471))) (-. (Ex Y, ((rR1 (iV8471) Y) /\ (-. (cC2 Y))))) ### NotExists 33 % 0.21/0.54 35. (-. (cC82 (iV8467))) (-. (Ex Y, ((rR1 (iV8471) Y) /\ (-. (cC2 Y))))) (-. (cC2 (iV8471))) (rR1 (iV8467) (iV8471)) ### Definition-Pseudo(cC82) 34 % 0.21/0.54 36. (rR1 (iV8467) (iV8470)) (-. (rR1 (iV8467) (iV8470))) ### Axiom % 0.21/0.54 37. (cTOP (iV8470)) (-. (cTOP (iV8470))) ### Axiom % 0.21/0.54 38. (-. ((rR1 (iV8467) (iV8470)) /\ (cTOP (iV8470)))) (cTOP (iV8470)) (rR1 (iV8467) (iV8470)) ### NotAnd 36 37 % 0.21/0.54 39. (-. (Ex Y, ((rR1 (iV8467) Y) /\ (cTOP Y)))) (rR1 (iV8467) (iV8470)) (cTOP (iV8470)) ### NotExists 38 % 0.21/0.54 40. (-. (cC14 (iV8467))) (cTOP (iV8470)) (rR1 (iV8467) (iV8470)) ### Definition-Pseudo(cC14) 39 % 0.21/0.54 41. (-. (cC20 (iV8467))) (-. (cC2 (iV8468))) (rR1 (iV8467) (iV8468)) ### Definition-Pseudo(cC20) 13 % 0.21/0.54 42. (cowlThing (iV8467)) (-. (cowlThing (iV8467))) ### Axiom % 0.21/0.54 43. (rR1 (iV8467) (iV8472)) (-. (rR1 (iV8467) (iV8472))) ### Axiom % 0.21/0.54 44. (rR1 (iV8472) (iV8476)) (-. (rR1 (iV8472) (iV8476))) ### Axiom % 0.21/0.54 45. (cC2 (iV8476)) (-. (cC2 (iV8476))) ### Axiom % 0.21/0.54 46. (-. ((rR1 (iV8472) (iV8476)) /\ (cC2 (iV8476)))) (cC2 (iV8476)) (rR1 (iV8472) (iV8476)) ### NotAnd 44 45 % 0.21/0.54 47. (-. (Ex Y, ((rR1 (iV8472) Y) /\ (cC2 Y)))) (rR1 (iV8472) (iV8476)) (cC2 (iV8476)) ### NotExists 46 % 0.21/0.54 48. (-. (cC58 (iV8472))) (cC2 (iV8476)) (rR1 (iV8472) (iV8476)) ### Definition-Pseudo(cC58) 47 % 0.21/0.54 49. (-. (cC2 (iV8472))) (cC2 (iV8472)) ### Axiom % 0.21/0.54 50. (-. (-. (cC2 (iV8472)))) (-. (cC2 (iV8472))) ### NotNot 49 % 0.21/0.54 51. (-. ((cC58 (iV8472)) /\ (-. (cC2 (iV8472))))) (-. (cC2 (iV8472))) (rR1 (iV8472) (iV8476)) (cC2 (iV8476)) ### NotAnd 48 50 % 0.21/0.54 52. (-. (cC60 (iV8472))) (cC2 (iV8476)) (rR1 (iV8472) (iV8476)) (-. (cC2 (iV8472))) ### Definition-Pseudo(cC60) 51 % 0.21/0.54 53. (-. ((rR1 (iV8467) (iV8472)) /\ (cC60 (iV8472)))) (-. (cC2 (iV8472))) (rR1 (iV8472) (iV8476)) (cC2 (iV8476)) (rR1 (iV8467) (iV8472)) ### NotAnd 43 52 % 0.21/0.54 54. (-. (Ex Y, ((rR1 (iV8467) Y) /\ (cC60 Y)))) (rR1 (iV8467) (iV8472)) (cC2 (iV8476)) (rR1 (iV8472) (iV8476)) (-. (cC2 (iV8472))) ### NotExists 53 % 0.21/0.54 55. (-. (cC62 (iV8467))) (-. (cC2 (iV8472))) (rR1 (iV8472) (iV8476)) (cC2 (iV8476)) (rR1 (iV8467) (iV8472)) ### Definition-Pseudo(cC62) 54 % 0.21/0.54 56. (rR1 (iV8467) (iV8474)) (-. (rR1 (iV8467) (iV8474))) ### Axiom % 0.21/0.54 57. (-. (Ex Y, ((rR1 (iV8474) Y) /\ (cC2 Y)))) (Ex Y, ((rR1 (iV8474) Y) /\ (cC2 Y))) ### Axiom % 0.21/0.54 58. (cC32 (iV8474)) (-. (Ex Y, ((rR1 (iV8474) Y) /\ (cC2 Y)))) ### Definition-Pseudo(cC32) 57 % 0.21/0.54 59. (-. (-. (cC32 (iV8474)))) (-. (Ex Y, ((rR1 (iV8474) Y) /\ (cC2 Y)))) ### NotNot 58 % 0.21/0.54 60. (-. ((rR1 (iV8467) (iV8474)) /\ (-. (cC32 (iV8474))))) (-. (Ex Y, ((rR1 (iV8474) Y) /\ (cC2 Y)))) (rR1 (iV8467) (iV8474)) ### NotAnd 56 59 % 0.21/0.54 61. (-. (Ex Y, ((rR1 (iV8467) Y) /\ (-. (cC32 Y))))) (rR1 (iV8467) (iV8474)) (-. (Ex Y, ((rR1 (iV8474) Y) /\ (cC2 Y)))) ### NotExists 60 % 0.21/0.54 62. (-. (cC34 (iV8467))) (-. (Ex Y, ((rR1 (iV8474) Y) /\ (cC2 Y)))) (rR1 (iV8467) (iV8474)) ### Definition-Pseudo(cC34) 61 % 0.21/0.54 63. (cowlThing (iV8471)) (-. (cowlThing (iV8471))) ### Axiom % 0.21/0.54 64. (cowlThing (iV8472)) (-. (cowlThing (iV8472))) ### Axiom % 0.21/0.54 65. (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC10 (iV8467)) /\ ((cC48 (iV8467)) /\ ((cC4 (iV8467)) /\ ((cC82 (iV8467)) /\ ((cC14 (iV8467)) /\ ((cC8 (iV8467)) /\ ((cC20 (iV8467)) /\ ((cowlThing (iV8467)) /\ ((cC62 (iV8467)) /\ ((cC34 (iV8467)) /\ ((cowlThing (iV8471)) /\ ((cC80 (iV8471)) /\ ((cC60 (iV8472)) /\ ((cowlThing (iV8472)) /\ (cC58 (iV8472))))))))))))))))))) (cowlThing (iV8472)) (cowlThing (iV8471)) (rR1 (iV8467) (iV8474)) (-. (Ex Y, ((rR1 (iV8474) Y) /\ (cC2 Y)))) (rR1 (iV8467) (iV8472)) (cC2 (iV8476)) (rR1 (iV8472) (iV8476)) (-. (cC2 (iV8472))) (cowlThing (iV8467)) (rR1 (iV8467) (iV8470)) (cTOP (iV8470)) (rR1 (iV8467) (iV8471)) (-. (cC2 (iV8471))) (-. (Ex Y, ((rR1 (iV8471) Y) /\ (-. (cC2 Y))))) (rR1 (iV8467) (iV8469)) (-. (Ex Y, ((rR1 (iV8469) Y) /\ (-. (cC2 Y))))) (rR1 (iV8467) (iV8468)) (-. (cC2 (iV8468))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### DisjTree 1 8 23 24 14 35 40 21 41 42 55 62 63 32 52 64 48 % 0.21/0.54 66. (-. (cC6 (iV8469))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC2 (iV8468))) (rR1 (iV8467) (iV8468)) (rR1 (iV8467) (iV8469)) (-. (Ex Y, ((rR1 (iV8471) Y) /\ (-. (cC2 Y))))) (-. (cC2 (iV8471))) (rR1 (iV8467) (iV8471)) (cTOP (iV8470)) (rR1 (iV8467) (iV8470)) (cowlThing (iV8467)) (-. (cC2 (iV8472))) (rR1 (iV8472) (iV8476)) (cC2 (iV8476)) (rR1 (iV8467) (iV8472)) (-. (Ex Y, ((rR1 (iV8474) Y) /\ (cC2 Y)))) (rR1 (iV8467) (iV8474)) (cowlThing (iV8471)) (cowlThing (iV8472)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC10 (iV8467)) /\ ((cC48 (iV8467)) /\ ((cC4 (iV8467)) /\ ((cC82 (iV8467)) /\ ((cC14 (iV8467)) /\ ((cC8 (iV8467)) /\ ((cC20 (iV8467)) /\ ((cowlThing (iV8467)) /\ ((cC62 (iV8467)) /\ ((cC34 (iV8467)) /\ ((cowlThing (iV8471)) /\ ((cC80 (iV8471)) /\ ((cC60 (iV8472)) /\ ((cowlThing (iV8472)) /\ (cC58 (iV8472))))))))))))))))))) ### Definition-Pseudo(cC6) 65 % 0.21/0.54 67. (-. (cC78 (iV8471))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC10 (iV8467)) /\ ((cC48 (iV8467)) /\ ((cC4 (iV8467)) /\ ((cC82 (iV8467)) /\ ((cC14 (iV8467)) /\ ((cC8 (iV8467)) /\ ((cC20 (iV8467)) /\ ((cowlThing (iV8467)) /\ ((cC62 (iV8467)) /\ ((cC34 (iV8467)) /\ ((cowlThing (iV8471)) /\ ((cC80 (iV8471)) /\ ((cC60 (iV8472)) /\ ((cowlThing (iV8472)) /\ (cC58 (iV8472))))))))))))))))))) (cowlThing (iV8472)) (cowlThing (iV8471)) (rR1 (iV8467) (iV8474)) (-. (Ex Y, ((rR1 (iV8474) Y) /\ (cC2 Y)))) (rR1 (iV8467) (iV8472)) (cC2 (iV8476)) (rR1 (iV8472) (iV8476)) (-. (cC2 (iV8472))) (cowlThing (iV8467)) (rR1 (iV8467) (iV8470)) (cTOP (iV8470)) (rR1 (iV8467) (iV8471)) (-. (cC2 (iV8471))) (rR1 (iV8467) (iV8469)) (rR1 (iV8467) (iV8468)) (-. (cC2 (iV8468))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC6 (iV8469))) ### Definition-Pseudo(cC78) 66 % 0.21/0.54 68. (-. (cC32 (iV8474))) (-. (cC6 (iV8469))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC2 (iV8468))) (rR1 (iV8467) (iV8468)) (rR1 (iV8467) (iV8469)) (-. (cC2 (iV8471))) (rR1 (iV8467) (iV8471)) (cTOP (iV8470)) (rR1 (iV8467) (iV8470)) (cowlThing (iV8467)) (-. (cC2 (iV8472))) (rR1 (iV8472) (iV8476)) (cC2 (iV8476)) (rR1 (iV8467) (iV8472)) (rR1 (iV8467) (iV8474)) (cowlThing (iV8471)) (cowlThing (iV8472)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC10 (iV8467)) /\ ((cC48 (iV8467)) /\ ((cC4 (iV8467)) /\ ((cC82 (iV8467)) /\ ((cC14 (iV8467)) /\ ((cC8 (iV8467)) /\ ((cC20 (iV8467)) /\ ((cowlThing (iV8467)) /\ ((cC62 (iV8467)) /\ ((cC34 (iV8467)) /\ ((cowlThing (iV8471)) /\ ((cC80 (iV8471)) /\ ((cC60 (iV8472)) /\ ((cowlThing (iV8472)) /\ (cC58 (iV8472))))))))))))))))))) (-. (cC78 (iV8471))) ### Definition-Pseudo(cC32) 67 % 0.21/0.54 % SZS output end Proof % 0.21/0.54 (* END-PROOF *) %------------------------------------------------------------------------------