%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : CSR061+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 : n020.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:34 EDT 2022 % Result : Theorem 21.93s 22.15s % Output : Proof 21.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : CSR061+1 : TPTP v8.1.0. Released v3.4.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.11/0.33 % Computer : n020.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Sat Jun 11 06:39:50 EDT 2022 % 0.11/0.33 % CPUTime : % 21.93/22.15 % SZS status Theorem % 21.93/22.15 (* PROOF-FOUND *) % 21.93/22.15 (* BEGIN-PROOF *) % 21.93/22.15 % SZS output start Proof % 21.93/22.15 1. (disjointwith (c_tptpcol_3_98305) (c_tptpcol_3_114688)) (-. (disjointwith (c_tptpcol_3_98305) (c_tptpcol_3_114688))) ### Axiom % 21.93/22.15 2. (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (-. (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117))) ### Axiom % 21.93/22.15 3. ((c_tptpcol_12_118116) != (c_tptpcol_12_118116)) ### NotEqual % 21.93/22.15 4. (-. (genls (c_tptpcol_14_118118) (c_tptpcol_12_118116))) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) ### Trans 2 3 % 21.93/22.15 5. ((c_tptpcol_11_118084) != (c_tptpcol_11_118084)) ### NotEqual % 21.93/22.15 6. (-. (genls (c_tptpcol_14_118118) (c_tptpcol_11_118084))) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) ### Trans 4 5 % 21.93/22.15 7. ((c_tptpcol_10_118020) != (c_tptpcol_10_118020)) ### NotEqual % 21.93/22.15 8. (-. (genls (c_tptpcol_14_118118) (c_tptpcol_10_118020))) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) ### Trans 6 7 % 21.93/22.15 9. ((c_tptpcol_9_118019) != (c_tptpcol_9_118019)) ### NotEqual % 21.93/22.15 10. (-. (genls (c_tptpcol_14_118118) (c_tptpcol_9_118019))) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) ### Trans 8 9 % 21.93/22.15 11. ((c_tptpcol_8_117763) != (c_tptpcol_8_117763)) ### NotEqual % 21.93/22.15 12. (-. (genls (c_tptpcol_14_118118) (c_tptpcol_8_117763))) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) ### Trans 10 11 % 21.93/22.15 13. ((c_tptpcol_7_117762) != (c_tptpcol_7_117762)) ### NotEqual % 21.93/22.15 14. (-. (genls (c_tptpcol_14_118118) (c_tptpcol_7_117762))) (genls (c_tptpcol_8_117763) (c_tptpcol_7_117762)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) ### Trans 12 13 % 21.93/22.15 15. ((c_tptpcol_6_116738) != (c_tptpcol_6_116738)) ### NotEqual % 21.93/22.15 16. (-. (genls (c_tptpcol_14_118118) (c_tptpcol_6_116738))) (genls (c_tptpcol_7_117762) (c_tptpcol_6_116738)) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_8_117763) (c_tptpcol_7_117762)) ### Trans 14 15 % 21.93/22.15 17. ((c_tptpcol_5_114690) != (c_tptpcol_5_114690)) ### NotEqual % 21.93/22.15 18. (-. (genls (c_tptpcol_14_118118) (c_tptpcol_5_114690))) (genls (c_tptpcol_6_116738) (c_tptpcol_5_114690)) (genls (c_tptpcol_8_117763) (c_tptpcol_7_117762)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) (genls (c_tptpcol_7_117762) (c_tptpcol_6_116738)) ### Trans 16 17 % 21.93/22.15 19. ((c_tptpcol_4_114689) != (c_tptpcol_4_114689)) ### NotEqual % 21.93/22.15 20. (-. (genls (c_tptpcol_14_118118) (c_tptpcol_4_114689))) (genls (c_tptpcol_5_114690) (c_tptpcol_4_114689)) (genls (c_tptpcol_7_117762) (c_tptpcol_6_116738)) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_8_117763) (c_tptpcol_7_117762)) (genls (c_tptpcol_6_116738) (c_tptpcol_5_114690)) ### Trans 18 19 % 21.93/22.15 21. ((c_tptpcol_3_114688) != (c_tptpcol_3_114688)) ### NotEqual % 21.93/22.15 22. (-. (genls (c_tptpcol_14_118118) (c_tptpcol_3_114688))) (genls (c_tptpcol_4_114689) (c_tptpcol_3_114688)) (genls (c_tptpcol_6_116738) (c_tptpcol_5_114690)) (genls (c_tptpcol_8_117763) (c_tptpcol_7_117762)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) (genls (c_tptpcol_7_117762) (c_tptpcol_6_116738)) (genls (c_tptpcol_5_114690) (c_tptpcol_4_114689)) ### Trans 20 21 % 21.93/22.15 23. (disjointwith (c_tptpcol_3_98305) (c_tptpcol_14_118118)) (-. (disjointwith (c_tptpcol_3_98305) (c_tptpcol_14_118118))) ### Axiom % 21.93/22.15 24. (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (-. (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665))) ### Axiom % 21.93/22.15 25. ((c_tptpcol_6_112641) != (c_tptpcol_6_112641)) ### NotEqual % 21.93/22.15 26. (-. (genls (c_tptpcol_8_114177) (c_tptpcol_6_112641))) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) ### Trans 24 25 % 21.93/22.15 27. ((c_tptpcol_5_110593) != (c_tptpcol_5_110593)) ### NotEqual % 21.93/22.15 28. (-. (genls (c_tptpcol_8_114177) (c_tptpcol_5_110593))) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) ### Trans 26 27 % 21.93/22.15 29. ((c_tptpcol_4_106497) != (c_tptpcol_4_106497)) ### NotEqual % 21.93/22.15 30. (-. (genls (c_tptpcol_8_114177) (c_tptpcol_4_106497))) (genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) ### Trans 28 29 % 21.93/22.15 31. ((c_tptpcol_3_98305) != (c_tptpcol_3_98305)) ### NotEqual % 21.93/22.15 32. (-. (genls (c_tptpcol_8_114177) (c_tptpcol_3_98305))) (genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) ### Trans 30 31 % 21.93/22.15 33. (-. (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))) (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118)) ### Axiom % 21.93/22.15 34. (((disjointwith (c_tptpcol_3_98305) (c_tptpcol_14_118118)) /\ (genls (c_tptpcol_8_114177) (c_tptpcol_3_98305))) => (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))) (-. (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))) (genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) (genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) (disjointwith (c_tptpcol_3_98305) (c_tptpcol_14_118118)) ### DisjTree 23 32 33 % 21.93/22.15 35. (All NEW, (((disjointwith (c_tptpcol_3_98305) (c_tptpcol_14_118118)) /\ (genls NEW (c_tptpcol_3_98305))) => (disjointwith NEW (c_tptpcol_14_118118)))) (disjointwith (c_tptpcol_3_98305) (c_tptpcol_14_118118)) (genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) (-. (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))) ### All 34 % 21.93/22.15 36. (All ARG2, (All NEW, (((disjointwith (c_tptpcol_3_98305) ARG2) /\ (genls NEW (c_tptpcol_3_98305))) => (disjointwith NEW ARG2)))) (-. (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))) (genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) (genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) (disjointwith (c_tptpcol_3_98305) (c_tptpcol_14_118118)) ### All 35 % 21.93/22.16 37. (((disjointwith (c_tptpcol_3_98305) (c_tptpcol_3_114688)) /\ (genls (c_tptpcol_14_118118) (c_tptpcol_3_114688))) => (disjointwith (c_tptpcol_3_98305) (c_tptpcol_14_118118))) (genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) (-. (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_3_98305) ARG2) /\ (genls NEW (c_tptpcol_3_98305))) => (disjointwith NEW ARG2)))) (genls (c_tptpcol_5_114690) (c_tptpcol_4_114689)) (genls (c_tptpcol_7_117762) (c_tptpcol_6_116738)) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_8_117763) (c_tptpcol_7_117762)) (genls (c_tptpcol_6_116738) (c_tptpcol_5_114690)) (genls (c_tptpcol_4_114689) (c_tptpcol_3_114688)) (disjointwith (c_tptpcol_3_98305) (c_tptpcol_3_114688)) ### DisjTree 1 22 36 % 21.93/22.16 38. (All NEW, (((disjointwith (c_tptpcol_3_98305) (c_tptpcol_3_114688)) /\ (genls NEW (c_tptpcol_3_114688))) => (disjointwith (c_tptpcol_3_98305) NEW))) (disjointwith (c_tptpcol_3_98305) (c_tptpcol_3_114688)) (genls (c_tptpcol_4_114689) (c_tptpcol_3_114688)) (genls (c_tptpcol_6_116738) (c_tptpcol_5_114690)) (genls (c_tptpcol_8_117763) (c_tptpcol_7_117762)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) (genls (c_tptpcol_7_117762) (c_tptpcol_6_116738)) (genls (c_tptpcol_5_114690) (c_tptpcol_4_114689)) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_3_98305) ARG2) /\ (genls NEW (c_tptpcol_3_98305))) => (disjointwith NEW ARG2)))) (-. (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))) (genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) (genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) ### All 37 % 21.93/22.16 39. (All OLD, (All NEW, (((disjointwith (c_tptpcol_3_98305) OLD) /\ (genls NEW OLD)) => (disjointwith (c_tptpcol_3_98305) NEW)))) (genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) (-. (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_3_98305) ARG2) /\ (genls NEW (c_tptpcol_3_98305))) => (disjointwith NEW ARG2)))) (genls (c_tptpcol_5_114690) (c_tptpcol_4_114689)) (genls (c_tptpcol_7_117762) (c_tptpcol_6_116738)) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_8_117763) (c_tptpcol_7_117762)) (genls (c_tptpcol_6_116738) (c_tptpcol_5_114690)) (genls (c_tptpcol_4_114689) (c_tptpcol_3_114688)) (disjointwith (c_tptpcol_3_98305) (c_tptpcol_3_114688)) ### All 38 % 21.93/22.16 40. (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (disjointwith (c_tptpcol_3_98305) (c_tptpcol_3_114688)) (genls (c_tptpcol_4_114689) (c_tptpcol_3_114688)) (genls (c_tptpcol_6_116738) (c_tptpcol_5_114690)) (genls (c_tptpcol_8_117763) (c_tptpcol_7_117762)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) (genls (c_tptpcol_7_117762) (c_tptpcol_6_116738)) (genls (c_tptpcol_5_114690) (c_tptpcol_4_114689)) (All ARG2, (All NEW, (((disjointwith (c_tptpcol_3_98305) ARG2) /\ (genls NEW (c_tptpcol_3_98305))) => (disjointwith NEW ARG2)))) (-. (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))) (genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) (genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) ### All 39 % 21.93/22.16 41. (All OLD, (All ARG2, (All NEW, (((disjointwith OLD ARG2) /\ (genls NEW OLD)) => (disjointwith NEW ARG2))))) (genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) (-. (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))) (genls (c_tptpcol_5_114690) (c_tptpcol_4_114689)) (genls (c_tptpcol_7_117762) (c_tptpcol_6_116738)) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_8_117763) (c_tptpcol_7_117762)) (genls (c_tptpcol_6_116738) (c_tptpcol_5_114690)) (genls (c_tptpcol_4_114689) (c_tptpcol_3_114688)) (disjointwith (c_tptpcol_3_98305) (c_tptpcol_3_114688)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) ### All 40 % 21.93/22.16 42. (-. ((mtvisible (c_timehasnoendmt)) => (disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118)))) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (disjointwith (c_tptpcol_3_98305) (c_tptpcol_3_114688)) (genls (c_tptpcol_4_114689) (c_tptpcol_3_114688)) (genls (c_tptpcol_6_116738) (c_tptpcol_5_114690)) (genls (c_tptpcol_8_117763) (c_tptpcol_7_117762)) (genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) (genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) (genls (c_tptpcol_14_118118) (c_tptpcol_13_118117)) (genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) (genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) (genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) (genls (c_tptpcol_7_117762) (c_tptpcol_6_116738)) (genls (c_tptpcol_5_114690) (c_tptpcol_4_114689)) (genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) (genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) (genls (c_tptpcol_8_114177) (c_tptpcol_7_113665)) (genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) (genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) (All OLD, (All ARG2, (All NEW, (((disjointwith OLD ARG2) /\ (genls NEW OLD)) => (disjointwith NEW ARG2))))) ### NotImply 41 % 21.93/22.16 % SZS output end Proof % 21.93/22.16 (* END-PROOF *) %------------------------------------------------------------------------------