%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : CSR036+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 : n017.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 : Fri Jul 15 23:29:10 EDT 2022 % Result : Theorem 240.50s 240.72s % Output : Proof 240.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : CSR036+1 : TPTP v8.1.0. Released v3.4.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n017.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 : Sat Jun 11 13:00:06 EDT 2022 % 0.12/0.33 % CPUTime : % 240.50/240.72 % SZS status Theorem % 240.50/240.72 (* PROOF-FOUND *) % 240.50/240.72 (* BEGIN-PROOF *) % 240.50/240.72 % SZS output start Proof % 240.50/240.72 1. (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (-. (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707))) ### Axiom % 240.50/240.72 2. ((c_tptpcol_6_71683) != (c_tptpcol_6_71683)) ### NotEqual % 240.50/240.72 3. (-. (genls (c_tptpcol_8_72708) (c_tptpcol_6_71683))) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) ### Trans 1 2 % 240.50/240.72 4. ((c_tptpcol_5_69635) != (c_tptpcol_5_69635)) ### NotEqual % 240.50/240.72 5. (-. (genls (c_tptpcol_8_72708) (c_tptpcol_5_69635))) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) ### Trans 3 4 % 240.50/240.72 6. (-. (collection (c_tptpcol_8_72708))) (collection (c_tptpcol_8_72708)) ### Axiom % 240.50/240.72 7. ((genls (c_tptpcol_8_72708) (c_tptpcol_5_69635)) => (collection (c_tptpcol_8_72708))) (-. (collection (c_tptpcol_8_72708))) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) ### Imply 5 6 % 240.50/240.72 8. (All ARG2, ((genls (c_tptpcol_8_72708) ARG2) => (collection (c_tptpcol_8_72708)))) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (-. (collection (c_tptpcol_8_72708))) ### All 7 % 240.50/240.72 9. (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) (-. (collection (c_tptpcol_8_72708))) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) ### All 8 % 240.50/240.72 10. (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (-. (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536))) ### Axiom % 240.50/240.72 11. ((c_tptpcol_4_65539) != (c_tptpcol_4_65539)) ### NotEqual % 240.50/240.72 12. (-. (genls (c_tptpcol_8_72708) (c_tptpcol_4_65539))) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) ### Trans 5 11 % 240.50/240.72 13. ((c_tptpcol_3_65538) != (c_tptpcol_3_65538)) ### NotEqual % 240.50/240.72 14. (-. (genls (c_tptpcol_8_72708) (c_tptpcol_3_65538))) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) ### Trans 12 13 % 240.50/240.72 15. ((c_tptpcol_2_65537) != (c_tptpcol_2_65537)) ### NotEqual % 240.50/240.72 16. (-. (genls (c_tptpcol_8_72708) (c_tptpcol_2_65537))) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) ### Trans 14 15 % 240.50/240.72 17. ((c_tptpcol_1_65536) != (c_tptpcol_1_65536)) ### NotEqual % 240.50/240.72 18. (-. (genls (c_tptpcol_8_72708) (c_tptpcol_1_65536))) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) ### Trans 16 17 % 240.50/240.72 19. (-. (disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708)) ### Axiom % 240.50/240.72 20. (((disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) /\ (genls (c_tptpcol_8_72708) (c_tptpcol_1_65536))) => (disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708))) (-. (disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708))) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) ### DisjTree 10 18 19 % 240.50/240.72 21. (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) /\ (genls NEW (c_tptpcol_1_65536))) => (disjointwith (c_tptpcol_1_1) NEW))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (-. (disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708))) ### All 20 % 240.50/240.72 22. (genls (c_tptpcol_8_72708) (c_tptpcol_8_72708)) (-. (genls (c_tptpcol_8_72708) (c_tptpcol_8_72708))) ### Axiom % 240.50/240.72 23. (disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708)) (-. (disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708))) ### Axiom % 240.50/240.72 24. (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (-. (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710))) ### Axiom % 240.50/240.72 25. ((c_tptpcol_9_72709) != (c_tptpcol_9_72709)) ### NotEqual % 240.50/240.72 26. (-. (genls (c_tptpcol_11_72774) (c_tptpcol_9_72709))) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) ### Trans 24 25 % 240.50/240.72 27. ((c_tptpcol_8_72708) != (c_tptpcol_8_72708)) ### NotEqual % 240.50/240.72 28. (-. (genls (c_tptpcol_11_72774) (c_tptpcol_8_72708))) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) ### Trans 26 27 % 240.50/240.72 29. (disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774)) (-. (disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774))) ### Axiom % 240.50/240.72 30. (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (-. (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793))) ### Axiom % 240.50/240.72 31. ((c_tptpcol_14_72792) != (c_tptpcol_14_72792)) ### NotEqual % 240.50/240.72 32. (-. (genls (c_tptpcol_16_72795) (c_tptpcol_14_72792))) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) ### Trans 30 31 % 240.50/240.72 33. ((c_tptpcol_13_72791) != (c_tptpcol_13_72791)) ### NotEqual % 240.50/240.72 34. (-. (genls (c_tptpcol_16_72795) (c_tptpcol_13_72791))) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) ### Trans 32 33 % 240.50/240.72 35. ((c_tptpcol_12_72775) != (c_tptpcol_12_72775)) ### NotEqual % 240.50/240.72 36. (-. (genls (c_tptpcol_16_72795) (c_tptpcol_12_72775))) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) ### Trans 34 35 % 240.50/240.72 37. ((c_tptpcol_11_72774) != (c_tptpcol_11_72774)) ### NotEqual % 240.50/240.72 38. (-. (genls (c_tptpcol_16_72795) (c_tptpcol_11_72774))) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) ### Trans 36 37 % 240.50/240.72 39. (disjointwith (c_tptpcol_1_1) (c_tptpcol_16_72795)) (-. (disjointwith (c_tptpcol_1_1) (c_tptpcol_16_72795))) ### Axiom % 240.50/240.72 40. (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (-. (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072))) ### Axiom % 240.50/240.72 41. ((c_tptpcol_13_22071) != (c_tptpcol_13_22071)) ### NotEqual % 240.50/240.72 42. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_13_22071))) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) ### Trans 40 41 % 240.50/240.72 43. ((c_tptpcol_12_22055) != (c_tptpcol_12_22055)) ### NotEqual % 240.50/240.72 44. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_12_22055))) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) ### Trans 42 43 % 240.50/240.72 45. ((c_tptpcol_11_22023) != (c_tptpcol_11_22023)) ### NotEqual % 240.50/240.72 46. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_11_22023))) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) ### Trans 44 45 % 240.50/240.72 47. ((c_tptpcol_10_22022) != (c_tptpcol_10_22022)) ### NotEqual % 240.50/240.72 48. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_10_22022))) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) ### Trans 46 47 % 240.50/240.72 49. ((c_tptpcol_9_22021) != (c_tptpcol_9_22021)) ### NotEqual % 240.50/240.72 50. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_9_22021))) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) ### Trans 48 49 % 240.50/240.72 51. ((c_tptpcol_8_22020) != (c_tptpcol_8_22020)) ### NotEqual % 240.50/240.72 52. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_8_22020))) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) ### Trans 50 51 % 240.50/240.72 53. ((c_tptpcol_7_21508) != (c_tptpcol_7_21508)) ### NotEqual % 240.50/240.72 54. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_7_21508))) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) ### Trans 52 53 % 240.50/240.72 55. ((c_tptpcol_6_20484) != (c_tptpcol_6_20484)) ### NotEqual % 240.50/240.72 56. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_6_20484))) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) ### Trans 54 55 % 240.50/240.72 57. ((c_tptpcol_5_20483) != (c_tptpcol_5_20483)) ### NotEqual % 240.50/240.72 58. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_5_20483))) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) ### Trans 56 57 % 240.50/240.72 59. ((c_tptpcol_4_16387) != (c_tptpcol_4_16387)) ### NotEqual % 240.50/240.72 60. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_4_16387))) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) ### Trans 58 59 % 240.50/240.72 61. ((c_tptpcol_3_16386) != (c_tptpcol_3_16386)) ### NotEqual % 240.50/240.72 62. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_3_16386))) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) ### Trans 60 61 % 240.50/240.72 63. ((c_tptpcol_2_2) != (c_tptpcol_2_2)) ### NotEqual % 240.50/240.72 64. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_2_2))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) ### Trans 62 63 % 240.50/240.72 65. ((c_tptpcol_1_1) != (c_tptpcol_1_1)) ### NotEqual % 240.50/240.72 66. (-. (genls (c_tptpcol_15_22076) (c_tptpcol_1_1))) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) ### Trans 64 65 % 240.50/240.72 67. (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795)) ### Axiom % 240.50/240.72 68. (((disjointwith (c_tptpcol_1_1) (c_tptpcol_16_72795)) /\ (genls (c_tptpcol_15_22076) (c_tptpcol_1_1))) => (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (disjointwith (c_tptpcol_1_1) (c_tptpcol_16_72795)) ### DisjTree 39 66 67 % 240.50/240.72 69. (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_16_72795)) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW (c_tptpcol_16_72795)))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_16_72795)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) ### All 68 % 240.50/240.72 70. (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (disjointwith (c_tptpcol_1_1) (c_tptpcol_16_72795)) ### All 69 % 240.50/240.72 71. (((disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774)) /\ (genls (c_tptpcol_16_72795) (c_tptpcol_11_72774))) => (disjointwith (c_tptpcol_1_1) (c_tptpcol_16_72795))) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774)) ### DisjTree 29 38 70 % 240.50/240.72 72. (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774)) /\ (genls NEW (c_tptpcol_11_72774))) => (disjointwith (c_tptpcol_1_1) NEW))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) ### All 71 % 240.50/240.72 73. (((disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708)) /\ (genls (c_tptpcol_11_72774) (c_tptpcol_8_72708))) => (disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774))) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774)) /\ (genls NEW (c_tptpcol_11_72774))) => (disjointwith (c_tptpcol_1_1) NEW))) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708)) ### DisjTree 23 28 72 % 240.50/240.72 74. (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708)) /\ (genls NEW (c_tptpcol_8_72708))) => (disjointwith (c_tptpcol_1_1) NEW))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708)) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774)) /\ (genls NEW (c_tptpcol_11_72774))) => (disjointwith (c_tptpcol_1_1) NEW))) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) ### All 73 % 240.50/240.72 75. (((disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708)) /\ (genls (c_tptpcol_8_72708) (c_tptpcol_8_72708))) => (disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708))) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774)) /\ (genls NEW (c_tptpcol_11_72774))) => (disjointwith (c_tptpcol_1_1) NEW))) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708)) /\ (genls NEW (c_tptpcol_8_72708))) => (disjointwith (c_tptpcol_1_1) NEW))) (genls (c_tptpcol_8_72708) (c_tptpcol_8_72708)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) /\ (genls NEW (c_tptpcol_1_65536))) => (disjointwith (c_tptpcol_1_1) NEW))) ### DisjTree 21 22 74 % 240.50/240.72 76. (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) /\ (genls NEW (c_tptpcol_1_65536))) => (disjointwith (c_tptpcol_1_1) NEW))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_8_72708) (c_tptpcol_8_72708)) (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_8_72708)) /\ (genls NEW (c_tptpcol_8_72708))) => (disjointwith (c_tptpcol_1_1) NEW))) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774)) /\ (genls NEW (c_tptpcol_11_72774))) => (disjointwith (c_tptpcol_1_1) NEW))) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) ### All 75 % 240.50/240.72 77. (All OLD, (All NEW, (((disjointwith (c_tptpcol_1_1) OLD) /\ (genls NEW OLD)) => (disjointwith (c_tptpcol_1_1) NEW)))) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_11_72774)) /\ (genls NEW (c_tptpcol_11_72774))) => (disjointwith (c_tptpcol_1_1) NEW))) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (genls (c_tptpcol_8_72708) (c_tptpcol_8_72708)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) /\ (genls NEW (c_tptpcol_1_65536))) => (disjointwith (c_tptpcol_1_1) NEW))) ### All 76 % 240.50/240.72 78. (All NEW, (((disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) /\ (genls NEW (c_tptpcol_1_65536))) => (disjointwith (c_tptpcol_1_1) NEW))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_8_72708) (c_tptpcol_8_72708)) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (All OLD, (All NEW, (((disjointwith (c_tptpcol_1_1) OLD) /\ (genls NEW OLD)) => (disjointwith (c_tptpcol_1_1) NEW)))) ### All 77 % 240.50/240.72 79. (All OLD, (All NEW, (((disjointwith (c_tptpcol_1_1) OLD) /\ (genls NEW OLD)) => (disjointwith (c_tptpcol_1_1) NEW)))) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (genls (c_tptpcol_8_72708) (c_tptpcol_8_72708)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) ### All 78 % 240.50/240.72 80. ((collection (c_tptpcol_8_72708)) => (genls (c_tptpcol_8_72708) (c_tptpcol_8_72708))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (All OLD, (All NEW, (((disjointwith (c_tptpcol_1_1) OLD) /\ (genls NEW OLD)) => (disjointwith (c_tptpcol_1_1) NEW)))) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) ### Imply 9 79 % 240.50/240.72 81. (All X, ((collection X) => (genls X X))) (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (All OLD, (All NEW, (((disjointwith (c_tptpcol_1_1) OLD) /\ (genls NEW OLD)) => (disjointwith (c_tptpcol_1_1) NEW)))) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) ### All 80 % 240.50/240.72 82. (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_1_1) ARG2) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith NEW ARG2)))) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) (All X, ((collection X) => (genls X X))) ### All 81 % 240.50/240.72 83. (All OLD, (All ARG2, (All NEW, (((disjointwith OLD ARG2) /\ (genls NEW OLD)) => (disjointwith NEW ARG2))))) (All X, ((collection X) => (genls X X))) (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (-. (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) ### All 82 % 240.50/240.72 84. (-. ((mtvisible (c_tptp_member974_mt)) => (disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795)))) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) (genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) (genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) (genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) (genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) (genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) (genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) (genls (c_tptpcol_14_72792) (c_tptpcol_13_72791)) (genls (c_tptpcol_16_72795) (c_tptpcol_15_72793)) (genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) (genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) (genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) (genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) (genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) (genls (c_tptpcol_15_22076) (c_tptpcol_14_22072)) (genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) (genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) (genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) (genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) (genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) (genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) (genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) (All X, ((collection X) => (genls X X))) (All OLD, (All ARG2, (All NEW, (((disjointwith OLD ARG2) /\ (genls NEW OLD)) => (disjointwith NEW ARG2))))) ### NotImply 83 % 240.50/240.73 % SZS output end Proof % 240.50/240.73 (* END-PROOF *) %------------------------------------------------------------------------------