%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : ALG236-1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 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 : 600s
% DateTime : Thu Jul 14 17:30:04 EDT 2022
% Result : Unsatisfiable 55.83s 14.28s
% Output : CNFRefutation 55.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : ALG236-1 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.11/0.33 % Computer : n025.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Wed Jun 8 15:20:19 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.11/0.33 24900: Facts:
% 0.11/0.34 24900: Id : 2, {_}:
% 0.11/0.34 mult ?2 (mult ?3 (mult ?2 ?3)) =>= mult ?2 ?3
% 0.11/0.34 [3, 2] by c01 ?2 ?3
% 0.11/0.34 24900: Id : 3, {_}:
% 0.11/0.34 mult ?5 (mult ?6 (mult ?7 ?8)) =?= mult ?7 (mult ?6 (mult ?5 ?8))
% 0.11/0.34 [8, 7, 6, 5] by c02 ?5 ?6 ?7 ?8
% 0.11/0.34 24900: Id : 4, {_}:
% 0.11/0.34 mult (mult ?10 (mult ?11 (mult ?12 ?11))) ?13
% 0.11/0.34 =?=
% 0.11/0.34 mult ?10 (mult ?13 (mult (mult ?12 ?11) ?13))
% 0.11/0.34 [13, 12, 11, 10] by c03 ?10 ?11 ?12 ?13
% 0.11/0.34 24900: Goal:
% 0.11/0.34 24900: Id : 1, {_}:
% 0.11/0.34 mult (mult a b) (mult c (mult d e))
% 0.11/0.34 =>=
% 0.11/0.34 mult a (mult c (mult (mult d b) e))
% 0.11/0.34 [] by goals
% 55.83/14.28 Statistics :
% 55.83/14.28 Max weight : 40
% 55.83/14.28 Found proof, 13.949659s
% 55.83/14.28 % SZS status Unsatisfiable for theBenchmark.p
% 55.83/14.28 % SZS output start CNFRefutation for theBenchmark.p
% 55.83/14.28 Id : 4, {_}: mult (mult ?10 (mult ?11 (mult ?12 ?11))) ?13 =?= mult ?10 (mult ?13 (mult (mult ?12 ?11) ?13)) [13, 12, 11, 10] by c03 ?10 ?11 ?12 ?13
% 55.83/14.28 Id : 5, {_}: mult ?15 (mult ?16 (mult ?15 ?16)) =>= mult ?15 ?16 [16, 15] by c01 ?15 ?16
% 55.83/14.28 Id : 2, {_}: mult ?2 (mult ?3 (mult ?2 ?3)) =>= mult ?2 ?3 [3, 2] by c01 ?2 ?3
% 55.83/14.28 Id : 13, {_}: mult ?42 (mult ?43 (mult ?44 ?45)) =?= mult ?44 (mult ?43 (mult ?42 ?45)) [45, 44, 43, 42] by c02 ?42 ?43 ?44 ?45
% 55.83/14.28 Id : 3, {_}: mult ?5 (mult ?6 (mult ?7 ?8)) =?= mult ?7 (mult ?6 (mult ?5 ?8)) [8, 7, 6, 5] by c02 ?5 ?6 ?7 ?8
% 55.83/14.28 Id : 15, {_}: mult ?52 (mult ?53 (mult ?54 (mult ?55 (mult ?56 ?57)))) =?= mult ?54 (mult ?53 (mult ?56 (mult ?55 (mult ?52 ?57)))) [57, 56, 55, 54, 53, 52] by Super 13 with 3 at 2,2,3
% 55.83/14.28 Id : 499, {_}: mult ?1062 (mult ?1063 (mult ?1062 (mult (mult ?1063 ?1064) ?1064))) =>= mult ?1062 (mult ?1063 ?1064) [1064, 1063, 1062] by Super 2 with 3 at 2,2
% 55.83/14.28 Id : 500, {_}: mult ?1066 (mult ?1067 (mult ?1066 (mult (mult ?1067 ?1068) (mult ?1068 (mult ?1067 ?1068))))) =>= mult ?1066 (mult ?1067 (mult ?1068 (mult ?1067 ?1068))) [1068, 1067, 1066] by Super 499 with 2 at 1,2,2,2,2
% 55.83/14.28 Id : 546, {_}: mult ?1066 (mult ?1067 (mult ?1066 (mult ?1067 (mult ?1068 (mult (mult ?1067 ?1068) ?1068))))) =>= mult ?1066 (mult ?1067 (mult ?1068 (mult ?1067 ?1068))) [1068, 1067, 1066] by Demod 500 with 3 at 2,2,2,2
% 55.83/14.28 Id : 547, {_}: mult ?1066 (mult ?1067 (mult ?1066 (mult ?1067 (mult ?1068 (mult (mult ?1067 ?1068) ?1068))))) =>= mult ?1066 (mult ?1067 ?1068) [1068, 1067, 1066] by Demod 546 with 2 at 2,3
% 55.83/14.28 Id : 125, {_}: mult ?497 (mult ?498 (mult ?499 (mult ?498 ?497))) =>= mult ?499 (mult ?498 ?497) [499, 498, 497] by Super 13 with 2 at 2,3
% 55.83/14.28 Id : 132, {_}: mult (mult ?534 ?535) (mult ?535 (mult ?534 ?535)) =>= mult ?534 (mult ?535 (mult ?534 ?535)) [535, 534] by Super 125 with 2 at 2,2,2
% 55.83/14.28 Id : 157, {_}: mult ?534 (mult ?535 (mult (mult ?534 ?535) ?535)) =>= mult ?534 (mult ?535 (mult ?534 ?535)) [535, 534] by Demod 132 with 3 at 2
% 55.83/14.28 Id : 158, {_}: mult ?534 (mult ?535 (mult (mult ?534 ?535) ?535)) =>= mult ?534 ?535 [535, 534] by Demod 157 with 2 at 3
% 55.83/14.28 Id : 762, {_}: mult ?1565 (mult ?1566 (mult ?1565 (mult ?1566 ?1567))) =>= mult ?1565 (mult ?1566 ?1567) [1567, 1566, 1565] by Demod 547 with 158 at 2,2,2,2
% 55.83/14.29 Id : 11, {_}: mult ?34 (mult ?35 (mult ?34 (mult (mult ?35 ?36) ?36))) =>= mult ?34 (mult ?35 ?36) [36, 35, 34] by Super 2 with 3 at 2,2
% 55.83/14.29 Id : 786, {_}: mult ?1676 (mult ?1677 (mult ?1676 ?1678)) =<= mult ?1676 (mult ?1677 (mult (mult ?1676 ?1678) ?1678)) [1678, 1677, 1676] by Super 762 with 11 at 2,2
% 55.83/14.29 Id : 17, {_}: mult ?66 (mult ?67 (mult ?68 (mult ?67 ?66))) =>= mult ?68 (mult ?67 ?66) [68, 67, 66] by Super 13 with 2 at 2,3
% 55.83/14.29 Id : 6, {_}: mult ?18 (mult (mult ?19 (mult ?18 ?19)) (mult ?18 ?19)) =>= mult ?18 (mult ?19 (mult ?18 ?19)) [19, 18] by Super 5 with 2 at 2,2,2
% 55.83/14.29 Id : 8, {_}: mult ?18 (mult (mult ?19 (mult ?18 ?19)) (mult ?18 ?19)) =>= mult ?18 ?19 [19, 18] by Demod 6 with 2 at 3
% 55.83/14.29 Id : 240, {_}: mult ?699 (mult ?700 ?699) =<= mult (mult ?699 (mult ?700 ?699)) (mult ?700 ?699) [700, 699] by Super 17 with 8 at 2,2
% 55.83/14.29 Id : 343, {_}: mult ?873 (mult (mult ?874 (mult ?873 ?874)) (mult ?875 ?874)) =>= mult ?875 (mult ?874 (mult ?873 ?874)) [875, 874, 873] by Super 3 with 240 at 2,3
% 55.83/14.29 Id : 1908, {_}: mult (mult ?4322 ?4323) (mult (mult ?4323 (mult ?4324 ?4323)) (mult ?4322 (mult ?4323 (mult ?4324 ?4323)))) =>= mult ?4324 (mult (mult ?4323 (mult ?4324 ?4323)) (mult ?4322 ?4323)) [4324, 4323, 4322] by Super 17 with 343 at 2,2,2
% 55.83/14.29 Id : 2001, {_}: mult ?4322 (mult (mult ?4323 (mult ?4324 ?4323)) (mult (mult ?4322 ?4323) (mult ?4323 (mult ?4324 ?4323)))) =>= mult ?4324 (mult (mult ?4323 (mult ?4324 ?4323)) (mult ?4322 ?4323)) [4324, 4323, 4322] by Demod 1908 with 3 at 2
% 55.83/14.29 Id : 2002, {_}: mult ?4322 (mult (mult ?4323 (mult ?4324 ?4323)) (mult (mult ?4322 ?4323) (mult ?4323 (mult ?4324 ?4323)))) =>= mult ?4322 (mult ?4323 (mult ?4324 ?4323)) [4324, 4323, 4322] by Demod 2001 with 343 at 3
% 55.83/14.29 Id : 2003, {_}: mult (mult ?4322 (mult ?4323 (mult ?4322 ?4323))) (mult ?4323 (mult ?4324 ?4323)) =>= mult ?4322 (mult ?4323 (mult ?4324 ?4323)) [4324, 4323, 4322] by Demod 2002 with 4 at 2
% 55.83/14.29 Id : 2004, {_}: mult (mult ?4322 ?4323) (mult ?4323 (mult ?4324 ?4323)) =>= mult ?4322 (mult ?4323 (mult ?4324 ?4323)) [4324, 4323, 4322] by Demod 2003 with 2 at 1,2
% 55.83/14.29 Id : 2366, {_}: mult (mult ?4790 ?4791) (mult ?4791 (mult (mult ?4790 ?4791) ?4791)) =>= mult ?4790 (mult ?4791 (mult (mult (mult ?4790 ?4791) ?4791) ?4791)) [4791, 4790] by Super 786 with 2004 at 3
% 55.83/14.29 Id : 2461, {_}: mult (mult ?4790 ?4791) ?4791 =<= mult ?4790 (mult ?4791 (mult (mult (mult ?4790 ?4791) ?4791) ?4791)) [4791, 4790] by Demod 2366 with 2 at 2
% 55.83/14.29 Id : 182, {_}: mult (mult (mult ?630 ?631) ?631) (mult ?631 (mult ?630 ?631)) =>= mult ?630 (mult ?631 (mult (mult ?630 ?631) ?631)) [631, 630] by Super 17 with 158 at 2,2,2
% 55.83/14.29 Id : 198, {_}: mult ?630 (mult ?631 (mult (mult (mult ?630 ?631) ?631) ?631)) =>= mult ?630 (mult ?631 (mult (mult ?630 ?631) ?631)) [631, 630] by Demod 182 with 3 at 2
% 55.83/14.29 Id : 199, {_}: mult ?630 (mult ?631 (mult (mult (mult ?630 ?631) ?631) ?631)) =>= mult ?630 ?631 [631, 630] by Demod 198 with 158 at 3
% 55.83/14.29 Id : 2462, {_}: mult (mult ?4790 ?4791) ?4791 =>= mult ?4790 ?4791 [4791, 4790] by Demod 2461 with 199 at 3
% 55.83/14.29 Id : 2746, {_}: mult (mult ?5135 ?5136) (mult ?5137 (mult ?5138 (mult ?5139 (mult ?5140 ?5136)))) =>= mult ?5138 (mult ?5137 (mult ?5140 (mult ?5139 (mult ?5135 ?5136)))) [5140, 5139, 5138, 5137, 5136, 5135] by Super 15 with 2462 at 2,2,2,2,3
% 55.83/14.29 Id : 768, {_}: mult ?1596 (mult ?1597 (mult ?1596 (mult ?1598 (mult ?1599 ?1597)))) =?= mult ?1596 (mult ?1597 (mult ?1599 (mult ?1598 (mult ?1599 ?1597)))) [1599, 1598, 1597, 1596] by Super 762 with 17 at 2,2,2,2
% 55.83/14.29 Id : 840, {_}: mult ?1596 (mult ?1597 (mult ?1596 (mult ?1598 (mult ?1599 ?1597)))) =>= mult ?1596 (mult ?1598 (mult ?1599 ?1597)) [1599, 1598, 1597, 1596] by Demod 768 with 17 at 2,3
% 55.83/14.29 Id : 599, {_}: mult ?1286 (mult ?1287 (mult ?1288 (mult ?1289 (mult ?1286 ?1289)))) =>= mult ?1288 (mult ?1287 (mult ?1286 ?1289)) [1289, 1288, 1287, 1286] by Super 13 with 2 at 2,2,3
% 55.83/14.29 Id : 3654, {_}: mult ?7992 (mult ?7993 (mult ?7992 (mult ?7994 (mult ?7995 ?7994)))) =>= mult ?7995 (mult ?7993 (mult ?7992 ?7994)) [7995, 7994, 7993, 7992] by Super 599 with 3 at 2,2,2
% 55.83/14.29 Id : 3690, {_}: mult ?8223 (mult ?8224 (mult (mult ?8223 (mult ?8225 (mult ?8226 ?8225))) ?8227)) =>= mult (mult ?8226 ?8225) (mult ?8224 (mult ?8223 ?8227)) [8227, 8226, 8225, 8224, 8223] by Super 3654 with 4 at 2,2,2
% 55.83/14.29 Id : 21056, {_}: mult (mult ?54967 ?54968) (mult ?54969 (mult ?54970 (mult ?54969 ?54970))) =?= mult (mult ?54970 (mult ?54968 (mult ?54967 ?54968))) (mult ?54969 ?54970) [54970, 54969, 54968, 54967] by Super 17 with 3690 at 2
% 55.83/14.29 Id : 22055, {_}: mult (mult ?58079 ?58080) (mult ?58081 ?58082) =<= mult (mult ?58082 (mult ?58080 (mult ?58079 ?58080))) (mult ?58081 ?58082) [58082, 58081, 58080, 58079] by Demod 21056 with 2 at 2,2
% 55.83/14.29 Id : 22985, {_}: mult (mult ?60214 ?60215) (mult ?60216 ?60217) =<= mult (mult ?60214 (mult ?60215 (mult ?60217 ?60215))) (mult ?60216 ?60217) [60217, 60216, 60215, 60214] by Super 22055 with 3 at 1,3
% 55.83/14.29 Id : 23120, {_}: mult (mult ?61175 ?61176) (mult ?61177 ?61178) =<= mult ?61175 (mult (mult ?61177 ?61178) (mult (mult ?61178 ?61176) (mult ?61177 ?61178))) [61178, 61177, 61176, 61175] by Super 22985 with 4 at 3
% 55.83/14.29 Id : 14, {_}: mult ?47 (mult ?48 (mult ?49 (mult ?50 (mult ?47 ?50)))) =>= mult ?49 (mult ?48 (mult ?47 ?50)) [50, 49, 48, 47] by Super 13 with 2 at 2,2,3
% 55.83/14.29 Id : 767, {_}: mult ?1590 (mult ?1591 (mult ?1590 (mult ?1592 (mult ?1593 (mult ?1591 ?1594))))) =?= mult ?1590 (mult ?1591 (mult ?1593 (mult ?1592 (mult ?1594 (mult ?1591 ?1594))))) [1594, 1593, 1592, 1591, 1590] by Super 762 with 14 at 2,2,2,2
% 55.83/14.29 Id : 839, {_}: mult ?1590 (mult ?1591 (mult ?1590 (mult ?1592 (mult ?1593 (mult ?1591 ?1594))))) =>= mult ?1590 (mult ?1592 (mult ?1593 (mult ?1591 ?1594))) [1594, 1593, 1592, 1591, 1590] by Demod 767 with 14 at 2,3
% 55.83/14.29 Id : 764, {_}: mult ?1573 (mult ?1574 (mult ?1573 (mult ?1575 (mult ?1576 (mult ?1574 ?1577))))) =>= mult ?1573 (mult ?1574 (mult ?1576 (mult ?1575 ?1577))) [1577, 1576, 1575, 1574, 1573] by Super 762 with 3 at 2,2,2,2
% 55.83/14.29 Id : 9595, {_}: mult ?1590 (mult ?1591 (mult ?1593 (mult ?1592 ?1594))) =?= mult ?1590 (mult ?1592 (mult ?1593 (mult ?1591 ?1594))) [1594, 1592, 1593, 1591, 1590] by Demod 839 with 764 at 2
% 55.83/14.29 Id : 23663, {_}: mult (mult ?61175 ?61176) (mult ?61177 ?61178) =<= mult ?61175 (mult ?61177 (mult (mult ?61178 ?61176) (mult (mult ?61177 ?61178) ?61178))) [61178, 61177, 61176, 61175] by Demod 23120 with 9595 at 3
% 55.83/14.29 Id : 23664, {_}: mult (mult ?61175 ?61176) (mult ?61177 ?61178) =<= mult ?61175 (mult ?61177 (mult (mult ?61178 ?61176) (mult ?61177 ?61178))) [61178, 61177, 61176, 61175] by Demod 23663 with 2462 at 2,2,2,3
% 55.83/14.29 Id : 25224, {_}: mult ?64534 (mult (mult ?64535 ?64536) (mult (mult ?64534 ?64537) (mult ?64535 ?64536))) =>= mult ?64534 (mult ?64535 (mult (mult ?64536 ?64537) (mult ?64535 ?64536))) [64537, 64536, 64535, 64534] by Super 840 with 23664 at 2,2,2
% 55.83/14.29 Id : 25545, {_}: mult ?64534 (mult ?64535 (mult (mult ?64534 ?64537) (mult (mult ?64535 ?64536) ?64536))) =>= mult ?64534 (mult ?64535 (mult (mult ?64536 ?64537) (mult ?64535 ?64536))) [64536, 64537, 64535, 64534] by Demod 25224 with 9595 at 2
% 55.83/14.29 Id : 25546, {_}: mult ?64534 (mult ?64535 (mult (mult ?64534 ?64537) (mult (mult ?64535 ?64536) ?64536))) =>= mult (mult ?64534 ?64537) (mult ?64535 ?64536) [64536, 64537, 64535, 64534] by Demod 25545 with 23664 at 3
% 55.83/14.29 Id : 25547, {_}: mult ?64534 (mult ?64535 (mult (mult ?64534 ?64537) (mult ?64535 ?64536))) =>= mult (mult ?64534 ?64537) (mult ?64535 ?64536) [64536, 64537, 64535, 64534] by Demod 25546 with 2462 at 2,2,2,2
% 55.83/14.29 Id : 29359, {_}: mult (mult (mult ?76389 ?76390) ?76391) (mult ?76392 (mult ?76393 ?76390)) =<= mult (mult (mult ?76389 ?76390) ?76391) (mult ?76392 (mult ?76393 (mult ?76392 (mult ?76389 ?76390)))) [76393, 76392, 76391, 76390, 76389] by Super 2746 with 25547 at 2
% 55.83/14.29 Id : 25194, {_}: mult (mult ?64365 ?64366) (mult ?64367 (mult ?64368 (mult ?64367 ?64365))) =>= mult (mult ?64368 ?64366) (mult ?64367 ?64365) [64368, 64367, 64366, 64365] by Super 3 with 23664 at 3
% 55.83/14.29 Id : 29884, {_}: mult (mult (mult ?76389 ?76390) ?76391) (mult ?76392 (mult ?76393 ?76390)) =>= mult (mult ?76393 ?76391) (mult ?76392 (mult ?76389 ?76390)) [76393, 76392, 76391, 76390, 76389] by Demod 29359 with 25194 at 3
% 55.83/14.29 Id : 26194, {_}: mult (mult ?67245 ?67246) (mult ?67247 (mult ?67248 (mult ?67247 ?67245))) =>= mult (mult ?67248 ?67246) (mult ?67247 ?67245) [67248, 67247, 67246, 67245] by Super 3 with 23664 at 3
% 55.83/14.29 Id : 2363, {_}: mult ?4776 (mult ?4777 (mult ?4778 (mult ?4779 (mult ?4776 ?4779)))) =>= mult (mult ?4778 ?4779) (mult ?4777 (mult ?4776 ?4779)) [4779, 4778, 4777, 4776] by Super 14 with 2004 at 2,2,2
% 55.83/14.29 Id : 2468, {_}: mult ?4778 (mult ?4777 (mult ?4776 ?4779)) =<= mult (mult ?4778 ?4779) (mult ?4777 (mult ?4776 ?4779)) [4779, 4776, 4777, 4778] by Demod 2363 with 14 at 2
% 55.83/14.29 Id : 26278, {_}: mult (mult (mult ?67840 ?67841) ?67842) (mult ?67843 (mult ?67844 (mult ?67843 (mult ?67840 ?67841)))) =>= mult (mult (mult ?67844 ?67841) ?67842) (mult ?67843 (mult ?67840 ?67841)) [67844, 67843, 67842, 67841, 67840] by Super 26194 with 2468 at 2,2,2
% 55.83/14.29 Id : 26846, {_}: mult (mult ?67844 ?67842) (mult ?67843 (mult ?67840 ?67841)) =<= mult (mult (mult ?67844 ?67841) ?67842) (mult ?67843 (mult ?67840 ?67841)) [67841, 67840, 67843, 67842, 67844] by Demod 26278 with 25194 at 2
% 55.83/14.29 Id : 37404, {_}: mult (mult ?76389 ?76391) (mult ?76392 (mult ?76393 ?76390)) =?= mult (mult ?76393 ?76391) (mult ?76392 (mult ?76389 ?76390)) [76390, 76393, 76392, 76391, 76389] by Demod 29884 with 26846 at 2
% 55.83/14.29 Id : 37623, {_}: mult ?97720 (mult ?97721 (mult (mult ?97722 ?97723) ?97724)) =<= mult (mult ?97720 ?97723) (mult ?97721 (mult ?97722 ?97724)) [97724, 97723, 97722, 97721, 97720] by Super 3 with 37404 at 3
% 55.83/14.29 Id : 38791, {_}: mult ?76389 (mult ?76392 (mult (mult ?76393 ?76391) ?76390)) =?= mult (mult ?76393 ?76391) (mult ?76392 (mult ?76389 ?76390)) [76390, 76391, 76393, 76392, 76389] by Demod 37404 with 37623 at 2
% 55.83/14.29 Id : 38792, {_}: mult ?76389 (mult ?76392 (mult (mult ?76393 ?76391) ?76390)) =?= mult ?76393 (mult ?76392 (mult (mult ?76389 ?76391) ?76390)) [76390, 76391, 76393, 76392, 76389] by Demod 38791 with 37623 at 3
% 55.83/14.29 Id : 40204, {_}: mult a (mult c (mult (mult d b) e)) =?= mult a (mult c (mult (mult d b) e)) [] by Demod 40203 with 38792 at 2
% 55.83/14.29 Id : 40203, {_}: mult d (mult c (mult (mult a b) e)) =>= mult a (mult c (mult (mult d b) e)) [] by Demod 1 with 3 at 2
% 55.83/14.29 Id : 1, {_}: mult (mult a b) (mult c (mult d e)) =>= mult a (mult c (mult (mult d b) e)) [] by goals
% 55.83/14.29 % SZS output end CNFRefutation for theBenchmark.p
% 55.83/14.29 24901: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 13.951758 using kbo
%------------------------------------------------------------------------------