%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS072+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:31:49 EDT 2022 % Result : Unsatisfiable 4.53s 4.74s % Output : Proof 4.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS072+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n018.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 20:25:51 EDT 2022 % 0.12/0.33 % CPUTime : % 4.53/4.74 % SZS status Theorem % 4.53/4.74 (* PROOF-FOUND *) % 4.53/4.74 (* BEGIN-PROOF *) % 4.53/4.74 % SZS output start Proof % 4.53/4.74 1. (rr T_0 T_1) (-. (rr T_0 T_1)) ### Axiom % 4.53/4.74 2. (rr T_0 (i2003_11_14_17_18_50190)) (-. (rr T_0 (i2003_11_14_17_18_50190))) ### Axiom % 4.53/4.74 3. (T_1 = (i2003_11_14_17_18_50190)) ((i2003_11_14_17_18_50190) != T_1) ### Sym(=) % 4.53/4.74 4. ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) (-. ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190)))) ### Axiom % 4.53/4.74 5. (-. (cUnsatisfiable (i2003_11_14_17_18_50190))) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) ### Definition-Pseudo(cUnsatisfiable) 4 % 4.53/4.74 6. (cp1 T_1) (-. (cp1 T_1)) ### Axiom % 4.53/4.74 7. (cp2 T_1) (-. (cp2 T_1)) ### Axiom % 4.53/4.74 8. (-. ((cp3 T_1) \/ ((cp2 T_1) \/ ((cp4 T_1) \/ (cp5 T_1))))) (cp2 T_1) ### ConjTree 7 % 4.53/4.74 9. ((cp1 T_1) => (-. ((cp3 T_1) \/ ((cp2 T_1) \/ ((cp4 T_1) \/ (cp5 T_1)))))) (cp2 T_1) (cp1 T_1) ### Imply 6 8 % 4.53/4.74 10. (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) (cp1 T_1) (cp2 T_1) ### All 9 % 4.53/4.74 11. ((Ex Y, ((rinvR T_1 Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 T_1)) (cp1 T_1) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) ### And 10 % 4.53/4.74 12. (cUnsatisfiable T_1) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) (cp1 T_1) ### Definition-Pseudo(cUnsatisfiable) 11 % 4.53/4.74 13. ((((i2003_11_14_17_18_50190) = T_1) /\ (cUnsatisfiable (i2003_11_14_17_18_50190))) => (cUnsatisfiable T_1)) (cp1 T_1) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) (T_1 = (i2003_11_14_17_18_50190)) ### DisjTree 3 5 12 % 4.53/4.74 14. (All B, ((((i2003_11_14_17_18_50190) = B) /\ (cUnsatisfiable (i2003_11_14_17_18_50190))) => (cUnsatisfiable B))) (T_1 = (i2003_11_14_17_18_50190)) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) (cp1 T_1) ### All 13 % 4.53/4.74 15. (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (cp1 T_1) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) (T_1 = (i2003_11_14_17_18_50190)) ### All 14 % 4.53/4.74 16. (((rr T_0 T_1) /\ (rr T_0 (i2003_11_14_17_18_50190))) => (T_1 = (i2003_11_14_17_18_50190))) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) (cp1 T_1) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (rr T_0 (i2003_11_14_17_18_50190)) (rr T_0 T_1) ### DisjTree 1 2 15 % 4.53/4.74 17. (All Z1, (((rr T_0 T_1) /\ (rr T_0 Z1)) => (T_1 = Z1))) (rr T_0 T_1) (rr T_0 (i2003_11_14_17_18_50190)) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (cp1 T_1) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) ### All 16 % 4.53/4.74 18. (All Z0, (All Z1, (((rr T_0 Z0) /\ (rr T_0 Z1)) => (Z0 = Z1)))) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) (cp1 T_1) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (rr T_0 (i2003_11_14_17_18_50190)) (rr T_0 T_1) ### All 17 % 4.53/4.74 19. ((rr T_0 T_1) /\ (cp1 T_1)) (rr T_0 (i2003_11_14_17_18_50190)) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) (All Z0, (All Z1, (((rr T_0 Z0) /\ (rr T_0 Z1)) => (Z0 = Z1)))) ### And 18 % 4.53/4.74 20. (Ex Z, ((rr T_0 Z) /\ (cp1 Z))) (All Z0, (All Z1, (((rr T_0 Z0) /\ (rr T_0 Z1)) => (Z0 = Z1)))) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (rr T_0 (i2003_11_14_17_18_50190)) ### Exists 19 % 4.53/4.74 21. (rinvR (i2003_11_14_17_18_50190) T_0) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) (All Z0, (All Z1, (((rr T_0 Z0) /\ (rr T_0 Z1)) => (Z0 = Z1)))) (Ex Z, ((rr T_0 Z) /\ (cp1 Z))) ### Definition-Pseudo(rinvR) 20 % 4.53/4.74 22. ((rinvR (i2003_11_14_17_18_50190) T_0) /\ ((All Z0, (All Z1, (((rr T_0 Z0) /\ (rr T_0 Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr T_0 Z) /\ (cp1 Z))))) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### ConjTree 21 % 4.53/4.74 23. (Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) ### Exists 22 % 4.53/4.74 24. ((Ex Y, ((rinvR (i2003_11_14_17_18_50190) Y) /\ ((All Z0, (All Z1, (((rr Y Z0) /\ (rr Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rr Y Z) /\ (cp1 Z)))))) /\ (cp2 (i2003_11_14_17_18_50190))) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) ### And 23 % 4.53/4.74 25. (cUnsatisfiable (i2003_11_14_17_18_50190)) (All A, (All B, (((A = B) /\ (cUnsatisfiable A)) => (cUnsatisfiable B)))) (All X, ((cp1 X) => (-. ((cp3 X) \/ ((cp2 X) \/ ((cp4 X) \/ (cp5 X))))))) ### Definition-Pseudo(cUnsatisfiable) 24 % 4.53/4.74 % SZS output end Proof % 4.53/4.74 (* END-PROOF *) %------------------------------------------------------------------------------