%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : LAT362+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n013.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 : Sun Jul 17 06:57:54 EDT 2022 % Result : Theorem 3.06s 3.24s % Output : Proof 3.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : LAT362+1 : TPTP v8.1.0. Released v3.4.0. % 0.06/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n013.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 : Thu Jun 30 07:08:14 EDT 2022 % 0.12/0.33 % CPUTime : % 3.06/3.24 % SZS status Theorem % 3.06/3.24 (* PROOF-FOUND *) % 3.06/3.24 (* BEGIN-PROOF *) % 3.06/3.24 % SZS output start Proof % 3.06/3.24 1. (-. (v2_setfam_1 T_0)) (v2_setfam_1 T_0) ### Axiom % 3.06/3.24 2. (-. (-. (v2_setfam_1 T_0))) (-. (v2_setfam_1 T_0)) ### NotNot 1 % 3.06/3.24 3. (v3_struct_0 (k4_waybel34 T_0)) (-. (v3_struct_0 (k4_waybel34 T_0))) ### Axiom % 3.06/3.24 4. ((-. (v3_struct_0 (k4_waybel34 T_0))) /\ ((v2_altcat_1 (k4_waybel34 T_0)) /\ ((v6_altcat_1 (k4_waybel34 T_0)) /\ ((v9_altcat_1 (k4_waybel34 T_0)) /\ ((v11_altcat_1 (k4_waybel34 T_0)) /\ ((v12_altcat_1 (k4_waybel34 T_0)) /\ ((v1_altcat_2 (k4_waybel34 T_0)) /\ ((v2_yellow18 (k4_waybel34 T_0)) /\ ((v3_yellow18 (k4_waybel34 T_0)) /\ ((v4_yellow18 (k4_waybel34 T_0)) /\ ((v1_yellow21 (k4_waybel34 T_0)) /\ ((v2_yellow21 (k4_waybel34 T_0)) /\ (v3_yellow21 (k4_waybel34 T_0)))))))))))))) (v3_struct_0 (k4_waybel34 T_0)) ### ConjTree 3 % 3.06/3.24 5. ((-. (v2_setfam_1 T_0)) => ((-. (v3_struct_0 (k4_waybel34 T_0))) /\ ((v2_altcat_1 (k4_waybel34 T_0)) /\ ((v6_altcat_1 (k4_waybel34 T_0)) /\ ((v9_altcat_1 (k4_waybel34 T_0)) /\ ((v11_altcat_1 (k4_waybel34 T_0)) /\ ((v12_altcat_1 (k4_waybel34 T_0)) /\ ((v1_altcat_2 (k4_waybel34 T_0)) /\ ((v2_yellow18 (k4_waybel34 T_0)) /\ ((v3_yellow18 (k4_waybel34 T_0)) /\ ((v4_yellow18 (k4_waybel34 T_0)) /\ ((v1_yellow21 (k4_waybel34 T_0)) /\ ((v2_yellow21 (k4_waybel34 T_0)) /\ (v3_yellow21 (k4_waybel34 T_0))))))))))))))) (v3_struct_0 (k4_waybel34 T_0)) (-. (v2_setfam_1 T_0)) ### Imply 2 4 % 3.06/3.24 6. (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v9_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v1_altcat_2 (k4_waybel34 A)) /\ ((v2_yellow18 (k4_waybel34 A)) /\ ((v3_yellow18 (k4_waybel34 A)) /\ ((v4_yellow18 (k4_waybel34 A)) /\ ((v1_yellow21 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (v3_yellow21 (k4_waybel34 A)))))))))))))))) (-. (v2_setfam_1 T_0)) (v3_struct_0 (k4_waybel34 T_0)) ### All 5 % 3.06/3.24 7. (-. (v2_altcat_1 (k4_waybel34 T_0))) (v2_altcat_1 (k4_waybel34 T_0)) ### Axiom % 3.06/3.24 8. ((-. (v3_struct_0 (k4_waybel34 T_0))) /\ ((v2_altcat_1 (k4_waybel34 T_0)) /\ ((v6_altcat_1 (k4_waybel34 T_0)) /\ ((v9_altcat_1 (k4_waybel34 T_0)) /\ ((v11_altcat_1 (k4_waybel34 T_0)) /\ ((v12_altcat_1 (k4_waybel34 T_0)) /\ ((v1_altcat_2 (k4_waybel34 T_0)) /\ ((v2_yellow18 (k4_waybel34 T_0)) /\ ((v3_yellow18 (k4_waybel34 T_0)) /\ ((v4_yellow18 (k4_waybel34 T_0)) /\ ((v1_yellow21 (k4_waybel34 T_0)) /\ ((v2_yellow21 (k4_waybel34 T_0)) /\ (v3_yellow21 (k4_waybel34 T_0)))))))))))))) (-. (v2_altcat_1 (k4_waybel34 T_0))) ### ConjTree 7 % 3.06/3.24 9. ((-. (v2_setfam_1 T_0)) => ((-. (v3_struct_0 (k4_waybel34 T_0))) /\ ((v2_altcat_1 (k4_waybel34 T_0)) /\ ((v6_altcat_1 (k4_waybel34 T_0)) /\ ((v9_altcat_1 (k4_waybel34 T_0)) /\ ((v11_altcat_1 (k4_waybel34 T_0)) /\ ((v12_altcat_1 (k4_waybel34 T_0)) /\ ((v1_altcat_2 (k4_waybel34 T_0)) /\ ((v2_yellow18 (k4_waybel34 T_0)) /\ ((v3_yellow18 (k4_waybel34 T_0)) /\ ((v4_yellow18 (k4_waybel34 T_0)) /\ ((v1_yellow21 (k4_waybel34 T_0)) /\ ((v2_yellow21 (k4_waybel34 T_0)) /\ (v3_yellow21 (k4_waybel34 T_0))))))))))))))) (-. (v2_altcat_1 (k4_waybel34 T_0))) (-. (v2_setfam_1 T_0)) ### Imply 2 8 % 3.06/3.24 10. (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v9_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v1_altcat_2 (k4_waybel34 A)) /\ ((v2_yellow18 (k4_waybel34 A)) /\ ((v3_yellow18 (k4_waybel34 A)) /\ ((v4_yellow18 (k4_waybel34 A)) /\ ((v1_yellow21 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (v3_yellow21 (k4_waybel34 A)))))))))))))))) (-. (v2_setfam_1 T_0)) (-. (v2_altcat_1 (k4_waybel34 T_0))) ### All 9 % 3.06/3.24 11. (-. (v12_altcat_1 (k4_waybel34 T_0))) (v12_altcat_1 (k4_waybel34 T_0)) ### Axiom % 3.06/3.24 12. ((-. (v3_struct_0 (k4_waybel34 T_0))) /\ ((v2_altcat_1 (k4_waybel34 T_0)) /\ ((v6_altcat_1 (k4_waybel34 T_0)) /\ ((v9_altcat_1 (k4_waybel34 T_0)) /\ ((v11_altcat_1 (k4_waybel34 T_0)) /\ ((v12_altcat_1 (k4_waybel34 T_0)) /\ ((v1_altcat_2 (k4_waybel34 T_0)) /\ ((v2_yellow18 (k4_waybel34 T_0)) /\ ((v3_yellow18 (k4_waybel34 T_0)) /\ ((v4_yellow18 (k4_waybel34 T_0)) /\ ((v1_yellow21 (k4_waybel34 T_0)) /\ ((v2_yellow21 (k4_waybel34 T_0)) /\ (v3_yellow21 (k4_waybel34 T_0)))))))))))))) (-. (v12_altcat_1 (k4_waybel34 T_0))) ### ConjTree 11 % 3.06/3.24 13. ((-. (v2_setfam_1 T_0)) => ((-. (v3_struct_0 (k4_waybel34 T_0))) /\ ((v2_altcat_1 (k4_waybel34 T_0)) /\ ((v6_altcat_1 (k4_waybel34 T_0)) /\ ((v9_altcat_1 (k4_waybel34 T_0)) /\ ((v11_altcat_1 (k4_waybel34 T_0)) /\ ((v12_altcat_1 (k4_waybel34 T_0)) /\ ((v1_altcat_2 (k4_waybel34 T_0)) /\ ((v2_yellow18 (k4_waybel34 T_0)) /\ ((v3_yellow18 (k4_waybel34 T_0)) /\ ((v4_yellow18 (k4_waybel34 T_0)) /\ ((v1_yellow21 (k4_waybel34 T_0)) /\ ((v2_yellow21 (k4_waybel34 T_0)) /\ (v3_yellow21 (k4_waybel34 T_0))))))))))))))) (-. (v12_altcat_1 (k4_waybel34 T_0))) (-. (v2_setfam_1 T_0)) ### Imply 2 12 % 3.06/3.24 14. (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v9_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v1_altcat_2 (k4_waybel34 A)) /\ ((v2_yellow18 (k4_waybel34 A)) /\ ((v3_yellow18 (k4_waybel34 A)) /\ ((v4_yellow18 (k4_waybel34 A)) /\ ((v1_yellow21 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (v3_yellow21 (k4_waybel34 A)))))))))))))))) (-. (v2_setfam_1 T_0)) (-. (v12_altcat_1 (k4_waybel34 T_0))) ### All 13 % 3.06/3.24 15. (v1_xboole_0 T_0) (-. (v1_xboole_0 T_0)) ### Axiom % 3.06/3.24 16. ((-. (v2_setfam_1 T_0)) => (-. (v1_xboole_0 T_0))) (v1_xboole_0 T_0) (-. (v2_setfam_1 T_0)) ### Imply 2 15 % 3.06/3.24 17. (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) (-. (v2_setfam_1 T_0)) (v1_xboole_0 T_0) ### All 16 % 3.06/3.24 18. (-. (-. (v1_xboole_0 T_0))) (-. (v2_setfam_1 T_0)) (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) ### NotNot 17 % 3.06/3.24 19. (-. (l2_altcat_1 (k4_waybel34 T_0))) (l2_altcat_1 (k4_waybel34 T_0)) ### Axiom % 3.06/3.24 20. ((-. (v3_struct_0 (k4_waybel34 T_0))) /\ ((v2_altcat_1 (k4_waybel34 T_0)) /\ ((v6_altcat_1 (k4_waybel34 T_0)) /\ ((v11_altcat_1 (k4_waybel34 T_0)) /\ ((v12_altcat_1 (k4_waybel34 T_0)) /\ ((v2_yellow21 (k4_waybel34 T_0)) /\ (l2_altcat_1 (k4_waybel34 T_0)))))))) (-. (l2_altcat_1 (k4_waybel34 T_0))) ### ConjTree 19 % 3.06/3.24 21. ((-. (v1_xboole_0 T_0)) => ((-. (v3_struct_0 (k4_waybel34 T_0))) /\ ((v2_altcat_1 (k4_waybel34 T_0)) /\ ((v6_altcat_1 (k4_waybel34 T_0)) /\ ((v11_altcat_1 (k4_waybel34 T_0)) /\ ((v12_altcat_1 (k4_waybel34 T_0)) /\ ((v2_yellow21 (k4_waybel34 T_0)) /\ (l2_altcat_1 (k4_waybel34 T_0))))))))) (-. (l2_altcat_1 (k4_waybel34 T_0))) (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) (-. (v2_setfam_1 T_0)) ### Imply 18 20 % 3.06/3.24 22. (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (l2_altcat_1 (k4_waybel34 A)))))))))) (-. (v2_setfam_1 T_0)) (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) (-. (l2_altcat_1 (k4_waybel34 T_0))) ### All 21 % 3.06/3.24 23. (v3_struct_0 (k5_waybel34 T_0)) (-. (v3_struct_0 (k5_waybel34 T_0))) ### Axiom % 3.06/3.24 24. ((-. (v3_struct_0 (k5_waybel34 T_0))) /\ ((v2_altcat_1 (k5_waybel34 T_0)) /\ ((v6_altcat_1 (k5_waybel34 T_0)) /\ ((v9_altcat_1 (k5_waybel34 T_0)) /\ ((v11_altcat_1 (k5_waybel34 T_0)) /\ ((v12_altcat_1 (k5_waybel34 T_0)) /\ ((v1_altcat_2 (k5_waybel34 T_0)) /\ ((v2_yellow18 (k5_waybel34 T_0)) /\ ((v3_yellow18 (k5_waybel34 T_0)) /\ ((v4_yellow18 (k5_waybel34 T_0)) /\ ((v1_yellow21 (k5_waybel34 T_0)) /\ ((v2_yellow21 (k5_waybel34 T_0)) /\ (v3_yellow21 (k5_waybel34 T_0)))))))))))))) (v3_struct_0 (k5_waybel34 T_0)) ### ConjTree 23 % 3.06/3.24 25. ((-. (v2_setfam_1 T_0)) => ((-. (v3_struct_0 (k5_waybel34 T_0))) /\ ((v2_altcat_1 (k5_waybel34 T_0)) /\ ((v6_altcat_1 (k5_waybel34 T_0)) /\ ((v9_altcat_1 (k5_waybel34 T_0)) /\ ((v11_altcat_1 (k5_waybel34 T_0)) /\ ((v12_altcat_1 (k5_waybel34 T_0)) /\ ((v1_altcat_2 (k5_waybel34 T_0)) /\ ((v2_yellow18 (k5_waybel34 T_0)) /\ ((v3_yellow18 (k5_waybel34 T_0)) /\ ((v4_yellow18 (k5_waybel34 T_0)) /\ ((v1_yellow21 (k5_waybel34 T_0)) /\ ((v2_yellow21 (k5_waybel34 T_0)) /\ (v3_yellow21 (k5_waybel34 T_0))))))))))))))) (v3_struct_0 (k5_waybel34 T_0)) (-. (v2_setfam_1 T_0)) ### Imply 2 24 % 3.06/3.31 26. (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v9_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v1_altcat_2 (k5_waybel34 A)) /\ ((v2_yellow18 (k5_waybel34 A)) /\ ((v3_yellow18 (k5_waybel34 A)) /\ ((v4_yellow18 (k5_waybel34 A)) /\ ((v1_yellow21 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (v3_yellow21 (k5_waybel34 A)))))))))))))))) (-. (v2_setfam_1 T_0)) (v3_struct_0 (k5_waybel34 T_0)) ### All 25 % 3.06/3.31 27. (-. (v2_altcat_1 (k5_waybel34 T_0))) (v2_altcat_1 (k5_waybel34 T_0)) ### Axiom % 3.06/3.31 28. ((-. (v3_struct_0 (k5_waybel34 T_0))) /\ ((v2_altcat_1 (k5_waybel34 T_0)) /\ ((v6_altcat_1 (k5_waybel34 T_0)) /\ ((v9_altcat_1 (k5_waybel34 T_0)) /\ ((v11_altcat_1 (k5_waybel34 T_0)) /\ ((v12_altcat_1 (k5_waybel34 T_0)) /\ ((v1_altcat_2 (k5_waybel34 T_0)) /\ ((v2_yellow18 (k5_waybel34 T_0)) /\ ((v3_yellow18 (k5_waybel34 T_0)) /\ ((v4_yellow18 (k5_waybel34 T_0)) /\ ((v1_yellow21 (k5_waybel34 T_0)) /\ ((v2_yellow21 (k5_waybel34 T_0)) /\ (v3_yellow21 (k5_waybel34 T_0)))))))))))))) (-. (v2_altcat_1 (k5_waybel34 T_0))) ### ConjTree 27 % 3.06/3.31 29. ((-. (v2_setfam_1 T_0)) => ((-. (v3_struct_0 (k5_waybel34 T_0))) /\ ((v2_altcat_1 (k5_waybel34 T_0)) /\ ((v6_altcat_1 (k5_waybel34 T_0)) /\ ((v9_altcat_1 (k5_waybel34 T_0)) /\ ((v11_altcat_1 (k5_waybel34 T_0)) /\ ((v12_altcat_1 (k5_waybel34 T_0)) /\ ((v1_altcat_2 (k5_waybel34 T_0)) /\ ((v2_yellow18 (k5_waybel34 T_0)) /\ ((v3_yellow18 (k5_waybel34 T_0)) /\ ((v4_yellow18 (k5_waybel34 T_0)) /\ ((v1_yellow21 (k5_waybel34 T_0)) /\ ((v2_yellow21 (k5_waybel34 T_0)) /\ (v3_yellow21 (k5_waybel34 T_0))))))))))))))) (-. (v2_altcat_1 (k5_waybel34 T_0))) (-. (v2_setfam_1 T_0)) ### Imply 2 28 % 3.06/3.31 30. (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v9_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v1_altcat_2 (k5_waybel34 A)) /\ ((v2_yellow18 (k5_waybel34 A)) /\ ((v3_yellow18 (k5_waybel34 A)) /\ ((v4_yellow18 (k5_waybel34 A)) /\ ((v1_yellow21 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (v3_yellow21 (k5_waybel34 A)))))))))))))))) (-. (v2_setfam_1 T_0)) (-. (v2_altcat_1 (k5_waybel34 T_0))) ### All 29 % 3.06/3.31 31. (-. (v12_altcat_1 (k5_waybel34 T_0))) (v12_altcat_1 (k5_waybel34 T_0)) ### Axiom % 3.06/3.31 32. ((-. (v3_struct_0 (k5_waybel34 T_0))) /\ ((v2_altcat_1 (k5_waybel34 T_0)) /\ ((v6_altcat_1 (k5_waybel34 T_0)) /\ ((v9_altcat_1 (k5_waybel34 T_0)) /\ ((v11_altcat_1 (k5_waybel34 T_0)) /\ ((v12_altcat_1 (k5_waybel34 T_0)) /\ ((v1_altcat_2 (k5_waybel34 T_0)) /\ ((v2_yellow18 (k5_waybel34 T_0)) /\ ((v3_yellow18 (k5_waybel34 T_0)) /\ ((v4_yellow18 (k5_waybel34 T_0)) /\ ((v1_yellow21 (k5_waybel34 T_0)) /\ ((v2_yellow21 (k5_waybel34 T_0)) /\ (v3_yellow21 (k5_waybel34 T_0)))))))))))))) (-. (v12_altcat_1 (k5_waybel34 T_0))) ### ConjTree 31 % 3.06/3.31 33. ((-. (v2_setfam_1 T_0)) => ((-. (v3_struct_0 (k5_waybel34 T_0))) /\ ((v2_altcat_1 (k5_waybel34 T_0)) /\ ((v6_altcat_1 (k5_waybel34 T_0)) /\ ((v9_altcat_1 (k5_waybel34 T_0)) /\ ((v11_altcat_1 (k5_waybel34 T_0)) /\ ((v12_altcat_1 (k5_waybel34 T_0)) /\ ((v1_altcat_2 (k5_waybel34 T_0)) /\ ((v2_yellow18 (k5_waybel34 T_0)) /\ ((v3_yellow18 (k5_waybel34 T_0)) /\ ((v4_yellow18 (k5_waybel34 T_0)) /\ ((v1_yellow21 (k5_waybel34 T_0)) /\ ((v2_yellow21 (k5_waybel34 T_0)) /\ (v3_yellow21 (k5_waybel34 T_0))))))))))))))) (-. (v12_altcat_1 (k5_waybel34 T_0))) (-. (v2_setfam_1 T_0)) ### Imply 2 32 % 3.06/3.31 34. (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v9_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v1_altcat_2 (k5_waybel34 A)) /\ ((v2_yellow18 (k5_waybel34 A)) /\ ((v3_yellow18 (k5_waybel34 A)) /\ ((v4_yellow18 (k5_waybel34 A)) /\ ((v1_yellow21 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (v3_yellow21 (k5_waybel34 A)))))))))))))))) (-. (v2_setfam_1 T_0)) (-. (v12_altcat_1 (k5_waybel34 T_0))) ### All 33 % 3.06/3.31 35. (-. (l2_altcat_1 (k5_waybel34 T_0))) (l2_altcat_1 (k5_waybel34 T_0)) ### Axiom % 3.06/3.31 36. ((-. (v3_struct_0 (k5_waybel34 T_0))) /\ ((v2_altcat_1 (k5_waybel34 T_0)) /\ ((v6_altcat_1 (k5_waybel34 T_0)) /\ ((v11_altcat_1 (k5_waybel34 T_0)) /\ ((v12_altcat_1 (k5_waybel34 T_0)) /\ ((v2_yellow21 (k5_waybel34 T_0)) /\ (l2_altcat_1 (k5_waybel34 T_0)))))))) (-. (l2_altcat_1 (k5_waybel34 T_0))) ### ConjTree 35 % 3.06/3.31 37. ((-. (v1_xboole_0 T_0)) => ((-. (v3_struct_0 (k5_waybel34 T_0))) /\ ((v2_altcat_1 (k5_waybel34 T_0)) /\ ((v6_altcat_1 (k5_waybel34 T_0)) /\ ((v11_altcat_1 (k5_waybel34 T_0)) /\ ((v12_altcat_1 (k5_waybel34 T_0)) /\ ((v2_yellow21 (k5_waybel34 T_0)) /\ (l2_altcat_1 (k5_waybel34 T_0))))))))) (-. (l2_altcat_1 (k5_waybel34 T_0))) (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) (-. (v2_setfam_1 T_0)) ### Imply 18 36 % 3.06/3.31 38. (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (l2_altcat_1 (k5_waybel34 A)))))))))) (-. (v2_setfam_1 T_0)) (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) (-. (l2_altcat_1 (k5_waybel34 T_0))) ### All 37 % 3.06/3.31 39. (m2_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (-. (m2_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0))) ### Axiom % 3.06/3.31 40. (v21_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (-. (v21_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0))) ### Axiom % 3.06/3.31 41. (v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (-. (v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0))) ### Axiom % 3.06/3.31 42. (-. ((m2_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v21_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0))))) (v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (v21_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (m2_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) ### DisjTree 39 40 41 % 3.06/3.31 43. (-. (Ex C, ((m2_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v21_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v16_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)))))) (m2_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (v21_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) ### NotExists 42 % 3.06/3.31 44. ((v9_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (m2_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)))) (v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (v21_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (-. (Ex C, ((m2_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v21_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v16_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)))))) ### ConjTree 43 % 3.06/3.31 45. ((-. (v2_setfam_1 T_0)) => ((v9_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (m2_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0))))) (-. (Ex C, ((m2_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v21_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v16_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)))))) (v21_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (-. (v2_setfam_1 T_0)) ### Imply 2 44 % 3.06/3.31 46. (All A, ((-. (v2_setfam_1 A)) => ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (m2_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)))))) (-. (v2_setfam_1 T_0)) (v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (v21_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) (-. (Ex C, ((m2_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v21_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v16_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)))))) ### All 45 % 3.06/3.33 47. ((v6_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v8_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v9_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v11_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v12_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v14_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v21_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0))))))))) (-. (Ex C, ((m2_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v21_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v16_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)))))) (-. (v2_setfam_1 T_0)) (All A, ((-. (v2_setfam_1 A)) => ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (m2_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)))))) ### ConjTree 46 % 3.06/3.33 48. ((-. (v2_setfam_1 T_0)) => ((v6_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v8_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v9_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v11_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v12_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v14_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v16_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v21_functor0 (k6_waybel34 T_0) (k4_waybel34 T_0) (k5_waybel34 T_0)))))))))) (All A, ((-. (v2_setfam_1 A)) => ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (m2_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)))))) (-. (Ex C, ((m2_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v21_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v16_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)))))) (-. (v2_setfam_1 T_0)) ### Imply 2 47 % 3.06/3.33 49. (All A, ((-. (v2_setfam_1 A)) => ((v6_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v8_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v11_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v12_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v14_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (v21_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A))))))))))) (-. (v2_setfam_1 T_0)) (-. (Ex C, ((m2_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v21_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v16_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)))))) (All A, ((-. (v2_setfam_1 A)) => ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (m2_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)))))) ### All 48 % 3.06/3.33 50. (-. (r2_functor0 (k4_waybel34 T_0) (k5_waybel34 T_0))) (r2_functor0 (k4_waybel34 T_0) (k5_waybel34 T_0)) ### Axiom % 3.06/3.33 51. ((r2_functor0 (k4_waybel34 T_0) (k5_waybel34 T_0)) <=> (Ex C, ((m2_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v21_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v16_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)))))) (-. (r2_functor0 (k4_waybel34 T_0) (k5_waybel34 T_0))) (All A, ((-. (v2_setfam_1 A)) => ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (m2_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)))))) (-. (v2_setfam_1 T_0)) (All A, ((-. (v2_setfam_1 A)) => ((v6_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v8_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v11_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v12_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v14_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (v21_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A))))))))))) ### Equiv 49 50 % 3.06/3.33 52. (((-. (v3_struct_0 (k5_waybel34 T_0))) /\ ((v2_altcat_1 (k5_waybel34 T_0)) /\ ((v12_altcat_1 (k5_waybel34 T_0)) /\ (l2_altcat_1 (k5_waybel34 T_0))))) => ((r2_functor0 (k4_waybel34 T_0) (k5_waybel34 T_0)) <=> (Ex C, ((m2_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ ((v21_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0)) /\ (v16_functor0 C (k4_waybel34 T_0) (k5_waybel34 T_0))))))) (All A, ((-. (v2_setfam_1 A)) => ((v6_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v8_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v11_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v12_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v14_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (v21_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A))))))))))) (All A, ((-. (v2_setfam_1 A)) => ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (m2_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)))))) (-. (r2_functor0 (k4_waybel34 T_0) (k5_waybel34 T_0))) (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (l2_altcat_1 (k5_waybel34 A)))))))))) (-. (v2_setfam_1 T_0)) (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v9_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v1_altcat_2 (k5_waybel34 A)) /\ ((v2_yellow18 (k5_waybel34 A)) /\ ((v3_yellow18 (k5_waybel34 A)) /\ ((v4_yellow18 (k5_waybel34 A)) /\ ((v1_yellow21 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (v3_yellow21 (k5_waybel34 A)))))))))))))))) ### DisjTree 26 30 34 38 51 % 3.06/3.33 53. (All B, (((-. (v3_struct_0 B)) /\ ((v2_altcat_1 B) /\ ((v12_altcat_1 B) /\ (l2_altcat_1 B)))) => ((r2_functor0 (k4_waybel34 T_0) B) <=> (Ex C, ((m2_functor0 C (k4_waybel34 T_0) B) /\ ((v21_functor0 C (k4_waybel34 T_0) B) /\ (v16_functor0 C (k4_waybel34 T_0) B))))))) (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v9_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v1_altcat_2 (k5_waybel34 A)) /\ ((v2_yellow18 (k5_waybel34 A)) /\ ((v3_yellow18 (k5_waybel34 A)) /\ ((v4_yellow18 (k5_waybel34 A)) /\ ((v1_yellow21 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (v3_yellow21 (k5_waybel34 A)))))))))))))))) (-. (v2_setfam_1 T_0)) (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (l2_altcat_1 (k5_waybel34 A)))))))))) (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) (-. (r2_functor0 (k4_waybel34 T_0) (k5_waybel34 T_0))) (All A, ((-. (v2_setfam_1 A)) => ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (m2_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)))))) (All A, ((-. (v2_setfam_1 A)) => ((v6_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v8_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v11_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v12_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v14_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (v21_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A))))))))))) ### All 52 % 3.16/3.34 54. (((-. (v3_struct_0 (k4_waybel34 T_0))) /\ ((v2_altcat_1 (k4_waybel34 T_0)) /\ ((v12_altcat_1 (k4_waybel34 T_0)) /\ (l2_altcat_1 (k4_waybel34 T_0))))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_altcat_1 B) /\ ((v12_altcat_1 B) /\ (l2_altcat_1 B)))) => ((r2_functor0 (k4_waybel34 T_0) B) <=> (Ex C, ((m2_functor0 C (k4_waybel34 T_0) B) /\ ((v21_functor0 C (k4_waybel34 T_0) B) /\ (v16_functor0 C (k4_waybel34 T_0) B)))))))) (All A, ((-. (v2_setfam_1 A)) => ((v6_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v8_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v11_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v12_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v14_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (v21_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A))))))))))) (All A, ((-. (v2_setfam_1 A)) => ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (m2_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)))))) (-. (r2_functor0 (k4_waybel34 T_0) (k5_waybel34 T_0))) (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (l2_altcat_1 (k5_waybel34 A)))))))))) (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v9_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v1_altcat_2 (k5_waybel34 A)) /\ ((v2_yellow18 (k5_waybel34 A)) /\ ((v3_yellow18 (k5_waybel34 A)) /\ ((v4_yellow18 (k5_waybel34 A)) /\ ((v1_yellow21 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (v3_yellow21 (k5_waybel34 A)))))))))))))))) (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (l2_altcat_1 (k4_waybel34 A)))))))))) (-. (v2_setfam_1 T_0)) (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v9_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v1_altcat_2 (k4_waybel34 A)) /\ ((v2_yellow18 (k4_waybel34 A)) /\ ((v3_yellow18 (k4_waybel34 A)) /\ ((v4_yellow18 (k4_waybel34 A)) /\ ((v1_yellow21 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (v3_yellow21 (k4_waybel34 A)))))))))))))))) ### DisjTree 6 10 14 22 53 % 3.16/3.34 55. (All A, (((-. (v3_struct_0 A)) /\ ((v2_altcat_1 A) /\ ((v12_altcat_1 A) /\ (l2_altcat_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_altcat_1 B) /\ ((v12_altcat_1 B) /\ (l2_altcat_1 B)))) => ((r2_functor0 A B) <=> (Ex C, ((m2_functor0 C A B) /\ ((v21_functor0 C A B) /\ (v16_functor0 C A B))))))))) (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v9_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v1_altcat_2 (k4_waybel34 A)) /\ ((v2_yellow18 (k4_waybel34 A)) /\ ((v3_yellow18 (k4_waybel34 A)) /\ ((v4_yellow18 (k4_waybel34 A)) /\ ((v1_yellow21 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (v3_yellow21 (k4_waybel34 A)))))))))))))))) (-. (v2_setfam_1 T_0)) (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (l2_altcat_1 (k4_waybel34 A)))))))))) (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v9_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v1_altcat_2 (k5_waybel34 A)) /\ ((v2_yellow18 (k5_waybel34 A)) /\ ((v3_yellow18 (k5_waybel34 A)) /\ ((v4_yellow18 (k5_waybel34 A)) /\ ((v1_yellow21 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (v3_yellow21 (k5_waybel34 A)))))))))))))))) (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (l2_altcat_1 (k5_waybel34 A)))))))))) (-. (r2_functor0 (k4_waybel34 T_0) (k5_waybel34 T_0))) (All A, ((-. (v2_setfam_1 A)) => ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (m2_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)))))) (All A, ((-. (v2_setfam_1 A)) => ((v6_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v8_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v11_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v12_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v14_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (v21_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A))))))))))) ### All 54 % 3.16/3.34 56. (-. ((-. (v2_setfam_1 T_0)) => (r2_functor0 (k4_waybel34 T_0) (k5_waybel34 T_0)))) (All A, ((-. (v2_setfam_1 A)) => ((v6_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v8_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v11_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v12_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v14_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (v21_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A))))))))))) (All A, ((-. (v2_setfam_1 A)) => ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (m2_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)))))) (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (l2_altcat_1 (k5_waybel34 A)))))))))) (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v9_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v1_altcat_2 (k5_waybel34 A)) /\ ((v2_yellow18 (k5_waybel34 A)) /\ ((v3_yellow18 (k5_waybel34 A)) /\ ((v4_yellow18 (k5_waybel34 A)) /\ ((v1_yellow21 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (v3_yellow21 (k5_waybel34 A)))))))))))))))) (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (l2_altcat_1 (k4_waybel34 A)))))))))) (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v9_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v1_altcat_2 (k4_waybel34 A)) /\ ((v2_yellow18 (k4_waybel34 A)) /\ ((v3_yellow18 (k4_waybel34 A)) /\ ((v4_yellow18 (k4_waybel34 A)) /\ ((v1_yellow21 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (v3_yellow21 (k4_waybel34 A)))))))))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_altcat_1 A) /\ ((v12_altcat_1 A) /\ (l2_altcat_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_altcat_1 B) /\ ((v12_altcat_1 B) /\ (l2_altcat_1 B)))) => ((r2_functor0 A B) <=> (Ex C, ((m2_functor0 C A B) /\ ((v21_functor0 C A B) /\ (v16_functor0 C A B))))))))) ### NotImply 55 % 3.16/3.35 57. (-. (All A, ((-. (v2_setfam_1 A)) => (r2_functor0 (k4_waybel34 A) (k5_waybel34 A))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_altcat_1 A) /\ ((v12_altcat_1 A) /\ (l2_altcat_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_altcat_1 B) /\ ((v12_altcat_1 B) /\ (l2_altcat_1 B)))) => ((r2_functor0 A B) <=> (Ex C, ((m2_functor0 C A B) /\ ((v21_functor0 C A B) /\ (v16_functor0 C A B))))))))) (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v9_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v1_altcat_2 (k4_waybel34 A)) /\ ((v2_yellow18 (k4_waybel34 A)) /\ ((v3_yellow18 (k4_waybel34 A)) /\ ((v4_yellow18 (k4_waybel34 A)) /\ ((v1_yellow21 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (v3_yellow21 (k4_waybel34 A)))))))))))))))) (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k4_waybel34 A))) /\ ((v2_altcat_1 (k4_waybel34 A)) /\ ((v6_altcat_1 (k4_waybel34 A)) /\ ((v11_altcat_1 (k4_waybel34 A)) /\ ((v12_altcat_1 (k4_waybel34 A)) /\ ((v2_yellow21 (k4_waybel34 A)) /\ (l2_altcat_1 (k4_waybel34 A)))))))))) (All A, ((-. (v2_setfam_1 A)) => (-. (v1_xboole_0 A)))) (All A, ((-. (v2_setfam_1 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v9_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v1_altcat_2 (k5_waybel34 A)) /\ ((v2_yellow18 (k5_waybel34 A)) /\ ((v3_yellow18 (k5_waybel34 A)) /\ ((v4_yellow18 (k5_waybel34 A)) /\ ((v1_yellow21 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (v3_yellow21 (k5_waybel34 A)))))))))))))))) (All A, ((-. (v1_xboole_0 A)) => ((-. (v3_struct_0 (k5_waybel34 A))) /\ ((v2_altcat_1 (k5_waybel34 A)) /\ ((v6_altcat_1 (k5_waybel34 A)) /\ ((v11_altcat_1 (k5_waybel34 A)) /\ ((v12_altcat_1 (k5_waybel34 A)) /\ ((v2_yellow21 (k5_waybel34 A)) /\ (l2_altcat_1 (k5_waybel34 A)))))))))) (All A, ((-. (v2_setfam_1 A)) => ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (m2_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)))))) (All A, ((-. (v2_setfam_1 A)) => ((v6_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v8_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v9_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v11_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v12_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v14_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ ((v16_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A)) /\ (v21_functor0 (k6_waybel34 A) (k4_waybel34 A) (k5_waybel34 A))))))))))) ### NotAllEx 56 % 3.16/3.35 % SZS output end Proof % 3.16/3.35 (* END-PROOF *) %------------------------------------------------------------------------------