%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS075+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 : n019.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:50 EDT 2022 % Result : Unsatisfiable 12.14s 12.33s % Output : Proof 12.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : KRS075+1 : TPTP v8.1.0. Released v3.1.0. % 0.12/0.14 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.35 % Computer : n019.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Tue Jun 7 18:06:40 EDT 2022 % 0.13/0.35 % CPUTime : % 12.14/12.33 % SZS status Theorem % 12.14/12.33 (* PROOF-FOUND *) % 12.14/12.33 (* BEGIN-PROOF *) % 12.14/12.33 % SZS output start Proof % 12.14/12.33 1. (rs (i2003_11_14_17_19_02584) T_0) (-. (rs (i2003_11_14_17_19_02584) T_0)) ### Axiom % 12.14/12.33 2. (-. (rf1 (i2003_11_14_17_19_02584) T_0)) (rf1 (i2003_11_14_17_19_02584) T_0) ### Axiom % 12.14/12.33 3. ((rs (i2003_11_14_17_19_02584) T_0) => (rf1 (i2003_11_14_17_19_02584) T_0)) (-. (rf1 (i2003_11_14_17_19_02584) T_0)) (rs (i2003_11_14_17_19_02584) T_0) ### Imply 1 2 % 12.14/12.33 4. (All Y, ((rs (i2003_11_14_17_19_02584) Y) => (rf1 (i2003_11_14_17_19_02584) Y))) (rs (i2003_11_14_17_19_02584) T_0) (-. (rf1 (i2003_11_14_17_19_02584) T_0)) ### All 3 % 12.14/12.33 5. (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (-. (rf1 (i2003_11_14_17_19_02584) T_0)) (rs (i2003_11_14_17_19_02584) T_0) ### All 4 % 12.14/12.33 6. (rf1 (i2003_11_14_17_19_02584) T_1) (-. (rf1 (i2003_11_14_17_19_02584) T_1)) ### Axiom % 12.14/12.33 7. (rf (i2003_11_14_17_19_02584) T_2) (-. (rf (i2003_11_14_17_19_02584) T_2)) ### Axiom % 12.14/12.33 8. (T_0 = T_1) (T_0 != T_1) ### Axiom % 12.14/12.33 9. (rs (i2003_11_14_17_19_02584) T_0) (-. (rs (i2003_11_14_17_19_02584) T_0)) ### Axiom % 12.14/12.33 10. (-. (rs (i2003_11_14_17_19_02584) T_1)) (rs (i2003_11_14_17_19_02584) T_1) ### Axiom % 12.14/12.33 11. (((T_0 = T_1) /\ (rs (i2003_11_14_17_19_02584) T_0)) => (rs (i2003_11_14_17_19_02584) T_1)) (-. (rs (i2003_11_14_17_19_02584) T_1)) (rs (i2003_11_14_17_19_02584) T_0) (T_0 = T_1) ### DisjTree 8 9 10 % 12.14/12.33 12. (All C, (((T_0 = T_1) /\ (rs C T_0)) => (rs C T_1))) (T_0 = T_1) (rs (i2003_11_14_17_19_02584) T_0) (-. (rs (i2003_11_14_17_19_02584) T_1)) ### All 11 % 12.14/12.33 13. (-. (rf (i2003_11_14_17_19_02584) T_1)) (rf (i2003_11_14_17_19_02584) T_1) ### Axiom % 12.14/12.33 14. ((rs (i2003_11_14_17_19_02584) T_1) => (rf (i2003_11_14_17_19_02584) T_1)) (-. (rf (i2003_11_14_17_19_02584) T_1)) (rs (i2003_11_14_17_19_02584) T_0) (T_0 = T_1) (All C, (((T_0 = T_1) /\ (rs C T_0)) => (rs C T_1))) ### Imply 12 13 % 12.14/12.33 15. (All Y, ((rs (i2003_11_14_17_19_02584) Y) => (rf (i2003_11_14_17_19_02584) Y))) (All C, (((T_0 = T_1) /\ (rs C T_0)) => (rs C T_1))) (T_0 = T_1) (rs (i2003_11_14_17_19_02584) T_0) (-. (rf (i2003_11_14_17_19_02584) T_1)) ### All 14 % 12.14/12.33 16. (All B, (All C, (((T_0 = B) /\ (rs C T_0)) => (rs C B)))) (-. (rf (i2003_11_14_17_19_02584) T_1)) (rs (i2003_11_14_17_19_02584) T_0) (T_0 = T_1) (All Y, ((rs (i2003_11_14_17_19_02584) Y) => (rf (i2003_11_14_17_19_02584) Y))) ### All 15 % 12.14/12.33 17. (All X, (All Y, ((rs X Y) => (rf X Y)))) (T_0 = T_1) (rs (i2003_11_14_17_19_02584) T_0) (-. (rf (i2003_11_14_17_19_02584) T_1)) (All B, (All C, (((T_0 = B) /\ (rs C T_0)) => (rs C B)))) ### All 16 % 12.14/12.33 18. (T_2 != T_1) (T_2 = T_1) ### Axiom % 12.14/12.33 19. (((rf (i2003_11_14_17_19_02584) T_2) /\ (rf (i2003_11_14_17_19_02584) T_1)) => (T_2 = T_1)) (T_2 != T_1) (All B, (All C, (((T_0 = B) /\ (rs C T_0)) => (rs C B)))) (rs (i2003_11_14_17_19_02584) T_0) (T_0 = T_1) (All X, (All Y, ((rs X Y) => (rf X Y)))) (rf (i2003_11_14_17_19_02584) T_2) ### DisjTree 7 17 18 % 12.14/12.33 20. (All Z, (((rf (i2003_11_14_17_19_02584) T_2) /\ (rf (i2003_11_14_17_19_02584) Z)) => (T_2 = Z))) (rf (i2003_11_14_17_19_02584) T_2) (All X, (All Y, ((rs X Y) => (rf X Y)))) (T_0 = T_1) (rs (i2003_11_14_17_19_02584) T_0) (All B, (All C, (((T_0 = B) /\ (rs C T_0)) => (rs C B)))) (T_2 != T_1) ### All 19 % 12.14/12.33 21. (((rf1 (i2003_11_14_17_19_02584) T_0) /\ (rf1 (i2003_11_14_17_19_02584) T_1)) => (T_0 = T_1)) (T_2 != T_1) (All B, (All C, (((T_0 = B) /\ (rs C T_0)) => (rs C B)))) (All X, (All Y, ((rs X Y) => (rf X Y)))) (rf (i2003_11_14_17_19_02584) T_2) (All Z, (((rf (i2003_11_14_17_19_02584) T_2) /\ (rf (i2003_11_14_17_19_02584) Z)) => (T_2 = Z))) (rf1 (i2003_11_14_17_19_02584) T_1) (rs (i2003_11_14_17_19_02584) T_0) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) ### DisjTree 5 6 20 % 12.14/12.33 22. (All Z, (((rf1 (i2003_11_14_17_19_02584) T_0) /\ (rf1 (i2003_11_14_17_19_02584) Z)) => (T_0 = Z))) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (rs (i2003_11_14_17_19_02584) T_0) (rf1 (i2003_11_14_17_19_02584) T_1) (All Z, (((rf (i2003_11_14_17_19_02584) T_2) /\ (rf (i2003_11_14_17_19_02584) Z)) => (T_2 = Z))) (rf (i2003_11_14_17_19_02584) T_2) (All X, (All Y, ((rs X Y) => (rf X Y)))) (All B, (All C, (((T_0 = B) /\ (rs C T_0)) => (rs C B)))) (T_2 != T_1) ### All 21 % 12.14/12.33 23. (All Y, (All Z, (((rf1 (i2003_11_14_17_19_02584) Y) /\ (rf1 (i2003_11_14_17_19_02584) Z)) => (Y = Z)))) (T_2 != T_1) (All B, (All C, (((T_0 = B) /\ (rs C T_0)) => (rs C B)))) (All X, (All Y, ((rs X Y) => (rf X Y)))) (rf (i2003_11_14_17_19_02584) T_2) (All Z, (((rf (i2003_11_14_17_19_02584) T_2) /\ (rf (i2003_11_14_17_19_02584) Z)) => (T_2 = Z))) (rf1 (i2003_11_14_17_19_02584) T_1) (rs (i2003_11_14_17_19_02584) T_0) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) ### All 22 % 12.14/12.33 24. (All Y, (All Z, (((rf (i2003_11_14_17_19_02584) Y) /\ (rf (i2003_11_14_17_19_02584) Z)) => (Y = Z)))) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (rs (i2003_11_14_17_19_02584) T_0) (rf1 (i2003_11_14_17_19_02584) T_1) (rf (i2003_11_14_17_19_02584) T_2) (All X, (All Y, ((rs X Y) => (rf X Y)))) (All B, (All C, (((T_0 = B) /\ (rs C T_0)) => (rs C B)))) (T_2 != T_1) (All Y, (All Z, (((rf1 (i2003_11_14_17_19_02584) Y) /\ (rf1 (i2003_11_14_17_19_02584) Z)) => (Y = Z)))) ### All 23 % 12.14/12.33 25. (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) (T_2 != T_1) (All B, (All C, (((T_0 = B) /\ (rs C T_0)) => (rs C B)))) (All X, (All Y, ((rs X Y) => (rf X Y)))) (rf (i2003_11_14_17_19_02584) T_2) (rf1 (i2003_11_14_17_19_02584) T_1) (rs (i2003_11_14_17_19_02584) T_0) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (All Y, (All Z, (((rf (i2003_11_14_17_19_02584) Y) /\ (rf (i2003_11_14_17_19_02584) Z)) => (Y = Z)))) ### All 24 % 12.14/12.33 26. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (rs (i2003_11_14_17_19_02584) T_0) (rf1 (i2003_11_14_17_19_02584) T_1) (rf (i2003_11_14_17_19_02584) T_2) (All X, (All Y, ((rs X Y) => (rf X Y)))) (All B, (All C, (((T_0 = B) /\ (rs C T_0)) => (rs C B)))) (T_2 != T_1) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) ### All 25 % 12.14/12.33 27. (-. (cp T_1)) (cp T_2) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) (All B, (All C, (((T_0 = B) /\ (rs C T_0)) => (rs C B)))) (All X, (All Y, ((rs X Y) => (rf X Y)))) (rf (i2003_11_14_17_19_02584) T_2) (rf1 (i2003_11_14_17_19_02584) T_1) (rs (i2003_11_14_17_19_02584) T_0) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### P-NotP 26 % 12.14/12.33 28. (All A, (All B, (All C, (((A = B) /\ (rs C A)) => (rs C B))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (rs (i2003_11_14_17_19_02584) T_0) (rf1 (i2003_11_14_17_19_02584) T_1) (rf (i2003_11_14_17_19_02584) T_2) (All X, (All Y, ((rs X Y) => (rf X Y)))) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) (cp T_2) (-. (cp T_1)) ### All 27 % 12.14/12.33 29. ((rf (i2003_11_14_17_19_02584) T_2) /\ (cp T_2)) (-. (cp T_1)) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) (All X, (All Y, ((rs X Y) => (rf X Y)))) (rf1 (i2003_11_14_17_19_02584) T_1) (rs (i2003_11_14_17_19_02584) T_0) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rs C A)) => (rs C B))))) ### And 28 % 12.14/12.33 30. (Ex Y, ((rf (i2003_11_14_17_19_02584) Y) /\ (cp Y))) (All A, (All B, (All C, (((A = B) /\ (rs C A)) => (rs C B))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (rs (i2003_11_14_17_19_02584) T_0) (rf1 (i2003_11_14_17_19_02584) T_1) (All X, (All Y, ((rs X Y) => (rf X Y)))) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) (-. (cp T_1)) ### Exists 29 % 12.14/12.33 31. ((rs (i2003_11_14_17_19_02584) T_0) /\ (cowlThing T_0)) (-. (cp T_1)) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) (All X, (All Y, ((rs X Y) => (rf X Y)))) (rf1 (i2003_11_14_17_19_02584) T_1) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rs C A)) => (rs C B))))) (Ex Y, ((rf (i2003_11_14_17_19_02584) Y) /\ (cp Y))) ### And 30 % 12.14/12.33 32. (Ex Y, ((rs (i2003_11_14_17_19_02584) Y) /\ (cowlThing Y))) (Ex Y, ((rf (i2003_11_14_17_19_02584) Y) /\ (cp Y))) (All A, (All B, (All C, (((A = B) /\ (rs C A)) => (rs C B))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (rf1 (i2003_11_14_17_19_02584) T_1) (All X, (All Y, ((rs X Y) => (rf X Y)))) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) (-. (cp T_1)) ### Exists 31 % 12.14/12.33 33. ((rf1 (i2003_11_14_17_19_02584) T_1) /\ (-. (cp T_1))) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) (All X, (All Y, ((rs X Y) => (rf X Y)))) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rs C A)) => (rs C B))))) (Ex Y, ((rf (i2003_11_14_17_19_02584) Y) /\ (cp Y))) (Ex Y, ((rs (i2003_11_14_17_19_02584) Y) /\ (cowlThing Y))) ### And 32 % 12.14/12.33 34. (Ex Y, ((rf1 (i2003_11_14_17_19_02584) Y) /\ (-. (cp Y)))) (Ex Y, ((rs (i2003_11_14_17_19_02584) Y) /\ (cowlThing Y))) (Ex Y, ((rf (i2003_11_14_17_19_02584) Y) /\ (cp Y))) (All A, (All B, (All C, (((A = B) /\ (rs C A)) => (rs C B))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (All X, (All Y, ((rs X Y) => (rf X Y)))) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) ### Exists 33 % 12.14/12.33 35. ((Ex Y, ((rf1 (i2003_11_14_17_19_02584) Y) /\ (-. (cp Y)))) /\ ((Ex Y, ((rs (i2003_11_14_17_19_02584) Y) /\ (cowlThing Y))) /\ (Ex Y, ((rf (i2003_11_14_17_19_02584) Y) /\ (cp Y))))) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) (All X, (All Y, ((rs X Y) => (rf X Y)))) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (rs C A)) => (rs C B))))) ### ConjTree 34 % 12.14/12.33 36. (cUnsatisfiable (i2003_11_14_17_19_02584)) (All A, (All B, (All C, (((A = B) /\ (rs C A)) => (rs C B))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All X, (All Y, ((rs X Y) => (rf1 X Y)))) (All X, (All Y, ((rs X Y) => (rf X Y)))) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) ### Definition-Pseudo(cUnsatisfiable) 35 % 12.14/12.33 % SZS output end Proof % 12.14/12.33 (* END-PROOF *) %------------------------------------------------------------------------------