%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS132+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 : n025.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:31:59 EDT 2022 % Result : Theorem 0.18s 0.42s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS132+1 : TPTP v8.1.0. Released v3.1.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n025.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue Jun 7 13:50:19 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.42 % SZS status Theorem % 0.18/0.42 (* PROOF-FOUND *) % 0.18/0.42 (* BEGIN-PROOF *) % 0.18/0.42 % SZS output start Proof % 0.18/0.42 1. (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (All X, ((cowlThing X) /\ (-. (cowlNothing X))))) ### Axiom % 0.18/0.42 2. (-. (xsd_integer T_0)) (xsd_integer T_0) ### Axiom % 0.18/0.42 3. (-. (xsd_string T_0)) (-. (xsd_integer T_0)) ### Extension/test/not_axiom_1 2 % 0.18/0.42 4. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### Axiom % 0.18/0.42 5. (xsd_string T_0) (-. (-. (xsd_integer T_0))) ### Extension/test/axiom_1 4 % 0.18/0.42 6. (-. ((xsd_string T_0) <=> (-. (xsd_integer T_0)))) ### NotEquiv 3 5 % 0.18/0.42 7. (-. (All X, ((xsd_string X) <=> (-. (xsd_integer X))))) ### NotAllEx 6 % 0.18/0.42 8. (rs T_1 T_2) (-. (rs T_1 T_2)) ### Axiom % 0.18/0.42 9. (-. (cowlThing T_2)) (cowlThing T_2) ### Axiom % 0.18/0.42 10. ((cowlThing T_2) /\ (-. (cowlNothing T_2))) (-. (cowlThing T_2)) ### And 9 % 0.18/0.42 11. (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cowlThing T_2)) ### All 10 % 0.18/0.42 12. (-. (cAorB T_1)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (rs T_1 T_2) ### Extension/test/not_axiom_3_inst 8 11 % 0.18/0.42 13. (-. ((rs T_1 T_2) => (cNothing T_2))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cAorB T_1)) ### NotImply 12 % 0.18/0.42 14. (-. (All Y, ((rs T_1 Y) => (cNothing Y)))) (-. (cAorB T_1)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### NotAllEx 13 % 0.18/0.42 15. (rr T_1 T_3) (-. (rr T_1 T_3)) ### Axiom % 0.18/0.42 16. (cNothing T_3) (-. (cNothing T_3)) ### Axiom % 0.18/0.42 17. (rp T_3 T_4) (-. (rp T_3 T_4)) ### Axiom % 0.18/0.42 18. (cNothing T_3) (rp T_3 T_4) ### Extension/test/axiom_6_inst 17 % 0.18/0.42 19. (Ex Y0, (rp T_3 Y0)) (cNothing T_3) ### Exists 18 % 0.18/0.42 20. ((cNothing T_3) => (Ex Y0, (rp T_3 Y0))) (cNothing T_3) ### Imply 16 19 % 0.18/0.42 21. (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (cNothing T_3) ### All 20 % 0.18/0.42 22. (cnotB T_1) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (rr T_1 T_3) ### Extension/test/axiom_10_inst 15 21 % 0.18/0.42 23. (cnotAorB T_1) (rr T_1 T_3) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) ### Extension/test/axiom_9 22 % 0.18/0.42 24. ((cnotAorB T_1) <=> (All Y, ((rs T_1 Y) => (cNothing Y)))) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (rr T_1 T_3) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cAorB T_1)) ### Equiv 14 23 % 0.18/0.42 25. (All X, ((cnotAorB X) <=> (All Y, ((rs X Y) => (cNothing Y))))) (-. (cAorB T_1)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (rr T_1 T_3) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) ### All 24 % 0.18/0.42 26. (cB T_1) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cAorB T_1)) (All X, ((cnotAorB X) <=> (All Y, ((rs X Y) => (cNothing Y))))) ### Extension/test/axiom_4 25 % 0.18/0.42 27. (rq T_1 T_5) (-. (rq T_1 T_5)) ### Axiom % 0.18/0.42 28. (cNothing T_5) (-. (cNothing T_5)) ### Axiom % 0.18/0.42 29. (rp T_5 T_6) (-. (rp T_5 T_6)) ### Axiom % 0.18/0.42 30. (cNothing T_5) (rp T_5 T_6) ### Extension/test/axiom_6_inst 29 % 0.18/0.42 31. (Ex Y0, (rp T_5 Y0)) (cNothing T_5) ### Exists 30 % 0.18/0.42 32. ((cNothing T_5) => (Ex Y0, (rp T_5 Y0))) (cNothing T_5) ### Imply 28 31 % 0.18/0.42 33. (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (cNothing T_5) ### All 32 % 0.18/0.42 34. (cnotA T_1) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (rq T_1 T_5) ### Extension/test/axiom_7_inst 27 33 % 0.18/0.42 35. (cnotAorB T_1) (rq T_1 T_5) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) ### Extension/test/axiom_9 34 % 0.18/0.42 36. ((cnotAorB T_1) <=> (All Y, ((rs T_1 Y) => (cNothing Y)))) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (rq T_1 T_5) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cAorB T_1)) ### Equiv 14 35 % 0.18/0.42 37. (All X, ((cnotAorB X) <=> (All Y, ((rs X Y) => (cNothing Y))))) (-. (cAorB T_1)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (rq T_1 T_5) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) ### All 36 % 0.18/0.42 38. (cA T_1) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cAorB T_1)) (All X, ((cnotAorB X) <=> (All Y, ((rs X Y) => (cNothing Y))))) ### Extension/test/axiom_2 37 % 0.18/0.42 39. ((cB T_1) \/ (cA T_1)) (All X, ((cnotAorB X) <=> (All Y, ((rs X Y) => (cNothing Y))))) (-. (cAorB T_1)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) ### Or 26 38 % 0.18/0.42 40. (rr T_1 T_7) (-. (rr T_1 T_7)) ### Axiom % 0.18/0.42 41. (-. (cowlThing T_7)) (cowlThing T_7) ### Axiom % 0.18/0.42 42. ((cowlThing T_7) /\ (-. (cowlNothing T_7))) (-. (cowlThing T_7)) ### And 41 % 0.18/0.42 43. (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cowlThing T_7)) ### All 42 % 0.18/0.42 44. (-. (cB T_1)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (rr T_1 T_7) ### Extension/test/not_axiom_4_inst 40 43 % 0.18/0.42 45. (-. (cnotB T_1)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cB T_1)) ### Extension/test/not_axiom_10 44 % 0.18/0.42 46. (rq T_1 T_8) (-. (rq T_1 T_8)) ### Axiom % 0.18/0.42 47. (-. (cowlThing T_8)) (cowlThing T_8) ### Axiom % 0.18/0.42 48. ((cowlThing T_8) /\ (-. (cowlNothing T_8))) (-. (cowlThing T_8)) ### And 47 % 0.18/0.42 49. (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cowlThing T_8)) ### All 48 % 0.18/0.42 50. (-. (cA T_1)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (rq T_1 T_8) ### Extension/test/not_axiom_2_inst 46 49 % 0.18/0.42 51. (-. (cnotA T_1)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cA T_1)) ### Extension/test/not_axiom_7 50 % 0.18/0.42 52. (-. (cnotAorB T_1)) (-. (cA T_1)) (-. (cB T_1)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### Extension/test/not_axiom_9 45 51 % 0.18/0.42 53. (rs T_1 T_9) (-. (rs T_1 T_9)) ### Axiom % 0.18/0.42 54. (cNothing T_9) (-. (cNothing T_9)) ### Axiom % 0.18/0.42 55. (rp T_9 T_10) (-. (rp T_9 T_10)) ### Axiom % 0.18/0.42 56. (cNothing T_9) (rp T_9 T_10) ### Extension/test/axiom_6_inst 55 % 0.18/0.42 57. (Ex Y0, (rp T_9 Y0)) (cNothing T_9) ### Exists 56 % 0.18/0.42 58. ((cNothing T_9) => (Ex Y0, (rp T_9 Y0))) (cNothing T_9) ### Imply 54 57 % 0.18/0.42 59. (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (cNothing T_9) ### All 58 % 0.18/0.42 60. ((rs T_1 T_9) => (cNothing T_9)) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (rs T_1 T_9) ### Imply 53 59 % 0.18/0.42 61. (All Y, ((rs T_1 Y) => (cNothing Y))) (rs T_1 T_9) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) ### All 60 % 0.18/0.42 62. ((cnotAorB T_1) <=> (All Y, ((rs T_1 Y) => (cNothing Y)))) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (rs T_1 T_9) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cB T_1)) (-. (cA T_1)) ### Equiv 52 61 % 0.18/0.42 63. (All X, ((cnotAorB X) <=> (All Y, ((rs X Y) => (cNothing Y))))) (-. (cA T_1)) (-. (cB T_1)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (rs T_1 T_9) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) ### All 62 % 0.18/0.42 64. (-. ((cB T_1) \/ (cA T_1))) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (rs T_1 T_9) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (All X, ((cnotAorB X) <=> (All Y, ((rs X Y) => (cNothing Y))))) ### NotOr 63 % 0.18/0.42 65. (cAorB T_1) (All X, ((cnotAorB X) <=> (All Y, ((rs X Y) => (cNothing Y))))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (-. ((cB T_1) \/ (cA T_1))) ### Extension/test/axiom_3 64 % 0.18/0.42 66. (-. ((cAorB T_1) <=> ((cB T_1) \/ (cA T_1)))) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (All X, ((cnotAorB X) <=> (All Y, ((rs X Y) => (cNothing Y))))) ### NotEquiv 39 65 % 0.18/0.42 67. (-. (All X, ((cAorB X) <=> ((cB X) \/ (cA X))))) (All X, ((cnotAorB X) <=> (All Y, ((rs X Y) => (cNothing Y))))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) ### NotAllEx 66 % 0.18/0.42 68. (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ (All X, ((cAorB X) <=> ((cB X) \/ (cA X))))))) (All X, ((cNothing X) => (Ex Y0, (rp X Y0)))) (All X, ((cnotAorB X) <=> (All Y, ((rs X Y) => (cNothing Y))))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### DisjTree 1 7 67 % 0.18/0.42 % SZS output end Proof % 0.18/0.42 (* END-PROOF *) %------------------------------------------------------------------------------