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