%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PHI023+1 : TPTP v8.1.2. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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.33s 1.38s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : PHI023+1 : TPTP v8.1.2. Released v7.4.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n006.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 : 300
% 0.12/0.33 % DateTime : Thu May 18 21:03:51 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.33/1.38
% 0.33/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.33/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 ncf(matrix, plain, [(907 ^ _96345) ^ [] : [-(god(905 ^ []))], (909 ^ _96345) ^ [] : [exists(905 ^ [])], (884 ^ _96345) ^ [_123768] : [inItself(_123768), -(selfCaused(_123768))], (890 ^ _96345) ^ [_123954] : [being(_123954), -(hasEssence(_123954))], (896 ^ _96345) ^ [_124120] : [-(exists(_124120)), essenceInvExistence(_124120), hasEssence(_124120)], (798 ^ _96345) ^ [_121025, _121027] : [exists(_121027), -(existsIn(_121027, _121027)), 805 ^ _96345 : [(806 ^ _96345) ^ [] : [-(existsIn(_121027, _121025))], (808 ^ _96345) ^ [] : [_121027 = _121025]]], (810 ^ _96345) ^ [_121351, _121353] : [-(exists(_121353)), 811 ^ _96345 : [(812 ^ _96345) ^ [] : [existsIn(_121353, _121353)], (814 ^ _96345) ^ [] : [existsIn(_121353, _121351), -(_121353 = _121351)]]], (822 ^ _96345) ^ [_121727, _121729] : [-(conceivedThru(_121729, _121729)), 825 ^ _96345 : [(826 ^ _96345) ^ [] : [-(conceivedThru(_121729, _121727))], (828 ^ _96345) ^ [] : [_121729 = _121727]]], (830 ^ _96345) ^ [_122016, _122018] : [definiteCause(_122018), 833 ^ _96345 : [(834 ^ _96345) ^ [] : [-(effectNecessarilyFollowsFrom(_122016, _122018))], (836 ^ _96345) ^ [] : [-(definiteCause(_122018)), effectNecessarilyFollowsFrom(_122016, _122018)]]], (842 ^ _96345) ^ [_122419, _122421] : [knowledgeOfEffect(_122421, _122419), -(knowledgeOfACause(_122421))], (848 ^ _96345) ^ [_122579, _122581] : [knowledgeOfACause(_122581), -(knowledgeOfEffect(_122581, _122579))], (854 ^ _96345) ^ [_122789, _122791] : [haveNothingInCommon(_122791, _122789), 857 ^ _96345 : [(858 ^ _96345) ^ [] : [canBeUnderstoodInTermsOf(_122791, _122789)], (860 ^ _96345) ^ [] : [canBeUnderstoodInTermsOf(_122789, _122791)], (862 ^ _96345) ^ [] : [conceptionInvolves(_122791, _122789)], (864 ^ _96345) ^ [] : [conceptionInvolves(_122789, _122791)]]], (878 ^ _96345) ^ [_123565] : [canBeConceivedAsNonExisting(_123565), essenceInvExistence(_123565)], (866 ^ _96345) ^ [_123226, _123228] : [trueIdea(_123228), 869 ^ _96345 : [(870 ^ _96345) ^ [] : [-(correspondWith(_123228, _123226))], (872 ^ _96345) ^ [] : [-(ideateOf(_123226, _123228)), -(objectOf(_123226, _123228))]]], (576 ^ _96345) ^ [_114368] : [selfCaused(_114368), 579 ^ _96345 : [(580 ^ _96345) ^ [] : [-(essenceInvExistence(_114368))], (582 ^ _96345) ^ [] : [-(natureConcOnlyByExistence(_114368))]]], (584 ^ _96345) ^ [_114591] : [-(selfCaused(_114591)), essenceInvExistence(_114591), natureConcOnlyByExistence(_114591)], (594 ^ _96345) ^ [_114905, _114907] : [finiteAfterItsKind(_114907), 597 ^ _96345 : [(598 ^ _96345) ^ [] : [-(canBeLimitedBy(_114907, _114905))], (600 ^ _96345) ^ [] : [-(sameKind(_114907, _114905))]]], (602 ^ _96345) ^ [_115140, _115142] : [-(finiteAfterItsKind(_115142)), canBeLimitedBy(_115142, _115140), sameKind(_115142, _115140)], (612 ^ _96345) ^ [_115454] : [substance(_115454), 615 ^ _96345 : [(616 ^ _96345) ^ [] : [-(inItself(_115454))], (618 ^ _96345) ^ [] : [-(conceivedThruItself(_115454))]]], (620 ^ _96345) ^ [_115677] : [-(substance(_115677)), inItself(_115677), conceivedThruItself(_115677)], (630 ^ _96345) ^ [_115977] : [attribute(_115977), -(intPercAsConstEssSub(_115977))], (636 ^ _96345) ^ [_116129] : [intPercAsConstEssSub(_116129), -(attribute(_116129))], (642 ^ _96345) ^ [_116374, _116376, _116378] : [(mode _116378), 647 ^ _96345 : [(648 ^ _96345) ^ [] : [-(modification(_116378, _116376))], (650 ^ _96345) ^ [] : [-(substance(_116376))]], 651 ^ _96345 : [(652 ^ _96345) ^ [] : [-(existsIn(_116378, _116374))], (654 ^ _96345) ^ [] : [-(conceivedThru(_116378, _116374))]]], (656 ^ _96345) ^ [_116786, _116788, _116790] : [-((mode _116790)), 657 ^ _96345 : [(658 ^ _96345) ^ [] : [modification(_116790, _116788), substance(_116788)], (664 ^ _96345) ^ [] : [existsIn(_116790, _116786), conceivedThru(_116790, _116786)]]], (672 ^ _96345) ^ [_117277] : [god(_117277), 675 ^ _96345 : [(676 ^ _96345) ^ [] : [-(being(_117277))], (678 ^ _96345) ^ [] : [-(absolutelyInfinite(_117277))]]], (680 ^ _96345) ^ [_117500] : [-(god(_117500)), being(_117500), absolutelyInfinite(_117500)], (690 ^ _96345) ^ [_117814, _117816] : [absolutelyInfinite(_117816), 693 ^ _96345 : [(694 ^ _96345) ^ [] : [-(substance(_117816))], (696 ^ _96345) ^ [] : [-(constInInfAttributes(_117816))], (698 ^ _96345) ^ [] : [attributeOf(_117814, _117816), 701 ^ _96345 : [(702 ^ _96345) ^ [] : [-(expressesEternalEssentiality(_117814))], (704 ^ _96345) ^ [] : [-(expressesInfiniteEssentiality(_117814))]]]]], (706 ^ _96345) ^ [_118279, _118281] : [-(absolutelyInfinite(_118281)), substance(_118281), constInInfAttributes(_118281), 715 ^ _96345 : [(716 ^ _96345) ^ [] : [-(attributeOf(_118279, _118281))], (718 ^ _96345) ^ [] : [expressesEternalEssentiality(_118279), expressesInfiniteEssentiality(_118279)]]], (726 ^ _96345) ^ [_118852, _118854] : [free(_118854), 729 ^ _96345 : [(730 ^ _96345) ^ [] : [-(existsOnlyByNecessityOfOwnNature(_118854))], (732 ^ _96345) ^ [] : [actionOf(_118852, _118854), -(determinedByItselfAlone(_118852, _118854))]]], (738 ^ _96345) ^ [_119174, _119176] : [-(free(_119176)), existsOnlyByNecessityOfOwnNature(_119176), 743 ^ _96345 : [(744 ^ _96345) ^ [] : [-(actionOf(_119174, _119176))], (746 ^ _96345) ^ [] : [determinedByItselfAlone(_119174, _119176)]]], (786 ^ _96345) ^ [_120586] : [eternity(_120586), -(existConcFollowFromDefEternal(_120586))], (792 ^ _96345) ^ [_120738] : [existConcFollowFromDefEternal(_120738), -(eternity(_120738))], (750 ^ _96345) ^ [_119575, _119577] : [necessary(_119577), 753 ^ _96345 : [(754 ^ _96345) ^ [] : [-(externalTo(_119575, _119577))], (756 ^ _96345) ^ [] : [-(determinedByFixedMethod(_119577, _119575))], (758 ^ _96345) ^ [] : [-(determinedByDefiniteMethod(_119577, _119575))], (760 ^ _96345) ^ [] : [-(isMethodAction(_119575)), -(isMethodExistence(_119575))]]], (766 ^ _96345) ^ [_120044, _120046] : [-(necessary(_120046)), externalTo(_120044, _120046), determinedByFixedMethod(_120046, _120044), determinedByDefiniteMethod(_120046, _120044), 779 ^ _96345 : [(780 ^ _96345) ^ [] : [isMethodAction(_120044)], (782 ^ _96345) ^ [] : [isMethodExistence(_120044)]]], (2 ^ _96345) ^ [_96469] : [-(_96469 = _96469)], (4 ^ _96345) ^ [_96576, _96578] : [_96578 = _96576, -(_96576 = _96578)], (10 ^ _96345) ^ [_96780, _96782, _96784] : [-(_96784 = _96780), _96784 = _96782, _96782 = _96780], (20 ^ _96345) ^ [_97093, _97095] : [-(natureConcOnlyByExistence(_97093)), _97095 = _97093, natureConcOnlyByExistence(_97095)], (30 ^ _96345) ^ [_97388, _97390] : [-(finiteAfterItsKind(_97388)), _97390 = _97388, finiteAfterItsKind(_97390)], (40 ^ _96345) ^ [_97711, _97713, _97715, _97717] : [-(canBeLimitedBy(_97715, _97711)), canBeLimitedBy(_97717, _97713), _97717 = _97715, _97713 = _97711], (54 ^ _96345) ^ [_98155, _98157, _98159, _98161] : [-(sameKind(_98159, _98155)), sameKind(_98161, _98157), _98161 = _98159, _98157 = _98155], (68 ^ _96345) ^ [_98571, _98573] : [-(conceivedThruItself(_98571)), _98573 = _98571, conceivedThruItself(_98573)], (78 ^ _96345) ^ [_98866, _98868] : [-(attribute(_98866)), _98868 = _98866, attribute(_98868)], (88 ^ _96345) ^ [_99161, _99163] : [-(intPercAsConstEssSub(_99161)), _99163 = _99161, intPercAsConstEssSub(_99163)], (98 ^ _96345) ^ [_99456, _99458] : [-((mode _99456)), _99458 = _99456, (mode _99458)], (108 ^ _96345) ^ [_99779, _99781, _99783, _99785] : [-(modification(_99783, _99779)), modification(_99785, _99781), _99785 = _99783, _99781 = _99779], (122 ^ _96345) ^ [_100195, _100197] : [-(absolutelyInfinite(_100195)), _100197 = _100195, absolutelyInfinite(_100197)], (132 ^ _96345) ^ [_100490, _100492] : [-(substance(_100490)), _100492 = _100490, substance(_100492)], (142 ^ _96345) ^ [_100785, _100787] : [-(constInInfAttributes(_100785)), _100787 = _100785, constInInfAttributes(_100787)], (152 ^ _96345) ^ [_101108, _101110, _101112, _101114] : [-(attributeOf(_101112, _101108)), attributeOf(_101114, _101110), _101114 = _101112, _101110 = _101108], (166 ^ _96345) ^ [_101524, _101526] : [-(expressesEternalEssentiality(_101524)), _101526 = _101524, expressesEternalEssentiality(_101526)], (176 ^ _96345) ^ [_101819, _101821] : [-(expressesInfiniteEssentiality(_101819)), _101821 = _101819, expressesInfiniteEssentiality(_101821)], (186 ^ _96345) ^ [_102114, _102116] : [-(free(_102114)), _102116 = _102114, free(_102116)], (196 ^ _96345) ^ [_102409, _102411] : [-(existsOnlyByNecessityOfOwnNature(_102409)), _102411 = _102409, existsOnlyByNecessityOfOwnNature(_102411)], (206 ^ _96345) ^ [_102732, _102734, _102736, _102738] : [-(actionOf(_102736, _102732)), actionOf(_102738, _102734), _102738 = _102736, _102734 = _102732], (220 ^ _96345) ^ [_103176, _103178, _103180, _103182] : [-(determinedByItselfAlone(_103180, _103176)), determinedByItselfAlone(_103182, _103178), _103182 = _103180, _103178 = _103176], (234 ^ _96345) ^ [_103592, _103594] : [-(necessary(_103592)), _103594 = _103592, necessary(_103594)], (244 ^ _96345) ^ [_103915, _103917, _103919, _103921] : [-(externalTo(_103919, _103915)), externalTo(_103921, _103917), _103921 = _103919, _103917 = _103915], (258 ^ _96345) ^ [_104359, _104361, _104363, _104365] : [-(determinedByFixedMethod(_104363, _104359)), determinedByFixedMethod(_104365, _104361), _104365 = _104363, _104361 = _104359], (272 ^ _96345) ^ [_104803, _104805, _104807, _104809] : [-(determinedByDefiniteMethod(_104807, _104803)), determinedByDefiniteMethod(_104809, _104805), _104809 = _104807, _104805 = _104803], (286 ^ _96345) ^ [_105219, _105221] : [-(isMethodAction(_105219)), _105221 = _105219, isMethodAction(_105221)], (296 ^ _96345) ^ [_105514, _105516] : [-(isMethodExistence(_105514)), _105516 = _105514, isMethodExistence(_105516)], (306 ^ _96345) ^ [_105809, _105811] : [-(eternity(_105809)), _105811 = _105809, eternity(_105811)], (316 ^ _96345) ^ [_106104, _106106] : [-(existConcFollowFromDefEternal(_106104)), _106106 = _106104, existConcFollowFromDefEternal(_106106)], (326 ^ _96345) ^ [_106427, _106429, _106431, _106433] : [-(existsIn(_106431, _106427)), existsIn(_106433, _106429), _106433 = _106431, _106429 = _106427], (340 ^ _96345) ^ [_106871, _106873, _106875, _106877] : [-(conceivedThru(_106875, _106871)), conceivedThru(_106877, _106873), _106877 = _106875, _106873 = _106871], (354 ^ _96345) ^ [_107287, _107289] : [-(definiteCause(_107287)), _107289 = _107287, definiteCause(_107289)], (364 ^ _96345) ^ [_107610, _107612, _107614, _107616] : [-(effectNecessarilyFollowsFrom(_107614, _107610)), effectNecessarilyFollowsFrom(_107616, _107612), _107616 = _107614, _107612 = _107610], (378 ^ _96345) ^ [_108054, _108056, _108058, _108060] : [-(knowledgeOfEffect(_108058, _108054)), knowledgeOfEffect(_108060, _108056), _108060 = _108058, _108056 = _108054], (392 ^ _96345) ^ [_108470, _108472] : [-(knowledgeOfACause(_108470)), _108472 = _108470, knowledgeOfACause(_108472)], (402 ^ _96345) ^ [_108793, _108795, _108797, _108799] : [-(haveNothingInCommon(_108797, _108793)), haveNothingInCommon(_108799, _108795), _108799 = _108797, _108795 = _108793], (416 ^ _96345) ^ [_109237, _109239, _109241, _109243] : [-(canBeUnderstoodInTermsOf(_109241, _109237)), canBeUnderstoodInTermsOf(_109243, _109239), _109243 = _109241, _109239 = _109237], (430 ^ _96345) ^ [_109681, _109683, _109685, _109687] : [-(conceptionInvolves(_109685, _109681)), conceptionInvolves(_109687, _109683), _109687 = _109685, _109683 = _109681], (444 ^ _96345) ^ [_110097, _110099] : [-(trueIdea(_110097)), _110099 = _110097, trueIdea(_110099)], (454 ^ _96345) ^ [_110420, _110422, _110424, _110426] : [-(correspondWith(_110424, _110420)), correspondWith(_110426, _110422), _110426 = _110424, _110422 = _110420], (468 ^ _96345) ^ [_110864, _110866, _110868, _110870] : [-(ideateOf(_110868, _110864)), ideateOf(_110870, _110866), _110870 = _110868, _110866 = _110864], (482 ^ _96345) ^ [_111308, _111310, _111312, _111314] : [-(objectOf(_111312, _111308)), objectOf(_111314, _111310), _111314 = _111312, _111310 = _111308], (496 ^ _96345) ^ [_111724, _111726] : [-(canBeConceivedAsNonExisting(_111724)), _111726 = _111724, canBeConceivedAsNonExisting(_111726)], (506 ^ _96345) ^ [_112019, _112021] : [-(inItself(_112019)), _112021 = _112019, inItself(_112021)], (516 ^ _96345) ^ [_112314, _112316] : [-(selfCaused(_112314)), _112316 = _112314, selfCaused(_112316)], (526 ^ _96345) ^ [_112609, _112611] : [-(being(_112609)), _112611 = _112609, being(_112611)], (536 ^ _96345) ^ [_112904, _112906] : [-(essenceInvExistence(_112904)), _112906 = _112904, essenceInvExistence(_112906)], (546 ^ _96345) ^ [_113199, _113201] : [-(hasEssence(_113199)), _113201 = _113199, hasEssence(_113201)], (556 ^ _96345) ^ [_113494, _113496] : [-(god(_113494)), _113496 = _113494, god(_113496)], (566 ^ _96345) ^ [_113769, _113771] : [-(exists(_113769)), _113771 = _113769, exists(_113771)]], input).
% 0.33/1.38 ncf('1',plain,[exists(905 ^ [])],start(909 ^ 0)).
% 0.33/1.38 ncf('1.1',plain,[-(exists(905 ^ [])), essenceInvExistence(905 ^ []), hasEssence(905 ^ [])],extension(896 ^ 1,bind([[_124120], [905 ^ []]]))).
% 0.33/1.38 ncf('1.1.1',plain,[-(essenceInvExistence(905 ^ [])), selfCaused(905 ^ [])],extension(576 ^ 2,bind([[_114368], [905 ^ []]]))).
% 0.33/1.38 ncf('1.1.1.1',plain,[-(selfCaused(905 ^ [])), inItself(905 ^ [])],extension(884 ^ 3,bind([[_123768], [905 ^ []]]))).
% 0.33/1.38 ncf('1.1.1.1.1',plain,[-(inItself(905 ^ [])), substance(905 ^ [])],extension(612 ^ 4,bind([[_115454], [905 ^ []]]))).
% 0.33/1.38 ncf('1.1.1.1.1.1',plain,[-(substance(905 ^ [])), absolutelyInfinite(905 ^ [])],extension(690 ^ 5,bind([[_117814, _117816], [_68477, 905 ^ []]]))).
% 0.33/1.38 ncf('1.1.1.1.1.1.1',plain,[-(absolutelyInfinite(905 ^ [])), god(905 ^ [])],extension(672 ^ 6,bind([[_117277], [905 ^ []]]))).
% 0.33/1.38 ncf('1.1.1.1.1.1.1.1',plain,[-(god(905 ^ []))],extension(907 ^ 7)).
% 0.33/1.38 ncf('1.1.2',plain,[-(hasEssence(905 ^ [])), being(905 ^ [])],extension(890 ^ 2,bind([[_123954], [905 ^ []]]))).
% 0.33/1.38 ncf('1.1.2.1',plain,[-(being(905 ^ [])), god(905 ^ [])],extension(672 ^ 3,bind([[_117277], [905 ^ []]]))).
% 0.33/1.38 ncf('1.1.2.1.1',plain,[-(god(905 ^ []))],extension(907 ^ 4)).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------