%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : LAT327+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n015.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:28:49 EDT 2023
% Result : Theorem 0.36s 1.40s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : LAT327+1 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.35 % Computer : n015.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 18 14:25:37 EDT 2023
% 0.13/0.35 % CPUTime :
% 0.36/1.40
% 0.36/1.40 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.40 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.40 %-----------------------------------------------------
% 0.36/1.40 ncf(matrix, plain, [(732 ^ _101732) ^ [] : [v3_struct_0(730 ^ [])], (734 ^ _101732) ^ [] : [-(v10_lattices(730 ^ []))], (736 ^ _101732) ^ [] : [-(l3_lattices(730 ^ []))], (739 ^ _101732) ^ [] : [-(m1_subset_1(737 ^ [], u1_struct_0(730 ^ [])))], (742 ^ _101732) ^ [] : [-(m1_subset_1(740 ^ [], u1_struct_0(730 ^ [])))], (744 ^ _101732) ^ [] : [-(r3_lattices(730 ^ [], 737 ^ [], 740 ^ []))], (746 ^ _101732) ^ [] : [r2_hidden(737 ^ [], k22_filter_2(730 ^ [], 737 ^ [], 740 ^ [])), r2_hidden(740 ^ [], k22_filter_2(730 ^ [], 737 ^ [], 740 ^ []))], (252 ^ _101732) ^ [_109692, _109694] : [_109694 = _109692, -(k1_zfmisc_1(_109694) = k1_zfmisc_1(_109692))], (258 ^ _101732) ^ [_109910, _109912] : [_109912 = _109910, -(u1_struct_0(_109912) = u1_struct_0(_109910))], (264 ^ _101732) ^ [_110164, _110166, _110168, _110170, _110172, _110174] : [-(k22_filter_2(_110174, _110170, _110166) = k22_filter_2(_110172, _110168, _110164)), _110174 = _110172, _110170 = _110168, _110166 = _110164], (2 ^ _101732) ^ [_101876] : [-(_101876 = _101876)], (4 ^ _101732) ^ [_101983, _101985] : [_101985 = _101983, -(_101983 = _101985)], (10 ^ _101732) ^ [_102187, _102189, _102191] : [-(_102191 = _102187), _102191 = _102189, _102189 = _102187], (20 ^ _101732) ^ [_102528, _102530, _102532, _102534] : [-(r1_tarski(_102532, _102528)), r1_tarski(_102534, _102530), _102534 = _102532, _102530 = _102528], (34 ^ _101732) ^ [_102944, _102946] : [-(v1_funct_1(_102944)), _102946 = _102944, v1_funct_1(_102946)], (44 ^ _101732) ^ [_103239, _103241] : [-(l1_struct_0(_103239)), _103241 = _103239, l1_struct_0(_103241)], (54 ^ _101732) ^ [_103590, _103592, _103594, _103596, _103598, _103600] : [-(r1_lattices(_103598, _103594, _103590)), r1_lattices(_103600, _103596, _103592), _103600 = _103598, _103596 = _103594, _103592 = _103590], (72 ^ _101732) ^ [_104171, _104173, _104175, _104177] : [-(m2_lattice4(_104175, _104171)), m2_lattice4(_104177, _104173), _104177 = _104175, _104173 = _104171], (86 ^ _101732) ^ [_104587, _104589] : [-(l1_lattices(_104587)), _104589 = _104587, l1_lattices(_104589)], (96 ^ _101732) ^ [_104882, _104884] : [-(l2_lattices(_104882)), _104884 = _104882, l2_lattices(_104884)], (106 ^ _101732) ^ [_105177, _105179] : [-(v4_lattices(_105177)), _105179 = _105177, v4_lattices(_105179)], (116 ^ _101732) ^ [_105472, _105474] : [-(v5_lattices(_105472)), _105474 = _105472, v5_lattices(_105474)], (126 ^ _101732) ^ [_105767, _105769] : [-(v6_lattices(_105767)), _105769 = _105767, v6_lattices(_105769)], (136 ^ _101732) ^ [_106062, _106064] : [-(v7_lattices(_106062)), _106064 = _106062, v7_lattices(_106064)], (146 ^ _101732) ^ [_106357, _106359] : [-(v8_lattices(_106357)), _106359 = _106357, v8_lattices(_106359)], (156 ^ _101732) ^ [_106652, _106654] : [-(v9_lattices(_106652)), _106654 = _106652, v9_lattices(_106654)], (166 ^ _101732) ^ [_106947, _106949] : [-(v1_xboole_0(_106947)), _106949 = _106947, v1_xboole_0(_106949)], (176 ^ _101732) ^ [_107242, _107244] : [-(v3_struct_0(_107242)), _107244 = _107242, v3_struct_0(_107244)], (186 ^ _101732) ^ [_107537, _107539] : [-(v10_lattices(_107537)), _107539 = _107537, v10_lattices(_107539)], (196 ^ _101732) ^ [_107832, _107834] : [-(l3_lattices(_107832)), _107834 = _107832, l3_lattices(_107834)], (206 ^ _101732) ^ [_108155, _108157, _108159, _108161] : [-(m1_subset_1(_108159, _108155)), m1_subset_1(_108161, _108157), _108161 = _108159, _108157 = _108155], (238 ^ _101732) ^ [_109188, _109190, _109192, _109194] : [-(r2_hidden(_109192, _109188)), r2_hidden(_109194, _109190), _109194 = _109192, _109190 = _109188], (220 ^ _101732) ^ [_108627, _108629, _108631, _108633, _108635, _108637] : [-(r3_lattices(_108635, _108631, _108627)), r3_lattices(_108637, _108633, _108629), _108637 = _108635, _108633 = _108631, _108629 = _108627], (278 ^ _101732) ^ [_110623, _110625] : [-(r1_tarski(_110625, _110625))], (280 ^ _101732) ^ [] : [true___, -(true___)], (286 ^ _101732) ^ [] : [true___, -(true___)], (292 ^ _101732) ^ [_110940] : [v1_xboole_0(k1_zfmisc_1(_110940))], (294 ^ _101732) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (296 ^ _101732) ^ [_111087] : [-(v1_xboole_0(_111087)), 300 ^ _101732 : [(301 ^ _101732) ^ [] : [-(m1_subset_1(299 ^ [_111087], k1_zfmisc_1(_111087)))], (303 ^ _101732) ^ [] : [v1_xboole_0(299 ^ [_111087])]]], (306 ^ _101732) ^ [_111470] : [-(m1_subset_1(304 ^ [_111470], k1_zfmisc_1(_111470)))], (308 ^ _101732) ^ [_111521] : [-(v1_xboole_0(304 ^ [_111521]))], (310 ^ _101732) ^ [_111620] : [318 ^ _101732 : [(319 ^ _101732) ^ [] : [-(m1_subset_1(317 ^ [_111620], k1_zfmisc_1(u1_struct_0(_111620))))], (321 ^ _101732) ^ [] : [v1_xboole_0(317 ^ [_111620])]], -(v3_struct_0(_111620)), l1_struct_0(_111620)], (323 ^ _101732) ^ [_112084, _112086] : [m1_subset_1(_112086, k1_zfmisc_1(_112084)), -(r1_tarski(_112086, _112084))], (329 ^ _101732) ^ [_112250, _112252] : [r1_tarski(_112252, _112250), -(m1_subset_1(_112252, k1_zfmisc_1(_112250)))], (335 ^ _101732) ^ [_112480, _112482, _112484] : [-(m1_subset_1(_112484, _112480)), r2_hidden(_112484, _112482), m1_subset_1(_112482, k1_zfmisc_1(_112480))], (345 ^ _101732) ^ [_112807, _112809, _112811] : [r2_hidden(_112811, _112809), m1_subset_1(_112809, k1_zfmisc_1(_112807)), v1_xboole_0(_112807)], (355 ^ _101732) ^ [_113117, _113119] : [v1_xboole_0(_113119), -(_113119 = _113117), v1_xboole_0(_113117)], (366 ^ _101732) ^ [] : [-(l1_lattices(364 ^ []))], (369 ^ _101732) ^ [] : [-(l1_struct_0(367 ^ []))], (372 ^ _101732) ^ [] : [-(l2_lattices(370 ^ []))], (374 ^ _101732) ^ [_113667] : [-(m2_lattice4(385 ^ [_113667], _113667)), -(v3_struct_0(_113667)), v10_lattices(_113667), l3_lattices(_113667)], (389 ^ _101732) ^ [_114075] : [l1_lattices(_114075), -(l1_struct_0(_114075))], (395 ^ _101732) ^ [] : [true___, -(true___)], (401 ^ _101732) ^ [_114380] : [l2_lattices(_114380), -(l1_struct_0(_114380))], (407 ^ _101732) ^ [_114566] : [418 ^ _101732 : [(419 ^ _101732) ^ [_114870] : [m2_lattice4(_114870, _114566), -(m1_subset_1(_114870, k1_zfmisc_1(u1_struct_0(_114566))))]], -(v3_struct_0(_114566)), v10_lattices(_114566), l3_lattices(_114566)], (425 ^ _101732) ^ [_115081] : [v1_xboole_0(_115081), -(v1_funct_1(_115081))], (431 ^ _101732) ^ [_115267] : [l3_lattices(_115267), 462 ^ _101732 : [(463 ^ _101732) ^ [] : [v3_struct_0(_115267)], (465 ^ _101732) ^ [] : [-(v10_lattices(_115267))]], -(v3_struct_0(_115267)), v4_lattices(_115267), v5_lattices(_115267), v6_lattices(_115267), v7_lattices(_115267), v8_lattices(_115267), v9_lattices(_115267)], (467 ^ _101732) ^ [_116109] : [v1_xboole_0(u1_struct_0(_116109)), -(v3_struct_0(_116109)), l1_struct_0(_116109)], (477 ^ _101732) ^ [_116386] : [489 ^ _101732 : [(490 ^ _101732) ^ [] : [-(m2_lattice4(488 ^ [_116386], _116386))], (492 ^ _101732) ^ [] : [v1_xboole_0(488 ^ [_116386])]], -(v3_struct_0(_116386)), v10_lattices(_116386), l3_lattices(_116386)], (495 ^ _101732) ^ [] : [-(v1_xboole_0(493 ^ []))], (498 ^ _101732) ^ [] : [v1_xboole_0(496 ^ [])], (501 ^ _101732) ^ [] : [-(l1_struct_0(499 ^ []))], (503 ^ _101732) ^ [] : [v3_struct_0(499 ^ [])], (505 ^ _101732) ^ [_117221, _117223] : [m1_subset_1(_117223, _117221), -(v1_xboole_0(_117221)), -(r2_hidden(_117223, _117221))], (515 ^ _101732) ^ [_117505] : [v1_xboole_0(_117505), -(_117505 = k1_xboole_0)], (521 ^ _101732) ^ [_117707, _117709] : [r2_hidden(_117709, _117707), r2_hidden(_117707, _117709)], (527 ^ _101732) ^ [_117932, _117934, _117936] : [-(r3_lattices(_117936, _117934, _117934)), -(v3_struct_0(_117936)), v6_lattices(_117936), v8_lattices(_117936), v9_lattices(_117936), l3_lattices(_117936), m1_subset_1(_117934, u1_struct_0(_117936)), m1_subset_1(_117932, u1_struct_0(_117936))], (558 ^ _101732) ^ [] : [-(l3_lattices(556 ^ []))], (561 ^ _101732) ^ [_118808] : [-(m1_subset_1(559 ^ [_118808], _118808))], (563 ^ _101732) ^ [_118934, _118936, _118938] : [590 ^ _101732 : [(591 ^ _101732) ^ [] : [r3_lattices(_118938, _118936, _118934), -(r1_lattices(_118938, _118936, _118934))], (597 ^ _101732) ^ [] : [r1_lattices(_118938, _118936, _118934), -(r3_lattices(_118938, _118936, _118934))]], -(v3_struct_0(_118938)), v6_lattices(_118938), v8_lattices(_118938), v9_lattices(_118938), l3_lattices(_118938), m1_subset_1(_118936, u1_struct_0(_118938)), m1_subset_1(_118934, u1_struct_0(_118938))], (603 ^ _101732) ^ [_119989, _119991, _119993] : [622 ^ _101732 : [(623 ^ _101732) ^ [] : [v1_xboole_0(k22_filter_2(_119993, _119991, _119989))], (625 ^ _101732) ^ [] : [-(m2_lattice4(k22_filter_2(_119993, _119991, _119989), _119993))]], -(v3_struct_0(_119993)), v10_lattices(_119993), l3_lattices(_119993), m1_subset_1(_119991, u1_struct_0(_119993)), m1_subset_1(_119989, u1_struct_0(_119993))], (627 ^ _101732) ^ [_120660] : [l3_lattices(_120660), 630 ^ _101732 : [(631 ^ _101732) ^ [] : [-(l1_lattices(_120660))], (633 ^ _101732) ^ [] : [-(l2_lattices(_120660))]]], (635 ^ _101732) ^ [] : [true___, -(true___)], (641 ^ _101732) ^ [] : [true___, -(true___)], (647 ^ _101732) ^ [_121155] : [l3_lattices(_121155), 658 ^ _101732 : [(659 ^ _101732) ^ [] : [v3_struct_0(_121155)], (661 ^ _101732) ^ [] : [-(v4_lattices(_121155))], (663 ^ _101732) ^ [] : [-(v5_lattices(_121155))], (665 ^ _101732) ^ [] : [-(v6_lattices(_121155))], (667 ^ _101732) ^ [] : [-(v7_lattices(_121155))], (669 ^ _101732) ^ [] : [-(v8_lattices(_121155))], (671 ^ _101732) ^ [] : [-(v9_lattices(_121155))]], -(v3_struct_0(_121155)), v10_lattices(_121155)], (673 ^ _101732) ^ [_121946, _121948] : [r2_hidden(_121948, _121946), -(m1_subset_1(_121948, _121946))], (679 ^ _101732) ^ [_122156, _122158] : [r2_hidden(_122158, _122156), v1_xboole_0(_122156)], (685 ^ _101732) ^ [_122329] : [-(v3_struct_0(_122329)), v10_lattices(_122329), l3_lattices(_122329), 696 ^ _101732 : [(697 ^ _101732) ^ [_122682] : [m1_subset_1(_122682, u1_struct_0(_122329)), 700 ^ _101732 : [(701 ^ _101732) ^ [_122865] : [m1_subset_1(_122865, u1_struct_0(_122329)), 704 ^ _101732 : [(705 ^ _101732) ^ [_123041] : [m1_subset_1(_123041, u1_struct_0(_122329)), r3_lattices(_122329, _122682, _122865), 712 ^ _101732 : [(713 ^ _101732) ^ [] : [r2_hidden(_123041, k22_filter_2(_122329, _122682, _122865)), 716 ^ _101732 : [(717 ^ _101732) ^ [] : [-(r3_lattices(_122329, _122682, _123041))], (719 ^ _101732) ^ [] : [-(r3_lattices(_122329, _123041, _122865))]]], (721 ^ _101732) ^ [] : [-(r2_hidden(_123041, k22_filter_2(_122329, _122682, _122865))), r3_lattices(_122329, _122682, _123041), r3_lattices(_122329, _123041, _122865)]]]]]]]]]], input).
% 0.36/1.40 ncf('1',plain,[r2_hidden(737 ^ [], k22_filter_2(730 ^ [], 737 ^ [], 740 ^ [])), r2_hidden(740 ^ [], k22_filter_2(730 ^ [], 737 ^ [], 740 ^ []))],start(746 ^ 0)).
% 0.36/1.40 ncf('1.1',plain,[-(r2_hidden(737 ^ [], k22_filter_2(730 ^ [], 737 ^ [], 740 ^ []))), 721 : r3_lattices(730 ^ [], 737 ^ [], 737 ^ []), 721 : r3_lattices(730 ^ [], 737 ^ [], 740 ^ []), 721 : m1_subset_1(737 ^ [], u1_struct_0(730 ^ [])), 721 : r3_lattices(730 ^ [], 737 ^ [], 740 ^ []), 705 : m1_subset_1(740 ^ [], u1_struct_0(730 ^ [])), 701 : m1_subset_1(737 ^ [], u1_struct_0(730 ^ [])), 697 : -(v3_struct_0(730 ^ [])), 697 : v10_lattices(730 ^ []), 697 : l3_lattices(730 ^ [])],extension(685 ^ 1,bind([[_122329, _122682, _122865, _123041], [730 ^ [], 737 ^ [], 740 ^ [], 737 ^ []]]))).
% 0.36/1.40 ncf('1.1.1',plain,[-(r3_lattices(730 ^ [], 737 ^ [], 737 ^ [])), -(v3_struct_0(730 ^ [])), v6_lattices(730 ^ []), v8_lattices(730 ^ []), v9_lattices(730 ^ []), l3_lattices(730 ^ []), m1_subset_1(737 ^ [], u1_struct_0(730 ^ [])), m1_subset_1(737 ^ [], u1_struct_0(730 ^ []))],extension(527 ^ 10,bind([[_117932, _117934, _117936], [737 ^ [], 737 ^ [], 730 ^ []]]))).
% 0.36/1.40 ncf('1.1.1.1',plain,[v3_struct_0(730 ^ [])],extension(732 ^ 11)).
% 0.36/1.40 ncf('1.1.1.2',plain,[-(v6_lattices(730 ^ [])), l3_lattices(730 ^ []), -(v3_struct_0(730 ^ [])), v10_lattices(730 ^ [])],extension(647 ^ 11,bind([[_121155], [730 ^ []]]))).
% 0.36/1.40 ncf('1.1.1.2.1',plain,[-(l3_lattices(730 ^ []))],extension(736 ^ 12)).
% 0.36/1.40 ncf('1.1.1.2.2',plain,[v3_struct_0(730 ^ [])],lemmata('[1, 1].x')).
% 0.36/1.40 ncf('1.1.1.2.3',plain,[-(v10_lattices(730 ^ []))],extension(734 ^ 12)).
% 0.36/1.40 ncf('1.1.1.3',plain,[-(v8_lattices(730 ^ [])), l3_lattices(730 ^ []), -(v3_struct_0(730 ^ [])), v10_lattices(730 ^ [])],extension(647 ^ 11,bind([[_121155], [730 ^ []]]))).
% 0.36/1.40 ncf('1.1.1.3.1',plain,[-(l3_lattices(730 ^ []))],extension(736 ^ 12)).
% 0.36/1.40 ncf('1.1.1.3.2',plain,[v3_struct_0(730 ^ [])],lemmata('[1, 1].x')).
% 0.36/1.40 ncf('1.1.1.3.3',plain,[-(v10_lattices(730 ^ []))],extension(734 ^ 12)).
% 0.36/1.40 ncf('1.1.1.4',plain,[-(v9_lattices(730 ^ [])), l3_lattices(730 ^ []), -(v3_struct_0(730 ^ [])), v10_lattices(730 ^ [])],extension(647 ^ 11,bind([[_121155], [730 ^ []]]))).
% 0.36/1.40 ncf('1.1.1.4.1',plain,[-(l3_lattices(730 ^ []))],extension(736 ^ 12)).
% 0.36/1.40 ncf('1.1.1.4.2',plain,[v3_struct_0(730 ^ [])],lemmata('[1, 1].x')).
% 0.36/1.40 ncf('1.1.1.4.3',plain,[-(v10_lattices(730 ^ []))],extension(734 ^ 12)).
% 0.36/1.40 ncf('1.1.1.5',plain,[-(l3_lattices(730 ^ []))],extension(736 ^ 11)).
% 0.36/1.40 ncf('1.1.1.6',plain,[-(m1_subset_1(737 ^ [], u1_struct_0(730 ^ [])))],extension(739 ^ 11)).
% 0.36/1.40 ncf('1.1.1.7',plain,[-(m1_subset_1(737 ^ [], u1_struct_0(730 ^ [])))],extension(739 ^ 11)).
% 0.36/1.40 ncf('1.1.2',plain,[-(r3_lattices(730 ^ [], 737 ^ [], 740 ^ []))],extension(744 ^ 10)).
% 0.36/1.40 ncf('1.1.3',plain,[-(m1_subset_1(737 ^ [], u1_struct_0(730 ^ [])))],extension(739 ^ 8)).
% 0.36/1.40 ncf('1.1.4',plain,[-(r3_lattices(730 ^ [], 737 ^ [], 740 ^ []))],extension(744 ^ 8)).
% 0.36/1.40 ncf('1.1.5',plain,[-(m1_subset_1(740 ^ [], u1_struct_0(730 ^ [])))],extension(742 ^ 6)).
% 0.36/1.40 ncf('1.1.6',plain,[-(m1_subset_1(737 ^ [], u1_struct_0(730 ^ [])))],extension(739 ^ 4)).
% 0.36/1.40 ncf('1.1.7',plain,[v3_struct_0(730 ^ [])],extension(732 ^ 2)).
% 0.36/1.40 ncf('1.1.8',plain,[-(v10_lattices(730 ^ []))],extension(734 ^ 2)).
% 0.36/1.40 ncf('1.1.9',plain,[-(l3_lattices(730 ^ []))],extension(736 ^ 2)).
% 0.36/1.40 ncf('1.2',plain,[-(r2_hidden(740 ^ [], k22_filter_2(730 ^ [], 737 ^ [], 740 ^ []))), 721 : r3_lattices(730 ^ [], 737 ^ [], 740 ^ []), 721 : r3_lattices(730 ^ [], 740 ^ [], 740 ^ []), 721 : m1_subset_1(740 ^ [], u1_struct_0(730 ^ [])), 721 : r3_lattices(730 ^ [], 737 ^ [], 740 ^ []), 705 : m1_subset_1(740 ^ [], u1_struct_0(730 ^ [])), 701 : m1_subset_1(737 ^ [], u1_struct_0(730 ^ [])), 697 : -(v3_struct_0(730 ^ [])), 697 : v10_lattices(730 ^ []), 697 : l3_lattices(730 ^ [])],extension(685 ^ 1,bind([[_122329, _122682, _122865, _123041], [730 ^ [], 737 ^ [], 740 ^ [], 740 ^ []]]))).
% 0.36/1.40 ncf('1.2.1',plain,[-(r3_lattices(730 ^ [], 737 ^ [], 740 ^ []))],extension(744 ^ 10)).
% 0.36/1.40 ncf('1.2.2',plain,[-(r3_lattices(730 ^ [], 740 ^ [], 740 ^ [])), -(v3_struct_0(730 ^ [])), v6_lattices(730 ^ []), v8_lattices(730 ^ []), v9_lattices(730 ^ []), l3_lattices(730 ^ []), m1_subset_1(740 ^ [], u1_struct_0(730 ^ [])), m1_subset_1(737 ^ [], u1_struct_0(730 ^ []))],extension(527 ^ 10,bind([[_117932, _117934, _117936], [737 ^ [], 740 ^ [], 730 ^ []]]))).
% 0.36/1.40 ncf('1.2.2.1',plain,[v3_struct_0(730 ^ [])],extension(732 ^ 11)).
% 0.36/1.40 ncf('1.2.2.2',plain,[-(v6_lattices(730 ^ [])), l3_lattices(730 ^ []), -(v3_struct_0(730 ^ [])), v10_lattices(730 ^ [])],extension(647 ^ 11,bind([[_121155], [730 ^ []]]))).
% 0.36/1.40 ncf('1.2.2.2.1',plain,[-(l3_lattices(730 ^ []))],extension(736 ^ 12)).
% 0.36/1.40 ncf('1.2.2.2.2',plain,[v3_struct_0(730 ^ [])],lemmata('[2, 1].x')).
% 0.36/1.40 ncf('1.2.2.2.3',plain,[-(v10_lattices(730 ^ []))],extension(734 ^ 12)).
% 0.36/1.40 ncf('1.2.2.3',plain,[-(v8_lattices(730 ^ [])), l3_lattices(730 ^ []), -(v3_struct_0(730 ^ [])), v10_lattices(730 ^ [])],extension(647 ^ 11,bind([[_121155], [730 ^ []]]))).
% 0.36/1.40 ncf('1.2.2.3.1',plain,[-(l3_lattices(730 ^ []))],extension(736 ^ 12)).
% 0.36/1.40 ncf('1.2.2.3.2',plain,[v3_struct_0(730 ^ [])],lemmata('[2, 1].x')).
% 0.36/1.40 ncf('1.2.2.3.3',plain,[-(v10_lattices(730 ^ []))],extension(734 ^ 12)).
% 0.36/1.40 ncf('1.2.2.4',plain,[-(v9_lattices(730 ^ [])), l3_lattices(730 ^ []), -(v3_struct_0(730 ^ [])), v10_lattices(730 ^ [])],extension(647 ^ 11,bind([[_121155], [730 ^ []]]))).
% 0.36/1.40 ncf('1.2.2.4.1',plain,[-(l3_lattices(730 ^ []))],extension(736 ^ 12)).
% 0.36/1.40 ncf('1.2.2.4.2',plain,[v3_struct_0(730 ^ [])],lemmata('[2, 1].x')).
% 0.36/1.40 ncf('1.2.2.4.3',plain,[-(v10_lattices(730 ^ []))],extension(734 ^ 12)).
% 0.36/1.40 ncf('1.2.2.5',plain,[-(l3_lattices(730 ^ []))],extension(736 ^ 11)).
% 0.36/1.40 ncf('1.2.2.6',plain,[-(m1_subset_1(740 ^ [], u1_struct_0(730 ^ [])))],extension(742 ^ 11)).
% 0.36/1.40 ncf('1.2.2.7',plain,[-(m1_subset_1(737 ^ [], u1_struct_0(730 ^ [])))],extension(739 ^ 11)).
% 0.36/1.40 ncf('1.2.3',plain,[-(m1_subset_1(740 ^ [], u1_struct_0(730 ^ [])))],extension(742 ^ 8)).
% 0.36/1.40 ncf('1.2.4',plain,[-(r3_lattices(730 ^ [], 737 ^ [], 740 ^ []))],extension(744 ^ 8)).
% 0.36/1.40 ncf('1.2.5',plain,[-(m1_subset_1(740 ^ [], u1_struct_0(730 ^ [])))],extension(742 ^ 6)).
% 0.36/1.40 ncf('1.2.6',plain,[-(m1_subset_1(737 ^ [], u1_struct_0(730 ^ [])))],extension(739 ^ 4)).
% 0.36/1.40 ncf('1.2.7',plain,[v3_struct_0(730 ^ [])],extension(732 ^ 2)).
% 0.36/1.40 ncf('1.2.8',plain,[-(v10_lattices(730 ^ []))],extension(734 ^ 2)).
% 0.36/1.40 ncf('1.2.9',plain,[-(l3_lattices(730 ^ []))],extension(736 ^ 2)).
% 0.36/1.40 %-----------------------------------------------------
% 0.36/1.40 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------