%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS140+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 : n023.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:01 EDT 2022 % Result : Theorem 240.31s 240.55s % Output : Proof 240.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS140+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n023.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jun 7 15:29:53 EDT 2022 % 0.13/0.34 % CPUTime : % 240.31/240.55 % SZS status Theorem % 240.31/240.55 (* PROOF-FOUND *) % 240.31/240.55 (* BEGIN-PROOF *) % 240.31/240.55 % SZS output start Proof % 240.31/240.55 1. (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (All X, ((cowlThing X) /\ (-. (cowlNothing X))))) ### Axiom % 240.31/240.55 2. (-. (xsd_integer T_0)) (xsd_integer T_0) ### Axiom % 240.31/240.55 3. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### NotNot 2 % 240.31/240.55 4. (-. (xsd_string T_0)) (-. (xsd_integer T_0)) ### Definition-Pseudo(xsd_string) 3 % 240.31/240.55 5. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### Axiom % 240.31/240.55 6. (xsd_string T_0) (-. (-. (xsd_integer T_0))) ### Definition-Pseudo(xsd_string) 5 % 240.31/240.55 7. (-. ((xsd_string T_0) <=> (-. (xsd_integer T_0)))) ### NotEquiv 4 6 % 240.31/240.55 8. (-. (All X, ((xsd_string X) <=> (-. (xsd_integer X))))) ### NotAllEx 7 % 240.31/240.55 9. (rsymProp T_1 T_2) (-. (rsymProp T_2 T_1)) ### Sym(rsymProp) % 240.31/240.55 10. ((ia) != T_1) (T_1 = (ia)) ### Sym(=) % 240.31/240.55 11. ((ib) != T_1) (T_1 = (ib)) ### Sym(=) % 240.31/240.55 12. ((rsymProp T_2 T_1) => ((T_1 = (ia)) \/ (T_1 = (ib)))) ((ib) != T_1) ((ia) != T_1) (rsymProp T_1 T_2) ### DisjTree 9 10 11 % 240.31/240.55 13. (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_1 T_2) ((ia) != T_1) ((ib) != T_1) ### All 12 % 240.31/240.55 14. (rsymProp T_2 T_3) (-. (rsymProp T_2 T_3)) ### Axiom % 240.31/240.55 15. ((ia) != T_3) (T_3 = (ia)) ### Sym(=) % 240.31/240.55 16. (rsymProp T_1 T_2) (-. (rsymProp T_2 T_1)) ### Sym(rsymProp) % 240.31/240.55 17. (T_1 != T_1) ### Refl(=) % 240.31/240.55 18. (T_1 != T_1) ### Refl(=) % 240.31/240.55 19. (T_3 != T_3) ### Refl(=) % 240.31/240.55 20. (rsymProp T_1 T_2) (-. (rsymProp T_1 T_2)) ### Axiom % 240.31/240.55 21. ((ia) != T_2) (T_2 = (ia)) ### Sym(=) % 240.31/240.55 22. ((ib) != T_2) (T_2 = (ib)) ### Sym(=) % 240.31/240.55 23. ((rsymProp T_1 T_2) => ((T_2 = (ia)) \/ (T_2 = (ib)))) ((ib) != T_2) ((ia) != T_2) (rsymProp T_1 T_2) ### DisjTree 20 21 22 % 240.31/240.55 24. (All Y, ((rsymProp T_1 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_1 T_2) ((ia) != T_2) ((ib) != T_2) ### All 23 % 240.31/240.55 25. (T_3 != T_2) (T_3 = (ib)) ((ia) != T_2) (rsymProp T_1 T_2) (All Y, ((rsymProp T_1 Y) => ((Y = (ia)) \/ (Y = (ib))))) ### Trans 19 24 % 240.31/240.55 26. (rsymProp T_2 T_3) (-. (rsymProp T_2 T_3)) ### Axiom % 240.31/240.55 27. (-. (rsymProp T_2 T_2)) (rsymProp T_2 T_2) ### Axiom % 240.31/240.55 28. (((T_3 = T_2) /\ (rsymProp T_2 T_3)) => (rsymProp T_2 T_2)) (-. (rsymProp T_2 T_2)) (rsymProp T_2 T_3) (All Y, ((rsymProp T_1 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_1 T_2) ((ia) != T_2) (T_3 = (ib)) ### DisjTree 25 26 27 % 240.31/240.55 29. (All C, (((T_3 = T_2) /\ (rsymProp C T_3)) => (rsymProp C T_2))) (T_3 = (ib)) ((ia) != T_2) (rsymProp T_1 T_2) (All Y, ((rsymProp T_1 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_2 T_3) (-. (rsymProp T_2 T_2)) ### All 28 % 240.31/240.55 30. (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (-. (rsymProp T_2 T_2)) (rsymProp T_2 T_3) (rsymProp T_1 T_2) ((ia) != T_2) (T_3 = (ib)) (All C, (((T_3 = T_2) /\ (rsymProp C T_3)) => (rsymProp C T_2))) ### All 29 % 240.31/240.55 31. (T_2 != T_1) (T_1 = (ia)) (All C, (((T_3 = T_2) /\ (rsymProp C T_3)) => (rsymProp C T_2))) (T_3 = (ib)) (rsymProp T_1 T_2) (rsymProp T_2 T_3) (-. (rsymProp T_2 T_2)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) ### TransEq-sym 17 18 30 % 240.31/240.55 32. (T_1 != T_1) ### Refl(=) % 240.31/240.55 33. (T_1 != T_1) ### Refl(=) % 240.31/240.55 34. (T_2 = (ia)) ((ia) != T_2) ### Sym(=) % 240.31/240.55 35. (T_2 != T_1) (T_1 = (ia)) (T_2 = (ia)) ### TransEq-sym 32 33 34 % 240.31/240.55 36. (T_1 != T_1) ### Refl(=) % 240.31/240.55 37. (T_2 != T_2) ### Refl(=) % 240.31/240.55 38. (T_3 = (ib)) ((ib) != T_3) ### Sym(=) % 240.31/240.55 39. (T_2 != T_3) (T_2 = (ib)) (T_3 = (ib)) ### Trans 37 38 % 240.31/240.55 40. (-. (rsymProp T_1 T_3)) (rsymProp T_1 T_2) (T_3 = (ib)) (T_2 = (ib)) ### P-NotP 36 39 % 240.31/240.55 41. ((rsymProp T_2 T_2) => ((T_2 = (ia)) \/ (T_2 = (ib)))) (-. (rsymProp T_1 T_3)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp T_2 T_3) (rsymProp T_1 T_2) (T_3 = (ib)) (All C, (((T_3 = T_2) /\ (rsymProp C T_3)) => (rsymProp C T_2))) (T_1 = (ia)) (T_2 != T_1) ### DisjTree 31 35 40 % 240.31/240.55 42. (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (T_2 != T_1) (T_1 = (ia)) (All C, (((T_3 = T_2) /\ (rsymProp C T_3)) => (rsymProp C T_2))) (T_3 = (ib)) (rsymProp T_1 T_2) (rsymProp T_2 T_3) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (-. (rsymProp T_1 T_3)) ### All 41 % 240.31/240.55 43. ((ib) != T_1) (T_1 = (ib)) ### Sym(=) % 240.31/240.55 44. ((rsymProp T_2 T_1) => ((T_1 = (ia)) \/ (T_1 = (ib)))) ((ib) != T_1) (-. (rsymProp T_1 T_3)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp T_2 T_3) (T_3 = (ib)) (All C, (((T_3 = T_2) /\ (rsymProp C T_3)) => (rsymProp C T_2))) (T_2 != T_1) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_1 T_2) ### DisjTree 16 42 43 % 240.31/240.55 45. (rsymProp T_1 T_2) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (T_2 != T_1) (All C, (((T_3 = T_2) /\ (rsymProp C T_3)) => (rsymProp C T_2))) (T_3 = (ib)) (rsymProp T_2 T_3) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (-. (rsymProp T_1 T_3)) ((ib) != T_1) ### All 44 % 240.31/240.55 46. (T_3 != T_3) ### Refl(=) % 240.31/240.55 47. ((ib) != T_1) (-. (rsymProp T_1 T_3)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp T_2 T_3) (T_3 = (ib)) (All C, (((T_3 = T_2) /\ (rsymProp C T_3)) => (rsymProp C T_2))) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_1 T_2) ### P-NotP 45 46 % 240.31/240.55 48. (rsymProp T_1 T_2) (All C, (((T_3 = T_2) /\ (rsymProp C T_3)) => (rsymProp C T_2))) (T_3 = (ib)) (rsymProp T_2 T_3) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (-. (rsymProp T_1 T_3)) ((ib) != T_1) ### All 47 % 240.31/240.55 49. (All B, (All C, (((T_3 = B) /\ (rsymProp C T_3)) => (rsymProp C B)))) ((ib) != T_1) (-. (rsymProp T_1 T_3)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp T_2 T_3) (T_3 = (ib)) (rsymProp T_1 T_2) ### All 48 % 240.31/240.55 50. ((rsymProp T_2 T_3) => ((T_3 = (ia)) \/ (T_3 = (ib)))) (rsymProp T_1 T_2) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (-. (rsymProp T_1 T_3)) ((ib) != T_1) (All B, (All C, (((T_3 = B) /\ (rsymProp C T_3)) => (rsymProp C B)))) ((ia) != T_3) (rsymProp T_2 T_3) ### DisjTree 14 15 49 % 240.31/240.55 51. (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_2 T_3) ((ia) != T_3) (All B, (All C, (((T_3 = B) /\ (rsymProp C T_3)) => (rsymProp C B)))) ((ib) != T_1) (-. (rsymProp T_1 T_3)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp T_1 T_2) ### All 50 % 240.31/240.55 52. (rsymProp (ia) (ia)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (-. (rsymProp T_1 T_3)) (All B, (All C, (((T_3 = B) /\ (rsymProp C T_3)) => (rsymProp C B)))) (rsymProp T_2 T_3) ((ib) != T_1) (rsymProp T_1 T_2) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) ### P-NotP-sym(rsymProp) 13 51 % 240.31/240.55 53. (rsymProp T_1 T_2) (-. (rsymProp T_1 T_2)) ### Axiom % 240.31/240.55 54. (T_2 != T_2) ### Refl(=) % 240.31/240.55 55. (T_2 != T_2) ### Refl(=) % 240.31/240.55 56. (rsymProp T_2 T_3) (-. (rsymProp T_2 T_3)) ### Axiom % 240.31/240.55 57. ((ia) != T_3) (T_3 = (ia)) ### Sym(=) % 240.31/240.55 58. ((ib) != T_3) (T_3 = (ib)) ### Sym(=) % 240.31/240.55 59. ((rsymProp T_2 T_3) => ((T_3 = (ia)) \/ (T_3 = (ib)))) ((ib) != T_3) ((ia) != T_3) (rsymProp T_2 T_3) ### DisjTree 56 57 58 % 240.31/240.55 60. (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_2 T_3) ((ia) != T_3) ((ib) != T_3) ### All 59 % 240.31/240.55 61. (T_2 != T_3) (T_2 = (ia)) ((ib) != T_3) (rsymProp T_2 T_3) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) ### TransEq 54 55 60 % 240.31/240.55 62. (rsymProp T_1 T_2) (-. (rsymProp T_2 T_1)) ### Sym(rsymProp) % 240.31/240.55 63. ((ia) != T_1) (T_1 = (ia)) ### Sym(=) % 240.31/240.55 64. (T_2 != T_2) ### Refl(=) % 240.31/240.55 65. (T_1 = (ib)) ((ib) != T_1) ### Sym(=) % 240.31/240.55 66. (T_2 != T_1) (T_2 = (ib)) (T_1 = (ib)) ### Trans 64 65 % 240.31/240.55 67. (T_3 != T_3) ### Refl(=) % 240.31/240.55 68. (-. (rsymProp T_1 T_3)) (rsymProp T_2 T_3) (T_1 = (ib)) (T_2 = (ib)) ### P-NotP 66 67 % 240.31/240.55 69. ((rsymProp T_2 T_1) => ((T_1 = (ia)) \/ (T_1 = (ib)))) (T_2 = (ib)) (rsymProp T_2 T_3) (-. (rsymProp T_1 T_3)) ((ia) != T_1) (rsymProp T_1 T_2) ### DisjTree 62 63 68 % 240.31/240.55 70. ((rsymProp T_1 T_2) => ((T_2 = (ia)) \/ (T_2 = (ib)))) ((ia) != T_1) (-. (rsymProp T_1 T_3)) ((rsymProp T_2 T_1) => ((T_1 = (ia)) \/ (T_1 = (ib)))) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_2 T_3) ((ib) != T_3) (T_2 != T_3) (rsymProp T_1 T_2) ### DisjTree 53 61 69 % 240.31/240.55 71. (rsymProp T_1 T_2) (-. (rsymProp T_1 T_2)) ### Axiom % 240.31/240.55 72. (-. (rsymProp T_1 T_3)) (rsymProp T_1 T_3) ### Axiom % 240.31/240.55 73. (((T_2 = T_3) /\ (rsymProp T_1 T_2)) => (rsymProp T_1 T_3)) (rsymProp T_1 T_2) ((ib) != T_3) (rsymProp T_2 T_3) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) ((rsymProp T_2 T_1) => ((T_1 = (ia)) \/ (T_1 = (ib)))) (-. (rsymProp T_1 T_3)) ((ia) != T_1) ((rsymProp T_1 T_2) => ((T_2 = (ia)) \/ (T_2 = (ib)))) ### DisjTree 70 71 72 % 240.31/240.57 74. (All C, (((T_2 = T_3) /\ (rsymProp C T_2)) => (rsymProp C T_3))) ((rsymProp T_1 T_2) => ((T_2 = (ia)) \/ (T_2 = (ib)))) ((ia) != T_1) (-. (rsymProp T_1 T_3)) ((rsymProp T_2 T_1) => ((T_1 = (ia)) \/ (T_1 = (ib)))) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_2 T_3) ((ib) != T_3) (rsymProp T_1 T_2) ### All 73 % 240.31/240.57 75. (All Y, ((rsymProp T_1 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_1 T_2) ((ib) != T_3) (rsymProp T_2 T_3) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) ((rsymProp T_2 T_1) => ((T_1 = (ia)) \/ (T_1 = (ib)))) (-. (rsymProp T_1 T_3)) ((ia) != T_1) (All C, (((T_2 = T_3) /\ (rsymProp C T_2)) => (rsymProp C T_3))) ### All 74 % 240.31/240.57 76. (All C, (((T_2 = T_3) /\ (rsymProp C T_2)) => (rsymProp C T_3))) ((ia) != T_1) (-. (rsymProp T_1 T_3)) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_2 T_3) ((ib) != T_3) (rsymProp T_1 T_2) (All Y, ((rsymProp T_1 Y) => ((Y = (ia)) \/ (Y = (ib))))) ### All 75 % 240.31/240.57 77. (All B, (All C, (((T_2 = B) /\ (rsymProp C T_2)) => (rsymProp C B)))) (All Y, ((rsymProp T_1 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_1 T_2) ((ib) != T_3) (rsymProp T_2 T_3) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (-. (rsymProp T_1 T_3)) ((ia) != T_1) ### All 76 % 240.31/240.57 78. (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) ((ia) != T_1) (-. (rsymProp T_1 T_3)) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_2 T_3) ((ib) != T_3) (rsymProp T_1 T_2) (All B, (All C, (((T_2 = B) /\ (rsymProp C T_2)) => (rsymProp C B)))) ### All 77 % 240.31/240.57 79. (rsymProp (ia) (ia)) (All B, (All C, (((T_2 = B) /\ (rsymProp C T_2)) => (rsymProp C B)))) (rsymProp T_1 T_2) ((ib) != T_3) (rsymProp T_2 T_3) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (-. (rsymProp T_1 T_3)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) ### P-NotP-sym(rsymProp) 78 60 % 240.31/240.57 80. (rsymProp (ib) (ib)) (All B, (All C, (((T_2 = B) /\ (rsymProp C T_2)) => (rsymProp C B)))) (All Y, ((rsymProp T_2 Y) => ((Y = (ia)) \/ (Y = (ib))))) (rsymProp T_1 T_2) (rsymProp T_2 T_3) (All B, (All C, (((T_3 = B) /\ (rsymProp C T_3)) => (rsymProp C B)))) (-. (rsymProp T_1 T_3)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp (ia) (ia)) ### P-NotP-sym(rsymProp) 52 79 % 240.31/240.57 81. (rsymProp (ia) (ia)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (-. (rsymProp T_1 T_3)) (All B, (All C, (((T_3 = B) /\ (rsymProp C T_3)) => (rsymProp C B)))) (rsymProp T_2 T_3) (rsymProp T_1 T_2) (All B, (All C, (((T_2 = B) /\ (rsymProp C T_2)) => (rsymProp C B)))) (rsymProp (ib) (ib)) ### All 80 % 240.31/240.57 82. (All A, (All B, (All C, (((A = B) /\ (rsymProp C A)) => (rsymProp C B))))) (rsymProp (ib) (ib)) (rsymProp T_1 T_2) (rsymProp T_2 T_3) (All B, (All C, (((T_3 = B) /\ (rsymProp C T_3)) => (rsymProp C B)))) (-. (rsymProp T_1 T_3)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp (ia) (ia)) ### All 81 % 240.31/240.57 83. (rsymProp (ia) (ia)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (-. (rsymProp T_1 T_3)) (rsymProp T_2 T_3) (rsymProp T_1 T_2) (rsymProp (ib) (ib)) (All A, (All B, (All C, (((A = B) /\ (rsymProp C A)) => (rsymProp C B))))) ### All 82 % 240.31/240.57 84. (-. (((rsymProp T_1 T_2) /\ (rsymProp T_2 T_3)) => (rsymProp T_1 T_3))) (All A, (All B, (All C, (((A = B) /\ (rsymProp C A)) => (rsymProp C B))))) (rsymProp (ib) (ib)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp (ia) (ia)) ### ConjTree 83 % 240.31/240.57 85. (-. (All Z, (((rsymProp T_1 T_2) /\ (rsymProp T_2 Z)) => (rsymProp T_1 Z)))) (rsymProp (ia) (ia)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp (ib) (ib)) (All A, (All B, (All C, (((A = B) /\ (rsymProp C A)) => (rsymProp C B))))) ### NotAllEx 84 % 240.31/240.57 86. (-. (All Y, (All Z, (((rsymProp T_1 Y) /\ (rsymProp Y Z)) => (rsymProp T_1 Z))))) (All A, (All B, (All C, (((A = B) /\ (rsymProp C A)) => (rsymProp C B))))) (rsymProp (ib) (ib)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp (ia) (ia)) ### NotAllEx 85 % 240.31/240.57 87. (-. (All X, (All Y, (All Z, (((rsymProp X Y) /\ (rsymProp Y Z)) => (rsymProp X Z)))))) (rsymProp (ia) (ia)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp (ib) (ib)) (All A, (All B, (All C, (((A = B) /\ (rsymProp C A)) => (rsymProp C B))))) ### NotAllEx 86 % 240.31/240.57 88. (rsymProp (ia) (ia)) (-. (rsymProp (ia) (ia))) ### Axiom % 240.31/240.57 89. (cowlThing (ia)) (-. (cowlThing (ia))) ### Axiom % 240.31/240.57 90. (-. ((rsymProp (ia) (ia)) /\ (cowlThing (ia)))) (cowlThing (ia)) (rsymProp (ia) (ia)) ### NotAnd 88 89 % 240.31/240.57 91. (-. (Ex X, ((rsymProp (ia) X) /\ (cowlThing X)))) (rsymProp (ia) (ia)) (cowlThing (ia)) ### NotExists 90 % 240.31/240.57 92. (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((All X, (All Y, (All Z, (((rsymProp X Y) /\ (rsymProp Y Z)) => (rsymProp X Z))))) /\ (Ex X, ((rsymProp (ia) X) /\ (cowlThing X))))))) (cowlThing (ia)) (All A, (All B, (All C, (((A = B) /\ (rsymProp C A)) => (rsymProp C B))))) (rsymProp (ib) (ib)) (All X, (All Y, ((rsymProp X Y) => ((Y = (ia)) \/ (Y = (ib)))))) (rsymProp (ia) (ia)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### DisjTree 1 8 87 91 % 240.31/240.57 % SZS output end Proof % 240.31/240.57 (* END-PROOF *) %------------------------------------------------------------------------------