%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUN065+2 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n022.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 : 600s
% DateTime : Mon Jul 18 16:33:36 EDT 2022
% Result : Theorem 29.49s 29.39s
% Output : Proof 29.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUN065+2 : TPTP v8.1.0. Released v7.3.0.
% 0.12/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n022.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 : 600
% 0.12/0.33 % DateTime : Thu Jun 2 09:15:51 EDT 2022
% 0.12/0.33 % CPUTime :
% 29.49/29.39 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.49/29.39 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.49/29.40
% 29.49/29.40 %-----------------------------------------------------
% 29.49/29.40 fof(nononesexist, conjecture, ? [_45691] : (! [_45699] : (! [_45707] : (~ r1(_45707) | ~ r2(_45707, _45699)) | (! _45691) = _45699) & ! [_45744] : (~ r1(_45744) | (! _45691) = _45744)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', nononesexist)).
% 29.49/29.40 fof(axiom_2, axiom, ! [_46069] : ? [_46077] : ! [_46085] : (~ r2(_46069, _46085) & (! _46085) = _46077 | r2(_46069, _46085) & _46085 = _46077), file('/export/starexec/sandbox/benchmark/Axioms/NUM008+0.ax', axiom_2)).
% 29.49/29.40 fof(axiom_1a, axiom, ! [_46392, _46395] : ? [_46403] : (? [_46411] : (? [_46419] : (r2(_46395, _46419) & r3(_46392, _46419, _46411)) & _46411 = _46403) & ? [_46456] : (r2(_46456, _46403) & r3(_46392, _46395, _46456))), file('/export/starexec/sandbox/benchmark/Axioms/NUM008+0.ax', axiom_1a)).
% 29.49/29.40 fof(axiom_3a, axiom, ! [_46761, _46764] : (! [_46772] : (! [_46780] : (~ r2(_46761, _46780) | (! _46780) = _46772) | ~ r2(_46764, _46772)) | _46761 = _46764), file('/export/starexec/sandbox/benchmark/Axioms/NUM008+0.ax', axiom_3a)).
% 29.49/29.40 fof(axiom_7a, axiom, ! [_47044, _47047] : (! [_47055] : (~ r1(_47055) | (! _47055) = _47047) | ~ r2(_47044, _47047)), file('/export/starexec/sandbox/benchmark/Axioms/NUM008+0.ax', axiom_7a)).
% 29.49/29.40
% 29.49/29.40 cnf(1, plain, [-(35 ^ [_21578]), -(_21578 = 34 ^ [_21578])], clausify(nononesexist)).
% 29.49/29.40 cnf(2, plain, [-(35 ^ [_21578]), -(r1(34 ^ [_21578]))], clausify(nononesexist)).
% 29.49/29.40 cnf(3, plain, [-(33 ^ [_21578]), -(_21578 = 31 ^ [_21578])], clausify(nononesexist)).
% 29.49/29.40 cnf(4, plain, [-(33 ^ [_21578]), -(r2(32 ^ [_21578], 31 ^ [_21578]))], clausify(nononesexist)).
% 29.49/29.40 cnf(5, plain, [-(33 ^ [_21578]), -(r1(32 ^ [_21578]))], clausify(nononesexist)).
% 29.49/29.40 cnf(6, plain, [-(6 ^ [_23100, _14397]), -(_23100 = 4 ^ [_14397])], clausify(axiom_2)).
% 29.49/29.40 cnf(7, plain, [-(6 ^ [_23100, _14397]), -(r2(_14397, _23100))], clausify(axiom_2)).
% 29.49/29.40 cnf(8, plain, [-(5 ^ [_23100, _14397]), _23100 = 4 ^ [_14397]], clausify(axiom_2)).
% 29.49/29.40 cnf(9, plain, [-(5 ^ [_23100, _14397]), r2(_14397, _23100)], clausify(axiom_2)).
% 29.49/29.40 cnf(10, plain, [33 ^ [_21578], 35 ^ [_21578]], clausify(nononesexist)).
% 29.49/29.40 cnf(11, plain, [5 ^ [_23100, _14397], 6 ^ [_23100, _14397]], clausify(axiom_2)).
% 29.49/29.40 cnf(12, plain, [-(r2(_16650, 15 ^ [_16650, _16565]))], clausify(axiom_1a)).
% 29.49/29.40 cnf(13, plain, [-(_18571 = _18644), r2(_18644, _18726), r2(_18571, _18801), _18801 = _18726], clausify(axiom_3a)).
% 29.49/29.40 cnf(14, plain, [r2(_20921, _20982), r1(_21052), _21052 = _20982], clausify(axiom_7a)).
% 29.49/29.40 cnf(15, plain, [-(_9938 = _9938)], theory(equality)).
% 29.49/29.40 cnf(16, plain, [_10091 = _10136, -(_10136 = _10091)], theory(equality)).
% 29.49/29.40 cnf(17, plain, [-(r2(_11242, _11373)), r2(_11175, _11308), _11175 = _11242, _11308 = _11373], theory(equality)).
% 29.49/29.40
% 29.49/29.40 cnf('1',plain,[33 ^ [4 ^ [4 ^ [_29594]]], 35 ^ [4 ^ [4 ^ [_29594]]]],start(10,bind([[_21578], [4 ^ [4 ^ [_29594]]]]))).
% 29.49/29.40 cnf('1.1',plain,[-(33 ^ [4 ^ [4 ^ [_29594]]]), -(4 ^ [4 ^ [_29594]] = 31 ^ [4 ^ [4 ^ [_29594]]])],extension(3,bind([[_21578], [4 ^ [4 ^ [_29594]]]]))).
% 29.49/29.40 cnf('1.1.1',plain,[4 ^ [4 ^ [_29594]] = 31 ^ [4 ^ [4 ^ [_29594]]], -(32 ^ [4 ^ [4 ^ [_29594]]] = 4 ^ [_29594]), r2(4 ^ [_29594], 31 ^ [4 ^ [4 ^ [_29594]]]), r2(32 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [4 ^ [_29594]])],extension(13,bind([[_18644, _18726, _18571, _18801], [4 ^ [_29594], 31 ^ [4 ^ [4 ^ [_29594]]], 32 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [4 ^ [_29594]]]]))).
% 29.49/29.40 cnf('1.1.1.1',plain,[32 ^ [4 ^ [4 ^ [_29594]]] = 4 ^ [_29594], -(5 ^ [32 ^ [4 ^ [4 ^ [_29594]]], _29594])],extension(8,bind([[_23100, _14397], [32 ^ [4 ^ [4 ^ [_29594]]], _29594]]))).
% 29.49/29.40 cnf('1.1.1.1.1',plain,[5 ^ [32 ^ [4 ^ [4 ^ [_29594]]], _29594], 6 ^ [32 ^ [4 ^ [4 ^ [_29594]]], _29594]],extension(11,bind([[_23100, _14397], [32 ^ [4 ^ [4 ^ [_29594]]], _29594]]))).
% 29.49/29.40 cnf('1.1.1.1.1.1',plain,[-(6 ^ [32 ^ [4 ^ [4 ^ [_29594]]], _29594]), -(r2(_29594, 32 ^ [4 ^ [4 ^ [_29594]]]))],extension(7,bind([[_14397, _23100], [_29594, 32 ^ [4 ^ [4 ^ [_29594]]]]]))).
% 29.49/29.40 cnf('1.1.1.1.1.1.1',plain,[r2(_29594, 32 ^ [4 ^ [4 ^ [_29594]]]), r1(32 ^ [4 ^ [4 ^ [_29594]]]), 32 ^ [4 ^ [4 ^ [_29594]]] = 32 ^ [4 ^ [4 ^ [_29594]]]],extension(14,bind([[_20921, _21052, _20982], [_29594, 32 ^ [4 ^ [4 ^ [_29594]]], 32 ^ [4 ^ [4 ^ [_29594]]]]]))).
% 29.49/29.40 cnf('1.1.1.1.1.1.1.1',plain,[-(r1(32 ^ [4 ^ [4 ^ [_29594]]])), -(33 ^ [4 ^ [4 ^ [_29594]]])],extension(5,bind([[_21578], [4 ^ [4 ^ [_29594]]]]))).
% 29.49/29.40 cnf('1.1.1.1.1.1.1.1.1',plain,[33 ^ [4 ^ [4 ^ [_29594]]]],reduction('1')).
% 29.49/29.40 cnf('1.1.1.1.1.1.1.2',plain,[-(32 ^ [4 ^ [4 ^ [_29594]]] = 32 ^ [4 ^ [4 ^ [_29594]]])],extension(15,bind([[_9938], [32 ^ [4 ^ [4 ^ [_29594]]]]]))).
% 29.49/29.40 cnf('1.1.1.2',plain,[-(r2(4 ^ [_29594], 31 ^ [4 ^ [4 ^ [_29594]]])), -(6 ^ [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]])],extension(7,bind([[_23100, _14397], [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]]))).
% 29.49/29.40 cnf('1.1.1.2.1',plain,[6 ^ [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]], 5 ^ [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]],extension(11,bind([[_23100, _14397], [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]]))).
% 29.49/29.40 cnf('1.1.1.2.1.1',plain,[-(5 ^ [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]), 31 ^ [4 ^ [4 ^ [_29594]]] = 4 ^ [4 ^ [_29594]]],extension(8,bind([[_23100, _14397], [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]]))).
% 29.49/29.40 cnf('1.1.1.2.1.1.1',plain,[-(31 ^ [4 ^ [4 ^ [_29594]]] = 4 ^ [4 ^ [_29594]]), 4 ^ [4 ^ [_29594]] = 31 ^ [4 ^ [4 ^ [_29594]]]],extension(16,bind([[_10091, _10136], [4 ^ [4 ^ [_29594]], 31 ^ [4 ^ [4 ^ [_29594]]]]]))).
% 29.49/29.40 cnf('1.1.1.2.1.1.1.1',plain,[-(4 ^ [4 ^ [_29594]] = 31 ^ [4 ^ [4 ^ [_29594]]])],reduction('1.1')).
% 29.49/29.40 cnf('1.1.1.3',plain,[-(r2(32 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [4 ^ [_29594]])), r2(32 ^ [4 ^ [4 ^ [_29594]]], 31 ^ [4 ^ [4 ^ [_29594]]]), 32 ^ [4 ^ [4 ^ [_29594]]] = 32 ^ [4 ^ [4 ^ [_29594]]], 31 ^ [4 ^ [4 ^ [_29594]]] = 4 ^ [4 ^ [_29594]]],extension(17,bind([[_11175, _11242, _11308, _11373], [32 ^ [4 ^ [4 ^ [_29594]]], 32 ^ [4 ^ [4 ^ [_29594]]], 31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [4 ^ [_29594]]]]))).
% 29.49/29.40 cnf('1.1.1.3.1',plain,[-(r2(32 ^ [4 ^ [4 ^ [_29594]]], 31 ^ [4 ^ [4 ^ [_29594]]])), -(33 ^ [4 ^ [4 ^ [_29594]]])],extension(4,bind([[_21578], [4 ^ [4 ^ [_29594]]]]))).
% 29.49/29.40 cnf('1.1.1.3.1.1',plain,[33 ^ [4 ^ [4 ^ [_29594]]]],reduction('1')).
% 29.49/29.40 cnf('1.1.1.3.2',plain,[-(32 ^ [4 ^ [4 ^ [_29594]]] = 32 ^ [4 ^ [4 ^ [_29594]]]), r2(32 ^ [4 ^ [4 ^ [_29594]]], 31 ^ [4 ^ [4 ^ [_29594]]]), r2(32 ^ [4 ^ [4 ^ [_29594]]], 31 ^ [4 ^ [4 ^ [_29594]]]), 31 ^ [4 ^ [4 ^ [_29594]]] = 31 ^ [4 ^ [4 ^ [_29594]]]],extension(13,bind([[_18644, _18571, _18801, _18726], [32 ^ [4 ^ [4 ^ [_29594]]], 32 ^ [4 ^ [4 ^ [_29594]]], 31 ^ [4 ^ [4 ^ [_29594]]], 31 ^ [4 ^ [4 ^ [_29594]]]]]))).
% 29.49/29.40 cnf('1.1.1.3.2.1',plain,[-(r2(32 ^ [4 ^ [4 ^ [_29594]]], 31 ^ [4 ^ [4 ^ [_29594]]])), -(33 ^ [4 ^ [4 ^ [_29594]]])],extension(4,bind([[_21578], [4 ^ [4 ^ [_29594]]]]))).
% 29.49/29.40 cnf('1.1.1.3.2.1.1',plain,[33 ^ [4 ^ [4 ^ [_29594]]]],reduction('1')).
% 29.49/29.40 cnf('1.1.1.3.2.2',plain,[-(r2(32 ^ [4 ^ [4 ^ [_29594]]], 31 ^ [4 ^ [4 ^ [_29594]]])), -(33 ^ [4 ^ [4 ^ [_29594]]])],extension(4,bind([[_21578], [4 ^ [4 ^ [_29594]]]]))).
% 29.49/29.40 cnf('1.1.1.3.2.2.1',plain,[33 ^ [4 ^ [4 ^ [_29594]]]],reduction('1')).
% 29.49/29.40 cnf('1.1.1.3.2.3',plain,[-(31 ^ [4 ^ [4 ^ [_29594]]] = 31 ^ [4 ^ [4 ^ [_29594]]]), r2(31 ^ [4 ^ [4 ^ [_29594]]], 15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067]), r2(31 ^ [4 ^ [4 ^ [_29594]]], 15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067]), 15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067] = 15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067]],extension(13,bind([[_18644, _18571, _18801, _18726], [31 ^ [4 ^ [4 ^ [_29594]]], 31 ^ [4 ^ [4 ^ [_29594]]], 15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], 15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067]]]))).
% 29.49/29.40 cnf('1.1.1.3.2.3.1',plain,[-(r2(31 ^ [4 ^ [4 ^ [_29594]]], 15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067]))],extension(12,bind([[_16650, _16565], [31 ^ [4 ^ [4 ^ [_29594]]], _30067]]))).
% 29.49/29.40 cnf('1.1.1.3.2.3.2',plain,[-(r2(31 ^ [4 ^ [4 ^ [_29594]]], 15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067]))],extension(12,bind([[_16650, _16565], [31 ^ [4 ^ [4 ^ [_29594]]], _30067]]))).
% 29.49/29.40 cnf('1.1.1.3.2.3.3',plain,[-(15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067] = 15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067]), r2(15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], 15 ^ [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138]), r2(15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], 15 ^ [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138]), 15 ^ [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138] = 15 ^ [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138]],extension(13,bind([[_18644, _18571, _18801, _18726], [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], 15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], 15 ^ [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138], 15 ^ [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138]]]))).
% 29.49/29.40 cnf('1.1.1.3.2.3.3.1',plain,[-(r2(15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], 15 ^ [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138]))],extension(12,bind([[_16650, _16565], [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138]]))).
% 29.49/29.40 cnf('1.1.1.3.2.3.3.2',plain,[-(r2(15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], 15 ^ [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138]))],extension(12,bind([[_16650, _16565], [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138]]))).
% 29.49/29.40 cnf('1.1.1.3.2.3.3.3',plain,[-(15 ^ [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138] = 15 ^ [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138])],extension(15,bind([[_9938], [15 ^ [15 ^ [31 ^ [4 ^ [4 ^ [_29594]]], _30067], _30138]]]))).
% 29.49/29.40 cnf('1.1.1.3.3',plain,[-(31 ^ [4 ^ [4 ^ [_29594]]] = 4 ^ [4 ^ [_29594]]), -(6 ^ [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]])],extension(6,bind([[_23100, _14397], [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]]))).
% 29.49/29.40 cnf('1.1.1.3.3.1',plain,[6 ^ [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]], 5 ^ [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]],extension(11,bind([[_23100, _14397], [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]]))).
% 29.49/29.40 cnf('1.1.1.3.3.1.1',plain,[-(5 ^ [31 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]), r2(4 ^ [_29594], 31 ^ [4 ^ [4 ^ [_29594]]])],extension(9,bind([[_14397, _23100], [4 ^ [_29594], 31 ^ [4 ^ [4 ^ [_29594]]]]]))).
% 29.49/29.40 cnf('1.1.1.3.3.1.1.1',plain,[-(r2(4 ^ [_29594], 31 ^ [4 ^ [4 ^ [_29594]]]))],lemmata('1.1.1')).
% 29.49/29.40 cnf('1.2',plain,[-(35 ^ [4 ^ [4 ^ [_29594]]]), -(4 ^ [4 ^ [_29594]] = 34 ^ [4 ^ [4 ^ [_29594]]])],extension(1,bind([[_21578], [4 ^ [4 ^ [_29594]]]]))).
% 29.49/29.40 cnf('1.2.1',plain,[4 ^ [4 ^ [_29594]] = 34 ^ [4 ^ [4 ^ [_29594]]], -(34 ^ [4 ^ [4 ^ [_29594]]] = 4 ^ [4 ^ [_29594]])],extension(16,bind([[_10136, _10091], [34 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [4 ^ [_29594]]]]))).
% 29.49/29.40 cnf('1.2.1.1',plain,[34 ^ [4 ^ [4 ^ [_29594]]] = 4 ^ [4 ^ [_29594]], -(5 ^ [34 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]])],extension(8,bind([[_23100, _14397], [34 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]]))).
% 29.49/29.40 cnf('1.2.1.1.1',plain,[5 ^ [34 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]], 6 ^ [34 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]],extension(11,bind([[_23100, _14397], [34 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]]))).
% 29.49/29.40 cnf('1.2.1.1.1.1',plain,[-(6 ^ [34 ^ [4 ^ [4 ^ [_29594]]], 4 ^ [_29594]]), -(r2(4 ^ [_29594], 34 ^ [4 ^ [4 ^ [_29594]]]))],extension(7,bind([[_14397, _23100], [4 ^ [_29594], 34 ^ [4 ^ [4 ^ [_29594]]]]]))).
% 29.49/29.40 cnf('1.2.1.1.1.1.1',plain,[r2(4 ^ [_29594], 34 ^ [4 ^ [4 ^ [_29594]]]), r1(34 ^ [4 ^ [4 ^ [_29594]]]), 34 ^ [4 ^ [4 ^ [_29594]]] = 34 ^ [4 ^ [4 ^ [_29594]]]],extension(14,bind([[_20921, _21052, _20982], [4 ^ [_29594], 34 ^ [4 ^ [4 ^ [_29594]]], 34 ^ [4 ^ [4 ^ [_29594]]]]]))).
% 29.49/29.40 cnf('1.2.1.1.1.1.1.1',plain,[-(r1(34 ^ [4 ^ [4 ^ [_29594]]])), -(35 ^ [4 ^ [4 ^ [_29594]]])],extension(2,bind([[_21578], [4 ^ [4 ^ [_29594]]]]))).
% 29.49/29.40 cnf('1.2.1.1.1.1.1.1.1',plain,[35 ^ [4 ^ [4 ^ [_29594]]]],reduction('1')).
% 29.49/29.40 cnf('1.2.1.1.1.1.1.2',plain,[-(34 ^ [4 ^ [4 ^ [_29594]]] = 34 ^ [4 ^ [4 ^ [_29594]]])],extension(15,bind([[_9938], [34 ^ [4 ^ [4 ^ [_29594]]]]]))).
% 29.49/29.40 %-----------------------------------------------------
% 29.49/29.40
% 29.49/29.41 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------