%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS111+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 : n020.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:56 EDT 2022 % Result : Unsatisfiable 5.46s 5.66s % Output : Proof 5.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : KRS111+1 : TPTP v8.1.0. Released v3.1.0. % 0.12/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n020.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Tue Jun 7 13:41:36 EDT 2022 % 0.12/0.34 % CPUTime : % 5.46/5.66 % SZS status Theorem % 5.46/5.66 (* PROOF-FOUND *) % 5.46/5.66 (* BEGIN-PROOF *) % 5.46/5.66 % SZS output start Proof % 5.46/5.66 1. (rs (i2003_11_14_17_21_15425) T_0) (-. (rs (i2003_11_14_17_21_15425) T_0)) ### Axiom % 5.46/5.66 2. (-. (rf1 (i2003_11_14_17_21_15425) T_0)) (rs (i2003_11_14_17_21_15425) T_0) ### Extension/test/axiom_13ctrp 1 % 5.46/5.66 3. (rs (i2003_11_14_17_21_15425) T_0) (-. (rs (i2003_11_14_17_21_15425) T_0)) ### Axiom % 5.46/5.66 4. (-. (rf (i2003_11_14_17_21_15425) T_0)) (rs (i2003_11_14_17_21_15425) T_0) ### Extension/test/axiom_12ctrp 3 % 5.46/5.66 5. (rf (i2003_11_14_17_21_15425) T_1) (-. (rf (i2003_11_14_17_21_15425) T_1)) ### Axiom % 5.46/5.66 6. (T_0 != T_1) (T_0 = T_1) ### Axiom % 5.46/5.66 7. (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) T_1)) => (T_0 = T_1)) (T_0 != T_1) (rf (i2003_11_14_17_21_15425) T_1) (rs (i2003_11_14_17_21_15425) T_0) ### DisjTree 4 5 6 % 5.46/5.66 8. (All Z, (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rs (i2003_11_14_17_21_15425) T_0) (rf (i2003_11_14_17_21_15425) T_1) (T_0 != T_1) ### All 7 % 5.46/5.66 9. (rs (i2003_11_14_17_21_15425) T_0) (-. (rs (i2003_11_14_17_21_15425) T_0)) ### Axiom % 5.46/5.66 10. (-. (rinvS T_0 (i2003_11_14_17_21_15425))) (rs (i2003_11_14_17_21_15425) T_0) ### Extension/test/not_axiom_9 9 % 5.46/5.66 11. (-. (rf1 (i2003_11_14_17_21_15425) T_1)) (rf1 (i2003_11_14_17_21_15425) T_1) ### Axiom % 5.46/5.66 12. (rs (i2003_11_14_17_21_15425) T_1) (-. (rf1 (i2003_11_14_17_21_15425) T_1)) ### Extension/test/axiom_13 11 % 5.46/5.66 13. (rinvS T_1 (i2003_11_14_17_21_15425)) (-. (rf1 (i2003_11_14_17_21_15425) T_1)) ### Extension/test/axiom_9 12 % 5.46/5.66 14. (((T_0 = T_1) /\ (rinvS T_0 (i2003_11_14_17_21_15425))) => (rinvS T_1 (i2003_11_14_17_21_15425))) (-. (rf1 (i2003_11_14_17_21_15425) T_1)) (rf (i2003_11_14_17_21_15425) T_1) (rs (i2003_11_14_17_21_15425) T_0) (All Z, (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) ### DisjTree 8 10 13 % 5.46/5.66 15. (rf1 (i2003_11_14_17_21_15425) T_2) (-. (rf1 (i2003_11_14_17_21_15425) T_2)) ### Axiom % 5.46/5.66 16. (T_0 != T_2) (T_0 = T_2) ### Axiom % 5.46/5.66 17. (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) T_2)) => (T_0 = T_2)) (T_0 != T_2) (rf1 (i2003_11_14_17_21_15425) T_2) (rs (i2003_11_14_17_21_15425) T_0) ### DisjTree 2 15 16 % 5.46/5.66 18. (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rs (i2003_11_14_17_21_15425) T_0) (rf1 (i2003_11_14_17_21_15425) T_2) (T_0 != T_2) ### All 17 % 5.46/5.66 19. (rs (i2003_11_14_17_21_15425) T_2) (-. (rs (i2003_11_14_17_21_15425) T_2)) ### Axiom % 5.46/5.66 20. (-. (rf1 (i2003_11_14_17_21_15425) T_2)) (rs (i2003_11_14_17_21_15425) T_2) ### Extension/test/axiom_13ctrp 19 % 5.46/5.66 21. (T_2 != T_0) (T_0 = T_2) ### Sym(=) % 5.46/5.66 22. (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) T_2)) => (T_0 = T_2)) (T_2 != T_0) (rs (i2003_11_14_17_21_15425) T_2) (rs (i2003_11_14_17_21_15425) T_0) ### DisjTree 2 20 21 % 5.46/5.66 23. (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rs (i2003_11_14_17_21_15425) T_0) (rs (i2003_11_14_17_21_15425) T_2) (T_2 != T_0) ### All 22 % 5.46/5.66 24. (T_1 != T_1) ### Refl(=) % 5.46/5.66 25. (T_1 != T_1) ### Refl(=) % 5.46/5.66 26. (T_2 != T_1) (T_0 = T_1) (rs (i2003_11_14_17_21_15425) T_2) (rs (i2003_11_14_17_21_15425) T_0) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) ### TransEq 23 24 25 % 5.46/5.66 27. (rinvS T_2 (i2003_11_14_17_21_15425)) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rs (i2003_11_14_17_21_15425) T_0) (T_0 = T_1) (T_2 != T_1) ### Extension/test/axiom_9 26 % 5.46/5.66 28. (((T_0 = T_2) /\ (rinvS T_0 (i2003_11_14_17_21_15425))) => (rinvS T_2 (i2003_11_14_17_21_15425))) (T_2 != T_1) (T_0 = T_1) (rf1 (i2003_11_14_17_21_15425) T_2) (rs (i2003_11_14_17_21_15425) T_0) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) ### DisjTree 18 10 27 % 5.46/5.66 29. (All C, (((T_0 = T_2) /\ (rinvS T_0 C)) => (rinvS T_2 C))) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rs (i2003_11_14_17_21_15425) T_0) (rf1 (i2003_11_14_17_21_15425) T_2) (T_0 = T_1) (T_2 != T_1) ### All 28 % 5.46/5.66 30. (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (T_2 != T_1) (T_0 = T_1) (rf1 (i2003_11_14_17_21_15425) T_2) (rs (i2003_11_14_17_21_15425) T_0) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) ### All 29 % 5.46/5.66 31. (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) T_1)) => (T_0 = T_1)) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rf1 (i2003_11_14_17_21_15425) T_2) (T_2 != T_1) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (All Z, (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_21_15425) T_1) (((T_0 = T_1) /\ (rinvS T_0 (i2003_11_14_17_21_15425))) => (rinvS T_1 (i2003_11_14_17_21_15425))) (rs (i2003_11_14_17_21_15425) T_0) ### DisjTree 2 14 30 % 5.46/5.66 32. (rs (i2003_11_14_17_21_15425) T_0) (((T_0 = T_1) /\ (rinvS T_0 (i2003_11_14_17_21_15425))) => (rinvS T_1 (i2003_11_14_17_21_15425))) (rf (i2003_11_14_17_21_15425) T_1) (All Z, (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (T_2 != T_1) (rf1 (i2003_11_14_17_21_15425) T_2) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) ### All 31 % 5.46/5.66 33. (All C, (((T_0 = T_1) /\ (rinvS T_0 C)) => (rinvS T_1 C))) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rf1 (i2003_11_14_17_21_15425) T_2) (T_2 != T_1) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (All Z, (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_21_15425) T_1) (rs (i2003_11_14_17_21_15425) T_0) ### All 32 % 5.46/5.66 34. (rs (i2003_11_14_17_21_15425) T_0) (rf (i2003_11_14_17_21_15425) T_1) (All Z, (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (T_2 != T_1) (rf1 (i2003_11_14_17_21_15425) T_2) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) ### All 33 % 5.46/5.66 35. (ra_Px1 T_2 T_3) (-. (ra_Px1 T_2 T_3)) ### Axiom % 5.46/5.66 36. (-. (ra_Px1 T_1 T_3)) (ra_Px1 T_1 T_3) ### Axiom % 5.46/5.66 37. (((T_2 = T_1) /\ (ra_Px1 T_2 T_3)) => (ra_Px1 T_1 T_3)) (-. (ra_Px1 T_1 T_3)) (ra_Px1 T_2 T_3) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rf1 (i2003_11_14_17_21_15425) T_2) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (All Z, (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_21_15425) T_1) (rs (i2003_11_14_17_21_15425) T_0) ### DisjTree 34 35 36 % 5.46/5.66 38. (All C, (((T_2 = T_1) /\ (ra_Px1 T_2 C)) => (ra_Px1 T_1 C))) (rs (i2003_11_14_17_21_15425) T_0) (rf (i2003_11_14_17_21_15425) T_1) (All Z, (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (rf1 (i2003_11_14_17_21_15425) T_2) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (ra_Px1 T_2 T_3) (-. (ra_Px1 T_1 T_3)) ### All 37 % 5.46/5.66 39. (All B, (All C, (((T_2 = B) /\ (ra_Px1 T_2 C)) => (ra_Px1 B C)))) (-. (ra_Px1 T_1 T_3)) (ra_Px1 T_2 T_3) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rf1 (i2003_11_14_17_21_15425) T_2) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (All Z, (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_21_15425) T_1) (rs (i2003_11_14_17_21_15425) T_0) ### All 38 % 5.46/5.66 40. (cp T_1) (rs (i2003_11_14_17_21_15425) T_0) (rf (i2003_11_14_17_21_15425) T_1) (All Z, (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (rf1 (i2003_11_14_17_21_15425) T_2) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (ra_Px1 T_2 T_3) (All B, (All C, (((T_2 = B) /\ (ra_Px1 T_2 C)) => (ra_Px1 B C)))) ### Extension/test/axiom_3_inst 39 % 5.46/5.67 41. (All A, (All B, (All C, (((A = B) /\ (ra_Px1 A C)) => (ra_Px1 B C))))) (ra_Px1 T_2 T_3) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rf1 (i2003_11_14_17_21_15425) T_2) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (All Z, (((rf (i2003_11_14_17_21_15425) T_0) /\ (rf (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_21_15425) T_1) (rs (i2003_11_14_17_21_15425) T_0) (cp T_1) ### All 40 % 5.46/5.67 42. (All Y, (All Z, (((rf (i2003_11_14_17_21_15425) Y) /\ (rf (i2003_11_14_17_21_15425) Z)) => (Y = Z)))) (cp T_1) (rs (i2003_11_14_17_21_15425) T_0) (rf (i2003_11_14_17_21_15425) T_1) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (rf1 (i2003_11_14_17_21_15425) T_2) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (ra_Px1 T_2 T_3) (All A, (All B, (All C, (((A = B) /\ (ra_Px1 A C)) => (ra_Px1 B C))))) ### All 41 % 5.46/5.67 43. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (ra_Px1 A C)) => (ra_Px1 B C))))) (ra_Px1 T_2 T_3) (All Z, (((rf1 (i2003_11_14_17_21_15425) T_0) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (T_0 = Z))) (rf1 (i2003_11_14_17_21_15425) T_2) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (rf (i2003_11_14_17_21_15425) T_1) (rs (i2003_11_14_17_21_15425) T_0) (cp T_1) ### All 42 % 5.46/5.67 44. (All Y, (All Z, (((rf1 (i2003_11_14_17_21_15425) Y) /\ (rf1 (i2003_11_14_17_21_15425) Z)) => (Y = Z)))) (cp T_1) (rs (i2003_11_14_17_21_15425) T_0) (rf (i2003_11_14_17_21_15425) T_1) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (rf1 (i2003_11_14_17_21_15425) T_2) (ra_Px1 T_2 T_3) (All A, (All B, (All C, (((A = B) /\ (ra_Px1 A C)) => (ra_Px1 B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### All 43 % 5.46/5.67 45. (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (ra_Px1 A C)) => (ra_Px1 B C))))) (ra_Px1 T_2 T_3) (rf1 (i2003_11_14_17_21_15425) T_2) (All B, (All C, (((T_0 = B) /\ (rinvS T_0 C)) => (rinvS B C)))) (rf (i2003_11_14_17_21_15425) T_1) (rs (i2003_11_14_17_21_15425) T_0) (cp T_1) ### All 44 % 5.46/5.67 46. (All A, (All B, (All C, (((A = B) /\ (rinvS A C)) => (rinvS B C))))) (cp T_1) (rs (i2003_11_14_17_21_15425) T_0) (rf (i2003_11_14_17_21_15425) T_1) (rf1 (i2003_11_14_17_21_15425) T_2) (ra_Px1 T_2 T_3) (All A, (All B, (All C, (((A = B) /\ (ra_Px1 A C)) => (ra_Px1 B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) ### All 45 % 5.46/5.67 47. (cpxcomp T_2) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (All C, (((A = B) /\ (ra_Px1 A C)) => (ra_Px1 B C))))) (rf1 (i2003_11_14_17_21_15425) T_2) (rf (i2003_11_14_17_21_15425) T_1) (rs (i2003_11_14_17_21_15425) T_0) (cp T_1) (All A, (All B, (All C, (((A = B) /\ (rinvS A C)) => (rinvS B C))))) ### Extension/test/axiom_4 46 % 5.46/5.67 48. (cUnsatisfiable (i2003_11_14_17_21_15425)) (All A, (All B, (All C, (((A = B) /\ (rinvS A C)) => (rinvS B C))))) (All A, (All B, (All C, (((A = B) /\ (ra_Px1 A C)) => (ra_Px1 B C))))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All X, (All Y, (All Z, (((rf1 X Y) /\ (rf1 X Z)) => (Y = Z))))) ### Extension/test/axiom_2 47 % 5.46/5.67 % SZS output end Proof % 5.46/5.67 (* END-PROOF *) %------------------------------------------------------------------------------