%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN332+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 : n023.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:39 EDT 2022 % Result : Theorem 15.24s 15.41s % Output : Proof 15.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN332+1 : TPTP v8.1.0. Released v2.0.0. % 0.11/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.33 % Computer : n023.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.19/0.33 % CPULimit : 300 % 0.19/0.33 % WCLimit : 600 % 0.19/0.33 % DateTime : Tue Jul 12 04:47:24 EDT 2022 % 0.19/0.33 % CPUTime : % 15.24/15.41 % SZS status Theorem % 15.24/15.41 (* PROOF-FOUND *) % 15.24/15.41 (* BEGIN-PROOF *) % 15.24/15.41 % SZS output start Proof % 15.24/15.41 1. (big_f zenon_X0 T_1) (-. (big_f zenon_X0 T_1)) ### Axiom % 15.24/15.41 2. (-. (big_f zenon_X0 zenon_X0)) (big_f zenon_X0 zenon_X0) ### Axiom % 15.24/15.41 3. (-. (big_f zenon_X0 zenon_X0)) (big_f zenon_X0 zenon_X0) ### Axiom % 15.24/15.41 4. (-. ((big_f zenon_X0 zenon_X0) <=> (big_f zenon_X0 zenon_X0))) (-. (big_f zenon_X0 zenon_X0)) ### NotEquiv 2 3 % 15.24/15.41 5. (big_f T_1 zenon_X0) (-. (big_f T_1 zenon_X0)) ### Axiom % 15.24/15.41 6. (-. (((big_f zenon_X0 zenon_X0) <=> (big_f zenon_X0 zenon_X0)) <=> (big_f T_1 zenon_X0))) (big_f T_1 zenon_X0) (-. (big_f zenon_X0 zenon_X0)) ### NotEquiv 4 5 % 15.24/15.41 7. ((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) (-. (big_f zenon_X0 zenon_X0)) (-. (((big_f zenon_X0 zenon_X0) <=> (big_f zenon_X0 zenon_X0)) <=> (big_f T_1 zenon_X0))) (big_f zenon_X0 T_1) ### Equiv 1 6 % 15.24/15.41 8. (-. ((big_f zenon_X0 zenon_X0) /\ (big_f zenon_X0 zenon_X0))) (big_f zenon_X0 T_1) (-. (((big_f zenon_X0 zenon_X0) <=> (big_f zenon_X0 zenon_X0)) <=> (big_f T_1 zenon_X0))) ((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) ### NotAnd 7 7 % 15.24/15.41 9. (big_f zenon_X0 T_2) (-. (big_f zenon_X0 T_2)) ### Axiom % 15.24/15.41 10. ((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) (-. ((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0))) ### Axiom % 15.24/15.41 11. (big_f T_3 T_4) (-. (big_f T_3 T_4)) ### Axiom % 15.24/15.41 12. (-. (big_f T_3 T_3)) (big_f T_3 T_3) ### Axiom % 15.24/15.41 13. (-. (big_f T_3 T_3)) (big_f T_3 T_3) ### Axiom % 15.24/15.41 14. (-. ((big_f T_3 T_3) <=> (big_f T_3 T_3))) (-. (big_f T_3 T_3)) ### NotEquiv 12 13 % 15.24/15.41 15. (big_f T_4 T_3) (-. (big_f T_4 T_3)) ### Axiom % 15.24/15.41 16. (-. (((big_f T_3 T_3) <=> (big_f T_3 T_3)) <=> (big_f T_4 T_3))) (big_f T_4 T_3) (-. (big_f T_3 T_3)) ### NotEquiv 14 15 % 15.24/15.41 17. ((big_f T_3 T_4) <=> (big_f T_4 T_3)) (-. (big_f T_3 T_3)) (-. (((big_f T_3 T_3) <=> (big_f T_3 T_3)) <=> (big_f T_4 T_3))) (big_f T_3 T_4) ### Equiv 11 16 % 15.24/15.41 18. (-. (big_f T_3 T_3)) (big_f T_3 T_3) ### Axiom % 15.24/15.41 19. ((big_f T_3 T_3) /\ (big_f T_3 T_3)) (-. (big_f T_3 T_3)) ### And 18 % 15.24/15.41 20. (-. (((big_f T_3 T_3) /\ (big_f T_3 T_3)) <=> (big_f T_3 T_4))) (-. (((big_f T_3 T_3) <=> (big_f T_3 T_3)) <=> (big_f T_4 T_3))) (-. (big_f T_3 T_3)) ((big_f T_3 T_4) <=> (big_f T_4 T_3)) ### NotEquiv 17 19 % 15.24/15.41 21. (-. ((-. (((big_f T_3 T_3) /\ (big_f T_3 T_3)) <=> (big_f T_3 T_4))) => (((big_f T_3 T_4) <=> (big_f T_4 T_3)) => (((big_f T_3 T_4) <=> (big_f T_3 T_4)) => ((((big_f T_3 T_3) => (big_f T_3 T_3)) <=> (big_f T_4 T_4)) => (((big_f T_3 T_3) <=> (big_f T_3 T_3)) <=> (big_f T_4 T_3))))))) (-. (big_f T_3 T_3)) ### ConjTree 20 % 15.24/15.41 22. (-. (All Z, ((-. (((big_f T_3 T_3) /\ (big_f T_3 T_3)) <=> (big_f T_3 Z))) => (((big_f T_3 Z) <=> (big_f Z T_3)) => (((big_f T_3 Z) <=> (big_f T_3 Z)) => ((((big_f T_3 T_3) => (big_f T_3 T_3)) <=> (big_f Z Z)) => (((big_f T_3 T_3) <=> (big_f T_3 T_3)) <=> (big_f Z T_3)))))))) (-. (big_f T_3 T_3)) ### NotAllEx 21 % 15.24/15.41 23. (-. (Ex Y, (All Z, ((-. (((big_f T_3 Y) /\ (big_f Y T_3)) <=> (big_f T_3 Z))) => (((big_f T_3 Z) <=> (big_f Z T_3)) => (((big_f T_3 Z) <=> (big_f Y Z)) => ((((big_f Y T_3) => (big_f T_3 Y)) <=> (big_f Z Z)) => (((big_f T_3 Y) <=> (big_f Y T_3)) <=> (big_f Z Y))))))))) (-. (big_f T_3 T_3)) ### NotExists 22 % 15.24/15.41 24. (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) (-. (big_f T_3 T_3)) ### NotExists 23 % 15.24/15.41 25. (big_f T_1 T_2) (-. (big_f T_1 T_2)) ### Axiom % 15.24/15.41 26. (-. (big_f T_2 T_1)) (big_f T_2 T_1) ### Axiom % 15.24/15.41 27. ((big_f T_1 T_2) => (big_f T_2 T_1)) (-. (big_f T_2 T_1)) (big_f T_1 T_2) ### Imply 25 26 % 15.24/15.41 28. (((big_f T_1 T_2) => (big_f T_2 T_1)) <=> (big_f T_3 T_3)) (big_f T_1 T_2) (-. (big_f T_2 T_1)) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) ### Equiv 24 27 % 15.24/15.41 29. (-. ((-. (((big_f T_2 T_1) /\ (big_f T_1 T_2)) <=> (big_f T_2 T_3))) => (((big_f T_2 T_3) <=> (big_f T_3 T_2)) => (((big_f T_2 T_3) <=> (big_f T_1 T_3)) => ((((big_f T_1 T_2) => (big_f T_2 T_1)) <=> (big_f T_3 T_3)) => (((big_f T_2 T_1) <=> (big_f T_1 T_2)) <=> (big_f T_3 T_1))))))) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) (-. (big_f T_2 T_1)) (big_f T_1 T_2) ### ConjTree 28 % 15.24/15.41 30. (-. (All Z, ((-. (((big_f T_2 T_1) /\ (big_f T_1 T_2)) <=> (big_f T_2 Z))) => (((big_f T_2 Z) <=> (big_f Z T_2)) => (((big_f T_2 Z) <=> (big_f T_1 Z)) => ((((big_f T_1 T_2) => (big_f T_2 T_1)) <=> (big_f Z Z)) => (((big_f T_2 T_1) <=> (big_f T_1 T_2)) <=> (big_f Z T_1)))))))) (big_f T_1 T_2) (-. (big_f T_2 T_1)) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) ### NotAllEx 29 % 15.24/15.41 31. (-. (Ex Y, (All Z, ((-. (((big_f T_2 Y) /\ (big_f Y T_2)) <=> (big_f T_2 Z))) => (((big_f T_2 Z) <=> (big_f Z T_2)) => (((big_f T_2 Z) <=> (big_f Y Z)) => ((((big_f Y T_2) => (big_f T_2 Y)) <=> (big_f Z Z)) => (((big_f T_2 Y) <=> (big_f Y T_2)) <=> (big_f Z Y))))))))) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) (-. (big_f T_2 T_1)) (big_f T_1 T_2) ### NotExists 30 % 15.24/15.41 32. (big_f T_1 T_2) (-. (big_f T_2 T_1)) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) ### NotExists 31 % 15.24/15.41 33. (-. (((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) <=> (big_f T_2 T_1))) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) (big_f T_1 T_2) ((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) ### NotEquiv 10 32 % 15.24/15.41 34. ((big_f zenon_X0 T_2) <=> (big_f T_1 T_2)) ((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) (-. (((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) <=> (big_f T_2 T_1))) (big_f zenon_X0 T_2) ### Equiv 9 33 % 15.24/15.41 35. (-. (big_f zenon_X0 T_1)) (big_f zenon_X0 T_1) ### Axiom % 15.24/15.41 36. ((big_f zenon_X0 T_1) /\ (big_f T_1 zenon_X0)) (-. (big_f zenon_X0 T_1)) ### And 35 % 15.24/15.41 37. (-. (((big_f zenon_X0 T_1) /\ (big_f T_1 zenon_X0)) <=> (big_f zenon_X0 T_2))) (-. (big_f zenon_X0 T_1)) (-. (((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) <=> (big_f T_2 T_1))) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) ((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) ((big_f zenon_X0 T_2) <=> (big_f T_1 T_2)) ### NotEquiv 34 36 % 15.24/15.41 38. (-. ((-. (((big_f zenon_X0 T_1) /\ (big_f T_1 zenon_X0)) <=> (big_f zenon_X0 T_2))) => (((big_f zenon_X0 T_2) <=> (big_f T_2 zenon_X0)) => (((big_f zenon_X0 T_2) <=> (big_f T_1 T_2)) => ((((big_f T_1 zenon_X0) => (big_f zenon_X0 T_1)) <=> (big_f T_2 T_2)) => (((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) <=> (big_f T_2 T_1))))))) ((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) (-. (big_f zenon_X0 T_1)) ### ConjTree 37 % 15.31/15.48 39. (-. (All Z, ((-. (((big_f zenon_X0 T_1) /\ (big_f T_1 zenon_X0)) <=> (big_f zenon_X0 Z))) => (((big_f zenon_X0 Z) <=> (big_f Z zenon_X0)) => (((big_f zenon_X0 Z) <=> (big_f T_1 Z)) => ((((big_f T_1 zenon_X0) => (big_f zenon_X0 T_1)) <=> (big_f Z Z)) => (((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) <=> (big_f Z T_1)))))))) (-. (big_f zenon_X0 T_1)) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) ((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) ### NotAllEx 38 % 15.31/15.48 40. (-. (Ex Y, (All Z, ((-. (((big_f zenon_X0 Y) /\ (big_f Y zenon_X0)) <=> (big_f zenon_X0 Z))) => (((big_f zenon_X0 Z) <=> (big_f Z zenon_X0)) => (((big_f zenon_X0 Z) <=> (big_f Y Z)) => ((((big_f Y zenon_X0) => (big_f zenon_X0 Y)) <=> (big_f Z Z)) => (((big_f zenon_X0 Y) <=> (big_f Y zenon_X0)) <=> (big_f Z Y))))))))) ((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) (-. (big_f zenon_X0 T_1)) ### NotExists 39 % 15.31/15.48 41. (-. (((big_f zenon_X0 zenon_X0) /\ (big_f zenon_X0 zenon_X0)) <=> (big_f zenon_X0 T_1))) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) (-. (Ex Y, (All Z, ((-. (((big_f zenon_X0 Y) /\ (big_f Y zenon_X0)) <=> (big_f zenon_X0 Z))) => (((big_f zenon_X0 Z) <=> (big_f Z zenon_X0)) => (((big_f zenon_X0 Z) <=> (big_f Y Z)) => ((((big_f Y zenon_X0) => (big_f zenon_X0 Y)) <=> (big_f Z Z)) => (((big_f zenon_X0 Y) <=> (big_f Y zenon_X0)) <=> (big_f Z Y))))))))) ((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) (-. (((big_f zenon_X0 zenon_X0) <=> (big_f zenon_X0 zenon_X0)) <=> (big_f T_1 zenon_X0))) ### NotEquiv 8 40 % 15.31/15.48 42. (-. ((-. (((big_f zenon_X0 zenon_X0) /\ (big_f zenon_X0 zenon_X0)) <=> (big_f zenon_X0 T_1))) => (((big_f zenon_X0 T_1) <=> (big_f T_1 zenon_X0)) => (((big_f zenon_X0 T_1) <=> (big_f zenon_X0 T_1)) => ((((big_f zenon_X0 zenon_X0) => (big_f zenon_X0 zenon_X0)) <=> (big_f T_1 T_1)) => (((big_f zenon_X0 zenon_X0) <=> (big_f zenon_X0 zenon_X0)) <=> (big_f T_1 zenon_X0))))))) (-. (Ex Y, (All Z, ((-. (((big_f zenon_X0 Y) /\ (big_f Y zenon_X0)) <=> (big_f zenon_X0 Z))) => (((big_f zenon_X0 Z) <=> (big_f Z zenon_X0)) => (((big_f zenon_X0 Z) <=> (big_f Y Z)) => ((((big_f Y zenon_X0) => (big_f zenon_X0 Y)) <=> (big_f Z Z)) => (((big_f zenon_X0 Y) <=> (big_f Y zenon_X0)) <=> (big_f Z Y))))))))) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) ### ConjTree 41 % 15.31/15.48 43. (-. (All Z, ((-. (((big_f zenon_X0 zenon_X0) /\ (big_f zenon_X0 zenon_X0)) <=> (big_f zenon_X0 Z))) => (((big_f zenon_X0 Z) <=> (big_f Z zenon_X0)) => (((big_f zenon_X0 Z) <=> (big_f zenon_X0 Z)) => ((((big_f zenon_X0 zenon_X0) => (big_f zenon_X0 zenon_X0)) <=> (big_f Z Z)) => (((big_f zenon_X0 zenon_X0) <=> (big_f zenon_X0 zenon_X0)) <=> (big_f Z zenon_X0)))))))) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) (-. (Ex Y, (All Z, ((-. (((big_f zenon_X0 Y) /\ (big_f Y zenon_X0)) <=> (big_f zenon_X0 Z))) => (((big_f zenon_X0 Z) <=> (big_f Z zenon_X0)) => (((big_f zenon_X0 Z) <=> (big_f Y Z)) => ((((big_f Y zenon_X0) => (big_f zenon_X0 Y)) <=> (big_f Z Z)) => (((big_f zenon_X0 Y) <=> (big_f Y zenon_X0)) <=> (big_f Z Y))))))))) ### NotAllEx 42 % 15.31/15.48 44. (-. (Ex Y, (All Z, ((-. (((big_f zenon_X0 Y) /\ (big_f Y zenon_X0)) <=> (big_f zenon_X0 Z))) => (((big_f zenon_X0 Z) <=> (big_f Z zenon_X0)) => (((big_f zenon_X0 Z) <=> (big_f Y Z)) => ((((big_f Y zenon_X0) => (big_f zenon_X0 Y)) <=> (big_f Z Z)) => (((big_f zenon_X0 Y) <=> (big_f Y zenon_X0)) <=> (big_f Z Y))))))))) (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) ### NotExists 43 % 15.31/15.48 45. (-. (Ex X, (Ex Y, (All Z, ((-. (((big_f X Y) /\ (big_f Y X)) <=> (big_f X Z))) => (((big_f X Z) <=> (big_f Z X)) => (((big_f X Z) <=> (big_f Y Z)) => ((((big_f Y X) => (big_f X Y)) <=> (big_f Z Z)) => (((big_f X Y) <=> (big_f Y X)) <=> (big_f Z Y)))))))))) ### NotExists 44 % 15.31/15.48 % SZS output end Proof % 15.31/15.48 (* END-PROOF *) %------------------------------------------------------------------------------