%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN551+2 : TPTP v8.1.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n029.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 : Thu Jul 21 12:45:07 EDT 2022 % Result : Theorem 2.06s 2.26s % Output : Proof 2.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYN551+2 : TPTP v8.1.0. Bugfixed v3.1.0. % 0.12/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n029.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 : Mon Jul 11 13:30:47 EDT 2022 % 0.12/0.34 % CPUTime : % 2.06/2.26 % SZS status Theorem % 2.06/2.26 (* PROOF-FOUND *) % 2.06/2.26 (* BEGIN-PROOF *) % 2.06/2.26 % SZS output start Proof % 2.06/2.26 1. (T_0 != T_0) ### Refl(=) % 2.06/2.26 2. (T_0 = (g (f T_0))) (T_0 != (g (f T_0))) ### Axiom % 2.06/2.26 3. ((g (f T_0)) = (g (f (g (f T_0))))) ((g (f T_0)) != (g (f (g (f T_0))))) ### Axiom % 2.06/2.26 4. ((f (g (f T_0))) != (f (g (f (g (f T_0)))))) ((g (f T_0)) = (g (f (g (f T_0))))) ### NotEqual 3 % 2.06/2.26 5. ((g (f (g (f T_0)))) != (g (f (g (f (g (f T_0))))))) ((g (f T_0)) = (g (f (g (f T_0))))) ### NotEqual 4 % 2.06/2.26 6. ((g (f (g (f T_0)))) = (g (f (g (f (g (f T_0))))))) ((g (f (g (f T_0)))) != (g (f (g (f (g (f T_0))))))) ### Axiom % 2.06/2.26 7. ((f (g (f (g (f T_0))))) != (f (g (f (g (f (g (f T_0)))))))) ((g (f (g (f T_0)))) = (g (f (g (f (g (f T_0))))))) ### NotEqual 6 % 2.06/2.26 8. ((g (f (g (f (g (f T_0)))))) != (g (f (g (f (g (f (g (f T_0))))))))) ((g (f (g (f T_0)))) = (g (f (g (f (g (f T_0))))))) ### NotEqual 7 % 2.06/2.26 9. ((g (f (g (f (g (f T_0)))))) = (g (f (g (f (g (f (g (f T_0))))))))) ((g (f (g (f (g (f T_0)))))) != (g (f (g (f (g (f (g (f T_0))))))))) ### Axiom % 2.06/2.26 10. ((f (g (f (g (f (g (f T_0))))))) != (f (g (f (g (f (g (f (g (f T_0)))))))))) ((g (f (g (f (g (f T_0)))))) = (g (f (g (f (g (f (g (f T_0))))))))) ### NotEqual 9 % 2.06/2.26 11. ((g (f (g (f (g (f (g (f T_0)))))))) != (g (f (g (f (g (f (g (f (g (f T_0))))))))))) ((g (f (g (f (g (f T_0)))))) = (g (f (g (f (g (f (g (f T_0))))))))) ### NotEqual 10 % 2.06/2.26 12. ((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) ((g (f (g (f (g (f (g (f T_0)))))))) != (g (f (g (f (g (f (g (f (g (f T_0))))))))))) ### Axiom % 2.06/2.26 13. ((f (g (f (g (f (g (f (g (f T_0))))))))) != (f (g (f (g (f (g (f (g (f (g (f T_0)))))))))))) ((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) ### NotEqual 12 % 2.06/2.26 14. ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) != (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) ((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) ### NotEqual 13 % 2.06/2.26 15. ((f (g (f (g (f (g (f T_0))))))) = T_1) (T_1 != (f (g (f (g (f (g (f T_0)))))))) ### Sym(=) % 2.06/2.26 16. ((g T_1) != (g (f (g (f (g (f (g (f T_0))))))))) ((f (g (f (g (f (g (f T_0))))))) = T_1) ### NotEqual 15 % 2.06/2.26 17. (T_0 = (g (f (g (f T_0))))) ((g (f (g (f T_0)))) != T_0) ### Sym(=) % 2.06/2.26 18. ((f (g (f (g (f T_0))))) != (f T_0)) (T_0 = (g (f (g (f T_0))))) ### NotEqual 17 % 2.06/2.26 19. ((g (f (g (f (g (f T_0)))))) != (g (f T_0))) (T_0 = (g (f (g (f T_0))))) ### NotEqual 18 % 2.06/2.26 20. ((f (g (f (g (f (g (f T_0))))))) != (f (g (f T_0)))) (T_0 = (g (f (g (f T_0))))) ### NotEqual 19 % 2.06/2.26 21. ((g (f (g (f (g (f (g (f T_0)))))))) != (g (f (g (f T_0))))) (T_0 = (g (f (g (f T_0))))) ### NotEqual 20 % 2.06/2.26 22. ((f (g (f (g (f (g (f (g (f T_0))))))))) != (f (g (f (g (f T_0)))))) (T_0 = (g (f (g (f T_0))))) ### NotEqual 21 % 2.06/2.26 23. ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) != (g (f (g (f (g (f T_0))))))) (T_0 = (g (f (g (f T_0))))) ### NotEqual 22 % 2.06/2.26 24. ((g T_1) != (g (f (g (f (g (f T_0))))))) ((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) (T_0 = (g (f (g (f T_0))))) ((f (g (f (g (f (g (f T_0))))))) = T_1) ### Trans 16 23 % 2.06/2.26 25. ((f (g T_1)) != (f (g (f (g (f (g (f T_0)))))))) ((f (g (f (g (f (g (f T_0))))))) = T_1) (T_0 = (g (f (g (f T_0))))) ((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) ### NotEqual 24 % 2.06/2.26 26. (T_1 != T_1) ### Refl(=) % 2.06/2.26 27. (T_1 != (f (g T_1))) ((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) (T_0 = (g (f (g (f T_0))))) ((f (g (f (g (f (g (f T_0))))))) = T_1) ### Trans-sym 25 26 % 2.06/2.26 28. ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) != (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) ### Axiom % 2.06/2.26 29. ((f (g (f (g (f (g (f (g (f (g (f T_0))))))))))) != (f (g (f (g (f (g (f (g (f (g (f (g (f T_0)))))))))))))) ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) ### NotEqual 28 % 2.06/2.26 30. ((g (f (g (f (g (f (g (f (g (f (g (f T_0)))))))))))) != (g (f (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))))) ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) ### NotEqual 29 % 2.06/2.26 31. (T_1 != T_1) ### Refl(=) % 2.06/2.26 32. (T_1 != T_1) ### Refl(=) % 2.06/2.26 33. (T_1 = (f (g T_1))) (T_1 != (f (g T_1))) ### Axiom % 2.06/2.26 34. ((g T_1) != (g (f (g T_1)))) (T_1 = (f (g T_1))) ### NotEqual 33 % 2.06/2.26 35. (T_0 = (g T_1)) ((g T_1) != T_0) ### Sym(=) % 2.06/2.26 36. (T_0 = (g (f (g (f (g (f T_0))))))) ((g (f (g (f (g (f T_0)))))) != T_0) ### Sym(=) % 2.06/2.26 37. ((f (g (f (g (f (g (f T_0))))))) != (f T_0)) (T_0 = (g (f (g (f (g (f T_0))))))) ### NotEqual 36 % 2.06/2.26 38. ((g (f (g (f (g (f (g (f T_0)))))))) != (g (f T_0))) (T_0 = (g (f (g (f (g (f T_0))))))) ### NotEqual 37 % 2.06/2.26 39. ((f (g (f (g (f (g (f (g (f T_0))))))))) != (f (g (f T_0)))) (T_0 = (g (f (g (f (g (f T_0))))))) ### NotEqual 38 % 2.06/2.26 40. ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) != (g (f (g (f T_0))))) (T_0 = (g (f (g (f (g (f T_0))))))) ### NotEqual 39 % 2.06/2.26 41. ((f (g (f (g (f (g (f (g (f (g (f T_0))))))))))) != (f (g (f (g (f T_0)))))) (T_0 = (g (f (g (f (g (f T_0))))))) ### NotEqual 40 % 2.06/2.26 42. ((g (f (g (f (g (f (g (f (g (f (g (f T_0)))))))))))) != (g (f (g (f (g (f T_0))))))) (T_0 = (g (f (g (f (g (f T_0))))))) ### NotEqual 41 % 2.06/2.26 43. ((g T_1) != (g (f (g (f (g (f T_0))))))) (T_0 = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) (T_0 = (g (f (g (f (g (f T_0))))))) (T_0 = (g T_1)) ### Trans 35 42 % 2.06/2.26 44. (((g T_1) = (g (f (g T_1)))) <=> (T_0 = (g T_1))) (T_0 = (g (f (g (f (g (f T_0))))))) (T_0 = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) ((g T_1) != (g (f (g (f (g (f T_0))))))) (T_1 = (f (g T_1))) ### Equiv 34 43 % 2.06/2.26 45. (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (T_1 = (f (g T_1))) ((g T_1) != (g (f (g (f (g (f T_0))))))) (T_0 = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) (T_0 = (g (f (g (f (g (f T_0))))))) ### All 44 % 2.06/2.26 46. ((f (g T_1)) != (f (g (f (g (f (g (f T_0)))))))) (T_0 = (g (f (g (f (g (f T_0))))))) (T_0 = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) (T_1 = (f (g T_1))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) ### NotEqual 45 % 2.06/2.26 47. ((f (g (f (g (f (g (f T_0))))))) != T_1) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (T_1 = (f (g T_1))) (T_0 = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) (T_0 = (g (f (g (f (g (f T_0))))))) ### TransEq-sym 31 32 46 % 2.06/2.26 48. (((g (f (g (f (g (f (g (f (g (f (g (f T_0)))))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))))) <=> (T_0 = (g (f (g (f (g (f (g (f (g (f (g (f T_0)))))))))))))) (T_0 = (g (f (g (f (g (f T_0))))))) (T_1 = (f (g T_1))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) ((f (g (f (g (f (g (f T_0))))))) != T_1) ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) ### Equiv 30 47 % 2.06/2.26 49. ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) ((f (g (f (g (f (g (f T_0))))))) != T_1) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (T_1 = (f (g T_1))) (T_0 = (g (f (g (f (g (f T_0))))))) ### All 48 % 2.06/2.26 50. (-. ((T_1 = (f (g T_1))) <=> ((f (g (f (g (f (g (f T_0))))))) = T_1))) (T_0 = (g (f (g (f (g (f T_0))))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) (T_0 = (g (f (g (f T_0))))) ((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) ### NotEquiv 27 49 % 2.06/2.26 51. (-. (All Y, ((Y = (f (g Y))) <=> ((f (g (f (g (f (g (f T_0))))))) = Y)))) ((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) (T_0 = (g (f (g (f T_0))))) ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (T_0 = (g (f (g (f (g (f T_0))))))) ### NotAllEx 50 % 2.06/2.26 52. (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) (T_0 = (g (f (g (f (g (f T_0))))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) ((g (f (g (f (g (f (g (f (g (f T_0)))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) (T_0 = (g (f (g (f T_0))))) ((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) ### NotExists 51 % 2.06/2.27 53. (((g (f (g (f (g (f (g (f (g (f T_0)))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f T_0))))))))))))) <=> (T_0 = (g (f (g (f (g (f (g (f (g (f T_0)))))))))))) (T_0 = (g (f (g (f T_0))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (T_0 = (g (f (g (f (g (f T_0))))))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) ((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) ### Equiv 14 52 % 2.06/2.27 54. ((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) (T_0 = (g (f (g (f (g (f T_0))))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (T_0 = (g (f (g (f T_0))))) ### All 53 % 2.06/2.27 55. (((g (f (g (f (g (f (g (f T_0)))))))) = (g (f (g (f (g (f (g (f (g (f T_0))))))))))) <=> (T_0 = (g (f (g (f (g (f (g (f T_0)))))))))) (T_0 = (g (f (g (f T_0))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (T_0 = (g (f (g (f (g (f T_0))))))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) ((g (f (g (f (g (f T_0)))))) = (g (f (g (f (g (f (g (f T_0))))))))) ### Equiv 11 54 % 2.06/2.27 56. ((g (f (g (f (g (f T_0)))))) = (g (f (g (f (g (f (g (f T_0))))))))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) (T_0 = (g (f (g (f (g (f T_0))))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (T_0 = (g (f (g (f T_0))))) ### All 55 % 2.06/2.27 57. (((g (f (g (f (g (f T_0)))))) = (g (f (g (f (g (f (g (f T_0))))))))) <=> (T_0 = (g (f (g (f (g (f T_0)))))))) (T_0 = (g (f (g (f T_0))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) ((g (f (g (f T_0)))) = (g (f (g (f (g (f T_0))))))) ### Equiv 8 56 % 2.06/2.27 58. ((g (f (g (f T_0)))) = (g (f (g (f (g (f T_0))))))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (T_0 = (g (f (g (f T_0))))) ### All 57 % 2.06/2.27 59. (((g (f (g (f T_0)))) = (g (f (g (f (g (f T_0))))))) <=> (T_0 = (g (f (g (f T_0)))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) ((g (f T_0)) = (g (f (g (f T_0))))) ### Equiv 5 58 % 2.06/2.27 60. ((g (f T_0)) = (g (f (g (f T_0))))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) ### All 59 % 2.06/2.27 61. (((g (f T_0)) = (g (f (g (f T_0))))) <=> (T_0 = (g (f T_0)))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) (T_0 = (g (f T_0))) ### Equiv 2 60 % 2.06/2.27 62. (T_0 = (g (f T_0))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) ### All 61 % 2.06/2.27 63. ((T_0 = (g (f T_0))) <=> (T_0 = T_0)) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) ### Equiv 1 62 % 2.06/2.27 64. (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) (All Y, ((Y = (g (f Y))) <=> (T_0 = Y))) ### All 63 % 2.06/2.27 65. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y)))) (-. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y))))) ### Exists 64 % 2.06/2.27 66. (T_2 != T_2) ### Refl(=) % 2.06/2.27 67. (T_2 = (f (g T_2))) (T_2 != (f (g T_2))) ### Axiom % 2.06/2.27 68. ((f (g T_2)) = (f (g (f (g T_2))))) ((f (g T_2)) != (f (g (f (g T_2))))) ### Axiom % 2.06/2.27 69. ((g (f (g T_2))) != (g (f (g (f (g T_2)))))) ((f (g T_2)) = (f (g (f (g T_2))))) ### NotEqual 68 % 2.06/2.27 70. ((f (g (f (g T_2)))) != (f (g (f (g (f (g T_2))))))) ((f (g T_2)) = (f (g (f (g T_2))))) ### NotEqual 69 % 2.06/2.27 71. ((f (g (f (g T_2)))) = (f (g (f (g (f (g T_2))))))) ((f (g (f (g T_2)))) != (f (g (f (g (f (g T_2))))))) ### Axiom % 2.06/2.27 72. ((g (f (g (f (g T_2))))) != (g (f (g (f (g (f (g T_2)))))))) ((f (g (f (g T_2)))) = (f (g (f (g (f (g T_2))))))) ### NotEqual 71 % 2.06/2.27 73. ((f (g (f (g (f (g T_2)))))) != (f (g (f (g (f (g (f (g T_2))))))))) ((f (g (f (g T_2)))) = (f (g (f (g (f (g T_2))))))) ### NotEqual 72 % 2.06/2.27 74. ((f (g (f (g (f (g T_2)))))) = (f (g (f (g (f (g (f (g T_2))))))))) ((f (g (f (g (f (g T_2)))))) != (f (g (f (g (f (g (f (g T_2))))))))) ### Axiom % 2.06/2.27 75. ((g (f (g (f (g (f (g T_2))))))) != (g (f (g (f (g (f (g (f (g T_2)))))))))) ((f (g (f (g (f (g T_2)))))) = (f (g (f (g (f (g (f (g T_2))))))))) ### NotEqual 74 % 2.06/2.27 76. ((f (g (f (g (f (g (f (g T_2)))))))) != (f (g (f (g (f (g (f (g (f (g T_2))))))))))) ((f (g (f (g (f (g T_2)))))) = (f (g (f (g (f (g (f (g T_2))))))))) ### NotEqual 75 % 2.06/2.27 77. ((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) ((f (g (f (g (f (g (f (g T_2)))))))) != (f (g (f (g (f (g (f (g (f (g T_2))))))))))) ### Axiom % 2.06/2.27 78. ((g (f (g (f (g (f (g (f (g T_2))))))))) != (g (f (g (f (g (f (g (f (g (f (g T_2)))))))))))) ((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) ### NotEqual 77 % 2.06/2.27 79. ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) != (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) ((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) ### NotEqual 78 % 2.06/2.27 80. ((g (f (g (f (g (f (g T_2))))))) = T_3) (T_3 != (g (f (g (f (g (f (g T_2)))))))) ### Sym(=) % 2.06/2.27 81. ((f T_3) != (f (g (f (g (f (g (f (g T_2))))))))) ((g (f (g (f (g (f (g T_2))))))) = T_3) ### NotEqual 80 % 2.06/2.27 82. (T_2 = (f (g (f (g T_2))))) ((f (g (f (g T_2)))) != T_2) ### Sym(=) % 2.06/2.27 83. ((g (f (g (f (g T_2))))) != (g T_2)) (T_2 = (f (g (f (g T_2))))) ### NotEqual 82 % 2.06/2.27 84. ((f (g (f (g (f (g T_2)))))) != (f (g T_2))) (T_2 = (f (g (f (g T_2))))) ### NotEqual 83 % 2.06/2.27 85. ((g (f (g (f (g (f (g T_2))))))) != (g (f (g T_2)))) (T_2 = (f (g (f (g T_2))))) ### NotEqual 84 % 2.06/2.27 86. ((f (g (f (g (f (g (f (g T_2)))))))) != (f (g (f (g T_2))))) (T_2 = (f (g (f (g T_2))))) ### NotEqual 85 % 2.06/2.27 87. ((g (f (g (f (g (f (g (f (g T_2))))))))) != (g (f (g (f (g T_2)))))) (T_2 = (f (g (f (g T_2))))) ### NotEqual 86 % 2.06/2.27 88. ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) != (f (g (f (g (f (g T_2))))))) (T_2 = (f (g (f (g T_2))))) ### NotEqual 87 % 2.06/2.27 89. ((f T_3) != (f (g (f (g (f (g T_2))))))) ((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) (T_2 = (f (g (f (g T_2))))) ((g (f (g (f (g (f (g T_2))))))) = T_3) ### Trans 81 88 % 2.06/2.27 90. ((g (f T_3)) != (g (f (g (f (g (f (g T_2)))))))) ((g (f (g (f (g (f (g T_2))))))) = T_3) (T_2 = (f (g (f (g T_2))))) ((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) ### NotEqual 89 % 2.06/2.27 91. (T_3 != T_3) ### Refl(=) % 2.06/2.27 92. (T_3 != (g (f T_3))) ((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) (T_2 = (f (g (f (g T_2))))) ((g (f (g (f (g (f (g T_2))))))) = T_3) ### Trans-sym 90 91 % 2.06/2.27 93. ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) != (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) ### Axiom % 2.06/2.27 94. ((g (f (g (f (g (f (g (f (g (f (g T_2))))))))))) != (g (f (g (f (g (f (g (f (g (f (g (f (g T_2)))))))))))))) ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) ### NotEqual 93 % 2.06/2.27 95. ((f (g (f (g (f (g (f (g (f (g (f (g T_2)))))))))))) != (f (g (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))))) ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) ### NotEqual 94 % 2.06/2.27 96. (T_3 != T_3) ### Refl(=) % 2.06/2.27 97. (T_3 != T_3) ### Refl(=) % 2.06/2.27 98. (T_3 = (g (f T_3))) (T_3 != (g (f T_3))) ### Axiom % 2.06/2.27 99. ((f T_3) != (f (g (f T_3)))) (T_3 = (g (f T_3))) ### NotEqual 98 % 2.06/2.27 100. (T_2 = (f T_3)) ((f T_3) != T_2) ### Sym(=) % 2.06/2.27 101. (T_2 = (f (g (f (g (f (g T_2))))))) ((f (g (f (g (f (g T_2)))))) != T_2) ### Sym(=) % 2.06/2.27 102. ((g (f (g (f (g (f (g T_2))))))) != (g T_2)) (T_2 = (f (g (f (g (f (g T_2))))))) ### NotEqual 101 % 2.06/2.27 103. ((f (g (f (g (f (g (f (g T_2)))))))) != (f (g T_2))) (T_2 = (f (g (f (g (f (g T_2))))))) ### NotEqual 102 % 2.06/2.27 104. ((g (f (g (f (g (f (g (f (g T_2))))))))) != (g (f (g T_2)))) (T_2 = (f (g (f (g (f (g T_2))))))) ### NotEqual 103 % 2.06/2.27 105. ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) != (f (g (f (g T_2))))) (T_2 = (f (g (f (g (f (g T_2))))))) ### NotEqual 104 % 2.06/2.27 106. ((g (f (g (f (g (f (g (f (g (f (g T_2))))))))))) != (g (f (g (f (g T_2)))))) (T_2 = (f (g (f (g (f (g T_2))))))) ### NotEqual 105 % 2.06/2.27 107. ((f (g (f (g (f (g (f (g (f (g (f (g T_2)))))))))))) != (f (g (f (g (f (g T_2))))))) (T_2 = (f (g (f (g (f (g T_2))))))) ### NotEqual 106 % 2.06/2.27 108. ((f T_3) != (f (g (f (g (f (g T_2))))))) (T_2 = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) (T_2 = (f (g (f (g (f (g T_2))))))) (T_2 = (f T_3)) ### Trans 100 107 % 2.06/2.28 109. (((f T_3) = (f (g (f T_3)))) <=> (T_2 = (f T_3))) (T_2 = (f (g (f (g (f (g T_2))))))) (T_2 = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) ((f T_3) != (f (g (f (g (f (g T_2))))))) (T_3 = (g (f T_3))) ### Equiv 99 108 % 2.06/2.28 110. (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (T_3 = (g (f T_3))) ((f T_3) != (f (g (f (g (f (g T_2))))))) (T_2 = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) (T_2 = (f (g (f (g (f (g T_2))))))) ### All 109 % 2.06/2.28 111. ((g (f T_3)) != (g (f (g (f (g (f (g T_2)))))))) (T_2 = (f (g (f (g (f (g T_2))))))) (T_2 = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) (T_3 = (g (f T_3))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) ### NotEqual 110 % 2.06/2.28 112. ((g (f (g (f (g (f (g T_2))))))) != T_3) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (T_3 = (g (f T_3))) (T_2 = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) (T_2 = (f (g (f (g (f (g T_2))))))) ### TransEq-sym 96 97 111 % 2.06/2.28 113. (((f (g (f (g (f (g (f (g (f (g (f (g T_2)))))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))))) <=> (T_2 = (f (g (f (g (f (g (f (g (f (g (f (g T_2)))))))))))))) (T_2 = (f (g (f (g (f (g T_2))))))) (T_3 = (g (f T_3))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) ((g (f (g (f (g (f (g T_2))))))) != T_3) ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) ### Equiv 95 112 % 2.06/2.28 114. ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) ((g (f (g (f (g (f (g T_2))))))) != T_3) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (T_3 = (g (f T_3))) (T_2 = (f (g (f (g (f (g T_2))))))) ### All 113 % 2.06/2.28 115. (-. ((T_3 = (g (f T_3))) <=> ((g (f (g (f (g (f (g T_2))))))) = T_3))) (T_2 = (f (g (f (g (f (g T_2))))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) (T_2 = (f (g (f (g T_2))))) ((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) ### NotEquiv 92 114 % 2.06/2.28 116. (-. (All Y, ((Y = (g (f Y))) <=> ((g (f (g (f (g (f (g T_2))))))) = Y)))) ((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) (T_2 = (f (g (f (g T_2))))) ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (T_2 = (f (g (f (g (f (g T_2))))))) ### NotAllEx 115 % 2.06/2.28 117. (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) (T_2 = (f (g (f (g (f (g T_2))))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) ((f (g (f (g (f (g (f (g (f (g T_2)))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) (T_2 = (f (g (f (g T_2))))) ((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) ### NotExists 116 % 2.06/2.28 118. (((f (g (f (g (f (g (f (g (f (g T_2)))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g T_2))))))))))))) <=> (T_2 = (f (g (f (g (f (g (f (g (f (g T_2)))))))))))) (T_2 = (f (g (f (g T_2))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (T_2 = (f (g (f (g (f (g T_2))))))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) ((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) ### Equiv 79 117 % 2.06/2.28 119. ((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) (T_2 = (f (g (f (g (f (g T_2))))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (T_2 = (f (g (f (g T_2))))) ### All 118 % 2.06/2.28 120. (((f (g (f (g (f (g (f (g T_2)))))))) = (f (g (f (g (f (g (f (g (f (g T_2))))))))))) <=> (T_2 = (f (g (f (g (f (g (f (g T_2)))))))))) (T_2 = (f (g (f (g T_2))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (T_2 = (f (g (f (g (f (g T_2))))))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) ((f (g (f (g (f (g T_2)))))) = (f (g (f (g (f (g (f (g T_2))))))))) ### Equiv 76 119 % 2.06/2.28 121. ((f (g (f (g (f (g T_2)))))) = (f (g (f (g (f (g (f (g T_2))))))))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) (T_2 = (f (g (f (g (f (g T_2))))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (T_2 = (f (g (f (g T_2))))) ### All 120 % 2.06/2.28 122. (((f (g (f (g (f (g T_2)))))) = (f (g (f (g (f (g (f (g T_2))))))))) <=> (T_2 = (f (g (f (g (f (g T_2)))))))) (T_2 = (f (g (f (g T_2))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) ((f (g (f (g T_2)))) = (f (g (f (g (f (g T_2))))))) ### Equiv 73 121 % 2.06/2.28 123. ((f (g (f (g T_2)))) = (f (g (f (g (f (g T_2))))))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (T_2 = (f (g (f (g T_2))))) ### All 122 % 2.06/2.28 124. (((f (g (f (g T_2)))) = (f (g (f (g (f (g T_2))))))) <=> (T_2 = (f (g (f (g T_2)))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) ((f (g T_2)) = (f (g (f (g T_2))))) ### Equiv 70 123 % 2.06/2.28 125. ((f (g T_2)) = (f (g (f (g T_2))))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) ### All 124 % 2.06/2.28 126. (((f (g T_2)) = (f (g (f (g T_2))))) <=> (T_2 = (f (g T_2)))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) (T_2 = (f (g T_2))) ### Equiv 67 125 % 2.06/2.28 127. (T_2 = (f (g T_2))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) ### All 126 % 2.06/2.28 128. ((T_2 = (f (g T_2))) <=> (T_2 = T_2)) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) ### Equiv 66 127 % 2.06/2.28 129. (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) (All Y, ((Y = (f (g Y))) <=> (T_2 = Y))) ### All 128 % 2.06/2.28 130. (Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y)))) (-. (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y))))) ### Exists 129 % 2.06/2.28 131. (-. ((Ex X, (All Y, ((Y = (f (g Y))) <=> (X = Y)))) <=> (Ex X, (All Y, ((Y = (g (f Y))) <=> (X = Y)))))) ### NotEquiv 65 130 % 2.06/2.28 % SZS output end Proof % 2.06/2.28 (* END-PROOF *) %------------------------------------------------------------------------------