%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU408+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n021.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 12:03:26 EDT 2023
% Result : Theorem 0.91s 1.38s
% Output : Proof 0.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU408+1 : TPTP v8.1.2. Released v3.4.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n021.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 12:34:42 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.91/1.38
% 0.91/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.91/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.91/1.38 %-----------------------------------------------------
% 0.91/1.38 ncf(matrix, plain, [(705 ^ _110876) ^ [] : [v3_struct_0(703 ^ [])], (707 ^ _110876) ^ [] : [-(v2_orders_2(703 ^ []))], (709 ^ _110876) ^ [] : [-(v3_orders_2(703 ^ []))], (711 ^ _110876) ^ [] : [-(v4_orders_2(703 ^ []))], (713 ^ _110876) ^ [] : [-(v1_lattice3(703 ^ []))], (715 ^ _110876) ^ [] : [-(l1_orders_2(703 ^ []))], (718 ^ _110876) ^ [] : [v3_struct_0(716 ^ [])], (720 ^ _110876) ^ [] : [-(v2_orders_2(716 ^ []))], (722 ^ _110876) ^ [] : [-(v3_orders_2(716 ^ []))], (724 ^ _110876) ^ [] : [-(v4_orders_2(716 ^ []))], (726 ^ _110876) ^ [] : [-(v1_lattice3(716 ^ []))], (728 ^ _110876) ^ [] : [-(l1_orders_2(716 ^ []))], (731 ^ _110876) ^ [] : [-(r2_hidden(729 ^ [], u1_struct_0(716 ^ [])))], (733 ^ _110876) ^ [] : [m1_subset_1(729 ^ [], u1_struct_0(k1_latsum_1(703 ^ [], 716 ^ [])))], (198 ^ _110876) ^ [_117186, _117188, _117190, _117192] : [-(k2_zfmisc_1(_117192, _117188) = k2_zfmisc_1(_117190, _117186)), _117192 = _117190, _117188 = _117186], (208 ^ _110876) ^ [_117517, _117519] : [_117519 = _117517, -(u1_orders_2(_117519) = u1_orders_2(_117517))], (214 ^ _110876) ^ [_117763, _117765, _117767, _117769] : [-(g1_orders_2(_117769, _117765) = g1_orders_2(_117767, _117763)), _117769 = _117767, _117765 = _117763], (224 ^ _110876) ^ [_118234, _118236, _118238, _118240, _118242, _118244, _118246, _118248, _118250, _118252, _118254, _118256] : [-(k7_relset_1(_118256, _118252, _118248, _118244, _118240, _118236) = k7_relset_1(_118254, _118250, _118246, _118242, _118238, _118234)), _118256 = _118254, _118252 = _118250, _118248 = _118246, _118244 = _118242, _118240 = _118238, _118236 = _118234], (250 ^ _110876) ^ [_119205, _119207, _119209, _119211] : [-(k5_relat_1(_119211, _119207) = k5_relat_1(_119209, _119205)), _119211 = _119209, _119207 = _119205], (260 ^ _110876) ^ [_119564, _119566, _119568, _119570] : [-(k2_xboole_0(_119570, _119566) = k2_xboole_0(_119568, _119564)), _119570 = _119568, _119566 = _119564], (270 ^ _110876) ^ [_119895, _119897] : [_119897 = _119895, -(k1_zfmisc_1(_119897) = k1_zfmisc_1(_119895))], (276 ^ _110876) ^ [_120113, _120115] : [_120115 = _120113, -(u1_struct_0(_120115) = u1_struct_0(_120113))], (282 ^ _110876) ^ [_120339, _120341, _120343, _120345] : [-(k1_latsum_1(_120345, _120341) = k1_latsum_1(_120343, _120339)), _120345 = _120343, _120341 = _120339], (2 ^ _110876) ^ [_111020] : [-(_111020 = _111020)], (4 ^ _110876) ^ [_111127, _111129] : [_111129 = _111127, -(_111127 = _111129)], (10 ^ _110876) ^ [_111331, _111333, _111335] : [-(_111335 = _111331), _111335 = _111333, _111333 = _111331], (20 ^ _110876) ^ [_111644, _111646] : [-(v1_relat_1(_111644)), _111646 = _111644, v1_relat_1(_111646)], (30 ^ _110876) ^ [_111939, _111941] : [-(v1_orders_2(_111939)), _111941 = _111939, v1_orders_2(_111941)], (40 ^ _110876) ^ [_112234, _112236] : [-(l1_struct_0(_112234)), _112236 = _112234, l1_struct_0(_112236)], (50 ^ _110876) ^ [_112585, _112587, _112589, _112591, _112593, _112595] : [-(m2_relset_1(_112593, _112589, _112585)), m2_relset_1(_112595, _112591, _112587), _112595 = _112593, _112591 = _112589, _112587 = _112585], (68 ^ _110876) ^ [_113194, _113196, _113198, _113200, _113202, _113204] : [-(m1_relset_1(_113202, _113198, _113194)), m1_relset_1(_113204, _113200, _113196), _113204 = _113202, _113200 = _113198, _113196 = _113194], (86 ^ _110876) ^ [_113775, _113777, _113779, _113781] : [-(r1_tarski(_113779, _113775)), r1_tarski(_113781, _113777), _113781 = _113779, _113777 = _113775], (100 ^ _110876) ^ [_114191, _114193] : [-(v1_xboole_0(_114191)), _114193 = _114191, v1_xboole_0(_114193)], (110 ^ _110876) ^ [_114486, _114488] : [-(v3_struct_0(_114486)), _114488 = _114486, v3_struct_0(_114488)], (120 ^ _110876) ^ [_114781, _114783] : [-(v2_orders_2(_114781)), _114783 = _114781, v2_orders_2(_114783)], (130 ^ _110876) ^ [_115076, _115078] : [-(v3_orders_2(_115076)), _115078 = _115076, v3_orders_2(_115078)], (140 ^ _110876) ^ [_115371, _115373] : [-(v4_orders_2(_115371)), _115373 = _115371, v4_orders_2(_115373)], (150 ^ _110876) ^ [_115666, _115668] : [-(v1_lattice3(_115666)), _115668 = _115666, v1_lattice3(_115668)], (160 ^ _110876) ^ [_115961, _115963] : [-(l1_orders_2(_115961)), _115963 = _115961, l1_orders_2(_115963)], (170 ^ _110876) ^ [_116284, _116286, _116288, _116290] : [-(r2_hidden(_116288, _116284)), r2_hidden(_116290, _116286), _116290 = _116288, _116286 = _116284], (184 ^ _110876) ^ [_116708, _116710, _116712, _116714] : [-(m1_subset_1(_116712, _116708)), m1_subset_1(_116714, _116710), _116714 = _116712, _116710 = _116708], (292 ^ _110876) ^ [_120722] : [l1_orders_2(_120722), v1_orders_2(_120722), -(_120722 = g1_orders_2(u1_struct_0(_120722), u1_orders_2(_120722)))], (302 ^ _110876) ^ [_121021, _121023] : [r2_hidden(_121023, _121021), r2_hidden(_121021, _121023)], (308 ^ _110876) ^ [_121246, _121248, _121250] : [m1_subset_1(_121246, k1_zfmisc_1(k2_zfmisc_1(_121250, _121248))), -(v1_relat_1(_121246))], (314 ^ _110876) ^ [_121455, _121457] : [-(k2_xboole_0(_121457, _121455) = k2_xboole_0(_121455, _121457))], (316 ^ _110876) ^ [_121556] : [l1_orders_2(_121556), 319 ^ _110876 : [(320 ^ _110876) ^ [_121756] : [l1_orders_2(_121756), 323 ^ _110876 : [(324 ^ _110876) ^ [_121952] : [v1_orders_2(_121952), l1_orders_2(_121952), 331 ^ _110876 : [(332 ^ _110876) ^ [] : [_121952 = k1_latsum_1(_121556, _121756), 335 ^ _110876 : [(336 ^ _110876) ^ [] : [-(u1_struct_0(_121952) = k2_xboole_0(u1_struct_0(_121556), u1_struct_0(_121756)))], (338 ^ _110876) ^ [] : [-(u1_orders_2(_121952) = k2_xboole_0(k2_xboole_0(u1_orders_2(_121556), u1_orders_2(_121756)), k7_relset_1(u1_struct_0(_121556), u1_struct_0(_121556), u1_struct_0(_121756), u1_struct_0(_121756), u1_orders_2(_121556), u1_orders_2(_121756))))]]], (340 ^ _110876) ^ [] : [-(_121952 = k1_latsum_1(_121556, _121756)), u1_struct_0(_121952) = k2_xboole_0(u1_struct_0(_121556), u1_struct_0(_121756)), u1_orders_2(_121952) = k2_xboole_0(k2_xboole_0(u1_orders_2(_121556), u1_orders_2(_121756)), k7_relset_1(u1_struct_0(_121556), u1_struct_0(_121556), u1_struct_0(_121756), u1_struct_0(_121756), u1_orders_2(_121556), u1_orders_2(_121756)))]]]]]]], (372 ^ _110876) ^ [_123594, _123596, _123598] : [-(_123594 = k2_xboole_0(_123598, _123596)), 376 ^ _110876 : [(377 ^ _110876) ^ [] : [-(r2_hidden(373 ^ [_123594, _123596, _123598], _123594))], (379 ^ _110876) ^ [] : [r2_hidden(373 ^ [_123594, _123596, _123598], _123598)], (381 ^ _110876) ^ [] : [r2_hidden(373 ^ [_123594, _123596, _123598], _123596)]], 382 ^ _110876 : [(389 ^ _110876) ^ [] : [r2_hidden(373 ^ [_123594, _123596, _123598], _123594)], (383 ^ _110876) ^ [] : [-(r2_hidden(373 ^ [_123594, _123596, _123598], _123598)), -(r2_hidden(373 ^ [_123594, _123596, _123598], _123596))]]], (350 ^ _110876) ^ [_122869, _122871, _122873] : [_122869 = k2_xboole_0(_122873, _122871), 353 ^ _110876 : [(364 ^ _110876) ^ [_123329] : [365 ^ _110876 : [(366 ^ _110876) ^ [] : [r2_hidden(_123329, _122873)], (368 ^ _110876) ^ [] : [r2_hidden(_123329, _122871)]], -(r2_hidden(_123329, _122869))], (354 ^ _110876) ^ [_123051] : [r2_hidden(_123051, _122869), -(r2_hidden(_123051, _122873)), -(r2_hidden(_123051, _122871))]]], (393 ^ _110876) ^ [_124345, _124347] : [m1_relset_1(_124345, _124347, _124347), 396 ^ _110876 : [(397 ^ _110876) ^ [] : [-(v1_orders_2(g1_orders_2(_124347, _124345)))], (399 ^ _110876) ^ [] : [-(l1_orders_2(g1_orders_2(_124347, _124345)))]]], (401 ^ _110876) ^ [_124640, _124642] : [408 ^ _110876 : [(409 ^ _110876) ^ [] : [-(v1_orders_2(k1_latsum_1(_124642, _124640)))], (411 ^ _110876) ^ [] : [-(l1_orders_2(k1_latsum_1(_124642, _124640)))]], l1_orders_2(_124642), l1_orders_2(_124640)], (413 ^ _110876) ^ [] : [true___, -(true___)], (419 ^ _110876) ^ [] : [true___, -(true___)], (425 ^ _110876) ^ [] : [true___, -(true___)], (431 ^ _110876) ^ [] : [true___, -(true___)], (437 ^ _110876) ^ [_125494, _125496] : [-(v1_relat_1(k5_relat_1(_125496, _125494))), v1_relat_1(_125496), v1_relat_1(_125494)], (447 ^ _110876) ^ [_125849, _125851, _125853, _125855, _125857, _125859] : [-(m2_relset_1(k7_relset_1(_125859, _125857, _125855, _125853, _125851, _125849), _125859, _125853)), m1_relset_1(_125851, _125859, _125857), m1_relset_1(_125849, _125855, _125853)], (457 ^ _110876) ^ [_126194] : [l1_orders_2(_126194), -(l1_struct_0(_126194))], (463 ^ _110876) ^ [] : [true___, -(true___)], (469 ^ _110876) ^ [] : [true___, -(true___)], (475 ^ _110876) ^ [] : [true___, -(true___)], (481 ^ _110876) ^ [_126765, _126767, _126769] : [m2_relset_1(_126765, _126769, _126767), -(m1_subset_1(_126765, k1_zfmisc_1(k2_zfmisc_1(_126769, _126767))))], (487 ^ _110876) ^ [_126979] : [l1_orders_2(_126979), -(m2_relset_1(u1_orders_2(_126979), u1_struct_0(_126979), u1_struct_0(_126979)))], (493 ^ _110876) ^ [] : [true___, -(true___)], (500 ^ _110876) ^ [] : [-(l1_orders_2(498 ^ []))], (503 ^ _110876) ^ [] : [-(l1_struct_0(501 ^ []))], (506 ^ _110876) ^ [_127519, _127521] : [-(m1_relset_1(504 ^ [_127519, _127521], _127521, _127519))], (509 ^ _110876) ^ [_127646] : [-(m1_subset_1(507 ^ [_127646], _127646))], (512 ^ _110876) ^ [_127785, _127787] : [-(m2_relset_1(510 ^ [_127785, _127787], _127787, _127785))], (514 ^ _110876) ^ [_127902, _127904] : [525 ^ _110876 : [(526 ^ _110876) ^ [] : [v3_struct_0(k1_latsum_1(_127904, _127902))], (528 ^ _110876) ^ [] : [-(v1_orders_2(k1_latsum_1(_127904, _127902)))]], l1_orders_2(_127904), -(v3_struct_0(_127902)), l1_orders_2(_127902)], (530 ^ _110876) ^ [_128357] : [v1_xboole_0(u1_struct_0(_128357)), -(v3_struct_0(_128357)), l1_struct_0(_128357)], (540 ^ _110876) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (542 ^ _110876) ^ [_128701, _128703] : [553 ^ _110876 : [(554 ^ _110876) ^ [] : [v3_struct_0(k1_latsum_1(_128703, _128701))], (556 ^ _110876) ^ [] : [-(v1_orders_2(k1_latsum_1(_128703, _128701)))]], -(v3_struct_0(_128703)), l1_orders_2(_128703), l1_orders_2(_128701)], (558 ^ _110876) ^ [_129170, _129172] : [-(v1_xboole_0(_129172)), v1_xboole_0(k2_xboole_0(_129172, _129170))], (564 ^ _110876) ^ [_129386, _129388] : [-(v1_xboole_0(_129388)), v1_xboole_0(k2_xboole_0(_129386, _129388))], (570 ^ _110876) ^ [_129602, _129604] : [m1_relset_1(_129602, _129604, _129604), 573 ^ _110876 : [(574 ^ _110876) ^ [_129772, _129774] : [g1_orders_2(_129604, _129602) = g1_orders_2(_129774, _129772), 577 ^ _110876 : [(578 ^ _110876) ^ [] : [-(_129604 = _129774)], (580 ^ _110876) ^ [] : [-(_129602 = _129772)]]]]], (582 ^ _110876) ^ [_130079, _130081] : [-(k2_xboole_0(_130081, _130081) = _130081)], (585 ^ _110876) ^ [] : [-(v1_xboole_0(583 ^ []))], (588 ^ _110876) ^ [] : [v1_xboole_0(586 ^ [])], (591 ^ _110876) ^ [] : [-(l1_struct_0(589 ^ []))], (593 ^ _110876) ^ [] : [v3_struct_0(589 ^ [])], (595 ^ _110876) ^ [_130506] : [603 ^ _110876 : [(604 ^ _110876) ^ [] : [-(m1_subset_1(602 ^ [_130506], k1_zfmisc_1(u1_struct_0(_130506))))], (606 ^ _110876) ^ [] : [v1_xboole_0(602 ^ [_130506])]], -(v3_struct_0(_130506)), l1_struct_0(_130506)], (608 ^ _110876) ^ [_130997, _130999, _131001, _131003, _131005, _131007] : [-(k7_relset_1(_131007, _131005, _131003, _131001, _130999, _130997) = k5_relat_1(_130999, _130997)), m1_relset_1(_130999, _131007, _131005), m1_relset_1(_130997, _131003, _131001)], (618 ^ _110876) ^ [_131403, _131405, _131407] : [m2_relset_1(_131403, _131407, _131405), -(m1_relset_1(_131403, _131407, _131405))], (624 ^ _110876) ^ [_131575, _131577, _131579] : [m1_relset_1(_131575, _131579, _131577), -(m2_relset_1(_131575, _131579, _131577))], (630 ^ _110876) ^ [_131782, _131784] : [-(r1_tarski(_131784, _131784))], (632 ^ _110876) ^ [_131862] : [-(k2_xboole_0(_131862, k1_xboole_0) = _131862)], (634 ^ _110876) ^ [_131972, _131974] : [r2_hidden(_131974, _131972), -(m1_subset_1(_131974, _131972))], (640 ^ _110876) ^ [_132182, _132184] : [m1_subset_1(_132184, _132182), -(v1_xboole_0(_132182)), -(r2_hidden(_132184, _132182))], (650 ^ _110876) ^ [_132509, _132511] : [m1_subset_1(_132511, k1_zfmisc_1(_132509)), -(r1_tarski(_132511, _132509))], (656 ^ _110876) ^ [_132675, _132677] : [r1_tarski(_132677, _132675), -(m1_subset_1(_132677, k1_zfmisc_1(_132675)))], (662 ^ _110876) ^ [_132905, _132907, _132909] : [-(m1_subset_1(_132909, _132905)), r2_hidden(_132909, _132907), m1_subset_1(_132907, k1_zfmisc_1(_132905))], (672 ^ _110876) ^ [_133232, _133234, _133236] : [r2_hidden(_133236, _133234), m1_subset_1(_133234, k1_zfmisc_1(_133232)), v1_xboole_0(_133232)], (682 ^ _110876) ^ [_133528] : [v1_xboole_0(_133528), -(_133528 = k1_xboole_0)], (688 ^ _110876) ^ [_133730, _133732] : [r2_hidden(_133732, _133730), v1_xboole_0(_133730)], (694 ^ _110876) ^ [_133917, _133919] : [v1_xboole_0(_133919), -(_133919 = _133917), v1_xboole_0(_133917)]], input).
% 0.91/1.38 ncf('1',plain,[v3_struct_0(716 ^ [])],start(718 ^ 0)).
% 0.91/1.38 ncf('1.1',plain,[-(v3_struct_0(716 ^ [])), 528 : -(v1_orders_2(k1_latsum_1(703 ^ [], 716 ^ []))), 528 : l1_orders_2(703 ^ []), 528 : l1_orders_2(716 ^ [])],extension(514 ^ 1,bind([[_127902, _127904], [716 ^ [], 703 ^ []]]))).
% 0.91/1.38 ncf('1.1.1',plain,[v1_orders_2(k1_latsum_1(703 ^ [], 716 ^ [])), 324 : l1_orders_2(k1_latsum_1(703 ^ [], 716 ^ [])), 332 : k1_latsum_1(703 ^ [], 716 ^ []) = k1_latsum_1(703 ^ [], 716 ^ []), 336 : -(u1_struct_0(k1_latsum_1(703 ^ [], 716 ^ [])) = k2_xboole_0(u1_struct_0(703 ^ []), u1_struct_0(716 ^ []))), 324 : l1_orders_2(716 ^ []), 320 : l1_orders_2(703 ^ [])],extension(316 ^ 4,bind([[_121556, _121756, _121952], [703 ^ [], 716 ^ [], k1_latsum_1(703 ^ [], 716 ^ [])]]))).
% 0.91/1.38 ncf('1.1.1.1',plain,[-(l1_orders_2(k1_latsum_1(703 ^ [], 716 ^ []))), l1_orders_2(703 ^ []), l1_orders_2(716 ^ [])],extension(401 ^ 9,bind([[_124640, _124642], [716 ^ [], 703 ^ []]]))).
% 0.91/1.38 ncf('1.1.1.1.1',plain,[-(l1_orders_2(703 ^ []))],extension(715 ^ 10)).
% 0.91/1.38 ncf('1.1.1.1.2',plain,[-(l1_orders_2(716 ^ []))],extension(728 ^ 10)).
% 0.91/1.38 ncf('1.1.1.2',plain,[-(k1_latsum_1(703 ^ [], 716 ^ []) = k1_latsum_1(703 ^ [], 716 ^ [])), 703 ^ [] = 703 ^ [], 716 ^ [] = 716 ^ []],extension(282 ^ 11,bind([[_120339, _120341, _120343, _120345], [716 ^ [], 716 ^ [], 703 ^ [], 703 ^ []]]))).
% 0.91/1.38 ncf('1.1.1.2.1',plain,[-(703 ^ [] = 703 ^ [])],extension(2 ^ 12,bind([[_111020], [703 ^ []]]))).
% 0.91/1.38 ncf('1.1.1.2.2',plain,[-(716 ^ [] = 716 ^ [])],extension(2 ^ 12,bind([[_111020], [716 ^ []]]))).
% 0.91/1.38 ncf('1.1.1.3',plain,[u1_struct_0(k1_latsum_1(703 ^ [], 716 ^ [])) = k2_xboole_0(u1_struct_0(703 ^ []), u1_struct_0(716 ^ [])), 368 : r2_hidden(729 ^ [], u1_struct_0(716 ^ [])), 368 : -(r2_hidden(729 ^ [], u1_struct_0(k1_latsum_1(703 ^ [], 716 ^ []))))],extension(350 ^ 13,bind([[_122869, _122871, _122873, _123329], [u1_struct_0(k1_latsum_1(703 ^ [], 716 ^ [])), u1_struct_0(716 ^ []), u1_struct_0(703 ^ []), 729 ^ []]]))).
% 0.91/1.38 ncf('1.1.1.3.1',plain,[-(r2_hidden(729 ^ [], u1_struct_0(716 ^ [])))],extension(731 ^ 18)).
% 0.91/1.38 ncf('1.1.1.3.2',plain,[r2_hidden(729 ^ [], u1_struct_0(k1_latsum_1(703 ^ [], 716 ^ []))), -(m1_subset_1(729 ^ [], u1_struct_0(k1_latsum_1(703 ^ [], 716 ^ []))))],extension(634 ^ 16,bind([[_131972, _131974], [u1_struct_0(k1_latsum_1(703 ^ [], 716 ^ [])), 729 ^ []]]))).
% 0.91/1.38 ncf('1.1.1.3.2.1',plain,[m1_subset_1(729 ^ [], u1_struct_0(k1_latsum_1(703 ^ [], 716 ^ [])))],extension(733 ^ 17)).
% 0.91/1.38 ncf('1.1.1.4',plain,[-(l1_orders_2(716 ^ []))],extension(728 ^ 7)).
% 0.91/1.38 ncf('1.1.1.5',plain,[-(l1_orders_2(703 ^ []))],extension(715 ^ 5)).
% 0.91/1.38 ncf('1.1.2',plain,[-(l1_orders_2(703 ^ []))],extension(715 ^ 2)).
% 0.91/1.38 ncf('1.1.3',plain,[-(l1_orders_2(716 ^ []))],extension(728 ^ 2)).
% 0.91/1.38 %-----------------------------------------------------
% 0.91/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------