%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SET768+4 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n028.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 : Tue Jul 19 05:43:51 EDT 2022 % Result : Theorem 0.51s 0.74s % Output : Proof 0.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET768+4 : TPTP v8.1.0. Released v2.2.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sun Jul 10 01:34:11 EDT 2022 % 0.13/0.34 % CPUTime : % 0.51/0.74 % SZS status Theorem % 0.51/0.74 (* PROOF-FOUND *) % 0.51/0.74 (* BEGIN-PROOF *) % 0.51/0.74 % SZS output start Proof % 0.51/0.74 1. (member T_0 (equivalence_class T_1 T_2 T_3)) (-. (member T_0 (equivalence_class T_1 T_2 T_3))) ### Axiom % 0.51/0.74 2. (-. (member T_0 T_2)) (member T_0 T_2) ### Axiom % 0.51/0.74 3. ((member T_0 T_2) /\ (apply T_3 T_1 T_0)) (-. (member T_0 T_2)) ### And 2 % 0.51/0.74 4. ((member T_0 (equivalence_class T_1 T_2 T_3)) <=> ((member T_0 T_2) /\ (apply T_3 T_1 T_0))) (-. (member T_0 T_2)) (member T_0 (equivalence_class T_1 T_2 T_3)) ### Equiv 1 3 % 0.51/0.74 5. (All X, ((member X (equivalence_class T_1 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_1 X)))) (member T_0 (equivalence_class T_1 T_2 T_3)) (-. (member T_0 T_2)) ### All 4 % 0.51/0.74 6. (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (-. (member T_0 T_2)) (member T_0 (equivalence_class T_1 T_2 T_3)) ### All 5 % 0.51/0.74 7. (member T_0 (equivalence_class T_1 T_2 T_3)) (-. (member T_0 (equivalence_class T_1 T_2 T_3))) ### Axiom % 0.51/0.74 8. (member T_4 T_2) (-. (member T_4 T_2)) ### Axiom % 0.51/0.74 9. (member T_1 T_2) (-. (member T_1 T_2)) ### Axiom % 0.51/0.74 10. (member T_0 T_2) (-. (member T_0 T_2)) ### Axiom % 0.51/0.74 11. (member T_1 T_2) (-. (member T_1 T_2)) ### Axiom % 0.51/0.74 12. (member T_4 T_2) (-. (member T_4 T_2)) ### Axiom % 0.51/0.74 13. (apply T_3 T_1 T_4) (-. (apply T_3 T_1 T_4)) ### Axiom % 0.51/0.74 14. (-. (apply T_3 T_4 T_1)) (apply T_3 T_4 T_1) ### Axiom % 0.51/0.74 15. (((member T_1 T_2) /\ (member T_4 T_2)) => ((apply T_3 T_1 T_4) => (apply T_3 T_4 T_1))) (-. (apply T_3 T_4 T_1)) (apply T_3 T_1 T_4) (member T_4 T_2) (member T_1 T_2) ### DisjTree 11 12 13 14 % 0.51/0.74 16. (All Y, (((member T_1 T_2) /\ (member Y T_2)) => ((apply T_3 T_1 Y) => (apply T_3 Y T_1)))) (member T_1 T_2) (member T_4 T_2) (apply T_3 T_1 T_4) (-. (apply T_3 T_4 T_1)) ### All 15 % 0.51/0.74 17. (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (-. (apply T_3 T_4 T_1)) (apply T_3 T_1 T_4) (member T_4 T_2) (member T_1 T_2) ### All 16 % 0.51/0.74 18. (member T_0 (equivalence_class T_1 T_2 T_3)) (-. (member T_0 (equivalence_class T_1 T_2 T_3))) ### Axiom % 0.51/0.74 19. (-. (apply T_3 T_1 T_0)) (apply T_3 T_1 T_0) ### Axiom % 0.51/0.74 20. ((member T_0 T_2) /\ (apply T_3 T_1 T_0)) (-. (apply T_3 T_1 T_0)) ### And 19 % 0.51/0.74 21. ((member T_0 (equivalence_class T_1 T_2 T_3)) <=> ((member T_0 T_2) /\ (apply T_3 T_1 T_0))) (-. (apply T_3 T_1 T_0)) (member T_0 (equivalence_class T_1 T_2 T_3)) ### Equiv 18 20 % 0.51/0.74 22. (All X, ((member X (equivalence_class T_1 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_1 X)))) (member T_0 (equivalence_class T_1 T_2 T_3)) (-. (apply T_3 T_1 T_0)) ### All 21 % 0.51/0.74 23. (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (-. (apply T_3 T_1 T_0)) (member T_0 (equivalence_class T_1 T_2 T_3)) ### All 22 % 0.51/0.74 24. (-. (apply T_3 T_4 T_0)) (apply T_3 T_4 T_0) ### Axiom % 0.51/0.74 25. (((member T_4 T_2) /\ ((member T_1 T_2) /\ (member T_0 T_2))) => (((apply T_3 T_4 T_1) /\ (apply T_3 T_1 T_0)) => (apply T_3 T_4 T_0))) (-. (apply T_3 T_4 T_0)) (member T_0 (equivalence_class T_1 T_2 T_3)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (apply T_3 T_1 T_4) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (member T_0 T_2) (member T_1 T_2) (member T_4 T_2) ### DisjTree 8 9 10 17 23 24 % 0.51/0.74 26. (All Z, (((member T_4 T_2) /\ ((member T_1 T_2) /\ (member Z T_2))) => (((apply T_3 T_4 T_1) /\ (apply T_3 T_1 Z)) => (apply T_3 T_4 Z)))) (member T_4 T_2) (member T_1 T_2) (member T_0 T_2) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (apply T_3 T_1 T_4) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (member T_0 (equivalence_class T_1 T_2 T_3)) (-. (apply T_3 T_4 T_0)) ### All 25 % 0.51/0.74 27. (All Y, (All Z, (((member T_4 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_4 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_4 Z))))) (-. (apply T_3 T_4 T_0)) (member T_0 (equivalence_class T_1 T_2 T_3)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (apply T_3 T_1 T_4) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (member T_0 T_2) (member T_1 T_2) (member T_4 T_2) ### All 26 % 0.51/0.74 28. ((member T_0 T_2) /\ (apply T_3 T_1 T_0)) (member T_4 T_2) (member T_1 T_2) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (apply T_3 T_1 T_4) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (member T_0 (equivalence_class T_1 T_2 T_3)) (-. (apply T_3 T_4 T_0)) (All Y, (All Z, (((member T_4 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_4 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_4 Z))))) ### And 27 % 0.51/0.74 29. ((member T_0 (equivalence_class T_1 T_2 T_3)) <=> ((member T_0 T_2) /\ (apply T_3 T_1 T_0))) (All Y, (All Z, (((member T_4 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_4 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_4 Z))))) (-. (apply T_3 T_4 T_0)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (apply T_3 T_1 T_4) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (member T_1 T_2) (member T_4 T_2) (member T_0 (equivalence_class T_1 T_2 T_3)) ### Equiv 7 28 % 0.51/0.74 30. (All X, ((member X (equivalence_class T_1 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_1 X)))) (member T_0 (equivalence_class T_1 T_2 T_3)) (member T_4 T_2) (member T_1 T_2) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (apply T_3 T_1 T_4) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (-. (apply T_3 T_4 T_0)) (All Y, (All Z, (((member T_4 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_4 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_4 Z))))) ### All 29 % 0.51/0.74 31. (All Y, (All Z, (((member T_4 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_4 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_4 Z))))) (-. (apply T_3 T_4 T_0)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (apply T_3 T_1 T_4) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (member T_1 T_2) (member T_4 T_2) (member T_0 (equivalence_class T_1 T_2 T_3)) ### All 30 % 0.51/0.74 32. (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_0 (equivalence_class T_1 T_2 T_3)) (member T_4 T_2) (member T_1 T_2) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (apply T_3 T_1 T_4) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (-. (apply T_3 T_4 T_0)) ### All 31 % 0.51/0.74 33. (-. ((member T_0 T_2) /\ (apply T_3 T_4 T_0))) (apply T_3 T_1 T_4) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (member T_1 T_2) (member T_4 T_2) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_0 (equivalence_class T_1 T_2 T_3)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) ### NotAnd 6 32 % 0.51/0.74 34. (-. (member T_0 (equivalence_class T_4 T_2 T_3))) (member T_0 (equivalence_class T_4 T_2 T_3)) ### Axiom % 0.51/0.74 35. ((member T_0 (equivalence_class T_4 T_2 T_3)) <=> ((member T_0 T_2) /\ (apply T_3 T_4 T_0))) (-. (member T_0 (equivalence_class T_4 T_2 T_3))) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (member T_0 (equivalence_class T_1 T_2 T_3)) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_4 T_2) (member T_1 T_2) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (apply T_3 T_1 T_4) ### Equiv 33 34 % 0.51/0.74 36. (All X, ((member X (equivalence_class T_4 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_4 X)))) (apply T_3 T_1 T_4) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (member T_1 T_2) (member T_4 T_2) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_0 (equivalence_class T_1 T_2 T_3)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (-. (member T_0 (equivalence_class T_4 T_2 T_3))) ### All 35 % 0.58/0.76 37. (-. (member T_0 (equivalence_class T_4 T_2 T_3))) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (member T_0 (equivalence_class T_1 T_2 T_3)) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_4 T_2) (member T_1 T_2) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (apply T_3 T_1 T_4) ### All 36 % 0.58/0.76 38. (All E, (All A, (All X, ((member X (equivalence_class A E T_3)) <=> ((member X E) /\ (apply T_3 A X)))))) (apply T_3 T_1 T_4) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (member T_1 T_2) (member T_4 T_2) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_0 (equivalence_class T_1 T_2 T_3)) (-. (member T_0 (equivalence_class T_4 T_2 T_3))) ### All 37 % 0.58/0.76 39. (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (-. (member T_0 (equivalence_class T_4 T_2 T_3))) (member T_0 (equivalence_class T_1 T_2 T_3)) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_4 T_2) (member T_1 T_2) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (apply T_3 T_1 T_4) ### All 38 % 0.58/0.76 40. (-. ((member T_0 (equivalence_class T_1 T_2 T_3)) => (member T_0 (equivalence_class T_4 T_2 T_3)))) (apply T_3 T_1 T_4) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (member T_1 T_2) (member T_4 T_2) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) ### NotImply 39 % 0.58/0.76 41. (-. (All X, ((member X (equivalence_class T_1 T_2 T_3)) => (member X (equivalence_class T_4 T_2 T_3))))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_4 T_2) (member T_1 T_2) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (apply T_3 T_1 T_4) ### NotAllEx 40 % 0.58/0.76 42. (-. (subset (equivalence_class T_1 T_2 T_3) (equivalence_class T_4 T_2 T_3))) (apply T_3 T_1 T_4) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (member T_1 T_2) (member T_4 T_2) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) ### Definition-Pseudo(subset) 41 % 0.58/0.76 43. (member T_5 (equivalence_class T_4 T_2 T_3)) (-. (member T_5 (equivalence_class T_4 T_2 T_3))) ### Axiom % 0.58/0.76 44. (-. (member T_5 T_2)) (member T_5 T_2) ### Axiom % 0.58/0.76 45. ((member T_5 T_2) /\ (apply T_3 T_4 T_5)) (-. (member T_5 T_2)) ### And 44 % 0.58/0.76 46. ((member T_5 (equivalence_class T_4 T_2 T_3)) <=> ((member T_5 T_2) /\ (apply T_3 T_4 T_5))) (-. (member T_5 T_2)) (member T_5 (equivalence_class T_4 T_2 T_3)) ### Equiv 43 45 % 0.58/0.76 47. (All X, ((member X (equivalence_class T_4 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_4 X)))) (member T_5 (equivalence_class T_4 T_2 T_3)) (-. (member T_5 T_2)) ### All 46 % 0.58/0.76 48. (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (-. (member T_5 T_2)) (member T_5 (equivalence_class T_4 T_2 T_3)) ### All 47 % 0.58/0.76 49. (member T_5 (equivalence_class T_4 T_2 T_3)) (-. (member T_5 (equivalence_class T_4 T_2 T_3))) ### Axiom % 0.58/0.76 50. (member T_1 T_2) (-. (member T_1 T_2)) ### Axiom % 0.58/0.76 51. (member T_4 T_2) (-. (member T_4 T_2)) ### Axiom % 0.58/0.76 52. (member T_5 T_2) (-. (member T_5 T_2)) ### Axiom % 0.58/0.76 53. (apply T_3 T_1 T_4) (-. (apply T_3 T_1 T_4)) ### Axiom % 0.58/0.76 54. (member T_5 (equivalence_class T_4 T_2 T_3)) (-. (member T_5 (equivalence_class T_4 T_2 T_3))) ### Axiom % 0.58/0.76 55. (-. (apply T_3 T_4 T_5)) (apply T_3 T_4 T_5) ### Axiom % 0.58/0.76 56. ((member T_5 T_2) /\ (apply T_3 T_4 T_5)) (-. (apply T_3 T_4 T_5)) ### And 55 % 0.58/0.76 57. ((member T_5 (equivalence_class T_4 T_2 T_3)) <=> ((member T_5 T_2) /\ (apply T_3 T_4 T_5))) (-. (apply T_3 T_4 T_5)) (member T_5 (equivalence_class T_4 T_2 T_3)) ### Equiv 54 56 % 0.58/0.76 58. (All X, ((member X (equivalence_class T_4 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_4 X)))) (member T_5 (equivalence_class T_4 T_2 T_3)) (-. (apply T_3 T_4 T_5)) ### All 57 % 0.58/0.76 59. (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (-. (apply T_3 T_4 T_5)) (member T_5 (equivalence_class T_4 T_2 T_3)) ### All 58 % 0.58/0.76 60. (-. (apply T_3 T_1 T_5)) (apply T_3 T_1 T_5) ### Axiom % 0.58/0.76 61. (((member T_1 T_2) /\ ((member T_4 T_2) /\ (member T_5 T_2))) => (((apply T_3 T_1 T_4) /\ (apply T_3 T_4 T_5)) => (apply T_3 T_1 T_5))) (-. (apply T_3 T_1 T_5)) (member T_5 (equivalence_class T_4 T_2 T_3)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (apply T_3 T_1 T_4) (member T_5 T_2) (member T_4 T_2) (member T_1 T_2) ### DisjTree 50 51 52 53 59 60 % 0.58/0.76 62. (All Z, (((member T_1 T_2) /\ ((member T_4 T_2) /\ (member Z T_2))) => (((apply T_3 T_1 T_4) /\ (apply T_3 T_4 Z)) => (apply T_3 T_1 Z)))) (member T_1 T_2) (member T_4 T_2) (member T_5 T_2) (apply T_3 T_1 T_4) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (member T_5 (equivalence_class T_4 T_2 T_3)) (-. (apply T_3 T_1 T_5)) ### All 61 % 0.58/0.76 63. (All Y, (All Z, (((member T_1 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_1 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_1 Z))))) (-. (apply T_3 T_1 T_5)) (member T_5 (equivalence_class T_4 T_2 T_3)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (apply T_3 T_1 T_4) (member T_5 T_2) (member T_4 T_2) (member T_1 T_2) ### All 62 % 0.58/0.76 64. ((member T_5 T_2) /\ (apply T_3 T_4 T_5)) (member T_1 T_2) (member T_4 T_2) (apply T_3 T_1 T_4) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (member T_5 (equivalence_class T_4 T_2 T_3)) (-. (apply T_3 T_1 T_5)) (All Y, (All Z, (((member T_1 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_1 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_1 Z))))) ### And 63 % 0.58/0.76 65. ((member T_5 (equivalence_class T_4 T_2 T_3)) <=> ((member T_5 T_2) /\ (apply T_3 T_4 T_5))) (All Y, (All Z, (((member T_1 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_1 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_1 Z))))) (-. (apply T_3 T_1 T_5)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (apply T_3 T_1 T_4) (member T_4 T_2) (member T_1 T_2) (member T_5 (equivalence_class T_4 T_2 T_3)) ### Equiv 49 64 % 0.58/0.76 66. (All X, ((member X (equivalence_class T_4 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_4 X)))) (member T_5 (equivalence_class T_4 T_2 T_3)) (member T_1 T_2) (member T_4 T_2) (apply T_3 T_1 T_4) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (-. (apply T_3 T_1 T_5)) (All Y, (All Z, (((member T_1 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_1 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_1 Z))))) ### All 65 % 0.58/0.77 67. (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (-. (apply T_3 T_1 T_5)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (apply T_3 T_1 T_4) (member T_4 T_2) (member T_1 T_2) (member T_5 (equivalence_class T_4 T_2 T_3)) (All X, ((member X (equivalence_class T_4 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_4 X)))) ### All 66 % 0.58/0.77 68. (member T_5 (equivalence_class T_4 T_2 T_3)) (member T_1 T_2) (member T_4 T_2) (apply T_3 T_1 T_4) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (-. (apply T_3 T_1 T_5)) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### All 67 % 0.58/0.77 69. (-. ((member T_5 T_2) /\ (apply T_3 T_1 T_5))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (apply T_3 T_1 T_4) (member T_4 T_2) (member T_1 T_2) (member T_5 (equivalence_class T_4 T_2 T_3)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) ### NotAnd 48 68 % 0.58/0.77 70. (-. (member T_5 (equivalence_class T_1 T_2 T_3))) (member T_5 (equivalence_class T_1 T_2 T_3)) ### Axiom % 0.58/0.77 71. ((member T_5 (equivalence_class T_1 T_2 T_3)) <=> ((member T_5 T_2) /\ (apply T_3 T_1 T_5))) (-. (member T_5 (equivalence_class T_1 T_2 T_3))) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (member T_5 (equivalence_class T_4 T_2 T_3)) (member T_1 T_2) (member T_4 T_2) (apply T_3 T_1 T_4) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### Equiv 69 70 % 0.58/0.77 72. (All X, ((member X (equivalence_class T_1 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_1 X)))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (apply T_3 T_1 T_4) (member T_4 T_2) (member T_1 T_2) (member T_5 (equivalence_class T_4 T_2 T_3)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (-. (member T_5 (equivalence_class T_1 T_2 T_3))) ### All 71 % 0.58/0.77 73. (-. (member T_5 (equivalence_class T_1 T_2 T_3))) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (member T_5 (equivalence_class T_4 T_2 T_3)) (member T_1 T_2) (member T_4 T_2) (apply T_3 T_1 T_4) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### All 72 % 0.58/0.77 74. (All E, (All A, (All X, ((member X (equivalence_class A E T_3)) <=> ((member X E) /\ (apply T_3 A X)))))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (apply T_3 T_1 T_4) (member T_4 T_2) (member T_1 T_2) (member T_5 (equivalence_class T_4 T_2 T_3)) (-. (member T_5 (equivalence_class T_1 T_2 T_3))) ### All 73 % 0.58/0.77 75. (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (-. (member T_5 (equivalence_class T_1 T_2 T_3))) (member T_5 (equivalence_class T_4 T_2 T_3)) (member T_1 T_2) (member T_4 T_2) (apply T_3 T_1 T_4) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### All 74 % 0.58/0.77 76. (-. ((member T_5 (equivalence_class T_4 T_2 T_3)) => (member T_5 (equivalence_class T_1 T_2 T_3)))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (apply T_3 T_1 T_4) (member T_4 T_2) (member T_1 T_2) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) ### NotImply 75 % 0.58/0.77 77. (-. (All X, ((member X (equivalence_class T_4 T_2 T_3)) => (member X (equivalence_class T_1 T_2 T_3))))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (member T_1 T_2) (member T_4 T_2) (apply T_3 T_1 T_4) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### NotAllEx 76 % 0.58/0.77 78. (-. (subset (equivalence_class T_4 T_2 T_3) (equivalence_class T_1 T_2 T_3))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (apply T_3 T_1 T_4) (member T_4 T_2) (member T_1 T_2) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) ### Definition-Pseudo(subset) 77 % 0.58/0.77 79. (-. ((subset (equivalence_class T_1 T_2 T_3) (equivalence_class T_4 T_2 T_3)) /\ (subset (equivalence_class T_4 T_2 T_3) (equivalence_class T_1 T_2 T_3)))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_4 T_2) (member T_1 T_2) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (apply T_3 T_1 T_4) ### NotAnd 42 78 % 0.58/0.77 80. (-. (equal_set (equivalence_class T_1 T_2 T_3) (equivalence_class T_4 T_2 T_3))) (apply T_3 T_1 T_4) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (member T_1 T_2) (member T_4 T_2) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) ### Definition-Pseudo(equal_set) 79 % 0.58/0.77 81. (member T_4 T_2) (-. (member T_4 T_2)) ### Axiom % 0.58/0.77 82. (member T_4 T_2) (-. (member T_4 T_2)) ### Axiom % 0.58/0.77 83. (apply T_3 T_4 T_4) (-. (apply T_3 T_4 T_4)) ### Axiom % 0.58/0.77 84. (-. ((member T_4 T_2) /\ (apply T_3 T_4 T_4))) (apply T_3 T_4 T_4) (member T_4 T_2) ### NotAnd 82 83 % 0.58/0.77 85. (-. (member T_4 (equivalence_class T_4 T_2 T_3))) (member T_4 (equivalence_class T_4 T_2 T_3)) ### Axiom % 0.58/0.77 86. ((member T_4 (equivalence_class T_4 T_2 T_3)) <=> ((member T_4 T_2) /\ (apply T_3 T_4 T_4))) (-. (member T_4 (equivalence_class T_4 T_2 T_3))) (member T_4 T_2) (apply T_3 T_4 T_4) ### Equiv 84 85 % 0.58/0.77 87. (All X, ((member X (equivalence_class T_4 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_4 X)))) (apply T_3 T_4 T_4) (member T_4 T_2) (-. (member T_4 (equivalence_class T_4 T_2 T_3))) ### All 86 % 0.58/0.77 88. (-. (member T_4 (equivalence_class T_1 T_2 T_3))) (member T_4 (equivalence_class T_1 T_2 T_3)) ### Axiom % 0.58/0.77 89. ((member T_4 (equivalence_class T_4 T_2 T_3)) => (member T_4 (equivalence_class T_1 T_2 T_3))) (-. (member T_4 (equivalence_class T_1 T_2 T_3))) (member T_4 T_2) (apply T_3 T_4 T_4) (All X, ((member X (equivalence_class T_4 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_4 X)))) ### Imply 87 88 % 0.58/0.77 90. (All X, ((member X (equivalence_class T_4 T_2 T_3)) => (member X (equivalence_class T_1 T_2 T_3)))) (All X, ((member X (equivalence_class T_4 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_4 X)))) (apply T_3 T_4 T_4) (member T_4 T_2) (-. (member T_4 (equivalence_class T_1 T_2 T_3))) ### All 89 % 0.58/0.77 91. (-. (apply T_3 T_1 T_4)) (apply T_3 T_1 T_4) ### Axiom % 0.58/0.77 92. ((member T_4 T_2) /\ (apply T_3 T_1 T_4)) (-. (apply T_3 T_1 T_4)) ### And 91 % 0.58/0.77 93. ((member T_4 (equivalence_class T_1 T_2 T_3)) <=> ((member T_4 T_2) /\ (apply T_3 T_1 T_4))) (-. (apply T_3 T_1 T_4)) (member T_4 T_2) (apply T_3 T_4 T_4) (All X, ((member X (equivalence_class T_4 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_4 X)))) (All X, ((member X (equivalence_class T_4 T_2 T_3)) => (member X (equivalence_class T_1 T_2 T_3)))) ### Equiv 90 92 % 0.58/0.79 94. (All X, ((member X (equivalence_class T_1 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_1 X)))) (All X, ((member X (equivalence_class T_4 T_2 T_3)) => (member X (equivalence_class T_1 T_2 T_3)))) (All X, ((member X (equivalence_class T_4 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_4 X)))) (apply T_3 T_4 T_4) (member T_4 T_2) (-. (apply T_3 T_1 T_4)) ### All 93 % 0.58/0.79 95. (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) (-. (apply T_3 T_1 T_4)) (member T_4 T_2) (apply T_3 T_4 T_4) (All X, ((member X (equivalence_class T_4 T_2 T_3)) => (member X (equivalence_class T_1 T_2 T_3)))) (All X, ((member X (equivalence_class T_1 T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 T_1 X)))) ### All 94 % 0.58/0.79 96. (All X, ((member X (equivalence_class T_4 T_2 T_3)) => (member X (equivalence_class T_1 T_2 T_3)))) (apply T_3 T_4 T_4) (member T_4 T_2) (-. (apply T_3 T_1 T_4)) (All A, (All X, ((member X (equivalence_class A T_2 T_3)) <=> ((member X T_2) /\ (apply T_3 A X))))) ### All 95 % 0.58/0.79 97. (All E, (All A, (All X, ((member X (equivalence_class A E T_3)) <=> ((member X E) /\ (apply T_3 A X)))))) (-. (apply T_3 T_1 T_4)) (member T_4 T_2) (apply T_3 T_4 T_4) (All X, ((member X (equivalence_class T_4 T_2 T_3)) => (member X (equivalence_class T_1 T_2 T_3)))) ### All 96 % 0.58/0.79 98. (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (All X, ((member X (equivalence_class T_4 T_2 T_3)) => (member X (equivalence_class T_1 T_2 T_3)))) (apply T_3 T_4 T_4) (member T_4 T_2) (-. (apply T_3 T_1 T_4)) ### All 97 % 0.58/0.79 99. ((member T_4 T_2) => (apply T_3 T_4 T_4)) (-. (apply T_3 T_1 T_4)) (All X, ((member X (equivalence_class T_4 T_2 T_3)) => (member X (equivalence_class T_1 T_2 T_3)))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (member T_4 T_2) ### Imply 81 98 % 0.58/0.79 100. (All X, ((member X T_2) => (apply T_3 X X))) (member T_4 T_2) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (All X, ((member X (equivalence_class T_4 T_2 T_3)) => (member X (equivalence_class T_1 T_2 T_3)))) (-. (apply T_3 T_1 T_4)) ### All 99 % 0.58/0.79 101. (subset (equivalence_class T_4 T_2 T_3) (equivalence_class T_1 T_2 T_3)) (-. (apply T_3 T_1 T_4)) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (member T_4 T_2) (All X, ((member X T_2) => (apply T_3 X X))) ### Definition-Pseudo(subset) 100 % 0.58/0.79 102. ((subset (equivalence_class T_1 T_2 T_3) (equivalence_class T_4 T_2 T_3)) /\ (subset (equivalence_class T_4 T_2 T_3) (equivalence_class T_1 T_2 T_3))) (All X, ((member X T_2) => (apply T_3 X X))) (member T_4 T_2) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (-. (apply T_3 T_1 T_4)) ### And 101 % 0.58/0.79 103. (equal_set (equivalence_class T_1 T_2 T_3) (equivalence_class T_4 T_2 T_3)) (-. (apply T_3 T_1 T_4)) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (member T_4 T_2) (All X, ((member X T_2) => (apply T_3 X X))) ### Definition-Pseudo(equal_set) 102 % 0.58/0.79 104. (-. ((equal_set (equivalence_class T_1 T_2 T_3) (equivalence_class T_4 T_2 T_3)) <=> (apply T_3 T_1 T_4))) (All X, ((member X T_2) => (apply T_3 X X))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_4 T_2) (member T_1 T_2) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) ### NotEquiv 80 103 % 0.58/0.79 105. ((All X, ((member X T_2) => (apply T_3 X X))) /\ ((All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) /\ (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))))) (member T_1 T_2) (member T_4 T_2) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (-. ((equal_set (equivalence_class T_1 T_2 T_3) (equivalence_class T_4 T_2 T_3)) <=> (apply T_3 T_1 T_4))) ### ConjTree 104 % 0.58/0.79 106. (equivalence T_3 T_2) (-. ((equal_set (equivalence_class T_1 T_2 T_3) (equivalence_class T_4 T_2 T_3)) <=> (apply T_3 T_1 T_4))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) (member T_4 T_2) (member T_1 T_2) ### Definition-Pseudo(equivalence) 105 % 0.58/0.79 107. (-. (((equivalence T_3 T_2) /\ ((member T_1 T_2) /\ (member T_4 T_2))) => ((equal_set (equivalence_class T_1 T_2 T_3) (equivalence_class T_4 T_2 T_3)) <=> (apply T_3 T_1 T_4)))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) ### ConjTree 106 % 0.58/0.79 108. (-. (All B, (((equivalence T_3 T_2) /\ ((member T_1 T_2) /\ (member B T_2))) => ((equal_set (equivalence_class T_1 T_2 T_3) (equivalence_class B T_2 T_3)) <=> (apply T_3 T_1 B))))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) ### NotAllEx 107 % 0.58/0.79 109. (-. (All A, (All B, (((equivalence T_3 T_2) /\ ((member A T_2) /\ (member B T_2))) => ((equal_set (equivalence_class A T_2 T_3) (equivalence_class B T_2 T_3)) <=> (apply T_3 A B)))))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) ### NotAllEx 108 % 0.58/0.79 110. (-. (All R, (All A, (All B, (((equivalence R T_2) /\ ((member A T_2) /\ (member B T_2))) => ((equal_set (equivalence_class A T_2 R) (equivalence_class B T_2 R)) <=> (apply R A B))))))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) ### NotAllEx 109 % 0.58/0.79 111. (-. (All E, (All R, (All A, (All B, (((equivalence R E) /\ ((member A E) /\ (member B E))) => ((equal_set (equivalence_class A E R) (equivalence_class B E R)) <=> (apply R A B)))))))) (All R, (All E, (All A, (All X, ((member X (equivalence_class A E R)) <=> ((member X E) /\ (apply R A X))))))) ### NotAllEx 110 % 0.58/0.79 % SZS output end Proof % 0.58/0.79 (* END-PROOF *) %------------------------------------------------------------------------------