%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : CSR063+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:36 EDT 2022 % Result : Theorem 63.59s 63.80s % Output : Proof 63.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : CSR063+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 : n020.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 01:45:20 EDT 2022 % 0.12/0.33 % CPUTime : % 63.59/63.80 % SZS status Theorem % 63.59/63.80 (* PROOF-FOUND *) % 63.59/63.80 (* BEGIN-PROOF *) % 63.59/63.80 % SZS output start Proof % 63.59/63.80 1. (genls (c_inanimateobject) (c_partiallytangible)) (-. (genls (c_inanimateobject) (c_partiallytangible))) ### Axiom % 63.59/63.80 2. (disjointwith (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (-. (disjointwith (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) ### Sym(disjointwith) % 63.59/63.80 3. (collection (c_inanimateobject)) (-. (collection (c_inanimateobject))) ### Axiom % 63.59/63.80 4. (disjointwith (c_intangible) (c_partiallytangible)) (-. (disjointwith (c_intangible) (c_partiallytangible))) ### Axiom % 63.59/63.80 5. (genls (c_inanimateobject) (c_partiallytangible)) (-. (genls (c_inanimateobject) (c_partiallytangible))) ### Axiom % 63.59/63.80 6. (-. (disjointwith (c_intangible) (c_inanimateobject))) (disjointwith (c_intangible) (c_inanimateobject)) ### Axiom % 63.59/63.80 7. (((disjointwith (c_intangible) (c_partiallytangible)) /\ (genls (c_inanimateobject) (c_partiallytangible))) => (disjointwith (c_intangible) (c_inanimateobject))) (-. (disjointwith (c_intangible) (c_inanimateobject))) (genls (c_inanimateobject) (c_partiallytangible)) (disjointwith (c_intangible) (c_partiallytangible)) ### DisjTree 4 5 6 % 63.59/63.80 8. (All NEW, (((disjointwith (c_intangible) (c_partiallytangible)) /\ (genls NEW (c_partiallytangible))) => (disjointwith (c_intangible) NEW))) (disjointwith (c_intangible) (c_partiallytangible)) (genls (c_inanimateobject) (c_partiallytangible)) (-. (disjointwith (c_intangible) (c_inanimateobject))) ### All 7 % 63.59/63.80 9. (genls (c_inanimateobject) (c_inanimateobject)) (-. (genls (c_inanimateobject) (c_inanimateobject))) ### Axiom % 63.59/63.80 10. (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (-. (no (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949))) ### Sym(no) % 63.59/63.80 11. (disjointwith (c_intangible) (c_inanimateobject)) (-. (disjointwith (c_inanimateobject) (c_intangible))) ### Sym(disjointwith) % 63.59/63.80 12. (genls (c_setorcollection) (c_mathematicalthing)) (-. (genls (c_setorcollection) (c_mathematicalthing))) ### Axiom % 63.59/63.80 13. ((c_mathematicalorcomputationalthing) != (c_mathematicalorcomputationalthing)) ### NotEqual % 63.59/63.80 14. (-. (genls (c_setorcollection) (c_mathematicalorcomputationalthing))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) ### Trans 12 13 % 63.59/63.80 15. ((c_intangible) != (c_intangible)) ### NotEqual % 63.59/63.80 16. (-. (genls (c_setorcollection) (c_intangible))) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) ### Trans 14 15 % 63.59/63.80 17. (disjointwith (c_inanimateobject) (c_setorcollection)) (-. (disjointwith (c_setorcollection) (c_inanimateobject))) ### Sym(disjointwith) % 63.59/63.80 18. (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (-. (genls (c_inanimateobject_nonnatural) (c_inanimateobject))) ### Axiom % 63.59/63.80 19. (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (-. (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949))) ### Axiom % 63.59/63.80 20. (-. (setorcollection (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) (setorcollection (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### Axiom % 63.59/63.80 21. ((few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) => (setorcollection (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) (-. (setorcollection (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) ### Imply 19 20 % 63.59/63.80 22. (All ARG2, ((few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) ARG2) => (setorcollection (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (-. (setorcollection (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) ### All 21 % 63.59/63.80 23. (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (-. (setorcollection (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) ### All 22 % 63.59/63.80 24. (-. (isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_setorcollection))) (isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_setorcollection)) ### Axiom % 63.59/63.80 25. ((setorcollection (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) => (isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_setorcollection))) (-. (isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_setorcollection))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) ### Imply 23 24 % 63.59/63.80 26. (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (-. (isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_setorcollection))) ### All 25 % 63.59/63.80 27. (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (-. (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) ### Axiom % 63.59/63.80 28. (-. (artifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) (artifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### Axiom % 63.59/63.80 29. ((computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) => (artifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) (-. (artifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### Imply 27 28 % 63.59/63.80 30. (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (-. (artifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) ### All 29 % 63.59/63.80 31. (-. (inanimateobject_nonnatural (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) (inanimateobject_nonnatural (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### Axiom % 63.59/63.80 32. ((artifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) => (inanimateobject_nonnatural (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) (-. (inanimateobject_nonnatural (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) ### Imply 30 31 % 63.59/63.80 33. (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (-. (inanimateobject_nonnatural (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) ### All 32 % 63.59/63.80 34. (-. (isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_inanimateobject_nonnatural))) (isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_inanimateobject_nonnatural)) ### Axiom % 63.59/63.80 35. ((inanimateobject_nonnatural (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) => (isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_inanimateobject_nonnatural))) (-. (isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_inanimateobject_nonnatural))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) ### Imply 33 34 % 63.59/63.80 36. (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (-. (isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_inanimateobject_nonnatural))) ### All 35 % 63.59/63.80 37. (disjointwith (c_setorcollection) (c_inanimateobject_nonnatural)) (-. (disjointwith (c_setorcollection) (c_inanimateobject_nonnatural))) ### Axiom % 63.59/63.80 38. (-. ((isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_setorcollection)) /\ ((isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_inanimateobject_nonnatural)) /\ (disjointwith (c_setorcollection) (c_inanimateobject_nonnatural))))) (disjointwith (c_setorcollection) (c_inanimateobject_nonnatural)) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) ### DisjTree 26 36 37 % 63.59/63.80 39. (All COL2, (-. ((isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_setorcollection)) /\ ((isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) COL2) /\ (disjointwith (c_setorcollection) COL2))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (disjointwith (c_setorcollection) (c_inanimateobject_nonnatural)) ### All 38 % 63.59/63.80 40. (All COL1, (All COL2, (-. ((isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) COL1) /\ ((isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) COL2) /\ (disjointwith COL1 COL2)))))) (disjointwith (c_setorcollection) (c_inanimateobject_nonnatural)) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) ### All 39 % 63.59/63.80 41. (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (disjointwith (c_setorcollection) (c_inanimateobject_nonnatural)) ### All 40 % 63.59/63.80 42. (((disjointwith (c_setorcollection) (c_inanimateobject)) /\ (genls (c_inanimateobject_nonnatural) (c_inanimateobject))) => (disjointwith (c_setorcollection) (c_inanimateobject_nonnatural))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (disjointwith (c_inanimateobject) (c_setorcollection)) ### DisjTree 17 18 41 % 63.59/63.80 43. (All NEW, (((disjointwith (c_setorcollection) (c_inanimateobject)) /\ (genls NEW (c_inanimateobject))) => (disjointwith (c_setorcollection) NEW))) (disjointwith (c_inanimateobject) (c_setorcollection)) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### All 42 % 63.59/63.80 44. (All OLD, (All NEW, (((disjointwith (c_setorcollection) OLD) /\ (genls NEW OLD)) => (disjointwith (c_setorcollection) NEW)))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (disjointwith (c_inanimateobject) (c_setorcollection)) ### All 43 % 63.59/63.80 45. (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (disjointwith (c_inanimateobject) (c_setorcollection)) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### All 44 % 63.59/63.80 46. (((disjointwith (c_inanimateobject) (c_intangible)) /\ (genls (c_setorcollection) (c_intangible))) => (disjointwith (c_inanimateobject) (c_setorcollection))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (disjointwith (c_intangible) (c_inanimateobject)) ### DisjTree 11 16 45 % 63.59/63.80 47. (All NEW, (((disjointwith (c_inanimateobject) (c_intangible)) /\ (genls NEW (c_intangible))) => (disjointwith (c_inanimateobject) NEW))) (disjointwith (c_intangible) (c_inanimateobject)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### All 46 % 63.59/63.80 48. (All OLD, (All NEW, (((disjointwith (c_inanimateobject) OLD) /\ (genls NEW OLD)) => (disjointwith (c_inanimateobject) NEW)))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (disjointwith (c_intangible) (c_inanimateobject)) ### All 47 % 63.59/63.80 49. (disjointwith (c_intangible) (c_inanimateobject)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### All 48 % 63.59/63.80 50. ((no (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) => (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (disjointwith (c_intangible) (c_inanimateobject)) (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### Imply 10 49 % 63.59/63.80 51. (All ARG2, ((no (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) ARG2) => (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) ARG2))) (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (disjointwith (c_intangible) (c_inanimateobject)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### All 50 % 63.59/63.80 52. (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (disjointwith (c_intangible) (c_inanimateobject)) (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### All 51 % 63.59/63.80 53. (((disjointwith (c_intangible) (c_inanimateobject)) /\ (genls (c_inanimateobject) (c_inanimateobject))) => (disjointwith (c_intangible) (c_inanimateobject))) (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (genls (c_inanimateobject) (c_inanimateobject)) (genls (c_inanimateobject) (c_partiallytangible)) (disjointwith (c_intangible) (c_partiallytangible)) (All NEW, (((disjointwith (c_intangible) (c_partiallytangible)) /\ (genls NEW (c_partiallytangible))) => (disjointwith (c_intangible) NEW))) ### DisjTree 8 9 52 % 63.59/63.81 54. (All NEW, (((disjointwith (c_intangible) (c_inanimateobject)) /\ (genls NEW (c_inanimateobject))) => (disjointwith (c_intangible) NEW))) (All NEW, (((disjointwith (c_intangible) (c_partiallytangible)) /\ (genls NEW (c_partiallytangible))) => (disjointwith (c_intangible) NEW))) (disjointwith (c_intangible) (c_partiallytangible)) (genls (c_inanimateobject) (c_partiallytangible)) (genls (c_inanimateobject) (c_inanimateobject)) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) ### All 53 % 63.59/63.81 55. (All OLD, (All NEW, (((disjointwith (c_intangible) OLD) /\ (genls NEW OLD)) => (disjointwith (c_intangible) NEW)))) (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (genls (c_inanimateobject) (c_inanimateobject)) (genls (c_inanimateobject) (c_partiallytangible)) (disjointwith (c_intangible) (c_partiallytangible)) (All NEW, (((disjointwith (c_intangible) (c_partiallytangible)) /\ (genls NEW (c_partiallytangible))) => (disjointwith (c_intangible) NEW))) ### All 54 % 63.59/63.81 56. (disjointwith (c_intangible) (c_partiallytangible)) (genls (c_inanimateobject) (c_partiallytangible)) (genls (c_inanimateobject) (c_inanimateobject)) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OLD, (All NEW, (((disjointwith (c_intangible) OLD) /\ (genls NEW OLD)) => (disjointwith (c_intangible) NEW)))) ### All 55 % 63.59/63.81 57. (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (genls (c_inanimateobject) (c_inanimateobject)) (genls (c_inanimateobject) (c_partiallytangible)) (disjointwith (c_intangible) (c_partiallytangible)) ### All 56 % 63.59/63.81 58. ((collection (c_inanimateobject)) => (genls (c_inanimateobject) (c_inanimateobject))) (disjointwith (c_intangible) (c_partiallytangible)) (genls (c_inanimateobject) (c_partiallytangible)) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (collection (c_inanimateobject)) ### Imply 3 57 % 63.59/63.81 59. (All X, ((collection X) => (genls X X))) (collection (c_inanimateobject)) (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (genls (c_inanimateobject) (c_partiallytangible)) (disjointwith (c_intangible) (c_partiallytangible)) ### All 58 % 63.59/63.81 60. ((disjointwith (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) => (no (c_tptpcol_16_118949) (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))) (disjointwith (c_intangible) (c_partiallytangible)) (genls (c_inanimateobject) (c_partiallytangible)) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (collection (c_inanimateobject)) (All X, ((collection X) => (genls X X))) (disjointwith (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) ### Imply 2 59 % 63.59/63.81 61. (All ARG2, ((disjointwith (c_tptpcol_16_118949) ARG2) => (no (c_tptpcol_16_118949) ARG2))) (disjointwith (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All X, ((collection X) => (genls X X))) (collection (c_inanimateobject)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (genls (c_inanimateobject) (c_partiallytangible)) (disjointwith (c_intangible) (c_partiallytangible)) ### All 60 % 63.59/63.81 62. ((genls (c_inanimateobject) (c_partiallytangible)) => (collection (c_inanimateobject))) (disjointwith (c_intangible) (c_partiallytangible)) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (All X, ((collection X) => (genls X X))) (disjointwith (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All ARG2, ((disjointwith (c_tptpcol_16_118949) ARG2) => (no (c_tptpcol_16_118949) ARG2))) (genls (c_inanimateobject) (c_partiallytangible)) ### Imply 1 61 % 63.59/63.81 63. (All ARG2, ((genls (c_inanimateobject) ARG2) => (collection (c_inanimateobject)))) (genls (c_inanimateobject) (c_partiallytangible)) (All ARG2, ((disjointwith (c_tptpcol_16_118949) ARG2) => (no (c_tptpcol_16_118949) ARG2))) (disjointwith (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All X, ((collection X) => (genls X X))) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (disjointwith (c_intangible) (c_partiallytangible)) ### All 62 % 63.62/63.82 64. (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) (disjointwith (c_intangible) (c_partiallytangible)) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (All X, ((collection X) => (genls X X))) (disjointwith (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All ARG2, ((disjointwith (c_tptpcol_16_118949) ARG2) => (no (c_tptpcol_16_118949) ARG2))) (genls (c_inanimateobject) (c_partiallytangible)) ### All 63 % 63.62/63.82 65. (All ARG1, (All ARG2, ((disjointwith ARG1 ARG2) => (no ARG1 ARG2)))) (genls (c_inanimateobject) (c_partiallytangible)) (disjointwith (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) (All X, ((collection X) => (genls X X))) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (disjointwith (c_intangible) (c_partiallytangible)) (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) ### All 64 % 63.62/63.82 66. (-. (-. (disjointwith (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)))) (All INS, (All ARG2, ((genls INS ARG2) => (collection INS)))) (disjointwith (c_intangible) (c_partiallytangible)) (All ARG1, (All ARG2, ((no ARG1 ARG2) => (few ARG1 ARG2)))) (computerdataartifact (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))) (All OBJ, ((computerdataartifact OBJ) => (artifact OBJ))) (All OBJ, ((artifact OBJ) => (inanimateobject_nonnatural OBJ))) (All X, ((inanimateobject_nonnatural X) => (isa X (c_inanimateobject_nonnatural)))) (All INS, (All ARG2, ((few INS ARG2) => (setorcollection INS)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (genls (c_inanimateobject_nonnatural) (c_inanimateobject)) (All ARG1, (All OLD, (All NEW, (((disjointwith ARG1 OLD) /\ (genls NEW OLD)) => (disjointwith ARG1 NEW))))) (genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) (genls (c_setorcollection) (c_mathematicalthing)) (genls (c_mathematicalorcomputationalthing) (c_intangible)) (All X, ((collection X) => (genls X X))) (genls (c_inanimateobject) (c_partiallytangible)) (All ARG1, (All ARG2, ((disjointwith ARG1 ARG2) => (no ARG1 ARG2)))) ### NotNot 65 % 63.62/63.82 % SZS output end Proof % 63.62/63.82 (* END-PROOF *) %------------------------------------------------------------------------------