%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS101+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 : n026.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:54 EDT 2022 % Result : Unsatisfiable 6.33s 6.58s % Output : Proof 6.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : KRS101+1 : TPTP v8.1.0. Released v3.1.0. % 0.06/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n026.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:56:46 EDT 2022 % 0.12/0.33 % CPUTime : % 6.33/6.58 % SZS status Theorem % 6.33/6.58 (* PROOF-FOUND *) % 6.33/6.58 (* BEGIN-PROOF *) % 6.33/6.58 % SZS output start Proof % 6.33/6.58 1. (rr (i2003_11_14_17_20_36582) T_0) (-. (rr (i2003_11_14_17_20_36582) T_0)) ### Axiom % 6.33/6.58 2. (rs T_0 T_1) (-. (rs T_0 T_1)) ### Axiom % 6.33/6.58 3. (rs T_0 T_2) (-. (rs T_0 T_2)) ### Axiom % 6.33/6.58 4. (T_2 != T_1) (T_1 = T_2) ### Sym(=) % 6.33/6.58 5. (-. ((rs T_0 T_1) /\ ((rs T_0 T_2) /\ (T_1 != T_2)))) (T_2 != T_1) (rs T_0 T_2) (rs T_0 T_1) ### DisjTree 2 3 4 % 6.33/6.58 6. (-. (Ex Z1, ((rs T_0 T_1) /\ ((rs T_0 Z1) /\ (T_1 != Z1))))) (rs T_0 T_1) (rs T_0 T_2) (T_2 != T_1) ### NotExists 5 % 6.33/6.58 7. (-. (Ex Z0, (Ex Z1, ((rs T_0 Z0) /\ ((rs T_0 Z1) /\ (Z0 != Z1)))))) (T_2 != T_1) (rs T_0 T_2) (rs T_0 T_1) ### NotExists 6 % 6.33/6.58 8. (-. (cc T_0)) (cc T_0) ### Axiom % 6.33/6.58 9. ((rr (i2003_11_14_17_20_36582) T_0) => ((-. (Ex Z0, (Ex Z1, ((rs T_0 Z0) /\ ((rs T_0 Z1) /\ (Z0 != Z1)))))) \/ (cc T_0))) (-. (cc T_0)) (rs T_0 T_1) (rs T_0 T_2) (T_2 != T_1) (rr (i2003_11_14_17_20_36582) T_0) ### DisjTree 1 7 8 % 6.33/6.58 10. (All Y, ((rr (i2003_11_14_17_20_36582) Y) => ((-. (Ex Z0, (Ex Z1, ((rs Y Z0) /\ ((rs Y Z1) /\ (Z0 != Z1)))))) \/ (cc Y)))) (rr (i2003_11_14_17_20_36582) T_0) (T_2 != T_1) (rs T_0 T_2) (rs T_0 T_1) (-. (cc T_0)) ### All 9 % 6.33/6.58 11. (rr (i2003_11_14_17_20_36582) T_0) (-. (rr (i2003_11_14_17_20_36582) T_0)) ### Axiom % 6.33/6.58 12. (-. (cd T_0)) (cd T_0) ### Axiom % 6.33/6.58 13. ((rr (i2003_11_14_17_20_36582) T_0) => (cd T_0)) (-. (cd T_0)) (rr (i2003_11_14_17_20_36582) T_0) ### Imply 11 12 % 6.33/6.58 14. (All Y, ((rr (i2003_11_14_17_20_36582) Y) => (cd Y))) (rr (i2003_11_14_17_20_36582) T_0) (-. (cd T_0)) ### All 13 % 6.33/6.58 15. ((cc T_0) => (-. (cd T_0))) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => (cd Y))) (rs T_0 T_1) (rs T_0 T_2) (T_2 != T_1) (rr (i2003_11_14_17_20_36582) T_0) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => ((-. (Ex Z0, (Ex Z1, ((rs Y Z0) /\ ((rs Y Z1) /\ (Z0 != Z1)))))) \/ (cc Y)))) ### Imply 10 14 % 6.33/6.58 16. (All X, ((cc X) => (-. (cd X)))) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => ((-. (Ex Z0, (Ex Z1, ((rs Y Z0) /\ ((rs Y Z1) /\ (Z0 != Z1)))))) \/ (cc Y)))) (rr (i2003_11_14_17_20_36582) T_0) (T_2 != T_1) (rs T_0 T_2) (rs T_0 T_1) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => (cd Y))) ### All 15 % 6.33/6.58 17. (-. (((rs T_0 T_2) /\ (rs T_0 T_1)) => (T_2 = T_1))) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => (cd Y))) (rr (i2003_11_14_17_20_36582) T_0) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => ((-. (Ex Z0, (Ex Z1, ((rs Y Z0) /\ ((rs Y Z1) /\ (Z0 != Z1)))))) \/ (cc Y)))) (All X, ((cc X) => (-. (cd X)))) ### ConjTree 16 % 6.33/6.58 18. (-. (All Z1, (((rs T_0 T_2) /\ (rs T_0 Z1)) => (T_2 = Z1)))) (All X, ((cc X) => (-. (cd X)))) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => ((-. (Ex Z0, (Ex Z1, ((rs Y Z0) /\ ((rs Y Z1) /\ (Z0 != Z1)))))) \/ (cc Y)))) (rr (i2003_11_14_17_20_36582) T_0) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => (cd Y))) ### NotAllEx 17 % 6.33/6.58 19. (-. (All Z0, (All Z1, (((rs T_0 Z0) /\ (rs T_0 Z1)) => (Z0 = Z1))))) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => (cd Y))) (rr (i2003_11_14_17_20_36582) T_0) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => ((-. (Ex Z0, (Ex Z1, ((rs Y Z0) /\ ((rs Y Z1) /\ (Z0 != Z1)))))) \/ (cc Y)))) (All X, ((cc X) => (-. (cd X)))) ### NotAllEx 18 % 6.33/6.58 20. ((rr (i2003_11_14_17_20_36582) T_0) /\ (-. (All Z0, (All Z1, (((rs T_0 Z0) /\ (rs T_0 Z1)) => (Z0 = Z1)))))) (All X, ((cc X) => (-. (cd X)))) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => ((-. (Ex Z0, (Ex Z1, ((rs Y Z0) /\ ((rs Y Z1) /\ (Z0 != Z1)))))) \/ (cc Y)))) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => (cd Y))) ### And 19 % 6.33/6.58 21. (Ex Y, ((rr (i2003_11_14_17_20_36582) Y) /\ (-. (All Z0, (All Z1, (((rs Y Z0) /\ (rs Y Z1)) => (Z0 = Z1))))))) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => (cd Y))) (All Y, ((rr (i2003_11_14_17_20_36582) Y) => ((-. (Ex Z0, (Ex Z1, ((rs Y Z0) /\ ((rs Y Z1) /\ (Z0 != Z1)))))) \/ (cc Y)))) (All X, ((cc X) => (-. (cd X)))) ### Exists 20 % 6.33/6.58 22. ((All Y, ((rr (i2003_11_14_17_20_36582) Y) => (cd Y))) /\ ((All Y, ((rr (i2003_11_14_17_20_36582) Y) => ((-. (Ex Z0, (Ex Z1, ((rs Y Z0) /\ ((rs Y Z1) /\ (Z0 != Z1)))))) \/ (cc Y)))) /\ (Ex Y, ((rr (i2003_11_14_17_20_36582) Y) /\ (-. (All Z0, (All Z1, (((rs Y Z0) /\ (rs Y Z1)) => (Z0 = Z1))))))))) (All X, ((cc X) => (-. (cd X)))) ### ConjTree 21 % 6.33/6.58 23. (cUnsatisfiable (i2003_11_14_17_20_36582)) (All X, ((cc X) => (-. (cd X)))) ### Definition-Pseudo(cUnsatisfiable) 22 % 6.33/6.58 % SZS output end Proof % 6.33/6.58 (* END-PROOF *) %------------------------------------------------------------------------------