%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SET774+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 : n015.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:53 EDT 2022 % Result : Theorem 0.51s 0.72s % Output : Proof 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SET774+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 : n015.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 10:51:38 EDT 2022 % 0.12/0.33 % CPUTime : % 0.51/0.72 % SZS status Theorem % 0.51/0.72 (* PROOF-FOUND *) % 0.51/0.72 (* BEGIN-PROOF *) % 0.51/0.72 % SZS output start Proof % 0.51/0.72 1. (member T_0 T_1) (-. (member T_0 T_1)) ### Axiom % 0.51/0.72 2. (-. (member T_0 T_2)) (member T_0 T_2) ### Axiom % 0.51/0.72 3. ((member T_0 T_1) => (member T_0 T_2)) (-. (member T_0 T_2)) (member T_0 T_1) ### Imply 1 2 % 0.51/0.72 4. (All X, ((member X T_1) => (member X T_2))) (member T_0 T_1) (-. (member T_0 T_2)) ### All 3 % 0.51/0.72 5. (-. (apply T_3 T_0 T_0)) (apply T_3 T_0 T_0) ### Axiom % 0.51/0.72 6. ((member T_0 T_2) => (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) => (member X T_2))) ### Imply 4 5 % 0.51/0.72 7. (All X, ((member X T_2) => (apply T_3 X X))) (All X, ((member X T_1) => (member X T_2))) (member T_0 T_1) (-. (apply T_3 T_0 T_0)) ### All 6 % 0.51/0.72 8. (-. ((member T_0 T_1) => (apply T_3 T_0 T_0))) (All X, ((member X T_1) => (member X T_2))) (All X, ((member X T_2) => (apply T_3 X X))) ### NotImply 7 % 0.51/0.72 9. (-. (All X, ((member X T_1) => (apply T_3 X X)))) (All X, ((member X T_2) => (apply T_3 X X))) (All X, ((member X T_1) => (member X T_2))) ### NotAllEx 8 % 0.51/0.72 10. (member T_4 T_1) (-. (member T_4 T_1)) ### Axiom % 0.51/0.72 11. (member T_5 T_1) (-. (member T_5 T_1)) ### Axiom % 0.51/0.72 12. (-. (member T_5 T_2)) (member T_5 T_2) ### Axiom % 0.51/0.72 13. ((member T_5 T_1) => (member T_5 T_2)) (-. (member T_5 T_2)) (member T_5 T_1) ### Imply 11 12 % 0.51/0.72 14. (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (-. (member T_5 T_2)) ### All 13 % 0.51/0.72 15. (member T_6 T_1) (-. (member T_6 T_1)) ### Axiom % 0.51/0.72 16. (member T_5 T_2) (-. (member T_5 T_2)) ### Axiom % 0.51/0.72 17. (member T_4 T_2) (-. (member T_4 T_2)) ### Axiom % 0.51/0.72 18. (member T_6 T_2) (-. (member T_6 T_2)) ### Axiom % 0.51/0.72 19. (apply T_3 T_5 T_4) (-. (apply T_3 T_5 T_4)) ### Axiom % 0.51/0.72 20. (apply T_3 T_4 T_6) (-. (apply T_3 T_4 T_6)) ### Axiom % 0.51/0.72 21. (-. (apply T_3 T_5 T_6)) (apply T_3 T_5 T_6) ### Axiom % 0.51/0.72 22. (((member T_5 T_2) /\ ((member T_4 T_2) /\ (member T_6 T_2))) => (((apply T_3 T_5 T_4) /\ (apply T_3 T_4 T_6)) => (apply T_3 T_5 T_6))) (-. (apply T_3 T_5 T_6)) (apply T_3 T_4 T_6) (apply T_3 T_5 T_4) (member T_6 T_2) (member T_4 T_2) (member T_5 T_2) ### DisjTree 16 17 18 19 20 21 % 0.51/0.72 23. (All Z, (((member T_5 T_2) /\ ((member T_4 T_2) /\ (member Z T_2))) => (((apply T_3 T_5 T_4) /\ (apply T_3 T_4 Z)) => (apply T_3 T_5 Z)))) (member T_5 T_2) (member T_4 T_2) (member T_6 T_2) (apply T_3 T_5 T_4) (apply T_3 T_4 T_6) (-. (apply T_3 T_5 T_6)) ### All 22 % 0.51/0.72 24. (All Y, (All Z, (((member T_5 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z))))) (-. (apply T_3 T_5 T_6)) (apply T_3 T_4 T_6) (apply T_3 T_5 T_4) (member T_6 T_2) (member T_4 T_2) (member T_5 T_2) ### All 23 % 0.51/0.72 25. (-. (-. (member T_6 T_2))) (member T_5 T_2) (member T_4 T_2) (apply T_3 T_5 T_4) (apply T_3 T_4 T_6) (-. (apply T_3 T_5 T_6)) (All Y, (All Z, (((member T_5 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z))))) ### NotNot 24 % 0.51/0.72 26. (-. ((member T_6 T_1) /\ (-. (member T_6 T_2)))) (All Y, (All Z, (((member T_5 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z))))) (-. (apply T_3 T_5 T_6)) (apply T_3 T_4 T_6) (apply T_3 T_5 T_4) (member T_4 T_2) (member T_5 T_2) (member T_6 T_1) ### NotAnd 15 25 % 0.51/0.72 27. (member T_6 T_1) (-. (member T_6 T_1)) ### Axiom % 0.51/0.72 28. (-. (member T_6 T_2)) (member T_6 T_2) ### Axiom % 0.51/0.72 29. ((member T_6 T_1) => (member T_6 T_2)) (-. (member T_6 T_2)) (member T_6 T_1) ### Imply 27 28 % 0.51/0.72 30. (All X, ((member X T_1) => (member X T_2))) (member T_6 T_1) (-. (member T_6 T_2)) ### All 29 % 0.51/0.72 31. ((member T_6 T_1) /\ (-. (member T_6 T_2))) (member T_6 T_1) (All X, ((member X T_1) => (member X T_2))) ### And 30 % 0.51/0.72 32. ((member T_6 (difference T_1 T_2)) <=> ((member T_6 T_1) /\ (-. (member T_6 T_2)))) (All X, ((member X T_1) => (member X T_2))) (member T_6 T_1) (member T_5 T_2) (member T_4 T_2) (apply T_3 T_5 T_4) (apply T_3 T_4 T_6) (-. (apply T_3 T_5 T_6)) (All Y, (All Z, (((member T_5 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z))))) ### Equiv 26 31 % 0.51/0.72 33. (All E, ((member T_6 (difference E T_2)) <=> ((member T_6 E) /\ (-. (member T_6 T_2))))) (All Y, (All Z, (((member T_5 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z))))) (-. (apply T_3 T_5 T_6)) (apply T_3 T_4 T_6) (apply T_3 T_5 T_4) (member T_4 T_2) (member T_5 T_2) (member T_6 T_1) (All X, ((member X T_1) => (member X T_2))) ### All 32 % 0.51/0.72 34. (All A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) (All X, ((member X T_1) => (member X T_2))) (member T_6 T_1) (member T_5 T_2) (member T_4 T_2) (apply T_3 T_5 T_4) (apply T_3 T_4 T_6) (-. (apply T_3 T_5 T_6)) (All Y, (All Z, (((member T_5 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z))))) ### All 33 % 0.51/0.72 35. (-. (-. (member T_5 T_2))) (All Y, (All Z, (((member T_5 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z))))) (-. (apply T_3 T_5 T_6)) (apply T_3 T_4 T_6) (apply T_3 T_5 T_4) (member T_4 T_2) (member T_6 T_1) (All X, ((member X T_1) => (member X T_2))) (All A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) ### NotNot 34 % 0.51/0.72 36. (-. ((member T_5 T_2) /\ (-. (member T_5 T_2)))) (All A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) (member T_6 T_1) (member T_4 T_2) (apply T_3 T_5 T_4) (apply T_3 T_4 T_6) (-. (apply T_3 T_5 T_6)) (All Y, (All Z, (((member T_5 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z))))) (member T_5 T_1) (All X, ((member X T_1) => (member X T_2))) ### NotAnd 14 35 % 0.51/0.72 37. (-. (member T_5 T_2)) (member T_5 T_2) ### Axiom % 0.51/0.72 38. ((member T_5 T_2) /\ (-. (member T_5 T_2))) ### And 37 % 0.51/0.72 39. ((member T_5 (difference T_2 T_2)) <=> ((member T_5 T_2) /\ (-. (member T_5 T_2)))) (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (All Y, (All Z, (((member T_5 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z))))) (-. (apply T_3 T_5 T_6)) (apply T_3 T_4 T_6) (apply T_3 T_5 T_4) (member T_4 T_2) (member T_6 T_1) (All A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) ### Equiv 36 38 % 0.51/0.72 40. (All E, ((member T_5 (difference E T_2)) <=> ((member T_5 E) /\ (-. (member T_5 T_2))))) (All A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) (member T_6 T_1) (member T_4 T_2) (apply T_3 T_5 T_4) (apply T_3 T_4 T_6) (-. (apply T_3 T_5 T_6)) (All Y, (All Z, (((member T_5 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z))))) (member T_5 T_1) (All X, ((member X T_1) => (member X T_2))) ### All 39 % 0.51/0.72 41. (All A, (All E, ((member T_5 (difference E A)) <=> ((member T_5 E) /\ (-. (member T_5 A)))))) (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (All Y, (All Z, (((member T_5 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z))))) (-. (apply T_3 T_5 T_6)) (apply T_3 T_4 T_6) (apply T_3 T_5 T_4) (member T_4 T_2) (member T_6 T_1) (All A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) ### All 40 % 0.51/0.72 42. (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 A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) (member T_6 T_1) (member T_4 T_2) (apply T_3 T_5 T_4) (apply T_3 T_4 T_6) (-. (apply T_3 T_5 T_6)) (member T_5 T_1) (All X, ((member X T_1) => (member X T_2))) (All A, (All E, ((member T_5 (difference E A)) <=> ((member T_5 E) /\ (-. (member T_5 A)))))) ### All 41 % 0.51/0.72 43. (-. (-. (member T_4 T_2))) (All A, (All E, ((member T_5 (difference E A)) <=> ((member T_5 E) /\ (-. (member T_5 A)))))) (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (-. (apply T_3 T_5 T_6)) (apply T_3 T_4 T_6) (apply T_3 T_5 T_4) (member T_6 T_1) (All A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) (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)))))) ### NotNot 42 % 0.57/0.74 44. (-. ((member T_4 T_1) /\ (-. (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 A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) (member T_6 T_1) (apply T_3 T_5 T_4) (apply T_3 T_4 T_6) (-. (apply T_3 T_5 T_6)) (member T_5 T_1) (All X, ((member X T_1) => (member X T_2))) (All A, (All E, ((member T_5 (difference E A)) <=> ((member T_5 E) /\ (-. (member T_5 A)))))) (member T_4 T_1) ### NotAnd 10 43 % 0.57/0.74 45. (member T_4 T_1) (-. (member T_4 T_1)) ### Axiom % 0.57/0.74 46. (-. (member T_4 T_2)) (member T_4 T_2) ### Axiom % 0.57/0.74 47. ((member T_4 T_1) => (member T_4 T_2)) (-. (member T_4 T_2)) (member T_4 T_1) ### Imply 45 46 % 0.57/0.74 48. (All X, ((member X T_1) => (member X T_2))) (member T_4 T_1) (-. (member T_4 T_2)) ### All 47 % 0.57/0.74 49. ((member T_4 T_1) /\ (-. (member T_4 T_2))) (member T_4 T_1) (All X, ((member X T_1) => (member X T_2))) ### And 48 % 0.57/0.74 50. ((member T_4 (difference T_1 T_2)) <=> ((member T_4 T_1) /\ (-. (member T_4 T_2)))) (member T_4 T_1) (All A, (All E, ((member T_5 (difference E A)) <=> ((member T_5 E) /\ (-. (member T_5 A)))))) (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (-. (apply T_3 T_5 T_6)) (apply T_3 T_4 T_6) (apply T_3 T_5 T_4) (member T_6 T_1) (All A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) (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 44 49 % 0.57/0.74 51. (All E, ((member T_4 (difference E T_2)) <=> ((member T_4 E) /\ (-. (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 A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) (member T_6 T_1) (apply T_3 T_5 T_4) (apply T_3 T_4 T_6) (-. (apply T_3 T_5 T_6)) (member T_5 T_1) (All X, ((member X T_1) => (member X T_2))) (All A, (All E, ((member T_5 (difference E A)) <=> ((member T_5 E) /\ (-. (member T_5 A)))))) (member T_4 T_1) ### All 50 % 0.57/0.74 52. (All A, (All E, ((member T_4 (difference E A)) <=> ((member T_4 E) /\ (-. (member T_4 A)))))) (member T_4 T_1) (All A, (All E, ((member T_5 (difference E A)) <=> ((member T_5 E) /\ (-. (member T_5 A)))))) (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (-. (apply T_3 T_5 T_6)) (apply T_3 T_4 T_6) (apply T_3 T_5 T_4) (member T_6 T_1) (All A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) (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 51 % 0.57/0.74 53. (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (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_6 T_1) (apply T_3 T_5 T_4) (apply T_3 T_4 T_6) (-. (apply T_3 T_5 T_6)) (member T_5 T_1) (All X, ((member X T_1) => (member X T_2))) (All A, (All E, ((member T_5 (difference E A)) <=> ((member T_5 E) /\ (-. (member T_5 A)))))) (member T_4 T_1) (All A, (All E, ((member T_4 (difference E A)) <=> ((member T_4 E) /\ (-. (member T_4 A)))))) ### All 52 % 0.57/0.74 54. (All A, (All E, ((member T_4 (difference E A)) <=> ((member T_4 E) /\ (-. (member T_4 A)))))) (member T_4 T_1) (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (-. (apply T_3 T_5 T_6)) (apply T_3 T_4 T_6) (apply T_3 T_5 T_4) (member T_6 T_1) (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 B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### All 53 % 0.57/0.74 55. (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (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_6 T_1) (apply T_3 T_5 T_4) (apply T_3 T_4 T_6) (-. (apply T_3 T_5 T_6)) (member T_5 T_1) (All X, ((member X T_1) => (member X T_2))) (member T_4 T_1) ### All 54 % 0.57/0.74 56. (-. (((member T_5 T_1) /\ ((member T_4 T_1) /\ (member T_6 T_1))) => (((apply T_3 T_5 T_4) /\ (apply T_3 T_4 T_6)) => (apply T_3 T_5 T_6)))) (All X, ((member X T_1) => (member X 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 B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### ConjTree 55 % 0.57/0.74 57. (-. (All Z, (((member T_5 T_1) /\ ((member T_4 T_1) /\ (member Z T_1))) => (((apply T_3 T_5 T_4) /\ (apply T_3 T_4 Z)) => (apply T_3 T_5 Z))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (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 X, ((member X T_1) => (member X T_2))) ### NotAllEx 56 % 0.57/0.74 58. (-. (All Y, (All Z, (((member T_5 T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 T_5 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_5 Z)))))) (All X, ((member X T_1) => (member X 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 B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### NotAllEx 57 % 0.57/0.74 59. (-. (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 B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (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 X, ((member X T_1) => (member X T_2))) ### NotAllEx 58 % 0.57/0.74 60. (-. ((All X, ((member X T_1) => (apply T_3 X 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_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 B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, ((member X T_1) => (member X T_2))) (All X, ((member X T_2) => (apply T_3 X X))) ### NotAnd 9 59 % 0.57/0.74 61. (-. (pre_order T_3 T_1)) (All X, ((member X T_2) => (apply T_3 X X))) (All X, ((member X T_1) => (member X T_2))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (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)))))) ### Definition-Pseudo(pre_order) 60 % 0.57/0.74 62. (subset T_1 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 B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, ((member X T_2) => (apply T_3 X X))) (-. (pre_order T_3 T_1)) ### Definition-Pseudo(subset) 61 % 0.57/0.74 63. ((All X, ((member X T_2) => (apply T_3 X 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))))))) (-. (pre_order T_3 T_1)) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (subset T_1 T_2) ### And 62 % 0.57/0.74 64. (pre_order T_3 T_2) (subset T_1 T_2) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (-. (pre_order T_3 T_1)) ### Definition-Pseudo(pre_order) 63 % 0.57/0.74 65. (-. (((pre_order T_3 T_2) /\ (subset T_1 T_2)) => (pre_order T_3 T_1))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### ConjTree 64 % 0.57/0.74 66. (-. (All R, (((pre_order R T_2) /\ (subset T_1 T_2)) => (pre_order R T_1)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### NotAllEx 65 % 0.57/0.74 67. (-. (All X, (All R, (((pre_order R T_2) /\ (subset X T_2)) => (pre_order R X))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### NotAllEx 66 % 0.57/0.74 68. (-. (All E, (All X, (All R, (((pre_order R E) /\ (subset X E)) => (pre_order R X)))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### NotAllEx 67 % 0.57/0.74 % SZS output end Proof % 0.57/0.74 (* END-PROOF *) %------------------------------------------------------------------------------