%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR040+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n016.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:35:57 EDT 2023
% Result : Theorem 43.54s 42.82s
% Output : Proof 43.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR040+1 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n016.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 : Fri May 19 01:11:42 EDT 2023
% 0.12/0.33 % CPUTime :
% 43.54/42.82
% 43.54/42.82 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 43.54/42.82 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 43.54/42.82 %-----------------------------------------------------
% 43.54/42.82 ncf(matrix, plain, [(758 ^ _144105) ^ [] : [-(tptpcol_15_109185(c_tptpcol_16_62187))], (756 ^ _144105) ^ [] : [-(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)), c_translation_14)))], !, (16 ^ _119279) ^ [] : [-(genlmt(c_universalvocabularymt, c_corecyclmt))], (270 ^ _119279) ^ [_127613] : [isa(_127613, c_tptpcol_15_109185), -(tptpcol_15_109185(_127613))], (8 ^ _119279) ^ [_119517] : [firstordercollection(_119517), -(fixedordercollection(_119517))], (474 ^ _119279) ^ [_134005] : [isa(_134005, c_individual), -(individual(_134005))], (348 ^ _119279) ^ [_130057] : [tptpcol_9_109060(_130057), -(isa(_130057, c_tptpcol_9_109060))], (732 ^ _119279) ^ [_142672, _142674, _142676] : [-(genlmt(_142676, _142672)), genlmt(_142676, _142674), genlmt(_142674, _142672)], (604 ^ _119279) ^ [_138230] : [firstordercollection(_138230), -(isa(_138230, c_firstordercollection))], (126 ^ _119279) ^ [_122994] : [tptpcol_10_109061(_122994), -(tptpcol_9_109060(_122994))], (486 ^ _119279) ^ [_134381] : [isa(_134381, c_collection), -(collection(_134381))], (378 ^ _119279) ^ [_130997] : [isa(_130997, c_tptpcol_6_108546), -(tptpcol_6_108546(_130997))], (628 ^ _119279) ^ [_139056, _139058] : [genls(_139058, _139056), -(collection(_139058))], (32 ^ _119279) ^ [] : [-(genlmt(c_basekb, c_universalvocabularymt))], (656 ^ _119279) ^ [_139977, _139979, _139981] : [-(genls(_139977, _139979)), genls(_139981, _139979), genls(_139977, _139981)], (250 ^ _119279) ^ [_126995, _126997, _126999] : [-(genlinverse(_126995, _126997)), genlinverse(_126999, _126997), genlpreds(_126995, _126999)], (68 ^ _119279) ^ [] : [-(genls(c_tptpcol_3_98305, c_tptpcol_2_98304))], (366 ^ _119279) ^ [_130621] : [isa(_130621, c_tptpcol_7_108547), -(tptpcol_7_108547(_130621))], (682 ^ _119279) ^ [_140794] : [-(uniformresourcelocator(f_urlfn(_140794)))], (498 ^ _119279) ^ [_134771, _134773] : [disjointwith(_134773, _134771), -(collection(_134771))], (216 ^ _119279) ^ [_125880, _125882, _125884] : [-(genlpreds(_125884, _125880)), genlpreds(_125884, _125882), genlpreds(_125882, _125880)], (134 ^ _119279) ^ [_123233] : [tptpcol_11_109125(_123233), -(tptpcol_10_109061(_123233))], (172 ^ _119279) ^ [_124403, _124405, _124407] : [isa(_124407, _124405), isa(_124407, _124403), disjointwith(_124405, _124403)], (18 ^ _119279) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (50 ^ _119279) ^ [] : [-(firstordercollection(c_tptpcol_16_62187))], (158 ^ _119279) ^ [_123950] : [tptpcol_14_109181(_123950), -(tptpcol_13_109173(_123950))], (4 ^ _119279) ^ [] : [-(genlmt(c_cycorpproductsmt, c_basekb))], (132 ^ _119279) ^ [] : [-(genls(c_tptpcol_11_109125, c_tptpcol_10_109061))], (432 ^ _119279) ^ [_132689] : [tptpcol_2_98304(_132689), -(isa(_132689, c_tptpcol_2_98304))], (156 ^ _119279) ^ [] : [-(genls(c_tptpcol_14_109181, c_tptpcol_13_109173))], (684 ^ _119279) ^ [_140873] : [-(natfunction(f_urlreferentfn(_140873), c_urlreferentfn))], (42 ^ _119279) ^ [] : [-(genls(c_tptpcol_0_0, c_individual))], (372 ^ _119279) ^ [_130809] : [tptpcol_7_108547(_130809), -(isa(_130809, c_tptpcol_7_108547))], (94 ^ _119279) ^ [_122038] : [tptpcol_6_108546(_122038), -(tptpcol_5_106498(_122038))], (536 ^ _119279) ^ [] : [-(mtvisible(c_logicaltruthmt))], (456 ^ _119279) ^ [_133441] : [tptpcol_16_62187(_133441), -(isa(_133441, c_tptpcol_16_62187))], (260 ^ _119279) ^ [_127318, _127320, _127322] : [-(genlinverse(_127322, _127318)), genlinverse(_127322, _127320), genlpreds(_127320, _127318)], (182 ^ _119279) ^ [_124725, _124727, _124729] : [-(genlpreds(_124729, _124725)), genlinverse(_124729, _124727), genlinverse(_124727, _124725)], (226 ^ _119279) ^ [_126175] : [predicate(_126175), -(genlpreds(_126175, _126175))], (70 ^ _119279) ^ [_121321] : [tptpcol_3_98305(_121321), -(tptpcol_2_98304(_121321))], (210 ^ _119279) ^ [_125658, _125660] : [genlpreds(_125660, _125658), -(predicate(_125660))], (34 ^ _119279) ^ [] : [-(genls(c_fixedordercollection, c_collection))], (164 ^ _119279) ^ [] : [-(genls(c_tptpcol_15_109185, c_tptpcol_14_109181))], (330 ^ _119279) ^ [_129493] : [isa(_129493, c_tptpcol_10_109061), -(tptpcol_10_109061(_129493))], (686 ^ _119279) ^ [_140953] : [-(natargument(f_urlreferentfn(_140953), n_1, _140953))], (198 ^ _119279) ^ [_125242, _125244] : [genlpreds(_125244, _125242), -(predicate(_125242))], (678 ^ _119279) ^ [_140633] : [-(natfunction(f_urlfn(_140633), c_urlfn))], (676 ^ _119279) ^ [] : [-(mtvisible(c_basekb))], (102 ^ _119279) ^ [_122277] : [tptpcol_7_108547(_122277), -(tptpcol_6_108546(_122277))], (288 ^ _119279) ^ [_128177] : [tptpcol_14_109181(_128177), -(isa(_128177, c_tptpcol_14_109181))], (360 ^ _119279) ^ [_130433] : [tptpcol_8_109059(_130433), -(isa(_130433, c_tptpcol_8_109059))], (116 ^ _119279) ^ [] : [-(genls(c_tptpcol_9_109060, c_tptpcol_8_109059))], (30 ^ _119279) ^ [] : [-(genlmt(c_machinelearningspindleheadmt, c_cycnounlearnermt))], (402 ^ _119279) ^ [_131749] : [isa(_131749, c_tptpcol_4_106497), -(tptpcol_4_106497(_131749))], (510 ^ _119279) ^ [_135187, _135189] : [disjointwith(_135189, _135187), -(disjointwith(_135187, _135189))], (694 ^ _119279) ^ [_141322, _141324] : [-(natargument(f_contentmtofcdafromeventfn(_141324, _141322), n_2, _141322))], (692 ^ _119279) ^ [_141224, _141226] : [-(natargument(f_contentmtofcdafromeventfn(_141226, _141224), n_1, _141226))], (584 ^ _119279) ^ [] : [-(mtvisible(c_corecyclmt))], (36 ^ _119279) ^ [_120312] : [fixedordercollection(_120312), -(collection(_120312))], (84 ^ _119279) ^ [] : [-(genls(c_tptpcol_5_106498, c_tptpcol_4_106497))], (616 ^ _119279) ^ [_138640, _138642] : [genls(_138642, _138640), -(collection(_138640))], (244 ^ _119279) ^ [_126773, _126775] : [genlinverse(_126775, _126773), -(binarypredicate(_126775))], (444 ^ _119279) ^ [_133065] : [tptpcol_1_65536(_133065), -(isa(_133065, c_tptpcol_1_65536))], (232 ^ _119279) ^ [_126363] : [predicate(_126363), -(genlpreds(_126363, _126363))], (166 ^ _119279) ^ [_124189] : [tptpcol_15_109185(_124189), -(tptpcol_14_109181(_124189))], (108 ^ _119279) ^ [] : [-(genls(c_tptpcol_8_109059, c_tptpcol_7_108547))], (714 ^ _119279) ^ [_142034, _142036] : [genlmt(_142036, _142034), -(microtheory(_142034))], (76 ^ _119279) ^ [] : [-(genls(c_tptpcol_4_106497, c_tptpcol_3_98305))], (390 ^ _119279) ^ [_131373] : [isa(_131373, c_tptpcol_5_106498), -(tptpcol_5_106498(_131373))], (742 ^ _119279) ^ [_142967] : [microtheory(_142967), -(genlmt(_142967, _142967))], (396 ^ _119279) ^ [_131561] : [tptpcol_5_106498(_131561), -(isa(_131561, c_tptpcol_5_106498))], (60 ^ _119279) ^ [] : [-(genls(c_tptpcol_2_98304, c_tptpcol_1_65536))], (318 ^ _119279) ^ [_129117] : [isa(_129117, c_tptpcol_11_109125), -(tptpcol_11_109125(_129117))], (150 ^ _119279) ^ [_123711] : [tptpcol_13_109173(_123711), -(tptpcol_12_109157(_123711))], (22 ^ _119279) ^ [_119915] : [collection(_119915), individual(_119915)], (306 ^ _119279) ^ [_128741] : [isa(_128741, c_tptpcol_12_109157), -(tptpcol_12_109157(_128741))], (384 ^ _119279) ^ [_131185] : [tptpcol_6_108546(_131185), -(isa(_131185, c_tptpcol_6_108546))], (148 ^ _119279) ^ [] : [-(genls(c_tptpcol_13_109173, c_tptpcol_12_109157))], (492 ^ _119279) ^ [_134569] : [collection(_134569), -(isa(_134569, c_collection))], (574 ^ _119279) ^ [_137318, _137320, _137322] : [-(isa(_137322, _137318)), isa(_137322, _137320), genls(_137320, _137318)], (354 ^ _119279) ^ [_130245] : [isa(_130245, c_tptpcol_8_109059), -(tptpcol_8_109059(_130245))], (538 ^ _119279) ^ [_136082] : [isa(_136082, c_transitivebinarypredicate), -(transitivebinarypredicate(_136082))], (726 ^ _119279) ^ [_142450, _142452] : [genlmt(_142452, _142450), -(microtheory(_142452))], (680 ^ _119279) ^ [_140713] : [-(natargument(f_urlfn(_140713), n_1, _140713))], (586 ^ _119279) ^ [_137666] : [isa(_137666, c_fixedordercollection), -(fixedordercollection(_137666))], (110 ^ _119279) ^ [_122516] : [tptpcol_8_109059(_122516), -(tptpcol_7_108547(_122516))], (342 ^ _119279) ^ [_129869] : [isa(_129869, c_tptpcol_9_109060), -(tptpcol_9_109060(_129869))], (592 ^ _119279) ^ [_137854] : [fixedordercollection(_137854), -(isa(_137854, c_fixedordercollection))], (118 ^ _119279) ^ [_122755] : [tptpcol_9_109060(_122755), -(tptpcol_8_109059(_122755))], (20 ^ _119279) ^ [] : [-(genlmt(c_corecyclmt, c_logicaltruthmt))], (698 ^ _119279) ^ [_141531, _141533] : [-(mtvisible(_141531)), mtvisible(_141533), genlmt(_141533, _141531)], (634 ^ _119279) ^ [_139278, _139280, _139282] : [-(genls(_139282, _139278)), genls(_139282, _139280), genls(_139280, _139278)], (690 ^ _119279) ^ [_141127, _141129] : [-(natfunction(f_contentmtofcdafromeventfn(_141129, _141127), c_contentmtofcdafromeventfn))], (516 ^ _119279) ^ [_135411, _135413, _135415] : [-(disjointwith(_135415, _135411)), disjointwith(_135415, _135413), genls(_135411, _135413)], (238 ^ _119279) ^ [_126565, _126567] : [genlinverse(_126567, _126565), -(binarypredicate(_126565))], (336 ^ _119279) ^ [_129681] : [tptpcol_10_109061(_129681), -(isa(_129681, c_tptpcol_10_109061))], (28 ^ _119279) ^ [] : [-(disjointwith(c_collection, c_individual))], (450 ^ _119279) ^ [_133253] : [isa(_133253, c_tptpcol_16_62187), -(tptpcol_16_62187(_133253))], (562 ^ _119279) ^ [_136888, _136890] : [isa(_136890, _136888), -(thing(_136890))], (92 ^ _119279) ^ [] : [-(genls(c_tptpcol_6_108546, c_tptpcol_5_106498))], (544 ^ _119279) ^ [_136270] : [transitivebinarypredicate(_136270), -(isa(_136270, c_transitivebinarypredicate))], (480 ^ _119279) ^ [_134193] : [individual(_134193), -(isa(_134193, c_individual))], (2 ^ _119279) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)), c_translation_14), c_machinelearningspindleheadmt))], (54 ^ _119279) ^ [_120843] : [tptpcol_1_65536(_120843), -(tptpcol_0_0(_120843))], (300 ^ _119279) ^ [_128553] : [tptpcol_13_109173(_128553), -(isa(_128553, c_tptpcol_13_109173))], (550 ^ _119279) ^ [_136472, _136474] : [isa(_136474, _136472), -(collection(_136472))], (666 ^ _119279) ^ [_140300, _140302, _140304] : [-(genls(_140304, _140300)), genls(_140304, _140302), genls(_140302, _140300)], (52 ^ _119279) ^ [] : [-(genls(c_tptpcol_1_65536, c_tptpcol_0_0))], (754 ^ _119279) ^ [] : [-(mtvisible(c_universalvocabularymt))], (526 ^ _119279) ^ [_135734, _135736, _135738] : [-(disjointwith(_135734, _135736)), disjointwith(_135738, _135736), genls(_135734, _135738)], (598 ^ _119279) ^ [_138042] : [isa(_138042, c_firstordercollection), -(firstordercollection(_138042))], (192 ^ _119279) ^ [_125034, _125036] : [genlpreds(_125036, _125034), -(predicate(_125034))], (556 ^ _119279) ^ [_136680, _136682] : [isa(_136682, _136680), -(collection(_136680))], (748 ^ _119279) ^ [_143155] : [microtheory(_143155), -(genlmt(_143155, _143155))], (462 ^ _119279) ^ [_133629] : [isa(_133629, c_tptpcol_0_0), -(tptpcol_0_0(_133629))], (324 ^ _119279) ^ [_129305] : [tptpcol_11_109125(_129305), -(isa(_129305, c_tptpcol_11_109125))], (78 ^ _119279) ^ [_121560] : [tptpcol_4_106497(_121560), -(tptpcol_3_98305(_121560))], (610 ^ _119279) ^ [_138432, _138434] : [genls(_138434, _138432), -(collection(_138432))], (696 ^ _119279) ^ [_141420, _141422] : [-(microtheory(f_contentmtofcdafromeventfn(_141422, _141420)))], (414 ^ _119279) ^ [_132125] : [isa(_132125, c_tptpcol_3_98305), -(tptpcol_3_98305(_132125))], (282 ^ _119279) ^ [_127989] : [isa(_127989, c_tptpcol_14_109181), -(tptpcol_14_109181(_127989))], (294 ^ _119279) ^ [_128365] : [isa(_128365, c_tptpcol_13_109173), -(tptpcol_13_109173(_128365))], (720 ^ _119279) ^ [_142242, _142244] : [genlmt(_142244, _142242), -(microtheory(_142244))], (100 ^ _119279) ^ [] : [-(genls(c_tptpcol_7_108547, c_tptpcol_6_108546))], (312 ^ _119279) ^ [_128929] : [tptpcol_12_109157(_128929), -(isa(_128929, c_tptpcol_12_109157))], (14 ^ _119279) ^ [] : [-(genlmt(c_cycnounlearnermt, c_cycorpproductsmt))], (568 ^ _119279) ^ [_137096, _137098] : [isa(_137098, _137096), -(thing(_137098))], (426 ^ _119279) ^ [_132501] : [isa(_132501, c_tptpcol_2_98304), -(tptpcol_2_98304(_132501))], (650 ^ _119279) ^ [_139761] : [collection(_139761), -(genls(_139761, _139761))], (644 ^ _119279) ^ [_139573] : [collection(_139573), -(genls(_139573, _139573))], (688 ^ _119279) ^ [_141034] : [-(computerdataartifact(f_urlreferentfn(_141034)))], (6 ^ _119279) ^ [] : [-(genls(c_firstordercollection, c_fixedordercollection))], (408 ^ _119279) ^ [_131937] : [tptpcol_4_106497(_131937), -(isa(_131937, c_tptpcol_4_106497))], (438 ^ _119279) ^ [_132877] : [isa(_132877, c_tptpcol_1_65536), -(tptpcol_1_65536(_132877))], (142 ^ _119279) ^ [_123472] : [tptpcol_12_109157(_123472), -(tptpcol_11_109125(_123472))], (420 ^ _119279) ^ [_132313] : [tptpcol_3_98305(_132313), -(isa(_132313, c_tptpcol_3_98305))], (708 ^ _119279) ^ [_141826, _141828] : [genlmt(_141828, _141826), -(microtheory(_141826))], (204 ^ _119279) ^ [_125450, _125452] : [genlpreds(_125452, _125450), -(predicate(_125452))], (124 ^ _119279) ^ [] : [-(genls(c_tptpcol_10_109061, c_tptpcol_9_109060))], (622 ^ _119279) ^ [_138848, _138850] : [genls(_138850, _138848), -(collection(_138850))], (140 ^ _119279) ^ [] : [-(genls(c_tptpcol_12_109157, c_tptpcol_11_109125))], (276 ^ _119279) ^ [_127801] : [tptpcol_15_109185(_127801), -(isa(_127801, c_tptpcol_15_109185))], (504 ^ _119279) ^ [_134979, _134981] : [disjointwith(_134981, _134979), -(collection(_134981))], (62 ^ _119279) ^ [_121082] : [tptpcol_2_98304(_121082), -(tptpcol_1_65536(_121082))], (86 ^ _119279) ^ [_121799] : [tptpcol_5_106498(_121799), -(tptpcol_4_106497(_121799))], (44 ^ _119279) ^ [_120551] : [tptpcol_0_0(_120551), -(individual(_120551))], (468 ^ _119279) ^ [_133817] : [tptpcol_0_0(_133817), -(isa(_133817, c_tptpcol_0_0))]], input).
% 43.54/42.82 ncf('1',plain,[-(tptpcol_15_109185(c_tptpcol_16_62187))],start(758 ^ 0)).
% 43.54/42.82 ncf('1.1',plain,[tptpcol_15_109185(c_tptpcol_16_62187), -(isa(c_tptpcol_16_62187, c_tptpcol_15_109185))],extension(276 ^ 1,bind([[_127801], [c_tptpcol_16_62187]]))).
% 43.54/42.82 ncf('1.1.1',plain,[isa(c_tptpcol_16_62187, c_tptpcol_15_109185), -(isa(c_tptpcol_16_62187, c_individual)), genls(c_tptpcol_15_109185, c_individual)],extension(574 ^ 2,bind([[_137318, _137320, _137322], [c_individual, c_tptpcol_15_109185, c_tptpcol_16_62187]]))).
% 43.54/42.82 ncf('1.1.1.1',plain,[isa(c_tptpcol_16_62187, c_individual), -(individual(c_tptpcol_16_62187))],extension(474 ^ 3,bind([[_134005], [c_tptpcol_16_62187]]))).
% 43.54/42.82 ncf('1.1.1.1.1',plain,[individual(c_tptpcol_16_62187), collection(c_tptpcol_16_62187)],extension(22 ^ 4,bind([[_119915], [c_tptpcol_16_62187]]))).
% 43.54/42.82 ncf('1.1.1.1.1.1',plain,[-(collection(c_tptpcol_16_62187)), fixedordercollection(c_tptpcol_16_62187)],extension(36 ^ 5,bind([[_120312], [c_tptpcol_16_62187]]))).
% 43.54/42.82 ncf('1.1.1.1.1.1.1',plain,[-(fixedordercollection(c_tptpcol_16_62187)), firstordercollection(c_tptpcol_16_62187)],extension(8 ^ 6,bind([[_119517], [c_tptpcol_16_62187]]))).
% 43.54/42.82 ncf('1.1.1.1.1.1.1.1',plain,[-(firstordercollection(c_tptpcol_16_62187))],extension(50 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2',plain,[-(genls(c_tptpcol_15_109185, c_individual)), genls(c_tptpcol_7_108547, c_individual), genls(c_tptpcol_15_109185, c_tptpcol_7_108547)],extension(656 ^ 3,bind([[_139977, _139979, _139981], [c_tptpcol_15_109185, c_individual, c_tptpcol_7_108547]]))).
% 43.54/42.82 ncf('1.1.1.2.1',plain,[-(genls(c_tptpcol_7_108547, c_individual)), genls(c_tptpcol_3_98305, c_individual), genls(c_tptpcol_7_108547, c_tptpcol_3_98305)],extension(656 ^ 4,bind([[_139977, _139979, _139981], [c_tptpcol_7_108547, c_individual, c_tptpcol_3_98305]]))).
% 43.54/42.82 ncf('1.1.1.2.1.1',plain,[-(genls(c_tptpcol_3_98305, c_individual)), genls(c_tptpcol_1_65536, c_individual), genls(c_tptpcol_3_98305, c_tptpcol_1_65536)],extension(656 ^ 5,bind([[_139977, _139979, _139981], [c_tptpcol_3_98305, c_individual, c_tptpcol_1_65536]]))).
% 43.54/42.82 ncf('1.1.1.2.1.1.1',plain,[-(genls(c_tptpcol_1_65536, c_individual)), genls(c_tptpcol_0_0, c_individual), genls(c_tptpcol_1_65536, c_tptpcol_0_0)],extension(656 ^ 6,bind([[_139977, _139979, _139981], [c_tptpcol_1_65536, c_individual, c_tptpcol_0_0]]))).
% 43.54/42.82 ncf('1.1.1.2.1.1.1.1',plain,[-(genls(c_tptpcol_0_0, c_individual))],extension(42 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.1.1.1.2',plain,[-(genls(c_tptpcol_1_65536, c_tptpcol_0_0))],extension(52 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.1.1.2',plain,[-(genls(c_tptpcol_3_98305, c_tptpcol_1_65536)), genls(c_tptpcol_2_98304, c_tptpcol_1_65536), genls(c_tptpcol_3_98305, c_tptpcol_2_98304)],extension(656 ^ 6,bind([[_139977, _139979, _139981], [c_tptpcol_3_98305, c_tptpcol_1_65536, c_tptpcol_2_98304]]))).
% 43.54/42.82 ncf('1.1.1.2.1.1.2.1',plain,[-(genls(c_tptpcol_2_98304, c_tptpcol_1_65536))],extension(60 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.1.1.2.2',plain,[-(genls(c_tptpcol_3_98305, c_tptpcol_2_98304))],extension(68 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.1.2',plain,[-(genls(c_tptpcol_7_108547, c_tptpcol_3_98305)), genls(c_tptpcol_5_106498, c_tptpcol_3_98305), genls(c_tptpcol_7_108547, c_tptpcol_5_106498)],extension(656 ^ 5,bind([[_139977, _139979, _139981], [c_tptpcol_7_108547, c_tptpcol_3_98305, c_tptpcol_5_106498]]))).
% 43.54/42.82 ncf('1.1.1.2.1.2.1',plain,[-(genls(c_tptpcol_5_106498, c_tptpcol_3_98305)), genls(c_tptpcol_4_106497, c_tptpcol_3_98305), genls(c_tptpcol_5_106498, c_tptpcol_4_106497)],extension(656 ^ 6,bind([[_139977, _139979, _139981], [c_tptpcol_5_106498, c_tptpcol_3_98305, c_tptpcol_4_106497]]))).
% 43.54/42.82 ncf('1.1.1.2.1.2.1.1',plain,[-(genls(c_tptpcol_4_106497, c_tptpcol_3_98305))],extension(76 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.1.2.1.2',plain,[-(genls(c_tptpcol_5_106498, c_tptpcol_4_106497))],extension(84 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.1.2.2',plain,[-(genls(c_tptpcol_7_108547, c_tptpcol_5_106498)), genls(c_tptpcol_6_108546, c_tptpcol_5_106498), genls(c_tptpcol_7_108547, c_tptpcol_6_108546)],extension(656 ^ 6,bind([[_139977, _139979, _139981], [c_tptpcol_7_108547, c_tptpcol_5_106498, c_tptpcol_6_108546]]))).
% 43.54/42.82 ncf('1.1.1.2.1.2.2.1',plain,[-(genls(c_tptpcol_6_108546, c_tptpcol_5_106498))],extension(92 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.1.2.2.2',plain,[-(genls(c_tptpcol_7_108547, c_tptpcol_6_108546))],extension(100 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.2',plain,[-(genls(c_tptpcol_15_109185, c_tptpcol_7_108547)), genls(c_tptpcol_11_109125, c_tptpcol_7_108547), genls(c_tptpcol_15_109185, c_tptpcol_11_109125)],extension(656 ^ 4,bind([[_139977, _139979, _139981], [c_tptpcol_15_109185, c_tptpcol_7_108547, c_tptpcol_11_109125]]))).
% 43.54/42.82 ncf('1.1.1.2.2.1',plain,[-(genls(c_tptpcol_11_109125, c_tptpcol_7_108547)), genls(c_tptpcol_9_109060, c_tptpcol_7_108547), genls(c_tptpcol_11_109125, c_tptpcol_9_109060)],extension(656 ^ 5,bind([[_139977, _139979, _139981], [c_tptpcol_11_109125, c_tptpcol_7_108547, c_tptpcol_9_109060]]))).
% 43.54/42.82 ncf('1.1.1.2.2.1.1',plain,[-(genls(c_tptpcol_9_109060, c_tptpcol_7_108547)), genls(c_tptpcol_8_109059, c_tptpcol_7_108547), genls(c_tptpcol_9_109060, c_tptpcol_8_109059)],extension(656 ^ 6,bind([[_139977, _139979, _139981], [c_tptpcol_9_109060, c_tptpcol_7_108547, c_tptpcol_8_109059]]))).
% 43.54/42.82 ncf('1.1.1.2.2.1.1.1',plain,[-(genls(c_tptpcol_8_109059, c_tptpcol_7_108547))],extension(108 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.2.1.1.2',plain,[-(genls(c_tptpcol_9_109060, c_tptpcol_8_109059))],extension(116 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.2.1.2',plain,[-(genls(c_tptpcol_11_109125, c_tptpcol_9_109060)), genls(c_tptpcol_10_109061, c_tptpcol_9_109060), genls(c_tptpcol_11_109125, c_tptpcol_10_109061)],extension(656 ^ 6,bind([[_139977, _139979, _139981], [c_tptpcol_11_109125, c_tptpcol_9_109060, c_tptpcol_10_109061]]))).
% 43.54/42.82 ncf('1.1.1.2.2.1.2.1',plain,[-(genls(c_tptpcol_10_109061, c_tptpcol_9_109060))],extension(124 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.2.1.2.2',plain,[-(genls(c_tptpcol_11_109125, c_tptpcol_10_109061))],extension(132 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.2.2',plain,[-(genls(c_tptpcol_15_109185, c_tptpcol_11_109125)), genls(c_tptpcol_13_109173, c_tptpcol_11_109125), genls(c_tptpcol_15_109185, c_tptpcol_13_109173)],extension(656 ^ 5,bind([[_139977, _139979, _139981], [c_tptpcol_15_109185, c_tptpcol_11_109125, c_tptpcol_13_109173]]))).
% 43.54/42.82 ncf('1.1.1.2.2.2.1',plain,[-(genls(c_tptpcol_13_109173, c_tptpcol_11_109125)), genls(c_tptpcol_12_109157, c_tptpcol_11_109125), genls(c_tptpcol_13_109173, c_tptpcol_12_109157)],extension(656 ^ 6,bind([[_139977, _139979, _139981], [c_tptpcol_13_109173, c_tptpcol_11_109125, c_tptpcol_12_109157]]))).
% 43.54/42.82 ncf('1.1.1.2.2.2.1.1',plain,[-(genls(c_tptpcol_12_109157, c_tptpcol_11_109125))],extension(140 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.2.2.1.2',plain,[-(genls(c_tptpcol_13_109173, c_tptpcol_12_109157))],extension(148 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.2.2.2',plain,[-(genls(c_tptpcol_15_109185, c_tptpcol_13_109173)), genls(c_tptpcol_14_109181, c_tptpcol_13_109173), genls(c_tptpcol_15_109185, c_tptpcol_14_109181)],extension(656 ^ 6,bind([[_139977, _139979, _139981], [c_tptpcol_15_109185, c_tptpcol_13_109173, c_tptpcol_14_109181]]))).
% 43.54/42.82 ncf('1.1.1.2.2.2.2.1',plain,[-(genls(c_tptpcol_14_109181, c_tptpcol_13_109173))],extension(156 ^ 7)).
% 43.54/42.82 ncf('1.1.1.2.2.2.2.2',plain,[-(genls(c_tptpcol_15_109185, c_tptpcol_14_109181))],extension(164 ^ 7)).
% 43.54/42.82 %-----------------------------------------------------
% 43.54/42.82 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------