%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR052+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n025.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 10:45:50 EDT 2023
% Result : Theorem 0.46s 1.39s
% Output : Proof 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR052+1 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n025.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri May 19 00:28:03 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.46/1.39
% 0.46/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.46/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.46/1.39 %-----------------------------------------------------
% 0.46/1.39 ncf(matrix, plain, [(516 ^ _75237) ^ [] : [-(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)), c_translation_33)))], (518 ^ _75237) ^ [] : [genls(c_tptpcol_15_40430, c_tptpcol_7_39939)], (2 ^ _75237) ^ [] : [-(transitivebinarypredicate(c_genls))], (4 ^ _75237) ^ [] : [-(genlmt(c_cycorpproductsmt, c_basekb))], (6 ^ _75237) ^ [] : [-(genlmt(c_cycnounlearnermt, c_cycorpproductsmt))], (8 ^ _75237) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)), c_translation_33), c_machinelearningspindleheadmt))], (10 ^ _75237) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (12 ^ _75237) ^ [] : [-(genlmt(c_machinelearningspindleheadmt, c_cycnounlearnermt))], (14 ^ _75237) ^ [] : [-(genlmt(c_basekb, c_universalvocabularymt))], (16 ^ _75237) ^ [] : [-(genls(c_tptpcol_8_39940, c_tptpcol_7_39939))], (18 ^ _75237) ^ [_75760] : [tptpcol_8_39940(_75760), -(tptpcol_7_39939(_75760))], (24 ^ _75237) ^ [] : [-(genls(c_tptpcol_9_40196, c_tptpcol_8_39940))], (26 ^ _75237) ^ [_75999] : [tptpcol_9_40196(_75999), -(tptpcol_8_39940(_75999))], (32 ^ _75237) ^ [] : [-(genls(c_tptpcol_10_40324, c_tptpcol_9_40196))], (34 ^ _75237) ^ [_76238] : [tptpcol_10_40324(_76238), -(tptpcol_9_40196(_76238))], (40 ^ _75237) ^ [] : [-(genls(c_tptpcol_11_40388, c_tptpcol_10_40324))], (42 ^ _75237) ^ [_76477] : [tptpcol_11_40388(_76477), -(tptpcol_10_40324(_76477))], (48 ^ _75237) ^ [] : [-(genls(c_tptpcol_12_40420, c_tptpcol_11_40388))], (50 ^ _75237) ^ [_76716] : [tptpcol_12_40420(_76716), -(tptpcol_11_40388(_76716))], (56 ^ _75237) ^ [] : [-(genls(c_tptpcol_13_40421, c_tptpcol_12_40420))], (58 ^ _75237) ^ [_76955] : [tptpcol_13_40421(_76955), -(tptpcol_12_40420(_76955))], (64 ^ _75237) ^ [] : [-(genls(c_tptpcol_14_40429, c_tptpcol_13_40421))], (66 ^ _75237) ^ [_77194] : [tptpcol_14_40429(_77194), -(tptpcol_13_40421(_77194))], (72 ^ _75237) ^ [] : [-(genls(c_tptpcol_15_40430, c_tptpcol_14_40429))], (74 ^ _75237) ^ [_77433] : [tptpcol_15_40430(_77433), -(tptpcol_14_40429(_77433))], (80 ^ _75237) ^ [_77647, _77649, _77651] : [isa(_77651, _77649), isa(_77651, _77647), disjointwith(_77649, _77647)], (90 ^ _75237) ^ [_77969, _77971, _77973] : [-(genlpreds(_77973, _77969)), genlinverse(_77973, _77971), genlinverse(_77971, _77969)], (100 ^ _75237) ^ [_78278, _78280] : [genlpreds(_78280, _78278), -(predicate(_78278))], (106 ^ _75237) ^ [_78486, _78488] : [genlpreds(_78488, _78486), -(predicate(_78486))], (112 ^ _75237) ^ [_78694, _78696] : [genlpreds(_78696, _78694), -(predicate(_78696))], (118 ^ _75237) ^ [_78902, _78904] : [genlpreds(_78904, _78902), -(predicate(_78904))], (124 ^ _75237) ^ [_79124, _79126, _79128] : [-(genlpreds(_79128, _79124)), genlpreds(_79128, _79126), genlpreds(_79126, _79124)], (134 ^ _75237) ^ [_79419] : [predicate(_79419), -(genlpreds(_79419, _79419))], (140 ^ _75237) ^ [_79607] : [predicate(_79607), -(genlpreds(_79607, _79607))], (146 ^ _75237) ^ [_79809, _79811] : [genlinverse(_79811, _79809), -(binarypredicate(_79809))], (152 ^ _75237) ^ [_80017, _80019] : [genlinverse(_80019, _80017), -(binarypredicate(_80019))], (158 ^ _75237) ^ [_80239, _80241, _80243] : [-(genlinverse(_80239, _80241)), genlinverse(_80243, _80241), genlpreds(_80239, _80243)], (168 ^ _75237) ^ [_80562, _80564, _80566] : [-(genlinverse(_80566, _80562)), genlinverse(_80566, _80564), genlpreds(_80564, _80562)], (178 ^ _75237) ^ [_80871, _80873] : [disjointwith(_80873, _80871), -(collection(_80871))], (184 ^ _75237) ^ [_81079, _81081] : [disjointwith(_81081, _81079), -(collection(_81081))], (190 ^ _75237) ^ [_81287, _81289] : [disjointwith(_81289, _81287), -(disjointwith(_81287, _81289))], (196 ^ _75237) ^ [_81511, _81513, _81515] : [-(disjointwith(_81515, _81511)), disjointwith(_81515, _81513), genls(_81511, _81513)], (206 ^ _75237) ^ [_81834, _81836, _81838] : [-(disjointwith(_81834, _81836)), disjointwith(_81838, _81836), genls(_81834, _81838)], (216 ^ _75237) ^ [_82129] : [isa(_82129, c_tptpcol_15_40430), -(tptpcol_15_40430(_82129))], (222 ^ _75237) ^ [_82317] : [tptpcol_15_40430(_82317), -(isa(_82317, c_tptpcol_15_40430))], (228 ^ _75237) ^ [_82505] : [isa(_82505, c_tptpcol_14_40429), -(tptpcol_14_40429(_82505))], (234 ^ _75237) ^ [_82693] : [tptpcol_14_40429(_82693), -(isa(_82693, c_tptpcol_14_40429))], (240 ^ _75237) ^ [_82881] : [isa(_82881, c_tptpcol_13_40421), -(tptpcol_13_40421(_82881))], (246 ^ _75237) ^ [_83069] : [tptpcol_13_40421(_83069), -(isa(_83069, c_tptpcol_13_40421))], (252 ^ _75237) ^ [_83257] : [isa(_83257, c_tptpcol_12_40420), -(tptpcol_12_40420(_83257))], (258 ^ _75237) ^ [_83445] : [tptpcol_12_40420(_83445), -(isa(_83445, c_tptpcol_12_40420))], (264 ^ _75237) ^ [_83633] : [isa(_83633, c_tptpcol_11_40388), -(tptpcol_11_40388(_83633))], (270 ^ _75237) ^ [_83821] : [tptpcol_11_40388(_83821), -(isa(_83821, c_tptpcol_11_40388))], (276 ^ _75237) ^ [_84009] : [isa(_84009, c_tptpcol_10_40324), -(tptpcol_10_40324(_84009))], (282 ^ _75237) ^ [_84197] : [tptpcol_10_40324(_84197), -(isa(_84197, c_tptpcol_10_40324))], (288 ^ _75237) ^ [_84385] : [isa(_84385, c_tptpcol_9_40196), -(tptpcol_9_40196(_84385))], (294 ^ _75237) ^ [_84573] : [tptpcol_9_40196(_84573), -(isa(_84573, c_tptpcol_9_40196))], (300 ^ _75237) ^ [_84761] : [isa(_84761, c_tptpcol_7_39939), -(tptpcol_7_39939(_84761))], (306 ^ _75237) ^ [_84949] : [tptpcol_7_39939(_84949), -(isa(_84949, c_tptpcol_7_39939))], (312 ^ _75237) ^ [_85137] : [isa(_85137, c_tptpcol_8_39940), -(tptpcol_8_39940(_85137))], (318 ^ _75237) ^ [_85325] : [tptpcol_8_39940(_85325), -(isa(_85325, c_tptpcol_8_39940))], (324 ^ _75237) ^ [_85498] : [-(natfunction(f_urlfn(_85498), c_urlfn))], (326 ^ _75237) ^ [_85578] : [-(natargument(f_urlfn(_85578), n_1, _85578))], (328 ^ _75237) ^ [_85659] : [-(uniformresourcelocator(f_urlfn(_85659)))], (330 ^ _75237) ^ [_85738] : [-(natfunction(f_urlreferentfn(_85738), c_urlreferentfn))], (332 ^ _75237) ^ [_85818] : [-(natargument(f_urlreferentfn(_85818), n_1, _85818))], (334 ^ _75237) ^ [_85899] : [-(computerdataartifact(f_urlreferentfn(_85899)))], (336 ^ _75237) ^ [_85992, _85994] : [-(natfunction(f_contentmtofcdafromeventfn(_85994, _85992), c_contentmtofcdafromeventfn))], (338 ^ _75237) ^ [_86089, _86091] : [-(natargument(f_contentmtofcdafromeventfn(_86091, _86089), n_1, _86091))], (340 ^ _75237) ^ [_86187, _86189] : [-(natargument(f_contentmtofcdafromeventfn(_86189, _86187), n_2, _86187))], (342 ^ _75237) ^ [_86285, _86287] : [-(microtheory(f_contentmtofcdafromeventfn(_86287, _86285)))], (344 ^ _75237) ^ [_86396, _86398] : [-(mtvisible(_86396)), mtvisible(_86398), genlmt(_86398, _86396)], (354 ^ _75237) ^ [_86691, _86693] : [genlmt(_86693, _86691), -(microtheory(_86691))], (360 ^ _75237) ^ [_86899, _86901] : [genlmt(_86901, _86899), -(microtheory(_86899))], (366 ^ _75237) ^ [_87107, _87109] : [genlmt(_87109, _87107), -(microtheory(_87109))], (372 ^ _75237) ^ [_87315, _87317] : [genlmt(_87317, _87315), -(microtheory(_87317))], (378 ^ _75237) ^ [_87537, _87539, _87541] : [-(genlmt(_87541, _87537)), genlmt(_87541, _87539), genlmt(_87539, _87537)], (388 ^ _75237) ^ [_87832] : [microtheory(_87832), -(genlmt(_87832, _87832))], (394 ^ _75237) ^ [_88020] : [microtheory(_88020), -(genlmt(_88020, _88020))], (400 ^ _75237) ^ [] : [-(mtvisible(c_basekb))], (402 ^ _75237) ^ [_88261] : [isa(_88261, c_transitivebinarypredicate), -(transitivebinarypredicate(_88261))], (408 ^ _75237) ^ [_88449] : [transitivebinarypredicate(_88449), -(isa(_88449, c_transitivebinarypredicate))], (414 ^ _75237) ^ [_88651, _88653] : [genls(_88653, _88651), -(collection(_88651))], (420 ^ _75237) ^ [_88859, _88861] : [genls(_88861, _88859), -(collection(_88859))], (426 ^ _75237) ^ [_89067, _89069] : [genls(_89069, _89067), -(collection(_89069))], (432 ^ _75237) ^ [_89275, _89277] : [genls(_89277, _89275), -(collection(_89277))], (438 ^ _75237) ^ [_89497, _89499, _89501] : [-(genls(_89501, _89497)), genls(_89501, _89499), genls(_89499, _89497)], (448 ^ _75237) ^ [_89792] : [collection(_89792), -(genls(_89792, _89792))], (454 ^ _75237) ^ [_89980] : [collection(_89980), -(genls(_89980, _89980))], (460 ^ _75237) ^ [_90196, _90198, _90200] : [-(genls(_90196, _90198)), genls(_90200, _90198), genls(_90196, _90200)], (470 ^ _75237) ^ [_90519, _90521, _90523] : [-(genls(_90523, _90519)), genls(_90523, _90521), genls(_90521, _90519)], (480 ^ _75237) ^ [_90828, _90830] : [isa(_90830, _90828), -(collection(_90828))], (486 ^ _75237) ^ [_91036, _91038] : [isa(_91038, _91036), -(collection(_91036))], (492 ^ _75237) ^ [_91244, _91246] : [isa(_91246, _91244), -(thing(_91246))], (498 ^ _75237) ^ [_91452, _91454] : [isa(_91454, _91452), -(thing(_91454))], (514 ^ _75237) ^ [] : [-(mtvisible(c_universalvocabularymt))], (504 ^ _75237) ^ [_91674, _91676, _91678] : [-(isa(_91678, _91674)), isa(_91678, _91676), genls(_91676, _91674)]], input).
% 0.46/1.39 ncf('1',plain,[genls(c_tptpcol_15_40430, c_tptpcol_7_39939)],start(518 ^ 0)).
% 0.46/1.39 ncf('1.1',plain,[-(genls(c_tptpcol_15_40430, c_tptpcol_7_39939)), genls(c_tptpcol_15_40430, c_tptpcol_14_40429), genls(c_tptpcol_14_40429, c_tptpcol_7_39939)],extension(438 ^ 1,bind([[_89497, _89499, _89501], [c_tptpcol_7_39939, c_tptpcol_14_40429, c_tptpcol_15_40430]]))).
% 0.46/1.39 ncf('1.1.1',plain,[-(genls(c_tptpcol_15_40430, c_tptpcol_14_40429))],extension(72 ^ 2)).
% 0.46/1.39 ncf('1.1.2',plain,[-(genls(c_tptpcol_14_40429, c_tptpcol_7_39939)), genls(c_tptpcol_14_40429, c_tptpcol_13_40421), genls(c_tptpcol_13_40421, c_tptpcol_7_39939)],extension(438 ^ 2,bind([[_89497, _89499, _89501], [c_tptpcol_7_39939, c_tptpcol_13_40421, c_tptpcol_14_40429]]))).
% 0.46/1.39 ncf('1.1.2.1',plain,[-(genls(c_tptpcol_14_40429, c_tptpcol_13_40421))],extension(64 ^ 3)).
% 0.46/1.39 ncf('1.1.2.2',plain,[-(genls(c_tptpcol_13_40421, c_tptpcol_7_39939)), genls(c_tptpcol_13_40421, c_tptpcol_12_40420), genls(c_tptpcol_12_40420, c_tptpcol_7_39939)],extension(438 ^ 3,bind([[_89497, _89499, _89501], [c_tptpcol_7_39939, c_tptpcol_12_40420, c_tptpcol_13_40421]]))).
% 0.46/1.39 ncf('1.1.2.2.1',plain,[-(genls(c_tptpcol_13_40421, c_tptpcol_12_40420))],extension(56 ^ 4)).
% 0.46/1.39 ncf('1.1.2.2.2',plain,[-(genls(c_tptpcol_12_40420, c_tptpcol_7_39939)), genls(c_tptpcol_12_40420, c_tptpcol_11_40388), genls(c_tptpcol_11_40388, c_tptpcol_7_39939)],extension(438 ^ 4,bind([[_89497, _89499, _89501], [c_tptpcol_7_39939, c_tptpcol_11_40388, c_tptpcol_12_40420]]))).
% 0.46/1.39 ncf('1.1.2.2.2.1',plain,[-(genls(c_tptpcol_12_40420, c_tptpcol_11_40388))],extension(48 ^ 5)).
% 0.46/1.39 ncf('1.1.2.2.2.2',plain,[-(genls(c_tptpcol_11_40388, c_tptpcol_7_39939)), genls(c_tptpcol_11_40388, c_tptpcol_10_40324), genls(c_tptpcol_10_40324, c_tptpcol_7_39939)],extension(438 ^ 5,bind([[_89497, _89499, _89501], [c_tptpcol_7_39939, c_tptpcol_10_40324, c_tptpcol_11_40388]]))).
% 0.46/1.39 ncf('1.1.2.2.2.2.1',plain,[-(genls(c_tptpcol_11_40388, c_tptpcol_10_40324))],extension(40 ^ 6)).
% 0.46/1.39 ncf('1.1.2.2.2.2.2',plain,[-(genls(c_tptpcol_10_40324, c_tptpcol_7_39939)), genls(c_tptpcol_10_40324, c_tptpcol_9_40196), genls(c_tptpcol_9_40196, c_tptpcol_7_39939)],extension(438 ^ 6,bind([[_89497, _89499, _89501], [c_tptpcol_7_39939, c_tptpcol_9_40196, c_tptpcol_10_40324]]))).
% 0.46/1.39 ncf('1.1.2.2.2.2.2.1',plain,[-(genls(c_tptpcol_10_40324, c_tptpcol_9_40196))],extension(32 ^ 7)).
% 0.46/1.39 ncf('1.1.2.2.2.2.2.2',plain,[-(genls(c_tptpcol_9_40196, c_tptpcol_7_39939)), genls(c_tptpcol_9_40196, c_tptpcol_8_39940), genls(c_tptpcol_8_39940, c_tptpcol_7_39939)],extension(438 ^ 7,bind([[_89497, _89499, _89501], [c_tptpcol_7_39939, c_tptpcol_8_39940, c_tptpcol_9_40196]]))).
% 0.46/1.39 ncf('1.1.2.2.2.2.2.2.1',plain,[-(genls(c_tptpcol_9_40196, c_tptpcol_8_39940))],extension(24 ^ 8)).
% 0.46/1.39 ncf('1.1.2.2.2.2.2.2.2',plain,[-(genls(c_tptpcol_8_39940, c_tptpcol_7_39939))],extension(16 ^ 8)).
% 0.46/1.39 %-----------------------------------------------------
% 0.46/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------