%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS138+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 : n032.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:00 EDT 2022 % Result : Theorem 1.62s 1.86s % Output : Proof 1.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : KRS138+1 : TPTP v8.1.0. Released v3.1.0. % 0.10/0.10 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.10/0.30 % Computer : n032.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 600 % 0.10/0.30 % DateTime : Tue Jun 7 10:35:20 EDT 2022 % 0.10/0.30 % CPUTime : % 1.62/1.86 % SZS status Theorem % 1.62/1.86 (* PROOF-FOUND *) % 1.62/1.86 (* BEGIN-PROOF *) % 1.62/1.86 % SZS output start Proof % 1.62/1.86 1. (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (All X, ((cowlThing X) /\ (-. (cowlNothing X))))) ### Axiom % 1.62/1.86 2. (-. (xsd_integer T_0)) (xsd_integer T_0) ### Axiom % 1.62/1.86 3. (-. (xsd_string T_0)) (-. (xsd_integer T_0)) ### Extension/test/not_axiom_1 2 % 1.62/1.86 4. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### Axiom % 1.62/1.86 5. (xsd_string T_0) (-. (-. (xsd_integer T_0))) ### Extension/test/axiom_1 4 % 1.62/1.86 6. (-. ((xsd_string T_0) <=> (-. (xsd_integer T_0)))) ### NotEquiv 3 5 % 1.62/1.86 7. (-. (All X, ((xsd_string X) <=> (-. (xsd_integer X))))) ### NotAllEx 6 % 1.62/1.86 8. (requalityOnA (ib) (ib)) (-. (requalityOnA (ib) (ib))) ### Axiom % 1.62/1.86 9. (T_1 = (ib)) (T_1 != (ib)) ### Axiom % 1.62/1.86 10. (requalityOnA T_2 T_1) (-. (requalityOnA T_2 T_1)) ### Axiom % 1.62/1.86 11. (-. (requalityOnA T_2 (ib))) (requalityOnA T_2 (ib)) ### Axiom % 1.62/1.86 12. (((T_1 = (ib)) /\ (requalityOnA T_2 T_1)) => (requalityOnA T_2 (ib))) (-. (requalityOnA T_2 (ib))) (requalityOnA T_2 T_1) (T_1 = (ib)) ### DisjTree 9 10 11 % 1.62/1.86 13. (All C, (((T_1 = (ib)) /\ (requalityOnA C T_1)) => (requalityOnA C (ib)))) (T_1 = (ib)) (requalityOnA T_2 T_1) (-. (requalityOnA T_2 (ib))) ### All 12 % 1.62/1.86 14. (T_2 != (ib)) ((ib) = T_2) ### Sym(=) % 1.62/1.86 15. (((requalityOnA (ib) (ib)) /\ (requalityOnA T_2 (ib))) => ((ib) = T_2)) (T_2 != (ib)) (requalityOnA T_2 T_1) (T_1 = (ib)) (All C, (((T_1 = (ib)) /\ (requalityOnA C T_1)) => (requalityOnA C (ib)))) (requalityOnA (ib) (ib)) ### DisjTree 8 13 14 % 1.62/1.86 16. (All Z, (((requalityOnA (ib) (ib)) /\ (requalityOnA Z (ib))) => ((ib) = Z))) (requalityOnA (ib) (ib)) (All C, (((T_1 = (ib)) /\ (requalityOnA C T_1)) => (requalityOnA C (ib)))) (T_1 = (ib)) (requalityOnA T_2 T_1) (T_2 != (ib)) ### All 15 % 1.62/1.86 17. (All Y, (All Z, (((requalityOnA Y (ib)) /\ (requalityOnA Z (ib))) => (Y = Z)))) (T_2 != (ib)) (requalityOnA T_2 T_1) (T_1 = (ib)) (All C, (((T_1 = (ib)) /\ (requalityOnA C T_1)) => (requalityOnA C (ib)))) (requalityOnA (ib) (ib)) ### All 16 % 1.62/1.86 18. (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (requalityOnA (ib) (ib)) (All C, (((T_1 = (ib)) /\ (requalityOnA C T_1)) => (requalityOnA C (ib)))) (T_1 = (ib)) (requalityOnA T_2 T_1) (T_2 != (ib)) ### All 17 % 1.62/1.86 19. (All B, (All C, (((T_1 = B) /\ (requalityOnA C T_1)) => (requalityOnA C B)))) (T_2 != (ib)) (requalityOnA T_2 T_1) (T_1 = (ib)) (requalityOnA (ib) (ib)) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) ### All 18 % 1.62/1.86 20. (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (requalityOnA (ib) (ib)) (T_1 = (ib)) (requalityOnA T_2 T_1) (T_2 != (ib)) ### All 19 % 1.62/1.86 21. (T_1 = (ia)) (T_1 != (ia)) ### Axiom % 1.62/1.86 22. (requalityOnA T_2 T_1) (-. (requalityOnA T_2 T_1)) ### Axiom % 1.62/1.86 23. (requalityOnA (ia) (ia)) (-. (requalityOnA (ia) (ia))) ### Axiom % 1.62/1.86 24. (requalityOnA T_2 (ia)) (-. (requalityOnA T_2 (ia))) ### Axiom % 1.62/1.86 25. (T_2 != (ia)) ((ia) = T_2) ### Sym(=) % 1.62/1.86 26. (((requalityOnA (ia) (ia)) /\ (requalityOnA T_2 (ia))) => ((ia) = T_2)) (T_2 != (ia)) (requalityOnA T_2 (ia)) (requalityOnA (ia) (ia)) ### DisjTree 23 24 25 % 1.62/1.86 27. (All Z, (((requalityOnA (ia) (ia)) /\ (requalityOnA Z (ia))) => ((ia) = Z))) (requalityOnA (ia) (ia)) (requalityOnA T_2 (ia)) (T_2 != (ia)) ### All 26 % 1.62/1.86 28. (((T_1 = (ia)) /\ (requalityOnA T_2 T_1)) => (requalityOnA T_2 (ia))) (T_2 != (ia)) (requalityOnA (ia) (ia)) (All Z, (((requalityOnA (ia) (ia)) /\ (requalityOnA Z (ia))) => ((ia) = Z))) (requalityOnA T_2 T_1) (T_1 = (ia)) ### DisjTree 21 22 27 % 1.62/1.86 29. (All C, (((T_1 = (ia)) /\ (requalityOnA C T_1)) => (requalityOnA C (ia)))) (T_1 = (ia)) (requalityOnA T_2 T_1) (All Z, (((requalityOnA (ia) (ia)) /\ (requalityOnA Z (ia))) => ((ia) = Z))) (requalityOnA (ia) (ia)) (T_2 != (ia)) ### All 28 % 1.62/1.86 30. (All Y, (All Z, (((requalityOnA Y (ia)) /\ (requalityOnA Z (ia))) => (Y = Z)))) (T_2 != (ia)) (requalityOnA (ia) (ia)) (requalityOnA T_2 T_1) (T_1 = (ia)) (All C, (((T_1 = (ia)) /\ (requalityOnA C T_1)) => (requalityOnA C (ia)))) ### All 29 % 1.62/1.86 31. (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (All C, (((T_1 = (ia)) /\ (requalityOnA C T_1)) => (requalityOnA C (ia)))) (T_1 = (ia)) (requalityOnA T_2 T_1) (requalityOnA (ia) (ia)) (T_2 != (ia)) ### All 30 % 1.62/1.86 32. (All B, (All C, (((T_1 = B) /\ (requalityOnA C T_1)) => (requalityOnA C B)))) (T_2 != (ia)) (requalityOnA (ia) (ia)) (requalityOnA T_2 T_1) (T_1 = (ia)) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) ### All 31 % 1.62/1.86 33. (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (T_1 = (ia)) (requalityOnA T_2 T_1) (requalityOnA (ia) (ia)) (T_2 != (ia)) ### All 32 % 1.62/1.86 34. (cA T_1) (T_2 != (ia)) (requalityOnA (ia) (ia)) (T_2 != (ib)) (requalityOnA T_2 T_1) (requalityOnA (ib) (ib)) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) ### Extension/test/axiom_2 20 33 % 1.62/1.86 35. (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (requalityOnA (ib) (ib)) (requalityOnA T_2 T_1) (T_2 != (ib)) (requalityOnA (ia) (ia)) (T_2 != (ia)) ### Extension/test/axiom_4 34 % 1.62/1.86 36. (-. ((requalityOnA T_2 T_1) => ((T_2 = (ia)) \/ ((T_2 = (ib)) \/ (T_2 = (ic)))))) (requalityOnA (ia) (ia)) (requalityOnA (ib) (ib)) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) ### ConjTree 35 % 1.62/1.86 37. (-. (All Y, ((requalityOnA T_2 Y) => ((T_2 = (ia)) \/ ((T_2 = (ib)) \/ (T_2 = (ic))))))) (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (requalityOnA (ib) (ib)) (requalityOnA (ia) (ia)) ### NotAllEx 36 % 1.62/1.86 38. (-. (All X, (All Y, ((requalityOnA X Y) => ((X = (ia)) \/ ((X = (ib)) \/ (X = (ic)))))))) (requalityOnA (ia) (ia)) (requalityOnA (ib) (ib)) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) ### NotAllEx 37 % 1.62/1.86 39. (T_3 = (ib)) ((ib) != T_3) ### Sym(=) % 1.62/1.86 40. (T_3 = (ib)) (T_3 != (ib)) ### Axiom % 1.62/1.86 41. (requalityOnA T_4 T_3) (-. (requalityOnA T_4 T_3)) ### Axiom % 1.62/1.86 42. (requalityOnA (ib) (ib)) (-. (requalityOnA (ib) (ib))) ### Axiom % 1.62/1.86 43. (requalityOnA T_4 (ib)) (-. (requalityOnA T_4 (ib))) ### Axiom % 1.62/1.86 44. ((ib) != T_4) ((ib) = T_4) ### Axiom % 1.62/1.86 45. (((requalityOnA (ib) (ib)) /\ (requalityOnA T_4 (ib))) => ((ib) = T_4)) ((ib) != T_4) (requalityOnA T_4 (ib)) (requalityOnA (ib) (ib)) ### DisjTree 42 43 44 % 1.62/1.86 46. (All Z, (((requalityOnA (ib) (ib)) /\ (requalityOnA Z (ib))) => ((ib) = Z))) (requalityOnA (ib) (ib)) (requalityOnA T_4 (ib)) ((ib) != T_4) ### All 45 % 1.62/1.86 47. (All Y, (All Z, (((requalityOnA Y (ib)) /\ (requalityOnA Z (ib))) => (Y = Z)))) ((ib) != T_4) (requalityOnA T_4 (ib)) (requalityOnA (ib) (ib)) ### All 46 % 1.62/1.86 48. (((T_3 = (ib)) /\ (requalityOnA T_4 T_3)) => (requalityOnA T_4 (ib))) (requalityOnA (ib) (ib)) ((ib) != T_4) (All Y, (All Z, (((requalityOnA Y (ib)) /\ (requalityOnA Z (ib))) => (Y = Z)))) (requalityOnA T_4 T_3) (T_3 = (ib)) ### DisjTree 40 41 47 % 1.62/1.86 49. (All C, (((T_3 = (ib)) /\ (requalityOnA C T_3)) => (requalityOnA C (ib)))) (T_3 = (ib)) (requalityOnA T_4 T_3) (All Y, (All Z, (((requalityOnA Y (ib)) /\ (requalityOnA Z (ib))) => (Y = Z)))) ((ib) != T_4) (requalityOnA (ib) (ib)) ### All 48 % 1.62/1.86 50. (-. (requalityOnA T_3 T_4)) (requalityOnA (ib) (ib)) (All Y, (All Z, (((requalityOnA Y (ib)) /\ (requalityOnA Z (ib))) => (Y = Z)))) (requalityOnA T_4 T_3) (All C, (((T_3 = (ib)) /\ (requalityOnA C T_3)) => (requalityOnA C (ib)))) (T_3 = (ib)) ### P-NotP 39 49 % 1.62/1.86 51. (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (T_3 = (ib)) (All C, (((T_3 = (ib)) /\ (requalityOnA C T_3)) => (requalityOnA C (ib)))) (requalityOnA T_4 T_3) (requalityOnA (ib) (ib)) (-. (requalityOnA T_3 T_4)) ### All 50 % 1.62/1.86 52. (All B, (All C, (((T_3 = B) /\ (requalityOnA C T_3)) => (requalityOnA C B)))) (-. (requalityOnA T_3 T_4)) (requalityOnA (ib) (ib)) (requalityOnA T_4 T_3) (T_3 = (ib)) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) ### All 51 % 1.62/1.86 53. (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (T_3 = (ib)) (requalityOnA T_4 T_3) (requalityOnA (ib) (ib)) (-. (requalityOnA T_3 T_4)) ### All 52 % 1.62/1.86 54. (T_3 = (ia)) ((ia) != T_3) ### Sym(=) % 1.62/1.86 55. (T_3 = (ia)) (T_3 != (ia)) ### Axiom % 1.62/1.86 56. (requalityOnA T_4 T_3) (-. (requalityOnA T_4 T_3)) ### Axiom % 1.62/1.86 57. (requalityOnA T_4 (ia)) (-. (requalityOnA T_4 (ia))) ### Axiom % 1.62/1.86 58. (requalityOnA (ia) (ia)) (-. (requalityOnA (ia) (ia))) ### Axiom % 1.62/1.86 59. ((ia) != T_4) (T_4 = (ia)) ### Sym(=) % 1.62/1.86 60. (((requalityOnA T_4 (ia)) /\ (requalityOnA (ia) (ia))) => (T_4 = (ia))) ((ia) != T_4) (requalityOnA (ia) (ia)) (requalityOnA T_4 (ia)) ### DisjTree 57 58 59 % 1.62/1.86 61. (All Z, (((requalityOnA T_4 (ia)) /\ (requalityOnA Z (ia))) => (T_4 = Z))) (requalityOnA T_4 (ia)) (requalityOnA (ia) (ia)) ((ia) != T_4) ### All 60 % 1.62/1.86 62. (All Y, (All Z, (((requalityOnA Y (ia)) /\ (requalityOnA Z (ia))) => (Y = Z)))) ((ia) != T_4) (requalityOnA (ia) (ia)) (requalityOnA T_4 (ia)) ### All 61 % 1.62/1.86 63. (((T_3 = (ia)) /\ (requalityOnA T_4 T_3)) => (requalityOnA T_4 (ia))) (requalityOnA (ia) (ia)) ((ia) != T_4) (All Y, (All Z, (((requalityOnA Y (ia)) /\ (requalityOnA Z (ia))) => (Y = Z)))) (requalityOnA T_4 T_3) (T_3 = (ia)) ### DisjTree 55 56 62 % 1.62/1.86 64. (All C, (((T_3 = (ia)) /\ (requalityOnA C T_3)) => (requalityOnA C (ia)))) (T_3 = (ia)) (requalityOnA T_4 T_3) (All Y, (All Z, (((requalityOnA Y (ia)) /\ (requalityOnA Z (ia))) => (Y = Z)))) ((ia) != T_4) (requalityOnA (ia) (ia)) ### All 63 % 1.62/1.86 65. (-. (requalityOnA T_3 T_4)) (requalityOnA (ia) (ia)) (All Y, (All Z, (((requalityOnA Y (ia)) /\ (requalityOnA Z (ia))) => (Y = Z)))) (requalityOnA T_4 T_3) (All C, (((T_3 = (ia)) /\ (requalityOnA C T_3)) => (requalityOnA C (ia)))) (T_3 = (ia)) ### P-NotP 54 64 % 1.62/1.86 66. (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (T_3 = (ia)) (All C, (((T_3 = (ia)) /\ (requalityOnA C T_3)) => (requalityOnA C (ia)))) (requalityOnA T_4 T_3) (requalityOnA (ia) (ia)) (-. (requalityOnA T_3 T_4)) ### All 65 % 1.62/1.86 67. (All B, (All C, (((T_3 = B) /\ (requalityOnA C T_3)) => (requalityOnA C B)))) (-. (requalityOnA T_3 T_4)) (requalityOnA (ia) (ia)) (requalityOnA T_4 T_3) (T_3 = (ia)) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) ### All 66 % 1.62/1.86 68. (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (T_3 = (ia)) (requalityOnA T_4 T_3) (requalityOnA (ia) (ia)) (-. (requalityOnA T_3 T_4)) ### All 67 % 1.62/1.86 69. (cA T_3) (requalityOnA (ia) (ia)) (-. (requalityOnA T_3 T_4)) (requalityOnA (ib) (ib)) (requalityOnA T_4 T_3) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) ### Extension/test/axiom_2 53 68 % 1.62/1.86 70. (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (requalityOnA T_4 T_3) (requalityOnA (ib) (ib)) (-. (requalityOnA T_3 T_4)) (requalityOnA (ia) (ia)) ### Extension/test/axiom_4 69 % 1.62/1.86 71. (-. ((requalityOnA T_4 T_3) => (requalityOnA T_3 T_4))) (requalityOnA (ia) (ia)) (requalityOnA (ib) (ib)) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) ### NotImply 70 % 1.62/1.86 72. (-. (All Y, ((requalityOnA T_4 Y) => (requalityOnA Y T_4)))) (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (requalityOnA (ib) (ib)) (requalityOnA (ia) (ia)) ### NotAllEx 71 % 1.62/1.86 73. (-. (All X, (All Y, ((requalityOnA X Y) => (requalityOnA Y X))))) (requalityOnA (ia) (ia)) (requalityOnA (ib) (ib)) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) ### NotAllEx 72 % 1.62/1.86 74. (cowlThing (ia)) (-. (cowlThing (ia))) ### Axiom % 1.62/1.86 75. (requalityOnA (ia) (ia)) (-. (requalityOnA (ia) (ia))) ### Axiom % 1.62/1.86 76. (cowlThing (ib)) (-. (cowlThing (ib))) ### Axiom % 1.62/1.86 77. (cowlThing (ic)) (-. (cowlThing (ic))) ### Axiom % 1.62/1.86 78. (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((All X, (All Y, ((requalityOnA X Y) => ((X = (ia)) \/ ((X = (ib)) \/ (X = (ic))))))) /\ ((All X, (All Y, ((requalityOnA X Y) => (requalityOnA Y X)))) /\ ((cowlThing (ia)) /\ ((requalityOnA (ia) (ia)) /\ ((cowlThing (ib)) /\ (cowlThing (ic)))))))))) (cowlThing (ic)) (cowlThing (ib)) (cowlThing (ia)) (All A, (All B, (All C, (((A = B) /\ (requalityOnA C A)) => (requalityOnA C B))))) (All X, (All Y, (All Z, (((requalityOnA Y X) /\ (requalityOnA Z X)) => (Y = Z))))) (requalityOnA (ib) (ib)) (requalityOnA (ia) (ia)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### DisjTree 1 7 38 73 74 75 76 77 % 1.62/1.86 % SZS output end Proof % 1.62/1.86 (* END-PROOF *) %------------------------------------------------------------------------------