%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : CSR044+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 : n028.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:18 EDT 2022 % Result : Theorem 0.20s 0.42s % Output : Proof 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : CSR044+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 : n028.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 07:13:48 EDT 2022 % 0.12/0.33 % CPUTime : % 0.20/0.42 % SZS status Theorem % 0.20/0.42 (* PROOF-FOUND *) % 0.20/0.42 (* BEGIN-PROOF *) % 0.20/0.42 % SZS output start Proof % 0.20/0.42 1. (mtvisible (c_tptp_member3633_mt)) (-. (mtvisible (c_tptp_member3633_mt))) ### Axiom % 0.20/0.42 2. (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) (-. (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt))) ### Axiom % 0.20/0.42 3. ((c_cyclistsmt) != (c_cyclistsmt)) ### NotEqual % 0.20/0.42 4. (-. (genlmt (c_tptp_member3633_mt) (c_cyclistsmt))) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) ### Trans 2 3 % 0.20/0.42 5. (-. (mtvisible (c_cyclistsmt))) (mtvisible (c_cyclistsmt)) ### Axiom % 0.20/0.42 6. (((mtvisible (c_tptp_member3633_mt)) /\ (genlmt (c_tptp_member3633_mt) (c_cyclistsmt))) => (mtvisible (c_cyclistsmt))) (-. (mtvisible (c_cyclistsmt))) (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (mtvisible (c_tptp_member3633_mt)) ### DisjTree 1 4 5 % 0.20/0.42 7. (All GENLMT, (((mtvisible (c_tptp_member3633_mt)) /\ (genlmt (c_tptp_member3633_mt) GENLMT)) => (mtvisible GENLMT))) (mtvisible (c_tptp_member3633_mt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) (-. (mtvisible (c_cyclistsmt))) ### All 6 % 0.20/0.42 8. (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) (-. (mtvisible (c_cyclistsmt))) (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (mtvisible (c_tptp_member3633_mt)) ### All 7 % 0.20/0.42 9. (-. ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) zenon_X0) /\ (tptpcol_16_29490 zenon_X0)))) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) (-. (mtvisible (c_cyclistsmt))) (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) ### NotImply 8 % 0.20/0.42 10. (-. (Ex X, ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) X) /\ (tptpcol_16_29490 X))))) (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) (-. (mtvisible (c_cyclistsmt))) (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) ### NotExists 9 % 0.20/0.42 11. (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) (-. (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90))) ### Axiom % 0.20/0.42 12. (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) (-. (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90))) ### Axiom % 0.20/0.42 13. (isa (c_tptpexecutionbyfiringsquad_90) (c_executionbyfiringsquad)) (-. (isa (c_tptpexecutionbyfiringsquad_90) (c_executionbyfiringsquad))) ### Axiom % 0.20/0.42 14. (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (-. (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) ### Axiom % 0.20/0.42 15. (-. (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (c_tptpcol_16_29490))) (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (c_tptpcol_16_29490)) ### Axiom % 0.20/0.42 16. (((isa (c_tptpexecutionbyfiringsquad_90) (c_executionbyfiringsquad)) /\ (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) => (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (c_tptpcol_16_29490))) (-. (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (c_tptpcol_16_29490))) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (isa (c_tptpexecutionbyfiringsquad_90) (c_executionbyfiringsquad)) ### DisjTree 13 14 15 % 0.20/0.42 17. (All DEPCOL, (((isa (c_tptpexecutionbyfiringsquad_90) (c_executionbyfiringsquad)) /\ (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) DEPCOL)) => (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) DEPCOL) DEPCOL))) (isa (c_tptpexecutionbyfiringsquad_90) (c_executionbyfiringsquad)) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (-. (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (c_tptpcol_16_29490))) ### All 16 % 0.20/0.42 18. (All PRED, (All DEPCOL, (((isa (c_tptpexecutionbyfiringsquad_90) (c_executionbyfiringsquad)) /\ (relationallexists PRED (c_executionbyfiringsquad) DEPCOL)) => (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) PRED (c_executionbyfiringsquad) DEPCOL) DEPCOL)))) (-. (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (c_tptpcol_16_29490))) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (isa (c_tptpexecutionbyfiringsquad_90) (c_executionbyfiringsquad)) ### All 17 % 0.20/0.42 19. (All INDEPCOL, (All PRED, (All DEPCOL, (((isa (c_tptpexecutionbyfiringsquad_90) INDEPCOL) /\ (relationallexists PRED INDEPCOL DEPCOL)) => (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) PRED INDEPCOL DEPCOL) DEPCOL))))) (isa (c_tptpexecutionbyfiringsquad_90) (c_executionbyfiringsquad)) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (-. (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (c_tptpcol_16_29490))) ### All 18 % 0.20/0.42 20. (All TERM, (All INDEPCOL, (All PRED, (All DEPCOL, (((isa TERM INDEPCOL) /\ (relationallexists PRED INDEPCOL DEPCOL)) => (isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL)))))) (-. (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (c_tptpcol_16_29490))) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (isa (c_tptpexecutionbyfiringsquad_90) (c_executionbyfiringsquad)) ### All 19 % 0.20/0.42 21. ((executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) => (isa (c_tptpexecutionbyfiringsquad_90) (c_executionbyfiringsquad))) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (-. (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (c_tptpcol_16_29490))) (All TERM, (All INDEPCOL, (All PRED, (All DEPCOL, (((isa TERM INDEPCOL) /\ (relationallexists PRED INDEPCOL DEPCOL)) => (isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL)))))) (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) ### Imply 12 20 % 0.20/0.42 22. (All X, ((executionbyfiringsquad X) => (isa X (c_executionbyfiringsquad)))) (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) (All TERM, (All INDEPCOL, (All PRED, (All DEPCOL, (((isa TERM INDEPCOL) /\ (relationallexists PRED INDEPCOL DEPCOL)) => (isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL)))))) (-. (isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (c_tptpcol_16_29490))) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) ### All 21 % 0.20/0.42 23. (tptp_9_720 (c_tptpexecutionbyfiringsquad_90) (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) (-. (tptp_9_720 (c_tptpexecutionbyfiringsquad_90) (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)))) ### Axiom % 0.20/0.42 24. (tptpcol_16_29490 (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) (-. (tptpcol_16_29490 (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)))) ### Axiom % 0.20/0.42 25. (-. ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) /\ (tptpcol_16_29490 (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))))) (tptpcol_16_29490 (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) (tptp_9_720 (c_tptpexecutionbyfiringsquad_90) (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) ### NotAnd 23 24 % 0.20/0.42 26. (-. ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) /\ (tptpcol_16_29490 (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)))))) (tptp_9_720 (c_tptpexecutionbyfiringsquad_90) (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) (tptpcol_16_29490 (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) ### NotImply 25 % 0.20/0.42 27. (-. (Ex X, ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) X) /\ (tptpcol_16_29490 X))))) (tptpcol_16_29490 (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) (tptp_9_720 (c_tptpexecutionbyfiringsquad_90) (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) ### NotExists 26 % 0.20/0.42 28. ((isa (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (c_tptpcol_16_29490)) => (tptpcol_16_29490 (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)))) (tptp_9_720 (c_tptpexecutionbyfiringsquad_90) (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) (-. (Ex X, ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) X) /\ (tptpcol_16_29490 X))))) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (All TERM, (All INDEPCOL, (All PRED, (All DEPCOL, (((isa TERM INDEPCOL) /\ (relationallexists PRED INDEPCOL DEPCOL)) => (isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL)))))) (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) (All X, ((executionbyfiringsquad X) => (isa X (c_executionbyfiringsquad)))) ### Imply 22 27 % 0.20/0.42 29. (All X, ((isa X (c_tptpcol_16_29490)) => (tptpcol_16_29490 X))) (All X, ((executionbyfiringsquad X) => (isa X (c_executionbyfiringsquad)))) (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) (All TERM, (All INDEPCOL, (All PRED, (All DEPCOL, (((isa TERM INDEPCOL) /\ (relationallexists PRED INDEPCOL DEPCOL)) => (isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL)))))) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (-. (Ex X, ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) X) /\ (tptpcol_16_29490 X))))) (tptp_9_720 (c_tptpexecutionbyfiringsquad_90) (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) ### All 28 % 0.20/0.42 30. (((mtvisible (c_cyclistsmt)) /\ (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90))) => (tptp_9_720 (c_tptpexecutionbyfiringsquad_90) (f_relationallexistsfn (c_tptpexecutionbyfiringsquad_90) (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)))) (-. (Ex X, ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) X) /\ (tptpcol_16_29490 X))))) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (All TERM, (All INDEPCOL, (All PRED, (All DEPCOL, (((isa TERM INDEPCOL) /\ (relationallexists PRED INDEPCOL DEPCOL)) => (isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL)))))) (All X, ((executionbyfiringsquad X) => (isa X (c_executionbyfiringsquad)))) (All X, ((isa X (c_tptpcol_16_29490)) => (tptpcol_16_29490 X))) (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) (mtvisible (c_tptp_member3633_mt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) ### DisjTree 8 11 29 % 0.20/0.42 31. (All TERM, (((mtvisible (c_cyclistsmt)) /\ (executionbyfiringsquad TERM)) => (tptp_9_720 TERM (f_relationallexistsfn TERM (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))))) (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (mtvisible (c_tptp_member3633_mt)) (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) (All X, ((isa X (c_tptpcol_16_29490)) => (tptpcol_16_29490 X))) (All X, ((executionbyfiringsquad X) => (isa X (c_executionbyfiringsquad)))) (All TERM, (All INDEPCOL, (All PRED, (All DEPCOL, (((isa TERM INDEPCOL) /\ (relationallexists PRED INDEPCOL DEPCOL)) => (isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL)))))) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (-. (Ex X, ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) X) /\ (tptpcol_16_29490 X))))) ### All 30 % 0.20/0.42 32. (-. ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) zenon_X0) /\ (tptpcol_16_29490 zenon_X0)))) (-. (Ex X, ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) X) /\ (tptpcol_16_29490 X))))) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (All TERM, (All INDEPCOL, (All PRED, (All DEPCOL, (((isa TERM INDEPCOL) /\ (relationallexists PRED INDEPCOL DEPCOL)) => (isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL)))))) (All X, ((executionbyfiringsquad X) => (isa X (c_executionbyfiringsquad)))) (All X, ((isa X (c_tptpcol_16_29490)) => (tptpcol_16_29490 X))) (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) (All TERM, (((mtvisible (c_cyclistsmt)) /\ (executionbyfiringsquad TERM)) => (tptp_9_720 TERM (f_relationallexistsfn TERM (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))))) ### NotImply 31 % 0.20/0.42 33. (All TERM, (((mtvisible (c_cyclistsmt)) /\ (executionbyfiringsquad TERM)) => (tptp_9_720 TERM (f_relationallexistsfn TERM (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))))) (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) (All X, ((isa X (c_tptpcol_16_29490)) => (tptpcol_16_29490 X))) (All X, ((executionbyfiringsquad X) => (isa X (c_executionbyfiringsquad)))) (All TERM, (All INDEPCOL, (All PRED, (All DEPCOL, (((isa TERM INDEPCOL) /\ (relationallexists PRED INDEPCOL DEPCOL)) => (isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL)))))) (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490)) (-. (Ex X, ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) X) /\ (tptpcol_16_29490 X))))) ### NotExists 32 % 0.20/0.42 34. ((mtvisible (c_cyclistsmt)) => (relationallexists (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))) (All TERM, (All INDEPCOL, (All PRED, (All DEPCOL, (((isa TERM INDEPCOL) /\ (relationallexists PRED INDEPCOL DEPCOL)) => (isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL)))))) (All X, ((executionbyfiringsquad X) => (isa X (c_executionbyfiringsquad)))) (All X, ((isa X (c_tptpcol_16_29490)) => (tptpcol_16_29490 X))) (executionbyfiringsquad (c_tptpexecutionbyfiringsquad_90)) (All TERM, (((mtvisible (c_cyclistsmt)) /\ (executionbyfiringsquad TERM)) => (tptp_9_720 TERM (f_relationallexistsfn TERM (c_tptp_9_720) (c_executionbyfiringsquad) (c_tptpcol_16_29490))))) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3633_mt) (c_tptp_spindleheadmt)) (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) (-. (Ex X, ((mtvisible (c_tptp_member3633_mt)) => ((tptp_9_720 (c_tptpexecutionbyfiringsquad_90) X) /\ (tptpcol_16_29490 X))))) ### Imply 10 33 % 0.20/0.42 % SZS output end Proof % 0.20/0.42 (* END-PROOF *) %------------------------------------------------------------------------------