%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PHI022+1 : TPTP v8.1.2. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n007.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 : 300s
% DateTime : Fri May 19 11:46:44 EDT 2023
% Result : Theorem 0.29s 1.38s
% Output : Proof 0.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : PHI022+1 : TPTP v8.1.2. Released v7.4.0.
% 0.10/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n007.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 20:54:53 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.29/1.38
% 0.29/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.29/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.29/1.38 %-----------------------------------------------------
% 0.29/1.38 ncf(matrix, plain, [(913 ^ _96350) ^ [] : [-(substance(911 ^ []))], (915 ^ _96350) ^ [] : [exists(911 ^ [])], (884 ^ _96350) ^ [_123773] : [substance(_123773), -(being(_123773))], (890 ^ _96350) ^ [_123959] : [inItself(_123959), -(selfCaused(_123959))], (896 ^ _96350) ^ [_124145] : [being(_124145), -(hasEssence(_124145))], (902 ^ _96350) ^ [_124311] : [-(exists(_124311)), essenceInvExistence(_124311), hasEssence(_124311)], (798 ^ _96350) ^ [_121030, _121032] : [exists(_121032), -(existsIn(_121032, _121032)), 805 ^ _96350 : [(806 ^ _96350) ^ [] : [-(existsIn(_121032, _121030))], (808 ^ _96350) ^ [] : [_121032 = _121030]]], (810 ^ _96350) ^ [_121356, _121358] : [-(exists(_121358)), 811 ^ _96350 : [(812 ^ _96350) ^ [] : [existsIn(_121358, _121358)], (814 ^ _96350) ^ [] : [existsIn(_121358, _121356), -(_121358 = _121356)]]], (822 ^ _96350) ^ [_121732, _121734] : [-(conceivedThru(_121734, _121734)), 825 ^ _96350 : [(826 ^ _96350) ^ [] : [-(conceivedThru(_121734, _121732))], (828 ^ _96350) ^ [] : [_121734 = _121732]]], (830 ^ _96350) ^ [_122021, _122023] : [definiteCause(_122023), 833 ^ _96350 : [(834 ^ _96350) ^ [] : [-(effectNecessarilyFollowsFrom(_122021, _122023))], (836 ^ _96350) ^ [] : [-(definiteCause(_122023)), effectNecessarilyFollowsFrom(_122021, _122023)]]], (842 ^ _96350) ^ [_122424, _122426] : [knowledgeOfEffect(_122426, _122424), -(knowledgeOfACause(_122426))], (848 ^ _96350) ^ [_122584, _122586] : [knowledgeOfACause(_122586), -(knowledgeOfEffect(_122586, _122584))], (854 ^ _96350) ^ [_122794, _122796] : [haveNothingInCommon(_122796, _122794), 857 ^ _96350 : [(858 ^ _96350) ^ [] : [canBeUnderstoodInTermsOf(_122796, _122794)], (860 ^ _96350) ^ [] : [canBeUnderstoodInTermsOf(_122794, _122796)], (862 ^ _96350) ^ [] : [conceptionInvolves(_122796, _122794)], (864 ^ _96350) ^ [] : [conceptionInvolves(_122794, _122796)]]], (878 ^ _96350) ^ [_123570] : [canBeConceivedAsNonExisting(_123570), essenceInvExistence(_123570)], (866 ^ _96350) ^ [_123231, _123233] : [trueIdea(_123233), 869 ^ _96350 : [(870 ^ _96350) ^ [] : [-(correspondWith(_123233, _123231))], (872 ^ _96350) ^ [] : [-(ideateOf(_123231, _123233)), -(objectOf(_123231, _123233))]]], (576 ^ _96350) ^ [_114373] : [selfCaused(_114373), 579 ^ _96350 : [(580 ^ _96350) ^ [] : [-(essenceInvExistence(_114373))], (582 ^ _96350) ^ [] : [-(natureConcOnlyByExistence(_114373))]]], (584 ^ _96350) ^ [_114596] : [-(selfCaused(_114596)), essenceInvExistence(_114596), natureConcOnlyByExistence(_114596)], (594 ^ _96350) ^ [_114910, _114912] : [finiteAfterItsKind(_114912), 597 ^ _96350 : [(598 ^ _96350) ^ [] : [-(canBeLimitedBy(_114912, _114910))], (600 ^ _96350) ^ [] : [-(sameKind(_114912, _114910))]]], (602 ^ _96350) ^ [_115145, _115147] : [-(finiteAfterItsKind(_115147)), canBeLimitedBy(_115147, _115145), sameKind(_115147, _115145)], (612 ^ _96350) ^ [_115459] : [substance(_115459), 615 ^ _96350 : [(616 ^ _96350) ^ [] : [-(inItself(_115459))], (618 ^ _96350) ^ [] : [-(conceivedThruItself(_115459))]]], (620 ^ _96350) ^ [_115682] : [-(substance(_115682)), inItself(_115682), conceivedThruItself(_115682)], (630 ^ _96350) ^ [_115982] : [attribute(_115982), -(intPercAsConstEssSub(_115982))], (636 ^ _96350) ^ [_116134] : [intPercAsConstEssSub(_116134), -(attribute(_116134))], (642 ^ _96350) ^ [_116379, _116381, _116383] : [(mode _116383), 647 ^ _96350 : [(648 ^ _96350) ^ [] : [-(modification(_116383, _116381))], (650 ^ _96350) ^ [] : [-(substance(_116381))]], 651 ^ _96350 : [(652 ^ _96350) ^ [] : [-(existsIn(_116383, _116379))], (654 ^ _96350) ^ [] : [-(conceivedThru(_116383, _116379))]]], (656 ^ _96350) ^ [_116791, _116793, _116795] : [-((mode _116795)), 657 ^ _96350 : [(658 ^ _96350) ^ [] : [modification(_116795, _116793), substance(_116793)], (664 ^ _96350) ^ [] : [existsIn(_116795, _116791), conceivedThru(_116795, _116791)]]], (672 ^ _96350) ^ [_117282] : [god(_117282), 675 ^ _96350 : [(676 ^ _96350) ^ [] : [-(being(_117282))], (678 ^ _96350) ^ [] : [-(absolutelyInfinite(_117282))]]], (680 ^ _96350) ^ [_117505] : [-(god(_117505)), being(_117505), absolutelyInfinite(_117505)], (690 ^ _96350) ^ [_117819, _117821] : [absolutelyInfinite(_117821), 693 ^ _96350 : [(694 ^ _96350) ^ [] : [-(substance(_117821))], (696 ^ _96350) ^ [] : [-(constInInfAttributes(_117821))], (698 ^ _96350) ^ [] : [attributeOf(_117819, _117821), 701 ^ _96350 : [(702 ^ _96350) ^ [] : [-(expressesEternalEssentiality(_117819))], (704 ^ _96350) ^ [] : [-(expressesInfiniteEssentiality(_117819))]]]]], (706 ^ _96350) ^ [_118284, _118286] : [-(absolutelyInfinite(_118286)), substance(_118286), constInInfAttributes(_118286), 715 ^ _96350 : [(716 ^ _96350) ^ [] : [-(attributeOf(_118284, _118286))], (718 ^ _96350) ^ [] : [expressesEternalEssentiality(_118284), expressesInfiniteEssentiality(_118284)]]], (726 ^ _96350) ^ [_118857, _118859] : [free(_118859), 729 ^ _96350 : [(730 ^ _96350) ^ [] : [-(existsOnlyByNecessityOfOwnNature(_118859))], (732 ^ _96350) ^ [] : [actionOf(_118857, _118859), -(determinedByItselfAlone(_118857, _118859))]]], (738 ^ _96350) ^ [_119179, _119181] : [-(free(_119181)), existsOnlyByNecessityOfOwnNature(_119181), 743 ^ _96350 : [(744 ^ _96350) ^ [] : [-(actionOf(_119179, _119181))], (746 ^ _96350) ^ [] : [determinedByItselfAlone(_119179, _119181)]]], (786 ^ _96350) ^ [_120591] : [eternity(_120591), -(existConcFollowFromDefEternal(_120591))], (792 ^ _96350) ^ [_120743] : [existConcFollowFromDefEternal(_120743), -(eternity(_120743))], (750 ^ _96350) ^ [_119580, _119582] : [necessary(_119582), 753 ^ _96350 : [(754 ^ _96350) ^ [] : [-(externalTo(_119580, _119582))], (756 ^ _96350) ^ [] : [-(determinedByFixedMethod(_119582, _119580))], (758 ^ _96350) ^ [] : [-(determinedByDefiniteMethod(_119582, _119580))], (760 ^ _96350) ^ [] : [-(isMethodAction(_119580)), -(isMethodExistence(_119580))]]], (766 ^ _96350) ^ [_120049, _120051] : [-(necessary(_120051)), externalTo(_120049, _120051), determinedByFixedMethod(_120051, _120049), determinedByDefiniteMethod(_120051, _120049), 779 ^ _96350 : [(780 ^ _96350) ^ [] : [isMethodAction(_120049)], (782 ^ _96350) ^ [] : [isMethodExistence(_120049)]]], (2 ^ _96350) ^ [_96474] : [-(_96474 = _96474)], (4 ^ _96350) ^ [_96581, _96583] : [_96583 = _96581, -(_96581 = _96583)], (10 ^ _96350) ^ [_96785, _96787, _96789] : [-(_96789 = _96785), _96789 = _96787, _96787 = _96785], (20 ^ _96350) ^ [_97098, _97100] : [-(natureConcOnlyByExistence(_97098)), _97100 = _97098, natureConcOnlyByExistence(_97100)], (30 ^ _96350) ^ [_97393, _97395] : [-(finiteAfterItsKind(_97393)), _97395 = _97393, finiteAfterItsKind(_97395)], (40 ^ _96350) ^ [_97716, _97718, _97720, _97722] : [-(canBeLimitedBy(_97720, _97716)), canBeLimitedBy(_97722, _97718), _97722 = _97720, _97718 = _97716], (54 ^ _96350) ^ [_98160, _98162, _98164, _98166] : [-(sameKind(_98164, _98160)), sameKind(_98166, _98162), _98166 = _98164, _98162 = _98160], (68 ^ _96350) ^ [_98576, _98578] : [-(conceivedThruItself(_98576)), _98578 = _98576, conceivedThruItself(_98578)], (78 ^ _96350) ^ [_98871, _98873] : [-(attribute(_98871)), _98873 = _98871, attribute(_98873)], (88 ^ _96350) ^ [_99166, _99168] : [-(intPercAsConstEssSub(_99166)), _99168 = _99166, intPercAsConstEssSub(_99168)], (98 ^ _96350) ^ [_99461, _99463] : [-((mode _99461)), _99463 = _99461, (mode _99463)], (108 ^ _96350) ^ [_99784, _99786, _99788, _99790] : [-(modification(_99788, _99784)), modification(_99790, _99786), _99790 = _99788, _99786 = _99784], (122 ^ _96350) ^ [_100200, _100202] : [-(god(_100200)), _100202 = _100200, god(_100202)], (132 ^ _96350) ^ [_100495, _100497] : [-(absolutelyInfinite(_100495)), _100497 = _100495, absolutelyInfinite(_100497)], (142 ^ _96350) ^ [_100790, _100792] : [-(constInInfAttributes(_100790)), _100792 = _100790, constInInfAttributes(_100792)], (152 ^ _96350) ^ [_101113, _101115, _101117, _101119] : [-(attributeOf(_101117, _101113)), attributeOf(_101119, _101115), _101119 = _101117, _101115 = _101113], (166 ^ _96350) ^ [_101529, _101531] : [-(expressesEternalEssentiality(_101529)), _101531 = _101529, expressesEternalEssentiality(_101531)], (176 ^ _96350) ^ [_101824, _101826] : [-(expressesInfiniteEssentiality(_101824)), _101826 = _101824, expressesInfiniteEssentiality(_101826)], (186 ^ _96350) ^ [_102119, _102121] : [-(free(_102119)), _102121 = _102119, free(_102121)], (196 ^ _96350) ^ [_102414, _102416] : [-(existsOnlyByNecessityOfOwnNature(_102414)), _102416 = _102414, existsOnlyByNecessityOfOwnNature(_102416)], (206 ^ _96350) ^ [_102737, _102739, _102741, _102743] : [-(actionOf(_102741, _102737)), actionOf(_102743, _102739), _102743 = _102741, _102739 = _102737], (220 ^ _96350) ^ [_103181, _103183, _103185, _103187] : [-(determinedByItselfAlone(_103185, _103181)), determinedByItselfAlone(_103187, _103183), _103187 = _103185, _103183 = _103181], (234 ^ _96350) ^ [_103597, _103599] : [-(necessary(_103597)), _103599 = _103597, necessary(_103599)], (244 ^ _96350) ^ [_103920, _103922, _103924, _103926] : [-(externalTo(_103924, _103920)), externalTo(_103926, _103922), _103926 = _103924, _103922 = _103920], (258 ^ _96350) ^ [_104364, _104366, _104368, _104370] : [-(determinedByFixedMethod(_104368, _104364)), determinedByFixedMethod(_104370, _104366), _104370 = _104368, _104366 = _104364], (272 ^ _96350) ^ [_104808, _104810, _104812, _104814] : [-(determinedByDefiniteMethod(_104812, _104808)), determinedByDefiniteMethod(_104814, _104810), _104814 = _104812, _104810 = _104808], (286 ^ _96350) ^ [_105224, _105226] : [-(isMethodAction(_105224)), _105226 = _105224, isMethodAction(_105226)], (296 ^ _96350) ^ [_105519, _105521] : [-(isMethodExistence(_105519)), _105521 = _105519, isMethodExistence(_105521)], (306 ^ _96350) ^ [_105814, _105816] : [-(eternity(_105814)), _105816 = _105814, eternity(_105816)], (316 ^ _96350) ^ [_106109, _106111] : [-(existConcFollowFromDefEternal(_106109)), _106111 = _106109, existConcFollowFromDefEternal(_106111)], (326 ^ _96350) ^ [_106432, _106434, _106436, _106438] : [-(existsIn(_106436, _106432)), existsIn(_106438, _106434), _106438 = _106436, _106434 = _106432], (340 ^ _96350) ^ [_106876, _106878, _106880, _106882] : [-(conceivedThru(_106880, _106876)), conceivedThru(_106882, _106878), _106882 = _106880, _106878 = _106876], (354 ^ _96350) ^ [_107292, _107294] : [-(definiteCause(_107292)), _107294 = _107292, definiteCause(_107294)], (364 ^ _96350) ^ [_107615, _107617, _107619, _107621] : [-(effectNecessarilyFollowsFrom(_107619, _107615)), effectNecessarilyFollowsFrom(_107621, _107617), _107621 = _107619, _107617 = _107615], (378 ^ _96350) ^ [_108059, _108061, _108063, _108065] : [-(knowledgeOfEffect(_108063, _108059)), knowledgeOfEffect(_108065, _108061), _108065 = _108063, _108061 = _108059], (392 ^ _96350) ^ [_108475, _108477] : [-(knowledgeOfACause(_108475)), _108477 = _108475, knowledgeOfACause(_108477)], (402 ^ _96350) ^ [_108798, _108800, _108802, _108804] : [-(haveNothingInCommon(_108802, _108798)), haveNothingInCommon(_108804, _108800), _108804 = _108802, _108800 = _108798], (416 ^ _96350) ^ [_109242, _109244, _109246, _109248] : [-(canBeUnderstoodInTermsOf(_109246, _109242)), canBeUnderstoodInTermsOf(_109248, _109244), _109248 = _109246, _109244 = _109242], (430 ^ _96350) ^ [_109686, _109688, _109690, _109692] : [-(conceptionInvolves(_109690, _109686)), conceptionInvolves(_109692, _109688), _109692 = _109690, _109688 = _109686], (444 ^ _96350) ^ [_110102, _110104] : [-(trueIdea(_110102)), _110104 = _110102, trueIdea(_110104)], (454 ^ _96350) ^ [_110425, _110427, _110429, _110431] : [-(correspondWith(_110429, _110425)), correspondWith(_110431, _110427), _110431 = _110429, _110427 = _110425], (468 ^ _96350) ^ [_110869, _110871, _110873, _110875] : [-(ideateOf(_110873, _110869)), ideateOf(_110875, _110871), _110875 = _110873, _110871 = _110869], (482 ^ _96350) ^ [_111313, _111315, _111317, _111319] : [-(objectOf(_111317, _111313)), objectOf(_111319, _111315), _111319 = _111317, _111315 = _111313], (496 ^ _96350) ^ [_111729, _111731] : [-(canBeConceivedAsNonExisting(_111729)), _111731 = _111729, canBeConceivedAsNonExisting(_111731)], (506 ^ _96350) ^ [_112024, _112026] : [-(inItself(_112024)), _112026 = _112024, inItself(_112026)], (516 ^ _96350) ^ [_112319, _112321] : [-(selfCaused(_112319)), _112321 = _112319, selfCaused(_112321)], (526 ^ _96350) ^ [_112614, _112616] : [-(being(_112614)), _112616 = _112614, being(_112616)], (536 ^ _96350) ^ [_112909, _112911] : [-(essenceInvExistence(_112909)), _112911 = _112909, essenceInvExistence(_112911)], (546 ^ _96350) ^ [_113204, _113206] : [-(hasEssence(_113204)), _113206 = _113204, hasEssence(_113206)], (556 ^ _96350) ^ [_113499, _113501] : [-(substance(_113499)), _113501 = _113499, substance(_113501)], (566 ^ _96350) ^ [_113774, _113776] : [-(exists(_113774)), _113776 = _113774, exists(_113776)]], input).
% 0.29/1.38 ncf('1',plain,[exists(911 ^ [])],start(915 ^ 0)).
% 0.29/1.38 ncf('1.1',plain,[-(exists(911 ^ [])), essenceInvExistence(911 ^ []), hasEssence(911 ^ [])],extension(902 ^ 1,bind([[_124311], [911 ^ []]]))).
% 0.29/1.38 ncf('1.1.1',plain,[-(essenceInvExistence(911 ^ [])), selfCaused(911 ^ [])],extension(576 ^ 2,bind([[_114373], [911 ^ []]]))).
% 0.29/1.38 ncf('1.1.1.1',plain,[-(selfCaused(911 ^ [])), inItself(911 ^ [])],extension(890 ^ 3,bind([[_123959], [911 ^ []]]))).
% 0.29/1.38 ncf('1.1.1.1.1',plain,[-(inItself(911 ^ [])), substance(911 ^ [])],extension(612 ^ 4,bind([[_115459], [911 ^ []]]))).
% 0.29/1.38 ncf('1.1.1.1.1.1',plain,[-(substance(911 ^ []))],extension(913 ^ 5)).
% 0.29/1.38 ncf('1.1.2',plain,[-(hasEssence(911 ^ [])), being(911 ^ [])],extension(896 ^ 2,bind([[_124145], [911 ^ []]]))).
% 0.29/1.38 ncf('1.1.2.1',plain,[-(being(911 ^ [])), substance(911 ^ [])],extension(884 ^ 3,bind([[_123773], [911 ^ []]]))).
% 0.29/1.38 ncf('1.1.2.1.1',plain,[-(substance(911 ^ []))],extension(913 ^ 4)).
% 0.29/1.38 %-----------------------------------------------------
% 0.29/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------