%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : CSR039+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 : n019.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:13 EDT 2022 % Result : Theorem 241.68s 241.88s % Output : Proof 241.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : CSR039+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 : n019.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 : Fri Jun 10 19:06:55 EDT 2022 % 0.12/0.33 % CPUTime : % 241.68/241.88 % SZS status Theorem % 241.68/241.88 (* PROOF-FOUND *) % 241.68/241.88 (* BEGIN-PROOF *) % 241.68/241.88 % SZS output start Proof % 241.68/241.88 1. (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (-. (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663))) ### Axiom % 241.68/241.88 2. ((c_tptpcol_11_18631) != (c_tptpcol_11_18631)) ### NotEqual % 241.68/241.88 3. (-. (genls (c_tptpcol_13_18664) (c_tptpcol_11_18631))) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) ### Trans 1 2 % 241.68/241.88 4. ((c_tptpcol_10_18567) != (c_tptpcol_10_18567)) ### NotEqual % 241.68/241.88 5. (-. (genls (c_tptpcol_13_18664) (c_tptpcol_10_18567))) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) ### Trans 3 4 % 241.68/241.88 6. ((c_tptpcol_9_18439) != (c_tptpcol_9_18439)) ### NotEqual % 241.68/241.88 7. (-. (genls (c_tptpcol_13_18664) (c_tptpcol_9_18439))) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) ### Trans 5 6 % 241.68/241.88 8. ((c_tptpcol_8_18438) != (c_tptpcol_8_18438)) ### NotEqual % 241.68/241.88 9. (-. (genls (c_tptpcol_13_18664) (c_tptpcol_8_18438))) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) ### Trans 7 8 % 241.68/241.88 10. ((c_tptpcol_7_18437) != (c_tptpcol_7_18437)) ### NotEqual % 241.68/241.88 11. (-. (genls (c_tptpcol_13_18664) (c_tptpcol_7_18437))) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) ### Trans 9 10 % 241.68/241.88 12. ((c_tptpcol_6_18436) != (c_tptpcol_6_18436)) ### NotEqual % 241.68/241.88 13. (-. (genls (c_tptpcol_13_18664) (c_tptpcol_6_18436))) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) ### Trans 11 12 % 241.68/241.88 14. ((c_tptpcol_5_16388) != (c_tptpcol_5_16388)) ### NotEqual % 241.68/241.88 15. (-. (genls (c_tptpcol_13_18664) (c_tptpcol_5_16388))) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) ### Trans 13 14 % 241.68/241.88 16. ((c_tptpcol_4_16387) != (c_tptpcol_4_16387)) ### NotEqual % 241.68/241.88 17. (-. (genls (c_tptpcol_13_18664) (c_tptpcol_4_16387))) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) ### Trans 15 16 % 241.68/241.88 18. ((c_tptpcol_3_16386) != (c_tptpcol_3_16386)) ### NotEqual % 241.68/241.88 19. (-. (genls (c_tptpcol_13_18664) (c_tptpcol_3_16386))) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) ### Trans 17 18 % 241.68/241.88 20. ((c_tptpcol_2_2) != (c_tptpcol_2_2)) ### NotEqual % 241.68/241.88 21. (-. (genls (c_tptpcol_13_18664) (c_tptpcol_2_2))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) ### Trans 19 20 % 241.68/241.88 22. ((c_tptpcol_1_1) != (c_tptpcol_1_1)) ### NotEqual % 241.68/241.88 23. (-. (genls (c_tptpcol_13_18664) (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_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) ### Trans 21 22 % 241.68/241.88 24. (-. (collection (c_tptpcol_13_18664))) (collection (c_tptpcol_13_18664)) ### Axiom % 241.68/241.88 25. ((genls (c_tptpcol_13_18664) (c_tptpcol_1_1)) => (collection (c_tptpcol_13_18664))) (-. (collection (c_tptpcol_13_18664))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) ### Imply 23 24 % 241.68/241.88 26. (All ARG2, ((genls (c_tptpcol_13_18664) ARG2) => (collection (c_tptpcol_13_18664)))) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (-. (collection (c_tptpcol_13_18664))) ### All 25 % 241.68/241.88 27. (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) (-. (collection (c_tptpcol_13_18664))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) ### All 26 % 241.68/241.88 28. (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (-. (disjointwith (c_tptpcol_1_65536) (c_tptpcol_1_1))) ### Sym(disjointwith) % 241.68/241.88 29. (-. (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664))) (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664)) ### Axiom % 241.68/241.88 30. (((disjointwith (c_tptpcol_1_65536) (c_tptpcol_1_1)) /\ (genls (c_tptpcol_13_18664) (c_tptpcol_1_1))) => (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664))) (-. (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (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_1_65536)) ### DisjTree 28 23 29 % 241.68/241.88 31. (All NEW, (((disjointwith (c_tptpcol_1_65536) (c_tptpcol_1_1)) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith (c_tptpcol_1_65536) NEW))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (-. (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664))) ### All 30 % 241.68/241.88 32. (genls (c_tptpcol_13_18664) (c_tptpcol_13_18664)) (-. (genls (c_tptpcol_13_18664) (c_tptpcol_13_18664))) ### Axiom % 241.68/241.88 33. (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664)) (-. (disjointwith (c_tptpcol_13_18664) (c_tptpcol_1_65536))) ### Sym(disjointwith) % 241.68/241.88 34. (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (-. (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774))) ### Axiom % 241.68/241.88 35. ((c_tptpcol_13_93766) != (c_tptpcol_13_93766)) ### NotEqual % 241.68/241.88 36. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_13_93766))) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) ### Trans 34 35 % 241.68/241.88 37. ((c_tptpcol_12_93765) != (c_tptpcol_12_93765)) ### NotEqual % 241.68/241.88 38. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_12_93765))) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) ### Trans 36 37 % 241.68/241.88 39. ((c_tptpcol_11_93764) != (c_tptpcol_11_93764)) ### NotEqual % 241.68/241.88 40. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_11_93764))) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) ### Trans 38 39 % 241.68/241.88 41. ((c_tptpcol_10_93700) != (c_tptpcol_10_93700)) ### NotEqual % 241.68/241.88 42. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_10_93700))) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) ### Trans 40 41 % 241.68/241.88 43. ((c_tptpcol_9_93699) != (c_tptpcol_9_93699)) ### NotEqual % 241.68/241.88 44. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_9_93699))) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) ### Trans 42 43 % 241.68/241.88 45. ((c_tptpcol_8_93698) != (c_tptpcol_8_93698)) ### NotEqual % 241.68/241.88 46. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_8_93698))) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) ### Trans 44 45 % 241.68/241.88 47. ((c_tptpcol_7_93186) != (c_tptpcol_7_93186)) ### NotEqual % 241.68/241.88 48. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_7_93186))) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) ### Trans 46 47 % 241.68/241.88 49. ((c_tptpcol_6_92162) != (c_tptpcol_6_92162)) ### NotEqual % 241.68/241.88 50. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_6_92162))) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) ### Trans 48 49 % 241.68/241.88 51. ((c_tptpcol_5_90114) != (c_tptpcol_5_90114)) ### NotEqual % 241.68/241.88 52. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_5_90114))) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) ### Trans 50 51 % 241.68/241.88 53. ((c_tptpcol_4_90113) != (c_tptpcol_4_90113)) ### NotEqual % 241.68/241.88 54. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_4_90113))) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) ### Trans 52 53 % 241.68/241.88 55. ((c_tptpcol_3_81921) != (c_tptpcol_3_81921)) ### NotEqual % 241.68/241.88 56. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_3_81921))) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) ### Trans 54 55 % 241.68/241.88 57. ((c_tptpcol_2_65537) != (c_tptpcol_2_65537)) ### NotEqual % 241.68/241.88 58. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_2_65537))) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) ### Trans 56 57 % 241.68/241.88 59. ((c_tptpcol_1_65536) != (c_tptpcol_1_65536)) ### NotEqual % 241.68/241.88 60. (-. (genls (c_tptpcol_15_93775) (c_tptpcol_1_65536))) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) ### Trans 58 59 % 241.68/241.88 61. (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) (disjointwith (c_tptpcol_13_18664) (c_tptpcol_15_93775)) ### Sym(disjointwith) % 241.68/241.88 62. (((disjointwith (c_tptpcol_13_18664) (c_tptpcol_1_65536)) /\ (genls (c_tptpcol_15_93775) (c_tptpcol_1_65536))) => (disjointwith (c_tptpcol_13_18664) (c_tptpcol_15_93775))) (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664)) ### DisjTree 33 60 61 % 241.68/241.88 63. (All NEW, (((disjointwith (c_tptpcol_13_18664) (c_tptpcol_1_65536)) /\ (genls NEW (c_tptpcol_1_65536))) => (disjointwith (c_tptpcol_13_18664) NEW))) (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) ### All 62 % 241.68/241.88 64. (All OLD, (All NEW, (((disjointwith (c_tptpcol_13_18664) OLD) /\ (genls NEW OLD)) => (disjointwith (c_tptpcol_13_18664) NEW)))) (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664)) ### All 63 % 241.68/241.88 65. (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) ### All 64 % 241.68/241.88 66. (((disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664)) /\ (genls (c_tptpcol_13_18664) (c_tptpcol_13_18664))) => (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664))) (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_tptpcol_13_18664) (c_tptpcol_13_18664)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (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_1_65536)) (All NEW, (((disjointwith (c_tptpcol_1_65536) (c_tptpcol_1_1)) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith (c_tptpcol_1_65536) NEW))) ### DisjTree 31 32 65 % 241.68/241.88 67. (All NEW, (((disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664)) /\ (genls NEW (c_tptpcol_13_18664))) => (disjointwith (c_tptpcol_1_65536) NEW))) (All NEW, (((disjointwith (c_tptpcol_1_65536) (c_tptpcol_1_1)) /\ (genls NEW (c_tptpcol_1_1))) => (disjointwith (c_tptpcol_1_65536) NEW))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_13_18664) (c_tptpcol_13_18664)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) ### All 66 % 241.68/241.88 68. (All OLD, (All NEW, (((disjointwith (c_tptpcol_1_65536) OLD) /\ (genls NEW OLD)) => (disjointwith (c_tptpcol_1_65536) NEW)))) (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_tptpcol_13_18664) (c_tptpcol_13_18664)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (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_1_65536)) (All NEW, (((disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664)) /\ (genls NEW (c_tptpcol_13_18664))) => (disjointwith (c_tptpcol_1_65536) NEW))) ### All 67 % 241.68/241.88 69. (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_13_18664) (c_tptpcol_13_18664)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) (All OLD, (All NEW, (((disjointwith (c_tptpcol_1_65536) OLD) /\ (genls NEW OLD)) => (disjointwith (c_tptpcol_1_65536) NEW)))) ### All 68 % 241.68/241.88 70. (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_tptpcol_13_18664) (c_tptpcol_13_18664)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (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_1_65536)) ### All 69 % 241.68/241.88 71. ((collection (c_tptpcol_13_18664)) => (genls (c_tptpcol_13_18664) (c_tptpcol_13_18664))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) ### Imply 27 70 % 241.68/241.88 72. (All X, ((collection X) => (genls X X))) (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (-. (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) ### All 71 % 241.68/241.88 73. (-. ((mtvisible (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn (s_http_wwwpoweripodsearchinfobrown_ipodhtml))) (c_translation_7))) => (disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664)))) (disjointwith (c_tptpcol_1_1) (c_tptpcol_1_65536)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) (genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) (genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) (genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) (genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) (genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) (genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) (genls (c_tptpcol_15_93775) (c_tptpcol_14_93774)) (genls (c_tptpcol_13_93766) (c_tptpcol_12_93765)) (genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) (genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) (genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) (genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) (genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) (genls (c_tptpcol_2_2) (c_tptpcol_1_1)) (genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) (genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) (genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) (genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) (genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) (genls (c_tptpcol_13_18664) (c_tptpcol_12_18663)) (genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) (genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) (genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) (genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) (genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) (All X, ((collection X) => (genls X X))) ### NotImply 72 % 241.68/241.88 % SZS output end Proof % 241.68/241.88 (* END-PROOF *) %------------------------------------------------------------------------------