%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN345+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 : n012.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:49 EDT 2022 % Result : Theorem 0.20s 0.45s % Output : Proof 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SYN345+1 : TPTP v8.1.0. Released v2.0.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.35 % Computer : n012.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Mon Jul 11 18:40:13 EDT 2022 % 0.13/0.35 % CPUTime : % 0.20/0.45 % SZS status Theorem % 0.20/0.45 (* PROOF-FOUND *) % 0.20/0.45 (* BEGIN-PROOF *) % 0.20/0.45 % SZS output start Proof % 0.20/0.45 1. (big_f T_0 T_0 T_1) (-. (big_f T_0 T_0 T_1)) ### Axiom % 0.20/0.45 2. (-. (big_f T_0 T_2 T_2)) (big_f T_0 T_2 T_2) ### Axiom % 0.20/0.45 3. (-. ((big_f T_0 T_2 T_2) => (big_f T_2 T_3 T_3))) (-. (big_f T_0 T_2 T_2)) ### NotImply 2 % 0.20/0.45 4. (big_f T_4 T_0 T_0) (-. (big_f T_4 T_0 T_0)) ### Axiom % 0.20/0.45 5. (-. (big_f T_4 T_4 T_0)) (big_f T_4 T_4 T_0) ### Axiom % 0.20/0.45 6. (((big_f T_0 T_2 T_2) => (big_f T_2 T_3 T_3)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) (-. (big_f T_4 T_4 T_0)) (big_f T_4 T_0 T_0) (-. (big_f T_0 T_2 T_2)) ### DisjTree 3 4 5 % 0.20/0.45 7. (-. ((((big_f T_4 T_0 T_2) => (big_f T_2 T_2 T_3)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_2 T_2) => (big_f T_2 T_3 T_3)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_2 T_2 T_3) => ((big_f T_0 T_0 T_2) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))))))) (-. (big_f T_0 T_2 T_2)) (big_f T_4 T_0 T_0) (-. (big_f T_4 T_4 T_0)) ### ConjTree 6 % 0.20/0.45 8. (-. (All Z, ((((big_f T_4 T_0 T_2) => (big_f T_2 T_2 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_2 T_2) => (big_f T_2 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_2 T_2 Z) => ((big_f T_0 T_0 T_2) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))) (-. (big_f T_4 T_4 T_0)) (big_f T_4 T_0 T_0) (-. (big_f T_0 T_2 T_2)) ### NotAllEx 7 % 0.20/0.45 9. (-. (Ex Y2, (All Z, ((((big_f T_4 T_0 T_2) => (big_f Y2 T_2 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_2 Y2) => (big_f T_2 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_2 Y2 Z) => ((big_f T_0 T_0 T_2) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))))))))) (-. (big_f T_0 T_2 T_2)) (big_f T_4 T_0 T_0) (-. (big_f T_4 T_4 T_0)) ### NotExists 8 % 0.20/0.45 10. (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) (-. (big_f T_4 T_4 T_0)) (big_f T_4 T_0 T_0) (-. (big_f T_0 T_2 T_2)) ### NotExists 9 % 0.20/0.45 11. (-. ((big_f T_0 T_0 zenon_X5) => (big_f T_0 T_2 T_2))) (big_f T_4 T_0 T_0) (-. (big_f T_4 T_4 T_0)) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) ### NotImply 10 % 0.20/0.45 12. (big_f T_4 T_0 T_0) (-. (big_f T_4 T_0 T_0)) ### Axiom % 0.20/0.45 13. (-. (big_f T_4 T_4 T_0)) (big_f T_4 T_4 T_0) ### Axiom % 0.20/0.45 14. (((big_f T_0 T_0 zenon_X5) => (big_f T_0 T_2 T_2)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) (-. (big_f T_4 T_4 T_0)) (big_f T_4 T_0 T_0) ### DisjTree 11 12 13 % 0.20/0.45 15. (-. ((((big_f T_4 T_0 T_0) => (big_f zenon_X5 T_0 T_2)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_0 zenon_X5) => (big_f T_0 T_2 T_2)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_0 zenon_X5 T_2) => ((big_f T_0 T_0 T_0) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))))))) (big_f T_4 T_0 T_0) (-. (big_f T_4 T_4 T_0)) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) ### ConjTree 14 % 0.20/0.45 16. (-. (All Z, ((((big_f T_4 T_0 T_0) => (big_f zenon_X5 T_0 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_0 zenon_X5) => (big_f T_0 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_0 zenon_X5 Z) => ((big_f T_0 T_0 T_0) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) (-. (big_f T_4 T_4 T_0)) (big_f T_4 T_0 T_0) ### NotAllEx 15 % 0.20/0.45 17. (-. (Ex Y2, (All Z, ((((big_f T_4 T_0 T_0) => (big_f Y2 T_0 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_0 Y2) => (big_f T_0 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_0 Y2 Z) => ((big_f T_0 T_0 T_0) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))))))))) (big_f T_4 T_0 T_0) (-. (big_f T_4 T_4 T_0)) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) ### NotExists 16 % 0.20/0.45 18. (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) (-. (big_f T_4 T_4 T_0)) (big_f T_4 T_0 T_0) ### NotExists 17 % 0.20/0.45 19. (big_f T_4 T_0 T_0) (-. (big_f T_4 T_0 T_0)) ### Axiom % 0.20/0.45 20. (-. ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))) (big_f T_4 T_0 T_0) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) ### NotEquiv 18 19 % 0.20/0.45 21. (-. (big_f T_4 T_0 T_0)) (big_f T_4 T_0 T_0) ### Axiom % 0.20/0.45 22. (-. ((big_f T_4 T_0 T_0) => (big_f zenon_X5 T_0 T_2))) (-. (big_f T_4 T_0 T_0)) ### NotImply 21 % 0.20/0.45 23. (big_f T_4 T_4 T_0) (-. (big_f T_4 T_4 T_0)) ### Axiom % 0.20/0.45 24. (-. (big_f T_4 T_0 T_0)) (big_f T_4 T_0 T_0) ### Axiom % 0.20/0.45 25. (((big_f T_4 T_0 T_0) => (big_f zenon_X5 T_0 T_2)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) (big_f T_4 T_4 T_0) (-. (big_f T_4 T_0 T_0)) ### DisjTree 22 23 24 % 0.20/0.45 26. (-. ((((big_f T_4 T_0 T_0) => (big_f zenon_X5 T_0 T_2)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_0 zenon_X5) => (big_f T_0 T_2 T_2)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_0 zenon_X5 T_2) => ((big_f T_0 T_0 T_0) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))))))) (-. (big_f T_4 T_0 T_0)) (big_f T_4 T_4 T_0) ### ConjTree 25 % 0.20/0.45 27. (-. (All Z, ((((big_f T_4 T_0 T_0) => (big_f zenon_X5 T_0 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_0 zenon_X5) => (big_f T_0 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_0 zenon_X5 Z) => ((big_f T_0 T_0 T_0) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))) (big_f T_4 T_4 T_0) (-. (big_f T_4 T_0 T_0)) ### NotAllEx 26 % 0.20/0.45 28. (-. (Ex Y2, (All Z, ((((big_f T_4 T_0 T_0) => (big_f Y2 T_0 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_0 Y2) => (big_f T_0 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_0 Y2 Z) => ((big_f T_0 T_0 T_0) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))))))))) (-. (big_f T_4 T_0 T_0)) (big_f T_4 T_4 T_0) ### NotExists 27 % 0.20/0.45 29. (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) (big_f T_4 T_4 T_0) (-. (big_f T_4 T_0 T_0)) ### NotExists 28 % 0.20/0.45 30. (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) (-. ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))) ### NotEquiv 20 29 % 0.20/0.46 31. (-. ((big_f T_0 T_0 T_1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) (big_f T_0 T_0 T_1) ### NotAnd 1 30 % 0.20/0.46 32. (-. ((((big_f T_4 T_0 T_1) => (big_f zenon_X6 T_1 T_7)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_1 zenon_X6) => (big_f T_1 T_7 T_7)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_1 zenon_X6 T_7) => ((big_f T_0 T_0 T_1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))))))) (big_f T_0 T_0 T_1) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) ### ConjTree 31 % 0.20/0.46 33. (-. (All Z, ((((big_f T_4 T_0 T_1) => (big_f zenon_X6 T_1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_1 zenon_X6) => (big_f T_1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_1 zenon_X6 Z) => ((big_f T_0 T_0 T_1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) (big_f T_0 T_0 T_1) ### NotAllEx 32 % 0.20/0.46 34. (-. (Ex Y2, (All Z, ((((big_f T_4 T_0 T_1) => (big_f Y2 T_1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_1 Y2) => (big_f T_1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_1 Y2 Z) => ((big_f T_0 T_0 T_1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))))))))) (big_f T_0 T_0 T_1) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) ### NotExists 33 % 0.20/0.46 35. (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) (big_f T_0 T_0 T_1) ### NotExists 34 % 0.20/0.46 36. (-. ((((big_f T_4 T_0 T_0) => (big_f T_0 T_0 T_1)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_0 T_0) => (big_f T_0 T_1 T_1)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_0 T_0 T_1) => ((big_f T_0 T_0 T_0) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))))))) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) ### ConjTree 35 % 0.20/0.46 37. (-. (All Z, ((((big_f T_4 T_0 T_0) => (big_f T_0 T_0 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_0 T_0) => (big_f T_0 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_0 T_0 Z) => ((big_f T_0 T_0 T_0) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) ### NotAllEx 36 % 0.20/0.46 38. (-. (Ex Y2, (All Z, ((((big_f T_4 T_0 T_0) => (big_f Y2 T_0 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 T_0 Y2) => (big_f T_0 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f T_0 Y2 Z) => ((big_f T_0 T_0 T_0) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0))))))))) (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) ### NotExists 37 % 0.20/0.46 39. (-. (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 T_0 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 T_0) => (big_f T_4 T_0 T_0))) => ((((big_f T_0 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 T_0 T_0) => (big_f T_4 T_4 T_0))) => ((big_f Y1 Y2 Z) => ((big_f T_0 T_0 Y1) /\ ((big_f T_4 T_4 T_0) <=> (big_f T_4 T_0 T_0)))))))))) ### NotExists 38 % 0.20/0.46 40. (-. (All X2, (Ex Y1, (Ex Y2, (All Z, ((((big_f T_4 X2 Y1) => (big_f Y2 Y1 Z)) => ((big_f T_4 T_4 X2) => (big_f T_4 X2 X2))) => ((((big_f X2 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f T_4 X2 X2) => (big_f T_4 T_4 X2))) => ((big_f Y1 Y2 Z) => ((big_f X2 X2 Y1) /\ ((big_f T_4 T_4 X2) <=> (big_f T_4 X2 X2))))))))))) ### NotAllEx 39 % 0.20/0.46 41. (-. (All X1, (All X2, (Ex Y1, (Ex Y2, (All Z, ((((big_f X1 X2 Y1) => (big_f Y2 Y1 Z)) => ((big_f X1 X1 X2) => (big_f X1 X2 X2))) => ((((big_f X2 Y1 Y2) => (big_f Y1 Z Z)) => ((big_f X1 X2 X2) => (big_f X1 X1 X2))) => ((big_f Y1 Y2 Z) => ((big_f X2 X2 Y1) /\ ((big_f X1 X1 X2) <=> (big_f X1 X2 X2)))))))))))) ### NotAllEx 40 % 0.20/0.46 % SZS output end Proof % 0.20/0.46 (* END-PROOF *) %------------------------------------------------------------------------------