%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SET773+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 : n009.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:52 EDT 2022 % Result : Theorem 0.82s 0.97s % Output : Proof 0.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET773+4 : TPTP v8.1.0. Released v2.2.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n009.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 : Sun Jul 10 16:25:52 EDT 2022 % 0.12/0.33 % CPUTime : % 0.82/0.97 % SZS status Theorem % 0.82/0.97 (* PROOF-FOUND *) % 0.82/0.97 (* BEGIN-PROOF *) % 0.82/0.97 % SZS output start Proof % 0.82/0.97 1. (member T_0 T_1) (-. (member T_0 T_1)) ### Axiom % 0.82/0.97 2. (member T_0 T_1) (-. (member T_0 T_1)) ### Axiom % 0.82/0.97 3. (member T_0 T_1) (-. (member T_0 T_1)) ### Axiom % 0.82/0.97 4. (member T_0 T_1) (-. (member T_0 T_1)) ### Axiom % 0.82/0.97 5. (-. (apply T_2 T_0 T_0)) (apply T_2 T_0 T_0) ### Axiom % 0.82/0.97 6. ((member T_0 T_1) => (apply T_2 T_0 T_0)) (-. (apply T_2 T_0 T_0)) (member T_0 T_1) ### Imply 4 5 % 0.82/0.97 7. (All X, ((member X T_1) => (apply T_2 X X))) (member T_0 T_1) (-. (apply T_2 T_0 T_0)) ### All 6 % 0.82/0.97 8. (apply T_3 T_0 T_0) (-. (apply T_3 T_0 T_0)) ### Axiom % 0.82/0.97 9. (-. ((apply T_2 T_0 T_0) /\ (apply T_3 T_0 T_0))) (apply T_3 T_0 T_0) (member T_0 T_1) (All X, ((member X T_1) => (apply T_2 X X))) ### NotAnd 7 8 % 0.82/0.97 10. (-. (apply T_4 T_0 T_0)) (apply T_4 T_0 T_0) ### Axiom % 0.82/0.97 11. ((apply T_4 T_0 T_0) <=> ((apply T_2 T_0 T_0) /\ (apply T_3 T_0 T_0))) (-. (apply T_4 T_0 T_0)) (All X, ((member X T_1) => (apply T_2 X X))) (member T_0 T_1) (apply T_3 T_0 T_0) ### Equiv 9 10 % 0.82/0.97 12. (((member T_0 T_1) /\ (member T_0 T_1)) => ((apply T_4 T_0 T_0) <=> ((apply T_2 T_0 T_0) /\ (apply T_3 T_0 T_0)))) (apply T_3 T_0 T_0) (All X, ((member X T_1) => (apply T_2 X X))) (-. (apply T_4 T_0 T_0)) (member T_0 T_1) ### DisjTree 2 3 11 % 0.82/0.97 13. (All B, (((member T_0 T_1) /\ (member B T_1)) => ((apply T_4 T_0 B) <=> ((apply T_2 T_0 B) /\ (apply T_3 T_0 B))))) (member T_0 T_1) (-. (apply T_4 T_0 T_0)) (All X, ((member X T_1) => (apply T_2 X X))) (apply T_3 T_0 T_0) ### All 12 % 0.82/0.97 14. (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_3 T_0 T_0) (All X, ((member X T_1) => (apply T_2 X X))) (-. (apply T_4 T_0 T_0)) (member T_0 T_1) ### All 13 % 0.82/0.97 15. ((member T_0 T_1) => (apply T_3 T_0 T_0)) (-. (apply T_4 T_0 T_0)) (All X, ((member X T_1) => (apply T_2 X X))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (member T_0 T_1) ### Imply 1 14 % 0.82/0.97 16. (All X, ((member X T_1) => (apply T_3 X X))) (member T_0 T_1) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, ((member X T_1) => (apply T_2 X X))) (-. (apply T_4 T_0 T_0)) ### All 15 % 0.82/0.97 17. (-. ((member T_0 T_1) => (apply T_4 T_0 T_0))) (All X, ((member X T_1) => (apply T_2 X X))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, ((member X T_1) => (apply T_3 X X))) ### NotImply 16 % 0.82/0.97 18. (-. (All X, ((member X T_1) => (apply T_4 X X)))) (All X, ((member X T_1) => (apply T_3 X X))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, ((member X T_1) => (apply T_2 X X))) ### NotAllEx 17 % 0.82/0.97 19. (member T_5 T_1) (-. (member T_5 T_1)) ### Axiom % 0.82/0.97 20. (member T_6 T_1) (-. (member T_6 T_1)) ### Axiom % 0.82/0.97 21. (member T_6 T_1) (-. (member T_6 T_1)) ### Axiom % 0.82/0.97 22. (member T_5 T_1) (-. (member T_5 T_1)) ### Axiom % 0.82/0.97 23. (member T_6 T_1) (-. (member T_6 T_1)) ### Axiom % 0.82/0.97 24. (member T_5 T_1) (-. (member T_5 T_1)) ### Axiom % 0.82/0.97 25. (apply T_4 T_6 T_5) (-. (apply T_4 T_6 T_5)) ### Axiom % 0.82/0.97 26. (-. (apply T_2 T_6 T_5)) (apply T_2 T_6 T_5) ### Axiom % 0.82/0.97 27. ((apply T_2 T_6 T_5) /\ (apply T_3 T_6 T_5)) (-. (apply T_2 T_6 T_5)) ### And 26 % 0.82/0.97 28. ((apply T_4 T_6 T_5) <=> ((apply T_2 T_6 T_5) /\ (apply T_3 T_6 T_5))) (-. (apply T_2 T_6 T_5)) (apply T_4 T_6 T_5) ### Equiv 25 27 % 0.82/0.97 29. (((member T_6 T_1) /\ (member T_5 T_1)) => ((apply T_4 T_6 T_5) <=> ((apply T_2 T_6 T_5) /\ (apply T_3 T_6 T_5)))) (apply T_4 T_6 T_5) (-. (apply T_2 T_6 T_5)) (member T_5 T_1) (member T_6 T_1) ### DisjTree 23 24 28 % 0.82/0.97 30. (All B, (((member T_6 T_1) /\ (member B T_1)) => ((apply T_4 T_6 B) <=> ((apply T_2 T_6 B) /\ (apply T_3 T_6 B))))) (member T_6 T_1) (member T_5 T_1) (-. (apply T_2 T_6 T_5)) (apply T_4 T_6 T_5) ### All 29 % 0.82/0.97 31. (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_6 T_5) (-. (apply T_2 T_6 T_5)) (member T_5 T_1) (member T_6 T_1) ### All 30 % 0.82/0.97 32. (-. (apply T_2 T_5 T_6)) (apply T_2 T_5 T_6) ### Axiom % 0.82/0.97 33. (((member T_6 T_1) /\ (member T_5 T_1)) => ((apply T_2 T_6 T_5) => (apply T_2 T_5 T_6))) (-. (apply T_2 T_5 T_6)) (apply T_4 T_6 T_5) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (member T_5 T_1) (member T_6 T_1) ### DisjTree 21 22 31 32 % 0.82/0.97 34. (All Y, (((member T_6 T_1) /\ (member Y T_1)) => ((apply T_2 T_6 Y) => (apply T_2 Y T_6)))) (member T_6 T_1) (member T_5 T_1) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_6 T_5) (-. (apply T_2 T_5 T_6)) ### All 33 % 0.82/0.97 35. (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) (-. (apply T_2 T_5 T_6)) (apply T_4 T_6 T_5) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (member T_5 T_1) (member T_6 T_1) ### All 34 % 0.82/0.97 36. (member T_6 T_1) (-. (member T_6 T_1)) ### Axiom % 0.82/0.97 37. (member T_5 T_1) (-. (member T_5 T_1)) ### Axiom % 0.82/0.97 38. (member T_6 T_1) (-. (member T_6 T_1)) ### Axiom % 0.82/0.97 39. (member T_5 T_1) (-. (member T_5 T_1)) ### Axiom % 0.82/0.97 40. (apply T_4 T_6 T_5) (-. (apply T_4 T_6 T_5)) ### Axiom % 0.82/0.97 41. (-. (apply T_3 T_6 T_5)) (apply T_3 T_6 T_5) ### Axiom % 0.82/0.97 42. ((apply T_2 T_6 T_5) /\ (apply T_3 T_6 T_5)) (-. (apply T_3 T_6 T_5)) ### And 41 % 0.82/0.97 43. ((apply T_4 T_6 T_5) <=> ((apply T_2 T_6 T_5) /\ (apply T_3 T_6 T_5))) (-. (apply T_3 T_6 T_5)) (apply T_4 T_6 T_5) ### Equiv 40 42 % 0.82/0.97 44. (((member T_6 T_1) /\ (member T_5 T_1)) => ((apply T_4 T_6 T_5) <=> ((apply T_2 T_6 T_5) /\ (apply T_3 T_6 T_5)))) (apply T_4 T_6 T_5) (-. (apply T_3 T_6 T_5)) (member T_5 T_1) (member T_6 T_1) ### DisjTree 38 39 43 % 0.82/0.97 45. (All B, (((member T_6 T_1) /\ (member B T_1)) => ((apply T_4 T_6 B) <=> ((apply T_2 T_6 B) /\ (apply T_3 T_6 B))))) (member T_6 T_1) (member T_5 T_1) (-. (apply T_3 T_6 T_5)) (apply T_4 T_6 T_5) ### All 44 % 0.82/0.97 46. (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_6 T_5) (-. (apply T_3 T_6 T_5)) (member T_5 T_1) (member T_6 T_1) ### All 45 % 0.82/0.97 47. (-. (apply T_3 T_5 T_6)) (apply T_3 T_5 T_6) ### Axiom % 0.82/0.97 48. (((member T_6 T_1) /\ (member T_5 T_1)) => ((apply T_3 T_6 T_5) => (apply T_3 T_5 T_6))) (-. (apply T_3 T_5 T_6)) (apply T_4 T_6 T_5) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (member T_5 T_1) (member T_6 T_1) ### DisjTree 36 37 46 47 % 0.82/0.97 49. (All Y, (((member T_6 T_1) /\ (member Y T_1)) => ((apply T_3 T_6 Y) => (apply T_3 Y T_6)))) (member T_6 T_1) (member T_5 T_1) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_6 T_5) (-. (apply T_3 T_5 T_6)) ### All 48 % 0.82/0.97 50. (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (-. (apply T_3 T_5 T_6)) (apply T_4 T_6 T_5) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (member T_5 T_1) (member T_6 T_1) ### All 49 % 0.82/0.97 51. (-. ((apply T_2 T_5 T_6) /\ (apply T_3 T_5 T_6))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (member T_6 T_1) (member T_5 T_1) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_6 T_5) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) ### NotAnd 35 50 % 0.82/0.97 52. (-. (apply T_4 T_5 T_6)) (apply T_4 T_5 T_6) ### Axiom % 0.82/0.97 53. ((apply T_4 T_5 T_6) <=> ((apply T_2 T_5 T_6) /\ (apply T_3 T_5 T_6))) (-. (apply T_4 T_5 T_6)) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) (apply T_4 T_6 T_5) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (member T_5 T_1) (member T_6 T_1) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) ### Equiv 51 52 % 0.82/0.99 54. (((member T_5 T_1) /\ (member T_6 T_1)) => ((apply T_4 T_5 T_6) <=> ((apply T_2 T_5 T_6) /\ (apply T_3 T_5 T_6)))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_6 T_5) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) (-. (apply T_4 T_5 T_6)) (member T_6 T_1) (member T_5 T_1) ### DisjTree 19 20 53 % 0.82/0.99 55. (All B, (((member T_5 T_1) /\ (member B T_1)) => ((apply T_4 T_5 B) <=> ((apply T_2 T_5 B) /\ (apply T_3 T_5 B))))) (member T_5 T_1) (member T_6 T_1) (-. (apply T_4 T_5 T_6)) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) (apply T_4 T_6 T_5) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) ### All 54 % 0.82/0.99 56. (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_6 T_5) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) (-. (apply T_4 T_5 T_6)) (member T_6 T_1) (member T_5 T_1) ### All 55 % 0.82/0.99 57. (-. (((member T_6 T_1) /\ (member T_5 T_1)) => ((apply T_4 T_6 T_5) => (apply T_4 T_5 T_6)))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) ### ConjTree 56 % 0.82/0.99 58. (-. (All Y, (((member T_6 T_1) /\ (member Y T_1)) => ((apply T_4 T_6 Y) => (apply T_4 Y T_6))))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) ### NotAllEx 57 % 0.82/0.99 59. (-. (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_4 X Y) => (apply T_4 Y X)))))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) ### NotAllEx 58 % 0.82/0.99 60. (member T_7 T_1) (-. (member T_7 T_1)) ### Axiom % 0.82/0.99 61. (member T_8 T_1) (-. (member T_8 T_1)) ### Axiom % 0.82/0.99 62. (member T_7 T_1) (-. (member T_7 T_1)) ### Axiom % 0.82/0.99 63. (member T_9 T_1) (-. (member T_9 T_1)) ### Axiom % 0.82/0.99 64. (member T_8 T_1) (-. (member T_8 T_1)) ### Axiom % 0.82/0.99 65. (member T_7 T_1) (-. (member T_7 T_1)) ### Axiom % 0.82/0.99 66. (member T_9 T_1) (-. (member T_9 T_1)) ### Axiom % 0.82/0.99 67. (apply T_4 T_7 T_9) (-. (apply T_4 T_7 T_9)) ### Axiom % 0.82/0.99 68. (-. (apply T_2 T_7 T_9)) (apply T_2 T_7 T_9) ### Axiom % 0.82/0.99 69. ((apply T_2 T_7 T_9) /\ (apply T_3 T_7 T_9)) (-. (apply T_2 T_7 T_9)) ### And 68 % 0.82/0.99 70. ((apply T_4 T_7 T_9) <=> ((apply T_2 T_7 T_9) /\ (apply T_3 T_7 T_9))) (-. (apply T_2 T_7 T_9)) (apply T_4 T_7 T_9) ### Equiv 67 69 % 0.82/0.99 71. (((member T_7 T_1) /\ (member T_9 T_1)) => ((apply T_4 T_7 T_9) <=> ((apply T_2 T_7 T_9) /\ (apply T_3 T_7 T_9)))) (apply T_4 T_7 T_9) (-. (apply T_2 T_7 T_9)) (member T_9 T_1) (member T_7 T_1) ### DisjTree 65 66 70 % 0.82/0.99 72. (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (member T_7 T_1) (member T_9 T_1) (-. (apply T_2 T_7 T_9)) (apply T_4 T_7 T_9) ### All 71 % 0.82/0.99 73. (member T_9 T_1) (-. (member T_9 T_1)) ### Axiom % 0.82/0.99 74. (member T_8 T_1) (-. (member T_8 T_1)) ### Axiom % 0.82/0.99 75. (apply T_4 T_9 T_8) (-. (apply T_4 T_9 T_8)) ### Axiom % 0.82/0.99 76. (-. (apply T_2 T_9 T_8)) (apply T_2 T_9 T_8) ### Axiom % 0.82/0.99 77. ((apply T_2 T_9 T_8) /\ (apply T_3 T_9 T_8)) (-. (apply T_2 T_9 T_8)) ### And 76 % 0.82/0.99 78. ((apply T_4 T_9 T_8) <=> ((apply T_2 T_9 T_8) /\ (apply T_3 T_9 T_8))) (-. (apply T_2 T_9 T_8)) (apply T_4 T_9 T_8) ### Equiv 75 77 % 0.82/0.99 79. (((member T_9 T_1) /\ (member T_8 T_1)) => ((apply T_4 T_9 T_8) <=> ((apply T_2 T_9 T_8) /\ (apply T_3 T_9 T_8)))) (apply T_4 T_9 T_8) (-. (apply T_2 T_9 T_8)) (member T_8 T_1) (member T_9 T_1) ### DisjTree 73 74 78 % 0.82/0.99 80. (All B, (((member T_9 T_1) /\ (member B T_1)) => ((apply T_4 T_9 B) <=> ((apply T_2 T_9 B) /\ (apply T_3 T_9 B))))) (member T_9 T_1) (member T_8 T_1) (-. (apply T_2 T_9 T_8)) (apply T_4 T_9 T_8) ### All 79 % 0.82/0.99 81. (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_9 T_8) (-. (apply T_2 T_9 T_8)) (member T_8 T_1) (member T_9 T_1) ### All 80 % 0.82/0.99 82. (-. (apply T_2 T_7 T_8)) (apply T_2 T_7 T_8) ### Axiom % 0.82/0.99 83. (((member T_7 T_1) /\ ((member T_9 T_1) /\ (member T_8 T_1))) => (((apply T_2 T_7 T_9) /\ (apply T_2 T_9 T_8)) => (apply T_2 T_7 T_8))) (-. (apply T_2 T_7 T_8)) (apply T_4 T_9 T_8) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_7 T_9) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (member T_8 T_1) (member T_9 T_1) (member T_7 T_1) ### DisjTree 62 63 64 72 81 82 % 0.82/0.99 84. (All Z, (((member T_7 T_1) /\ ((member T_9 T_1) /\ (member Z T_1))) => (((apply T_2 T_7 T_9) /\ (apply T_2 T_9 Z)) => (apply T_2 T_7 Z)))) (member T_7 T_1) (member T_9 T_1) (member T_8 T_1) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (apply T_4 T_7 T_9) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_9 T_8) (-. (apply T_2 T_7 T_8)) ### All 83 % 0.82/0.99 85. (All Y, (All Z, (((member T_7 T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 T_7 Y) /\ (apply T_2 Y Z)) => (apply T_2 T_7 Z))))) (-. (apply T_2 T_7 T_8)) (apply T_4 T_9 T_8) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_7 T_9) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (member T_8 T_1) (member T_9 T_1) (member T_7 T_1) ### All 84 % 0.82/0.99 86. (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) (member T_7 T_1) (member T_9 T_1) (member T_8 T_1) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (apply T_4 T_7 T_9) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_9 T_8) (-. (apply T_2 T_7 T_8)) ### All 85 % 0.82/0.99 87. (member T_7 T_1) (-. (member T_7 T_1)) ### Axiom % 0.82/0.99 88. (member T_9 T_1) (-. (member T_9 T_1)) ### Axiom % 0.82/0.99 89. (member T_8 T_1) (-. (member T_8 T_1)) ### Axiom % 0.82/0.99 90. (member T_7 T_1) (-. (member T_7 T_1)) ### Axiom % 0.82/0.99 91. (member T_9 T_1) (-. (member T_9 T_1)) ### Axiom % 0.82/0.99 92. (apply T_4 T_7 T_9) (-. (apply T_4 T_7 T_9)) ### Axiom % 0.82/0.99 93. (-. (apply T_3 T_7 T_9)) (apply T_3 T_7 T_9) ### Axiom % 0.82/0.99 94. ((apply T_2 T_7 T_9) /\ (apply T_3 T_7 T_9)) (-. (apply T_3 T_7 T_9)) ### And 93 % 0.82/0.99 95. ((apply T_4 T_7 T_9) <=> ((apply T_2 T_7 T_9) /\ (apply T_3 T_7 T_9))) (-. (apply T_3 T_7 T_9)) (apply T_4 T_7 T_9) ### Equiv 92 94 % 0.82/0.99 96. (((member T_7 T_1) /\ (member T_9 T_1)) => ((apply T_4 T_7 T_9) <=> ((apply T_2 T_7 T_9) /\ (apply T_3 T_7 T_9)))) (apply T_4 T_7 T_9) (-. (apply T_3 T_7 T_9)) (member T_9 T_1) (member T_7 T_1) ### DisjTree 90 91 95 % 0.82/0.99 97. (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (member T_7 T_1) (member T_9 T_1) (-. (apply T_3 T_7 T_9)) (apply T_4 T_7 T_9) ### All 96 % 0.82/1.01 98. (member T_9 T_1) (-. (member T_9 T_1)) ### Axiom % 0.82/1.01 99. (member T_8 T_1) (-. (member T_8 T_1)) ### Axiom % 0.82/1.01 100. (apply T_4 T_9 T_8) (-. (apply T_4 T_9 T_8)) ### Axiom % 0.82/1.01 101. (-. (apply T_3 T_9 T_8)) (apply T_3 T_9 T_8) ### Axiom % 0.82/1.01 102. ((apply T_2 T_9 T_8) /\ (apply T_3 T_9 T_8)) (-. (apply T_3 T_9 T_8)) ### And 101 % 0.82/1.01 103. ((apply T_4 T_9 T_8) <=> ((apply T_2 T_9 T_8) /\ (apply T_3 T_9 T_8))) (-. (apply T_3 T_9 T_8)) (apply T_4 T_9 T_8) ### Equiv 100 102 % 0.82/1.01 104. (((member T_9 T_1) /\ (member T_8 T_1)) => ((apply T_4 T_9 T_8) <=> ((apply T_2 T_9 T_8) /\ (apply T_3 T_9 T_8)))) (apply T_4 T_9 T_8) (-. (apply T_3 T_9 T_8)) (member T_8 T_1) (member T_9 T_1) ### DisjTree 98 99 103 % 0.82/1.01 105. (All B, (((member T_9 T_1) /\ (member B T_1)) => ((apply T_4 T_9 B) <=> ((apply T_2 T_9 B) /\ (apply T_3 T_9 B))))) (member T_9 T_1) (member T_8 T_1) (-. (apply T_3 T_9 T_8)) (apply T_4 T_9 T_8) ### All 104 % 0.82/1.01 106. (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_9 T_8) (-. (apply T_3 T_9 T_8)) (member T_8 T_1) (member T_9 T_1) ### All 105 % 0.82/1.01 107. (-. (apply T_3 T_7 T_8)) (apply T_3 T_7 T_8) ### Axiom % 0.82/1.01 108. (((member T_7 T_1) /\ ((member T_9 T_1) /\ (member T_8 T_1))) => (((apply T_3 T_7 T_9) /\ (apply T_3 T_9 T_8)) => (apply T_3 T_7 T_8))) (-. (apply T_3 T_7 T_8)) (apply T_4 T_9 T_8) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_7 T_9) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (member T_8 T_1) (member T_9 T_1) (member T_7 T_1) ### DisjTree 87 88 89 97 106 107 % 0.82/1.01 109. (All Z, (((member T_7 T_1) /\ ((member T_9 T_1) /\ (member Z T_1))) => (((apply T_3 T_7 T_9) /\ (apply T_3 T_9 Z)) => (apply T_3 T_7 Z)))) (member T_7 T_1) (member T_9 T_1) (member T_8 T_1) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (apply T_4 T_7 T_9) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_9 T_8) (-. (apply T_3 T_7 T_8)) ### All 108 % 0.82/1.01 110. (All Y, (All Z, (((member T_7 T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 T_7 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_7 Z))))) (-. (apply T_3 T_7 T_8)) (apply T_4 T_9 T_8) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_7 T_9) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (member T_8 T_1) (member T_9 T_1) (member T_7 T_1) ### All 109 % 0.82/1.01 111. (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_7 T_1) (member T_9 T_1) (member T_8 T_1) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (apply T_4 T_7 T_9) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_9 T_8) (-. (apply T_3 T_7 T_8)) ### All 110 % 0.82/1.01 112. (-. ((apply T_2 T_7 T_8) /\ (apply T_3 T_7 T_8))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (apply T_4 T_9 T_8) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_7 T_9) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (member T_8 T_1) (member T_9 T_1) (member T_7 T_1) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) ### NotAnd 86 111 % 0.82/1.01 113. (-. (apply T_4 T_7 T_8)) (apply T_4 T_7 T_8) ### Axiom % 0.82/1.01 114. ((apply T_4 T_7 T_8) <=> ((apply T_2 T_7 T_8) /\ (apply T_3 T_7 T_8))) (-. (apply T_4 T_7 T_8)) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) (member T_7 T_1) (member T_9 T_1) (member T_8 T_1) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (apply T_4 T_7 T_9) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_9 T_8) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### Equiv 112 113 % 0.82/1.01 115. (((member T_7 T_1) /\ (member T_8 T_1)) => ((apply T_4 T_7 T_8) <=> ((apply T_2 T_7 T_8) /\ (apply T_3 T_7 T_8)))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (apply T_4 T_9 T_8) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_7 T_9) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (member T_9 T_1) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) (-. (apply T_4 T_7 T_8)) (member T_8 T_1) (member T_7 T_1) ### DisjTree 60 61 114 % 0.82/1.01 116. (member T_7 T_1) (member T_8 T_1) (-. (apply T_4 T_7 T_8)) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) (member T_9 T_1) (All B, (((member T_7 T_1) /\ (member B T_1)) => ((apply T_4 T_7 B) <=> ((apply T_2 T_7 B) /\ (apply T_3 T_7 B))))) (apply T_4 T_7 T_9) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_9 T_8) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### All 115 % 0.82/1.01 117. (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (apply T_4 T_9 T_8) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (apply T_4 T_7 T_9) (member T_9 T_1) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) (-. (apply T_4 T_7 T_8)) (member T_8 T_1) (member T_7 T_1) ### All 116 % 0.82/1.01 118. (-. (((member T_7 T_1) /\ ((member T_9 T_1) /\ (member T_8 T_1))) => (((apply T_4 T_7 T_9) /\ (apply T_4 T_9 T_8)) => (apply T_4 T_7 T_8)))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### ConjTree 117 % 0.82/1.01 119. (-. (All Z, (((member T_7 T_1) /\ ((member T_9 T_1) /\ (member Z T_1))) => (((apply T_4 T_7 T_9) /\ (apply T_4 T_9 Z)) => (apply T_4 T_7 Z))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) ### NotAllEx 118 % 0.82/1.01 120. (-. (All Y, (All Z, (((member T_7 T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_4 T_7 Y) /\ (apply T_4 Y Z)) => (apply T_4 T_7 Z)))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### NotAllEx 119 % 0.82/1.01 121. (-. (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_4 X Y) /\ (apply T_4 Y Z)) => (apply T_4 X Z))))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) ### NotAllEx 120 % 0.82/1.01 122. (-. ((All X, ((member X T_1) => (apply T_4 X X))) /\ ((All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_4 X Y) => (apply T_4 Y X))))) /\ (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_4 X Y) /\ (apply T_4 Y Z)) => (apply T_4 X Z))))))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) (All X, ((member X T_1) => (apply T_2 X X))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, ((member X T_1) => (apply T_3 X X))) ### DisjTree 18 59 121 % 0.82/1.01 123. (-. (equivalence T_4 T_1)) (All X, ((member X T_1) => (apply T_3 X X))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, ((member X T_1) => (apply T_2 X X))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) ### Definition-Pseudo(equivalence) 122 % 0.82/1.01 124. ((All X, ((member X T_1) => (apply T_3 X X))) /\ ((All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) /\ (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) (All X, ((member X T_1) => (apply T_2 X X))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (-. (equivalence T_4 T_1)) ### ConjTree 123 % 0.82/1.01 125. (equivalence T_3 T_1) (-. (equivalence T_4 T_1)) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (All X, ((member X T_1) => (apply T_2 X X))) (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))) ### Definition-Pseudo(equivalence) 124 % 0.82/1.01 126. ((All X, ((member X T_1) => (apply T_2 X X))) /\ ((All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_2 X Y) => (apply T_2 Y X))))) /\ (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_2 X Y) /\ (apply T_2 Y Z)) => (apply T_2 X Z)))))))) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) (-. (equivalence T_4 T_1)) (equivalence T_3 T_1) ### ConjTree 125 % 0.82/1.01 127. (equivalence T_2 T_1) (equivalence T_3 T_1) (-. (equivalence T_4 T_1)) (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))) ### Definition-Pseudo(equivalence) 126 % 0.82/1.01 128. (-. (((equivalence T_2 T_1) /\ ((equivalence T_3 T_1) /\ (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply T_4 A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))))) => (equivalence T_4 T_1))) ### ConjTree 127 % 0.82/1.01 129. (-. (All R, (((equivalence T_2 T_1) /\ ((equivalence T_3 T_1) /\ (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply R A B) <=> ((apply T_2 A B) /\ (apply T_3 A B)))))))) => (equivalence R T_1)))) ### NotAllEx 128 % 0.82/1.01 130. (-. (All R2, (All R, (((equivalence T_2 T_1) /\ ((equivalence R2 T_1) /\ (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply R A B) <=> ((apply T_2 A B) /\ (apply R2 A B)))))))) => (equivalence R T_1))))) ### NotAllEx 129 % 0.82/1.01 131. (-. (All R1, (All R2, (All R, (((equivalence R1 T_1) /\ ((equivalence R2 T_1) /\ (All A, (All B, (((member A T_1) /\ (member B T_1)) => ((apply R A B) <=> ((apply R1 A B) /\ (apply R2 A B)))))))) => (equivalence R T_1)))))) ### NotAllEx 130 % 0.82/1.01 132. (-. (All E, (All R1, (All R2, (All R, (((equivalence R1 E) /\ ((equivalence R2 E) /\ (All A, (All B, (((member A E) /\ (member B E)) => ((apply R A B) <=> ((apply R1 A B) /\ (apply R2 A B)))))))) => (equivalence R E))))))) ### NotAllEx 131 % 0.82/1.01 % SZS output end Proof % 0.82/1.01 (* END-PROOF *) %------------------------------------------------------------------------------