%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS172+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 : n018.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:06 EDT 2022 % Result : Theorem 22.32s 22.55s % Output : Proof 22.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : KRS172+1 : TPTP v8.1.0. Released v3.1.0. % 0.08/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n018.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 08:46:50 EDT 2022 % 0.13/0.35 % CPUTime : % 22.32/22.55 % SZS status Theorem % 22.32/22.55 (* PROOF-FOUND *) % 22.32/22.55 (* BEGIN-PROOF *) % 22.32/22.55 % SZS output start Proof % 22.32/22.55 1. (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (All X, ((cowlThing X) /\ (-. (cowlNothing X))))) ### Axiom % 22.32/22.55 2. (-. (xsd_integer T_0)) (xsd_integer T_0) ### Axiom % 22.32/22.55 3. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### NotNot 2 % 22.32/22.55 4. (-. (xsd_string T_0)) (-. (xsd_integer T_0)) ### Definition-Pseudo(xsd_string) 3 % 22.32/22.55 5. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### Axiom % 22.32/22.55 6. (xsd_string T_0) (-. (-. (xsd_integer T_0))) ### Definition-Pseudo(xsd_string) 5 % 22.32/22.55 7. (-. ((xsd_string T_0) <=> (-. (xsd_integer T_0)))) ### NotEquiv 4 6 % 22.32/22.55 8. (-. (All X, ((xsd_string X) <=> (-. (xsd_integer X))))) ### NotAllEx 7 % 22.32/22.55 9. (rp T_1 T_2) (-. (rp T_1 T_2)) ### Axiom % 22.32/22.55 10. (rp T_1 T_2) (-. (rp T_1 T_2)) ### Axiom % 22.32/22.55 11. (-. (cd T_1)) (cd T_1) ### Axiom % 22.32/22.55 12. ((rp T_1 T_2) => (cd T_1)) (-. (cd T_1)) (rp T_1 T_2) ### Imply 10 11 % 22.32/22.55 13. (All Y, ((rp T_1 Y) => (cd T_1))) (rp T_1 T_2) (-. (cd T_1)) ### All 12 % 22.32/22.55 14. (All X, (All Y, ((rp X Y) => (cd X)))) (-. (cd T_1)) (rp T_1 T_2) ### All 13 % 22.32/22.55 15. (-. (rp T_1 (iv))) (rp T_1 (iv)) ### Axiom % 22.32/22.55 16. ((cd T_1) <=> (rp T_1 (iv))) (-. (rp T_1 (iv))) (rp T_1 T_2) (All X, (All Y, ((rp X Y) => (cd X)))) ### Equiv 14 15 % 22.32/22.55 17. (All X, ((cd X) <=> (rp X (iv)))) (All X, (All Y, ((rp X Y) => (cd X)))) (rp T_1 T_2) (-. (rp T_1 (iv))) ### All 16 % 22.32/22.55 18. (T_2 = (iv)) ((iv) != T_2) ### Sym(=) % 22.32/22.55 19. (rq T_1 (iv)) (-. (rq T_1 (iv))) ### Axiom % 22.32/22.55 20. (-. (rq T_1 T_2)) (rq T_1 T_2) ### Axiom % 22.32/22.55 21. ((((iv) = T_2) /\ (rq T_1 (iv))) => (rq T_1 T_2)) (-. (rq T_1 T_2)) (rq T_1 (iv)) (T_2 = (iv)) ### DisjTree 18 19 20 % 22.32/22.55 22. (All C, ((((iv) = T_2) /\ (rq C (iv))) => (rq C T_2))) (T_2 = (iv)) (rq T_1 (iv)) (-. (rq T_1 T_2)) ### All 21 % 22.32/22.55 23. (All B, (All C, ((((iv) = B) /\ (rq C (iv))) => (rq C B)))) (-. (rq T_1 T_2)) (rq T_1 (iv)) (T_2 = (iv)) ### All 22 % 22.32/22.55 24. (All A, (All B, (All C, (((A = B) /\ (rq C A)) => (rq C B))))) (T_2 = (iv)) (rq T_1 (iv)) (-. (rq T_1 T_2)) ### All 23 % 22.32/22.55 25. ((cd T_1) <=> (rq T_1 (iv))) (-. (rq T_1 T_2)) (T_2 = (iv)) (All A, (All B, (All C, (((A = B) /\ (rq C A)) => (rq C B))))) (rp T_1 T_2) (All X, (All Y, ((rp X Y) => (cd X)))) ### Equiv 14 24 % 22.32/22.55 26. (All X, ((cd X) <=> (rq X (iv)))) (All X, (All Y, ((rp X Y) => (cd X)))) (rp T_1 T_2) (All A, (All B, (All C, (((A = B) /\ (rq C A)) => (rq C B))))) (T_2 = (iv)) (-. (rq T_1 T_2)) ### All 25 % 22.32/22.55 27. (((rp T_1 T_2) /\ (rp T_1 (iv))) => (T_2 = (iv))) (-. (rq T_1 T_2)) (All A, (All B, (All C, (((A = B) /\ (rq C A)) => (rq C B))))) (All X, ((cd X) <=> (rq X (iv)))) (All X, (All Y, ((rp X Y) => (cd X)))) (All X, ((cd X) <=> (rp X (iv)))) (rp T_1 T_2) ### DisjTree 9 17 26 % 22.32/22.55 28. (All Z, (((rp T_1 T_2) /\ (rp T_1 Z)) => (T_2 = Z))) (rp T_1 T_2) (All X, ((cd X) <=> (rp X (iv)))) (All X, (All Y, ((rp X Y) => (cd X)))) (All X, ((cd X) <=> (rq X (iv)))) (All A, (All B, (All C, (((A = B) /\ (rq C A)) => (rq C B))))) (-. (rq T_1 T_2)) ### All 27 % 22.32/22.55 29. (All Y, (All Z, (((rp T_1 Y) /\ (rp T_1 Z)) => (Y = Z)))) (-. (rq T_1 T_2)) (All A, (All B, (All C, (((A = B) /\ (rq C A)) => (rq C B))))) (All X, ((cd X) <=> (rq X (iv)))) (All X, (All Y, ((rp X Y) => (cd X)))) (All X, ((cd X) <=> (rp X (iv)))) (rp T_1 T_2) ### All 28 % 22.32/22.55 30. (All X, (All Y, (All Z, (((rp X Y) /\ (rp X Z)) => (Y = Z))))) (rp T_1 T_2) (All X, ((cd X) <=> (rp X (iv)))) (All X, (All Y, ((rp X Y) => (cd X)))) (All X, ((cd X) <=> (rq X (iv)))) (All A, (All B, (All C, (((A = B) /\ (rq C A)) => (rq C B))))) (-. (rq T_1 T_2)) ### All 29 % 22.32/22.55 31. (rq T_1 T_2) (-. (rq T_1 T_2)) ### Axiom % 22.32/22.55 32. (rq T_1 T_2) (-. (rq T_1 T_2)) ### Axiom % 22.32/22.55 33. (-. (cd T_1)) (cd T_1) ### Axiom % 22.32/22.55 34. ((rq T_1 T_2) => (cd T_1)) (-. (cd T_1)) (rq T_1 T_2) ### Imply 32 33 % 22.32/22.55 35. (All Y, ((rq T_1 Y) => (cd T_1))) (rq T_1 T_2) (-. (cd T_1)) ### All 34 % 22.32/22.55 36. (All X, (All Y, ((rq X Y) => (cd X)))) (-. (cd T_1)) (rq T_1 T_2) ### All 35 % 22.32/22.55 37. (-. (rq T_1 (iv))) (rq T_1 (iv)) ### Axiom % 22.32/22.55 38. ((cd T_1) <=> (rq T_1 (iv))) (-. (rq T_1 (iv))) (rq T_1 T_2) (All X, (All Y, ((rq X Y) => (cd X)))) ### Equiv 36 37 % 22.32/22.55 39. (All X, ((cd X) <=> (rq X (iv)))) (All X, (All Y, ((rq X Y) => (cd X)))) (rq T_1 T_2) (-. (rq T_1 (iv))) ### All 38 % 22.32/22.55 40. (T_2 = (iv)) ((iv) != T_2) ### Sym(=) % 22.32/22.55 41. (rp T_1 (iv)) (-. (rp T_1 (iv))) ### Axiom % 22.32/22.55 42. (-. (rp T_1 T_2)) (rp T_1 T_2) ### Axiom % 22.32/22.55 43. ((((iv) = T_2) /\ (rp T_1 (iv))) => (rp T_1 T_2)) (-. (rp T_1 T_2)) (rp T_1 (iv)) (T_2 = (iv)) ### DisjTree 40 41 42 % 22.32/22.55 44. (All C, ((((iv) = T_2) /\ (rp C (iv))) => (rp C T_2))) (T_2 = (iv)) (rp T_1 (iv)) (-. (rp T_1 T_2)) ### All 43 % 22.32/22.55 45. (All B, (All C, ((((iv) = B) /\ (rp C (iv))) => (rp C B)))) (-. (rp T_1 T_2)) (rp T_1 (iv)) (T_2 = (iv)) ### All 44 % 22.32/22.55 46. (All A, (All B, (All C, (((A = B) /\ (rp C A)) => (rp C B))))) (T_2 = (iv)) (rp T_1 (iv)) (-. (rp T_1 T_2)) ### All 45 % 22.32/22.55 47. ((cd T_1) <=> (rp T_1 (iv))) (-. (rp T_1 T_2)) (T_2 = (iv)) (All A, (All B, (All C, (((A = B) /\ (rp C A)) => (rp C B))))) (rq T_1 T_2) (All X, (All Y, ((rq X Y) => (cd X)))) ### Equiv 36 46 % 22.32/22.55 48. (All X, ((cd X) <=> (rp X (iv)))) (All X, (All Y, ((rq X Y) => (cd X)))) (rq T_1 T_2) (All A, (All B, (All C, (((A = B) /\ (rp C A)) => (rp C B))))) (T_2 = (iv)) (-. (rp T_1 T_2)) ### All 47 % 22.32/22.55 49. (((rq T_1 T_2) /\ (rq T_1 (iv))) => (T_2 = (iv))) (-. (rp T_1 T_2)) (All A, (All B, (All C, (((A = B) /\ (rp C A)) => (rp C B))))) (All X, ((cd X) <=> (rp X (iv)))) (All X, (All Y, ((rq X Y) => (cd X)))) (All X, ((cd X) <=> (rq X (iv)))) (rq T_1 T_2) ### DisjTree 31 39 48 % 22.32/22.55 50. (All Z, (((rq T_1 T_2) /\ (rq T_1 Z)) => (T_2 = Z))) (rq T_1 T_2) (All X, ((cd X) <=> (rq X (iv)))) (All X, (All Y, ((rq X Y) => (cd X)))) (All X, ((cd X) <=> (rp X (iv)))) (All A, (All B, (All C, (((A = B) /\ (rp C A)) => (rp C B))))) (-. (rp T_1 T_2)) ### All 49 % 22.32/22.55 51. (All Y, (All Z, (((rq T_1 Y) /\ (rq T_1 Z)) => (Y = Z)))) (-. (rp T_1 T_2)) (All A, (All B, (All C, (((A = B) /\ (rp C A)) => (rp C B))))) (All X, ((cd X) <=> (rp X (iv)))) (All X, (All Y, ((rq X Y) => (cd X)))) (All X, ((cd X) <=> (rq X (iv)))) (rq T_1 T_2) ### All 50 % 22.32/22.55 52. (All X, (All Y, (All Z, (((rq X Y) /\ (rq X Z)) => (Y = Z))))) (rq T_1 T_2) (All X, ((cd X) <=> (rq X (iv)))) (All X, (All Y, ((rq X Y) => (cd X)))) (All X, ((cd X) <=> (rp X (iv)))) (All A, (All B, (All C, (((A = B) /\ (rp C A)) => (rp C B))))) (-. (rp T_1 T_2)) ### All 51 % 22.32/22.55 53. (-. ((rq T_1 T_2) <=> (rp T_1 T_2))) (All A, (All B, (All C, (((A = B) /\ (rp C A)) => (rp C B))))) (All X, (All Y, ((rq X Y) => (cd X)))) (All X, (All Y, (All Z, (((rq X Y) /\ (rq X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rq C A)) => (rq C B))))) (All X, ((cd X) <=> (rq X (iv)))) (All X, (All Y, ((rp X Y) => (cd X)))) (All X, ((cd X) <=> (rp X (iv)))) (All X, (All Y, (All Z, (((rp X Y) /\ (rp X Z)) => (Y = Z))))) ### NotEquiv 30 52 % 22.32/22.55 54. (-. (All Y, ((rq T_1 Y) <=> (rp T_1 Y)))) (All X, (All Y, (All Z, (((rp X Y) /\ (rp X Z)) => (Y = Z))))) (All X, ((cd X) <=> (rp X (iv)))) (All X, (All Y, ((rp X Y) => (cd X)))) (All X, ((cd X) <=> (rq X (iv)))) (All A, (All B, (All C, (((A = B) /\ (rq C A)) => (rq C B))))) (All X, (All Y, (All Z, (((rq X Y) /\ (rq X Z)) => (Y = Z))))) (All X, (All Y, ((rq X Y) => (cd X)))) (All A, (All B, (All C, (((A = B) /\ (rp C A)) => (rp C B))))) ### NotAllEx 53 % 22.32/22.55 55. (-. (All X, (All Y, ((rq X Y) <=> (rp X Y))))) (All A, (All B, (All C, (((A = B) /\ (rp C A)) => (rp C B))))) (All X, (All Y, ((rq X Y) => (cd X)))) (All X, (All Y, (All Z, (((rq X Y) /\ (rq X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rq C A)) => (rq C B))))) (All X, ((cd X) <=> (rq X (iv)))) (All X, (All Y, ((rp X Y) => (cd X)))) (All X, ((cd X) <=> (rp X (iv)))) (All X, (All Y, (All Z, (((rp X Y) /\ (rp X Z)) => (Y = Z))))) ### NotAllEx 54 % 22.32/22.55 56. (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ (All X, (All Y, ((rq X Y) <=> (rp X Y))))))) (All X, (All Y, (All Z, (((rp X Y) /\ (rp X Z)) => (Y = Z))))) (All X, ((cd X) <=> (rp X (iv)))) (All X, (All Y, ((rp X Y) => (cd X)))) (All X, ((cd X) <=> (rq X (iv)))) (All A, (All B, (All C, (((A = B) /\ (rq C A)) => (rq C B))))) (All X, (All Y, (All Z, (((rq X Y) /\ (rq X Z)) => (Y = Z))))) (All X, (All Y, ((rq X Y) => (cd X)))) (All A, (All B, (All C, (((A = B) /\ (rp C A)) => (rp C B))))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### DisjTree 1 8 55 % 22.32/22.55 % SZS output end Proof % 22.32/22.55 (* END-PROOF *) %------------------------------------------------------------------------------