%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS098+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 : n021.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:53 EDT 2022 % Result : Unsatisfiable 134.01s 134.27s % Output : Proof 134.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : KRS098+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 : n021.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:01:06 EDT 2022 % 0.12/0.33 % CPUTime : % 134.01/134.27 % SZS status Theorem % 134.01/134.27 (* PROOF-FOUND *) % 134.01/134.27 (* BEGIN-PROOF *) % 134.01/134.27 % SZS output start Proof % 134.01/134.27 1. (rr1 (i2003_11_14_17_20_25524) T_0) (-. (rr1 (i2003_11_14_17_20_25524) T_0)) ### Axiom % 134.01/134.27 2. (-. (rr (i2003_11_14_17_20_25524) T_0)) (rr (i2003_11_14_17_20_25524) T_0) ### Axiom % 134.01/134.27 3. ((rr1 (i2003_11_14_17_20_25524) T_0) => (rr (i2003_11_14_17_20_25524) T_0)) (-. (rr (i2003_11_14_17_20_25524) T_0)) (rr1 (i2003_11_14_17_20_25524) T_0) ### Imply 1 2 % 134.01/134.27 4. (All Y, ((rr1 (i2003_11_14_17_20_25524) Y) => (rr (i2003_11_14_17_20_25524) Y))) (rr1 (i2003_11_14_17_20_25524) T_0) (-. (rr (i2003_11_14_17_20_25524) T_0)) ### All 3 % 134.01/134.27 5. (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (-. (rr (i2003_11_14_17_20_25524) T_0)) (rr1 (i2003_11_14_17_20_25524) T_0) ### All 4 % 134.01/134.27 6. (rr3 (i2003_11_14_17_20_25524) T_1) (-. (rr3 (i2003_11_14_17_20_25524) T_1)) ### Axiom % 134.01/134.27 7. (-. (rr (i2003_11_14_17_20_25524) T_1)) (rr (i2003_11_14_17_20_25524) T_1) ### Axiom % 134.01/134.27 8. ((rr3 (i2003_11_14_17_20_25524) T_1) => (rr (i2003_11_14_17_20_25524) T_1)) (-. (rr (i2003_11_14_17_20_25524) T_1)) (rr3 (i2003_11_14_17_20_25524) T_1) ### Imply 6 7 % 134.01/134.27 9. (All Y, ((rr3 (i2003_11_14_17_20_25524) Y) => (rr (i2003_11_14_17_20_25524) Y))) (rr3 (i2003_11_14_17_20_25524) T_1) (-. (rr (i2003_11_14_17_20_25524) T_1)) ### All 8 % 134.01/134.27 10. (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (-. (rr (i2003_11_14_17_20_25524) T_1)) (rr3 (i2003_11_14_17_20_25524) T_1) ### All 9 % 134.01/134.27 11. (rt1 T_0 T_2) (-. (rt1 T_0 T_2)) ### Axiom % 134.01/134.27 12. (-. (rtt T_0 T_2)) (rtt T_0 T_2) ### Axiom % 134.01/134.27 13. ((rt1 T_0 T_2) => (rtt T_0 T_2)) (-. (rtt T_0 T_2)) (rt1 T_0 T_2) ### Imply 11 12 % 134.01/134.27 14. (All Y, ((rt1 T_0 Y) => (rtt T_0 Y))) (rt1 T_0 T_2) (-. (rtt T_0 T_2)) ### All 13 % 134.01/134.27 15. (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (-. (rtt T_0 T_2)) (rt1 T_0 T_2) ### All 14 % 134.01/134.27 16. (T_3 != T_3) ### Refl(=) % 134.01/134.27 17. (rt3 T_1 T_3) (-. (rt3 T_1 T_3)) ### Axiom % 134.01/134.27 18. (-. (rtt T_1 T_3)) (rtt T_1 T_3) ### Axiom % 134.01/134.27 19. ((rt3 T_1 T_3) => (rtt T_1 T_3)) (-. (rtt T_1 T_3)) (rt3 T_1 T_3) ### Imply 17 18 % 134.01/134.27 20. (All Y, ((rt3 T_1 Y) => (rtt T_1 Y))) (rt3 T_1 T_3) (-. (rtt T_1 T_3)) ### All 19 % 134.01/134.27 21. (T_0 = T_1) (T_1 != T_0) ### Sym(=) % 134.01/134.27 22. (rtt T_1 T_3) (-. (rtt T_1 T_3)) ### Axiom % 134.01/134.27 23. (-. (rtt T_0 T_3)) (rtt T_0 T_3) ### Axiom % 134.01/134.27 24. (((T_1 = T_0) /\ (rtt T_1 T_3)) => (rtt T_0 T_3)) (-. (rtt T_0 T_3)) (rtt T_1 T_3) (T_0 = T_1) ### DisjTree 21 22 23 % 134.01/134.27 25. (All C, (((T_1 = T_0) /\ (rtt T_1 C)) => (rtt T_0 C))) (T_0 = T_1) (rtt T_1 T_3) (-. (rtt T_0 T_3)) ### All 24 % 134.01/134.27 26. (All B, (All C, (((T_1 = B) /\ (rtt T_1 C)) => (rtt B C)))) (-. (rtt T_0 T_3)) (rtt T_1 T_3) (T_0 = T_1) ### All 25 % 134.01/134.27 27. (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (T_0 = T_1) (rtt T_1 T_3) (-. (rtt T_0 T_3)) ### All 26 % 134.01/134.27 28. (((T_3 = T_3) /\ (rtt T_1 T_3)) => (rtt T_1 T_3)) (-. (rtt T_0 T_3)) (T_0 = T_1) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (rt3 T_1 T_3) (All Y, ((rt3 T_1 Y) => (rtt T_1 Y))) ### DisjTree 16 20 27 % 134.01/134.27 29. (All C, (((T_3 = T_3) /\ (rtt C T_3)) => (rtt C T_3))) (All Y, ((rt3 T_1 Y) => (rtt T_1 Y))) (rt3 T_1 T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (T_0 = T_1) (-. (rtt T_0 T_3)) ### All 28 % 134.01/134.27 30. (All B, (All C, (((T_3 = B) /\ (rtt C T_3)) => (rtt C B)))) (-. (rtt T_0 T_3)) (T_0 = T_1) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (rt3 T_1 T_3) (All Y, ((rt3 T_1 Y) => (rtt T_1 Y))) ### All 29 % 134.01/134.27 31. (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt3 T_1 T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (T_0 = T_1) (-. (rtt T_0 T_3)) (All B, (All C, (((T_3 = B) /\ (rtt C T_3)) => (rtt C B)))) ### All 30 % 134.01/134.27 32. (T_3 != T_2) (T_2 = T_3) ### Sym(=) % 134.01/134.27 33. (((rtt T_0 T_2) /\ (rtt T_0 T_3)) => (T_2 = T_3)) (T_3 != T_2) (All B, (All C, (((T_3 = B) /\ (rtt C T_3)) => (rtt C B)))) (T_0 = T_1) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (rt3 T_1 T_3) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) ### DisjTree 15 31 32 % 134.01/134.27 34. (All Z1, (((rtt T_0 T_2) /\ (rtt T_0 Z1)) => (T_2 = Z1))) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt3 T_1 T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (T_0 = T_1) (All B, (All C, (((T_3 = B) /\ (rtt C T_3)) => (rtt C B)))) (T_3 != T_2) ### All 33 % 134.01/134.27 35. (-. ((rr (i2003_11_14_17_20_25524) T_0) /\ ((rr (i2003_11_14_17_20_25524) T_1) /\ (T_0 != T_1)))) (T_3 != T_2) (All B, (All C, (((T_3 = B) /\ (rtt C T_3)) => (rtt C B)))) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (rt3 T_1 T_3) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (All Z1, (((rtt T_0 T_2) /\ (rtt T_0 Z1)) => (T_2 = Z1))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) ### DisjTree 5 10 34 % 134.01/134.27 36. (-. (Ex Y1, ((rr (i2003_11_14_17_20_25524) T_0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (T_0 != Y1))))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All Z1, (((rtt T_0 T_2) /\ (rtt T_0 Z1)) => (T_2 = Z1))) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt3 T_1 T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (All B, (All C, (((T_3 = B) /\ (rtt C T_3)) => (rtt C B)))) (T_3 != T_2) ### NotExists 35 % 134.01/134.27 37. (ce T_3) (-. (ce T_3)) ### Axiom % 134.01/134.27 38. (-. (ce T_2)) (ce T_2) ### Axiom % 134.01/134.27 39. (((T_3 = T_2) /\ (ce T_3)) => (ce T_2)) (-. (ce T_2)) (ce T_3) (All B, (All C, (((T_3 = B) /\ (rtt C T_3)) => (rtt C B)))) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (rt3 T_1 T_3) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (All Z1, (((rtt T_0 T_2) /\ (rtt T_0 Z1)) => (T_2 = Z1))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (-. (Ex Y1, ((rr (i2003_11_14_17_20_25524) T_0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (T_0 != Y1))))) ### DisjTree 36 37 38 % 134.01/134.27 40. (All B, (((T_3 = B) /\ (ce T_3)) => (ce B))) (-. (Ex Y1, ((rr (i2003_11_14_17_20_25524) T_0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (T_0 != Y1))))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All Z1, (((rtt T_0 T_2) /\ (rtt T_0 Z1)) => (T_2 = Z1))) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt3 T_1 T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (All B, (All C, (((T_3 = B) /\ (rtt C T_3)) => (rtt C B)))) (ce T_3) (-. (ce T_2)) ### All 39 % 134.01/134.27 41. (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (-. (ce T_2)) (ce T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (rt3 T_1 T_3) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (All Z1, (((rtt T_0 T_2) /\ (rtt T_0 Z1)) => (T_2 = Z1))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (-. (Ex Y1, ((rr (i2003_11_14_17_20_25524) T_0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (T_0 != Y1))))) (All B, (((T_3 = B) /\ (ce T_3)) => (ce B))) ### All 40 % 134.01/134.27 42. (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (-. (Ex Y1, ((rr (i2003_11_14_17_20_25524) T_0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (T_0 != Y1))))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All Z1, (((rtt T_0 T_2) /\ (rtt T_0 Z1)) => (T_2 = Z1))) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt3 T_1 T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (ce T_3) (-. (ce T_2)) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) ### All 41 % 134.01/134.27 43. (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (-. (ce T_2)) (ce T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (rt3 T_1 T_3) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (All Z1, (((rtt T_0 T_2) /\ (rtt T_0 Z1)) => (T_2 = Z1))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) ### NotExists 42 % 134.09/134.30 44. (All Z0, (All Z1, (((rtt T_0 Z0) /\ (rtt T_0 Z1)) => (Z0 = Z1)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt3 T_1 T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (ce T_3) (-. (ce T_2)) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) ### All 43 % 134.09/134.30 45. (cc T_2) (-. (cc T_2)) ### Axiom % 134.09/134.30 46. (-. ((ce T_2) /\ (cc T_2))) (cc T_2) (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (ce T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (rt3 T_1 T_3) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All Z0, (All Z1, (((rtt T_0 Z0) /\ (rtt T_0 Z1)) => (Z0 = Z1)))) ### NotAnd 44 45 % 134.09/134.30 47. (All X, (-. ((ce X) /\ (cc X)))) (All Z0, (All Z1, (((rtt T_0 Z0) /\ (rtt T_0 Z1)) => (Z0 = Z1)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (rt1 T_0 T_2) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt3 T_1 T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (ce T_3) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) (cc T_2) ### All 46 % 134.09/134.30 48. ((rt1 T_0 T_2) /\ (cc T_2)) (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (ce T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (rt3 T_1 T_3) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All Z0, (All Z1, (((rtt T_0 Z0) /\ (rtt T_0 Z1)) => (Z0 = Z1)))) (All X, (-. ((ce X) /\ (cc X)))) ### And 47 % 134.09/134.30 49. (Ex Z, ((rt1 T_0 Z) /\ (cc Z))) (All X, (-. ((ce X) /\ (cc X)))) (All Z0, (All Z1, (((rtt T_0 Z0) /\ (rtt T_0 Z1)) => (Z0 = Z1)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (rr1 (i2003_11_14_17_20_25524) T_0) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt3 T_1 T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (ce T_3) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) ### Exists 48 % 134.09/134.31 50. ((rr1 (i2003_11_14_17_20_25524) T_0) /\ ((All Z0, (All Z1, (((rtt T_0 Z0) /\ (rtt T_0 Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rt1 T_0 Z) /\ (cc Z))))) (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (ce T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (rt3 T_1 T_3) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All X, (-. ((ce X) /\ (cc X)))) ### ConjTree 49 % 134.09/134.31 51. (Ex Y, ((rr1 (i2003_11_14_17_20_25524) Y) /\ ((All Z0, (All Z1, (((rtt Y Z0) /\ (rtt Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rt1 Y Z) /\ (cc Z)))))) (All X, (-. ((ce X) /\ (cc X)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (rt3 T_1 T_3) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (ce T_3) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) ### Exists 50 % 134.09/134.31 52. ((rt3 T_1 T_3) /\ (ce T_3)) (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All X, (-. ((ce X) /\ (cc X)))) (Ex Y, ((rr1 (i2003_11_14_17_20_25524) Y) /\ ((All Z0, (All Z1, (((rtt Y Z0) /\ (rtt Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rt1 Y Z) /\ (cc Z)))))) ### And 51 % 134.09/134.31 53. (Ex Z, ((rt3 T_1 Z) /\ (ce Z))) (Ex Y, ((rr1 (i2003_11_14_17_20_25524) Y) /\ ((All Z0, (All Z1, (((rtt Y Z0) /\ (rtt Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rt1 Y Z) /\ (cc Z)))))) (All X, (-. ((ce X) /\ (cc X)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (rr3 (i2003_11_14_17_20_25524) T_1) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) ### Exists 52 % 134.09/134.31 54. ((rr3 (i2003_11_14_17_20_25524) T_1) /\ ((Ex Z, ((rt3 T_1 Z) /\ (ce Z))) /\ (All Z0, (All Z1, (((rtt T_1 Z0) /\ (rtt T_1 Z1)) => (Z0 = Z1)))))) (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All X, (-. ((ce X) /\ (cc X)))) (Ex Y, ((rr1 (i2003_11_14_17_20_25524) Y) /\ ((All Z0, (All Z1, (((rtt Y Z0) /\ (rtt Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rt1 Y Z) /\ (cc Z)))))) ### ConjTree 53 % 134.09/134.31 55. (Ex Y, ((rr3 (i2003_11_14_17_20_25524) Y) /\ ((Ex Z, ((rt3 Y Z) /\ (ce Z))) /\ (All Z0, (All Z1, (((rtt Y Z0) /\ (rtt Y Z1)) => (Z0 = Z1))))))) (Ex Y, ((rr1 (i2003_11_14_17_20_25524) Y) /\ ((All Z0, (All Z1, (((rtt Y Z0) /\ (rtt Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rt1 Y Z) /\ (cc Z)))))) (All X, (-. ((ce X) /\ (cc X)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) ### Exists 54 % 134.09/134.31 56. ((Ex Y, ((rr3 (i2003_11_14_17_20_25524) Y) /\ ((Ex Z, ((rt3 Y Z) /\ (ce Z))) /\ (All Z0, (All Z1, (((rtt Y Z0) /\ (rtt Y Z1)) => (Z0 = Z1))))))) /\ ((Ex Y, ((rr2 (i2003_11_14_17_20_25524) Y) /\ ((All Z0, (All Z1, (((rtt Y Z0) /\ (rtt Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rt2 Y Z) /\ (cd Z)))))) /\ ((-. (Ex Y0, (Ex Y1, ((rr (i2003_11_14_17_20_25524) Y0) /\ ((rr (i2003_11_14_17_20_25524) Y1) /\ (Y0 != Y1)))))) /\ (Ex Y, ((rr1 (i2003_11_14_17_20_25524) Y) /\ ((All Z0, (All Z1, (((rtt Y Z0) /\ (rtt Y Z1)) => (Z0 = Z1)))) /\ (Ex Z, ((rt1 Y Z) /\ (cc Z))))))))) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All X, (-. ((ce X) /\ (cc X)))) ### ConjTree 55 % 134.09/134.31 57. (cUnsatisfiable (i2003_11_14_17_20_25524)) (All X, (-. ((ce X) /\ (cc X)))) (All A, (All B, (((A = B) /\ (ce A)) => (ce B)))) (All X, (All Y, ((rr1 X Y) => (rr X Y)))) (All X, (All Y, ((rr3 X Y) => (rr X Y)))) (All X, (All Y, ((rt1 X Y) => (rtt X Y)))) (All X, (All Y, ((rt3 X Y) => (rtt X Y)))) (All A, (All B, (All C, (((A = B) /\ (rtt A C)) => (rtt B C))))) (All A, (All B, (All C, (((A = B) /\ (rtt C A)) => (rtt C B))))) ### Definition-Pseudo(cUnsatisfiable) 56 % 134.09/134.31 % SZS output end Proof % 134.09/134.31 (* END-PROOF *) %------------------------------------------------------------------------------