%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : CSR064+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 : n029.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:37 EDT 2022 % Result : Theorem 11.21s 11.40s % Output : Proof 11.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : CSR064+1 : TPTP v8.1.0. Released v3.4.0. % 0.00/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 9 21:19:22 EDT 2022 % 0.12/0.33 % CPUTime : % 11.21/11.40 % SZS status Theorem % 11.21/11.40 (* PROOF-FOUND *) % 11.21/11.40 (* BEGIN-PROOF *) % 11.21/11.40 % SZS output start Proof % 11.21/11.40 1. (genls (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (-. (genls (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743))) ### Axiom % 11.21/11.40 2. (subsetof (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (-. (subsetof (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743))) ### Axiom % 11.21/11.40 3. (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (-. (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))))) ### Axiom % 11.21/11.40 4. (-. (isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_individual))) (isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_individual)) ### Axiom % 11.21/11.40 5. ((individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) => (isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_individual))) (-. (isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_individual))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) ### Imply 3 4 % 11.21/11.40 6. (All X, ((individual X) => (isa X (c_individual)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (-. (isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_individual))) ### All 5 % 11.21/11.40 7. (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (-. (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743))) ### Axiom % 11.21/11.40 8. (-. (setorcollection (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))))) (setorcollection (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) ### Axiom % 11.21/11.40 9. ((most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) => (setorcollection (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))))) (-. (setorcollection (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))))) (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) ### Imply 7 8 % 11.21/11.40 10. (All ARG2, ((most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) ARG2) => (setorcollection (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))))) (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (-. (setorcollection (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))))) ### All 9 % 11.21/11.40 11. (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (-. (setorcollection (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))))) (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) ### All 10 % 11.21/11.40 12. (-. (isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_setorcollection))) (isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_setorcollection)) ### Axiom % 11.21/11.40 13. ((setorcollection (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) => (isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_setorcollection))) (-. (isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_setorcollection))) (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) ### Imply 11 12 % 11.21/11.40 14. (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (-. (isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_setorcollection))) ### All 13 % 11.21/11.40 15. (disjointwith (c_individual) (c_setorcollection)) (-. (disjointwith (c_individual) (c_setorcollection))) ### Axiom % 11.21/11.40 16. (-. ((isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_individual)) /\ ((isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_setorcollection)) /\ (disjointwith (c_individual) (c_setorcollection))))) (disjointwith (c_individual) (c_setorcollection)) (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (All X, ((individual X) => (isa X (c_individual)))) ### DisjTree 6 14 15 % 11.21/11.40 17. (All COL2, (-. ((isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_individual)) /\ ((isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) COL2) /\ (disjointwith (c_individual) COL2))))) (All X, ((individual X) => (isa X (c_individual)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (disjointwith (c_individual) (c_setorcollection)) ### All 16 % 11.21/11.40 18. (All COL1, (All COL2, (-. ((isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) COL1) /\ ((isa (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) COL2) /\ (disjointwith COL1 COL2)))))) (disjointwith (c_individual) (c_setorcollection)) (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (All X, ((individual X) => (isa X (c_individual)))) ### All 17 % 11.21/11.40 19. (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((individual X) => (isa X (c_individual)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (disjointwith (c_individual) (c_setorcollection)) ### All 18 % 11.21/11.40 20. ((subsetof (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) => (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743))) (disjointwith (c_individual) (c_setorcollection)) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (All X, ((individual X) => (isa X (c_individual)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (subsetof (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) ### Imply 2 19 % 11.21/11.40 21. (All ARG2, ((subsetof (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) ARG2) => (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) ARG2))) (subsetof (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((individual X) => (isa X (c_individual)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (disjointwith (c_individual) (c_setorcollection)) ### All 20 % 11.21/11.41 22. ((genls (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) => (subsetof (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743))) (disjointwith (c_individual) (c_setorcollection)) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (All X, ((individual X) => (isa X (c_individual)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All ARG2, ((subsetof (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) ARG2) => (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) ARG2))) (genls (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) ### Imply 1 21 % 11.21/11.41 23. (All ARG2, ((genls (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) ARG2) => (subsetof (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) ARG2))) (genls (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (All ARG2, ((subsetof (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) ARG2) => (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) ARG2))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((individual X) => (isa X (c_individual)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (disjointwith (c_individual) (c_setorcollection)) ### All 22 % 11.21/11.41 24. (All ARG1, (All ARG2, ((genls ARG1 ARG2) => (subsetof ARG1 ARG2)))) (disjointwith (c_individual) (c_setorcollection)) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (All X, ((individual X) => (isa X (c_individual)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All ARG2, ((subsetof (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) ARG2) => (most (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) ARG2))) (genls (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) ### All 23 % 11.21/11.41 25. (All ARG1, (All ARG2, ((subsetof ARG1 ARG2) => (most ARG1 ARG2)))) (genls (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All X, ((individual X) => (isa X (c_individual)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (disjointwith (c_individual) (c_setorcollection)) (All ARG1, (All ARG2, ((genls ARG1 ARG2) => (subsetof ARG1 ARG2)))) ### All 24 % 11.21/11.41 26. (-. (-. (genls (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))) (c_tptpcol_15_74743)))) (All ARG1, (All ARG2, ((genls ARG1 ARG2) => (subsetof ARG1 ARG2)))) (disjointwith (c_individual) (c_setorcollection)) (All ARG1, (All ARG2, ((most ARG1 ARG2) => (setorcollection ARG1)))) (All X, ((setorcollection X) => (isa X (c_setorcollection)))) (individual (f_urlfn (f_urlfn (s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))) (All X, ((individual X) => (isa X (c_individual)))) (All OBJ, (All COL1, (All COL2, (-. ((isa OBJ COL1) /\ ((isa OBJ COL2) /\ (disjointwith COL1 COL2))))))) (All ARG1, (All ARG2, ((subsetof ARG1 ARG2) => (most ARG1 ARG2)))) ### NotNot 25 % 11.21/11.41 % SZS output end Proof % 11.21/11.41 (* END-PROOF *) %------------------------------------------------------------------------------